%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP217-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 : n014.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:31:50 PM UTC 2026
% Result : Unsatisfiable 26.05s 4.32s
% Output : CNFRefutation 26.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 40
% Syntax : Number of formulae : 440 ( 74 unt; 0 def)
% Number of atoms : 1075 (1028 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 1137 ( 502 ~; 635 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 304 ( 0 sgn 304 !; 0 ?; 254 :)
% 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_c6,sk_c7) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c11 = multiply(sk_c6,sk_c7)
| inverse(sk_c1) = sk_c11 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c6) = sk_c7
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c7 = inverse(sk_c6)
| inverse(sk_c1) = sk_c11 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| inverse(sk_c1) = sk_c11 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( multiply(sk_c11,sk_c9) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c10 = multiply(sk_c11,sk_c9)
| inverse(sk_c1) = sk_c11 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c9
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c9 = multiply(sk_c8,sk_c11)
| inverse(sk_c1) = sk_c11 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( inverse(sk_c8) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c11 = inverse(sk_c8)
| inverse(sk_c1) = sk_c11 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c11 = multiply(sk_c6,sk_c7)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c7 = inverse(sk_c6)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f19]) ).
fof(f23,negated_conjecture,
( multiply(sk_c11,sk_c9) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c10 = multiply(sk_c11,sk_c9)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c9 = multiply(sk_c8,sk_c11)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( inverse(sk_c8) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f28,plain,
( sk_c11 = inverse(sk_c8)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f27]) ).
fof(f31,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c2,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c7 = inverse(sk_c6)
| sk_c10 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f31]) ).
fof(f37,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c9
| multiply(sk_c2,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c9 = multiply(sk_c8,sk_c11)
| sk_c10 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( inverse(sk_c8) = sk_c11
| multiply(sk_c2,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c11 = inverse(sk_c8)
| sk_c10 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c11
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f42,plain,
( sk_c11 = multiply(sk_c6,sk_c7)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( inverse(sk_c6) = sk_c7
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f44,plain,
( sk_c7 = inverse(sk_c6)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f43]) ).
fof(f47,negated_conjecture,
( multiply(sk_c11,sk_c9) = sk_c10
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f48,plain,
( sk_c10 = multiply(sk_c11,sk_c9)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c9
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f50,plain,
( sk_c9 = multiply(sk_c8,sk_c11)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( inverse(sk_c8) = sk_c11
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c11 = inverse(sk_c8)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f51]) ).
fof(f65,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c11
| multiply(sk_c11,sk_c5) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c11 = multiply(sk_c6,sk_c7)
| sk_c10 = multiply(sk_c11,sk_c5) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c11,sk_c5) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f68,plain,
( sk_c7 = inverse(sk_c6)
| sk_c10 = multiply(sk_c11,sk_c5) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| multiply(sk_c11,sk_c5) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f70,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| sk_c10 = multiply(sk_c11,sk_c5) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c11,sk_c9) = sk_c10
| multiply(sk_c11,sk_c5) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f72,plain,
( sk_c10 = multiply(sk_c11,sk_c9)
| sk_c10 = multiply(sk_c11,sk_c5) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c9
| multiply(sk_c11,sk_c5) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f74,plain,
( sk_c9 = multiply(sk_c8,sk_c11)
| sk_c10 = multiply(sk_c11,sk_c5) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( inverse(sk_c8) = sk_c11
| multiply(sk_c11,sk_c5) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c11 = inverse(sk_c8)
| sk_c10 = multiply(sk_c11,sk_c5) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c11
| multiply(sk_c4,sk_c11) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
( sk_c11 = multiply(sk_c6,sk_c7)
| sk_c5 = multiply(sk_c4,sk_c11) ),
inference(reorient_equations,[],[f77]) ).
fof(f79,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c4,sk_c11) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_38) ).
fof(f80,plain,
( sk_c7 = inverse(sk_c6)
| sk_c5 = multiply(sk_c4,sk_c11) ),
inference(reorient_equations,[],[f79]) ).
fof(f87,negated_conjecture,
( inverse(sk_c8) = sk_c11
| multiply(sk_c4,sk_c11) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c11 = inverse(sk_c8)
| sk_c5 = multiply(sk_c4,sk_c11) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c11
| inverse(sk_c4) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f90,plain,
( sk_c11 = multiply(sk_c6,sk_c7)
| sk_c11 = inverse(sk_c4) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,negated_conjecture,
( inverse(sk_c6) = sk_c7
| inverse(sk_c4) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f92,plain,
( sk_c7 = inverse(sk_c6)
| sk_c11 = inverse(sk_c4) ),
inference(reorient_equations,[],[f91]) ).
fof(f93,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| inverse(sk_c4) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f94,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| sk_c11 = inverse(sk_c4) ),
inference(reorient_equations,[],[f93]) ).
fof(f99,negated_conjecture,
( inverse(sk_c8) = sk_c11
| inverse(sk_c4) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f100,plain,
( sk_c11 = inverse(sk_c8)
| sk_c11 = inverse(sk_c4) ),
inference(reorient_equations,[],[f99]) ).
fof(f101,negated_conjecture,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( inverse(X8) != sk_c11
| multiply(X8,sk_c11) != X7
| multiply(sk_c11,X7) != sk_c10
| multiply(X6,sk_c10) != sk_c11
| inverse(X5) != X6
| multiply(X5,X6) != sk_c11
| inverse(X4) != sk_c11
| multiply(X4,sk_c11) != X3
| multiply(sk_c11,X3) != sk_c10
| multiply(X2,sk_c11) != sk_c10
| inverse(X1) != X2
| multiply(X1,X2) != sk_c10
| multiply(X0,sk_c10) != sk_c11
| inverse(X0) != sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_49) ).
fof(f102,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( sk_c11 != inverse(X8)
| multiply(X8,sk_c11) != X7
| sk_c10 != multiply(sk_c11,X7)
| sk_c11 != multiply(X6,sk_c10)
| inverse(X5) != X6
| sk_c11 != multiply(X5,X6)
| sk_c11 != inverse(X4)
| multiply(X4,sk_c11) != X3
| sk_c10 != multiply(sk_c11,X3)
| sk_c10 != multiply(X2,sk_c11)
| inverse(X1) != X2
| multiply(X1,X2) != sk_c10
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11 ),
inference(reorient_equations,[],[f101]) ).
fof(f103,plain,
! [X3,X0,X1,X8,X6,X7,X4,X5] :
( sk_c11 != inverse(X8)
| multiply(X8,sk_c11) != X7
| sk_c10 != multiply(sk_c11,X7)
| sk_c11 != multiply(X6,sk_c10)
| inverse(X5) != X6
| sk_c11 != multiply(X5,X6)
| sk_c11 != inverse(X4)
| multiply(X4,sk_c11) != X3
| sk_c10 != multiply(sk_c11,X3)
| sk_c10 != multiply(inverse(X1),sk_c11)
| sk_c10 != multiply(X1,inverse(X1))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11 ),
inference(equality_resolution,[],[f102]) ).
fof(f104,plain,
! [X0,X1,X8,X6,X7,X4,X5] :
( sk_c11 != inverse(X8)
| multiply(X8,sk_c11) != X7
| sk_c10 != multiply(sk_c11,X7)
| sk_c11 != multiply(X6,sk_c10)
| inverse(X5) != X6
| sk_c11 != multiply(X5,X6)
| sk_c11 != inverse(X4)
| sk_c10 != multiply(sk_c11,multiply(X4,sk_c11))
| sk_c10 != multiply(inverse(X1),sk_c11)
| sk_c10 != multiply(X1,inverse(X1))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11 ),
inference(equality_resolution,[],[f103]) ).
fof(f105,plain,
! [X0,X1,X8,X7,X4,X5] :
( sk_c11 != inverse(X8)
| multiply(X8,sk_c11) != X7
| sk_c10 != multiply(sk_c11,X7)
| sk_c11 != multiply(inverse(X5),sk_c10)
| sk_c11 != multiply(X5,inverse(X5))
| sk_c11 != inverse(X4)
| sk_c10 != multiply(sk_c11,multiply(X4,sk_c11))
| sk_c10 != multiply(inverse(X1),sk_c11)
| sk_c10 != multiply(X1,inverse(X1))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11 ),
inference(equality_resolution,[],[f104]) ).
fof(f106,plain,
! [X0,X1,X8,X4,X5] :
( sk_c11 != inverse(X8)
| sk_c10 != multiply(sk_c11,multiply(X8,sk_c11))
| sk_c11 != multiply(inverse(X5),sk_c10)
| sk_c11 != multiply(X5,inverse(X5))
| sk_c11 != inverse(X4)
| sk_c10 != multiply(sk_c11,multiply(X4,sk_c11))
| sk_c10 != multiply(inverse(X1),sk_c11)
| sk_c10 != multiply(X1,inverse(X1))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11 ),
inference(equality_resolution,[],[f105]) ).
tcf(c_101,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_102,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_104,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c6,sk_c7) = sk_c11 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_105,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c8) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_110,negated_conjecture,
( ( multiply(sk_c6,sk_c7) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_113,negated_conjecture,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_114,negated_conjecture,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c2,sk_c3) = sk_c10 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c2,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c6,sk_c7) = sk_c11 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_134,negated_conjecture,
( ( multiply(sk_c6,sk_c7) = sk_c11 )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_135,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c7,sk_c10) = sk_c11 )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_137,negated_conjecture,
( ( multiply(sk_c11,sk_c5) = sk_c10 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_138,negated_conjecture,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_140,negated_conjecture,
( ( multiply(sk_c4,sk_c11) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c11 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c11) = sk_c5 ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_145,negated_conjecture,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c4,sk_c11) = sk_c5 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c6,sk_c7) = sk_c11 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_148,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( inverse(sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_152,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(X3) != sk_c11 )
| ( inverse(X2) != sk_c11 )
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 )
| ( multiply(inverse(X4),sk_c11) != sk_c10 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X4,inverse(X4)) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(sk_c11,multiply(X3,sk_c11)) != sk_c10 )
| ( multiply(sk_c11,multiply(X2,sk_c11)) != sk_c10 ) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_153,plain,
multiply(identity,sk_c11) = sk_c11,
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_154,plain,
multiply(inverse(sk_c11),sk_c11) = identity,
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_379,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( multiply(inverse(X0),sk_c11) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_152]) ).
tcf(c_380,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_152]) ).
tcf(c_381,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_152]) ).
tcf(c_382,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c11 )
| ( multiply(sk_c11,multiply(X0,sk_c11)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_152]) ).
tcf(c_383,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_152]) ).
tcf(c_384,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_385,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_386,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_387,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_390,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_643,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c11) = sk_c10 )
| ( sk_c10 != X1 )
| ( multiply(inverse(X0),sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_644,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c10 )
| ( sk_c10 != sk_c11 )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_643]) ).
tcf(c_646,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_385]) ).
tcf(c_665,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_670,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_675,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_385]) ).
tcf(c_676,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_646]) ).
tcf(c_683,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_684,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_687,plain,
! [X0: $i] :
( ( inverse(sk_c8) = X0 )
| ( X0 != sk_c11 )
| ( inverse(sk_c8) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_693,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = X0 )
| ( X0 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_675]) ).
tcf(c_696,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_675]) ).
tcf(c_697,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = inverse(X0) )
| ( sk_c11 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_700,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c10) )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_702,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_714,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c8) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_717,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_722,plain,
( ( sk_c11 = inverse(sk_c8) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c8) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_728,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_730,plain,
multiply(inverse(sk_c10),sk_c10) = identity,
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_735,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c10) )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_700]) ).
tcf(c_753,plain,
( ( sk_c11 = multiply(sk_c6,sk_c7) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c6,sk_c7) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_702]) ).
tcf(c_757,plain,
! [X0: $i] :
( ( sk_c11 = multiply(identity,X0) )
| ( sk_c11 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_702]) ).
tcf(c_758,plain,
( ( sk_c11 = multiply(identity,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_757]) ).
tcf(c_764,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_765,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_702]) ).
tcf(c_768,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_387]) ).
tcf(c_804,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(sk_c10),sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_806,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c10),sk_c10) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_807,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(sk_c11),sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != identity )
| ( multiply(inverse(sk_c11),sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_806]) ).
tcf(c_809,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_822,plain,
! [X0: $i] :
( ( sk_c11 = sk_c10 )
| ( sk_c10 != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_842,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(inverse(X0),sk_c10) )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_851,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = X1 )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_764]) ).
tcf(c_852,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),X0) = X1 )
| ( X1 != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_764]) ).
tcf(c_859,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X0,X1) = X4 )
| ( X4 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_764]) ).
tcf(c_872,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(identity,X1) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_676]) ).
tcf(c_873,plain,
( ( multiply(inverse(sk_c11),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_872]) ).
tcf(c_896,plain,
( ( sk_c10 = multiply(sk_c11,sk_c9) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_898,plain,
( ( sk_c10 = multiply(identity,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_902,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_903,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X1,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_768]) ).
tcf(c_918,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_765]) ).
tcf(c_925,plain,
( ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 )
| ( multiply(sk_c1,sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_380]) ).
tcf(c_998,plain,
( ( sk_c10 = multiply(sk_c11,sk_c5) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c11,sk_c5) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_999,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c5) = X0 )
| ( X0 != sk_c10 )
| ( multiply(sk_c11,sk_c5) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_764]) ).
tcf(c_1071,plain,
multiply(identity,identity) = identity,
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_1075,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != multiply(sk_c11,sk_c9) )
| ( X0 != multiply(sk_c11,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_1078,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != multiply(sk_c11,sk_c9) )
| ( sk_c11 != multiply(sk_c11,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_1117,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( X0 != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_1245,plain,
! [X0: $i] :
( ( sk_c11 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_735]) ).
tcf(c_1246,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = X1 )
| ( X1 != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_1248,plain,
( ( sk_c11 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(inverse(sk_c11),sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(sk_c11),sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1245]) ).
tcf(c_1271,plain,
! [X0: $i] :
( ( inverse(sk_c8) = identity )
| ( identity != X0 )
| ( inverse(sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_714]) ).
tcf(c_1273,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c8) = multiply(inverse(X0),sk_c10) )
| ( inverse(sk_c8) != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_714]) ).
tcf(c_1418,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(inverse(X1),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_903]) ).
tcf(c_1434,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_902]) ).
tcf(c_1435,plain,
( ( identity = sk_c11 )
| ( identity != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_1434]) ).
tcf(c_1439,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(sk_c11,sk_c9) )
| ( sk_c11 != multiply(sk_c11,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_822]) ).
tcf(c_1443,plain,
multiply(identity,sk_c10) = sk_c10,
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_1457,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c10),sk_c10) )
| ( X0 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_842]) ).
tcf(c_1469,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = inverse(X1) )
| ( inverse(X1) != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_851]) ).
tcf(c_1477,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(identity,X0) )
| ( sk_c11 != X1 )
| ( multiply(identity,X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_702]) ).
tcf(c_1501,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),X0) = multiply(identity,X1) )
| ( multiply(identity,X1) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_852]) ).
tcf(c_1515,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(identity,X0) )
| ( sk_c11 != multiply(identity,X1) )
| ( multiply(identity,X0) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_918]) ).
tcf(c_1520,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = multiply(identity,X2) )
| ( X1 != X2 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_387]) ).
tcf(c_1566,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(X0,X1) )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_1577,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = sk_c11 )
| ( sk_c11 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_859]) ).
tcf(c_1611,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(sk_c6,sk_c7) )
| ( multiply(X0,X1) != multiply(sk_c6,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_765]) ).
tcf(c_1616,plain,
( ( multiply(inverse(sk_c6),sk_c10) = multiply(sk_c7,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c6) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_903]) ).
tcf(c_2022,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(X0,X1) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1117]) ).
tcf(c_2023,plain,
( ( sk_c10 = multiply(sk_c11,sk_c11) )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(sk_c11,sk_c11) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2022]) ).
tcf(c_2036,plain,
( ( sk_c11 = multiply(identity,identity) )
| ( sk_c11 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_757]) ).
tcf(c_2228,plain,
( ( identity = multiply(inverse(sk_c10),sk_c10) )
| ( identity != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_1457]) ).
tcf(c_2516,plain,
( ( inverse(sk_c6) = sk_c7 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_380,c_111]) ).
tcf(c_2517,plain,
( ( inverse(sk_c8) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_380,c_115]) ).
tcf(c_2526,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c6,sk_c7) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c6,sk_c7) != X0 ) ),
inference(instantiation,[status(thm)],[c_764]) ).
tcf(c_2557,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c6,multiply(sk_c7,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_104,c_103]) ).
tcf(c_2560,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c7,multiply(sk_c10,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_106,c_103]) ).
tcf(c_2580,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(X0,X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_101,c_103]) ).
tcf(c_2581,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_102,c_103]) ).
tcf(c_2617,plain,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( multiply(inverse(sk_c1),sk_c11) = multiply(identity,sk_c10) ) ),
inference(superposition,[status(thm)],[c_114,c_2581]) ).
tcf(c_2618,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( multiply(inverse(sk_c1),sk_c11) = multiply(identity,sk_c10) ) ),
inference(superposition,[status(thm)],[c_113,c_2581]) ).
tcf(c_2621,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(inverse(sk_c1),sk_c11) = multiply(identity,sk_c10) ) ),
inference(superposition,[status(thm)],[c_115,c_2581]) ).
tcf(c_2622,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(inverse(sk_c1),sk_c11) = multiply(identity,sk_c10) ) ),
inference(superposition,[status(thm)],[c_111,c_2581]) ).
tcf(c_2631,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(inverse(sk_c4),sk_c5) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_145,c_2581]) ).
tcf(c_2632,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(inverse(sk_c4),sk_c5) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_141,c_2581]) ).
tcf(c_2633,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_101,c_2581]) ).
tcf(c_2634,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_102,c_2581]) ).
tcf(c_2753,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c10) )
| ( sk_c11 != multiply(inverse(X1),sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(X1),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_735]) ).
tcf(c_2787,plain,
! [X0: $i] :
( ( multiply(sk_c6,sk_c7) = X0 )
| ( multiply(sk_c11,sk_c5) = sk_c10 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_385,c_134]) ).
tcf(c_2798,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c9) = X0 )
| ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_385,c_113]) ).
tcf(c_2803,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c8,sk_c11) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_385,c_108]) ).
tcf(c_2804,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c8,sk_c11) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_385,c_126]) ).
tcf(c_2864,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X1) = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_385,c_101]) ).
tcf(c_2865,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_385,c_102]) ).
tcf(c_2866,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c11 )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_2865]) ).
tcf(c_2869,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_385,c_384]) ).
tcf(c_2907,plain,
! [X0: $i] :
( ( sk_c11 = multiply(identity,identity) )
| ( sk_c11 != X0 )
| ( multiply(identity,identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_1477]) ).
tcf(c_2946,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(X0),sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1246]) ).
tcf(c_2947,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(sk_c11),sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2946]) ).
tcf(c_2964,plain,
! [X0: $i,X1: $i] :
( ( multiply(multiply(identity,identity),X0) = multiply(identity,X1) )
| ( X0 != X1 )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_1520]) ).
tcf(c_2965,plain,
( ( multiply(multiply(identity,identity),sk_c11) = multiply(identity,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_2964]) ).
tcf(c_2983,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = multiply(identity,X1) )
| ( multiply(identity,X1) != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_851]) ).
tcf(c_3015,plain,
! [X0: $i] :
( ( sk_c11 = multiply(identity,X0) )
| ( sk_c11 != multiply(sk_c6,sk_c7) )
| ( multiply(identity,X0) != multiply(sk_c6,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_1611]) ).
tcf(c_3111,plain,
! [X0: $i] :
( ( multiply(inverse(X0),X0) = multiply(identity,identity) )
| ( multiply(identity,identity) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_1501]) ).
tcf(c_3112,plain,
( ( multiply(inverse(sk_c11),sk_c11) = multiply(identity,identity) )
| ( multiply(identity,identity) != identity )
| ( multiply(inverse(sk_c11),sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_3111]) ).
tcf(c_3200,plain,
! [X0: $i] :
( ( multiply(identity,X0) = inverse(sk_c8) )
| ( inverse(sk_c8) != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_1469]) ).
tcf(c_3215,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c8) = multiply(X0,X1) )
| ( inverse(sk_c8) != sk_c11 )
| ( multiply(X0,X1) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_687]) ).
tcf(c_3715,plain,
( ( multiply(sk_c6,sk_c7) = sk_c11 )
| ( multiply(inverse(sk_c4),sk_c5) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_140,c_2581]) ).
tcf(c_3762,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(sk_c8) = multiply(inverse(X0),sk_c10) )
| ( inverse(sk_c8) != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_1273]) ).
tcf(c_3874,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,multiply(sk_c10,X0)) = multiply(sk_c6,multiply(sk_c11,X0)) ) ),
inference(superposition,[status(thm)],[c_2560,c_2557]) ).
tcf(c_3934,plain,
! [X0: $i] :
( ( X0 = multiply(identity,identity) )
| ( X0 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_1566]) ).
tcf(c_3977,plain,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_114,c_380]) ).
tcf(c_3981,plain,
( ( inverse(sk_c8) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_115,c_380]) ).
tcf(c_3982,plain,
( ( inverse(sk_c6) = sk_c7 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_111,c_380]) ).
tcf(c_3983,plain,
( ~ iPr_def_11
| ( sk_c11 != sk_c10 )
| ( inverse(identity) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_101,c_380]) ).
tcf(c_4016,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_4236,plain,
( ( multiply(sk_c11,sk_c5) = sk_c10 )
| ~ iPr_def_13
| ( inverse(sk_c8) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_138,c_382]) ).
tcf(c_4239,plain,
( ( inverse(sk_c2) = sk_c3 )
| ~ iPr_def_13
| ( inverse(sk_c8) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_126,c_382]) ).
tcf(c_4240,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_13
| ( inverse(sk_c8) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_108,c_382]) ).
tcf(c_4249,plain,
( ( inverse(sk_c8) = sk_c11 )
| ~ iPr_def_13
| ( inverse(sk_c4) != sk_c11 )
| ( multiply(sk_c11,sk_c5) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_145,c_382]) ).
tcf(c_4250,plain,
( ( inverse(sk_c6) = sk_c7 )
| ~ iPr_def_13
| ( inverse(sk_c4) != sk_c11 )
| ( multiply(sk_c11,sk_c5) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_141,c_382]) ).
tcf(c_4345,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c6),sk_c10) = X0 )
| ( X0 != multiply(sk_c7,sk_c10) )
| ( multiply(inverse(sk_c6),sk_c10) != multiply(sk_c7,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_4346,plain,
( ( multiply(inverse(sk_c6),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(sk_c7,sk_c10) )
| ( multiply(inverse(sk_c6),sk_c10) != multiply(sk_c7,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_4345]) ).
tcf(c_4617,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(sk_c11,sk_c5) )
| ( sk_c11 != multiply(sk_c11,sk_c5) ) ),
inference(instantiation,[status(thm)],[c_822]) ).
tcf(c_4987,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_102,c_103]) ).
tcf(c_5103,plain,
! [X0: $i] :
( ( sk_c11 = multiply(identity,identity) )
| ( sk_c11 != multiply(identity,X0) )
| ( multiply(identity,identity) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_1515]) ).
tcf(c_5104,plain,
( ( sk_c11 = multiply(identity,identity) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(identity,identity) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_5103]) ).
tcf(c_5208,plain,
( ( sk_c11 = multiply(sk_c6,sk_c7) )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2869,c_104]) ).
tcf(c_5211,plain,
( ( sk_c11 = multiply(sk_c6,sk_c7) )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2869,c_110]) ).
tcf(c_5212,plain,
( ( sk_c11 = multiply(sk_c6,sk_c7) )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2869,c_134]) ).
tcf(c_5218,plain,
( ( sk_c11 = multiply(sk_c7,sk_c10) )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2869,c_136]) ).
tcf(c_5219,plain,
( ( sk_c10 = multiply(sk_c11,sk_c9) )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2869,c_107]) ).
tcf(c_5222,plain,
( ( sk_c10 = multiply(sk_c11,sk_c9) )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2869,c_113]) ).
tcf(c_5245,plain,
( ( sk_c10 = multiply(sk_c11,sk_c5) )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(resolution,[status(thm)],[c_2869,c_135]) ).
tcf(c_5258,plain,
! [X0: $i] : identity = multiply(inverse(X0),X0),
inference(resolution,[status(thm)],[c_2869,c_102]) ).
tcf(c_5395,plain,
( ( sk_c11 = identity )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_5397,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( X0 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_902]) ).
tcf(c_5761,plain,
! [X0: $i] :
( ( multiply(sk_c6,sk_c7) = sk_c10 )
| ( sk_c10 != X0 )
| ( multiply(sk_c6,sk_c7) != X0 ) ),
inference(instantiation,[status(thm)],[c_2526]) ).
tcf(c_6213,plain,
( ( inverse(sk_c8) = sk_c11 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_3981,c_109,c_2517]) ).
tcf(c_6215,plain,
( ( inverse(sk_c6) = sk_c7 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_3982,c_105,c_2516]) ).
tcf(c_7604,plain,
! [X0: $i] :
( ( multiply(identity,identity) = X0 )
| ( X0 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_851]) ).
tcf(c_7642,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(X0) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1418]) ).
tcf(c_7643,plain,
( ( multiply(inverse(sk_c11),sk_c10) = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c11) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_7642]) ).
tcf(c_7981,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(identity,X1) = X2 )
| ( X2 != X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2864,c_385]) ).
tcf(c_8268,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c11,sk_c11) = multiply(identity,sk_c10) ) ),
inference(superposition,[status(thm)],[c_109,c_2621]) ).
tcf(c_8483,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c11,sk_c11) = multiply(identity,sk_c10) ) ),
inference(superposition,[status(thm)],[c_105,c_2622]) ).
tcf(c_8588,plain,
( ( identity = multiply(identity,identity) )
| ( identity != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_3934]) ).
tcf(c_8647,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(multiply(identity,identity),X0) )
| ( sk_c11 != multiply(identity,X1) )
| ( multiply(multiply(identity,identity),X0) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_918]) ).
tcf(c_8648,plain,
( ( sk_c11 = multiply(multiply(identity,identity),sk_c11) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(multiply(identity,identity),sk_c11) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_8647]) ).
tcf(c_8690,plain,
! [X0: $i] :
( ( multiply(identity,identity) = multiply(identity,X0) )
| ( multiply(identity,identity) != identity )
| ( multiply(identity,X0) != identity ) ),
inference(instantiation,[status(thm)],[c_2983]) ).
tcf(c_8691,plain,
( ( multiply(identity,identity) = multiply(identity,sk_c11) )
| ( multiply(identity,identity) != identity )
| ( multiply(identity,sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_8690]) ).
tcf(c_8887,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c11,sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_8268,c_101]) ).
tcf(c_9369,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X2),X2) = X0 )
| ( X1 != identity )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2865,c_385]) ).
tcf(c_9425,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c11,sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_8483,c_101]) ).
tcf(c_9723,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(inverse(sk_c11),sk_c10) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_8887,c_4987]) ).
tcf(c_9770,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(inverse(sk_c11),sk_c10) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_9425,c_4987]) ).
tcf(c_9801,plain,
! [X0: $i] :
( ( multiply(inverse(X0),X0) = sk_c11 )
| ( sk_c11 != multiply(identity,identity) )
| ( multiply(inverse(X0),X0) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_1577]) ).
tcf(c_9804,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c11 )
| ( sk_c11 != multiply(identity,identity) )
| ( multiply(inverse(sk_c11),sk_c11) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_9801]) ).
tcf(c_9956,plain,
( ( multiply(identity,identity) = inverse(sk_c8) )
| ( inverse(sk_c8) != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_3200]) ).
tcf(c_10281,plain,
! [X0: $i] :
( ( inverse(sk_c8) = multiply(identity,X0) )
| ( inverse(sk_c8) != sk_c11 )
| ( multiply(identity,X0) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3215]) ).
tcf(c_10282,plain,
( ( inverse(sk_c8) = multiply(identity,sk_c11) )
| ( inverse(sk_c8) != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_10281]) ).
tcf(c_10849,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c11,sk_c5) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_147,c_2632]) ).
tcf(c_11075,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c11,sk_c5) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_10849,c_101]) ).
tcf(c_11486,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_102,c_103]) ).
tcf(c_11665,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),multiply(identity,X1)) = multiply(multiply(identity,X0),X1),
inference(superposition,[status(thm)],[c_2634,c_103]) ).
tcf(c_11765,plain,
! [X0: $i] : multiply(inverse(inverse(identity)),X0) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_2633,c_11486]) ).
tcf(c_11793,plain,
multiply(identity,inverse(identity)) = identity,
inference(superposition,[status(thm)],[c_11765,c_102]) ).
tcf(c_11822,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_11793,c_101]) ).
tcf(c_11835,plain,
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( sk_c11 != sk_c10 ) ),
inference(superposition,[status(thm)],[c_11822,c_3983]) ).
tcf(c_13452,plain,
! [X0: $i] :
( ( sk_c11 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(inverse(X0),sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2753]) ).
tcf(c_13453,plain,
( ( sk_c11 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(inverse(sk_c11),sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(sk_c11),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_13452]) ).
tcf(c_13575,plain,
( ( sk_c11 = multiply(sk_c6,sk_c7) )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_5211,c_380]) ).
tcf(c_13607,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(X0,X1) )
| ( sk_c11 != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_822]) ).
tcf(c_13610,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(sk_c11,sk_c11) )
| ( sk_c11 != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_13607]) ).
tcf(c_13620,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != multiply(X1,X2) )
| ( X0 != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_13623,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != multiply(sk_c11,sk_c11) )
| ( sk_c11 != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_13620]) ).
tcf(c_13662,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(multiply(identity,X0),X1),
inference(superposition,[status(thm)],[c_101,c_11665]) ).
tcf(c_13855,plain,
! [X0: $i] :
( ( sk_c11 = multiply(sk_c6,sk_c7) )
| ( multiply(sk_c11,sk_c5) = X0 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_5212,c_385]) ).
tcf(c_14101,plain,
( ( sk_c10 = multiply(sk_c11,sk_c9) )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_5222,c_380]) ).
tcf(c_14455,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c10) )
| ( sk_c11 != multiply(identity,X1) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_735]) ).
tcf(c_14457,plain,
( ( sk_c11 = multiply(inverse(sk_c11),sk_c10) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_14455]) ).
tcf(c_17844,plain,
! [X0: $i] : multiply(multiply(identity,X0),inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_13662,c_102]) ).
tcf(c_18443,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c8,sk_c11) )
| ( inverse(sk_c1) = sk_c11 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_2803,c_2869]) ).
tcf(c_18453,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c8,sk_c11) )
| ( inverse(sk_c2) = sk_c3 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_2804,c_2869]) ).
tcf(c_18855,plain,
( ( sk_c11 = multiply(sk_c6,sk_c7) )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_13575,c_5208,c_13575]) ).
tcf(c_18867,plain,
( ( sk_c10 = multiply(sk_c11,sk_c9) )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_14101,c_5219,c_14101]) ).
tcf(c_20409,plain,
( ( sk_c11 = identity )
| ( identity != multiply(identity,identity) )
| ( sk_c11 != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_20412,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != multiply(identity,identity) )
| ( X0 != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_902]) ).
tcf(c_20413,plain,
( ( identity = sk_c11 )
| ( identity != multiply(identity,identity) )
| ( sk_c11 != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_20412]) ).
tcf(c_20420,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c11,sk_c5) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_151,c_2631]) ).
tcf(c_20434,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c6,sk_c7) )
| ( multiply(sk_c11,sk_c5) = sk_c10 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_2787,c_2869]) ).
tcf(c_20637,plain,
! [X0: $i] :
( ( identity = multiply(inverse(X0),sk_c10) )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_5397]) ).
tcf(c_20638,plain,
( ( identity = multiply(inverse(sk_c11),sk_c10) )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_20637]) ).
tcf(c_20774,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c11,sk_c5) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_20420,c_101]) ).
tcf(c_21184,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_101,c_17844]) ).
tcf(c_21854,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c10) )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_21855,plain,
( ( inverse(sk_c11) = inverse(sk_c10) )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_21854]) ).
tcf(c_23054,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c2,sk_c3) = identity ) ),
inference(superposition,[status(thm)],[c_127,c_21184]) ).
tcf(c_23055,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c3) = identity ) ),
inference(superposition,[status(thm)],[c_123,c_21184]) ).
tcf(c_23057,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_147,c_21184]) ).
tcf(c_23073,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( multiply(inverse(X0),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_21184,c_381]) ).
tcf(c_23074,plain,
! [X0: $i] :
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( multiply(inverse(X0),sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_21184,c_379]) ).
tcf(c_23104,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_23074]) ).
tcf(c_23105,plain,
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c11),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_23073]) ).
tcf(c_23512,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(multiply(identity,identity),X2) )
| ( multiply(X0,X1) != multiply(multiply(identity,identity),X2) ) ),
inference(instantiation,[status(thm)],[c_765]) ).
tcf(c_23513,plain,
( ( sk_c11 = multiply(sk_c11,sk_c11) )
| ( sk_c11 != multiply(multiply(identity,identity),sk_c11) )
| ( multiply(sk_c11,sk_c11) != multiply(multiply(identity,identity),sk_c11) ) ),
inference(instantiation,[status(thm)],[c_23512]) ).
tcf(c_26395,plain,
( ( sk_c11 = sk_c10 )
| ( inverse(sk_c8) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_20774,c_139]) ).
tcf(c_29813,plain,
! [X0: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c11) )
| ( sk_c11 != sk_c10 )
| ( multiply(inverse(X0),sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_702]) ).
tcf(c_29814,plain,
( ( sk_c11 = multiply(inverse(sk_c11),sk_c11) )
| ( sk_c11 != sk_c10 )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_29813]) ).
tcf(c_31871,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ~ iPr_def_11
| ( X0 != multiply(sk_c6,sk_c7) ) ),
inference(resolution,[status(thm)],[c_18855,c_385]) ).
tcf(c_32465,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c8) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_23054,c_121]) ).
tcf(c_32475,plain,
inverse(sk_c8) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_32465,c_153,c_151,c_139,c_390,c_383,c_644,c_684,c_717,c_730,c_758,c_804,c_873,c_2228,c_2866,c_2947,c_4016,c_4249,c_5395,c_6213,c_7643,c_9723,c_13453,c_14457,c_21855,c_23104,c_23105,c_26395,c_32465]) ).
tcf(c_32513,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_23055,c_117]) ).
tcf(c_32899,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c10 )
| ( sk_c10 != identity )
| ( multiply(inverse(sk_c11),sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_643]) ).
tcf(c_34804,plain,
( ( sk_c11 = multiply(sk_c11,sk_c9) )
| ( multiply(sk_c1,sk_c10) = sk_c11 )
| ~ iPr_def_11
| ( multiply(sk_c6,sk_c7) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_31871,c_2798]) ).
tcf(c_34838,plain,
! [X0: $i] :
( ( sk_c11 = multiply(inverse(X0),X0) )
| ~ iPr_def_11
| ( multiply(sk_c6,sk_c7) != identity ) ),
inference(resolution,[status(thm)],[c_31871,c_2865]) ).
tcf(c_36103,plain,
( ( sk_c11 = multiply(sk_c11,sk_c5) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c11,sk_c5) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_702]) ).
tcf(c_36311,plain,
inverse(sk_c6) = sk_c7,
inference(global_subsumption_just,[status(thm)],[c_23057,c_153,c_154,c_147,c_135,c_390,c_383,c_730,c_758,c_807,c_873,c_1248,c_2228,c_4016,c_4250,c_4617,c_5245,c_5395,c_6215,c_9770,c_11075,c_23104,c_23105,c_29814,c_32513,c_32899,c_36103]) ).
tcf(c_36317,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm)],[c_36311,c_21184]) ).
tcf(c_36325,plain,
( ~ iPr_def_12
| ( multiply(sk_c6,sk_c7) != sk_c11 )
| ( multiply(inverse(sk_c6),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_36311,c_381]) ).
tcf(c_36924,negated_conjecture,
inverse(sk_c6) = sk_c7,
inference(global_subsumption_just,[status(thm)],[c_105,c_153,c_154,c_147,c_135,c_390,c_383,c_730,c_758,c_807,c_873,c_1248,c_2228,c_4016,c_4250,c_4617,c_5245,c_5395,c_6215,c_9770,c_11075,c_23104,c_23105,c_29814,c_32513,c_32899,c_36103]) ).
tcf(c_36926,negated_conjecture,
inverse(sk_c8) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_109,c_153,c_151,c_139,c_390,c_383,c_644,c_684,c_717,c_730,c_758,c_804,c_873,c_2228,c_2866,c_2947,c_4016,c_4249,c_5395,c_6213,c_7643,c_9723,c_13453,c_14457,c_21855,c_23104,c_23105,c_26395,c_32465]) ).
tcf(c_36929,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm)],[c_36926,c_102]) ).
tcf(c_36930,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,multiply(sk_c10,sk_c9)) = multiply(sk_c6,sk_c10) ) ),
inference(superposition,[status(thm)],[c_107,c_3874]) ).
tcf(c_36970,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_102,c_103]) ).
tcf(c_36991,plain,
( ~ iPr_def_11
| ( sk_c11 != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_3983,c_102,c_730,c_806,c_1245,c_2228,c_4016,c_5395,c_11835,c_34838,c_36317]) ).
tcf(c_37072,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c8,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_36929,c_103]) ).
tcf(c_37076,plain,
! [X0: $i,X1: $i] : multiply(inverse(identity),multiply(X0,X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_2633,c_103]) ).
tcf(c_37086,plain,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(identity,sk_c11) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_148,c_2580]) ).
tcf(c_37145,plain,
( ( multiply(sk_c11,sk_c5) = sk_c10 )
| ( multiply(sk_c11,sk_c9) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_138,c_37072]) ).
tcf(c_37148,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c11,sk_c9) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_126,c_37072]) ).
tcf(c_37149,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_108,c_37072]) ).
tcf(c_37152,plain,
( ~ iPr_def_13
| ( inverse(sk_c8) != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_37072,c_382]) ).
tcf(c_37158,plain,
multiply(identity,sk_c11) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_37086,c_153]) ).
tcf(c_37173,plain,
multiply(inverse(sk_c7),identity) = multiply(identity,sk_c6),
inference(superposition,[status(thm)],[c_36924,c_2634]) ).
tcf(c_37174,plain,
multiply(inverse(sk_c11),identity) = multiply(identity,sk_c8),
inference(superposition,[status(thm)],[c_36926,c_2634]) ).
tcf(c_37178,plain,
! [X0: $i] : multiply(inverse(sk_c7),multiply(identity,X0)) = multiply(multiply(identity,sk_c6),X0),
inference(superposition,[status(thm)],[c_37173,c_103]) ).
tcf(c_37266,plain,
multiply(inverse(inverse(sk_c11)),multiply(identity,sk_c8)) = multiply(identity,identity),
inference(superposition,[status(thm)],[c_37174,c_36970]) ).
tcf(c_37375,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c11,sk_c9) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_37148,c_101]) ).
tcf(c_37475,plain,
multiply(inverse(identity),multiply(identity,identity)) = multiply(identity,identity),
inference(superposition,[status(thm)],[c_37266,c_37076]) ).
tcf(c_37491,plain,
multiply(inverse(inverse(identity)),multiply(identity,identity)) = multiply(identity,multiply(identity,identity)),
inference(superposition,[status(thm)],[c_37475,c_36970]) ).
tcf(c_37503,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_37149,c_101]) ).
tcf(c_37576,plain,
( ( sk_c11 = sk_c10 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_37375,c_125]) ).
tcf(c_37597,plain,
! [X0: $i] : multiply(multiply(identity,sk_c6),X0) = multiply(inverse(sk_c7),X0),
inference(superposition,[status(thm)],[c_101,c_37178]) ).
tcf(c_37630,plain,
! [X0: $i] : multiply(inverse(sk_c7),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_101,c_37597]) ).
tcf(c_37693,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm)],[c_37630,c_102]) ).
tcf(c_37713,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_37693,c_134]) ).
tcf(c_37715,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_37693,c_146]) ).
tcf(c_37716,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_37693,c_122]) ).
tcf(c_37717,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_37693,c_104]) ).
tcf(c_37916,plain,
multiply(inverse(inverse(identity)),identity) = identity,
inference(superposition,[status(thm)],[c_101,c_37491]) ).
tcf(c_37927,plain,
! [X0: $i] : multiply(inverse(inverse(identity)),multiply(identity,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_37916,c_103]) ).
tcf(c_37930,plain,
! [X0: $i] : multiply(inverse(inverse(identity)),X0) = X0,
inference(superposition,[status(thm)],[c_101,c_37927]) ).
tcf(c_37996,plain,
! [X0: $i] : multiply(inverse(inverse(inverse(identity))),X0) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_37930,c_36970]) ).
tcf(c_38132,plain,
( ( multiply(sk_c11,sk_c5) = sk_c10 )
| ( multiply(sk_c11,sk_c9) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_37145,c_101]) ).
tcf(c_38183,plain,
multiply(identity,inverse(inverse(identity))) = identity,
inference(superposition,[status(thm)],[c_37996,c_102]) ).
tcf(c_38203,plain,
inverse(inverse(identity)) = identity,
inference(superposition,[status(thm)],[c_38183,c_101]) ).
tcf(c_38208,plain,
multiply(identity,inverse(identity)) = identity,
inference(superposition,[status(thm)],[c_38203,c_102]) ).
tcf(c_38372,plain,
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( multiply(inverse(identity),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_38208,c_381]) ).
tcf(c_38373,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( multiply(inverse(identity),sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_38208,c_379]) ).
tcf(c_38409,plain,
( ( sk_c11 = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_37503,c_107]) ).
tcf(c_41862,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = multiply(multiply(identity,identity),X2) )
| ( X1 != X2 )
| ( X0 != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_387]) ).
tcf(c_41863,plain,
( ( multiply(sk_c11,sk_c11) = multiply(multiply(identity,identity),sk_c11) )
| ( sk_c11 != sk_c11 )
| ( sk_c11 != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_41862]) ).
tcf(c_42466,plain,
! [X0: $i] :
( ( inverse(sk_c8) = identity )
| ( identity != multiply(inverse(X0),sk_c10) )
| ( inverse(sk_c8) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1271]) ).
tcf(c_42467,plain,
( ( inverse(sk_c8) = identity )
| ( identity != multiply(inverse(sk_c11),sk_c10) )
| ( inverse(sk_c8) != multiply(inverse(sk_c11),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_42466]) ).
tcf(c_43319,plain,
( ( sk_c11 = multiply(identity,identity) )
| ( sk_c11 != inverse(sk_c8) )
| ( multiply(identity,identity) != inverse(sk_c8) ) ),
inference(instantiation,[status(thm)],[c_2907]) ).
tcf(c_44507,plain,
( ( multiply(identity,identity) = multiply(sk_c6,sk_c7) )
| ( multiply(identity,identity) != identity )
| ( multiply(sk_c6,sk_c7) != identity ) ),
inference(instantiation,[status(thm)],[c_7604]) ).
tcf(c_44513,plain,
( ( multiply(sk_c6,sk_c7) = sk_c10 )
| ( sk_c10 != identity )
| ( multiply(sk_c6,sk_c7) != identity ) ),
inference(instantiation,[status(thm)],[c_5761]) ).
tcf(c_45789,plain,
( ( sk_c11 = sk_c10 )
| ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( multiply(sk_c11,sk_c11) = multiply(identity,sk_c10) ) ),
inference(superposition,[status(thm)],[c_38409,c_2618]) ).
tcf(c_57367,plain,
( ( sk_c11 = multiply(identity,identity) )
| ( sk_c11 != multiply(sk_c6,sk_c7) )
| ( multiply(identity,identity) != multiply(sk_c6,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_3015]) ).
tcf(c_60928,plain,
! [X0: $i] :
( ( multiply(identity,X0) = sk_c11 )
| ~ iPr_def_11
| ( multiply(sk_c6,sk_c7) != X0 ) ),
inference(resolution,[status(thm)],[c_7981,c_18855]) ).
tcf(c_61024,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X1) = identity )
| ( multiply(inverse(X0),X0) != X1 ) ),
inference(resolution,[status(thm)],[c_7981,c_5258]) ).
tcf(c_61025,plain,
( ( multiply(identity,sk_c11) = identity )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_61024]) ).
tcf(c_63657,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c8) = multiply(inverse(X0),sk_c10) )
| ( inverse(sk_c8) != multiply(identity,X1) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_3762]) ).
tcf(c_63658,plain,
( ( inverse(sk_c8) = multiply(inverse(sk_c11),sk_c10) )
| ( inverse(sk_c8) != multiply(identity,sk_c11) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_63657]) ).
tcf(c_66322,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c6,sk_c7) = sk_c11 )
| ( multiply(sk_c11,sk_c5) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_37715,c_3715]) ).
tcf(c_69537,plain,
! [X0: $i] :
( ( sk_c11 = multiply(sk_c11,sk_c9) )
| ( sk_c11 != X0 )
| ( multiply(sk_c11,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_702]) ).
tcf(c_69538,plain,
( ( sk_c11 = multiply(sk_c11,sk_c9) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_69537]) ).
tcf(c_70185,plain,
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( sk_c11 != sk_c10 ) ),
inference(superposition,[status(thm)],[c_2633,c_38372]) ).
tcf(c_70344,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(global_subsumption_just,[status(thm)],[c_38373,c_154,c_23104,c_32899]) ).
tcf(c_71586,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( identity != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_809]) ).
tcf(c_71587,plain,
( ( sk_c10 = identity )
| ( identity != sk_c11 )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_71586]) ).
tcf(c_71705,plain,
inverse(sk_c1) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_18443,c_153,c_102,c_151,c_139,c_107,c_390,c_383,c_644,c_684,c_717,c_730,c_758,c_804,c_806,c_873,c_1245,c_1435,c_2228,c_2866,c_2947,c_4016,c_4249,c_4240,c_5395,c_6213,c_7643,c_9723,c_11835,c_13453,c_14457,c_21855,c_23104,c_23105,c_26395,c_32465,c_34838,c_36317,c_37717,c_38409,c_70185,c_70344,c_71587]) ).
tcf(c_71715,plain,
inverse(sk_c2) = sk_c3,
inference(global_subsumption_just,[status(thm)],[c_18453,c_125,c_383,c_684,c_717,c_1435,c_4016,c_4239,c_32475,c_36991,c_37576,c_37716,c_70185,c_70344,c_71587]) ).
tcf(c_71804,plain,
( ~ iPr_def_11
| ( inverse(identity) != sk_c11 )
| ( multiply(sk_c6,sk_c7) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_60928,c_380]) ).
tcf(c_71808,plain,
( ~ iPr_def_11
| ( multiply(sk_c6,sk_c7) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_71804,c_153,c_102,c_151,c_139,c_107,c_390,c_383,c_644,c_684,c_717,c_730,c_758,c_804,c_806,c_873,c_925,c_1245,c_1435,c_1439,c_2228,c_2866,c_2947,c_4016,c_4249,c_4240,c_5395,c_6213,c_7643,c_9723,c_11835,c_13453,c_14457,c_18867,c_21855,c_23104,c_23105,c_26395,c_32465,c_34804,c_34838,c_36317,c_37717,c_38409,c_70185,c_70344,c_71587]) ).
tcf(c_71906,plain,
! [X0: $i] :
( ( X0 != sk_c10 )
| ( multiply(sk_c11,sk_c5) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_13855,c_153,c_102,c_154,c_151,c_147,c_139,c_135,c_137,c_134,c_390,c_383,c_644,c_684,c_717,c_730,c_758,c_804,c_806,c_807,c_873,c_896,c_999,c_1078,c_1245,c_1248,c_1435,c_1439,c_1616,c_2228,c_2866,c_2947,c_4016,c_4250,c_4249,c_4236,c_4346,c_4617,c_5218,c_5245,c_5395,c_6213,c_6215,c_7643,c_9723,c_9770,c_11075,c_11835,c_13453,c_14457,c_21855,c_23104,c_23105,c_26395,c_29814,c_32465,c_32513,c_32899,c_34838,c_36103,c_36317,c_36325,c_37713,c_38132,c_69538,c_71587]) ).
tcf(c_71907,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c5) = X0 )
| ( X0 != sk_c10 ) ),
inference(renaming,[status(thm)],[c_71906]) ).
tcf(c_72209,plain,
multiply(sk_c11,sk_c5) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_20434,c_153,c_102,c_154,c_151,c_147,c_139,c_135,c_137,c_134,c_390,c_383,c_644,c_684,c_717,c_730,c_758,c_804,c_806,c_807,c_873,c_896,c_1078,c_1245,c_1248,c_1435,c_1439,c_1616,c_2228,c_2866,c_2947,c_4016,c_4250,c_4249,c_4236,c_4346,c_4617,c_5218,c_5245,c_5395,c_6213,c_6215,c_7643,c_9723,c_9770,c_11075,c_11835,c_13453,c_14457,c_21855,c_23104,c_23105,c_26395,c_29814,c_32465,c_32513,c_32899,c_34838,c_36103,c_36317,c_36325,c_37713,c_38132,c_69538,c_71587]) ).
tcf(c_72642,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( identity != sk_c10 )
| ( X0 != multiply(sk_c11,sk_c5) ) ),
inference(resolution,[status(thm)],[c_71907,c_9369]) ).
tcf(c_72643,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c11 )
| ( identity != sk_c10 )
| ( sk_c11 != multiply(sk_c11,sk_c5) ) ),
inference(instantiation,[status(thm)],[c_72642]) ).
tcf(c_72990,plain,
inverse(sk_c1) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_36930,c_153,c_102,c_151,c_139,c_107,c_390,c_383,c_644,c_684,c_717,c_730,c_758,c_804,c_806,c_873,c_1245,c_1435,c_2228,c_2866,c_2947,c_4016,c_4249,c_4240,c_5395,c_6213,c_7643,c_9723,c_11835,c_13453,c_14457,c_21855,c_23104,c_23105,c_26395,c_32465,c_34838,c_36317,c_37717,c_38409,c_70185,c_70344,c_71587]) ).
tcf(c_72995,plain,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( multiply(sk_c11,sk_c11) = multiply(identity,sk_c10) ) ),
inference(superposition,[status(thm)],[c_72990,c_2617]) ).
tcf(c_74749,plain,
! [X0: $i] :
( ( sk_c11 = multiply(sk_c11,sk_c9) )
| ( sk_c11 != multiply(identity,X0) )
| ( multiply(sk_c11,sk_c9) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_918]) ).
tcf(c_74750,plain,
( ( sk_c11 = multiply(sk_c11,sk_c9) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(sk_c11,sk_c9) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_74749]) ).
tcf(c_74760,plain,
! [X0: $i] :
( ( sk_c11 = multiply(sk_c11,sk_c5) )
| ( sk_c11 != multiply(identity,X0) )
| ( multiply(sk_c11,sk_c5) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_918]) ).
tcf(c_74761,plain,
( ( sk_c11 = multiply(sk_c11,sk_c5) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(sk_c11,sk_c5) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_74760]) ).
tcf(c_76983,plain,
( ( identity = sk_c10 )
| ( identity != identity )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_1434]) ).
tcf(c_79222,plain,
( ~ iPr_def_13
| ( multiply(identity,sk_c11) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_37152,c_153,c_151,c_139,c_390,c_383,c_644,c_684,c_717,c_730,c_758,c_804,c_873,c_2228,c_2866,c_2947,c_4016,c_4249,c_5395,c_6213,c_7643,c_9723,c_13453,c_14457,c_21855,c_23104,c_23105,c_26395,c_32465,c_37152]) ).
tcf(c_79230,plain,
( ~ iPr_def_13
| ( sk_c11 != sk_c10 ) ),
inference(superposition,[status(thm)],[c_37158,c_79222]) ).
tcf(c_81338,negated_conjecture,
inverse(sk_c8) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_109,c_153,c_151,c_139,c_390,c_383,c_644,c_684,c_717,c_730,c_758,c_804,c_873,c_2228,c_2866,c_2947,c_4016,c_4249,c_5395,c_6213,c_7643,c_9723,c_13453,c_14457,c_21855,c_23104,c_23105,c_26395,c_32465]) ).
tcf(c_81340,negated_conjecture,
inverse(sk_c1) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_104,c_153,c_102,c_151,c_139,c_107,c_390,c_383,c_644,c_684,c_717,c_730,c_758,c_804,c_806,c_873,c_1245,c_1435,c_2228,c_2866,c_2947,c_4016,c_4249,c_4240,c_5395,c_6213,c_7643,c_9723,c_11835,c_13453,c_14457,c_21855,c_23104,c_23105,c_26395,c_32465,c_34838,c_36317,c_37717,c_38409,c_70185,c_70344,c_71587]) ).
tcf(c_81344,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm)],[c_81338,c_102]) ).
tcf(c_81361,negated_conjecture,
inverse(sk_c2) = sk_c3,
inference(global_subsumption_just,[status(thm)],[c_122,c_71715]) ).
tcf(c_81363,plain,
multiply(sk_c3,sk_c2) = identity,
inference(superposition,[status(thm)],[c_81361,c_102]) ).
tcf(c_81490,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c8,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_81344,c_103]) ).
tcf(c_81532,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_81363,c_103]) ).
tcf(c_81611,plain,
multiply(inverse(sk_c11),identity) = multiply(identity,sk_c1),
inference(superposition,[status(thm)],[c_81340,c_2634]) ).
tcf(c_81621,plain,
! [X0: $i] : multiply(inverse(sk_c11),multiply(identity,X0)) = multiply(multiply(identity,sk_c1),X0),
inference(superposition,[status(thm)],[c_81611,c_103]) ).
tcf(c_81661,plain,
( ( multiply(sk_c3,sk_c10) = multiply(identity,sk_c3) )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_120,c_81532]) ).
tcf(c_81925,plain,
! [X0: $i] : multiply(multiply(identity,sk_c1),X0) = multiply(inverse(sk_c11),X0),
inference(superposition,[status(thm)],[c_101,c_81621]) ).
tcf(c_81961,plain,
! [X0: $i] : multiply(identity,multiply(sk_c1,X0)) = multiply(inverse(sk_c11),X0),
inference(superposition,[status(thm)],[c_81925,c_103]) ).
tcf(c_82135,plain,
( ( multiply(sk_c6,sk_c7) = sk_c11 )
| ( multiply(inverse(sk_c11),sk_c10) = multiply(identity,sk_c11) ) ),
inference(superposition,[status(thm)],[c_110,c_81961]) ).
tcf(c_82263,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_81661,c_153,c_154,c_390,c_383,c_644,c_717,c_722,c_730,c_753,c_758,c_898,c_998,c_1071,c_1443,c_2023,c_2036,c_2228,c_2965,c_3112,c_3977,c_4016,c_4617,c_7643,c_8588,c_8648,c_9804,c_9956,c_10282,c_13610,c_13623,c_20409,c_20413,c_20638,c_21855,c_23104,c_23513,c_32475,c_36317,c_41863,c_42467,c_43319,c_44507,c_57367,c_63658,c_66322,c_70185,c_71587,c_71705,c_72209,c_72995,c_74761,c_79230,c_82135]) ).
tcf(c_82272,plain,
multiply(sk_c11,sk_c9) = multiply(identity,sk_c11),
inference(superposition,[status(thm)],[c_82263,c_81490]) ).
tcf(c_82287,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_82272,c_82135,c_79230,c_76983,c_74761,c_74750,c_72643,c_72209,c_71808,c_71587,c_70344,c_70185,c_66322,c_63658,c_61025,c_57367,c_45789,c_44513,c_44507,c_43319,c_42467,c_41863,c_36317,c_32475,c_23513,c_21855,c_20638,c_20413,c_20409,c_13623,c_13610,c_10282,c_9956,c_8691,c_8648,c_8588,c_7643,c_5104,c_4617,c_4016,c_2965,c_2228,c_2036,c_2023,c_1443,c_1439,c_1078,c_1071,c_998,c_898,c_896,c_758,c_753,c_730,c_722,c_717,c_684,c_383,c_390,c_153]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP217-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n014.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 14:10:03 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 26.05/4.32 % SZS status Started for theBenchmark.p
% 26.05/4.32 % SZS status Unsatisfiable for theBenchmark.p
% 26.05/4.32
% 26.05/4.32 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 26.05/4.32
% 26.05/4.32 % ------ iProver source info
% 26.05/4.32
% 26.05/4.32 % git: date: 2026-07-19 20:42:38 +0200
% 26.05/4.32 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 26.05/4.32 % git: non_committed_changes: false
% 26.05/4.32
% 26.05/4.32 % ------ Parsing...% successful
% 26.05/4.32
% 26.05/4.32
% 26.05/4.32 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 26.05/4.32
% 26.05/4.32 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 26.05/4.32
% 26.05/4.32 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 26.05/4.32
% 26.05/4.32 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 26.05/4.32 % ------ Proving...
% 26.05/4.32 % ------ Problem Properties
% 26.05/4.32
% 26.05/4.32 %
% 26.05/4.32 % clauses 56
% 26.05/4.32 % conjectures 53
% 26.05/4.32 % EPR 1
% 26.05/4.32 % Horn 7
% 26.05/4.32 % unary 3
% 26.05/4.32 % binary 48
% 26.05/4.32 % lits 115
% 26.05/4.32 % lits eq 107
% 26.05/4.32 % fd_pure 0
% 26.05/4.32 % fd_pseudo 0
% 26.05/4.32 % fd_cond 0
% 26.05/4.32 % fd_pseudo_cond 0
% 26.05/4.32 % AC symbols 0
% 26.05/4.32
% 26.05/4.32 % ------ Input Options Time Limit: Unbounded
% 26.05/4.32
% 26.05/4.32
% 26.05/4.32 % ------
% 26.05/4.32 % Current options:
% 26.05/4.32 % ------
% 26.05/4.32
% 26.05/4.32
% 26.05/4.32 %
% 26.05/4.32
% 26.05/4.32 % ------ Proving...
% 26.05/4.32 %
% 26.05/4.32
% 26.05/4.32 % SZS status Unsatisfiable for theBenchmark.p
% 26.05/4.32
% 26.05/4.32 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 26.05/4.33
% 26.05/4.33
%------------------------------------------------------------------------------