%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : BOO015-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n019.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:14 PM UTC 2026
% Result : Unsatisfiable 6.15s 7.29s
% Output : CNFRefutation 6.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 20
% Syntax : Number of formulae : 229 ( 211 unt; 5 def)
% Number of atoms : 1142 ( 218 equ)
% Maximal formula atoms : 5 ( 4 avg)
% Number of connectives : 113 ( 59 ~; 54 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 6 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-1 aty)
% Number of variables : 254 ( 0 sgn 254 !; 0 ?; 214 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X2,X0,X1] :
( sum(X1,X0,X2)
| ~ sum(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',commutativity_of_addition) ).
fof(f4,axiom,
! [X2,X0,X1] :
( product(X1,X0,X2)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',commutativity_of_multiplication) ).
fof(f5,axiom,
! [X0] : sum(additive_identity,X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',additive_identity1) ).
fof(f6,axiom,
! [X0] : sum(X0,additive_identity,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',additive_identity2) ).
fof(f7,axiom,
! [X0] : product(multiplicative_identity,X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',multiplicative_identity1) ).
fof(f8,axiom,
! [X0] : product(X0,multiplicative_identity,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',multiplicative_identity2) ).
fof(f10,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( product(X0,X5,X6)
| ~ sum(X2,X4,X6)
| ~ sum(X1,X3,X5)
| ~ product(X0,X3,X4)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',distributivity2) ).
fof(f12,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( product(X5,X1,X6)
| ~ sum(X2,X4,X6)
| ~ sum(X0,X3,X5)
| ~ product(X3,X1,X4)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',distributivity4) ).
fof(f14,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( sum(X0,X5,X6)
| ~ product(X2,X4,X6)
| ~ product(X1,X3,X5)
| ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',distributivity6) ).
fof(f16,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( sum(X5,X1,X6)
| ~ product(X2,X4,X6)
| ~ product(X0,X3,X5)
| ~ sum(X3,X1,X4)
| ~ sum(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',distributivity8) ).
fof(f18,axiom,
! [X0] : sum(X0,inverse(X0),multiplicative_identity),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',additive_inverse2) ).
fof(f20,axiom,
! [X0] : product(X0,inverse(X0),additive_identity),
file('/export/starexec/sandbox2/benchmark/Axioms/BOO002-0.ax',multiplicative_inverse2) ).
fof(f23,negated_conjecture,
product(x,y,x_times_y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_times_y) ).
fof(f24,negated_conjecture,
sum(inverse(x),inverse(y),x_inverse_plus_y_inverse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_inverse_plus_y_inverse) ).
fof(f25,negated_conjecture,
inverse(x_times_y) != x_inverse_plus_y_inverse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_equation) ).
fof(f26,plain,
x_inverse_plus_y_inverse != inverse(x_times_y),
inference(reorient_equations,[],[f25]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i] :
( sum(X1,X0,X2)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i] :
( product(X1,X0,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_78,plain,
! [X0: $i] : sum(additive_identity,X0,X0),
inference(cnf_transformation,[],[f5]) ).
tcf(c_79,plain,
! [X0: $i] : sum(X0,additive_identity,X0),
inference(cnf_transformation,[],[f6]) ).
tcf(c_80,plain,
! [X0: $i] : product(multiplicative_identity,X0,X0),
inference(cnf_transformation,[],[f7]) ).
tcf(c_81,plain,
! [X0: $i] : product(X0,multiplicative_identity,X0),
inference(cnf_transformation,[],[f8]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( product(X0,X5,X6)
| ~ sum(X2,X4,X6)
| ~ sum(X1,X3,X5)
| ~ product(X0,X3,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( product(X5,X1,X6)
| ~ sum(X2,X4,X6)
| ~ sum(X0,X3,X5)
| ~ product(X3,X1,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( sum(X6,X2,X5)
| ~ sum(X6,X1,X4)
| ~ sum(X6,X0,X3)
| ~ product(X3,X4,X5)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( sum(X2,X6,X5)
| ~ sum(X1,X6,X4)
| ~ sum(X0,X6,X3)
| ~ product(X3,X4,X5)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_91,plain,
! [X0: $i] : sum(X0,inverse(X0),multiplicative_identity),
inference(cnf_transformation,[],[f18]) ).
tcf(c_93,plain,
! [X0: $i] : product(X0,inverse(X0),additive_identity),
inference(cnf_transformation,[],[f20]) ).
tcf(c_96,negated_conjecture,
product(x,y,x_times_y),
inference(cnf_transformation,[],[f23]) ).
tcf(c_97,negated_conjecture,
sum(inverse(x),inverse(y),x_inverse_plus_y_inverse),
inference(cnf_transformation,[],[f24]) ).
tcf(c_98,negated_conjecture,
inverse(x_times_y) != x_inverse_plus_y_inverse,
inference(cnf_transformation,[],[f26]) ).
tcf(c_110,plain,
multiply(x,y) = x_times_y,
inference(well_definedness,[status(thm)],[c_96]) ).
tcf(c_111,plain,
add(inverse(x),inverse(y)) = x_inverse_plus_y_inverse,
inference(well_definedness,[status(thm)],[c_97]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( add(X1,X0) = X2 )
| ( add(X0,X1) != X2 ) ),
inference(well_definedness,[status(thm)],[c_76]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X1,X0) = X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(well_definedness,[status(thm)],[c_77]) ).
tcf(c_118,plain,
! [X0: $i] : add(additive_identity,X0) = X0,
inference(well_definedness,[status(thm)],[c_78]) ).
tcf(c_119,plain,
! [X0: $i] : add(X0,additive_identity) = X0,
inference(well_definedness,[status(thm)],[c_79]) ).
tcf(c_120,plain,
! [X0: $i] : multiply(multiplicative_identity,X0) = X0,
inference(well_definedness,[status(thm)],[c_80]) ).
tcf(c_121,plain,
! [X0: $i] : multiply(X0,multiplicative_identity) = X0,
inference(well_definedness,[status(thm)],[c_81]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( multiply(X6,X2) = X5 )
| ( multiply(X6,X1) != X4 )
| ( multiply(X6,X0) != X3 )
| ( add(X3,X4) != X5 )
| ( add(X0,X1) != X2 ) ),
inference(well_definedness,[status(thm)],[c_83]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( multiply(X2,X6) = X5 )
| ( multiply(X1,X6) != X4 )
| ( multiply(X0,X6) != X3 )
| ( add(X3,X4) != X5 )
| ( add(X0,X1) != X2 ) ),
inference(well_definedness,[status(thm)],[c_85]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( add(X0,X5) = X6 )
| ( multiply(X2,X4) != X6 )
| ( multiply(X1,X3) != X5 )
| ( add(X0,X3) != X4 )
| ( add(X0,X1) != X2 ) ),
inference(well_definedness,[status(thm)],[c_87]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( add(X5,X1) = X6 )
| ( multiply(X2,X4) != X6 )
| ( multiply(X0,X3) != X5 )
| ( add(X3,X1) != X4 )
| ( add(X0,X1) != X2 ) ),
inference(well_definedness,[status(thm)],[c_89]) ).
tcf(c_139,plain,
! [X0: $i] : add(X0,inverse(X0)) = multiplicative_identity,
inference(well_definedness,[status(thm)],[c_91]) ).
tcf(c_141,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = additive_identity,
inference(well_definedness,[status(thm)],[c_93]) ).
tcf(c_283,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = multiply(X1,X0),
inference(unflattening,[status(thm)],[c_116]) ).
tcf(c_285,plain,
! [X0: $i,X1: $i] : add(X0,X1) = add(X1,X0),
inference(unflattening,[status(thm)],[c_114]) ).
tcf(c_289,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,X1),add(X2,X1)) = add(multiply(X0,X2),X1),
inference(unflattening,[status(thm)],[c_136]) ).
tcf(c_291,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,X1),add(X0,X2)) = add(X0,multiply(X1,X2)),
inference(unflattening,[status(thm)],[c_132]) ).
tcf(c_293,plain,
! [X0: $i,X1: $i,X2: $i] : add(multiply(X0,X1),multiply(X2,X1)) = multiply(add(X0,X2),X1),
inference(unflattening,[status(thm)],[c_128]) ).
tcf(c_295,plain,
! [X0: $i,X1: $i,X2: $i] : add(multiply(X0,X1),multiply(X0,X2)) = multiply(X0,add(X1,X2)),
inference(unflattening,[status(thm)],[c_124]) ).
tcf(c_341,definition,
iPr_def_10 = inverse(x),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_342,definition,
iPr_def_11 = inverse(y),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_343,definition,
iPr_def_12 = add(iPr_def_10,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_344,definition,
iPr_def_13 = multiply(x,y),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_345,definition,
iPr_def_14 = inverse(x_times_y),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_346,plain,
iPr_def_12 = x_inverse_plus_y_inverse,
inference(demodulation,[status(thm)],[c_111,c_342,c_341,c_343]) ).
tcf(c_347,plain,
iPr_def_13 = x_times_y,
inference(demodulation,[status(thm)],[c_110,c_344]) ).
tcf(c_348,negated_conjecture,
iPr_def_14 != x_inverse_plus_y_inverse,
inference(demodulation,[status(thm)],[c_98,c_345]) ).
tcf(c_420,plain,
iPr_def_12 != iPr_def_14,
inference(light_normalisation,[status(thm)],[c_348,c_346]) ).
tcf(c_421,plain,
inverse(iPr_def_13) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_345,c_347]) ).
tcf(c_423,plain,
add(x,iPr_def_10) = multiplicative_identity,
inference(superposition,[status(thm)],[c_341,c_139]) ).
tcf(c_424,plain,
add(y,iPr_def_11) = multiplicative_identity,
inference(superposition,[status(thm)],[c_342,c_139]) ).
tcf(c_425,plain,
add(iPr_def_13,iPr_def_14) = multiplicative_identity,
inference(superposition,[status(thm)],[c_421,c_139]) ).
tcf(c_428,plain,
add(iPr_def_10,x) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_423,c_285]) ).
tcf(c_429,plain,
add(iPr_def_11,y) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_424,c_285]) ).
tcf(c_431,plain,
multiply(x,iPr_def_10) = additive_identity,
inference(superposition,[status(thm)],[c_341,c_141]) ).
tcf(c_432,plain,
multiply(y,iPr_def_11) = additive_identity,
inference(superposition,[status(thm)],[c_342,c_141]) ).
tcf(c_434,plain,
multiply(iPr_def_13,iPr_def_14) = additive_identity,
inference(superposition,[status(thm)],[c_421,c_141]) ).
tcf(c_438,plain,
multiply(iPr_def_10,x) = additive_identity,
inference(demodulation,[status(thm)],[c_431,c_283]) ).
tcf(c_439,plain,
multiply(iPr_def_11,y) = additive_identity,
inference(demodulation,[status(thm)],[c_432,c_283]) ).
tcf(c_456,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(multiply(X0,X1),multiply(X0,X2)),add(multiply(X2,X1),multiply(X2,X2))) = add(multiply(X0,X1),X2),
inference(demodulation,[status(thm)],[c_289,c_293,c_295]) ).
tcf(c_462,plain,
! [X0: $i] : add(add(iPr_def_13,multiply(x,X0)),add(multiply(X0,y),multiply(X0,X0))) = add(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_344,c_456]) ).
tcf(c_466,plain,
! [X0: $i,X1: $i] : add(add(additive_identity,multiply(X0,X1)),add(multiply(X1,inverse(X0)),multiply(X1,X1))) = add(additive_identity,X1),
inference(superposition,[status(thm)],[c_141,c_456]) ).
tcf(c_477,plain,
! [X0: $i] : add(add(multiply(iPr_def_10,X0),additive_identity),add(multiply(x,X0),multiply(x,x))) = add(multiply(iPr_def_10,X0),x),
inference(superposition,[status(thm)],[c_438,c_456]) ).
tcf(c_486,plain,
! [X0: $i,X1: $i] : add(add(multiply(X0,inverse(X1)),multiply(X0,X1)),add(additive_identity,multiply(X1,X1))) = add(multiply(X0,inverse(X1)),X1),
inference(superposition,[status(thm)],[c_141,c_456]) ).
tcf(c_487,plain,
! [X0: $i] : add(add(multiply(X0,iPr_def_14),multiply(X0,iPr_def_13)),add(additive_identity,multiply(iPr_def_13,iPr_def_13))) = add(multiply(X0,iPr_def_14),iPr_def_13),
inference(superposition,[status(thm)],[c_434,c_456]) ).
tcf(c_489,plain,
! [X0: $i] : add(add(multiply(X0,y),multiply(X0,iPr_def_11)),add(additive_identity,multiply(iPr_def_11,iPr_def_11))) = add(multiply(X0,y),iPr_def_11),
inference(superposition,[status(thm)],[c_439,c_456]) ).
tcf(c_521,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(multiply(X0,X0),multiply(X0,X1)),add(multiply(X2,X0),multiply(X2,X1))) = add(X0,multiply(X2,X1)),
inference(demodulation,[status(thm)],[c_291,c_293,c_295]) ).
tcf(c_547,plain,
! [X0: $i] : add(add(multiply(x,x),multiply(x,X0)),add(additive_identity,multiply(iPr_def_10,X0))) = add(x,multiply(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_438,c_521]) ).
tcf(c_577,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),multiply(inverse(X0),X1)) = multiply(multiplicative_identity,X1),
inference(superposition,[status(thm)],[c_139,c_293]) ).
tcf(c_578,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),multiply(iPr_def_11,X0)) = multiply(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_343,c_293]) ).
tcf(c_579,plain,
! [X0: $i] : add(multiply(iPr_def_13,X0),multiply(iPr_def_14,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_425,c_293]) ).
tcf(c_580,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),multiply(x,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_428,c_293]) ).
tcf(c_581,plain,
! [X0: $i] : add(multiply(iPr_def_11,X0),multiply(y,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_429,c_293]) ).
tcf(c_593,plain,
! [X0: $i,X1: $i] : add(multiply(X0,inverse(add(X0,X1))),multiply(X1,inverse(add(X0,X1)))) = additive_identity,
inference(superposition,[status(thm)],[c_293,c_141]) ).
tcf(c_600,plain,
! [X0: $i] : add(multiply(iPr_def_11,X0),multiply(y,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_581,c_120]) ).
tcf(c_601,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),multiply(x,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_580,c_120]) ).
tcf(c_602,plain,
! [X0: $i] : add(multiply(iPr_def_13,X0),multiply(iPr_def_14,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_579,c_120]) ).
tcf(c_620,plain,
add(add(iPr_def_13,multiply(x,iPr_def_12)),add(multiply(iPr_def_12,y),add(multiply(iPr_def_10,iPr_def_12),multiply(iPr_def_11,iPr_def_12)))) = add(iPr_def_13,iPr_def_12),
inference(superposition,[status(thm)],[c_578,c_462]) ).
tcf(c_633,plain,
! [X0: $i,X1: $i] : add(multiply(X0,additive_identity),multiply(X0,X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_118,c_295]) ).
tcf(c_635,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),multiply(X0,inverse(X1))) = multiply(X0,multiplicative_identity),
inference(superposition,[status(thm)],[c_139,c_295]) ).
tcf(c_636,plain,
! [X0: $i] : add(multiply(X0,iPr_def_10),multiply(X0,iPr_def_11)) = multiply(X0,iPr_def_12),
inference(superposition,[status(thm)],[c_343,c_295]) ).
tcf(c_637,plain,
! [X0: $i] : add(multiply(X0,iPr_def_13),multiply(X0,iPr_def_14)) = multiply(X0,multiplicative_identity),
inference(superposition,[status(thm)],[c_425,c_295]) ).
tcf(c_639,plain,
! [X0: $i] : add(multiply(X0,iPr_def_11),multiply(X0,y)) = multiply(X0,multiplicative_identity),
inference(superposition,[status(thm)],[c_429,c_295]) ).
tcf(c_659,plain,
! [X0: $i] : add(multiply(X0,iPr_def_11),multiply(X0,y)) = X0,
inference(light_normalisation,[status(thm)],[c_639,c_121]) ).
tcf(c_661,plain,
! [X0: $i] : add(multiply(X0,iPr_def_13),multiply(X0,iPr_def_14)) = X0,
inference(light_normalisation,[status(thm)],[c_637,c_121]) ).
tcf(c_662,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),multiply(X0,inverse(X1))) = X0,
inference(light_normalisation,[status(thm)],[c_635,c_121]) ).
tcf(c_672,plain,
add(additive_identity,multiply(y,inverse(iPr_def_11))) = inverse(iPr_def_11),
inference(superposition,[status(thm)],[c_141,c_600]) ).
tcf(c_673,plain,
add(additive_identity,multiply(y,y)) = y,
inference(superposition,[status(thm)],[c_439,c_600]) ).
tcf(c_678,plain,
add(multiply(iPr_def_11,inverse(y)),additive_identity) = inverse(y),
inference(superposition,[status(thm)],[c_141,c_600]) ).
tcf(c_681,plain,
add(multiply(iPr_def_11,iPr_def_11),additive_identity) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_678,c_342]) ).
tcf(c_682,plain,
multiply(y,y) = y,
inference(demodulation,[status(thm)],[c_673,c_118]) ).
tcf(c_724,plain,
! [X0: $i] : add(X0,multiply(iPr_def_13,iPr_def_13)) = add(iPr_def_13,multiply(X0,iPr_def_14)),
inference(demodulation,[status(thm)],[c_487,c_118,c_285,c_661]) ).
tcf(c_731,plain,
add(iPr_def_13,multiply(iPr_def_13,iPr_def_13)) = add(iPr_def_13,additive_identity),
inference(superposition,[status(thm)],[c_434,c_724]) ).
tcf(c_747,plain,
add(iPr_def_13,multiply(iPr_def_13,iPr_def_13)) = iPr_def_13,
inference(demodulation,[status(thm)],[c_731,c_119]) ).
tcf(c_762,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),add(multiply(X1,inverse(X0)),multiply(X1,X1))) = X1,
inference(demodulation,[status(thm)],[c_466,c_118]) ).
tcf(c_789,plain,
! [X0: $i] : add(multiply(iPr_def_13,X0),add(multiply(X0,iPr_def_14),multiply(X0,X0))) = X0,
inference(superposition,[status(thm)],[c_421,c_762]) ).
tcf(c_843,plain,
! [X0: $i] : add(multiply(X0,iPr_def_10),multiply(X0,iPr_def_11)) = multiply(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_636,c_283]) ).
tcf(c_931,plain,
multiply(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_681,c_119]) ).
tcf(c_953,plain,
add(additive_identity,multiply(x,inverse(iPr_def_10))) = inverse(iPr_def_10),
inference(superposition,[status(thm)],[c_141,c_601]) ).
tcf(c_954,plain,
add(additive_identity,multiply(x,x)) = x,
inference(superposition,[status(thm)],[c_438,c_601]) ).
tcf(c_961,plain,
add(multiply(iPr_def_10,inverse(x)),additive_identity) = inverse(x),
inference(superposition,[status(thm)],[c_141,c_601]) ).
tcf(c_965,plain,
add(multiply(iPr_def_10,iPr_def_10),additive_identity) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_961,c_341]) ).
tcf(c_980,plain,
! [X0: $i] : add(multiply(iPr_def_13,X0),add(multiply(X0,X0),multiply(X0,iPr_def_14))) = X0,
inference(superposition,[status(thm)],[c_285,c_789]) ).
tcf(c_1130,plain,
multiply(x,x) = x,
inference(demodulation,[status(thm)],[c_954,c_118]) ).
tcf(c_1170,plain,
multiply(iPr_def_10,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_965,c_119]) ).
tcf(c_1223,plain,
add(multiply(iPr_def_13,iPr_def_13),add(multiply(iPr_def_13,iPr_def_13),additive_identity)) = iPr_def_13,
inference(superposition,[status(thm)],[c_434,c_980]) ).
tcf(c_1236,plain,
add(multiply(iPr_def_13,iPr_def_13),multiply(iPr_def_13,iPr_def_13)) = iPr_def_13,
inference(demodulation,[status(thm)],[c_1223,c_119]) ).
tcf(c_1242,plain,
add(iPr_def_13,multiply(iPr_def_13,iPr_def_13)) = add(iPr_def_13,iPr_def_13),
inference(superposition,[status(thm)],[c_1236,c_521]) ).
tcf(c_1243,plain,
add(iPr_def_13,iPr_def_13) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_1242,c_747]) ).
tcf(c_1428,plain,
add(additive_identity,multiply(iPr_def_14,iPr_def_14)) = iPr_def_14,
inference(superposition,[status(thm)],[c_434,c_602]) ).
tcf(c_1439,plain,
! [X0: $i] : add(multiply(X0,iPr_def_13),multiply(X0,iPr_def_13)) = multiply(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_1243,c_295]) ).
tcf(c_1441,plain,
multiply(iPr_def_13,iPr_def_13) = iPr_def_13,
inference(demodulation,[status(thm)],[c_1236,c_1439]) ).
tcf(c_1446,plain,
! [X0: $i] : add(iPr_def_13,multiply(X0,iPr_def_14)) = add(X0,iPr_def_13),
inference(demodulation,[status(thm)],[c_724,c_1441]) ).
tcf(c_1506,plain,
multiply(iPr_def_14,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_1428,c_118]) ).
tcf(c_1528,plain,
add(add(iPr_def_13,multiply(x,iPr_def_14)),add(multiply(iPr_def_14,y),iPr_def_14)) = add(iPr_def_13,iPr_def_14),
inference(superposition,[status(thm)],[c_1506,c_462]) ).
tcf(c_1538,plain,
add(add(iPr_def_13,multiply(x,iPr_def_14)),add(multiply(iPr_def_14,y),iPr_def_14)) = multiplicative_identity,
inference(light_normalisation,[status(thm)],[c_1528,c_425]) ).
tcf(c_1541,plain,
add(add(iPr_def_13,x),add(iPr_def_14,multiply(iPr_def_14,y))) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_1538,c_285,c_1446]) ).
tcf(c_1622,plain,
! [X0: $i] : add(add(multiply(iPr_def_10,X0),additive_identity),add(multiply(x,X0),x)) = add(multiply(iPr_def_10,X0),x),
inference(light_normalisation,[status(thm)],[c_477,c_1130]) ).
tcf(c_1623,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),add(x,multiply(x,X0))) = add(multiply(iPr_def_10,X0),x),
inference(demodulation,[status(thm)],[c_1622,c_119,c_285]) ).
tcf(c_2187,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X1,inverse(X0))) = add(multiply(X0,X0),X1),
inference(demodulation,[status(thm)],[c_486,c_118,c_285,c_662]) ).
tcf(c_2191,plain,
! [X0: $i] : add(multiply(X0,X0),multiplicative_identity) = add(X0,inverse(X0)),
inference(superposition,[status(thm)],[c_120,c_2187]) ).
tcf(c_2195,plain,
! [X0: $i] : add(multiply(x,x),X0) = add(x,multiply(X0,iPr_def_10)),
inference(superposition,[status(thm)],[c_341,c_2187]) ).
tcf(c_2219,plain,
! [X0: $i] : add(multiply(X0,X0),multiplicative_identity) = multiplicative_identity,
inference(light_normalisation,[status(thm)],[c_2191,c_139]) ).
tcf(c_2222,plain,
! [X0: $i] : add(x,multiply(X0,iPr_def_10)) = add(x,X0),
inference(light_normalisation,[status(thm)],[c_2195,c_1130]) ).
tcf(c_2445,plain,
! [X0: $i] : add(multiplicative_identity,multiply(X0,X0)) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_2219,c_285]) ).
tcf(c_2452,plain,
add(multiplicative_identity,y) = multiplicative_identity,
inference(superposition,[status(thm)],[c_682,c_2445]) ).
tcf(c_2460,plain,
! [X0: $i,X1: $i] : add(multiply(X0,multiplicative_identity),multiply(X0,multiply(X1,X1))) = multiply(X0,multiplicative_identity),
inference(superposition,[status(thm)],[c_2445,c_295]) ).
tcf(c_2461,plain,
! [X0: $i,X1: $i] : add(multiply(multiplicative_identity,X0),multiply(multiply(X1,X1),X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_2445,c_293]) ).
tcf(c_2466,plain,
! [X0: $i,X1: $i] : add(X0,multiply(multiply(X1,X1),X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2461,c_120]) ).
tcf(c_2467,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X0,multiply(X1,X1))) = X0,
inference(light_normalisation,[status(thm)],[c_2460,c_121]) ).
tcf(c_2468,plain,
! [X0: $i] : add(multiply(X0,multiplicative_identity),multiply(X0,y)) = multiply(X0,multiplicative_identity),
inference(superposition,[status(thm)],[c_2452,c_295]) ).
tcf(c_2471,plain,
! [X0: $i] : add(X0,multiply(X0,y)) = X0,
inference(light_normalisation,[status(thm)],[c_2468,c_121]) ).
tcf(c_2472,plain,
add(add(iPr_def_13,x),iPr_def_14) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_1541,c_2471]) ).
tcf(c_2548,plain,
! [X0: $i] : add(add(multiply(X0,y),multiply(X0,iPr_def_11)),add(additive_identity,iPr_def_11)) = add(multiply(X0,y),iPr_def_11),
inference(light_normalisation,[status(thm)],[c_489,c_931]) ).
tcf(c_2549,plain,
! [X0: $i] : add(iPr_def_11,multiply(X0,y)) = add(iPr_def_11,X0),
inference(demodulation,[status(thm)],[c_2548,c_118,c_285,c_659]) ).
tcf(c_2553,plain,
add(iPr_def_11,y) = add(iPr_def_11,multiplicative_identity),
inference(superposition,[status(thm)],[c_120,c_2549]) ).
tcf(c_2560,plain,
add(iPr_def_11,multiplicative_identity) = multiplicative_identity,
inference(light_normalisation,[status(thm)],[c_2553,c_429]) ).
tcf(c_2637,plain,
! [X0: $i] : add(multiply(iPr_def_11,X0),multiply(multiplicative_identity,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_2560,c_293]) ).
tcf(c_2638,plain,
! [X0: $i] : add(multiply(iPr_def_11,X0),X0) = X0,
inference(light_normalisation,[status(thm)],[c_2637,c_120]) ).
tcf(c_2963,plain,
add(x,iPr_def_13) = x,
inference(superposition,[status(thm)],[c_344,c_2471]) ).
tcf(c_2982,plain,
add(iPr_def_13,x) = x,
inference(demodulation,[status(thm)],[c_2963,c_285]) ).
tcf(c_3016,plain,
add(x,iPr_def_14) = multiplicative_identity,
inference(light_normalisation,[status(thm)],[c_2472,c_2982]) ).
tcf(c_3017,plain,
add(iPr_def_14,x) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_3016,c_285]) ).
tcf(c_3019,plain,
! [X0: $i] : add(multiply(iPr_def_14,X0),multiply(x,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_3017,c_293]) ).
tcf(c_3020,plain,
! [X0: $i] : add(multiply(iPr_def_14,X0),multiply(x,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3019,c_120]) ).
tcf(c_3167,plain,
! [X0: $i] : add(X0,multiply(iPr_def_11,X0)) = X0,
inference(demodulation,[status(thm)],[c_2638,c_285]) ).
tcf(c_3179,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),multiply(multiply(iPr_def_11,X0),X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_3167,c_293]) ).
tcf(c_3594,plain,
multiply(inverse(iPr_def_11),y) = inverse(iPr_def_11),
inference(demodulation,[status(thm)],[c_672,c_118,c_283]) ).
tcf(c_3663,plain,
multiply(inverse(iPr_def_10),x) = inverse(iPr_def_10),
inference(demodulation,[status(thm)],[c_953,c_118,c_283]) ).
tcf(c_3969,plain,
! [X0: $i] : add(x,multiply(iPr_def_10,X0)) = add(x,X0),
inference(superposition,[status(thm)],[c_283,c_2222]) ).
tcf(c_3973,plain,
add(x,add(multiply(iPr_def_10,iPr_def_10),multiply(iPr_def_11,iPr_def_10))) = add(x,iPr_def_12),
inference(superposition,[status(thm)],[c_578,c_2222]) ).
tcf(c_3974,plain,
! [X0: $i] : add(multiply(X0,iPr_def_10),x) = add(x,X0),
inference(superposition,[status(thm)],[c_2222,c_285]) ).
tcf(c_3984,plain,
add(x,add(iPr_def_10,multiply(iPr_def_11,iPr_def_10))) = add(x,iPr_def_12),
inference(light_normalisation,[status(thm)],[c_3973,c_1170]) ).
tcf(c_4220,plain,
add(multiply(iPr_def_14,inverse(x)),additive_identity) = inverse(x),
inference(superposition,[status(thm)],[c_141,c_3020]) ).
tcf(c_4230,plain,
add(multiply(iPr_def_14,iPr_def_10),additive_identity) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_4220,c_341]) ).
tcf(c_4341,plain,
multiply(iPr_def_10,iPr_def_14) = iPr_def_10,
inference(demodulation,[status(thm)],[c_4230,c_119,c_283]) ).
tcf(c_4506,plain,
! [X0: $i] : add(add(x,multiply(x,X0)),add(additive_identity,multiply(iPr_def_10,X0))) = add(x,X0),
inference(light_normalisation,[status(thm)],[c_547,c_1130,c_3969]) ).
tcf(c_4507,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),x) = add(x,X0),
inference(demodulation,[status(thm)],[c_4506,c_118,c_285,c_1623]) ).
tcf(c_4522,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),x) = add(X0,x),
inference(superposition,[status(thm)],[c_4507,c_285]) ).
tcf(c_5406,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_577,c_120]) ).
tcf(c_5447,plain,
add(multiply(iPr_def_10,x),inverse(iPr_def_10)) = x,
inference(superposition,[status(thm)],[c_3663,c_5406]) ).
tcf(c_5448,plain,
add(multiply(iPr_def_11,y),inverse(iPr_def_11)) = y,
inference(superposition,[status(thm)],[c_3594,c_5406]) ).
tcf(c_5462,plain,
add(additive_identity,inverse(iPr_def_11)) = y,
inference(light_normalisation,[status(thm)],[c_5448,c_439]) ).
tcf(c_5463,plain,
add(additive_identity,inverse(iPr_def_10)) = x,
inference(light_normalisation,[status(thm)],[c_5447,c_438]) ).
tcf(c_5516,plain,
multiply(x,add(additive_identity,inverse(iPr_def_11))) = iPr_def_13,
inference(demodulation,[status(thm)],[c_344,c_5462]) ).
tcf(c_5517,plain,
inverse(add(additive_identity,inverse(iPr_def_11))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_342,c_5462]) ).
tcf(c_5587,plain,
inverse(iPr_def_11) = y,
inference(demodulation,[status(thm)],[c_5462,c_118]) ).
tcf(c_5588,plain,
inverse(iPr_def_10) = x,
inference(demodulation,[status(thm)],[c_5463,c_118]) ).
tcf(c_5754,plain,
inverse(inverse(iPr_def_11)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_5517,c_118]) ).
tcf(c_6023,plain,
! [X0: $i] : add(multiply(X0,inverse(X0)),multiply(additive_identity,inverse(X0))) = additive_identity,
inference(superposition,[status(thm)],[c_119,c_593]) ).
tcf(c_6123,plain,
! [X0: $i] : add(additive_identity,multiply(additive_identity,inverse(X0))) = additive_identity,
inference(light_normalisation,[status(thm)],[c_6023,c_141]) ).
tcf(c_6161,plain,
! [X0: $i] : multiply(additive_identity,inverse(X0)) = additive_identity,
inference(demodulation,[status(thm)],[c_6123,c_118]) ).
tcf(c_6172,plain,
! [X0: $i] : add(multiply(X0,X0),additive_identity) = add(X0,additive_identity),
inference(superposition,[status(thm)],[c_6161,c_2187]) ).
tcf(c_6182,plain,
! [X0: $i] : add(multiply(X0,X0),additive_identity) = X0,
inference(light_normalisation,[status(thm)],[c_6172,c_119]) ).
tcf(c_6522,plain,
! [X0: $i] : multiply(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_6182,c_119]) ).
tcf(c_6531,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X1,inverse(X0))) = add(X0,X1),
inference(demodulation,[status(thm)],[c_2187,c_6522]) ).
tcf(c_6535,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_2467,c_6522]) ).
tcf(c_6536,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X1,X0)) = X0,
inference(demodulation,[status(thm)],[c_2466,c_6522]) ).
tcf(c_6594,plain,
add(multiply(iPr_def_10,iPr_def_12),multiply(iPr_def_11,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_6522,c_578]) ).
tcf(c_6839,plain,
! [X0: $i,X1: $i] : add(multiply(X0,inverse(X0)),multiply(multiply(X0,X1),inverse(X0))) = additive_identity,
inference(superposition,[status(thm)],[c_6535,c_593]) ).
tcf(c_6846,plain,
! [X0: $i,X1: $i] : add(additive_identity,multiply(multiply(X0,X1),inverse(X0))) = additive_identity,
inference(light_normalisation,[status(thm)],[c_6839,c_141]) ).
tcf(c_6945,plain,
! [X0: $i] : add(inverse(iPr_def_10),multiply(iPr_def_10,X0)) = add(inverse(iPr_def_10),X0),
inference(light_normalisation,[status(thm)],[c_3969,c_5588]) ).
tcf(c_6963,plain,
! [X0: $i] : add(multiply(X0,iPr_def_10),inverse(iPr_def_10)) = add(inverse(iPr_def_10),X0),
inference(light_normalisation,[status(thm)],[c_3974,c_5588]) ).
tcf(c_6968,plain,
! [X0: $i,X1: $i] : add(add(multiply(X0,iPr_def_10),multiply(X1,iPr_def_10)),inverse(iPr_def_10)) = add(inverse(iPr_def_10),add(X0,X1)),
inference(superposition,[status(thm)],[c_293,c_6963]) ).
tcf(c_6980,plain,
! [X0: $i] : add(multiply(X0,iPr_def_10),inverse(iPr_def_10)) = add(X0,inverse(iPr_def_10)),
inference(superposition,[status(thm)],[c_6963,c_285]) ).
tcf(c_6986,plain,
! [X0: $i] : add(multiply(multiply(iPr_def_10,X0),iPr_def_10),inverse(iPr_def_10)) = add(inverse(iPr_def_10),X0),
inference(superposition,[status(thm)],[c_6963,c_6945]) ).
tcf(c_7017,plain,
add(add(iPr_def_13,multiply(inverse(iPr_def_10),iPr_def_12)),add(multiply(iPr_def_12,inverse(iPr_def_11)),iPr_def_12)) = add(iPr_def_13,iPr_def_12),
inference(light_normalisation,[status(thm)],[c_620,c_5587,c_5588,c_6594]) ).
tcf(c_7018,plain,
add(iPr_def_12,add(iPr_def_13,multiply(iPr_def_11,inverse(iPr_def_10)))) = add(iPr_def_12,iPr_def_13),
inference(demodulation,[status(thm)],[c_7017,c_118,c_141,c_285,c_578,c_636,c_843,c_6535]) ).
tcf(c_7178,plain,
multiply(inverse(iPr_def_10),add(additive_identity,inverse(iPr_def_11))) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_5516,c_5588]) ).
tcf(c_7179,plain,
multiply(inverse(iPr_def_10),inverse(iPr_def_11)) = iPr_def_13,
inference(demodulation,[status(thm)],[c_7178,c_295,c_633]) ).
tcf(c_7257,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),inverse(iPr_def_10)) = add(X0,inverse(iPr_def_10)),
inference(light_normalisation,[status(thm)],[c_4522,c_5588]) ).
tcf(c_7358,plain,
! [X0: $i] : add(additive_identity,multiply(X0,inverse(inverse(X0)))) = X0,
inference(superposition,[status(thm)],[c_141,c_662]) ).
tcf(c_7370,plain,
add(iPr_def_13,multiply(inverse(iPr_def_10),inverse(inverse(iPr_def_11)))) = inverse(iPr_def_10),
inference(superposition,[status(thm)],[c_7179,c_662]) ).
tcf(c_7403,plain,
add(iPr_def_13,multiply(inverse(iPr_def_10),iPr_def_11)) = inverse(iPr_def_10),
inference(light_normalisation,[status(thm)],[c_7370,c_5754]) ).
tcf(c_7442,plain,
! [X0: $i] : multiply(X0,inverse(inverse(X0))) = X0,
inference(demodulation,[status(thm)],[c_7358,c_118]) ).
tcf(c_7458,plain,
! [X0: $i] : add(inverse(inverse(X0)),X0) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_7442,c_6536]) ).
tcf(c_7839,plain,
add(iPr_def_13,multiply(iPr_def_11,inverse(iPr_def_10))) = inverse(iPr_def_10),
inference(demodulation,[status(thm)],[c_7403,c_283]) ).
tcf(c_7840,plain,
add(iPr_def_12,inverse(iPr_def_10)) = add(iPr_def_12,iPr_def_13),
inference(demodulation,[status(thm)],[c_7018,c_7839]) ).
tcf(c_7853,plain,
! [X0: $i] : add(X0,inverse(inverse(X0))) = inverse(inverse(X0)),
inference(demodulation,[status(thm)],[c_7458,c_285]) ).
tcf(c_8815,plain,
! [X0: $i,X1: $i] : add(X0,multiply(inverse(X0),X1)) = add(X0,X1),
inference(superposition,[status(thm)],[c_283,c_6531]) ).
tcf(c_8923,plain,
! [X0: $i] : add(X0,inverse(inverse(X0))) = add(X0,additive_identity),
inference(superposition,[status(thm)],[c_141,c_8815]) ).
tcf(c_8948,plain,
! [X0: $i] : add(X0,inverse(inverse(X0))) = X0,
inference(light_normalisation,[status(thm)],[c_8923,c_119,c_7853]) ).
tcf(c_8952,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_7853,c_8948]) ).
tcf(c_8991,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X1),inverse(X0)) = additive_identity,
inference(demodulation,[status(thm)],[c_6846,c_118]) ).
tcf(c_8994,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X1),inverse(X1)) = additive_identity,
inference(superposition,[status(thm)],[c_283,c_8991]) ).
tcf(c_9213,plain,
multiply(iPr_def_13,inverse(inverse(iPr_def_11))) = additive_identity,
inference(superposition,[status(thm)],[c_7179,c_8994]) ).
tcf(c_9349,plain,
multiply(iPr_def_11,iPr_def_13) = additive_identity,
inference(demodulation,[status(thm)],[c_9213,c_283,c_8952]) ).
tcf(c_9371,plain,
add(additive_identity,multiply(iPr_def_11,iPr_def_14)) = iPr_def_11,
inference(superposition,[status(thm)],[c_9349,c_661]) ).
tcf(c_9567,plain,
add(inverse(iPr_def_10),add(iPr_def_10,multiply(iPr_def_11,iPr_def_10))) = add(inverse(iPr_def_10),iPr_def_12),
inference(light_normalisation,[status(thm)],[c_3984,c_5588]) ).
tcf(c_9568,plain,
add(iPr_def_12,iPr_def_13) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_9567,c_139,c_3179,c_6522,c_6968,c_6980,c_6986,c_7257,c_7840]) ).
tcf(c_9572,plain,
! [X0: $i] : add(multiply(iPr_def_12,X0),multiply(iPr_def_13,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_9568,c_293]) ).
tcf(c_9575,plain,
! [X0: $i] : add(add(multiply(iPr_def_10,X0),multiply(iPr_def_11,X0)),multiply(iPr_def_13,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_9572,c_120,c_578]) ).
tcf(c_9851,plain,
multiply(iPr_def_11,iPr_def_14) = iPr_def_11,
inference(demodulation,[status(thm)],[c_9371,c_118]) ).
tcf(c_29347,plain,
add(add(multiply(iPr_def_10,iPr_def_14),multiply(iPr_def_11,iPr_def_14)),additive_identity) = iPr_def_14,
inference(superposition,[status(thm)],[c_434,c_9575]) ).
tcf(c_29386,plain,
add(iPr_def_12,additive_identity) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_29347,c_343,c_4341,c_9851]) ).
tcf(c_29437,plain,
iPr_def_12 = iPr_def_14,
inference(demodulation,[status(thm)],[c_29386,c_119]) ).
tcf(c_29438,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_29437,c_420]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO015-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/5.37 % Computer : n019.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Fri Sep 25 06:33:10 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/5.42 Running first-order theorem proving
% 0.13/5.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/5.43
% 0.13/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.13/5.43
% 0.13/5.43 % Detected problem language: tptp
% 0.13/5.44 % Proving...
% 6.15/7.29 % SZS status Started for theBenchmark.p
% 6.15/7.29 % SZS status Unsatisfiable for theBenchmark.p
% 6.15/7.29
% 6.15/7.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.15/7.29
% 6.15/7.29 % ------ iProver source info
% 6.15/7.29
% 6.15/7.29 % git: date: 2026-07-19 20:42:38 +0200
% 6.15/7.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.15/7.29 % git: non_committed_changes: false
% 6.15/7.29
% 6.15/7.29 % ------ Parsing...% successful
% 6.15/7.29
% 6.15/7.29
% 6.15/7.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.15/7.29
% 6.15/7.29 % ------ Preprocessing... sup_sim: 18 sf_s rm: 0 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.15/7.29
% 6.15/7.29 % ------ Preprocessing...% ------ preprocesses with Option_UEQ
% 6.15/7.29 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.15/7.29
% 6.15/7.29 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 6.15/7.29 % ------ Proving...
% 6.15/7.29 % ------ Problem Properties
% 6.15/7.29
% 6.15/7.29 %
% 6.15/7.29 % clauses 20
% 6.15/7.29 % conjectures 1
% 6.15/7.29 % EPR 3
% 6.15/7.29 % Horn 20
% 6.15/7.29 % unary 20
% 6.15/7.29 % binary 0
% 6.15/7.29 % lits 20
% 6.15/7.29 % lits eq 20
% 6.15/7.29 % fd_pure 0
% 6.15/7.29 % fd_pseudo 0
% 6.15/7.29 % fd_cond 0
% 6.15/7.29 % fd_pseudo_cond 0
% 6.15/7.29 % AC symbols 0
% 6.15/7.29
% 6.15/7.29 % ------ Schedule UEQ
% 6.15/7.29
% 6.15/7.29 % ------ Option_UEQ Time Limit: 10.
% 6.15/7.29
% 6.15/7.29
% 6.15/7.29 % ------
% 6.15/7.29 % Current options:
% 6.15/7.29 % ------
% 6.15/7.29
% 6.15/7.29
% 6.15/7.29 %
% 6.15/7.29
% 6.15/7.29 % ------ Proving...
% 6.15/7.29 %
% 6.15/7.29
% 6.15/7.29 % SZS status Unsatisfiable for theBenchmark.p
% 6.15/7.29
% 6.15/7.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.15/7.29
% 6.15/7.29
%------------------------------------------------------------------------------