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