WATCH: 0.00 CPU 0.01 WC ----- Otter 3.3f, August 2004 ----- The process was started by sutcliff on cl5-009, Wed Aug 3 14:21:54 2011 The command was "/CW/home-0/sutcliff/Systems/Otter---3.3/otter". The process ID is 24440. set(prolog_style_variables). set(tptp_eq). set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). clear(print_given). formula_list(usable). all X Y Z (r1(X,Y)&r1(Y,Z)->r1(X,Z)). all X r1(X,X). -(-(exists X (-(-((all Y (-r1(X,Y)| (-(all X (-(-p15(X)& -p115(X)&p114(X))| -r1(Y,X)))& -(all X (-(p15(X)&p114(X)& -p115(X))| -r1(Y,X)))| -(p113(Y)& -p114(Y)))& (-(all X (-(p13(X)& -p113(X)&p112(X))| -r1(Y,X)))& -(all X (-(-p13(X)& -p113(X)&p112(X))| -r1(Y,X)))| -(p111(Y)& -p112(Y)))& (-(-p106(Y)&p105(Y))| -(all X (-(-p107(X)&p106(X)&p7(X))| -r1(Y,X)))& -(all X (-r1(Y,X)| -(-p107(X)&p106(X)& -p7(X)))))& (-(all X (-(-p105(X)&p104(X)& -p5(X))| -r1(Y,X)))& -(all X (-r1(Y,X)| -(p104(X)& -p105(X)&p5(X))))| -(p103(Y)& -p104(Y)))& (-(-p103(Y)&p102(Y))| -(all X (-r1(Y,X)| -(p4(X)& -p104(X)&p103(X))))& -(all X (-(-p4(X)& -p104(X)&p103(X))| -r1(Y,X))))& (-(all X (-(-p3(X)& -p103(X)&p102(X))| -r1(Y,X)))& -(all X (-r1(Y,X)| -(p102(X)& -p103(X)&p3(X))))| -(-p102(Y)&p101(Y)))& (-(all X (-r1(Y,X)| -(-p2(X)&p101(X)& -p102(X))))& -(all X (-(p2(X)&p101(X)& -p102(X))| -r1(Y,X)))| -(p100(Y)& -p101(Y)))& (((all X (-p16(X)| -p115(X)| -r1(Y,X)))|p16(Y))& ((all X (-p115(X)|p16(X)| -r1(Y,X)))| -p16(Y))| -p115(Y))& (-p114(Y)| (p15(Y)| (all X (-r1(Y,X)| -p15(X)| -p114(X))))& (-p15(Y)| (all X (-r1(Y,X)|p15(X)| -p114(X)))))& (-p113(Y)| (p14(Y)| (all X (-p113(X)| -p14(X)| -r1(Y,X))))& (-p14(Y)| (all X (-p113(X)|p14(X)| -r1(Y,X)))))& ((-p13(Y)| (all X (-r1(Y,X)|p13(X)| -p112(X))))& (p13(Y)| (all X (-p112(X)| -p13(X)| -r1(Y,X))))| -p112(Y))& (((all X (-r1(Y,X)| -p100(X)| -p1(X)))|p1(Y))& (-p1(Y)| (all X (-r1(Y,X)|p1(X)| -p100(X))))| -p100(Y))& (p113(Y)| -p114(Y))& (p111(Y)| -p112(Y))& (p110(Y)| -p111(Y))& (p109(Y)| -p110(Y))& (p108(Y)| -p109(Y))& (-p108(Y)|p107(Y))& (p106(Y)| -p107(Y))& (p104(Y)| -p105(Y))& (-p103(Y)|p102(Y))& (p100(Y)| -p101(Y))& (p101(Y)| -p102(Y))& (p103(Y)| -p104(Y))& (p105(Y)| -p106(Y))& (-p113(Y)|p112(Y))& (p114(Y)| -p115(Y))& (p115(Y)| -p116(Y))& ((-p2(Y)| (all X (-p101(X)|p2(X)| -r1(Y,X))))& (p2(Y)| (all X (-r1(Y,X)| -p2(X)| -p101(X))))| -p101(Y))& (((all X (p3(X)| -p102(X)| -r1(Y,X)))| -p3(Y))& ((all X (-p3(X)| -p102(X)| -r1(Y,X)))|p3(Y))| -p102(Y))& (-p103(Y)| (p4(Y)| (all X (-p103(X)| -p4(X)| -r1(Y,X))))& ((all X (-r1(Y,X)|p4(X)| -p103(X)))| -p4(Y)))& (((all X (p5(X)| -p104(X)| -r1(Y,X)))| -p5(Y))& (p5(Y)| (all X (-r1(Y,X)| -p104(X)| -p5(X))))| -p104(Y))& ((-p6(Y)| (all X (-p105(X)|p6(X)| -r1(Y,X))))& ((all X (-p105(X)| -p6(X)| -r1(Y,X)))|p6(Y))| -p105(Y))& (-p106(Y)| ((all X (-r1(Y,X)| -p7(X)| -p106(X)))|p7(Y))& ((all X (-r1(Y,X)| -p106(X)|p7(X)))| -p7(Y)))& ((p8(Y)| (all X (-p8(X)| -p107(X)| -r1(Y,X))))& (-p8(Y)| (all X (-r1(Y,X)| -p107(X)|p8(X))))| -p107(Y))& (-p108(Y)| (-p9(Y)| (all X (-p108(X)|p9(X)| -r1(Y,X))))& ((all X (-r1(Y,X)| -p108(X)| -p9(X)))|p9(Y)))& ((p10(Y)| (all X (-p109(X)| -p10(X)| -r1(Y,X))))& (-p10(Y)| (all X (-r1(Y,X)| -p109(X)|p10(X))))| -p109(Y))& (-p110(Y)| ((all X (-r1(Y,X)|p11(X)| -p110(X)))| -p11(Y))& (p11(Y)| (all X (-p11(X)| -p110(X)| -r1(Y,X)))))& (-p111(Y)| (p12(Y)| (all X (-p12(X)| -p111(X)| -r1(Y,X))))& (-p12(Y)| (all X (p12(X)| -p111(X)| -r1(Y,X)))))& (-(all X (-(-p6(X)&p105(X)& -p106(X))| -r1(Y,X)))& -(all X (-r1(Y,X)| -(p6(X)&p105(X)& -p106(X))))| -(-p105(Y)&p104(Y)))& (-(all X (-r1(Y,X)| -(-p8(X)& -p108(X)&p107(X))))& -(all X (-r1(Y,X)| -(p8(X)& -p108(X)&p107(X))))| -(-p107(Y)&p106(Y)))& (-(p107(Y)& -p108(Y))| -(all X (-r1(Y,X)| -(-p109(X)&p108(X)&p9(X))))& -(all X (-(p108(X)& -p109(X)& -p9(X))| -r1(Y,X))))& (-(all X (-(p109(X)& -p110(X)& -p10(X))| -r1(Y,X)))& -(all X (-(p109(X)& -p110(X)&p10(X))| -r1(Y,X)))| -(-p109(Y)&p108(Y)))& (-(all X (-(p11(X)& -p111(X)&p110(X))| -r1(Y,X)))& -(all X (-r1(Y,X)| -(-p111(X)&p110(X)& -p11(X))))| -(-p110(Y)&p109(Y)))& (-(p110(Y)& -p111(Y))| -(all X (-(-p112(X)&p111(X)&p12(X))| -r1(Y,X)))& -(all X (-(-p112(X)&p111(X)& -p12(X))| -r1(Y,X))))& (-(-p113(Y)&p112(Y))| -(all X (-r1(Y,X)| -(p113(X)& -p114(X)&p14(X))))& -(all X (-(p113(X)& -p114(X)& -p14(X))| -r1(Y,X))))& (-(all X (-(-p116(X)&p115(X)& -p16(X))| -r1(Y,X)))& -(all X (-r1(Y,X)| -(-p116(X)&p115(X)&p16(X))))| -(-p115(Y)&p114(Y)))))&p100(X)& -p101(X))| -(all Y (-r1(X,Y)|p7(Y))))))). end_of_list. -------> usable clausifies to: list(usable). 0 [] -r1(X,Y)| -r1(Y,Z)|r1(X,Z). 0 [] r1(X,X). 0 [] -r1($c1,Y)| -p15($f1(Y))| -p113(Y)|p114(Y). 0 [] -r1($c1,Y)| -p115($f1(Y))| -p113(Y)|p114(Y). 0 [] -r1($c1,Y)|p114($f1(Y))| -p113(Y)|p114(Y). 0 [] -r1($c1,Y)|r1(Y,$f1(Y))| -p113(Y)|p114(Y). 0 [] -r1($c1,Y)|p15($f2(Y))| -p113(Y)|p114(Y). 0 [] -r1($c1,Y)|p114($f2(Y))| -p113(Y)|p114(Y). 0 [] -r1($c1,Y)| -p115($f2(Y))| -p113(Y)|p114(Y). 0 [] -r1($c1,Y)|r1(Y,$f2(Y))| -p113(Y)|p114(Y). 0 [] -r1($c1,Y)|p13($f3(Y))| -p111(Y)|p112(Y). 0 [] -r1($c1,Y)| -p113($f3(Y))| -p111(Y)|p112(Y). 0 [] -r1($c1,Y)|p112($f3(Y))| -p111(Y)|p112(Y). 0 [] -r1($c1,Y)|r1(Y,$f3(Y))| -p111(Y)|p112(Y). 0 [] -r1($c1,Y)| -p13($f4(Y))| -p111(Y)|p112(Y). 0 [] -r1($c1,Y)| -p113($f4(Y))| -p111(Y)|p112(Y). 0 [] -r1($c1,Y)|p112($f4(Y))| -p111(Y)|p112(Y). 0 [] -r1($c1,Y)|r1(Y,$f4(Y))| -p111(Y)|p112(Y). 0 [] -r1($c1,Y)|p106(Y)| -p105(Y)| -p107($f5(Y)). 0 [] -r1($c1,Y)|p106(Y)| -p105(Y)|p106($f5(Y)). 0 [] -r1($c1,Y)|p106(Y)| -p105(Y)|p7($f5(Y)). 0 [] -r1($c1,Y)|p106(Y)| -p105(Y)|r1(Y,$f5(Y)). 0 [] -r1($c1,Y)|p106(Y)| -p105(Y)|r1(Y,$f6(Y)). 0 [] -r1($c1,Y)|p106(Y)| -p105(Y)| -p107($f6(Y)). 0 [] -r1($c1,Y)|p106(Y)| -p105(Y)|p106($f6(Y)). 0 [] -r1($c1,Y)|p106(Y)| -p105(Y)| -p7($f6(Y)). 0 [] -r1($c1,Y)| -p105($f7(Y))| -p103(Y)|p104(Y). 0 [] -r1($c1,Y)|p104($f7(Y))| -p103(Y)|p104(Y). 0 [] -r1($c1,Y)| -p5($f7(Y))| -p103(Y)|p104(Y). 0 [] -r1($c1,Y)|r1(Y,$f7(Y))| -p103(Y)|p104(Y). 0 [] -r1($c1,Y)|r1(Y,$f8(Y))| -p103(Y)|p104(Y). 0 [] -r1($c1,Y)|p104($f8(Y))| -p103(Y)|p104(Y). 0 [] -r1($c1,Y)| -p105($f8(Y))| -p103(Y)|p104(Y). 0 [] -r1($c1,Y)|p5($f8(Y))| -p103(Y)|p104(Y). 0 [] -r1($c1,Y)|p103(Y)| -p102(Y)|r1(Y,$f9(Y)). 0 [] -r1($c1,Y)|p103(Y)| -p102(Y)|p4($f9(Y)). 0 [] -r1($c1,Y)|p103(Y)| -p102(Y)| -p104($f9(Y)). 0 [] -r1($c1,Y)|p103(Y)| -p102(Y)|p103($f9(Y)). 0 [] -r1($c1,Y)|p103(Y)| -p102(Y)| -p4($f10(Y)). 0 [] -r1($c1,Y)|p103(Y)| -p102(Y)| -p104($f10(Y)). 0 [] -r1($c1,Y)|p103(Y)| -p102(Y)|p103($f10(Y)). 0 [] -r1($c1,Y)|p103(Y)| -p102(Y)|r1(Y,$f10(Y)). 0 [] -r1($c1,Y)| -p3($f11(Y))|p102(Y)| -p101(Y). 0 [] -r1($c1,Y)| -p103($f11(Y))|p102(Y)| -p101(Y). 0 [] -r1($c1,Y)|p102($f11(Y))|p102(Y)| -p101(Y). 0 [] -r1($c1,Y)|r1(Y,$f11(Y))|p102(Y)| -p101(Y). 0 [] -r1($c1,Y)|r1(Y,$f12(Y))|p102(Y)| -p101(Y). 0 [] -r1($c1,Y)|p102($f12(Y))|p102(Y)| -p101(Y). 0 [] -r1($c1,Y)| -p103($f12(Y))|p102(Y)| -p101(Y). 0 [] -r1($c1,Y)|p3($f12(Y))|p102(Y)| -p101(Y). 0 [] -r1($c1,Y)|r1(Y,$f13(Y))| -p100(Y)|p101(Y). 0 [] -r1($c1,Y)| -p2($f13(Y))| -p100(Y)|p101(Y). 0 [] -r1($c1,Y)|p101($f13(Y))| -p100(Y)|p101(Y). 0 [] -r1($c1,Y)| -p102($f13(Y))| -p100(Y)|p101(Y). 0 [] -r1($c1,Y)|p2($f14(Y))| -p100(Y)|p101(Y). 0 [] -r1($c1,Y)|p101($f14(Y))| -p100(Y)|p101(Y). 0 [] -r1($c1,Y)| -p102($f14(Y))| -p100(Y)|p101(Y). 0 [] -r1($c1,Y)|r1(Y,$f14(Y))| -p100(Y)|p101(Y). 0 [] -r1($c1,Y)| -p16(X)| -p115(X)| -r1(Y,X)|p16(Y)| -p115(Y). 0 [] -r1($c1,Y)| -p115(X1)|p16(X1)| -r1(Y,X1)| -p16(Y)| -p115(Y). 0 [] -r1($c1,Y)| -p114(Y)|p15(Y)| -r1(Y,X2)| -p15(X2)| -p114(X2). 0 [] -r1($c1,Y)| -p114(Y)| -p15(Y)| -r1(Y,X3)|p15(X3)| -p114(X3). 0 [] -r1($c1,Y)| -p113(Y)|p14(Y)| -p113(X4)| -p14(X4)| -r1(Y,X4). 0 [] -r1($c1,Y)| -p113(Y)| -p14(Y)| -p113(X5)|p14(X5)| -r1(Y,X5). 0 [] -r1($c1,Y)| -p13(Y)| -r1(Y,X6)|p13(X6)| -p112(X6)| -p112(Y). 0 [] -r1($c1,Y)|p13(Y)| -p112(X7)| -p13(X7)| -r1(Y,X7)| -p112(Y). 0 [] -r1($c1,Y)| -r1(Y,X8)| -p100(X8)| -p1(X8)|p1(Y)| -p100(Y). 0 [] -r1($c1,Y)| -p1(Y)| -r1(Y,X9)|p1(X9)| -p100(X9)| -p100(Y). 0 [] -r1($c1,Y)|p113(Y)| -p114(Y). 0 [] -r1($c1,Y)|p111(Y)| -p112(Y). 0 [] -r1($c1,Y)|p110(Y)| -p111(Y). 0 [] -r1($c1,Y)|p109(Y)| -p110(Y). 0 [] -r1($c1,Y)|p108(Y)| -p109(Y). 0 [] -r1($c1,Y)| -p108(Y)|p107(Y). 0 [] -r1($c1,Y)|p106(Y)| -p107(Y). 0 [] -r1($c1,Y)|p104(Y)| -p105(Y). 0 [] -r1($c1,Y)| -p103(Y)|p102(Y). 0 [] -r1($c1,Y)|p100(Y)| -p101(Y). 0 [] -r1($c1,Y)|p101(Y)| -p102(Y). 0 [] -r1($c1,Y)|p103(Y)| -p104(Y). 0 [] -r1($c1,Y)|p105(Y)| -p106(Y). 0 [] -r1($c1,Y)| -p113(Y)|p112(Y). 0 [] -r1($c1,Y)|p114(Y)| -p115(Y). 0 [] -r1($c1,Y)|p115(Y)| -p116(Y). 0 [] -r1($c1,Y)| -p2(Y)| -p101(X10)|p2(X10)| -r1(Y,X10)| -p101(Y). 0 [] -r1($c1,Y)|p2(Y)| -r1(Y,X11)| -p2(X11)| -p101(X11)| -p101(Y). 0 [] -r1($c1,Y)|p3(X12)| -p102(X12)| -r1(Y,X12)| -p3(Y)| -p102(Y). 0 [] -r1($c1,Y)| -p3(X13)| -p102(X13)| -r1(Y,X13)|p3(Y)| -p102(Y). 0 [] -r1($c1,Y)| -p103(Y)|p4(Y)| -p103(X14)| -p4(X14)| -r1(Y,X14). 0 [] -r1($c1,Y)| -p103(Y)| -r1(Y,X15)|p4(X15)| -p103(X15)| -p4(Y). 0 [] -r1($c1,Y)|p5(X16)| -p104(X16)| -r1(Y,X16)| -p5(Y)| -p104(Y). 0 [] -r1($c1,Y)|p5(Y)| -r1(Y,X17)| -p104(X17)| -p5(X17)| -p104(Y). 0 [] -r1($c1,Y)| -p6(Y)| -p105(X18)|p6(X18)| -r1(Y,X18)| -p105(Y). 0 [] -r1($c1,Y)| -p105(X19)| -p6(X19)| -r1(Y,X19)|p6(Y)| -p105(Y). 0 [] -r1($c1,Y)| -p106(Y)| -r1(Y,X20)| -p7(X20)| -p106(X20)|p7(Y). 0 [] -r1($c1,Y)| -p106(Y)| -r1(Y,X21)| -p106(X21)|p7(X21)| -p7(Y). 0 [] -r1($c1,Y)|p8(Y)| -p8(X22)| -p107(X22)| -r1(Y,X22)| -p107(Y). 0 [] -r1($c1,Y)| -p8(Y)| -r1(Y,X23)| -p107(X23)|p8(X23)| -p107(Y). 0 [] -r1($c1,Y)| -p108(Y)| -p9(Y)| -p108(X24)|p9(X24)| -r1(Y,X24). 0 [] -r1($c1,Y)| -p108(Y)| -r1(Y,X25)| -p108(X25)| -p9(X25)|p9(Y). 0 [] -r1($c1,Y)|p10(Y)| -p109(X26)| -p10(X26)| -r1(Y,X26)| -p109(Y). 0 [] -r1($c1,Y)| -p10(Y)| -r1(Y,X27)| -p109(X27)|p10(X27)| -p109(Y). 0 [] -r1($c1,Y)| -p110(Y)| -r1(Y,X28)|p11(X28)| -p110(X28)| -p11(Y). 0 [] -r1($c1,Y)| -p110(Y)|p11(Y)| -p11(X29)| -p110(X29)| -r1(Y,X29). 0 [] -r1($c1,Y)| -p111(Y)|p12(Y)| -p12(X30)| -p111(X30)| -r1(Y,X30). 0 [] -r1($c1,Y)| -p111(Y)| -p12(Y)|p12(X31)| -p111(X31)| -r1(Y,X31). 0 [] -r1($c1,Y)| -p6($f15(Y))|p105(Y)| -p104(Y). 0 [] -r1($c1,Y)|p105($f15(Y))|p105(Y)| -p104(Y). 0 [] -r1($c1,Y)| -p106($f15(Y))|p105(Y)| -p104(Y). 0 [] -r1($c1,Y)|r1(Y,$f15(Y))|p105(Y)| -p104(Y). 0 [] -r1($c1,Y)|r1(Y,$f16(Y))|p105(Y)| -p104(Y). 0 [] -r1($c1,Y)|p6($f16(Y))|p105(Y)| -p104(Y). 0 [] -r1($c1,Y)|p105($f16(Y))|p105(Y)| -p104(Y). 0 [] -r1($c1,Y)| -p106($f16(Y))|p105(Y)| -p104(Y). 0 [] -r1($c1,Y)|r1(Y,$f17(Y))|p107(Y)| -p106(Y). 0 [] -r1($c1,Y)| -p8($f17(Y))|p107(Y)| -p106(Y). 0 [] -r1($c1,Y)| -p108($f17(Y))|p107(Y)| -p106(Y). 0 [] -r1($c1,Y)|p107($f17(Y))|p107(Y)| -p106(Y). 0 [] -r1($c1,Y)|r1(Y,$f18(Y))|p107(Y)| -p106(Y). 0 [] -r1($c1,Y)|p8($f18(Y))|p107(Y)| -p106(Y). 0 [] -r1($c1,Y)| -p108($f18(Y))|p107(Y)| -p106(Y). 0 [] -r1($c1,Y)|p107($f18(Y))|p107(Y)| -p106(Y). 0 [] -r1($c1,Y)| -p107(Y)|p108(Y)|r1(Y,$f19(Y)). 0 [] -r1($c1,Y)| -p107(Y)|p108(Y)| -p109($f19(Y)). 0 [] -r1($c1,Y)| -p107(Y)|p108(Y)|p108($f19(Y)). 0 [] -r1($c1,Y)| -p107(Y)|p108(Y)|p9($f19(Y)). 0 [] -r1($c1,Y)| -p107(Y)|p108(Y)|p108($f20(Y)). 0 [] -r1($c1,Y)| -p107(Y)|p108(Y)| -p109($f20(Y)). 0 [] -r1($c1,Y)| -p107(Y)|p108(Y)| -p9($f20(Y)). 0 [] -r1($c1,Y)| -p107(Y)|p108(Y)|r1(Y,$f20(Y)). 0 [] -r1($c1,Y)|p109($f21(Y))|p109(Y)| -p108(Y). 0 [] -r1($c1,Y)| -p110($f21(Y))|p109(Y)| -p108(Y). 0 [] -r1($c1,Y)| -p10($f21(Y))|p109(Y)| -p108(Y). 0 [] -r1($c1,Y)|r1(Y,$f21(Y))|p109(Y)| -p108(Y). 0 [] -r1($c1,Y)|p109($f22(Y))|p109(Y)| -p108(Y). 0 [] -r1($c1,Y)| -p110($f22(Y))|p109(Y)| -p108(Y). 0 [] -r1($c1,Y)|p10($f22(Y))|p109(Y)| -p108(Y). 0 [] -r1($c1,Y)|r1(Y,$f22(Y))|p109(Y)| -p108(Y). 0 [] -r1($c1,Y)|p11($f23(Y))|p110(Y)| -p109(Y). 0 [] -r1($c1,Y)| -p111($f23(Y))|p110(Y)| -p109(Y). 0 [] -r1($c1,Y)|p110($f23(Y))|p110(Y)| -p109(Y). 0 [] -r1($c1,Y)|r1(Y,$f23(Y))|p110(Y)| -p109(Y). 0 [] -r1($c1,Y)|r1(Y,$f24(Y))|p110(Y)| -p109(Y). 0 [] -r1($c1,Y)| -p111($f24(Y))|p110(Y)| -p109(Y). 0 [] -r1($c1,Y)|p110($f24(Y))|p110(Y)| -p109(Y). 0 [] -r1($c1,Y)| -p11($f24(Y))|p110(Y)| -p109(Y). 0 [] -r1($c1,Y)| -p110(Y)|p111(Y)| -p112($f25(Y)). 0 [] -r1($c1,Y)| -p110(Y)|p111(Y)|p111($f25(Y)). 0 [] -r1($c1,Y)| -p110(Y)|p111(Y)|p12($f25(Y)). 0 [] -r1($c1,Y)| -p110(Y)|p111(Y)|r1(Y,$f25(Y)). 0 [] -r1($c1,Y)| -p110(Y)|p111(Y)| -p112($f26(Y)). 0 [] -r1($c1,Y)| -p110(Y)|p111(Y)|p111($f26(Y)). 0 [] -r1($c1,Y)| -p110(Y)|p111(Y)| -p12($f26(Y)). 0 [] -r1($c1,Y)| -p110(Y)|p111(Y)|r1(Y,$f26(Y)). 0 [] -r1($c1,Y)|p113(Y)| -p112(Y)|r1(Y,$f27(Y)). 0 [] -r1($c1,Y)|p113(Y)| -p112(Y)|p113($f27(Y)). 0 [] -r1($c1,Y)|p113(Y)| -p112(Y)| -p114($f27(Y)). 0 [] -r1($c1,Y)|p113(Y)| -p112(Y)|p14($f27(Y)). 0 [] -r1($c1,Y)|p113(Y)| -p112(Y)|p113($f28(Y)). 0 [] -r1($c1,Y)|p113(Y)| -p112(Y)| -p114($f28(Y)). 0 [] -r1($c1,Y)|p113(Y)| -p112(Y)| -p14($f28(Y)). 0 [] -r1($c1,Y)|p113(Y)| -p112(Y)|r1(Y,$f28(Y)). 0 [] -r1($c1,Y)| -p116($f29(Y))|p115(Y)| -p114(Y). 0 [] -r1($c1,Y)|p115($f29(Y))|p115(Y)| -p114(Y). 0 [] -r1($c1,Y)| -p16($f29(Y))|p115(Y)| -p114(Y). 0 [] -r1($c1,Y)|r1(Y,$f29(Y))|p115(Y)| -p114(Y). 0 [] -r1($c1,Y)|r1(Y,$f30(Y))|p115(Y)| -p114(Y). 0 [] -r1($c1,Y)| -p116($f30(Y))|p115(Y)| -p114(Y). 0 [] -r1($c1,Y)|p115($f30(Y))|p115(Y)| -p114(Y). 0 [] -r1($c1,Y)|p16($f30(Y))|p115(Y)| -p114(Y). 0 [] p100($c1). 0 [] -p101($c1). 0 [] -r1($c1,X32)|p7(X32). end_of_list. SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=6. This is a non-Horn set without equality. The strategy will be ordered hyper_res, unit deletion, and factoring, with satellites in sos and with nuclei in usable. dependent: set(hyper_res). dependent: set(factor). dependent: set(unit_deletion). ------------> process usable: ** KEPT (pick-wt=9): 1 [] -r1(A,B)| -r1(B,C)|r1(A,C). ** KEPT (pick-wt=10): 2 [] -r1($c1,A)| -p15($f1(A))| -p113(A)|p114(A). ** KEPT (pick-wt=10): 3 [] -r1($c1,A)| -p115($f1(A))| -p113(A)|p114(A). ** KEPT (pick-wt=10): 4 [] -r1($c1,A)|p114($f1(A))| -p113(A)|p114(A). ** KEPT (pick-wt=11): 5 [] -r1($c1,A)|r1(A,$f1(A))| -p113(A)|p114(A). ** KEPT (pick-wt=10): 6 [] -r1($c1,A)|p15($f2(A))| -p113(A)|p114(A). ** KEPT (pick-wt=10): 7 [] -r1($c1,A)|p114($f2(A))| -p113(A)|p114(A). ** KEPT (pick-wt=10): 8 [] -r1($c1,A)| -p115($f2(A))| -p113(A)|p114(A). ** KEPT (pick-wt=11): 9 [] -r1($c1,A)|r1(A,$f2(A))| -p113(A)|p114(A). ** KEPT (pick-wt=10): 10 [] -r1($c1,A)|p13($f3(A))| -p111(A)|p112(A). ** KEPT (pick-wt=10): 11 [] -r1($c1,A)| -p113($f3(A))| -p111(A)|p112(A). ** KEPT (pick-wt=10): 12 [] -r1($c1,A)|p112($f3(A))| -p111(A)|p112(A). ** KEPT (pick-wt=11): 13 [] -r1($c1,A)|r1(A,$f3(A))| -p111(A)|p112(A). ** KEPT (pick-wt=10): 14 [] -r1($c1,A)| -p13($f4(A))| -p111(A)|p112(A). ** KEPT (pick-wt=10): 15 [] -r1($c1,A)| -p113($f4(A))| -p111(A)|p112(A). ** KEPT (pick-wt=10): 16 [] -r1($c1,A)|p112($f4(A))| -p111(A)|p112(A). ** KEPT (pick-wt=11): 17 [] -r1($c1,A)|r1(A,$f4(A))| -p111(A)|p112(A). ** KEPT (pick-wt=10): 18 [] -r1($c1,A)|p106(A)| -p105(A)| -p107($f5(A)). ** KEPT (pick-wt=10): 19 [] -r1($c1,A)|p106(A)| -p105(A)|p106($f5(A)). ** KEPT (pick-wt=10): 20 [] -r1($c1,A)|p106(A)| -p105(A)|p7($f5(A)). ** KEPT (pick-wt=11): 21 [] -r1($c1,A)|p106(A)| -p105(A)|r1(A,$f5(A)). ** KEPT (pick-wt=11): 22 [] -r1($c1,A)|p106(A)| -p105(A)|r1(A,$f6(A)). ** KEPT (pick-wt=10): 23 [] -r1($c1,A)|p106(A)| -p105(A)| -p107($f6(A)). ** KEPT (pick-wt=10): 24 [] -r1($c1,A)|p106(A)| -p105(A)|p106($f6(A)). ** KEPT (pick-wt=10): 25 [] -r1($c1,A)|p106(A)| -p105(A)| -p7($f6(A)). ** KEPT (pick-wt=10): 26 [] -r1($c1,A)| -p105($f7(A))| -p103(A)|p104(A). ** KEPT (pick-wt=10): 27 [] -r1($c1,A)|p104($f7(A))| -p103(A)|p104(A). ** KEPT (pick-wt=10): 28 [] -r1($c1,A)| -p5($f7(A))| -p103(A)|p104(A). ** KEPT (pick-wt=11): 29 [] -r1($c1,A)|r1(A,$f7(A))| -p103(A)|p104(A). ** KEPT (pick-wt=11): 30 [] -r1($c1,A)|r1(A,$f8(A))| -p103(A)|p104(A). ** KEPT (pick-wt=10): 31 [] -r1($c1,A)|p104($f8(A))| -p103(A)|p104(A). ** KEPT (pick-wt=10): 32 [] -r1($c1,A)| -p105($f8(A))| -p103(A)|p104(A). ** KEPT (pick-wt=10): 33 [] -r1($c1,A)|p5($f8(A))| -p103(A)|p104(A). ** KEPT (pick-wt=11): 34 [] -r1($c1,A)|p103(A)| -p102(A)|r1(A,$f9(A)). ** KEPT (pick-wt=10): 35 [] -r1($c1,A)|p103(A)| -p102(A)|p4($f9(A)). ** KEPT (pick-wt=10): 36 [] -r1($c1,A)|p103(A)| -p102(A)| -p104($f9(A)). ** KEPT (pick-wt=10): 37 [] -r1($c1,A)|p103(A)| -p102(A)|p103($f9(A)). ** KEPT (pick-wt=10): 38 [] -r1($c1,A)|p103(A)| -p102(A)| -p4($f10(A)). ** KEPT (pick-wt=10): 39 [] -r1($c1,A)|p103(A)| -p102(A)| -p104($f10(A)). ** KEPT (pick-wt=10): 40 [] -r1($c1,A)|p103(A)| -p102(A)|p103($f10(A)). ** KEPT (pick-wt=11): 41 [] -r1($c1,A)|p103(A)| -p102(A)|r1(A,$f10(A)). ** KEPT (pick-wt=10): 42 [] -r1($c1,A)| -p3($f11(A))|p102(A)| -p101(A). ** KEPT (pick-wt=10): 43 [] -r1($c1,A)| -p103($f11(A))|p102(A)| -p101(A). ** KEPT (pick-wt=10): 44 [] -r1($c1,A)|p102($f11(A))|p102(A)| -p101(A). ** KEPT (pick-wt=11): 45 [] -r1($c1,A)|r1(A,$f11(A))|p102(A)| -p101(A). ** KEPT (pick-wt=11): 46 [] -r1($c1,A)|r1(A,$f12(A))|p102(A)| -p101(A). ** KEPT (pick-wt=10): 47 [] -r1($c1,A)|p102($f12(A))|p102(A)| -p101(A). ** KEPT (pick-wt=10): 48 [] -r1($c1,A)| -p103($f12(A))|p102(A)| -p101(A). ** KEPT (pick-wt=10): 49 [] -r1($c1,A)|p3($f12(A))|p102(A)| -p101(A). ** KEPT (pick-wt=11): 50 [] -r1($c1,A)|r1(A,$f13(A))| -p100(A)|p101(A). ** KEPT (pick-wt=10): 51 [] -r1($c1,A)| -p2($f13(A))| -p100(A)|p101(A). ** KEPT (pick-wt=10): 52 [] -r1($c1,A)|p101($f13(A))| -p100(A)|p101(A). ** KEPT (pick-wt=10): 53 [] -r1($c1,A)| -p102($f13(A))| -p100(A)|p101(A). ** KEPT (pick-wt=10): 54 [] -r1($c1,A)|p2($f14(A))| -p100(A)|p101(A). ** KEPT (pick-wt=10): 55 [] -r1($c1,A)|p101($f14(A))| -p100(A)|p101(A). ** KEPT (pick-wt=10): 56 [] -r1($c1,A)| -p102($f14(A))| -p100(A)|p101(A). ** KEPT (pick-wt=11): 57 [] -r1($c1,A)|r1(A,$f14(A))| -p100(A)|p101(A). ** KEPT (pick-wt=14): 58 [] -r1($c1,A)| -p16(B)| -p115(B)| -r1(A,B)|p16(A)| -p115(A). ** KEPT (pick-wt=14): 59 [] -r1($c1,A)| -p115(B)|p16(B)| -r1(A,B)| -p16(A)| -p115(A). ** KEPT (pick-wt=14): 60 [] -r1($c1,A)| -p114(A)|p15(A)| -r1(A,B)| -p15(B)| -p114(B). ** KEPT (pick-wt=14): 61 [] -r1($c1,A)| -p114(A)| -p15(A)| -r1(A,B)|p15(B)| -p114(B). ** KEPT (pick-wt=14): 62 [] -r1($c1,A)| -p113(A)|p14(A)| -p113(B)| -p14(B)| -r1(A,B). ** KEPT (pick-wt=14): 63 [] -r1($c1,A)| -p113(A)| -p14(A)| -p113(B)|p14(B)| -r1(A,B). ** KEPT (pick-wt=14): 64 [] -r1($c1,A)| -p13(A)| -r1(A,B)|p13(B)| -p112(B)| -p112(A). ** KEPT (pick-wt=14): 65 [] -r1($c1,A)|p13(A)| -p112(B)| -p13(B)| -r1(A,B)| -p112(A). ** KEPT (pick-wt=14): 66 [] -r1($c1,A)| -r1(A,B)| -p100(B)| -p1(B)|p1(A)| -p100(A). ** KEPT (pick-wt=14): 67 [] -r1($c1,A)| -p1(A)| -r1(A,B)|p1(B)| -p100(B)| -p100(A). ** KEPT (pick-wt=7): 68 [] -r1($c1,A)|p113(A)| -p114(A). ** KEPT (pick-wt=7): 69 [] -r1($c1,A)|p111(A)| -p112(A). ** KEPT (pick-wt=7): 70 [] -r1($c1,A)|p110(A)| -p111(A). ** KEPT (pick-wt=7): 71 [] -r1($c1,A)|p109(A)| -p110(A). ** KEPT (pick-wt=7): 72 [] -r1($c1,A)|p108(A)| -p109(A). ** KEPT (pick-wt=7): 73 [] -r1($c1,A)| -p108(A)|p107(A). ** KEPT (pick-wt=7): 74 [] -r1($c1,A)|p106(A)| -p107(A). ** KEPT (pick-wt=7): 75 [] -r1($c1,A)|p104(A)| -p105(A). ** KEPT (pick-wt=7): 76 [] -r1($c1,A)| -p103(A)|p102(A). ** KEPT (pick-wt=7): 77 [] -r1($c1,A)|p100(A)| -p101(A). ** KEPT (pick-wt=7): 78 [] -r1($c1,A)|p101(A)| -p102(A). ** KEPT (pick-wt=7): 79 [] -r1($c1,A)|p103(A)| -p104(A). ** KEPT (pick-wt=7): 80 [] -r1($c1,A)|p105(A)| -p106(A). ** KEPT (pick-wt=7): 81 [] -r1($c1,A)| -p113(A)|p112(A). ** KEPT (pick-wt=7): 82 [] -r1($c1,A)|p114(A)| -p115(A). ** KEPT (pick-wt=7): 83 [] -r1($c1,A)|p115(A)| -p116(A). ** KEPT (pick-wt=14): 84 [] -r1($c1,A)| -p2(A)| -p101(B)|p2(B)| -r1(A,B)| -p101(A). ** KEPT (pick-wt=14): 85 [] -r1($c1,A)|p2(A)| -r1(A,B)| -p2(B)| -p101(B)| -p101(A). ** KEPT (pick-wt=14): 86 [] -r1($c1,A)|p3(B)| -p102(B)| -r1(A,B)| -p3(A)| -p102(A). ** KEPT (pick-wt=14): 87 [] -r1($c1,A)| -p3(B)| -p102(B)| -r1(A,B)|p3(A)| -p102(A). ** KEPT (pick-wt=14): 88 [] -r1($c1,A)| -p103(A)|p4(A)| -p103(B)| -p4(B)| -r1(A,B). ** KEPT (pick-wt=14): 89 [] -r1($c1,A)| -p103(A)| -r1(A,B)|p4(B)| -p103(B)| -p4(A). ** KEPT (pick-wt=14): 90 [] -r1($c1,A)|p5(B)| -p104(B)| -r1(A,B)| -p5(A)| -p104(A). ** KEPT (pick-wt=14): 91 [] -r1($c1,A)|p5(A)| -r1(A,B)| -p104(B)| -p5(B)| -p104(A). ** KEPT (pick-wt=14): 92 [] -r1($c1,A)| -p6(A)| -p105(B)|p6(B)| -r1(A,B)| -p105(A). ** KEPT (pick-wt=14): 93 [] -r1($c1,A)| -p105(B)| -p6(B)| -r1(A,B)|p6(A)| -p105(A). ** KEPT (pick-wt=14): 94 [] -r1($c1,A)| -p106(A)| -r1(A,B)| -p7(B)| -p106(B)|p7(A). ** KEPT (pick-wt=14): 95 [] -r1($c1,A)| -p106(A)| -r1(A,B)| -p106(B)|p7(B)| -p7(A). ** KEPT (pick-wt=14): 96 [] -r1($c1,A)|p8(A)| -p8(B)| -p107(B)| -r1(A,B)| -p107(A). ** KEPT (pick-wt=14): 97 [] -r1($c1,A)| -p8(A)| -r1(A,B)| -p107(B)|p8(B)| -p107(A). ** KEPT (pick-wt=14): 98 [] -r1($c1,A)| -p108(A)| -p9(A)| -p108(B)|p9(B)| -r1(A,B). ** KEPT (pick-wt=14): 99 [] -r1($c1,A)| -p108(A)| -r1(A,B)| -p108(B)| -p9(B)|p9(A). ** KEPT (pick-wt=14): 100 [] -r1($c1,A)|p10(A)| -p109(B)| -p10(B)| -r1(A,B)| -p109(A). ** KEPT (pick-wt=14): 101 [] -r1($c1,A)| -p10(A)| -r1(A,B)| -p109(B)|p10(B)| -p109(A). ** KEPT (pick-wt=14): 102 [] -r1($c1,A)| -p110(A)| -r1(A,B)|p11(B)| -p110(B)| -p11(A). ** KEPT (pick-wt=14): 103 [] -r1($c1,A)| -p110(A)|p11(A)| -p11(B)| -p110(B)| -r1(A,B). ** KEPT (pick-wt=14): 104 [] -r1($c1,A)| -p111(A)|p12(A)| -p12(B)| -p111(B)| -r1(A,B). ** KEPT (pick-wt=14): 105 [] -r1($c1,A)| -p111(A)| -p12(A)|p12(B)| -p111(B)| -r1(A,B). ** KEPT (pick-wt=10): 106 [] -r1($c1,A)| -p6($f15(A))|p105(A)| -p104(A). ** KEPT (pick-wt=10): 107 [] -r1($c1,A)|p105($f15(A))|p105(A)| -p104(A). ** KEPT (pick-wt=10): 108 [] -r1($c1,A)| -p106($f15(A))|p105(A)| -p104(A). ** KEPT (pick-wt=11): 109 [] -r1($c1,A)|r1(A,$f15(A))|p105(A)| -p104(A). ** KEPT (pick-wt=11): 110 [] -r1($c1,A)|r1(A,$f16(A))|p105(A)| -p104(A). ** KEPT (pick-wt=10): 111 [] -r1($c1,A)|p6($f16(A))|p105(A)| -p104(A). ** KEPT (pick-wt=10): 112 [] -r1($c1,A)|p105($f16(A))|p105(A)| -p104(A). ** KEPT (pick-wt=10): 113 [] -r1($c1,A)| -p106($f16(A))|p105(A)| -p104(A). ** KEPT (pick-wt=11): 114 [] -r1($c1,A)|r1(A,$f17(A))|p107(A)| -p106(A). ** KEPT (pick-wt=10): 115 [] -r1($c1,A)| -p8($f17(A))|p107(A)| -p106(A). ** KEPT (pick-wt=10): 116 [] -r1($c1,A)| -p108($f17(A))|p107(A)| -p106(A). ** KEPT (pick-wt=10): 117 [] -r1($c1,A)|p107($f17(A))|p107(A)| -p106(A). ** KEPT (pick-wt=11): 118 [] -r1($c1,A)|r1(A,$f18(A))|p107(A)| -p106(A). ** KEPT (pick-wt=10): 119 [] -r1($c1,A)|p8($f18(A))|p107(A)| -p106(A). ** KEPT (pick-wt=10): 120 [] -r1($c1,A)| -p108($f18(A))|p107(A)| -p106(A). ** KEPT (pick-wt=10): 121 [] -r1($c1,A)|p107($f18(A))|p107(A)| -p106(A). ** KEPT (pick-wt=11): 122 [] -r1($c1,A)| -p107(A)|p108(A)|r1(A,$f19(A)). ** KEPT (pick-wt=10): 123 [] -r1($c1,A)| -p107(A)|p108(A)| -p109($f19(A)). ** KEPT (pick-wt=10): 124 [] -r1($c1,A)| -p107(A)|p108(A)|p108($f19(A)). ** KEPT (pick-wt=10): 125 [] -r1($c1,A)| -p107(A)|p108(A)|p9($f19(A)). ** KEPT (pick-wt=10): 126 [] -r1($c1,A)| -p107(A)|p108(A)|p108($f20(A)). ** KEPT (pick-wt=10): 127 [] -r1($c1,A)| -p107(A)|p108(A)| -p109($f20(A)). ** KEPT (pick-wt=10): 128 [] -r1($c1,A)| -p107(A)|p108(A)| -p9($f20(A)). ** KEPT (pick-wt=11): 129 [] -r1($c1,A)| -p107(A)|p108(A)|r1(A,$f20(A)). ** KEPT (pick-wt=10): 130 [] -r1($c1,A)|p109($f21(A))|p109(A)| -p108(A). ** KEPT (pick-wt=10): 131 [] -r1($c1,A)| -p110($f21(A))|p109(A)| -p108(A). ** KEPT (pick-wt=10): 132 [] -r1($c1,A)| -p10($f21(A))|p109(A)| -p108(A). ** KEPT (pick-wt=11): 133 [] -r1($c1,A)|r1(A,$f21(A))|p109(A)| -p108(A). ** KEPT (pick-wt=10): 134 [] -r1($c1,A)|p109($f22(A))|p109(A)| -p108(A). ** KEPT (pick-wt=10): 135 [] -r1($c1,A)| -p110($f22(A))|p109(A)| -p108(A). ** KEPT (pick-wt=10): 136 [] -r1($c1,A)|p10($f22(A))|p109(A)| -p108(A). ** KEPT (pick-wt=11): 137 [] -r1($c1,A)|r1(A,$f22(A))|p109(A)| -p108(A). ** KEPT (pick-wt=10): 138 [] -r1($c1,A)|p11($f23(A))|p110(A)| -p109(A). ** KEPT (pick-wt=10): 139 [] -r1($c1,A)| -p111($f23(A))|p110(A)| -p109(A). ** KEPT (pick-wt=10): 140 [] -r1($c1,A)|p110($f23(A))|p110(A)| -p109(A). ** KEPT (pick-wt=11): 141 [] -r1($c1,A)|r1(A,$f23(A))|p110(A)| -p109(A). ** KEPT (pick-wt=11): 142 [] -r1($c1,A)|r1(A,$f24(A))|p110(A)| -p109(A). ** KEPT (pick-wt=10): 143 [] -r1($c1,A)| -p111($f24(A))|p110(A)| -p109(A). ** KEPT (pick-wt=10): 144 [] -r1($c1,A)|p110($f24(A))|p110(A)| -p109(A). ** KEPT (pick-wt=10): 145 [] -r1($c1,A)| -p11($f24(A))|p110(A)| -p109(A). ** KEPT (pick-wt=10): 146 [] -r1($c1,A)| -p110(A)|p111(A)| -p112($f25(A)). ** KEPT (pick-wt=10): 147 [] -r1($c1,A)| -p110(A)|p111(A)|p111($f25(A)). ** KEPT (pick-wt=10): 148 [] -r1($c1,A)| -p110(A)|p111(A)|p12($f25(A)). ** KEPT (pick-wt=11): 149 [] -r1($c1,A)| -p110(A)|p111(A)|r1(A,$f25(A)). ** KEPT (pick-wt=10): 150 [] -r1($c1,A)| -p110(A)|p111(A)| -p112($f26(A)). ** KEPT (pick-wt=10): 151 [] -r1($c1,A)| -p110(A)|p111(A)|p111($f26(A)). ** KEPT (pick-wt=10): 152 [] -r1($c1,A)| -p110(A)|p111(A)| -p12($f26(A)). ** KEPT (pick-wt=11): 153 [] -r1($c1,A)| -p110(A)|p111(A)|r1(A,$f26(A)). ** KEPT (pick-wt=11): 154 [] -r1($c1,A)|p113(A)| -p112(A)|r1(A,$f27(A)). ** KEPT (pick-wt=10): 155 [] -r1($c1,A)|p113(A)| -p112(A)|p113($f27(A)). ** KEPT (pick-wt=10): 156 [] -r1($c1,A)|p113(A)| -p112(A)| -p114($f27(A)). ** KEPT (pick-wt=10): 157 [] -r1($c1,A)|p113(A)| -p112(A)|p14($f27(A)). ** KEPT (pick-wt=10): 158 [] -r1($c1,A)|p113(A)| -p112(A)|p113($f28(A)). ** KEPT (pick-wt=10): 159 [] -r1($c1,A)|p113(A)| -p112(A)| -p114($f28(A)). ** KEPT (pick-wt=10): 160 [] -r1($c1,A)|p113(A)| -p112(A)| -p14($f28(A)). ** KEPT (pick-wt=11): 161 [] -r1($c1,A)|p113(A)| -p112(A)|r1(A,$f28(A)). ** KEPT (pick-wt=10): 162 [] -r1($c1,A)| -p116($f29(A))|p115(A)| -p114(A). ** KEPT (pick-wt=10): 163 [] -r1($c1,A)|p115($f29(A))|p115(A)| -p114(A). ** KEPT (pick-wt=10): 164 [] -r1($c1,A)| -p16($f29(A))|p115(A)| -p114(A). ** KEPT (pick-wt=11): 165 [] -r1($c1,A)|r1(A,$f29(A))|p115(A)| -p114(A). ** KEPT (pick-wt=11): 166 [] -r1($c1,A)|r1(A,$f30(A))|p115(A)| -p114(A). ** KEPT (pick-wt=10): 167 [] -r1($c1,A)| -p116($f30(A))|p115(A)| -p114(A). ** KEPT (pick-wt=10): 168 [] -r1($c1,A)|p115($f30(A))|p115(A)| -p114(A). ** KEPT (pick-wt=10): 169 [] -r1($c1,A)|p16($f30(A))|p115(A)| -p114(A). ** KEPT (pick-wt=2): 170 [] -p101($c1). ** KEPT (pick-wt=5): 171 [] -r1($c1,A)|p7(A). 171 back subsumes 94. ------------> process sos: ** KEPT (pick-wt=3): 172 [] r1(A,A). ** KEPT (pick-wt=2): 173 [] p100($c1). ======= end of input processing ======= =========== start of search ===========  Resetting weight limit to 15. Resetting weight limit to 15. sos_size=408 Search stopped because sos empty. Search stopped because sos empty. ============ end of search ============ -------------- statistics ------------- clauses given 981 clauses generated 11575 clauses kept 1340 clauses forward subsumed 1760 clauses back subsumed 335 Kbytes malloced 6835 ----------- times (seconds) ----------- user CPU time 0.59 (0 hr, 0 min, 0 sec) system CPU time 0.01 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) Process 24440 finished Wed Aug 3 14:21:55 2011 Otter interrupted PROOF NOT FOUND WATCH: 0.82 CPU 0.94 WC FINAL WATCH: 0.82 CPU 0.94 WC