%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP259-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 : n007.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:37 PM UTC 2026
% Result : Unsatisfiable 16.08s 3.27s
% Output : CNFRefutation 16.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 51
% Syntax : Number of formulae : 568 ( 111 unt; 12 def)
% Number of atoms : 2280 (1140 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 1071 ( 375 ~; 696 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 17 usr; 18 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 143 ( 0 sgn 143 !; 0 ?; 127 :)
% 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(f6,negated_conjecture,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f7,plain,
( sk_c8 = inverse(sk_c4)
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f6]) ).
fof(f8,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f9,plain,
( sk_c8 = multiply(sk_c4,sk_c7)
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f8]) ).
fof(f10,negated_conjecture,
( inverse(sk_c5) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c7 = inverse(sk_c5)
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c7 = multiply(sk_c5,sk_c6)
| multiply(sk_c1,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f12]) ).
fof(f16,negated_conjecture,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f17,plain,
( sk_c8 = inverse(sk_c4)
| sk_c8 = inverse(sk_c1) ),
inference(reorient_equations,[],[f16]) ).
fof(f18,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,plain,
( sk_c8 = multiply(sk_c4,sk_c7)
| sk_c8 = inverse(sk_c1) ),
inference(reorient_equations,[],[f18]) ).
fof(f20,negated_conjecture,
( inverse(sk_c5) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f21,plain,
( sk_c7 = inverse(sk_c5)
| sk_c8 = inverse(sk_c1) ),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f23,plain,
( sk_c7 = multiply(sk_c5,sk_c6)
| sk_c8 = inverse(sk_c1) ),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| sk_c6 = multiply(sk_c2,sk_c7) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( inverse(sk_c4) = sk_c8
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c8 = inverse(sk_c4)
| sk_c6 = multiply(sk_c2,sk_c7) ),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f29,plain,
( sk_c8 = multiply(sk_c4,sk_c7)
| sk_c6 = multiply(sk_c2,sk_c7) ),
inference(reorient_equations,[],[f28]) ).
fof(f30,negated_conjecture,
( inverse(sk_c5) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f31,plain,
( sk_c7 = inverse(sk_c5)
| sk_c6 = multiply(sk_c2,sk_c7) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c7 = multiply(sk_c5,sk_c6)
| sk_c6 = multiply(sk_c2,sk_c7) ),
inference(reorient_equations,[],[f32]) ).
fof(f34,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c2) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f35,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| sk_c7 = inverse(sk_c2) ),
inference(reorient_equations,[],[f34]) ).
fof(f36,negated_conjecture,
( inverse(sk_c4) = sk_c8
| inverse(sk_c2) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f37,plain,
( sk_c8 = inverse(sk_c4)
| sk_c7 = inverse(sk_c2) ),
inference(reorient_equations,[],[f36]) ).
fof(f38,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f39,plain,
( sk_c8 = multiply(sk_c4,sk_c7)
| sk_c7 = inverse(sk_c2) ),
inference(reorient_equations,[],[f38]) ).
fof(f40,negated_conjecture,
( inverse(sk_c5) = sk_c7
| inverse(sk_c2) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f41,plain,
( sk_c7 = inverse(sk_c5)
| sk_c7 = inverse(sk_c2) ),
inference(reorient_equations,[],[f40]) ).
fof(f42,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f43,plain,
( sk_c7 = multiply(sk_c5,sk_c6)
| sk_c7 = inverse(sk_c2) ),
inference(reorient_equations,[],[f42]) ).
fof(f44,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c6,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f45,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| sk_c7 = multiply(sk_c6,sk_c8) ),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
( inverse(sk_c4) = sk_c8
| multiply(sk_c6,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f47,plain,
( sk_c8 = inverse(sk_c4)
| sk_c7 = multiply(sk_c6,sk_c8) ),
inference(reorient_equations,[],[f46]) ).
fof(f48,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c6,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f49,plain,
( sk_c8 = multiply(sk_c4,sk_c7)
| sk_c7 = multiply(sk_c6,sk_c8) ),
inference(reorient_equations,[],[f48]) ).
fof(f50,negated_conjecture,
( inverse(sk_c5) = sk_c7
| multiply(sk_c6,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f51,plain,
( sk_c7 = inverse(sk_c5)
| sk_c7 = multiply(sk_c6,sk_c8) ),
inference(reorient_equations,[],[f50]) ).
fof(f52,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c6,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f53,plain,
( sk_c7 = multiply(sk_c5,sk_c6)
| sk_c7 = multiply(sk_c6,sk_c8) ),
inference(reorient_equations,[],[f52]) ).
fof(f56,negated_conjecture,
( inverse(sk_c4) = sk_c8
| multiply(sk_c3,sk_c6) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f57,plain,
( sk_c8 = inverse(sk_c4)
| sk_c8 = multiply(sk_c3,sk_c6) ),
inference(reorient_equations,[],[f56]) ).
fof(f58,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c3,sk_c6) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f59,plain,
( sk_c8 = multiply(sk_c4,sk_c7)
| sk_c8 = multiply(sk_c3,sk_c6) ),
inference(reorient_equations,[],[f58]) ).
fof(f60,negated_conjecture,
( inverse(sk_c5) = sk_c7
| multiply(sk_c3,sk_c6) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f61,plain,
( sk_c7 = inverse(sk_c5)
| sk_c8 = multiply(sk_c3,sk_c6) ),
inference(reorient_equations,[],[f60]) ).
fof(f62,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c3,sk_c6) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_30) ).
fof(f63,plain,
( sk_c7 = multiply(sk_c5,sk_c6)
| sk_c8 = multiply(sk_c3,sk_c6) ),
inference(reorient_equations,[],[f62]) ).
fof(f64,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c3) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f65,plain,
( multiply(sk_c7,sk_c8) = sk_c6
| sk_c6 = inverse(sk_c3) ),
inference(reorient_equations,[],[f64]) ).
fof(f66,negated_conjecture,
( inverse(sk_c4) = sk_c8
| inverse(sk_c3) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f67,plain,
( sk_c8 = inverse(sk_c4)
| sk_c6 = inverse(sk_c3) ),
inference(reorient_equations,[],[f66]) ).
fof(f68,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c3) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f69,plain,
( sk_c8 = multiply(sk_c4,sk_c7)
| sk_c6 = inverse(sk_c3) ),
inference(reorient_equations,[],[f68]) ).
fof(f70,negated_conjecture,
( inverse(sk_c5) = sk_c7
| inverse(sk_c3) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f71,plain,
( sk_c7 = inverse(sk_c5)
| sk_c6 = inverse(sk_c3) ),
inference(reorient_equations,[],[f70]) ).
fof(f72,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c3) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f73,plain,
( sk_c7 = multiply(sk_c5,sk_c6)
| sk_c6 = inverse(sk_c3) ),
inference(reorient_equations,[],[f72]) ).
fof(f74,negated_conjecture,
! [X2,X3,X0,X1,X4] :
( multiply(X4,sk_c6) != sk_c7
| inverse(X4) != sk_c7
| multiply(X3,sk_c7) != sk_c8
| inverse(X3) != sk_c8
| multiply(sk_c7,sk_c8) != sk_c6
| inverse(X2) != sk_c6
| multiply(X2,sk_c6) != sk_c8
| multiply(sk_c6,sk_c8) != sk_c7
| inverse(X1) != sk_c7
| multiply(X1,sk_c7) != sk_c6
| inverse(X0) != sk_c8
| multiply(X0,sk_c8) != sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f75,plain,
! [X2,X3,X0,X1,X4] :
( sk_c7 != multiply(X4,sk_c6)
| sk_c7 != inverse(X4)
| sk_c8 != multiply(X3,sk_c7)
| sk_c8 != inverse(X3)
| multiply(sk_c7,sk_c8) != sk_c6
| sk_c6 != inverse(X2)
| sk_c8 != multiply(X2,sk_c6)
| sk_c7 != multiply(sk_c6,sk_c8)
| sk_c7 != inverse(X1)
| sk_c6 != multiply(X1,sk_c7)
| inverse(X0) != sk_c8
| sk_c7 != multiply(X0,sk_c8) ),
inference(reorient_equations,[],[f74]) ).
tcf(c_88,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_89,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_92,negated_conjecture,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_93,negated_conjecture,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_94,negated_conjecture,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_95,negated_conjecture,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_97,negated_conjecture,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_98,negated_conjecture,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_99,negated_conjecture,
( ( inverse(sk_c5) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_100,negated_conjecture,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_101,negated_conjecture,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_102,negated_conjecture,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_103,negated_conjecture,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_104,negated_conjecture,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_105,negated_conjecture,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c5) = sk_c7 ) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_111,negated_conjecture,
( ( multiply(sk_c6,sk_c8) = sk_c7 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_112,negated_conjecture,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_113,negated_conjecture,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_115,negated_conjecture,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c3,sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_118,negated_conjecture,
( ( multiply(sk_c3,sk_c6) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c3,sk_c6) = sk_c8 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c3) = sk_c6 )
| ( inverse(sk_c4) = sk_c8 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c3) = sk_c6 )
| ( inverse(sk_c5) = sk_c7 ) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_126,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(X4) != sk_c7 )
| ( inverse(X3) != sk_c7 )
| ( inverse(X2) != sk_c6 )
| ( inverse(X1) != sk_c8 )
| ( inverse(X0) != sk_c8 )
| ( multiply(sk_c6,sk_c8) != sk_c7 )
| ( multiply(sk_c7,sk_c8) != sk_c6 )
| ( multiply(X4,sk_c7) != sk_c6 )
| ( multiply(X3,sk_c6) != sk_c7 )
| ( multiply(X2,sk_c6) != sk_c8 )
| ( multiply(X1,sk_c7) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c7 ) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_467,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_126]) ).
tcf(c_468,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_126]) ).
tcf(c_469,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c7) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_126]) ).
tcf(c_470,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != sk_c6 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_126]) ).
tcf(c_471,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_126]) ).
tcf(c_472,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c6,sk_c8) != sk_c7 )
| ( multiply(sk_c7,sk_c8) != sk_c6 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_126]) ).
tcf(c_473,definition,
iPr_def_15 = multiply(sk_c7,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_474,definition,
iPr_def_16 = multiply(sk_c6,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_475,definition,
iPr_def_17 = multiply(sk_c5,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_476,definition,
iPr_def_18 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_477,definition,
iPr_def_19 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_478,definition,
iPr_def_20 = multiply(sk_c4,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_479,definition,
iPr_def_21 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_480,definition,
iPr_def_22 = multiply(sk_c3,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_481,definition,
iPr_def_23 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_482,definition,
iPr_def_24 = multiply(sk_c2,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_483,definition,
iPr_def_25 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_484,definition,
iPr_def_26 = multiply(sk_c1,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_485,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_16 != sk_c7 )
| ( iPr_def_15 != sk_c6 ) ),
inference(demodulation,[status(thm)],[c_472,c_474,c_473]) ).
tcf(c_486,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_471]) ).
tcf(c_487,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm)],[c_470]) ).
tcf(c_488,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c7) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_469]) ).
tcf(c_489,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_468]) ).
tcf(c_490,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_467]) ).
tcf(c_491,negated_conjecture,
( ( iPr_def_18 = sk_c6 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_125,c_476,c_475]) ).
tcf(c_492,negated_conjecture,
( ( iPr_def_19 = sk_c7 )
| ( iPr_def_18 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_124,c_477]) ).
tcf(c_493,negated_conjecture,
( ( iPr_def_20 = sk_c8 )
| ( iPr_def_18 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_123,c_478]) ).
tcf(c_494,negated_conjecture,
( ( iPr_def_21 = sk_c8 )
| ( iPr_def_18 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_122,c_479]) ).
tcf(c_495,negated_conjecture,
( ( iPr_def_18 = sk_c6 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_496,negated_conjecture,
( ( iPr_def_22 = sk_c8 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_120,c_480]) ).
tcf(c_497,negated_conjecture,
( ( iPr_def_22 = sk_c8 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_498,negated_conjecture,
( ( iPr_def_22 = sk_c8 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_118]) ).
tcf(c_499,negated_conjecture,
( ( iPr_def_22 = sk_c8 )
| ( iPr_def_21 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_501,negated_conjecture,
( ( iPr_def_17 = sk_c7 )
| ( iPr_def_16 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_115]) ).
tcf(c_502,negated_conjecture,
( ( iPr_def_19 = sk_c7 )
| ( iPr_def_16 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_503,negated_conjecture,
( ( iPr_def_20 = sk_c8 )
| ( iPr_def_16 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_504,negated_conjecture,
( ( iPr_def_21 = sk_c8 )
| ( iPr_def_16 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_505,negated_conjecture,
( ( iPr_def_16 = sk_c7 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_111]) ).
tcf(c_506,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_110,c_481]) ).
tcf(c_507,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_508,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_509,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_21 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_510,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_511,negated_conjecture,
( ( iPr_def_24 = sk_c6 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_105,c_482]) ).
tcf(c_512,negated_conjecture,
( ( iPr_def_24 = sk_c6 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_104]) ).
tcf(c_513,negated_conjecture,
( ( iPr_def_24 = sk_c6 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_103]) ).
tcf(c_514,negated_conjecture,
( ( iPr_def_24 = sk_c6 )
| ( iPr_def_21 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_102]) ).
tcf(c_515,negated_conjecture,
( ( iPr_def_24 = sk_c6 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_101]) ).
tcf(c_516,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_100,c_483]) ).
tcf(c_517,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_99]) ).
tcf(c_518,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_98]) ).
tcf(c_519,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_21 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_97]) ).
tcf(c_521,negated_conjecture,
( ( iPr_def_26 = sk_c7 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_95,c_484]) ).
tcf(c_522,negated_conjecture,
( ( iPr_def_26 = sk_c7 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_94]) ).
tcf(c_523,negated_conjecture,
( ( iPr_def_26 = sk_c7 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_93]) ).
tcf(c_524,negated_conjecture,
( ( iPr_def_26 = sk_c7 )
| ( iPr_def_21 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_92]) ).
tcf(c_526,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_527,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_529,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_532,plain,
sk_c7 = sk_c7,
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_800,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(sk_c7,iPr_def_22) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_498,c_473]) ).
tcf(c_810,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(iPr_def_18,sk_c8) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_494,c_474]) ).
tcf(c_811,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(iPr_def_18,sk_c8) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_493,c_474]) ).
tcf(c_812,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_18,sk_c8) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_492,c_474]) ).
tcf(c_813,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_18,sk_c8) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_491,c_474]) ).
tcf(c_834,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(sk_c5,iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_494,c_475]) ).
tcf(c_835,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(sk_c5,iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_493,c_475]) ).
tcf(c_836,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c5,iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_492,c_475]) ).
tcf(c_837,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c5,iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_491,c_475]) ).
tcf(c_904,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( sk_c7 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_501,c_502]) ).
tcf(c_950,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( sk_c7 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_504,c_503]) ).
tcf(c_1027,plain,
! [X0: $i] :
( ( iPr_def_16 = sk_c7 )
| ( iPr_def_16 != X0 )
| ( sk_c7 != X0 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_1028,plain,
( ( iPr_def_16 = sk_c7 )
| ( iPr_def_16 != iPr_def_16 )
| ( sk_c7 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1027]) ).
tcf(c_1029,plain,
iPr_def_16 = iPr_def_16,
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_1030,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_1032,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_506,c_478]) ).
tcf(c_1033,plain,
( ( sk_c7 = iPr_def_16 )
| ( multiply(sk_c4,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_502,c_478]) ).
tcf(c_1034,plain,
( ( sk_c7 = iPr_def_16 )
| ( multiply(sk_c4,iPr_def_17) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_501,c_478]) ).
tcf(c_1044,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(sk_c3,iPr_def_18) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_494,c_480]) ).
tcf(c_1045,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(sk_c3,iPr_def_18) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_493,c_480]) ).
tcf(c_1046,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c3,iPr_def_18) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_492,c_480]) ).
tcf(c_1047,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c3,iPr_def_18) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_491,c_480]) ).
tcf(c_1065,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_1068,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_1070,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_506,c_482]) ).
tcf(c_1083,plain,
( ( sk_c7 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_503,c_484]) ).
tcf(c_1104,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1068]) ).
tcf(c_1108,plain,
sk_c6 = sk_c6,
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_1110,plain,
! [X0: $i,X1: $i] :
( ( sk_c6 = X0 )
| ( sk_c6 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_1111,plain,
multiply(iPr_def_21,sk_c4) = identity,
inference(superposition,[status(thm)],[c_479,c_89]) ).
tcf(c_1112,plain,
multiply(iPr_def_19,sk_c5) = identity,
inference(superposition,[status(thm)],[c_477,c_89]) ).
tcf(c_1113,plain,
multiply(iPr_def_25,sk_c1) = identity,
inference(superposition,[status(thm)],[c_483,c_89]) ).
tcf(c_1114,plain,
multiply(iPr_def_23,sk_c2) = identity,
inference(superposition,[status(thm)],[c_481,c_89]) ).
tcf(c_1115,plain,
multiply(iPr_def_18,sk_c3) = identity,
inference(superposition,[status(thm)],[c_476,c_89]) ).
tcf(c_1121,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_1130,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_23 )
| ( iPr_def_23 != inverse(sk_c2) )
| ( inverse(X0) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1104]) ).
tcf(c_1135,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_16 = inverse(X0) )
| ( iPr_def_16 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1030]) ).
tcf(c_1145,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_507,c_482]) ).
tcf(c_1171,plain,
( ( sk_c7 = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_508,c_484]) ).
tcf(c_1214,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( sk_c7 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_509,c_508]) ).
tcf(c_1250,plain,
! [X0: $i] :
( ( sk_c6 = X0 )
| ( sk_c6 != sk_c6 )
| ( X0 != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_1110]) ).
tcf(c_1302,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_23 )
| ( inverse(X0) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1068]) ).
tcf(c_1323,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_511,c_480]) ).
tcf(c_1372,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_23 )
| ( inverse(X0) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1121]) ).
tcf(c_1376,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1121]) ).
tcf(c_1391,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_512,c_480]) ).
tcf(c_1434,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_513,c_480]) ).
tcf(c_1438,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_513,c_474]) ).
tcf(c_1441,plain,
( ( iPr_def_18 = iPr_def_24 )
| ( sk_c8 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_513,c_493]) ).
tcf(c_1511,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_514,c_480]) ).
tcf(c_1515,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_514,c_474]) ).
tcf(c_1517,plain,
( ( iPr_def_18 = iPr_def_24 )
| ( sk_c8 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_514,c_494]) ).
tcf(c_1546,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_21 )
| ( iPr_def_21 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_1596,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_23 )
| ( iPr_def_23 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_1598,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_16 )
| ( iPr_def_16 != iPr_def_23 )
| ( inverse(X0) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1302]) ).
tcf(c_1599,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_23 )
| ( iPr_def_23 != X0 )
| ( iPr_def_16 != X0 ) ),
inference(instantiation,[status(thm)],[c_1030]) ).
tcf(c_1601,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( iPr_def_23 != sk_c7 )
| ( iPr_def_16 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1599]) ).
tcf(c_1616,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_516,c_484]) ).
tcf(c_1624,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_516,c_496]) ).
tcf(c_1672,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_517,c_484]) ).
tcf(c_1679,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c7 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_517,c_497]) ).
tcf(c_1731,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_518,c_484]) ).
tcf(c_1737,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c8 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_518,c_498]) ).
tcf(c_1788,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_519,c_484]) ).
tcf(c_1791,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c8 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_519,c_499]) ).
tcf(c_1962,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c2) )
| ( X0 != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_529]) ).
tcf(c_1963,plain,
( ( inverse(sk_c7) = inverse(sk_c2) )
| ( sk_c7 != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_1962]) ).
tcf(c_1964,plain,
( ( inverse(sk_c2) = iPr_def_23 )
| ( iPr_def_23 != inverse(sk_c2) )
| ( inverse(sk_c2) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1130]) ).
tcf(c_1965,plain,
inverse(sk_c2) = inverse(sk_c2),
inference(instantiation,[status(thm)],[c_1065]) ).
tcf(c_1977,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c2,iPr_def_26) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_521,c_482]) ).
tcf(c_1979,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_521,c_506]) ).
tcf(c_2017,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c7 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_522,c_507]) ).
tcf(c_2018,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_26) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_522,c_482]) ).
tcf(c_2042,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c6 )
| ( sk_c6 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_2068,plain,
( ( sk_c7 = iPr_def_26 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_523,c_484]) ).
tcf(c_2124,plain,
iPr_def_21 = iPr_def_21,
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_2167,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( sk_c7 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_524,c_523]) ).
tcf(c_2173,plain,
( ( sk_c7 = iPr_def_26 )
| ( multiply(sk_c1,iPr_def_21) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_524,c_484]) ).
tcf(c_2395,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c6 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_18 )
| ( sk_c7 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_495,c_485]) ).
tcf(c_2397,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c8 = iPr_def_20 )
| ( iPr_def_15 != iPr_def_18 )
| ( sk_c7 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_493,c_485]) ).
tcf(c_2559,plain,
( ~ iPr_def_14
| ( sk_c7 != iPr_def_26 )
| ( inverse(sk_c1) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_484,c_486]) ).
tcf(c_2563,plain,
( ~ iPr_def_14
| ( sk_c7 != identity )
| ( inverse(inverse(sk_c8)) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_89,c_486]) ).
tcf(c_2587,plain,
( ~ iPr_def_14
| ( sk_c7 != iPr_def_26 )
| ( sk_c8 != iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_2559,c_483]) ).
tcf(c_2734,plain,
( ~ iPr_def_13
| ( sk_c6 != iPr_def_24 )
| ( inverse(sk_c2) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_482,c_487]) ).
tcf(c_2746,plain,
( ~ iPr_def_13
| ( sk_c6 != iPr_def_24 )
| ( sk_c7 != iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_2734,c_481]) ).
tcf(c_2820,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_21 = X0 )
| ( iPr_def_21 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_2829,plain,
( ~ iPr_def_12
| ( sk_c8 != iPr_def_20 )
| ( inverse(sk_c4) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_478,c_488]) ).
tcf(c_2830,plain,
( ~ iPr_def_12
| ( sk_c8 != iPr_def_24 )
| ( inverse(sk_c2) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_482,c_488]) ).
tcf(c_2831,plain,
( ~ iPr_def_12
| ( sk_c8 != sk_c7 )
| ( inverse(identity) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_88,c_488]) ).
tcf(c_2842,plain,
( ~ iPr_def_12
| ( sk_c8 != iPr_def_24 )
| ( sk_c8 != iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_2830,c_481]) ).
tcf(c_2846,plain,
( ~ iPr_def_12
| ( sk_c8 != iPr_def_21 )
| ( sk_c8 != iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_2829,c_479]) ).
tcf(c_2887,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( iPr_def_23 != inverse(sk_c2) )
| ( iPr_def_16 != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1599]) ).
tcf(c_2903,plain,
( ~ iPr_def_11
| ( sk_c7 != iPr_def_17 )
| ( inverse(sk_c5) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_475,c_489]) ).
tcf(c_2905,plain,
( ~ iPr_def_11
| ( sk_c7 != sk_c6 )
| ( inverse(identity) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_88,c_489]) ).
tcf(c_2910,plain,
! [X0: $i] :
( ( sk_c8 = iPr_def_21 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,iPr_def_24) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_514,c_489]) ).
tcf(c_2911,plain,
! [X0: $i] :
( ( sk_c8 = iPr_def_20 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,iPr_def_24) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_513,c_489]) ).
tcf(c_2912,plain,
! [X0: $i] :
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,iPr_def_24) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_512,c_489]) ).
tcf(c_2913,plain,
! [X0: $i] :
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,iPr_def_24) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_511,c_489]) ).
tcf(c_2929,plain,
( ~ iPr_def_11
| ( sk_c7 != iPr_def_19 )
| ( sk_c7 != iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_2903,c_477]) ).
tcf(c_3004,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_11
| ( inverse(sk_c7) != sk_c7 )
| ( multiply(sk_c7,iPr_def_24) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_2913]) ).
tcf(c_3005,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_11
| ( inverse(sk_c7) != sk_c7 )
| ( multiply(sk_c7,iPr_def_24) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_2912]) ).
tcf(c_3006,plain,
( ( sk_c8 = iPr_def_20 )
| ~ iPr_def_11
| ( inverse(sk_c7) != sk_c7 )
| ( multiply(sk_c7,iPr_def_24) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_2911]) ).
tcf(c_3007,plain,
( ( sk_c8 = iPr_def_21 )
| ~ iPr_def_11
| ( inverse(sk_c7) != sk_c7 )
| ( multiply(sk_c7,iPr_def_24) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_2910]) ).
tcf(c_3120,plain,
! [X0: $i] :
( ( X0 = iPr_def_21 )
| ( iPr_def_21 != sk_c8 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1546]) ).
tcf(c_3123,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c8,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_473,c_90]) ).
tcf(c_3124,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c7,X0)) = multiply(iPr_def_20,X0),
inference(superposition,[status(thm)],[c_478,c_90]) ).
tcf(c_3125,plain,
! [X0: $i] : multiply(sk_c5,multiply(sk_c6,X0)) = multiply(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_475,c_90]) ).
tcf(c_3127,plain,
! [X0: $i] : multiply(sk_c6,multiply(sk_c8,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_474,c_90]) ).
tcf(c_3128,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c6,X0)) = multiply(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_480,c_90]) ).
tcf(c_3130,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_89,c_90]) ).
tcf(c_3133,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1111,c_90]) ).
tcf(c_3134,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1112,c_90]) ).
tcf(c_3135,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1113,c_90]) ).
tcf(c_3136,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1114,c_90]) ).
tcf(c_3137,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1115,c_90]) ).
tcf(c_3143,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3137,c_88]) ).
tcf(c_3144,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3136,c_88]) ).
tcf(c_3145,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3135,c_88]) ).
tcf(c_3146,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3134,c_88]) ).
tcf(c_3147,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3133,c_88]) ).
tcf(c_3183,plain,
! [X0: $i] :
( ( X0 = iPr_def_23 )
| ( iPr_def_23 != inverse(sk_c2) )
| ( X0 != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1596]) ).
tcf(c_3184,plain,
( ( sk_c7 = iPr_def_23 )
| ( iPr_def_23 != inverse(sk_c2) )
| ( sk_c7 != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_3183]) ).
tcf(c_3255,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( iPr_def_16 = iPr_def_23 )
| ( sk_c7 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_904,c_507]) ).
tcf(c_3258,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( iPr_def_16 = iPr_def_23 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_904,c_506]) ).
tcf(c_3261,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( multiply(iPr_def_16,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_904,c_473]) ).
tcf(c_3302,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c2 )
| ( sk_c2 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_3438,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1214,c_482]) ).
tcf(c_3752,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_18 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1517,c_1441]) ).
tcf(c_3788,plain,
( ~ iPr_def_10
| ( sk_c8 != iPr_def_22 )
| ( inverse(sk_c3) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_480,c_490]) ).
tcf(c_3789,plain,
( ~ iPr_def_10
| ( sk_c8 != sk_c6 )
| ( inverse(identity) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_88,c_490]) ).
tcf(c_3810,plain,
( ~ iPr_def_10
| ( sk_c6 != iPr_def_18 )
| ( sk_c8 != iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_3788,c_476]) ).
tcf(c_3977,plain,
! [X0: $i] :
( ( X0 = sk_c6 )
| ( sk_c6 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2042]) ).
tcf(c_4027,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_21 != sk_c8 )
| ( iPr_def_20 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_3120]) ).
tcf(c_4154,plain,
( ( iPr_def_15 = sk_c6 )
| ( iPr_def_15 != iPr_def_15 )
| ( sk_c6 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_3977]) ).
tcf(c_4155,plain,
iPr_def_15 = iPr_def_15,
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_4293,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( iPr_def_17 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1679,c_1624]) ).
tcf(c_4491,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( iPr_def_20 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_1791,c_1737]) ).
tcf(c_4669,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_19 )
| ( iPr_def_19 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_4670,plain,
( ( sk_c7 = iPr_def_19 )
| ( iPr_def_19 != sk_c7 )
| ( sk_c7 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_4669]) ).
tcf(c_4765,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_17 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_2017,c_1979]) ).
tcf(c_4890,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_20 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_2167,c_1214]) ).
tcf(c_4893,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( sk_c8 = iPr_def_20 )
| ( multiply(iPr_def_26,iPr_def_22) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2167,c_800]) ).
tcf(c_4902,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( multiply(iPr_def_26,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2167,c_473]) ).
tcf(c_4938,plain,
multiply(iPr_def_18,iPr_def_22) = sk_c6,
inference(superposition,[status(thm)],[c_480,c_3143]) ).
tcf(c_4943,plain,
multiply(iPr_def_23,iPr_def_24) = sk_c7,
inference(superposition,[status(thm)],[c_482,c_3144]) ).
tcf(c_4946,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(iPr_def_24,X0)) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_4943,c_90]) ).
tcf(c_4948,plain,
multiply(iPr_def_25,iPr_def_26) = sk_c8,
inference(superposition,[status(thm)],[c_484,c_3145]) ).
tcf(c_4992,plain,
multiply(iPr_def_19,iPr_def_17) = sk_c6,
inference(superposition,[status(thm)],[c_475,c_3146]) ).
tcf(c_5174,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(iPr_def_18,iPr_def_22) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_499,c_810]) ).
tcf(c_5180,plain,
( ( sk_c6 = iPr_def_16 )
| ( sk_c8 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_5174,c_4938]) ).
tcf(c_5271,plain,
! [X0: $i] :
( ( inverse(sk_c2) = X0 )
| ( X0 != iPr_def_23 )
| ( inverse(sk_c2) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1302]) ).
tcf(c_5272,plain,
( ( inverse(sk_c2) = sk_c7 )
| ( sk_c7 != iPr_def_23 )
| ( inverse(sk_c2) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_5271]) ).
tcf(c_5292,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(iPr_def_18,iPr_def_22) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_498,c_811]) ).
tcf(c_5297,plain,
( ( sk_c6 = iPr_def_16 )
| ( sk_c8 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_5292,c_4938]) ).
tcf(c_5365,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c2) )
| ( X0 != iPr_def_23 )
| ( inverse(sk_c2) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1372]) ).
tcf(c_5366,plain,
( ( sk_c7 = inverse(sk_c2) )
| ( sk_c7 != iPr_def_23 )
| ( inverse(sk_c2) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_5365]) ).
tcf(c_5380,plain,
! [X0: $i] :
( ( iPr_def_21 = X0 )
| ( iPr_def_21 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_2820]) ).
tcf(c_5402,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_18,iPr_def_22) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_497,c_812]) ).
tcf(c_5406,plain,
( ( sk_c6 = iPr_def_16 )
| ( sk_c7 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_5402,c_4938]) ).
tcf(c_5440,plain,
( ( sk_c6 = iPr_def_18 )
| ( iPr_def_18 != sk_c6 )
| ( sk_c6 != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_1250]) ).
tcf(c_5468,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_18,iPr_def_22) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_496,c_813]) ).
tcf(c_5471,plain,
( ( sk_c6 = iPr_def_16 )
| ( sk_c7 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_5468,c_4938]) ).
tcf(c_5501,plain,
( ( sk_c6 = iPr_def_24 )
| ( iPr_def_24 != sk_c6 )
| ( sk_c6 != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_1250]) ).
tcf(c_5509,plain,
( ( inverse(sk_c2) = iPr_def_16 )
| ( iPr_def_16 != iPr_def_23 )
| ( inverse(sk_c2) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1598]) ).
tcf(c_5739,plain,
multiply(iPr_def_21,iPr_def_20) = sk_c7,
inference(superposition,[status(thm)],[c_478,c_3147]) ).
tcf(c_5742,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(iPr_def_20,X0)) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_5739,c_90]) ).
tcf(c_5770,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c8 = iPr_def_21 )
| ( iPr_def_15 != iPr_def_16 )
| ( sk_c7 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5180,c_485]) ).
tcf(c_5783,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(iPr_def_16,sk_c8) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5180,c_474]) ).
tcf(c_5959,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( multiply(iPr_def_22,iPr_def_26) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_4293,c_4948]) ).
tcf(c_6253,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(iPr_def_19,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_834,c_3146]) ).
tcf(c_6254,plain,
( ( sk_c6 = iPr_def_18 )
| ( sk_c8 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_6253,c_4992]) ).
tcf(c_6265,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(iPr_def_19,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_835,c_3146]) ).
tcf(c_6266,plain,
( ( sk_c6 = iPr_def_18 )
| ( sk_c8 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_6265,c_4992]) ).
tcf(c_6277,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_19,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_836,c_3146]) ).
tcf(c_6278,plain,
( ( sk_c6 = iPr_def_18 )
| ( sk_c7 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_6277,c_4992]) ).
tcf(c_6289,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_19,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_837,c_3146]) ).
tcf(c_6290,plain,
( ( sk_c6 = iPr_def_18 )
| ( sk_c7 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_6289,c_4992]) ).
tcf(c_6528,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c8 = iPr_def_20 )
| ( iPr_def_15 != iPr_def_16 )
| ( sk_c7 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5297,c_485]) ).
tcf(c_6541,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(iPr_def_16,sk_c8) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5297,c_474]) ).
tcf(c_6697,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c7 = iPr_def_19 )
| ( iPr_def_15 != iPr_def_16 )
| ( sk_c7 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5406,c_485]) ).
tcf(c_6710,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_16,sk_c8) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5406,c_474]) ).
tcf(c_6898,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c7 = iPr_def_17 )
| ( iPr_def_15 != iPr_def_16 )
| ( sk_c7 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5471,c_485]) ).
tcf(c_6911,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_16,sk_c8) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5471,c_474]) ).
tcf(c_8621,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_21,iPr_def_20) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1032,c_3147]) ).
tcf(c_8622,plain,
( ( sk_c7 = iPr_def_23 )
| ( sk_c7 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_8621,c_5739]) ).
tcf(c_8636,plain,
( ( sk_c7 = iPr_def_16 )
| ( multiply(iPr_def_21,iPr_def_20) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1033,c_3147]) ).
tcf(c_8637,plain,
( ( sk_c7 = iPr_def_19 )
| ( sk_c7 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_8636,c_5739]) ).
tcf(c_8648,plain,
( ( sk_c7 = iPr_def_16 )
| ( multiply(iPr_def_21,iPr_def_20) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_1034,c_3147]) ).
tcf(c_8649,plain,
( ( sk_c7 = iPr_def_17 )
| ( sk_c7 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_8648,c_5739]) ).
tcf(c_8957,plain,
( ( sk_c7 = iPr_def_16 )
| ( multiply(iPr_def_25,iPr_def_26) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_1083,c_3145]) ).
tcf(c_8958,plain,
( ( sk_c7 = iPr_def_16 )
| ( sk_c8 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_8957,c_4948]) ).
tcf(c_9402,plain,
( ( sk_c7 = iPr_def_23 )
| ( multiply(iPr_def_25,iPr_def_26) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_1171,c_3145]) ).
tcf(c_9403,plain,
( ( sk_c7 = iPr_def_23 )
| ( sk_c8 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_9402,c_4948]) ).
tcf(c_9806,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_18,iPr_def_22) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1323,c_3143]) ).
tcf(c_9807,plain,
( ( sk_c6 = iPr_def_24 )
| ( sk_c7 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_9806,c_4938]) ).
tcf(c_10160,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_18,iPr_def_22) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1391,c_3143]) ).
tcf(c_10161,plain,
( ( sk_c6 = iPr_def_24 )
| ( sk_c7 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_10160,c_4938]) ).
tcf(c_10286,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(iPr_def_18,iPr_def_22) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1434,c_3143]) ).
tcf(c_10287,plain,
( ( sk_c6 = iPr_def_24 )
| ( sk_c8 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_10286,c_4938]) ).
tcf(c_10376,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(iPr_def_18,iPr_def_22) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1511,c_3143]) ).
tcf(c_10377,plain,
( ( sk_c6 = iPr_def_24 )
| ( sk_c8 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_10376,c_4938]) ).
tcf(c_11686,plain,
( ( sk_c8 = iPr_def_23 )
| ( iPr_def_23 != inverse(sk_c2) )
| ( sk_c8 != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_3183]) ).
tcf(c_11911,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1977,c_3144]) ).
tcf(c_11912,plain,
( ( sk_c7 = iPr_def_26 )
| ( sk_c7 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_11911,c_4943]) ).
tcf(c_11985,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2018,c_3144]) ).
tcf(c_11986,plain,
( ( sk_c7 = iPr_def_26 )
| ( sk_c7 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_11985,c_4943]) ).
tcf(c_12056,plain,
( ( sk_c7 = iPr_def_26 )
| ( multiply(iPr_def_25,iPr_def_26) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_2068,c_3145]) ).
tcf(c_12057,plain,
( ( sk_c7 = iPr_def_26 )
| ( sk_c8 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_12056,c_4948]) ).
tcf(c_12451,plain,
( ( sk_c7 = iPr_def_26 )
| ( multiply(iPr_def_25,iPr_def_26) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_2173,c_3145]) ).
tcf(c_12452,plain,
( ( sk_c7 = iPr_def_26 )
| ( sk_c8 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_12451,c_4948]) ).
tcf(c_12943,plain,
multiply(sk_c4,iPr_def_15) = multiply(iPr_def_20,sk_c8),
inference(superposition,[status(thm)],[c_473,c_3124]) ).
tcf(c_13082,plain,
! [X0: $i] :
( ( iPr_def_16 = inverse(sk_c2) )
| ( iPr_def_16 != X0 )
| ( inverse(sk_c2) != X0 ) ),
inference(instantiation,[status(thm)],[c_1135]) ).
tcf(c_13084,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c2) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c2) != X0 ) ),
inference(instantiation,[status(thm)],[c_1068]) ).
tcf(c_13088,plain,
( ( iPr_def_16 = inverse(sk_c2) )
| ( iPr_def_16 != sk_c7 )
| ( inverse(sk_c2) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_13082]) ).
tcf(c_13135,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c2) )
| ( X0 != iPr_def_16 )
| ( inverse(sk_c2) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1376]) ).
tcf(c_13138,plain,
( ( sk_c7 = inverse(sk_c2) )
| ( sk_c7 != iPr_def_16 )
| ( inverse(sk_c2) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_13135]) ).
tcf(c_13602,plain,
multiply(sk_c5,iPr_def_16) = multiply(iPr_def_17,sk_c8),
inference(superposition,[status(thm)],[c_474,c_3125]) ).
tcf(c_14537,plain,
multiply(sk_c3,iPr_def_16) = multiply(iPr_def_22,sk_c8),
inference(superposition,[status(thm)],[c_474,c_3128]) ).
tcf(c_17033,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_16 )
| ( sk_c8 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_5783,c_3261]) ).
tcf(c_17659,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_16 )
| ( sk_c8 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_6541,c_3261]) ).
tcf(c_18010,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_16 )
| ( sk_c7 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_6710,c_3261]) ).
tcf(c_18266,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_16 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_6911,c_3261]) ).
tcf(c_19006,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_3130,c_88]) ).
tcf(c_19013,plain,
multiply(inverse(sk_c7),iPr_def_15) = sk_c8,
inference(superposition,[status(thm)],[c_473,c_19006]) ).
tcf(c_19017,plain,
multiply(inverse(sk_c6),iPr_def_16) = sk_c8,
inference(superposition,[status(thm)],[c_474,c_19006]) ).
tcf(c_19019,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_88,c_19006]) ).
tcf(c_19020,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_89,c_19006]) ).
tcf(c_19215,plain,
! [X0: $i] : multiply(inverse(iPr_def_21),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_3147,c_19006]) ).
tcf(c_19216,plain,
! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_3146,c_19006]) ).
tcf(c_19217,plain,
! [X0: $i] : multiply(inverse(iPr_def_25),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_3145,c_19006]) ).
tcf(c_19218,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_3144,c_19006]) ).
tcf(c_19219,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_3143,c_19006]) ).
tcf(c_19253,plain,
multiply(inverse(sk_c5),multiply(iPr_def_17,sk_c8)) = iPr_def_16,
inference(superposition,[status(thm)],[c_13602,c_19006]) ).
tcf(c_19302,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_19006,c_19006]) ).
tcf(c_19919,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != inverse(sk_c2) )
| ( inverse(X0) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1104]) ).
tcf(c_19920,plain,
( ( inverse(sk_c7) = sk_c7 )
| ( sk_c7 != inverse(sk_c2) )
| ( inverse(sk_c7) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_19919]) ).
tcf(c_19963,plain,
( ( sk_c2 = inverse(sk_c2) )
| ( sk_c2 != iPr_def_23 )
| ( inverse(sk_c2) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_5365]) ).
tcf(c_20635,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_19020,c_19302]) ).
tcf(c_20648,plain,
multiply(sk_c6,sk_c8) = multiply(iPr_def_16,identity),
inference(superposition,[status(thm)],[c_20635,c_3127]) ).
tcf(c_20649,plain,
multiply(sk_c7,sk_c8) = multiply(iPr_def_15,identity),
inference(superposition,[status(thm)],[c_20635,c_3123]) ).
tcf(c_20651,plain,
multiply(sk_c7,identity) = multiply(iPr_def_21,iPr_def_20),
inference(superposition,[status(thm)],[c_20635,c_5742]) ).
tcf(c_20657,plain,
multiply(sk_c7,identity) = multiply(iPr_def_23,iPr_def_24),
inference(superposition,[status(thm)],[c_20635,c_4946]) ).
tcf(c_20664,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_20635,c_19019]) ).
tcf(c_20666,plain,
multiply(sk_c7,identity) = sk_c7,
inference(light_normalisation,[status(thm)],[c_20657,c_4943]) ).
tcf(c_20674,plain,
multiply(iPr_def_15,identity) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_20649,c_473]) ).
tcf(c_20675,plain,
multiply(iPr_def_16,identity) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_20648,c_474]) ).
tcf(c_21012,plain,
( ( sk_c7 = iPr_def_19 )
| ( iPr_def_16 = iPr_def_23 ) ),
inference(global_subsumption_just,[status(thm)],[c_3255,c_532,c_507,c_1028,c_1029,c_1601,c_4670,c_8637]) ).
tcf(c_21013,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( sk_c7 = iPr_def_19 ) ),
inference(renaming,[status(thm)],[c_21012]) ).
tcf(c_21238,plain,
( ( sk_c7 = iPr_def_17 )
| ( iPr_def_16 = iPr_def_23 ) ),
inference(global_subsumption_just,[status(thm)],[c_3258,c_481,c_1028,c_1029,c_1964,c_1965,c_2887,c_5272,c_8622,c_8649,c_13088]) ).
tcf(c_21239,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( sk_c7 = iPr_def_17 ) ),
inference(renaming,[status(thm)],[c_21238]) ).
tcf(c_21265,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( iPr_def_16 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_21239,c_21013]) ).
tcf(c_21725,plain,
( ( sk_c8 = iPr_def_21 )
| ~ iPr_def_14
| ( sk_c7 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_519,c_2587]) ).
tcf(c_21726,plain,
( ( sk_c8 = iPr_def_20 )
| ~ iPr_def_14
| ( sk_c7 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_518,c_2587]) ).
tcf(c_21727,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_14
| ( sk_c7 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_517,c_2587]) ).
tcf(c_21728,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_14
| ( sk_c7 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_516,c_2587]) ).
tcf(c_22186,plain,
( ( sk_c8 = iPr_def_20 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_21726,c_12057,c_21726]) ).
tcf(c_22197,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_21727,c_11986,c_21727]) ).
tcf(c_22251,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_13
| ( sk_c6 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_507,c_2746]) ).
tcf(c_22252,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_13
| ( sk_c6 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_506,c_2746]) ).
tcf(c_22455,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_22251,c_10161,c_22251]) ).
tcf(c_22628,plain,
( ~ iPr_def_14
| ( inverse(inverse(iPr_def_21)) != sk_c8 )
| ( multiply(sk_c4,sk_c8) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_19215,c_486]) ).
tcf(c_22629,plain,
multiply(sk_c4,iPr_def_21) = identity,
inference(superposition,[status(thm)],[c_19215,c_89]) ).
tcf(c_22632,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_21)) != sk_c8 )
| ( multiply(sk_c4,sk_c7) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_19215,c_488]) ).
tcf(c_22636,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_21,X0)) = X0,
inference(superposition,[status(thm)],[c_19215,c_19006]) ).
tcf(c_22637,plain,
multiply(sk_c4,identity) = inverse(iPr_def_21),
inference(superposition,[status(thm)],[c_19215,c_20635]) ).
tcf(c_22772,plain,
inverse(iPr_def_21) = sk_c4,
inference(demodulation,[status(thm)],[c_22637,c_20635]) ).
tcf(c_22780,plain,
multiply(sk_c4,sk_c7) = iPr_def_20,
inference(superposition,[status(thm)],[c_5739,c_22636]) ).
tcf(c_22971,plain,
( ( sk_c8 = iPr_def_21 )
| ~ iPr_def_12
| ( iPr_def_22 != iPr_def_24 )
| ( sk_c8 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_499,c_2842]) ).
tcf(c_22972,plain,
( ( sk_c8 = iPr_def_20 )
| ~ iPr_def_12
| ( iPr_def_22 != iPr_def_24 )
| ( sk_c8 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_498,c_2842]) ).
tcf(c_23228,plain,
multiply(sk_c5,iPr_def_19) = identity,
inference(superposition,[status(thm)],[c_19216,c_89]) ).
tcf(c_23232,plain,
( ~ iPr_def_13
| ( inverse(inverse(iPr_def_19)) != sk_c7 )
| ( multiply(sk_c5,sk_c7) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_19216,c_487]) ).
tcf(c_23235,plain,
! [X0: $i] : multiply(sk_c5,multiply(iPr_def_19,X0)) = X0,
inference(superposition,[status(thm)],[c_19216,c_19006]) ).
tcf(c_23236,plain,
multiply(sk_c5,identity) = inverse(iPr_def_19),
inference(superposition,[status(thm)],[c_19216,c_20635]) ).
tcf(c_23268,plain,
inverse(iPr_def_19) = sk_c5,
inference(demodulation,[status(thm)],[c_23236,c_20635]) ).
tcf(c_23533,plain,
( ( sk_c7 = iPr_def_16 )
| ~ iPr_def_11
| ( sk_c7 != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_501,c_2929]) ).
tcf(c_23721,plain,
( ( sk_c7 = iPr_def_16 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_23533,c_8637,c_23533]) ).
tcf(c_23765,plain,
( ( sk_c8 = iPr_def_21 )
| ~ iPr_def_10
| ( sk_c6 != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_499,c_3810]) ).
tcf(c_23766,plain,
( ( sk_c8 = iPr_def_20 )
| ~ iPr_def_10
| ( sk_c6 != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_498,c_3810]) ).
tcf(c_23767,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_10
| ( sk_c6 != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_497,c_3810]) ).
tcf(c_23768,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_10
| ( sk_c6 != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_496,c_3810]) ).
tcf(c_23861,plain,
multiply(sk_c5,sk_c6) = iPr_def_17,
inference(superposition,[status(thm)],[c_4992,c_23235]) ).
tcf(c_24000,plain,
( ~ iPr_def_14
| ( inverse(inverse(iPr_def_25)) != sk_c8 )
| ( multiply(sk_c1,sk_c8) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_19217,c_486]) ).
tcf(c_24001,plain,
multiply(sk_c1,iPr_def_25) = identity,
inference(superposition,[status(thm)],[c_19217,c_89]) ).
tcf(c_24004,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_25)) != sk_c8 )
| ( multiply(sk_c1,sk_c7) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_19217,c_488]) ).
tcf(c_24008,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_25,X0)) = X0,
inference(superposition,[status(thm)],[c_19217,c_19006]) ).
tcf(c_24009,plain,
multiply(sk_c1,identity) = inverse(iPr_def_25),
inference(superposition,[status(thm)],[c_19217,c_20635]) ).
tcf(c_24026,plain,
( ~ iPr_def_14
| ( sk_c7 != iPr_def_26 )
| ( inverse(inverse(iPr_def_25)) != sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_24000,c_484]) ).
tcf(c_24030,plain,
( ( identity = iPr_def_26 )
| ( sk_c8 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_1788,c_24001]) ).
tcf(c_24031,plain,
( ( identity = iPr_def_26 )
| ( sk_c8 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_1731,c_24001]) ).
tcf(c_24032,plain,
( ( identity = iPr_def_26 )
| ( sk_c7 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1672,c_24001]) ).
tcf(c_24033,plain,
( ( identity = iPr_def_26 )
| ( sk_c7 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_1616,c_24001]) ).
tcf(c_24089,plain,
( ( sk_c8 = iPr_def_20 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_23766,c_6266,c_23766]) ).
tcf(c_24095,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_23767,c_6278,c_23767]) ).
tcf(c_24484,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_24031,c_24030]) ).
tcf(c_24777,plain,
! [X0: $i] :
( ( X0 = sk_c2 )
| ( sk_c2 != inverse(sk_c2) )
| ( X0 != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_3302]) ).
tcf(c_24778,plain,
( ( sk_c7 = sk_c2 )
| ( sk_c2 != inverse(sk_c2) )
| ( sk_c7 != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_24777]) ).
tcf(c_25060,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_24033,c_24032]) ).
tcf(c_25201,plain,
inverse(iPr_def_25) = sk_c1,
inference(demodulation,[status(thm)],[c_24009,c_20635]) ).
tcf(c_25203,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( inverse(iPr_def_22) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_4491,c_25201]) ).
tcf(c_25212,plain,
multiply(sk_c1,sk_c8) = iPr_def_26,
inference(superposition,[status(thm)],[c_4948,c_24008]) ).
tcf(c_25420,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( inverse(iPr_def_26) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_24484,c_20664]) ).
tcf(c_25422,plain,
! [X0: $i] :
( ( iPr_def_20 = iPr_def_21 )
| ( multiply(iPr_def_26,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_24484,c_88]) ).
tcf(c_25777,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( inverse(iPr_def_26) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_25060,c_20664]) ).
tcf(c_25794,plain,
multiply(sk_c2,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_19218,c_89]) ).
tcf(c_25798,plain,
( ~ iPr_def_13
| ( inverse(inverse(iPr_def_23)) != sk_c7 )
| ( multiply(sk_c2,sk_c7) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_19218,c_487]) ).
tcf(c_25801,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_23,X0)) = X0,
inference(superposition,[status(thm)],[c_19218,c_19006]) ).
tcf(c_25802,plain,
multiply(sk_c2,identity) = inverse(iPr_def_23),
inference(superposition,[status(thm)],[c_19218,c_20635]) ).
tcf(c_25813,plain,
( ~ iPr_def_13
| ( sk_c6 != iPr_def_24 )
| ( inverse(inverse(iPr_def_23)) != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_25798,c_482]) ).
tcf(c_25824,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( identity = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_3438,c_25794]) ).
tcf(c_25825,plain,
( ( identity = iPr_def_24 )
| ( sk_c7 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1145,c_25794]) ).
tcf(c_25826,plain,
( ( identity = iPr_def_24 )
| ( sk_c7 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_1070,c_25794]) ).
tcf(c_25849,plain,
inverse(iPr_def_23) = sk_c2,
inference(demodulation,[status(thm)],[c_25802,c_20635]) ).
tcf(c_25884,plain,
! [X0: $i] :
( ( iPr_def_20 = iPr_def_21 )
| ( multiply(X0,iPr_def_24) = X0 ) ),
inference(superposition,[status(thm)],[c_25824,c_20635]) ).
tcf(c_25885,plain,
! [X0: $i] :
( ( iPr_def_20 = iPr_def_21 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_25824,c_88]) ).
tcf(c_25895,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( multiply(sk_c7,iPr_def_24) = sk_c7 ) ),
inference(instantiation,[status(thm)],[c_25884]) ).
tcf(c_26162,plain,
( ( iPr_def_21 = sk_c8 )
| ( iPr_def_21 != iPr_def_21 )
| ( sk_c8 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_5380]) ).
tcf(c_26293,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( identity = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_25826,c_25825]) ).
tcf(c_26779,plain,
multiply(sk_c2,sk_c7) = iPr_def_24,
inference(superposition,[status(thm)],[c_4943,c_25801]) ).
tcf(c_27088,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_19 )
| ( multiply(X0,iPr_def_24) = X0 ) ),
inference(superposition,[status(thm)],[c_26293,c_20635]) ).
tcf(c_27089,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_19 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_26293,c_88]) ).
tcf(c_27099,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( multiply(sk_c7,iPr_def_24) = sk_c7 ) ),
inference(instantiation,[status(thm)],[c_27088]) ).
tcf(c_28271,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( sk_c8 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_25422,c_4902]) ).
tcf(c_28525,plain,
( ( iPr_def_20 = iPr_def_21 )
| ~ iPr_def_10
| ( iPr_def_15 != iPr_def_22 )
| ( sk_c6 != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_28271,c_3810]) ).
tcf(c_28526,plain,
( ( iPr_def_20 = iPr_def_21 )
| ~ iPr_def_12
| ( iPr_def_15 != iPr_def_20 )
| ( sk_c8 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_28271,c_2846]) ).
tcf(c_28528,plain,
( ( iPr_def_20 = iPr_def_21 )
| ~ iPr_def_14
| ( iPr_def_15 != iPr_def_25 )
| ( sk_c7 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_28271,c_2587]) ).
tcf(c_28607,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_15 = iPr_def_25 )
| ( sk_c8 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_28271,c_519]) ).
tcf(c_28608,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_15 = iPr_def_25 )
| ( sk_c8 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_28271,c_518]) ).
tcf(c_28972,plain,
multiply(sk_c3,iPr_def_18) = identity,
inference(superposition,[status(thm)],[c_19219,c_89]) ).
tcf(c_28977,plain,
( ~ iPr_def_10
| ( inverse(inverse(iPr_def_18)) != sk_c6 )
| ( multiply(sk_c3,sk_c6) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_19219,c_490]) ).
tcf(c_28979,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_18,X0)) = X0,
inference(superposition,[status(thm)],[c_19219,c_19006]) ).
tcf(c_28980,plain,
multiply(sk_c3,identity) = inverse(iPr_def_18),
inference(superposition,[status(thm)],[c_19219,c_20635]) ).
tcf(c_28985,plain,
( ~ iPr_def_10
| ( sk_c8 != iPr_def_22 )
| ( inverse(inverse(iPr_def_18)) != sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_28977,c_480]) ).
tcf(c_28998,plain,
( ( identity = iPr_def_22 )
| ( sk_c7 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_1047,c_28972]) ).
tcf(c_28999,plain,
( ( identity = iPr_def_22 )
| ( sk_c7 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1046,c_28972]) ).
tcf(c_29000,plain,
( ( identity = iPr_def_22 )
| ( sk_c8 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_1045,c_28972]) ).
tcf(c_29001,plain,
( ( identity = iPr_def_22 )
| ( sk_c8 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_1044,c_28972]) ).
tcf(c_29345,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( identity = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_28999,c_28998]) ).
tcf(c_30095,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( identity = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_29001,c_29000]) ).
tcf(c_30285,plain,
inverse(iPr_def_18) = sk_c3,
inference(demodulation,[status(thm)],[c_28980,c_20635]) ).
tcf(c_30295,plain,
multiply(sk_c3,sk_c6) = iPr_def_22,
inference(superposition,[status(thm)],[c_4938,c_28979]) ).
tcf(c_30791,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( sk_c8 = iPr_def_20 )
| ( sk_c8 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_25885,c_1438]) ).
tcf(c_30982,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( iPr_def_17 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_29345,c_26293]) ).
tcf(c_30988,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_19 )
| ( multiply(iPr_def_22,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_29345,c_88]) ).
tcf(c_31016,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( iPr_def_20 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_30095,c_25824]) ).
tcf(c_35009,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_18 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_31016,c_3752]) ).
tcf(c_35919,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( sk_c8 = iPr_def_21 )
| ( sk_c8 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_27089,c_1515]) ).
tcf(c_35920,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( sk_c8 = iPr_def_20 )
| ( sk_c8 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_27089,c_1438]) ).
tcf(c_36359,plain,
! [X0: $i] :
( ( X0 = sk_c6 )
| ( sk_c6 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_2042]) ).
tcf(c_36364,plain,
( ( sk_c7 = sk_c6 )
| ( sk_c6 != iPr_def_16 )
| ( sk_c7 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_36359]) ).
tcf(c_37530,plain,
! [X0: $i] :
( ( inverse(sk_c2) = iPr_def_16 )
| ( iPr_def_16 != X0 )
| ( inverse(sk_c2) != X0 ) ),
inference(instantiation,[status(thm)],[c_13084]) ).
tcf(c_37532,plain,
( ( inverse(sk_c2) = iPr_def_16 )
| ( iPr_def_16 != sk_c7 )
| ( inverse(sk_c2) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_37530]) ).
tcf(c_37745,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( inverse(iPr_def_18) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_35009,c_25203]) ).
tcf(c_37753,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( sk_c1 = sk_c3 ) ),
inference(light_normalisation,[status(thm)],[c_37745,c_30285]) ).
tcf(c_37786,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( inverse(sk_c1) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_37753,c_476]) ).
tcf(c_37787,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_18 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_37786,c_483]) ).
tcf(c_38269,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( inverse(iPr_def_23) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_4890,c_25420]) ).
tcf(c_38273,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( sk_c2 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_38269,c_25849]) ).
tcf(c_38581,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( inverse(iPr_def_23) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_4765,c_25777]) ).
tcf(c_38584,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( sk_c2 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_38581,c_25849]) ).
tcf(c_39548,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_15 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_28608,c_28607]) ).
tcf(c_39701,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( sk_c8 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_30988,c_5959]) ).
tcf(c_40423,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_39548,c_37787]) ).
tcf(c_40459,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_15 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_39548,c_4491]) ).
tcf(c_40947,plain,
( ( iPr_def_17 = iPr_def_19 )
| ~ iPr_def_12
| ( iPr_def_20 != iPr_def_26 )
| ( sk_c8 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_39701,c_2846]) ).
tcf(c_41028,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_17 = iPr_def_19 )
| ( sk_c8 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_39701,c_519]) ).
tcf(c_41029,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_17 = iPr_def_19 )
| ( sk_c8 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_39701,c_518]) ).
tcf(c_41030,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_17 = iPr_def_19 )
| ( sk_c7 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_39701,c_517]) ).
tcf(c_41031,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_17 = iPr_def_19 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_39701,c_516]) ).
tcf(c_43469,plain,
( ( sk_c8 = inverse(sk_c2) )
| ( sk_c8 != iPr_def_16 )
| ( inverse(sk_c2) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_13135]) ).
tcf(c_44580,plain,
( ( sk_c8 = iPr_def_21 )
| ( iPr_def_17 = iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_41028,c_481,c_904,c_1963,c_1964,c_1965,c_2746,c_3007,c_3184,c_5509,c_5770,c_6254,c_10377,c_11686,c_12452,c_13138,c_17033,c_19920,c_19963,c_21265,c_21725,c_22971,c_23765,c_24778,c_27099,c_30982,c_35919,c_38584,c_43469]) ).
tcf(c_44581,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( sk_c8 = iPr_def_21 ) ),
inference(renaming,[status(thm)],[c_44580]) ).
tcf(c_45565,plain,
( ( sk_c8 = iPr_def_20 )
| ( iPr_def_17 = iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_41029,c_481,c_904,c_1963,c_1964,c_1965,c_2746,c_3006,c_3184,c_5509,c_6266,c_6528,c_10287,c_11686,c_12057,c_13138,c_17659,c_19920,c_19963,c_21265,c_21726,c_22972,c_23766,c_24778,c_27099,c_30982,c_35920,c_38584,c_43469]) ).
tcf(c_45566,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( sk_c8 = iPr_def_20 ) ),
inference(renaming,[status(thm)],[c_45565]) ).
tcf(c_45605,plain,
( ( iPr_def_20 = iPr_def_26 )
| ( iPr_def_17 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_45566,c_39701]) ).
tcf(c_45618,plain,
( ( iPr_def_17 = iPr_def_19 )
| ~ iPr_def_12
| ( sk_c8 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_45566,c_2846]) ).
tcf(c_45841,plain,
( ( sk_c7 = iPr_def_19 )
| ( iPr_def_17 = iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_41030,c_481,c_904,c_1963,c_1964,c_1965,c_3005,c_5509,c_6697,c_13138,c_18010,c_19920,c_19963,c_21265,c_22197,c_22455,c_24095,c_24778,c_27099,c_38584,c_44581,c_45618]) ).
tcf(c_45842,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( sk_c7 = iPr_def_19 ) ),
inference(renaming,[status(thm)],[c_45841]) ).
tcf(c_46098,plain,
( ( sk_c7 = iPr_def_17 )
| ( iPr_def_17 = iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_41031,c_481,c_904,c_1963,c_1964,c_1965,c_3004,c_5509,c_6290,c_6898,c_9807,c_11912,c_13138,c_18266,c_19920,c_19963,c_21265,c_21728,c_22252,c_23768,c_24778,c_27099,c_38584,c_40947,c_44581,c_45605]) ).
tcf(c_46099,plain,
( ( iPr_def_17 = iPr_def_19 )
| ( sk_c7 = iPr_def_17 ) ),
inference(renaming,[status(thm)],[c_46098]) ).
tcf(c_46130,plain,
iPr_def_17 = iPr_def_19,
inference(superposition,[status(thm)],[c_46099,c_45842]) ).
tcf(c_46219,plain,
( ~ iPr_def_11
| ( sk_c7 != iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_2929,c_46130]) ).
tcf(c_46220,plain,
inverse(iPr_def_17) = sk_c5,
inference(demodulation,[status(thm)],[c_23268,c_46130]) ).
tcf(c_46221,plain,
multiply(sk_c5,iPr_def_17) = identity,
inference(demodulation,[status(thm)],[c_23228,c_46130]) ).
tcf(c_46286,plain,
multiply(iPr_def_17,iPr_def_17) = sk_c6,
inference(demodulation,[status(thm)],[c_4992,c_46130]) ).
tcf(c_46300,plain,
inverse(sk_c5) = iPr_def_17,
inference(demodulation,[status(thm)],[c_477,c_46130]) ).
tcf(c_46310,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( sk_c8 = iPr_def_20 ) ),
inference(global_subsumption_just,[status(thm)],[c_4893,c_481,c_1028,c_1029,c_1963,c_1964,c_1965,c_2397,c_2746,c_3006,c_5272,c_5366,c_8958,c_9403,c_10287,c_11686,c_19920,c_19963,c_22186,c_22972,c_24089,c_24778,c_25895,c_30791,c_31016,c_37532,c_38273,c_40423,c_43469]) ).
tcf(c_46347,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_15 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_46310,c_28271]) ).
tcf(c_46351,plain,
( ( iPr_def_20 = iPr_def_21 )
| ~ iPr_def_10
| ( iPr_def_20 != iPr_def_22 )
| ( sk_c6 != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_46310,c_3810]) ).
tcf(c_46352,plain,
( ( iPr_def_20 = iPr_def_21 )
| ~ iPr_def_12
| ( sk_c8 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_46310,c_2846]) ).
tcf(c_46354,plain,
( ( iPr_def_20 = iPr_def_21 )
| ~ iPr_def_14
| ( iPr_def_20 != iPr_def_25 )
| ( sk_c7 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_46310,c_2587]) ).
tcf(c_46408,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( iPr_def_20 = iPr_def_21 )
| ( sk_c8 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_46310,c_519]) ).
tcf(c_46410,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( iPr_def_20 = iPr_def_21 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_46310,c_516]) ).
tcf(c_46862,plain,
( ( identity = iPr_def_26 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_24033,c_46219]) ).
tcf(c_47102,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( iPr_def_20 = iPr_def_21 ) ),
inference(global_subsumption_just,[status(thm)],[c_46408,c_485,c_493,c_513,c_950,c_1028,c_1029,c_1108,c_1214,c_2124,c_2167,c_2395,c_2746,c_4027,c_4154,c_4155,c_5440,c_5501,c_26162,c_28528,c_28526,c_28525,c_39548,c_40459,c_40423,c_46219,c_46347,c_46410,c_46408]) ).
tcf(c_47580,plain,
( ~ iPr_def_12
| ( sk_c8 != identity )
| ( sk_c8 != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_2831,c_20664]) ).
tcf(c_47804,plain,
( ~ iPr_def_11
| ( inverse(identity) != sk_c7 ) ),
inference(global_subsumption_just,[status(thm)],[c_2905,c_2905,c_5471,c_23721,c_36364,c_46219]) ).
tcf(c_47806,plain,
( ~ iPr_def_11
| ( sk_c7 != identity ) ),
inference(light_normalisation,[status(thm)],[c_47804,c_20664]) ).
tcf(c_47828,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_11
| ( identity != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_521,c_47806]) ).
tcf(c_47945,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_47828,c_46219,c_46862,c_47828]) ).
tcf(c_47947,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c6 != iPr_def_15 )
| ( sk_c7 != iPr_def_16 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_485,c_47945]) ).
tcf(c_48288,plain,
( ~ iPr_def_10
| ( sk_c6 != identity )
| ( sk_c8 != sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_3789,c_20664]) ).
tcf(c_49532,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_48288,c_47947,c_47945,c_47580,c_47102,c_46354,c_46352,c_46351,c_46300,c_46286,c_46221,c_46220,c_46130,c_30295,c_30285,c_28985,c_28972,c_26779,c_25849,c_25813,c_25794,c_25212,c_25201,c_24026,c_24004,c_24001,c_23861,c_23268,c_23232,c_22780,c_22772,c_22632,c_22628,c_22629,c_20675,c_20674,c_20666,c_20651,c_20649,c_20648,c_19253,c_19017,c_19013,c_14537,c_13602,c_12943,c_2846,c_2563,c_2167,c_524,c_522,c_519,c_517,c_515,c_512,c_510,c_507,c_505,c_504,c_503,c_502,c_499,c_497,c_495,c_494,c_493,c_492,c_485,c_483,c_481,c_479,c_476]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP259-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 : n007.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:15:37 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.43 % Proving...
% 16.08/3.27 % SZS status Started for theBenchmark.p
% 16.08/3.27 % SZS status Unsatisfiable for theBenchmark.p
% 16.08/3.27
% 16.08/3.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 16.08/3.27
% 16.08/3.27 % ------ iProver source info
% 16.08/3.27
% 16.08/3.27 % git: date: 2026-07-19 20:42:38 +0200
% 16.08/3.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 16.08/3.27 % git: non_committed_changes: false
% 16.08/3.27
% 16.08/3.27 % ------ Parsing...% successful
% 16.08/3.27
% 16.08/3.27
% 16.08/3.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 16.08/3.27
% 16.08/3.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 16.08/3.27
% 16.08/3.27 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 16.08/3.27
% 16.08/3.27 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 16.08/3.27 % ------ Proving...
% 16.08/3.27 % ------ Problem Properties
% 16.08/3.27
% 16.08/3.27 %
% 16.08/3.27 % clauses 56
% 16.08/3.27 % conjectures 41
% 16.08/3.27 % EPR 36
% 16.08/3.27 % Horn 20
% 16.08/3.27 % unary 15
% 16.08/3.27 % binary 35
% 16.08/3.27 % lits 107
% 16.08/3.27 % lits eq 97
% 16.08/3.27 % fd_pure 0
% 16.08/3.27 % fd_pseudo 0
% 16.08/3.27 % fd_cond 0
% 16.08/3.27 % fd_pseudo_cond 0
% 16.08/3.27 % AC symbols 0
% 16.08/3.27
% 16.08/3.27 % ------ Schedule dynamic 5 is on
% 16.08/3.27
% 16.08/3.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 16.08/3.27
% 16.08/3.27
% 16.08/3.27 % ------
% 16.08/3.27 % Current options:
% 16.08/3.27 % ------
% 16.08/3.27
% 16.08/3.27
% 16.08/3.27 %
% 16.08/3.27
% 16.08/3.27 % ------ Proving...
% 16.08/3.27 %
% 16.08/3.27
% 16.08/3.27 % SZS status Unsatisfiable for theBenchmark.p
% 16.08/3.27
% 16.08/3.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 16.08/3.28
% 16.08/3.28
%------------------------------------------------------------------------------