%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP237-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 : n011.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:15 PM UTC 2026
% Result : Unsatisfiable 24.13s 25.25s
% Output : CNFRefutation 24.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 40
% Syntax : Number of formulae : 498 ( 71 unt; 0 def)
% Number of atoms : 1246 (1189 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1328 ( 580 ~; 748 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 355 ( 0 sgn 355 !; 0 ?; 320 :)
% 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_c4,sk_c5) = sk_c9
| inverse(sk_c9) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c9 = multiply(sk_c4,sk_c5)
| inverse(sk_c9) = sk_c8 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c4) = sk_c5
| inverse(sk_c9) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c5 = inverse(sk_c4)
| inverse(sk_c9) = sk_c8 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c9) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| inverse(sk_c9) = sk_c8 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c9) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| inverse(sk_c9) = sk_c8 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c9) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| inverse(sk_c9) = sk_c8 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c9) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c9 = inverse(sk_c6)
| inverse(sk_c9) = sk_c8 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c9 = multiply(sk_c4,sk_c5)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( inverse(sk_c4) = sk_c5
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c5 = inverse(sk_c4)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f28,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f30,plain,
( sk_c9 = multiply(sk_c4,sk_c5)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c5 = inverse(sk_c4)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f36,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f35]) ).
fof(f37,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f39]) ).
fof(f43,negated_conjecture,
( inverse(sk_c4) = sk_c5
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f44,plain,
( sk_c5 = inverse(sk_c4)
| sk_c8 = multiply(sk_c9,sk_c3) ),
inference(reorient_equations,[],[f43]) ).
fof(f47,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f48,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c8 = multiply(sk_c9,sk_c3) ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f50,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c8 = multiply(sk_c9,sk_c3) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c9 = inverse(sk_c6)
| sk_c8 = multiply(sk_c9,sk_c3) ),
inference(reorient_equations,[],[f51]) ).
fof(f55,negated_conjecture,
( inverse(sk_c4) = sk_c5
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c5 = inverse(sk_c4)
| sk_c3 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f55]) ).
fof(f59,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c3 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c3 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c9 = inverse(sk_c6)
| sk_c3 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c9 = multiply(sk_c4,sk_c5)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( inverse(sk_c4) = sk_c5
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f68,plain,
( sk_c5 = inverse(sk_c4)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f70,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f72,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f74,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
! [X2,X3,X0,X1,X6,X4,X5] :
( inverse(X6) != sk_c9
| multiply(X6,sk_c9) != X5
| multiply(sk_c9,X5) != sk_c8
| multiply(X4,sk_c8) != sk_c9
| inverse(X3) != X4
| multiply(X3,X4) != sk_c9
| inverse(X2) != sk_c9
| multiply(X2,sk_c9) != X1
| multiply(sk_c9,X1) != sk_c8
| multiply(X0,sk_c8) != sk_c9
| inverse(X0) != sk_c9
| inverse(sk_c9) != sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( sk_c9 != inverse(X6)
| multiply(X6,sk_c9) != X5
| sk_c8 != multiply(sk_c9,X5)
| sk_c9 != multiply(X4,sk_c8)
| inverse(X3) != X4
| sk_c9 != multiply(X3,X4)
| sk_c9 != inverse(X2)
| multiply(X2,sk_c9) != X1
| sk_c8 != multiply(sk_c9,X1)
| sk_c9 != multiply(X0,sk_c8)
| inverse(X0) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(reorient_equations,[],[f77]) ).
fof(f79,plain,
! [X2,X3,X0,X6,X4,X5] :
( sk_c9 != inverse(X6)
| multiply(X6,sk_c9) != X5
| sk_c8 != multiply(sk_c9,X5)
| sk_c9 != multiply(X4,sk_c8)
| inverse(X3) != X4
| sk_c9 != multiply(X3,X4)
| sk_c9 != inverse(X2)
| sk_c8 != multiply(sk_c9,multiply(X2,sk_c9))
| sk_c9 != multiply(X0,sk_c8)
| inverse(X0) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(equality_resolution,[],[f78]) ).
fof(f80,plain,
! [X2,X3,X0,X6,X5] :
( sk_c9 != inverse(X6)
| multiply(X6,sk_c9) != X5
| sk_c8 != multiply(sk_c9,X5)
| sk_c9 != multiply(inverse(X3),sk_c8)
| sk_c9 != multiply(X3,inverse(X3))
| sk_c9 != inverse(X2)
| sk_c8 != multiply(sk_c9,multiply(X2,sk_c9))
| sk_c9 != multiply(X0,sk_c8)
| inverse(X0) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(equality_resolution,[],[f79]) ).
fof(f81,plain,
! [X2,X3,X0,X6] :
( sk_c9 != inverse(X6)
| sk_c8 != multiply(sk_c9,multiply(X6,sk_c9))
| sk_c9 != multiply(inverse(X3),sk_c8)
| sk_c9 != multiply(X3,inverse(X3))
| sk_c9 != inverse(X2)
| sk_c8 != multiply(sk_c9,multiply(X2,sk_c9))
| sk_c9 != multiply(X0,sk_c8)
| inverse(X0) != sk_c9
| inverse(sk_c9) != sk_c8 ),
inference(equality_resolution,[],[f80]) ).
tcf(c_89,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_90,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_92,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c4,sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_93,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_94,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_95,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_96,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_97,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_98,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c4,sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_99,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c4) = sk_c5 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_100,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_101,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_102,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_103,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_104,negated_conjecture,
( ( multiply(sk_c1,sk_c8) = sk_c9 )
| ( multiply(sk_c4,sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_105,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c1,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_106,negated_conjecture,
( ( multiply(sk_c1,sk_c8) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_107,negated_conjecture,
( ( multiply(sk_c1,sk_c8) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_108,negated_conjecture,
( ( multiply(sk_c1,sk_c8) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c9,sk_c3) = sk_c8 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_113,negated_conjecture,
( ( multiply(sk_c9,sk_c3) = sk_c8 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_114,negated_conjecture,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c9,sk_c3) = sk_c8 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c9,sk_c3) = sk_c8 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c2,sk_c9) = sk_c3 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_119,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c3 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c3 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c3 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c4,sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c4) = sk_c5 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_128,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(sk_c9) != sk_c8 )
| ( inverse(X3) != sk_c9 )
| ( inverse(X2) != sk_c9 )
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c8) != sk_c9 )
| ( multiply(inverse(X1),sk_c8) != sk_c9 )
| ( multiply(X1,inverse(X1)) != sk_c9 )
| ( multiply(sk_c9,multiply(X3,sk_c9)) != sk_c8 )
| ( multiply(sk_c9,multiply(X2,sk_c9)) != sk_c8 ) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_129,plain,
multiply(identity,sk_c9) = sk_c9,
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_130,plain,
multiply(inverse(sk_c9),sk_c9) = identity,
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_305,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_128]) ).
tcf(c_306,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c8) != sk_c9 )
| ( multiply(X0,inverse(X0)) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_128]) ).
tcf(c_307,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(sk_c9,multiply(X0,sk_c9)) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_128]) ).
tcf(c_308,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c9) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_128]) ).
tcf(c_309,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_310,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_311,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_312,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_313,plain,
( ( inverse(sk_c9) = inverse(sk_c9) )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_315,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_309]) ).
tcf(c_513,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c9 )
| ( sk_c9 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_514,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c8) = sk_c9 )
| ( sk_c9 != X1 )
| ( multiply(inverse(X0),sk_c8) != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_516,plain,
! [X0: $i] :
( ( inverse(sk_c9) = sk_c8 )
| ( sk_c8 != X0 )
| ( inverse(sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_517,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( sk_c8 != sk_c9 )
| ( inverse(sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_516]) ).
tcf(c_531,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c9) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_535,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c9 )
| ( sk_c9 != inverse(X0) )
| ( inverse(X0) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_513]) ).
tcf(c_537,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_538,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c9 )
| ( sk_c9 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_513]) ).
tcf(c_539,plain,
( ( multiply(inverse(sk_c8),sk_c8) = sk_c9 )
| ( sk_c9 != identity )
| ( multiply(inverse(sk_c8),sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_514]) ).
tcf(c_542,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c8) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c8) != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_543,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c8) = sk_c9 )
| ( sk_c9 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c8) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_514]) ).
tcf(c_549,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( identity != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_551,plain,
! [X0: $i] :
( ( inverse(sk_c9) = X0 )
| ( X0 != inverse(sk_c9) )
| ( inverse(sk_c9) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_531]) ).
tcf(c_556,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != inverse(X0) )
| ( inverse(X0) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_537]) ).
tcf(c_559,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c8),sk_c8) = X0 )
| ( X0 != identity )
| ( multiply(inverse(sk_c8),sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_542]) ).
tcf(c_562,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(inverse(X0),sk_c8) = X3 )
| ( X3 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c8) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_542]) ).
tcf(c_564,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = inverse(X0) )
| ( sk_c9 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_567,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(inverse(X0),sk_c8) )
| ( sk_c9 != X1 )
| ( multiply(inverse(X0),sk_c8) != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_569,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_572,plain,
! [X0: $i,X1: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_573,plain,
( ( inverse(sk_c9) = multiply(identity,inverse(sk_c9)) )
| ( inverse(sk_c9) != inverse(sk_c9) )
| ( multiply(identity,inverse(sk_c9)) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_551]) ).
tcf(c_582,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c6) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c6) != X0 ) ),
inference(instantiation,[status(thm)],[c_537]) ).
tcf(c_589,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_593,plain,
( ( sk_c9 = inverse(sk_c6) )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c6) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_597,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = inverse(X0) )
| ( sk_c9 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_598,plain,
multiply(inverse(sk_c8),sk_c8) = identity,
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_604,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_609,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c9 = multiply(inverse(X0),sk_c8) )
| ( sk_c9 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c8) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_567]) ).
tcf(c_626,plain,
( ( sk_c9 = multiply(sk_c5,sk_c8) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c5,sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_569]) ).
tcf(c_629,plain,
! [X0: $i] :
( ( sk_c9 = multiply(identity,X0) )
| ( sk_c9 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_569]) ).
tcf(c_630,plain,
( ( sk_c9 = multiply(identity,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_636,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_637,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_569]) ).
tcf(c_640,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c8) = multiply(X1,X2) )
| ( sk_c8 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_312]) ).
tcf(c_642,plain,
sk_c8 = sk_c8,
inference(instantiation,[status(thm)],[c_309]) ).
tcf(c_644,plain,
! [X0: $i] :
( ( inverse(sk_c6) = X0 )
| ( X0 != inverse(sk_c6) )
| ( inverse(sk_c6) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_649,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != sk_c8 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_572]) ).
tcf(c_655,plain,
multiply(identity,inverse(sk_c9)) = inverse(sk_c9),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_671,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_589]) ).
tcf(c_679,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = X1 )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_680,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),X0) = X1 )
| ( X1 != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_687,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_636]) ).
tcf(c_691,plain,
! [X0: $i] :
( ( sk_c9 = sk_c8 )
| ( sk_c8 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_697,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c8),sk_c8) = multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c8),sk_c8) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_559]) ).
tcf(c_698,plain,
( ( multiply(inverse(sk_c8),sk_c8) = multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c8),sk_c8) != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_751,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c8) = sk_c9 )
| ( sk_c9 != multiply(identity,X1) )
| ( multiply(inverse(X0),sk_c8) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_543]) ).
tcf(c_752,plain,
( ( multiply(inverse(sk_c9),sk_c8) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(inverse(sk_c9),sk_c8) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_751]) ).
tcf(c_758,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(inverse(X0),sk_c8) )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c8) != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_764,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_604]) ).
tcf(c_765,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c8) = multiply(X1,sk_c8) )
| ( sk_c8 != sk_c8 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_640]) ).
tcf(c_801,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_808,plain,
( ( sk_c9 = inverse(sk_c9) )
| ( sk_c9 != sk_c8 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_809,plain,
! [X0: $i] :
( ( inverse(sk_c9) = X0 )
| ( X0 != sk_c8 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_537]) ).
tcf(c_839,plain,
( ( sk_c9 = inverse(sk_c1) )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_840,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( X0 != sk_c9 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_537]) ).
tcf(c_868,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c3) = X0 )
| ( X0 != sk_c8 )
| ( multiply(sk_c9,sk_c3) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_912,plain,
( ( inverse(sk_c9) = multiply(sk_c9,sk_c3) )
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c9,sk_c3) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_809]) ).
tcf(c_913,plain,
( ( inverse(sk_c9) = multiply(identity,sk_c8) )
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(identity,sk_c8) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_809]) ).
tcf(c_915,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_922,plain,
! [X0: $i] :
( ( inverse(sk_c1) = inverse(X0) )
| ( inverse(sk_c1) != sk_c9 )
| ( inverse(X0) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_840]) ).
tcf(c_925,plain,
( ( inverse(sk_c1) = identity )
| ( identity != sk_c9 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_840]) ).
tcf(c_932,plain,
inverse(sk_c6) = inverse(sk_c6),
inference(instantiation,[status(thm)],[c_309]) ).
tcf(c_944,plain,
( ( inverse(sk_c9) = sk_c9 )
| ( sk_c9 != multiply(identity,inverse(sk_c9)) )
| ( inverse(sk_c9) != multiply(identity,inverse(sk_c9)) ) ),
inference(instantiation,[status(thm)],[c_513]) ).
tcf(c_1042,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c6) )
| ( X1 != X0 )
| ( inverse(sk_c6) != X0 ) ),
inference(instantiation,[status(thm)],[c_604]) ).
tcf(c_1050,plain,
! [X0: $i] :
( ( inverse(sk_c6) = identity )
| ( identity != X0 )
| ( inverse(sk_c6) != X0 ) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_1051,plain,
( ( inverse(sk_c6) = identity )
| ( identity != sk_c9 )
| ( inverse(sk_c6) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1050]) ).
tcf(c_1081,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(X0,X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_89,c_91]) ).
tcf(c_1082,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_90,c_91]) ).
tcf(c_1117,plain,
! [X0: $i] :
( ( sk_c9 = inverse(X0) )
| ( sk_c9 != inverse(sk_c6) )
| ( inverse(X0) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_597]) ).
tcf(c_1118,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c9 )
| ( sk_c9 != inverse(sk_c6) )
| ( inverse(X0) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_538]) ).
tcf(c_1120,plain,
( ( sk_c9 = inverse(sk_c9) )
| ( sk_c9 != inverse(sk_c6) )
| ( inverse(sk_c9) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1117]) ).
tcf(c_1160,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c8),sk_c8) = X1 )
| ( X1 != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c8),sk_c8) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_562]) ).
tcf(c_1252,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = inverse(X1) )
| ( inverse(X1) != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_679]) ).
tcf(c_1260,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(identity,X0) = X2 )
| ( X2 != X1 )
| ( multiply(identity,X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_1274,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),X0) = multiply(identity,X1) )
| ( multiply(identity,X1) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_680]) ).
tcf(c_1275,plain,
( ( multiply(inverse(sk_c9),sk_c9) = multiply(identity,sk_c9) )
| ( multiply(identity,sk_c9) != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_1274]) ).
tcf(c_1281,plain,
( ( sk_c8 = multiply(sk_c9,sk_c7) )
| ( sk_c8 != sk_c8 )
| ( multiply(sk_c9,sk_c7) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_1286,plain,
! [X0: $i] :
( ( sk_c8 = multiply(identity,X0) )
| ( sk_c8 != sk_c8 )
| ( multiply(identity,X0) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_1293,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c8),sk_c8) )
| ( X0 != identity )
| ( multiply(inverse(sk_c8),sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_758]) ).
tcf(c_1300,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(inverse(X0),sk_c8) )
| ( X3 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c8) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_758]) ).
tcf(c_1301,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(identity,X0) )
| ( sk_c9 != multiply(identity,X1) )
| ( multiply(identity,X0) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_801]) ).
tcf(c_1336,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X2) = multiply(inverse(X1),sk_c8) )
| ( X2 != sk_c8 )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_312]) ).
tcf(c_1337,plain,
( ( multiply(sk_c9,sk_c9) = multiply(inverse(sk_c9),sk_c8) )
| ( sk_c9 != sk_c8 )
| ( sk_c9 != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1336]) ).
tcf(c_1360,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(X0,X1) )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_1365,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(identity,sk_c9) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_124,c_1081]) ).
tcf(c_1368,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(identity,sk_c8) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_125,c_1081]) ).
tcf(c_1397,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X1,X2) = multiply(inverse(sk_c8),sk_c8) )
| ( multiply(X1,X2) != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c8),sk_c8) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_687]) ).
tcf(c_1398,plain,
( ( multiply(sk_c9,sk_c9) = multiply(inverse(sk_c8),sk_c8) )
| ( multiply(sk_c9,sk_c9) != multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c8),sk_c8) != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1397]) ).
tcf(c_1432,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_309]) ).
tcf(c_1434,plain,
( ( multiply(inverse(sk_c4),sk_c8) = multiply(sk_c5,sk_c8) )
| ( sk_c8 != sk_c8 )
| ( inverse(sk_c4) != sk_c5 ) ),
inference(instantiation,[status(thm)],[c_765]) ).
tcf(c_1547,plain,
multiply(identity,sk_c8) = sk_c8,
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_1635,plain,
( ( multiply(sk_c9,sk_c3) = inverse(sk_c9) )
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c9,sk_c3) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_868]) ).
tcf(c_1656,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(inverse(sk_c6),sk_c7) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_102,c_1082]) ).
tcf(c_1657,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(inverse(sk_c6),sk_c7) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_96,c_1082]) ).
tcf(c_1658,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(sk_c1),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_109,c_1082]) ).
tcf(c_1659,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(inverse(sk_c1),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_105,c_1082]) ).
tcf(c_1662,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(sk_c2),sk_c3) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_121,c_1082]) ).
tcf(c_1663,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(inverse(sk_c2),sk_c3) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_117,c_1082]) ).
tcf(c_1664,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_89,c_1082]) ).
tcf(c_1665,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_90,c_1082]) ).
tcf(c_1685,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c1),sk_c8) = multiply(X0,sk_c8) )
| ( sk_c8 != sk_c8 )
| ( inverse(sk_c1) != X0 ) ),
inference(instantiation,[status(thm)],[c_765]) ).
tcf(c_1690,plain,
( ( multiply(inverse(sk_c1),sk_c8) = multiply(sk_c9,sk_c8) )
| ( sk_c8 != sk_c8 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1685]) ).
tcf(c_1775,plain,
! [X0: $i] :
( ( sk_c9 = sk_c8 )
| ( sk_c8 != inverse(X0) )
| ( sk_c9 != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_691]) ).
tcf(c_1787,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(sk_c6) )
| ( inverse(sk_c6) != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1042]) ).
tcf(c_1791,plain,
! [X0: $i] :
( ( sk_c8 = inverse(sk_c6) )
| ( sk_c8 != X0 )
| ( inverse(sk_c6) != X0 ) ),
inference(instantiation,[status(thm)],[c_1042]) ).
tcf(c_1803,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != inverse(sk_c6) )
| ( inverse(X0) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_764]) ).
tcf(c_1806,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = inverse(sk_c6) )
| ( inverse(sk_c6) != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_1042]) ).
tcf(c_1880,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c6) = multiply(X0,X1) )
| ( inverse(sk_c6) != inverse(sk_c6) )
| ( multiply(X0,X1) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_644]) ).
tcf(c_2082,plain,
( ( inverse(sk_c4) = sk_c5 )
| ~ iPr_def_10
| ( inverse(sk_c1) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_305,c_105]) ).
tcf(c_2083,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c1) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_305,c_109]) ).
tcf(c_2084,plain,
( ( multiply(sk_c4,sk_c5) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c1) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_305,c_104]) ).
tcf(c_2086,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c1) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_305,c_107]) ).
tcf(c_2153,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c6) )
| ( X0 != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_2186,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = identity )
| ( identity != X1 )
| ( multiply(identity,X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1260]) ).
tcf(c_2225,plain,
( ( sk_c9 = sk_c8 )
| ( sk_c8 != multiply(sk_c9,sk_c7) )
| ( sk_c9 != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_691]) ).
tcf(c_2227,plain,
! [X0: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != multiply(sk_c9,sk_c7) )
| ( X0 != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_915]) ).
tcf(c_2228,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != multiply(sk_c9,sk_c7) )
| ( X0 != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_572]) ).
tcf(c_2230,plain,
( ( sk_c8 = sk_c9 )
| ( sk_c8 != multiply(sk_c9,sk_c7) )
| ( sk_c9 != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_2228]) ).
tcf(c_2266,plain,
( ( inverse(sk_c4) = sk_c5 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_2082,c_99,c_2082]) ).
tcf(c_2276,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_2083,c_103,c_2083]) ).
tcf(c_2292,plain,
( ( multiply(sk_c4,sk_c5) = sk_c9 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_2084,c_98,c_2084]) ).
tcf(c_2342,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c9,sk_c3) = X0 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_310,c_111]) ).
tcf(c_2343,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c9,sk_c3) = X0 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_310,c_115]) ).
tcf(c_2344,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c3) = X0 )
| ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_310,c_113]) ).
tcf(c_2366,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X1) = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_310,c_89]) ).
tcf(c_2371,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_310,c_309]) ).
tcf(c_2372,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_310,c_311]) ).
tcf(c_2382,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c4),sk_c8) = X0 )
| ( X0 != multiply(sk_c5,sk_c8) )
| ( multiply(inverse(sk_c4),sk_c8) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_562]) ).
tcf(c_2383,plain,
( ( multiply(inverse(sk_c4),sk_c8) = sk_c9 )
| ( sk_c9 != multiply(sk_c5,sk_c8) )
| ( multiply(inverse(sk_c4),sk_c8) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_2382]) ).
tcf(c_2496,plain,
( ( inverse(sk_c1) = inverse(sk_c6) )
| ( inverse(sk_c1) != sk_c9 )
| ( inverse(sk_c6) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_922]) ).
tcf(c_2628,plain,
( ( multiply(sk_c4,sk_c5) = sk_c9 )
| ( multiply(inverse(sk_c1),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_104,c_1082]) ).
tcf(c_2654,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(inverse(sk_c1),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_106,c_1082]) ).
tcf(c_2655,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(inverse(sk_c1),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_107,c_1082]) ).
tcf(c_2670,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(inverse(sk_c1),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_108,c_1082]) ).
tcf(c_2731,plain,
! [X0: $i] :
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c1,multiply(sk_c8,X0)) = multiply(sk_c9,X0) ) ),
inference(superposition,[status(thm)],[c_108,c_91]) ).
tcf(c_2732,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(sk_c1,multiply(sk_c8,X0)) = multiply(sk_c9,X0) ) ),
inference(superposition,[status(thm)],[c_107,c_91]) ).
tcf(c_2733,plain,
! [X0: $i] :
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c1,multiply(sk_c8,X0)) = multiply(sk_c9,X0) ) ),
inference(superposition,[status(thm)],[c_106,c_91]) ).
tcf(c_2734,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c5) = sk_c9 )
| ( multiply(sk_c1,multiply(sk_c8,X0)) = multiply(sk_c9,X0) ) ),
inference(superposition,[status(thm)],[c_104,c_91]) ).
tcf(c_2741,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(X0,X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_89,c_91]) ).
tcf(c_2773,plain,
( ( sk_c8 = multiply(identity,sk_c8) )
| ( sk_c8 != sk_c8 )
| ( multiply(identity,sk_c8) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1286]) ).
tcf(c_2836,plain,
( ( identity = multiply(inverse(sk_c8),sk_c8) )
| ( identity != identity )
| ( multiply(inverse(sk_c8),sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_1293]) ).
tcf(c_2991,plain,
multiply(identity,sk_c9) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_1365,c_129]) ).
tcf(c_2994,plain,
multiply(inverse(identity),sk_c9) = sk_c9,
inference(superposition,[status(thm)],[c_2991,c_1082]) ).
tcf(c_2995,plain,
multiply(identity,sk_c8) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_1368,c_1547]) ).
tcf(c_2997,plain,
! [X0: $i] : multiply(identity,multiply(sk_c8,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_2995,c_91]) ).
tcf(c_2998,plain,
multiply(inverse(identity),sk_c8) = sk_c8,
inference(superposition,[status(thm)],[c_2995,c_1082]) ).
tcf(c_3007,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(inverse(sk_c2),sk_c3) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_119,c_1082]) ).
tcf(c_3040,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(sk_c8),sk_c8) = multiply(X1,X2) )
| ( multiply(X1,X2) != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c8),sk_c8) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_1160]) ).
tcf(c_3041,plain,
( ( multiply(inverse(sk_c8),sk_c8) = multiply(sk_c9,sk_c9) )
| ( multiply(sk_c9,sk_c9) != multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c8),sk_c8) != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_3040]) ).
tcf(c_3043,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(inverse(sk_c2),sk_c3) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_120,c_1082]) ).
tcf(c_3046,plain,
( ( multiply(identity,sk_c9) = inverse(sk_c6) )
| ( inverse(sk_c6) != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1252]) ).
tcf(c_3080,plain,
( ~ iPr_def_10
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c8)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_90,c_305]) ).
tcf(c_3082,plain,
( ~ iPr_def_10
| ( sk_c9 != sk_c8 )
| ( inverse(identity) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_2995,c_305]) ).
tcf(c_3128,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = multiply(identity,X1) )
| ( multiply(identity,X1) != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_679]) ).
tcf(c_3251,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ~ iPr_def_12
| ( inverse(sk_c2) != sk_c9 )
| ( multiply(sk_c9,sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_120,c_307]) ).
tcf(c_3252,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ~ iPr_def_12
| ( inverse(sk_c2) != sk_c9 )
| ( multiply(sk_c9,sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_119,c_307]) ).
tcf(c_3255,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c2) != sk_c9 )
| ( multiply(sk_c9,sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_121,c_307]) ).
tcf(c_3256,plain,
( ( inverse(sk_c4) = sk_c5 )
| ~ iPr_def_12
| ( inverse(sk_c2) != sk_c9 )
| ( multiply(sk_c9,sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_117,c_307]) ).
tcf(c_3345,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(sk_c6) = multiply(X0,X1) )
| ( inverse(sk_c6) != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_3410,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,X1) )
| ( X2 != inverse(sk_c6) )
| ( multiply(X0,X1) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1360]) ).
tcf(c_3411,plain,
( ( sk_c9 = multiply(sk_c9,sk_c9) )
| ( sk_c9 != inverse(sk_c6) )
| ( multiply(sk_c9,sk_c9) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_3410]) ).
tcf(c_3482,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X2) = multiply(inverse(X1),X1) )
| ( X2 != X1 )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_312]) ).
tcf(c_3483,plain,
( ( multiply(sk_c9,sk_c9) = multiply(inverse(sk_c9),sk_c9) )
| ( sk_c9 != sk_c9 )
| ( sk_c9 != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_3482]) ).
tcf(c_3713,plain,
( ( identity = multiply(sk_c4,sk_c5) )
| ( identity != identity )
| ( multiply(sk_c4,sk_c5) != identity ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_3720,plain,
! [X0: $i] :
( ( identity = multiply(inverse(X0),X0) )
| ( identity != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_3721,plain,
( ( identity = multiply(inverse(sk_c9),sk_c9) )
| ( identity != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_3720]) ).
tcf(c_3755,plain,
multiply(identity,sk_c9) = sk_c9,
inference(superposition,[status(thm)],[c_2994,c_2741]) ).
tcf(c_3943,plain,
( ( sk_c9 = inverse(sk_c9) )
| ( sk_c9 != multiply(sk_c9,sk_c3) )
| ( inverse(sk_c9) != multiply(sk_c9,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_4001,plain,
( ( sk_c9 = sk_c8 )
| ( sk_c8 != multiply(sk_c9,sk_c3) )
| ( sk_c9 != multiply(sk_c9,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_691]) ).
tcf(c_4143,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( sk_c9 != inverse(sk_c2) )
| ( inverse(sk_c2) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_535]) ).
tcf(c_4195,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X0,X2) = X4 )
| ( X4 != multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_312,c_310]) ).
tcf(c_4245,plain,
( ( sk_c5 = inverse(sk_c4) )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_2371,c_93]) ).
tcf(c_4246,plain,
( ( sk_c5 = inverse(sk_c4) )
| ~ iPr_def_10 ),
inference(resolution,[status(thm)],[c_2371,c_2266]) ).
tcf(c_4258,plain,
( ( sk_c9 = inverse(sk_c6) )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_2371,c_97]) ).
tcf(c_4259,plain,
( ( sk_c9 = inverse(sk_c6) )
| ~ iPr_def_10 ),
inference(resolution,[status(thm)],[c_2371,c_2276]) ).
tcf(c_4270,plain,
( ( sk_c8 = multiply(sk_c9,sk_c3) )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2371,c_115]) ).
tcf(c_4280,plain,
( ( sk_c9 = inverse(sk_c2) )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2371,c_127]) ).
tcf(c_4378,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = inverse(sk_c9) )
| ( inverse(sk_c9) != multiply(identity,sk_c8) )
| ( multiply(X0,X1) != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_687]) ).
tcf(c_4379,plain,
( ( multiply(sk_c9,sk_c9) = inverse(sk_c9) )
| ( inverse(sk_c9) != multiply(identity,sk_c8) )
| ( multiply(sk_c9,sk_c9) != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_4378]) ).
tcf(c_4496,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(inverse(sk_c1),sk_c8) )
| ( X1 != multiply(X0,sk_c8) )
| ( multiply(inverse(sk_c1),sk_c8) != multiply(X0,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1300]) ).
tcf(c_4508,plain,
( ( multiply(inverse(sk_c1),sk_c8) = multiply(identity,sk_c8) )
| ( sk_c8 != sk_c8 )
| ( inverse(sk_c1) != identity ) ),
inference(instantiation,[status(thm)],[c_1685]) ).
tcf(c_4731,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c1) )
| ( X0 != inverse(sk_c6) )
| ( inverse(sk_c1) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1803]) ).
tcf(c_5121,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c8 )
| ( sk_c8 != multiply(identity,sk_c8) )
| ( multiply(X0,X1) != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_687]) ).
tcf(c_5122,plain,
( ( multiply(sk_c9,sk_c9) = sk_c8 )
| ( sk_c8 != multiply(identity,sk_c8) )
| ( multiply(sk_c9,sk_c9) != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_5121]) ).
tcf(c_5268,plain,
( ( sk_c9 = identity )
| ( identity != multiply(inverse(sk_c8),sk_c8) )
| ( sk_c9 != multiply(inverse(sk_c8),sk_c8) ) ),
inference(instantiation,[status(thm)],[c_549]) ).
tcf(c_5271,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != multiply(inverse(sk_c8),sk_c8) )
| ( X0 != multiply(inverse(sk_c8),sk_c8) ) ),
inference(instantiation,[status(thm)],[c_589]) ).
tcf(c_6193,plain,
inverse(sk_c2) = inverse(sk_c2),
inference(instantiation,[status(thm)],[c_309]) ).
tcf(c_6520,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(identity,X1) = X2 )
| ( X2 != X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2366,c_310]) ).
tcf(c_6595,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c9,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_99,c_1659]) ).
tcf(c_6959,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c5 = inverse(sk_c4) ) ),
inference(resolution,[status(thm)],[c_4245,c_308]) ).
tcf(c_7032,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 = inverse(sk_c6) ) ),
inference(resolution,[status(thm)],[c_4258,c_308]) ).
tcf(c_7268,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c9,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_6595,c_89]) ).
tcf(c_7328,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c9,sk_c3) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_127,c_1662]) ).
tcf(c_7418,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = inverse(sk_c6) )
| ( inverse(sk_c6) != sk_c8 )
| ( multiply(X0,X1) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1806]) ).
tcf(c_7419,plain,
( ( multiply(sk_c9,sk_c9) = inverse(sk_c6) )
| ( inverse(sk_c6) != sk_c8 )
| ( multiply(sk_c9,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_7418]) ).
tcf(c_7529,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c9,sk_c3) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_7328,c_89]) ).
tcf(c_7612,plain,
! [X0: $i] :
( ( sk_c9 = multiply(identity,inverse(sk_c9)) )
| ( sk_c9 != multiply(identity,X0) )
| ( multiply(identity,inverse(sk_c9)) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_1301]) ).
tcf(c_7613,plain,
( ( sk_c9 = multiply(identity,inverse(sk_c9)) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(identity,inverse(sk_c9)) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_7612]) ).
tcf(c_7632,plain,
( ( sk_c9 = inverse(sk_c2) )
| ( sk_c9 = inverse(sk_c6) ) ),
inference(resolution,[status(thm)],[c_4280,c_2371]) ).
tcf(c_7907,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),multiply(identity,X1)) = multiply(multiply(identity,X0),X1),
inference(superposition,[status(thm)],[c_1665,c_91]) ).
tcf(c_7945,plain,
multiply(identity,sk_c8) = sk_c8,
inference(superposition,[status(thm)],[c_2998,c_2741]) ).
tcf(c_8034,plain,
! [X0: $i] : multiply(inverse(inverse(identity)),X0) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1664,c_1082]) ).
tcf(c_8058,plain,
multiply(identity,inverse(identity)) = identity,
inference(superposition,[status(thm)],[c_8034,c_90]) ).
tcf(c_8086,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_8058,c_89]) ).
tcf(c_8097,plain,
( ~ iPr_def_10
| ( sk_c9 != identity )
| ( sk_c9 != sk_c8 ) ),
inference(superposition,[status(thm)],[c_8086,c_3082]) ).
tcf(c_8644,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(multiply(identity,X0),X1),
inference(superposition,[status(thm)],[c_89,c_7907]) ).
tcf(c_9146,plain,
! [X0: $i] :
( ( inverse(sk_c6) = multiply(identity,X0) )
| ( inverse(sk_c6) != inverse(sk_c6) )
| ( multiply(identity,X0) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1880]) ).
tcf(c_9147,plain,
( ( inverse(sk_c6) = multiply(identity,sk_c9) )
| ( inverse(sk_c6) != inverse(sk_c6) )
| ( multiply(identity,sk_c9) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_9146]) ).
tcf(c_9491,plain,
! [X0: $i] :
( ( multiply(identity,X0) = identity )
| ( identity != multiply(sk_c4,sk_c5) )
| ( multiply(identity,X0) != multiply(sk_c4,sk_c5) ) ),
inference(instantiation,[status(thm)],[c_2186]) ).
tcf(c_9492,plain,
( ( multiply(identity,sk_c9) = identity )
| ( identity != multiply(sk_c4,sk_c5) )
| ( multiply(identity,sk_c9) != multiply(sk_c4,sk_c5) ) ),
inference(instantiation,[status(thm)],[c_9491]) ).
tcf(c_10080,plain,
! [X0: $i] :
( ( multiply(identity,inverse(sk_c9)) = multiply(identity,X0) )
| ( multiply(identity,X0) != inverse(sk_c9) )
| ( multiply(identity,inverse(sk_c9)) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_3128]) ).
tcf(c_10081,plain,
( ( multiply(identity,inverse(sk_c9)) = multiply(identity,sk_c9) )
| ( multiply(identity,sk_c9) != inverse(sk_c9) )
| ( multiply(identity,inverse(sk_c9)) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_10080]) ).
tcf(c_10737,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c9,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_103,c_1658]) ).
tcf(c_10999,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( identity != multiply(inverse(X0),X0) )
| ( sk_c9 != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_549]) ).
tcf(c_11000,plain,
( ( sk_c9 = identity )
| ( identity != multiply(inverse(sk_c9),sk_c9) )
| ( sk_c9 != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_10999]) ).
tcf(c_11009,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != multiply(inverse(X1),X1) )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(instantiation,[status(thm)],[c_589]) ).
tcf(c_11010,plain,
( ( identity = sk_c9 )
| ( identity != multiply(inverse(sk_c9),sk_c9) )
| ( sk_c9 != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_11009]) ).
tcf(c_11307,plain,
! [X0: $i] : multiply(multiply(identity,X0),inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_8644,c_90]) ).
tcf(c_12087,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_89,c_11307]) ).
tcf(c_12412,plain,
( ( sk_c8 = multiply(inverse(sk_c1),sk_c8) )
| ( sk_c8 != multiply(identity,sk_c8) )
| ( multiply(inverse(sk_c1),sk_c8) != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_4496]) ).
tcf(c_12649,plain,
! [X0: $i] :
( ( inverse(X0) = multiply(sk_c9,sk_c3) )
| ( inverse(X0) != inverse(X0) )
| ( multiply(sk_c9,sk_c3) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_556]) ).
tcf(c_12657,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c9,sk_c3) )
| ( X1 != inverse(X0) )
| ( multiply(sk_c9,sk_c3) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1360]) ).
tcf(c_12735,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_2086,c_101,c_2086]) ).
tcf(c_12745,plain,
( ( sk_c8 = multiply(sk_c9,sk_c7) )
| ~ iPr_def_10 ),
inference(resolution,[status(thm)],[c_12735,c_2371]) ).
tcf(c_13999,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c9,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_10737,c_7945]) ).
tcf(c_14465,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(X2) )
| ( X2 != X1 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2372,c_311]) ).
tcf(c_14505,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(X1) = multiply(sk_c9,sk_c3) )
| ( X1 != X0 )
| ( inverse(X0) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_2372,c_2342]) ).
tcf(c_14506,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(X1) = multiply(sk_c9,sk_c3) )
| ( X1 != X0 )
| ( inverse(X0) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_2372,c_2343]) ).
tcf(c_14507,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c9) = multiply(sk_c9,sk_c3) )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_14506]) ).
tcf(c_14508,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c9) = multiply(sk_c9,sk_c3) )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_14505]) ).
tcf(c_14657,plain,
( ( sk_c9 = sk_c8 )
| ( sk_c8 != inverse(sk_c6) )
| ( sk_c9 != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1775]) ).
tcf(c_14940,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c6) = multiply(X0,X1) )
| ( inverse(sk_c6) != sk_c8 )
| ( multiply(X0,X1) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_3345]) ).
tcf(c_14941,plain,
( ( inverse(sk_c6) = multiply(sk_c9,sk_c9) )
| ( inverse(sk_c6) != sk_c8 )
| ( multiply(sk_c9,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_14940]) ).
tcf(c_14960,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c6) = multiply(X0,X1) )
| ( inverse(sk_c6) != multiply(sk_c9,sk_c3) )
| ( multiply(X0,X1) != multiply(sk_c9,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_3345]) ).
tcf(c_14961,plain,
( ( inverse(sk_c6) = multiply(sk_c9,sk_c9) )
| ( inverse(sk_c6) != multiply(sk_c9,sk_c3) )
| ( multiply(sk_c9,sk_c9) != multiply(sk_c9,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_14960]) ).
tcf(c_15668,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(sk_c9,sk_c3) )
| ( inverse(X0) != multiply(sk_c9,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_1787]) ).
tcf(c_15669,plain,
( ( inverse(sk_c9) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(sk_c9,sk_c3) )
| ( inverse(sk_c9) != multiply(sk_c9,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_15668]) ).
tcf(c_16000,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( multiply(inverse(X0),sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_12087,c_306]) ).
tcf(c_16026,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( multiply(inverse(sk_c9),sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_16000]) ).
tcf(c_16109,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(sk_c9,sk_c3) )
| ( multiply(X0,X1) != multiply(sk_c9,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_1806]) ).
tcf(c_16110,plain,
( ( multiply(sk_c9,sk_c9) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(sk_c9,sk_c3) )
| ( multiply(sk_c9,sk_c9) != multiply(sk_c9,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_16109]) ).
tcf(c_17312,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(sk_c9),sk_c8) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_13999,c_1082]) ).
tcf(c_18404,plain,
! [X0: $i] :
( ( inverse(sk_c6) = multiply(sk_c9,sk_c3) )
| ( inverse(sk_c6) != X0 )
| ( multiply(sk_c9,sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_3345]) ).
tcf(c_18405,plain,
( ( inverse(sk_c6) = multiply(sk_c9,sk_c3) )
| ( inverse(sk_c6) != sk_c9 )
| ( multiply(sk_c9,sk_c3) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_18404]) ).
tcf(c_18584,plain,
! [X0: $i,X1: $i] :
( ( inverse(X1) = multiply(sk_c9,sk_c3) )
| ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( X1 != X0 )
| ( inverse(X0) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_2344,c_2372]) ).
tcf(c_18585,plain,
( ( inverse(sk_c9) = multiply(sk_c9,sk_c3) )
| ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_18584]) ).
tcf(c_18784,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(sk_c6) )
| ( X2 != multiply(X0,X1) )
| ( inverse(sk_c6) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_1042]) ).
tcf(c_18997,plain,
( ( sk_c9 = identity )
| ( identity != inverse(sk_c1) )
| ( sk_c9 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_549]) ).
tcf(c_19613,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c5 = inverse(sk_c4) ) ),
inference(global_subsumption_just,[status(thm)],[c_6959,c_4246,c_6959]) ).
tcf(c_19641,plain,
( iPr_def_12
| iPr_def_11
| ( inverse(sk_c4) = sk_c5 ) ),
inference(resolution,[status(thm)],[c_19613,c_2371]) ).
tcf(c_19721,plain,
( ( sk_c9 = inverse(sk_c6) )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_7032,c_115,c_315,c_593,c_3255,c_4143,c_4259,c_6193,c_7032,c_7632]) ).
tcf(c_19722,plain,
( iPr_def_11
| ( sk_c9 = inverse(sk_c6) ) ),
inference(renaming,[status(thm)],[c_19721]) ).
tcf(c_19731,plain,
( iPr_def_11
| ( inverse(sk_c6) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_19722,c_2371]) ).
tcf(c_19733,plain,
! [X0: $i] :
( iPr_def_11
| ( inverse(X0) = sk_c9 )
| ( X0 != sk_c6 ) ),
inference(resolution,[status(thm)],[c_19722,c_2372]) ).
tcf(c_20041,plain,
( ( identity = inverse(sk_c1) )
| ( identity != inverse(sk_c6) )
| ( inverse(sk_c1) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_4731]) ).
tcf(c_20273,plain,
( ( inverse(sk_c4) = sk_c5 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_19641,c_123,c_111,c_3256,c_19641]) ).
tcf(c_20274,plain,
( iPr_def_11
| ( inverse(sk_c4) = sk_c5 ) ),
inference(renaming,[status(thm)],[c_20273]) ).
tcf(c_20641,plain,
! [X0: $i,X1: $i] :
( ( identity = multiply(X0,X1) )
| ( identity != multiply(inverse(sk_c8),sk_c8) )
| ( multiply(X0,X1) != multiply(inverse(sk_c8),sk_c8) ) ),
inference(instantiation,[status(thm)],[c_5271]) ).
tcf(c_20642,plain,
( ( identity = multiply(sk_c9,sk_c9) )
| ( identity != multiply(inverse(sk_c8),sk_c8) )
| ( multiply(sk_c9,sk_c9) != multiply(inverse(sk_c8),sk_c8) ) ),
inference(instantiation,[status(thm)],[c_20641]) ).
tcf(c_21427,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != multiply(inverse(X2),sk_c8) )
| ( multiply(X0,X1) != multiply(inverse(X2),sk_c8) ) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_21428,plain,
( ( sk_c9 = multiply(sk_c9,sk_c9) )
| ( sk_c9 != multiply(inverse(sk_c9),sk_c8) )
| ( multiply(sk_c9,sk_c9) != multiply(inverse(sk_c9),sk_c8) ) ),
inference(instantiation,[status(thm)],[c_21427]) ).
tcf(c_21797,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),multiply(identity,X1)) = multiply(multiply(identity,X0),X1),
inference(superposition,[status(thm)],[c_1665,c_91]) ).
tcf(c_22492,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c9,sk_c7) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_97,c_1657]) ).
tcf(c_22515,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c9,sk_c7) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_22492,c_3755]) ).
tcf(c_22546,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c9,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_99,c_1659]) ).
tcf(c_22565,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c9,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_22546,c_89]) ).
tcf(c_22610,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(inverse(sk_c9),sk_c8) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_22565,c_1082]) ).
tcf(c_22697,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c9,sk_c3) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_123,c_1663]) ).
tcf(c_22722,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c9,sk_c3) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_22697,c_3755]) ).
tcf(c_22818,plain,
( ( sk_c9 = sk_c8 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_22515,c_95]) ).
tcf(c_23512,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(multiply(identity,X0),X1),
inference(superposition,[status(thm)],[c_89,c_21797]) ).
tcf(c_24627,plain,
! [X0: $i] : multiply(multiply(identity,X0),inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_23512,c_90]) ).
tcf(c_24768,plain,
! [X0: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != multiply(inverse(sk_c1),sk_c8) )
| ( X0 != multiply(inverse(sk_c1),sk_c8) ) ),
inference(instantiation,[status(thm)],[c_915]) ).
tcf(c_24858,plain,
( ( inverse(sk_c6) = multiply(sk_c9,sk_c3) )
| ( inverse(sk_c6) != inverse(sk_c6) )
| ( multiply(sk_c9,sk_c3) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_12649]) ).
tcf(c_25140,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(inverse(X0),sk_c8) )
| ( sk_c9 != multiply(identity,X1) )
| ( multiply(inverse(X0),sk_c8) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_801]) ).
tcf(c_25141,plain,
( ( sk_c9 = multiply(inverse(sk_c9),sk_c8) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(inverse(sk_c9),sk_c8) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_25140]) ).
tcf(c_25510,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(X2,X3) = multiply(sk_c9,sk_c3) )
| ( X3 != X1 )
| ( X2 != X0 )
| ( multiply(X0,X1) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_4195,c_2342]) ).
tcf(c_25512,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(X2,X3) = multiply(sk_c9,sk_c3) )
| ( X3 != X1 )
| ( X2 != X0 )
| ( multiply(X0,X1) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_4195,c_2344]) ).
tcf(c_25513,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(sk_c9,sk_c9) = multiply(sk_c9,sk_c3) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c9,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_25512]) ).
tcf(c_25515,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c9,sk_c9) = multiply(sk_c9,sk_c3) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c9,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_25510]) ).
tcf(c_25544,plain,
! [X0: $i] :
( ( sk_c9 = multiply(sk_c9,sk_c3) )
| ( sk_c9 != X0 )
| ( multiply(sk_c9,sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_569]) ).
tcf(c_25545,plain,
( ( sk_c9 = multiply(sk_c9,sk_c3) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c9,sk_c3) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_25544]) ).
tcf(c_26074,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_89,c_24627]) ).
tcf(c_26130,plain,
! [X0: $i] : multiply(identity,multiply(X0,inverse(X0))) = identity,
inference(superposition,[status(thm)],[c_24627,c_91]) ).
tcf(c_27058,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(inverse(sk_c8),sk_c8) )
| ( sk_c9 != multiply(X0,X1) )
| ( multiply(inverse(sk_c8),sk_c8) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_609]) ).
tcf(c_27059,plain,
( ( sk_c9 = multiply(inverse(sk_c8),sk_c8) )
| ( sk_c9 != multiply(sk_c9,sk_c9) )
| ( multiply(inverse(sk_c8),sk_c8) != multiply(sk_c9,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_27058]) ).
tcf(c_27397,plain,
( ( sk_c9 = sk_c8 )
| ( multiply(sk_c9,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_22818,c_26074]) ).
tcf(c_27400,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_103,c_26074]) ).
tcf(c_27401,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_99,c_26074]) ).
tcf(c_27558,plain,
( ( sk_c8 = identity )
| ( identity != sk_c8 )
| ( sk_c8 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_30864,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( sk_c8 != multiply(sk_c9,sk_c7) )
| ( inverse(sk_c6) != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_2227]) ).
tcf(c_32151,plain,
inverse(sk_c6) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_27400,c_129,c_130,c_97,c_315,c_598,c_630,c_698,c_752,c_1337,c_1432,c_2836,c_3041,c_3483,c_3943,c_4001,c_4270,c_5268,c_7529,c_14507,c_16026,c_17312,c_19731,c_21428,c_25141,c_25545,c_27059]) ).
tcf(c_32155,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_32151,c_1656]) ).
tcf(c_32341,plain,
inverse(sk_c4) = sk_c5,
inference(global_subsumption_just,[status(thm)],[c_27401,c_129,c_130,c_97,c_93,c_315,c_593,c_598,c_630,c_698,c_752,c_1337,c_1432,c_2836,c_3041,c_3411,c_3483,c_3943,c_4001,c_4270,c_5268,c_7268,c_7529,c_14507,c_14508,c_16026,c_16110,c_17312,c_18405,c_19731,c_20274,c_21428,c_22610,c_22722,c_25141,c_25515,c_25545,c_27059]) ).
tcf(c_32346,plain,
multiply(sk_c4,sk_c5) = identity,
inference(superposition,[status(thm)],[c_32341,c_26074]) ).
tcf(c_32352,plain,
( ~ iPr_def_11
| ( multiply(sk_c4,sk_c5) != sk_c9 )
| ( multiply(inverse(sk_c4),sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_32341,c_306]) ).
tcf(c_32599,plain,
multiply(sk_c8,inverse(sk_c8)) = identity,
inference(superposition,[status(thm)],[c_26130,c_2997]) ).
tcf(c_32661,plain,
! [X0: $i] :
( ( sk_c9 = multiply(sk_c9,sk_c7) )
| ( sk_c9 != multiply(identity,X0) )
| ( multiply(sk_c9,sk_c7) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_801]) ).
tcf(c_32662,plain,
( ( sk_c9 = multiply(sk_c9,sk_c7) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(sk_c9,sk_c7) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_32661]) ).
tcf(c_33058,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( multiply(inverse(sk_c8),sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_32599,c_306]) ).
tcf(c_33363,plain,
! [X0: $i] :
( ( X0 != sk_c6 )
| ( inverse(X0) = sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_19733,c_129,c_130,c_97,c_315,c_593,c_598,c_630,c_698,c_752,c_1118,c_1337,c_1432,c_2153,c_2836,c_3041,c_3483,c_3943,c_4001,c_4270,c_5268,c_7529,c_14507,c_16026,c_17312,c_19731,c_21428,c_25141,c_25545,c_27059]) ).
tcf(c_33364,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c9 )
| ( X0 != sk_c6 ) ),
inference(renaming,[status(thm)],[c_33363]) ).
tcf(c_34169,plain,
! [X0: $i,X1: $i] :
( ( identity = inverse(sk_c6) )
| ( identity != multiply(X0,X1) )
| ( inverse(sk_c6) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_18784]) ).
tcf(c_34170,plain,
( ( identity = inverse(sk_c6) )
| ( identity != multiply(sk_c9,sk_c9) )
| ( inverse(sk_c6) != multiply(sk_c9,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_34169]) ).
tcf(c_34209,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c3) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(X0,X1) )
| ( multiply(sk_c9,sk_c3) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_18784]) ).
tcf(c_36676,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(inverse(X0),X0) )
| ( sk_c9 != multiply(identity,X1) )
| ( multiply(inverse(X0),X0) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_801]) ).
tcf(c_36681,plain,
( ( sk_c9 = multiply(inverse(sk_c9),sk_c9) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_36676]) ).
tcf(c_40185,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c7) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(X0,X1) )
| ( multiply(sk_c9,sk_c7) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_18784]) ).
tcf(c_41499,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c3) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(identity,X0) )
| ( multiply(sk_c9,sk_c3) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_34209]) ).
tcf(c_41500,plain,
( ( multiply(sk_c9,sk_c3) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(identity,sk_c9) )
| ( multiply(sk_c9,sk_c3) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_41499]) ).
tcf(c_42819,plain,
! [X0: $i] :
( ( multiply(identity,X0) = multiply(sk_c4,sk_c5) )
| ~ iPr_def_10
| ( sk_c9 != X0 ) ),
inference(resolution,[status(thm)],[c_6520,c_2292]) ).
tcf(c_42824,plain,
( ( multiply(identity,sk_c9) = multiply(sk_c4,sk_c5) )
| ~ iPr_def_10
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_42819]) ).
tcf(c_44191,plain,
( ( identity = multiply(sk_c9,sk_c8) )
| ( identity != identity )
| ( multiply(sk_c9,sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_44231,plain,
( ( identity = sk_c8 )
| ( identity != multiply(inverse(sk_c1),sk_c8) )
| ( sk_c8 != multiply(inverse(sk_c1),sk_c8) ) ),
inference(instantiation,[status(thm)],[c_24768]) ).
tcf(c_48452,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c7) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c9,sk_c7) != X0 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_51814,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c7) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(identity,X0) )
| ( multiply(sk_c9,sk_c7) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_40185]) ).
tcf(c_51815,plain,
( ( multiply(sk_c9,sk_c7) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(identity,sk_c9) )
| ( multiply(sk_c9,sk_c7) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_51814]) ).
tcf(c_52096,plain,
( ( sk_c8 = inverse(sk_c6) )
| ( sk_c8 != identity )
| ( inverse(sk_c6) != identity ) ),
inference(instantiation,[status(thm)],[c_1791]) ).
tcf(c_53717,plain,
( ( inverse(sk_c6) = multiply(sk_c9,sk_c7) )
| ( inverse(sk_c6) != inverse(sk_c6) )
| ( multiply(sk_c9,sk_c7) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1880]) ).
tcf(c_54257,plain,
( ( identity = multiply(inverse(sk_c1),sk_c8) )
| ( identity != multiply(sk_c9,sk_c8) )
| ( multiply(inverse(sk_c1),sk_c8) != multiply(sk_c9,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_4496]) ).
tcf(c_54773,negated_conjecture,
( iPr_def_12
| iPr_def_11
| ( inverse(sk_c9) != sk_c8 ) ),
inference(global_subsumption_just,[status(thm)],[c_308,c_129,c_130,c_97,c_315,c_308,c_593,c_598,c_630,c_642,c_698,c_752,c_925,c_1051,c_1275,c_1337,c_1432,c_1547,c_1690,c_2225,c_2773,c_2836,c_3041,c_3483,c_3713,c_3721,c_3943,c_4001,c_4270,c_4508,c_5268,c_7529,c_8097,c_9492,c_11000,c_11010,c_12412,c_12745,c_14507,c_14657,c_16026,c_17312,c_19731,c_21428,c_25141,c_25545,c_27059,c_27397,c_27558,c_32155,c_32346,c_32662,c_36681,c_42824,c_44191,c_44231,c_52096,c_54257]) ).
tcf(c_54775,negated_conjecture,
inverse(sk_c4) = sk_c5,
inference(global_subsumption_just,[status(thm)],[c_93,c_129,c_130,c_97,c_93,c_315,c_593,c_598,c_630,c_698,c_752,c_1337,c_1432,c_2836,c_3041,c_3411,c_3483,c_3943,c_4001,c_4270,c_5268,c_7268,c_7529,c_14507,c_14508,c_16026,c_16110,c_17312,c_18405,c_19731,c_20274,c_21428,c_22610,c_22722,c_25141,c_25515,c_25545,c_27059]) ).
tcf(c_54777,negated_conjecture,
inverse(sk_c6) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_97,c_129,c_130,c_97,c_315,c_598,c_630,c_698,c_752,c_1337,c_1432,c_2836,c_3041,c_3483,c_3943,c_4001,c_4270,c_5268,c_7529,c_14507,c_16026,c_17312,c_19731,c_21428,c_25141,c_25545,c_27059]) ).
tcf(c_54780,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm)],[c_54777,c_90]) ).
tcf(c_54836,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_3080,c_129,c_130,c_97,c_315,c_593,c_598,c_630,c_642,c_698,c_752,c_925,c_1051,c_1275,c_1337,c_1432,c_1547,c_1690,c_2225,c_2773,c_2836,c_3041,c_3483,c_3713,c_3721,c_3943,c_4001,c_4270,c_4508,c_5268,c_7529,c_8097,c_9492,c_11000,c_11010,c_12412,c_12745,c_14507,c_14657,c_16026,c_17312,c_19731,c_21428,c_25141,c_25545,c_27059,c_27397,c_27558,c_32155,c_32346,c_32662,c_36681,c_42824,c_44191,c_44231,c_52096,c_54257]) ).
tcf(c_54871,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_54780,c_91]) ).
tcf(c_54878,plain,
multiply(inverse(sk_c5),identity) = multiply(identity,sk_c4),
inference(superposition,[status(thm)],[c_54775,c_1665]) ).
tcf(c_54881,plain,
! [X0: $i] : multiply(inverse(sk_c5),multiply(identity,X0)) = multiply(multiply(identity,sk_c4),X0),
inference(superposition,[status(thm)],[c_54878,c_91]) ).
tcf(c_54890,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_126,c_54871]) ).
tcf(c_54892,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c9,sk_c7) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_96,c_54871]) ).
tcf(c_54895,plain,
( ~ iPr_def_12
| ( inverse(sk_c6) != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_54871,c_307]) ).
tcf(c_54899,plain,
! [X0: $i] : multiply(multiply(identity,sk_c4),X0) = multiply(inverse(sk_c5),X0),
inference(superposition,[status(thm)],[c_89,c_54881]) ).
tcf(c_55009,plain,
! [X0: $i] : multiply(inverse(inverse(identity)),X0) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1664,c_1082]) ).
tcf(c_55033,plain,
multiply(identity,inverse(identity)) = identity,
inference(superposition,[status(thm)],[c_55009,c_90]) ).
tcf(c_55045,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( multiply(inverse(identity),sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_55033,c_306]) ).
tcf(c_55047,plain,
! [X0: $i] : multiply(inverse(sk_c5),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_89,c_54899]) ).
tcf(c_55051,plain,
! [X0: $i] : multiply(identity,multiply(sk_c4,X0)) = multiply(inverse(sk_c5),X0),
inference(superposition,[status(thm)],[c_54899,c_91]) ).
tcf(c_55087,plain,
multiply(sk_c4,sk_c5) = identity,
inference(superposition,[status(thm)],[c_55047,c_90]) ).
tcf(c_55104,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_55087,c_122]) ).
tcf(c_55105,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_55087,c_98]) ).
tcf(c_55373,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_54890,c_89]) ).
tcf(c_55901,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(inverse(sk_c5),sk_c5) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_92,c_55051]) ).
tcf(c_56168,plain,
( ( sk_c9 = sk_c8 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_55373,c_125]) ).
tcf(c_56461,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(identity,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_55901,c_90]) ).
tcf(c_57725,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c4,sk_c5) = sk_c9 )
| ( multiply(sk_c9,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_55105,c_2628]) ).
tcf(c_57749,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c9,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_55105,c_2654]) ).
tcf(c_58017,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(sk_c9,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_55105,c_2655]) ).
tcf(c_58275,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c9,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_55105,c_2670]) ).
tcf(c_58626,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c9,sk_c7) = identity ) ),
inference(superposition,[status(thm)],[c_56461,c_54892]) ).
tcf(c_58912,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = multiply(sk_c9,sk_c3) )
| ( multiply(sk_c9,sk_c3) != inverse(X2) )
| ( multiply(X0,X1) != inverse(X2) ) ),
inference(instantiation,[status(thm)],[c_12657]) ).
tcf(c_58913,plain,
( ( multiply(sk_c9,sk_c9) = multiply(sk_c9,sk_c3) )
| ( multiply(sk_c9,sk_c3) != inverse(sk_c9) )
| ( multiply(sk_c9,sk_c9) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_58912]) ).
tcf(c_64958,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c7) = sk_c6 )
| ( sk_c6 != X0 )
| ( multiply(sk_c9,sk_c7) != X0 ) ),
inference(instantiation,[status(thm)],[c_48452]) ).
tcf(c_76159,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c9,sk_c3) = multiply(identity,sk_c9) )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_55104,c_3007]) ).
tcf(c_76623,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c9,sk_c3) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_55104,c_3043]) ).
tcf(c_76805,plain,
! [X0: $i] :
( ( inverse(sk_c9) = sk_c8 )
| ( inverse(X0) = inverse(multiply(sk_c9,sk_c7)) )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_14465,c_95]) ).
tcf(c_79716,plain,
( ( multiply(sk_c9,sk_c7) = sk_c6 )
| ( sk_c6 != identity )
| ( multiply(sk_c9,sk_c7) != identity ) ),
inference(instantiation,[status(thm)],[c_64958]) ).
tcf(c_85560,plain,
( ~ iPr_def_12
| ( multiply(identity,sk_c9) != sk_c8 ) ),
inference(global_subsumption_just,[status(thm)],[c_54895,c_129,c_130,c_97,c_315,c_598,c_630,c_698,c_752,c_1337,c_1432,c_2836,c_3041,c_3483,c_3943,c_4001,c_4270,c_5268,c_7529,c_14507,c_16026,c_17312,c_19731,c_21428,c_25141,c_25545,c_27059,c_54895]) ).
tcf(c_85571,plain,
( ~ iPr_def_12
| ( sk_c9 != sk_c8 ) ),
inference(superposition,[status(thm)],[c_3755,c_85560]) ).
tcf(c_86036,plain,
( ~ iPr_def_11
| ( sk_c9 != identity ) ),
inference(global_subsumption_just,[status(thm)],[c_55045,c_539,c_598,c_33058]) ).
tcf(c_89050,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(global_subsumption_just,[status(thm)],[c_2731,c_129,c_130,c_97,c_126,c_102,c_96,c_114,c_315,c_593,c_598,c_630,c_698,c_752,c_839,c_912,c_913,c_932,c_1120,c_1337,c_1398,c_1432,c_1547,c_1635,c_2496,c_2836,c_3041,c_3046,c_3251,c_3483,c_3943,c_4001,c_4270,c_4379,c_5268,c_7529,c_9147,c_14507,c_14961,c_15669,c_16026,c_17312,c_18997,c_19731,c_20041,c_20642,c_21428,c_24858,c_25141,c_25545,c_27059,c_34170,c_41500,c_54773,c_58275,c_58913,c_76623,c_86036]) ).
tcf(c_89067,plain,
( ~ iPr_def_12
| ( inverse(sk_c6) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_89050,c_307]) ).
tcf(c_89069,plain,
multiply(sk_c9,sk_c7) = multiply(identity,sk_c9),
inference(superposition,[status(thm)],[c_89050,c_54871]) ).
tcf(c_89071,plain,
~ iPr_def_12,
inference(global_subsumption_just,[status(thm)],[c_89067,c_129,c_130,c_97,c_113,c_315,c_598,c_630,c_698,c_752,c_1337,c_1432,c_2836,c_3041,c_3252,c_3483,c_3943,c_4001,c_4270,c_5268,c_7529,c_14507,c_16026,c_17312,c_19731,c_21428,c_25141,c_25545,c_27059,c_56168,c_85571,c_89067]) ).
tcf(c_89075,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_2732,c_129,c_130,c_97,c_101,c_95,c_113,c_315,c_593,c_598,c_630,c_642,c_698,c_752,c_839,c_932,c_1120,c_1337,c_1398,c_1432,c_1547,c_2496,c_2773,c_2836,c_3041,c_3046,c_3252,c_3483,c_3943,c_4001,c_4270,c_5122,c_5268,c_7529,c_9147,c_14507,c_14961,c_15669,c_16026,c_17312,c_18585,c_18997,c_19731,c_20041,c_20642,c_21428,c_24858,c_25141,c_25513,c_25545,c_27059,c_34170,c_41500,c_54773,c_56168,c_58017,c_76159,c_85571,c_86036,c_89067]) ).
tcf(c_89097,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_2733,c_129,c_130,c_97,c_101,c_100,c_95,c_94,c_113,c_315,c_593,c_598,c_630,c_642,c_698,c_752,c_808,c_839,c_932,c_1120,c_1281,c_1337,c_1398,c_1432,c_1547,c_2225,c_2496,c_2773,c_2836,c_3041,c_3046,c_3252,c_3483,c_3943,c_4001,c_4270,c_5122,c_5268,c_7529,c_9147,c_14507,c_14941,c_14961,c_15669,c_16026,c_17312,c_18585,c_18997,c_19731,c_20041,c_20642,c_21428,c_24858,c_25141,c_25513,c_25545,c_27059,c_30864,c_32662,c_34170,c_41500,c_51815,c_53717,c_54773,c_56168,c_57749,c_58017,c_76159,c_85571,c_86036,c_89069,c_89067]) ).
tcf(c_89110,plain,
multiply(sk_c4,sk_c5) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_2734,c_129,c_130,c_92,c_315,c_308,c_593,c_598,c_630,c_642,c_698,c_808,c_932,c_1281,c_1432,c_1547,c_2225,c_2773,c_2836,c_3041,c_3046,c_3411,c_3483,c_5122,c_5268,c_7419,c_9147,c_27059,c_30864,c_32151,c_32662,c_51815,c_53717,c_54836,c_57725,c_86036,c_89069,c_89071,c_89075]) ).
tcf(c_89121,plain,
sk_c9 = identity,
inference(superposition,[status(thm)],[c_89110,c_55087]) ).
tcf(c_89982,plain,
! [X0: $i] :
( ( X0 != sk_c8 )
| ( inverse(X0) = inverse(multiply(sk_c9,sk_c7)) ) ),
inference(global_subsumption_just,[status(thm)],[c_76805,c_129,c_130,c_97,c_93,c_101,c_95,c_92,c_113,c_315,c_308,c_593,c_598,c_626,c_630,c_642,c_698,c_752,c_808,c_839,c_925,c_932,c_1051,c_1120,c_1275,c_1281,c_1337,c_1398,c_1432,c_1434,c_1547,c_1690,c_2225,c_2383,c_2496,c_2773,c_2836,c_3041,c_3046,c_3252,c_3411,c_3483,c_3713,c_3721,c_3943,c_4001,c_4270,c_4508,c_5122,c_5268,c_7268,c_7419,c_7529,c_8097,c_9147,c_9492,c_11000,c_11010,c_12412,c_12745,c_14507,c_14508,c_14657,c_14961,c_15669,c_16026,c_16110,c_17312,c_18405,c_18585,c_18997,c_19731,c_20041,c_20274,c_20642,c_21428,c_22610,c_22722,c_24858,c_25141,c_25513,c_25515,c_25545,c_27059,c_27397,c_27558,c_30864,c_32155,c_32346,c_32352,c_32662,c_34170,c_36681,c_41500,c_42824,c_44191,c_44231,c_51815,c_52096,c_53717,c_54257,c_54773,c_56168,c_57725,c_58017,c_76159,c_76805,c_85571,c_86036,c_89069,c_89067,c_89097]) ).
tcf(c_89983,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(multiply(sk_c9,sk_c7)) )
| ( X0 != sk_c8 ) ),
inference(renaming,[status(thm)],[c_89982]) ).
tcf(c_89999,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = inverse(X1) )
| ( X1 != sk_c8 )
| ( inverse(multiply(sk_c9,sk_c7)) != X0 ) ),
inference(resolution,[status(thm)],[c_89983,c_6520]) ).
tcf(c_93010,plain,
! [X0: $i] :
( ( multiply(identity,sk_c9) = inverse(X0) )
| ( X0 != sk_c8 )
| ( multiply(sk_c9,sk_c7) != sk_c6 ) ),
inference(resolution,[status(thm)],[c_89999,c_33364]) ).
tcf(c_93011,plain,
( ( multiply(identity,sk_c9) = inverse(sk_c9) )
| ( sk_c9 != sk_c8 )
| ( multiply(sk_c9,sk_c7) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_93010]) ).
tcf(c_140006,negated_conjecture,
inverse(sk_c6) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_97,c_129,c_130,c_97,c_315,c_598,c_630,c_698,c_752,c_1337,c_1432,c_2836,c_3041,c_3483,c_3943,c_4001,c_4270,c_5268,c_7529,c_14507,c_16026,c_17312,c_19731,c_21428,c_25141,c_25545,c_27059]) ).
tcf(c_140011,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm)],[c_140006,c_90]) ).
tcf(c_140016,plain,
! [X0: $i] : multiply(sk_c9,X0) = X0,
inference(superposition,[status(thm)],[c_89121,c_89]) ).
tcf(c_140090,plain,
sk_c6 = identity,
inference(superposition,[status(thm)],[c_140016,c_140011]) ).
tcf(c_140092,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_140090,c_93011,c_89110,c_89097,c_89075,c_89071,c_89069,c_79716,c_58626,c_54773,c_32662,c_32352,c_32341,c_10081,c_7613,c_2383,c_2230,c_2225,c_1434,c_1281,c_944,c_655,c_642,c_630,c_626,c_573,c_517,c_315,c_313,c_129]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP237-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.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/20.94 % CPULimit : 300
% 0.10/20.94 % WCLimit : 300
% 0.10/20.94 % DateTime : Wed Sep 23 14:13:18 UTC 2026
% 0.10/20.94 % CPUTime :
% 0.10/20.94 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/20.97 Running first-order theorem proving
% 0.10/20.97 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.10/20.99
% 0.10/20.99 % ======== iProver multi-core TPTP/SMT =========
% 0.10/20.99
% 0.10/20.99 % Detected problem language: tptp
% 0.10/21.00 % Proving...
% 24.13/25.25 % SZS status Started for theBenchmark.p
% 24.13/25.25 % SZS status Unsatisfiable for theBenchmark.p
% 24.13/25.25
% 24.13/25.25 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 24.13/25.25
% 24.13/25.25 % ------ iProver source info
% 24.13/25.25
% 24.13/25.25 % git: date: 2026-07-19 20:42:38 +0200
% 24.13/25.25 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 24.13/25.25 % git: non_committed_changes: false
% 24.13/25.25
% 24.13/25.25 % ------ Parsing...% successful
% 24.13/25.25
% 24.13/25.25
% 24.13/25.25 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 24.13/25.25
% 24.13/25.25 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 24.13/25.25
% 24.13/25.25 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 24.13/25.25
% 24.13/25.25 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 24.13/25.25 % ------ Proving...
% 24.13/25.25 % ------ Problem Properties
% 24.13/25.25
% 24.13/25.25 %
% 24.13/25.25 % clauses 43
% 24.13/25.25 % conjectures 40
% 24.13/25.25 % EPR 0
% 24.13/25.25 % Horn 6
% 24.13/25.25 % unary 3
% 24.13/25.25 % binary 36
% 24.13/25.25 % lits 88
% 24.13/25.25 % lits eq 82
% 24.13/25.25 % fd_pure 0
% 24.13/25.25 % fd_pseudo 0
% 24.13/25.25 % fd_cond 0
% 24.13/25.25 % fd_pseudo_cond 0
% 24.13/25.25 % AC symbols 0
% 24.13/25.25
% 24.13/25.25 % ------ Input Options Time Limit: Unbounded
% 24.13/25.25
% 24.13/25.25
% 24.13/25.25 % ------
% 24.13/25.25 % Current options:
% 24.13/25.25 % ------
% 24.13/25.25
% 24.13/25.25
% 24.13/25.25 %
% 24.13/25.25
% 24.13/25.25 % ------ Proving...
% 24.13/25.25 %
% 24.13/25.25
% 24.13/25.25 % SZS status Unsatisfiable for theBenchmark.p
% 24.13/25.25
% 24.13/25.25 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 24.13/25.26
% 24.13/25.26
%------------------------------------------------------------------------------