%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP333-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n006.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:33:02 PM UTC 2026
% Result : Unsatisfiable 15.68s 13.36s
% Output : CNFRefutation 15.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 33
% Syntax : Number of formulae : 615 ( 140 unt; 9 def)
% Number of atoms : 2550 (1176 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 1204 ( 480 ~; 724 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 15 ( 13 usr; 14 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 162 ( 0 sgn 162 !; 0 ?; 148 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
multiply(sk_c6,sk_c7) = sk_c5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,negated_conjecture,
( multiply(sk_c3,sk_c7) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f7,plain,
( sk_c6 = multiply(sk_c3,sk_c7)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f6]) ).
fof(f8,negated_conjecture,
( inverse(sk_c3) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f9,plain,
( sk_c7 = inverse(sk_c3)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f8]) ).
fof(f10,negated_conjecture,
( multiply(sk_c4,sk_c6) = sk_c5
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c5 = multiply(sk_c4,sk_c6)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( inverse(sk_c4) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c6 = inverse(sk_c4)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( multiply(sk_c3,sk_c7) = sk_c6
| inverse(sk_c1) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c6 = multiply(sk_c3,sk_c7)
| sk_c6 = inverse(sk_c1) ),
inference(reorient_equations,[],[f14]) ).
fof(f16,negated_conjecture,
( inverse(sk_c3) = sk_c7
| inverse(sk_c1) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f17,plain,
( sk_c7 = inverse(sk_c3)
| sk_c6 = inverse(sk_c1) ),
inference(reorient_equations,[],[f16]) ).
fof(f18,negated_conjecture,
( multiply(sk_c4,sk_c6) = sk_c5
| inverse(sk_c1) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,plain,
( sk_c5 = multiply(sk_c4,sk_c6)
| sk_c6 = inverse(sk_c1) ),
inference(reorient_equations,[],[f18]) ).
fof(f20,negated_conjecture,
( inverse(sk_c4) = sk_c6
| inverse(sk_c1) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f21,plain,
( sk_c6 = inverse(sk_c4)
| sk_c6 = inverse(sk_c1) ),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
( multiply(sk_c3,sk_c7) = sk_c6
| inverse(sk_c2) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f23,plain,
( sk_c6 = multiply(sk_c3,sk_c7)
| sk_c6 = inverse(sk_c2) ),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
( inverse(sk_c3) = sk_c7
| inverse(sk_c2) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c7 = inverse(sk_c3)
| sk_c6 = inverse(sk_c2) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( multiply(sk_c4,sk_c6) = sk_c5
| inverse(sk_c2) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c5 = multiply(sk_c4,sk_c6)
| sk_c6 = inverse(sk_c2) ),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
( inverse(sk_c4) = sk_c6
| inverse(sk_c2) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f29,plain,
( sk_c6 = inverse(sk_c4)
| sk_c6 = inverse(sk_c2) ),
inference(reorient_equations,[],[f28]) ).
fof(f30,negated_conjecture,
( multiply(sk_c3,sk_c7) = sk_c6
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f31,plain,
( sk_c6 = multiply(sk_c3,sk_c7)
| sk_c6 = multiply(sk_c2,sk_c5) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
( inverse(sk_c3) = sk_c7
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c7 = inverse(sk_c3)
| sk_c6 = multiply(sk_c2,sk_c5) ),
inference(reorient_equations,[],[f32]) ).
fof(f34,negated_conjecture,
( multiply(sk_c4,sk_c6) = sk_c5
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f35,plain,
( sk_c5 = multiply(sk_c4,sk_c6)
| sk_c6 = multiply(sk_c2,sk_c5) ),
inference(reorient_equations,[],[f34]) ).
fof(f36,negated_conjecture,
( inverse(sk_c4) = sk_c6
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f37,plain,
( sk_c6 = inverse(sk_c4)
| sk_c6 = multiply(sk_c2,sk_c5) ),
inference(reorient_equations,[],[f36]) ).
fof(f38,negated_conjecture,
! [X2,X3,X0,X1] :
( inverse(X3) != sk_c6
| multiply(X3,sk_c6) != sk_c5
| inverse(X2) != sk_c7
| multiply(X2,sk_c7) != sk_c6
| multiply(X1,sk_c5) != sk_c6
| inverse(X1) != sk_c6
| inverse(X0) != sk_c6
| multiply(X0,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f39,plain,
! [X2,X3,X0,X1] :
( sk_c6 != inverse(X3)
| sk_c5 != multiply(X3,sk_c6)
| sk_c7 != inverse(X2)
| sk_c6 != multiply(X2,sk_c7)
| sk_c6 != multiply(X1,sk_c5)
| sk_c6 != inverse(X1)
| inverse(X0) != sk_c6
| sk_c7 != multiply(X0,sk_c6)
| multiply(sk_c6,sk_c7) != sk_c5 ),
inference(reorient_equations,[],[f38]) ).
tcf(c_70,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_71,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_73,negated_conjecture,
multiply(sk_c6,sk_c7) = sk_c5,
inference(cnf_transformation,[],[f5]) ).
tcf(c_74,negated_conjecture,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_75,negated_conjecture,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_76,negated_conjecture,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_77,negated_conjecture,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_78,negated_conjecture,
( ( inverse(sk_c1) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_79,negated_conjecture,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c6 ) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_80,negated_conjecture,
( ( inverse(sk_c1) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_81,negated_conjecture,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c6 ) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_82,negated_conjecture,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_83,negated_conjecture,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_84,negated_conjecture,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_85,negated_conjecture,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_86,negated_conjecture,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_87,negated_conjecture,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_88,negated_conjecture,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_89,negated_conjecture,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_90,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(X3) != sk_c6 )
| ( inverse(X2) != sk_c7 )
| ( inverse(X1) != sk_c6 )
| ( inverse(X0) != sk_c6 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( multiply(X3,sk_c6) != sk_c5 )
| ( multiply(X2,sk_c7) != sk_c6 )
| ( multiply(X1,sk_c5) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(X3) != sk_c6 )
| ( inverse(X2) != sk_c7 )
| ( inverse(X1) != sk_c6 )
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 )
| ( multiply(X1,sk_c5) != sk_c6 )
| ( multiply(X2,sk_c7) != sk_c6 )
| ( multiply(X3,sk_c6) != sk_c5 ) ),
inference(global_subsumption_just,[status(thm)],[c_90,c_73,c_90]) ).
tcf(c_96,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(X3) != sk_c6 )
| ( inverse(X2) != sk_c7 )
| ( inverse(X1) != sk_c6 )
| ( inverse(X0) != sk_c6 )
| ( multiply(X3,sk_c6) != sk_c5 )
| ( multiply(X2,sk_c7) != sk_c6 )
| ( multiply(X1,sk_c5) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(renaming,[status(thm)],[c_95]) ).
tcf(c_268,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != sk_c6 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_96]) ).
tcf(c_269,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c5) != sk_c6 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_96]) ).
tcf(c_270,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c5 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_96]) ).
tcf(c_271,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_96]) ).
tcf(c_272,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_96]) ).
tcf(c_273,definition,
iPr_def_14 = multiply(sk_c2,sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_274,definition,
iPr_def_15 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_275,definition,
iPr_def_16 = multiply(sk_c4,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_276,definition,
iPr_def_17 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_277,definition,
iPr_def_18 = multiply(sk_c3,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_278,definition,
iPr_def_19 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_279,definition,
iPr_def_20 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_280,definition,
iPr_def_21 = multiply(sk_c1,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_281,definition,
iPr_def_22 = multiply(sk_c6,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_282,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_272]) ).
tcf(c_283,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_271]) ).
tcf(c_284,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm)],[c_270]) ).
tcf(c_285,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c5) != sk_c6 ) ),
inference(demodulation,[status(thm)],[c_269]) ).
tcf(c_286,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm)],[c_268]) ).
tcf(c_287,negated_conjecture,
( ( iPr_def_15 = sk_c6 )
| ( iPr_def_14 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_89,c_274,c_273]) ).
tcf(c_288,negated_conjecture,
( ( iPr_def_16 = sk_c5 )
| ( iPr_def_14 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_88,c_275]) ).
tcf(c_289,negated_conjecture,
( ( iPr_def_17 = sk_c7 )
| ( iPr_def_14 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_87,c_276]) ).
tcf(c_290,negated_conjecture,
( ( iPr_def_18 = sk_c6 )
| ( iPr_def_14 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_86,c_277]) ).
tcf(c_291,negated_conjecture,
( ( iPr_def_19 = sk_c6 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_85,c_278]) ).
tcf(c_292,negated_conjecture,
( ( iPr_def_19 = sk_c6 )
| ( iPr_def_16 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_84]) ).
tcf(c_293,negated_conjecture,
( ( iPr_def_19 = sk_c6 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_83]) ).
tcf(c_294,negated_conjecture,
( ( iPr_def_19 = sk_c6 )
| ( iPr_def_18 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_82]) ).
tcf(c_295,negated_conjecture,
( ( iPr_def_20 = sk_c6 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_81,c_279]) ).
tcf(c_296,negated_conjecture,
( ( iPr_def_20 = sk_c6 )
| ( iPr_def_16 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_80]) ).
tcf(c_297,negated_conjecture,
( ( iPr_def_20 = sk_c6 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_79]) ).
tcf(c_298,negated_conjecture,
( ( iPr_def_20 = sk_c6 )
| ( iPr_def_18 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_78]) ).
tcf(c_299,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_77,c_280]) ).
tcf(c_300,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_16 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_76]) ).
tcf(c_301,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_75]) ).
tcf(c_302,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_18 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_74]) ).
tcf(c_303,negated_conjecture,
iPr_def_22 = sk_c5,
inference(demodulation,[status(thm)],[c_73,c_281]) ).
tcf(c_304,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_305,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_307,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_463,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c6 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_288,c_303]) ).
tcf(c_486,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c6 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_290,c_287]) ).
tcf(c_511,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c6 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_292,c_303]) ).
tcf(c_529,plain,
multiply(sk_c2,iPr_def_22) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_273,c_303]) ).
tcf(c_532,plain,
( ( sk_c6 = iPr_def_14 )
| ( multiply(sk_c4,iPr_def_18) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_290,c_275]) ).
tcf(c_534,plain,
( ( sk_c6 = iPr_def_14 )
| ( multiply(sk_c4,iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_287,c_275]) ).
tcf(c_545,plain,
( ( sk_c6 = iPr_def_14 )
| ( multiply(sk_c3,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_289,c_277]) ).
tcf(c_549,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(sk_c1,iPr_def_19) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_291,c_280]) ).
tcf(c_567,plain,
( ( sk_c6 = iPr_def_19 )
| ( multiply(sk_c3,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_293,c_277]) ).
tcf(c_577,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_19) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_294,c_280]) ).
tcf(c_603,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_295,c_280]) ).
tcf(c_606,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( sk_c6 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_295,c_291]) ).
tcf(c_633,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c6 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_296,c_303]) ).
tcf(c_647,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_633,c_280]) ).
tcf(c_649,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_16 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_633,c_511]) ).
tcf(c_666,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_304]) ).
tcf(c_669,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_675,plain,
( ( sk_c6 = iPr_def_20 )
| ( multiply(sk_c3,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_297,c_277]) ).
tcf(c_688,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( sk_c6 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_298,c_294]) ).
tcf(c_689,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_298,c_280]) ).
tcf(c_715,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_669]) ).
tcf(c_731,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(sk_c3,iPr_def_21) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_299,c_277]) ).
tcf(c_749,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_751,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(X2) )
| ( inverse(X2) != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_715]) ).
tcf(c_752,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_15 )
| ( iPr_def_15 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_715]) ).
tcf(c_756,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_19 )
| ( iPr_def_19 != inverse(sk_c2) )
| ( inverse(X0) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_715]) ).
tcf(c_761,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c7 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_300,c_303]) ).
tcf(c_777,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(iPr_def_20,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_298,c_281]) ).
tcf(c_778,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(iPr_def_20,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_633,c_281]) ).
tcf(c_779,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_20,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_295,c_281]) ).
tcf(c_781,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(iPr_def_19,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_511,c_281]) ).
tcf(c_782,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_19,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_291,c_281]) ).
tcf(c_783,plain,
( ( sk_c6 = iPr_def_14 )
| ( multiply(iPr_def_18,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_290,c_281]) ).
tcf(c_784,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(iPr_def_14,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_463,c_281]) ).
tcf(c_787,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(sk_c6,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_299,c_281]) ).
tcf(c_822,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_669]) ).
tcf(c_826,plain,
multiply(iPr_def_17,sk_c3) = identity,
inference(superposition,[status(thm)],[c_276,c_71]) ).
tcf(c_827,plain,
multiply(iPr_def_15,sk_c4) = identity,
inference(superposition,[status(thm)],[c_274,c_71]) ).
tcf(c_828,plain,
multiply(iPr_def_20,sk_c1) = identity,
inference(superposition,[status(thm)],[c_279,c_71]) ).
tcf(c_829,plain,
multiply(iPr_def_19,sk_c2) = identity,
inference(superposition,[status(thm)],[c_278,c_71]) ).
tcf(c_834,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_19 )
| ( inverse(X0) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_669]) ).
tcf(c_848,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c3,iPr_def_21) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_301,c_277]) ).
tcf(c_877,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(sk_c3,iPr_def_21) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_302,c_277]) ).
tcf(c_901,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_749]) ).
tcf(c_905,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_19 )
| ( inverse(X0) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_749]) ).
tcf(c_910,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c6,X0)) = multiply(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_280,c_72]) ).
tcf(c_912,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c6,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_275,c_72]) ).
tcf(c_914,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_71,c_72]) ).
tcf(c_916,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_22,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_529,c_72]) ).
tcf(c_931,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_826,c_72]) ).
tcf(c_932,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_931,c_70]) ).
tcf(c_934,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_827,c_72]) ).
tcf(c_935,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_934,c_70]) ).
tcf(c_953,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_828,c_72]) ).
tcf(c_954,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_953,c_70]) ).
tcf(c_956,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_829,c_72]) ).
tcf(c_957,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_956,c_70]) ).
tcf(c_965,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_21 )
| ( inverse(sk_c1) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_280,c_283]) ).
tcf(c_966,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_16 )
| ( inverse(sk_c4) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_275,c_283]) ).
tcf(c_967,plain,
( ~ iPr_def_13
| ( sk_c6 != sk_c7 )
| ( inverse(identity) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_70,c_283]) ).
tcf(c_968,plain,
( ~ iPr_def_13
| ( sk_c7 != identity )
| ( inverse(inverse(sk_c6)) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_71,c_283]) ).
tcf(c_969,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(multiply(X0,X1)) != sk_c6 )
| ( multiply(X0,multiply(X1,sk_c6)) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_72,c_283]) ).
tcf(c_971,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_22 )
| ~ iPr_def_13
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,iPr_def_20) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_633,c_283]) ).
tcf(c_982,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_16 )
| ( sk_c6 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_966,c_274]) ).
tcf(c_986,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_21 )
| ( sk_c6 != iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_965,c_279]) ).
tcf(c_1059,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c4) )
| ( X0 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_307]) ).
tcf(c_1060,plain,
( ( inverse(sk_c6) = inverse(sk_c4) )
| ( sk_c6 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1061,plain,
( ( inverse(sk_c4) = iPr_def_15 )
| ( iPr_def_15 != inverse(sk_c4) )
| ( inverse(sk_c4) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_752]) ).
tcf(c_1062,plain,
inverse(sk_c4) = inverse(sk_c4),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1065,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_284,c_303]) ).
tcf(c_1076,plain,
( ~ iPr_def_12
| ( iPr_def_16 != iPr_def_22 )
| ( inverse(sk_c4) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_275,c_1065]) ).
tcf(c_1077,plain,
( ~ iPr_def_12
| ( sk_c6 != iPr_def_22 )
| ( inverse(identity) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_70,c_1065]) ).
tcf(c_1086,plain,
! [X0: $i] :
( ( sk_c6 = iPr_def_14 )
| ~ iPr_def_12
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,iPr_def_18) != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_290,c_1065]) ).
tcf(c_1092,plain,
( ~ iPr_def_12
| ( iPr_def_16 != iPr_def_22 )
| ( sk_c6 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_1076,c_274]) ).
tcf(c_1190,plain,
( ( inverse(sk_c2) = iPr_def_19 )
| ( iPr_def_19 != inverse(sk_c2) )
| ( inverse(sk_c2) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_756]) ).
tcf(c_1191,plain,
inverse(sk_c2) = inverse(sk_c2),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1226,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,iPr_def_22) != sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_285,c_303]) ).
tcf(c_1239,plain,
( ~ iPr_def_11
| ( sk_c6 != iPr_def_14 )
| ( inverse(sk_c2) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_529,c_1226]) ).
tcf(c_1240,plain,
( ~ iPr_def_11
| ( sk_c6 != iPr_def_19 )
| ( sk_c6 != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_1239,c_278]) ).
tcf(c_1270,plain,
( ~ iPr_def_10
| ( sk_c6 != iPr_def_18 )
| ( inverse(sk_c3) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_277,c_286]) ).
tcf(c_1271,plain,
( ~ iPr_def_10
| ( sk_c6 != sk_c7 )
| ( inverse(identity) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_70,c_286]) ).
tcf(c_1272,plain,
( ~ iPr_def_10
| ( sk_c6 != identity )
| ( inverse(inverse(sk_c7)) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_71,c_286]) ).
tcf(c_1284,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_17 )
| ( sk_c6 != iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_1270,c_276]) ).
tcf(c_1383,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( iPr_def_14 = iPr_def_19 )
| ( sk_c6 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_486,c_294]) ).
tcf(c_1387,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( iPr_def_14 = iPr_def_19 )
| ( sk_c6 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_486,c_291]) ).
tcf(c_1489,plain,
! [X0: $i] :
( ( iPr_def_19 = iPr_def_20 )
| ~ iPr_def_13
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,iPr_def_15) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_606,c_283]) ).
tcf(c_1495,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_15) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_606,c_280]) ).
tcf(c_1496,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( multiply(sk_c4,iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_606,c_275]) ).
tcf(c_1537,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c4) )
| ( X0 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_901]) ).
tcf(c_1538,plain,
! [X0: $i] :
( ( inverse(sk_c4) = X0 )
| ( X0 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_822]) ).
tcf(c_1539,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( sk_c6 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1538]) ).
tcf(c_1540,plain,
( ( sk_c6 = inverse(sk_c4) )
| ( sk_c6 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1537]) ).
tcf(c_1571,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_688,c_606]) ).
tcf(c_1575,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( multiply(iPr_def_18,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_688,c_281]) ).
tcf(c_1632,plain,
! [X0: $i] :
( ( inverse(sk_c2) = X0 )
| ( X0 != iPr_def_19 )
| ( inverse(sk_c2) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_1633,plain,
( ( inverse(sk_c2) = sk_c6 )
| ( sk_c6 != iPr_def_19 )
| ( inverse(sk_c2) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1632]) ).
tcf(c_1706,plain,
! [X0: $i] :
( ( iPr_def_19 = iPr_def_20 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,iPr_def_16) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_649,c_1226]) ).
tcf(c_1714,plain,
( ( iPr_def_19 = iPr_def_20 )
| ~ iPr_def_11
| ( inverse(sk_c6) != sk_c6 )
| ( multiply(sk_c6,iPr_def_16) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_1706]) ).
tcf(c_1734,plain,
multiply(iPr_def_17,iPr_def_18) = sk_c7,
inference(superposition,[status(thm)],[c_277,c_932]) ).
tcf(c_1749,plain,
multiply(iPr_def_15,iPr_def_16) = sk_c6,
inference(superposition,[status(thm)],[c_275,c_935]) ).
tcf(c_1764,plain,
multiply(iPr_def_20,iPr_def_21) = sk_c6,
inference(superposition,[status(thm)],[c_280,c_954]) ).
tcf(c_1775,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_1782,plain,
( ( sk_c6 = iPr_def_14 )
| ( multiply(iPr_def_15,iPr_def_16) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_532,c_935]) ).
tcf(c_1783,plain,
( ( sk_c6 = iPr_def_18 )
| ( sk_c6 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_1782,c_1749]) ).
tcf(c_1794,plain,
( ( sk_c6 = iPr_def_14 )
| ( multiply(iPr_def_15,iPr_def_16) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_534,c_935]) ).
tcf(c_1795,plain,
( ( sk_c6 = iPr_def_15 )
| ( sk_c6 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_1794,c_1749]) ).
tcf(c_1805,plain,
! [X0: $i] :
( ( sk_c6 = iPr_def_14 )
| ( multiply(sk_c3,multiply(iPr_def_17,X0)) = multiply(iPr_def_18,X0) ) ),
inference(superposition,[status(thm)],[c_545,c_72]) ).
tcf(c_1806,plain,
( ( sk_c6 = iPr_def_14 )
| ( multiply(iPr_def_17,iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_545,c_932]) ).
tcf(c_1807,plain,
( ( sk_c7 = iPr_def_17 )
| ( sk_c6 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_1806,c_1734]) ).
tcf(c_1818,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_549,c_954]) ).
tcf(c_1819,plain,
( ( sk_c6 = iPr_def_19 )
| ( sk_c6 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_1818,c_1764]) ).
tcf(c_1850,plain,
( ( sk_c6 = iPr_def_19 )
| ( multiply(iPr_def_17,iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_567,c_932]) ).
tcf(c_1851,plain,
( ( sk_c7 = iPr_def_17 )
| ( sk_c6 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_1850,c_1734]) ).
tcf(c_1862,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_577,c_954]) ).
tcf(c_1863,plain,
( ( sk_c6 = iPr_def_19 )
| ( sk_c6 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_1862,c_1764]) ).
tcf(c_1871,plain,
multiply(iPr_def_19,iPr_def_14) = iPr_def_22,
inference(superposition,[status(thm)],[c_529,c_957]) ).
tcf(c_1874,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(iPr_def_14,X0)) = multiply(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_1871,c_72]) ).
tcf(c_2013,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_603,c_954]) ).
tcf(c_2014,plain,
( ( sk_c6 = iPr_def_20 )
| ( sk_c6 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_2013,c_1764]) ).
tcf(c_2049,plain,
( ( sk_c6 = iPr_def_20 )
| ( multiply(iPr_def_17,iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_675,c_932]) ).
tcf(c_2050,plain,
( ( sk_c7 = iPr_def_17 )
| ( sk_c6 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_2049,c_1734]) ).
tcf(c_2062,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_689,c_954]) ).
tcf(c_2063,plain,
( ( sk_c6 = iPr_def_20 )
| ( sk_c6 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_2062,c_1764]) ).
tcf(c_2085,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_17,iPr_def_18) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_731,c_932]) ).
tcf(c_2086,plain,
( ( sk_c7 = iPr_def_21 )
| ( sk_c6 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_2085,c_1734]) ).
tcf(c_2098,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_302,c_777]) ).
tcf(c_2107,plain,
( ( sk_c6 = iPr_def_22 )
| ( sk_c6 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_2098,c_1764]) ).
tcf(c_2128,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c4 )
| ( sk_c4 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_2198,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( sk_c6 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_2107,c_294]) ).
tcf(c_2341,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c4) = inverse(X0) )
| ( inverse(sk_c4) != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_751]) ).
tcf(c_2653,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_299,c_779]) ).
tcf(c_2659,plain,
( ( sk_c6 = iPr_def_22 )
| ( sk_c6 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_2653,c_1764]) ).
tcf(c_2779,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_19,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_299,c_782]) ).
tcf(c_2813,plain,
( ( sk_c6 = iPr_def_14 )
| ( multiply(iPr_def_18,iPr_def_17) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_289,c_783]) ).
tcf(c_3046,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_715]) ).
tcf(c_3047,plain,
( ( inverse(sk_c6) = sk_c6 )
| ( sk_c6 != inverse(sk_c4) )
| ( inverse(sk_c6) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_3046]) ).
tcf(c_3100,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_22,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_2659,c_281]) ).
tcf(c_3108,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( sk_c6 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2659,c_291]) ).
tcf(c_3202,plain,
( ( inverse(sk_c4) = iPr_def_19 )
| ( iPr_def_19 != inverse(sk_c2) )
| ( inverse(sk_c4) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_756]) ).
tcf(c_3204,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c4) )
| ( X0 != iPr_def_19 )
| ( inverse(sk_c4) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_905]) ).
tcf(c_3367,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_3108,c_2198]) ).
tcf(c_3375,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( multiply(iPr_def_15,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_3108,c_281]) ).
tcf(c_3381,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( multiply(sk_c4,iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_3108,c_275]) ).
tcf(c_3732,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_17,iPr_def_18) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_848,c_932]) ).
tcf(c_3733,plain,
( ( sk_c7 = iPr_def_21 )
| ( sk_c7 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_3732,c_1734]) ).
tcf(c_3750,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_19 )
| ( iPr_def_19 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_3800,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(iPr_def_17,iPr_def_18) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_877,c_932]) ).
tcf(c_3801,plain,
( ( sk_c7 = iPr_def_21 )
| ( sk_c6 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_3800,c_1734]) ).
tcf(c_3953,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_19) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_3367,c_529]) ).
tcf(c_4033,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_761,c_778]) ).
tcf(c_4039,plain,
( ( iPr_def_16 = iPr_def_22 )
| ~ iPr_def_10
| ( sk_c6 != iPr_def_22 )
| ( inverse(iPr_def_20) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_778,c_286]) ).
tcf(c_4040,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c6 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_4033,c_1764]) ).
tcf(c_4132,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( iPr_def_16 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_4040,c_511]) ).
tcf(c_4279,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_19) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_4132,c_529]) ).
tcf(c_4411,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(iPr_def_14,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_761,c_784]) ).
tcf(c_4467,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != inverse(sk_c4) )
| ( X0 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1775]) ).
tcf(c_4468,plain,
( ( identity = inverse(sk_c4) )
| ( identity != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1537]) ).
tcf(c_4469,plain,
( ( sk_c6 = identity )
| ( identity != inverse(sk_c4) )
| ( sk_c6 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_4467]) ).
tcf(c_4560,plain,
multiply(sk_c1,iPr_def_22) = multiply(iPr_def_21,sk_c7),
inference(superposition,[status(thm)],[c_281,c_910]) ).
tcf(c_4662,plain,
! [X0: $i] :
( ( inverse(sk_c4) = inverse(X0) )
| ( inverse(sk_c4) != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2341]) ).
tcf(c_4812,plain,
multiply(sk_c4,iPr_def_22) = multiply(iPr_def_16,sk_c7),
inference(superposition,[status(thm)],[c_281,c_912]) ).
tcf(c_5035,plain,
( ~ iPr_def_11
| ( inverse(sk_c4) != sk_c6 )
| ( multiply(iPr_def_16,sk_c7) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_4812,c_1226]) ).
tcf(c_5053,plain,
( ~ iPr_def_11
| ( sk_c6 != iPr_def_15 )
| ( multiply(iPr_def_16,sk_c7) != sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_5035,c_274]) ).
tcf(c_5478,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1387,c_1383]) ).
tcf(c_5521,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_914,c_70]) ).
tcf(c_5530,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_70,c_5521]) ).
tcf(c_5531,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_71,c_5521]) ).
tcf(c_5585,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_932,c_5521]) ).
tcf(c_5586,plain,
! [X0: $i] : multiply(inverse(iPr_def_15),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_935,c_5521]) ).
tcf(c_5587,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_954,c_5521]) ).
tcf(c_5588,plain,
! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_957,c_5521]) ).
tcf(c_5599,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_5521,c_5521]) ).
tcf(c_5815,plain,
( ( sk_c4 = inverse(sk_c4) )
| ( sk_c4 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1537]) ).
tcf(c_6041,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_5531,c_5599]) ).
tcf(c_6058,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_6041,c_5530]) ).
tcf(c_6578,plain,
multiply(sk_c3,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_5585,c_71]) ).
tcf(c_6582,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_17,X0)) = X0,
inference(superposition,[status(thm)],[c_5585,c_5521]) ).
tcf(c_6584,plain,
multiply(sk_c3,identity) = inverse(iPr_def_17),
inference(superposition,[status(thm)],[c_5585,c_6041]) ).
tcf(c_6598,plain,
( ( identity = iPr_def_18 )
| ( sk_c6 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_675,c_6578]) ).
tcf(c_6599,plain,
( ( identity = iPr_def_18 )
| ( sk_c6 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_567,c_6578]) ).
tcf(c_6600,plain,
( ( identity = iPr_def_18 )
| ( sk_c6 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_545,c_6578]) ).
tcf(c_6632,plain,
inverse(iPr_def_17) = sk_c3,
inference(demodulation,[status(thm)],[c_6584,c_6041]) ).
tcf(c_6642,plain,
( ~ iPr_def_13
| ( sk_c6 != identity )
| ( sk_c6 != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_967,c_6058]) ).
tcf(c_6658,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_13
| ( sk_c6 != iPr_def_21 )
| ( sk_c6 != identity ) ),
inference(superposition,[status(thm)],[c_302,c_6642]) ).
tcf(c_6661,plain,
( ( sk_c6 = iPr_def_15 )
| ~ iPr_def_13
| ( sk_c6 != iPr_def_21 )
| ( sk_c6 != identity ) ),
inference(superposition,[status(thm)],[c_299,c_6642]) ).
tcf(c_6663,plain,
( ( sk_c6 = iPr_def_19 )
| ~ iPr_def_13
| ( sk_c6 != iPr_def_17 )
| ( sk_c6 != identity ) ),
inference(superposition,[status(thm)],[c_293,c_6642]) ).
tcf(c_6805,plain,
( ~ iPr_def_10
| ( sk_c7 != identity )
| ( sk_c6 != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_1271,c_6058]) ).
tcf(c_6821,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_10
| ( sk_c7 != identity )
| ( sk_c6 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_302,c_6805]) ).
tcf(c_6822,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_10
| ( sk_c7 != identity )
| ( sk_c6 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_301,c_6805]) ).
tcf(c_6826,plain,
( ( sk_c6 = iPr_def_19 )
| ~ iPr_def_10
| ( sk_c7 != identity )
| ( sk_c6 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_293,c_6805]) ).
tcf(c_6827,plain,
( ( sk_c6 = iPr_def_14 )
| ~ iPr_def_10
| ( sk_c7 != identity )
| ( sk_c6 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_289,c_6805]) ).
tcf(c_7082,plain,
( ( identity = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_6598,c_280]) ).
tcf(c_7170,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c2) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c2) != X0 ) ),
inference(instantiation,[status(thm)],[c_669]) ).
tcf(c_7183,plain,
( ( inverse(sk_c2) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_19 )
| ( inverse(sk_c2) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1632]) ).
tcf(c_7184,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c2) )
| ( X0 != iPr_def_15 )
| ( inverse(sk_c2) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_901]) ).
tcf(c_7187,plain,
( ( sk_c6 = inverse(sk_c2) )
| ( sk_c6 != iPr_def_15 )
| ( inverse(sk_c2) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_7184]) ).
tcf(c_7268,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( identity = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_6599,c_6598]) ).
tcf(c_7298,plain,
( ( identity = iPr_def_18 )
| ( multiply(iPr_def_19,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_6599,c_281]) ).
tcf(c_7403,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( identity = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_6600,c_6599]) ).
tcf(c_7620,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( inverse(iPr_def_18) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_7268,c_6058]) ).
tcf(c_7622,plain,
! [X0: $i] :
( ( iPr_def_19 = iPr_def_20 )
| ( multiply(iPr_def_18,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_7268,c_70]) ).
tcf(c_7635,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( inverse(iPr_def_18) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_7403,c_6058]) ).
tcf(c_7715,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_10
| ( sk_c6 != identity )
| ( inverse(inverse(iPr_def_21)) != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_302,c_1272]) ).
tcf(c_7716,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_10
| ( sk_c6 != identity )
| ( inverse(inverse(iPr_def_21)) != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_301,c_1272]) ).
tcf(c_7941,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_6658,c_986,c_2063,c_3801]) ).
tcf(c_8212,plain,
multiply(sk_c4,iPr_def_15) = identity,
inference(superposition,[status(thm)],[c_5586,c_71]) ).
tcf(c_8216,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_15,X0)) = X0,
inference(superposition,[status(thm)],[c_5586,c_5521]) ).
tcf(c_8218,plain,
multiply(sk_c4,identity) = inverse(iPr_def_15),
inference(superposition,[status(thm)],[c_5586,c_6041]) ).
tcf(c_8234,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( identity = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1496,c_8212]) ).
tcf(c_8235,plain,
( ( identity = iPr_def_16 )
| ( sk_c6 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_534,c_8212]) ).
tcf(c_8299,plain,
( ( sk_c6 = iPr_def_15 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_6661,c_986,c_2014,c_2086]) ).
tcf(c_8305,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c6 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_282,c_8299]) ).
tcf(c_8310,plain,
( iPr_def_12
| ( sk_c6 = iPr_def_15 )
| iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_8305,c_282,c_1240,c_1795,c_1819,c_8299]) ).
tcf(c_8311,plain,
( iPr_def_12
| iPr_def_10
| ( sk_c6 = iPr_def_15 ) ),
inference(renaming,[status(thm)],[c_8310]) ).
tcf(c_8328,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_16 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_8234,c_7268]) ).
tcf(c_8330,plain,
! [X0: $i] :
( ( iPr_def_19 = iPr_def_20 )
| ( multiply(X0,iPr_def_16) = X0 ) ),
inference(superposition,[status(thm)],[c_8234,c_6041]) ).
tcf(c_8341,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( multiply(sk_c6,iPr_def_16) = sk_c6 ) ),
inference(instantiation,[status(thm)],[c_8330]) ).
tcf(c_8431,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( identity = iPr_def_16 )
| ( sk_c6 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_8235,c_291]) ).
tcf(c_8604,plain,
inverse(iPr_def_15) = sk_c4,
inference(demodulation,[status(thm)],[c_8218,c_6041]) ).
tcf(c_9655,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( identity = iPr_def_16 )
| ( multiply(sk_c4,iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_8431,c_275]) ).
tcf(c_9663,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( identity = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_9655,c_8212]) ).
tcf(c_9985,plain,
( ( sk_c6 != iPr_def_21 )
| ( sk_c7 != identity )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_6821,c_1284,c_6822,c_6821]) ).
tcf(c_9986,plain,
( ~ iPr_def_10
| ( sk_c7 != identity )
| ( sk_c6 != iPr_def_21 ) ),
inference(renaming,[status(thm)],[c_9985]) ).
tcf(c_9999,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_10
| ( identity != iPr_def_21 )
| ( sk_c6 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_302,c_9986]) ).
tcf(c_10000,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_10
| ( identity != iPr_def_21 )
| ( sk_c6 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_301,c_9986]) ).
tcf(c_10472,plain,
multiply(sk_c1,iPr_def_20) = identity,
inference(superposition,[status(thm)],[c_5587,c_71]) ).
tcf(c_10478,plain,
multiply(sk_c1,identity) = inverse(iPr_def_20),
inference(superposition,[status(thm)],[c_5587,c_6041]) ).
tcf(c_10504,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( identity = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_647,c_10472]) ).
tcf(c_10505,plain,
( ( identity = iPr_def_21 )
| ( sk_c6 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_689,c_10472]) ).
tcf(c_10506,plain,
( ( identity = iPr_def_21 )
| ( sk_c6 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_603,c_10472]) ).
tcf(c_10589,plain,
( ( sk_c6 = iPr_def_19 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_6826,c_1284,c_1851,c_1863]) ).
tcf(c_10595,plain,
( ( sk_c6 = iPr_def_14 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_6827,c_1284,c_1783,c_1807]) ).
tcf(c_10981,plain,
! [X0: $i] :
( ( X0 = sk_c4 )
| ( sk_c4 != inverse(sk_c4) )
| ( X0 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2128]) ).
tcf(c_10982,plain,
( ( sk_c6 = sk_c4 )
| ( sk_c4 != inverse(sk_c4) )
| ( sk_c6 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_10981]) ).
tcf(c_11202,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( identity = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_10506,c_10505]) ).
tcf(c_11247,plain,
( ( identity = iPr_def_21 )
| ( multiply(sk_c4,iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_10506,c_275]) ).
tcf(c_11254,plain,
( ( identity = iPr_def_21 )
| ( identity = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_11247,c_8212]) ).
tcf(c_11358,plain,
! [X0: $i] :
( ( identity = iPr_def_16 )
| ( multiply(iPr_def_21,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_11254,c_70]) ).
tcf(c_11373,plain,
inverse(iPr_def_20) = sk_c1,
inference(demodulation,[status(thm)],[c_10478,c_6041]) ).
tcf(c_11378,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( inverse(iPr_def_19) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_1571,c_11373]) ).
tcf(c_11550,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_10
| ( sk_c6 != iPr_def_21 ) ),
inference(global_subsumption_just,[status(thm)],[c_9999,c_1284,c_10000,c_9999,c_10505]) ).
tcf(c_11574,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_10
| ( iPr_def_21 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_2107,c_11550]) ).
tcf(c_11716,plain,
( ( sk_c6 != iPr_def_21 )
| ( identity != iPr_def_21 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_10000,c_1284,c_10000,c_9999]) ).
tcf(c_11717,plain,
( ~ iPr_def_10
| ( identity != iPr_def_21 )
| ( sk_c6 != iPr_def_21 ) ),
inference(renaming,[status(thm)],[c_11716]) ).
tcf(c_11726,plain,
( ( identity = iPr_def_16 )
| ~ iPr_def_10
| ( iPr_def_14 != iPr_def_21 )
| ( identity != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_8235,c_11717]) ).
tcf(c_11734,plain,
( ( sk_c6 = iPr_def_15 )
| ~ iPr_def_10
| ( iPr_def_21 != iPr_def_22 )
| ( identity != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_2659,c_11717]) ).
tcf(c_11753,plain,
( ( iPr_def_16 = iPr_def_22 )
| ~ iPr_def_10
| ( iPr_def_14 != iPr_def_21 )
| ( identity != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_463,c_11717]) ).
tcf(c_11938,plain,
( ( identity = inverse(sk_c4) )
| ( identity != iPr_def_19 )
| ( inverse(sk_c4) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_3204]) ).
tcf(c_12009,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_22) = multiply(iPr_def_14,sk_c7) ) ),
inference(superposition,[status(thm)],[c_3100,c_916]) ).
tcf(c_12010,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_14,sk_c7) = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_12009,c_529]) ).
tcf(c_12135,plain,
multiply(sk_c2,iPr_def_19) = identity,
inference(superposition,[status(thm)],[c_5588,c_71]) ).
tcf(c_12139,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_19,X0)) = X0,
inference(superposition,[status(thm)],[c_5588,c_5521]) ).
tcf(c_12141,plain,
multiply(sk_c2,identity) = inverse(iPr_def_19),
inference(superposition,[status(thm)],[c_5588,c_6041]) ).
tcf(c_12368,plain,
inverse(iPr_def_19) = sk_c2,
inference(demodulation,[status(thm)],[c_12141,c_6041]) ).
tcf(c_12371,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( inverse(iPr_def_14) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_5478,c_12368]) ).
tcf(c_12378,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_22) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_781,c_12139]) ).
tcf(c_12384,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_22) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_2779,c_12139]) ).
tcf(c_12395,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( sk_c6 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_12384,c_529]) ).
tcf(c_12404,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c7 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_12378,c_529]) ).
tcf(c_12619,plain,
! [X0: $i] :
( ( X0 = iPr_def_19 )
| ( iPr_def_19 != inverse(sk_c2) )
| ( X0 != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_3750]) ).
tcf(c_12620,plain,
( ( sk_c6 = iPr_def_19 )
| ( iPr_def_19 != inverse(sk_c2) )
| ( sk_c6 != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_12619]) ).
tcf(c_12645,plain,
! [X0: $i] :
( ( sk_c6 = iPr_def_14 )
| ( multiply(iPr_def_18,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_1805,c_6582]) ).
tcf(c_12666,plain,
( ( sk_c7 = iPr_def_22 )
| ( sk_c6 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_12645,c_783]) ).
tcf(c_12670,plain,
( ( iPr_def_17 = iPr_def_22 )
| ( sk_c6 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_12645,c_2813]) ).
tcf(c_13331,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( multiply(iPr_def_15,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_12395,c_281]) ).
tcf(c_13337,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( multiply(sk_c4,iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_12395,c_275]) ).
tcf(c_13344,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( identity = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_13337,c_8212]) ).
tcf(c_14395,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( identity = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_3381,c_8212]) ).
tcf(c_14495,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( iPr_def_14 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_12404,c_761]) ).
tcf(c_14660,plain,
( ( sk_c6 = iPr_def_14 )
| ( multiply(sk_c6,iPr_def_22) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_12666,c_281]) ).
tcf(c_14906,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_22 )
| ~ iPr_def_13
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,iPr_def_14) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_12670,c_283]) ).
tcf(c_16166,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( identity = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_3953,c_12135]) ).
tcf(c_16197,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( inverse(iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_16166,c_6058]) ).
tcf(c_17198,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( identity = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_4279,c_12135]) ).
tcf(c_17229,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( inverse(iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_17198,c_6058]) ).
tcf(c_17231,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(iPr_def_14,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_17198,c_70]) ).
tcf(c_17580,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c1 = sk_c2 ) ),
inference(light_normalisation,[status(thm)],[c_11378,c_12368]) ).
tcf(c_17601,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_17580,c_529]) ).
tcf(c_17603,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_21,sk_c7) = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_17601,c_4560]) ).
tcf(c_17699,plain,
( ( iPr_def_16 = iPr_def_22 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_4039,c_10504,c_11753,c_14495]) ).
tcf(c_17836,plain,
( ( identity = iPr_def_21 )
| ( identity = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_7082,c_10472]) ).
tcf(c_17865,plain,
( ( identity = iPr_def_18 )
| ( inverse(iPr_def_21) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_17836,c_6058]) ).
tcf(c_18444,plain,
( ( identity = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_22) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_7298,c_12139]) ).
tcf(c_18446,plain,
( ( identity = iPr_def_18 )
| ( sk_c7 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_18444,c_529]) ).
tcf(c_18572,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( identity = iPr_def_18 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_18446,c_301]) ).
tcf(c_18920,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c2 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_16197,c_12371]) ).
tcf(c_19062,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( identity = iPr_def_18 )
| ( multiply(sk_c3,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_18572,c_277]) ).
tcf(c_19066,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( identity = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_19062,c_6578]) ).
tcf(c_19181,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( inverse(iPr_def_18) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_19066,c_6058]) ).
tcf(c_19183,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_21 )
| ( multiply(iPr_def_18,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_19066,c_70]) ).
tcf(c_19229,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( sk_c7 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_7622,c_1575]) ).
tcf(c_19294,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_19,iPr_def_14) = identity ) ),
inference(superposition,[status(thm)],[c_18920,c_829]) ).
tcf(c_19301,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( identity = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_19294,c_1871]) ).
tcf(c_19455,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c6 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_288,c_303]) ).
tcf(c_19478,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c6 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_290,c_287]) ).
tcf(c_19503,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c6 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_292,c_303]) ).
tcf(c_19573,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( sk_c6 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_295,c_291]) ).
tcf(c_19588,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c6 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_296,c_303]) ).
tcf(c_19604,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_16 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_19588,c_19503]) ).
tcf(c_19662,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c7 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_300,c_303]) ).
tcf(c_19679,plain,
multiply(sk_c2,iPr_def_22) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_273,c_303]) ).
tcf(c_19832,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_16 )
| ( inverse(sk_c4) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_275,c_283]) ).
tcf(c_19848,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_16 )
| ( sk_c6 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_19832,c_274]) ).
tcf(c_19892,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_284,c_303]) ).
tcf(c_19902,plain,
( ~ iPr_def_12
| ( iPr_def_21 != iPr_def_22 )
| ( inverse(sk_c1) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_280,c_19892]) ).
tcf(c_19903,plain,
( ~ iPr_def_12
| ( iPr_def_16 != iPr_def_22 )
| ( inverse(sk_c4) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_275,c_19892]) ).
tcf(c_19904,plain,
( ~ iPr_def_12
| ( sk_c6 != iPr_def_22 )
| ( inverse(identity) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_70,c_19892]) ).
tcf(c_19919,plain,
( ~ iPr_def_12
| ( iPr_def_16 != iPr_def_22 )
| ( sk_c6 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_19903,c_274]) ).
tcf(c_19923,plain,
( ~ iPr_def_12
| ( iPr_def_21 != iPr_def_22 )
| ( sk_c6 != iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_19902,c_279]) ).
tcf(c_19963,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,iPr_def_22) != sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_285,c_303]) ).
tcf(c_19973,plain,
( ~ iPr_def_11
| ( sk_c6 != iPr_def_22 )
| ( inverse(identity) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_70,c_19963]) ).
tcf(c_19974,plain,
( ~ iPr_def_11
| ( sk_c6 != iPr_def_14 )
| ( inverse(sk_c2) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_19679,c_19963]) ).
tcf(c_19976,plain,
( ~ iPr_def_11
| ( sk_c6 != iPr_def_19 )
| ( sk_c6 != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_19974,c_278]) ).
tcf(c_19993,plain,
( ~ iPr_def_10
| ( sk_c6 != iPr_def_18 )
| ( inverse(sk_c3) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_277,c_286]) ).
tcf(c_20005,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_17 )
| ( sk_c6 != iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_19993,c_276]) ).
tcf(c_20115,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_15 = iPr_def_18 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_19573,c_19478]) ).
tcf(c_20156,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( multiply(iPr_def_15,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_19573,c_281]) ).
tcf(c_20161,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_20,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_295,c_281]) ).
tcf(c_20167,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(iPr_def_14,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_19455,c_281]) ).
tcf(c_20218,plain,
multiply(iPr_def_20,sk_c1) = identity,
inference(superposition,[status(thm)],[c_279,c_71]) ).
tcf(c_20222,plain,
( ~ iPr_def_10
| ( sk_c6 != identity )
| ( inverse(inverse(sk_c7)) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_71,c_286]) ).
tcf(c_20241,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_71,c_72]) ).
tcf(c_20412,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_20218,c_72]) ).
tcf(c_20413,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_20412,c_70]) ).
tcf(c_20442,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_15,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_301,c_20156]) ).
tcf(c_20653,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c6 = iPr_def_18 )
| ( multiply(iPr_def_14,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_302,c_20167]) ).
tcf(c_20654,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_14,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_301,c_20167]) ).
tcf(c_20824,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_299,c_20161]) ).
tcf(c_20925,plain,
multiply(iPr_def_20,iPr_def_21) = sk_c6,
inference(superposition,[status(thm)],[c_280,c_20413]) ).
tcf(c_21784,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_17 = iPr_def_22 )
| ( sk_c6 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_19229,c_297]) ).
tcf(c_21785,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_17 = iPr_def_22 )
| ( sk_c6 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_19229,c_293]) ).
tcf(c_21925,plain,
! [X0: $i] :
( ( inverse(sk_c2) = inverse(sk_c4) )
| ( inverse(sk_c2) != X0 )
| ( inverse(sk_c4) != X0 ) ),
inference(instantiation,[status(thm)],[c_7170]) ).
tcf(c_21928,plain,
( ( inverse(sk_c4) = inverse(sk_c2) )
| ( inverse(sk_c2) != inverse(sk_c4) )
| ( inverse(sk_c4) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_4662]) ).
tcf(c_21931,plain,
( ( inverse(sk_c2) = inverse(sk_c4) )
| ( inverse(sk_c2) != sk_c6 )
| ( inverse(sk_c4) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_21925]) ).
tcf(c_22568,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_17 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_21785,c_21784]) ).
tcf(c_22699,plain,
( ( sk_c6 = iPr_def_22 )
| ( sk_c6 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_20824,c_20925]) ).
tcf(c_22986,plain,
( ( iPr_def_21 = iPr_def_22 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_19301,c_11202]) ).
tcf(c_23040,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_16 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_22568,c_649]) ).
tcf(c_27221,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( multiply(iPr_def_14,iPr_def_14) = identity ) ),
inference(superposition,[status(thm)],[c_17229,c_71]) ).
tcf(c_27287,plain,
( ( identity = iPr_def_18 )
| ( multiply(iPr_def_21,iPr_def_21) = identity ) ),
inference(superposition,[status(thm)],[c_17865,c_71]) ).
tcf(c_27366,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_20241,c_70]) ).
tcf(c_27375,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_70,c_27366]) ).
tcf(c_27376,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_71,c_27366]) ).
tcf(c_27461,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_27366,c_27366]) ).
tcf(c_27743,plain,
( ( inverse(inverse(iPr_def_21)) != iPr_def_21 )
| ( sk_c6 != identity )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_7715,c_1284,c_7716,c_7715]) ).
tcf(c_27744,plain,
( ~ iPr_def_10
| ( sk_c6 != identity )
| ( inverse(inverse(iPr_def_21)) != iPr_def_21 ) ),
inference(renaming,[status(thm)],[c_27743]) ).
tcf(c_27848,plain,
( ( identity = iPr_def_16 )
| ~ iPr_def_10
| ( sk_c6 != sk_c7 )
| ( inverse(iPr_def_21) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_11358,c_286]) ).
tcf(c_28419,plain,
( ( identity = iPr_def_16 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_27848,c_11254,c_11726,c_13344]) ).
tcf(c_28671,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(superposition,[status(thm)],[c_5599,c_5521]) ).
tcf(c_28673,plain,
! [X0: $i] : multiply(X0,identity) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_5599,c_6041]) ).
tcf(c_28674,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_28673,c_6041]) ).
tcf(c_28705,plain,
( ~ iPr_def_10
| ( sk_c6 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_27744,c_28674]) ).
tcf(c_28707,plain,
( ~ iPr_def_13
| ( sk_c7 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_968,c_28674]) ).
tcf(c_28732,plain,
inverse(sk_c1) = iPr_def_20,
inference(superposition,[status(thm)],[c_11373,c_28674]) ).
tcf(c_28741,plain,
inverse(sk_c3) = iPr_def_17,
inference(superposition,[status(thm)],[c_6632,c_28674]) ).
tcf(c_29318,plain,
( ( iPr_def_19 = iPr_def_20 )
| ~ iPr_def_10
| ( identity != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_688,c_28705]) ).
tcf(c_29324,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_10
| ( identity != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_294,c_28705]) ).
tcf(c_29326,plain,
( ( sk_c6 = iPr_def_15 )
| ~ iPr_def_10
| ( identity != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_291,c_28705]) ).
tcf(c_29553,plain,
( ( iPr_def_16 = iPr_def_22 )
| ~ iPr_def_13
| ( identity != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_761,c_28707]) ).
tcf(c_29680,plain,
( ( identity != iPr_def_19 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_29324,c_274,c_278,c_1061,c_1062,c_1190,c_1191,c_1539,c_1540,c_1633,c_3202,c_4469,c_10589,c_11938,c_21931,c_21928,c_28705,c_29326]) ).
tcf(c_29681,plain,
( ~ iPr_def_10
| ( identity != iPr_def_19 ) ),
inference(renaming,[status(thm)],[c_29680]) ).
tcf(c_29995,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_27376,c_27461]) ).
tcf(c_30014,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_29995,c_27375]) ).
tcf(c_35518,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_16 ) ),
inference(global_subsumption_just,[status(thm)],[c_19848,c_986,c_982,c_2014,c_2086]) ).
tcf(c_35529,plain,
( ( iPr_def_16 = iPr_def_22 )
| ~ iPr_def_13
| ( iPr_def_16 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_19662,c_35518]) ).
tcf(c_36431,plain,
! [X0: $i,X1: $i] :
( ( sk_c6 = iPr_def_14 )
| ~ iPr_def_13
| ( inverse(multiply(X0,X1)) != sk_c6 )
| ( multiply(X0,multiply(X1,iPr_def_18)) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_290,c_969]) ).
tcf(c_37109,plain,
( ( iPr_def_16 = iPr_def_22 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_971,c_10504,c_29553]) ).
tcf(c_37115,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_16 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_282,c_37109]) ).
tcf(c_37251,plain,
( ( iPr_def_21 = iPr_def_22 )
| ( iPr_def_16 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_17231,c_4411]) ).
tcf(c_37441,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_16 = iPr_def_22 ) ),
inference(global_subsumption_just,[status(thm)],[c_37115,c_282,c_17699,c_37109]) ).
tcf(c_37757,plain,
( ( iPr_def_19 = iPr_def_20 )
| ~ iPr_def_12
| ( sk_c6 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_19604,c_19919]) ).
tcf(c_37935,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_12
| ( iPr_def_21 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_298,c_19923]) ).
tcf(c_37936,plain,
( ( iPr_def_16 = iPr_def_22 )
| ~ iPr_def_12
| ( iPr_def_21 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_19588,c_19923]) ).
tcf(c_37937,plain,
( ( sk_c6 = iPr_def_15 )
| ~ iPr_def_12
| ( iPr_def_21 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_295,c_19923]) ).
tcf(c_38464,plain,
( ( iPr_def_16 = iPr_def_22 )
| ~ iPr_def_11
| ( sk_c6 != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_19455,c_19976]) ).
tcf(c_38996,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c6 = iPr_def_18 )
| ( multiply(iPr_def_21,iPr_def_21) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_302,c_17603]) ).
tcf(c_39109,plain,
( ( sk_c6 = iPr_def_18 )
| ( iPr_def_21 != iPr_def_22 ) ),
inference(global_subsumption_just,[status(thm)],[c_37935,c_282,c_1240,c_1783,c_1863,c_7941,c_11574,c_37935]) ).
tcf(c_39387,plain,
( ( sk_c6 = iPr_def_15 )
| ( iPr_def_21 != iPr_def_22 ) ),
inference(global_subsumption_just,[status(thm)],[c_37937,c_8311,c_10506,c_11734,c_37937]) ).
tcf(c_41132,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_10
| ( iPr_def_18 != iPr_def_20 )
| ( sk_c7 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_298,c_20005]) ).
tcf(c_41408,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c6 = iPr_def_18 ) ),
inference(global_subsumption_just,[status(thm)],[c_38996,c_282,c_1240,c_1783,c_1863,c_7941,c_11574,c_22986,c_37935]) ).
tcf(c_41505,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( iPr_def_15 = iPr_def_18 )
| ( sk_c6 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_41408,c_295]) ).
tcf(c_41751,plain,
( ( sk_c6 = iPr_def_15 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(global_subsumption_just,[status(thm)],[c_41505,c_8311,c_10506,c_11734,c_22986,c_37937]) ).
tcf(c_41752,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c6 = iPr_def_15 ) ),
inference(renaming,[status(thm)],[c_41751]) ).
tcf(c_41788,plain,
iPr_def_15 = iPr_def_18,
inference(superposition,[status(thm)],[c_41752,c_41408]) ).
tcf(c_41896,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( inverse(iPr_def_15) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_19181,c_41788]) ).
tcf(c_41912,plain,
( ( identity = iPr_def_15 )
| ( sk_c7 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_18446,c_41788]) ).
tcf(c_41931,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( inverse(iPr_def_15) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_7635,c_41788]) ).
tcf(c_41932,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( inverse(iPr_def_15) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_7620,c_41788]) ).
tcf(c_41951,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_15 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_8328,c_41788]) ).
tcf(c_41964,plain,
( ( identity = iPr_def_15 )
| ( sk_c6 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_6600,c_41788]) ).
tcf(c_41999,plain,
multiply(sk_c3,sk_c7) = iPr_def_15,
inference(demodulation,[status(thm)],[c_277,c_41788]) ).
tcf(c_42027,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( sk_c4 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_41932,c_8604]) ).
tcf(c_42030,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c4 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_41931,c_8604]) ).
tcf(c_42096,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( sk_c4 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_41896,c_8604]) ).
tcf(c_42340,plain,
( ~ iPr_def_10
| ( sk_c6 != iPr_def_15 )
| ( inverse(sk_c3) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_41999,c_286]) ).
tcf(c_42350,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_17 )
| ( sk_c6 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_42340,c_28741]) ).
tcf(c_42620,plain,
( ( sk_c6 = iPr_def_14 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_1086,c_1092,c_1795,c_37251,c_37936]) ).
tcf(c_43008,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_21 )
| ( multiply(iPr_def_15,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_19183,c_41788]) ).
tcf(c_43035,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( sk_c7 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_43008,c_13331]) ).
tcf(c_43041,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( sk_c4 = identity ) ),
inference(superposition,[status(thm)],[c_43008,c_827]) ).
tcf(c_43374,plain,
! [X0: $i] :
( ( iPr_def_19 = iPr_def_20 )
| ( multiply(X0,iPr_def_15) != sk_c7 )
| ( inverse(X0) != sk_c6 ) ),
inference(global_subsumption_just,[status(thm)],[c_1489,c_282,c_274,c_606,c_1060,c_1061,c_1062,c_1489,c_1540,c_1714,c_3047,c_5815,c_7268,c_8341,c_10982,c_29318,c_37757,c_42027]) ).
tcf(c_43375,plain,
! [X0: $i] :
( ( iPr_def_19 = iPr_def_20 )
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,iPr_def_15) != sk_c7 ) ),
inference(renaming,[status(thm)],[c_43374]) ).
tcf(c_43391,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( sk_c7 != iPr_def_21 )
| ( inverse(sk_c1) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_1495,c_43375]) ).
tcf(c_43413,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( sk_c7 != iPr_def_21 )
| ( sk_c6 != iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_43391,c_28732]) ).
tcf(c_43941,plain,
iPr_def_15 = iPr_def_18,
inference(global_subsumption_just,[status(thm)],[c_20115,c_41788]) ).
tcf(c_44032,plain,
( ~ iPr_def_10
| ( sk_c6 != identity ) ),
inference(global_subsumption_just,[status(thm)],[c_20222,c_28705]) ).
tcf(c_44094,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( sk_c7 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_20442,c_2050,c_3733,c_43413]) ).
tcf(c_44106,plain,
( ( iPr_def_19 = iPr_def_20 )
| ~ iPr_def_13
| ( iPr_def_16 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_44094,c_35518]) ).
tcf(c_44125,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( iPr_def_17 = iPr_def_21 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_44094,c_301]) ).
tcf(c_44163,plain,
iPr_def_19 = iPr_def_20,
inference(global_subsumption_just,[status(thm)],[c_44125,c_282,c_274,c_606,c_1060,c_1061,c_1062,c_1540,c_1714,c_3047,c_5815,c_7268,c_8341,c_10982,c_23040,c_29318,c_37757,c_42027,c_44106]) ).
tcf(c_44330,plain,
( ( iPr_def_16 = iPr_def_22 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_35529,c_37109]) ).
tcf(c_44336,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_16 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_282,c_44330]) ).
tcf(c_44409,plain,
( ( iPr_def_16 = iPr_def_22 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_44336,c_37251,c_37441,c_37936]) ).
tcf(c_44410,plain,
( iPr_def_11
| ( iPr_def_16 = iPr_def_22 ) ),
inference(renaming,[status(thm)],[c_44409]) ).
tcf(c_44417,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c6 = iPr_def_18 ) ),
inference(global_subsumption_just,[status(thm)],[c_20653,c_37251,c_39109]) ).
tcf(c_44419,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( sk_c6 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_44417,c_43941]) ).
tcf(c_44452,plain,
( ( iPr_def_16 = iPr_def_22 )
| ( iPr_def_15 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_44419,c_19503]) ).
tcf(c_44496,plain,
iPr_def_16 = iPr_def_22,
inference(global_subsumption_just,[status(thm)],[c_20654,c_278,c_1190,c_1191,c_7183,c_7187,c_12620,c_37251,c_38464,c_39387,c_44410,c_44452]) ).
tcf(c_44507,plain,
( ~ iPr_def_12
| ( iPr_def_16 != iPr_def_16 )
| ( sk_c6 != iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_19919,c_44496]) ).
tcf(c_44527,plain,
( ( sk_c6 = iPr_def_16 )
| ( sk_c6 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_22699,c_44496]) ).
tcf(c_44577,plain,
( ~ iPr_def_12
| ( sk_c6 != iPr_def_15 ) ),
inference(equality_resolution_simp,[status(thm)],[c_44507]) ).
tcf(c_45028,plain,
( ( sk_c6 = iPr_def_15 )
| ~ iPr_def_10
| ( identity != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_44527,c_44032]) ).
tcf(c_45631,plain,
( ( identity = iPr_def_15 )
| ~ iPr_def_13
| ( identity != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_41912,c_28707]) ).
tcf(c_46143,plain,
( ( sk_c7 != iPr_def_17 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_41132,c_11254,c_11726,c_13344,c_42350,c_45028]) ).
tcf(c_46144,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_17 ) ),
inference(renaming,[status(thm)],[c_46143]) ).
tcf(c_46242,plain,
( ~ iPr_def_12
| ( inverse(identity) != sk_c6 ) ),
inference(global_subsumption_just,[status(thm)],[c_19904,c_278,c_1092,c_1077,c_1190,c_1191,c_2659,c_7183,c_7187,c_12620,c_37251,c_38464,c_39387,c_44410,c_44452]) ).
tcf(c_46244,plain,
( ~ iPr_def_12
| ( sk_c6 != identity ) ),
inference(light_normalisation,[status(thm)],[c_46242,c_30014]) ).
tcf(c_46255,plain,
( ( sk_c6 = iPr_def_15 )
| ~ iPr_def_12
| ( identity != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_291,c_46244]) ).
tcf(c_46266,plain,
( ( sk_c6 = iPr_def_15 )
| ( identity != iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_46255,c_8311,c_29681,c_46255]) ).
tcf(c_46844,plain,
( ~ iPr_def_11
| ( sk_c6 != iPr_def_16 )
| ( sk_c6 != identity ) ),
inference(light_normalisation,[status(thm)],[c_19973,c_30014,c_44496]) ).
tcf(c_46859,plain,
( ( sk_c6 = iPr_def_14 )
| ~ iPr_def_11
| ( identity != iPr_def_15 )
| ( sk_c6 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_287,c_46844]) ).
tcf(c_47222,plain,
iPr_def_16 = iPr_def_22,
inference(global_subsumption_just,[status(thm)],[c_27221,c_278,c_1190,c_1191,c_7183,c_7187,c_12620,c_37251,c_38464,c_39387,c_44410,c_44452]) ).
tcf(c_47248,plain,
( ( sk_c6 = iPr_def_14 )
| ( multiply(sk_c6,iPr_def_16) = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_14660,c_47222]) ).
tcf(c_47289,plain,
( ( sk_c7 = iPr_def_16 )
| ( sk_c6 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_12666,c_47222]) ).
tcf(c_47291,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_14395,c_47222]) ).
tcf(c_47293,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_15,sk_c7) = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_3375,c_47222]) ).
tcf(c_47299,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(iPr_def_14,X0)) = multiply(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_1874,c_47222]) ).
tcf(c_47304,plain,
multiply(sk_c4,iPr_def_16) = multiply(iPr_def_16,sk_c7),
inference(demodulation,[status(thm)],[c_4812,c_47222]) ).
tcf(c_47305,plain,
multiply(sk_c1,iPr_def_16) = multiply(iPr_def_21,sk_c7),
inference(demodulation,[status(thm)],[c_4560,c_47222]) ).
tcf(c_47325,plain,
( ( sk_c6 = iPr_def_15 )
| ( multiply(sk_c6,iPr_def_21) = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_787,c_47222]) ).
tcf(c_47331,plain,
multiply(iPr_def_19,iPr_def_14) = iPr_def_16,
inference(demodulation,[status(thm)],[c_1871,c_47222]) ).
tcf(c_47339,plain,
multiply(sk_c2,iPr_def_16) = iPr_def_14,
inference(demodulation,[status(thm)],[c_529,c_47222]) ).
tcf(c_47934,plain,
iPr_def_19 = iPr_def_20,
inference(global_subsumption_just,[status(thm)],[c_41951,c_44163]) ).
tcf(c_47964,plain,
inverse(iPr_def_19) = sk_c1,
inference(demodulation,[status(thm)],[c_11373,c_47934]) ).
tcf(c_47975,plain,
multiply(iPr_def_19,iPr_def_21) = sk_c6,
inference(demodulation,[status(thm)],[c_1764,c_47934]) ).
tcf(c_47978,plain,
multiply(iPr_def_19,sk_c1) = identity,
inference(demodulation,[status(thm)],[c_828,c_47934]) ).
tcf(c_47981,plain,
inverse(sk_c1) = iPr_def_19,
inference(demodulation,[status(thm)],[c_279,c_47934]) ).
tcf(c_47989,plain,
sk_c1 = sk_c2,
inference(demodulation,[status(thm)],[c_12368,c_47964]) ).
tcf(c_47991,plain,
multiply(sk_c1,iPr_def_16) = iPr_def_14,
inference(demodulation,[status(thm)],[c_47339,c_47989]) ).
tcf(c_48008,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_17 )
| ~ iPr_def_13
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,iPr_def_14) != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_14906,c_47222]) ).
tcf(c_48021,plain,
( ( iPr_def_16 = iPr_def_17 )
| ~ iPr_def_13
| ( sk_c7 != iPr_def_14 )
| ( inverse(identity) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_70,c_48008]) ).
tcf(c_48039,plain,
( ( iPr_def_16 = iPr_def_17 )
| ~ iPr_def_13
| ( sk_c7 != iPr_def_14 )
| ( sk_c6 != identity ) ),
inference(light_normalisation,[status(thm)],[c_48021,c_6058]) ).
tcf(c_48122,plain,
multiply(iPr_def_21,sk_c7) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_47305,c_47991]) ).
tcf(c_48134,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_21,iPr_def_21) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_301,c_48122]) ).
tcf(c_48136,plain,
( ( sk_c6 = iPr_def_19 )
| ( multiply(iPr_def_21,iPr_def_17) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_293,c_48122]) ).
tcf(c_48138,plain,
multiply(inverse(iPr_def_21),iPr_def_14) = sk_c7,
inference(superposition,[status(thm)],[c_48122,c_5521]) ).
tcf(c_48415,plain,
( ( identity = iPr_def_15 )
| ( multiply(iPr_def_21,iPr_def_21) = identity ) ),
inference(light_normalisation,[status(thm)],[c_27287,c_41788]) ).
tcf(c_48436,plain,
( ( identity = iPr_def_15 )
| ( identity = iPr_def_14 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_48415,c_48134]) ).
tcf(c_48745,plain,
( ( sk_c6 = iPr_def_14 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_36431,c_986,c_982,c_2014,c_2086,c_47289]) ).
tcf(c_48751,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c6 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_282,c_48745]) ).
tcf(c_48756,plain,
( ( sk_c6 = iPr_def_14 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_48751,c_10595,c_42620,c_48751]) ).
tcf(c_48757,plain,
( iPr_def_11
| ( sk_c6 = iPr_def_14 ) ),
inference(renaming,[status(thm)],[c_48756]) ).
tcf(c_48785,plain,
( ( sk_c6 = iPr_def_15 )
| ~ iPr_def_10
| ( sk_c6 != iPr_def_14 )
| ( inverse(iPr_def_14) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_12010,c_286]) ).
tcf(c_48877,plain,
( ( identity = iPr_def_15 )
| ~ iPr_def_10
| ( identity != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_41964,c_28705]) ).
tcf(c_49029,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_48785,c_274,c_1061,c_1062,c_1540,c_4469,c_4468,c_28419,c_28705,c_45028,c_46144,c_48436,c_48877]) ).
tcf(c_49033,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_282,c_49029]) ).
tcf(c_49086,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( multiply(iPr_def_15,iPr_def_16) = multiply(iPr_def_16,sk_c7) ) ),
inference(superposition,[status(thm)],[c_42030,c_47304]) ).
tcf(c_49098,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( multiply(iPr_def_15,sk_c6) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_42030,c_275]) ).
tcf(c_49106,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( multiply(iPr_def_16,sk_c7) = sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_49086,c_1749]) ).
tcf(c_49125,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( multiply(iPr_def_15,iPr_def_16) = multiply(iPr_def_16,sk_c7) ) ),
inference(superposition,[status(thm)],[c_42096,c_47304]) ).
tcf(c_49143,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( multiply(iPr_def_16,sk_c7) = sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_49125,c_1749]) ).
tcf(c_49372,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( sk_c7 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_43035,c_47222]) ).
tcf(c_49398,plain,
( ( iPr_def_14 = iPr_def_21 )
| ~ iPr_def_13
| ( identity != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_49372,c_28707]) ).
tcf(c_49444,plain,
iPr_def_14 = iPr_def_21,
inference(global_subsumption_just,[status(thm)],[c_43041,c_282,c_274,c_278,c_1061,c_1062,c_1092,c_1190,c_1191,c_1540,c_4469,c_4468,c_5053,c_7183,c_7187,c_12395,c_12620,c_13344,c_28419,c_28705,c_37251,c_38464,c_39387,c_44410,c_44452,c_45028,c_46144,c_48436,c_48877,c_49143,c_49398]) ).
tcf(c_49449,plain,
multiply(inverse(iPr_def_14),iPr_def_14) = sk_c7,
inference(demodulation,[status(thm)],[c_48138,c_49444]) ).
tcf(c_49450,plain,
multiply(iPr_def_19,iPr_def_14) = sk_c6,
inference(demodulation,[status(thm)],[c_47975,c_49444]) ).
tcf(c_49454,plain,
( ( sk_c6 = iPr_def_19 )
| ( multiply(iPr_def_14,iPr_def_17) = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_48136,c_49444]) ).
tcf(c_49457,plain,
multiply(iPr_def_14,sk_c7) = iPr_def_14,
inference(demodulation,[status(thm)],[c_48122,c_49444]) ).
tcf(c_49486,plain,
( ( sk_c7 = iPr_def_17 )
| ( sk_c7 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_301,c_49444]) ).
tcf(c_49489,plain,
sk_c6 = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_49450,c_47331]) ).
tcf(c_49563,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_13
| ( iPr_def_16 != iPr_def_17 )
| ( identity != iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_6663,c_49489]) ).
tcf(c_49576,plain,
multiply(iPr_def_15,iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_1749,c_49489]) ).
tcf(c_49578,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != iPr_def_16 )
| ( multiply(X0,iPr_def_16) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_283,c_49489]) ).
tcf(c_49798,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_14 )
| ( inverse(sk_c1) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_47991,c_49578]) ).
tcf(c_49802,plain,
( ~ iPr_def_13
| ( iPr_def_16 != iPr_def_19 )
| ( sk_c7 != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_49798,c_47981]) ).
tcf(c_49852,plain,
( ( sk_c7 = iPr_def_14 )
| ( multiply(iPr_def_14,iPr_def_17) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_49486,c_49457]) ).
tcf(c_49926,plain,
sk_c6 = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_47248,c_41964,c_46859,c_48757,c_49489]) ).
tcf(c_49928,plain,
iPr_def_14 = iPr_def_16,
inference(demodulation,[status(thm)],[c_49489,c_49926]) ).
tcf(c_49950,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( identity = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_9663,c_49928]) ).
tcf(c_50106,plain,
multiply(iPr_def_15,iPr_def_14) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_49576,c_49928]) ).
tcf(c_50109,plain,
multiply(sk_c4,iPr_def_14) = iPr_def_14,
inference(superposition,[status(thm)],[c_50106,c_8216]) ).
tcf(c_50163,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( multiply(iPr_def_15,sk_c7) = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_47293,c_49928]) ).
tcf(c_50175,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_14) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_50163,c_8216]) ).
tcf(c_50176,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c7 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_50175,c_50109]) ).
tcf(c_50187,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(iPr_def_14,X0)) = multiply(iPr_def_14,X0),
inference(light_normalisation,[status(thm)],[c_47299,c_49928]) ).
tcf(c_50191,plain,
! [X0: $i] : multiply(iPr_def_19,X0) = X0,
inference(superposition,[status(thm)],[c_28671,c_50187]) ).
tcf(c_50195,plain,
sk_c1 = identity,
inference(demodulation,[status(thm)],[c_47978,c_50191]) ).
tcf(c_50198,plain,
inverse(identity) = iPr_def_19,
inference(demodulation,[status(thm)],[c_47981,c_50195]) ).
tcf(c_50199,plain,
inverse(iPr_def_19) = identity,
inference(demodulation,[status(thm)],[c_47964,c_50195]) ).
tcf(c_50201,plain,
identity = iPr_def_19,
inference(demodulation,[status(thm)],[c_6058,c_50198]) ).
tcf(c_50244,plain,
sk_c6 = iPr_def_15,
inference(global_subsumption_just,[status(thm)],[c_47325,c_274,c_1061,c_1062,c_1540,c_4469,c_4468,c_8311,c_28419,c_28705,c_45028,c_46144,c_46255,c_48436,c_48877,c_50201]) ).
tcf(c_50246,plain,
iPr_def_14 = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_50244,c_49926]) ).
tcf(c_50250,plain,
multiply(iPr_def_14,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_50106,c_50246]) ).
tcf(c_50291,plain,
inverse(iPr_def_19) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_50199,c_50201]) ).
tcf(c_50322,plain,
iPr_def_14 = iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_49098,c_274,c_278,c_1061,c_1062,c_1092,c_1190,c_1191,c_1540,c_4469,c_4468,c_5053,c_7183,c_7187,c_8311,c_12620,c_28419,c_28705,c_37251,c_38464,c_39387,c_44410,c_44452,c_45028,c_45631,c_46144,c_46255,c_47291,c_48039,c_48436,c_48877,c_49033,c_49106,c_49563,c_49802,c_49950,c_50176,c_50201]) ).
tcf(c_50324,plain,
inverse(iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_50291,c_50322]) ).
tcf(c_50325,plain,
identity = iPr_def_14,
inference(demodulation,[status(thm)],[c_50201,c_50322]) ).
tcf(c_50336,plain,
multiply(iPr_def_14,iPr_def_17) = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_49454,c_274,c_278,c_1061,c_1062,c_1092,c_1190,c_1191,c_1240,c_1540,c_4469,c_4468,c_7183,c_7187,c_8311,c_12620,c_28419,c_28705,c_37251,c_38464,c_39387,c_41964,c_44410,c_44452,c_45028,c_45631,c_46144,c_46255,c_46859,c_47291,c_48039,c_48436,c_48757,c_48877,c_49033,c_49489,c_49454,c_49563,c_49802,c_49852,c_50201,c_50325]) ).
tcf(c_50338,plain,
multiply(inverse(iPr_def_14),iPr_def_14) = iPr_def_17,
inference(superposition,[status(thm)],[c_50336,c_5521]) ).
tcf(c_50340,plain,
iPr_def_14 = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_50338,c_49449,c_50250,c_50324]) ).
tcf(c_50342,plain,
sk_c7 = iPr_def_14,
inference(demodulation,[status(thm)],[c_49486,c_50340]) ).
tcf(c_50541,plain,
~ iPr_def_13,
inference(global_subsumption_just,[status(thm)],[c_982,c_274,c_1061,c_1062,c_1540,c_4469,c_4468,c_8311,c_28419,c_28705,c_45028,c_45631,c_46144,c_46255,c_47291,c_48039,c_48436,c_48877,c_49563,c_49802,c_50201,c_50325,c_50342]) ).
tcf(c_50574,plain,
sk_c6 != iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_1240,c_1240,c_44577,c_46266,c_49033,c_49926,c_50201,c_50541]) ).
tcf(c_50576,plain,
$false,
inference(ground_joinability,[status(thm)],[c_50574,c_49926,c_50322]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP333-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/10.39 % Computer : n006.cluster.edu
% 0.12/10.39 % Model : x86_64 x86_64
% 0.12/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.39 % Memory : 8046.5625MB
% 0.12/10.39 % OS : Linux 6.8.0-71-generic
% 0.12/10.39 % CPULimit : 300
% 0.12/10.39 % WCLimit : 300
% 0.12/10.39 % DateTime : Wed Sep 23 14:29:52 UTC 2026
% 0.16/10.40 % CPUTime :
% 0.16/10.40 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.16/10.44 Running first-order theorem proving
% 0.16/10.44 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/10.45
% 0.16/10.45 % ======== iProver multi-core TPTP/SMT =========
% 0.16/10.45
% 0.16/10.45 % Detected problem language: tptp
% 0.16/10.46 % Proving...
% 15.68/13.36 % SZS status Started for theBenchmark.p
% 15.68/13.36 % SZS status Unsatisfiable for theBenchmark.p
% 15.68/13.36
% 15.68/13.36 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 15.68/13.36
% 15.68/13.36 % ------ iProver source info
% 15.68/13.36
% 15.68/13.36 % git: date: 2026-07-19 20:42:38 +0200
% 15.68/13.36 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 15.68/13.36 % git: non_committed_changes: false
% 15.68/13.36
% 15.68/13.36 % ------ Parsing...% successful
% 15.68/13.36
% 15.68/13.36
% 15.68/13.36 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 15.68/13.36
% 15.68/13.36 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 15.68/13.36
% 15.68/13.36 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 15.68/13.36
% 15.68/13.36 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 15.68/13.36 % ------ Proving...
% 15.68/13.36 % ------ Problem Properties
% 15.68/13.36
% 15.68/13.36 %
% 15.68/13.36 % clauses 34
% 15.68/13.36 % conjectures 22
% 15.68/13.36 % EPR 18
% 15.68/13.36 % Horn 17
% 15.68/13.36 % unary 13
% 15.68/13.36 % binary 16
% 15.68/13.36 % lits 61
% 15.68/13.36 % lits eq 53
% 15.68/13.36 % fd_pure 0
% 15.68/13.36 % fd_pseudo 0
% 15.68/13.36 % fd_cond 0
% 15.68/13.36 % fd_pseudo_cond 0
% 15.68/13.36 % AC symbols 0
% 15.68/13.36
% 15.68/13.36 % ------ Schedule dynamic 5 is on
% 15.68/13.36
% 15.68/13.36 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 15.68/13.36
% 15.68/13.36
% 15.68/13.36 % ------
% 15.68/13.36 % Current options:
% 15.68/13.36 % ------
% 15.68/13.36
% 15.68/13.36
% 15.68/13.36 %
% 15.68/13.36
% 15.68/13.36 % ------ Proving...
% 15.68/13.36 %
% 15.68/13.36
% 15.68/13.36 % SZS status Unsatisfiable for theBenchmark.p
% 15.68/13.36
% 15.68/13.36 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 15.68/13.37
% 15.68/13.37
%------------------------------------------------------------------------------