%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP389-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n013.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:38 PM UTC 2026
% Result : Unsatisfiable 10.06s 5.34s
% Output : CNFRefutation 10.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 43
% Syntax : Number of formulae : 367 ( 149 unt; 15 def)
% Number of atoms : 1198 ( 633 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 560 ( 199 ~; 361 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 2 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 : 21 ( 19 usr; 20 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 122 ( 0 sgn 122 !; 0 ?; 87 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c4,sk_c11) = sk_c10
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c4,sk_c11)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c4) = sk_c11
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c4)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c5,sk_c10) = sk_c9
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c9 = multiply(sk_c5,sk_c10)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( inverse(sk_c5) = sk_c10
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c10 = inverse(sk_c5)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f11]) ).
fof(f17,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( inverse(sk_c7) = sk_c8
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c8 = inverse(sk_c7)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f19]) ).
fof(f23,negated_conjecture,
( multiply(sk_c4,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c10 = multiply(sk_c4,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c4) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c11 = inverse(sk_c4)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f31,negated_conjecture,
( inverse(sk_c6) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c11 = inverse(sk_c6)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f33]) ).
fof(f37,negated_conjecture,
( inverse(sk_c7) = sk_c8
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c8 = inverse(sk_c7)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f37]) ).
fof(f49,negated_conjecture,
( inverse(sk_c6) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_23) ).
fof(f50,plain,
( sk_c11 = inverse(sk_c6)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f51]) ).
fof(f55,negated_conjecture,
( inverse(sk_c7) = sk_c8
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c8 = inverse(sk_c7)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f55]) ).
fof(f59,negated_conjecture,
( multiply(sk_c4,sk_c11) = sk_c10
| multiply(sk_c2,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c10 = multiply(sk_c4,sk_c11)
| sk_c10 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( inverse(sk_c4) = sk_c11
| multiply(sk_c2,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c11 = inverse(sk_c4)
| sk_c10 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f61]) ).
fof(f77,negated_conjecture,
( multiply(sk_c4,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
( sk_c10 = multiply(sk_c4,sk_c11)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f77]) ).
fof(f79,negated_conjecture,
( inverse(sk_c4) = sk_c11
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_38) ).
fof(f80,plain,
( sk_c11 = inverse(sk_c4)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f79]) ).
fof(f95,negated_conjecture,
( multiply(sk_c4,sk_c11) = sk_c10
| multiply(sk_c3,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_46) ).
fof(f96,plain,
( sk_c10 = multiply(sk_c4,sk_c11)
| sk_c10 = multiply(sk_c3,sk_c9) ),
inference(reorient_equations,[],[f95]) ).
fof(f97,negated_conjecture,
( inverse(sk_c4) = sk_c11
| multiply(sk_c3,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_47) ).
fof(f98,plain,
( sk_c11 = inverse(sk_c4)
| sk_c10 = multiply(sk_c3,sk_c9) ),
inference(reorient_equations,[],[f97]) ).
fof(f99,negated_conjecture,
( multiply(sk_c5,sk_c10) = sk_c9
| multiply(sk_c3,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_48) ).
fof(f100,plain,
( sk_c9 = multiply(sk_c5,sk_c10)
| sk_c10 = multiply(sk_c3,sk_c9) ),
inference(reorient_equations,[],[f99]) ).
fof(f101,negated_conjecture,
( inverse(sk_c5) = sk_c10
| multiply(sk_c3,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_49) ).
fof(f102,plain,
( sk_c10 = inverse(sk_c5)
| sk_c10 = multiply(sk_c3,sk_c9) ),
inference(reorient_equations,[],[f101]) ).
fof(f113,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X7,sk_c9) != sk_c10
| inverse(X6) != X7
| multiply(X6,X7) != sk_c10
| multiply(X5,sk_c10) != sk_c11
| inverse(X5) != sk_c11
| inverse(X4) != sk_c10
| multiply(X4,sk_c10) != sk_c9
| inverse(X3) != sk_c11
| multiply(X3,sk_c11) != sk_c10
| multiply(X2,sk_c9) != sk_c10
| inverse(X1) != X2
| multiply(X1,X2) != sk_c10
| multiply(X0,sk_c10) != sk_c11
| inverse(X0) != sk_c11
| inverse(sk_c10) != sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_55) ).
fof(f114,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( sk_c10 != multiply(X7,sk_c9)
| inverse(X6) != X7
| sk_c10 != multiply(X6,X7)
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c10 != inverse(X4)
| sk_c9 != multiply(X4,sk_c10)
| sk_c11 != inverse(X3)
| sk_c10 != multiply(X3,sk_c11)
| sk_c10 != multiply(X2,sk_c9)
| inverse(X1) != X2
| multiply(X1,X2) != sk_c10
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11
| inverse(sk_c10) != sk_c9 ),
inference(reorient_equations,[],[f113]) ).
fof(f115,plain,
! [X3,X0,X1,X6,X7,X4,X5] :
( sk_c10 != multiply(X7,sk_c9)
| inverse(X6) != X7
| sk_c10 != multiply(X6,X7)
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c10 != inverse(X4)
| sk_c9 != multiply(X4,sk_c10)
| sk_c11 != inverse(X3)
| sk_c10 != multiply(X3,sk_c11)
| sk_c10 != multiply(inverse(X1),sk_c9)
| sk_c10 != multiply(X1,inverse(X1))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11
| inverse(sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f114]) ).
fof(f116,plain,
! [X3,X0,X1,X6,X4,X5] :
( sk_c10 != multiply(inverse(X6),sk_c9)
| sk_c10 != multiply(X6,inverse(X6))
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c10 != inverse(X4)
| sk_c9 != multiply(X4,sk_c10)
| sk_c11 != inverse(X3)
| sk_c10 != multiply(X3,sk_c11)
| sk_c10 != multiply(inverse(X1),sk_c9)
| sk_c10 != multiply(X1,inverse(X1))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11
| inverse(sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f115]) ).
tcf(c_107,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_108,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_112,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c5,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c5) = sk_c10 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c7) = sk_c8 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_120,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c6) = sk_c11 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c6) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_133,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_135,negated_conjecture,
( ( inverse(sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_137,negated_conjecture,
( ( multiply(sk_c2,sk_c3) = sk_c10 )
| ( multiply(sk_c4,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c2,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c4,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_155,negated_conjecture,
( ( multiply(sk_c3,sk_c9) = sk_c10 )
| ( multiply(sk_c4,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_156,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c3,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_157,negated_conjecture,
( ( multiply(sk_c3,sk_c9) = sk_c10 )
| ( multiply(sk_c5,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_158,negated_conjecture,
( ( inverse(sk_c5) = sk_c10 )
| ( multiply(sk_c3,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_164,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(sk_c10) != sk_c9 )
| ( inverse(X5) != sk_c11 )
| ( inverse(X4) != sk_c10 )
| ( inverse(X3) != sk_c11 )
| ( inverse(X0) != sk_c11 )
| ( multiply(X5,sk_c10) != sk_c11 )
| ( multiply(X4,sk_c10) != sk_c9 )
| ( multiply(X3,sk_c11) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c11 )
| ( multiply(inverse(X2),sk_c9) != sk_c10 )
| ( multiply(inverse(X1),sk_c9) != sk_c10 )
| ( multiply(X2,inverse(X2)) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c10 ) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_661,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_164]) ).
tcf(c_662,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_164]) ).
tcf(c_663,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_164]) ).
tcf(c_664,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( multiply(inverse(X0),sk_c9) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_164]) ).
tcf(c_665,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_164]) ).
tcf(c_666,definition,
iPr_def_14 = inverse(sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_667,definition,
iPr_def_15 = multiply(sk_c8,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_668,definition,
iPr_def_16 = multiply(sk_c3,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_669,definition,
iPr_def_17 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_670,definition,
iPr_def_18 = multiply(sk_c7,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_671,definition,
iPr_def_19 = multiply(sk_c6,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_672,definition,
iPr_def_20 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_673,definition,
iPr_def_21 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_674,definition,
iPr_def_22 = multiply(sk_c5,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_675,definition,
iPr_def_23 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_676,definition,
iPr_def_24 = multiply(sk_c4,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_677,definition,
iPr_def_25 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_678,definition,
iPr_def_26 = multiply(sk_c2,sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_679,definition,
iPr_def_27 = multiply(sk_c1,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_680,definition,
iPr_def_28 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_681,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_665,c_666]) ).
tcf(c_684,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( multiply(inverse(X0),sk_c9) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_664]) ).
tcf(c_685,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_663]) ).
tcf(c_686,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_662]) ).
tcf(c_687,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_661]) ).
tcf(c_693,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_158,c_673]) ).
tcf(c_694,negated_conjecture,
( ( iPr_def_22 = sk_c9 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_157,c_674]) ).
tcf(c_695,negated_conjecture,
( ( iPr_def_23 = sk_c11 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_156,c_675]) ).
tcf(c_696,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_155,c_676]) ).
tcf(c_704,negated_conjecture,
( ( iPr_def_25 = sk_c3 )
| ( iPr_def_23 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_147]) ).
tcf(c_705,negated_conjecture,
( ( iPr_def_25 = sk_c3 )
| ( iPr_def_24 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_146]) ).
tcf(c_713,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_23 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_138]) ).
tcf(c_714,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_24 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_716,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_17 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_135]) ).
tcf(c_718,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_133]) ).
tcf(c_719,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_132]) ).
tcf(c_725,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_17 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_727,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_728,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_731,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_23 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_732,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_24 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_734,negated_conjecture,
( ( iPr_def_17 = sk_c8 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_735,negated_conjecture,
( ( iPr_def_18 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_738,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_739,negated_conjecture,
( ( iPr_def_22 = sk_c9 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_740,negated_conjecture,
( ( iPr_def_23 = sk_c11 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_111]) ).
tcf(c_741,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_742,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_743,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1230,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_695,c_676]) ).
tcf(c_1269,plain,
multiply(iPr_def_14,sk_c10) = identity,
inference(superposition,[status(thm)],[c_666,c_108]) ).
tcf(c_1270,plain,
multiply(iPr_def_23,sk_c4) = identity,
inference(superposition,[status(thm)],[c_675,c_108]) ).
tcf(c_1271,plain,
multiply(iPr_def_21,sk_c5) = identity,
inference(superposition,[status(thm)],[c_673,c_108]) ).
tcf(c_1273,plain,
multiply(iPr_def_17,sk_c7) = identity,
inference(superposition,[status(thm)],[c_669,c_108]) ).
tcf(c_1274,plain,
multiply(iPr_def_28,sk_c1) = identity,
inference(superposition,[status(thm)],[c_680,c_108]) ).
tcf(c_1275,plain,
multiply(iPr_def_25,sk_c2) = identity,
inference(superposition,[status(thm)],[c_677,c_108]) ).
tcf(c_1292,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_704,c_678]) ).
tcf(c_1302,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_705,c_678]) ).
tcf(c_1303,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(iPr_def_25,sk_c9) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_705,c_668]) ).
tcf(c_1346,plain,
! [X0: $i] :
( ( iPr_def_14 = sk_c9 )
| ( iPr_def_14 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_743]) ).
tcf(c_1349,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_743]) ).
tcf(c_1350,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1349]) ).
tcf(c_1351,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_742]) ).
tcf(c_1361,plain,
( ( sk_c9 = iPr_def_22 )
| ( iPr_def_22 != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1350]) ).
tcf(c_1413,plain,
( ( sk_c9 = iPr_def_14 )
| ( iPr_def_14 != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1350]) ).
tcf(c_1541,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_713,c_676]) ).
tcf(c_1599,plain,
( ( iPr_def_14 = sk_c9 )
| ( iPr_def_14 != iPr_def_22 )
| ( sk_c9 != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_1346]) ).
tcf(c_1675,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(sk_c7,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_716,c_670]) ).
tcf(c_1746,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_27) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_718,c_676]) ).
tcf(c_1794,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c4,iPr_def_27) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_719,c_676]) ).
tcf(c_2079,plain,
( ( sk_c11 = iPr_def_28 )
| ( multiply(sk_c7,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_725,c_670]) ).
tcf(c_2206,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_28) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_727,c_676]) ).
tcf(c_2290,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c4,iPr_def_28) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_728,c_676]) ).
tcf(c_2656,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c7,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_734,c_670]) ).
tcf(c_2657,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_17,sk_c9) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_734,c_667]) ).
tcf(c_2862,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_739,c_738]) ).
tcf(c_2865,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_739,c_735]) ).
tcf(c_2867,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c3,iPr_def_22) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_739,c_668]) ).
tcf(c_2868,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c8,iPr_def_22) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_739,c_667]) ).
tcf(c_3018,plain,
! [X0: $i] : multiply(sk_c5,multiply(sk_c10,X0)) = multiply(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_674,c_109]) ).
tcf(c_3020,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c8,X0)) = multiply(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_670,c_109]) ).
tcf(c_3022,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c10,X0)) = multiply(iPr_def_27,X0),
inference(superposition,[status(thm)],[c_679,c_109]) ).
tcf(c_3023,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c3,X0)) = multiply(iPr_def_26,X0),
inference(superposition,[status(thm)],[c_678,c_109]) ).
tcf(c_3026,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_108,c_109]) ).
tcf(c_3028,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c10,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1269,c_109]) ).
tcf(c_3029,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1270,c_109]) ).
tcf(c_3030,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1271,c_109]) ).
tcf(c_3032,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1273,c_109]) ).
tcf(c_3033,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1274,c_109]) ).
tcf(c_3034,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1275,c_109]) ).
tcf(c_3036,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3034,c_107]) ).
tcf(c_3037,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3033,c_107]) ).
tcf(c_3038,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3032,c_107]) ).
tcf(c_3040,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3030,c_107]) ).
tcf(c_3041,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3029,c_107]) ).
tcf(c_3042,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3028,c_107]) ).
tcf(c_3665,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_741,c_681]) ).
tcf(c_3666,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c11 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_740,c_681]) ).
tcf(c_3668,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_738,c_681]) ).
tcf(c_3671,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_735,c_681]) ).
tcf(c_3769,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_22 )
| ( inverse(sk_c5) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_674,c_685]) ).
tcf(c_3775,plain,
( ~ iPr_def_12
| ( sk_c9 != identity )
| ( inverse(iPr_def_14) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_1269,c_685]) ).
tcf(c_3804,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_22 )
| ( sk_c10 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_3769,c_673]) ).
tcf(c_3956,plain,
( ~ iPr_def_11
| ( sk_c11 != iPr_def_19 )
| ( inverse(sk_c6) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_671,c_686]) ).
tcf(c_3957,plain,
( ~ iPr_def_11
| ( sk_c11 != iPr_def_27 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_679,c_686]) ).
tcf(c_3982,plain,
( ~ iPr_def_11
| ( sk_c11 != iPr_def_28 )
| ( sk_c11 != iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_3957,c_680]) ).
tcf(c_3986,plain,
( ~ iPr_def_11
| ( sk_c11 != iPr_def_20 )
| ( sk_c11 != iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_3956,c_672]) ).
tcf(c_4159,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_24 )
| ( inverse(sk_c4) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_676,c_687]) ).
tcf(c_4161,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_108,c_687]) ).
tcf(c_4186,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_23 )
| ( sk_c10 != iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_4159,c_675]) ).
tcf(c_4350,plain,
( ~ iPr_def_13
| ( inverse(identity) != sk_c10 )
| ( multiply(inverse(identity),sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_107,c_684]) ).
tcf(c_6244,plain,
multiply(iPr_def_28,iPr_def_27) = sk_c10,
inference(superposition,[status(thm)],[c_679,c_3037]) ).
tcf(c_6247,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(iPr_def_27,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_6244,c_109]) ).
tcf(c_6457,plain,
multiply(iPr_def_21,iPr_def_22) = sk_c10,
inference(superposition,[status(thm)],[c_674,c_3040]) ).
tcf(c_6470,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(iPr_def_22,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_6457,c_109]) ).
tcf(c_6472,plain,
multiply(iPr_def_23,iPr_def_24) = sk_c11,
inference(superposition,[status(thm)],[c_676,c_3041]) ).
tcf(c_6485,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(iPr_def_24,X0)) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_6472,c_109]) ).
tcf(c_8369,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(iPr_def_25,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_741,c_1303]) ).
tcf(c_9196,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1746,c_3041]) ).
tcf(c_9197,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c11 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_9196,c_6472]) ).
tcf(c_9208,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1794,c_3041]) ).
tcf(c_9209,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c11 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_9208,c_6472]) ).
tcf(c_9608,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2206,c_3041]) ).
tcf(c_9609,plain,
( ( sk_c11 = iPr_def_28 )
| ( sk_c11 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_9608,c_6472]) ).
tcf(c_9629,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2290,c_3041]) ).
tcf(c_9630,plain,
( ( sk_c11 = iPr_def_28 )
| ( sk_c11 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_9629,c_6472]) ).
tcf(c_10906,plain,
multiply(sk_c7,iPr_def_15) = multiply(iPr_def_18,sk_c9),
inference(superposition,[status(thm)],[c_667,c_3020]) ).
tcf(c_10907,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c7,iPr_def_15) = multiply(iPr_def_18,iPr_def_22) ) ),
inference(superposition,[status(thm)],[c_2868,c_3020]) ).
tcf(c_11468,plain,
multiply(sk_c2,iPr_def_16) = multiply(iPr_def_26,sk_c9),
inference(superposition,[status(thm)],[c_668,c_3023]) ).
tcf(c_12916,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_3026,c_107]) ).
tcf(c_12946,plain,
multiply(inverse(sk_c4),iPr_def_24) = sk_c11,
inference(superposition,[status(thm)],[c_676,c_12916]) ).
tcf(c_12950,plain,
multiply(inverse(sk_c8),iPr_def_15) = sk_c9,
inference(superposition,[status(thm)],[c_667,c_12916]) ).
tcf(c_12954,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_107,c_12916]) ).
tcf(c_12955,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_108,c_12916]) ).
tcf(c_12956,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_109,c_12916]) ).
tcf(c_13043,plain,
multiply(inverse(iPr_def_14),identity) = sk_c10,
inference(superposition,[status(thm)],[c_1269,c_12916]) ).
tcf(c_13128,plain,
! [X0: $i] : multiply(inverse(iPr_def_14),X0) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_3042,c_12916]) ).
tcf(c_13129,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_3041,c_12916]) ).
tcf(c_13130,plain,
! [X0: $i] : multiply(inverse(iPr_def_21),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_3040,c_12916]) ).
tcf(c_13132,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_3038,c_12916]) ).
tcf(c_13133,plain,
! [X0: $i] : multiply(inverse(iPr_def_28),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_3037,c_12916]) ).
tcf(c_13134,plain,
! [X0: $i] : multiply(inverse(iPr_def_25),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_3036,c_12916]) ).
tcf(c_13173,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_12916,c_12916]) ).
tcf(c_13784,plain,
multiply(sk_c10,identity) = sk_c10,
inference(demodulation,[status(thm)],[c_13043,c_13128]) ).
tcf(c_13817,plain,
multiply(sk_c1,sk_c10) = multiply(iPr_def_27,identity),
inference(superposition,[status(thm)],[c_13784,c_3022]) ).
tcf(c_13819,plain,
multiply(sk_c5,sk_c10) = multiply(iPr_def_22,identity),
inference(superposition,[status(thm)],[c_13784,c_3018]) ).
tcf(c_13822,plain,
multiply(iPr_def_22,identity) = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_13819,c_674]) ).
tcf(c_13824,plain,
multiply(iPr_def_27,identity) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_13817,c_679]) ).
tcf(c_13963,plain,
multiply(sk_c10,identity) = multiply(iPr_def_21,iPr_def_22),
inference(superposition,[status(thm)],[c_13822,c_6470]) ).
tcf(c_13971,plain,
multiply(inverse(iPr_def_27),iPr_def_27) = identity,
inference(superposition,[status(thm)],[c_13824,c_12916]) ).
tcf(c_13973,plain,
multiply(sk_c10,identity) = multiply(iPr_def_28,iPr_def_27),
inference(superposition,[status(thm)],[c_13824,c_6247]) ).
tcf(c_14116,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_12955,c_13173]) ).
tcf(c_14136,plain,
multiply(sk_c11,identity) = multiply(iPr_def_23,iPr_def_24),
inference(superposition,[status(thm)],[c_14116,c_6485]) ).
tcf(c_14150,plain,
multiply(sk_c2,sk_c3) = multiply(iPr_def_26,identity),
inference(superposition,[status(thm)],[c_14116,c_3023]) ).
tcf(c_14157,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_14116,c_12954]) ).
tcf(c_14158,plain,
multiply(iPr_def_26,identity) = iPr_def_26,
inference(light_normalisation,[status(thm)],[c_14150,c_678]) ).
tcf(c_14165,plain,
multiply(sk_c11,identity) = sk_c11,
inference(light_normalisation,[status(thm)],[c_14136,c_6472]) ).
tcf(c_14177,plain,
( ( sk_c10 = iPr_def_21 )
| ( sk_c9 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_2862,c_739,c_1351,c_1361,c_1413,c_1599,c_2862]) ).
tcf(c_14178,plain,
( ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_21 ) ),
inference(renaming,[status(thm)],[c_14177]) ).
tcf(c_14282,plain,
( ( sk_c10 = iPr_def_18 )
| ( sk_c9 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_2865,c_739,c_1351,c_1361,c_1413,c_1599,c_2865]) ).
tcf(c_14283,plain,
( ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_18 ) ),
inference(renaming,[status(thm)],[c_14282]) ).
tcf(c_14440,plain,
multiply(sk_c10,iPr_def_14) = identity,
inference(superposition,[status(thm)],[c_13128,c_108]) ).
tcf(c_14443,plain,
! [X0: $i] : multiply(sk_c10,multiply(iPr_def_14,X0)) = X0,
inference(superposition,[status(thm)],[c_13128,c_12916]) ).
tcf(c_14444,plain,
multiply(sk_c10,identity) = inverse(iPr_def_14),
inference(superposition,[status(thm)],[c_13128,c_14116]) ).
tcf(c_14492,plain,
multiply(sk_c1,identity) = multiply(iPr_def_27,iPr_def_14),
inference(superposition,[status(thm)],[c_14440,c_3022]) ).
tcf(c_14494,plain,
multiply(sk_c5,identity) = multiply(iPr_def_22,iPr_def_14),
inference(superposition,[status(thm)],[c_14440,c_3018]) ).
tcf(c_14572,plain,
inverse(iPr_def_14) = sk_c10,
inference(demodulation,[status(thm)],[c_14444,c_14116]) ).
tcf(c_15632,plain,
multiply(iPr_def_27,iPr_def_14) = sk_c1,
inference(demodulation,[status(thm)],[c_14492,c_14116]) ).
tcf(c_15633,plain,
multiply(inverse(iPr_def_27),sk_c1) = iPr_def_14,
inference(superposition,[status(thm)],[c_15632,c_12916]) ).
tcf(c_15635,plain,
multiply(sk_c10,iPr_def_14) = multiply(iPr_def_28,sk_c1),
inference(superposition,[status(thm)],[c_15632,c_6247]) ).
tcf(c_15638,plain,
! [X0: $i] : multiply(inverse(iPr_def_27),multiply(sk_c1,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_15633,c_109]) ).
tcf(c_15666,plain,
multiply(inverse(iPr_def_27),iPr_def_27) = multiply(iPr_def_14,sk_c10),
inference(superposition,[status(thm)],[c_679,c_15638]) ).
tcf(c_15959,plain,
multiply(iPr_def_22,iPr_def_14) = sk_c5,
inference(demodulation,[status(thm)],[c_14494,c_14116]) ).
tcf(c_15960,plain,
multiply(inverse(iPr_def_22),sk_c5) = iPr_def_14,
inference(superposition,[status(thm)],[c_15959,c_12916]) ).
tcf(c_15965,plain,
! [X0: $i] : multiply(inverse(iPr_def_22),multiply(sk_c5,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_15960,c_109]) ).
tcf(c_16404,plain,
multiply(inverse(iPr_def_22),iPr_def_22) = multiply(iPr_def_14,sk_c10),
inference(superposition,[status(thm)],[c_674,c_15965]) ).
tcf(c_18841,plain,
multiply(sk_c4,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_13129,c_108]) ).
tcf(c_18842,plain,
( ~ iPr_def_10
| ( multiply(sk_c4,sk_c11) != sk_c10 )
| ( inverse(inverse(iPr_def_23)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_13129,c_687]) ).
tcf(c_18844,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_23,X0)) = X0,
inference(superposition,[status(thm)],[c_13129,c_12916]) ).
tcf(c_18845,plain,
multiply(sk_c4,identity) = inverse(iPr_def_23),
inference(superposition,[status(thm)],[c_13129,c_14116]) ).
tcf(c_18846,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_24 )
| ( inverse(inverse(iPr_def_23)) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_18842,c_676]) ).
tcf(c_18860,plain,
( ( identity = iPr_def_24 )
| ( sk_c10 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_1541,c_18841]) ).
tcf(c_18861,plain,
( ( identity = iPr_def_24 )
| ( sk_c10 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1230,c_18841]) ).
tcf(c_18882,plain,
multiply(iPr_def_23,identity) = iPr_def_23,
inference(superposition,[status(thm)],[c_18841,c_3041]) ).
tcf(c_18885,plain,
inverse(iPr_def_23) = sk_c4,
inference(demodulation,[status(thm)],[c_18845,c_14116]) ).
tcf(c_19262,plain,
( ( identity = iPr_def_24 )
| ( inverse(iPr_def_26) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_18860,c_666]) ).
tcf(c_19474,plain,
( ( iPr_def_16 = iPr_def_26 )
| ( identity = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_18861,c_18860]) ).
tcf(c_19702,plain,
multiply(sk_c4,sk_c11) = iPr_def_24,
inference(superposition,[status(thm)],[c_6472,c_18844]) ).
tcf(c_19762,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_26 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_19474,c_107]) ).
tcf(c_19777,plain,
( ~ iPr_def_12
| ( multiply(sk_c5,sk_c10) != sk_c9 )
| ( inverse(inverse(iPr_def_21)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_13130,c_685]) ).
tcf(c_19780,plain,
multiply(sk_c5,iPr_def_21) = identity,
inference(superposition,[status(thm)],[c_13130,c_108]) ).
tcf(c_19783,plain,
! [X0: $i] : multiply(sk_c5,multiply(iPr_def_21,X0)) = X0,
inference(superposition,[status(thm)],[c_13130,c_12916]) ).
tcf(c_19784,plain,
multiply(sk_c5,identity) = inverse(iPr_def_21),
inference(superposition,[status(thm)],[c_13130,c_14116]) ).
tcf(c_19792,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_22 )
| ( inverse(inverse(iPr_def_21)) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_19777,c_674]) ).
tcf(c_19842,plain,
multiply(inverse(iPr_def_22),identity) = multiply(iPr_def_14,iPr_def_21),
inference(superposition,[status(thm)],[c_19780,c_15965]) ).
tcf(c_20225,plain,
inverse(iPr_def_21) = sk_c5,
inference(demodulation,[status(thm)],[c_19784,c_14116]) ).
tcf(c_20240,plain,
multiply(sk_c5,identity) = sk_c5,
inference(superposition,[status(thm)],[c_1271,c_19783]) ).
tcf(c_20242,plain,
multiply(sk_c5,sk_c10) = iPr_def_22,
inference(superposition,[status(thm)],[c_6457,c_19783]) ).
tcf(c_20896,plain,
multiply(sk_c7,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_13132,c_108]) ).
tcf(c_20899,plain,
! [X0: $i] : multiply(sk_c7,multiply(iPr_def_17,X0)) = X0,
inference(superposition,[status(thm)],[c_13132,c_12916]) ).
tcf(c_20913,plain,
( ( identity = iPr_def_18 )
| ( sk_c9 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_2656,c_20896]) ).
tcf(c_20914,plain,
( ( identity = iPr_def_18 )
| ( sk_c11 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_2079,c_20896]) ).
tcf(c_20915,plain,
( ( identity = iPr_def_18 )
| ( sk_c11 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_1675,c_20896]) ).
tcf(c_21020,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( identity = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_20913,c_681]) ).
tcf(c_21324,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c7,iPr_def_15) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_2657,c_20899]) ).
tcf(c_21372,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_18,sk_c9) = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_21324,c_10906]) ).
tcf(c_21682,plain,
( iPr_def_13
| iPr_def_12
| ( identity = iPr_def_18 )
| iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_21020,c_3982,c_20915,c_20914,c_21020]) ).
tcf(c_21683,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( identity = iPr_def_18 ) ),
inference(renaming,[status(thm)],[c_21682]) ).
tcf(c_22094,plain,
multiply(sk_c1,iPr_def_28) = identity,
inference(superposition,[status(thm)],[c_13133,c_108]) ).
tcf(c_22098,plain,
multiply(sk_c1,identity) = inverse(iPr_def_28),
inference(superposition,[status(thm)],[c_13133,c_14116]) ).
tcf(c_22180,plain,
multiply(inverse(iPr_def_27),identity) = multiply(iPr_def_14,iPr_def_28),
inference(superposition,[status(thm)],[c_22094,c_15638]) ).
tcf(c_22478,plain,
inverse(iPr_def_28) = sk_c1,
inference(demodulation,[status(thm)],[c_22098,c_14116]) ).
tcf(c_22628,plain,
multiply(sk_c2,iPr_def_25) = identity,
inference(superposition,[status(thm)],[c_13134,c_108]) ).
tcf(c_22630,plain,
( ~ iPr_def_13
| ( multiply(sk_c2,inverse(inverse(iPr_def_25))) != sk_c10 )
| ( multiply(inverse(inverse(iPr_def_25)),sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_13134,c_684]) ).
tcf(c_22631,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_25,X0)) = X0,
inference(superposition,[status(thm)],[c_13134,c_12916]) ).
tcf(c_22632,plain,
multiply(sk_c2,identity) = inverse(iPr_def_25),
inference(superposition,[status(thm)],[c_13134,c_14116]) ).
tcf(c_22645,plain,
( ( identity = iPr_def_26 )
| ( sk_c10 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_1302,c_22628]) ).
tcf(c_22646,plain,
( ( identity = iPr_def_26 )
| ( sk_c11 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_1292,c_22628]) ).
tcf(c_23054,plain,
( ( identity = iPr_def_26 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_22646,c_676]) ).
tcf(c_23057,plain,
( ( identity = iPr_def_26 )
| ( identity = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_23054,c_18841]) ).
tcf(c_23347,plain,
inverse(iPr_def_25) = sk_c2,
inference(demodulation,[status(thm)],[c_22632,c_14116]) ).
tcf(c_23356,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(sk_c2,iPr_def_16) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_1303,c_22631]) ).
tcf(c_23426,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(iPr_def_26,sk_c9) = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_23356,c_11468]) ).
tcf(c_24561,plain,
( ( identity = iPr_def_24 )
| ( inverse(iPr_def_26) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_23057,c_14157]) ).
tcf(c_24563,plain,
! [X0: $i] :
( ( identity = iPr_def_24 )
| ( multiply(iPr_def_26,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_23057,c_107]) ).
tcf(c_27575,plain,
multiply(iPr_def_14,iPr_def_21) = inverse(iPr_def_22),
inference(demodulation,[status(thm)],[c_19842,c_14116]) ).
tcf(c_27590,plain,
multiply(sk_c10,inverse(iPr_def_22)) = iPr_def_21,
inference(superposition,[status(thm)],[c_27575,c_14443]) ).
tcf(c_28316,plain,
multiply(iPr_def_22,inverse(iPr_def_22)) = multiply(sk_c5,iPr_def_21),
inference(superposition,[status(thm)],[c_27590,c_3018]) ).
tcf(c_28319,plain,
multiply(iPr_def_22,inverse(iPr_def_22)) = identity,
inference(light_normalisation,[status(thm)],[c_28316,c_19780]) ).
tcf(c_28583,plain,
( ~ iPr_def_13
| ( sk_c10 != identity )
| ( multiply(inverse(iPr_def_22),sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_28319,c_684]) ).
tcf(c_30908,plain,
multiply(iPr_def_14,iPr_def_28) = inverse(iPr_def_27),
inference(demodulation,[status(thm)],[c_22180,c_14116]) ).
tcf(c_30932,plain,
multiply(sk_c10,inverse(iPr_def_27)) = iPr_def_28,
inference(superposition,[status(thm)],[c_30908,c_14443]) ).
tcf(c_31047,plain,
! [X0: $i] : multiply(sk_c10,multiply(inverse(iPr_def_27),X0)) = multiply(iPr_def_28,X0),
inference(superposition,[status(thm)],[c_30932,c_109]) ).
tcf(c_31048,plain,
multiply(iPr_def_27,inverse(iPr_def_27)) = multiply(sk_c1,iPr_def_28),
inference(superposition,[status(thm)],[c_30932,c_3022]) ).
tcf(c_31053,plain,
multiply(iPr_def_27,inverse(iPr_def_27)) = identity,
inference(light_normalisation,[status(thm)],[c_31048,c_22094]) ).
tcf(c_31166,plain,
multiply(sk_c10,inverse(iPr_def_27)) = multiply(iPr_def_28,identity),
inference(superposition,[status(thm)],[c_31053,c_6247]) ).
tcf(c_31315,plain,
( ~ iPr_def_12
| ( sk_c9 != identity ) ),
inference(ground_joinability,[status(thm)],[c_3775,c_14572]) ).
tcf(c_31333,plain,
( ( sk_c9 = iPr_def_14 )
| ~ iPr_def_12
| ( identity != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_739,c_31315]) ).
tcf(c_31826,plain,
( ( sk_c9 = iPr_def_14 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_31333,c_739,c_1351,c_1361,c_1413,c_3804,c_14178]) ).
tcf(c_33339,plain,
( ( sk_c10 = iPr_def_24 )
| ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(iPr_def_28)) != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_732,c_4161]) ).
tcf(c_33340,plain,
( ( sk_c11 = iPr_def_23 )
| ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(iPr_def_28)) != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_731,c_4161]) ).
tcf(c_33423,plain,
( ( sk_c11 = iPr_def_23 )
| ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(ground_joinability,[status(thm)],[c_33340,c_680,c_22478]) ).
tcf(c_33427,plain,
( ( sk_c10 = iPr_def_24 )
| ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(ground_joinability,[status(thm)],[c_33339,c_680,c_22478]) ).
tcf(c_33570,plain,
( ( identity = iPr_def_24 )
| ~ iPr_def_12
| ( sk_c10 != sk_c9 )
| ( inverse(iPr_def_26) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_24563,c_685]) ).
tcf(c_33891,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( identity = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_24561,c_19262]) ).
tcf(c_34804,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_26 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_33891,c_107]) ).
tcf(c_42385,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_108,c_687]) ).
tcf(c_53023,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_24 )
| ( multiply(iPr_def_26,multiply(inverse(iPr_def_27),X0)) = multiply(iPr_def_28,X0) ) ),
inference(superposition,[status(thm)],[c_714,c_31047]) ).
tcf(c_54518,plain,
( ~ iPr_def_11
| ( sk_c11 != iPr_def_28 ) ),
inference(global_subsumption_just,[status(thm)],[c_3982,c_3986,c_3982,c_9197,c_9209]) ).
tcf(c_54520,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_54518,c_3986,c_9609,c_9630,c_54518]) ).
tcf(c_54523,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c10 = iPr_def_18 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3671,c_54520]) ).
tcf(c_54526,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c10 = iPr_def_21 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3668,c_54520]) ).
tcf(c_54527,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c11 = iPr_def_23 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3666,c_54520]) ).
tcf(c_54528,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c10 = iPr_def_24 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3665,c_54520]) ).
tcf(c_54529,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c9 != iPr_def_14 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_681,c_54520]) ).
tcf(c_57155,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c8)),multiply(X0,iPr_def_15)) = sk_c9,
inference(superposition,[status(thm)],[c_667,c_12956]) ).
tcf(c_57160,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c3)),multiply(X0,iPr_def_16)) = sk_c9,
inference(superposition,[status(thm)],[c_668,c_12956]) ).
tcf(c_57186,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_14 )
| ( multiply(inverse(multiply(X0,sk_c3)),multiply(X0,iPr_def_16)) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_2867,c_12956]) ).
tcf(c_57226,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c4)),multiply(X0,identity)) = iPr_def_23,
inference(superposition,[status(thm)],[c_18841,c_12956]) ).
tcf(c_57253,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_14)),multiply(X0,identity)) = sk_c10,
inference(superposition,[status(thm)],[c_1269,c_12956]) ).
tcf(c_57255,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_21)),multiply(X0,identity)) = sk_c5,
inference(superposition,[status(thm)],[c_1271,c_12956]) ).
tcf(c_57322,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c10)),multiply(X0,identity)) = iPr_def_14,
inference(superposition,[status(thm)],[c_14440,c_12956]) ).
tcf(c_57544,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c10)),X0) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_57322,c_14116]) ).
tcf(c_57549,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_21)),X0) = sk_c5,
inference(light_normalisation,[status(thm)],[c_57255,c_14116]) ).
tcf(c_57551,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_14)),X0) = sk_c10,
inference(light_normalisation,[status(thm)],[c_57253,c_14116]) ).
tcf(c_57553,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c4)),X0) = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_57226,c_14116]) ).
tcf(c_62454,plain,
multiply(inverse(identity),multiply(inverse(sk_c8),iPr_def_15)) = sk_c9,
inference(superposition,[status(thm)],[c_108,c_57155]) ).
tcf(c_62532,plain,
multiply(identity,sk_c9) = sk_c9,
inference(light_normalisation,[status(thm)],[c_62454,c_12950,c_14157]) ).
tcf(c_67689,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( multiply(inverse(sk_c10),iPr_def_24) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_34804,c_57544]) ).
tcf(c_67690,plain,
( ( iPr_def_16 = iPr_def_26 )
| ( multiply(inverse(sk_c10),iPr_def_24) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_19762,c_57544]) ).
tcf(c_67838,plain,
( ( iPr_def_16 = iPr_def_26 )
| ( multiply(iPr_def_14,iPr_def_24) = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_67690,c_666]) ).
tcf(c_67841,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( multiply(iPr_def_14,iPr_def_24) = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_67689,c_666]) ).
tcf(c_70240,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(global_subsumption_just,[status(thm)],[c_42385,c_4186,c_33427,c_33423]) ).
tcf(c_70269,plain,
( ( sk_c10 = iPr_def_24 )
| ~ iPr_def_10
| ( identity != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_714,c_70240]) ).
tcf(c_70799,plain,
( ( sk_c10 = iPr_def_24 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_70269,c_22645,c_70269]) ).
tcf(c_75611,plain,
multiply(inverse(sk_c5),inverse(multiply(iPr_def_14,iPr_def_21))) = sk_c10,
inference(superposition,[status(thm)],[c_57549,c_57551]) ).
tcf(c_75621,plain,
( ~ iPr_def_10
| ( inverse(inverse(multiply(sk_c11,iPr_def_14))) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_57551,c_687]) ).
tcf(c_75649,plain,
multiply(iPr_def_21,inverse(inverse(iPr_def_22))) = sk_c10,
inference(light_normalisation,[status(thm)],[c_75611,c_673,c_27575]) ).
tcf(c_76099,plain,
inverse(inverse(iPr_def_22)) = multiply(sk_c5,sk_c10),
inference(superposition,[status(thm)],[c_75649,c_19783]) ).
tcf(c_76100,plain,
inverse(inverse(iPr_def_22)) = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_76099,c_20242]) ).
tcf(c_76161,plain,
( ( sk_c10 = iPr_def_24 )
| ~ iPr_def_10
| ( inverse(inverse(multiply(iPr_def_28,iPr_def_14))) != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_732,c_75621]) ).
tcf(c_78525,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(iPr_def_26,identity) = multiply(iPr_def_28,iPr_def_27) ) ),
inference(superposition,[status(thm)],[c_108,c_53023]) ).
tcf(c_78528,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(iPr_def_26,iPr_def_14) = multiply(iPr_def_28,sk_c1) ) ),
inference(superposition,[status(thm)],[c_15633,c_53023]) ).
tcf(c_80665,plain,
( ( sk_c10 = iPr_def_24 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_76161,c_70799]) ).
tcf(c_80671,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c10 = iPr_def_24 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_54528,c_80665]) ).
tcf(c_81469,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( multiply(inverse(sk_c4),iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_34804,c_57553]) ).
tcf(c_81470,plain,
( ( iPr_def_16 = iPr_def_26 )
| ( multiply(inverse(sk_c4),iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_19762,c_57553]) ).
tcf(c_81930,plain,
( ~ iPr_def_13
| ( sk_c10 != identity )
| ( multiply(identity,sk_c9) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_4350,c_14157]) ).
tcf(c_81938,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_81930,c_81470,c_81469,c_78528,c_78525,c_76100,c_76099,c_80671,c_67841,c_67838,c_57186,c_57160,c_54529,c_33570,c_33423,c_31826,c_54523,c_31315,c_54526,c_54527,c_31166,c_30932,c_28583,c_28319,c_28316,c_23426,c_23347,c_22646,c_22645,c_22630,c_22628,c_21683,c_21372,c_20913,c_20240,c_20225,c_19792,c_19702,c_18885,c_18882,c_18846,c_18842,c_18841,c_16404,c_15666,c_15635,c_14572,c_14444,c_14440,c_14283,c_14178,c_14165,c_14158,c_14136,c_14157,c_13973,c_13971,c_13963,c_12946,c_10907,c_10906,c_8369,c_62532,c_731,c_696,c_695,c_694,c_693,c_677,c_675,c_673,c_666]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP389-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n013.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 14:38:21 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 10.06/5.34 % SZS status Started for theBenchmark.p
% 10.06/5.34 % SZS status Unsatisfiable for theBenchmark.p
% 10.06/5.34
% 10.06/5.34 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.06/5.34
% 10.06/5.34 % ------ iProver source info
% 10.06/5.34
% 10.06/5.34 % git: date: 2026-07-19 20:42:38 +0200
% 10.06/5.34 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.06/5.34 % git: non_committed_changes: false
% 10.06/5.34
% 10.06/5.34 % ------ Parsing...% successful
% 10.06/5.34
% 10.06/5.34
% 10.06/5.34 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 10.06/5.34
% 10.06/5.34 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 10.06/5.34
% 10.06/5.34 % ------ Preprocessing... gs_s sp: 6 0s gs_e snvd_s sp: 0 0s snvd_e %
% 10.06/5.34
% 10.06/5.34 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 10.06/5.34 % ------ Proving...
% 10.06/5.34 % ------ Problem Properties
% 10.06/5.34
% 10.06/5.34 %
% 10.06/5.34 % clauses 77
% 10.06/5.34 % conjectures 59
% 10.06/5.34 % EPR 55
% 10.06/5.34 % Horn 22
% 10.06/5.34 % unary 18
% 10.06/5.34 % binary 54
% 10.06/5.34 % lits 143
% 10.06/5.34 % lits eq 135
% 10.06/5.34 % fd_pure 0
% 10.06/5.34 % fd_pseudo 0
% 10.06/5.34 % fd_cond 0
% 10.06/5.34 % fd_pseudo_cond 0
% 10.06/5.34 % AC symbols 0
% 10.06/5.34
% 10.06/5.34 % ------ Schedule dynamic 5 is on
% 10.06/5.34
% 10.06/5.34 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 10.06/5.34
% 10.06/5.34
% 10.06/5.34 % ------
% 10.06/5.34 % Current options:
% 10.06/5.34 % ------
% 10.06/5.34
% 10.06/5.34
% 10.06/5.34 %
% 10.06/5.34
% 10.06/5.34 % ------ Proving...
% 10.06/5.34 %
% 10.06/5.34
% 10.06/5.34 % SZS status Unsatisfiable for theBenchmark.p
% 10.06/5.34
% 10.06/5.34 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.06/5.35
% 10.06/5.35
%------------------------------------------------------------------------------