%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP384-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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:33:37 PM UTC 2026
% Result : Unsatisfiable 54.29s 8.88s
% Output : CNFRefutation 54.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 26
% Syntax : Number of formulae : 278 ( 81 unt; 0 def)
% Number of atoms : 667 ( 609 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 693 ( 304 ~; 389 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 199 ( 0 sgn 199 !; 0 ?; 159 :)
% 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_c3,sk_c11) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c3)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c10 = inverse(sk_c4)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c8 = inverse(sk_c5)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f14]) ).
fof(f27,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c10,sk_c9) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f28,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c11 = multiply(sk_c10,sk_c9) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c10,sk_c9) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = multiply(sk_c10,sk_c9) ),
inference(reorient_equations,[],[f29]) ).
fof(f49,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f49]) ).
fof(f63,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c1,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f64,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c1,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f65]) ).
fof(f69,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f69]) ).
fof(f77,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c1,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_38) ).
fof(f78,plain,
( inverse(sk_c7) = sk_c6
| sk_c10 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f77]) ).
fof(f81,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c1,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_40) ).
fof(f82,plain,
( sk_c6 = multiply(sk_c7,sk_c8)
| sk_c10 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f84,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f86,plain,
( sk_c11 = inverse(sk_c3)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f85]) ).
fof(f97,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f98,plain,
( inverse(sk_c7) = sk_c6
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f97]) ).
fof(f99,negated_conjecture,
( inverse(sk_c6) = sk_c8
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_49) ).
fof(f100,plain,
( sk_c8 = inverse(sk_c6)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f99]) ).
fof(f123,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| multiply(X5,sk_c10) != sk_c11
| inverse(X4) != X5
| multiply(X4,X5) != sk_c11
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != sk_c9
| inverse(X2) != sk_c11
| multiply(X2,sk_c11) != sk_c10
| multiply(X1,sk_c9) != sk_c10
| inverse(X0) != X1
| multiply(X0,X1) != sk_c10
| multiply(sk_c11,sk_c9) != sk_c10
| multiply(sk_c10,sk_c9) != sk_c11
| inverse(sk_c11) != sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_61) ).
fof(f124,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c10 != multiply(X1,sk_c9)
| inverse(X0) != X1
| multiply(X0,X1) != sk_c10
| sk_c10 != multiply(sk_c11,sk_c9)
| sk_c11 != multiply(sk_c10,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(reorient_equations,[],[f123]) ).
fof(f125,plain,
! [X2,X3,X0,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c10 != multiply(inverse(X0),sk_c9)
| sk_c10 != multiply(X0,inverse(X0))
| sk_c10 != multiply(sk_c11,sk_c9)
| sk_c11 != multiply(sk_c10,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f124]) ).
fof(f126,plain,
! [X2,X3,X0,X6,X7,X4] :
( multiply(X6,inverse(X4)) != X7
| inverse(X4) != inverse(X7)
| inverse(X6) != X7
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c10 != multiply(inverse(X0),sk_c9)
| sk_c10 != multiply(X0,inverse(X0))
| sk_c10 != multiply(sk_c11,sk_c9)
| sk_c11 != multiply(sk_c10,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f125]) ).
fof(f127,plain,
! [X2,X3,X0,X6,X4] :
( inverse(X6) != multiply(X6,inverse(X4))
| inverse(X4) != inverse(inverse(X6))
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c10 != multiply(inverse(X0),sk_c9)
| sk_c10 != multiply(X0,inverse(X0))
| sk_c10 != multiply(sk_c11,sk_c9)
| sk_c11 != multiply(sk_c10,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f126]) ).
tcf(c_113,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_114,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_118,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_120,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_128,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_146,negated_conjecture,
( ( multiply(sk_c1,sk_c2) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_153,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_155,negated_conjecture,
( ( multiply(sk_c1,sk_c2) = sk_c10 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_156,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_163,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_164,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_176,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c11) != sk_c10 )
| ( inverse(X4) != sk_c10 )
| ( inverse(X2) != sk_c11 )
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 )
| ( multiply(X4,sk_c10) != sk_c9 )
| ( multiply(X2,sk_c11) != sk_c10 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X3),sk_c9) != sk_c10 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X3,inverse(X3)) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_721,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_176]) ).
tcf(c_722,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_176]) ).
tcf(c_723,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( multiply(inverse(X0),sk_c9) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_176]) ).
tcf(c_724,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_176]) ).
tcf(c_725,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_176]) ).
tcf(c_726,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_727,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_728,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_729,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_730,plain,
( ( inverse(sk_c10) = inverse(sk_c10) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_732,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_1043,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1047,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != inverse(X0) )
| ( inverse(sk_c11) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1043]) ).
tcf(c_1048,plain,
! [X0: $i] :
( ( inverse(sk_c11) = inverse(X0) )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_1049,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != inverse(sk_c10) )
| ( inverse(sk_c11) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1047]) ).
tcf(c_1050,plain,
( ( inverse(sk_c11) = inverse(sk_c10) )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1048]) ).
tcf(c_1051,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c11) )
| ( sk_c10 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1052,plain,
( ( sk_c10 = inverse(sk_c11) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1051]) ).
tcf(c_1054,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1057,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1069,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != sk_c11 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1057]) ).
tcf(c_1070,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_1079,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1083,plain,
multiply(identity,inverse(sk_c11)) = inverse(sk_c11),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_1087,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c11) )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_1089,plain,
( ( inverse(sk_c10) = inverse(sk_c11) )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1087]) ).
tcf(c_1106,plain,
( ( sk_c11 = multiply(identity,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1069]) ).
tcf(c_1107,plain,
multiply(identity,sk_c11) = sk_c11,
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_1175,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1079]) ).
tcf(c_1275,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_114,c_115]) ).
tcf(c_1490,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,inverse(sk_c11)) )
| ( X1 != X0 )
| ( multiply(identity,inverse(sk_c11)) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1633,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != inverse(sk_c11) )
| ( inverse(X0) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1175]) ).
tcf(c_1634,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != inverse(sk_c11) )
| ( inverse(sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1633]) ).
tcf(c_1637,plain,
! [X0: $i] :
( ( inverse(X0) = multiply(identity,inverse(sk_c11)) )
| ( inverse(X0) != inverse(sk_c11) )
| ( multiply(identity,inverse(sk_c11)) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1175]) ).
tcf(c_1638,plain,
( ( inverse(sk_c10) = multiply(identity,inverse(sk_c11)) )
| ( inverse(sk_c10) != inverse(sk_c11) )
| ( multiply(identity,inverse(sk_c11)) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1637]) ).
tcf(c_2172,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_725,c_129]) ).
tcf(c_2439,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_727,c_114]) ).
tcf(c_2443,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_727,c_726]) ).
tcf(c_2792,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,inverse(sk_c11)) = X1 )
| ( X1 != X0 )
| ( multiply(identity,inverse(sk_c11)) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_2967,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,sk_c11) )
| ( X1 != sk_c11 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_729]) ).
tcf(c_3050,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_3052,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_3053,plain,
( ( sk_c10 = identity )
| ( identity != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3052]) ).
tcf(c_3816,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1275,c_113]) ).
tcf(c_3899,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_3816,c_3816]) ).
tcf(c_4088,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_3899,c_114]) ).
tcf(c_4217,plain,
( ( sk_c10 = multiply(sk_c1,sk_c2) )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2443,c_146]) ).
tcf(c_4240,plain,
! [X0: $i] : identity = multiply(inverse(X0),X0),
inference(resolution,[status(thm)],[c_2443,c_114]) ).
tcf(c_4399,plain,
! [X0: $i] :
( ( identity = sk_c10 )
| ( identity != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_4486,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_157,c_4088]) ).
tcf(c_4487,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_117,c_4088]) ).
tcf(c_4491,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_121,c_4088]) ).
tcf(c_4499,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_4088,c_115]) ).
tcf(c_4665,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_4486,c_156]) ).
tcf(c_4711,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_4665,c_4088]) ).
tcf(c_4834,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_4487,c_116]) ).
tcf(c_5073,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_4491,c_120]) ).
tcf(c_5329,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,X0))) = multiply(inverse(X1),identity),
inference(superposition,[status(thm)],[c_4499,c_3816]) ).
tcf(c_6317,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = multiply(inverse(identity),identity),
inference(superposition,[status(thm)],[c_113,c_5329]) ).
tcf(c_6602,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(demodulation,[status(thm)],[c_6317,c_114]) ).
tcf(c_6605,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_157,c_6602]) ).
tcf(c_6615,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_6602,c_115]) ).
tcf(c_6635,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_6615,c_113]) ).
tcf(c_6638,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(superposition,[status(thm)],[c_114,c_6635]) ).
tcf(c_6639,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(X0,identity),
inference(superposition,[status(thm)],[c_6602,c_6635]) ).
tcf(c_6662,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_6639,c_6638]) ).
tcf(c_6713,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_114,c_721]) ).
tcf(c_6715,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6713,c_6662]) ).
tcf(c_6733,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( sk_c10 != identity )
| ( multiply(inverse(X0),sk_c9) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_723,c_6602]) ).
tcf(c_6740,plain,
( ~ iPr_def_12
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm)],[c_114,c_6733]) ).
tcf(c_6764,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(light_normalisation,[status(thm)],[c_724,c_6662]) ).
tcf(c_6765,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_6764,c_6602]) ).
tcf(c_6779,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(X0) != identity )
| ( inverse(X0) != X0 )
| ( multiply(inverse(X0),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_6602,c_6765]) ).
tcf(c_6791,plain,
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(sk_c10) != identity )
| ( inverse(sk_c10) != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_6779]) ).
tcf(c_6867,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_6605,c_156]) ).
tcf(c_6875,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_6867,c_6602]) ).
tcf(c_7015,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_6875,c_149]) ).
tcf(c_7016,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_6875,c_147]) ).
tcf(c_7792,plain,
! [X0: $i] :
( ( multiply(identity,inverse(sk_c11)) = X0 )
| ( X0 != inverse(sk_c11) )
| ( multiply(identity,inverse(sk_c11)) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_2792]) ).
tcf(c_7793,plain,
( ( multiply(identity,inverse(sk_c11)) = sk_c10 )
| ( sk_c10 != inverse(sk_c11) )
| ( multiply(identity,inverse(sk_c11)) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_7792]) ).
tcf(c_8066,plain,
! [X0: $i] :
( ( multiply(X0,sk_c11) = multiply(identity,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_2967]) ).
tcf(c_8067,plain,
( ( multiply(sk_c10,sk_c11) = multiply(identity,sk_c11) )
| ( sk_c10 != identity )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_8066]) ).
tcf(c_8341,plain,
( ( sk_c10 = multiply(sk_c1,sk_c2) )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_4217,c_721]) ).
tcf(c_9596,plain,
( ( sk_c10 = multiply(sk_c1,sk_c2) )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_8341,c_6715,c_7016,c_8341]) ).
tcf(c_10520,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != multiply(identity,inverse(sk_c11)) )
| ( X0 != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_3052]) ).
tcf(c_11543,plain,
! [X0: $i] :
( ( identity = multiply(identity,inverse(sk_c11)) )
| ( identity != X0 )
| ( multiply(identity,inverse(sk_c11)) != X0 ) ),
inference(instantiation,[status(thm)],[c_1490]) ).
tcf(c_11544,plain,
( ( identity = multiply(identity,inverse(sk_c11)) )
| ( identity != sk_c10 )
| ( multiply(identity,inverse(sk_c11)) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_11543]) ).
tcf(c_13403,plain,
( iPr_def_13
| ( inverse(sk_c4) = sk_c10 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_2172,c_119,c_139,c_2172,c_6715,c_6740,c_7015]) ).
tcf(c_13404,plain,
( iPr_def_13
| iPr_def_11
| ( inverse(sk_c4) = sk_c10 ) ),
inference(renaming,[status(thm)],[c_13403]) ).
tcf(c_14212,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1275,c_113]) ).
tcf(c_14273,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_113,c_14212]) ).
tcf(c_14274,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_14212]) ).
tcf(c_14275,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_115,c_14212]) ).
tcf(c_14285,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_14212,c_14212]) ).
tcf(c_14291,plain,
( ~ iPr_def_10
| ( sk_c11 != sk_c10 )
| ( inverse(inverse(identity)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_14273,c_721]) ).
tcf(c_14305,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_14274,c_14285]) ).
tcf(c_14320,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_14285,c_114]) ).
tcf(c_14336,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(X0,identity),
inference(superposition,[status(thm)],[c_14305,c_14285]) ).
tcf(c_14337,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_14336,c_14305]) ).
tcf(c_14349,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_163,c_14337]) ).
tcf(c_14468,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_14320,c_115]) ).
tcf(c_14481,plain,
( ( sk_c8 = sk_c7 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_14349,c_164]) ).
tcf(c_14498,plain,
( ( sk_c8 = sk_c7 )
| ( multiply(sk_c1,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_14481,c_14320]) ).
tcf(c_14588,plain,
( ( sk_c8 = sk_c7 )
| ( sk_c10 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_14498,c_147]) ).
tcf(c_15949,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( sk_c10 = identity ) ),
inference(global_subsumption_just,[status(thm)],[c_14588,c_7016]) ).
tcf(c_15950,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(renaming,[status(thm)],[c_15949]) ).
tcf(c_15959,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_15950,c_14320]) ).
tcf(c_16363,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,identity)) = inverse(X1),
inference(superposition,[status(thm)],[c_14320,c_14275]) ).
tcf(c_16452,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,identity)) = multiply(X2,inverse(multiply(X1,X2))),
inference(superposition,[status(thm)],[c_14468,c_14275]) ).
tcf(c_16509,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,X0))) = inverse(X1),
inference(light_normalisation,[status(thm)],[c_16452,c_16363]) ).
tcf(c_17647,plain,
( ( identity = sk_c10 )
| ( identity != identity )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_4399]) ).
tcf(c_18556,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_15959,c_146]) ).
tcf(c_18642,plain,
! [X0: $i] : multiply(X0,inverse(identity)) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_114,c_16509]) ).
tcf(c_19561,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_4240,c_727]) ).
tcf(c_19562,plain,
( ( identity = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_19561]) ).
tcf(c_19764,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ~ iPr_def_10
| ( X0 != multiply(sk_c1,sk_c2) ) ),
inference(resolution,[status(thm)],[c_9596,c_727]) ).
tcf(c_20991,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != identity )
| ( inverse(X0) != identity ) ),
inference(instantiation,[status(thm)],[c_1054]) ).
tcf(c_20993,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != identity )
| ( inverse(sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_20991]) ).
tcf(c_20997,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_3052]) ).
tcf(c_21004,plain,
( ( sk_c11 = identity )
| ( identity != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_20997]) ).
tcf(c_25150,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),X0) )
| ~ iPr_def_10
| ( multiply(sk_c1,sk_c2) != identity ) ),
inference(resolution,[status(thm)],[c_19764,c_2439]) ).
tcf(c_25151,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ~ iPr_def_10
| ( multiply(sk_c1,sk_c2) != identity ) ),
inference(instantiation,[status(thm)],[c_25150]) ).
tcf(c_26876,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1057]) ).
tcf(c_26877,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_26876]) ).
tcf(c_28285,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_14291,c_732,c_3053,c_4711,c_6715,c_19562,c_25151]) ).
tcf(c_28789,plain,
inverse(inverse(identity)) = inverse(identity),
inference(superposition,[status(thm)],[c_18642,c_113]) ).
tcf(c_28790,plain,
inverse(inverse(inverse(inverse(identity)))) = identity,
inference(superposition,[status(thm)],[c_18642,c_114]) ).
tcf(c_28791,plain,
inverse(identity) = identity,
inference(light_normalisation,[status(thm)],[c_28790,c_28789]) ).
tcf(c_28793,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(X0,identity),
inference(demodulation,[status(thm)],[c_18642,c_28791]) ).
tcf(c_28989,plain,
! [X0: $i] : multiply(multiply(X0,identity),inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_28793,c_114]) ).
tcf(c_28991,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(demodulation,[status(thm)],[c_28989,c_113,c_115]) ).
tcf(c_28994,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_157,c_28991]) ).
tcf(c_29006,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_28991,c_115]) ).
tcf(c_29008,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_28991,c_115]) ).
tcf(c_29011,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_29006,c_113]) ).
tcf(c_29014,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(superposition,[status(thm)],[c_114,c_29011]) ).
tcf(c_29018,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,multiply(sk_c11,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_117,c_29011]) ).
tcf(c_29036,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_28793,c_29014]) ).
tcf(c_29045,negated_conjecture,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_721,c_732,c_3053,c_4711,c_6715,c_19562,c_25151]) ).
tcf(c_29047,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_725,c_29045]) ).
tcf(c_29303,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_28994,c_156]) ).
tcf(c_29310,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_29303,c_28991]) ).
tcf(c_29522,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_29310,c_153]) ).
tcf(c_29540,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_29522,c_29036]) ).
tcf(c_29610,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(sk_c6,multiply(sk_c7,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_29540,c_29011]) ).
tcf(c_29699,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,multiply(sk_c11,inverse(sk_c10))) = identity ) ),
inference(superposition,[status(thm)],[c_116,c_29008]) ).
tcf(c_29707,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c4,multiply(sk_c10,inverse(sk_c9))) = identity ) ),
inference(superposition,[status(thm)],[c_118,c_29008]) ).
tcf(c_30667,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c2) = sk_c10 )
| ( multiply(sk_c6,sk_c6) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_155,c_29610]) ).
tcf(c_30898,plain,
( ( inverse(sk_c10) = identity )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_29699,c_29018]) ).
tcf(c_30916,plain,
inverse(sk_c11) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_29707,c_1049,c_1050,c_4834,c_5073,c_20993,c_26877,c_30898]) ).
tcf(c_30948,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_29047,c_30916]) ).
tcf(c_30953,plain,
multiply(sk_c10,sk_c11) = identity,
inference(superposition,[status(thm)],[c_30916,c_114]) ).
tcf(c_31000,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c11,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_30953,c_115]) ).
tcf(c_31021,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c11,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_31000,c_113]) ).
tcf(c_31028,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_139,c_31021]) ).
tcf(c_31162,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_11
| ( inverse(sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_31028,c_722]) ).
tcf(c_44947,plain,
! [X0: $i] :
( ( inverse(X0) = identity )
| ( identity != multiply(identity,inverse(sk_c11)) )
| ( inverse(X0) != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_10520]) ).
tcf(c_44950,plain,
( ( inverse(sk_c10) = identity )
| ( identity != multiply(identity,inverse(sk_c11)) )
| ( inverse(sk_c10) != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_44947]) ).
tcf(c_57587,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_57590,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_57602,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_57613,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( X0 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_57590]) ).
tcf(c_57682,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(X0,X1) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_57613]) ).
tcf(c_57694,plain,
! [X0: $i] : multiply(inverse(X0),multiply(X0,sk_c11)) = multiply(identity,sk_c11),
inference(instantiation,[status(thm)],[c_1275]) ).
tcf(c_57696,plain,
multiply(inverse(sk_c10),multiply(sk_c10,sk_c11)) = multiply(identity,sk_c11),
inference(instantiation,[status(thm)],[c_57694]) ).
tcf(c_57806,plain,
! [X0: $i] :
( ( sk_c11 = multiply(inverse(X0),multiply(X0,sk_c11)) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(inverse(X0),multiply(X0,sk_c11)) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_57682]) ).
tcf(c_57807,plain,
( ( sk_c11 = multiply(inverse(sk_c10),multiply(sk_c10,sk_c11)) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(inverse(sk_c10),multiply(sk_c10,sk_c11)) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_57806]) ).
tcf(c_58029,plain,
! [X0: $i] :
( ( sk_c11 = multiply(X0,sk_c11) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(X0,sk_c11) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_57682]) ).
tcf(c_58030,plain,
( ( sk_c11 = multiply(sk_c10,sk_c11) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(sk_c10,sk_c11) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_58029]) ).
tcf(c_58110,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(inverse(X1),multiply(X1,sk_c11)) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(X1),multiply(X1,sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_57587]) ).
tcf(c_58111,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(inverse(sk_c10),multiply(sk_c10,sk_c11)) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(sk_c10),multiply(sk_c10,sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_58110]) ).
tcf(c_58506,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(inverse(X1),multiply(X1,sk_c11)) )
| ( sk_c10 != multiply(X1,sk_c11) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_729]) ).
tcf(c_58507,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(sk_c10),multiply(sk_c10,sk_c11)) )
| ( sk_c10 != multiply(sk_c10,sk_c11) )
| ( inverse(sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_58506]) ).
tcf(c_59213,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != multiply(X1,sk_c11) )
| ( X0 != multiply(X1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_57602]) ).
tcf(c_59214,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != multiply(X1,sk_c11) )
| ( X0 != multiply(X1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_57590]) ).
tcf(c_59217,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c11) )
| ( sk_c11 != multiply(sk_c10,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_59214]) ).
tcf(c_59218,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != multiply(sk_c10,sk_c11) )
| ( sk_c11 != multiply(sk_c10,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_59213]) ).
tcf(c_61158,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,sk_c11) )
| ( X2 != X1 )
| ( multiply(X0,sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_61159,plain,
( ( sk_c10 = multiply(sk_c10,sk_c11) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c10,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_61158]) ).
tcf(c_86791,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c2) = sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_30667,c_18556]) ).
tcf(c_86800,plain,
sk_c10 = identity,
inference(superposition,[status(thm)],[c_86791,c_29310]) ).
tcf(c_86809,plain,
~ iPr_def_12,
inference(backward_subsumption_resolution,[status(thm)],[c_6740,c_86800]) ).
tcf(c_97823,negated_conjecture,
inverse(sk_c11) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_117,c_30916]) ).
tcf(c_97825,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_725,c_97823]) ).
tcf(c_97830,plain,
! [X0: $i] : multiply(sk_c10,X0) = X0,
inference(light_normalisation,[status(thm)],[c_113,c_86800]) ).
tcf(c_97831,plain,
! [X0: $i] : multiply(inverse(X0),X0) = sk_c10,
inference(light_normalisation,[status(thm)],[c_114,c_86800]) ).
tcf(c_97832,plain,
multiply(sk_c10,sk_c11) = sk_c10,
inference(superposition,[status(thm)],[c_97823,c_97831]) ).
tcf(c_97842,plain,
~ iPr_def_12,
inference(backward_subsumption_resolution,[status(thm)],[c_6740,c_86800]) ).
tcf(c_97843,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_97825,c_97842]) ).
tcf(c_97847,negated_conjecture,
inverse(sk_c4) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_129,c_730,c_732,c_1049,c_1050,c_1052,c_1070,c_1083,c_1089,c_1106,c_1107,c_1634,c_1638,c_3050,c_4834,c_5073,c_6791,c_7793,c_8067,c_11544,c_13404,c_17647,c_20993,c_21004,c_26877,c_30898,c_31162,c_44950,c_57696,c_57807,c_58030,c_58111,c_58507,c_59217,c_59218,c_61159,c_86800,c_97832]) ).
tcf(c_97849,plain,
multiply(sk_c10,sk_c4) = sk_c10,
inference(superposition,[status(thm)],[c_97847,c_97831]) ).
tcf(c_97863,plain,
! [X0: $i] : multiply(X0,inverse(sk_c10)) = inverse(inverse(X0)),
inference(light_normalisation,[status(thm)],[c_18642,c_86800]) ).
tcf(c_97866,plain,
inverse(inverse(inverse(inverse(sk_c10)))) = sk_c10,
inference(superposition,[status(thm)],[c_97863,c_97831]) ).
tcf(c_97867,plain,
inverse(inverse(sk_c10)) = inverse(sk_c10),
inference(superposition,[status(thm)],[c_97863,c_97830]) ).
tcf(c_97868,plain,
inverse(sk_c10) = sk_c10,
inference(light_normalisation,[status(thm)],[c_97866,c_97867]) ).
tcf(c_97875,plain,
( ( sk_c11 = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_128,c_97830]) ).
tcf(c_97976,negated_conjecture,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_721,c_28285]) ).
tcf(c_97978,plain,
( iPr_def_13
| iPr_def_11
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_97843,c_97976]) ).
tcf(c_97979,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm)],[c_97832,c_97830]) ).
tcf(c_97995,plain,
( ( sk_c10 = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_97875,c_97979]) ).
tcf(c_98014,plain,
( ( multiply(sk_c11,sk_c9) != sk_c10 )
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_97978,c_730,c_732,c_1049,c_1050,c_1052,c_1070,c_1083,c_1089,c_1106,c_1107,c_1634,c_1638,c_3050,c_4834,c_5073,c_6791,c_7793,c_8067,c_11544,c_17647,c_20993,c_21004,c_26877,c_30898,c_30948,c_44950,c_57696,c_57807,c_58030,c_58111,c_58507,c_59217,c_59218,c_61159,c_86809,c_86800,c_97832]) ).
tcf(c_98015,plain,
( iPr_def_11
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(renaming,[status(thm)],[c_98014]) ).
tcf(c_98016,plain,
( iPr_def_11
| ( multiply(sk_c10,sk_c9) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_98015,c_97979]) ).
tcf(c_98017,plain,
( iPr_def_11
| ( sk_c10 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_98016,c_97830]) ).
tcf(c_98032,plain,
( ~ iPr_def_11
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_97830,c_722]) ).
tcf(c_98033,plain,
( ~ iPr_def_11
| ( sk_c10 != sk_c9 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_98032,c_97868]) ).
tcf(c_98041,plain,
sk_c10 = sk_c4,
inference(demodulation,[status(thm)],[c_97849,c_97830]) ).
tcf(c_98070,plain,
sk_c10 != sk_c9,
inference(forward_subsumption_resolution,[status(thm)],[c_98033,c_98017]) ).
tcf(c_98072,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(backward_subsumption_resolution,[status(thm)],[c_97995,c_98070]) ).
tcf(c_99242,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(light_normalisation,[status(thm)],[c_98072,c_98041]) ).
tcf(c_99243,plain,
sk_c10 = sk_c9,
inference(demodulation,[status(thm)],[c_99242,c_97830]) ).
tcf(c_99244,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_99243,c_98070]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP384-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/0.36 % Computer : n005.cluster.edu
% 0.04/0.36 % Model : x86_64 x86_64
% 0.04/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.36 % Memory : 8046.5625MB
% 0.04/0.36 % OS : Linux 6.8.0-71-generic
% 0.04/0.36 % CPULimit : 300
% 0.04/0.36 % WCLimit : 300
% 0.04/0.36 % DateTime : Wed Sep 23 14:38:02 UTC 2026
% 0.04/0.37 % CPUTime :
% 0.04/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/0.40 Running first-order theorem proving
% 0.04/0.40 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.04/0.42
% 0.04/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.04/0.42
% 0.04/0.42 % Detected problem language: tptp
% 0.04/0.43 % Proving...
% 54.29/8.88 % SZS status Started for theBenchmark.p
% 54.29/8.88 % SZS status Unsatisfiable for theBenchmark.p
% 54.29/8.88
% 54.29/8.88 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 54.29/8.88
% 54.29/8.88 % ------ iProver source info
% 54.29/8.88
% 54.29/8.88 % git: date: 2026-07-19 20:42:38 +0200
% 54.29/8.88 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 54.29/8.88 % git: non_committed_changes: false
% 54.29/8.88
% 54.29/8.88 % ------ Parsing...% successful
% 54.29/8.88
% 54.29/8.88
% 54.29/8.88 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 54.29/8.88
% 54.29/8.88 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 54.29/8.88
% 54.29/8.88 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 54.29/8.88
% 54.29/8.88 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 54.29/8.88 % ------ Proving...
% 54.29/8.88 % ------ Problem Properties
% 54.29/8.88
% 54.29/8.88 %
% 54.29/8.88 % clauses 68
% 54.29/8.88 % conjectures 65
% 54.29/8.88 % EPR 0
% 54.29/8.88 % Horn 7
% 54.29/8.88 % unary 3
% 54.29/8.88 % binary 60
% 54.29/8.88 % lits 144
% 54.29/8.88 % lits eq 136
% 54.29/8.88 % fd_pure 0
% 54.29/8.88 % fd_pseudo 0
% 54.29/8.88 % fd_cond 0
% 54.29/8.88 % fd_pseudo_cond 0
% 54.29/8.88 % AC symbols 0
% 54.29/8.88
% 54.29/8.88 % ------ Input Options Time Limit: Unbounded
% 54.29/8.88
% 54.29/8.88
% 54.29/8.88 % ------
% 54.29/8.88 % Current options:
% 54.29/8.88 % ------
% 54.29/8.88
% 54.29/8.88
% 54.29/8.88 %
% 54.29/8.88
% 54.29/8.88 % ------ Proving...
% 54.29/8.88 %
% 54.29/8.88
% 54.29/8.88 % SZS status Unsatisfiable for theBenchmark.p
% 54.29/8.88
% 54.29/8.88 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 54.29/8.88
% 54.29/8.88
%------------------------------------------------------------------------------