%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP339-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:33:15 PM UTC 2026
% Result : Unsatisfiable 9.17s 4.15s
% Output : CNFRefutation 9.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 52
% Syntax : Number of formulae : 520 ( 135 unt; 14 def)
% Number of atoms : 1960 (1005 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 946 ( 355 ~; 591 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 20 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 151 ( 0 sgn 151 !; 0 ?; 128 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
multiply(sk_c8,sk_c9) = sk_c7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f7,plain,
( sk_c8 = multiply(sk_c3,sk_c9)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f6]) ).
fof(f8,negated_conjecture,
( inverse(sk_c3) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f9,plain,
( sk_c9 = inverse(sk_c3)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f8]) ).
fof(f10,negated_conjecture,
( inverse(sk_c8) = sk_c7
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c7 = inverse(sk_c8)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f12]) ).
fof(f18,negated_conjecture,
( inverse(sk_c6) = sk_c5
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,plain,
( inverse(sk_c6) = sk_c5
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f18]) ).
fof(f20,negated_conjecture,
( inverse(sk_c5) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_9) ).
fof(f21,plain,
( sk_c9 = inverse(sk_c5)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c5
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f23,plain,
( sk_c5 = multiply(sk_c6,sk_c9)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c8 = multiply(sk_c3,sk_c9)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( inverse(sk_c3) = sk_c9
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c9 = inverse(sk_c3)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
( inverse(sk_c8) = sk_c7
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f29,plain,
( sk_c7 = inverse(sk_c8)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f28]) ).
fof(f30,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f31,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c8 = inverse(sk_c4)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f32]) ).
fof(f34,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c8
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f35,plain,
( sk_c8 = multiply(sk_c4,sk_c7)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f34]) ).
fof(f36,negated_conjecture,
( inverse(sk_c6) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f37,plain,
( inverse(sk_c6) = sk_c5
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f36]) ).
fof(f40,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c5
| multiply(sk_c1,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_19) ).
fof(f41,plain,
( sk_c5 = multiply(sk_c6,sk_c9)
| sk_c9 = multiply(sk_c1,sk_c8) ),
inference(reorient_equations,[],[f40]) ).
fof(f42,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_20) ).
fof(f43,plain,
( sk_c8 = multiply(sk_c3,sk_c9)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f42]) ).
fof(f44,negated_conjecture,
( inverse(sk_c3) = sk_c9
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f45,plain,
( sk_c9 = inverse(sk_c3)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
( inverse(sk_c8) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f47,plain,
( sk_c7 = inverse(sk_c8)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f46]) ).
fof(f48,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_23) ).
fof(f49,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f48]) ).
fof(f54,negated_conjecture,
( inverse(sk_c6) = sk_c5
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f55,plain,
( inverse(sk_c6) = sk_c5
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f54]) ).
fof(f58,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c5
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_28) ).
fof(f59,plain,
( sk_c5 = multiply(sk_c6,sk_c9)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f58]) ).
fof(f60,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_29) ).
fof(f61,plain,
( sk_c8 = multiply(sk_c3,sk_c9)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f60]) ).
fof(f62,negated_conjecture,
( inverse(sk_c3) = sk_c9
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f63,plain,
( sk_c9 = inverse(sk_c3)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f62]) ).
fof(f64,negated_conjecture,
( inverse(sk_c8) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f65,plain,
( sk_c7 = inverse(sk_c8)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f64]) ).
fof(f66,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f67,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f66]) ).
fof(f68,negated_conjecture,
( inverse(sk_c4) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_33) ).
fof(f69,plain,
( sk_c8 = inverse(sk_c4)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f68]) ).
fof(f70,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f71,plain,
( sk_c8 = multiply(sk_c4,sk_c7)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f70]) ).
fof(f72,negated_conjecture,
( inverse(sk_c6) = sk_c5
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_35) ).
fof(f73,plain,
( inverse(sk_c6) = sk_c5
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f72]) ).
fof(f74,negated_conjecture,
( inverse(sk_c5) = sk_c9
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f75,plain,
( sk_c9 = inverse(sk_c5)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f74]) ).
fof(f76,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c5
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_37) ).
fof(f77,plain,
( sk_c5 = multiply(sk_c6,sk_c9)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f76]) ).
fof(f78,negated_conjecture,
! [X2,X3,X0,X1,X4,X5] :
( multiply(X4,sk_c9) != X5
| inverse(X5) != sk_c9
| inverse(X4) != X5
| multiply(X3,sk_c7) != sk_c8
| inverse(X3) != sk_c8
| multiply(sk_c9,sk_c7) != sk_c8
| inverse(sk_c8) != sk_c7
| inverse(X2) != sk_c9
| multiply(X2,sk_c9) != sk_c8
| inverse(X1) != sk_c8
| multiply(X1,sk_c8) != sk_c9
| multiply(X0,sk_c8) != sk_c9
| inverse(X0) != sk_c9
| multiply(sk_c8,sk_c9) != sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_38) ).
fof(f79,plain,
! [X2,X3,X0,X1,X4,X5] :
( multiply(X4,sk_c9) != X5
| sk_c9 != inverse(X5)
| inverse(X4) != X5
| sk_c8 != multiply(X3,sk_c7)
| sk_c8 != inverse(X3)
| sk_c8 != multiply(sk_c9,sk_c7)
| sk_c7 != inverse(sk_c8)
| sk_c9 != inverse(X2)
| sk_c8 != multiply(X2,sk_c9)
| sk_c8 != inverse(X1)
| sk_c9 != multiply(X1,sk_c8)
| sk_c9 != multiply(X0,sk_c8)
| inverse(X0) != sk_c9
| multiply(sk_c8,sk_c9) != sk_c7 ),
inference(reorient_equations,[],[f78]) ).
fof(f80,plain,
! [X2,X3,X0,X1,X4] :
( inverse(X4) != multiply(X4,sk_c9)
| sk_c9 != inverse(inverse(X4))
| sk_c8 != multiply(X3,sk_c7)
| sk_c8 != inverse(X3)
| sk_c8 != multiply(sk_c9,sk_c7)
| sk_c7 != inverse(sk_c8)
| sk_c9 != inverse(X2)
| sk_c8 != multiply(X2,sk_c9)
| sk_c8 != inverse(X1)
| sk_c9 != multiply(X1,sk_c8)
| sk_c9 != multiply(X0,sk_c8)
| inverse(X0) != sk_c9
| multiply(sk_c8,sk_c9) != sk_c7 ),
inference(equality_resolution,[],[f79]) ).
tcf(c_90,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_91,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_93,negated_conjecture,
multiply(sk_c8,sk_c9) = sk_c7,
inference(cnf_transformation,[],[f5]) ).
tcf(c_94,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_95,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_96,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_97,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_100,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_101,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_102,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c5 ) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_103,negated_conjecture,
( ( multiply(sk_c3,sk_c9) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_104,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c1,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_105,negated_conjecture,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_106,negated_conjecture,
( ( multiply(sk_c1,sk_c8) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_108,negated_conjecture,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c1,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_111,negated_conjecture,
( ( multiply(sk_c6,sk_c9) = sk_c5 )
| ( multiply(sk_c1,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_112,negated_conjecture,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_115,negated_conjecture,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_118,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c5 ) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c6) = sk_c5 ) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c6,sk_c9) = sk_c5 ) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_130,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c8) != sk_c7 )
| ( inverse(X4) != sk_c8 )
| ( inverse(X3) != sk_c9 )
| ( inverse(X2) != sk_c8 )
| ( inverse(X1) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 )
| ( inverse(inverse(X0)) != sk_c9 )
| ( multiply(X4,sk_c8) != sk_c9 )
| ( multiply(X3,sk_c9) != sk_c8 )
| ( multiply(X2,sk_c7) != sk_c8 )
| ( multiply(X1,sk_c8) != sk_c9 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c8) != sk_c7 )
| ( inverse(X4) != sk_c8 )
| ( inverse(X3) != sk_c9 )
| ( inverse(X2) != sk_c8 )
| ( inverse(X1) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( multiply(X0,sk_c9) != inverse(X0) )
| ( multiply(X1,sk_c8) != sk_c9 )
| ( multiply(X2,sk_c7) != sk_c8 )
| ( multiply(X3,sk_c9) != sk_c8 )
| ( multiply(X4,sk_c8) != sk_c9 )
| ( inverse(inverse(X0)) != sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_130,c_93,c_130]) ).
tcf(c_136,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c8) != sk_c7 )
| ( inverse(X4) != sk_c8 )
| ( inverse(X3) != sk_c9 )
| ( inverse(X2) != sk_c8 )
| ( inverse(X1) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(inverse(X0)) != sk_c9 )
| ( multiply(X4,sk_c8) != sk_c9 )
| ( multiply(X3,sk_c9) != sk_c8 )
| ( multiply(X2,sk_c7) != sk_c8 )
| ( multiply(X1,sk_c8) != sk_c9 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(renaming,[status(thm)],[c_135]) ).
tcf(c_484,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c7) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_136]) ).
tcf(c_485,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_136]) ).
tcf(c_486,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_136]) ).
tcf(c_487,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_136]) ).
tcf(c_488,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(inverse(X0)) != sk_c9 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_136]) ).
tcf(c_489,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c8) != sk_c7 )
| ( multiply(sk_c9,sk_c7) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_136]) ).
tcf(c_490,definition,
iPr_def_15 = multiply(sk_c9,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_491,definition,
iPr_def_16 = inverse(sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_492,definition,
iPr_def_17 = multiply(sk_c6,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_493,definition,
iPr_def_18 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_494,definition,
iPr_def_19 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_495,definition,
iPr_def_20 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_496,definition,
iPr_def_21 = multiply(sk_c4,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_497,definition,
iPr_def_22 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_498,definition,
iPr_def_23 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_499,definition,
iPr_def_24 = multiply(sk_c3,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_500,definition,
iPr_def_25 = multiply(sk_c2,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_501,definition,
iPr_def_26 = multiply(sk_c1,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_502,definition,
iPr_def_27 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_503,definition,
iPr_def_28 = multiply(sk_c8,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_504,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_c8 ) ),
inference(demodulation,[status(thm)],[c_489,c_491,c_490]) ).
tcf(c_505,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(inverse(X0)) != sk_c9 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_488]) ).
tcf(c_506,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_487]) ).
tcf(c_507,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_486]) ).
tcf(c_508,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_485]) ).
tcf(c_509,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c7) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_484]) ).
tcf(c_510,negated_conjecture,
( ( iPr_def_18 = sk_c8 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_129,c_493,c_492]) ).
tcf(c_511,negated_conjecture,
( ( iPr_def_19 = sk_c9 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_128,c_494]) ).
tcf(c_512,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_127,c_495]) ).
tcf(c_513,negated_conjecture,
( ( iPr_def_21 = sk_c8 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_126,c_496]) ).
tcf(c_514,negated_conjecture,
( ( iPr_def_22 = sk_c8 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_125,c_497]) ).
tcf(c_515,negated_conjecture,
( ( iPr_def_18 = sk_c8 )
| ( iPr_def_15 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_516,negated_conjecture,
( ( iPr_def_18 = sk_c8 )
| ( iPr_def_16 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_517,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_122,c_498]) ).
tcf(c_518,negated_conjecture,
( ( iPr_def_24 = sk_c8 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_121,c_499]) ).
tcf(c_519,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_120,c_500]) ).
tcf(c_521,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_20 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_118]) ).
tcf(c_524,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_15 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_115]) ).
tcf(c_525,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_16 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_526,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_23 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_527,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_24 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_528,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_111,c_501]) ).
tcf(c_530,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_20 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_531,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_21 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_532,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_22 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_533,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_15 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_534,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_16 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_535,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_23 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_104]) ).
tcf(c_536,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_24 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_103]) ).
tcf(c_537,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_102,c_502]) ).
tcf(c_538,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_101]) ).
tcf(c_539,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_20 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_100]) ).
tcf(c_542,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_15 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_97]) ).
tcf(c_543,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_16 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_96]) ).
tcf(c_544,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_23 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_95]) ).
tcf(c_545,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_24 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_94]) ).
tcf(c_546,negated_conjecture,
iPr_def_28 = sk_c7,
inference(demodulation,[status(thm)],[c_93,c_503]) ).
tcf(c_547,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_548,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_550,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_552,plain,
( ( inverse(sk_c8) = inverse(sk_c8) )
| ( sk_c8 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_550]) ).
tcf(c_553,plain,
sk_c8 = sk_c8,
inference(instantiation,[status(thm)],[c_547]) ).
tcf(c_811,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c8 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_510,c_512]) ).
tcf(c_841,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( sk_c8 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_516,c_546]) ).
tcf(c_852,plain,
multiply(sk_c9,iPr_def_28) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_490,c_546]) ).
tcf(c_942,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c9 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_521,c_519]) ).
tcf(c_990,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(iPr_def_25,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_524,c_852]) ).
tcf(c_1004,plain,
( ( sk_c8 = iPr_def_18 )
| ( multiply(sk_c6,iPr_def_23) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_517,c_492]) ).
tcf(c_1018,plain,
multiply(sk_c4,iPr_def_28) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_496,c_546]) ).
tcf(c_1023,plain,
( ( sk_c8 = iPr_def_18 )
| ( multiply(sk_c3,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_517,c_499]) ).
tcf(c_1037,plain,
( ( sk_c8 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_518,c_500]) ).
tcf(c_1041,plain,
( ( sk_c8 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_21) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_513,c_500]) ).
tcf(c_1067,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c8 )
| ( sk_c8 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_548]) ).
tcf(c_1069,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_547]) ).
tcf(c_1072,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_548]) ).
tcf(c_1075,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( multiply(iPr_def_18,sk_c9) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_841,c_503]) ).
tcf(c_1076,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(iPr_def_18,sk_c9) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_515,c_503]) ).
tcf(c_1077,plain,
( ( sk_c8 = iPr_def_18 )
| ( multiply(iPr_def_22,sk_c9) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_514,c_503]) ).
tcf(c_1108,plain,
! [X0: $i,X1: $i] :
( ( sk_c8 = inverse(X0) )
| ( sk_c8 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_548]) ).
tcf(c_1114,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_1125,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_548]) ).
tcf(c_1127,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_16 )
| ( iPr_def_16 != inverse(sk_c8) )
| ( inverse(X0) != inverse(sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1114]) ).
tcf(c_1128,plain,
( ( inverse(sk_c8) = iPr_def_16 )
| ( iPr_def_16 != inverse(sk_c8) )
| ( inverse(sk_c8) != inverse(sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1127]) ).
tcf(c_1129,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_18 )
| ( iPr_def_18 != inverse(sk_c2) )
| ( inverse(X0) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1114]) ).
tcf(c_1139,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_27 )
| ( iPr_def_27 != inverse(sk_c1) )
| ( inverse(X0) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_1114]) ).
tcf(c_1142,plain,
multiply(iPr_def_27,sk_c1) = identity,
inference(superposition,[status(thm)],[c_502,c_91]) ).
tcf(c_1143,plain,
multiply(iPr_def_23,sk_c3) = identity,
inference(superposition,[status(thm)],[c_498,c_91]) ).
tcf(c_1144,plain,
multiply(iPr_def_16,sk_c8) = identity,
inference(superposition,[status(thm)],[c_491,c_91]) ).
tcf(c_1145,plain,
multiply(iPr_def_22,sk_c4) = identity,
inference(superposition,[status(thm)],[c_497,c_91]) ).
tcf(c_1146,plain,
multiply(iPr_def_20,sk_c6) = identity,
inference(superposition,[status(thm)],[c_495,c_91]) ).
tcf(c_1147,plain,
multiply(iPr_def_19,sk_c5) = identity,
inference(superposition,[status(thm)],[c_494,c_91]) ).
tcf(c_1148,plain,
multiply(iPr_def_18,sk_c2) = identity,
inference(superposition,[status(thm)],[c_493,c_91]) ).
tcf(c_1149,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( sk_c9 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_525,c_546]) ).
tcf(c_1178,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c8,iPr_def_25) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_526,c_503]) ).
tcf(c_1182,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_25,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_526,c_852]) ).
tcf(c_1200,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_1210,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(sk_c8,iPr_def_25) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_527,c_503]) ).
tcf(c_1212,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(sk_c6,iPr_def_25) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_527,c_492]) ).
tcf(c_1214,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_25,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_527,c_852]) ).
tcf(c_1230,plain,
! [X0: $i] :
( ( sk_c8 = inverse(X0) )
| ( sk_c8 != iPr_def_18 )
| ( inverse(X0) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1108]) ).
tcf(c_1231,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_18 )
| ( inverse(X0) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_1236,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_19 )
| ( inverse(X0) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_1322,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c9 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_530,c_528]) ).
tcf(c_1396,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1125]) ).
tcf(c_1479,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(sk_c8,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_533,c_503]) ).
tcf(c_1487,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(iPr_def_26,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_533,c_852]) ).
tcf(c_1529,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( sk_c9 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_534,c_546]) ).
tcf(c_1568,plain,
! [X0: $i] :
( ( sk_c8 = iPr_def_27 )
| ( iPr_def_27 != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_548]) ).
tcf(c_1576,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_16 )
| ( iPr_def_16 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_548]) ).
tcf(c_1594,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c8,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_535,c_503]) ).
tcf(c_1602,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_26,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_535,c_852]) ).
tcf(c_1642,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(sk_c8,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_536,c_503]) ).
tcf(c_1644,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(sk_c6,iPr_def_26) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_536,c_492]) ).
tcf(c_1650,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_26,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_536,c_852]) ).
tcf(c_1785,plain,
( ( sk_c9 = iPr_def_19 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_538,c_492]) ).
tcf(c_1828,plain,
( ( inverse(sk_c2) = iPr_def_18 )
| ( iPr_def_18 != inverse(sk_c2) )
| ( inverse(sk_c2) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1129]) ).
tcf(c_1829,plain,
inverse(sk_c2) = inverse(sk_c2),
inference(instantiation,[status(thm)],[c_1069]) ).
tcf(c_1850,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c9 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_539,c_537]) ).
tcf(c_1853,plain,
( ( sk_c9 = iPr_def_27 )
| ( inverse(iPr_def_20) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_539,c_494]) ).
tcf(c_2118,plain,
( ( inverse(sk_c1) = iPr_def_27 )
| ( iPr_def_27 != inverse(sk_c1) )
| ( inverse(sk_c1) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_1139]) ).
tcf(c_2119,plain,
inverse(sk_c1) = inverse(sk_c1),
inference(instantiation,[status(thm)],[c_1069]) ).
tcf(c_2133,plain,
iPr_def_16 = iPr_def_16,
inference(instantiation,[status(thm)],[c_547]) ).
tcf(c_2168,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_542,c_492]) ).
tcf(c_2261,plain,
! [X0: $i] :
( ( iPr_def_27 = inverse(X0) )
| ( iPr_def_27 != inverse(sk_c1) )
| ( inverse(X0) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_1396]) ).
tcf(c_2266,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( sk_c9 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_543,c_546]) ).
tcf(c_2364,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_544,c_492]) ).
tcf(c_2370,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_544,c_852]) ).
tcf(c_2451,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(sk_c8,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_545,c_503]) ).
tcf(c_2453,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_545,c_492]) ).
tcf(c_2484,plain,
( ( sk_c8 = inverse(sk_c2) )
| ( sk_c8 != iPr_def_18 )
| ( inverse(sk_c2) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1230]) ).
tcf(c_2485,plain,
! [X0: $i] :
( ( inverse(sk_c2) = X0 )
| ( X0 != iPr_def_18 )
| ( inverse(sk_c2) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1231]) ).
tcf(c_2507,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(iPr_def_18,sk_c9) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_811,c_503]) ).
tcf(c_2511,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( inverse(iPr_def_18) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_811,c_491]) ).
tcf(c_2539,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c9,X0)) = multiply(iPr_def_28,X0),
inference(superposition,[status(thm)],[c_503,c_92]) ).
tcf(c_2540,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c9,X0)) = multiply(iPr_def_24,X0),
inference(superposition,[status(thm)],[c_499,c_92]) ).
tcf(c_2542,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c8,X0)) = multiply(iPr_def_26,X0),
inference(superposition,[status(thm)],[c_501,c_92]) ).
tcf(c_2543,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c8,X0)) = multiply(iPr_def_25,X0),
inference(superposition,[status(thm)],[c_500,c_92]) ).
tcf(c_2545,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_91,c_92]) ).
tcf(c_2549,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1142,c_92]) ).
tcf(c_2550,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1143,c_92]) ).
tcf(c_2551,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c8,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1144,c_92]) ).
tcf(c_2552,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1145,c_92]) ).
tcf(c_2553,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1146,c_92]) ).
tcf(c_2554,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1147,c_92]) ).
tcf(c_2556,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2554,c_90]) ).
tcf(c_2557,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2553,c_90]) ).
tcf(c_2558,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2552,c_90]) ).
tcf(c_2559,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c8,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2551,c_90]) ).
tcf(c_2560,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2550,c_90]) ).
tcf(c_2561,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2549,c_90]) ).
tcf(c_2667,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1148,c_92]) ).
tcf(c_2668,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2667,c_90]) ).
tcf(c_2717,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_548]) ).
tcf(c_3169,plain,
! [X0: $i] :
( ( X0 = iPr_def_16 )
| ( iPr_def_16 != sk_c7 )
| ( X0 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1576]) ).
tcf(c_3215,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_16 != iPr_def_28 )
| ( sk_c8 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_504,c_546]) ).
tcf(c_3241,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_17 = iPr_def_20 )
| ( iPr_def_16 != iPr_def_28 )
| ( iPr_def_15 != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_811,c_3215]) ).
tcf(c_3339,plain,
( ~ iPr_def_13
| ( sk_c9 != iPr_def_25 )
| ( inverse(sk_c2) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_500,c_506]) ).
tcf(c_3343,plain,
( ~ iPr_def_13
| ( sk_c9 != identity )
| ( inverse(iPr_def_16) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_1144,c_506]) ).
tcf(c_3360,plain,
( ~ iPr_def_13
| ( sk_c9 != iPr_def_25 )
| ( sk_c8 != iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_3339,c_493]) ).
tcf(c_3463,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_26 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_501,c_507]) ).
tcf(c_3465,plain,
( ~ iPr_def_12
| ( sk_c8 != sk_c9 )
| ( inverse(identity) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_90,c_507]) ).
tcf(c_3489,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_27 )
| ( sk_c9 != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_3463,c_502]) ).
tcf(c_3598,plain,
( ~ iPr_def_11
| ( sk_c8 != iPr_def_24 )
| ( inverse(sk_c3) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_499,c_508]) ).
tcf(c_3600,plain,
( ~ iPr_def_11
| ( sk_c8 != sk_c9 )
| ( inverse(identity) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_90,c_508]) ).
tcf(c_3635,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_23 )
| ( sk_c8 != iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_3598,c_498]) ).
tcf(c_3850,plain,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,iPr_def_28) != sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_509,c_546]) ).
tcf(c_3861,plain,
( ~ iPr_def_10
| ( sk_c8 != identity )
| ( inverse(inverse(iPr_def_28)) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_91,c_3850]) ).
tcf(c_3863,plain,
( ~ iPr_def_10
| ( sk_c8 != iPr_def_15 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_852,c_3850]) ).
tcf(c_3864,plain,
( ~ iPr_def_10
| ( sk_c8 != iPr_def_21 )
| ( inverse(sk_c4) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_1018,c_3850]) ).
tcf(c_3865,plain,
( ~ iPr_def_10
| ( sk_c8 != iPr_def_22 )
| ( sk_c8 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_3864,c_497]) ).
tcf(c_3901,plain,
( ~ iPr_def_14
| ( inverse(sk_c6) != iPr_def_17 )
| ( inverse(inverse(sk_c6)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_492,c_505]) ).
tcf(c_3902,plain,
( ~ iPr_def_14
| ( inverse(identity) != sk_c9 )
| ( inverse(inverse(identity)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_90,c_505]) ).
tcf(c_3933,plain,
( ~ iPr_def_14
| ( iPr_def_17 != iPr_def_20 )
| ( inverse(iPr_def_20) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_3901,c_495]) ).
tcf(c_4206,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_17 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_1322,c_942]) ).
tcf(c_4372,plain,
! [X0: $i] :
( ( sk_c8 = sk_c9 )
| ( sk_c9 != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_548]) ).
tcf(c_4388,plain,
( ( iPr_def_28 = iPr_def_16 )
| ( iPr_def_28 != sk_c7 )
| ( iPr_def_16 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_3169]) ).
tcf(c_5141,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_18 )
| ( iPr_def_18 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_548]) ).
tcf(c_5954,plain,
! [X0: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != sk_c7 )
| ( X0 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_2717]) ).
tcf(c_5956,plain,
! [X0: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_2717]) ).
tcf(c_7548,plain,
multiply(iPr_def_20,iPr_def_17) = sk_c9,
inference(superposition,[status(thm)],[c_492,c_2557]) ).
tcf(c_7551,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(iPr_def_17,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_7548,c_92]) ).
tcf(c_7557,plain,
multiply(iPr_def_22,iPr_def_21) = iPr_def_28,
inference(superposition,[status(thm)],[c_1018,c_2558]) ).
tcf(c_7635,plain,
multiply(iPr_def_16,iPr_def_28) = sk_c9,
inference(superposition,[status(thm)],[c_503,c_2559]) ).
tcf(c_7920,plain,
( ~ iPr_def_10
| ( sk_c8 != sk_c9 )
| ( inverse(iPr_def_16) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_7635,c_3850]) ).
tcf(c_7959,plain,
multiply(iPr_def_23,iPr_def_24) = sk_c9,
inference(superposition,[status(thm)],[c_499,c_2560]) ).
tcf(c_7964,plain,
multiply(iPr_def_27,iPr_def_26) = sk_c8,
inference(superposition,[status(thm)],[c_501,c_2561]) ).
tcf(c_7969,plain,
multiply(iPr_def_18,iPr_def_25) = sk_c8,
inference(superposition,[status(thm)],[c_500,c_2668]) ).
tcf(c_8097,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(iPr_def_25,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_7969,c_92]) ).
tcf(c_8240,plain,
( ( sk_c8 = iPr_def_18 )
| ( multiply(iPr_def_20,iPr_def_17) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1004,c_2557]) ).
tcf(c_8241,plain,
( ( sk_c9 = iPr_def_23 )
| ( sk_c8 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_8240,c_7548]) ).
tcf(c_8467,plain,
( ( sk_c8 = iPr_def_18 )
| ( multiply(iPr_def_18,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1037,c_2668]) ).
tcf(c_8468,plain,
( ( sk_c8 = iPr_def_24 )
| ( sk_c8 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_8467,c_7969]) ).
tcf(c_8589,plain,
( ( sk_c8 = iPr_def_18 )
| ( multiply(iPr_def_18,iPr_def_25) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_1041,c_2668]) ).
tcf(c_8590,plain,
( ( sk_c8 = iPr_def_21 )
| ( sk_c8 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_8589,c_7969]) ).
tcf(c_8720,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(iPr_def_18,iPr_def_25) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_524,c_1076]) ).
tcf(c_8729,plain,
( ( sk_c8 = iPr_def_28 )
| ( sk_c8 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_8720,c_7969]) ).
tcf(c_8975,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c8 = iPr_def_15 )
| ( iPr_def_16 != iPr_def_28 )
| ( iPr_def_15 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_8729,c_3215]) ).
tcf(c_8981,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(iPr_def_16,iPr_def_28) = identity ) ),
inference(superposition,[status(thm)],[c_8729,c_1144]) ).
tcf(c_9001,plain,
( ( sk_c9 = identity )
| ( sk_c8 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_8981,c_7635]) ).
tcf(c_9568,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_28 )
| ( iPr_def_28 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1200]) ).
tcf(c_9569,plain,
( ( inverse(sk_c8) = iPr_def_28 )
| ( iPr_def_28 != iPr_def_16 )
| ( inverse(sk_c8) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_9568]) ).
tcf(c_9981,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( iPr_def_28 != sk_c7 )
| ( iPr_def_16 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_5954]) ).
tcf(c_10164,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_16,iPr_def_28) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1178,c_2559]) ).
tcf(c_10165,plain,
( ( sk_c9 = iPr_def_25 )
| ( sk_c9 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_10164,c_7635]) ).
tcf(c_10249,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c9 )
| ( sk_c9 != iPr_def_19 )
| ( inverse(X0) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1236]) ).
tcf(c_10428,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_16,iPr_def_28) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1210,c_2559]) ).
tcf(c_10429,plain,
( ( sk_c9 = iPr_def_25 )
| ( sk_c8 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_10428,c_7635]) ).
tcf(c_11270,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( multiply(iPr_def_18,iPr_def_25) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_1149,c_1075]) ).
tcf(c_11280,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( sk_c8 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_11270,c_7969]) ).
tcf(c_11393,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( multiply(iPr_def_16,iPr_def_28) = identity ) ),
inference(superposition,[status(thm)],[c_11280,c_1144]) ).
tcf(c_11413,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( sk_c9 = identity ) ),
inference(light_normalisation,[status(thm)],[c_11393,c_7635]) ).
tcf(c_12156,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(iPr_def_16,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1479,c_2559]) ).
tcf(c_12157,plain,
( ( sk_c9 = iPr_def_26 )
| ( sk_c8 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_12156,c_7635]) ).
tcf(c_12263,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_16,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1594,c_2559]) ).
tcf(c_12264,plain,
( ( sk_c9 = iPr_def_26 )
| ( sk_c9 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_12263,c_7635]) ).
tcf(c_12810,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_16,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1642,c_2559]) ).
tcf(c_12811,plain,
( ( sk_c9 = iPr_def_26 )
| ( sk_c8 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_12810,c_7635]) ).
tcf(c_13377,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(identity,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_9001,c_852]) ).
tcf(c_15450,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( identity = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_11413,c_2266]) ).
tcf(c_15457,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_11413,c_1529]) ).
tcf(c_16229,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_28 )
| ( multiply(iPr_def_27,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_15450,c_90]) ).
tcf(c_16239,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_28 )
| ( multiply(iPr_def_26,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_15457,c_90]) ).
tcf(c_16893,plain,
( ( sk_c9 = iPr_def_23 )
| ~ iPr_def_10
| ( sk_c8 != iPr_def_15 )
| ( inverse(iPr_def_27) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_2370,c_3850]) ).
tcf(c_17095,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_16,iPr_def_28) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2451,c_2559]) ).
tcf(c_17096,plain,
( ( sk_c9 = iPr_def_27 )
| ( sk_c8 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_17095,c_7635]) ).
tcf(c_17809,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(iPr_def_18,iPr_def_25) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_942,c_2507]) ).
tcf(c_17836,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c8 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_17809,c_7969]) ).
tcf(c_18042,plain,
multiply(sk_c8,iPr_def_15) = multiply(iPr_def_28,iPr_def_28),
inference(superposition,[status(thm)],[c_852,c_2539]) ).
tcf(c_18530,plain,
( ( iPr_def_18 = iPr_def_28 )
| ( iPr_def_17 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_17836,c_811]) ).
tcf(c_18531,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(iPr_def_16,iPr_def_28) = identity ) ),
inference(superposition,[status(thm)],[c_17836,c_1144]) ).
tcf(c_18551,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c9 = identity ) ),
inference(light_normalisation,[status(thm)],[c_18531,c_7635]) ).
tcf(c_19275,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( identity = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_18551,c_1850]) ).
tcf(c_19491,plain,
multiply(sk_c3,iPr_def_15) = multiply(iPr_def_24,iPr_def_28),
inference(superposition,[status(thm)],[c_852,c_2540]) ).
tcf(c_19778,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(iPr_def_27,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_19275,c_90]) ).
tcf(c_20514,plain,
( ( sk_c8 = iPr_def_27 )
| ( iPr_def_27 != inverse(sk_c2) )
| ( sk_c8 != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1568]) ).
tcf(c_20769,plain,
( ( inverse(sk_c2) = inverse(sk_c1) )
| ( inverse(sk_c2) != iPr_def_18 )
| ( inverse(sk_c1) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_2485]) ).
tcf(c_20771,plain,
( ( iPr_def_27 = inverse(sk_c2) )
| ( iPr_def_27 != inverse(sk_c1) )
| ( inverse(sk_c2) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_2261]) ).
tcf(c_21816,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_2545,c_90]) ).
tcf(c_21866,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_90,c_21816]) ).
tcf(c_21867,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_91,c_21816]) ).
tcf(c_21869,plain,
multiply(inverse(sk_c9),iPr_def_15) = iPr_def_28,
inference(superposition,[status(thm)],[c_852,c_21816]) ).
tcf(c_22046,plain,
! [X0: $i] : multiply(inverse(iPr_def_27),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_2561,c_21816]) ).
tcf(c_22047,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_2560,c_21816]) ).
tcf(c_22048,plain,
! [X0: $i] : multiply(inverse(iPr_def_16),X0) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_2559,c_21816]) ).
tcf(c_22049,plain,
! [X0: $i] : multiply(inverse(iPr_def_22),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_2558,c_21816]) ).
tcf(c_22051,plain,
! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_2556,c_21816]) ).
tcf(c_22052,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_2668,c_21816]) ).
tcf(c_22073,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_21816,c_21816]) ).
tcf(c_22980,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_21867,c_22073]) ).
tcf(c_22986,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(X0,iPr_def_27) = X0 ) ),
inference(superposition,[status(thm)],[c_19275,c_22980]) ).
tcf(c_23008,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_22980,c_21866]) ).
tcf(c_23033,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(sk_c8,iPr_def_27) = sk_c8 ) ),
inference(instantiation,[status(thm)],[c_22986]) ).
tcf(c_23042,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = iPr_def_18 )
| ( iPr_def_18 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_5141]) ).
tcf(c_23881,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_27,X0)) = X0,
inference(superposition,[status(thm)],[c_22046,c_21816]) ).
tcf(c_23883,plain,
multiply(sk_c1,identity) = inverse(iPr_def_27),
inference(superposition,[status(thm)],[c_22046,c_22980]) ).
tcf(c_24195,plain,
inverse(iPr_def_27) = sk_c1,
inference(demodulation,[status(thm)],[c_23883,c_22980]) ).
tcf(c_24458,plain,
multiply(sk_c1,sk_c8) = iPr_def_26,
inference(superposition,[status(thm)],[c_7964,c_23881]) ).
tcf(c_24796,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_23)) != sk_c9 )
| ( multiply(sk_c3,sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_22047,c_507]) ).
tcf(c_24798,plain,
multiply(sk_c3,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_22047,c_91]) ).
tcf(c_24802,plain,
( ~ iPr_def_11
| ( inverse(inverse(iPr_def_23)) != sk_c9 )
| ( multiply(sk_c3,sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_22047,c_508]) ).
tcf(c_24803,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_23,X0)) = X0,
inference(superposition,[status(thm)],[c_22047,c_21816]) ).
tcf(c_24805,plain,
multiply(sk_c3,identity) = inverse(iPr_def_23),
inference(superposition,[status(thm)],[c_22047,c_22980]) ).
tcf(c_24809,plain,
( ~ iPr_def_11
| ( sk_c8 != iPr_def_24 )
| ( inverse(inverse(iPr_def_23)) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_24802,c_499]) ).
tcf(c_24824,plain,
( ( identity = iPr_def_24 )
| ( sk_c8 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_1023,c_24798]) ).
tcf(c_24936,plain,
multiply(iPr_def_23,identity) = iPr_def_23,
inference(superposition,[status(thm)],[c_24798,c_2560]) ).
tcf(c_24939,plain,
inverse(iPr_def_23) = sk_c3,
inference(demodulation,[status(thm)],[c_24805,c_22980]) ).
tcf(c_25095,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( identity = iPr_def_24 )
| ( iPr_def_16 != iPr_def_28 )
| ( iPr_def_15 != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_24824,c_3215]) ).
tcf(c_25849,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm)],[c_1143,c_24803]) ).
tcf(c_25850,plain,
multiply(sk_c3,sk_c9) = iPr_def_24,
inference(superposition,[status(thm)],[c_7959,c_24803]) ).
tcf(c_25927,plain,
multiply(sk_c8,iPr_def_16) = identity,
inference(superposition,[status(thm)],[c_22048,c_91]) ).
tcf(c_25932,plain,
! [X0: $i] : multiply(sk_c8,multiply(iPr_def_16,X0)) = X0,
inference(superposition,[status(thm)],[c_22048,c_21816]) ).
tcf(c_25934,plain,
multiply(sk_c8,identity) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_22048,c_22980]) ).
tcf(c_26006,plain,
multiply(sk_c2,identity) = multiply(iPr_def_25,iPr_def_16),
inference(superposition,[status(thm)],[c_25927,c_2543]) ).
tcf(c_26007,plain,
multiply(sk_c1,identity) = multiply(iPr_def_26,iPr_def_16),
inference(superposition,[status(thm)],[c_25927,c_2542]) ).
tcf(c_26008,plain,
multiply(iPr_def_16,identity) = iPr_def_16,
inference(superposition,[status(thm)],[c_25927,c_2559]) ).
tcf(c_26602,plain,
inverse(iPr_def_16) = sk_c8,
inference(demodulation,[status(thm)],[c_25934,c_22980]) ).
tcf(c_26640,plain,
multiply(sk_c8,identity) = sk_c8,
inference(superposition,[status(thm)],[c_1144,c_25932]) ).
tcf(c_27052,plain,
multiply(iPr_def_25,iPr_def_16) = sk_c2,
inference(demodulation,[status(thm)],[c_26006,c_22980]) ).
tcf(c_27206,plain,
multiply(iPr_def_26,iPr_def_16) = sk_c1,
inference(demodulation,[status(thm)],[c_26007,c_22980]) ).
tcf(c_27214,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(iPr_def_25,iPr_def_16) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_4206,c_27206]) ).
tcf(c_27215,plain,
multiply(inverse(iPr_def_26),sk_c1) = iPr_def_16,
inference(superposition,[status(thm)],[c_27206,c_21816]) ).
tcf(c_27217,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c1 = sk_c2 ) ),
inference(light_normalisation,[status(thm)],[c_27214,c_27052]) ).
tcf(c_27263,plain,
multiply(inverse(inverse(iPr_def_26)),iPr_def_16) = sk_c1,
inference(superposition,[status(thm)],[c_27215,c_21816]) ).
tcf(c_31126,plain,
( ( sk_c8 = sk_c9 )
| ( sk_c9 != iPr_def_27 )
| ( sk_c8 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_4372]) ).
tcf(c_32748,plain,
( ~ iPr_def_13
| ( inverse(inverse(iPr_def_22)) != sk_c8 )
| ( multiply(sk_c4,sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_22049,c_506]) ).
tcf(c_32749,plain,
multiply(sk_c4,iPr_def_22) = identity,
inference(superposition,[status(thm)],[c_22049,c_91]) ).
tcf(c_32754,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_22,X0)) = X0,
inference(superposition,[status(thm)],[c_22049,c_21816]) ).
tcf(c_32756,plain,
multiply(sk_c4,identity) = inverse(iPr_def_22),
inference(superposition,[status(thm)],[c_22049,c_22980]) ).
tcf(c_32824,plain,
inverse(iPr_def_22) = sk_c4,
inference(demodulation,[status(thm)],[c_32756,c_22980]) ).
tcf(c_33059,plain,
( ( sk_c8 = iPr_def_18 )
| ( multiply(sk_c4,iPr_def_28) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_1077,c_32754]) ).
tcf(c_33077,plain,
( ( sk_c9 = iPr_def_21 )
| ( sk_c8 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_33059,c_1018]) ).
tcf(c_38306,plain,
( ( inverse(sk_c1) = iPr_def_18 )
| ( iPr_def_18 != iPr_def_27 )
| ( inverse(sk_c1) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_23042]) ).
tcf(c_40348,plain,
multiply(sk_c9,identity) = multiply(iPr_def_20,iPr_def_17),
inference(superposition,[status(thm)],[c_22980,c_7551]) ).
tcf(c_40355,plain,
multiply(sk_c9,identity) = sk_c9,
inference(light_normalisation,[status(thm)],[c_40348,c_7548]) ).
tcf(c_42507,plain,
multiply(sk_c8,identity) = multiply(iPr_def_18,iPr_def_25),
inference(superposition,[status(thm)],[c_22980,c_8097]) ).
tcf(c_45951,plain,
( ( iPr_def_16 = sk_c7 )
| ( iPr_def_16 != iPr_def_16 )
| ( sk_c7 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_5956]) ).
tcf(c_48206,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c8 )
| ( sk_c8 != iPr_def_28 )
| ( inverse(X0) != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_1067]) ).
tcf(c_48207,plain,
( ( inverse(sk_c8) = sk_c8 )
| ( sk_c8 != iPr_def_28 )
| ( inverse(sk_c8) != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_48206]) ).
tcf(c_50071,plain,
( ( inverse(iPr_def_20) = sk_c9 )
| ( sk_c9 != iPr_def_19 )
| ( inverse(iPr_def_20) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_10249]) ).
tcf(c_52367,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_19)) != sk_c9 )
| ( multiply(sk_c5,sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_22051,c_507]) ).
tcf(c_52369,plain,
multiply(sk_c5,iPr_def_19) = identity,
inference(superposition,[status(thm)],[c_22051,c_91]) ).
tcf(c_52376,plain,
multiply(sk_c5,identity) = inverse(iPr_def_19),
inference(superposition,[status(thm)],[c_22051,c_22980]) ).
tcf(c_52416,plain,
inverse(iPr_def_19) = sk_c5,
inference(demodulation,[status(thm)],[c_52376,c_22980]) ).
tcf(c_53381,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( sk_c8 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_13377,c_90]) ).
tcf(c_53460,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( iPr_def_15 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_53381,c_17836]) ).
tcf(c_54208,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_53460,c_18530]) ).
tcf(c_54960,plain,
multiply(sk_c2,iPr_def_18) = identity,
inference(superposition,[status(thm)],[c_22052,c_91]) ).
tcf(c_54965,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_18,X0)) = X0,
inference(superposition,[status(thm)],[c_22052,c_21816]) ).
tcf(c_54967,plain,
multiply(sk_c2,identity) = inverse(iPr_def_18),
inference(superposition,[status(thm)],[c_22052,c_22980]) ).
tcf(c_55577,plain,
inverse(iPr_def_18) = sk_c2,
inference(demodulation,[status(thm)],[c_54967,c_22980]) ).
tcf(c_55586,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c2 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_2511,c_55577]) ).
tcf(c_55629,plain,
multiply(sk_c2,sk_c8) = iPr_def_25,
inference(superposition,[status(thm)],[c_7969,c_54965]) ).
tcf(c_57546,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c1 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_55586,c_27217]) ).
tcf(c_59313,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( inverse(iPr_def_16) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_57546,c_502]) ).
tcf(c_59314,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c8 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_59313,c_26602]) ).
tcf(c_61289,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( sk_c1 = identity ) ),
inference(superposition,[status(thm)],[c_16229,c_1142]) ).
tcf(c_63476,plain,
( ( iPr_def_27 = iPr_def_28 )
| ( iPr_def_17 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_59314,c_17836]) ).
tcf(c_65336,plain,
( ~ iPr_def_13
| ( sk_c9 != identity ) ),
inference(ground_joinability,[status(thm)],[c_3343,c_26602]) ).
tcf(c_65347,plain,
( ( iPr_def_17 = iPr_def_20 )
| ~ iPr_def_13 ),
inference(superposition,[status(thm)],[c_18551,c_65336]) ).
tcf(c_65363,plain,
( ( sk_c8 = iPr_def_15 )
| ~ iPr_def_13 ),
inference(superposition,[status(thm)],[c_9001,c_65336]) ).
tcf(c_65379,plain,
( ( sk_c8 = iPr_def_24 )
| ~ iPr_def_13
| ( identity != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_545,c_65336]) ).
tcf(c_65380,plain,
( ( sk_c9 = iPr_def_23 )
| ~ iPr_def_13
| ( identity != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_544,c_65336]) ).
tcf(c_65598,plain,
( ( sk_c8 = iPr_def_24 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_65379,c_3360,c_8468,c_10429]) ).
tcf(c_65626,plain,
( ( sk_c9 = iPr_def_23 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_65380,c_3360,c_8241,c_10165]) ).
tcf(c_65687,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( sk_c1 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_16239,c_27206]) ).
tcf(c_67661,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_20 )
| ~ iPr_def_10
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,iPr_def_27) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_63476,c_3850]) ).
tcf(c_67775,plain,
( ( iPr_def_17 = iPr_def_20 )
| ~ iPr_def_10
| ( inverse(sk_c8) != sk_c8 )
| ( multiply(sk_c8,iPr_def_27) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_67661]) ).
tcf(c_68261,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( identity = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_61289,c_65687]) ).
tcf(c_68647,plain,
( ~ iPr_def_12
| ( sk_c9 != identity )
| ( sk_c8 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_3465,c_23008]) ).
tcf(c_68686,plain,
( ( iPr_def_17 = iPr_def_20 )
| ~ iPr_def_12
| ( sk_c9 != identity )
| ( sk_c8 != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1850,c_68647]) ).
tcf(c_70405,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( inverse(iPr_def_16) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_68261,c_23008]) ).
tcf(c_70420,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( sk_c8 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_70405,c_26602]) ).
tcf(c_71222,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( sk_c8 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_3600,c_23008]) ).
tcf(c_71261,plain,
( ( iPr_def_17 = iPr_def_20 )
| ~ iPr_def_11
| ( sk_c9 != identity )
| ( sk_c8 != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1850,c_71222]) ).
tcf(c_71275,plain,
( ( sk_c8 = iPr_def_24 )
| ~ iPr_def_11
| ( sk_c9 != identity )
| ( sk_c8 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_536,c_71222]) ).
tcf(c_74160,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c1 = identity ) ),
inference(superposition,[status(thm)],[c_19778,c_1142]) ).
tcf(c_74171,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c8 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_19778,c_7964]) ).
tcf(c_75015,plain,
iPr_def_16 = iPr_def_28,
inference(superposition,[status(thm)],[c_70420,c_11280]) ).
tcf(c_75060,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c8 != iPr_def_15 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3215,c_75015]) ).
tcf(c_75108,plain,
multiply(inverse(sk_c9),iPr_def_15) = iPr_def_16,
inference(demodulation,[status(thm)],[c_21869,c_75015]) ).
tcf(c_75126,plain,
multiply(sk_c3,iPr_def_15) = multiply(iPr_def_24,iPr_def_16),
inference(demodulation,[status(thm)],[c_19491,c_75015]) ).
tcf(c_75129,plain,
multiply(sk_c8,iPr_def_15) = multiply(iPr_def_16,iPr_def_16),
inference(demodulation,[status(thm)],[c_18042,c_75015]) ).
tcf(c_75153,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_26,iPr_def_16) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1650,c_75015]) ).
tcf(c_75155,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_26,iPr_def_16) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1602,c_75015]) ).
tcf(c_75157,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(iPr_def_26,iPr_def_16) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1487,c_75015]) ).
tcf(c_75167,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_25,iPr_def_16) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1214,c_75015]) ).
tcf(c_75168,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(sk_c8,iPr_def_25) = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1210,c_75015]) ).
tcf(c_75169,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_25,iPr_def_16) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1182,c_75015]) ).
tcf(c_75170,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c8,iPr_def_25) = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1178,c_75015]) ).
tcf(c_75183,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(iPr_def_25,iPr_def_16) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_990,c_75015]) ).
tcf(c_75188,plain,
multiply(iPr_def_16,iPr_def_16) = sk_c9,
inference(demodulation,[status(thm)],[c_7635,c_75015]) ).
tcf(c_75189,plain,
multiply(iPr_def_22,iPr_def_21) = iPr_def_16,
inference(demodulation,[status(thm)],[c_7557,c_75015]) ).
tcf(c_75192,plain,
multiply(sk_c8,sk_c9) = iPr_def_16,
inference(demodulation,[status(thm)],[c_503,c_75015]) ).
tcf(c_75195,plain,
sk_c7 = iPr_def_16,
inference(demodulation,[status(thm)],[c_546,c_75015]) ).
tcf(c_75218,plain,
( ( sk_c2 = iPr_def_15 )
| ( sk_c8 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_75183,c_27052]) ).
tcf(c_75247,plain,
( ( sk_c2 = iPr_def_15 )
| ( sk_c9 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_75169,c_27052]) ).
tcf(c_75252,plain,
( ( sk_c2 = iPr_def_15 )
| ( sk_c8 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_75167,c_27052]) ).
tcf(c_75275,plain,
( ( sk_c1 = iPr_def_15 )
| ( sk_c8 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_75157,c_27206]) ).
tcf(c_75280,plain,
( ( sk_c1 = iPr_def_15 )
| ( sk_c9 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_75155,c_27206]) ).
tcf(c_75285,plain,
( ( sk_c1 = iPr_def_15 )
| ( sk_c8 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_75153,c_27206]) ).
tcf(c_75754,plain,
( ~ iPr_def_14
| ( inverse(sk_c8) != iPr_def_16 )
| ( inverse(inverse(sk_c8)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_75192,c_505]) ).
tcf(c_75823,plain,
( ~ iPr_def_14
| ( inverse(inverse(sk_c8)) != sk_c9 ) ),
inference(ground_joinability,[status(thm)],[c_75754,c_491]) ).
tcf(c_75824,plain,
( ~ iPr_def_14
| ( sk_c8 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_75823,c_491,c_26602]) ).
tcf(c_76025,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(inverse(iPr_def_26),iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_535,c_75108]) ).
tcf(c_76026,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(inverse(iPr_def_26),iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_533,c_75108]) ).
tcf(c_76027,plain,
( ( sk_c8 = iPr_def_22 )
| ( multiply(inverse(iPr_def_26),iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_532,c_75108]) ).
tcf(c_76028,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(inverse(iPr_def_26),iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_531,c_75108]) ).
tcf(c_76135,plain,
( ( sk_c8 = iPr_def_18 )
| ~ iPr_def_14
| ( sk_c8 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_33077,c_75824]) ).
tcf(c_76164,plain,
( ( iPr_def_17 = iPr_def_20 )
| ~ iPr_def_14
| ( sk_c8 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1322,c_75824]) ).
tcf(c_76167,plain,
( ( sk_c8 = iPr_def_24 )
| ~ iPr_def_14
| ( sk_c8 != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_545,c_75824]) ).
tcf(c_76172,plain,
( ( sk_c9 = iPr_def_19 )
| ~ iPr_def_14
| ( sk_c8 != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_538,c_75824]) ).
tcf(c_76185,plain,
( ( sk_c8 = iPr_def_18 )
| ~ iPr_def_14
| ( sk_c8 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_517,c_75824]) ).
tcf(c_76392,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(inverse(inverse(iPr_def_26)),iPr_def_16) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_76025,c_21816]) ).
tcf(c_76467,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(inverse(inverse(iPr_def_26)),iPr_def_16) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_76026,c_21816]) ).
tcf(c_76542,plain,
( ( sk_c8 = iPr_def_22 )
| ( multiply(inverse(inverse(iPr_def_26)),iPr_def_16) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_76027,c_21816]) ).
tcf(c_76617,plain,
( ( sk_c8 = iPr_def_21 )
| ( multiply(inverse(inverse(iPr_def_26)),iPr_def_16) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_76028,c_21816]) ).
tcf(c_76943,plain,
iPr_def_17 = iPr_def_20,
inference(global_subsumption_just,[status(thm)],[c_74160,c_552,c_553,c_491,c_546,c_1128,c_2133,c_3241,c_4388,c_9569,c_9981,c_17836,c_18551,c_23033,c_45951,c_48207,c_54208,c_59314,c_65347,c_67775,c_68686,c_71261,c_74171,c_75195,c_76164]) ).
tcf(c_76993,plain,
multiply(iPr_def_17,iPr_def_17) = sk_c9,
inference(demodulation,[status(thm)],[c_7548,c_76943]) ).
tcf(c_76994,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c6,X0)) = X0,
inference(demodulation,[status(thm)],[c_2557,c_76943]) ).
tcf(c_77225,plain,
( ( sk_c8 != iPr_def_27 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_76167,c_1853,c_3933,c_31126,c_50071,c_75824,c_76172,c_76943]) ).
tcf(c_77226,plain,
( ~ iPr_def_14
| ( sk_c8 != iPr_def_27 ) ),
inference(renaming,[status(thm)],[c_77225]) ).
tcf(c_77273,plain,
( ( sk_c8 = iPr_def_15 )
| ~ iPr_def_14
| ( iPr_def_18 != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_515,c_77226]) ).
tcf(c_77823,plain,
( ( sk_c8 = iPr_def_18 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_76185,c_8590,c_76135]) ).
tcf(c_77833,plain,
( ( iPr_def_18 != iPr_def_27 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_77273,c_493,c_502,c_1828,c_1829,c_2118,c_2119,c_2484,c_20514,c_20769,c_20771,c_38306,c_77226,c_77823]) ).
tcf(c_77834,plain,
( ~ iPr_def_14
| ( iPr_def_18 != iPr_def_27 ) ),
inference(renaming,[status(thm)],[c_77833]) ).
tcf(c_78437,plain,
multiply(iPr_def_23,multiply(iPr_def_24,iPr_def_16)) = iPr_def_15,
inference(superposition,[status(thm)],[c_75126,c_2560]) ).
tcf(c_78444,plain,
multiply(sk_c8,iPr_def_15) = sk_c9,
inference(light_normalisation,[status(thm)],[c_75129,c_75188]) ).
tcf(c_78493,plain,
multiply(sk_c2,sk_c9) = multiply(iPr_def_25,iPr_def_15),
inference(superposition,[status(thm)],[c_78444,c_2543]) ).
tcf(c_78495,plain,
multiply(iPr_def_16,sk_c9) = iPr_def_15,
inference(superposition,[status(thm)],[c_78444,c_2559]) ).
tcf(c_78644,plain,
( ~ iPr_def_14
| ( inverse(iPr_def_16) != iPr_def_15 )
| ( inverse(inverse(iPr_def_16)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_78495,c_505]) ).
tcf(c_78717,plain,
( ~ iPr_def_14
| ( sk_c9 != iPr_def_16 )
| ( sk_c8 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_78644,c_491,c_26602]) ).
tcf(c_80747,plain,
( ( sk_c8 = iPr_def_15 )
| ( inverse(iPr_def_15) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_75218,c_493]) ).
tcf(c_80835,plain,
( ( sk_c9 = iPr_def_23 )
| ( inverse(iPr_def_15) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_75247,c_493]) ).
tcf(c_81388,plain,
( ( sk_c8 = iPr_def_24 )
| ( inverse(iPr_def_15) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_75252,c_493]) ).
tcf(c_84323,plain,
( ( sk_c8 = iPr_def_15 )
| ( inverse(iPr_def_15) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_75275,c_502]) ).
tcf(c_84396,plain,
( ( sk_c9 = iPr_def_23 )
| ( inverse(iPr_def_15) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_75280,c_502]) ).
tcf(c_84497,plain,
( ( sk_c8 = iPr_def_24 )
| ( inverse(iPr_def_15) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_75285,c_502]) ).
tcf(c_84609,plain,
( ( iPr_def_18 = iPr_def_27 )
| ( sk_c8 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_84323,c_80747]) ).
tcf(c_84655,plain,
( ( iPr_def_18 = iPr_def_27 )
| ( sk_c9 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_84396,c_80835]) ).
tcf(c_84785,plain,
( ( iPr_def_18 = iPr_def_27 )
| ( sk_c8 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_84497,c_81388]) ).
tcf(c_84850,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_17,iPr_def_17) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1212,c_76994]) ).
tcf(c_84864,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_17,iPr_def_17) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1644,c_76994]) ).
tcf(c_84870,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_17,iPr_def_17) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2453,c_76994]) ).
tcf(c_84871,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_17,iPr_def_17) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2364,c_76994]) ).
tcf(c_84872,plain,
( ( sk_c8 = iPr_def_15 )
| ( multiply(iPr_def_17,iPr_def_17) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2168,c_76994]) ).
tcf(c_84875,plain,
( ( sk_c9 = iPr_def_19 )
| ( multiply(iPr_def_17,iPr_def_17) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1785,c_76994]) ).
tcf(c_84939,plain,
( ~ iPr_def_14
| ( sk_c9 != identity ) ),
inference(light_normalisation,[status(thm)],[c_3902,c_23008]) ).
tcf(c_84964,plain,
( ( sk_c8 = iPr_def_15 )
| ~ iPr_def_14 ),
inference(superposition,[status(thm)],[c_9001,c_84939]) ).
tcf(c_84977,plain,
( ( sk_c8 = iPr_def_24 )
| ~ iPr_def_14
| ( identity != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_545,c_84939]) ).
tcf(c_84978,plain,
( ( sk_c9 = iPr_def_23 )
| ~ iPr_def_14
| ( identity != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_544,c_84939]) ).
tcf(c_85201,plain,
( ( sk_c8 = iPr_def_24 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_84977,c_77834,c_84785]) ).
tcf(c_85314,plain,
( ( sk_c9 = iPr_def_23 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_84978,c_77834,c_84655]) ).
tcf(c_85760,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(sk_c2,iPr_def_25) = multiply(iPr_def_25,iPr_def_15) ) ),
inference(superposition,[status(thm)],[c_527,c_78493]) ).
tcf(c_85761,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c2,iPr_def_25) = multiply(iPr_def_25,iPr_def_15) ) ),
inference(superposition,[status(thm)],[c_526,c_78493]) ).
tcf(c_86436,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_85761,c_85760,c_85314,c_85201,c_84964,c_84875,c_84872,c_84871,c_84870,c_84864,c_84850,c_84785,c_84655,c_84609,c_78717,c_78495,c_78493,c_78444,c_78437,c_76993,c_76943,c_76617,c_76542,c_76467,c_76392,c_75824,c_75189,c_75170,c_75168,c_75126,c_75108,c_75192,c_75060,c_75015,c_71275,c_65626,c_65598,c_65363,c_65336,c_55629,c_55577,c_54960,c_53381,c_52416,c_52367,c_52369,c_42507,c_40355,c_32824,c_32748,c_32749,c_27263,c_26640,c_26602,c_26008,c_25927,c_25850,c_25849,c_25095,c_24939,c_24936,c_24809,c_24796,c_24798,c_24458,c_24195,c_17096,c_16893,c_12811,c_12264,c_12157,c_8975,c_7920,c_3865,c_3863,c_3861,c_3635,c_3489,c_1144,c_518,c_517,c_515,c_514,c_513,c_512,c_511,c_498,c_497,c_494,c_491]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP339-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.36 % Computer : n001.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 14:37:05 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.43 % Proving...
% 9.17/4.15 % SZS status Started for theBenchmark.p
% 9.17/4.15 % SZS status Unsatisfiable for theBenchmark.p
% 9.17/4.15
% 9.17/4.15 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 9.17/4.15
% 9.17/4.15 % ------ iProver source info
% 9.17/4.15
% 9.17/4.15 % git: date: 2026-07-19 20:42:38 +0200
% 9.17/4.15 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 9.17/4.15 % git: non_committed_changes: false
% 9.17/4.15
% 9.17/4.15 % ------ Parsing...% successful
% 9.17/4.15
% 9.17/4.15
% 9.17/4.15 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 9.17/4.15
% 9.17/4.15 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 9.17/4.15
% 9.17/4.15 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 9.17/4.15
% 9.17/4.15 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 9.17/4.15 % ------ Proving...
% 9.17/4.15 % ------ Problem Properties
% 9.17/4.15
% 9.17/4.15 %
% 9.17/4.15 % clauses 60
% 9.17/4.15 % conjectures 43
% 9.17/4.15 % EPR 38
% 9.17/4.15 % Horn 23
% 9.17/4.15 % unary 18
% 9.17/4.15 % binary 36
% 9.17/4.15 % lits 112
% 9.17/4.15 % lits eq 102
% 9.17/4.15 % fd_pure 0
% 9.17/4.15 % fd_pseudo 0
% 9.17/4.15 % fd_cond 0
% 9.17/4.15 % fd_pseudo_cond 0
% 9.17/4.15 % AC symbols 0
% 9.17/4.15
% 9.17/4.15 % ------ Schedule dynamic 5 is on
% 9.17/4.15
% 9.17/4.15 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 9.17/4.15
% 9.17/4.15
% 9.17/4.15 % ------
% 9.17/4.15 % Current options:
% 9.17/4.15 % ------
% 9.17/4.15
% 9.17/4.15
% 9.17/4.15 %
% 9.17/4.15
% 9.17/4.15 % ------ Proving...
% 9.17/4.15 %
% 9.17/4.15
% 9.17/4.15 % SZS status Unsatisfiable for theBenchmark.p
% 9.17/4.15
% 9.17/4.15 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 9.17/4.15
% 9.17/4.15
%------------------------------------------------------------------------------