%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : ROB022-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n014.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:12:23 EDT 2022
% Result : Unsatisfiable 1.83s 2.02s
% Output : Refutation 1.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 6
% Syntax : Number of clauses : 32 ( 32 unt; 0 nHn; 12 RR)
% Number of literals : 32 ( 31 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 33 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
add(negate(add(a,negate(b))),negate(add(negate(a),negate(b)))) != b,
file('ROB022-1.p',unknown),
[] ).
cnf(2,axiom,
A = A,
file('ROB022-1.p',unknown),
[] ).
cnf(3,axiom,
add(A,B) = add(B,A),
file('ROB022-1.p',unknown),
[] ).
cnf(5,axiom,
add(add(A,B),C) = add(A,add(B,C)),
file('ROB022-1.p',unknown),
[] ).
cnf(7,axiom,
negate(add(negate(add(A,B)),negate(add(A,negate(B))))) = A,
file('ROB022-1.p',unknown),
[] ).
cnf(8,axiom,
add(c,negate(c)) = c,
file('ROB022-1.p',unknown),
[] ).
cnf(11,plain,
add(negate(c),c) = c,
inference(flip,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[3,8])]),
[iquote('para_into,3.1.1,8.1.1,flip.1')] ).
cnf(14,plain,
add(negate(add(negate(b),a)),negate(add(negate(a),negate(b)))) != b,
inference(para_from,[status(thm),theory(equality)],[3,1]),
[iquote('para_from,3.1.1,1.1.1.1.1')] ).
cnf(15,plain,
add(negate(c),add(c,A)) = add(c,A),
inference(flip,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[5,11])]),
[iquote('para_into,4.1.1.1,10.1.1,flip.1')] ).
cnf(26,plain,
negate(add(negate(add(A,add(B,C))),negate(add(A,add(B,negate(C)))))) = add(A,B),
inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[7,5]),5]),
[iquote('para_into,6.1.1.1.1.1,4.1.1,demod,5')] ).
cnf(28,plain,
negate(add(negate(add(A,B)),negate(add(B,negate(A))))) = B,
inference(para_into,[status(thm),theory(equality)],[7,3]),
[iquote('para_into,6.1.1.1.1.1,3.1.1')] ).
cnf(32,plain,
negate(add(negate(add(A,add(negate(add(B,C)),negate(add(B,negate(C)))))),negate(add(A,B)))) = A,
inference(para_into,[status(thm),theory(equality)],[7,7]),
[iquote('para_into,6.1.1.1.2.1.2,6.1.1')] ).
cnf(34,plain,
negate(add(negate(add(c,c)),negate(c))) = c,
inference(para_into,[status(thm),theory(equality)],[7,8]),
[iquote('para_into,6.1.1.1.2.1,8.1.1')] ).
cnf(36,plain,
negate(add(negate(add(A,B)),negate(add(negate(B),A)))) = A,
inference(para_into,[status(thm),theory(equality)],[7,3]),
[iquote('para_into,6.1.1.1.2.1,3.1.1')] ).
cnf(40,plain,
negate(add(negate(add(A,negate(B))),negate(add(A,B)))) = A,
inference(para_into,[status(thm),theory(equality)],[7,3]),
[iquote('para_into,6.1.1.1,3.1.1')] ).
cnf(43,plain,
add(negate(c),add(A,c)) = add(c,A),
inference(para_into,[status(thm),theory(equality)],[15,3]),
[iquote('para_into,15.1.1.2,3.1.1')] ).
cnf(50,plain,
negate(add(negate(c),negate(add(c,c)))) = c,
inference(para_into,[status(thm),theory(equality)],[34,3]),
[iquote('para_into,34.1.1.1,3.1.1')] ).
cnf(52,plain,
negate(add(negate(add(negate(add(c,c)),c)),c)) = negate(add(c,c)),
inference(para_from,[status(thm),theory(equality)],[34,7]),
[iquote('para_from,34.1.1,6.1.1.1.2')] ).
cnf(73,plain,
negate(add(negate(add(c,c)),c)) = negate(c),
inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[50,7]),43]),
[iquote('para_from,50.1.1,6.1.1.1.2,demod,43')] ).
cnf(79,plain,
negate(add(c,c)) = negate(c),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[52]),73,11])]),
[iquote('back_demod,52,demod,73,11,flip.1')] ).
cnf(84,plain,
negate(add(negate(c),negate(c))) = c,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[50]),79]),
[iquote('back_demod,50,demod,79')] ).
cnf(160,plain,
negate(add(negate(add(A,c)),negate(add(A,add(negate(c),negate(c)))))) = add(A,negate(c)),
inference(para_into,[status(thm),theory(equality)],[26,11]),
[iquote('para_into,26.1.1.1.1.1.2,10.1.1')] ).
cnf(171,plain,
negate(add(negate(add(c,A)),negate(add(negate(c),add(A,negate(c)))))) = add(negate(c),A),
inference(para_into,[status(thm),theory(equality)],[26,43]),
[iquote('para_into,26.1.1.1.1.1,42.1.1')] ).
cnf(248,plain,
negate(add(negate(add(A,B)),negate(add(negate(A),B)))) = B,
inference(para_into,[status(thm),theory(equality)],[28,3]),
[iquote('para_into,28.1.1.1.2.1,3.1.1')] ).
cnf(434,plain,
add(A,negate(c)) = A,
inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[40,84]),160]),
[iquote('para_into,40.1.1.1.1.1.2,84.1.1,demod,160')] ).
cnf(508,plain,
add(negate(c),A) = A,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[171]),434,248])]),
[iquote('back_demod,171,demod,434,248,flip.1')] ).
cnf(661,plain,
negate(add(A,negate(A))) = negate(c),
inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[508,32]),7,508]),
[iquote('para_from,507.1.1,32.1.1.1.1.1,demod,7,508')] ).
cnf(674,plain,
negate(negate(add(negate(negate(A)),A))) = negate(negate(A)),
inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[661,36]),434]),
[iquote('para_from,661.1.1,36.1.1.1.2,demod,434')] ).
cnf(686,plain,
negate(negate(A)) = A,
inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[661,36]),508,674]),
[iquote('para_from,661.1.1,36.1.1.1.1,demod,508,674')] ).
cnf(704,plain,
add(negate(add(A,B)),negate(add(negate(B),A))) = negate(A),
inference(flip,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[686,36])]),
[iquote('para_into,685.1.1.1,36.1.1,flip.1')] ).
cnf(709,plain,
b != b,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[14]),704,686]),
[iquote('back_demod,14,demod,704,686')] ).
cnf(710,plain,
$false,
inference(binary,[status(thm)],[709,2]),
[iquote('binary,709.1,2.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ROB022-1 : TPTP v8.1.0. Released v1.0.0.
% 0.07/0.13 % Command : otter-tptp-script %s
% 0.13/0.34 % Computer : n014.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Jul 27 04:04:39 EDT 2022
% 0.13/0.34 % CPUTime :
% 1.83/2.02 ----- Otter 3.3f, August 2004 -----
% 1.83/2.02 The process was started by sandbox2 on n014.cluster.edu,
% 1.83/2.02 Wed Jul 27 04:04:39 2022
% 1.83/2.02 The command was "./otter". The process ID is 22620.
% 1.83/2.02
% 1.83/2.02 set(prolog_style_variables).
% 1.83/2.02 set(auto).
% 1.83/2.02 dependent: set(auto1).
% 1.83/2.02 dependent: set(process_input).
% 1.83/2.02 dependent: clear(print_kept).
% 1.83/2.02 dependent: clear(print_new_demod).
% 1.83/2.02 dependent: clear(print_back_demod).
% 1.83/2.02 dependent: clear(print_back_sub).
% 1.83/2.02 dependent: set(control_memory).
% 1.83/2.02 dependent: assign(max_mem, 12000).
% 1.83/2.02 dependent: assign(pick_given_ratio, 4).
% 1.83/2.02 dependent: assign(stats_level, 1).
% 1.83/2.02 dependent: assign(max_seconds, 10800).
% 1.83/2.02 clear(print_given).
% 1.83/2.02
% 1.83/2.02 list(usable).
% 1.83/2.02 0 [] A=A.
% 1.83/2.02 0 [] add(X,Y)=add(Y,X).
% 1.83/2.02 0 [] add(add(X,Y),Z)=add(X,add(Y,Z)).
% 1.83/2.02 0 [] negate(add(negate(add(X,Y)),negate(add(X,negate(Y)))))=X.
% 1.83/2.02 0 [] add(c,negate(c))=c.
% 1.83/2.02 0 [] add(negate(add(a,negate(b))),negate(add(negate(a),negate(b))))!=b.
% 1.83/2.02 end_of_list.
% 1.83/2.02
% 1.83/2.02 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1.
% 1.83/2.02
% 1.83/2.02 All clauses are units, and equality is present; the
% 1.83/2.02 strategy will be Knuth-Bendix with positive clauses in sos.
% 1.83/2.02
% 1.83/2.02 dependent: set(knuth_bendix).
% 1.83/2.02 dependent: set(anl_eq).
% 1.83/2.02 dependent: set(para_from).
% 1.83/2.02 dependent: set(para_into).
% 1.83/2.02 dependent: clear(para_from_right).
% 1.83/2.02 dependent: clear(para_into_right).
% 1.83/2.02 dependent: set(para_from_vars).
% 1.83/2.02 dependent: set(eq_units_both_ways).
% 1.83/2.02 dependent: set(dynamic_demod_all).
% 1.83/2.02 dependent: set(dynamic_demod).
% 1.83/2.02 dependent: set(order_eq).
% 1.83/2.02 dependent: set(back_demod).
% 1.83/2.02 dependent: set(lrpo).
% 1.83/2.02
% 1.83/2.02 ------------> process usable:
% 1.83/2.02 ** KEPT (pick-wt=14): 1 [] add(negate(add(a,negate(b))),negate(add(negate(a),negate(b))))!=b.
% 1.83/2.02
% 1.83/2.02 ------------> process sos:
% 1.83/2.02 ** KEPT (pick-wt=3): 2 [] A=A.
% 1.83/2.02 ** KEPT (pick-wt=7): 3 [] add(A,B)=add(B,A).
% 1.83/2.02 ** KEPT (pick-wt=11): 4 [] add(add(A,B),C)=add(A,add(B,C)).
% 1.83/2.02 ---> New Demodulator: 5 [new_demod,4] add(add(A,B),C)=add(A,add(B,C)).
% 1.83/2.02 ** KEPT (pick-wt=13): 6 [] negate(add(negate(add(A,B)),negate(add(A,negate(B)))))=A.
% 1.83/2.02 ---> New Demodulator: 7 [new_demod,6] negate(add(negate(add(A,B)),negate(add(A,negate(B)))))=A.
% 1.83/2.02 ** KEPT (pick-wt=6): 8 [] add(c,negate(c))=c.
% 1.83/2.02 ---> New Demodulator: 9 [new_demod,8] add(c,negate(c))=c.
% 1.83/2.02 Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] A=A.
% 1.83/2.02 Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] add(A,B)=add(B,A).
% 1.83/2.02 >>>> Starting back demodulation with 5.
% 1.83/2.02 >>>> Starting back demodulation with 7.
% 1.83/2.02 >>>> Starting back demodulation with 9.
% 1.83/2.02
% 1.83/2.02 ======= end of input processing =======
% 1.83/2.02
% 1.83/2.02 =========== start of search ===========
% 1.83/2.02
% 1.83/2.02
% 1.83/2.02 Resetting weight limit to 13.
% 1.83/2.02
% 1.83/2.02
% 1.83/2.02 Resetting weight limit to 13.
% 1.83/2.02
% 1.83/2.02 sos_size=236
% 1.83/2.02
% 1.83/2.02 -------- PROOF --------
% 1.83/2.02
% 1.83/2.02 ----> UNIT CONFLICT at 0.03 sec ----> 710 [binary,709.1,2.1] $F.
% 1.83/2.02
% 1.83/2.02 Length of proof is 25. Level of proof is 13.
% 1.83/2.02
% 1.83/2.02 ---------------- PROOF ----------------
% 1.83/2.02 % SZS status Unsatisfiable
% 1.83/2.02 % SZS output start Refutation
% See solution above
% 1.83/2.02 ------------ end of proof -------------
% 1.83/2.02
% 1.83/2.02
% 1.83/2.02 Search stopped by max_proofs option.
% 1.83/2.02
% 1.83/2.02
% 1.83/2.02 Search stopped by max_proofs option.
% 1.83/2.02
% 1.83/2.02 ============ end of search ============
% 1.83/2.02
% 1.83/2.02 -------------- statistics -------------
% 1.83/2.02 clauses given 39
% 1.83/2.02 clauses generated 881
% 1.83/2.02 clauses kept 376
% 1.83/2.02 clauses forward subsumed 667
% 1.83/2.02 clauses back subsumed 0
% 1.83/2.02 Kbytes malloced 4882
% 1.83/2.02
% 1.83/2.02 ----------- times (seconds) -----------
% 1.83/2.02 user CPU time 0.03 (0 hr, 0 min, 0 sec)
% 1.83/2.02 system CPU time 0.01 (0 hr, 0 min, 0 sec)
% 1.83/2.02 wall-clock time 2 (0 hr, 0 min, 2 sec)
% 1.83/2.02
% 1.83/2.02 That finishes the proof of the theorem.
% 1.83/2.02
% 1.83/2.02 Process 22620 finished Wed Jul 27 04:04:41 2022
% 1.83/2.02 Otter interrupted
% 1.83/2.02 PROOF FOUND
%------------------------------------------------------------------------------