%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP380-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 : n026.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:36 PM UTC 2026
% Result : Unsatisfiable 68.49s 10.95s
% Output : CNFRefutation 68.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 29
% Syntax : Number of formulae : 283 ( 84 unt; 0 def)
% Number of atoms : 648 ( 581 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 630 ( 265 ~; 365 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 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 : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 207 ( 0 sgn 207 !; 0 ?; 167 :)
% 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_c3,sk_c11) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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(f43,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c1,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c1,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f45]) ).
fof(f49,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f49]) ).
fof(f63,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f64,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c11 = inverse(sk_c3)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_33) ).
fof(f68,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c10 = inverse(sk_c4)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_35) ).
fof(f72,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f74,plain,
( sk_c8 = inverse(sk_c5)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_37) ).
fof(f76,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f75]) ).
fof(f79,negated_conjecture,
( inverse(sk_c6) = sk_c8
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_39) ).
fof(f80,plain,
( sk_c8 = inverse(sk_c6)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f79]) ).
fof(f87,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_43) ).
fof(f88,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_44) ).
fof(f90,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f89]) ).
fof(f103,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_c10,sk_c9) != sk_c11
| inverse(sk_c11) != sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_51) ).
fof(f104,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_c11 != multiply(sk_c10,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(reorient_equations,[],[f103]) ).
fof(f105,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_c11 != multiply(sk_c10,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f104]) ).
fof(f106,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_c11 != multiply(sk_c10,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f105]) ).
fof(f107,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_c11 != multiply(sk_c10,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f106]) ).
tcf(c_103,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_104,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_118,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c1,sk_c2) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_140,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_148,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_156,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(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,[],[f107]) ).
tcf(c_617,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_156]) ).
tcf(c_618,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_156]) ).
tcf(c_619,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_156]) ).
tcf(c_620,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_156]) ).
tcf(c_621,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 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_156]) ).
tcf(c_622,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_623,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_624,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_625,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_628,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_897,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_901,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != inverse(X0) )
| ( inverse(sk_c11) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_897]) ).
tcf(c_902,plain,
! [X0: $i] :
( ( inverse(sk_c11) = inverse(X0) )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_903,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != inverse(sk_c10) )
| ( inverse(sk_c11) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_901]) ).
tcf(c_908,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_911,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_938,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_1113,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_104,c_105]) ).
tcf(c_1184,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_938]) ).
tcf(c_1208,plain,
( ( inverse(sk_c11) = inverse(multiply(sk_c5,sk_c8)) )
| ( sk_c11 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_902]) ).
tcf(c_1768,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_623,c_104]) ).
tcf(c_1769,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c10 )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_1768]) ).
tcf(c_1772,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_623,c_622]) ).
tcf(c_1773,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_623,c_624]) ).
tcf(c_1866,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(X2) )
| ( inverse(X2) != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1184]) ).
tcf(c_2065,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c10) = sk_c9 )
| ( sk_c9 != X1 )
| ( multiply(X0,sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_2066,plain,
( ( multiply(sk_c10,sk_c10) = sk_c9 )
| ( sk_c9 != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2065]) ).
tcf(c_2576,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_2578,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_2579,plain,
( ( sk_c10 = identity )
| ( identity != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2578]) ).
tcf(c_2728,plain,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_118,c_618]) ).
tcf(c_2729,plain,
( ( inverse(sk_c1) = sk_c2 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_138,c_618]) ).
tcf(c_2772,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c11) = inverse(X0) )
| ( inverse(sk_c11) != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1866]) ).
tcf(c_2799,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X0,X2) = X4 )
| ( X4 != multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_625,c_623]) ).
tcf(c_2813,plain,
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1772,c_110]) ).
tcf(c_2835,plain,
( ( sk_c10 = multiply(sk_c1,sk_c2) )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1772,c_126]) ).
tcf(c_2855,plain,
! [X0: $i] : X0 = multiply(identity,X0),
inference(resolution,[status(thm)],[c_1772,c_103]) ).
tcf(c_2857,plain,
! [X0: $i] : identity = multiply(inverse(X0),X0),
inference(resolution,[status(thm)],[c_1772,c_104]) ).
tcf(c_3262,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1113,c_103]) ).
tcf(c_3281,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(inverse(sk_c4),sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_138,c_3262]) ).
tcf(c_3332,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_3262,c_3262]) ).
tcf(c_3381,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_3472,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_3332,c_104]) ).
tcf(c_3679,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_139,c_3281]) ).
tcf(c_3773,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c1) = sk_c2 )
| ( sk_c11 != sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_3679,c_621]) ).
tcf(c_3870,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_137,c_3472]) ).
tcf(c_3871,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_107,c_3472]) ).
tcf(c_3874,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_141,c_3472]) ).
tcf(c_3875,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_111,c_3472]) ).
tcf(c_3883,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_3472,c_105]) ).
tcf(c_4009,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_3870,c_136]) ).
tcf(c_4021,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_4009,c_3472]) ).
tcf(c_4124,plain,
! [X0: $i,X1: $i] :
( ( X0 = multiply(inverse(X1),X1) )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_1768,c_1772]) ).
tcf(c_4125,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_4124]) ).
tcf(c_4143,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_3871,c_106]) ).
tcf(c_4277,plain,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_618,c_118]) ).
tcf(c_4386,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_621,c_119]) ).
tcf(c_4429,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_3874,c_140]) ).
tcf(c_4630,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c5,sk_c8) )
| ( X1 != X0 )
| ( multiply(sk_c5,sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_4969,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,X0))) = multiply(inverse(X1),identity),
inference(superposition,[status(thm)],[c_3883,c_3262]) ).
tcf(c_5825,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_5935,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = multiply(inverse(identity),identity),
inference(superposition,[status(thm)],[c_103,c_4969]) ).
tcf(c_6139,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(demodulation,[status(thm)],[c_5935,c_104]) ).
tcf(c_6142,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_137,c_6139]) ).
tcf(c_6152,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_6139,c_105]) ).
tcf(c_6160,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_6152,c_103]) ).
tcf(c_6163,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(superposition,[status(thm)],[c_104,c_6160]) ).
tcf(c_6164,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(X0,identity),
inference(superposition,[status(thm)],[c_6139,c_6160]) ).
tcf(c_6184,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_6164,c_6163]) ).
tcf(c_6226,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_104,c_617]) ).
tcf(c_6228,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6226,c_6184]) ).
tcf(c_6256,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( sk_c10 != identity )
| ( multiply(inverse(X0),sk_c9) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_619,c_6139]) ).
tcf(c_6263,plain,
( ~ iPr_def_12
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm)],[c_104,c_6256]) ).
tcf(c_6275,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_620,c_6184]) ).
tcf(c_6276,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_6275,c_6139]) ).
tcf(c_6287,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(X0) != identity )
| ( inverse(X0) != inverse(identity) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_103,c_6276]) ).
tcf(c_6303,plain,
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(sk_c10) != identity )
| ( inverse(sk_c10) != inverse(identity) )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_6287]) ).
tcf(c_6380,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_6142,c_136]) ).
tcf(c_6388,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_6380,c_6139]) ).
tcf(c_6484,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_6388,c_129]) ).
tcf(c_6485,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_6388,c_127]) ).
tcf(c_7369,plain,
( ( sk_c10 = multiply(sk_c1,sk_c2) )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_2835,c_617]) ).
tcf(c_7607,plain,
! [X0: $i] :
( ( inverse(sk_c11) = inverse(X0) )
| ( inverse(sk_c11) != inverse(multiply(sk_c5,sk_c8)) )
| ( inverse(X0) != inverse(multiply(sk_c5,sk_c8)) ) ),
inference(instantiation,[status(thm)],[c_2772]) ).
tcf(c_7608,plain,
( ( inverse(sk_c11) = inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(multiply(sk_c5,sk_c8)) )
| ( inverse(sk_c11) != inverse(multiply(sk_c5,sk_c8)) ) ),
inference(instantiation,[status(thm)],[c_7607]) ).
tcf(c_7789,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_3381]) ).
tcf(c_7790,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_7791,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c9 != sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_7789]) ).
tcf(c_8380,plain,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_4277,c_119,c_2728]) ).
tcf(c_8577,plain,
( ( sk_c10 = multiply(sk_c1,sk_c2) )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_7369,c_6228,c_6485,c_7369]) ).
tcf(c_8881,plain,
( iPr_def_13
| ( inverse(sk_c4) = sk_c10 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_4386,c_109,c_119,c_621,c_6228,c_6263,c_6484]) ).
tcf(c_8882,plain,
( iPr_def_13
| iPr_def_11
| ( inverse(sk_c4) = sk_c10 ) ),
inference(renaming,[status(thm)],[c_8881]) ).
tcf(c_10481,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(X2) )
| ( X2 != X1 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_1773,c_624]) ).
tcf(c_12140,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ~ iPr_def_10
| ( X0 != multiply(sk_c1,sk_c2) ) ),
inference(resolution,[status(thm)],[c_8577,c_623]) ).
tcf(c_12569,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1113,c_103]) ).
tcf(c_12620,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_103,c_12569]) ).
tcf(c_12622,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_105,c_12569]) ).
tcf(c_12637,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_12569,c_12569]) ).
tcf(c_12645,plain,
( ~ iPr_def_10
| ( sk_c11 != sk_c10 )
| ( inverse(inverse(identity)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_12620,c_617]) ).
tcf(c_12680,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_12637,c_104]) ).
tcf(c_12814,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_12680,c_105]) ).
tcf(c_14149,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,identity)) = inverse(X1),
inference(superposition,[status(thm)],[c_12680,c_12622]) ).
tcf(c_14223,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_12814,c_12622]) ).
tcf(c_14262,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,X0))) = inverse(X1),
inference(light_normalisation,[status(thm)],[c_14223,c_14149]) ).
tcf(c_15084,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(multiply(sk_c5,sk_c8)) )
| ( X0 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_15085,plain,
( ( inverse(sk_c10) = inverse(multiply(sk_c5,sk_c8)) )
| ( sk_c10 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_15084]) ).
tcf(c_15809,plain,
! [X0: $i] : multiply(X0,inverse(identity)) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_104,c_14262]) ).
tcf(c_17281,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X2,X0) = X1 )
| ( X2 != identity )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2855,c_2799]) ).
tcf(c_17282,plain,
( ( multiply(sk_c10,sk_c10) = sk_c10 )
| ( sk_c10 != identity )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_17281]) ).
tcf(c_17310,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_2857,c_623]) ).
tcf(c_17311,plain,
( ( identity = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_17310]) ).
tcf(c_20725,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = identity )
| ( identity != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_2578]) ).
tcf(c_20732,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != identity )
| ( inverse(X0) != identity ) ),
inference(instantiation,[status(thm)],[c_908]) ).
tcf(c_20734,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != identity )
| ( inverse(sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_20732]) ).
tcf(c_20786,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c5,sk_c8) )
| ( X0 != identity )
| ( multiply(sk_c5,sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_4630]) ).
tcf(c_20788,plain,
( ( sk_c10 = multiply(sk_c5,sk_c8) )
| ( sk_c10 != identity )
| ( multiply(sk_c5,sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_20786]) ).
tcf(c_22294,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),X0) )
| ~ iPr_def_10
| ( multiply(sk_c1,sk_c2) != identity ) ),
inference(resolution,[status(thm)],[c_12140,c_1768]) ).
tcf(c_22295,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ~ iPr_def_10
| ( multiply(sk_c1,sk_c2) != identity ) ),
inference(instantiation,[status(thm)],[c_22294]) ).
tcf(c_23986,plain,
! [X0: $i] :
( ( identity = sk_c11 )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_5825]) ).
tcf(c_25569,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_12645,c_628,c_2579,c_4021,c_6228,c_17311,c_22295]) ).
tcf(c_27024,plain,
inverse(inverse(identity)) = inverse(identity),
inference(superposition,[status(thm)],[c_15809,c_103]) ).
tcf(c_27025,plain,
inverse(inverse(inverse(inverse(identity)))) = identity,
inference(superposition,[status(thm)],[c_15809,c_104]) ).
tcf(c_27026,plain,
inverse(identity) = identity,
inference(light_normalisation,[status(thm)],[c_27025,c_27024]) ).
tcf(c_27028,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(X0,identity),
inference(demodulation,[status(thm)],[c_15809,c_27026]) ).
tcf(c_27293,plain,
! [X0: $i] : multiply(multiply(X0,identity),inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_27028,c_104]) ).
tcf(c_27300,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(demodulation,[status(thm)],[c_27293,c_103,c_105]) ).
tcf(c_27318,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_27300,c_105]) ).
tcf(c_27320,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_27300,c_105]) ).
tcf(c_27327,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_27318,c_103]) ).
tcf(c_27330,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(superposition,[status(thm)],[c_104,c_27327]) ).
tcf(c_27333,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,multiply(sk_c11,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_137,c_27327]) ).
tcf(c_27334,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,multiply(sk_c11,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_107,c_27327]) ).
tcf(c_27341,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c6,multiply(sk_c8,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_144,c_27327]) ).
tcf(c_27367,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_27028,c_27330]) ).
tcf(c_27909,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,multiply(sk_c11,inverse(sk_c10))) = identity ) ),
inference(superposition,[status(thm)],[c_136,c_27320]) ).
tcf(c_27910,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,multiply(sk_c11,inverse(sk_c10))) = identity ) ),
inference(superposition,[status(thm)],[c_106,c_27320]) ).
tcf(c_27917,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c4,multiply(sk_c10,inverse(sk_c9))) = identity ) ),
inference(superposition,[status(thm)],[c_108,c_27320]) ).
tcf(c_28237,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c6,sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_142,c_27341]) ).
tcf(c_28257,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c6,multiply(sk_c11,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_28237,c_105]) ).
tcf(c_28800,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_27909,c_27333]) ).
tcf(c_28815,plain,
( ( inverse(sk_c10) = identity )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_27910,c_27334]) ).
tcf(c_28830,plain,
inverse(sk_c11) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_27917,c_903,c_1208,c_2813,c_3875,c_4143,c_7608,c_15085,c_20734,c_20788,c_28815]) ).
tcf(c_28869,plain,
inverse(sk_c10) = sk_c11,
inference(superposition,[status(thm)],[c_28830,c_27367]) ).
tcf(c_28870,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c10,X0)) = X0,
inference(superposition,[status(thm)],[c_28830,c_27327]) ).
tcf(c_40771,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_10481,c_2857]) ).
tcf(c_40772,plain,
( ( inverse(sk_c10) = inverse(identity) )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_40771]) ).
tcf(c_42569,plain,
( ( identity = sk_c11 )
| ( identity != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_23986]) ).
tcf(c_42879,plain,
! [X0: $i] :
( ( inverse(X0) = identity )
| ( identity != sk_c11 )
| ( inverse(X0) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_20725]) ).
tcf(c_42880,plain,
( ( inverse(sk_c10) = identity )
| ( identity != sk_c11 )
| ( inverse(sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_42879]) ).
tcf(c_43721,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_911]) ).
tcf(c_43722,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_43721]) ).
tcf(c_47542,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_623]) ).
tcf(c_47543,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c11 )
| ( sk_c11 != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_47542]) ).
tcf(c_64925,plain,
inverse(sk_c1) = sk_c2,
inference(global_subsumption_just,[status(thm)],[c_28257,c_139,c_628,c_903,c_1208,c_1769,c_2579,c_2729,c_2813,c_3773,c_3875,c_4009,c_4021,c_4125,c_4143,c_4429,c_6228,c_6263,c_6303,c_7608,c_15085,c_17311,c_20734,c_20788,c_22295,c_28800,c_28815,c_40772,c_43722,c_47543]) ).
tcf(c_81562,negated_conjecture,
inverse(sk_c11) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_107,c_28830]) ).
tcf(c_81564,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c10,sk_c9) != sk_c11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_621,c_81562]) ).
tcf(c_81565,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( multiply(sk_c10,sk_c9) != sk_c11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_81564,c_25569]) ).
tcf(c_81566,negated_conjecture,
inverse(sk_c1) = sk_c2,
inference(global_subsumption_just,[status(thm)],[c_137,c_64925]) ).
tcf(c_81568,plain,
multiply(sk_c10,sk_c11) = identity,
inference(superposition,[status(thm)],[c_81562,c_104]) ).
tcf(c_81646,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_119,c_81565]) ).
tcf(c_81699,plain,
( iPr_def_13
| ( inverse(sk_c4) = sk_c10 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_81646,c_8882]) ).
tcf(c_81700,plain,
( iPr_def_13
| iPr_def_11
| ( inverse(sk_c4) = sk_c10 ) ),
inference(renaming,[status(thm)],[c_81699]) ).
tcf(c_81714,plain,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_118,c_618]) ).
tcf(c_81748,plain,
inverse(inverse(identity)) = inverse(identity),
inference(superposition,[status(thm)],[c_15809,c_103]) ).
tcf(c_81749,plain,
inverse(inverse(inverse(inverse(identity)))) = identity,
inference(superposition,[status(thm)],[c_15809,c_104]) ).
tcf(c_81754,plain,
inverse(identity) = identity,
inference(light_normalisation,[status(thm)],[c_81749,c_81748]) ).
tcf(c_81765,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(X0,identity),
inference(demodulation,[status(thm)],[c_15809,c_81754]) ).
tcf(c_81781,plain,
! [X0: $i] : multiply(multiply(X0,identity),inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_81765,c_104]) ).
tcf(c_81795,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(demodulation,[status(thm)],[c_81781,c_103,c_105]) ).
tcf(c_81800,plain,
multiply(sk_c1,sk_c2) = identity,
inference(superposition,[status(thm)],[c_81566,c_81795]) ).
tcf(c_81804,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_81795,c_105]) ).
tcf(c_81813,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_126,c_81800]) ).
tcf(c_81818,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_127,c_81800]) ).
tcf(c_81819,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_81800,c_105]) ).
tcf(c_81849,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_81818,c_81795]) ).
tcf(c_81921,plain,
sk_c10 = identity,
inference(superposition,[status(thm)],[c_81849,c_81813]) ).
tcf(c_81924,plain,
~ iPr_def_12,
inference(backward_subsumption_resolution,[status(thm)],[c_6263,c_81921]) ).
tcf(c_81925,plain,
( iPr_def_13
| iPr_def_11
| ( multiply(sk_c10,sk_c9) != sk_c11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_81565,c_81924]) ).
tcf(c_81943,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_81819,c_103]) ).
tcf(c_81947,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_149,c_81943]) ).
tcf(c_81968,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(sk_c10,X1),
inference(light_normalisation,[status(thm)],[c_81804,c_81921]) ).
tcf(c_81971,plain,
! [X0: $i] : multiply(X0,identity) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_104,c_81968]) ).
tcf(c_81975,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c10,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_81562,c_81968]) ).
tcf(c_82006,plain,
! [X0: $i] : multiply(sk_c10,X0) = X0,
inference(demodulation,[status(thm)],[c_81975,c_28870]) ).
tcf(c_82007,plain,
sk_c11 = identity,
inference(demodulation,[status(thm)],[c_81568,c_82006]) ).
tcf(c_82011,plain,
( ( sk_c11 = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_118,c_82006]) ).
tcf(c_82024,plain,
( ~ iPr_def_11
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_82006,c_618]) ).
tcf(c_82025,plain,
inverse(sk_c10) = identity,
inference(superposition,[status(thm)],[c_82006,c_81795]) ).
tcf(c_82030,plain,
( ~ iPr_def_11
| ( sk_c10 != identity )
| ( sk_c10 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_82024,c_82025]) ).
tcf(c_82031,plain,
( ~ iPr_def_11
| ( sk_c10 != sk_c9 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_82030,c_81921]) ).
tcf(c_82067,plain,
! [X0: $i] : multiply(X0,sk_c11) = X0,
inference(light_normalisation,[status(thm)],[c_81971,c_82006,c_82007]) ).
tcf(c_82082,plain,
sk_c11 = sk_c10,
inference(superposition,[status(thm)],[c_82067,c_82006]) ).
tcf(c_82118,plain,
( ( sk_c10 = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_82011,c_82082]) ).
tcf(c_82182,plain,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_81714,c_8380]) ).
tcf(c_82184,plain,
( ( multiply(sk_c10,sk_c9) = sk_c10 )
| ~ iPr_def_11 ),
inference(light_normalisation,[status(thm)],[c_82182,c_82082]) ).
tcf(c_82185,plain,
( ( sk_c10 = sk_c9 )
| ~ iPr_def_11 ),
inference(demodulation,[status(thm)],[c_82184,c_82006]) ).
tcf(c_82188,plain,
~ iPr_def_11,
inference(forward_subsumption_resolution,[status(thm)],[c_82185,c_82031]) ).
tcf(c_82189,plain,
( iPr_def_13
| ( multiply(sk_c10,sk_c9) != sk_c11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_81925,c_82188]) ).
tcf(c_82193,plain,
( iPr_def_13
| ( inverse(sk_c4) = sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_81700,c_82188]) ).
tcf(c_82195,plain,
inverse(sk_c4) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_81947,c_1769,c_2576,c_4125,c_6303,c_28869,c_40772,c_42569,c_42880,c_43722,c_47543,c_81921,c_82007,c_82193]) ).
tcf(c_82201,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm)],[c_82195,c_104]) ).
tcf(c_82213,plain,
multiply(sk_c10,sk_c4) = sk_c10,
inference(light_normalisation,[status(thm)],[c_82201,c_82007,c_82082]) ).
tcf(c_82214,plain,
sk_c10 = sk_c4,
inference(demodulation,[status(thm)],[c_82213,c_82006]) ).
tcf(c_82216,plain,
( ( sk_c10 = sk_c9 )
| ( multiply(sk_c10,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_82118,c_82214]) ).
tcf(c_82217,plain,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c10,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_148,c_82214]) ).
tcf(c_82224,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_82217,c_628,c_2066,c_7791,c_7790,c_17282,c_81921,c_82216]) ).
tcf(c_82226,plain,
sk_c10 = sk_c9,
inference(demodulation,[status(thm)],[c_82224,c_82006]) ).
tcf(c_84354,plain,
multiply(sk_c10,sk_c9) != sk_c11,
inference(global_subsumption_just,[status(thm)],[c_82189,c_1769,c_2576,c_4125,c_6303,c_28869,c_40772,c_42569,c_42880,c_43722,c_47543,c_81921,c_82007,c_82189]) ).
tcf(c_84356,plain,
$false,
inference(ground_joinability,[status(thm)],[c_84354,c_82006,c_82082,c_82226]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP380-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n026.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 14:40:09 UTC 2026
% 0.15/0.39 % CPUTime :
% 0.15/0.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/0.43 Running first-order theorem proving
% 0.15/0.43 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.15/0.44
% 0.15/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.15/0.44
% 0.15/0.44 % Detected problem language: tptp
% 0.15/0.45 % Proving...
% 68.49/10.95 % SZS status Started for theBenchmark.p
% 68.49/10.95 % SZS status Unsatisfiable for theBenchmark.p
% 68.49/10.95
% 68.49/10.95 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 68.49/10.95
% 68.49/10.95 % ------ iProver source info
% 68.49/10.95
% 68.49/10.95 % git: date: 2026-07-19 20:42:38 +0200
% 68.49/10.95 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 68.49/10.95 % git: non_committed_changes: false
% 68.49/10.95
% 68.49/10.95 % ------ Parsing...% successful
% 68.49/10.95
% 68.49/10.95
% 68.49/10.95 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 68.49/10.95
% 68.49/10.95 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 68.49/10.95
% 68.49/10.95 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 68.49/10.95
% 68.49/10.95 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 68.49/10.95 % ------ Proving...
% 68.49/10.95 % ------ Problem Properties
% 68.49/10.95
% 68.49/10.95 %
% 68.49/10.95 % clauses 58
% 68.49/10.95 % conjectures 55
% 68.49/10.95 % EPR 0
% 68.49/10.95 % Horn 7
% 68.49/10.95 % unary 3
% 68.49/10.95 % binary 50
% 68.49/10.95 % lits 123
% 68.49/10.95 % lits eq 115
% 68.49/10.95 % fd_pure 0
% 68.49/10.95 % fd_pseudo 0
% 68.49/10.95 % fd_cond 0
% 68.49/10.95 % fd_pseudo_cond 0
% 68.49/10.95 % AC symbols 0
% 68.49/10.95
% 68.49/10.95 % ------ Input Options Time Limit: Unbounded
% 68.49/10.95
% 68.49/10.95
% 68.49/10.95 % ------
% 68.49/10.95 % Current options:
% 68.49/10.95 % ------
% 68.49/10.95
% 68.49/10.95
% 68.49/10.95 %
% 68.49/10.95
% 68.49/10.95 % ------ Proving...
% 68.49/10.95 %
% 68.49/10.95
% 68.49/10.95 % SZS status Unsatisfiable for theBenchmark.p
% 68.49/10.95
% 68.49/10.95 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 68.49/10.95
% 68.49/10.95
%------------------------------------------------------------------------------