%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : BOO014-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:00:13 PM UTC 2026
% Result : Unsatisfiable 11.01s 2.25s
% Output : CNFRefutation 11.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 20
% Syntax : Number of formulae : 137 ( 137 unt; 5 def)
% Number of atoms : 263 ( 136 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 6 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 126 ( 0 sgn 126 !; 0 ?; 104 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : add(X0,X1) = add(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',commutativity_of_add) ).
fof(f2,axiom,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',commutativity_of_multiply) ).
fof(f3,axiom,
! [X2,X0,X1] : add(multiply(X0,X1),X2) = multiply(add(X0,X2),add(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',distributivity1) ).
fof(f4,axiom,
! [X2,X0,X1] : add(X0,multiply(X1,X2)) = multiply(add(X0,X1),add(X0,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',distributivity2) ).
fof(f5,axiom,
! [X2,X0,X1] : multiply(add(X0,X1),X2) = add(multiply(X0,X2),multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',distributivity3) ).
fof(f6,axiom,
! [X2,X0,X1] : multiply(X0,add(X1,X2)) = add(multiply(X0,X1),multiply(X0,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',distributivity4) ).
fof(f7,axiom,
! [X0] : add(X0,inverse(X0)) = multiplicative_identity,
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',additive_inverse1) ).
fof(f10,axiom,
! [X0] : multiply(X0,inverse(X0)) = additive_identity,
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',multiplicative_inverse1) ).
fof(f13,axiom,
! [X0] : multiply(X0,multiplicative_identity) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',multiplicative_id1) ).
fof(f14,axiom,
! [X0] : multiply(multiplicative_identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',multiplicative_id2) ).
fof(f15,axiom,
! [X0] : add(X0,additive_identity) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',additive_id1) ).
fof(f16,axiom,
! [X0] : add(additive_identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/BOO003-0.ax',additive_id2) ).
fof(f17,axiom,
add(a,b) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_plus_b_is_c) ).
fof(f18,axiom,
multiply(inverse(a),inverse(b)) = d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_inverse_times_b_inverse_is_d) ).
fof(f19,negated_conjecture,
inverse(c) != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_c_inverse_is_d) ).
fof(f20,plain,
d != inverse(c),
inference(reorient_equations,[],[f19]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] : add(X0,X1) = add(X1,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = multiply(X1,X0),
inference(cnf_transformation,[],[f2]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,X1),add(X2,X1)) = add(multiply(X0,X2),X1),
inference(cnf_transformation,[],[f3]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,X1),add(X0,X2)) = add(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] : add(multiply(X0,X1),multiply(X2,X1)) = multiply(add(X0,X2),X1),
inference(cnf_transformation,[],[f5]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i] : add(multiply(X0,X1),multiply(X0,X2)) = multiply(X0,add(X1,X2)),
inference(cnf_transformation,[],[f6]) ).
tcf(c_72,plain,
! [X0: $i] : add(X0,inverse(X0)) = multiplicative_identity,
inference(cnf_transformation,[],[f7]) ).
tcf(c_74,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = additive_identity,
inference(cnf_transformation,[],[f10]) ).
tcf(c_76,plain,
! [X0: $i] : multiply(X0,multiplicative_identity) = X0,
inference(cnf_transformation,[],[f13]) ).
tcf(c_77,plain,
! [X0: $i] : multiply(multiplicative_identity,X0) = X0,
inference(cnf_transformation,[],[f14]) ).
tcf(c_78,plain,
! [X0: $i] : add(X0,additive_identity) = X0,
inference(cnf_transformation,[],[f15]) ).
tcf(c_79,plain,
! [X0: $i] : add(additive_identity,X0) = X0,
inference(cnf_transformation,[],[f16]) ).
tcf(c_80,plain,
add(a,b) = c,
inference(cnf_transformation,[],[f17]) ).
tcf(c_81,plain,
multiply(inverse(a),inverse(b)) = d,
inference(cnf_transformation,[],[f18]) ).
tcf(c_82,negated_conjecture,
inverse(c) != d,
inference(cnf_transformation,[],[f20]) ).
tcf(c_135,definition,
iPr_def_10 = inverse(c),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_136,definition,
iPr_def_11 = inverse(a),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_137,definition,
iPr_def_12 = inverse(b),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_138,definition,
iPr_def_13 = multiply(iPr_def_11,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_139,definition,
iPr_def_14 = add(a,b),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_140,negated_conjecture,
iPr_def_10 != d,
inference(demodulation,[status(thm)],[c_82,c_135]) ).
tcf(c_141,plain,
! [X0: $i] : add(additive_identity,X0) = X0,
inference(demodulation,[status(thm)],[c_79]) ).
tcf(c_142,plain,
! [X0: $i] : add(X0,additive_identity) = X0,
inference(demodulation,[status(thm)],[c_78]) ).
tcf(c_143,plain,
! [X0: $i] : multiply(multiplicative_identity,X0) = X0,
inference(demodulation,[status(thm)],[c_77]) ).
tcf(c_144,plain,
! [X0: $i] : multiply(X0,multiplicative_identity) = X0,
inference(demodulation,[status(thm)],[c_76]) ).
tcf(c_146,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = additive_identity,
inference(demodulation,[status(thm)],[c_74]) ).
tcf(c_148,plain,
! [X0: $i] : add(X0,inverse(X0)) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_72]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i,X2: $i] : add(multiply(X0,X1),multiply(X0,X2)) = multiply(X0,add(X1,X2)),
inference(demodulation,[status(thm)],[c_71]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i,X2: $i] : add(multiply(X0,X1),multiply(X2,X1)) = multiply(add(X0,X2),X1),
inference(demodulation,[status(thm)],[c_70]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,X1),add(X0,X2)) = add(X0,multiply(X1,X2)),
inference(demodulation,[status(thm)],[c_69]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,X1),add(X2,X1)) = add(multiply(X0,X2),X1),
inference(demodulation,[status(thm)],[c_68]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = multiply(X1,X0),
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_154,plain,
! [X0: $i,X1: $i] : add(X0,X1) = add(X1,X0),
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_155,plain,
iPr_def_13 = d,
inference(demodulation,[status(thm)],[c_81,c_137,c_136,c_138]) ).
tcf(c_156,plain,
iPr_def_14 = c,
inference(demodulation,[status(thm)],[c_80,c_139]) ).
tcf(c_232,plain,
inverse(iPr_def_14) = iPr_def_10,
inference(demodulation,[status(thm)],[c_135,c_156]) ).
tcf(c_233,plain,
iPr_def_10 != iPr_def_13,
inference(demodulation,[status(thm)],[c_140,c_155]) ).
tcf(c_237,plain,
multiply(a,iPr_def_11) = additive_identity,
inference(superposition,[status(thm)],[c_136,c_146]) ).
tcf(c_238,plain,
multiply(b,iPr_def_12) = additive_identity,
inference(superposition,[status(thm)],[c_137,c_146]) ).
tcf(c_239,plain,
multiply(iPr_def_14,iPr_def_10) = additive_identity,
inference(superposition,[status(thm)],[c_232,c_146]) ).
tcf(c_240,plain,
inverse(multiplicative_identity) = additive_identity,
inference(superposition,[status(thm)],[c_146,c_143]) ).
tcf(c_242,plain,
add(a,iPr_def_11) = multiplicative_identity,
inference(superposition,[status(thm)],[c_136,c_148]) ).
tcf(c_243,plain,
add(b,iPr_def_12) = multiplicative_identity,
inference(superposition,[status(thm)],[c_137,c_148]) ).
tcf(c_244,plain,
add(iPr_def_14,iPr_def_10) = multiplicative_identity,
inference(superposition,[status(thm)],[c_232,c_148]) ).
tcf(c_245,plain,
inverse(additive_identity) = multiplicative_identity,
inference(superposition,[status(thm)],[c_148,c_141]) ).
tcf(c_257,plain,
multiply(iPr_def_12,iPr_def_11) = iPr_def_13,
inference(superposition,[status(thm)],[c_153,c_138]) ).
tcf(c_270,plain,
! [X0: $i,X1: $i] : multiply(X0,add(inverse(X0),X1)) = add(additive_identity,multiply(X0,X1)),
inference(superposition,[status(thm)],[c_146,c_149]) ).
tcf(c_273,plain,
! [X0: $i] : add(iPr_def_13,multiply(iPr_def_11,X0)) = multiply(iPr_def_11,add(iPr_def_12,X0)),
inference(superposition,[status(thm)],[c_138,c_149]) ).
tcf(c_276,plain,
! [X0: $i,X1: $i] : multiply(X0,add(X1,inverse(X0))) = add(multiply(X0,X1),additive_identity),
inference(superposition,[status(thm)],[c_146,c_149]) ).
tcf(c_289,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X1,X0)) = multiply(add(multiplicative_identity,X1),X0),
inference(superposition,[status(thm)],[c_143,c_150]) ).
tcf(c_324,plain,
! [X0: $i] : add(a,multiply(b,X0)) = multiply(iPr_def_14,add(a,X0)),
inference(superposition,[status(thm)],[c_139,c_151]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i] : add(X0,multiply(inverse(X0),X1)) = multiply(multiplicative_identity,add(X0,X1)),
inference(superposition,[status(thm)],[c_148,c_151]) ).
tcf(c_330,plain,
! [X0: $i,X1: $i] : multiply(X0,add(X0,X1)) = add(X0,multiply(additive_identity,X1)),
inference(superposition,[status(thm)],[c_142,c_151]) ).
tcf(c_337,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X1,inverse(X0))) = multiply(add(X0,X1),multiplicative_identity),
inference(superposition,[status(thm)],[c_148,c_151]) ).
tcf(c_396,plain,
add(iPr_def_12,b) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_243,c_154]) ).
tcf(c_397,plain,
add(iPr_def_11,a) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_242,c_154]) ).
tcf(c_398,plain,
multiply(iPr_def_12,b) = additive_identity,
inference(demodulation,[status(thm)],[c_238,c_153]) ).
tcf(c_399,plain,
multiply(iPr_def_11,a) = additive_identity,
inference(demodulation,[status(thm)],[c_237,c_153]) ).
tcf(c_411,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X1,inverse(X0))) = add(X0,X1),
inference(demodulation,[status(thm)],[c_337,c_144]) ).
tcf(c_412,plain,
! [X0: $i,X1: $i] : add(X0,multiply(inverse(X0),X1)) = add(X0,X1),
inference(demodulation,[status(thm)],[c_329,c_143]) ).
tcf(c_413,plain,
! [X0: $i,X1: $i] : multiply(X0,add(X1,inverse(X0))) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_276,c_142]) ).
tcf(c_414,plain,
! [X0: $i,X1: $i] : multiply(X0,add(inverse(X0),X1)) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_270,c_141]) ).
tcf(c_554,plain,
! [X0: $i] : add(additive_identity,multiply(X0,iPr_def_10)) = multiply(add(iPr_def_14,X0),iPr_def_10),
inference(superposition,[status(thm)],[c_239,c_150]) ).
tcf(c_558,plain,
! [X0: $i] : add(multiply(iPr_def_14,X0),iPr_def_10) = multiply(multiplicative_identity,add(X0,iPr_def_10)),
inference(superposition,[status(thm)],[c_244,c_152]) ).
tcf(c_568,plain,
! [X0: $i] : add(iPr_def_12,multiply(X0,b)) = multiply(add(iPr_def_12,X0),multiplicative_identity),
inference(superposition,[status(thm)],[c_396,c_151]) ).
tcf(c_572,plain,
! [X0: $i] : add(iPr_def_11,multiply(X0,a)) = multiply(add(iPr_def_11,X0),multiplicative_identity),
inference(superposition,[status(thm)],[c_397,c_151]) ).
tcf(c_586,plain,
! [X0: $i] : add(X0,X0) = add(X0,additive_identity),
inference(superposition,[status(thm)],[c_146,c_411]) ).
tcf(c_604,plain,
! [X0: $i] : add(X0,inverse(X0)) = add(X0,multiplicative_identity),
inference(superposition,[status(thm)],[c_144,c_412]) ).
tcf(c_609,plain,
! [X0: $i] : add(multiplicative_identity,multiply(additive_identity,X0)) = add(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_240,c_412]) ).
tcf(c_620,plain,
! [X0: $i] : multiply(X0,X0) = multiply(X0,multiplicative_identity),
inference(superposition,[status(thm)],[c_148,c_413]) ).
tcf(c_622,plain,
! [X0: $i] : multiply(a,add(X0,iPr_def_11)) = multiply(a,X0),
inference(superposition,[status(thm)],[c_136,c_413]) ).
tcf(c_624,plain,
! [X0: $i] : multiply(additive_identity,add(X0,multiplicative_identity)) = multiply(additive_identity,X0),
inference(superposition,[status(thm)],[c_245,c_413]) ).
tcf(c_643,plain,
! [X0: $i] : multiply(b,add(iPr_def_12,X0)) = multiply(b,X0),
inference(superposition,[status(thm)],[c_137,c_414]) ).
tcf(c_698,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X0,X1)) = multiply(add(multiplicative_identity,X1),X0),
inference(superposition,[status(thm)],[c_153,c_289]) ).
tcf(c_776,plain,
multiply(add(multiplicative_identity,b),a) = multiply(iPr_def_14,add(a,a)),
inference(superposition,[status(thm)],[c_324,c_289]) ).
tcf(c_780,plain,
! [X0: $i,X1: $i] : multiply(X0,add(X1,X0)) = add(X0,multiply(additive_identity,X1)),
inference(superposition,[status(thm)],[c_154,c_330]) ).
tcf(c_824,plain,
! [X0: $i] : multiply(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_620,c_144]) ).
tcf(c_825,plain,
! [X0: $i] : add(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_586,c_142]) ).
tcf(c_827,plain,
! [X0: $i] : add(X0,multiplicative_identity) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_604,c_148]) ).
tcf(c_850,plain,
! [X0: $i] : multiply(additive_identity,X0) = multiply(additive_identity,multiplicative_identity),
inference(demodulation,[status(thm)],[c_624,c_827]) ).
tcf(c_851,plain,
! [X0: $i] : multiply(additive_identity,X0) = additive_identity,
inference(demodulation,[status(thm)],[c_850,c_144]) ).
tcf(c_852,plain,
! [X0: $i] : add(multiplicative_identity,X0) = add(multiplicative_identity,additive_identity),
inference(demodulation,[status(thm)],[c_609,c_851]) ).
tcf(c_853,plain,
! [X0: $i] : add(multiplicative_identity,X0) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_852,c_142]) ).
tcf(c_871,plain,
! [X0: $i,X1: $i] : multiply(X0,add(X1,X0)) = add(X0,additive_identity),
inference(demodulation,[status(thm)],[c_780,c_851]) ).
tcf(c_872,plain,
! [X0: $i,X1: $i] : multiply(X0,add(X1,X0)) = X0,
inference(demodulation,[status(thm)],[c_871,c_142]) ).
tcf(c_873,plain,
multiply(multiplicative_identity,a) = multiply(iPr_def_14,a),
inference(demodulation,[status(thm)],[c_776,c_825,c_853]) ).
tcf(c_874,plain,
multiply(iPr_def_14,a) = a,
inference(demodulation,[status(thm)],[c_873,c_143]) ).
tcf(c_886,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X0,X1)) = multiply(multiplicative_identity,X0),
inference(demodulation,[status(thm)],[c_698,c_853]) ).
tcf(c_887,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_886,c_143]) ).
tcf(c_901,plain,
! [X0: $i] : add(iPr_def_11,multiply(X0,a)) = add(iPr_def_11,X0),
inference(demodulation,[status(thm)],[c_572,c_144]) ).
tcf(c_905,plain,
! [X0: $i] : add(iPr_def_12,multiply(X0,b)) = add(iPr_def_12,X0),
inference(demodulation,[status(thm)],[c_568,c_144]) ).
tcf(c_915,plain,
! [X0: $i] : add(iPr_def_10,multiply(iPr_def_14,X0)) = add(X0,iPr_def_10),
inference(demodulation,[status(thm)],[c_558,c_154,c_143]) ).
tcf(c_919,plain,
! [X0: $i] : multiply(iPr_def_10,add(iPr_def_14,X0)) = multiply(X0,iPr_def_10),
inference(demodulation,[status(thm)],[c_554,c_153,c_141]) ).
tcf(c_1620,plain,
multiply(iPr_def_11,add(iPr_def_12,iPr_def_11)) = add(iPr_def_13,iPr_def_11),
inference(superposition,[status(thm)],[c_824,c_273]) ).
tcf(c_1854,plain,
add(iPr_def_13,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_1620,c_872]) ).
tcf(c_2224,plain,
multiply(b,iPr_def_14) = b,
inference(superposition,[status(thm)],[c_139,c_872]) ).
tcf(c_2347,plain,
add(iPr_def_12,iPr_def_13) = iPr_def_12,
inference(superposition,[status(thm)],[c_257,c_887]) ).
tcf(c_2391,plain,
multiply(iPr_def_14,b) = b,
inference(demodulation,[status(thm)],[c_2224,c_153]) ).
tcf(c_2715,plain,
multiply(a,iPr_def_11) = multiply(a,iPr_def_13),
inference(superposition,[status(thm)],[c_1854,c_622]) ).
tcf(c_2902,plain,
multiply(b,iPr_def_12) = multiply(b,iPr_def_13),
inference(superposition,[status(thm)],[c_2347,c_643]) ).
tcf(c_2920,plain,
multiply(iPr_def_13,b) = additive_identity,
inference(demodulation,[status(thm)],[c_2902,c_153,c_398]) ).
tcf(c_2921,plain,
multiply(iPr_def_13,a) = additive_identity,
inference(demodulation,[status(thm)],[c_2715,c_153,c_399]) ).
tcf(c_3473,plain,
! [X0: $i] : add(multiply(iPr_def_13,X0),additive_identity) = multiply(iPr_def_13,add(X0,b)),
inference(superposition,[status(thm)],[c_2920,c_149]) ).
tcf(c_3692,plain,
! [X0: $i] : multiply(iPr_def_13,add(X0,b)) = multiply(iPr_def_13,X0),
inference(demodulation,[status(thm)],[c_3473,c_142]) ).
tcf(c_4302,plain,
add(iPr_def_11,a) = add(iPr_def_11,iPr_def_14),
inference(superposition,[status(thm)],[c_874,c_901]) ).
tcf(c_4439,plain,
add(iPr_def_14,iPr_def_11) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_4302,c_154,c_397]) ).
tcf(c_4545,plain,
! [X0: $i] : add(iPr_def_14,multiply(iPr_def_11,X0)) = multiply(multiplicative_identity,add(iPr_def_14,X0)),
inference(superposition,[status(thm)],[c_4439,c_151]) ).
tcf(c_4641,plain,
add(iPr_def_12,b) = add(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_2391,c_905]) ).
tcf(c_4810,plain,
add(iPr_def_14,iPr_def_12) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_4641,c_154,c_396]) ).
tcf(c_4828,plain,
! [X0: $i] : add(iPr_def_14,multiply(iPr_def_11,X0)) = add(iPr_def_14,X0),
inference(demodulation,[status(thm)],[c_4545,c_143]) ).
tcf(c_5358,plain,
multiply(iPr_def_13,a) = multiply(iPr_def_13,iPr_def_14),
inference(superposition,[status(thm)],[c_139,c_3692]) ).
tcf(c_5501,plain,
add(iPr_def_14,iPr_def_12) = add(iPr_def_14,iPr_def_13),
inference(superposition,[status(thm)],[c_138,c_4828]) ).
tcf(c_5533,plain,
add(iPr_def_14,iPr_def_13) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_5501,c_4810]) ).
tcf(c_5536,plain,
multiply(iPr_def_14,iPr_def_13) = additive_identity,
inference(demodulation,[status(thm)],[c_5358,c_153,c_2921]) ).
tcf(c_5825,plain,
multiply(iPr_def_10,multiplicative_identity) = multiply(iPr_def_13,iPr_def_10),
inference(superposition,[status(thm)],[c_5533,c_919]) ).
tcf(c_5837,plain,
add(iPr_def_10,additive_identity) = add(iPr_def_13,iPr_def_10),
inference(superposition,[status(thm)],[c_5536,c_915]) ).
tcf(c_5927,plain,
add(iPr_def_13,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_5837,c_142]) ).
tcf(c_5928,plain,
multiply(iPr_def_13,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_5825,c_144]) ).
tcf(c_6122,plain,
add(iPr_def_13,iPr_def_10) = iPr_def_13,
inference(superposition,[status(thm)],[c_5928,c_887]) ).
tcf(c_6478,plain,
iPr_def_10 = iPr_def_13,
inference(superposition,[status(thm)],[c_6122,c_5927]) ).
tcf(c_6673,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_6478,c_233]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO014-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.36 % Computer : n002.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 06:34:49 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.39 Running UEQ theorem proving
% 0.09/0.39 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.40
% 0.09/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.40
% 0.09/0.40 % Detected problem language: tptp
% 0.09/0.42 % Proving...
% 11.01/2.25 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 11.01/2.25 % SZS status Started for theBenchmark.p
% 11.01/2.25 % SZS status Unsatisfiable for theBenchmark.p
% 11.01/2.25
% 11.01/2.25 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 11.01/2.25
% 11.01/2.25 % ------ iProver source info
% 11.01/2.25
% 11.01/2.25 % git: date: 2026-07-19 20:42:38 +0200
% 11.01/2.25 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 11.01/2.25 % git: non_committed_changes: false
% 11.01/2.25
% 11.01/2.25 % ------ Parsing...% successful
% 11.01/2.25
% 11.01/2.25
% 11.01/2.25 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 11.01/2.25
% 11.01/2.25 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 11.01/2.25
% 11.01/2.25 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 11.01/2.25
% 11.01/2.25 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 11.01/2.25 % ------ Proving...
% 11.01/2.25 % ------ Problem Properties
% 11.01/2.25
% 11.01/2.25 %
% 11.01/2.25 % clauses 22
% 11.01/2.25 % conjectures 1
% 11.01/2.25 % EPR 3
% 11.01/2.25 % Horn 22
% 11.01/2.25 % unary 22
% 11.01/2.25 % binary 0
% 11.01/2.25 % lits 22
% 11.01/2.25 % lits eq 22
% 11.01/2.25 % fd_pure 0
% 11.01/2.25 % fd_pseudo 0
% 11.01/2.25 % fd_cond 0
% 11.01/2.25 % fd_pseudo_cond 0
% 11.01/2.25 % AC symbols 0
% 11.01/2.25
% 11.01/2.25 % ------ Input Options Time Limit: Unbounded
% 11.01/2.25
% 11.01/2.25
% 11.01/2.25 % ------
% 11.01/2.25 % Current options:
% 11.01/2.25 % ------
% 11.01/2.25
% 11.01/2.25
% 11.01/2.25 %
% 11.01/2.25
% 11.01/2.25 % ------ Proving...
% 11.01/2.25 %
% 11.01/2.25
% 11.01/2.25 % SZS status Unsatisfiable for theBenchmark.p
% 11.01/2.25
% 11.01/2.25 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 11.01/2.26
% 11.01/2.26
%------------------------------------------------------------------------------