%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : COL074-3 : TPTP v8.1.0. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n022.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 12:48:11 EDT 2022
% Result : Unsatisfiable 1.93s 2.09s
% Output : Refutation 1.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of clauses : 30 ( 20 unt; 1 nHn; 16 RR)
% Number of literals : 40 ( 39 equ; 12 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 36 ( 5 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( A = B
| apply(A,n(A,B)) != apply(B,n(A,B)) ),
file('COL074-3.p',unknown),
[] ).
cnf(2,axiom,
projection1 != projection2,
file('COL074-3.p',unknown),
[] ).
cnf(3,plain,
projection2 != projection1,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[2])]),
[iquote('copy,2,flip.1')] ).
cnf(4,axiom,
A = A,
file('COL074-3.p',unknown),
[] ).
cnf(6,axiom,
apply(apply(k,A),B) = A,
file('COL074-3.p',unknown),
[] ).
cnf(13,axiom,
apply(pair(A,B),C) = pair(apply(A,C),apply(B,C)),
file('COL074-3.p',unknown),
[] ).
cnf(14,plain,
pair(apply(A,B),apply(C,B)) = apply(pair(A,C),B),
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[13])]),
[iquote('copy,13,flip.1')] ).
cnf(17,axiom,
apply(e_q,pair(A,A)) = projection1,
file('COL074-3.p',unknown),
[] ).
cnf(19,axiom,
( A = B
| apply(e_q,pair(A,B)) = projection2 ),
file('COL074-3.p',unknown),
[] ).
cnf(23,axiom,
apply(k,projection2) = k_projection2,
file('COL074-3.p',unknown),
[] ).
cnf(24,axiom,
s = apply(e_q,pair(apply(k,s),apply(k,projection2))),
file('COL074-3.p',unknown),
[] ).
cnf(25,plain,
apply(e_q,pair(apply(k,s),k_projection2)) = s,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(copy,[status(thm)],[24]),23])]),
[iquote('copy,24,demod,23,flip.1')] ).
cnf(37,plain,
apply(k_projection2,A) = projection2,
inference(para_into,[status(thm),theory(equality)],[6,23]),
[iquote('para_into,5.1.1.1,22.1.1')] ).
cnf(41,plain,
( apply(A,B) = C
| apply(A,n(apply(k,C),A)) != C ),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[6,1]),6])]),
[iquote('para_into,5.1.1.1,1.1.1,demod,6,flip.2')] ).
cnf(45,plain,
( apply(k,A) = B
| apply(B,n(apply(k,A),B)) != A ),
inference(flip,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[6,1])]),
[iquote('para_from,5.1.1,1.2.1,flip.2')] ).
cnf(81,plain,
pair(apply(A,projection2),k_projection2) = apply(pair(A,k),projection2),
inference(para_into,[status(thm),theory(equality)],[14,23]),
[iquote('para_into,14.1.1.2,22.1.1')] ).
cnf(92,plain,
pair(apply(A,B),C) = apply(pair(A,apply(k,C)),B),
inference(para_into,[status(thm),theory(equality)],[14,6]),
[iquote('para_into,14.1.1.2,5.1.1')] ).
cnf(106,plain,
apply(pair(A,apply(k,k_projection2)),projection2) = apply(pair(A,k),projection2),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[81]),92]),
[iquote('back_demod,81,demod,92')] ).
cnf(110,plain,
apply(e_q,apply(pair(k,apply(k,k_projection2)),s)) = s,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[25]),92]),
[iquote('back_demod,25,demod,92')] ).
cnf(112,plain,
apply(pair(A,apply(k,apply(B,C))),C) = apply(pair(A,B),C),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[14]),92]),
[iquote('back_demod,14,demod,92')] ).
cnf(940,plain,
( A = B
| B != A ),
inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[41,6]),6]),
[iquote('para_from,41.1.1,5.1.1,demod,6')] ).
cnf(990,plain,
( apply(A,B) = projection2
| A != k_projection2 ),
inference(para_from,[status(thm),theory(equality)],[940,37]),
[iquote('para_from,940.1.1,37.1.1.1')] ).
cnf(1285,plain,
( apply(k,A) = k_projection2
| projection2 != A ),
inference(para_into,[status(thm),theory(equality)],[45,37]),
[iquote('para_into,45.2.1,37.1.1')] ).
cnf(1361,plain,
( A = projection2
| apply(k,A) != k_projection2 ),
inference(para_into,[status(thm),theory(equality)],[990,6]),
[iquote('para_into,990.1.1,5.1.1')] ).
cnf(1723,plain,
apply(e_q,apply(pair(A,A),B)) = projection1,
inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[92,17]),112]),
[iquote('para_from,91.1.1,17.1.1.2,demod,112')] ).
cnf(1770,plain,
( s = projection1
| apply(k,s) != k_projection2 ),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[110,1361]),106,1723])]),
[iquote('para_into,109.1.1.2.2,1361.1.1,demod,106,1723,flip.1')] ).
cnf(1778,plain,
apply(k,s) != k_projection2,
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[1770,1361]),3])]),
[iquote('para_into,1770.1.1,1361.1.1,unit_del,3,factor_simp')] ).
cnf(1779,plain,
( s = projection1
| s != projection2 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[1770,1285]),4])]),
[iquote('para_into,1770.2.1,1285.1.1,unit_del,4,flip.2')] ).
cnf(1781,plain,
s = projection2,
inference(demod,[status(thm),theory(equality)],[inference(hyper,[status(thm)],[1778,19]),92,110]),
[iquote('hyper,1778,19,demod,92,110')] ).
cnf(1782,plain,
$false,
inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[1779]),1781,1781]),3,4]),
[iquote('back_demod,1779,demod,1781,1781,unit_del,3,4')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : COL074-3 : TPTP v8.1.0. Released v1.2.0.
% 0.07/0.13 % Command : otter-tptp-script %s
% 0.14/0.34 % Computer : n022.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Jul 27 02:23:35 EDT 2022
% 0.14/0.35 % CPUTime :
% 1.67/1.83 ----- Otter 3.3f, August 2004 -----
% 1.67/1.83 The process was started by sandbox2 on n022.cluster.edu,
% 1.67/1.83 Wed Jul 27 02:23:35 2022
% 1.67/1.83 The command was "./otter". The process ID is 6801.
% 1.67/1.83
% 1.67/1.83 set(prolog_style_variables).
% 1.67/1.83 set(auto).
% 1.67/1.83 dependent: set(auto1).
% 1.67/1.83 dependent: set(process_input).
% 1.67/1.83 dependent: clear(print_kept).
% 1.67/1.83 dependent: clear(print_new_demod).
% 1.67/1.83 dependent: clear(print_back_demod).
% 1.67/1.83 dependent: clear(print_back_sub).
% 1.67/1.83 dependent: set(control_memory).
% 1.67/1.83 dependent: assign(max_mem, 12000).
% 1.67/1.83 dependent: assign(pick_given_ratio, 4).
% 1.67/1.83 dependent: assign(stats_level, 1).
% 1.67/1.83 dependent: assign(max_seconds, 10800).
% 1.67/1.83 clear(print_given).
% 1.67/1.83
% 1.67/1.83 list(usable).
% 1.67/1.83 0 [] A=A.
% 1.67/1.83 0 [] apply(apply(k,X),Y)=X.
% 1.67/1.83 0 [] apply(projection1,pair(X,Y))=X.
% 1.67/1.83 0 [] apply(projection2,pair(X,Y))=Y.
% 1.67/1.83 0 [] pair(apply(projection1,X),apply(projection2,X))=X.
% 1.67/1.83 0 [] apply(pair(X,Y),Z)=pair(apply(X,Z),apply(Y,Z)).
% 1.67/1.83 0 [] apply(apply(apply(abstraction,X),Y),Z)=apply(apply(X,apply(k,Z)),apply(Y,Z)).
% 1.67/1.83 0 [] apply(e_q,pair(X,X))=projection1.
% 1.67/1.83 0 [] X=Y|apply(e_q,pair(X,Y))=projection2.
% 1.67/1.83 0 [] X=Y|apply(X,n(X,Y))!=apply(Y,n(X,Y)).
% 1.67/1.83 0 [] projection1!=projection2.
% 1.67/1.83 0 [] apply(k,projection1)=k_projection1.
% 1.67/1.83 0 [] apply(k,projection2)=k_projection2.
% 1.67/1.83 0 [] s=apply(e_q,pair(apply(k,s),apply(k,projection2))).
% 1.67/1.83 end_of_list.
% 1.67/1.83
% 1.67/1.83 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2.
% 1.67/1.83
% 1.67/1.83 This ia a non-Horn set with equality. The strategy will be
% 1.67/1.83 Knuth-Bendix, ordered hyper_res, factoring, and unit
% 1.67/1.83 deletion, with positive clauses in sos and nonpositive
% 1.67/1.83 clauses in usable.
% 1.67/1.83
% 1.67/1.83 dependent: set(knuth_bendix).
% 1.67/1.83 dependent: set(anl_eq).
% 1.67/1.83 dependent: set(para_from).
% 1.67/1.83 dependent: set(para_into).
% 1.67/1.83 dependent: clear(para_from_right).
% 1.67/1.83 dependent: clear(para_into_right).
% 1.67/1.83 dependent: set(para_from_vars).
% 1.67/1.83 dependent: set(eq_units_both_ways).
% 1.67/1.83 dependent: set(dynamic_demod_all).
% 1.67/1.83 dependent: set(dynamic_demod).
% 1.67/1.83 dependent: set(order_eq).
% 1.67/1.83 dependent: set(back_demod).
% 1.67/1.83 dependent: set(lrpo).
% 1.67/1.83 dependent: set(hyper_res).
% 1.67/1.83 dependent: set(unit_deletion).
% 1.67/1.83 dependent: set(factor).
% 1.67/1.83
% 1.67/1.83 ------------> process usable:
% 1.67/1.83 ** KEPT (pick-wt=14): 1 [] A=B|apply(A,n(A,B))!=apply(B,n(A,B)).
% 1.67/1.83 ** KEPT (pick-wt=3): 3 [copy,2,flip.1] projection2!=projection1.
% 1.67/1.83
% 1.67/1.83 ------------> process sos:
% 1.67/1.83 ** KEPT (pick-wt=3): 4 [] A=A.
% 1.67/1.83 ** KEPT (pick-wt=7): 5 [] apply(apply(k,A),B)=A.
% 1.67/1.83 ---> New Demodulator: 6 [new_demod,5] apply(apply(k,A),B)=A.
% 1.67/1.83 ** KEPT (pick-wt=7): 7 [] apply(projection1,pair(A,B))=A.
% 1.67/1.83 ---> New Demodulator: 8 [new_demod,7] apply(projection1,pair(A,B))=A.
% 1.67/1.83 ** KEPT (pick-wt=7): 9 [] apply(projection2,pair(A,B))=B.
% 1.67/1.83 ---> New Demodulator: 10 [new_demod,9] apply(projection2,pair(A,B))=B.
% 1.67/1.83 ** KEPT (pick-wt=9): 11 [] pair(apply(projection1,A),apply(projection2,A))=A.
% 1.67/1.83 ---> New Demodulator: 12 [new_demod,11] pair(apply(projection1,A),apply(projection2,A))=A.
% 1.67/1.83 ** KEPT (pick-wt=13): 14 [copy,13,flip.1] pair(apply(A,B),apply(C,B))=apply(pair(A,C),B).
% 1.67/1.83 ---> New Demodulator: 15 [new_demod,14] pair(apply(A,B),apply(C,B))=apply(pair(A,C),B).
% 1.67/1.83 ** KEPT (pick-wt=17): 16 [] apply(apply(apply(abstraction,A),B),C)=apply(apply(A,apply(k,C)),apply(B,C)).
% 1.67/1.83 ** KEPT (pick-wt=7): 17 [] apply(e_q,pair(A,A))=projection1.
% 1.67/1.83 ---> New Demodulator: 18 [new_demod,17] apply(e_q,pair(A,A))=projection1.
% 1.67/1.83 ** KEPT (pick-wt=10): 19 [] A=B|apply(e_q,pair(A,B))=projection2.
% 1.67/1.83 ** KEPT (pick-wt=5): 20 [] apply(k,projection1)=k_projection1.
% 1.67/1.83 ---> New Demodulator: 21 [new_demod,20] apply(k,projection1)=k_projection1.
% 1.67/1.83 ** KEPT (pick-wt=5): 22 [] apply(k,projection2)=k_projection2.
% 1.67/1.83 ---> New Demodulator: 23 [new_demod,22] apply(k,projection2)=k_projection2.
% 1.67/1.83 ** KEPT (pick-wt=9): 25 [copy,24,demod,23,flip.1] apply(e_q,pair(apply(k,s),k_projection2))=s.
% 1.67/1.83 ---> New Demodulator: 26 [new_demod,25] apply(e_q,pair(apply(k,s),k_projection2))=s.
% 1.67/1.83 Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] A=A.
% 1.67/1.83 >>>> Starting back demodulation with 6.
% 1.67/1.83 >>>> Starting back demodulation with 8.
% 1.67/1.83 >>>> Starting back demodulation with 10.
% 1.67/1.83 >>>> Starting back demodulation with 12.
% 1.67/1.83 >>>> Starting back demodulation with 15.
% 1.67/1.83 >> back demodulating 11 with 15.
% 1.67/1.83 ** KEPT (pick-wt=17): 29 [copy,16,flip.1] apply(apply(A,apply(k,B)),apply(C,B))=apply(apply(apply(abstraction,A),C),B).
% 1.93/2.09 >>>> Starting back demodulation with 18.
% 1.93/2.09 >>>> Starting back demodulation with 21.
% 1.93/2.09 >>>> Starting back demodulation with 23.
% 1.93/2.09 >>>> Starting back demodulation with 26.
% 1.93/2.09 >>>> Starting back demodulation with 28.
% 1.93/2.09 Following clause subsumed by 16 during input processing: 0 [copy,29,flip.1] apply(apply(apply(abstraction,A),B),C)=apply(apply(A,apply(k,C)),apply(B,C)).
% 1.93/2.09
% 1.93/2.09 ======= end of input processing =======
% 1.93/2.09
% 1.93/2.09 =========== start of search ===========
% 1.93/2.09
% 1.93/2.09
% 1.93/2.09 Resetting weight limit to 10.
% 1.93/2.09
% 1.93/2.09
% 1.93/2.09 Resetting weight limit to 10.
% 1.93/2.09
% 1.93/2.09 sos_size=847
% 1.93/2.09
% 1.93/2.09
% 1.93/2.09 Resetting weight limit to 9.
% 1.93/2.09
% 1.93/2.09
% 1.93/2.09 Resetting weight limit to 9.
% 1.93/2.09
% 1.93/2.09 sos_size=1025
% 1.93/2.09
% 1.93/2.09 -------- PROOF --------
% 1.93/2.09
% 1.93/2.09 -----> EMPTY CLAUSE at 0.26 sec ----> 1782 [back_demod,1779,demod,1781,1781,unit_del,3,4] $F.
% 1.93/2.09
% 1.93/2.09 Length of proof is 20. Level of proof is 7.
% 1.93/2.09
% 1.93/2.09 ---------------- PROOF ----------------
% 1.93/2.09 % SZS status Unsatisfiable
% 1.93/2.09 % SZS output start Refutation
% See solution above
% 1.93/2.09 ------------ end of proof -------------
% 1.93/2.09
% 1.93/2.09
% 1.93/2.09 Search stopped by max_proofs option.
% 1.93/2.09
% 1.93/2.09
% 1.93/2.09 Search stopped by max_proofs option.
% 1.93/2.09
% 1.93/2.09 ============ end of search ============
% 1.93/2.09
% 1.93/2.09 -------------- statistics -------------
% 1.93/2.09 clauses given 255
% 1.93/2.09 clauses generated 18217
% 1.93/2.09 clauses kept 1660
% 1.93/2.09 clauses forward subsumed 6294
% 1.93/2.09 clauses back subsumed 398
% 1.93/2.09 Kbytes malloced 4882
% 1.93/2.09
% 1.93/2.09 ----------- times (seconds) -----------
% 1.93/2.09 user CPU time 0.26 (0 hr, 0 min, 0 sec)
% 1.93/2.09 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 1.93/2.09 wall-clock time 2 (0 hr, 0 min, 2 sec)
% 1.93/2.09
% 1.93/2.09 That finishes the proof of the theorem.
% 1.93/2.09
% 1.93/2.09 Process 6801 finished Wed Jul 27 02:23:37 2022
% 1.93/2.09 Otter interrupted
% 1.93/2.09 PROOF FOUND
%------------------------------------------------------------------------------