%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP312-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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:32:48 PM UTC 2026
% Result : Unsatisfiable 44.46s 9.34s
% Output : CNFRefutation 44.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 42
% Syntax : Number of formulae : 423 ( 78 unt; 0 def)
% Number of atoms : 989 ( 913 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 952 ( 386 ~; 566 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 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 : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 245 ( 0 sgn 245 !; 0 ?; 206 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| multiply(sk_c11,sk_c12) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| multiply(sk_c11,sk_c12) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c11,sk_c12) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c12 = inverse(sk_c4)
| multiply(sk_c11,sk_c12) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f11,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c11,sk_c12) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c11 = inverse(sk_c5)
| multiply(sk_c11,sk_c12) = sk_c10 ),
inference(reorient_equations,[],[f11]) ).
fof(f15,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c11,sk_c12) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c9 = inverse(sk_c6)
| multiply(sk_c11,sk_c12) = sk_c10 ),
inference(reorient_equations,[],[f15]) ).
fof(f22,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c7
| multiply(sk_c11,sk_c12) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f23,plain,
( sk_c7 = multiply(sk_c8,sk_c9)
| multiply(sk_c11,sk_c12) = sk_c10 ),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c11 = multiply(sk_c1,sk_c12) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c12 = inverse(sk_c4)
| sk_c11 = multiply(sk_c1,sk_c12) ),
inference(reorient_equations,[],[f26]) ).
fof(f30,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f31,plain,
( sk_c11 = inverse(sk_c5)
| sk_c11 = multiply(sk_c1,sk_c12) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c11 = multiply(sk_c1,sk_c12) ),
inference(reorient_equations,[],[f32]) ).
fof(f34,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f35,plain,
( sk_c9 = inverse(sk_c6)
| sk_c11 = multiply(sk_c1,sk_c12) ),
inference(reorient_equations,[],[f34]) ).
fof(f44,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f45,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
( inverse(sk_c4) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f47,plain,
( sk_c12 = inverse(sk_c4)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f46]) ).
fof(f50,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f51,plain,
( sk_c11 = inverse(sk_c5)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f50]) ).
fof(f54,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f55,plain,
( sk_c9 = inverse(sk_c6)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f54]) ).
fof(f66,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f67,plain,
( sk_c12 = inverse(sk_c4)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f66]) ).
fof(f68,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f69,plain,
( sk_c10 = multiply(sk_c5,sk_c11)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f68]) ).
fof(f70,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f71,plain,
( sk_c11 = inverse(sk_c5)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f70]) ).
fof(f74,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f75,plain,
( sk_c9 = inverse(sk_c6)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f74]) ).
fof(f84,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f85,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f84]) ).
fof(f86,negated_conjecture,
( inverse(sk_c4) = sk_c12
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f87,plain,
( sk_c12 = inverse(sk_c4)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f86]) ).
fof(f88,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f89,plain,
( sk_c10 = multiply(sk_c5,sk_c11)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f88]) ).
fof(f90,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f91,plain,
( sk_c11 = inverse(sk_c5)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f90]) ).
fof(f92,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f93,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f92]) ).
fof(f94,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f95,plain,
( sk_c9 = inverse(sk_c6)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f94]) ).
fof(f98,negated_conjecture,
( inverse(sk_c8) = sk_c7
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f99,plain,
( inverse(sk_c8) = sk_c7
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f98]) ).
fof(f106,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_52) ).
fof(f107,plain,
( sk_c12 = inverse(sk_c4)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f106]) ).
fof(f110,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_54) ).
fof(f111,plain,
( sk_c11 = inverse(sk_c5)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f110]) ).
fof(f112,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_55) ).
fof(f113,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f112]) ).
fof(f114,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_56) ).
fof(f115,plain,
( sk_c9 = inverse(sk_c6)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f114]) ).
fof(f124,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| inverse(sk_c3) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_61) ).
fof(f125,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c11 = inverse(sk_c3) ),
inference(reorient_equations,[],[f124]) ).
fof(f126,negated_conjecture,
( inverse(sk_c4) = sk_c12
| inverse(sk_c3) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_62) ).
fof(f127,plain,
( sk_c12 = inverse(sk_c4)
| sk_c11 = inverse(sk_c3) ),
inference(reorient_equations,[],[f126]) ).
fof(f130,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c3) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_64) ).
fof(f131,plain,
( sk_c11 = inverse(sk_c5)
| sk_c11 = inverse(sk_c3) ),
inference(reorient_equations,[],[f130]) ).
fof(f132,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| inverse(sk_c3) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_65) ).
fof(f133,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c11 = inverse(sk_c3) ),
inference(reorient_equations,[],[f132]) ).
fof(f134,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c3) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_66) ).
fof(f135,plain,
( sk_c9 = inverse(sk_c6)
| sk_c11 = inverse(sk_c3) ),
inference(reorient_equations,[],[f134]) ).
fof(f144,negated_conjecture,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X7,X6) != X8
| inverse(X8) != X6
| inverse(X7) != X8
| multiply(X6,sk_c11) != sk_c12
| inverse(X5) != X6
| multiply(X5,X6) != sk_c12
| inverse(X4) != sk_c11
| multiply(X4,sk_c11) != sk_c10
| inverse(X3) != sk_c12
| multiply(X3,sk_c12) != sk_c11
| inverse(X2) != sk_c11
| multiply(X2,sk_c11) != sk_c12
| inverse(X1) != sk_c11
| multiply(X1,sk_c11) != sk_c10
| inverse(X0) != sk_c12
| multiply(X0,sk_c12) != sk_c11
| multiply(sk_c11,sk_c12) != sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_71) ).
fof(f145,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X7,X6) != X8
| inverse(X8) != X6
| inverse(X7) != X8
| sk_c12 != multiply(X6,sk_c11)
| inverse(X5) != X6
| sk_c12 != multiply(X5,X6)
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(X3,sk_c12)
| sk_c11 != inverse(X2)
| sk_c12 != multiply(X2,sk_c11)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(X1,sk_c11)
| inverse(X0) != sk_c12
| sk_c11 != multiply(X0,sk_c12)
| multiply(sk_c11,sk_c12) != sk_c10 ),
inference(reorient_equations,[],[f144]) ).
fof(f146,plain,
! [X2,X3,X0,X1,X8,X7,X4,X5] :
( multiply(X7,inverse(X5)) != X8
| inverse(X5) != inverse(X8)
| inverse(X7) != X8
| sk_c12 != multiply(inverse(X5),sk_c11)
| sk_c12 != multiply(X5,inverse(X5))
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(X3,sk_c12)
| sk_c11 != inverse(X2)
| sk_c12 != multiply(X2,sk_c11)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(X1,sk_c11)
| inverse(X0) != sk_c12
| sk_c11 != multiply(X0,sk_c12)
| multiply(sk_c11,sk_c12) != sk_c10 ),
inference(equality_resolution,[],[f145]) ).
fof(f147,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( inverse(X7) != multiply(X7,inverse(X5))
| inverse(X5) != inverse(inverse(X7))
| sk_c12 != multiply(inverse(X5),sk_c11)
| sk_c12 != multiply(X5,inverse(X5))
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(X3,sk_c12)
| sk_c11 != inverse(X2)
| sk_c12 != multiply(X2,sk_c11)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(X1,sk_c11)
| inverse(X0) != sk_c12
| sk_c11 != multiply(X0,sk_c12)
| multiply(sk_c11,sk_c12) != sk_c10 ),
inference(equality_resolution,[],[f146]) ).
tcf(c_123,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_124,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c4,sk_c12) = sk_c11 )
| ( multiply(sk_c11,sk_c12) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c11,sk_c12) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c11,sk_c12) = sk_c10 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c11,sk_c12) = sk_c10 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_135,negated_conjecture,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( multiply(sk_c11,sk_c12) = sk_c10 ) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c1,sk_c12) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_140,negated_conjecture,
( ( multiply(sk_c1,sk_c12) = sk_c11 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c2,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_158,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_159,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_161,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_166,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_167,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_168,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_169,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_170,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_171,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_173,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_177,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c3,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_179,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_180,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c12 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_181,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_186,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_187,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_189,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_190,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_191,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_196,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( inverse(X6) != sk_c11 )
| ( inverse(X5) != sk_c11 )
| ( inverse(X4) != sk_c11 )
| ( inverse(X3) != sk_c12 )
| ( inverse(X2) != sk_c12 )
| ( multiply(sk_c11,sk_c12) != sk_c10 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(X6,sk_c11) != sk_c12 )
| ( multiply(X5,sk_c11) != sk_c10 )
| ( multiply(X4,sk_c11) != sk_c10 )
| ( multiply(X3,sk_c12) != sk_c11 )
| ( multiply(X2,sk_c12) != sk_c11 )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_198,plain,
multiply(inverse(sk_c11),sk_c11) = identity,
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_829,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_196]) ).
tcf(c_830,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c12) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_196]) ).
tcf(c_831,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c12 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_196]) ).
tcf(c_832,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_196]) ).
tcf(c_833,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c11,sk_c12) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_196]) ).
tcf(c_834,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_835,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_836,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_837,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_840,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_1187,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c12) = sk_c10 )
| ( sk_c10 != X0 )
| ( multiply(sk_c11,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_1188,plain,
( ( multiply(sk_c11,sk_c12) = sk_c10 )
| ( sk_c10 != sk_c11 )
| ( multiply(sk_c11,sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1187]) ).
tcf(c_1191,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c12) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c11,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_1192,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c12) = sk_c10 )
| ( sk_c10 != multiply(X0,X1) )
| ( multiply(sk_c11,sk_c12) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_1187]) ).
tcf(c_1193,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c12) = multiply(X0,X1) )
| ( sk_c12 != X1 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_836]) ).
tcf(c_1194,plain,
( ( multiply(sk_c11,sk_c12) = sk_c10 )
| ( sk_c10 != multiply(sk_c11,sk_c11) )
| ( multiply(sk_c11,sk_c12) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1192]) ).
tcf(c_1195,plain,
( ( multiply(sk_c11,sk_c12) = multiply(sk_c11,sk_c11) )
| ( sk_c12 != sk_c11 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1193]) ).
tcf(c_1206,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_1207,plain,
( ( sk_c10 = multiply(sk_c11,sk_c11) )
| ( sk_c10 != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1206]) ).
tcf(c_1208,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c12) = multiply(X0,sk_c12) )
| ( sk_c12 != sk_c12 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_1193]) ).
tcf(c_1209,plain,
sk_c12 = sk_c12,
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_1210,plain,
! [X0: $i,X1: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_1213,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_1214,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_1225,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c12) = X1 )
| ( X1 != multiply(X0,sk_c12) )
| ( multiply(sk_c11,sk_c12) != multiply(X0,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1191]) ).
tcf(c_1231,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != sk_c12 )
| ( X0 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1210]) ).
tcf(c_1237,plain,
! [X0: $i] : multiply(identity,multiply(X0,sk_c12)) = multiply(X0,sk_c12),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_1239,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,sk_c12) )
| ( X2 != X1 )
| ( multiply(X0,sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_1246,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != sk_c10 )
| ( multiply(X0,X1) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1206]) ).
tcf(c_1256,plain,
( ( sk_c12 = multiply(identity,sk_c12) )
| ( sk_c12 != sk_c12 )
| ( multiply(identity,sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1231]) ).
tcf(c_1257,plain,
multiply(identity,sk_c12) = sk_c12,
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_1259,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_1375,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c12) = X1 )
| ( X1 != multiply(identity,multiply(X0,sk_c12)) )
| ( multiply(sk_c11,sk_c12) != multiply(identity,multiply(X0,sk_c12)) ) ),
inference(instantiation,[status(thm)],[c_1191]) ).
tcf(c_1499,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c12) = X2 )
| ( X2 != X1 )
| ( multiply(X0,sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_1501,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c12) = multiply(X1,X2) )
| ( sk_c12 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_836]) ).
tcf(c_1555,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_124,c_125]) ).
tcf(c_1619,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != multiply(identity,sk_c12) )
| ( X0 != multiply(identity,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1210]) ).
tcf(c_1624,plain,
( ( multiply(sk_c11,sk_c12) = sk_c12 )
| ( sk_c12 != multiply(identity,sk_c12) )
| ( multiply(sk_c11,sk_c12) != multiply(identity,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1225]) ).
tcf(c_1628,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_1922,plain,
( ( multiply(sk_c11,sk_c12) = multiply(identity,sk_c12) )
| ( sk_c12 != sk_c12 )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_1208]) ).
tcf(c_1930,plain,
( ( sk_c12 = multiply(identity,multiply(identity,sk_c12)) )
| ( sk_c12 != multiply(identity,sk_c12) )
| ( multiply(identity,multiply(identity,sk_c12)) != multiply(identity,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1619]) ).
tcf(c_1931,plain,
multiply(identity,multiply(identity,sk_c12)) = multiply(identity,sk_c12),
inference(instantiation,[status(thm)],[c_1237]) ).
tcf(c_2219,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_2221,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_2468,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1555,c_123]) ).
tcf(c_2492,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(inverse(sk_c4),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_166,c_2468]) ).
tcf(c_2499,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c6),sk_c12) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_190,c_2468]) ).
tcf(c_2500,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(inverse(sk_c6),sk_c12) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_170,c_2468]) ).
tcf(c_2517,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(sk_c2),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_161,c_2468]) ).
tcf(c_2518,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(inverse(sk_c2),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_159,c_2468]) ).
tcf(c_2519,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(inverse(sk_c2),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_157,c_2468]) ).
tcf(c_2525,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_123,c_2468]) ).
tcf(c_2526,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_124,c_2468]) ).
tcf(c_2527,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_125,c_2468]) ).
tcf(c_2540,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_2468,c_2468]) ).
tcf(c_2720,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c12) = multiply(X1,multiply(identity,sk_c12)) )
| ( sk_c12 != multiply(identity,sk_c12) )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_1501]) ).
tcf(c_2975,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_835,c_124]) ).
tcf(c_2979,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_835,c_834]) ).
tcf(c_3030,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c4,sk_c12) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c4,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_1499]) ).
tcf(c_3031,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c4,sk_c12) )
| ( X1 != X0 )
| ( multiply(sk_c4,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_1239]) ).
tcf(c_3146,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c12) = X0 )
| ( X0 != sk_c10 )
| ( multiply(sk_c11,sk_c12) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1191]) ).
tcf(c_3162,plain,
( ( sk_c10 = multiply(sk_c2,sk_c11) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c2,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1246]) ).
tcf(c_3169,plain,
( ~ iPr_def_10
| ( inverse(sk_c2) != sk_c11 )
| ( multiply(sk_c2,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_829]) ).
tcf(c_3176,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = sk_c11 )
| ( sk_c11 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_3541,plain,
( ( multiply(sk_c2,sk_c11) = sk_c10 )
| ~ iPr_def_10
| ( inverse(sk_c5) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_158,c_829]) ).
tcf(c_3545,plain,
( ( inverse(sk_c2) = sk_c11 )
| ~ iPr_def_10
| ( inverse(sk_c5) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_168,c_829]) ).
tcf(c_3555,plain,
( ( inverse(sk_c5) = sk_c11 )
| ~ iPr_def_10
| ( inverse(sk_c2) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_159,c_829]) ).
tcf(c_3717,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_186,c_830]) ).
tcf(c_3719,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_146,c_830]) ).
tcf(c_3723,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_141,c_830]) ).
tcf(c_3724,plain,
( ( inverse(sk_c5) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_139,c_830]) ).
tcf(c_3725,plain,
( ( inverse(sk_c4) = sk_c12 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_137,c_830]) ).
tcf(c_3777,plain,
( ( multiply(sk_c11,sk_c12) = sk_c12 )
| ( sk_c12 != multiply(identity,multiply(identity,sk_c12)) )
| ( multiply(sk_c11,sk_c12) != multiply(identity,multiply(identity,sk_c12)) ) ),
inference(instantiation,[status(thm)],[c_1375]) ).
tcf(c_3942,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_836,c_835]) ).
tcf(c_4000,plain,
( ( sk_c11 = multiply(sk_c4,sk_c12) )
| ( multiply(sk_c11,sk_c12) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2979,c_126]) ).
tcf(c_4062,plain,
! [X0: $i] : X0 = multiply(identity,X0),
inference(resolution,[status(thm)],[c_2979,c_123]) ).
tcf(c_4209,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_2540,c_124]) ).
tcf(c_4454,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( multiply(sk_c11,sk_c12) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_833,c_169,c_833,c_3169,c_3555,c_3545,c_3541]) ).
tcf(c_4462,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_131,c_4454]) ).
tcf(c_4463,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c5) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_129,c_4454]) ).
tcf(c_4464,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c4) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_127,c_4454]) ).
tcf(c_4840,plain,
! [X0: $i] :
( ( multiply(X0,sk_c12) = multiply(identity,multiply(identity,sk_c12)) )
| ( sk_c12 != multiply(identity,sk_c12) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_2720]) ).
tcf(c_4843,plain,
( ( multiply(sk_c11,sk_c12) = multiply(identity,multiply(identity,sk_c12)) )
| ( sk_c12 != multiply(identity,sk_c12) )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_4840]) ).
tcf(c_4936,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c3) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_181,c_831]) ).
tcf(c_4937,plain,
( ( inverse(sk_c5) = sk_c11 )
| ~ iPr_def_12
| ( inverse(sk_c3) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_179,c_831]) ).
tcf(c_4938,plain,
( ( inverse(sk_c4) = sk_c12 )
| ~ iPr_def_12
| ( inverse(sk_c3) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_177,c_831]) ).
tcf(c_5159,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != multiply(sk_c2,sk_c11) )
| ( X0 != multiply(sk_c2,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1628]) ).
tcf(c_5162,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(sk_c2,sk_c11) )
| ( sk_c11 != multiply(sk_c2,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_5159]) ).
tcf(c_5187,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_187,c_4209]) ).
tcf(c_5188,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_167,c_4209]) ).
tcf(c_5191,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_169,c_4209]) ).
tcf(c_5307,plain,
( iPr_def_13
| ( inverse(sk_c6) = sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_4462,c_191,c_169,c_151,c_131,c_833,c_3169,c_3555,c_3545,c_3541,c_3723,c_4936]) ).
tcf(c_5311,plain,
( iPr_def_13
| ( inverse(sk_c5) = sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_4463,c_189,c_169,c_149,c_129,c_833,c_3169,c_3555,c_3545,c_3541,c_3724,c_4937]) ).
tcf(c_5418,plain,
( iPr_def_13
| ( inverse(sk_c4) = sk_c12 ) ),
inference(global_subsumption_just,[status(thm)],[c_4464,c_187,c_169,c_147,c_127,c_833,c_3169,c_3555,c_3545,c_3541,c_3725,c_4938]) ).
tcf(c_5799,plain,
( ( inverse(sk_c2) = sk_c11 )
| ~ iPr_def_10
| ( inverse(sk_c5) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_829,c_168]) ).
tcf(c_6172,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_5187,c_186]) ).
tcf(c_6301,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c12) = sk_c10 )
| ( sk_c10 != X0 )
| ( multiply(sk_c4,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_3030]) ).
tcf(c_6340,plain,
! [X0: $i] :
( ( sk_c10 = multiply(sk_c4,sk_c12) )
| ( sk_c10 != X0 )
| ( multiply(sk_c4,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_3031]) ).
tcf(c_6341,plain,
( ( multiply(sk_c11,sk_c12) = sk_c10 )
| ( sk_c10 != multiply(sk_c4,sk_c12) )
| ( multiply(sk_c11,sk_c12) != multiply(sk_c4,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1192]) ).
tcf(c_6365,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c12) = multiply(sk_c4,sk_c12) )
| ( multiply(sk_c4,sk_c12) != X0 )
| ( multiply(sk_c11,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_3031]) ).
tcf(c_6366,plain,
( ( multiply(sk_c11,sk_c12) = multiply(sk_c4,sk_c12) )
| ( multiply(sk_c4,sk_c12) != sk_c11 )
| ( multiply(sk_c11,sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_6365]) ).
tcf(c_6378,plain,
! [X0: $i] :
( ( identity = multiply(sk_c4,sk_c12) )
| ( identity != X0 )
| ( multiply(sk_c4,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_3031]) ).
tcf(c_6379,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != multiply(sk_c4,sk_c12) )
| ( X0 != multiply(sk_c4,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_2221]) ).
tcf(c_6381,plain,
( ( sk_c11 = identity )
| ( identity != multiply(sk_c4,sk_c12) )
| ( sk_c11 != multiply(sk_c4,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_6379]) ).
tcf(c_6504,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_5188,c_166]) ).
tcf(c_6516,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_830,c_146]) ).
tcf(c_6520,plain,
( ( inverse(sk_c4) = sk_c12 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_830,c_137]) ).
tcf(c_6525,plain,
( ( multiply(sk_c4,sk_c12) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_830,c_136]) ).
tcf(c_6527,plain,
( ( multiply(sk_c6,sk_c9) = sk_c12 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_830,c_140]) ).
tcf(c_6595,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( multiply(inverse(sk_c11),X0) = multiply(sk_c2,X0) ) ),
inference(superposition,[status(thm)],[c_6504,c_2540]) ).
tcf(c_6839,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_5191,c_168]) ).
tcf(c_6843,plain,
( ( inverse(sk_c2) = sk_c11 )
| ~ iPr_def_12
| ( sk_c12 != identity )
| ( inverse(sk_c5) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_5191,c_831]) ).
tcf(c_6893,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(inverse(sk_c11),X0) = multiply(sk_c2,X0) ) ),
inference(superposition,[status(thm)],[c_6839,c_2540]) ).
tcf(c_7080,plain,
! [X0: $i,X1: $i] :
( ( X0 = multiply(inverse(X1),X1) )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_2975,c_2979]) ).
tcf(c_7081,plain,
( ( sk_c11 = multiply(inverse(sk_c11),sk_c11) )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_7080]) ).
tcf(c_7821,plain,
( ( sk_c11 = identity )
| ( multiply(inverse(sk_c11),identity) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_6172,c_2526]) ).
tcf(c_7872,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1555,c_123]) ).
tcf(c_7973,plain,
! [X0: $i] : multiply(inverse(inverse(identity)),X0) = X0,
inference(superposition,[status(thm)],[c_2525,c_7872]) ).
tcf(c_7983,plain,
multiply(inverse(inverse(identity)),sk_c11) = sk_c11,
inference(instantiation,[status(thm)],[c_7973]) ).
tcf(c_8030,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c12,sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_167,c_2492]) ).
tcf(c_8038,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(inverse(sk_c12),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_8030,c_7872]) ).
tcf(c_8099,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_8038,c_124]) ).
tcf(c_8105,plain,
( ( sk_c11 = identity )
| ( multiply(inverse(sk_c11),identity) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_8099,c_2526]) ).
tcf(c_8117,plain,
( ( sk_c2 = sk_c3 )
| ( sk_c11 = identity ) ),
inference(superposition,[status(thm)],[c_8105,c_7821]) ).
tcf(c_8714,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c12) = sk_c11 )
| ( sk_c11 != X0 )
| ( multiply(sk_c4,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_3176]) ).
tcf(c_12549,plain,
( ( multiply(sk_c11,sk_c12) = sk_c12 )
| ( sk_c12 != sk_c10 )
| ( multiply(sk_c11,sk_c12) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3146]) ).
tcf(c_12820,plain,
( ( inverse(sk_c2) = sk_c11 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_5799,c_169,c_3169,c_3555,c_3545,c_3541]) ).
tcf(c_12822,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_12820,c_3169,c_3555,c_3541,c_12820]) ).
tcf(c_12999,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_6516,c_147,c_3719]) ).
tcf(c_13088,plain,
( ( multiply(sk_c4,sk_c12) = sk_c11 )
| ~ iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_6525,c_12999]) ).
tcf(c_13089,plain,
( ( multiply(sk_c6,sk_c9) = sk_c12 )
| ~ iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_6527,c_12999]) ).
tcf(c_13092,plain,
( ( inverse(sk_c4) = sk_c12 )
| ~ iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_6520,c_12999]) ).
tcf(c_13428,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),X0) )
| ( sk_c10 != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_1206]) ).
tcf(c_13429,plain,
( ( sk_c10 = multiply(inverse(sk_c11),sk_c11) )
| ( sk_c10 != identity )
| ( multiply(inverse(sk_c11),sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_13428]) ).
tcf(c_16199,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c12) = X0 )
| ( X0 != sk_c12 )
| ( multiply(sk_c11,sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1191]) ).
tcf(c_16200,plain,
( ( multiply(sk_c11,sk_c12) = sk_c11 )
| ( sk_c11 != sk_c12 )
| ( multiply(sk_c11,sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_16199]) ).
tcf(c_16256,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != multiply(inverse(X1),X1) )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(instantiation,[status(thm)],[c_1214]) ).
tcf(c_16257,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != multiply(inverse(sk_c11),sk_c11) )
| ( sk_c11 != multiply(inverse(sk_c11),sk_c11) ) ),
inference(instantiation,[status(thm)],[c_16256]) ).
tcf(c_16880,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c2,sk_c11) )
| ( X1 != X0 )
| ( multiply(sk_c2,sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_16881,plain,
( ( sk_c11 = multiply(sk_c2,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c2,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_16880]) ).
tcf(c_17690,plain,
( ~ iPr_def_12
| ( sk_c12 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_124,c_831]) ).
tcf(c_17782,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1555,c_123]) ).
tcf(c_17883,plain,
! [X0: $i] : multiply(inverse(inverse(inverse(X0))),X0) = identity,
inference(superposition,[status(thm)],[c_2526,c_17782]) ).
tcf(c_18059,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,sk_c12) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_191,c_2499]) ).
tcf(c_18068,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c9),sk_c9) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_18059,c_17782]) ).
tcf(c_18073,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c9,sk_c12) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_171,c_2500]) ).
tcf(c_18081,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(inverse(sk_c9),sk_c9) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_18073,c_17782]) ).
tcf(c_18236,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_18068,c_124]) ).
tcf(c_18243,plain,
( ( sk_c12 = identity )
| ( multiply(inverse(sk_c11),identity) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_18236,c_2526]) ).
tcf(c_18347,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_18081,c_124]) ).
tcf(c_18358,plain,
! [X0: $i] :
( ( sk_c12 = identity )
| ( multiply(sk_c11,multiply(sk_c2,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_18347,c_17782]) ).
tcf(c_18359,plain,
( ( sk_c12 = identity )
| ( multiply(inverse(sk_c11),identity) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_18347,c_2526]) ).
tcf(c_18367,plain,
( ( sk_c2 = sk_c3 )
| ( sk_c12 = identity ) ),
inference(superposition,[status(thm)],[c_18359,c_18243]) ).
tcf(c_18694,plain,
! [X0: $i] :
( ( sk_c12 = identity )
| ( multiply(inverse(sk_c11),X0) = multiply(sk_c2,X0) ) ),
inference(superposition,[status(thm)],[c_18358,c_17782]) ).
tcf(c_19028,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,identity)),multiply(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_123,c_2527]) ).
tcf(c_19029,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,identity)) = X1,
inference(superposition,[status(thm)],[c_124,c_2527]) ).
tcf(c_19142,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(inverse(inverse(X1))))),multiply(X0,identity)) = X1,
inference(superposition,[status(thm)],[c_17883,c_2527]) ).
tcf(c_19161,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_19142,c_19029]) ).
tcf(c_19231,plain,
( ~ iPr_def_12
| ( sk_c12 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_17690,c_19161]) ).
tcf(c_19233,plain,
inverse(inverse(sk_c11)) = sk_c11,
inference(instantiation,[status(thm)],[c_19161]) ).
tcf(c_20974,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(X0),identity)),identity) = X0,
inference(superposition,[status(thm)],[c_124,c_19028]) ).
tcf(c_21384,plain,
! [X0: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1259]) ).
tcf(c_21385,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1210]) ).
tcf(c_21388,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c12 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_21385]) ).
tcf(c_21389,plain,
( ( sk_c11 = sk_c12 )
| ( sk_c12 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_21384]) ).
tcf(c_22272,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != multiply(inverse(X1),X1) )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(instantiation,[status(thm)],[c_1628]) ).
tcf(c_22273,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c11),sk_c11) )
| ( sk_c11 != multiply(inverse(sk_c11),sk_c11) ) ),
inference(instantiation,[status(thm)],[c_22272]) ).
tcf(c_22473,plain,
! [X0: $i] : multiply(inverse(X0),identity) = inverse(X0),
inference(superposition,[status(thm)],[c_2526,c_20974]) ).
tcf(c_22482,plain,
multiply(inverse(identity),identity) = inverse(inverse(identity)),
inference(superposition,[status(thm)],[c_17883,c_20974]) ).
tcf(c_22518,plain,
inverse(inverse(identity)) = inverse(identity),
inference(demodulation,[status(thm)],[c_22482,c_22473]) ).
tcf(c_24946,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( multiply(sk_c11,sk_c12) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_833,c_12822]) ).
tcf(c_24969,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X2,X0) = X1 )
| ( X2 != identity )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_4062,c_3942]) ).
tcf(c_24970,plain,
( ( multiply(sk_c11,sk_c11) = sk_c11 )
| ( sk_c11 != identity )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_24969]) ).
tcf(c_26459,plain,
( ~ iPr_def_11
| ( inverse(sk_c4) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_13088,c_830]) ).
tcf(c_26462,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_13089,c_13092,c_26459]) ).
tcf(c_26471,plain,
( iPr_def_13
| iPr_def_12
| ( multiply(sk_c11,sk_c12) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_24946,c_26462]) ).
tcf(c_27905,plain,
( ( sk_c12 = sk_c10 )
| ( sk_c10 != multiply(sk_c2,sk_c11) )
| ( sk_c12 != multiply(sk_c2,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_5159]) ).
tcf(c_27907,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1210]) ).
tcf(c_27910,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c12 != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_27907]) ).
tcf(c_30000,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c4,sk_c12) )
| ( X0 != sk_c10 )
| ( multiply(sk_c4,sk_c12) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3031]) ).
tcf(c_30003,plain,
( ( sk_c11 = multiply(sk_c4,sk_c12) )
| ( sk_c11 != sk_c10 )
| ( multiply(sk_c4,sk_c12) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_30000]) ).
tcf(c_32822,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_3717,c_13092,c_26459]) ).
tcf(c_33762,plain,
! [X0: $i] :
( ( sk_c12 = sk_c10 )
| ( sk_c10 != X0 )
| ( sk_c12 != X0 ) ),
inference(instantiation,[status(thm)],[c_1628]) ).
tcf(c_33764,plain,
( ( sk_c12 = sk_c10 )
| ( sk_c10 != sk_c11 )
| ( sk_c12 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_33762]) ).
tcf(c_35595,plain,
( ( identity = multiply(sk_c4,sk_c12) )
| ( identity != identity )
| ( multiply(sk_c4,sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_6378]) ).
tcf(c_37262,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( multiply(sk_c11,sk_c12) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_833,c_32822]) ).
tcf(c_37264,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(inverse(sk_c12),X0) = multiply(sk_c4,X0) ) ),
inference(superposition,[status(thm)],[c_167,c_2540]) ).
tcf(c_37265,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(inverse(sk_c12),X0) = multiply(sk_c4,X0) ) ),
inference(superposition,[status(thm)],[c_147,c_2540]) ).
tcf(c_37266,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(inverse(sk_c11),X0) = multiply(sk_c5,X0) ) ),
inference(superposition,[status(thm)],[c_169,c_2540]) ).
tcf(c_37268,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(inverse(sk_c9),X0) = multiply(sk_c6,X0) ) ),
inference(superposition,[status(thm)],[c_171,c_2540]) ).
tcf(c_37274,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_2540,c_124]) ).
tcf(c_37293,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c9),X0) = multiply(sk_c6,X0) ) ),
inference(superposition,[status(thm)],[c_191,c_2540]) ).
tcf(c_37323,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_124,c_37264]) ).
tcf(c_37327,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c4,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_124,c_37265]) ).
tcf(c_37333,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_37266,c_124]) ).
tcf(c_37367,plain,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_124,c_37268]) ).
tcf(c_37547,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_37293,c_124]) ).
tcf(c_37622,negated_conjecture,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_829,c_169,c_3169,c_3555,c_3545,c_3541]) ).
tcf(c_37624,plain,
( iPr_def_13
| iPr_def_12
| ( multiply(sk_c11,sk_c12) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_37262,c_37622]) ).
tcf(c_37657,plain,
( ~ iPr_def_12
| ( sk_c12 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_124,c_831]) ).
tcf(c_37786,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_37274,c_125]) ).
tcf(c_38337,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_2526,c_2540]) ).
tcf(c_38363,plain,
! [X0: $i] : multiply(X0,identity) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_38337,c_2540]) ).
tcf(c_38380,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_38363,c_38337]) ).
tcf(c_38420,plain,
( ~ iPr_def_12
| ( sk_c12 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_37657,c_38380]) ).
tcf(c_38511,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_37786,c_123]) ).
tcf(c_38562,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c8,multiply(sk_c7,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_173,c_38511]) ).
tcf(c_39277,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_37323,c_166]) ).
tcf(c_39287,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c2,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_39277,c_37274]) ).
tcf(c_39310,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_37327,c_146]) ).
tcf(c_39352,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( multiply(sk_c2,multiply(sk_c11,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_39287,c_125]) ).
tcf(c_39424,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c1,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_39310,c_37274]) ).
tcf(c_39517,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_37333,c_168]) ).
tcf(c_39528,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c2,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_39517,c_37274]) ).
tcf(c_39577,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_39424,c_141]) ).
tcf(c_39578,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_39424,c_139]) ).
tcf(c_39579,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_39424,c_137]) ).
tcf(c_39706,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_39528,c_161]) ).
tcf(c_39707,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_39528,c_159]) ).
tcf(c_39711,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(sk_c2,multiply(sk_c11,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_39528,c_125]) ).
tcf(c_40337,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_37367,c_170]) ).
tcf(c_40350,plain,
! [X0: $i] :
( ( sk_c12 = identity )
| ( multiply(sk_c2,multiply(sk_c11,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_40337,c_38511]) ).
tcf(c_40351,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c11) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_40337,c_38380]) ).
tcf(c_40352,plain,
( ( sk_c12 = identity )
| ( multiply(sk_c2,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_40337,c_37274]) ).
tcf(c_40413,plain,
! [X0: $i] :
( ( sk_c12 = identity )
| ( multiply(sk_c2,multiply(sk_c11,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_40352,c_125]) ).
tcf(c_41124,plain,
! [X0: $i] :
( ( sk_c12 = identity )
| ( multiply(inverse(sk_c11),X0) = multiply(sk_c2,X0) ) ),
inference(superposition,[status(thm)],[c_38511,c_40350]) ).
tcf(c_41349,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_37547,c_190]) ).
tcf(c_41367,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c11) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_41349,c_38380]) ).
tcf(c_41368,plain,
( ( sk_c12 = identity )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_41349,c_37274]) ).
tcf(c_41379,plain,
( ( sk_c2 = sk_c3 )
| ( sk_c12 = identity ) ),
inference(superposition,[status(thm)],[c_41367,c_40351]) ).
tcf(c_41393,plain,
( ( sk_c2 = sk_c3 )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_41379,c_38420]) ).
tcf(c_41394,plain,
! [X0: $i] :
( ( sk_c2 = sk_c3 )
| ( multiply(X0,sk_c12) = X0 ) ),
inference(superposition,[status(thm)],[c_41379,c_38337]) ).
tcf(c_41396,plain,
! [X0: $i] :
( ( sk_c2 = sk_c3 )
| ( multiply(sk_c12,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_41379,c_123]) ).
tcf(c_41398,plain,
( ( sk_c2 = sk_c3 )
| ( multiply(sk_c11,sk_c12) = sk_c11 ) ),
inference(instantiation,[status(thm)],[c_41394]) ).
tcf(c_41410,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_41368,c_181]) ).
tcf(c_41411,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_41368,c_179]) ).
tcf(c_41412,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_41368,c_177]) ).
tcf(c_41551,plain,
! [X0: $i,X1: $i] :
( ( sk_c2 = sk_c3 )
| ( multiply(sk_c12,multiply(X0,X1)) = multiply(X0,X1) ) ),
inference(superposition,[status(thm)],[c_41396,c_125]) ).
tcf(c_46877,plain,
( ( sk_c12 = multiply(sk_c2,sk_c11) )
| ( sk_c12 != sk_c12 )
| ( multiply(sk_c2,sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1231]) ).
tcf(c_49744,plain,
( ( sk_c10 = multiply(sk_c4,sk_c12) )
| ( sk_c10 != identity )
| ( multiply(sk_c4,sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_6340]) ).
tcf(c_49745,plain,
( ( multiply(sk_c4,sk_c12) = sk_c10 )
| ( sk_c10 != identity )
| ( multiply(sk_c4,sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_6301]) ).
tcf(c_49750,plain,
( ( multiply(sk_c4,sk_c12) = sk_c11 )
| ( sk_c11 != identity )
| ( multiply(sk_c4,sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_8714]) ).
tcf(c_57333,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(X1) )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_837]) ).
tcf(c_57341,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(inverse(X1)) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_57333]) ).
tcf(c_57350,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),inverse(inverse(X0))) = sk_c12 )
| ( sk_c12 != X1 )
| ( multiply(inverse(X0),inverse(inverse(X0))) != X1 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_57371,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X1)) != inverse(inverse(X0)) )
| ( multiply(inverse(inverse(X0)),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(inverse(X0))) != inverse(X1) )
| ( multiply(inverse(X0),inverse(inverse(X0))) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_57404,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),inverse(inverse(X0))) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),inverse(inverse(X0))) != X1 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_57410,plain,
multiply(inverse(identity),inverse(inverse(identity))) = inverse(inverse(identity)),
inference(instantiation,[status(thm)],[c_2525]) ).
tcf(c_57500,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(inverse(identity)) )
| ( multiply(inverse(inverse(identity)),sk_c11) != sk_c12 )
| ( multiply(X0,inverse(inverse(identity))) != inverse(X0) )
| ( multiply(inverse(identity),inverse(inverse(identity))) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_57371]) ).
tcf(c_57520,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_57626,plain,
! [X0: $i] :
( ( multiply(inverse(identity),inverse(inverse(identity))) = X0 )
| ( X0 != inverse(inverse(identity)) )
| ( multiply(inverse(identity),inverse(inverse(identity))) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_57404]) ).
tcf(c_57721,plain,
! [X0: $i] :
( ( multiply(inverse(inverse(identity)),sk_c11) = sk_c12 )
| ( sk_c12 != X0 )
| ( multiply(inverse(inverse(identity)),sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_835]) ).
tcf(c_57722,plain,
( ( multiply(inverse(inverse(identity)),sk_c11) = sk_c12 )
| ( sk_c12 != sk_c11 )
| ( multiply(inverse(inverse(identity)),sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_57721]) ).
tcf(c_58324,plain,
! [X0: $i] :
( ( inverse(inverse(X0)) = inverse(inverse(identity)) )
| ( inverse(X0) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_57341]) ).
tcf(c_58326,plain,
( ( inverse(inverse(sk_c11)) = inverse(inverse(identity)) )
| ( inverse(sk_c11) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_58324]) ).
tcf(c_58350,plain,
! [X0: $i] :
( ( multiply(inverse(identity),inverse(inverse(identity))) = inverse(X0) )
| ( inverse(X0) != inverse(inverse(identity)) )
| ( multiply(inverse(identity),inverse(inverse(identity))) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_57626]) ).
tcf(c_58363,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(identity),inverse(inverse(identity))) = X1 )
| ( X1 != X0 )
| ( multiply(inverse(identity),inverse(inverse(identity))) != X0 ) ),
inference(instantiation,[status(thm)],[c_57404]) ).
tcf(c_58364,plain,
! [X0: $i] :
( ( multiply(inverse(identity),inverse(inverse(identity))) = sk_c12 )
| ( sk_c12 != X0 )
| ( multiply(inverse(identity),inverse(inverse(identity))) != X0 ) ),
inference(instantiation,[status(thm)],[c_57350]) ).
tcf(c_58365,plain,
( ( multiply(inverse(identity),inverse(inverse(identity))) = sk_c12 )
| ( sk_c12 != sk_c11 )
| ( multiply(inverse(identity),inverse(inverse(identity))) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_58364]) ).
tcf(c_61131,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_837]) ).
tcf(c_61132,plain,
( ( inverse(sk_c11) = inverse(identity) )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_61131]) ).
tcf(c_63426,plain,
! [X0: $i] :
( ( multiply(inverse(identity),inverse(inverse(identity))) = inverse(inverse(X0)) )
| ( inverse(inverse(X0)) != inverse(inverse(identity)) )
| ( multiply(inverse(identity),inverse(inverse(identity))) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_58350]) ).
tcf(c_63427,plain,
( ( multiply(inverse(identity),inverse(inverse(identity))) = inverse(inverse(sk_c11)) )
| ( inverse(inverse(sk_c11)) != inverse(inverse(identity)) )
| ( multiply(inverse(identity),inverse(inverse(identity))) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_63426]) ).
tcf(c_66508,plain,
( ~ iPr_def_13
| ( inverse(inverse(inverse(identity))) != inverse(inverse(identity)) )
| ( multiply(inverse(inverse(identity)),sk_c11) != sk_c12 )
| ( multiply(inverse(identity),inverse(inverse(identity))) != sk_c12 )
| ( multiply(inverse(identity),inverse(inverse(identity))) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_57500]) ).
tcf(c_70500,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(inverse(X0)) )
| ( X2 != X1 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_57520]) ).
tcf(c_70504,plain,
( ( sk_c11 = inverse(inverse(sk_c11)) )
| ( sk_c11 != sk_c11 )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_70500]) ).
tcf(c_73416,plain,
( ( inverse(inverse(inverse(identity))) = inverse(inverse(identity)) )
| ( inverse(inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_58324]) ).
tcf(c_77681,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(identity),inverse(inverse(identity))) = X1 )
| ( X1 != inverse(inverse(X0)) )
| ( multiply(inverse(identity),inverse(inverse(identity))) != inverse(inverse(X0)) ) ),
inference(instantiation,[status(thm)],[c_58363]) ).
tcf(c_77685,plain,
( ( multiply(inverse(identity),inverse(inverse(identity))) = sk_c11 )
| ( sk_c11 != inverse(inverse(sk_c11)) )
| ( multiply(inverse(identity),inverse(inverse(identity))) != inverse(inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_77681]) ).
tcf(c_86447,plain,
inverse(sk_c2) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_38562,c_198,c_169,c_840,c_1194,c_1195,c_1207,c_2219,c_5188,c_6381,c_6504,c_6839,c_6843,c_7081,c_7983,c_13429,c_16257,c_19233,c_21388,c_22273,c_22518,c_24970,c_26471,c_27910,c_30003,c_33764,c_35595,c_40337,c_49745,c_57410,c_57722,c_58326,c_58365,c_61132,c_63427,c_66508,c_70504,c_73416,c_77685]) ).
tcf(c_86459,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_2519,c_86447]) ).
tcf(c_86460,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_2518,c_86447]) ).
tcf(c_86461,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_2517,c_86447]) ).
tcf(c_86505,plain,
multiply(sk_c11,sk_c2) = identity,
inference(superposition,[status(thm)],[c_86447,c_124]) ).
tcf(c_86565,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_86505,c_125]) ).
tcf(c_86586,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_86565,c_123]) ).
tcf(c_86820,plain,
inverse(sk_c4) = sk_c12,
inference(global_subsumption_just,[status(thm)],[c_86459,c_840,c_5418,c_7983,c_19233,c_21388,c_22518,c_39579,c_41412,c_57410,c_57722,c_58326,c_58365,c_61132,c_63427,c_66508,c_70504,c_73416,c_77685]) ).
tcf(c_86835,plain,
multiply(sk_c4,sk_c12) = identity,
inference(superposition,[status(thm)],[c_86820,c_37274]) ).
tcf(c_86882,plain,
inverse(sk_c5) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_86460,c_198,c_840,c_2219,c_5311,c_6381,c_7081,c_7983,c_13429,c_16257,c_19233,c_21388,c_22273,c_22518,c_27910,c_30003,c_33764,c_35595,c_39578,c_39707,c_41411,c_49745,c_57410,c_57722,c_58326,c_58365,c_61132,c_63427,c_66508,c_70504,c_73416,c_77685,c_86835]) ).
tcf(c_86900,plain,
inverse(sk_c11) = sk_c5,
inference(superposition,[status(thm)],[c_86882,c_38380]) ).
tcf(c_86950,plain,
inverse(sk_c6) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_86461,c_198,c_840,c_2219,c_5307,c_6381,c_7081,c_7983,c_13429,c_16257,c_19233,c_21388,c_22273,c_22518,c_27910,c_30003,c_33764,c_35595,c_39577,c_39706,c_41410,c_49745,c_57410,c_57722,c_58326,c_58365,c_61132,c_63427,c_66508,c_70504,c_73416,c_77685,c_86835]) ).
tcf(c_86965,plain,
multiply(sk_c6,sk_c9) = identity,
inference(superposition,[status(thm)],[c_86950,c_37274]) ).
tcf(c_86978,plain,
! [X0: $i] : multiply(inverse(sk_c11),X0) = multiply(sk_c2,X0),
inference(global_subsumption_just,[status(thm)],[c_41124,c_198,c_840,c_1188,c_1209,c_1256,c_1257,c_1624,c_1922,c_2219,c_6381,c_6595,c_6893,c_7081,c_7983,c_13429,c_16200,c_16257,c_18694,c_19233,c_19231,c_21388,c_21389,c_22273,c_22518,c_26471,c_27910,c_30003,c_33764,c_35595,c_49745,c_57410,c_57722,c_58326,c_58365,c_61132,c_63427,c_66508,c_70504,c_73416,c_77685,c_86835]) ).
tcf(c_86981,plain,
! [X0: $i] : multiply(sk_c5,X0) = multiply(sk_c2,X0),
inference(light_normalisation,[status(thm)],[c_86978,c_86900]) ).
tcf(c_86983,plain,
multiply(sk_c2,sk_c11) = sk_c10,
inference(demodulation,[status(thm)],[c_158,c_86981]) ).
tcf(c_87038,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c11,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_86983,c_125]) ).
tcf(c_87039,plain,
( ~ iPr_def_12
| ( sk_c12 != sk_c10 )
| ( inverse(sk_c2) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_86983,c_831]) ).
tcf(c_87043,plain,
( ~ iPr_def_12
| ( sk_c12 != sk_c10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_87039,c_86447]) ).
tcf(c_87092,plain,
multiply(sk_c10,identity) = multiply(sk_c2,sk_c11),
inference(superposition,[status(thm)],[c_38337,c_87038]) ).
tcf(c_87312,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c11,X0)) = multiply(identity,X0),
inference(global_subsumption_just,[status(thm)],[c_39352,c_198,c_840,c_1188,c_1209,c_1256,c_1257,c_1624,c_1922,c_2219,c_6381,c_7081,c_7983,c_13429,c_16200,c_16257,c_19233,c_19231,c_21388,c_21389,c_22273,c_22518,c_26471,c_27910,c_30003,c_33764,c_35595,c_39352,c_39711,c_40413,c_49745,c_57410,c_57722,c_58326,c_58365,c_61132,c_63427,c_66508,c_70504,c_73416,c_77685,c_86835]) ).
tcf(c_87315,plain,
! [X0: $i] : multiply(sk_c10,X0) = X0,
inference(light_normalisation,[status(thm)],[c_87312,c_123,c_87038]) ).
tcf(c_87328,plain,
sk_c10 = identity,
inference(superposition,[status(thm)],[c_87315,c_38337]) ).
tcf(c_87514,plain,
sk_c2 = sk_c3,
inference(global_subsumption_just,[status(thm)],[c_41551,c_198,c_169,c_840,c_833,c_2219,c_3169,c_3555,c_3545,c_3541,c_6341,c_6366,c_6381,c_7081,c_7983,c_8117,c_13092,c_13429,c_16257,c_18367,c_19233,c_21388,c_22273,c_22518,c_26459,c_27910,c_30003,c_33764,c_35595,c_41393,c_41398,c_49750,c_49745,c_49744,c_57410,c_57722,c_58326,c_58365,c_61132,c_63427,c_66508,c_70504,c_73416,c_77685,c_86835,c_87328]) ).
tcf(c_87522,plain,
( ( multiply(sk_c2,sk_c11) = sk_c12 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_180,c_87514]) ).
tcf(c_87541,plain,
( ( sk_c12 = sk_c10 )
| ( multiply(sk_c10,sk_c10) = sk_c12 ) ),
inference(light_normalisation,[status(thm)],[c_87522,c_86965,c_87092,c_87328]) ).
tcf(c_87542,plain,
sk_c12 = sk_c10,
inference(demodulation,[status(thm)],[c_87541,c_87315]) ).
tcf(c_87553,plain,
! [X0: $i] : multiply(sk_c12,X0) = X0,
inference(demodulation,[status(thm)],[c_87315,c_87542]) ).
tcf(c_87556,plain,
multiply(sk_c2,sk_c11) = sk_c12,
inference(demodulation,[status(thm)],[c_86983,c_87542]) ).
tcf(c_87558,plain,
( iPr_def_13
| iPr_def_12
| ( multiply(sk_c11,sk_c12) != sk_c12 ) ),
inference(demodulation,[status(thm)],[c_37624,c_87542]) ).
tcf(c_87559,plain,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( multiply(sk_c11,sk_c12) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_135,c_87542]) ).
tcf(c_87562,plain,
~ iPr_def_12,
inference(backward_subsumption_resolution,[status(thm)],[c_87043,c_87542]) ).
tcf(c_87563,plain,
( iPr_def_13
| ( multiply(sk_c11,sk_c12) != sk_c12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_87558,c_87562]) ).
tcf(c_87569,plain,
multiply(sk_c11,sk_c12) = sk_c12,
inference(global_subsumption_just,[status(thm)],[c_87559,c_1209,c_1213,c_1256,c_1257,c_1930,c_1931,c_2219,c_3162,c_3777,c_4000,c_4843,c_6381,c_12549,c_27905,c_35595,c_46877,c_86835,c_86983,c_87556]) ).
tcf(c_87591,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c12,X0)) = multiply(sk_c12,X0),
inference(superposition,[status(thm)],[c_87569,c_125]) ).
tcf(c_87598,plain,
! [X0: $i] : multiply(sk_c11,X0) = X0,
inference(light_normalisation,[status(thm)],[c_87591,c_87553]) ).
tcf(c_87603,plain,
! [X0: $i] : multiply(sk_c2,X0) = X0,
inference(demodulation,[status(thm)],[c_86586,c_87598]) ).
tcf(c_87605,plain,
multiply(sk_c2,sk_c11) = sk_c11,
inference(instantiation,[status(thm)],[c_87603]) ).
tcf(c_87606,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_87605,c_87569,c_87563,c_87556,c_87328,c_86983,c_86835,c_77685,c_73416,c_70504,c_66508,c_63427,c_61132,c_58365,c_58326,c_57722,c_57410,c_49745,c_46877,c_35595,c_30003,c_27910,c_27905,c_22518,c_19233,c_16881,c_7983,c_6381,c_5162,c_3162,c_2219,c_1213,c_1209,c_840]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP312-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.13/0.38 % Computer : n017.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Wed Sep 23 14:21:16 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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.13/0.43
% 0.13/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.43
% 0.13/0.43 % Detected problem language: tptp
% 0.13/0.44 % Proving...
% 44.46/9.34 % SZS status Started for theBenchmark.p
% 44.46/9.34 % SZS status Unsatisfiable for theBenchmark.p
% 44.46/9.34
% 44.46/9.34 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 44.46/9.34
% 44.46/9.34 % ------ iProver source info
% 44.46/9.34
% 44.46/9.34 % git: date: 2026-07-19 20:42:38 +0200
% 44.46/9.34 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 44.46/9.34 % git: non_committed_changes: false
% 44.46/9.34
% 44.46/9.34 % ------ Parsing...% successful
% 44.46/9.34
% 44.46/9.34
% 44.46/9.34 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 44.46/9.34
% 44.46/9.34 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 44.46/9.34
% 44.46/9.34 % ------ Preprocessing... gs_s sp: 6 0s gs_e snvd_s sp: 0 0s snvd_e %
% 44.46/9.34
% 44.46/9.34 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 44.46/9.34 % ------ Proving...
% 44.46/9.34 % ------ Problem Properties
% 44.46/9.34
% 44.46/9.34 %
% 44.46/9.34 % clauses 78
% 44.46/9.34 % conjectures 75
% 44.46/9.34 % EPR 0
% 44.46/9.34 % Horn 7
% 44.46/9.34 % unary 3
% 44.46/9.34 % binary 70
% 44.46/9.34 % lits 162
% 44.46/9.34 % lits eq 154
% 44.46/9.34 % fd_pure 0
% 44.46/9.34 % fd_pseudo 0
% 44.46/9.34 % fd_cond 0
% 44.46/9.34 % fd_pseudo_cond 0
% 44.46/9.34 % AC symbols 0
% 44.46/9.34
% 44.46/9.34 % ------ Input Options Time Limit: Unbounded
% 44.46/9.34
% 44.46/9.34
% 44.46/9.34 % ------
% 44.46/9.34 % Current options:
% 44.46/9.34 % ------
% 44.46/9.34
% 44.46/9.34
% 44.46/9.34 %
% 44.46/9.34
% 44.46/9.34 % ------ Proving...
% 44.46/9.34 %
% 44.46/9.34
% 44.46/9.34 % SZS status Unsatisfiable for theBenchmark.p
% 44.46/9.34
% 44.46/9.34 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 44.46/9.34
% 44.46/9.34
%------------------------------------------------------------------------------