%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP002-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n008.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:29:51 PM UTC 2026
% Result : Unsatisfiable 1.22s 1.75s
% Output : CNFRefutation 1.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 21
% Syntax : Number of formulae : 267 ( 261 unt; 9 def)
% Number of atoms : 1445 ( 246 equ)
% Maximal formula atoms : 4 ( 5 avg)
% Number of connectives : 29 ( 17 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 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 : 13 ( 11 usr; 10 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-1 aty)
% Number of variables : 133 ( 0 sgn 133 !; 0 ?; 121 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : product(identity,X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : product(X0,identity,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',right_identity) ).
fof(f3,axiom,
! [X0] : product(inverse(X0),X0,identity),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',left_inverse) ).
fof(f4,axiom,
! [X0] : product(X0,inverse(X0),identity),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',right_inverse) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X4,X5] :
( product(X2,X3,X5)
| ~ product(X0,X4,X5)
| ~ product(X1,X3,X4)
| ~ product(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',associativity2) ).
fof(f9,axiom,
! [X0,X1] :
( product(X0,X1,identity)
| ~ product(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_cubed_is_identity_1) ).
fof(f11,negated_conjecture,
product(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_times_b_is_c) ).
fof(f12,negated_conjecture,
product(c,inverse(a),d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_times_inverse_a_is_d) ).
fof(f13,negated_conjecture,
product(d,inverse(b),h),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_times_inverse_b_is_h) ).
fof(f14,negated_conjecture,
product(h,b,j),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_times_b_is_j) ).
fof(f15,negated_conjecture,
product(j,inverse(h),k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',j_times_inverse_h_is_k) ).
fof(f16,negated_conjecture,
~ product(k,inverse(b),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_k_times_inverse_b_is_e) ).
tcf(c_65,plain,
! [X0: $i] : product(identity,X0,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_66,plain,
! [X0: $i] : product(X0,identity,X0),
inference(cnf_transformation,[],[f2]) ).
tcf(c_67,plain,
! [X0: $i] : product(inverse(X0),X0,identity),
inference(cnf_transformation,[],[f3]) ).
tcf(c_68,plain,
! [X0: $i] : product(X0,inverse(X0),identity),
inference(cnf_transformation,[],[f4]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( product(X2,X5,X4)
| ~ product(X1,X5,X3)
| ~ product(X0,X3,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( product(X0,X1,identity)
| ~ product(X0,X0,X1) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_75,negated_conjecture,
product(a,b,c),
inference(cnf_transformation,[],[f11]) ).
tcf(c_76,negated_conjecture,
product(c,inverse(a),d),
inference(cnf_transformation,[],[f12]) ).
tcf(c_77,negated_conjecture,
product(d,inverse(b),h),
inference(cnf_transformation,[],[f13]) ).
tcf(c_78,negated_conjecture,
product(h,b,j),
inference(cnf_transformation,[],[f14]) ).
tcf(c_79,negated_conjecture,
product(j,inverse(h),k),
inference(cnf_transformation,[],[f15]) ).
tcf(c_80,negated_conjecture,
~ product(k,inverse(b),identity),
inference(cnf_transformation,[],[f16]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = identity )
| ( multiply(X0,X0) != X1 ) ),
inference(well_definedness,[status(thm)],[c_73]) ).
tcf(c_90,plain,
multiply(a,b) = c,
inference(well_definedness,[status(thm)],[c_75]) ).
tcf(c_91,plain,
multiply(c,inverse(a)) = d,
inference(well_definedness,[status(thm)],[c_76]) ).
tcf(c_92,plain,
multiply(d,inverse(b)) = h,
inference(well_definedness,[status(thm)],[c_77]) ).
tcf(c_93,plain,
multiply(h,b) = j,
inference(well_definedness,[status(thm)],[c_78]) ).
tcf(c_94,plain,
multiply(j,inverse(h)) = k,
inference(well_definedness,[status(thm)],[c_79]) ).
tcf(c_95,plain,
multiply(k,inverse(b)) != identity,
inference(well_definedness,[status(thm)],[c_80]) ).
tcf(c_96,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(well_definedness,[status(thm)],[c_65]) ).
tcf(c_97,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(well_definedness,[status(thm)],[c_66]) ).
tcf(c_98,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(well_definedness,[status(thm)],[c_67]) ).
tcf(c_99,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(well_definedness,[status(thm)],[c_68]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( multiply(X2,X5) = X4 )
| ( multiply(X1,X5) != X3 )
| ( multiply(X0,X3) != X4 )
| ( multiply(X0,X1) != X2 ) ),
inference(well_definedness,[status(thm)],[c_72]) ).
tcf(c_165,plain,
! [X0: $i] : multiply(X0,multiply(X0,X0)) = identity,
inference(unflattening,[status(thm)],[c_86]) ).
tcf(c_167,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(unflattening,[status(thm)],[c_105]) ).
tcf(c_204,definition,
iPr_def_10 = inverse(b),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_205,definition,
iPr_def_11 = multiply(k,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_206,definition,
iPr_def_12 = inverse(h),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_207,definition,
iPr_def_13 = multiply(j,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_208,definition,
iPr_def_14 = multiply(h,b),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_209,definition,
iPr_def_15 = multiply(d,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_210,definition,
iPr_def_16 = inverse(a),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_211,definition,
iPr_def_17 = multiply(c,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_212,definition,
iPr_def_18 = multiply(a,b),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_213,plain,
iPr_def_11 != identity,
inference(demodulation,[status(thm)],[c_95,c_204,c_205]) ).
tcf(c_214,plain,
iPr_def_13 = k,
inference(demodulation,[status(thm)],[c_94,c_206,c_207]) ).
tcf(c_215,plain,
iPr_def_14 = j,
inference(demodulation,[status(thm)],[c_93,c_208]) ).
tcf(c_216,plain,
iPr_def_15 = h,
inference(demodulation,[status(thm)],[c_92,c_209]) ).
tcf(c_217,plain,
iPr_def_17 = d,
inference(demodulation,[status(thm)],[c_91,c_210,c_211]) ).
tcf(c_218,plain,
iPr_def_18 = c,
inference(demodulation,[status(thm)],[c_90,c_212]) ).
tcf(c_285,plain,
inverse(iPr_def_15) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_206,c_216]) ).
tcf(c_286,plain,
multiply(iPr_def_13,iPr_def_10) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_205,c_214]) ).
tcf(c_287,plain,
multiply(iPr_def_14,iPr_def_12) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_207,c_215]) ).
tcf(c_288,plain,
multiply(iPr_def_15,b) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_208,c_216]) ).
tcf(c_289,plain,
multiply(iPr_def_17,iPr_def_10) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_209,c_217]) ).
tcf(c_290,plain,
multiply(iPr_def_18,iPr_def_16) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_211,c_218]) ).
tcf(c_292,plain,
multiply(iPr_def_16,a) = identity,
inference(superposition,[status(thm)],[c_210,c_98]) ).
tcf(c_293,plain,
multiply(iPr_def_10,b) = identity,
inference(superposition,[status(thm)],[c_204,c_98]) ).
tcf(c_294,plain,
multiply(iPr_def_12,iPr_def_15) = identity,
inference(superposition,[status(thm)],[c_285,c_98]) ).
tcf(c_298,plain,
multiply(a,iPr_def_16) = identity,
inference(superposition,[status(thm)],[c_210,c_99]) ).
tcf(c_299,plain,
multiply(b,iPr_def_10) = identity,
inference(superposition,[status(thm)],[c_204,c_99]) ).
tcf(c_301,plain,
multiply(iPr_def_15,iPr_def_12) = identity,
inference(superposition,[status(thm)],[c_285,c_99]) ).
tcf(c_308,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_165,c_167]) ).
tcf(c_309,plain,
! [X0: $i] : multiply(a,multiply(b,X0)) = multiply(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_212,c_167]) ).
tcf(c_312,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_98,c_167]) ).
tcf(c_315,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(iPr_def_10,X0)) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_286,c_167]) ).
tcf(c_316,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(iPr_def_12,X0)) = multiply(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_287,c_167]) ).
tcf(c_317,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(b,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_288,c_167]) ).
tcf(c_318,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(iPr_def_10,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_289,c_167]) ).
tcf(c_320,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(a,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_292,c_167]) ).
tcf(c_321,plain,
! [X0: $i] : multiply(iPr_def_10,multiply(b,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_293,c_167]) ).
tcf(c_322,plain,
! [X0: $i] : multiply(iPr_def_12,multiply(iPr_def_15,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_294,c_167]) ).
tcf(c_323,plain,
! [X0: $i] : multiply(a,multiply(iPr_def_16,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_298,c_167]) ).
tcf(c_324,plain,
! [X0: $i] : multiply(b,multiply(iPr_def_10,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_299,c_167]) ).
tcf(c_325,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(iPr_def_12,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_301,c_167]) ).
tcf(c_331,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(iPr_def_12,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_325,c_96]) ).
tcf(c_332,plain,
! [X0: $i] : multiply(b,multiply(iPr_def_10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_324,c_96]) ).
tcf(c_333,plain,
! [X0: $i] : multiply(a,multiply(iPr_def_16,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_323,c_96]) ).
tcf(c_334,plain,
! [X0: $i] : multiply(iPr_def_12,multiply(iPr_def_15,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_322,c_96]) ).
tcf(c_335,plain,
! [X0: $i] : multiply(iPr_def_10,multiply(b,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_321,c_96]) ).
tcf(c_336,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(a,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_320,c_96]) ).
tcf(c_341,plain,
multiply(a,identity) = multiply(iPr_def_18,iPr_def_10),
inference(superposition,[status(thm)],[c_299,c_309]) ).
tcf(c_348,plain,
multiply(iPr_def_15,identity) = inverse(iPr_def_12),
inference(superposition,[status(thm)],[c_99,c_331]) ).
tcf(c_351,plain,
inverse(iPr_def_12) = iPr_def_15,
inference(demodulation,[status(thm)],[c_348,c_97]) ).
tcf(c_357,plain,
multiply(b,identity) = inverse(iPr_def_10),
inference(superposition,[status(thm)],[c_99,c_332]) ).
tcf(c_361,plain,
inverse(iPr_def_10) = b,
inference(demodulation,[status(thm)],[c_357,c_97]) ).
tcf(c_365,plain,
multiply(a,identity) = multiply(iPr_def_16,iPr_def_16),
inference(superposition,[status(thm)],[c_165,c_333]) ).
tcf(c_367,plain,
multiply(a,identity) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_99,c_333]) ).
tcf(c_374,plain,
multiply(iPr_def_11,b) = multiply(iPr_def_13,identity),
inference(superposition,[status(thm)],[c_293,c_315]) ).
tcf(c_380,plain,
multiply(iPr_def_13,identity) = multiply(iPr_def_14,iPr_def_12),
inference(superposition,[status(thm)],[c_97,c_316]) ).
tcf(c_382,plain,
multiply(iPr_def_13,iPr_def_15) = multiply(iPr_def_14,identity),
inference(superposition,[status(thm)],[c_294,c_316]) ).
tcf(c_384,plain,
multiply(iPr_def_11,b) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_380,c_287,c_374]) ).
tcf(c_389,plain,
multiply(iPr_def_14,identity) = multiply(iPr_def_15,b),
inference(superposition,[status(thm)],[c_97,c_317]) ).
tcf(c_395,plain,
multiply(iPr_def_13,iPr_def_15) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_389,c_288,c_382]) ).
tcf(c_398,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(iPr_def_15,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_395,c_167]) ).
tcf(c_403,plain,
multiply(iPr_def_15,b) = multiply(iPr_def_17,identity),
inference(superposition,[status(thm)],[c_293,c_318]) ).
tcf(c_405,plain,
multiply(iPr_def_17,identity) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_403,c_288]) ).
tcf(c_408,plain,
iPr_def_14 = iPr_def_17,
inference(demodulation,[status(thm)],[c_405,c_97]) ).
tcf(c_410,plain,
multiply(iPr_def_18,iPr_def_16) = iPr_def_14,
inference(demodulation,[status(thm)],[c_290,c_408]) ).
tcf(c_411,plain,
multiply(iPr_def_14,iPr_def_10) = iPr_def_15,
inference(demodulation,[status(thm)],[c_289,c_408]) ).
tcf(c_414,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X0,multiply(X0,X1))) = X1,
inference(demodulation,[status(thm)],[c_308,c_96,c_167]) ).
tcf(c_421,plain,
multiply(a,multiply(a,iPr_def_18)) = b,
inference(superposition,[status(thm)],[c_212,c_414]) ).
tcf(c_424,plain,
! [X0: $i] : multiply(X0,multiply(X0,identity)) = inverse(X0),
inference(superposition,[status(thm)],[c_99,c_414]) ).
tcf(c_426,plain,
multiply(iPr_def_13,multiply(iPr_def_13,iPr_def_11)) = iPr_def_10,
inference(superposition,[status(thm)],[c_286,c_414]) ).
tcf(c_428,plain,
multiply(iPr_def_15,multiply(iPr_def_15,iPr_def_14)) = b,
inference(superposition,[status(thm)],[c_288,c_414]) ).
tcf(c_439,plain,
! [X0: $i] : multiply(a,multiply(a,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_333,c_414]) ).
tcf(c_441,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(iPr_def_15,X0)) = multiply(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_331,c_414]) ).
tcf(c_442,plain,
multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_13)) = b,
inference(superposition,[status(thm)],[c_384,c_414]) ).
tcf(c_443,plain,
multiply(iPr_def_13,multiply(iPr_def_13,iPr_def_14)) = iPr_def_15,
inference(superposition,[status(thm)],[c_395,c_414]) ).
tcf(c_452,plain,
! [X0: $i] : multiply(iPr_def_12,multiply(iPr_def_12,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_414,c_331]) ).
tcf(c_458,plain,
! [X0: $i] : multiply(X0,X0) = inverse(X0),
inference(light_normalisation,[status(thm)],[c_424,c_97]) ).
tcf(c_461,plain,
multiply(iPr_def_16,iPr_def_18) = b,
inference(demodulation,[status(thm)],[c_421,c_439]) ).
tcf(c_463,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(iPr_def_18,X0)) = multiply(b,X0),
inference(superposition,[status(thm)],[c_461,c_167]) ).
tcf(c_465,plain,
multiply(iPr_def_18,multiply(iPr_def_18,iPr_def_14)) = iPr_def_16,
inference(superposition,[status(thm)],[c_410,c_414]) ).
tcf(c_466,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(iPr_def_16,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_410,c_167]) ).
tcf(c_467,plain,
multiply(iPr_def_14,multiply(iPr_def_14,iPr_def_15)) = iPr_def_10,
inference(superposition,[status(thm)],[c_411,c_414]) ).
tcf(c_471,plain,
inverse(iPr_def_16) = a,
inference(demodulation,[status(thm)],[c_367,c_97]) ).
tcf(c_479,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X0,X1)) = multiply(inverse(X0),X1),
inference(superposition,[status(thm)],[c_458,c_167]) ).
tcf(c_482,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,multiply(X0,X1))) = inverse(multiply(X0,X1)),
inference(superposition,[status(thm)],[c_458,c_167]) ).
tcf(c_483,plain,
multiply(iPr_def_15,inverse(b)) = multiply(iPr_def_14,b),
inference(superposition,[status(thm)],[c_458,c_317]) ).
tcf(c_487,plain,
multiply(iPr_def_14,inverse(iPr_def_12)) = multiply(iPr_def_13,iPr_def_12),
inference(superposition,[status(thm)],[c_458,c_316]) ).
tcf(c_493,plain,
multiply(iPr_def_13,iPr_def_12) = multiply(iPr_def_14,iPr_def_15),
inference(light_normalisation,[status(thm)],[c_487,c_351]) ).
tcf(c_496,plain,
multiply(iPr_def_14,b) = multiply(iPr_def_15,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_483,c_204]) ).
tcf(c_498,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_414,c_479]) ).
tcf(c_499,plain,
multiply(inverse(iPr_def_13),iPr_def_11) = iPr_def_10,
inference(demodulation,[status(thm)],[c_426,c_479]) ).
tcf(c_500,plain,
! [X0: $i] : multiply(inverse(iPr_def_13),multiply(iPr_def_11,X0)) = multiply(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_499,c_167]) ).
tcf(c_503,plain,
multiply(iPr_def_12,iPr_def_14) = b,
inference(demodulation,[status(thm)],[c_428,c_441]) ).
tcf(c_504,plain,
! [X0: $i] : multiply(iPr_def_12,multiply(iPr_def_14,X0)) = multiply(b,X0),
inference(superposition,[status(thm)],[c_503,c_167]) ).
tcf(c_505,plain,
multiply(iPr_def_13,iPr_def_14) = multiply(iPr_def_14,b),
inference(superposition,[status(thm)],[c_503,c_316]) ).
tcf(c_511,plain,
multiply(inverse(iPr_def_11),iPr_def_13) = b,
inference(demodulation,[status(thm)],[c_442,c_479]) ).
tcf(c_512,plain,
! [X0: $i] : multiply(inverse(iPr_def_11),multiply(iPr_def_13,X0)) = multiply(b,X0),
inference(superposition,[status(thm)],[c_511,c_167]) ).
tcf(c_535,plain,
multiply(iPr_def_16,inverse(a)) = a,
inference(superposition,[status(thm)],[c_458,c_336]) ).
tcf(c_544,plain,
multiply(iPr_def_16,iPr_def_16) = a,
inference(light_normalisation,[status(thm)],[c_535,c_210]) ).
tcf(c_545,plain,
multiply(iPr_def_18,iPr_def_10) = a,
inference(light_normalisation,[status(thm)],[c_341,c_365,c_544]) ).
tcf(c_547,plain,
multiply(inverse(iPr_def_13),iPr_def_14) = iPr_def_15,
inference(demodulation,[status(thm)],[c_443,c_479]) ).
tcf(c_548,plain,
! [X0: $i] : multiply(inverse(iPr_def_13),multiply(iPr_def_14,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_547,c_167]) ).
tcf(c_549,plain,
multiply(inverse(iPr_def_18),iPr_def_14) = iPr_def_16,
inference(demodulation,[status(thm)],[c_465,c_479]) ).
tcf(c_550,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),multiply(iPr_def_14,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_549,c_167]) ).
tcf(c_551,plain,
multiply(iPr_def_14,multiply(iPr_def_13,iPr_def_12)) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_467,c_493]) ).
tcf(c_573,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_312,c_96]) ).
tcf(c_588,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_167,c_573]) ).
tcf(c_610,plain,
multiply(inverse(iPr_def_18),a) = iPr_def_10,
inference(superposition,[status(thm)],[c_545,c_573]) ).
tcf(c_648,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),multiply(a,X0)) = multiply(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_610,c_167]) ).
tcf(c_668,plain,
multiply(iPr_def_14,a) = multiply(iPr_def_18,identity),
inference(superposition,[status(thm)],[c_292,c_466]) ).
tcf(c_691,plain,
multiply(iPr_def_14,a) = iPr_def_18,
inference(demodulation,[status(thm)],[c_668,c_97]) ).
tcf(c_692,plain,
multiply(inverse(iPr_def_14),iPr_def_18) = a,
inference(superposition,[status(thm)],[c_691,c_573]) ).
tcf(c_700,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(X0,identity),
inference(superposition,[status(thm)],[c_99,c_498]) ).
tcf(c_734,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_700,c_97]) ).
tcf(c_749,plain,
inverse(a) = iPr_def_16,
inference(superposition,[status(thm)],[c_471,c_734]) ).
tcf(c_765,plain,
! [X0: $i] : multiply(inverse(iPr_def_14),multiply(iPr_def_18,X0)) = multiply(a,X0),
inference(superposition,[status(thm)],[c_692,c_167]) ).
tcf(c_790,plain,
! [X0: $i] : multiply(multiply(iPr_def_13,iPr_def_12),X0) = multiply(iPr_def_14,multiply(iPr_def_15,X0)),
inference(superposition,[status(thm)],[c_493,c_167]) ).
tcf(c_807,plain,
multiply(iPr_def_13,iPr_def_14) = multiply(iPr_def_15,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_496,c_505]) ).
tcf(c_819,plain,
multiply(iPr_def_12,inverse(iPr_def_14)) = multiply(b,iPr_def_14),
inference(superposition,[status(thm)],[c_458,c_504]) ).
tcf(c_821,plain,
multiply(b,inverse(iPr_def_14)) = multiply(iPr_def_12,identity),
inference(superposition,[status(thm)],[c_99,c_504]) ).
tcf(c_822,plain,
multiply(b,iPr_def_12) = multiply(iPr_def_12,iPr_def_13),
inference(superposition,[status(thm)],[c_287,c_504]) ).
tcf(c_823,plain,
! [X0: $i] : multiply(b,multiply(inverse(iPr_def_14),X0)) = multiply(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_498,c_504]) ).
tcf(c_824,plain,
! [X0: $i] : multiply(b,multiply(iPr_def_12,X0)) = multiply(iPr_def_12,multiply(iPr_def_13,X0)),
inference(superposition,[status(thm)],[c_316,c_504]) ).
tcf(c_864,plain,
multiply(b,inverse(iPr_def_14)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_821,c_97]) ).
tcf(c_869,plain,
multiply(iPr_def_10,iPr_def_12) = inverse(iPr_def_14),
inference(superposition,[status(thm)],[c_864,c_335]) ).
tcf(c_900,plain,
! [X0: $i] : multiply(iPr_def_10,multiply(iPr_def_12,X0)) = multiply(inverse(iPr_def_14),X0),
inference(superposition,[status(thm)],[c_869,c_167]) ).
tcf(c_1220,plain,
multiply(inverse(iPr_def_13),iPr_def_10) = multiply(iPr_def_13,iPr_def_11),
inference(superposition,[status(thm)],[c_286,c_479]) ).
tcf(c_1221,plain,
multiply(inverse(iPr_def_14),iPr_def_12) = multiply(iPr_def_14,iPr_def_13),
inference(superposition,[status(thm)],[c_287,c_479]) ).
tcf(c_1223,plain,
multiply(inverse(iPr_def_18),iPr_def_16) = multiply(iPr_def_18,iPr_def_14),
inference(superposition,[status(thm)],[c_410,c_479]) ).
tcf(c_1245,plain,
multiply(inverse(iPr_def_11),b) = multiply(iPr_def_11,iPr_def_13),
inference(superposition,[status(thm)],[c_384,c_479]) ).
tcf(c_1252,plain,
multiply(inverse(iPr_def_16),iPr_def_18) = multiply(iPr_def_16,b),
inference(superposition,[status(thm)],[c_461,c_479]) ).
tcf(c_1259,plain,
multiply(iPr_def_15,multiply(iPr_def_13,iPr_def_14)) = multiply(inverse(iPr_def_15),iPr_def_10),
inference(superposition,[status(thm)],[c_807,c_479]) ).
tcf(c_1281,plain,
multiply(inverse(iPr_def_10),iPr_def_12) = multiply(iPr_def_10,inverse(iPr_def_14)),
inference(superposition,[status(thm)],[c_869,c_479]) ).
tcf(c_1304,plain,
! [X0: $i] : multiply(iPr_def_12,multiply(iPr_def_13,multiply(iPr_def_12,X0))) = multiply(b,multiply(inverse(iPr_def_12),X0)),
inference(superposition,[status(thm)],[c_479,c_824]) ).
tcf(c_1308,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(inverse(iPr_def_15),X0)) = multiply(iPr_def_14,multiply(iPr_def_15,X0)),
inference(superposition,[status(thm)],[c_479,c_398]) ).
tcf(c_1315,plain,
multiply(a,iPr_def_18) = multiply(iPr_def_16,b),
inference(light_normalisation,[status(thm)],[c_1252,c_471]) ).
tcf(c_1329,plain,
multiply(iPr_def_10,inverse(iPr_def_14)) = multiply(iPr_def_12,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_1281,c_361,c_822]) ).
tcf(c_1345,plain,
multiply(iPr_def_15,multiply(iPr_def_13,iPr_def_14)) = multiply(iPr_def_12,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_1259,c_285]) ).
tcf(c_1358,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(iPr_def_12,X0)) = multiply(iPr_def_14,multiply(iPr_def_15,X0)),
inference(light_normalisation,[status(thm)],[c_1308,c_285]) ).
tcf(c_1375,plain,
! [X0: $i] : multiply(iPr_def_12,multiply(iPr_def_13,multiply(iPr_def_12,X0))) = multiply(b,multiply(iPr_def_15,X0)),
inference(light_normalisation,[status(thm)],[c_1304,c_351]) ).
tcf(c_1382,plain,
multiply(iPr_def_10,inverse(iPr_def_14)) = multiply(b,iPr_def_12),
inference(demodulation,[status(thm)],[c_822,c_1329]) ).
tcf(c_1454,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(iPr_def_12,multiply(b,X0))) = multiply(iPr_def_14,multiply(iPr_def_14,X0)),
inference(superposition,[status(thm)],[c_317,c_1358]) ).
tcf(c_1486,plain,
multiply(inverse(iPr_def_13),identity) = multiply(iPr_def_10,inverse(iPr_def_11)),
inference(superposition,[status(thm)],[c_99,c_500]) ).
tcf(c_1499,plain,
multiply(iPr_def_10,inverse(iPr_def_11)) = inverse(iPr_def_13),
inference(demodulation,[status(thm)],[c_1486,c_97]) ).
tcf(c_1500,plain,
multiply(inverse(iPr_def_10),inverse(iPr_def_11)) = multiply(iPr_def_10,inverse(iPr_def_13)),
inference(superposition,[status(thm)],[c_1499,c_479]) ).
tcf(c_1508,plain,
multiply(b,inverse(iPr_def_11)) = multiply(iPr_def_10,inverse(iPr_def_13)),
inference(light_normalisation,[status(thm)],[c_1500,c_361]) ).
tcf(c_1638,plain,
multiply(iPr_def_15,multiply(iPr_def_13,iPr_def_12)) = multiply(inverse(iPr_def_13),iPr_def_10),
inference(superposition,[status(thm)],[c_551,c_548]) ).
tcf(c_1651,plain,
multiply(iPr_def_15,multiply(iPr_def_13,iPr_def_12)) = multiply(iPr_def_13,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_1638,c_1220]) ).
tcf(c_1662,plain,
multiply(inverse(iPr_def_18),identity) = multiply(iPr_def_16,inverse(iPr_def_14)),
inference(superposition,[status(thm)],[c_99,c_550]) ).
tcf(c_1665,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),multiply(iPr_def_13,X0)) = multiply(iPr_def_16,multiply(iPr_def_12,X0)),
inference(superposition,[status(thm)],[c_316,c_550]) ).
tcf(c_1721,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(multiply(iPr_def_13,iPr_def_12),X0)) = multiply(multiply(iPr_def_13,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_1651,c_167]) ).
tcf(c_1729,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(iPr_def_13,multiply(iPr_def_12,X0))) = multiply(multiply(iPr_def_13,iPr_def_11),X0),
inference(light_normalisation,[status(thm)],[c_1721,c_790,c_1358]) ).
tcf(c_1741,plain,
multiply(iPr_def_16,inverse(iPr_def_14)) = inverse(iPr_def_18),
inference(demodulation,[status(thm)],[c_1662,c_97]) ).
tcf(c_1751,plain,
multiply(inverse(iPr_def_18),inverse(a)) = multiply(iPr_def_10,a),
inference(superposition,[status(thm)],[c_458,c_648]) ).
tcf(c_1772,plain,
multiply(iPr_def_10,a) = multiply(iPr_def_18,iPr_def_14),
inference(light_normalisation,[status(thm)],[c_1751,c_749,c_1223]) ).
tcf(c_1779,plain,
multiply(inverse(iPr_def_18),iPr_def_16) = multiply(iPr_def_10,a),
inference(demodulation,[status(thm)],[c_1223,c_1772]) ).
tcf(c_1783,plain,
multiply(inverse(iPr_def_14),inverse(iPr_def_18)) = multiply(a,iPr_def_18),
inference(superposition,[status(thm)],[c_458,c_765]) ).
tcf(c_1802,plain,
multiply(inverse(iPr_def_14),inverse(iPr_def_18)) = multiply(iPr_def_16,b),
inference(light_normalisation,[status(thm)],[c_1783,c_1315]) ).
tcf(c_1812,plain,
multiply(inverse(iPr_def_14),iPr_def_12) = multiply(iPr_def_10,inverse(iPr_def_12)),
inference(superposition,[status(thm)],[c_458,c_900]) ).
tcf(c_1824,plain,
! [X0: $i] : multiply(inverse(iPr_def_10),multiply(iPr_def_12,X0)) = multiply(iPr_def_10,multiply(inverse(iPr_def_14),X0)),
inference(superposition,[status(thm)],[c_900,c_479]) ).
tcf(c_1835,plain,
multiply(inverse(iPr_def_14),iPr_def_12) = multiply(iPr_def_10,iPr_def_15),
inference(light_normalisation,[status(thm)],[c_1812,c_351,c_1221]) ).
tcf(c_1841,plain,
! [X0: $i] : multiply(iPr_def_10,multiply(inverse(iPr_def_14),X0)) = multiply(iPr_def_12,multiply(iPr_def_13,X0)),
inference(light_normalisation,[status(thm)],[c_1824,c_361,c_824]) ).
tcf(c_1844,plain,
! [X0: $i] : multiply(iPr_def_10,multiply(inverse(iPr_def_14),X0)) = multiply(b,multiply(iPr_def_12,X0)),
inference(demodulation,[status(thm)],[c_824,c_1841]) ).
tcf(c_1928,plain,
multiply(iPr_def_16,multiply(iPr_def_10,a)) = multiply(b,iPr_def_14),
inference(superposition,[status(thm)],[c_1772,c_463]) ).
tcf(c_1929,plain,
multiply(iPr_def_16,multiply(iPr_def_10,a)) = multiply(iPr_def_12,inverse(iPr_def_14)),
inference(light_normalisation,[status(thm)],[c_1928,c_819]) ).
tcf(c_2032,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(iPr_def_12,multiply(iPr_def_10,X0))) = multiply(inverse(iPr_def_18),multiply(iPr_def_11,X0)),
inference(superposition,[status(thm)],[c_315,c_1665]) ).
tcf(c_2216,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(iPr_def_12,multiply(b,X0))) = multiply(inverse(iPr_def_14),X0),
inference(demodulation,[status(thm)],[c_1454,c_479]) ).
tcf(c_2253,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(iPr_def_13,multiply(iPr_def_12,X0))) = multiply(iPr_def_13,multiply(iPr_def_11,X0)),
inference(demodulation,[status(thm)],[c_1729,c_167]) ).
tcf(c_2263,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(iPr_def_11,multiply(iPr_def_15,X0))) = multiply(iPr_def_15,multiply(iPr_def_13,X0)),
inference(superposition,[status(thm)],[c_334,c_2253]) ).
tcf(c_2270,plain,
! [X0: $i] : multiply(inverse(iPr_def_15),multiply(iPr_def_13,multiply(iPr_def_12,X0))) = multiply(iPr_def_15,multiply(iPr_def_13,multiply(iPr_def_11,X0))),
inference(superposition,[status(thm)],[c_2253,c_479]) ).
tcf(c_2288,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(iPr_def_13,multiply(iPr_def_11,X0))) = multiply(b,multiply(iPr_def_15,X0)),
inference(light_normalisation,[status(thm)],[c_2270,c_285,c_1375]) ).
tcf(c_2327,plain,
! [X0: $i] : multiply(iPr_def_12,multiply(b,multiply(iPr_def_15,X0))) = multiply(iPr_def_13,multiply(iPr_def_11,X0)),
inference(superposition,[status(thm)],[c_2288,c_334]) ).
tcf(c_2513,plain,
multiply(iPr_def_16,multiply(inverse(iPr_def_14),inverse(iPr_def_18))) = inverse(inverse(iPr_def_18)),
inference(superposition,[status(thm)],[c_1741,c_482]) ).
tcf(c_2563,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(X0,multiply(b,X0))) = multiply(iPr_def_15,inverse(multiply(b,X0))),
inference(superposition,[status(thm)],[c_482,c_317]) ).
tcf(c_2702,plain,
multiply(iPr_def_16,multiply(iPr_def_16,b)) = inverse(inverse(iPr_def_18)),
inference(light_normalisation,[status(thm)],[c_2513,c_1802]) ).
tcf(c_3141,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,identity)) = inverse(X1),
inference(superposition,[status(thm)],[c_99,c_588]) ).
tcf(c_3324,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),X0) = inverse(X1),
inference(light_normalisation,[status(thm)],[c_3141,c_97]) ).
tcf(c_3572,plain,
multiply(inverse(iPr_def_18),multiply(iPr_def_16,multiply(iPr_def_10,a))) = inverse(multiply(iPr_def_10,a)),
inference(superposition,[status(thm)],[c_1779,c_482]) ).
tcf(c_3580,plain,
multiply(inverse(iPr_def_18),multiply(iPr_def_12,inverse(iPr_def_14))) = inverse(multiply(iPr_def_10,a)),
inference(light_normalisation,[status(thm)],[c_3572,c_1929]) ).
tcf(c_3645,plain,
! [X0: $i] : inverse(multiply(b,X0)) = multiply(inverse(X0),iPr_def_10),
inference(superposition,[status(thm)],[c_335,c_3324]) ).
tcf(c_3648,plain,
! [X0: $i] : inverse(multiply(iPr_def_10,X0)) = multiply(inverse(X0),b),
inference(superposition,[status(thm)],[c_332,c_3324]) ).
tcf(c_3991,plain,
! [X0: $i] : multiply(iPr_def_12,multiply(b,multiply(inverse(iPr_def_15),X0))) = multiply(iPr_def_13,multiply(iPr_def_11,multiply(iPr_def_15,X0))),
inference(superposition,[status(thm)],[c_479,c_2327]) ).
tcf(c_4026,plain,
! [X0: $i] : multiply(iPr_def_12,multiply(iPr_def_10,multiply(inverse(iPr_def_14),X0))) = multiply(iPr_def_15,multiply(iPr_def_13,X0)),
inference(light_normalisation,[status(thm)],[c_3991,c_285,c_1844,c_2263]) ).
tcf(c_4268,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),multiply(iPr_def_11,multiply(inverse(iPr_def_14),X0))) = multiply(iPr_def_16,multiply(iPr_def_15,multiply(iPr_def_13,X0))),
inference(superposition,[status(thm)],[c_4026,c_2032]) ).
tcf(c_4465,plain,
! [X0: $i] : multiply(inverse(iPr_def_14),multiply(inverse(iPr_def_14),X0)) = multiply(iPr_def_13,multiply(iPr_def_12,multiply(iPr_def_12,X0))),
inference(superposition,[status(thm)],[c_823,c_2216]) ).
tcf(c_4474,plain,
! [X0: $i] : multiply(inverse(iPr_def_14),multiply(inverse(iPr_def_14),X0)) = multiply(iPr_def_14,X0),
inference(light_normalisation,[status(thm)],[c_4465,c_398,c_452]) ).
tcf(c_4528,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(X0,multiply(b,X0))) = multiply(iPr_def_15,multiply(inverse(X0),iPr_def_10)),
inference(light_normalisation,[status(thm)],[c_2563,c_3645]) ).
tcf(c_4569,plain,
multiply(iPr_def_15,multiply(inverse(iPr_def_12),iPr_def_10)) = multiply(iPr_def_13,multiply(b,iPr_def_12)),
inference(superposition,[status(thm)],[c_4528,c_316]) ).
tcf(c_4584,plain,
multiply(iPr_def_13,multiply(iPr_def_10,inverse(iPr_def_14))) = multiply(iPr_def_12,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_4569,c_351,c_807,c_1345,c_1382]) ).
tcf(c_4622,plain,
multiply(iPr_def_11,inverse(iPr_def_14)) = multiply(iPr_def_12,iPr_def_10),
inference(demodulation,[status(thm)],[c_4584,c_315]) ).
tcf(c_4630,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,inverse(iPr_def_14)),X0) = multiply(iPr_def_12,multiply(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_4622,c_167]) ).
tcf(c_4641,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(inverse(iPr_def_14),X0)) = multiply(iPr_def_12,multiply(iPr_def_10,X0)),
inference(demodulation,[status(thm)],[c_4630,c_167]) ).
tcf(c_4647,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(inverse(iPr_def_14),multiply(inverse(iPr_def_14),X0))) = multiply(iPr_def_15,multiply(iPr_def_13,X0)),
inference(demodulation,[status(thm)],[c_4026,c_4641]) ).
tcf(c_4650,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_14,X0)) = multiply(iPr_def_15,multiply(iPr_def_13,X0)),
inference(light_normalisation,[status(thm)],[c_4647,c_4474]) ).
tcf(c_4653,plain,
multiply(iPr_def_11,multiply(iPr_def_14,iPr_def_12)) = multiply(iPr_def_13,iPr_def_11),
inference(demodulation,[status(thm)],[c_1651,c_4650]) ).
tcf(c_4655,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_14,multiply(iPr_def_12,X0))) = multiply(iPr_def_13,multiply(iPr_def_11,X0)),
inference(demodulation,[status(thm)],[c_2253,c_4650]) ).
tcf(c_4657,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_13,X0)) = multiply(iPr_def_13,multiply(iPr_def_11,X0)),
inference(light_normalisation,[status(thm)],[c_4655,c_316]) ).
tcf(c_4662,plain,
multiply(iPr_def_11,iPr_def_13) = multiply(iPr_def_13,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_4653,c_287]) ).
tcf(c_4664,plain,
multiply(inverse(iPr_def_13),iPr_def_10) = multiply(iPr_def_11,iPr_def_13),
inference(demodulation,[status(thm)],[c_1220,c_4662]) ).
tcf(c_4672,plain,
multiply(iPr_def_11,multiply(inverse(iPr_def_14),iPr_def_12)) = multiply(iPr_def_12,inverse(iPr_def_14)),
inference(superposition,[status(thm)],[c_869,c_4641]) ).
tcf(c_4687,plain,
multiply(iPr_def_11,multiply(iPr_def_10,iPr_def_15)) = multiply(iPr_def_12,inverse(iPr_def_14)),
inference(light_normalisation,[status(thm)],[c_4672,c_1835]) ).
tcf(c_4726,plain,
multiply(iPr_def_13,multiply(iPr_def_11,iPr_def_13)) = multiply(inverse(iPr_def_13),iPr_def_11),
inference(superposition,[status(thm)],[c_4662,c_479]) ).
tcf(c_4727,plain,
multiply(inverse(iPr_def_13),multiply(iPr_def_11,iPr_def_13)) = iPr_def_11,
inference(superposition,[status(thm)],[c_4662,c_573]) ).
tcf(c_4732,plain,
multiply(iPr_def_13,multiply(iPr_def_11,iPr_def_13)) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_4726,c_499]) ).
tcf(c_4742,plain,
multiply(iPr_def_11,inverse(iPr_def_13)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_4732,c_458,c_4657]) ).
tcf(c_4746,plain,
multiply(inverse(iPr_def_13),iPr_def_10) = multiply(iPr_def_10,inverse(iPr_def_13)),
inference(superposition,[status(thm)],[c_4742,c_500]) ).
tcf(c_4768,plain,
multiply(iPr_def_10,inverse(iPr_def_13)) = multiply(iPr_def_11,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_4664,c_4746]) ).
tcf(c_4769,plain,
multiply(iPr_def_10,inverse(iPr_def_13)) = multiply(iPr_def_13,iPr_def_11),
inference(demodulation,[status(thm)],[c_4662,c_4768]) ).
tcf(c_4770,plain,
multiply(inverse(iPr_def_11),b) = multiply(iPr_def_10,inverse(iPr_def_13)),
inference(demodulation,[status(thm)],[c_1245,c_4768]) ).
tcf(c_4774,plain,
multiply(inverse(iPr_def_13),multiply(iPr_def_10,inverse(iPr_def_13))) = multiply(iPr_def_10,iPr_def_13),
inference(superposition,[status(thm)],[c_4768,c_500]) ).
tcf(c_4776,plain,
multiply(iPr_def_10,iPr_def_13) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_4727,c_4768,c_4774]) ).
tcf(c_4785,plain,
multiply(b,iPr_def_11) = iPr_def_13,
inference(superposition,[status(thm)],[c_4776,c_332]) ).
tcf(c_6222,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),multiply(iPr_def_11,multiply(inverse(iPr_def_14),X0))) = multiply(iPr_def_16,multiply(iPr_def_11,multiply(iPr_def_14,X0))),
inference(light_normalisation,[status(thm)],[c_4268,c_4650]) ).
tcf(c_6238,plain,
multiply(inverse(iPr_def_18),multiply(iPr_def_11,multiply(iPr_def_10,iPr_def_15))) = multiply(iPr_def_16,multiply(iPr_def_11,multiply(iPr_def_14,iPr_def_12))),
inference(superposition,[status(thm)],[c_1835,c_6222]) ).
tcf(c_6252,plain,
multiply(iPr_def_16,multiply(iPr_def_10,inverse(iPr_def_13))) = inverse(multiply(iPr_def_10,a)),
inference(light_normalisation,[status(thm)],[c_6238,c_287,c_3580,c_4687,c_4768]) ).
tcf(c_6262,plain,
multiply(iPr_def_16,multiply(iPr_def_10,inverse(iPr_def_13))) = multiply(iPr_def_16,b),
inference(demodulation,[status(thm)],[c_6252,c_749,c_3648]) ).
tcf(c_6263,plain,
multiply(inverse(iPr_def_16),multiply(iPr_def_10,inverse(iPr_def_13))) = multiply(iPr_def_16,multiply(iPr_def_16,b)),
inference(superposition,[status(thm)],[c_6262,c_479]) ).
tcf(c_6273,plain,
multiply(a,multiply(iPr_def_10,inverse(iPr_def_13))) = inverse(inverse(iPr_def_18)),
inference(light_normalisation,[status(thm)],[c_6263,c_471,c_2702]) ).
tcf(c_6365,plain,
multiply(a,multiply(iPr_def_10,inverse(iPr_def_13))) = multiply(iPr_def_18,inverse(iPr_def_11)),
inference(superposition,[status(thm)],[c_1508,c_309]) ).
tcf(c_6367,plain,
multiply(iPr_def_18,inverse(iPr_def_11)) = inverse(inverse(iPr_def_18)),
inference(light_normalisation,[status(thm)],[c_6365,c_6273]) ).
tcf(c_6430,plain,
multiply(iPr_def_18,inverse(iPr_def_11)) = iPr_def_18,
inference(demodulation,[status(thm)],[c_6367,c_734]) ).
tcf(c_6436,plain,
multiply(b,inverse(iPr_def_11)) = multiply(iPr_def_16,iPr_def_18),
inference(superposition,[status(thm)],[c_6430,c_463]) ).
tcf(c_6437,plain,
multiply(iPr_def_10,inverse(iPr_def_13)) = b,
inference(light_normalisation,[status(thm)],[c_6436,c_461,c_1508]) ).
tcf(c_6443,plain,
multiply(iPr_def_13,iPr_def_11) = b,
inference(demodulation,[status(thm)],[c_4769,c_6437]) ).
tcf(c_6451,plain,
multiply(inverse(iPr_def_11),b) = multiply(b,iPr_def_11),
inference(superposition,[status(thm)],[c_6443,c_512]) ).
tcf(c_6455,plain,
b = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_6451,c_4770,c_4785,c_6437]) ).
tcf(c_6547,plain,
multiply(iPr_def_10,iPr_def_13) = identity,
inference(demodulation,[status(thm)],[c_293,c_6455]) ).
tcf(c_6570,plain,
identity = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_6547,c_4776]) ).
tcf(c_6580,plain,
iPr_def_11 != iPr_def_11,
inference(demodulation,[status(thm)],[c_213,c_6570]) ).
tcf(c_6581,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_6580]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP002-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n008.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 13:12:09 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/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.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 1.22/1.75 % SZS status Started for theBenchmark.p
% 1.22/1.75 % SZS status Unsatisfiable for theBenchmark.p
% 1.22/1.75
% 1.22/1.75 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.22/1.75
% 1.22/1.75 % ------ iProver source info
% 1.22/1.75
% 1.22/1.75 % git: date: 2026-07-19 20:42:38 +0200
% 1.22/1.75 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.22/1.75 % git: non_committed_changes: false
% 1.22/1.75
% 1.22/1.75 % ------ Parsing...% successful
% 1.22/1.75
% 1.22/1.75
% 1.22/1.75 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.22/1.75
% 1.22/1.75 % ------ Preprocessing... sup_sim: 8 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 %
% 1.22/1.75
% 1.22/1.75 % ------ Preprocessing...% ------ preprocesses with Option_UEQ
% 1.22/1.75 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 1.22/1.75
% 1.22/1.75 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 1.22/1.75 % ------ Proving...
% 1.22/1.75 % ------ Problem Properties
% 1.22/1.75
% 1.22/1.75 %
% 1.22/1.75 % clauses 21
% 1.22/1.75 % conjectures 0
% 1.22/1.75 % EPR 6
% 1.22/1.75 % Horn 21
% 1.22/1.75 % unary 21
% 1.22/1.75 % binary 0
% 1.22/1.76 % lits 21
% 1.22/1.76 % lits eq 21
% 1.22/1.76 % fd_pure 0
% 1.22/1.76 % fd_pseudo 0
% 1.22/1.76 % fd_cond 0
% 1.22/1.76 % fd_pseudo_cond 0
% 1.22/1.76 % AC symbols 0
% 1.22/1.76
% 1.22/1.76 % ------ Schedule UEQ
% 1.22/1.76
% 1.22/1.76 % ------ Option_UEQ Time Limit: 10.
% 1.22/1.76
% 1.22/1.76
% 1.22/1.76 % ------
% 1.22/1.76 % Current options:
% 1.22/1.76 % ------
% 1.22/1.76
% 1.22/1.76
% 1.22/1.76 %
% 1.22/1.76
% 1.22/1.76 % ------ Proving...
% 1.22/1.76 %
% 1.22/1.76
% 1.22/1.76 % SZS status Unsatisfiable for theBenchmark.p
% 1.22/1.76
% 1.22/1.76 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.22/1.76
% 1.22/1.76
%------------------------------------------------------------------------------