%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP373-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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:33:26 PM UTC 2026
% Result : Unsatisfiable 39.94s 7.33s
% Output : CNFRefutation 39.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 45
% Syntax : Number of formulae : 526 ( 101 unt; 0 def)
% Number of atoms : 1228 (1155 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 1195 ( 493 ~; 702 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 3 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 338 ( 0 sgn 338 !; 0 ?; 303 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c3)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c10 = inverse(sk_c4)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c8 = inverse(sk_c5)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f14]) ).
fof(f23,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f24,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f28,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c10 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f29]) ).
fof(f41,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f42,plain,
( sk_c6 = multiply(sk_c7,sk_c8)
| sk_c10 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f48,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f52,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f54,plain,
( sk_c8 = inverse(sk_c5)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f56,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f58,plain,
( inverse(sk_c7) = sk_c6
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( inverse(sk_c6) = sk_c8
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f60,plain,
( sk_c8 = inverse(sk_c6)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_30) ).
fof(f62,plain,
( sk_c6 = multiply(sk_c7,sk_c8)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f61]) ).
fof(f65,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f68,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f69]) ).
fof(f77,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_38) ).
fof(f78,plain,
( inverse(sk_c7) = sk_c6
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f77]) ).
fof(f85,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f86,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f88,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f90,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f89]) ).
fof(f97,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f98,plain,
( inverse(sk_c7) = sk_c6
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f97]) ).
fof(f101,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_50) ).
fof(f102,plain,
( sk_c6 = multiply(sk_c7,sk_c8)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f101]) ).
fof(f103,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_51) ).
fof(f104,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f103]) ).
fof(f105,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_52) ).
fof(f106,plain,
( sk_c11 = inverse(sk_c3)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f105]) ).
fof(f107,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_53) ).
fof(f108,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f107]) ).
fof(f109,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_54) ).
fof(f110,plain,
( sk_c10 = inverse(sk_c4)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f109]) ).
fof(f111,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_55) ).
fof(f112,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f111]) ).
fof(f113,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_56) ).
fof(f114,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f113]) ).
fof(f115,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_57) ).
fof(f116,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f115]) ).
fof(f123,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| multiply(X5,sk_c10) != sk_c11
| inverse(X4) != X5
| multiply(X4,X5) != sk_c11
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != sk_c9
| inverse(X2) != sk_c11
| multiply(X2,sk_c11) != sk_c10
| inverse(X1) != sk_c9
| multiply(X1,sk_c9) != sk_c10
| multiply(sk_c11,sk_c9) != sk_c10
| inverse(X0) != sk_c11
| multiply(X0,sk_c11) != sk_c10
| inverse(sk_c11) != sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_61) ).
fof(f124,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c9 != inverse(X1)
| sk_c10 != multiply(X1,sk_c9)
| sk_c10 != multiply(sk_c11,sk_c9)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11)
| inverse(sk_c11) != sk_c10 ),
inference(reorient_equations,[],[f123]) ).
fof(f125,plain,
! [X2,X3,X0,X1,X6,X7,X4] :
( multiply(X6,inverse(X4)) != X7
| inverse(X4) != inverse(X7)
| inverse(X6) != X7
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c9 != inverse(X1)
| sk_c10 != multiply(X1,sk_c9)
| sk_c10 != multiply(sk_c11,sk_c9)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f124]) ).
fof(f126,plain,
! [X2,X3,X0,X1,X6,X4] :
( inverse(X6) != multiply(X6,inverse(X4))
| inverse(X4) != inverse(inverse(X6))
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c9 != inverse(X1)
| sk_c10 != multiply(X1,sk_c9)
| sk_c10 != multiply(sk_c11,sk_c9)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f125]) ).
tcf(c_113,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_114,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_118,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_120,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_128,negated_conjecture,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_135,negated_conjecture,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_140,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_143,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_145,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_148,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_153,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_158,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_159,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_163,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_165,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_166,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_167,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_168,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_169,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_170,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_171,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_172,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_176,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(sk_c11) != sk_c10 )
| ( inverse(X5) != sk_c10 )
| ( inverse(X4) != sk_c9 )
| ( inverse(X3) != sk_c11 )
| ( inverse(X2) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 )
| ( multiply(X5,sk_c10) != sk_c9 )
| ( multiply(X4,sk_c9) != sk_c10 )
| ( multiply(X3,sk_c11) != sk_c10 )
| ( multiply(X2,sk_c11) != sk_c10 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_725,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_176]) ).
tcf(c_726,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_176]) ).
tcf(c_727,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_176]) ).
tcf(c_728,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_176]) ).
tcf(c_729,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_176]) ).
tcf(c_730,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_731,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_732,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_733,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_734,plain,
( ( inverse(sk_c10) = inverse(sk_c10) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_736,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_730]) ).
tcf(c_740,plain,
( ~ iPr_def_13
| ( inverse(inverse(sk_c10)) != inverse(sk_c10) )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c11 )
| ( multiply(sk_c10,inverse(sk_c10)) != inverse(sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_1045,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1048,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c11) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1049,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != inverse(X0) )
| ( inverse(sk_c11) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1045]) ).
tcf(c_1050,plain,
! [X0: $i] :
( ( inverse(sk_c11) = inverse(X0) )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_1051,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != inverse(sk_c10) )
| ( inverse(sk_c11) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1049]) ).
tcf(c_1052,plain,
( ( inverse(sk_c11) = inverse(sk_c10) )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1050]) ).
tcf(c_1053,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c11) )
| ( sk_c10 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1054,plain,
( ( sk_c10 = inverse(sk_c11) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1053]) ).
tcf(c_1056,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1057,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1056]) ).
tcf(c_1059,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1071,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != sk_c11 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1072,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_730]) ).
tcf(c_1081,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1082,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1056]) ).
tcf(c_1087,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c11) )
| ( X1 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1108,plain,
( ( sk_c11 = multiply(identity,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1071]) ).
tcf(c_1109,plain,
multiply(identity,sk_c11) = sk_c11,
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_1111,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1112,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1111]) ).
tcf(c_1163,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( X0 != sk_c11 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_1166,plain,
! [X0: $i] :
( ( inverse(sk_c5) = X0 )
| ( X0 != sk_c8 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_1177,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_1198,plain,
( ( inverse(sk_c11) = inverse(multiply(sk_c5,sk_c8)) )
| ( sk_c11 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1050]) ).
tcf(c_1199,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != multiply(sk_c5,sk_c8) )
| ( X0 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1200,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(sk_c5,sk_c8) )
| ( sk_c11 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1199]) ).
tcf(c_1331,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_114,c_115]) ).
tcf(c_1390,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c3) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_1408,plain,
( ( inverse(sk_c5) = inverse(sk_c6) )
| ( inverse(sk_c6) != sk_c8 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1166]) ).
tcf(c_1416,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( X0 != sk_c11 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_1418,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( sk_c10 != sk_c11 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1416]) ).
tcf(c_1472,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != inverse(sk_c11) )
| ( inverse(X0) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1082]) ).
tcf(c_1473,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != inverse(sk_c11) )
| ( inverse(sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1472]) ).
tcf(c_1535,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(sk_c11) )
| ( inverse(sk_c11) != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1087]) ).
tcf(c_1564,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( X0 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1621,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1649,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c9)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_114,c_725]) ).
tcf(c_1664,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != inverse(sk_c11) )
| ( inverse(X0) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1177]) ).
tcf(c_1665,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != inverse(sk_c11) )
| ( inverse(sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1664]) ).
tcf(c_1995,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != multiply(sk_c5,sk_c8) )
| ( X0 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1111]) ).
tcf(c_1997,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != multiply(sk_c5,sk_c8) )
| ( sk_c11 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1995]) ).
tcf(c_1999,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != multiply(sk_c8,sk_c10) )
| ( X0 != multiply(sk_c8,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1111]) ).
tcf(c_2138,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1331,c_113]) ).
tcf(c_2154,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(inverse(sk_c3),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_136,c_2138]) ).
tcf(c_2155,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(inverse(sk_c3),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_116,c_2138]) ).
tcf(c_2156,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(inverse(sk_c4),sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_138,c_2138]) ).
tcf(c_2157,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(inverse(sk_c4),sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_118,c_2138]) ).
tcf(c_2169,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(inverse(sk_c11),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_153,c_2138]) ).
tcf(c_2171,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(inverse(sk_c11),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_149,c_2138]) ).
tcf(c_2172,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c11),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_147,c_2138]) ).
tcf(c_2173,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_113,c_2138]) ).
tcf(c_2174,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_2138]) ).
tcf(c_2185,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_2138,c_2138]) ).
tcf(c_2214,plain,
( ( inverse(sk_c3) = multiply(sk_c5,sk_c8) )
| ( inverse(sk_c3) != sk_c11 )
| ( multiply(sk_c5,sk_c8) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1163]) ).
tcf(c_2267,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_2281,plain,
! [X0: $i] :
( ( inverse(sk_c11) = X0 )
| ( X0 != inverse(multiply(sk_c5,sk_c8)) )
| ( inverse(sk_c11) != inverse(multiply(sk_c5,sk_c8)) ) ),
inference(instantiation,[status(thm)],[c_1048]) ).
tcf(c_2374,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c5,sk_c8) )
| ( X1 != X0 )
| ( multiply(sk_c5,sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_2377,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c5,sk_c8) )
| ( X1 != sk_c8 )
| ( X0 != sk_c5 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_2389,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c8,sk_c10) )
| ( X1 != sk_c10 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_2401,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_727,c_138]) ).
tcf(c_2402,plain,
( ( inverse(sk_c2) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_727,c_168]) ).
tcf(c_2442,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c11) )
| ( X0 != inverse(multiply(sk_c5,sk_c8)) )
| ( inverse(sk_c11) != inverse(multiply(sk_c5,sk_c8)) ) ),
inference(instantiation,[status(thm)],[c_1087]) ).
tcf(c_2457,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_729,c_149]) ).
tcf(c_2459,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_729,c_153]) ).
tcf(c_2543,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_726,c_136]) ).
tcf(c_2546,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_726,c_127]) ).
tcf(c_2551,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_726,c_126]) ).
tcf(c_2584,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c2),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_157,c_2138]) ).
tcf(c_2587,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(inverse(sk_c2),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_159,c_2138]) ).
tcf(c_2593,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(inverse(sk_c2),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_163,c_2138]) ).
tcf(c_2655,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(inverse(sk_c3),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_166,c_2138]) ).
tcf(c_2658,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(inverse(sk_c4),sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_168,c_2138]) ).
tcf(c_2664,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(inverse(sk_c8),sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_172,c_2138]) ).
tcf(c_2755,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_115,c_2138]) ).
tcf(c_3011,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( inverse(sk_c11) = sk_c10 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_731,c_117]) ).
tcf(c_3101,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_731,c_114]) ).
tcf(c_3105,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_731,c_730]) ).
tcf(c_3106,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_731,c_732]) ).
tcf(c_3113,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(X0,X1) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1564]) ).
tcf(c_3114,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,sk_c11) )
| ( X1 != sk_c11 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_3115,plain,
( ( sk_c11 = multiply(sk_c10,sk_c10) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(sk_c10,sk_c10) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_3113]) ).
tcf(c_3116,plain,
( ( multiply(sk_c10,sk_c10) = multiply(identity,sk_c11) )
| ( sk_c10 != identity )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3114]) ).
tcf(c_3159,plain,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( multiply(inverse(sk_c7),sk_c6) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_135,c_2138]) ).
tcf(c_3173,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_3192,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( multiply(inverse(sk_c4),sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_148,c_2138]) ).
tcf(c_3239,plain,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(inverse(sk_c7),sk_c6) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_165,c_2138]) ).
tcf(c_3306,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c3) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_136,c_726]) ).
tcf(c_3346,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(sk_c11) )
| ( inverse(sk_c11) != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1535]) ).
tcf(c_3347,plain,
( ( inverse(sk_c10) = inverse(sk_c11) )
| ( inverse(sk_c10) != inverse(sk_c10) )
| ( inverse(sk_c11) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_3346]) ).
tcf(c_3419,plain,
( ( inverse(sk_c11) = sk_c10 )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_118,c_727]) ).
tcf(c_3425,plain,
( ~ iPr_def_12
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_114,c_727]) ).
tcf(c_3459,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c7) )
| ( X0 != sk_c6 )
| ( inverse(sk_c7) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_1621]) ).
tcf(c_3511,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_113,c_728]) ).
tcf(c_3514,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c9 )
| ~ iPr_def_13
| ( multiply(X0,sk_c11) != inverse(X0) )
| ( inverse(inverse(X0)) != inverse(sk_c3) )
| ( multiply(sk_c3,inverse(sk_c3)) != sk_c11 )
| ( multiply(inverse(sk_c3),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_167,c_728]) ).
tcf(c_3521,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_13
| ( multiply(X0,sk_c8) != inverse(X0) )
| ( inverse(inverse(X0)) != inverse(sk_c5) )
| ( multiply(sk_c5,inverse(sk_c5)) != sk_c11 )
| ( multiply(inverse(sk_c5),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_141,c_728]) ).
tcf(c_3529,plain,
( ~ iPr_def_13
| ( inverse(sk_c10) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(sk_c10) )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3511]) ).
tcf(c_3545,plain,
( ( inverse(sk_c2) = sk_c9 )
| ~ iPr_def_13
| ( multiply(sk_c10,sk_c11) != inverse(sk_c10) )
| ( inverse(inverse(sk_c10)) != inverse(sk_c3) )
| ( multiply(sk_c3,inverse(sk_c3)) != sk_c11 )
| ( multiply(inverse(sk_c3),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3514]) ).
tcf(c_3679,plain,
( ( multiply(sk_c7,sk_c8) = inverse(sk_c7) )
| ( inverse(sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c8) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_3459]) ).
tcf(c_3864,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_2185,c_114]) ).
tcf(c_4513,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_167,c_3864]) ).
tcf(c_4514,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_137,c_3864]) ).
tcf(c_4515,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_117,c_3864]) ).
tcf(c_4516,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_169,c_3864]) ).
tcf(c_4517,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_139,c_3864]) ).
tcf(c_4519,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_171,c_3864]) ).
tcf(c_4520,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_141,c_3864]) ).
tcf(c_4521,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_121,c_3864]) ).
tcf(c_4593,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_733,c_731]) ).
tcf(c_4831,plain,
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_3105,c_120]) ).
tcf(c_4832,plain,
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_3105,c_140]) ).
tcf(c_4833,plain,
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_3105,c_170]) ).
tcf(c_4837,plain,
( ( sk_c11 = multiply(sk_c8,sk_c10) )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_3105,c_142]) ).
tcf(c_4847,plain,
( ( sk_c10 = multiply(sk_c1,sk_c11) )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_3105,c_129]) ).
tcf(c_4852,plain,
( ( sk_c10 = multiply(sk_c1,sk_c11) )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_3105,c_128]) ).
tcf(c_4867,plain,
( ( sk_c10 = multiply(sk_c2,sk_c9) )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_3105,c_159]) ).
tcf(c_4872,plain,
( ( sk_c10 = multiply(sk_c2,sk_c9) )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_3105,c_158]) ).
tcf(c_4883,plain,
! [X0: $i] : identity = multiply(inverse(X0),X0),
inference(resolution,[status(thm)],[c_3105,c_114]) ).
tcf(c_4935,plain,
! [X0: $i] :
( ( inverse(sk_c11) = inverse(X0) )
| ( inverse(sk_c11) != inverse(multiply(sk_c5,sk_c8)) )
| ( inverse(X0) != inverse(multiply(sk_c5,sk_c8)) ) ),
inference(instantiation,[status(thm)],[c_2281]) ).
tcf(c_4937,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(multiply(sk_c5,sk_c8)) )
| ( X0 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_4938,plain,
( ( inverse(sk_c11) = inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(multiply(sk_c5,sk_c8)) )
| ( inverse(sk_c11) != inverse(multiply(sk_c5,sk_c8)) ) ),
inference(instantiation,[status(thm)],[c_4935]) ).
tcf(c_4939,plain,
( ( inverse(sk_c10) = inverse(multiply(sk_c5,sk_c8)) )
| ( sk_c10 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_4937]) ).
tcf(c_5055,plain,
! [X0: $i,X1: $i] :
( ( sk_c3 = X0 )
| ( sk_c3 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_5118,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c11) )
| ( inverse(sk_c11) != inverse(multiply(sk_c5,sk_c8)) )
| ( inverse(X0) != inverse(multiply(sk_c5,sk_c8)) ) ),
inference(instantiation,[status(thm)],[c_2442]) ).
tcf(c_5120,plain,
( ( inverse(sk_c10) = inverse(sk_c11) )
| ( inverse(sk_c10) != inverse(multiply(sk_c5,sk_c8)) )
| ( inverse(sk_c11) != inverse(multiply(sk_c5,sk_c8)) ) ),
inference(instantiation,[status(thm)],[c_5118]) ).
tcf(c_5253,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_4513,c_166]) ).
tcf(c_5280,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_4514,c_136]) ).
tcf(c_5367,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_4515,c_116]) ).
tcf(c_5541,plain,
! [X0: $i] :
( ( multiply(sk_c5,X0) = multiply(sk_c5,sk_c8) )
| ( sk_c5 != sk_c5 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_2377]) ).
tcf(c_5542,plain,
sk_c5 = sk_c5,
inference(instantiation,[status(thm)],[c_730]) ).
tcf(c_5574,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_4516,c_168]) ).
tcf(c_5735,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_4517,c_138]) ).
tcf(c_5940,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_4519,c_170]) ).
tcf(c_6810,plain,
( ( sk_c9 = identity )
| ( multiply(inverse(sk_c9),identity) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_5574,c_2174]) ).
tcf(c_6826,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( multiply(inverse(sk_c9),multiply(identity,X0)) = multiply(sk_c2,X0) ) ),
inference(superposition,[status(thm)],[c_6810,c_115]) ).
tcf(c_6864,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1331,c_113]) ).
tcf(c_7007,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_139,c_2156]) ).
tcf(c_7014,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_7007,c_6864]) ).
tcf(c_7188,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_7014,c_114]) ).
tcf(c_7199,plain,
( ( sk_c9 = identity )
| ( multiply(inverse(sk_c11),identity) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_7188,c_2174]) ).
tcf(c_7209,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( multiply(inverse(sk_c11),multiply(identity,X0)) = multiply(sk_c1,X0) ) ),
inference(superposition,[status(thm)],[c_7199,c_115]) ).
tcf(c_7684,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c3) )
| ( inverse(sk_c11) = sk_c10 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_3011,c_3105]) ).
tcf(c_10011,plain,
( ( sk_c10 = multiply(sk_c1,sk_c11) )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_4852,c_727]) ).
tcf(c_10188,plain,
( ( sk_c10 = multiply(sk_c2,sk_c9) )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_4872,c_727]) ).
tcf(c_10436,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_3306,c_137,c_2543]) ).
tcf(c_11407,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c5),X0) = multiply(sk_c8,sk_c10) )
| ( X0 != sk_c10 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_2389]) ).
tcf(c_11411,plain,
( ( multiply(inverse(sk_c5),sk_c10) = multiply(sk_c8,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_11407]) ).
tcf(c_11537,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( X0 != multiply(sk_c5,sk_c8) )
| ( inverse(sk_c3) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1390]) ).
tcf(c_11539,plain,
( ( inverse(sk_c3) = sk_c10 )
| ( sk_c10 != multiply(sk_c5,sk_c8) )
| ( inverse(sk_c3) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_11537]) ).
tcf(c_12566,plain,
( ( inverse(sk_c2) = sk_c9 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_2402,c_169,c_2402]) ).
tcf(c_12739,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_2543,c_10436]) ).
tcf(c_12750,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ~ iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_2551,c_12739]) ).
tcf(c_12758,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_2546,c_12739]) ).
tcf(c_13795,plain,
( ( sk_c10 = multiply(sk_c1,sk_c11) )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_10011,c_4847,c_10011]) ).
tcf(c_13827,plain,
( ( sk_c10 = multiply(sk_c2,sk_c9) )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_10188,c_4867,c_10188]) ).
tcf(c_13864,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_13865,plain,
( ( sk_c10 = multiply(sk_c10,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_13864]) ).
tcf(c_13951,plain,
( ( multiply(sk_c5,inverse(sk_c5)) = multiply(sk_c5,sk_c8) )
| ( sk_c5 != sk_c5 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_5541]) ).
tcf(c_14363,plain,
! [X0: $i] :
( ( sk_c3 = X0 )
| ( sk_c3 != sk_c3 )
| ( X0 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_5055]) ).
tcf(c_14364,plain,
sk_c3 = sk_c3,
inference(instantiation,[status(thm)],[c_730]) ).
tcf(c_14365,plain,
( ( sk_c3 = sk_c10 )
| ( sk_c3 != sk_c3 )
| ( sk_c10 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_14363]) ).
tcf(c_15632,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c9,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_5574,c_114]) ).
tcf(c_16022,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1331,c_113]) ).
tcf(c_16118,plain,
! [X0: $i] : multiply(inverse(inverse(inverse(X0))),X0) = identity,
inference(superposition,[status(thm)],[c_2174,c_16022]) ).
tcf(c_16232,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_139,c_2156]) ).
tcf(c_16241,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_10
| ( inverse(sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_16232,c_725]) ).
tcf(c_16247,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_119,c_2157]) ).
tcf(c_16253,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_16247,c_16022]) ).
tcf(c_16411,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_12
| ( inverse(inverse(sk_c11)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_2172,c_727]) ).
tcf(c_16517,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_169,c_2658]) ).
tcf(c_16536,plain,
( ( inverse(sk_c2) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_16517,c_725]) ).
tcf(c_16571,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_16253,c_114]) ).
tcf(c_16594,plain,
( ( inverse(sk_c2) = sk_c9 )
| ~ iPr_def_11
| ( inverse(inverse(sk_c8)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_2664,c_726]) ).
tcf(c_17104,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X0)),identity) = X1,
inference(superposition,[status(thm)],[c_114,c_2755]) ).
tcf(c_17176,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,identity)),multiply(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_113,c_2755]) ).
tcf(c_17177,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,identity)) = X1,
inference(superposition,[status(thm)],[c_114,c_2755]) ).
tcf(c_17291,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(inverse(inverse(X1))))),multiply(X0,identity)) = X1,
inference(superposition,[status(thm)],[c_16118,c_2755]) ).
tcf(c_17307,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_17291,c_17177]) ).
tcf(c_17371,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1649,c_17307]) ).
tcf(c_17372,plain,
inverse(inverse(sk_c10)) = sk_c10,
inference(instantiation,[status(thm)],[c_17307]) ).
tcf(c_17470,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(X0),identity)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_17176]) ).
tcf(c_18257,plain,
( ( multiply(sk_c5,inverse(sk_c5)) = sk_c11 )
| ( sk_c11 != multiply(sk_c5,sk_c8) )
| ( multiply(sk_c5,inverse(sk_c5)) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1995]) ).
tcf(c_18388,plain,
! [X0: $i] : multiply(inverse(X0),identity) = inverse(X0),
inference(superposition,[status(thm)],[c_2174,c_17470]) ).
tcf(c_18399,plain,
multiply(inverse(identity),identity) = inverse(inverse(identity)),
inference(superposition,[status(thm)],[c_16118,c_17470]) ).
tcf(c_18437,plain,
inverse(inverse(identity)) = inverse(identity),
inference(demodulation,[status(thm)],[c_18399,c_18388]) ).
tcf(c_18531,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c5),X0) = sk_c11 )
| ( sk_c11 != multiply(sk_c8,sk_c10) )
| ( multiply(inverse(sk_c5),X0) != multiply(sk_c8,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1999]) ).
tcf(c_18533,plain,
( ( multiply(inverse(sk_c5),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(sk_c8,sk_c10) )
| ( multiply(inverse(sk_c5),sk_c10) != multiply(sk_c8,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_18531]) ).
tcf(c_18854,plain,
( ( sk_c9 = identity )
| ( multiply(inverse(multiply(inverse(identity),sk_c9)),identity) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_15632,c_17104]) ).
tcf(c_21498,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_3173]) ).
tcf(c_21503,plain,
( ( sk_c11 = identity )
| ( identity != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_21498]) ).
tcf(c_21531,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c5,sk_c8) )
| ( X0 != identity )
| ( multiply(sk_c5,sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_2374]) ).
tcf(c_21534,plain,
( ( sk_c10 = multiply(sk_c5,sk_c8) )
| ( sk_c10 != identity )
| ( multiply(sk_c5,sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_21531]) ).
tcf(c_22517,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_4883,c_731]) ).
tcf(c_22518,plain,
( ( identity = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_22517]) ).
tcf(c_22521,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X2,X0) = identity )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_4883,c_4593]) ).
tcf(c_22522,plain,
( ( multiply(sk_c10,sk_c10) = identity )
| ( sk_c10 != sk_c10 )
| ( sk_c10 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_22521]) ).
tcf(c_22585,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_16241,c_5280,c_17371]) ).
tcf(c_22623,plain,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ~ iPr_def_12 ),
inference(resolution,[status(thm)],[c_13795,c_3105]) ).
tcf(c_22791,plain,
( ( inverse(sk_c2) = sk_c9 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_16536,c_5253,c_17371]) ).
tcf(c_22799,plain,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ~ iPr_def_12 ),
inference(resolution,[status(thm)],[c_13827,c_3105]) ).
tcf(c_22800,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ~ iPr_def_12
| ( X0 != multiply(sk_c2,sk_c9) ) ),
inference(resolution,[status(thm)],[c_13827,c_731]) ).
tcf(c_23863,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_12
| ( inverse(sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_16571,c_16411]) ).
tcf(c_23959,plain,
( ~ iPr_def_11
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_12750,c_726]) ).
tcf(c_23975,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_23959,c_12758,c_23959]) ).
tcf(c_24468,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_16594,c_12758,c_23959]) ).
tcf(c_30834,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),X0) )
| ~ iPr_def_12
| ( multiply(sk_c2,sk_c9) != identity ) ),
inference(resolution,[status(thm)],[c_22800,c_3101]) ).
tcf(c_30835,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ~ iPr_def_12
| ( multiply(sk_c2,sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_30834]) ).
tcf(c_31332,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( inverse(X0) = X1 )
| ( X1 != sk_c11 )
| ( X0 != sk_c3 ) ),
inference(resolution,[status(thm)],[c_7684,c_3106]) ).
tcf(c_31333,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != sk_c3 )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_31332]) ).
tcf(c_31804,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_729,c_24468]) ).
tcf(c_31964,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c9,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_5253,c_114]) ).
tcf(c_31968,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c9,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_5574,c_114]) ).
tcf(c_32010,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(sk_c9,multiply(sk_c2,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_31964,c_115]) ).
tcf(c_32011,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(sk_c9,multiply(sk_c2,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_32010,c_113]) ).
tcf(c_32119,plain,
( ( sk_c11 = identity )
| ( multiply(inverse(sk_c9),identity) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_5940,c_2174]) ).
tcf(c_32120,plain,
( ( sk_c9 = identity )
| ( multiply(inverse(sk_c9),identity) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_5574,c_2174]) ).
tcf(c_32134,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( multiply(inverse(sk_c9),multiply(identity,X0)) = multiply(sk_c2,X0) ) ),
inference(superposition,[status(thm)],[c_32119,c_115]) ).
tcf(c_32137,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( multiply(inverse(sk_c9),multiply(identity,X0)) = multiply(sk_c2,X0) ) ),
inference(superposition,[status(thm)],[c_32120,c_115]) ).
tcf(c_32169,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1331,c_113]) ).
tcf(c_32252,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(inverse(sk_c9),X0) = multiply(sk_c2,X0) ) ),
inference(superposition,[status(thm)],[c_32011,c_32169]) ).
tcf(c_32289,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c2,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_32252,c_114]) ).
tcf(c_32315,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_137,c_2154]) ).
tcf(c_32323,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,multiply(sk_c10,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_32315,c_115]) ).
tcf(c_32329,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_117,c_2155]) ).
tcf(c_32335,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(inverse(sk_c11),sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_32329,c_32169]) ).
tcf(c_32341,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_139,c_2156]) ).
tcf(c_32359,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_32289,c_157]) ).
tcf(c_32430,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_32341,c_32169]) ).
tcf(c_32537,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_32335,c_114]) ).
tcf(c_32761,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_32430,c_114]) ).
tcf(c_32772,plain,
( ( sk_c9 = identity )
| ( multiply(inverse(sk_c11),identity) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_32761,c_2174]) ).
tcf(c_32779,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( multiply(inverse(sk_c11),multiply(identity,X0)) = multiply(sk_c1,X0) ) ),
inference(superposition,[status(thm)],[c_32772,c_115]) ).
tcf(c_32799,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_167,c_2655]) ).
tcf(c_32808,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c11,multiply(sk_c10,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_32799,c_115]) ).
tcf(c_33439,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X0)),identity) = X1,
inference(superposition,[status(thm)],[c_114,c_2755]) ).
tcf(c_33523,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,identity)),multiply(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_113,c_2755]) ).
tcf(c_33524,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,identity)) = X1,
inference(superposition,[status(thm)],[c_114,c_2755]) ).
tcf(c_33620,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(inverse(multiply(X0,sk_c11)),multiply(X0,multiply(sk_c11,X1))) = multiply(sk_c10,X1) ) ),
inference(superposition,[status(thm)],[c_32808,c_2755]) ).
tcf(c_33621,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(inverse(multiply(X0,sk_c11)),multiply(X0,multiply(sk_c11,X1))) = multiply(sk_c10,X1) ) ),
inference(superposition,[status(thm)],[c_32323,c_2755]) ).
tcf(c_33707,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(demodulation,[status(thm)],[c_33621,c_2755]) ).
tcf(c_33708,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(demodulation,[status(thm)],[c_33620,c_2755]) ).
tcf(c_33709,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c10,sk_c10) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_33708]) ).
tcf(c_33710,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c10,sk_c10) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_33707]) ).
tcf(c_33918,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,multiply(X1,identity))),multiply(multiply(X0,X1),X2)) = X2,
inference(superposition,[status(thm)],[c_115,c_33523]) ).
tcf(c_33983,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(X0),identity)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_33523]) ).
tcf(c_34010,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(X0),identity)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_32169,c_33523]) ).
tcf(c_34192,plain,
! [X0: $i] : multiply(inverse(X0),identity) = inverse(X0),
inference(superposition,[status(thm)],[c_2174,c_33983]) ).
tcf(c_34424,plain,
( ( sk_c9 = identity )
| ( multiply(inverse(multiply(inverse(identity),sk_c9)),identity) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_31968,c_33439]) ).
tcf(c_34938,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_2174,c_34192]) ).
tcf(c_34943,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1649,c_34938]) ).
tcf(c_34983,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_34192,c_2173]) ).
tcf(c_34993,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c11) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_32359,c_34938]) ).
tcf(c_34994,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c11) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_167,c_34938]) ).
tcf(c_35019,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(superposition,[status(thm)],[c_34938,c_34192]) ).
tcf(c_35021,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_34938,c_114]) ).
tcf(c_35323,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(inverse(multiply(sk_c11,identity)),X0) = multiply(sk_c3,X0) ) ),
inference(superposition,[status(thm)],[c_32359,c_34010]) ).
tcf(c_35359,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,identity)),X1) = multiply(inverse(X0),X1),
inference(superposition,[status(thm)],[c_34938,c_34010]) ).
tcf(c_35391,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(inverse(sk_c11),X0) = multiply(sk_c3,X0) ) ),
inference(demodulation,[status(thm)],[c_35323,c_35359]) ).
tcf(c_37369,plain,
( ( sk_c10 = identity )
| ( sk_c10 = sk_c3 ) ),
inference(superposition,[status(thm)],[c_34993,c_32537]) ).
tcf(c_37465,plain,
( ( sk_c10 = sk_c3 )
| ( inverse(sk_c10) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_37369,c_34983]) ).
tcf(c_37519,plain,
inverse(sk_c11) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_3419,c_736,c_1051,c_1057,c_1198,c_1997,c_4521,c_4831,c_4938,c_4939,c_5367,c_21534,c_31333,c_37465]) ).
tcf(c_37531,plain,
( ( sk_c10 = sk_c3 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_34994,c_37519]) ).
tcf(c_37540,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_2171,c_37519]) ).
tcf(c_37542,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_2169,c_37519]) ).
tcf(c_37561,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_31804,c_37519]) ).
tcf(c_37574,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(equality_resolution_simp,[status(thm)],[c_37561]) ).
tcf(c_37576,plain,
multiply(sk_c11,sk_c10) = identity,
inference(superposition,[status(thm)],[c_37519,c_35021]) ).
tcf(c_37579,plain,
multiply(sk_c10,sk_c11) = identity,
inference(superposition,[status(thm)],[c_37519,c_114]) ).
tcf(c_38306,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_12
| ( inverse(sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_37540,c_727]) ).
tcf(c_38432,plain,
( ( inverse(sk_c7) = sk_c6 )
| ~ iPr_def_12
| ( inverse(sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_37542,c_727]) ).
tcf(c_38456,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(X1))),X0) = X1,
inference(light_normalisation,[status(thm)],[c_33524,c_35019]) ).
tcf(c_38459,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,multiply(X1,inverse(X2)))),multiply(X0,X1)) = X2,
inference(superposition,[status(thm)],[c_115,c_38456]) ).
tcf(c_38477,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(inverse(multiply(X0,sk_c8)),X0) = sk_c5 ) ),
inference(superposition,[status(thm)],[c_171,c_38456]) ).
tcf(c_38478,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(inverse(multiply(X0,sk_c8)),X0) = sk_c5 ) ),
inference(superposition,[status(thm)],[c_141,c_38456]) ).
tcf(c_43683,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_2267]) ).
tcf(c_43684,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c9 != identity )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_43683]) ).
tcf(c_46880,plain,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(inverse(sk_c11),sk_c5) = sk_c5 ) ),
inference(superposition,[status(thm)],[c_170,c_38477]) ).
tcf(c_47032,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_1111]) ).
tcf(c_47033,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c11 )
| ( sk_c11 != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_47032]) ).
tcf(c_47705,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(X1) )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_47706,plain,
( ( inverse(inverse(sk_c10)) = inverse(sk_c10) )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_47705]) ).
tcf(c_47707,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(inverse(X0)) = inverse(X2) )
| ( inverse(X2) != X1 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_47708,plain,
! [X0: $i] :
( ( multiply(sk_c3,inverse(sk_c3)) = sk_c11 )
| ( sk_c11 != X0 )
| ( multiply(sk_c3,inverse(sk_c3)) != X0 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_47725,plain,
inverse(identity) = inverse(identity),
inference(instantiation,[status(thm)],[c_730]) ).
tcf(c_47726,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(identity) )
| ( inverse(identity) != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_47728,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_47745,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X0)) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_47746,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = sk_c11 )
| ( sk_c11 != sk_c10 )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_47745]) ).
tcf(c_47750,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(sk_c5) )
| ( inverse(sk_c5) != X1 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_47707]) ).
tcf(c_47758,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c3,inverse(sk_c3)) = sk_c11 )
| ( sk_c11 != multiply(X0,X1) )
| ( multiply(sk_c3,inverse(sk_c3)) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_47708]) ).
tcf(c_47759,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c3,inverse(sk_c3)) = multiply(X1,X0) )
| ( sk_c3 != X1 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_47760,plain,
( ( multiply(sk_c3,inverse(sk_c3)) = sk_c11 )
| ( sk_c11 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c3,inverse(sk_c3)) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_47758]) ).
tcf(c_47761,plain,
( ( multiply(sk_c3,inverse(sk_c3)) = multiply(sk_c10,sk_c10) )
| ( sk_c3 != sk_c10 )
| ( inverse(sk_c3) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_47759]) ).
tcf(c_47808,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = X2 )
| ( X2 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_47810,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = multiply(X2,X1) )
| ( X0 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_47812,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = multiply(sk_c10,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_47810]) ).
tcf(c_47822,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(sk_c5) )
| ( inverse(sk_c5) != inverse(X1) )
| ( inverse(inverse(X0)) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_47750]) ).
tcf(c_47904,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c11) = inverse(X0) )
| ( inverse(X0) != X1 )
| ( multiply(X0,sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_47905,plain,
( ( multiply(sk_c10,sk_c11) = inverse(sk_c10) )
| ( inverse(sk_c10) != sk_c10 )
| ( multiply(sk_c10,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_47904]) ).
tcf(c_47992,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c11) = X2 )
| ( X2 != X1 )
| ( multiply(X0,sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_47994,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c11) = multiply(X1,X2) )
| ( sk_c11 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_47996,plain,
( ( multiply(sk_c10,sk_c11) = multiply(sk_c10,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_47994]) ).
tcf(c_48008,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(sk_c3) )
| ( inverse(sk_c3) != X1 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_47707]) ).
tcf(c_48009,plain,
( ( inverse(inverse(sk_c10)) = inverse(sk_c3) )
| ( inverse(sk_c3) != sk_c10 )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_48008]) ).
tcf(c_48028,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( sk_c10 != X0 )
| ( multiply(sk_c11,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_48116,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,inverse(X0)) = X3 )
| ( X3 != multiply(X1,X2) )
| ( multiply(X0,inverse(X0)) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_47808]) ).
tcf(c_48118,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c10,inverse(sk_c10)) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_48116]) ).
tcf(c_48186,plain,
! [X0: $i,X1: $i] :
( ( inverse(identity) = X1 )
| ( X1 != X0 )
| ( inverse(identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_48219,plain,
! [X0: $i,X1: $i] :
( ( inverse(multiply(X0,X1)) = inverse(identity) )
| ( multiply(X0,X1) != identity ) ),
inference(instantiation,[status(thm)],[c_47728]) ).
tcf(c_48221,plain,
( ( inverse(multiply(sk_c10,sk_c10)) = inverse(identity) )
| ( multiply(sk_c10,sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_48219]) ).
tcf(c_48493,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( sk_c10 != multiply(X0,X1) )
| ( multiply(sk_c11,sk_c9) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_48028]) ).
tcf(c_48494,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c9) = multiply(X0,X1) )
| ( sk_c9 != X1 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_48495,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c11,sk_c9) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_48493]) ).
tcf(c_48496,plain,
( ( multiply(sk_c11,sk_c9) = multiply(sk_c10,sk_c10) )
| ( sk_c9 != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_48494]) ).
tcf(c_48594,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(multiply(X1,X2)) )
| ( X0 != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_48595,plain,
( ( inverse(sk_c10) = inverse(multiply(sk_c10,sk_c10)) )
| ( sk_c10 != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_48594]) ).
tcf(c_48903,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,sk_c11) = X3 )
| ( X3 != multiply(X1,X2) )
| ( multiply(X0,sk_c11) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_47992]) ).
tcf(c_48905,plain,
( ( multiply(sk_c10,sk_c11) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c10,sk_c11) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_48903]) ).
tcf(c_49494,plain,
! [X0: $i] :
( ( inverse(identity) = X0 )
| ( X0 != inverse(identity) )
| ( inverse(identity) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_48186]) ).
tcf(c_50762,plain,
! [X0: $i] :
( ( inverse(inverse(X0)) = inverse(sk_c6) )
| ( inverse(X0) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_47705]) ).
tcf(c_50850,plain,
! [X0: $i] :
( ( inverse(inverse(X0)) = inverse(sk_c5) )
| ( inverse(sk_c5) != inverse(sk_c6) )
| ( inverse(inverse(X0)) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_47822]) ).
tcf(c_51093,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_51095,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X1,X2) )
| ( sk_c10 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_51097,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(sk_c10,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_51095]) ).
tcf(c_51709,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(identity)) = inverse(X1) )
| ( inverse(X1) != X0 )
| ( inverse(inverse(identity)) != X0 ) ),
inference(instantiation,[status(thm)],[c_47707]) ).
tcf(c_52155,plain,
( ( inverse(inverse(sk_c7)) = inverse(sk_c6) )
| ( inverse(sk_c7) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_50762]) ).
tcf(c_52301,plain,
inverse(sk_c2) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_46880,c_167,c_170,c_736,c_729,c_1054,c_1072,c_1108,c_1109,c_1198,c_1200,c_1665,c_1997,c_2214,c_2655,c_3115,c_3116,c_3545,c_4519,c_4833,c_4939,c_5120,c_5253,c_5574,c_11539,c_12566,c_13865,c_14365,c_14364,c_17372,c_21534,c_22791,c_23975,c_33709,c_37519,c_37531,c_43684,c_47760,c_47761,c_47905,c_47996,c_48009,c_48495,c_48496,c_48905]) ).
tcf(c_52349,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c9,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_2593,c_52301]) ).
tcf(c_52351,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_2587,c_52301]) ).
tcf(c_52352,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_2584,c_52301]) ).
tcf(c_52370,plain,
multiply(sk_c2,sk_c9) = identity,
inference(superposition,[status(thm)],[c_52301,c_35021]) ).
tcf(c_52371,plain,
inverse(sk_c9) = sk_c2,
inference(superposition,[status(thm)],[c_52301,c_34938]) ).
tcf(c_52810,plain,
! [X0: $i,X1: $i] :
( ( inverse(identity) = inverse(multiply(X0,X1)) )
| ( inverse(identity) != inverse(identity) )
| ( inverse(multiply(X0,X1)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_49494]) ).
tcf(c_52811,plain,
( ( inverse(identity) = inverse(multiply(sk_c10,sk_c10)) )
| ( inverse(identity) != inverse(identity) )
| ( inverse(multiply(sk_c10,sk_c10)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_52810]) ).
tcf(c_53617,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X1)) = inverse(X0) )
| ( inverse(X0) != X2 )
| ( multiply(X0,inverse(X1)) != X2 ) ),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_53618,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = inverse(sk_c10) )
| ( inverse(sk_c10) != sk_c10 )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_53617]) ).
tcf(c_53755,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(identity) )
| ( inverse(identity) != inverse(multiply(X1,X2)) )
| ( inverse(X0) != inverse(multiply(X1,X2)) ) ),
inference(instantiation,[status(thm)],[c_47726]) ).
tcf(c_53758,plain,
( ( inverse(sk_c10) = inverse(identity) )
| ( inverse(identity) != inverse(multiply(sk_c10,sk_c10)) )
| ( inverse(sk_c10) != inverse(multiply(sk_c10,sk_c10)) ) ),
inference(instantiation,[status(thm)],[c_53755]) ).
tcf(c_56185,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(inverse(X0),sk_c10) = X3 )
| ( X3 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_51093]) ).
tcf(c_56187,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_56185]) ).
tcf(c_56552,plain,
( ( inverse(inverse(sk_c7)) = inverse(sk_c5) )
| ( inverse(sk_c5) != inverse(sk_c6) )
| ( inverse(inverse(sk_c7)) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_50850]) ).
tcf(c_57932,plain,
! [X0: $i] :
( ( inverse(inverse(identity)) = inverse(X0) )
| ( inverse(X0) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_51709]) ).
tcf(c_57941,plain,
( ( inverse(inverse(identity)) = inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_57932]) ).
tcf(c_63135,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_13
| ( multiply(sk_c7,sk_c8) != inverse(sk_c7) )
| ( inverse(inverse(sk_c7)) != inverse(sk_c5) )
| ( multiply(sk_c5,inverse(sk_c5)) != sk_c11 )
| ( multiply(inverse(sk_c5),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3521]) ).
tcf(c_63549,plain,
inverse(sk_c1) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_38478,c_144,c_143,c_141,c_139,c_145,c_736,c_1200,c_1408,c_2401,c_3679,c_4520,c_4832,c_4837,c_5280,c_5542,c_5735,c_11411,c_13865,c_13951,c_18257,c_18533,c_21534,c_22585,c_33710,c_37574,c_43684,c_48495,c_48496,c_52155,c_56552,c_63135]) ).
tcf(c_63617,plain,
multiply(sk_c1,sk_c11) = identity,
inference(superposition,[status(thm)],[c_63549,c_35021]) ).
tcf(c_63618,plain,
inverse(sk_c11) = sk_c1,
inference(superposition,[status(thm)],[c_63549,c_34938]) ).
tcf(c_63758,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(sk_c3,X0) = multiply(sk_c1,X0) ) ),
inference(light_normalisation,[status(thm)],[c_35391,c_63618]) ).
tcf(c_63770,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_63758,c_126]) ).
tcf(c_63796,plain,
sk_c10 = identity,
inference(light_normalisation,[status(thm)],[c_63770,c_63617]) ).
tcf(c_63847,plain,
multiply(sk_c10,sk_c11) = sk_c10,
inference(demodulation,[status(thm)],[c_37579,c_63796]) ).
tcf(c_63851,plain,
( ~ iPr_def_10
| ( sk_c10 != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_34943,c_63796]) ).
tcf(c_63870,plain,
! [X0: $i] : multiply(sk_c10,X0) = X0,
inference(demodulation,[status(thm)],[c_113,c_63796]) ).
tcf(c_63871,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm)],[c_63847,c_63870]) ).
tcf(c_63876,plain,
~ iPr_def_10,
inference(equality_resolution_simp,[status(thm)],[c_63851]) ).
tcf(c_63947,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(instantiation,[status(thm)],[c_63870]) ).
tcf(c_63977,plain,
inverse(sk_c7) = sk_c6,
inference(global_subsumption_just,[status(thm)],[c_52349,c_734,c_736,c_740,c_1052,c_1054,c_1665,c_2459,c_3347,c_13865,c_23975,c_37519,c_38432,c_47033,c_47706,c_47746,c_47812,c_48118,c_51097,c_53618,c_56187,c_63876,c_63871,c_63947]) ).
tcf(c_63981,plain,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c6,sk_c6) = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_3239,c_63977]) ).
tcf(c_63983,plain,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( multiply(sk_c6,sk_c6) = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_3159,c_63977]) ).
tcf(c_64007,plain,
inverse(sk_c4) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_52351,c_734,c_736,c_1051,c_1052,c_1054,c_1057,c_1198,c_1473,c_1665,c_1997,c_2457,c_3347,c_3529,c_4521,c_4831,c_4938,c_4939,c_5367,c_12758,c_13865,c_18437,c_21534,c_22522,c_23959,c_31333,c_37465,c_38306,c_47033,c_47725,c_47746,c_47812,c_48118,c_48221,c_48595,c_51097,c_52811,c_53758,c_56187,c_57941,c_63876,c_63871,c_63947]) ).
tcf(c_64009,plain,
inverse(sk_c4) = sk_c11,
inference(light_normalisation,[status(thm)],[c_64007,c_63871]) ).
tcf(c_64013,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(demodulation,[status(thm)],[c_3192,c_64009]) ).
tcf(c_64024,plain,
inverse(sk_c3) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_52352,c_734,c_736,c_729,c_1051,c_1052,c_1054,c_1057,c_1198,c_1473,c_1665,c_1997,c_3347,c_3425,c_3529,c_4521,c_4831,c_4938,c_4939,c_5367,c_12758,c_13865,c_17372,c_18437,c_21534,c_22522,c_23863,c_23959,c_31333,c_37465,c_47033,c_47725,c_47746,c_47812,c_48118,c_48221,c_48595,c_51097,c_52811,c_53758,c_56187,c_57941,c_63876,c_63871,c_63947,c_64013]) ).
tcf(c_64032,plain,
inverse(sk_c11) = sk_c3,
inference(superposition,[status(thm)],[c_64024,c_34938]) ).
tcf(c_64056,plain,
multiply(sk_c2,sk_c9) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_63981,c_734,c_736,c_740,c_729,c_1052,c_1054,c_1665,c_3347,c_13865,c_22799,c_23975,c_37519,c_47033,c_47706,c_47746,c_47812,c_48118,c_51097,c_53618,c_56187,c_63876,c_63871,c_63947,c_64013]) ).
tcf(c_64058,plain,
multiply(sk_c2,sk_c9) = sk_c11,
inference(light_normalisation,[status(thm)],[c_64056,c_52370,c_63871]) ).
tcf(c_64082,plain,
multiply(sk_c1,sk_c11) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_63983,c_734,c_736,c_729,c_1051,c_1052,c_1054,c_1057,c_1198,c_1473,c_1665,c_1997,c_3347,c_3529,c_4521,c_4831,c_4938,c_4939,c_5367,c_12758,c_13865,c_18437,c_21534,c_22522,c_22623,c_23959,c_31333,c_37465,c_47033,c_47725,c_47746,c_47812,c_48118,c_48221,c_48595,c_51097,c_52811,c_53758,c_56187,c_57941,c_63876,c_63871,c_63947,c_64013]) ).
tcf(c_64084,plain,
multiply(sk_c1,sk_c11) = sk_c11,
inference(light_normalisation,[status(thm)],[c_64082,c_63617,c_63871]) ).
tcf(c_64093,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c11,X0)) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_64084,c_115]) ).
tcf(c_64173,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,multiply(X1,sk_c11))),multiply(X0,X1)) = sk_c3,
inference(superposition,[status(thm)],[c_64024,c_38459]) ).
tcf(c_64178,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,multiply(X1,sk_c11))),multiply(X0,X1)) = sk_c1,
inference(superposition,[status(thm)],[c_63549,c_38459]) ).
tcf(c_64202,plain,
sk_c3 = sk_c1,
inference(light_normalisation,[status(thm)],[c_64173,c_64178]) ).
tcf(c_64320,plain,
sk_c11 = identity,
inference(global_subsumption_just,[status(thm)],[c_32134,c_734,c_736,c_729,c_1051,c_1052,c_1054,c_1057,c_1198,c_1473,c_1665,c_1997,c_3347,c_3529,c_4521,c_4831,c_4938,c_4939,c_5367,c_12758,c_13865,c_18437,c_21503,c_21534,c_22518,c_22522,c_23959,c_30835,c_31333,c_37465,c_47033,c_47725,c_47746,c_47812,c_48118,c_48221,c_48595,c_51097,c_52370,c_52811,c_53758,c_56187,c_57941,c_63876,c_63871,c_63947,c_64013]) ).
tcf(c_64323,plain,
! [X0: $i] : multiply(inverse(sk_c9),multiply(identity,X0)) = multiply(sk_c2,X0),
inference(global_subsumption_just,[status(thm)],[c_32137,c_734,c_736,c_729,c_1051,c_1052,c_1054,c_1057,c_1198,c_1473,c_1665,c_1997,c_3347,c_3425,c_3529,c_4521,c_4831,c_4938,c_4939,c_5367,c_6826,c_12758,c_13865,c_17372,c_18437,c_21534,c_22522,c_23959,c_31333,c_37465,c_47033,c_47725,c_47746,c_47812,c_48118,c_48221,c_48595,c_51097,c_52811,c_53758,c_56187,c_57941,c_63876,c_63871,c_63947,c_64013]) ).
tcf(c_64326,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c11,X0)) = multiply(sk_c2,X0),
inference(light_normalisation,[status(thm)],[c_64323,c_52371,c_64320]) ).
tcf(c_64346,plain,
! [X0: $i] : multiply(inverse(sk_c11),multiply(identity,X0)) = multiply(sk_c1,X0),
inference(global_subsumption_just,[status(thm)],[c_32779,c_734,c_736,c_729,c_1051,c_1052,c_1054,c_1057,c_1198,c_1473,c_1665,c_1997,c_3347,c_3425,c_3529,c_4521,c_4831,c_4938,c_4939,c_5367,c_7209,c_12758,c_13865,c_17372,c_18437,c_21534,c_22522,c_23959,c_31333,c_37465,c_47033,c_47725,c_47746,c_47812,c_48118,c_48221,c_48595,c_51097,c_52811,c_53758,c_56187,c_57941,c_63876,c_63871,c_63947,c_64013]) ).
tcf(c_64349,plain,
! [X0: $i] : multiply(sk_c11,X0) = multiply(sk_c1,X0),
inference(light_normalisation,[status(thm)],[c_64346,c_64032,c_64093,c_64202,c_64320]) ).
tcf(c_64359,plain,
( ~ iPr_def_12
| ( inverse(sk_c1) != sk_c10 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_64349,c_727]) ).
tcf(c_64380,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,multiply(X1,sk_c11))),multiply(multiply(X0,X1),X2)) = X2,
inference(light_normalisation,[status(thm)],[c_33918,c_64320]) ).
tcf(c_64381,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,multiply(X1,sk_c11))),multiply(X0,multiply(X1,X2))) = X2,
inference(demodulation,[status(thm)],[c_64380,c_115]) ).
tcf(c_64418,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,multiply(sk_c2,sk_c11))),multiply(X0,multiply(sk_c2,X1))) = multiply(sk_c11,X1),
inference(superposition,[status(thm)],[c_64326,c_64381]) ).
tcf(c_64429,plain,
! [X0: $i] : multiply(sk_c11,X0) = X0,
inference(demodulation,[status(thm)],[c_64418,c_64381]) ).
tcf(c_64529,plain,
multiply(sk_c11,sk_c10) != sk_c9,
inference(global_subsumption_just,[status(thm)],[c_64359,c_144,c_143,c_141,c_139,c_145,c_734,c_736,c_729,c_1051,c_1052,c_1054,c_1057,c_1112,c_1198,c_1200,c_1408,c_1418,c_1473,c_1665,c_1997,c_2401,c_3347,c_3529,c_3679,c_4521,c_4520,c_4832,c_4831,c_4837,c_4938,c_4939,c_5280,c_5367,c_5542,c_5735,c_11411,c_12758,c_13865,c_13951,c_18257,c_18437,c_18533,c_21534,c_22522,c_22585,c_23959,c_31333,c_33710,c_37465,c_37574,c_43684,c_47033,c_47725,c_47746,c_47812,c_48118,c_48221,c_48495,c_48496,c_48595,c_51097,c_52155,c_52811,c_53758,c_56187,c_56552,c_57941,c_63135,c_63876,c_63871,c_63947,c_64013,c_64359]) ).
tcf(c_64531,plain,
sk_c11 != sk_c9,
inference(light_normalisation,[status(thm)],[c_64529,c_37576,c_64320]) ).
tcf(c_64607,plain,
multiply(inverse(multiply(inverse(identity),sk_c9)),identity) = sk_c2,
inference(global_subsumption_just,[status(thm)],[c_34424,c_734,c_736,c_729,c_1051,c_1052,c_1054,c_1057,c_1198,c_1473,c_1665,c_1997,c_3347,c_3425,c_3529,c_4521,c_4831,c_4938,c_4939,c_5367,c_12758,c_13865,c_17372,c_18437,c_18854,c_21534,c_22522,c_23959,c_31333,c_37465,c_47033,c_47725,c_47746,c_47812,c_48118,c_48221,c_48595,c_51097,c_52811,c_53758,c_56187,c_57941,c_63876,c_63871,c_63947,c_64013]) ).
tcf(c_64609,plain,
multiply(inverse(multiply(sk_c1,sk_c9)),sk_c11) = sk_c2,
inference(light_normalisation,[status(thm)],[c_64607,c_64032,c_64202,c_64320]) ).
tcf(c_64610,plain,
multiply(inverse(multiply(sk_c11,sk_c9)),sk_c11) = sk_c2,
inference(demodulation,[status(thm)],[c_64609,c_64349]) ).
tcf(c_64611,plain,
multiply(sk_c1,sk_c11) = sk_c2,
inference(light_normalisation,[status(thm)],[c_64610,c_63871,c_64013,c_64032,c_64202]) ).
tcf(c_64612,plain,
multiply(sk_c11,sk_c11) = sk_c2,
inference(demodulation,[status(thm)],[c_64611,c_64349]) ).
tcf(c_64620,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c11,X0)) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_64612,c_115]) ).
tcf(c_64632,plain,
! [X0: $i] : multiply(sk_c2,X0) = X0,
inference(light_normalisation,[status(thm)],[c_64620,c_64429]) ).
tcf(c_64634,plain,
sk_c11 = sk_c9,
inference(demodulation,[status(thm)],[c_64058,c_64632]) ).
tcf(c_64637,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_64634,c_64531]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP373-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.09/0.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 14:36:23 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.41
% 0.09/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.41
% 0.09/0.41 % Detected problem language: tptp
% 0.09/0.42 % Proving...
% 39.94/7.33 % SZS status Started for theBenchmark.p
% 39.94/7.33 % SZS status Unsatisfiable for theBenchmark.p
% 39.94/7.33
% 39.94/7.33 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 39.94/7.33
% 39.94/7.33 % ------ iProver source info
% 39.94/7.33
% 39.94/7.33 % git: date: 2026-07-19 20:42:38 +0200
% 39.94/7.33 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 39.94/7.33 % git: non_committed_changes: false
% 39.94/7.33
% 39.94/7.33 % ------ Parsing...% successful
% 39.94/7.33
% 39.94/7.33
% 39.94/7.33 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 39.94/7.33
% 39.94/7.33 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 39.94/7.33
% 39.94/7.33 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 39.94/7.33
% 39.94/7.33 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 39.94/7.33 % ------ Proving...
% 39.94/7.33 % ------ Problem Properties
% 39.94/7.33
% 39.94/7.33 %
% 39.94/7.33 % clauses 68
% 39.94/7.33 % conjectures 65
% 39.94/7.33 % EPR 0
% 39.94/7.33 % Horn 7
% 39.94/7.33 % unary 3
% 39.94/7.33 % binary 60
% 39.94/7.33 % lits 143
% 39.94/7.33 % lits eq 135
% 39.94/7.33 % fd_pure 0
% 39.94/7.33 % fd_pseudo 0
% 39.94/7.33 % fd_cond 0
% 39.94/7.33 % fd_pseudo_cond 0
% 39.94/7.33 % AC symbols 0
% 39.94/7.33
% 39.94/7.33 % ------ Input Options Time Limit: Unbounded
% 39.94/7.33
% 39.94/7.33
% 39.94/7.33 % ------
% 39.94/7.33 % Current options:
% 39.94/7.33 % ------
% 39.94/7.33
% 39.94/7.33
% 39.94/7.33 %
% 39.94/7.33
% 39.94/7.33 % ------ Proving...
% 39.94/7.33 %
% 39.94/7.33
% 39.94/7.33 % SZS status Unsatisfiable for theBenchmark.p
% 39.94/7.33
% 39.94/7.33 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 39.94/7.34
% 39.94/7.34
%------------------------------------------------------------------------------