%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP313-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n006.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:48 PM UTC 2026
% Result : Unsatisfiable 25.82s 5.20s
% Output : CNFRefutation 25.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 50
% Syntax : Number of formulae : 479 ( 76 unt; 0 def)
% Number of atoms : 1118 (1048 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 1088 ( 449 ~; 639 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 3 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 : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 243 ( 0 sgn 243 !; 0 ?; 225 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c8 = multiply(sk_c4,sk_c9)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c4) = sk_c9
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c9 = inverse(sk_c4)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c7
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c7 = multiply(sk_c5,sk_c8)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c8 = inverse(sk_c5)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c7 = inverse(sk_c6)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c8 = multiply(sk_c4,sk_c9)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( inverse(sk_c4) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c9 = inverse(sk_c4)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c7
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c7 = multiply(sk_c5,sk_c8)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c8 = inverse(sk_c5)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f25]) ).
fof(f29,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f30,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c7 = inverse(sk_c6)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( multiply(sk_c4,sk_c9) = sk_c8
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c8 = multiply(sk_c4,sk_c9)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( inverse(sk_c4) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f36,plain,
( sk_c9 = inverse(sk_c4)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f35]) ).
fof(f39,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f39]) ).
fof(f45,negated_conjecture,
( inverse(sk_c6) = sk_c7
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c7 = inverse(sk_c6)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f45]) ).
fof(f49,negated_conjecture,
( inverse(sk_c4) = sk_c9
| multiply(sk_c2,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_23) ).
fof(f50,plain,
( sk_c9 = inverse(sk_c4)
| sk_c7 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c7 = multiply(sk_c5,sk_c8)
| sk_c7 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c8 = inverse(sk_c5)
| sk_c7 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f53]) ).
fof(f59,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c7 = inverse(sk_c6)
| sk_c7 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( multiply(sk_c4,sk_c9) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c8 = multiply(sk_c4,sk_c9)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( inverse(sk_c4) = sk_c9
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c9 = inverse(sk_c4)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c7 = multiply(sk_c5,sk_c8)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f68,plain,
( sk_c8 = inverse(sk_c5)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_33) ).
fof(f70,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f72,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c6) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_35) ).
fof(f74,plain,
( sk_c7 = inverse(sk_c6)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( multiply(sk_c4,sk_c9) = sk_c8
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c8 = multiply(sk_c4,sk_c9)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
( inverse(sk_c4) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
( sk_c9 = inverse(sk_c4)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f77]) ).
fof(f79,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c7
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_38) ).
fof(f80,plain,
( sk_c7 = multiply(sk_c5,sk_c8)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f79]) ).
fof(f81,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_39) ).
fof(f82,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_40) ).
fof(f84,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_41) ).
fof(f86,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c7 = inverse(sk_c6)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( multiply(sk_c4,sk_c9) = sk_c8
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_43) ).
fof(f90,plain,
( sk_c8 = multiply(sk_c4,sk_c9)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,negated_conjecture,
( inverse(sk_c4) = sk_c9
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_44) ).
fof(f92,plain,
( sk_c9 = inverse(sk_c4)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f91]) ).
fof(f93,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c7
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_45) ).
fof(f94,plain,
( sk_c7 = multiply(sk_c5,sk_c8)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f93]) ).
fof(f95,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_46) ).
fof(f96,plain,
( sk_c8 = inverse(sk_c5)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f95]) ).
fof(f97,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_47) ).
fof(f98,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f97]) ).
fof(f99,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_48) ).
fof(f100,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f99]) ).
fof(f101,negated_conjecture,
( inverse(sk_c6) = sk_c7
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_49) ).
fof(f102,plain,
( sk_c7 = inverse(sk_c6)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f101]) ).
fof(f103,negated_conjecture,
! [X2,X3,X0,X1,X4,X5] :
( inverse(X5) != sk_c7
| multiply(X5,sk_c7) != sk_c9
| multiply(sk_c7,sk_c9) != sk_c8
| inverse(X4) != sk_c8
| multiply(X4,sk_c8) != sk_c7
| inverse(X3) != sk_c9
| multiply(X3,sk_c9) != sk_c8
| inverse(X2) != sk_c8
| multiply(X2,sk_c8) != sk_c9
| inverse(X1) != sk_c8
| multiply(X1,sk_c8) != sk_c7
| inverse(X0) != sk_c9
| multiply(X0,sk_c9) != sk_c8
| multiply(sk_c8,sk_c9) != sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_50) ).
fof(f104,plain,
! [X2,X3,X0,X1,X4,X5] :
( sk_c7 != inverse(X5)
| sk_c9 != multiply(X5,sk_c7)
| sk_c8 != multiply(sk_c7,sk_c9)
| sk_c8 != inverse(X4)
| sk_c7 != multiply(X4,sk_c8)
| sk_c9 != inverse(X3)
| sk_c8 != multiply(X3,sk_c9)
| sk_c8 != inverse(X2)
| sk_c9 != multiply(X2,sk_c8)
| sk_c8 != inverse(X1)
| sk_c7 != multiply(X1,sk_c8)
| inverse(X0) != sk_c9
| sk_c8 != multiply(X0,sk_c9)
| multiply(sk_c8,sk_c9) != sk_c7 ),
inference(reorient_equations,[],[f103]) ).
tcf(c_102,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_103,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_105,negated_conjecture,
( ( multiply(sk_c4,sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_107,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_109,negated_conjecture,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_110,negated_conjecture,
( ( multiply(sk_c6,sk_c7) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_112,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c4,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_114,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_117,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c6,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_118,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c4,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_120,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c2,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_128,negated_conjecture,
( ( multiply(sk_c2,sk_c8) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c4,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_135,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c6,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_140,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c9 )
| ( multiply(sk_c4,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c3,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_142,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_143,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_144,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c9 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_145,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c9 )
| ( multiply(sk_c6,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c4,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_148,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_150,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_152,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c6,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_153,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_154,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(X5) != sk_c7 )
| ( inverse(X4) != sk_c8 )
| ( inverse(X3) != sk_c8 )
| ( inverse(X2) != sk_c8 )
| ( inverse(X1) != sk_c9 )
| ( inverse(X0) != sk_c9 )
| ( multiply(sk_c7,sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 )
| ( multiply(X5,sk_c7) != sk_c9 )
| ( multiply(X4,sk_c8) != sk_c9 )
| ( multiply(X3,sk_c8) != sk_c7 )
| ( multiply(X2,sk_c8) != sk_c7 )
| ( multiply(X1,sk_c9) != sk_c8 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_155,plain,
multiply(identity,sk_c8) = sk_c8,
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_393,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_154]) ).
tcf(c_394,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_154]) ).
tcf(c_395,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_154]) ).
tcf(c_396,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_154]) ).
tcf(c_397,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c7,sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_154]) ).
tcf(c_398,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_399,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_400,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_401,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_404,plain,
sk_c8 = sk_c8,
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_669,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c7 )
| ( sk_c7 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_671,plain,
( ~ iPr_def_12
| ( inverse(sk_c4) != sk_c9 )
| ( multiply(sk_c4,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_395]) ).
tcf(c_673,plain,
( ~ iPr_def_10
| ( inverse(sk_c5) != sk_c8 )
| ( multiply(sk_c5,sk_c8) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_393]) ).
tcf(c_674,plain,
( ~ iPr_def_13
| ( inverse(sk_c6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_396]) ).
tcf(c_676,plain,
! [X0: $i] :
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( sk_c7 != X0 )
| ( multiply(sk_c8,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_677,plain,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( sk_c7 != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_676]) ).
tcf(c_702,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c8,sk_c9) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c8,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_703,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( sk_c7 != multiply(X0,X1) )
| ( multiply(sk_c8,sk_c9) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_676]) ).
tcf(c_710,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_720,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( sk_c7 != sk_c8 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_669]) ).
tcf(c_729,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(sk_c8,sk_c9) = X2 )
| ( X2 != multiply(X0,X1) )
| ( multiply(sk_c8,sk_c9) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_702]) ).
tcf(c_732,plain,
! [X0: $i] :
( ( inverse(sk_c5) = X0 )
| ( X0 != sk_c8 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_710]) ).
tcf(c_733,plain,
! [X0: $i] :
( ( inverse(sk_c6) = X0 )
| ( X0 != sk_c7 )
| ( inverse(sk_c6) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_710]) ).
tcf(c_737,plain,
! [X0: $i] :
( ( sk_c7 = multiply(sk_c8,sk_c9) )
| ( sk_c7 != X0 )
| ( multiply(sk_c8,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_743,plain,
! [X0: $i] :
( ( sk_c9 = sk_c8 )
| ( sk_c9 != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_744,plain,
! [X0: $i] :
( ( sk_c9 = sk_c7 )
| ( sk_c7 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_746,plain,
! [X0: $i] :
( ( sk_c7 = sk_c9 )
| ( sk_c7 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_747,plain,
( ( sk_c7 = sk_c9 )
| ( sk_c7 != sk_c8 )
| ( sk_c9 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_746]) ).
tcf(c_748,plain,
! [X0: $i] :
( ( sk_c7 = sk_c8 )
| ( sk_c7 != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_749,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c7 = multiply(X0,X1) )
| ( sk_c7 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_751,plain,
! [X0: $i,X1: $i] :
( ( sk_c8 = inverse(X0) )
| ( sk_c8 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_757,plain,
! [X0: $i,X1: $i] :
( ( sk_c7 = inverse(X0) )
| ( sk_c7 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_762,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c8,sk_c9) )
| ( X1 != X0 )
| ( multiply(sk_c8,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_763,plain,
( ( sk_c8 = multiply(sk_c8,sk_c9) )
| ( sk_c8 != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_762]) ).
tcf(c_770,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_774,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c5) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c5) != X0 ) ),
inference(instantiation,[status(thm)],[c_710]) ).
tcf(c_775,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c7 )
| ( sk_c7 != X0 )
| ( inverse(sk_c5) != X0 ) ),
inference(instantiation,[status(thm)],[c_669]) ).
tcf(c_780,plain,
( ( inverse(sk_c6) = multiply(sk_c5,sk_c8) )
| ( inverse(sk_c6) != sk_c7 )
| ( multiply(sk_c5,sk_c8) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_786,plain,
( ( sk_c7 = multiply(sk_c8,sk_c9) )
| ( sk_c7 != sk_c7 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_737]) ).
tcf(c_787,plain,
! [X0: $i,X1: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_789,plain,
( ( sk_c8 = inverse(sk_c5) )
| ( sk_c8 != sk_c8 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_751]) ).
tcf(c_797,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c8,sk_c9) = multiply(X0,X1) )
| ( sk_c9 != X1 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_400]) ).
tcf(c_800,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_808,plain,
! [X0: $i] :
( ( sk_c7 = inverse(X0) )
| ( sk_c7 != sk_c7 )
| ( inverse(X0) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_757]) ).
tcf(c_816,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_832,plain,
multiply(sk_c8,sk_c9) = multiply(sk_c8,sk_c9),
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_843,plain,
! [X0: $i] :
( ( inverse(sk_c5) = multiply(sk_c8,sk_c9) )
| ( inverse(sk_c5) != X0 )
| ( multiply(sk_c8,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_774]) ).
tcf(c_877,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(sk_c8,sk_c9) )
| ( X2 != multiply(X0,X1) )
| ( multiply(sk_c8,sk_c9) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_762]) ).
tcf(c_888,plain,
sk_c7 = sk_c7,
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_898,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_905,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c8,sk_c9) )
| ( X1 != sk_c9 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_400]) ).
tcf(c_907,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_800]) ).
tcf(c_914,plain,
! [X0: $i] :
( ( multiply(sk_c8,sk_c9) = multiply(X0,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_797]) ).
tcf(c_977,plain,
! [X0: $i] :
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( sk_c8 != X0 )
| ( multiply(sk_c7,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_1023,plain,
( ( sk_c8 = inverse(sk_c2) )
| ( sk_c8 != sk_c8 )
| ( inverse(sk_c2) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_751]) ).
tcf(c_1024,plain,
! [X0: $i] :
( ( inverse(sk_c2) = X0 )
| ( X0 != sk_c8 )
| ( inverse(sk_c2) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_710]) ).
tcf(c_1130,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c2) )
| ( X1 != X0 )
| ( inverse(sk_c2) != X0 ) ),
inference(instantiation,[status(thm)],[c_816]) ).
tcf(c_1132,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c2) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c2) != X0 ) ),
inference(instantiation,[status(thm)],[c_710]) ).
tcf(c_1139,plain,
! [X0: $i] :
( ( inverse(sk_c2) = inverse(X0) )
| ( inverse(sk_c2) != sk_c8 )
| ( inverse(X0) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1024]) ).
tcf(c_1184,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c5) = multiply(sk_c8,sk_c9) )
| ( inverse(sk_c5) != multiply(X0,X1) )
| ( multiply(sk_c8,sk_c9) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_843]) ).
tcf(c_1203,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c8,sk_c9) = X1 )
| ( X1 != multiply(X0,sk_c9) )
| ( multiply(sk_c8,sk_c9) != multiply(X0,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_729]) ).
tcf(c_1206,plain,
( ( multiply(sk_c8,sk_c9) = multiply(identity,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( sk_c8 != identity ) ),
inference(instantiation,[status(thm)],[c_914]) ).
tcf(c_1222,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c5) )
| ( X1 != X0 )
| ( inverse(sk_c5) != X0 ) ),
inference(instantiation,[status(thm)],[c_816]) ).
tcf(c_1357,plain,
! [X0: $i] :
( ( multiply(X0,sk_c9) = multiply(sk_c8,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_905]) ).
tcf(c_1400,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c8,sk_c9) )
| ( X1 != multiply(X0,sk_c9) )
| ( multiply(sk_c8,sk_c9) != multiply(X0,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_877]) ).
tcf(c_1449,plain,
multiply(identity,sk_c9) = sk_c9,
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_1461,plain,
( ( sk_c7 = inverse(sk_c6) )
| ( sk_c7 != sk_c7 )
| ( inverse(sk_c6) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_808]) ).
tcf(c_1473,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c6) )
| ( X0 != multiply(sk_c5,sk_c8) )
| ( inverse(sk_c6) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_816]) ).
tcf(c_1494,plain,
multiply(identity,sk_c7) = sk_c7,
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_1562,plain,
( ( sk_c9 = multiply(identity,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_907]) ).
tcf(c_1720,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c6,multiply(sk_c7,X0)) = multiply(sk_c9,X0) ) ),
inference(superposition,[status(thm)],[c_152,c_104]) ).
tcf(c_1733,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(X0,X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_102,c_104]) ).
tcf(c_1734,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_103,c_104]) ).
tcf(c_1905,plain,
! [X0: $i] :
( ( inverse(sk_c2) = multiply(sk_c8,sk_c9) )
| ( inverse(sk_c2) != X0 )
| ( multiply(sk_c8,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_1132]) ).
tcf(c_2199,plain,
( ( sk_c7 = sk_c8 )
| ( sk_c7 != inverse(sk_c6) )
| ( sk_c8 != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_748]) ).
tcf(c_2205,plain,
! [X0: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != inverse(sk_c6) )
| ( X0 != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_787]) ).
tcf(c_2222,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(identity,sk_c7) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_149,c_1733]) ).
tcf(c_2247,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(identity,multiply(X0,multiply(X1,X2))) = multiply(X0,multiply(X1,X2)),
inference(superposition,[status(thm)],[c_104,c_1733]) ).
tcf(c_2338,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( X0 != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_770]) ).
tcf(c_2339,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( X0 != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_800]) ).
tcf(c_2461,plain,
( ( multiply(identity,sk_c9) = multiply(sk_c8,sk_c9) )
| ( identity != sk_c8 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1357]) ).
tcf(c_2495,plain,
( ( multiply(identity,multiply(sk_c5,sk_c8)) = inverse(sk_c6) )
| ( inverse(sk_c6) != multiply(sk_c5,sk_c8) )
| ( multiply(identity,multiply(sk_c5,sk_c8)) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1473]) ).
tcf(c_2715,plain,
( ( inverse(sk_c2) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c5) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_393,c_135]) ).
tcf(c_2719,plain,
( ( inverse(sk_c5) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c2) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_393,c_129]) ).
tcf(c_2722,plain,
( ( multiply(sk_c5,sk_c8) = sk_c7 )
| ~ iPr_def_10
| ( inverse(sk_c2) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_393,c_128]) ).
tcf(c_2727,plain,
( ( multiply(sk_c8,sk_c9) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(sk_c8,sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1203]) ).
tcf(c_2739,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,sk_c9) )
| ( X2 != X1 )
| ( multiply(X0,sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_2760,plain,
( ( sk_c9 = multiply(sk_c8,sk_c9) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(sk_c8,sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1400]) ).
tcf(c_2803,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( sk_c7 != multiply(sk_c8,sk_c9) )
| ( inverse(sk_c5) != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_775]) ).
tcf(c_2804,plain,
( ( sk_c7 = sk_c8 )
| ( sk_c7 != multiply(sk_c8,sk_c9) )
| ( sk_c8 != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_748]) ).
tcf(c_2806,plain,
( ( sk_c9 = sk_c7 )
| ( sk_c7 != multiply(sk_c8,sk_c9) )
| ( sk_c9 != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_744]) ).
tcf(c_2810,plain,
! [X0: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != multiply(sk_c8,sk_c9) )
| ( X0 != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_787]) ).
tcf(c_2815,plain,
! [X0: $i,X1: $i] :
( ( sk_c7 = multiply(X0,X1) )
| ( sk_c7 != multiply(sk_c8,sk_c9) )
| ( multiply(X0,X1) != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_749]) ).
tcf(c_2934,plain,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( sk_c8 != inverse(sk_c2) )
| ( multiply(sk_c7,sk_c9) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_977]) ).
tcf(c_2938,plain,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( sk_c8 != multiply(sk_c8,sk_c9) )
| ( multiply(sk_c7,sk_c9) != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_977]) ).
tcf(c_2939,plain,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( sk_c8 != multiply(sk_c7,sk_c9) )
| ( multiply(sk_c7,sk_c9) != multiply(sk_c7,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_977]) ).
tcf(c_3017,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(inverse(sk_c2),sk_c7) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_132,c_1734]) ).
tcf(c_3019,plain,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(inverse(sk_c2),sk_c7) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_127,c_1734]) ).
tcf(c_3020,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(inverse(sk_c3),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_146,c_1734]) ).
tcf(c_3021,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(inverse(sk_c3),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_143,c_1734]) ).
tcf(c_3022,plain,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(inverse(sk_c3),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_141,c_1734]) ).
tcf(c_3023,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_102,c_1734]) ).
tcf(c_3024,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_103,c_1734]) ).
tcf(c_3422,plain,
( ( inverse(sk_c2) = inverse(sk_c5) )
| ( inverse(sk_c2) != sk_c8 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1139]) ).
tcf(c_3488,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c5) = multiply(X0,X1) )
| ( inverse(sk_c5) != sk_c8 )
| ( multiply(X0,X1) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_3597,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c9) = X0 )
| ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_399,c_105]) ).
tcf(c_3601,plain,
! [X0: $i] :
( ( multiply(sk_c5,sk_c8) = X0 )
| ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( X0 != sk_c7 ) ),
inference(resolution,[status(thm)],[c_399,c_107]) ).
tcf(c_3624,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c9) = X0 )
| ( multiply(sk_c6,sk_c7) = sk_c9 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_399,c_117]) ).
tcf(c_3665,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X1) = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_399,c_102]) ).
tcf(c_3666,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_399,c_103]) ).
tcf(c_3670,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_399,c_398]) ).
tcf(c_3671,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_399,c_401]) ).
tcf(c_4088,plain,
multiply(identity,multiply(sk_c5,sk_c8)) = multiply(sk_c5,sk_c8),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_4170,plain,
! [X0: $i] :
( ( multiply(sk_c8,sk_c9) = inverse(sk_c5) )
| ( inverse(sk_c5) != X0 )
| ( multiply(sk_c8,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_1222]) ).
tcf(c_4409,plain,
multiply(identity,sk_c7) = sk_c7,
inference(global_subsumption_just,[status(thm)],[c_2222,c_1494]) ).
tcf(c_4411,plain,
multiply(inverse(identity),sk_c7) = sk_c7,
inference(superposition,[status(thm)],[c_4409,c_1734]) ).
tcf(c_4425,plain,
( ( sk_c7 = multiply(identity,multiply(sk_c5,sk_c8)) )
| ( sk_c7 != inverse(sk_c6) )
| ( multiply(identity,multiply(sk_c5,sk_c8)) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_2205]) ).
tcf(c_4628,plain,
( ( multiply(sk_c4,sk_c9) = sk_c8 )
| ( multiply(inverse(sk_c3),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_140,c_1734]) ).
tcf(c_4647,plain,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( multiply(inverse(sk_c3),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_144,c_1734]) ).
tcf(c_4650,plain,
! [X0: $i] :
( ( inverse(sk_c2) = multiply(sk_c8,sk_c9) )
| ( inverse(sk_c2) != inverse(X0) )
| ( multiply(sk_c8,sk_c9) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1905]) ).
tcf(c_4670,plain,
( ( multiply(sk_c6,sk_c7) = sk_c9 )
| ( multiply(inverse(sk_c3),sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_145,c_1734]) ).
tcf(c_4693,plain,
( ( inverse(sk_c2) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c5) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_135,c_393]) ).
tcf(c_5034,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(X0,X1) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_2338]) ).
tcf(c_5084,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c4,sk_c9) )
| ( X0 != sk_c8 )
| ( multiply(sk_c4,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_2739]) ).
tcf(c_5085,plain,
( ( sk_c8 = multiply(sk_c4,sk_c9) )
| ( sk_c8 != sk_c8 )
| ( multiply(sk_c4,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_5084]) ).
tcf(c_5100,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c9),sk_c9) )
| ( X0 != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_2739]) ).
tcf(c_5101,plain,
( ( sk_c8 = multiply(inverse(sk_c9),sk_c9) )
| ( sk_c8 != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_5100]) ).
tcf(c_5105,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c9) = X2 )
| ( X2 != X1 )
| ( multiply(X0,sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_399]) ).
tcf(c_5120,plain,
( ( multiply(sk_c5,sk_c8) = sk_c7 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_142,c_394]) ).
tcf(c_5121,plain,
( ( multiply(sk_c4,sk_c9) = sk_c8 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_140,c_394]) ).
tcf(c_5122,plain,
( ( inverse(sk_c6) = sk_c7 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_146,c_394]) ).
tcf(c_5123,plain,
( ( inverse(sk_c5) = sk_c8 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_143,c_394]) ).
tcf(c_5124,plain,
( ( inverse(sk_c4) = sk_c9 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_141,c_394]) ).
tcf(c_5216,plain,
! [X0: $i] :
( ( multiply(sk_c7,sk_c9) = inverse(sk_c2) )
| ( inverse(sk_c2) != X0 )
| ( multiply(sk_c7,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_1130]) ).
tcf(c_6003,plain,
( ( inverse(sk_c2) = sk_c8 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_4693,c_136,c_673,c_2715,c_2722,c_2719]) ).
tcf(c_6005,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_6003,c_673,c_2722,c_2719,c_6003]) ).
tcf(c_6162,plain,
( ( inverse(sk_c1) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_119,c_395]) ).
tcf(c_6170,plain,
( ( multiply(sk_c4,sk_c9) = sk_c8 )
| ~ iPr_def_12
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_112,c_395]) ).
tcf(c_6173,plain,
( ( inverse(sk_c4) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_113,c_395]) ).
tcf(c_6185,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_400,c_399]) ).
tcf(c_6240,plain,
! [X0: $i] :
( ( sk_c7 = multiply(X0,sk_c9) )
| ( sk_c7 != multiply(sk_c8,sk_c9) )
| ( multiply(X0,sk_c9) != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_2815]) ).
tcf(c_6496,plain,
( ( sk_c7 = multiply(sk_c8,sk_c9) )
| ( inverse(sk_c4) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_3670,c_106]) ).
tcf(c_6497,plain,
( ( sk_c7 = multiply(sk_c8,sk_c9) )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_3670,c_108]) ).
tcf(c_6498,plain,
( ( sk_c7 = multiply(sk_c8,sk_c9) )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(resolution,[status(thm)],[c_3670,c_111]) ).
tcf(c_6502,plain,
( ( sk_c8 = multiply(sk_c4,sk_c9) )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(resolution,[status(thm)],[c_3670,c_105]) ).
tcf(c_6508,plain,
( ( sk_c8 = multiply(sk_c7,sk_c9) )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_3670,c_137]) ).
tcf(c_6509,plain,
( ( sk_c8 = multiply(sk_c7,sk_c9) )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_3670,c_151]) ).
tcf(c_6510,plain,
( ( sk_c8 = multiply(sk_c7,sk_c9) )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(resolution,[status(thm)],[c_3670,c_109]) ).
tcf(c_6512,plain,
( ( sk_c9 = multiply(sk_c6,sk_c7) )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_3670,c_138]) ).
tcf(c_6513,plain,
( ( sk_c9 = multiply(sk_c6,sk_c7) )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_3670,c_152]) ).
tcf(c_6537,plain,
( ( sk_c9 = multiply(sk_c3,sk_c8) )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(resolution,[status(thm)],[c_3670,c_146]) ).
tcf(c_6538,plain,
( ( sk_c9 = multiply(sk_c3,sk_c8) )
| ( multiply(sk_c4,sk_c9) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_3670,c_140]) ).
tcf(c_6541,plain,
( ( sk_c9 = multiply(sk_c3,sk_c8) )
| ( multiply(sk_c6,sk_c7) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_3670,c_145]) ).
tcf(c_6547,plain,
! [X0: $i] : identity = multiply(inverse(X0),X0),
inference(resolution,[status(thm)],[c_3670,c_103]) ).
tcf(c_7507,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c7,sk_c9) )
| ( X0 != sk_c8 )
| ( multiply(sk_c7,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_2739]) ).
tcf(c_7508,plain,
( ( sk_c8 = multiply(sk_c7,sk_c9) )
| ( sk_c8 != sk_c8 )
| ( multiply(sk_c7,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_7507]) ).
tcf(c_7554,plain,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ~ iPr_def_13
| ( inverse(sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_110,c_396]) ).
tcf(c_7555,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_13
| ( inverse(sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_152,c_396]) ).
tcf(c_7556,plain,
( ( inverse(sk_c2) = sk_c8 )
| ~ iPr_def_13
| ( inverse(sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_138,c_396]) ).
tcf(c_7648,plain,
( ( inverse(sk_c6) = sk_c7 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_5122,c_153,c_5122]) ).
tcf(c_9279,plain,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( sk_c7 != multiply(identity,multiply(sk_c5,sk_c8)) )
| ( multiply(sk_c8,sk_c9) != multiply(identity,multiply(sk_c5,sk_c8)) ) ),
inference(instantiation,[status(thm)],[c_703]) ).
tcf(c_10264,plain,
( ( sk_c7 = inverse(sk_c5) )
| ( sk_c7 != multiply(sk_c8,sk_c9) )
| ( inverse(sk_c5) != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_2810]) ).
tcf(c_10284,plain,
( ( inverse(sk_c1) = sk_c9 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_6162,c_120,c_671,c_6173,c_6162,c_6170]) ).
tcf(c_10286,plain,
~ iPr_def_12,
inference(global_subsumption_just,[status(thm)],[c_10284,c_671,c_6173,c_6170,c_10284]) ).
tcf(c_10454,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(identity,X1) = X2 )
| ( X2 != X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_3665,c_399]) ).
tcf(c_10526,plain,
! [X0: $i,X1: $i] :
( ( X0 = multiply(inverse(X1),X1) )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_3666,c_3670]) ).
tcf(c_10527,plain,
( ( sk_c8 = multiply(inverse(sk_c8),sk_c8) )
| ( sk_c8 != identity ) ),
inference(instantiation,[status(thm)],[c_10526]) ).
tcf(c_10600,plain,
( ( inverse(sk_c6) = sk_c7 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_394,c_146]) ).
tcf(c_10601,plain,
( ( multiply(sk_c4,sk_c9) = sk_c8 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_394,c_140]) ).
tcf(c_10602,plain,
( ( multiply(sk_c5,sk_c8) = sk_c7 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_394,c_142]) ).
tcf(c_10897,plain,
! [X0: $i] : multiply(identity,multiply(X0,sk_c7)) = multiply(X0,sk_c7),
inference(superposition,[status(thm)],[c_4411,c_2247]) ).
tcf(c_11180,plain,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ~ iPr_def_13
| ( inverse(sk_c6) != sk_c7 ) ),
inference(resolution,[status(thm)],[c_396,c_110]) ).
tcf(c_11426,plain,
( iPr_def_13
| ( multiply(sk_c7,sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_397,c_136,c_120,c_397,c_671,c_673,c_2715,c_2722,c_2719,c_6173,c_6162,c_6170]) ).
tcf(c_11427,negated_conjecture,
( iPr_def_13
| iPr_def_11
| ( multiply(sk_c7,sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(renaming,[status(thm)],[c_11426]) ).
tcf(c_11565,plain,
( iPr_def_13
| iPr_def_11
| ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(resolution,[status(thm)],[c_11427,c_151]) ).
tcf(c_11597,plain,
( ( inverse(sk_c5) = multiply(identity,sk_c8) )
| ( inverse(sk_c5) != sk_c8 )
| ( multiply(identity,sk_c8) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_3488]) ).
tcf(c_12336,plain,
multiply(sk_c7,sk_c9) = multiply(sk_c7,sk_c9),
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_13061,plain,
multiply(identity,sk_c7) = sk_c7,
inference(superposition,[status(thm)],[c_4411,c_10897]) ).
tcf(c_13208,plain,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ~ iPr_def_13
| ( inverse(sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_110,c_396]) ).
tcf(c_13215,plain,
( ~ iPr_def_13
| ( sk_c9 != sk_c7 )
| ( inverse(identity) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_13061,c_396]) ).
tcf(c_13281,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),multiply(identity,X1)) = multiply(multiply(identity,X0),X1),
inference(superposition,[status(thm)],[c_3024,c_104]) ).
tcf(c_13396,plain,
! [X0: $i] : multiply(inverse(inverse(identity)),X0) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_3023,c_1734]) ).
tcf(c_13418,plain,
multiply(identity,inverse(identity)) = identity,
inference(superposition,[status(thm)],[c_13396,c_103]) ).
tcf(c_13442,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_13418,c_102]) ).
tcf(c_13602,plain,
( ~ iPr_def_13
| ( sk_c7 != identity )
| ( sk_c9 != sk_c7 ) ),
inference(superposition,[status(thm)],[c_13442,c_13215]) ).
tcf(c_13687,plain,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_13208,c_111,c_7554]) ).
tcf(c_14029,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,X0),X1) = multiply(inverse(inverse(X0)),X1),
inference(superposition,[status(thm)],[c_102,c_13281]) ).
tcf(c_15139,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c9) = X0 )
| ( X0 != sk_c8 )
| ( multiply(sk_c4,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_5105]) ).
tcf(c_15389,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( inverse(sk_c2) = sk_c8 )
| ( X0 != multiply(sk_c7,sk_c9) ) ),
inference(resolution,[status(thm)],[c_6508,c_399]) ).
tcf(c_15451,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( inverse(sk_c3) = sk_c8 )
| ( X0 != multiply(sk_c7,sk_c9) ) ),
inference(resolution,[status(thm)],[c_6509,c_399]) ).
tcf(c_15643,plain,
! [X0: $i] : multiply(multiply(identity,X0),inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_14029,c_103]) ).
tcf(c_16040,plain,
( ( multiply(sk_c8,sk_c9) = inverse(sk_c5) )
| ( inverse(sk_c5) != multiply(sk_c8,sk_c9) )
| ( multiply(sk_c8,sk_c9) != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_4170]) ).
tcf(c_16069,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( inverse(sk_c2) = sk_c8 )
| ( X0 != multiply(sk_c6,sk_c7) ) ),
inference(resolution,[status(thm)],[c_6512,c_399]) ).
tcf(c_16076,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( inverse(sk_c3) = sk_c8 )
| ( X0 != multiply(sk_c6,sk_c7) ) ),
inference(resolution,[status(thm)],[c_6513,c_399]) ).
tcf(c_16414,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_102,c_15643]) ).
tcf(c_16468,plain,
( ( inverse(sk_c2) = multiply(sk_c8,sk_c9) )
| ( inverse(sk_c2) != inverse(sk_c5) )
| ( multiply(sk_c8,sk_c9) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_4650]) ).
tcf(c_16583,plain,
( ( sk_c7 = multiply(identity,sk_c9) )
| ( sk_c7 != multiply(sk_c8,sk_c9) )
| ( multiply(identity,sk_c9) != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_6240]) ).
tcf(c_17076,plain,
( ( sk_c7 = multiply(sk_c8,sk_c9) )
| ( sk_c8 = multiply(sk_c7,sk_c9) ) ),
inference(resolution,[status(thm)],[c_6510,c_3670]) ).
tcf(c_17254,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_125,c_16414]) ).
tcf(c_17255,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_122,c_16414]) ).
tcf(c_17256,plain,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_120,c_16414]) ).
tcf(c_17257,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_139,c_16414]) ).
tcf(c_17258,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_136,c_16414]) ).
tcf(c_17259,plain,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c2,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_134,c_16414]) ).
tcf(c_19258,plain,
! [X0: $i] :
( ( sk_c9 = multiply(sk_c3,sk_c8) )
| ( multiply(sk_c4,sk_c9) = X0 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_6538,c_399]) ).
tcf(c_20570,plain,
( ( sk_c9 = multiply(sk_c3,sk_c8) )
| ~ iPr_def_13
| ( inverse(sk_c6) != sk_c7 ) ),
inference(resolution,[status(thm)],[c_6541,c_396]) ).
tcf(c_21104,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_17254,c_118]) ).
tcf(c_21874,plain,
( ( inverse(sk_c6) = sk_c7 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_10600,c_7648]) ).
tcf(c_21922,plain,
! [X0: $i] :
( ( inverse(sk_c6) = X0 )
| ~ iPr_def_11
| ( X0 != sk_c7 ) ),
inference(resolution,[status(thm)],[c_21874,c_399]) ).
tcf(c_22004,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_17255,c_115]) ).
tcf(c_22703,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c4) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_17256,c_113]) ).
tcf(c_23418,plain,
( ( sk_c7 = identity )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_17257,c_132]) ).
tcf(c_23613,plain,
( ( multiply(sk_c4,sk_c9) = sk_c8 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_10601,c_147,c_5121]) ).
tcf(c_23624,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c9) = X0 )
| ~ iPr_def_11
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_23613,c_399]) ).
tcf(c_23625,plain,
( ( multiply(sk_c5,sk_c8) = sk_c7 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_10602,c_149,c_5120]) ).
tcf(c_23636,plain,
! [X0: $i] :
( ( multiply(sk_c5,sk_c8) = X0 )
| ~ iPr_def_11
| ( X0 != sk_c7 ) ),
inference(resolution,[status(thm)],[c_23625,c_399]) ).
tcf(c_25557,plain,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_11180,c_13687]) ).
tcf(c_25579,plain,
( ( sk_c7 = multiply(sk_c8,sk_c9) )
| ~ iPr_def_13 ),
inference(resolution,[status(thm)],[c_25557,c_3670]) ).
tcf(c_25788,plain,
( ( sk_c9 = multiply(sk_c3,sk_c8) )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_20570,c_6537,c_20570]) ).
tcf(c_26440,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(X2) )
| ( X2 != X1 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_3671,c_401]) ).
tcf(c_27474,plain,
( ( sk_c7 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_17258,c_129]) ).
tcf(c_27944,plain,
( ( sk_c7 = identity )
| ( inverse(sk_c4) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_17259,c_127]) ).
tcf(c_28190,plain,
! [X0: $i] :
( ( multiply(sk_c8,sk_c9) = X0 )
| ( X0 != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_702]) ).
tcf(c_28191,plain,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( sk_c7 != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_676]) ).
tcf(c_28192,plain,
( ( multiply(sk_c8,sk_c9) = sk_c8 )
| ( sk_c8 != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_28190]) ).
tcf(c_28234,plain,
( ( multiply(sk_c7,sk_c9) = multiply(sk_c8,sk_c9) )
| ( sk_c7 != sk_c8 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1357]) ).
tcf(c_28432,plain,
multiply(inverse(sk_c9),sk_c9) = identity,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_28771,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c5,sk_c8) = X0 )
| ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( X1 != sk_c7 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_3601,c_399]) ).
tcf(c_30411,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c9) )
| ( multiply(sk_c6,sk_c7) = sk_c9 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_3624,c_3670]) ).
tcf(c_31331,plain,
( ( sk_c9 = sk_c7 )
| ( sk_c7 != multiply(identity,sk_c9) )
| ( sk_c9 != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_2339]) ).
tcf(c_33314,plain,
( ( sk_c9 = multiply(inverse(sk_c9),sk_c9) )
| ( sk_c9 != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_5100]) ).
tcf(c_34194,plain,
( ( multiply(sk_c7,sk_c9) = inverse(sk_c2) )
| ( inverse(sk_c2) != multiply(sk_c8,sk_c9) )
| ( multiply(sk_c7,sk_c9) != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_5216]) ).
tcf(c_34617,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),multiply(identity,X1)) = multiply(multiply(identity,X0),X1),
inference(superposition,[status(thm)],[c_3024,c_104]) ).
tcf(c_36496,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_139,c_3017]) ).
tcf(c_36514,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_36496,c_102]) ).
tcf(c_36576,plain,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c8,sk_c7) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_134,c_3019]) ).
tcf(c_36592,plain,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c8,sk_c7) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_36576,c_102]) ).
tcf(c_36613,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c8,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_153,c_3020]) ).
tcf(c_36634,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c8,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_36613,c_102]) ).
tcf(c_36710,plain,
inverse(sk_c6) = sk_c7,
inference(global_subsumption_just,[status(thm)],[c_36514,c_153,c_136,c_120,c_111,c_404,c_397,c_671,c_673,c_763,c_898,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_5122,c_6173,c_6162,c_6170,c_6498,c_13602,c_21104,c_23418,c_28234,c_36634]) ).
tcf(c_36982,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_150,c_3021]) ).
tcf(c_37027,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_36982,c_102]) ).
tcf(c_37234,plain,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_148,c_3022]) ).
tcf(c_37293,plain,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_37234,c_102]) ).
tcf(c_37734,plain,
inverse(sk_c4) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_36592,c_148,c_136,c_120,c_106,c_404,c_397,c_671,c_673,c_763,c_898,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_5124,c_6173,c_6162,c_6170,c_6496,c_13602,c_22703,c_27944,c_28234,c_37293]) ).
tcf(c_38184,plain,
( ~ iPr_def_13
| ( inverse(sk_c5) != sk_c7 )
| ( multiply(sk_c5,sk_c7) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_396]) ).
tcf(c_39331,plain,
inverse(sk_c5) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_37027,c_150,c_136,c_120,c_108,c_404,c_397,c_671,c_673,c_763,c_898,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_5123,c_6173,c_6162,c_6170,c_6497,c_13602,c_22004,c_27474,c_28234,c_37027]) ).
tcf(c_39864,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ~ iPr_def_13
| ( X1 != sk_c8 )
| ( X0 != sk_c3 ) ),
inference(resolution,[status(thm)],[c_6185,c_25788]) ).
tcf(c_46336,plain,
( ( inverse(sk_c5) = multiply(sk_c8,sk_c9) )
| ( inverse(sk_c5) != multiply(identity,sk_c8) )
| ( multiply(sk_c8,sk_c9) != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1184]) ).
tcf(c_47095,plain,
! [X0: $i] :
( ( sk_c9 = multiply(sk_c5,sk_c8) )
| ( sk_c9 != X0 )
| ( multiply(sk_c5,sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_800]) ).
tcf(c_47096,plain,
( ( sk_c9 = multiply(sk_c5,sk_c8) )
| ( sk_c9 != sk_c8 )
| ( multiply(sk_c5,sk_c8) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_47095]) ).
tcf(c_50063,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_6547,c_399]) ).
tcf(c_50064,plain,
( ( identity = sk_c8 )
| ( sk_c8 != multiply(inverse(sk_c8),sk_c8) ) ),
inference(instantiation,[status(thm)],[c_50063]) ).
tcf(c_52626,plain,
! [X0: $i] :
( ( inverse(sk_c6) = X0 )
| ( X0 != sk_c7 ) ),
inference(global_subsumption_just,[status(thm)],[c_21922,c_153,c_136,c_120,c_111,c_404,c_397,c_671,c_673,c_733,c_763,c_898,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_5122,c_6173,c_6162,c_6170,c_6498,c_13602,c_21104,c_23418,c_28234,c_36634]) ).
tcf(c_54629,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c5,sk_c8) = X0 )
| ~ iPr_def_11
| ( X1 != sk_c7 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_23636,c_399]) ).
tcf(c_54631,plain,
( ~ iPr_def_11
| ( sk_c9 != sk_c7 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_23636,c_394]) ).
tcf(c_59422,plain,
! [X0: $i] :
( ( sk_c8 = multiply(sk_c4,sk_c9) )
| ( multiply(identity,X0) = multiply(sk_c8,sk_c9) )
| ( sk_c7 != X0 ) ),
inference(resolution,[status(thm)],[c_10454,c_6502]) ).
tcf(c_59424,plain,
! [X0: $i] :
( ( sk_c8 = multiply(sk_c7,sk_c9) )
| ( multiply(identity,X0) = multiply(sk_c8,sk_c9) )
| ( sk_c7 != X0 ) ),
inference(resolution,[status(thm)],[c_10454,c_6510]) ).
tcf(c_59503,plain,
! [X0: $i] :
( ( multiply(sk_c5,sk_c8) = sk_c7 )
| ( multiply(identity,X0) = multiply(sk_c1,sk_c9) )
| ( sk_c8 != X0 ) ),
inference(resolution,[status(thm)],[c_10454,c_114]) ).
tcf(c_60539,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,X0),X1) = multiply(inverse(inverse(X0)),X1),
inference(superposition,[status(thm)],[c_102,c_34617]) ).
tcf(c_62499,plain,
! [X0: $i] : multiply(multiply(identity,X0),inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_60539,c_103]) ).
tcf(c_64470,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_102,c_62499]) ).
tcf(c_69063,plain,
multiply(sk_c4,sk_c9) = identity,
inference(superposition,[status(thm)],[c_37734,c_64470]) ).
tcf(c_69686,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c9) = multiply(identity,X0) )
| ( multiply(sk_c5,sk_c8) = sk_c7 )
| ( sk_c8 != X0 ) ),
inference(resolution,[status(thm)],[c_59503,c_3670]) ).
tcf(c_80308,negated_conjecture,
inverse(sk_c4) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_120,c_37734]) ).
tcf(c_80310,negated_conjecture,
inverse(sk_c5) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_122,c_150,c_136,c_120,c_108,c_404,c_397,c_671,c_673,c_763,c_898,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_5123,c_6173,c_6162,c_6170,c_6497,c_13602,c_22004,c_27474,c_28234,c_37027]) ).
tcf(c_80312,negated_conjecture,
inverse(sk_c6) = sk_c7,
inference(global_subsumption_just,[status(thm)],[c_125,c_153,c_136,c_120,c_111,c_404,c_397,c_671,c_673,c_763,c_898,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_5122,c_6173,c_6162,c_6170,c_6498,c_13602,c_21104,c_23418,c_28234,c_36634]) ).
tcf(c_80316,plain,
multiply(sk_c7,sk_c6) = identity,
inference(superposition,[status(thm)],[c_80312,c_103]) ).
tcf(c_80342,plain,
multiply(identity,sk_c7) = sk_c7,
inference(superposition,[status(thm)],[c_4411,c_10897]) ).
tcf(c_80485,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_80316,c_104]) ).
tcf(c_80502,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c7,sk_c9) = multiply(identity,sk_c7) ) ),
inference(superposition,[status(thm)],[c_152,c_80485]) ).
tcf(c_80503,plain,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c7,sk_c9) = multiply(identity,sk_c7) ) ),
inference(superposition,[status(thm)],[c_138,c_80485]) ).
tcf(c_80584,plain,
multiply(inverse(sk_c9),identity) = multiply(identity,sk_c4),
inference(superposition,[status(thm)],[c_80308,c_3024]) ).
tcf(c_80585,plain,
multiply(inverse(sk_c8),identity) = multiply(identity,sk_c5),
inference(superposition,[status(thm)],[c_80310,c_3024]) ).
tcf(c_80586,plain,
multiply(inverse(sk_c7),identity) = multiply(identity,sk_c6),
inference(superposition,[status(thm)],[c_80312,c_3024]) ).
tcf(c_80590,plain,
! [X0: $i] : multiply(inverse(sk_c9),multiply(identity,X0)) = multiply(multiply(identity,sk_c4),X0),
inference(superposition,[status(thm)],[c_80584,c_104]) ).
tcf(c_80592,plain,
! [X0: $i] : multiply(inverse(sk_c8),multiply(identity,X0)) = multiply(multiply(identity,sk_c5),X0),
inference(superposition,[status(thm)],[c_80585,c_104]) ).
tcf(c_80594,plain,
! [X0: $i] : multiply(inverse(sk_c7),multiply(identity,X0)) = multiply(multiply(identity,sk_c6),X0),
inference(superposition,[status(thm)],[c_80586,c_104]) ).
tcf(c_80961,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c7,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_80502,c_80342]) ).
tcf(c_80975,plain,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c7,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_80503,c_80342]) ).
tcf(c_81024,plain,
! [X0: $i] : multiply(multiply(identity,sk_c4),X0) = multiply(inverse(sk_c9),X0),
inference(superposition,[status(thm)],[c_102,c_80590]) ).
tcf(c_81070,plain,
! [X0: $i] : multiply(inverse(sk_c9),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_102,c_81024]) ).
tcf(c_81097,plain,
multiply(sk_c4,sk_c9) = identity,
inference(superposition,[status(thm)],[c_81070,c_103]) ).
tcf(c_81125,plain,
( ( sk_c8 = identity )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_81097,c_105]) ).
tcf(c_81126,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_81097,c_147]) ).
tcf(c_81127,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_81097,c_133]) ).
tcf(c_81331,plain,
! [X0: $i] : multiply(multiply(identity,sk_c5),X0) = multiply(inverse(sk_c8),X0),
inference(superposition,[status(thm)],[c_102,c_80592]) ).
tcf(c_81422,plain,
! [X0: $i] : multiply(inverse(sk_c8),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_102,c_81331]) ).
tcf(c_81447,plain,
multiply(sk_c5,sk_c8) = identity,
inference(superposition,[status(thm)],[c_81422,c_103]) ).
tcf(c_81458,plain,
! [X0: $i] : multiply(sk_c5,multiply(sk_c8,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_81422,c_1734]) ).
tcf(c_81475,plain,
( ( sk_c7 = identity )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_81447,c_107]) ).
tcf(c_81483,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_81447,c_394]) ).
tcf(c_81505,plain,
! [X0: $i] : multiply(multiply(identity,sk_c6),X0) = multiply(inverse(sk_c7),X0),
inference(superposition,[status(thm)],[c_102,c_80594]) ).
tcf(c_81556,plain,
! [X0: $i] : multiply(inverse(sk_c7),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_102,c_81505]) ).
tcf(c_81644,plain,
( ~ iPr_def_11
| ( sk_c9 != identity ) ),
inference(global_subsumption_just,[status(thm)],[c_81483,c_150,c_136,c_120,c_108,c_404,c_397,c_671,c_673,c_763,c_898,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_5123,c_6173,c_6162,c_6170,c_6497,c_13602,c_22004,c_27474,c_28234,c_37027,c_81483]) ).
tcf(c_81663,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm)],[c_81556,c_103]) ).
tcf(c_81694,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_81663,c_110]) ).
tcf(c_81695,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_81663,c_152]) ).
tcf(c_81696,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_81663,c_138]) ).
tcf(c_81702,plain,
( ~ iPr_def_13
| ( sk_c9 != identity )
| ( inverse(sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_81663,c_396]) ).
tcf(c_81838,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c5,sk_c7) = multiply(identity,sk_c9) ) ),
inference(superposition,[status(thm)],[c_81694,c_81458]) ).
tcf(c_83373,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c9,sk_c6) = multiply(sk_c6,identity) ) ),
inference(superposition,[status(thm)],[c_80316,c_1720]) ).
tcf(c_87582,plain,
( ( multiply(sk_c5,sk_c7) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(sk_c5,sk_c7) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_5034]) ).
tcf(c_88970,plain,
( ( sk_c9 = sk_c8 )
| ( sk_c9 != multiply(inverse(sk_c9),sk_c9) )
| ( sk_c8 != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_743]) ).
tcf(c_89071,plain,
( ( sk_c7 = sk_c8 )
| ( sk_c7 != inverse(sk_c5) )
| ( sk_c8 != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_748]) ).
tcf(c_89256,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c8,sk_c9) )
| ( X0 != inverse(sk_c5) )
| ( multiply(sk_c8,sk_c9) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_762]) ).
tcf(c_89257,plain,
( ( sk_c8 = multiply(sk_c8,sk_c9) )
| ( sk_c8 != inverse(sk_c5) )
| ( multiply(sk_c8,sk_c9) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_89256]) ).
tcf(c_89664,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(inverse(sk_c9),sk_c9) )
| ( X0 != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_770]) ).
tcf(c_89665,plain,
( ( sk_c8 = sk_c9 )
| ( sk_c9 != multiply(inverse(sk_c9),sk_c9) )
| ( sk_c8 != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_89664]) ).
tcf(c_91251,plain,
( ( sk_c8 = inverse(sk_c6) )
| ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c7,sk_c9) != sk_c7 ) ),
inference(resolution,[status(thm)],[c_15389,c_52626]) ).
tcf(c_91866,plain,
( ( sk_c8 = inverse(sk_c6) )
| ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c7,sk_c9) != sk_c7 ) ),
inference(resolution,[status(thm)],[c_15451,c_52626]) ).
tcf(c_93632,plain,
inverse(sk_c2) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_16069,c_153,c_150,c_136,c_120,c_137,c_111,c_108,c_404,c_397,c_671,c_673,c_747,c_763,c_888,c_898,c_1206,c_1449,c_1461,c_1562,c_2199,c_2715,c_2722,c_2719,c_2727,c_2760,c_2806,c_2804,c_2938,c_5101,c_5123,c_5122,c_6173,c_6162,c_6170,c_6498,c_6497,c_7556,c_13602,c_21104,c_22004,c_23418,c_27474,c_28191,c_28234,c_28432,c_33314,c_36634,c_37027,c_80975,c_81127,c_81483,c_81696,c_88970,c_91251]) ).
tcf(c_93642,plain,
inverse(sk_c3) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_16076,c_153,c_136,c_120,c_111,c_404,c_397,c_671,c_673,c_677,c_763,c_888,c_898,c_1206,c_1449,c_1461,c_1562,c_2199,c_2715,c_2722,c_2719,c_2727,c_2760,c_2806,c_2804,c_2938,c_5101,c_5122,c_6173,c_6162,c_6170,c_6498,c_7555,c_11565,c_13602,c_21104,c_23418,c_28192,c_28234,c_28432,c_33314,c_36634,c_80961,c_81126,c_81644,c_81695,c_89665,c_91866]) ).
tcf(c_93692,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(multiply(sk_c4,sk_c9)) )
| ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_26440,c_105]) ).
tcf(c_94050,plain,
! [X0: $i] :
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( inverse(multiply(sk_c4,sk_c9)) = inverse(X0) )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_93692,c_3670]) ).
tcf(c_94378,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c9) )
| ~ iPr_def_13
| ( X0 != sk_c8 )
| ( inverse(sk_c6) != sk_c7 ) ),
inference(resolution,[status(thm)],[c_30411,c_396]) ).
tcf(c_94395,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c9) )
| ~ iPr_def_13
| ( X0 != sk_c8 ) ),
inference(global_subsumption_just,[status(thm)],[c_94378,c_153,c_136,c_120,c_111,c_404,c_397,c_671,c_673,c_763,c_898,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_5122,c_6173,c_6162,c_6170,c_6498,c_13602,c_21104,c_23418,c_28234,c_36634,c_94378]) ).
tcf(c_94411,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ iPr_def_13
| ( X1 != multiply(sk_c1,sk_c9) )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_94395,c_399]) ).
tcf(c_94745,plain,
inverse(sk_c3) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_83373,c_93642]) ).
tcf(c_101361,plain,
( ( multiply(sk_c4,sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_94745,c_4628]) ).
tcf(c_107602,plain,
! [X0: $i] :
( ( X0 != sk_c8 )
| ( multiply(sk_c4,sk_c9) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_19258,c_155,c_404,c_397,c_786,c_789,c_832,c_888,c_898,c_1449,c_1562,c_2803,c_2938,c_3597,c_6005,c_10264,c_10286,c_11597,c_15139,c_16040,c_23624,c_28234,c_36710,c_38184,c_39331,c_46336,c_81702,c_81838,c_87582,c_89071,c_89257,c_101361]) ).
tcf(c_107603,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c9) = X0 )
| ( X0 != sk_c8 ) ),
inference(renaming,[status(thm)],[c_107602]) ).
tcf(c_107604,plain,
( ( multiply(sk_c4,sk_c9) = sk_c8 )
| ( sk_c8 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_107603]) ).
tcf(c_114842,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( sk_c7 != sk_c8 )
| ( X0 != sk_c3 )
| ( inverse(X0) != sk_c7 ) ),
inference(resolution,[status(thm)],[c_39864,c_396]) ).
tcf(c_114892,plain,
( ~ iPr_def_13
| ( sk_c7 != sk_c8 ) ),
inference(global_subsumption_just,[status(thm)],[c_114842,c_153,c_150,c_136,c_120,c_111,c_108,c_404,c_397,c_671,c_673,c_720,c_763,c_898,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_5123,c_5122,c_6173,c_6162,c_6170,c_6498,c_6497,c_13602,c_21104,c_22004,c_23418,c_27474,c_28234,c_36634,c_37027,c_38184,c_81702,c_81838,c_87582]) ).
tcf(c_116766,plain,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_94745,c_4647]) ).
tcf(c_117092,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ iPr_def_13
| ( X1 != sk_c8 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_94411,c_94395]) ).
tcf(c_117693,plain,
( ( multiply(sk_c6,sk_c7) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = multiply(identity,sk_c8) ) ),
inference(superposition,[status(thm)],[c_94745,c_4670]) ).
tcf(c_121335,plain,
~ iPr_def_13,
inference(global_subsumption_just,[status(thm)],[c_117092,c_155,c_153,c_150,c_136,c_120,c_111,c_108,c_404,c_397,c_671,c_673,c_674,c_763,c_789,c_898,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_5123,c_5122,c_6173,c_6162,c_6170,c_6498,c_6497,c_10264,c_11597,c_13602,c_21104,c_22004,c_23418,c_25579,c_27474,c_28234,c_36634,c_37027,c_46336,c_89071,c_114892,c_117693]) ).
tcf(c_121610,plain,
( ( multiply(sk_c8,sk_c9) = multiply(identity,multiply(sk_c5,sk_c8)) )
| ( sk_c9 != multiply(sk_c5,sk_c8) )
| ( sk_c8 != identity ) ),
inference(instantiation,[status(thm)],[c_797]) ).
tcf(c_122326,plain,
sk_c8 = multiply(sk_c4,sk_c9),
inference(global_subsumption_just,[status(thm)],[c_59422,c_404,c_5085,c_107604]) ).
tcf(c_122334,plain,
sk_c8 = multiply(sk_c7,sk_c9),
inference(global_subsumption_just,[status(thm)],[c_59424,c_155,c_150,c_136,c_120,c_108,c_404,c_397,c_671,c_673,c_763,c_789,c_832,c_898,c_1023,c_1206,c_1449,c_1562,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2934,c_2938,c_3422,c_5123,c_6173,c_6162,c_6170,c_6497,c_7508,c_10264,c_11597,c_13602,c_16040,c_16468,c_17076,c_22004,c_27474,c_28234,c_34194,c_37027,c_46336,c_89071,c_93632,c_116766]) ).
tcf(c_122435,plain,
multiply(sk_c5,sk_c8) = sk_c7,
inference(global_subsumption_just,[status(thm)],[c_69686,c_153,c_136,c_120,c_111,c_107,c_404,c_397,c_671,c_673,c_677,c_763,c_888,c_898,c_1206,c_1449,c_1461,c_1562,c_2199,c_2715,c_2722,c_2719,c_2727,c_2760,c_2806,c_2804,c_2938,c_2939,c_5101,c_5122,c_5120,c_6173,c_6162,c_6170,c_6498,c_7555,c_11565,c_12336,c_13602,c_21104,c_23418,c_28192,c_28234,c_28432,c_33314,c_36634,c_80961,c_81126,c_81644,c_81695,c_89665,c_91866,c_121335,c_122334]) ).
tcf(c_122566,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c5,sk_c8) = X0 )
| ( X0 != X1 )
| ( X1 != sk_c7 ) ),
inference(global_subsumption_just,[status(thm)],[c_28771,c_155,c_153,c_150,c_136,c_120,c_137,c_111,c_108,c_404,c_397,c_671,c_673,c_674,c_747,c_763,c_789,c_832,c_888,c_898,c_1023,c_1206,c_1449,c_1461,c_1562,c_2199,c_2715,c_2722,c_2719,c_2727,c_2760,c_2806,c_2804,c_2934,c_2938,c_2939,c_3422,c_5101,c_5123,c_5122,c_6173,c_6162,c_6170,c_6498,c_6497,c_7508,c_7556,c_10264,c_11597,c_12336,c_13602,c_16040,c_16468,c_17076,c_21104,c_22004,c_23418,c_25579,c_27474,c_28191,c_28234,c_28432,c_28771,c_33314,c_34194,c_36634,c_37027,c_46336,c_54629,c_80975,c_81127,c_81483,c_81696,c_88970,c_89071,c_91251,c_114892,c_116766,c_117693]) ).
tcf(c_122567,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c5,sk_c8) = X0 )
| ( X1 != sk_c7 )
| ( X0 != X1 ) ),
inference(renaming,[status(thm)],[c_122566]) ).
tcf(c_122639,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c5,sk_c8) = X0 )
| ( sk_c7 != identity )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_122567,c_3666]) ).
tcf(c_122640,plain,
( ( multiply(sk_c5,sk_c8) = sk_c8 )
| ( sk_c7 != identity )
| ( sk_c8 != multiply(inverse(sk_c8),sk_c8) ) ),
inference(instantiation,[status(thm)],[c_122639]) ).
tcf(c_122729,plain,
multiply(sk_c8,sk_c9) = sk_c7,
inference(global_subsumption_just,[status(thm)],[c_94050,c_153,c_136,c_120,c_111,c_404,c_397,c_671,c_673,c_763,c_780,c_888,c_898,c_1206,c_1449,c_1461,c_1562,c_2495,c_2715,c_2722,c_2719,c_2760,c_2806,c_2804,c_2938,c_4088,c_4425,c_5101,c_5122,c_6173,c_6162,c_6170,c_6498,c_9279,c_10527,c_13602,c_21104,c_23418,c_28234,c_28432,c_33314,c_36634,c_47096,c_81125,c_81475,c_81694,c_88970,c_121610,c_122435,c_122640]) ).
tcf(c_123054,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( X0 != multiply(sk_c4,sk_c9) ) ),
inference(resolution,[status(thm)],[c_122326,c_399]) ).
tcf(c_123670,plain,
! [X0: $i] :
( ( sk_c8 = multiply(inverse(X0),X0) )
| ( multiply(sk_c4,sk_c9) != identity ) ),
inference(resolution,[status(thm)],[c_123054,c_3666]) ).
tcf(c_123671,plain,
( ( sk_c8 = multiply(inverse(sk_c8),sk_c8) )
| ( multiply(sk_c4,sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_123670]) ).
tcf(c_123672,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_123671,c_122729,c_122334,c_121335,c_69063,c_54631,c_50064,c_39331,c_31331,c_16583,c_12336,c_10286,c_6005,c_2939,c_2461,c_1562,c_1449,c_898,c_888,c_786,c_397]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP313-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 14:26:30 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 25.82/5.20 % SZS status Started for theBenchmark.p
% 25.82/5.20 % SZS status Unsatisfiable for theBenchmark.p
% 25.82/5.20
% 25.82/5.20 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 25.82/5.20
% 25.82/5.20 % ------ iProver source info
% 25.82/5.20
% 25.82/5.20 % git: date: 2026-07-19 20:42:38 +0200
% 25.82/5.20 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 25.82/5.20 % git: non_committed_changes: false
% 25.82/5.20
% 25.82/5.20 % ------ Parsing...% successful
% 25.82/5.20
% 25.82/5.20
% 25.82/5.20 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 25.82/5.20
% 25.82/5.20 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 25.82/5.20
% 25.82/5.20 % ------ Preprocessing... gs_s sp: 6 0s gs_e snvd_s sp: 0 0s snvd_e %
% 25.82/5.20
% 25.82/5.20 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 25.82/5.20 % ------ Proving...
% 25.82/5.20 % ------ Problem Properties
% 25.82/5.20
% 25.82/5.20 %
% 25.82/5.20 % clauses 57
% 25.82/5.20 % conjectures 54
% 25.82/5.20 % EPR 0
% 25.82/5.20 % Horn 7
% 25.82/5.20 % unary 3
% 25.82/5.20 % binary 49
% 25.82/5.20 % lits 119
% 25.82/5.20 % lits eq 111
% 25.82/5.20 % fd_pure 0
% 25.82/5.20 % fd_pseudo 0
% 25.82/5.20 % fd_cond 0
% 25.82/5.20 % fd_pseudo_cond 0
% 25.82/5.20 % AC symbols 0
% 25.82/5.20
% 25.82/5.20 % ------ Input Options Time Limit: Unbounded
% 25.82/5.20
% 25.82/5.20
% 25.82/5.20 % ------
% 25.82/5.20 % Current options:
% 25.82/5.20 % ------
% 25.82/5.20
% 25.82/5.20
% 25.82/5.20 %
% 25.82/5.20
% 25.82/5.20 % ------ Proving...
% 25.82/5.20 %
% 25.82/5.20
% 25.82/5.20 % SZS status Unsatisfiable for theBenchmark.p
% 25.82/5.20
% 25.82/5.20 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 25.82/5.21
% 25.82/5.21
%------------------------------------------------------------------------------