%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : BOO014-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 : n005.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 10.46s 2.72s
% Output : CNFRefutation 10.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 20
% Syntax : Number of formulae : 233 ( 215 unt; 5 def)
% Number of atoms : 1057 ( 222 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 : 251 ( 0 sgn 251 !; 0 ?; 211 :)
% 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,
sum(x,y,x_plus_y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_plus_y) ).
fof(f24,negated_conjecture,
product(inverse(x),inverse(y),x_inverse_times_y_inverse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_inverse_times_y_inverse) ).
fof(f25,negated_conjecture,
inverse(x_plus_y) != x_inverse_times_y_inverse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_equation) ).
fof(f26,plain,
x_inverse_times_y_inverse != inverse(x_plus_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(X6,X2,X5)
| ~ product(X6,X1,X4)
| ~ product(X6,X0,X3)
| ~ sum(X3,X4,X5)
| ~ sum(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(X2,X6,X5)
| ~ product(X1,X6,X4)
| ~ product(X0,X6,X3)
| ~ sum(X3,X4,X5)
| ~ sum(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(X0,X5,X6)
| ~ product(X2,X4,X6)
| ~ product(X1,X3,X5)
| ~ sum(X0,X3,X4)
| ~ sum(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(X5,X1,X6)
| ~ product(X2,X4,X6)
| ~ product(X0,X3,X5)
| ~ sum(X3,X1,X4)
| ~ sum(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,
sum(x,y,x_plus_y),
inference(cnf_transformation,[],[f23]) ).
tcf(c_97,negated_conjecture,
product(inverse(x),inverse(y),x_inverse_times_y_inverse),
inference(cnf_transformation,[],[f24]) ).
tcf(c_98,negated_conjecture,
inverse(x_plus_y) != x_inverse_times_y_inverse,
inference(cnf_transformation,[],[f26]) ).
tcf(c_110,plain,
add(x,y) = x_plus_y,
inference(well_definedness,[status(thm)],[c_96]) ).
tcf(c_111,plain,
multiply(inverse(x),inverse(y)) = x_inverse_times_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 = multiply(iPr_def_10,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_344,definition,
iPr_def_13 = add(x,y),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_345,definition,
iPr_def_14 = inverse(x_plus_y),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_346,plain,
iPr_def_12 = x_inverse_times_y_inverse,
inference(demodulation,[status(thm)],[c_111,c_342,c_341,c_343]) ).
tcf(c_347,plain,
iPr_def_13 = x_plus_y,
inference(demodulation,[status(thm)],[c_110,c_344]) ).
tcf(c_348,negated_conjecture,
iPr_def_14 != x_inverse_times_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_465,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_485,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_488,plain,
! [X0: $i] : add(add(multiply(X0,x),multiply(X0,iPr_def_10)),add(additive_identity,multiply(iPr_def_10,iPr_def_10))) = add(multiply(X0,x),iPr_def_10),
inference(superposition,[status(thm)],[c_438,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_502,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),add(multiply(X1,inverse(X0)),multiply(X1,X1))) = X1,
inference(demodulation,[status(thm)],[c_465,c_118]) ).
tcf(c_511,plain,
add(additive_identity,add(multiply(iPr_def_14,inverse(iPr_def_13)),multiply(iPr_def_14,iPr_def_14))) = iPr_def_14,
inference(superposition,[status(thm)],[c_434,c_502]) ).
tcf(c_523,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_502]) ).
tcf(c_531,plain,
add(additive_identity,add(multiply(iPr_def_14,iPr_def_14),multiply(iPr_def_14,iPr_def_14))) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_511,c_421]) ).
tcf(c_536,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_575,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X0),X1) = add(X0,multiply(X1,X1)),
inference(superposition,[status(thm)],[c_536,c_456]) ).
tcf(c_589,plain,
! [X0: $i] : add(multiply(x,X0),multiply(y,X0)) = multiply(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_344,c_293]) ).
tcf(c_593,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_594,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_595,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_596,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_610,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_617,plain,
! [X0: $i] : add(multiply(iPr_def_11,X0),multiply(y,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_596,c_120]) ).
tcf(c_618,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),multiply(x,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_595,c_120]) ).
tcf(c_619,plain,
! [X0: $i] : add(multiply(iPr_def_13,X0),multiply(iPr_def_14,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_594,c_120]) ).
tcf(c_623,plain,
! [X0: $i] : add(multiply(X0,x),multiply(y,X0)) = multiply(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_283,c_589]) ).
tcf(c_627,plain,
! [X0: $i] : add(multiply(x,X0),multiply(X0,y)) = multiply(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_283,c_589]) ).
tcf(c_639,plain,
add(additive_identity,multiply(y,inverse(iPr_def_11))) = inverse(iPr_def_11),
inference(superposition,[status(thm)],[c_141,c_617]) ).
tcf(c_640,plain,
add(additive_identity,multiply(y,y)) = y,
inference(superposition,[status(thm)],[c_439,c_617]) ).
tcf(c_644,plain,
add(multiply(iPr_def_11,inverse(y)),additive_identity) = inverse(y),
inference(superposition,[status(thm)],[c_141,c_617]) ).
tcf(c_646,plain,
add(multiply(iPr_def_11,iPr_def_11),additive_identity) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_644,c_342]) ).
tcf(c_647,plain,
multiply(y,y) = y,
inference(demodulation,[status(thm)],[c_640,c_118]) ).
tcf(c_659,plain,
add(multiply(x,y),y) = multiply(iPr_def_13,y),
inference(superposition,[status(thm)],[c_647,c_589]) ).
tcf(c_662,plain,
add(multiply(iPr_def_14,iPr_def_14),multiply(iPr_def_14,iPr_def_14)) = iPr_def_14,
inference(demodulation,[status(thm)],[c_531,c_118]) ).
tcf(c_679,plain,
! [X0: $i] : add(multiply(iPr_def_13,X0),add(multiply(iPr_def_14,X0),multiply(X0,X0))) = X0,
inference(superposition,[status(thm)],[c_283,c_523]) ).
tcf(c_770,plain,
! [X0: $i] : add(multiply(X0,x),multiply(X0,y)) = multiply(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_344,c_295]) ).
tcf(c_774,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_776,plain,
! [X0: $i] : add(multiply(X0,iPr_def_10),multiply(X0,x)) = multiply(X0,multiplicative_identity),
inference(superposition,[status(thm)],[c_428,c_295]) ).
tcf(c_777,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_815,plain,
! [X0: $i] : add(multiply(X0,iPr_def_11),multiply(X0,y)) = X0,
inference(light_normalisation,[status(thm)],[c_777,c_121]) ).
tcf(c_816,plain,
! [X0: $i] : add(multiply(X0,iPr_def_10),multiply(X0,x)) = X0,
inference(light_normalisation,[status(thm)],[c_776,c_121]) ).
tcf(c_818,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),multiply(X0,inverse(X1))) = X0,
inference(light_normalisation,[status(thm)],[c_774,c_121]) ).
tcf(c_849,plain,
! [X0: $i] : add(multiply(x,X0),multiply(X0,y)) = multiply(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_283,c_770]) ).
tcf(c_854,plain,
! [X0: $i] : add(multiply(X0,x),multiply(y,X0)) = multiply(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_283,c_770]) ).
tcf(c_919,plain,
multiply(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_646,c_119]) ).
tcf(c_1142,plain,
add(additive_identity,multiply(x,inverse(iPr_def_10))) = inverse(iPr_def_10),
inference(superposition,[status(thm)],[c_141,c_618]) ).
tcf(c_1144,plain,
add(additive_identity,multiply(x,x)) = x,
inference(superposition,[status(thm)],[c_438,c_618]) ).
tcf(c_1145,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),multiply(X0,x)) = X0,
inference(superposition,[status(thm)],[c_283,c_618]) ).
tcf(c_1149,plain,
add(multiply(iPr_def_10,inverse(x)),additive_identity) = inverse(x),
inference(superposition,[status(thm)],[c_141,c_618]) ).
tcf(c_1152,plain,
add(multiply(iPr_def_10,iPr_def_10),additive_identity) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_1149,c_341]) ).
tcf(c_1170,plain,
multiply(x,x) = x,
inference(demodulation,[status(thm)],[c_1144,c_118]) ).
tcf(c_1441,plain,
multiply(iPr_def_10,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_1152,c_119]) ).
tcf(c_1542,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X1,inverse(X0))) = add(multiply(X0,X0),X1),
inference(demodulation,[status(thm)],[c_485,c_118,c_285,c_818]) ).
tcf(c_1546,plain,
! [X0: $i] : add(multiply(X0,X0),multiplicative_identity) = add(X0,inverse(X0)),
inference(superposition,[status(thm)],[c_120,c_1542]) ).
tcf(c_1548,plain,
! [X0: $i] : add(multiply(X0,X0),X0) = add(X0,additive_identity),
inference(superposition,[status(thm)],[c_141,c_1542]) ).
tcf(c_1563,plain,
! [X0: $i] : add(multiply(X0,X0),X0) = X0,
inference(light_normalisation,[status(thm)],[c_1548,c_119]) ).
tcf(c_1565,plain,
! [X0: $i] : add(multiply(X0,X0),multiplicative_identity) = multiplicative_identity,
inference(light_normalisation,[status(thm)],[c_1546,c_139]) ).
tcf(c_1647,plain,
! [X0: $i] : add(X0,multiply(X0,X0)) = X0,
inference(demodulation,[status(thm)],[c_1563,c_575]) ).
tcf(c_1649,plain,
add(multiplicative_identity,multiplicative_identity) = multiplicative_identity,
inference(superposition,[status(thm)],[c_120,c_1647]) ).
tcf(c_1848,plain,
! [X0: $i] : add(add(multiply(X0,x),multiply(X0,iPr_def_10)),add(additive_identity,iPr_def_10)) = add(multiply(X0,x),iPr_def_10),
inference(light_normalisation,[status(thm)],[c_488,c_1441]) ).
tcf(c_1849,plain,
! [X0: $i] : add(iPr_def_10,multiply(X0,x)) = add(iPr_def_10,X0),
inference(demodulation,[status(thm)],[c_1848,c_118,c_285,c_816]) ).
tcf(c_1853,plain,
add(iPr_def_10,x) = add(iPr_def_10,multiplicative_identity),
inference(superposition,[status(thm)],[c_120,c_1849]) ).
tcf(c_1860,plain,
add(iPr_def_10,multiplicative_identity) = multiplicative_identity,
inference(light_normalisation,[status(thm)],[c_1853,c_428]) ).
tcf(c_1867,plain,
! [X0: $i] : add(multiply(multiplicative_identity,X0),multiply(multiplicative_identity,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_1649,c_293]) ).
tcf(c_1868,plain,
! [X0: $i] : add(X0,X0) = X0,
inference(light_normalisation,[status(thm)],[c_1867,c_120]) ).
tcf(c_1870,plain,
multiply(iPr_def_14,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_662,c_1868]) ).
tcf(c_2101,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_919]) ).
tcf(c_2102,plain,
! [X0: $i] : add(iPr_def_11,multiply(X0,y)) = add(iPr_def_11,X0),
inference(demodulation,[status(thm)],[c_2101,c_118,c_285,c_815]) ).
tcf(c_2105,plain,
add(iPr_def_11,y) = add(iPr_def_11,multiplicative_identity),
inference(superposition,[status(thm)],[c_120,c_2102]) ).
tcf(c_2113,plain,
add(iPr_def_11,multiplicative_identity) = multiplicative_identity,
inference(light_normalisation,[status(thm)],[c_2105,c_429]) ).
tcf(c_2118,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),multiply(multiplicative_identity,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_1860,c_293]) ).
tcf(c_2119,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),X0) = X0,
inference(light_normalisation,[status(thm)],[c_2118,c_120]) ).
tcf(c_2185,plain,
! [X0: $i] : add(multiply(iPr_def_11,X0),multiply(multiplicative_identity,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_2113,c_293]) ).
tcf(c_2186,plain,
! [X0: $i] : add(multiply(iPr_def_11,X0),X0) = X0,
inference(light_normalisation,[status(thm)],[c_2185,c_120]) ).
tcf(c_2209,plain,
! [X0: $i] : add(multiplicative_identity,multiply(X0,X0)) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_1565,c_285]) ).
tcf(c_2217,plain,
add(multiplicative_identity,iPr_def_14) = multiplicative_identity,
inference(superposition,[status(thm)],[c_1870,c_2209]) ).
tcf(c_2218,plain,
add(multiplicative_identity,x) = multiplicative_identity,
inference(superposition,[status(thm)],[c_1170,c_2209]) ).
tcf(c_2219,plain,
add(multiplicative_identity,y) = multiplicative_identity,
inference(superposition,[status(thm)],[c_647,c_2209]) ).
tcf(c_2222,plain,
! [X0: $i,X1: $i] : add(multiply(X0,multiplicative_identity),multiply(X0,multiply(X1,X1))) = multiply(X0,multiplicative_identity),
inference(superposition,[status(thm)],[c_2209,c_295]) ).
tcf(c_2223,plain,
! [X0: $i,X1: $i] : add(multiply(multiplicative_identity,X0),multiply(multiply(X1,X1),X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_2209,c_293]) ).
tcf(c_2227,plain,
! [X0: $i,X1: $i] : add(X0,multiply(multiply(X1,X1),X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2223,c_120]) ).
tcf(c_2228,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X0,multiply(X1,X1))) = X0,
inference(light_normalisation,[status(thm)],[c_2222,c_121]) ).
tcf(c_2474,plain,
add(iPr_def_14,multiplicative_identity) = multiplicative_identity,
inference(demodulation,[status(thm)],[c_2217,c_285]) ).
tcf(c_2477,plain,
! [X0: $i] : add(multiply(iPr_def_14,X0),multiply(multiplicative_identity,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_2474,c_293]) ).
tcf(c_2478,plain,
! [X0: $i] : add(multiply(iPr_def_14,X0),X0) = X0,
inference(light_normalisation,[status(thm)],[c_2477,c_120]) ).
tcf(c_2481,plain,
! [X0: $i] : add(multiply(multiplicative_identity,X0),multiply(x,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_2218,c_293]) ).
tcf(c_2482,plain,
! [X0: $i] : add(X0,multiply(x,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2481,c_120]) ).
tcf(c_2484,plain,
! [X0: $i] : add(multiply(X0,multiplicative_identity),multiply(X0,y)) = multiply(X0,multiplicative_identity),
inference(superposition,[status(thm)],[c_2219,c_295]) ).
tcf(c_2487,plain,
! [X0: $i] : add(X0,multiply(X0,y)) = X0,
inference(light_normalisation,[status(thm)],[c_2484,c_121]) ).
tcf(c_2496,plain,
! [X0: $i] : add(X0,multiply(iPr_def_10,X0)) = X0,
inference(demodulation,[status(thm)],[c_2119,c_285]) ).
tcf(c_2503,plain,
add(iPr_def_11,iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_343,c_2496]) ).
tcf(c_2515,plain,
! [X0: $i] : add(multiply(X0,iPr_def_11),multiply(X0,iPr_def_12)) = multiply(X0,iPr_def_11),
inference(superposition,[status(thm)],[c_2503,c_295]) ).
tcf(c_2830,plain,
! [X0: $i] : add(X0,multiply(iPr_def_11,X0)) = X0,
inference(demodulation,[status(thm)],[c_2186,c_285]) ).
tcf(c_2832,plain,
! [X0: $i] : add(X0,multiply(X0,iPr_def_11)) = X0,
inference(superposition,[status(thm)],[c_283,c_2830]) ).
tcf(c_3177,plain,
! [X0: $i] : add(X0,multiply(iPr_def_14,X0)) = X0,
inference(demodulation,[status(thm)],[c_2478,c_285]) ).
tcf(c_3190,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),multiply(multiply(iPr_def_14,X0),X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_3177,c_293]) ).
tcf(c_3442,plain,
add(iPr_def_10,iPr_def_12) = iPr_def_10,
inference(superposition,[status(thm)],[c_343,c_2832]) ).
tcf(c_3460,plain,
! [X0: $i] : add(multiply(iPr_def_10,X0),multiply(iPr_def_12,X0)) = multiply(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_3442,c_293]) ).
tcf(c_3647,plain,
! [X0: $i] : add(multiply(X0,iPr_def_13),multiply(iPr_def_14,X0)) = X0,
inference(superposition,[status(thm)],[c_283,c_619]) ).
tcf(c_3858,plain,
multiply(inverse(iPr_def_11),y) = inverse(iPr_def_11),
inference(demodulation,[status(thm)],[c_639,c_118,c_283]) ).
tcf(c_3905,plain,
multiply(iPr_def_13,y) = y,
inference(demodulation,[status(thm)],[c_659,c_285,c_2482]) ).
tcf(c_3922,plain,
add(iPr_def_13,y) = iPr_def_13,
inference(superposition,[status(thm)],[c_3905,c_2487]) ).
tcf(c_3923,plain,
add(iPr_def_11,y) = add(iPr_def_11,iPr_def_13),
inference(superposition,[status(thm)],[c_3905,c_2102]) ).
tcf(c_3928,plain,
add(iPr_def_11,iPr_def_13) = multiplicative_identity,
inference(light_normalisation,[status(thm)],[c_3923,c_429]) ).
tcf(c_4000,plain,
! [X0: $i] : add(multiply(iPr_def_11,X0),multiply(iPr_def_13,X0)) = multiply(multiplicative_identity,X0),
inference(superposition,[status(thm)],[c_3928,c_293]) ).
tcf(c_4002,plain,
! [X0: $i] : add(multiply(iPr_def_11,X0),multiply(iPr_def_13,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4000,c_120]) ).
tcf(c_4050,plain,
multiply(inverse(iPr_def_10),x) = inverse(iPr_def_10),
inference(demodulation,[status(thm)],[c_1142,c_118,c_283]) ).
tcf(c_4089,plain,
! [X0: $i] : add(multiply(X0,x),multiply(iPr_def_10,X0)) = X0,
inference(superposition,[status(thm)],[c_1145,c_285]) ).
tcf(c_5126,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_593,c_120]) ).
tcf(c_5163,plain,
! [X0: $i] : add(multiply(X0,inverse(inverse(X0))),additive_identity) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_141,c_5126]) ).
tcf(c_5164,plain,
add(multiply(iPr_def_10,x),inverse(iPr_def_10)) = x,
inference(superposition,[status(thm)],[c_4050,c_5126]) ).
tcf(c_5165,plain,
add(multiply(iPr_def_11,y),inverse(iPr_def_11)) = y,
inference(superposition,[status(thm)],[c_3858,c_5126]) ).
tcf(c_5179,plain,
add(additive_identity,inverse(iPr_def_11)) = y,
inference(light_normalisation,[status(thm)],[c_5165,c_439]) ).
tcf(c_5180,plain,
add(additive_identity,inverse(iPr_def_10)) = x,
inference(light_normalisation,[status(thm)],[c_5164,c_438]) ).
tcf(c_5209,plain,
add(iPr_def_13,add(additive_identity,inverse(iPr_def_11))) = iPr_def_13,
inference(demodulation,[status(thm)],[c_3922,c_5179]) ).
tcf(c_5263,plain,
inverse(iPr_def_11) = y,
inference(demodulation,[status(thm)],[c_5179,c_118]) ).
tcf(c_5264,plain,
inverse(iPr_def_10) = x,
inference(demodulation,[status(thm)],[c_5180,c_118]) ).
tcf(c_5504,plain,
! [X0: $i] : add(multiply(iPr_def_14,X0),multiply(X0,iPr_def_13)) = X0,
inference(superposition,[status(thm)],[c_3647,c_285]) ).
tcf(c_6341,plain,
! [X0: $i] : add(multiply(X0,inverse(X0)),multiply(additive_identity,inverse(X0))) = additive_identity,
inference(superposition,[status(thm)],[c_119,c_610]) ).
tcf(c_6352,plain,
! [X0: $i] : add(multiply(multiply(iPr_def_13,X0),inverse(X0)),multiply(add(multiply(iPr_def_14,X0),multiply(X0,X0)),inverse(X0))) = additive_identity,
inference(superposition,[status(thm)],[c_679,c_610]) ).
tcf(c_6452,plain,
! [X0: $i] : add(additive_identity,multiply(additive_identity,inverse(X0))) = additive_identity,
inference(light_normalisation,[status(thm)],[c_6341,c_141]) ).
tcf(c_6502,plain,
! [X0: $i] : multiply(additive_identity,inverse(X0)) = additive_identity,
inference(demodulation,[status(thm)],[c_6452,c_118]) ).
tcf(c_6520,plain,
! [X0: $i] : add(multiply(X0,X0),additive_identity) = add(X0,additive_identity),
inference(superposition,[status(thm)],[c_6502,c_1542]) ).
tcf(c_6527,plain,
! [X0: $i] : add(multiply(X0,X0),additive_identity) = X0,
inference(light_normalisation,[status(thm)],[c_6520,c_119]) ).
tcf(c_6541,plain,
! [X0: $i] : multiply(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_6527,c_119]) ).
tcf(c_6551,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_2228,c_6541]) ).
tcf(c_6552,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X1,X0)) = X0,
inference(demodulation,[status(thm)],[c_2227,c_6541]) ).
tcf(c_7314,plain,
! [X0: $i] : add(multiply(X0,inverse(iPr_def_10)),multiply(inverse(iPr_def_11),X0)) = multiply(iPr_def_13,X0),
inference(light_normalisation,[status(thm)],[c_623,c_854,c_5263,c_5264]) ).
tcf(c_7353,plain,
add(multiply(iPr_def_11,iPr_def_14),additive_identity) = iPr_def_14,
inference(superposition,[status(thm)],[c_434,c_4002]) ).
tcf(c_7383,plain,
multiply(iPr_def_11,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_7353,c_119]) ).
tcf(c_7385,plain,
add(iPr_def_11,iPr_def_14) = iPr_def_11,
inference(superposition,[status(thm)],[c_7383,c_6551]) ).
tcf(c_7395,plain,
! [X0: $i] : add(multiply(X0,iPr_def_11),multiply(X0,iPr_def_14)) = multiply(X0,iPr_def_11),
inference(superposition,[status(thm)],[c_7385,c_295]) ).
tcf(c_7410,plain,
! [X0: $i] : add(multiply(inverse(iPr_def_10),X0),multiply(X0,inverse(iPr_def_11))) = multiply(iPr_def_13,X0),
inference(light_normalisation,[status(thm)],[c_627,c_849,c_5263,c_5264]) ).
tcf(c_7567,plain,
! [X0: $i] : add(multiply(X0,inverse(iPr_def_10)),multiply(iPr_def_10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4089,c_5264]) ).
tcf(c_7591,plain,
add(iPr_def_13,inverse(iPr_def_11)) = iPr_def_13,
inference(demodulation,[status(thm)],[c_5209,c_118]) ).
tcf(c_7592,plain,
add(multiply(iPr_def_13,inverse(iPr_def_13)),multiply(inverse(iPr_def_11),inverse(iPr_def_13))) = additive_identity,
inference(superposition,[status(thm)],[c_7591,c_610]) ).
tcf(c_7595,plain,
add(additive_identity,multiply(inverse(iPr_def_11),iPr_def_14)) = additive_identity,
inference(light_normalisation,[status(thm)],[c_7592,c_421,c_434]) ).
tcf(c_7596,plain,
multiply(iPr_def_14,inverse(iPr_def_11)) = additive_identity,
inference(demodulation,[status(thm)],[c_7595,c_118,c_283]) ).
tcf(c_7600,plain,
add(multiply(inverse(iPr_def_11),iPr_def_13),additive_identity) = inverse(iPr_def_11),
inference(superposition,[status(thm)],[c_7596,c_3647]) ).
tcf(c_7602,plain,
add(multiply(inverse(iPr_def_10),iPr_def_14),additive_identity) = multiply(iPr_def_13,iPr_def_14),
inference(superposition,[status(thm)],[c_7596,c_7410]) ).
tcf(c_7605,plain,
add(multiply(inverse(iPr_def_10),iPr_def_14),additive_identity) = additive_identity,
inference(light_normalisation,[status(thm)],[c_7602,c_434]) ).
tcf(c_7606,plain,
multiply(iPr_def_14,inverse(iPr_def_10)) = additive_identity,
inference(demodulation,[status(thm)],[c_7605,c_119,c_283]) ).
tcf(c_7612,plain,
add(additive_identity,multiply(iPr_def_10,iPr_def_14)) = iPr_def_14,
inference(superposition,[status(thm)],[c_7606,c_7567]) ).
tcf(c_7615,plain,
multiply(iPr_def_13,inverse(iPr_def_11)) = inverse(iPr_def_11),
inference(demodulation,[status(thm)],[c_7600,c_119,c_283]) ).
tcf(c_7670,plain,
multiply(iPr_def_10,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_7612,c_118]) ).
tcf(c_8880,plain,
! [X0: $i] : add(multiply(multiply(iPr_def_13,X0),inverse(X0)),multiply(add(multiply(iPr_def_14,X0),X0),inverse(X0))) = additive_identity,
inference(light_normalisation,[status(thm)],[c_6352,c_6541]) ).
tcf(c_8881,plain,
! [X0: $i] : multiply(multiply(iPr_def_13,X0),inverse(X0)) = additive_identity,
inference(demodulation,[status(thm)],[c_8880,c_119,c_141,c_285,c_293,c_3190]) ).
tcf(c_8882,plain,
! [X0: $i] : multiply(multiply(X0,iPr_def_13),inverse(X0)) = additive_identity,
inference(superposition,[status(thm)],[c_283,c_8881]) ).
tcf(c_9191,plain,
! [X0: $i] : add(additive_identity,multiply(X0,inverse(inverse(X0)))) = X0,
inference(superposition,[status(thm)],[c_141,c_818]) ).
tcf(c_9352,plain,
! [X0: $i] : multiply(X0,inverse(inverse(X0))) = X0,
inference(demodulation,[status(thm)],[c_9191,c_118]) ).
tcf(c_12556,plain,
! [X0: $i] : add(multiply(iPr_def_11,X0),multiply(X0,iPr_def_12)) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_283,c_2515]) ).
tcf(c_13140,plain,
add(additive_identity,multiply(iPr_def_12,inverse(iPr_def_10))) = additive_identity,
inference(superposition,[status(thm)],[c_141,c_3460]) ).
tcf(c_13175,plain,
multiply(iPr_def_12,inverse(iPr_def_10)) = additive_identity,
inference(demodulation,[status(thm)],[c_13140,c_118]) ).
tcf(c_13193,plain,
add(additive_identity,multiply(inverse(iPr_def_11),iPr_def_12)) = multiply(iPr_def_13,iPr_def_12),
inference(superposition,[status(thm)],[c_13175,c_7314]) ).
tcf(c_13862,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_5163,c_119,c_9352]) ).
tcf(c_13872,plain,
! [X0: $i] : multiply(multiply(inverse(X0),iPr_def_13),X0) = additive_identity,
inference(superposition,[status(thm)],[c_13862,c_8882]) ).
tcf(c_13879,plain,
! [X0: $i] : multiply(X0,multiply(iPr_def_13,inverse(X0))) = additive_identity,
inference(demodulation,[status(thm)],[c_13872,c_283]) ).
tcf(c_15333,plain,
add(iPr_def_12,multiply(iPr_def_10,iPr_def_14)) = iPr_def_12,
inference(superposition,[status(thm)],[c_343,c_7395]) ).
tcf(c_15364,plain,
add(iPr_def_12,iPr_def_14) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_15333,c_7670]) ).
tcf(c_16128,plain,
add(additive_identity,multiply(multiply(iPr_def_13,inverse(iPr_def_11)),iPr_def_12)) = additive_identity,
inference(superposition,[status(thm)],[c_13879,c_12556]) ).
tcf(c_16152,plain,
multiply(iPr_def_13,iPr_def_12) = additive_identity,
inference(light_normalisation,[status(thm)],[c_16128,c_7615,c_13193]) ).
tcf(c_16190,plain,
multiply(iPr_def_12,iPr_def_13) = additive_identity,
inference(demodulation,[status(thm)],[c_16152,c_283]) ).
tcf(c_16233,plain,
add(multiply(iPr_def_14,iPr_def_12),additive_identity) = iPr_def_12,
inference(superposition,[status(thm)],[c_16190,c_5504]) ).
tcf(c_16264,plain,
multiply(iPr_def_12,iPr_def_14) = iPr_def_12,
inference(demodulation,[status(thm)],[c_16233,c_119,c_283]) ).
tcf(c_16279,plain,
add(iPr_def_14,iPr_def_12) = iPr_def_14,
inference(superposition,[status(thm)],[c_16264,c_6552]) ).
tcf(c_16313,plain,
iPr_def_12 = iPr_def_14,
inference(demodulation,[status(thm)],[c_16279,c_285,c_15364]) ).
tcf(c_16314,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_16313,c_420]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO014-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.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 06:32:17 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.43 % Proving...
% 10.46/2.72 % SZS status Started for theBenchmark.p
% 10.46/2.72 % SZS status Unsatisfiable for theBenchmark.p
% 10.46/2.72
% 10.46/2.72 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.46/2.72
% 10.46/2.72 % ------ iProver source info
% 10.46/2.72
% 10.46/2.72 % git: date: 2026-07-19 20:42:38 +0200
% 10.46/2.72 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.46/2.72 % git: non_committed_changes: false
% 10.46/2.72
% 10.46/2.72 % ------ Parsing...% successful
% 10.46/2.72
% 10.46/2.72
% 10.46/2.72 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 10.46/2.72
% 10.46/2.72 % ------ 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 %
% 10.46/2.72
% 10.46/2.72 % ------ Preprocessing...% ------ preprocesses with Option_UEQ
% 10.46/2.72 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 10.46/2.72
% 10.46/2.72 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 10.46/2.72 % ------ Proving...
% 10.46/2.72 % ------ Problem Properties
% 10.46/2.72
% 10.46/2.72 %
% 10.46/2.72 % clauses 20
% 10.46/2.72 % conjectures 1
% 10.46/2.72 % EPR 3
% 10.46/2.72 % Horn 20
% 10.46/2.72 % unary 20
% 10.46/2.72 % binary 0
% 10.46/2.72 % lits 20
% 10.46/2.72 % lits eq 20
% 10.46/2.72 % fd_pure 0
% 10.46/2.72 % fd_pseudo 0
% 10.46/2.72 % fd_cond 0
% 10.46/2.72 % fd_pseudo_cond 0
% 10.46/2.72 % AC symbols 0
% 10.46/2.72
% 10.46/2.72 % ------ Schedule UEQ
% 10.46/2.72
% 10.46/2.72 % ------ Option_UEQ Time Limit: 10.
% 10.46/2.72
% 10.46/2.72
% 10.46/2.72 % ------
% 10.46/2.72 % Current options:
% 10.46/2.72 % ------
% 10.46/2.72
% 10.46/2.72
% 10.46/2.72 %
% 10.46/2.72
% 10.46/2.72 % ------ Proving...
% 10.46/2.72 %
% 10.46/2.72
% 10.46/2.72 % SZS status Unsatisfiable for theBenchmark.p
% 10.46/2.72
% 10.46/2.72 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.46/2.73
% 10.46/2.73
%------------------------------------------------------------------------------