%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP271-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 : n002.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:32:40 PM UTC 2026
% Result : Unsatisfiable 43.26s 17.04s
% Output : CNFRefutation 43.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 36
% Syntax : Number of formulae : 489 ( 86 unt; 0 def)
% Number of atoms : 1157 (1102 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 1142 ( 474 ~; 668 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 3 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 337 ( 0 sgn 337 !; 0 ?; 302 :)
% 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
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c3)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f12,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c8 = inverse(sk_c5)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f14]) ).
fof(f18,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,negated_conjecture,
( inverse(sk_c6) = sk_c8
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f20,plain,
( sk_c8 = inverse(sk_c6)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f19]) ).
fof(f23,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f24,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f28,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f27]) ).
fof(f31,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f32,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f34,plain,
( sk_c8 = inverse(sk_c5)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f36,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f35]) ).
fof(f37,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f38,plain,
( inverse(sk_c7) = sk_c6
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( inverse(sk_c6) = sk_c8
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f40,plain,
( sk_c8 = inverse(sk_c6)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f39]) ).
fof(f45,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f48,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f47]) ).
fof(f51,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f52,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f54,plain,
( sk_c8 = inverse(sk_c5)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f53]) ).
fof(f57,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f58,plain,
( inverse(sk_c7) = sk_c6
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( inverse(sk_c6) = sk_c8
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f60,plain,
( sk_c8 = inverse(sk_c6)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f59]) ).
fof(f67,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f68,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c10 = inverse(sk_c4)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f72,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f71]) ).
fof(f83,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f84,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f86,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f88,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f90,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = inverse(sk_c2) ),
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
| inverse(X1) != sk_c10
| multiply(X1,sk_c10) != sk_c9
| multiply(sk_c11,sk_c9) != sk_c10
| inverse(X0) != sk_c11
| multiply(X0,sk_c11) != sk_c10 ),
file('/export/starexec/sandbox/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 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| sk_c10 != multiply(sk_c11,sk_c9)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(reorient_equations,[],[f103]) ).
fof(f105,plain,
! [X2,X3,X0,X1,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 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| sk_c10 != multiply(sk_c11,sk_c9)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(equality_resolution,[],[f104]) ).
fof(f106,plain,
! [X2,X3,X0,X1,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 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| sk_c10 != multiply(sk_c11,sk_c9)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(equality_resolution,[],[f105]) ).
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,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_108,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_110,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_118,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_120,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c6) = sk_c8 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_128,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_138,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_140,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_148,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_156,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(X5) != sk_c10 )
| ( inverse(X4) != sk_c10 )
| ( inverse(X3) != sk_c11 )
| ( inverse(X2) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(X5,sk_c10) != sk_c9 )
| ( multiply(X4,sk_c10) != sk_c9 )
| ( multiply(X3,sk_c11) != sk_c10 )
| ( multiply(X2,sk_c11) != sk_c10 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_157,plain,
multiply(identity,sk_c10) = sk_c10,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_158,plain,
multiply(inverse(sk_c10),sk_c10) = identity,
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_621,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_156]) ).
tcf(c_622,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_156]) ).
tcf(c_623,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ( 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_12])],[c_156]) ).
tcf(c_624,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_156]) ).
tcf(c_625,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_626,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_627,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,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_630,plain,
( ( inverse(sk_c10) = inverse(sk_c10) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_631,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_889,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( sk_c10 != X0 )
| ( multiply(sk_c11,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_893,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( sk_c10 != multiply(X0,X1) )
| ( multiply(sk_c11,sk_c9) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_889]) ).
tcf(c_894,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c9) = multiply(X0,X1) )
| ( sk_c9 != X1 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_627]) ).
tcf(c_895,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c11,sk_c9) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_893]) ).
tcf(c_896,plain,
( ( multiply(sk_c11,sk_c9) = multiply(sk_c10,sk_c10) )
| ( sk_c9 != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_894]) ).
tcf(c_906,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_909,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_911,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_919,plain,
multiply(identity,multiply(sk_c11,sk_c9)) = multiply(sk_c11,sk_c9),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_928,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_932,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_911]) ).
tcf(c_933,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c9 != sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_932]) ).
tcf(c_939,plain,
! [X0: $i] :
( ( sk_c10 = multiply(identity,X0) )
| ( sk_c10 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_906]) ).
tcf(c_940,plain,
( ( sk_c10 = multiply(identity,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_939]) ).
tcf(c_941,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),X0) )
| ( sk_c10 != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_906]) ).
tcf(c_946,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_947,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_906]) ).
tcf(c_950,plain,
! [X0: $i] :
( ( sk_c10 = sk_c9 )
| ( sk_c9 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_952,plain,
! [X0: $i] :
( ( sk_c10 = sk_c11 )
| ( sk_c10 != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_985,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != sk_c11 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_986,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_993,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_1052,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_127,c_624]) ).
tcf(c_1054,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c10) = X0 )
| ( X0 != sk_c9 )
| ( multiply(sk_c4,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_946]) ).
tcf(c_1055,plain,
( ( multiply(sk_c4,sk_c10) = sk_c10 )
| ( sk_c10 != sk_c9 )
| ( multiply(sk_c4,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1054]) ).
tcf(c_1062,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = X1 )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_946]) ).
tcf(c_1063,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),X0) = X1 )
| ( X1 != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_946]) ).
tcf(c_1067,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = X2 )
| ( X2 != multiply(X0,X1) )
| ( multiply(X0,X1) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_946]) ).
tcf(c_1068,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = multiply(X0,X1),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_1072,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X0,X1) = X4 )
| ( X4 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_946]) ).
tcf(c_1081,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_131,c_624]) ).
tcf(c_1084,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c7) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_133,c_624]) ).
tcf(c_1139,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c11,multiply(sk_c9,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_134,c_105]) ).
tcf(c_1140,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c11,multiply(sk_c9,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_133,c_105]) ).
tcf(c_1141,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,multiply(sk_c9,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_131,c_105]) ).
tcf(c_1143,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,multiply(sk_c9,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_127,c_105]) ).
tcf(c_1150,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_104,c_105]) ).
tcf(c_1179,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != multiply(sk_c3,sk_c11) )
| ( multiply(X0,X1) != multiply(sk_c3,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_947]) ).
tcf(c_1184,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_947]) ).
tcf(c_1185,plain,
( ( sk_c10 = multiply(sk_c10,sk_c10) )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(sk_c10,sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1184]) ).
tcf(c_1186,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != multiply(inverse(X2),X2) )
| ( multiply(X0,X1) != multiply(inverse(X2),X2) ) ),
inference(instantiation,[status(thm)],[c_947]) ).
tcf(c_1203,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_1306,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,multiply(sk_c11,sk_c9)) )
| ( X1 != X0 )
| ( multiply(identity,multiply(sk_c11,sk_c9)) != X0 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_1314,plain,
( ( sk_c10 = multiply(identity,multiply(sk_c11,sk_c9)) )
| ( sk_c10 != multiply(sk_c11,sk_c9) )
| ( multiply(identity,multiply(sk_c11,sk_c9)) != multiply(sk_c11,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_939]) ).
tcf(c_1507,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1150,c_103]) ).
tcf(c_1509,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,multiply(sk_c3,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_117,c_1507]) ).
tcf(c_1518,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(inverse(sk_c1),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_114,c_1507]) ).
tcf(c_1519,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(inverse(sk_c1),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_113,c_1507]) ).
tcf(c_1520,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(inverse(sk_c1),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_111,c_1507]) ).
tcf(c_1522,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c1),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_107,c_1507]) ).
tcf(c_1523,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(inverse(sk_c3),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_146,c_1507]) ).
tcf(c_1525,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(inverse(sk_c4),sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_148,c_1507]) ).
tcf(c_1529,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(inverse(sk_c8),sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_122,c_1507]) ).
tcf(c_1542,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_104,c_1507]) ).
tcf(c_1549,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_1507,c_1507]) ).
tcf(c_1564,plain,
( ( sk_c11 = inverse(sk_c3) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_985]) ).
tcf(c_1589,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( X0 != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_993]) ).
tcf(c_1643,plain,
! [X0: $i] :
( ( multiply(inverse(X0),X0) = multiply(identity,identity) )
| ( multiply(identity,identity) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_1644,plain,
multiply(identity,identity) = identity,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_1645,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(identity,identity) )
| ( multiply(identity,identity) != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_1643]) ).
tcf(c_1649,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_1650,plain,
( ( sk_c10 = identity )
| ( identity != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1649]) ).
tcf(c_1651,plain,
! [X0: $i] :
( ( multiply(inverse(X0),X0) = multiply(sk_c3,sk_c11) )
| ( multiply(sk_c3,sk_c11) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_1653,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(sk_c3,sk_c11) )
| ( multiply(sk_c3,sk_c11) != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_1651]) ).
tcf(c_1791,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = multiply(identity,X2) )
| ( X1 != X2 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_627]) ).
tcf(c_1792,plain,
( ( multiply(sk_c10,sk_c10) = multiply(identity,sk_c10) )
| ( sk_c10 != identity )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1791]) ).
tcf(c_1923,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( inverse(sk_c1) = sk_c11 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_626,c_117]) ).
tcf(c_1924,plain,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1923]) ).
tcf(c_1925,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_626,c_118]) ).
tcf(c_1936,plain,
! [X0: $i] :
( ( multiply(sk_c5,sk_c8) = X0 )
| ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_626,c_110]) ).
tcf(c_1994,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X1) = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_626,c_103]) ).
tcf(c_1999,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_626,c_625]) ).
tcf(c_2000,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_626,c_628]) ).
tcf(c_2012,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(X0,X1) )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_2019,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( multiply(sk_c4,sk_c10) != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1067]) ).
tcf(c_2037,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = sk_c10 )
| ( sk_c10 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_2040,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( multiply(X0,X1) != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_2161,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != inverse(sk_c3) )
| ( X0 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_2162,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != inverse(sk_c3) )
| ( sk_c11 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_2161]) ).
tcf(c_2175,plain,
( ( sk_c11 = inverse(sk_c1) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_985]) ).
tcf(c_2222,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_1507]) ).
tcf(c_2245,plain,
( ~ iPr_def_10
| ( inverse(sk_c2) != sk_c10 )
| ( multiply(sk_c2,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_621]) ).
tcf(c_2246,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_2502,plain,
! [X0: $i] :
( ( identity = sk_c10 )
| ( identity != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_2508,plain,
multiply(sk_c4,sk_c10) = multiply(sk_c4,sk_c10),
inference(instantiation,[status(thm)],[c_1068]) ).
tcf(c_2512,plain,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_138,c_621]) ).
tcf(c_2524,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_10
| ( inverse(sk_c2) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_139,c_621]) ).
tcf(c_2527,plain,
( ~ iPr_def_10
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_104,c_621]) ).
tcf(c_2687,plain,
sk_c3 = sk_c3,
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_2704,plain,
( ( inverse(sk_c6) = sk_c8 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_114,c_622]) ).
tcf(c_2708,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_107,c_622]) ).
tcf(c_2715,plain,
( ~ iPr_def_11
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_104,c_622]) ).
tcf(c_2811,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(identity,multiply(sk_c11,sk_c9)) )
| ( X2 != multiply(X0,X1) )
| ( multiply(identity,multiply(sk_c11,sk_c9)) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_1306]) ).
tcf(c_2812,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,multiply(sk_c11,sk_c9)) = multiply(X1,X0) )
| ( identity != X1 )
| ( multiply(sk_c11,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_627]) ).
tcf(c_2814,plain,
( ( multiply(identity,multiply(sk_c11,sk_c9)) = multiply(sk_c10,sk_c10) )
| ( identity != sk_c10 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2812]) ).
tcf(c_2839,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_2985,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_1542,c_1549]) ).
tcf(c_2998,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_1549,c_104]) ).
tcf(c_3111,plain,
( ( sk_c10 = multiply(sk_c3,sk_c11) )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1999,c_106]) ).
tcf(c_3114,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_1999,c_118]) ).
tcf(c_3116,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1999,c_108]) ).
tcf(c_3117,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1999,c_128]) ).
tcf(c_3136,plain,
( ( sk_c10 = multiply(sk_c11,sk_c9) )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_1999,c_131]) ).
tcf(c_3137,plain,
( ( sk_c10 = multiply(sk_c11,sk_c9) )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(resolution,[status(thm)],[c_1999,c_133]) ).
tcf(c_3145,plain,
( ( sk_c9 = multiply(sk_c2,sk_c10) )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_1999,c_138]) ).
tcf(c_3156,plain,
! [X0: $i] : identity = multiply(inverse(X0),X0),
inference(resolution,[status(thm)],[c_1999,c_104]) ).
tcf(c_3236,plain,
! [X0: $i] :
( ( multiply(inverse(X0),X0) = sk_c10 )
| ( sk_c10 != multiply(identity,identity) )
| ( multiply(inverse(X0),X0) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_2037]) ).
tcf(c_3237,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),X0) )
| ( sk_c10 != multiply(identity,identity) )
| ( multiply(inverse(X0),X0) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_1184]) ).
tcf(c_3238,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != multiply(identity,identity) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_3237]) ).
tcf(c_3239,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(identity,identity) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_3236]) ).
tcf(c_3563,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(inverse(X0),X0) )
| ( X1 != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_2012]) ).
tcf(c_3603,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_117,c_2998]) ).
tcf(c_3604,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_149,c_2998]) ).
tcf(c_3607,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_121,c_2998]) ).
tcf(c_3613,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_2998,c_103]) ).
tcf(c_3817,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_623,c_2998]) ).
tcf(c_3832,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( inverse(X0) != identity )
| ( inverse(inverse(X0)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_2998,c_3817]) ).
tcf(c_3844,plain,
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( inverse(sk_c10) != identity )
| ( inverse(inverse(sk_c10)) != inverse(sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3832]) ).
tcf(c_4069,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != multiply(sk_c1,sk_c11) )
| ( multiply(X0,X1) != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_947]) ).
tcf(c_4081,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != inverse(sk_c1) )
| ( X0 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_4082,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != inverse(sk_c1) )
| ( sk_c11 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_4081]) ).
tcf(c_4126,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ( sk_c9 != multiply(sk_c2,sk_c10) )
| ( multiply(X0,X1) != multiply(sk_c2,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_4403,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_3603,c_116]) ).
tcf(c_4416,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_4403,c_2998]) ).
tcf(c_4463,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_3604,c_148]) ).
tcf(c_4525,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( multiply(inverse(sk_c10),X0) = multiply(sk_c2,X0) ) ),
inference(superposition,[status(thm)],[c_4463,c_1549]) ).
tcf(c_4529,plain,
( ( sk_c9 = identity )
| ( multiply(inverse(sk_c10),sk_c10) = multiply(sk_c2,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_4525]) ).
tcf(c_4678,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c3) )
| ( sk_c10 != X0 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_4818,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_622,c_107]) ).
tcf(c_4824,plain,
( ( inverse(sk_c2) = sk_c10 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_622,c_146]) ).
tcf(c_4903,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_3607,c_120]) ).
tcf(c_5026,plain,
sk_c4 = sk_c4,
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_5049,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_946]) ).
tcf(c_5050,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_5049]) ).
tcf(c_5059,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != sk_c11 )
| ( multiply(X0,X1) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_985]) ).
tcf(c_5069,plain,
( ( sk_c11 = multiply(sk_c10,sk_c10) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c10,sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_5059]) ).
tcf(c_5218,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),X0) )
| ( sk_c10 != multiply(sk_c3,sk_c11) )
| ( multiply(inverse(X0),X0) != multiply(sk_c3,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1179]) ).
tcf(c_5219,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != multiply(sk_c3,sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c3,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_5218]) ).
tcf(c_5276,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(identity) != inverse(X0) )
| ( inverse(inverse(identity)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_1994,c_623]) ).
tcf(c_5277,plain,
( ~ iPr_def_12
| ( inverse(identity) != inverse(sk_c10) )
| ( inverse(inverse(identity)) != inverse(sk_c10) )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_5276]) ).
tcf(c_5488,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c4,sk_c10) = multiply(X1,X0) )
| ( sk_c4 != X1 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_627]) ).
tcf(c_5490,plain,
( ( multiply(sk_c4,sk_c10) = multiply(sk_c10,sk_c10) )
| ( sk_c4 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_5488]) ).
tcf(c_5968,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_147,c_1523]) ).
tcf(c_5975,plain,
( ( inverse(sk_c2) = sk_c10 )
| ~ iPr_def_10
| ( sk_c11 != sk_c9 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_5968,c_621]) ).
tcf(c_5976,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_1542,c_2985]) ).
tcf(c_5978,plain,
( ~ iPr_def_11
| ( sk_c10 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2715,c_5976]) ).
tcf(c_5979,plain,
( ~ iPr_def_10
| ( sk_c9 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2527,c_5976]) ).
tcf(c_5991,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_5976,c_104]) ).
tcf(c_5995,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_117,c_5991]) ).
tcf(c_5996,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_149,c_5991]) ).
tcf(c_6290,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_5975,c_2245,c_2524,c_2512,c_4463,c_5979]) ).
tcf(c_6366,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_5995,c_116]) ).
tcf(c_6379,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_6366,c_5991]) ).
tcf(c_6419,plain,
! [X0: $i,X1: $i] :
( ( sk_c3 = X0 )
| ( sk_c3 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_6437,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_5996,c_148]) ).
tcf(c_6480,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c2,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_6437,c_5991]) ).
tcf(c_6740,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_6379,c_107]) ).
tcf(c_6764,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_6480,c_139]) ).
tcf(c_6917,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c11 )
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_6933,plain,
! [X0: $i] :
( ( multiply(inverse(X0),X0) = sk_c9 )
| ( sk_c9 != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_6937,plain,
! [X0: $i] :
( ( sk_c9 = multiply(inverse(X0),X0) )
| ( sk_c9 != sk_c9 )
| ( multiply(inverse(X0),X0) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_932]) ).
tcf(c_6938,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c9 )
| ( sk_c9 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_6933]) ).
tcf(c_6958,plain,
! [X0: $i] :
( ( multiply(inverse(X0),X0) = multiply(sk_c4,sk_c10) )
| ( multiply(sk_c4,sk_c10) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_6960,plain,
! [X0: $i] :
( ( multiply(inverse(X0),X0) = sk_c9 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( multiply(inverse(X0),X0) != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2040]) ).
tcf(c_6961,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(sk_c4,sk_c10) )
| ( multiply(sk_c4,sk_c10) != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_6958]) ).
tcf(c_6962,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c9 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_6960]) ).
tcf(c_7113,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_6740,c_5991]) ).
tcf(c_7257,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_6764,c_5991]) ).
tcf(c_7533,plain,
( ( identity = sk_c10 )
| ( identity != identity )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_2502]) ).
tcf(c_7625,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(sk_c4,sk_c10) = X2 )
| ( X2 != multiply(X0,X1) )
| ( multiply(sk_c4,sk_c10) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_7626,plain,
( ( multiply(sk_c4,sk_c10) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c4,sk_c10) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_7625]) ).
tcf(c_7968,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != multiply(identity,multiply(sk_c11,sk_c9)) )
| ( X0 != multiply(identity,multiply(sk_c11,sk_c9)) ) ),
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_7969,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(identity,multiply(sk_c11,sk_c9)) )
| ( sk_c11 != multiply(identity,multiply(sk_c11,sk_c9)) ) ),
inference(instantiation,[status(thm)],[c_7968]) ).
tcf(c_8160,plain,
( ( sk_c10 = multiply(sk_c3,sk_c11) )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_3111,c_622]) ).
tcf(c_8161,plain,
( ( sk_c10 = multiply(sk_c3,sk_c11) )
| ( sk_c10 = multiply(sk_c1,sk_c11) ) ),
inference(resolution,[status(thm)],[c_3111,c_1999]) ).
tcf(c_8389,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_3116,c_622]) ).
tcf(c_8391,plain,
! [X0: $i] :
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( multiply(sk_c1,sk_c11) = X0 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_3116,c_626]) ).
tcf(c_8467,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 = multiply(sk_c4,sk_c10) ) ),
inference(resolution,[status(thm)],[c_3117,c_624]) ).
tcf(c_8592,plain,
( iPr_def_12
| ( sk_c9 = multiply(sk_c4,sk_c10) ) ),
inference(global_subsumption_just,[status(thm)],[c_8467,c_624,c_2245,c_2524,c_2512,c_3117,c_3114,c_4463,c_5979,c_8389]) ).
tcf(c_8603,plain,
! [X0: $i] :
( iPr_def_12
| ( sk_c9 = X0 )
| ( X0 != multiply(sk_c4,sk_c10) ) ),
inference(resolution,[status(thm)],[c_8592,c_626]) ).
tcf(c_8684,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(identity,multiply(sk_c11,sk_c9)) )
| ( sk_c11 != multiply(X0,X1) )
| ( multiply(identity,multiply(sk_c11,sk_c9)) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_2811]) ).
tcf(c_8685,plain,
( ( sk_c11 = multiply(identity,multiply(sk_c11,sk_c9)) )
| ( sk_c11 != multiply(sk_c10,sk_c10) )
| ( multiply(identity,multiply(sk_c11,sk_c9)) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_8684]) ).
tcf(c_9048,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(X3) = multiply(X0,X1) )
| ( inverse(X3) != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_2012]) ).
tcf(c_9110,plain,
! [X0: $i,X1: $i] :
( ( identity = sk_c10 )
| ( identity != multiply(X0,X1) )
| ( sk_c10 != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_2502]) ).
tcf(c_9222,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_11
| ( inverse(inverse(sk_c8)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_1529,c_622]) ).
tcf(c_9318,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c4,sk_c10) )
| ( inverse(sk_c1) = sk_c11 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_1925,c_1999]) ).
tcf(c_9436,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_9222,c_4403,c_5978]) ).
tcf(c_9492,plain,
( ( sk_c9 = multiply(sk_c2,sk_c10) )
| ( sk_c9 = multiply(sk_c4,sk_c10) ) ),
inference(resolution,[status(thm)],[c_3145,c_1999]) ).
tcf(c_9800,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_4818,c_2708,c_9436]) ).
tcf(c_9813,plain,
( ( inverse(sk_c2) = sk_c10 )
| ~ iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4824,c_9800]) ).
tcf(c_10231,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X1,X2) = multiply(inverse(X0),X0) )
| ( multiply(X1,X2) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_3563]) ).
tcf(c_10283,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = sk_c9 )
| ( sk_c9 != multiply(X0,X1) )
| ( sk_c10 != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_950]) ).
tcf(c_10289,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != multiply(X1,X2) )
| ( X0 != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_10290,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( sk_c11 != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_10289]) ).
tcf(c_10472,plain,
( ( sk_c10 = multiply(sk_c3,sk_c11) )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_8160,c_8160,c_9436]) ).
tcf(c_11048,plain,
! [X0: $i] :
( ( inverse(inverse(X0)) = inverse(sk_c10) )
| ( inverse(X0) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_11049,plain,
( ( inverse(inverse(sk_c10)) = inverse(sk_c10) )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_11048]) ).
tcf(c_11249,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c1) )
| ( sk_c10 != X0 )
| ( inverse(sk_c1) != X0 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_11368,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_11369,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_11368]) ).
tcf(c_11784,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(X2) )
| ( X2 != X1 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2000,c_628]) ).
tcf(c_12026,plain,
! [X0: $i] :
( ( sk_c4 = sk_c10 )
| ( sk_c4 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_12836,plain,
! [X0: $i] :
( ( multiply(inverse(X0),X0) = sk_c9 )
| ( sk_c9 != multiply(sk_c2,sk_c10) )
| ( multiply(inverse(X0),X0) != multiply(sk_c2,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_4126]) ).
tcf(c_12838,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c9 )
| ( sk_c9 != multiply(sk_c2,sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c2,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_12836]) ).
tcf(c_13321,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c1) = multiply(X0,X1) )
| ( inverse(sk_c1) != sk_c11 )
| ( multiply(X0,X1) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_9048]) ).
tcf(c_14616,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c3) )
| ( sk_c10 != inverse(X0) )
| ( inverse(sk_c3) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_4678]) ).
tcf(c_14617,plain,
! [X0: $i] :
( ( inverse(sk_c3) = inverse(X0) )
| ( sk_c3 != X0 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_14618,plain,
( ( sk_c10 = inverse(sk_c3) )
| ( sk_c10 != inverse(sk_c10) )
| ( inverse(sk_c3) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_14616]) ).
tcf(c_14619,plain,
( ( inverse(sk_c3) = inverse(sk_c10) )
| ( sk_c3 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_14617]) ).
tcf(c_18321,plain,
! [X0: $i] :
( ( sk_c3 = X0 )
| ( sk_c3 != sk_c3 )
| ( X0 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_6419]) ).
tcf(c_18322,plain,
( ( sk_c3 = sk_c10 )
| ( sk_c3 != sk_c3 )
| ( sk_c10 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_18321]) ).
tcf(c_21030,negated_conjecture,
( iPr_def_12
| iPr_def_11
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_624,c_624,c_2245,c_2524,c_2512,c_4463,c_5979]) ).
tcf(c_21509,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_1542,c_2985]) ).
tcf(c_21522,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_21509,c_104]) ).
tcf(c_21526,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_117,c_21522]) ).
tcf(c_21537,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_21522,c_105]) ).
tcf(c_21540,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_21522,c_105]) ).
tcf(c_21575,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_21537,c_103]) ).
tcf(c_21587,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,multiply(sk_c11,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_117,c_21575]) ).
tcf(c_21598,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_21509,c_21575]) ).
tcf(c_21859,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_21526,c_116]) ).
tcf(c_22125,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,multiply(sk_c11,inverse(sk_c10))) = identity ) ),
inference(superposition,[status(thm)],[c_116,c_21540]) ).
tcf(c_22419,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_149,c_1525]) ).
tcf(c_22432,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_22419,c_21598]) ).
tcf(c_22991,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,identity) = inverse(sk_c3) ) ),
inference(superposition,[status(thm)],[c_21522,c_1509]) ).
tcf(c_23328,plain,
! [X0: $i] :
( ( sk_c10 = sk_c9 )
| ( sk_c9 != multiply(inverse(X0),X0) )
| ( sk_c10 != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_10283]) ).
tcf(c_24366,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_3156,c_626]) ).
tcf(c_24367,plain,
( ( identity = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_24366]) ).
tcf(c_24397,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_9813,c_158,c_631,c_1650,c_1653,c_5219,c_5978,c_7113,c_10472,c_24367]) ).
tcf(c_25490,plain,
( iPr_def_12
| ( sk_c9 = multiply(sk_c5,sk_c8) )
| ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_8603,c_1936]) ).
tcf(c_25918,plain,
( ( sk_c10 = multiply(identity,identity) )
| ( sk_c10 != multiply(sk_c1,sk_c11) )
| ( multiply(identity,identity) != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_4069]) ).
tcf(c_25921,plain,
! [X0: $i] :
( ( sk_c10 = multiply(identity,identity) )
| ( sk_c10 != multiply(inverse(X0),X0) )
| ( multiply(identity,identity) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_1186]) ).
tcf(c_27319,plain,
! [X0: $i] :
( ( identity = sk_c10 )
| ( identity != multiply(inverse(X0),X0) )
| ( sk_c10 != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_9110]) ).
tcf(c_27843,plain,
! [X0: $i] :
( ( multiply(identity,identity) = multiply(inverse(X0),X0) )
| ( multiply(identity,identity) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_10231]) ).
tcf(c_29186,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_2704,c_158,c_631,c_1650,c_1653,c_5219,c_5978,c_7113,c_10472,c_24367]) ).
tcf(c_29193,plain,
( iPr_def_12
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_21030,c_29186]) ).
tcf(c_31479,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_22432,c_158,c_4529,c_6938,c_6961,c_6962,c_7257,c_9492,c_12838]) ).
tcf(c_31481,plain,
sk_c9 = identity,
inference(demodulation,[status(thm)],[c_31479,c_104]) ).
tcf(c_31538,plain,
( ( sk_c10 = sk_c9 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_21859,c_31481]) ).
tcf(c_31557,plain,
! [X0: $i] : multiply(inverse(X0),X0) = sk_c9,
inference(demodulation,[status(thm)],[c_104,c_31481]) ).
tcf(c_32725,plain,
! [X0: $i] :
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( sk_c9 != X0 )
| ( multiply(sk_c4,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_911]) ).
tcf(c_32726,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( sk_c9 != sk_c10 )
| ( multiply(sk_c4,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_32725]) ).
tcf(c_32843,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != sk_c9 )
| ( inverse(X0) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2246]) ).
tcf(c_32845,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_32843]) ).
tcf(c_33010,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = inverse(sk_c3) ) ),
inference(light_normalisation,[status(thm)],[c_22991,c_31481]) ).
tcf(c_33020,plain,
( iPr_def_12
| ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c3) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_33010,c_29193]) ).
tcf(c_33397,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,multiply(sk_c11,inverse(sk_c10))) = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_22125,c_31481]) ).
tcf(c_33411,plain,
( ( inverse(sk_c10) = sk_c9 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_33397,c_21587]) ).
tcf(c_34055,plain,
! [X0: $i] : multiply(sk_c9,X0) = X0,
inference(light_normalisation,[status(thm)],[c_103,c_31481]) ).
tcf(c_34056,plain,
! [X0: $i] : multiply(inverse(X0),X0) = sk_c9,
inference(light_normalisation,[status(thm)],[c_104,c_31481]) ).
tcf(c_34072,plain,
! [X0: $i] : multiply(X0,sk_c9) = X0,
inference(light_normalisation,[status(thm)],[c_2985,c_31481]) ).
tcf(c_34073,plain,
inverse(sk_c9) = sk_c9,
inference(superposition,[status(thm)],[c_34056,c_34072]) ).
tcf(c_34076,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(sk_c9,X1),
inference(light_normalisation,[status(thm)],[c_1150,c_31481]) ).
tcf(c_34077,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_34076,c_34055]) ).
tcf(c_34305,plain,
( ( sk_c11 = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_128,c_34072]) ).
tcf(c_34313,plain,
( ( sk_c11 = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_130,c_34072]) ).
tcf(c_34318,plain,
! [X0: $i] :
( ( sk_c11 = sk_c10 )
| ( multiply(sk_c5,multiply(sk_c8,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_34313,c_105]) ).
tcf(c_34513,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(inverse(inverse(sk_c1)),sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_1518,c_34077]) ).
tcf(c_34518,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(inverse(inverse(sk_c1)),multiply(sk_c11,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_34513,c_105]) ).
tcf(c_34596,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(inverse(inverse(sk_c1)),sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_1519,c_34077]) ).
tcf(c_34614,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(inverse(sk_c1)),sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_1522,c_34077]) ).
tcf(c_34768,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(inverse(inverse(sk_c1)),multiply(sk_c11,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_34596,c_105]) ).
tcf(c_34792,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(inverse(sk_c1)),multiply(sk_c11,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_34614,c_105]) ).
tcf(c_35224,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(inverse(multiply(X0,X1))),X2) = multiply(X0,multiply(X1,X2)),
inference(superposition,[status(thm)],[c_2222,c_34077]) ).
tcf(c_36411,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c11,X0) = multiply(sk_c10,X0) ) ),
inference(light_normalisation,[status(thm)],[c_1139,c_34055]) ).
tcf(c_36457,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c11,X0) = multiply(sk_c10,X0) ) ),
inference(light_normalisation,[status(thm)],[c_1140,c_34055]) ).
tcf(c_36503,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,X0) = multiply(sk_c10,X0) ) ),
inference(light_normalisation,[status(thm)],[c_1141,c_34055]) ).
tcf(c_36595,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,X0) = multiply(sk_c10,X0) ) ),
inference(light_normalisation,[status(thm)],[c_1143,c_34055]) ).
tcf(c_41263,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = sk_c9,
inference(superposition,[status(thm)],[c_35224,c_34056]) ).
tcf(c_42003,plain,
( ( multiply(identity,identity) = multiply(sk_c1,sk_c11) )
| ( multiply(identity,identity) != identity )
| ( multiply(sk_c1,sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_1062]) ).
tcf(c_42326,plain,
( ( sk_c10 = inverse(sk_c1) )
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_11249]) ).
tcf(c_42679,plain,
( ( sk_c4 = sk_c10 )
| ( sk_c4 != sk_c4 )
| ( sk_c10 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_12026]) ).
tcf(c_45721,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,multiply(X2,inverse(multiply(X0,multiply(X1,X2)))))) = sk_c9,
inference(superposition,[status(thm)],[c_105,c_41263]) ).
tcf(c_45760,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c1,multiply(sk_c11,inverse(sk_c10))) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_113,c_41263]) ).
tcf(c_45761,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,multiply(sk_c11,inverse(sk_c10))) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_111,c_41263]) ).
tcf(c_45763,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,multiply(sk_c11,inverse(sk_c10))) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_107,c_41263]) ).
tcf(c_45770,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,multiply(sk_c11,inverse(sk_c10))) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_116,c_41263]) ).
tcf(c_49499,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = identity )
| ( identity != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1649]) ).
tcf(c_49505,plain,
( ( inverse(sk_c10) = identity )
| ( identity != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_49499]) ).
tcf(c_49509,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_1649]) ).
tcf(c_49527,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_952]) ).
tcf(c_49529,plain,
( ( sk_c11 = identity )
| ( identity != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_49509]) ).
tcf(c_49614,plain,
inverse(sk_c1) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_9318,c_158,c_1924,c_2839,c_3844,c_4403,c_4903,c_6917,c_7533,c_11049,c_31538,c_32845,c_33020,c_33411,c_49505,c_49527]) ).
tcf(c_50798,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_11784,c_3156]) ).
tcf(c_50799,plain,
( ( inverse(sk_c10) = inverse(identity) )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_50798]) ).
tcf(c_53400,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(inverse(sk_c1),sk_c9) = multiply(sk_c11,inverse(sk_c10)) ) ),
inference(superposition,[status(thm)],[c_45760,c_34077]) ).
tcf(c_53615,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,multiply(multiply(sk_c11,inverse(sk_c10)),X0)) = multiply(sk_c9,X0) ) ),
inference(superposition,[status(thm)],[c_45761,c_105]) ).
tcf(c_53616,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(inverse(sk_c1),sk_c9) = multiply(sk_c11,inverse(sk_c10)) ) ),
inference(superposition,[status(thm)],[c_45761,c_34077]) ).
tcf(c_53982,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,multiply(multiply(sk_c11,inverse(sk_c10)),X0)) = multiply(sk_c9,X0) ) ),
inference(superposition,[status(thm)],[c_45763,c_105]) ).
tcf(c_53983,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c1),sk_c9) = multiply(sk_c11,inverse(sk_c10)) ) ),
inference(superposition,[status(thm)],[c_45763,c_34077]) ).
tcf(c_54153,plain,
inverse(sk_c1) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_45770,c_49614]) ).
tcf(c_54211,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_1522,c_54153]) ).
tcf(c_54213,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_1520,c_54153]) ).
tcf(c_54214,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_1519,c_54153]) ).
tcf(c_54217,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_1518,c_54153]) ).
tcf(c_54264,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c10,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_54211,c_36595]) ).
tcf(c_54348,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c10,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_54213,c_36503]) ).
tcf(c_54390,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_54214,c_36457]) ).
tcf(c_54473,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c10,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_54217,c_36411]) ).
tcf(c_54791,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c11,inverse(sk_c10)) = multiply(sk_c11,sk_c9) ) ),
inference(light_normalisation,[status(thm)],[c_53400,c_54153]) ).
tcf(c_54792,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c11,inverse(sk_c10)) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_54791,c_34072]) ).
tcf(c_54820,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,inverse(sk_c10)) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_54792,c_36457]) ).
tcf(c_54840,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,inverse(sk_c10)) = multiply(sk_c11,sk_c9) ) ),
inference(light_normalisation,[status(thm)],[c_53616,c_54153]) ).
tcf(c_54841,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,inverse(sk_c10)) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_54840,c_34072]) ).
tcf(c_54868,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c10,inverse(sk_c10)) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_54841,c_36503]) ).
tcf(c_54938,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,inverse(sk_c10)) = multiply(sk_c11,sk_c9) ) ),
inference(light_normalisation,[status(thm)],[c_53983,c_54153]) ).
tcf(c_54939,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,inverse(sk_c10)) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_54938,c_34072]) ).
tcf(c_54964,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c10,inverse(sk_c10)) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_54939,c_36595]) ).
tcf(c_55248,plain,
! [X0: $i] :
( ( sk_c11 = sk_c10 )
| ( multiply(X0,multiply(sk_c5,multiply(sk_c8,inverse(multiply(X0,sk_c11))))) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_34313,c_45721]) ).
tcf(c_55249,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( multiply(X0,multiply(sk_c5,multiply(sk_c8,inverse(multiply(X0,sk_c11))))) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_110,c_45721]) ).
tcf(c_57866,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(inverse(sk_c11),multiply(sk_c11,X0)) = multiply(sk_c10,X0) ) ),
inference(light_normalisation,[status(thm)],[c_34518,c_54153]) ).
tcf(c_57867,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(demodulation,[status(thm)],[c_57866,c_34077]) ).
tcf(c_57895,plain,
( ( sk_c10 = sk_c9 )
| ( inverse(sk_c6) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_57867,c_34072]) ).
tcf(c_57950,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(inverse(sk_c11),multiply(sk_c11,X0)) = multiply(sk_c10,X0) ) ),
inference(light_normalisation,[status(thm)],[c_34768,c_54153]) ).
tcf(c_57951,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(demodulation,[status(thm)],[c_57950,c_34077]) ).
tcf(c_57978,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ~ iPr_def_12
| ( inverse(X0) != inverse(sk_c10) )
| ( inverse(inverse(sk_c10)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_57951,c_623]) ).
tcf(c_58033,plain,
( ( inverse(sk_c7) = sk_c6 )
| ~ iPr_def_12
| ( inverse(sk_c10) != inverse(sk_c10) )
| ( inverse(inverse(sk_c10)) != inverse(sk_c10) )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_57978]) ).
tcf(c_58212,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c11),multiply(sk_c11,X0)) = multiply(sk_c10,X0) ) ),
inference(light_normalisation,[status(thm)],[c_34792,c_54153]) ).
tcf(c_58213,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(demodulation,[status(thm)],[c_58212,c_34077]) ).
tcf(c_58227,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c10),X0) = X0 ) ),
inference(superposition,[status(thm)],[c_58213,c_34077]) ).
tcf(c_58285,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_58227]) ).
tcf(c_64979,plain,
( ( inverse(sk_c1) = multiply(sk_c4,sk_c10) )
| ( inverse(sk_c1) != sk_c11 )
| ( multiply(sk_c4,sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_13321]) ).
tcf(c_64981,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( inverse(sk_c1) != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1589]) ).
tcf(c_67118,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c10) = sk_c11 )
| ( sk_c11 != X0 )
| ( multiply(sk_c4,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_1203]) ).
tcf(c_67121,plain,
( ( multiply(sk_c4,sk_c10) = sk_c11 )
| ( sk_c11 != sk_c10 )
| ( multiply(sk_c4,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_67118]) ).
tcf(c_70607,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_70637,plain,
! [X0: $i] :
( ( inverse(identity) = inverse(X0) )
| ( identity != X0 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_70639,plain,
( ( inverse(identity) = inverse(sk_c10) )
| ( identity != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_70637]) ).
tcf(c_70706,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_70607]) ).
tcf(c_70752,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_70754,plain,
( ( inverse(sk_c10) = inverse(identity) )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_70752]) ).
tcf(c_70763,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(inverse(identity)) )
| ( X1 != X0 )
| ( inverse(inverse(identity)) != X0 ) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_70766,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(inverse(identity)) )
| ( X0 != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_71571,plain,
! [X0: $i] :
( ( inverse(inverse(X0)) = inverse(inverse(identity)) )
| ( inverse(X0) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_70766]) ).
tcf(c_71572,plain,
( ( inverse(inverse(sk_c10)) = inverse(inverse(identity)) )
| ( inverse(sk_c10) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_71571]) ).
tcf(c_71592,plain,
! [X0: $i] :
( ( X0 = inverse(inverse(identity)) )
| ( X0 != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_70763]) ).
tcf(c_71593,plain,
( ( inverse(inverse(identity)) = inverse(identity) )
| ( inverse(identity) != identity ) ),
inference(instantiation,[status(thm)],[c_70752]) ).
tcf(c_71604,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(X2) )
| ( inverse(X2) != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_70706]) ).
tcf(c_76008,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(inverse(identity)) )
| ( inverse(X0) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_71592]) ).
tcf(c_76009,plain,
( ( inverse(sk_c10) = inverse(inverse(identity)) )
| ( inverse(sk_c10) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_76008]) ).
tcf(c_77520,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(inverse(X0)) = inverse(X2) )
| ( inverse(X2) != inverse(X1) )
| ( inverse(inverse(X0)) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_71604]) ).
tcf(c_80910,plain,
! [X0: $i] :
( ( inverse(inverse(identity)) = inverse(X0) )
| ( inverse(X0) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_77520]) ).
tcf(c_80911,plain,
( ( inverse(inverse(identity)) = inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_80910]) ).
tcf(c_80926,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(X1) )
| ( inverse(X1) != inverse(inverse(identity)) )
| ( inverse(inverse(X0)) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_77520]) ).
tcf(c_80927,plain,
( ( inverse(inverse(sk_c10)) = inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(inverse(identity)) )
| ( inverse(inverse(sk_c10)) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_80926]) ).
tcf(c_95070,plain,
inverse(sk_c5) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_53615,c_104,c_158,c_131,c_631,c_919,c_941,c_986,c_1081,c_1314,c_1643,c_1645,c_1644,c_1650,c_1651,c_1653,c_2245,c_2524,c_2512,c_2814,c_3136,c_3156,c_3237,c_3238,c_3239,c_3613,c_4416,c_4463,c_5050,c_5069,c_5218,c_5219,c_5277,c_5979,c_5978,c_7113,c_7969,c_8161,c_8685,c_10472,c_24367,c_25921,c_25918,c_27319,c_27843,c_42003,c_50799,c_54348,c_54868,c_70639,c_71593,c_80911]) ).
tcf(c_95487,plain,
inverse(sk_c3) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_53982,c_157,c_631,c_940,c_986,c_1052,c_1185,c_1792,c_2839,c_3613,c_5050,c_5069,c_5277,c_6290,c_6740,c_7533,c_10290,c_24397,c_54264,c_54964,c_58285,c_70639,c_70754,c_71593,c_80911]) ).
tcf(c_97162,plain,
sk_c10 = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_57895,c_104,c_909,c_941,c_1643,c_1644,c_1651,c_3237,c_4416,c_5218,c_6937,c_7113,c_8161,c_23328,c_25918,c_31557,c_42003]) ).
tcf(c_97213,plain,
( ( sk_c11 = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_34305,c_97162]) ).
tcf(c_97217,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm)],[c_34073,c_97162]) ).
tcf(c_97218,plain,
! [X0: $i] : multiply(X0,sk_c10) = X0,
inference(demodulation,[status(thm)],[c_34072,c_97162]) ).
tcf(c_97222,plain,
( ( sk_c10 = sk_c4 )
| ( sk_c11 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_97213,c_97218]) ).
tcf(c_97312,plain,
! [X0: $i] : multiply(X0,multiply(sk_c5,multiply(sk_c8,inverse(multiply(X0,sk_c11))))) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_55249,c_157,c_104,c_158,c_631,c_624,c_895,c_896,c_909,c_933,c_940,c_941,c_1185,c_1643,c_1645,c_1644,c_1650,c_1651,c_1653,c_1792,c_2245,c_2524,c_2512,c_3156,c_3237,c_3238,c_3239,c_3613,c_3844,c_4416,c_4463,c_5050,c_5218,c_5219,c_5979,c_5978,c_6937,c_7113,c_8161,c_10472,c_23328,c_24367,c_25921,c_25918,c_27319,c_27843,c_31557,c_42003,c_49505,c_49529,c_50799,c_55248,c_71572,c_71593,c_76009,c_80927,c_97217]) ).
tcf(c_97315,plain,
! [X0: $i] : multiply(X0,multiply(sk_c5,multiply(sk_c8,inverse(multiply(X0,sk_c11))))) = sk_c10,
inference(light_normalisation,[status(thm)],[c_97312,c_97162]) ).
tcf(c_97328,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c1,multiply(sk_c5,multiply(sk_c8,inverse(sk_c10)))) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_113,c_97315]) ).
tcf(c_97475,plain,
inverse(sk_c7) = sk_c6,
inference(global_subsumption_just,[status(thm)],[c_97328,c_104,c_158,c_133,c_630,c_631,c_919,c_941,c_986,c_1084,c_1314,c_1643,c_1645,c_1644,c_1650,c_1651,c_1653,c_2245,c_2524,c_2512,c_2814,c_3137,c_3156,c_3237,c_3238,c_3239,c_3613,c_4416,c_4463,c_5050,c_5069,c_5218,c_5219,c_5979,c_5978,c_7113,c_7969,c_8161,c_8685,c_10472,c_24367,c_25921,c_25918,c_27319,c_27843,c_42003,c_50799,c_54390,c_54820,c_58033,c_71572,c_71593,c_76009,c_80927]) ).
tcf(c_107651,plain,
sk_c9 = multiply(sk_c4,sk_c10),
inference(global_subsumption_just,[status(thm)],[c_8391,c_157,c_104,c_158,c_631,c_624,c_895,c_896,c_909,c_933,c_940,c_941,c_1185,c_1643,c_1645,c_1644,c_1650,c_1651,c_1653,c_1792,c_2245,c_2524,c_2512,c_3156,c_3237,c_3238,c_3239,c_3613,c_3844,c_4416,c_4463,c_5026,c_5050,c_5218,c_5219,c_5490,c_5979,c_5978,c_6937,c_7113,c_7626,c_8161,c_10472,c_23328,c_24367,c_25921,c_25918,c_27319,c_27843,c_31557,c_32726,c_42003,c_42679,c_49505,c_49529,c_50799,c_71572,c_71593,c_76009,c_80927,c_97217,c_97222]) ).
tcf(c_109954,plain,
multiply(sk_c4,sk_c10) != sk_c11,
inference(global_subsumption_just,[status(thm)],[c_25490,c_157,c_104,c_158,c_631,c_624,c_895,c_896,c_909,c_933,c_940,c_941,c_986,c_1185,c_1643,c_1645,c_1644,c_1650,c_1651,c_1653,c_1792,c_1924,c_2175,c_2245,c_2524,c_2512,c_2839,c_3156,c_3237,c_3238,c_3239,c_3613,c_3844,c_4082,c_4403,c_4416,c_4463,c_4903,c_5026,c_5050,c_5218,c_5219,c_5490,c_5979,c_5978,c_6917,c_6937,c_7113,c_7533,c_7626,c_8161,c_10472,c_11049,c_23328,c_24367,c_25921,c_25918,c_27319,c_27843,c_31557,c_31538,c_32726,c_32845,c_33020,c_33411,c_42003,c_42326,c_42679,c_49505,c_49529,c_49527,c_50799,c_64979,c_64981,c_71572,c_71593,c_76009,c_80927,c_97217,c_97222]) ).
tcf(c_111273,negated_conjecture,
inverse(sk_c3) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_117,c_95487]) ).
tcf(c_111287,negated_conjecture,
inverse(sk_c5) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_121,c_95070]) ).
tcf(c_111289,negated_conjecture,
inverse(sk_c7) = sk_c6,
inference(global_subsumption_just,[status(thm)],[c_123,c_97475]) ).
tcf(c_111291,negated_conjecture,
inverse(sk_c6) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_124,c_157,c_104,c_158,c_631,c_624,c_895,c_896,c_909,c_933,c_940,c_941,c_986,c_1185,c_1643,c_1645,c_1644,c_1650,c_1651,c_1653,c_1792,c_2245,c_2524,c_2512,c_3156,c_3237,c_3238,c_3239,c_3613,c_3844,c_4416,c_4463,c_5050,c_5069,c_5218,c_5219,c_5979,c_5978,c_6937,c_7113,c_8161,c_10290,c_10472,c_23328,c_24367,c_25921,c_25918,c_27319,c_27843,c_31557,c_42003,c_49505,c_49529,c_50799,c_54473,c_71572,c_71593,c_76009,c_80927,c_97217]) ).
tcf(c_111293,plain,
! [X0: $i] : multiply(sk_c9,X0) = X0,
inference(light_normalisation,[status(thm)],[c_103,c_31481]) ).
tcf(c_111294,plain,
! [X0: $i] : multiply(inverse(X0),X0) = sk_c9,
inference(light_normalisation,[status(thm)],[c_104,c_31481]) ).
tcf(c_111303,plain,
sk_c10 = sk_c9,
inference(superposition,[status(thm)],[c_97218,c_111293]) ).
tcf(c_111344,plain,
! [X0: $i] : multiply(inverse(X0),X0) = sk_c10,
inference(demodulation,[status(thm)],[c_111294,c_111303]) ).
tcf(c_111345,plain,
! [X0: $i] : multiply(sk_c10,X0) = X0,
inference(demodulation,[status(thm)],[c_111293,c_111303]) ).
tcf(c_111361,plain,
! [X0: $i] : multiply(inverse(sk_c8),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_111287,c_1549]) ).
tcf(c_111362,plain,
! [X0: $i] : multiply(inverse(sk_c6),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_111289,c_1549]) ).
tcf(c_111363,plain,
! [X0: $i] : multiply(inverse(sk_c8),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_111291,c_1549]) ).
tcf(c_111368,plain,
! [X0: $i] : multiply(sk_c5,X0) = multiply(sk_c6,X0),
inference(light_normalisation,[status(thm)],[c_111361,c_111363]) ).
tcf(c_111410,plain,
multiply(sk_c11,sk_c3) = sk_c10,
inference(superposition,[status(thm)],[c_111273,c_111344]) ).
tcf(c_111413,plain,
multiply(sk_c6,sk_c7) = sk_c10,
inference(superposition,[status(thm)],[c_111289,c_111344]) ).
tcf(c_111715,plain,
( ( multiply(sk_c2,sk_c10) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_140,c_111303]) ).
tcf(c_111716,plain,
( ( sk_c10 = sk_c2 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_111715,c_97218]) ).
tcf(c_111722,plain,
! [X0: $i] :
( ( sk_c10 = sk_c2 )
| ( multiply(sk_c5,multiply(sk_c8,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_111716,c_105]) ).
tcf(c_111799,plain,
! [X0: $i] : multiply(sk_c5,multiply(sk_c8,X0)) = multiply(sk_c11,X0),
inference(global_subsumption_just,[status(thm)],[c_111722,c_157,c_104,c_158,c_631,c_624,c_895,c_896,c_909,c_933,c_940,c_941,c_1185,c_1643,c_1645,c_1644,c_1650,c_1651,c_1653,c_1792,c_2245,c_2524,c_2512,c_3156,c_3237,c_3238,c_3239,c_3613,c_3844,c_4416,c_4463,c_5050,c_5218,c_5219,c_5979,c_5978,c_6937,c_7113,c_8161,c_10472,c_23328,c_24367,c_25921,c_25918,c_27319,c_27843,c_31557,c_34318,c_42003,c_49505,c_49529,c_50799,c_71572,c_71593,c_76009,c_80927,c_97217]) ).
tcf(c_111898,plain,
! [X0: $i] : multiply(sk_c6,multiply(sk_c7,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_111413,c_105]) ).
tcf(c_112132,plain,
! [X0: $i] : multiply(sk_c8,X0) = multiply(sk_c7,X0),
inference(light_normalisation,[status(thm)],[c_111362,c_111291]) ).
tcf(c_112252,plain,
! [X0: $i] : multiply(sk_c6,multiply(sk_c8,X0)) = multiply(sk_c11,X0),
inference(demodulation,[status(thm)],[c_111799,c_111368]) ).
tcf(c_112327,plain,
! [X0: $i] : multiply(sk_c11,X0) = X0,
inference(light_normalisation,[status(thm)],[c_111898,c_111345,c_112132,c_112252]) ).
tcf(c_112329,plain,
sk_c10 = sk_c3,
inference(demodulation,[status(thm)],[c_111410,c_112327]) ).
tcf(c_112330,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_112329,c_109954,c_107651,c_97217,c_97162,c_95487,c_67121,c_18322,c_14619,c_14618,c_11369,c_2687,c_2508,c_2162,c_2019,c_1564,c_1055,c_986,c_631]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP271-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.10/6.00 % Computer : n002.cluster.edu
% 0.10/6.00 % Model : x86_64 x86_64
% 0.10/6.00 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/6.00 % Memory : 8046.5625MB
% 0.10/6.00 % OS : Linux 6.8.0-71-generic
% 0.10/6.00 % CPULimit : 300
% 0.10/6.00 % WCLimit : 300
% 0.10/6.00 % DateTime : Wed Sep 23 14:22:42 UTC 2026
% 0.10/6.01 % CPUTime :
% 0.10/6.01 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/6.05 Running first-order theorem proving
% 0.15/6.05 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.15/6.06
% 0.15/6.06 % ======== iProver multi-core TPTP/SMT =========
% 0.15/6.06
% 0.15/6.06 % Detected problem language: tptp
% 0.15/6.07 % Proving...
% 43.26/17.04 % SZS status Started for theBenchmark.p
% 43.26/17.04 ERROR - "ProverProcess:heur/445550:16.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( sk_c9 != identity | ~iPr_def_10 )")
% 43.26/17.04 Fatal error: exception Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( sk_c9 != identity | ~iPr_def_10 )")
% 43.26/17.04 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode time_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 1.6084091637003026 --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd false --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red true --prep_gs_sim false --prep_res_sim true --prep_sem_filter neg --prep_sup_sim_all true --prep_sup_sim_sup true --prep_unflatten true --prep_upred false --preprocessing_flag true --prolific_symb_bound 32768 --prop_solver_per_cl 4096 --pure_diseq_elim false --res_backward_subs subset_subsumption --res_backward_subs_resolution false --res_forward_subs subset_subsumption --res_forward_subs_resolution false --res_lit_sel adaptive --res_lit_sel_side num_var --res_ordering kbo --res_passive_queue_type stack --res_passive_queues "[[-num_lits;+conj_symb;-num_symb];[-num_lits;+min_def_symb]]" --res_passive_queues_freq "[1;3]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input false --res_time_limit 202.19 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl true --splitting_grd true --splitting_mode input --splitting_nvd 16 --stats_out none --sub_typing false --subs_bck_mult 1 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[DemodLightNormLoopTriv;ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 640 --sup_share_score_frac 0.1 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.9903106699302947 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 5.33" --time_out_real 16.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_5h2wcexp/ogdux7sw 2>> /export/starexec/sandbox/tmp/iprover_out_5h2wcexp/ogdux7sw_error
% 43.26/17.04 % SZS status Unsatisfiable for theBenchmark.p
% 43.26/17.04
% 43.26/17.04 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 43.26/17.04
% 43.26/17.04 % ------ iProver source info
% 43.26/17.04
% 43.26/17.04 % git: date: 2026-07-19 20:42:38 +0200
% 43.26/17.04 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 43.26/17.04 % git: non_committed_changes: false
% 43.26/17.04
% 43.26/17.04 % ------ Parsing...% successful
% 43.26/17.04
% 43.26/17.04
% 43.26/17.04 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 43.26/17.04
% 43.26/17.04 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 43.26/17.04
% 43.26/17.04 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 43.26/17.04
% 43.26/17.04 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 43.26/17.04 % ------ Proving...
% 43.26/17.04 % ------ Problem Properties
% 43.26/17.04
% 43.26/17.04 %
% 43.26/17.04 % clauses 57
% 43.26/17.04 % conjectures 54
% 43.26/17.04 % EPR 0
% 43.26/17.04 % Horn 6
% 43.26/17.04 % unary 3
% 43.26/17.04 % binary 50
% 43.26/17.04 % lits 118
% 43.26/17.04 % lits eq 112
% 43.26/17.04 % fd_pure 0
% 43.26/17.04 % fd_pseudo 0
% 43.26/17.04 % fd_cond 0
% 43.26/17.04 % fd_pseudo_cond 0
% 43.26/17.04 % AC symbols 0
% 43.26/17.04
% 43.26/17.04 % ------ Input Options Time Limit: Unbounded
% 43.26/17.04
% 43.26/17.04
% 43.26/17.04 % ------
% 43.26/17.04 % Current options:
% 43.26/17.04 % ------
% 43.26/17.04
% 43.26/17.04
% 43.26/17.04 %
% 43.26/17.04
% 43.26/17.04 % ------ Proving...
% 43.26/17.04 %
% 43.26/17.04
% 43.26/17.04 % SZS status Unsatisfiable for theBenchmark.p
% 43.26/17.04
% 43.26/17.04 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 43.26/17.05
% 43.26/17.05
%------------------------------------------------------------------------------