%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWW102+1 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jul 27 13:22:01 EDT 2022 % Result : Unknown 10.07s 10.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SWW102+1 : TPTP v8.1.0. Released v5.2.0. % 0.07/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n006.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jul 27 02:57:01 EDT 2022 % 0.12/0.33 % CPUTime : % 2.16/2.36 ----- Otter 3.3f, August 2004 ----- % 2.16/2.36 The process was started by sandbox on n006.cluster.edu, % 2.16/2.36 Wed Jul 27 02:57:02 2022 % 2.16/2.36 The command was "./otter". The process ID is 29835. % 2.16/2.36 % 2.16/2.36 set(prolog_style_variables). % 2.16/2.36 set(auto). % 2.16/2.36 dependent: set(auto1). % 2.16/2.36 dependent: set(process_input). % 2.16/2.36 dependent: clear(print_kept). % 2.16/2.36 dependent: clear(print_new_demod). % 2.16/2.36 dependent: clear(print_back_demod). % 2.16/2.36 dependent: clear(print_back_sub). % 2.16/2.36 dependent: set(control_memory). % 2.16/2.36 dependent: assign(max_mem, 12000). % 2.16/2.36 dependent: assign(pick_given_ratio, 4). % 2.16/2.36 dependent: assign(stats_level, 1). % 2.16/2.36 dependent: assign(max_seconds, 10800). % 2.16/2.36 clear(print_given). % 2.16/2.36 % 2.16/2.36 formula_list(usable). % 2.16/2.36 all A (A=A). % 2.16/2.36 all X (bool(X)<->X=false|X=true). % 2.16/2.36 true!=false. % 2.16/2.36 true!=err. % 2.16/2.36 false!=err. % 2.16/2.36 d(true). % 2.16/2.36 d(false). % 2.16/2.36 d(err). % 2.16/2.36 all X Y (forallprefers(X,Y)<-> -d(X)&d(Y)|d(X)&d(Y)& -bool(X)&bool(Y)|X=false&Y=true). % 2.16/2.36 all X Y (existsprefers(X,Y)<-> -d(X)&d(Y)|d(X)&d(Y)& -bool(X)&bool(Y)|X=true&Y=false). % 2.16/2.36 all X (d(X)&phi(X)=X| -d(X)&phi(X)=err). % 2.16/2.36 all X (prop(X)=true<->bool(X)). % 2.16/2.36 all X (prop(X)=false<-> -bool(X)). % 2.16/2.36 all A B (-bool(A)->impl(A,B)=phi(A)). % 2.16/2.36 all A B (bool(A)& -bool(B)->impl(A,B)=phi(B)). % 2.16/2.36 all B (bool(B)->impl(false,B)=true). % 2.16/2.36 all B (bool(B)->impl(true,B)=B). % 2.16/2.36 all A B (-bool(A)->lazy_impl(A,B)=phi(A)). % 2.16/2.36 all B (lazy_impl(false,B)=true). % 2.16/2.36 all B (lazy_impl(true,B)=phi(B)). % 2.16/2.36 all A B (-bool(A)->and1(A,B)=phi(A)). % 2.16/2.36 all A B (bool(A)& -bool(B)->and1(A,B)=phi(B)). % 2.16/2.36 all B (bool(B)->and1(false,B)=false). % 2.16/2.36 all B (bool(B)->and1(true,B)=B). % 2.16/2.36 all P Q R (f1(P,Q,R)=lazy_impl(prop(R),impl(impl(P,impl(Q,R)),R))). % 2.16/2.36 all P Q exists R (and2(P,Q)=phi(f1(P,Q,R))& -(exists R1 forallprefers(f1(P,Q,R1),f1(P,Q,R)))). % 2.16/2.36 all A B (-bool(A)->lazy_and1(A,B)=phi(A)). % 2.16/2.36 all B (lazy_and1(false,B)=false). % 2.16/2.36 all B (lazy_and1(true,B)=phi(B)). % 2.16/2.36 all P Q R (f2(P,Q,R)=lazy_impl(prop(R),impl(lazy_impl(P,impl(Q,R)),R))). % 2.16/2.36 all P Q exists R (lazy_and2(P,Q)=phi(f2(P,Q,R))& -(exists R1 forallprefers(f2(P,Q,R1),f2(P,Q,R)))). % 2.16/2.36 all A B (-bool(A)->or1(A,B)=phi(A)). % 2.16/2.36 all A B (bool(A)& -bool(B)->or1(A,B)=phi(B)). % 2.16/2.36 all B (bool(B)->or1(true,B)=true). % 2.16/2.36 all B (bool(B)->or1(false,B)=B). % 2.16/2.36 all P Q R (f3(P,Q,R)=lazy_impl(prop(R),impl(impl(P,R),impl(impl(Q,R),R)))). % 2.16/2.36 all P Q exists R (or2(P,Q)=phi(f3(P,Q,R))& -(exists R1 forallprefers(f3(P,Q,R1),f3(P,Q,R)))). % 2.16/2.36 all P exists X (exists1(P)=phi(apply(P,X))& -(exists X1 existsprefers(apply(P,X1),apply(P,X)))). % 2.16/2.36 all P X R (f4(P,X,R)=impl(apply(P,X),R)). % 2.16/2.36 all P R exists X (f5(P,R)=phi(f4(P,X,R))& -(exists X1 forallprefers(f4(P,X1,R),f4(P,X,R)))). % 2.16/2.36 all P R (f6(P,R)=lazy_impl(prop(R),impl(f5(P,R),R))). % 2.16/2.36 all P exists R (exists2(P)=phi(f6(P,R))& -(exists R1 forallprefers(f6(P,R1),f6(P,R)))). % 2.16/2.36 false1=false. % 2.16/2.36 all P (f7(P)=lazy_impl(prop(P),P)). % 2.16/2.36 exists P (false2=phi(f7(P))& -(exists P1 forallprefers(f7(P1),f7(P)))). % 2.16/2.36 all A (-bool(A)->not1(A)=phi(A)). % 2.16/2.36 not1(false)=true. % 2.16/2.36 not1(true)=false. % 2.16/2.36 all P (not2(P)=impl(P,false2)). % 2.16/2.36 -(all P (not1(P)=not2(P))). % 2.16/2.36 end_of_list. % 2.16/2.36 % 2.16/2.36 -------> usable clausifies to: % 2.16/2.36 % 2.16/2.36 list(usable). % 2.16/2.36 0 [] A=A. % 2.16/2.36 0 [] -bool(X)|X=false|X=true. % 2.16/2.36 0 [] bool(X)|X!=false. % 2.16/2.36 0 [] bool(X)|X!=true. % 2.16/2.36 0 [] true!=false. % 2.16/2.36 0 [] true!=err. % 2.16/2.36 0 [] false!=err. % 2.16/2.36 0 [] d(true). % 2.16/2.36 0 [] d(false). % 2.16/2.36 0 [] d(err). % 2.16/2.36 0 [] -forallprefers(X,Y)| -d(X)| -bool(X)|X=false. % 2.16/2.36 0 [] -forallprefers(X,Y)| -d(X)| -bool(X)|Y=true. % 2.16/2.36 0 [] -forallprefers(X,Y)| -d(X)|bool(Y)|X=false. % 2.16/2.36 0 [] -forallprefers(X,Y)| -d(X)|bool(Y)|Y=true. % 2.16/2.36 0 [] -forallprefers(X,Y)|d(Y)|X=false. % 2.16/2.36 0 [] -forallprefers(X,Y)|d(Y)|Y=true. % 2.16/2.36 0 [] forallprefers(X,Y)|d(X)| -d(Y). % 2.16/2.36 0 [] forallprefers(X,Y)| -d(X)| -d(Y)|bool(X)| -bool(Y). % 2.16/2.36 0 [] forallprefers(X,Y)|X!=false|Y!=true. % 2.16/2.36 0 [] -existsprefers(X,Y)| -d(X)| -bool(X)|X=true. % 2.16/2.36 0 [] -existsprefers(X,Y)| -d(X)| -bool(X)|Y=false. % 2.16/2.36 0 [] -existsprefers(X,Y)| -d(X)|bool(Y)|X=true. % 2.16/2.36 0 [] -existsprefers(X,Y)| -d(X)|bool(Y)|Y=false. % 2.16/2.36 0 [] -existsprefers(X,Y)|d(Y)|X=true. % 2.16/2.36 0 [] -existsprefers(X,Y)|d(Y)|Y=false. % 2.16/2.36 0 [] existsprefers(X,Y)|d(X)| -d(Y). % 2.16/2.36 0 [] existsprefers(X,Y)| -d(X)| -d(Y)|bool(X)| -bool(Y). % 2.16/2.36 0 [] existsprefers(X,Y)|X!=true|Y!=false. % 2.16/2.36 0 [] d(X)|phi(X)=err. % 2.16/2.36 0 [] phi(X)=X| -d(X). % 2.16/2.36 0 [] phi(X)=X|phi(X)=err. % 2.16/2.36 0 [] prop(X)!=true|bool(X). % 2.16/2.36 0 [] prop(X)=true| -bool(X). % 2.16/2.36 0 [] prop(X)!=false| -bool(X). % 2.16/2.36 0 [] prop(X)=false|bool(X). % 2.16/2.36 0 [] bool(A)|impl(A,B)=phi(A). % 2.16/2.36 0 [] -bool(A)|bool(B)|impl(A,B)=phi(B). % 2.16/2.36 0 [] -bool(B)|impl(false,B)=true. % 2.16/2.36 0 [] -bool(B)|impl(true,B)=B. % 2.16/2.36 0 [] bool(A)|lazy_impl(A,B)=phi(A). % 2.16/2.36 0 [] lazy_impl(false,B)=true. % 2.16/2.36 0 [] lazy_impl(true,B)=phi(B). % 2.16/2.36 0 [] bool(A)|and1(A,B)=phi(A). % 2.16/2.36 0 [] -bool(A)|bool(B)|and1(A,B)=phi(B). % 2.16/2.36 0 [] -bool(B)|and1(false,B)=false. % 2.16/2.36 0 [] -bool(B)|and1(true,B)=B. % 2.16/2.36 0 [] f1(P,Q,R)=lazy_impl(prop(R),impl(impl(P,impl(Q,R)),R)). % 2.16/2.36 0 [] and2(P,Q)=phi(f1(P,Q,$f1(P,Q))). % 2.16/2.36 0 [] -forallprefers(f1(P,Q,R1),f1(P,Q,$f1(P,Q))). % 2.16/2.36 0 [] bool(A)|lazy_and1(A,B)=phi(A). % 2.16/2.36 0 [] lazy_and1(false,B)=false. % 2.16/2.36 0 [] lazy_and1(true,B)=phi(B). % 2.16/2.36 0 [] f2(P,Q,R)=lazy_impl(prop(R),impl(lazy_impl(P,impl(Q,R)),R)). % 2.16/2.36 0 [] lazy_and2(P,Q)=phi(f2(P,Q,$f2(P,Q))). % 2.16/2.36 0 [] -forallprefers(f2(P,Q,R1),f2(P,Q,$f2(P,Q))). % 2.16/2.36 0 [] bool(A)|or1(A,B)=phi(A). % 2.16/2.36 0 [] -bool(A)|bool(B)|or1(A,B)=phi(B). % 2.16/2.36 0 [] -bool(B)|or1(true,B)=true. % 2.16/2.36 0 [] -bool(B)|or1(false,B)=B. % 2.16/2.36 0 [] f3(P,Q,R)=lazy_impl(prop(R),impl(impl(P,R),impl(impl(Q,R),R))). % 2.16/2.36 0 [] or2(P,Q)=phi(f3(P,Q,$f3(P,Q))). % 2.16/2.36 0 [] -forallprefers(f3(P,Q,R1),f3(P,Q,$f3(P,Q))). % 2.16/2.36 0 [] exists1(P)=phi(apply(P,$f4(P))). % 2.16/2.36 0 [] -existsprefers(apply(P,X1),apply(P,$f4(P))). % 2.16/2.36 0 [] f4(P,X,R)=impl(apply(P,X),R). % 2.16/2.36 0 [] f5(P,R)=phi(f4(P,$f5(P,R),R)). % 2.16/2.36 0 [] -forallprefers(f4(P,X1,R),f4(P,$f5(P,R),R)). % 2.16/2.36 0 [] f6(P,R)=lazy_impl(prop(R),impl(f5(P,R),R)). % 2.16/2.36 0 [] exists2(P)=phi(f6(P,$f6(P))). % 2.16/2.36 0 [] -forallprefers(f6(P,R1),f6(P,$f6(P))). % 2.16/2.36 0 [] false1=false. % 2.16/2.36 0 [] f7(P)=lazy_impl(prop(P),P). % 2.16/2.36 0 [] false2=phi(f7($c1)). % 2.16/2.36 0 [] -forallprefers(f7(P1),f7($c1)). % 2.16/2.36 0 [] bool(A)|not1(A)=phi(A). % 2.16/2.36 0 [] not1(false)=true. % 2.16/2.36 0 [] not1(true)=false. % 2.16/2.36 0 [] not2(P)=impl(P,false2). % 2.16/2.36 0 [] not1($c2)!=not2($c2). % 2.16/2.36 end_of_list. % 2.16/2.36 % 2.16/2.36 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5. % 2.16/2.36 % 2.16/2.36 This ia a non-Horn set with equality. The strategy will be % 2.16/2.36 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.16/2.36 deletion, with positive clauses in sos and nonpositive % 2.16/2.36 clauses in usable. % 2.16/2.36 % 2.16/2.36 dependent: set(knuth_bendix). % 2.16/2.36 dependent: set(anl_eq). % 2.16/2.36 dependent: set(para_from). % 2.16/2.36 dependent: set(para_into). % 2.16/2.36 dependent: clear(para_from_right). % 2.16/2.36 dependent: clear(para_into_right). % 2.16/2.36 dependent: set(para_from_vars). % 2.16/2.36 dependent: set(eq_units_both_ways). % 2.16/2.36 dependent: set(dynamic_demod_all). % 2.16/2.36 dependent: set(dynamic_demod). % 2.16/2.36 dependent: set(order_eq). % 2.16/2.36 dependent: set(back_demod). % 2.16/2.36 dependent: set(lrpo). % 2.16/2.36 dependent: set(hyper_res). % 2.16/2.36 dependent: set(unit_deletion). % 2.16/2.36 dependent: set(factor). % 2.16/2.36 % 2.16/2.36 ------------> process usable: % 2.16/2.36 ** KEPT (pick-wt=8): 1 [] -bool(A)|A=false|A=true. % 2.16/2.36 ** KEPT (pick-wt=5): 2 [] bool(A)|A!=false. % 2.16/2.36 ** KEPT (pick-wt=5): 3 [] bool(A)|A!=true. % 2.16/2.36 ** KEPT (pick-wt=3): 4 [] true!=false. % 2.16/2.36 ** KEPT (pick-wt=3): 5 [] true!=err. % 2.16/2.36 ** KEPT (pick-wt=3): 6 [] false!=err. % 2.16/2.36 ** KEPT (pick-wt=10): 7 [] -forallprefers(A,B)| -d(A)| -bool(A)|A=false. % 2.16/2.36 ** KEPT (pick-wt=10): 8 [] -forallprefers(A,B)| -d(A)| -bool(A)|B=true. % 2.16/2.36 ** KEPT (pick-wt=10): 9 [] -forallprefers(A,B)| -d(A)|bool(B)|A=false. % 2.16/2.36 ** KEPT (pick-wt=10): 10 [] -forallprefers(A,B)| -d(A)|bool(B)|B=true. % 2.16/2.36 ** KEPT (pick-wt=8): 11 [] -forallprefers(A,B)|d(B)|A=false. % 2.16/2.36 ** KEPT (pick-wt=8): 12 [] -forallprefers(A,B)|d(B)|B=true. % 2.16/2.36 ** KEPT (pick-wt=7): 13 [] forallprefers(A,B)|d(A)| -d(B). % 2.16/2.36 ** KEPT (pick-wt=11): 14 [] forallprefers(A,B)| -d(A)| -d(B)|bool(A)| -bool(B). % 2.16/2.36 ** KEPT (pick-wt=9): 15 [] forallprefers(A,B)|A!=false|B!=true. % 2.16/2.36 ** KEPT (pick-wt=10): 16 [] -existsprefers(A,B)| -d(A)| -bool(A)|A=true. % 2.16/2.36 ** KEPT (pick-wt=10): 17 [] -existsprefers(A,B)| -d(A)| -bool(A)|B=false. % 2.16/2.36 ** KEPT (pick-wt=10): 18 [] -existsprefers(A,B)| -d(A)|bool(B)|A=true. % 2.16/2.36 ** KEPT (pick-wt=10): 19 [] -existsprefers(A,B)| -d(A)|bool(B)|B=false. % 2.16/2.36 ** KEPT (pick-wt=8): 20 [] -existsprefers(A,B)|d(B)|A=true. % 2.16/2.36 ** KEPT (pick-wt=8): 21 [] -existsprefers(A,B)|d(B)|B=false. % 2.16/2.36 ** KEPT (pick-wt=7): 22 [] existsprefers(A,B)|d(A)| -d(B). % 2.16/2.36 ** KEPT (pick-wt=11): 23 [] existsprefers(A,B)| -d(A)| -d(B)|bool(A)| -bool(B). % 2.16/2.36 ** KEPT (pick-wt=9): 24 [] existsprefers(A,B)|A!=true|B!=false. % 2.16/2.36 ** KEPT (pick-wt=6): 25 [] phi(A)=A| -d(A). % 2.16/2.36 ** KEPT (pick-wt=6): 26 [] prop(A)!=true|bool(A). % 2.16/2.36 ** KEPT (pick-wt=6): 27 [] prop(A)=true| -bool(A). % 2.16/2.36 ** KEPT (pick-wt=6): 28 [] prop(A)!=false| -bool(A). % 2.16/2.36 ** KEPT (pick-wt=10): 29 [] -bool(A)|bool(B)|impl(A,B)=phi(B). % 2.16/2.36 ** KEPT (pick-wt=7): 30 [] -bool(A)|impl(false,A)=true. % 2.16/2.36 ** KEPT (pick-wt=7): 31 [] -bool(A)|impl(true,A)=A. % 2.16/2.36 ** KEPT (pick-wt=10): 32 [] -bool(A)|bool(B)|and1(A,B)=phi(B). % 2.16/2.36 ** KEPT (pick-wt=7): 33 [] -bool(A)|and1(false,A)=false. % 2.16/2.36 ** KEPT (pick-wt=7): 34 [] -bool(A)|and1(true,A)=A. % 2.16/2.36 ** KEPT (pick-wt=11): 35 [] -forallprefers(f1(A,B,C),f1(A,B,$f1(A,B))). % 2.16/2.36 ** KEPT (pick-wt=11): 36 [] -forallprefers(f2(A,B,C),f2(A,B,$f2(A,B))). % 2.16/2.36 ** KEPT (pick-wt=10): 37 [] -bool(A)|bool(B)|or1(A,B)=phi(B). % 2.16/2.36 ** KEPT (pick-wt=7): 38 [] -bool(A)|or1(true,A)=true. % 2.16/2.36 ** KEPT (pick-wt=7): 39 [] -bool(A)|or1(false,A)=A. % 2.16/2.36 ** KEPT (pick-wt=11): 40 [] -forallprefers(f3(A,B,C),f3(A,B,$f3(A,B))). % 2.16/2.36 ** KEPT (pick-wt=8): 41 [] -existsprefers(apply(A,B),apply(A,$f4(A))). % 2.16/2.36 ** KEPT (pick-wt=11): 42 [] -forallprefers(f4(A,B,C),f4(A,$f5(A,C),C)). % 2.16/2.36 ** KEPT (pick-wt=8): 43 [] -forallprefers(f6(A,B),f6(A,$f6(A))). % 2.16/2.36 ** KEPT (pick-wt=5): 44 [] -forallprefers(f7(A),f7($c1)). % 2.16/2.36 ** KEPT (pick-wt=5): 46 [copy,45,flip.1] not2($c2)!=not1($c2). % 2.16/2.36 % 2.16/2.36 ------------> process sos: % 2.16/2.36 ** KEPT (pick-wt=3): 47 [] A=A. % 2.16/2.36 ** KEPT (pick-wt=2): 48 [] d(true). % 2.16/2.36 ** KEPT (pick-wt=2): 49 [] d(false). % 2.16/2.36 ** KEPT (pick-wt=2): 50 [] d(err). % 2.16/2.36 ** KEPT (pick-wt=6): 51 [] d(A)|phi(A)=err. % 2.16/2.36 ** KEPT (pick-wt=8): 52 [] phi(A)=A|phi(A)=err. % 2.16/2.36 ** KEPT (pick-wt=6): 53 [] prop(A)=false|bool(A). % 2.16/2.36 ** KEPT (pick-wt=8): 54 [] bool(A)|impl(A,B)=phi(A). % 2.16/2.36 ** KEPT (pick-wt=8): 55 [] bool(A)|lazy_impl(A,B)=phi(A). % 2.16/2.36 ** KEPT (pick-wt=5): 56 [] lazy_impl(false,A)=true. % 2.16/2.36 ---> New Demodulator: 57 [new_demod,56] lazy_impl(false,A)=true. % 2.16/2.36 ** KEPT (pick-wt=6): 59 [copy,58,flip.1] phi(A)=lazy_impl(true,A). % 2.16/2.36 ---> New Demodulator: 60 [new_demod,59] phi(A)=lazy_impl(true,A). % 2.16/2.36 ** KEPT (pick-wt=9): 62 [copy,61,demod,60] bool(A)|and1(A,B)=lazy_impl(true,A). % 2.16/2.36 ** KEPT (pick-wt=15): 64 [copy,63,flip.1] lazy_impl(prop(A),impl(impl(B,impl(C,A)),A))=f1(B,C,A). % 2.16/2.36 ---> New Demodulator: 65 [new_demod,64] lazy_impl(prop(A),impl(impl(B,impl(C,A)),A))=f1(B,C,A). % 2.16/2.36 ** KEPT (pick-wt=12): 67 [copy,66,demod,60,flip.1] lazy_impl(true,f1(A,B,$f1(A,B)))=and2(A,B). % 2.16/2.36 ---> New Demodulator: 68 [new_demod,67] lazy_impl(true,f1(A,B,$f1(A,B)))=and2(A,B). % 2.16/2.36 ** KEPT (pick-wt=9): 70 [copy,69,demod,60] bool(A)|lazy_and1(A,B)=lazy_impl(true,A). % 2.16/2.36 ** KEPT (pick-wt=5): 71 [] lazy_and1(false,A)=false. % 2.16/2.36 ---> New Demodulator: 72 [new_demod,71] lazy_and1(false,A)=false. % 2.16/2.36 ** KEPT (pick-wt=7): 74 [copy,73,demod,60,flip.1] lazy_impl(true,A)=lazy_and1(true,A). % 2.16/2.36 ---> New Demodulator: 75 [new_demod,74] lazy_impl(true,A)=lazy_and1(true,A). % 2.16/2.36 ** KEPT (pick-wt=15): 77 [copy,76,flip.1] lazy_impl(prop(A),impl(lazy_impl(B,impl(C,A)),A))=f2(B,C,A). % 2.16/2.36 ---> New Demodulator: 78 [new_demod,77] lazy_impl(prop(A),impl(lazy_impl(B,impl(C,A)),A))=f2(B,C,A). % 2.16/2.36 ** KEPT (pick-wt=12): 80 [copy,79,demod,60,75] lazy_and2(A,B)=lazy_and1(true,f2(A,B,$f2(A,B))). % 2.16/2.36 ---> New Demodulator: 81 [new_demod,80] lazy_and2(A,B)=lazy_and1(true,f2(A,B,$f2(A,B))). % 2.16/2.36 ** KEPT (pick-wt=9): 83 [copy,82,demod,60,75] bool(A)|or1(A,B)=lazy_and1(true,A). % 2.16/2.36 ** KEPT (pick-wt=17): 85 [copy,84,flip.1] lazy_impl(prop(A),impl(impl(B,A),impl(impl(C,A),A)))=f3(B,C,A). % 2.16/2.36 ---> New Demodulator: 86 [new_demod,85] lazy_impl(prop(A),impl(impl(B,A),impl(impl(C,A),A)))=f3(B,C,A). % 2.16/2.36 ** KEPT (pick-wt=12): 88 [copy,87,demod,60,75] or2(A,B)=lazy_and1(true,f3(A,B,$f3(A,B))). % 2.16/2.36 ---> New Demodulator: 89 [new_demod,88] or2(A,B)=lazy_and1(true,f3(A,B,$f3(A,B))). % 2.16/2.36 ** KEPT (pick-wt=9): 91 [copy,90,demod,60,75] exists1(A)=lazy_and1(true,apply(A,$f4(A))). % 2.16/2.36 ---> New Demodulator: 92 [new_demod,91] exists1(A)=lazy_and1(true,apply(A,$f4(A))). % 2.16/2.36 ** KEPT (pick-wt=10): 94 [copy,93,flip.1] impl(apply(A,B),C)=f4(A,B,C). % 2.16/2.36 ---> New Demodulator: 95 [new_demod,94] impl(apply(A,B),C)=f4(A,B,C). % 2.16/2.36 ** KEPT (pick-wt=12): 97 [copy,96,demod,60,75,flip.1] lazy_and1(true,f4(A,$f5(A,B),B))=f5(A,B). % 2.16/2.36 ---> New Demodulator: 98 [new_demod,97] lazy_and1(true,f4(A,$f5(A,B),B))=f5(A,B). % 2.16/2.36 ** KEPT (pick-wt=12): 100 [copy,99,flip.1] lazy_impl(prop(A),impl(f5(B,A),A))=f6(B,A). % 2.16/2.36 ---> New Demodulator: 101 [new_demod,100] lazy_impl(prop(A),impl(f5(B,A),A))=f6(B,A). % 10.07/10.24 ** KEPT (pick-wt=9): 103 [copy,102,demod,60,75] exists2(A)=lazy_and1(true,f6(A,$f6(A))). % 10.07/10.24 ---> New Demodulator: 104 [new_demod,103] exists2(A)=lazy_and1(true,f6(A,$f6(A))). % 10.07/10.24 ** KEPT (pick-wt=3): 105 [] false1=false. % 10.07/10.24 ---> New Demodulator: 106 [new_demod,105] false1=false. % 10.07/10.24 ** KEPT (pick-wt=7): 108 [copy,107,flip.1] lazy_impl(prop(A),A)=f7(A). % 10.07/10.24 ---> New Demodulator: 109 [new_demod,108] lazy_impl(prop(A),A)=f7(A). % 10.07/10.24 ** KEPT (pick-wt=6): 111 [copy,110,demod,60,75,flip.1] lazy_and1(true,f7($c1))=false2. % 10.07/10.24 ---> New Demodulator: 112 [new_demod,111] lazy_and1(true,f7($c1))=false2. % 10.07/10.24 ** KEPT (pick-wt=8): 114 [copy,113,demod,60,75] bool(A)|not1(A)=lazy_and1(true,A). % 10.07/10.24 ** KEPT (pick-wt=4): 115 [] not1(false)=true. % 10.07/10.24 ---> New Demodulator: 116 [new_demod,115] not1(false)=true. % 10.07/10.24 ** KEPT (pick-wt=4): 117 [] not1(true)=false. % 10.07/10.24 ---> New Demodulator: 118 [new_demod,117] not1(true)=false. % 10.07/10.24 ** KEPT (pick-wt=6): 119 [] not2(A)=impl(A,false2). % 10.07/10.24 ---> New Demodulator: 120 [new_demod,119] not2(A)=impl(A,false2). % 10.07/10.24 Following clause subsumed by 47 during input processing: 0 [copy,47,flip.1] A=A. % 10.07/10.24 >>>> Starting back demodulation with 57. % 10.07/10.24 >>>> Starting back demodulation with 60. % 10.07/10.24 >> back demodulating 55 with 60. % 10.07/10.24 >> back demodulating 54 with 60. % 10.07/10.24 >> back demodulating 52 with 60. % 10.07/10.24 >> back demodulating 51 with 60. % 10.07/10.24 >> back demodulating 37 with 60. % 10.07/10.24 >> back demodulating 32 with 60. % 10.07/10.24 >> back demodulating 29 with 60. % 10.07/10.24 >> back demodulating 25 with 60. % 10.07/10.24 >>>> Starting back demodulation with 65. % 10.07/10.24 >>>> Starting back demodulation with 68. % 10.07/10.24 >>>> Starting back demodulation with 72. % 10.07/10.24 >>>> Starting back demodulation with 75. % 10.07/10.24 >> back demodulating 70 with 75. % 10.07/10.24 >> back demodulating 67 with 75. % 10.07/10.24 >> back demodulating 62 with 75. % 10.07/10.24 >> back demodulating 59 with 75. % 10.07/10.24 >>>> Starting back demodulation with 78. % 10.07/10.24 >>>> Starting back demodulation with 81. % 10.07/10.24 >>>> Starting back demodulation with 86. % 10.07/10.24 >>>> Starting back demodulation with 89. % 10.07/10.24 >>>> Starting back demodulation with 92. % 10.07/10.24 >>>> Starting back demodulation with 95. % 10.07/10.24 >>>> Starting back demodulation with 98. % 10.07/10.24 >>>> Starting back demodulation with 101. % 10.07/10.24 >>>> Starting back demodulation with 104. % 10.07/10.24 >>>> Starting back demodulation with 106. % 10.07/10.24 >>>> Starting back demodulation with 109. % 10.07/10.24 >>>> Starting back demodulation with 112. % 10.07/10.24 >>>> Starting back demodulation with 116. % 10.07/10.24 >>>> Starting back demodulation with 118. % 10.07/10.24 >>>> Starting back demodulation with 120. % 10.07/10.24 >> back demodulating 46 with 120. % 10.07/10.24 >>>> Starting back demodulation with 122. % 10.07/10.24 >>>> Starting back demodulation with 133. % 10.07/10.24 >>>> Starting back demodulation with 136. % 10.07/10.24 % 10.07/10.24 ======= end of input processing ======= % 10.07/10.24 % 10.07/10.24 =========== start of search =========== % 10.07/10.24 % 10.07/10.24 % 10.07/10.24 Resetting weight limit to 8. % 10.07/10.24 % 10.07/10.24 % 10.07/10.24 Resetting weight limit to 8. % 10.07/10.24 % 10.07/10.24 sos_size=580 % 10.07/10.24 % 10.07/10.24 % 10.07/10.24 Resetting weight limit to 5. % 10.07/10.24 % 10.07/10.24 % 10.07/10.24 Resetting weight limit to 5. % 10.07/10.24 % 10.07/10.24 sos_size=330 % 10.07/10.24 % 10.07/10.24 Search stopped because sos empty. % 10.07/10.24 % 10.07/10.24 % 10.07/10.24 Search stopped because sos empty. % 10.07/10.24 % 10.07/10.24 ============ end of search ============ % 10.07/10.24 % 10.07/10.24 -------------- statistics ------------- % 10.07/10.24 clauses given 459 % 10.07/10.24 clauses generated 807496 % 10.07/10.24 clauses kept 1070 % 10.07/10.24 clauses forward subsumed 10374 % 10.07/10.24 clauses back subsumed 192 % 10.07/10.24 Kbytes malloced 4882 % 10.07/10.24 % 10.07/10.24 ----------- times (seconds) ----------- % 10.07/10.24 user CPU time 7.88 (0 hr, 0 min, 7 sec) % 10.07/10.24 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 10.07/10.24 wall-clock time 9 (0 hr, 0 min, 9 sec) % 10.07/10.24 % 10.07/10.24 Process 29835 finished Wed Jul 27 02:57:11 2022 % 10.07/10.24 Otter interrupted % 10.07/10.24 PROOF NOT FOUND %------------------------------------------------------------------------------