%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP248-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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:32:27 PM UTC 2026
% Result : Unsatisfiable 15.76s 8.29s
% Output : CNFRefutation 18.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 51
% Syntax : Number of formulae : 480 ( 159 unt; 13 def)
% Number of atoms : 1536 ( 835 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 691 ( 249 ~; 442 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 20 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 131 ( 0 sgn 131 !; 0 ?; 105 :)
% 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,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = inverse(sk_c4)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f5]) ).
fof(f9,negated_conjecture,
( inverse(sk_c5) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c9 = inverse(sk_c5)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c7 = inverse(sk_c6)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f15]) ).
fof(f19,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( multiply(sk_c4,sk_c9) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c10 = multiply(sk_c4,sk_c9)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( inverse(sk_c5) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c9 = inverse(sk_c5)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f28,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( inverse(sk_c6) = sk_c7
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f30,plain,
( sk_c7 = inverse(sk_c6)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f29]) ).
fof(f33,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c2,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c10 = inverse(sk_c4)
| sk_c8 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( multiply(sk_c4,sk_c9) = sk_c10
| multiply(sk_c2,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f36,plain,
( sk_c10 = multiply(sk_c4,sk_c9)
| sk_c8 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f35]) ).
fof(f37,negated_conjecture,
( inverse(sk_c5) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c9 = inverse(sk_c5)
| sk_c8 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c8 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_19) ).
fof(f42,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| sk_c8 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c2,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_20) ).
fof(f44,plain,
( sk_c7 = inverse(sk_c6)
| sk_c8 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c9 = multiply(sk_c7,sk_c8)
| sk_c8 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f45]) ).
fof(f51,negated_conjecture,
( inverse(sk_c5) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c9 = inverse(sk_c5)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( inverse(sk_c6) = sk_c7
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_27) ).
fof(f58,plain,
( sk_c7 = inverse(sk_c6)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f57]) ).
fof(f61,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( multiply(sk_c4,sk_c9) = sk_c10
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c10 = multiply(sk_c4,sk_c9)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c5) = sk_c9
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c9 = inverse(sk_c5)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f65]) ).
fof(f69,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_33) ).
fof(f70,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( inverse(sk_c6) = sk_c7
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f72,plain,
( sk_c7 = inverse(sk_c6)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f71]) ).
fof(f75,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
( multiply(sk_c4,sk_c9) = sk_c10
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
( sk_c10 = multiply(sk_c4,sk_c9)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f77]) ).
fof(f79,negated_conjecture,
( inverse(sk_c5) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_38) ).
fof(f80,plain,
( sk_c9 = inverse(sk_c5)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f79]) ).
fof(f81,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_39) ).
fof(f82,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_40) ).
fof(f84,plain,
( sk_c9 = multiply(sk_c6,sk_c7)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( inverse(sk_c6) = sk_c7
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_41) ).
fof(f86,plain,
( sk_c7 = inverse(sk_c6)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c9 = multiply(sk_c7,sk_c8)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
! [X2,X3,X0,X1,X6,X4,X5] :
( multiply(X6,sk_c8) != sk_c9
| inverse(X5) != X6
| multiply(X5,X6) != sk_c9
| multiply(X4,sk_c8) != sk_c9
| inverse(X4) != sk_c9
| multiply(X3,sk_c9) != sk_c10
| inverse(X3) != sk_c10
| multiply(X2,sk_c8) != sk_c10
| inverse(X2) != sk_c10
| inverse(X1) != sk_c9
| multiply(X1,sk_c9) != sk_c8
| inverse(X0) != sk_c10
| multiply(X0,sk_c10) != sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_43) ).
fof(f90,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( sk_c9 != multiply(X6,sk_c8)
| inverse(X5) != X6
| sk_c9 != multiply(X5,X6)
| sk_c9 != multiply(X4,sk_c8)
| sk_c9 != inverse(X4)
| sk_c10 != multiply(X3,sk_c9)
| sk_c10 != inverse(X3)
| sk_c10 != multiply(X2,sk_c8)
| sk_c10 != inverse(X2)
| sk_c9 != inverse(X1)
| sk_c8 != multiply(X1,sk_c9)
| inverse(X0) != sk_c10
| sk_c9 != multiply(X0,sk_c10) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,plain,
! [X2,X3,X0,X1,X4,X5] :
( sk_c9 != multiply(inverse(X5),sk_c8)
| sk_c9 != multiply(X5,inverse(X5))
| sk_c9 != multiply(X4,sk_c8)
| sk_c9 != inverse(X4)
| sk_c10 != multiply(X3,sk_c9)
| sk_c10 != inverse(X3)
| sk_c10 != multiply(X2,sk_c8)
| sk_c10 != inverse(X2)
| sk_c9 != inverse(X1)
| sk_c8 != multiply(X1,sk_c9)
| inverse(X0) != sk_c10
| sk_c9 != multiply(X0,sk_c10) ),
inference(equality_resolution,[],[f90]) ).
tcf(c_95,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_96,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_98,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_100,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_101,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_102,negated_conjecture,
( ( multiply(sk_c6,sk_c7) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_103,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_105,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c4,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c6,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_112,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_113,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( multiply(sk_c4,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_115,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_116,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( multiply(sk_c6,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_118,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( multiply(sk_c7,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c6,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c4,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c6,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_134,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c4,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_135,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_137,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c6,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_139,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c7,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_140,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(X5) != sk_c9 )
| ( inverse(X4) != sk_c9 )
| ( inverse(X2) != sk_c10 )
| ( inverse(X1) != sk_c10 )
| ( inverse(X0) != sk_c10 )
| ( multiply(X5,sk_c9) != sk_c8 )
| ( multiply(X4,sk_c8) != sk_c9 )
| ( multiply(X2,sk_c9) != sk_c10 )
| ( multiply(X1,sk_c8) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 )
| ( multiply(inverse(X3),sk_c8) != sk_c9 )
| ( multiply(X3,inverse(X3)) != sk_c9 ) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_537,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_140]) ).
tcf(c_538,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c8) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_140]) ).
tcf(c_539,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_140]) ).
tcf(c_540,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_140]) ).
tcf(c_541,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_140]) ).
tcf(c_542,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ( multiply(inverse(X0),sk_c8) != sk_c9 )
| ( multiply(X0,inverse(X0)) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_140]) ).
tcf(c_543,negated_conjecture,
( iPr_def_15
| iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_140]) ).
tcf(c_544,definition,
iPr_def_16 = multiply(sk_c7,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_545,definition,
iPr_def_17 = multiply(sk_c3,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_546,definition,
iPr_def_18 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_547,definition,
iPr_def_19 = multiply(sk_c6,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_548,definition,
iPr_def_20 = multiply(sk_c5,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_549,definition,
iPr_def_21 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_550,definition,
iPr_def_22 = multiply(sk_c4,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_551,definition,
iPr_def_23 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_552,definition,
iPr_def_24 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_553,definition,
iPr_def_25 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_554,definition,
iPr_def_26 = multiply(sk_c2,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_555,definition,
iPr_def_27 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_556,definition,
iPr_def_28 = multiply(sk_c1,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_557,negated_conjecture,
( iPr_def_15
| iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_543]) ).
tcf(c_558,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ( multiply(inverse(X0),sk_c8) != sk_c9 )
| ( multiply(X0,inverse(X0)) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_542]) ).
tcf(c_559,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_541]) ).
tcf(c_560,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_540]) ).
tcf(c_561,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_539]) ).
tcf(c_562,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c8) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_538]) ).
tcf(c_563,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_537]) ).
tcf(c_564,negated_conjecture,
( ( iPr_def_17 = sk_c10 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_139,c_545,c_544]) ).
tcf(c_565,negated_conjecture,
( ( iPr_def_18 = sk_c7 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_138,c_546]) ).
tcf(c_566,negated_conjecture,
( ( iPr_def_19 = sk_c9 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_137,c_547]) ).
tcf(c_567,negated_conjecture,
( ( iPr_def_20 = sk_c9 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_136,c_548]) ).
tcf(c_568,negated_conjecture,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_135,c_549]) ).
tcf(c_569,negated_conjecture,
( ( iPr_def_22 = sk_c10 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_134,c_550]) ).
tcf(c_570,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_133,c_551]) ).
tcf(c_572,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_18 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_573,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_575,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_21 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_128]) ).
tcf(c_576,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_22 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_577,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_579,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_18 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_580,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_581,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_582,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_21 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_585,negated_conjecture,
( ( iPr_def_26 = sk_c8 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_118,c_554]) ).
tcf(c_586,negated_conjecture,
( ( iPr_def_26 = sk_c8 )
| ( iPr_def_18 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_587,negated_conjecture,
( ( iPr_def_26 = sk_c8 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_588,negated_conjecture,
( ( iPr_def_26 = sk_c8 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_115]) ).
tcf(c_589,negated_conjecture,
( ( iPr_def_26 = sk_c8 )
| ( iPr_def_21 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_590,negated_conjecture,
( ( iPr_def_26 = sk_c8 )
| ( iPr_def_22 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_591,negated_conjecture,
( ( iPr_def_26 = sk_c8 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_593,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_18 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_594,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_595,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_596,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_21 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_597,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_22 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_598,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_600,negated_conjecture,
( ( iPr_def_28 = sk_c9 )
| ( iPr_def_18 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_103]) ).
tcf(c_601,negated_conjecture,
( ( iPr_def_28 = sk_c9 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_102]) ).
tcf(c_602,negated_conjecture,
( ( iPr_def_28 = sk_c9 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_101]) ).
tcf(c_603,negated_conjecture,
( ( iPr_def_28 = sk_c9 )
| ( iPr_def_21 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_100]) ).
tcf(c_605,negated_conjecture,
( ( iPr_def_28 = sk_c9 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_98]) ).
tcf(c_1135,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(sk_c6,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_572,c_547]) ).
tcf(c_1136,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(sk_c6,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_565,c_547]) ).
tcf(c_1147,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_24) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_577,c_556]) ).
tcf(c_1148,plain,
( ( sk_c10 = iPr_def_22 )
| ( multiply(sk_c1,iPr_def_24) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_576,c_556]) ).
tcf(c_1149,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_24) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_575,c_556]) ).
tcf(c_1151,plain,
( ( sk_c9 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_24) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_573,c_556]) ).
tcf(c_1153,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_570,c_556]) ).
tcf(c_1154,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(sk_c1,iPr_def_22) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_569,c_556]) ).
tcf(c_1183,plain,
multiply(iPr_def_23,sk_c4) = identity,
inference(superposition,[status(thm)],[c_551,c_96]) ).
tcf(c_1184,plain,
multiply(iPr_def_21,sk_c5) = identity,
inference(superposition,[status(thm)],[c_549,c_96]) ).
tcf(c_1185,plain,
multiply(iPr_def_18,sk_c6) = identity,
inference(superposition,[status(thm)],[c_546,c_96]) ).
tcf(c_1186,plain,
multiply(iPr_def_27,sk_c1) = identity,
inference(superposition,[status(thm)],[c_555,c_96]) ).
tcf(c_1187,plain,
multiply(iPr_def_25,sk_c2) = identity,
inference(superposition,[status(thm)],[c_553,c_96]) ).
tcf(c_1188,plain,
multiply(iPr_def_24,sk_c3) = identity,
inference(superposition,[status(thm)],[c_552,c_96]) ).
tcf(c_1193,plain,
( ( sk_c9 = iPr_def_25 )
| ( multiply(sk_c6,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_579,c_547]) ).
tcf(c_1205,plain,
( ( sk_c9 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_580,c_554]) ).
tcf(c_1221,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_581,c_554]) ).
tcf(c_1231,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_582,c_554]) ).
tcf(c_1232,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_582,c_550]) ).
tcf(c_1415,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c7,iPr_def_26) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_585,c_544]) ).
tcf(c_1432,plain,
( ( sk_c8 = iPr_def_26 )
| ( multiply(sk_c6,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_586,c_547]) ).
tcf(c_1444,plain,
( ( sk_c9 = iPr_def_19 )
| ( multiply(sk_c7,iPr_def_26) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_587,c_544]) ).
tcf(c_1463,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(sk_c7,iPr_def_26) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_588,c_544]) ).
tcf(c_1480,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(sk_c5,iPr_def_26) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_589,c_548]) ).
tcf(c_1482,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(sk_c7,iPr_def_26) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_589,c_544]) ).
tcf(c_1495,plain,
( ( sk_c10 = iPr_def_22 )
| ( multiply(sk_c7,iPr_def_26) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_590,c_544]) ).
tcf(c_1514,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c7,iPr_def_26) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_591,c_544]) ).
tcf(c_1612,plain,
( ( sk_c10 = iPr_def_27 )
| ( multiply(sk_c6,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_593,c_547]) ).
tcf(c_1655,plain,
( ( sk_c9 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_594,c_556]) ).
tcf(c_1737,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_595,c_556]) ).
tcf(c_1812,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_596,c_556]) ).
tcf(c_2004,plain,
( ( sk_c9 = iPr_def_28 )
| ( multiply(sk_c6,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_600,c_547]) ).
tcf(c_2029,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( sk_c9 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_601,c_580]) ).
tcf(c_2031,plain,
( ( sk_c9 = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_28) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_601,c_550]) ).
tcf(c_2054,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( sk_c9 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_602,c_581]) ).
tcf(c_2057,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(sk_c4,iPr_def_28) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_602,c_550]) ).
tcf(c_2085,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( sk_c9 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_603,c_582]) ).
tcf(c_2088,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_603,c_554]) ).
tcf(c_2089,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(sk_c4,iPr_def_28) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_603,c_550]) ).
tcf(c_2305,plain,
( ( sk_c9 = iPr_def_28 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_605,c_556]) ).
tcf(c_2719,plain,
( ~ iPr_def_14
| ( sk_c8 != iPr_def_26 )
| ( inverse(sk_c2) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_554,c_559]) ).
tcf(c_2736,plain,
( ~ iPr_def_14
| ( sk_c8 != iPr_def_26 )
| ( sk_c9 != iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_2719,c_553]) ).
tcf(c_2869,plain,
( ~ iPr_def_13
| ( sk_c9 != iPr_def_28 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_556,c_560]) ).
tcf(c_2898,plain,
( ~ iPr_def_13
| ( sk_c9 != iPr_def_28 )
| ( sk_c10 != iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_2869,c_555]) ).
tcf(c_3119,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_20 )
| ( inverse(sk_c5) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_548,c_561]) ).
tcf(c_3122,plain,
( ~ iPr_def_12
| ( sk_c9 != sk_c8 )
| ( inverse(identity) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_95,c_561]) ).
tcf(c_3140,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_21 )
| ( sk_c9 != iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_3119,c_549]) ).
tcf(c_3223,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_17 )
| ( inverse(sk_c3) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_545,c_562]) ).
tcf(c_3235,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_24 )
| ( sk_c10 != iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_3223,c_552]) ).
tcf(c_3305,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_22 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_550,c_563]) ).
tcf(c_3327,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_23 )
| ( sk_c10 != iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_3305,c_551]) ).
tcf(c_3466,plain,
( ~ iPr_def_15
| ( inverse(identity) != sk_c9 )
| ( multiply(inverse(identity),sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_95,c_558]) ).
tcf(c_3471,plain,
( ~ iPr_def_15
| ( multiply(sk_c2,iPr_def_25) != sk_c9 )
| ( multiply(inverse(sk_c2),sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_553,c_558]) ).
tcf(c_3480,plain,
( ~ iPr_def_15
| ( multiply(iPr_def_25,sk_c8) != sk_c9 )
| ( multiply(sk_c2,iPr_def_25) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_3471,c_553]) ).
tcf(c_3741,plain,
! [X0: $i] : multiply(sk_c5,multiply(sk_c8,X0)) = multiply(iPr_def_20,X0),
inference(superposition,[status(thm)],[c_548,c_97]) ).
tcf(c_3743,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c8,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_544,c_97]) ).
tcf(c_3747,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_96,c_97]) ).
tcf(c_3749,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1183,c_97]) ).
tcf(c_3750,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1184,c_97]) ).
tcf(c_3751,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1185,c_97]) ).
tcf(c_3752,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1186,c_97]) ).
tcf(c_3753,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1187,c_97]) ).
tcf(c_3754,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1188,c_97]) ).
tcf(c_3762,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3754,c_95]) ).
tcf(c_3763,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3753,c_95]) ).
tcf(c_3764,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3752,c_95]) ).
tcf(c_3765,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3751,c_95]) ).
tcf(c_3766,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3750,c_95]) ).
tcf(c_3767,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3749,c_95]) ).
tcf(c_5381,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( iPr_def_19 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_2054,c_2029]) ).
tcf(c_5475,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( iPr_def_20 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_2085,c_2054]) ).
tcf(c_5796,plain,
multiply(iPr_def_24,iPr_def_17) = sk_c8,
inference(superposition,[status(thm)],[c_545,c_3762]) ).
tcf(c_5803,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(iPr_def_17,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_5796,c_97]) ).
tcf(c_5809,plain,
multiply(iPr_def_25,iPr_def_26) = sk_c9,
inference(superposition,[status(thm)],[c_554,c_3763]) ).
tcf(c_5835,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(iPr_def_26,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_5809,c_97]) ).
tcf(c_6314,plain,
multiply(iPr_def_27,iPr_def_28) = sk_c10,
inference(superposition,[status(thm)],[c_556,c_3764]) ).
tcf(c_6323,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(iPr_def_28,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_6314,c_97]) ).
tcf(c_6325,plain,
multiply(iPr_def_18,iPr_def_19) = sk_c7,
inference(superposition,[status(thm)],[c_547,c_3765]) ).
tcf(c_6343,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(iPr_def_19,X0)) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_6325,c_97]) ).
tcf(c_6412,plain,
multiply(iPr_def_21,iPr_def_20) = sk_c8,
inference(superposition,[status(thm)],[c_548,c_3766]) ).
tcf(c_6415,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(iPr_def_20,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_6412,c_97]) ).
tcf(c_6435,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1149,c_3764]) ).
tcf(c_6436,plain,
( ( sk_c9 = iPr_def_21 )
| ( sk_c10 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_6435,c_6314]) ).
tcf(c_6497,plain,
( ( sk_c9 = iPr_def_19 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1151,c_3764]) ).
tcf(c_6498,plain,
( ( sk_c9 = iPr_def_19 )
| ( sk_c10 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_6497,c_6314]) ).
tcf(c_6527,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1153,c_3764]) ).
tcf(c_6528,plain,
( ( sk_c10 = iPr_def_23 )
| ( sk_c10 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_6527,c_6314]) ).
tcf(c_6539,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_1154,c_3764]) ).
tcf(c_6540,plain,
( ( sk_c10 = iPr_def_22 )
| ( sk_c10 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_6539,c_6314]) ).
tcf(c_6628,plain,
multiply(iPr_def_23,iPr_def_22) = sk_c9,
inference(superposition,[status(thm)],[c_550,c_3767]) ).
tcf(c_7243,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(iPr_def_21,iPr_def_20) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1480,c_3766]) ).
tcf(c_7244,plain,
( ( sk_c8 = iPr_def_26 )
| ( sk_c9 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_7243,c_6412]) ).
tcf(c_8061,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(iPr_def_25,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2088,c_3763]) ).
tcf(c_8062,plain,
( ( sk_c9 = iPr_def_28 )
| ( sk_c9 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_8061,c_5809]) ).
tcf(c_8158,plain,
( ( sk_c9 = iPr_def_28 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_2305,c_3764]) ).
tcf(c_8159,plain,
( ( sk_c9 = iPr_def_28 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_8158,c_6314]) ).
tcf(c_11194,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_3747,c_95]) ).
tcf(c_11205,plain,
multiply(inverse(sk_c7),iPr_def_16) = sk_c8,
inference(superposition,[status(thm)],[c_544,c_11194]) ).
tcf(c_11208,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_95,c_11194]) ).
tcf(c_11209,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_96,c_11194]) ).
tcf(c_11210,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_97,c_11194]) ).
tcf(c_11237,plain,
( ( sk_c10 = iPr_def_22 )
| ( multiply(inverse(sk_c1),iPr_def_28) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1148,c_11194]) ).
tcf(c_11238,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(inverse(sk_c1),iPr_def_28) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1147,c_11194]) ).
tcf(c_11332,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_3767,c_11194]) ).
tcf(c_11333,plain,
! [X0: $i] : multiply(inverse(iPr_def_21),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_3766,c_11194]) ).
tcf(c_11334,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_3765,c_11194]) ).
tcf(c_11335,plain,
! [X0: $i] : multiply(inverse(iPr_def_27),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_3764,c_11194]) ).
tcf(c_11336,plain,
! [X0: $i] : multiply(inverse(iPr_def_25),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_3763,c_11194]) ).
tcf(c_11337,plain,
! [X0: $i] : multiply(inverse(iPr_def_24),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_3762,c_11194]) ).
tcf(c_11355,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_11194,c_11194]) ).
tcf(c_11463,plain,
( ( sk_c10 = iPr_def_24 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_11238,c_555,c_6314]) ).
tcf(c_11466,plain,
( ( sk_c10 = iPr_def_24 )
| ( sk_c10 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_11237,c_555,c_6314]) ).
tcf(c_11753,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_11209,c_11355]) ).
tcf(c_11761,plain,
multiply(sk_c10,identity) = multiply(iPr_def_27,iPr_def_28),
inference(superposition,[status(thm)],[c_11753,c_6323]) ).
tcf(c_11766,plain,
multiply(sk_c8,identity) = multiply(iPr_def_21,iPr_def_20),
inference(superposition,[status(thm)],[c_11753,c_6415]) ).
tcf(c_11770,plain,
multiply(sk_c7,identity) = multiply(iPr_def_18,iPr_def_19),
inference(superposition,[status(thm)],[c_11753,c_6343]) ).
tcf(c_11772,plain,
multiply(sk_c9,identity) = multiply(iPr_def_25,iPr_def_26),
inference(superposition,[status(thm)],[c_11753,c_5835]) ).
tcf(c_11773,plain,
multiply(sk_c8,identity) = multiply(iPr_def_24,iPr_def_17),
inference(superposition,[status(thm)],[c_11753,c_5803]) ).
tcf(c_11780,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_11753,c_11208]) ).
tcf(c_11781,plain,
multiply(sk_c8,identity) = sk_c8,
inference(light_normalisation,[status(thm)],[c_11773,c_5796]) ).
tcf(c_11782,plain,
multiply(sk_c9,identity) = sk_c9,
inference(light_normalisation,[status(thm)],[c_11772,c_5809]) ).
tcf(c_11784,plain,
multiply(sk_c7,identity) = sk_c7,
inference(light_normalisation,[status(thm)],[c_11770,c_6325]) ).
tcf(c_11793,plain,
multiply(sk_c10,identity) = sk_c10,
inference(light_normalisation,[status(thm)],[c_11761,c_6314]) ).
tcf(c_11799,plain,
multiply(identity,identity) = identity,
inference(superposition,[status(thm)],[c_11780,c_96]) ).
tcf(c_12020,plain,
( ( sk_c9 = iPr_def_21 )
| ~ iPr_def_14
| ( sk_c8 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_582,c_2736]) ).
tcf(c_12143,plain,
( ( sk_c9 = iPr_def_21 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_12020,c_7244,c_12020]) ).
tcf(c_12421,plain,
( ( sk_c10 = iPr_def_23 )
| ~ iPr_def_13
| ( sk_c9 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_598,c_2898]) ).
tcf(c_12423,plain,
( ( sk_c9 = iPr_def_21 )
| ~ iPr_def_13
| ( sk_c9 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_596,c_2898]) ).
tcf(c_12548,plain,
( ( sk_c10 = iPr_def_23 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_12421,c_8159,c_12421]) ).
tcf(c_12740,plain,
( ( sk_c9 = iPr_def_21 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_12423,c_8062,c_12423]) ).
tcf(c_13060,plain,
( ( iPr_def_25 = iPr_def_28 )
| ~ iPr_def_12
| ( sk_c9 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_2054,c_3140]) ).
tcf(c_13267,plain,
( ( sk_c10 = iPr_def_23 )
| ~ iPr_def_11
| ( iPr_def_17 != iPr_def_27 )
| ( sk_c10 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_598,c_3235]) ).
tcf(c_13268,plain,
( ( sk_c10 = iPr_def_22 )
| ~ iPr_def_11
| ( iPr_def_17 != iPr_def_27 )
| ( sk_c10 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_597,c_3235]) ).
tcf(c_13283,plain,
( ( sk_c9 = iPr_def_21 )
| ~ iPr_def_11
| ( sk_c10 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_568,c_3235]) ).
tcf(c_13285,plain,
( ( sk_c9 = iPr_def_19 )
| ~ iPr_def_11
| ( sk_c10 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_566,c_3235]) ).
tcf(c_13444,plain,
( ( sk_c9 = iPr_def_21 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_13283,c_6436,c_13283]) ).
tcf(c_13509,plain,
( ( sk_c9 = iPr_def_19 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_13285,c_6498,c_13285]) ).
tcf(c_14190,plain,
( ~ iPr_def_13
| ( inverse(inverse(iPr_def_23)) != sk_c10 )
| ( multiply(sk_c4,sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_11332,c_560]) ).
tcf(c_14193,plain,
multiply(sk_c4,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_11332,c_96]) ).
tcf(c_14194,plain,
( ~ iPr_def_11
| ( inverse(inverse(iPr_def_23)) != sk_c10 )
| ( multiply(sk_c4,sk_c8) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_11332,c_562]) ).
tcf(c_14199,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_23,X0)) = X0,
inference(superposition,[status(thm)],[c_11332,c_11194]) ).
tcf(c_14200,plain,
multiply(sk_c4,identity) = inverse(iPr_def_23),
inference(superposition,[status(thm)],[c_11332,c_11753]) ).
tcf(c_14276,plain,
multiply(iPr_def_23,identity) = iPr_def_23,
inference(superposition,[status(thm)],[c_14193,c_3767]) ).
tcf(c_14279,plain,
inverse(iPr_def_23) = sk_c4,
inference(demodulation,[status(thm)],[c_14200,c_11753]) ).
tcf(c_14288,plain,
multiply(sk_c4,identity) = sk_c4,
inference(superposition,[status(thm)],[c_1183,c_14199]) ).
tcf(c_14289,plain,
multiply(sk_c4,sk_c9) = iPr_def_22,
inference(superposition,[status(thm)],[c_6628,c_14199]) ).
tcf(c_14387,plain,
multiply(sk_c5,iPr_def_21) = identity,
inference(superposition,[status(thm)],[c_11333,c_96]) ).
tcf(c_14389,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_21)) != sk_c9 )
| ( multiply(sk_c5,sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_11333,c_561]) ).
tcf(c_14391,plain,
( ~ iPr_def_14
| ( inverse(inverse(iPr_def_21)) != sk_c9 )
| ( multiply(sk_c5,sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_11333,c_559]) ).
tcf(c_14393,plain,
! [X0: $i] : multiply(sk_c5,multiply(iPr_def_21,X0)) = X0,
inference(superposition,[status(thm)],[c_11333,c_11194]) ).
tcf(c_14394,plain,
multiply(sk_c5,identity) = inverse(iPr_def_21),
inference(superposition,[status(thm)],[c_11333,c_11753]) ).
tcf(c_14401,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_20 )
| ( inverse(inverse(iPr_def_21)) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_14389,c_548]) ).
tcf(c_14435,plain,
inverse(iPr_def_21) = sk_c5,
inference(demodulation,[status(thm)],[c_14394,c_11753]) ).
tcf(c_14438,plain,
( ~ iPr_def_15
| ( multiply(iPr_def_21,sk_c5) != sk_c9 )
| ( multiply(inverse(iPr_def_21),sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_14435,c_558]) ).
tcf(c_14440,plain,
( ~ iPr_def_15
| ( sk_c9 != iPr_def_20 )
| ( sk_c9 != identity ) ),
inference(light_normalisation,[status(thm)],[c_14438,c_548,c_1184,c_14435]) ).
tcf(c_14470,plain,
multiply(sk_c5,identity) = sk_c5,
inference(superposition,[status(thm)],[c_1184,c_14393]) ).
tcf(c_14501,plain,
multiply(sk_c6,iPr_def_18) = identity,
inference(superposition,[status(thm)],[c_11334,c_96]) ).
tcf(c_14507,plain,
! [X0: $i] : multiply(sk_c6,multiply(iPr_def_18,X0)) = X0,
inference(superposition,[status(thm)],[c_11334,c_11194]) ).
tcf(c_14527,plain,
( ( identity = iPr_def_19 )
| ( sk_c9 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_2004,c_14501]) ).
tcf(c_14528,plain,
( ( identity = iPr_def_19 )
| ( sk_c10 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_1612,c_14501]) ).
tcf(c_14529,plain,
( ( identity = iPr_def_19 )
| ( sk_c8 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_1432,c_14501]) ).
tcf(c_14530,plain,
( ( identity = iPr_def_19 )
| ( sk_c9 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_1193,c_14501]) ).
tcf(c_14531,plain,
( ( identity = iPr_def_19 )
| ( sk_c10 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_1136,c_14501]) ).
tcf(c_14532,plain,
( ( identity = iPr_def_19 )
| ( sk_c10 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_1135,c_14501]) ).
tcf(c_14592,plain,
multiply(iPr_def_18,identity) = iPr_def_18,
inference(superposition,[status(thm)],[c_14501,c_3765]) ).
tcf(c_14675,plain,
( ( identity = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_14527,c_554]) ).
tcf(c_14676,plain,
( ( identity = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_28) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_14527,c_550]) ).
tcf(c_14980,plain,
( ( identity = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_14528,c_556]) ).
tcf(c_15158,plain,
( ( identity = iPr_def_19 )
| ( multiply(sk_c7,iPr_def_26) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_14529,c_544]) ).
tcf(c_15214,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( identity = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_14530,c_14527]) ).
tcf(c_15249,plain,
( ( identity = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_14530,c_554]) ).
tcf(c_15352,plain,
multiply(sk_c6,sk_c7) = iPr_def_19,
inference(superposition,[status(thm)],[c_6325,c_14507]) ).
tcf(c_15748,plain,
( ( iPr_def_17 = iPr_def_24 )
| ( identity = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_14532,c_14531]) ).
tcf(c_15753,plain,
( ( identity = iPr_def_19 )
| ~ iPr_def_11
| ( iPr_def_17 != iPr_def_24 )
| ( sk_c10 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_14532,c_3235]) ).
tcf(c_16117,plain,
multiply(sk_c1,iPr_def_27) = identity,
inference(superposition,[status(thm)],[c_11335,c_96]) ).
tcf(c_16123,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_27,X0)) = X0,
inference(superposition,[status(thm)],[c_11335,c_11194]) ).
tcf(c_16124,plain,
multiply(sk_c1,identity) = inverse(iPr_def_27),
inference(superposition,[status(thm)],[c_11335,c_11753]) ).
tcf(c_16179,plain,
( ( identity = iPr_def_28 )
| ( identity = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_14980,c_16117]) ).
tcf(c_16182,plain,
( ( identity = iPr_def_28 )
| ( sk_c9 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_1812,c_16117]) ).
tcf(c_16183,plain,
( ( identity = iPr_def_28 )
| ( sk_c9 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_1737,c_16117]) ).
tcf(c_16184,plain,
( ( identity = iPr_def_28 )
| ( sk_c9 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1655,c_16117]) ).
tcf(c_16293,plain,
multiply(iPr_def_27,identity) = iPr_def_27,
inference(superposition,[status(thm)],[c_16117,c_3764]) ).
tcf(c_16380,plain,
inverse(iPr_def_27) = sk_c1,
inference(demodulation,[status(thm)],[c_16124,c_11753]) ).
tcf(c_16435,plain,
multiply(sk_c1,identity) = sk_c1,
inference(superposition,[status(thm)],[c_1186,c_16123]) ).
tcf(c_16788,plain,
! [X0: $i] :
( ( identity = iPr_def_19 )
| ( multiply(iPr_def_28,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_16179,c_95]) ).
tcf(c_17424,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( identity = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_16183,c_16182]) ).
tcf(c_17428,plain,
( ( identity = iPr_def_28 )
| ~ iPr_def_12
| ( sk_c9 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_16183,c_3140]) ).
tcf(c_17549,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( identity = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_16184,c_16183]) ).
tcf(c_18637,plain,
multiply(sk_c2,iPr_def_25) = identity,
inference(superposition,[status(thm)],[c_11336,c_96]) ).
tcf(c_18643,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_25,X0)) = X0,
inference(superposition,[status(thm)],[c_11336,c_11194]) ).
tcf(c_18644,plain,
multiply(sk_c2,identity) = inverse(iPr_def_25),
inference(superposition,[status(thm)],[c_11336,c_11753]) ).
tcf(c_18665,plain,
( ( identity = iPr_def_26 )
| ( identity = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_15249,c_18637]) ).
tcf(c_18667,plain,
( ( identity = iPr_def_26 )
| ( sk_c9 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_1231,c_18637]) ).
tcf(c_18668,plain,
( ( identity = iPr_def_26 )
| ( sk_c9 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_1221,c_18637]) ).
tcf(c_18669,plain,
( ( identity = iPr_def_26 )
| ( sk_c9 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1205,c_18637]) ).
tcf(c_18776,plain,
multiply(iPr_def_25,identity) = iPr_def_25,
inference(superposition,[status(thm)],[c_18637,c_3763]) ).
tcf(c_18802,plain,
( ( iPr_def_26 = iPr_def_28 )
| ( identity = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_18665,c_16179]) ).
tcf(c_19117,plain,
inverse(iPr_def_25) = sk_c2,
inference(demodulation,[status(thm)],[c_18644,c_11753]) ).
tcf(c_19126,plain,
multiply(sk_c2,identity) = sk_c2,
inference(superposition,[status(thm)],[c_1187,c_18643]) ).
tcf(c_19127,plain,
multiply(sk_c2,sk_c9) = iPr_def_26,
inference(superposition,[status(thm)],[c_5809,c_18643]) ).
tcf(c_19221,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_18668,c_18667]) ).
tcf(c_19266,plain,
( ( identity = iPr_def_26 )
| ( multiply(sk_c4,iPr_def_20) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_18668,c_550]) ).
tcf(c_19382,plain,
( ( iPr_def_19 = iPr_def_20 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_18669,c_18668]) ).
tcf(c_19429,plain,
( ( identity = iPr_def_26 )
| ( multiply(sk_c4,iPr_def_19) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_18669,c_550]) ).
tcf(c_20109,plain,
( ( iPr_def_26 = iPr_def_28 )
| ( iPr_def_20 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_19221,c_17424]) ).
tcf(c_20206,plain,
( ( iPr_def_26 = iPr_def_28 )
| ( iPr_def_19 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_19382,c_17549]) ).
tcf(c_21042,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_20 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_20109,c_5475]) ).
tcf(c_21143,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_19 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_20206,c_5381]) ).
tcf(c_23272,plain,
( ~ iPr_def_12
| ( sk_c9 != identity )
| ( sk_c9 != sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_3122,c_11780]) ).
tcf(c_23318,plain,
( ( sk_c9 = iPr_def_21 )
| ~ iPr_def_12
| ( identity != iPr_def_28 )
| ( sk_c9 != sk_c8 ) ),
inference(superposition,[status(thm)],[c_603,c_23272]) ).
tcf(c_23319,plain,
( ( sk_c9 = iPr_def_20 )
| ~ iPr_def_12
| ( identity != iPr_def_28 )
| ( sk_c9 != sk_c8 ) ),
inference(superposition,[status(thm)],[c_602,c_23272]) ).
tcf(c_26179,plain,
multiply(sk_c3,iPr_def_24) = identity,
inference(superposition,[status(thm)],[c_11337,c_96]) ).
tcf(c_26185,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_24,X0)) = X0,
inference(superposition,[status(thm)],[c_11337,c_11194]) ).
tcf(c_26186,plain,
multiply(sk_c3,identity) = inverse(iPr_def_24),
inference(superposition,[status(thm)],[c_11337,c_11753]) ).
tcf(c_26308,plain,
inverse(iPr_def_24) = sk_c3,
inference(demodulation,[status(thm)],[c_26186,c_11753]) ).
tcf(c_26466,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm)],[c_1188,c_26185]) ).
tcf(c_26467,plain,
multiply(sk_c3,sk_c8) = iPr_def_17,
inference(superposition,[status(thm)],[c_5796,c_26185]) ).
tcf(c_28126,plain,
( ~ iPr_def_15
| ( sk_c9 != identity )
| ( multiply(identity,sk_c8) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_3466,c_11780]) ).
tcf(c_28127,plain,
( ~ iPr_def_15
| ( sk_c9 != identity )
| ( sk_c9 != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_28126,c_95]) ).
tcf(c_28173,plain,
( ( sk_c9 = iPr_def_21 )
| ~ iPr_def_15
| ( identity != iPr_def_28 )
| ( sk_c9 != sk_c8 ) ),
inference(superposition,[status(thm)],[c_603,c_28127]) ).
tcf(c_35518,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c4)),multiply(X0,iPr_def_22)) = sk_c9,
inference(superposition,[status(thm)],[c_14289,c_11210]) ).
tcf(c_35524,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c7)),multiply(X0,iPr_def_16)) = sk_c8,
inference(superposition,[status(thm)],[c_544,c_11210]) ).
tcf(c_35538,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c6)),multiply(X0,identity)) = iPr_def_18,
inference(superposition,[status(thm)],[c_14501,c_11210]) ).
tcf(c_35541,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_21 )
| ( multiply(inverse(multiply(X0,sk_c4)),multiply(X0,iPr_def_22)) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1232,c_11210]) ).
tcf(c_35545,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c2)),multiply(X0,identity)) = iPr_def_25,
inference(superposition,[status(thm)],[c_18637,c_11210]) ).
tcf(c_35571,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_23)),multiply(X0,identity)) = sk_c4,
inference(superposition,[status(thm)],[c_1183,c_11210]) ).
tcf(c_35572,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_21)),multiply(X0,identity)) = sk_c5,
inference(superposition,[status(thm)],[c_1184,c_11210]) ).
tcf(c_35573,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_18)),multiply(X0,identity)) = sk_c6,
inference(superposition,[status(thm)],[c_1185,c_11210]) ).
tcf(c_35575,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_25)),multiply(X0,identity)) = sk_c2,
inference(superposition,[status(thm)],[c_1187,c_11210]) ).
tcf(c_35576,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_24)),multiply(X0,identity)) = sk_c3,
inference(superposition,[status(thm)],[c_1188,c_11210]) ).
tcf(c_35591,plain,
! [X0: $i] :
( ( identity = iPr_def_19 )
| ( multiply(inverse(multiply(X0,sk_c7)),multiply(X0,iPr_def_16)) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_15158,c_11210]) ).
tcf(c_35592,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_23 )
| ( multiply(inverse(multiply(X0,sk_c7)),multiply(X0,iPr_def_16)) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1514,c_11210]) ).
tcf(c_35593,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_22 )
| ( multiply(inverse(multiply(X0,sk_c7)),multiply(X0,iPr_def_16)) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1495,c_11210]) ).
tcf(c_35594,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_21 )
| ( multiply(inverse(multiply(X0,sk_c7)),multiply(X0,iPr_def_16)) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1482,c_11210]) ).
tcf(c_35595,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_20 )
| ( multiply(inverse(multiply(X0,sk_c7)),multiply(X0,iPr_def_16)) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1463,c_11210]) ).
tcf(c_35596,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_19 )
| ( multiply(inverse(multiply(X0,sk_c7)),multiply(X0,iPr_def_16)) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1444,c_11210]) ).
tcf(c_35597,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_16 )
| ( multiply(inverse(multiply(X0,sk_c7)),multiply(X0,iPr_def_16)) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1415,c_11210]) ).
tcf(c_35605,plain,
! [X0: $i] :
( ( identity = iPr_def_19 )
| ( multiply(inverse(multiply(X0,sk_c4)),multiply(X0,iPr_def_22)) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_14676,c_11210]) ).
tcf(c_35607,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_21 )
| ( multiply(inverse(multiply(X0,sk_c4)),multiply(X0,iPr_def_22)) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2089,c_11210]) ).
tcf(c_35608,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_20 )
| ( multiply(inverse(multiply(X0,sk_c4)),multiply(X0,iPr_def_22)) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2057,c_11210]) ).
tcf(c_35609,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_19 )
| ( multiply(inverse(multiply(X0,sk_c4)),multiply(X0,iPr_def_22)) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2031,c_11210]) ).
tcf(c_35629,plain,
! [X0: $i] :
( ( identity = iPr_def_26 )
| ( multiply(inverse(multiply(X0,sk_c4)),multiply(X0,iPr_def_22)) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_19429,c_11210]) ).
tcf(c_35641,plain,
! [X0: $i] :
( ( identity = iPr_def_26 )
| ( multiply(inverse(multiply(X0,sk_c4)),multiply(X0,iPr_def_22)) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_19266,c_11210]) ).
tcf(c_35647,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c4)),multiply(X0,identity)) = iPr_def_23,
inference(superposition,[status(thm)],[c_14193,c_11210]) ).
tcf(c_35648,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c5)),multiply(X0,identity)) = iPr_def_21,
inference(superposition,[status(thm)],[c_14387,c_11210]) ).
tcf(c_35649,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c3)),multiply(X0,identity)) = iPr_def_24,
inference(superposition,[status(thm)],[c_26179,c_11210]) ).
tcf(c_35807,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c3)),X0) = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_35649,c_11753]) ).
tcf(c_35808,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c5)),X0) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_35648,c_11753]) ).
tcf(c_35809,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c4)),X0) = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_35647,c_11753]) ).
tcf(c_35811,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_24)),X0) = sk_c3,
inference(light_normalisation,[status(thm)],[c_35576,c_11753]) ).
tcf(c_35812,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_25)),X0) = sk_c2,
inference(light_normalisation,[status(thm)],[c_35575,c_11753]) ).
tcf(c_35814,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_18)),X0) = sk_c6,
inference(light_normalisation,[status(thm)],[c_35573,c_11753]) ).
tcf(c_35815,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_21)),X0) = sk_c5,
inference(light_normalisation,[status(thm)],[c_35572,c_11753]) ).
tcf(c_35816,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_23)),X0) = sk_c4,
inference(light_normalisation,[status(thm)],[c_35571,c_11753]) ).
tcf(c_35817,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c2)),X0) = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_35545,c_11753]) ).
tcf(c_35818,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c6)),X0) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_35538,c_11753]) ).
tcf(c_45605,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,multiply(X1,sk_c3))),multiply(X0,X1)) = iPr_def_24,
inference(superposition,[status(thm)],[c_97,c_35807]) ).
tcf(c_45606,plain,
multiply(inverse(identity),iPr_def_24) = iPr_def_24,
inference(superposition,[status(thm)],[c_1188,c_35807]) ).
tcf(c_45649,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_24 )
| ( inverse(inverse(multiply(sk_c8,sk_c3))) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_35807,c_562]) ).
tcf(c_45651,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_24 )
| ( inverse(inverse(multiply(sk_c9,sk_c3))) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_35807,c_563]) ).
tcf(c_45655,plain,
multiply(identity,iPr_def_24) = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_45606,c_11780]) ).
tcf(c_45950,plain,
( ( sk_c10 = iPr_def_23 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_13267,c_3235,c_6528,c_11463]) ).
tcf(c_45956,plain,
( ( sk_c10 = iPr_def_22 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_13268,c_3235,c_6540,c_11466]) ).
tcf(c_45991,plain,
multiply(inverse(identity),multiply(inverse(sk_c7),iPr_def_16)) = sk_c8,
inference(superposition,[status(thm)],[c_96,c_35524]) ).
tcf(c_46031,plain,
multiply(inverse(multiply(inverse(iPr_def_16),sk_c7)),identity) = sk_c8,
inference(superposition,[status(thm)],[c_96,c_35524]) ).
tcf(c_46078,plain,
multiply(identity,sk_c8) = sk_c8,
inference(light_normalisation,[status(thm)],[c_45991,c_11205,c_11780]) ).
tcf(c_46497,plain,
multiply(inverse(identity),iPr_def_21) = iPr_def_21,
inference(superposition,[status(thm)],[c_1184,c_35808]) ).
tcf(c_46524,plain,
( ~ iPr_def_13
| ( sk_c9 != iPr_def_21 )
| ( inverse(inverse(multiply(sk_c10,sk_c5))) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_35808,c_560]) ).
tcf(c_46531,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_21 )
| ( inverse(inverse(multiply(sk_c8,sk_c5))) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_35808,c_561]) ).
tcf(c_46533,plain,
( ~ iPr_def_14
| ( sk_c8 != iPr_def_21 )
| ( inverse(inverse(multiply(sk_c9,sk_c5))) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_35808,c_559]) ).
tcf(c_46538,plain,
multiply(inverse(iPr_def_21),inverse(multiply(sk_c3,sk_c5))) = iPr_def_24,
inference(superposition,[status(thm)],[c_35808,c_35807]) ).
tcf(c_46539,plain,
multiply(identity,iPr_def_21) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_46497,c_11780]) ).
tcf(c_46541,plain,
multiply(sk_c5,inverse(multiply(sk_c3,sk_c5))) = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_46538,c_14435]) ).
tcf(c_46886,plain,
multiply(inverse(identity),iPr_def_23) = iPr_def_23,
inference(superposition,[status(thm)],[c_1183,c_35809]) ).
tcf(c_46922,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_23 )
| ( inverse(inverse(multiply(sk_c9,sk_c4))) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_35809,c_563]) ).
tcf(c_46930,plain,
multiply(identity,iPr_def_23) = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_46886,c_11780]) ).
tcf(c_47303,plain,
inverse(multiply(inverse(iPr_def_16),sk_c7)) = sk_c8,
inference(demodulation,[status(thm)],[c_46031,c_11753]) ).
tcf(c_47317,plain,
( ~ iPr_def_15
| ( multiply(multiply(inverse(iPr_def_16),sk_c7),sk_c8) != sk_c9 )
| ( multiply(inverse(multiply(inverse(iPr_def_16),sk_c7)),sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_47303,c_558]) ).
tcf(c_47318,plain,
multiply(sk_c8,multiply(inverse(iPr_def_16),sk_c7)) = identity,
inference(superposition,[status(thm)],[c_47303,c_96]) ).
tcf(c_47333,plain,
( ~ iPr_def_15
| ( multiply(sk_c8,sk_c8) != sk_c9 )
| ( multiply(multiply(inverse(iPr_def_16),sk_c7),sk_c8) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_47317,c_47303]) ).
tcf(c_47396,plain,
multiply(iPr_def_16,multiply(inverse(iPr_def_16),sk_c7)) = multiply(sk_c7,identity),
inference(superposition,[status(thm)],[c_47318,c_3743]) ).
tcf(c_47397,plain,
multiply(iPr_def_20,multiply(inverse(iPr_def_16),sk_c7)) = multiply(sk_c5,identity),
inference(superposition,[status(thm)],[c_47318,c_3741]) ).
tcf(c_54162,plain,
multiply(inverse(identity),sk_c3) = sk_c3,
inference(superposition,[status(thm)],[c_26179,c_35811]) ).
tcf(c_54217,plain,
multiply(identity,sk_c3) = sk_c3,
inference(light_normalisation,[status(thm)],[c_54162,c_11780]) ).
tcf(c_58787,plain,
( ~ iPr_def_13
| ( sk_c9 != sk_c2 )
| ( inverse(inverse(multiply(sk_c10,iPr_def_25))) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_35812,c_560]) ).
tcf(c_58794,plain,
( ~ iPr_def_12
| ( sk_c9 != sk_c2 )
| ( inverse(inverse(multiply(sk_c8,iPr_def_25))) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_35812,c_561]) ).
tcf(c_64730,plain,
multiply(inverse(identity),sk_c6) = sk_c6,
inference(superposition,[status(thm)],[c_14501,c_35814]) ).
tcf(c_64784,plain,
multiply(identity,sk_c6) = sk_c6,
inference(light_normalisation,[status(thm)],[c_64730,c_11780]) ).
tcf(c_65509,plain,
( ( identity = iPr_def_19 )
| ( multiply(inverse(iPr_def_21),iPr_def_28) = sk_c5 ) ),
inference(superposition,[status(thm)],[c_16788,c_35815]) ).
tcf(c_65535,plain,
( ~ iPr_def_13
| ( sk_c9 != sk_c5 )
| ( inverse(inverse(multiply(sk_c10,iPr_def_21))) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_35815,c_560]) ).
tcf(c_65624,plain,
( ( identity = iPr_def_19 )
| ( multiply(sk_c5,iPr_def_28) = sk_c5 ) ),
inference(light_normalisation,[status(thm)],[c_65509,c_14435]) ).
tcf(c_68039,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(inverse(multiply(sk_c1,multiply(iPr_def_24,sk_c3))),iPr_def_28) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1149,c_45605]) ).
tcf(c_68689,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(inverse(multiply(sk_c1,identity)),iPr_def_28) = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_68039,c_1188]) ).
tcf(c_69893,plain,
multiply(inverse(identity),sk_c4) = sk_c4,
inference(superposition,[status(thm)],[c_14193,c_35816]) ).
tcf(c_69935,plain,
( ~ iPr_def_11
| ( sk_c10 != sk_c4 )
| ( inverse(inverse(multiply(sk_c8,iPr_def_23))) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_35816,c_562]) ).
tcf(c_69954,plain,
multiply(identity,sk_c4) = sk_c4,
inference(light_normalisation,[status(thm)],[c_69893,c_11780]) ).
tcf(c_70368,plain,
multiply(inverse(identity),iPr_def_25) = iPr_def_25,
inference(superposition,[status(thm)],[c_1187,c_35817]) ).
tcf(c_70438,plain,
multiply(identity,iPr_def_25) = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_70368,c_11780]) ).
tcf(c_76937,plain,
( ~ iPr_def_14
| ( sk_c8 != iPr_def_18 )
| ( inverse(inverse(multiply(sk_c9,sk_c6))) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_35818,c_559]) ).
tcf(c_79493,plain,
inverse(multiply(sk_c3,sk_c5)) = multiply(iPr_def_21,iPr_def_24),
inference(superposition,[status(thm)],[c_46541,c_3766]) ).
tcf(c_87585,plain,
( ~ iPr_def_13
| ( sk_c10 != iPr_def_23 )
| ( multiply(sk_c4,sk_c10) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_14190,c_551,c_14279]) ).
tcf(c_87589,plain,
( ~ iPr_def_13
| ( multiply(sk_c4,sk_c10) != sk_c9 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_87585,c_12548]) ).
tcf(c_93270,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_23 )
| ( multiply(sk_c4,sk_c8) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_14194,c_551,c_14279]) ).
tcf(c_94664,plain,
( ~ iPr_def_14
| ( sk_c9 != iPr_def_21 )
| ( multiply(sk_c5,sk_c9) != sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_14391,c_549,c_14435]) ).
tcf(c_94668,plain,
( ~ iPr_def_14
| ( multiply(sk_c5,sk_c9) != sk_c8 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_94664,c_12143]) ).
tcf(c_102059,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_94668,c_93270,c_87589,c_87585,c_79493,c_76937,c_69935,c_68689,c_65624,c_65535,c_58794,c_58787,c_47397,c_47396,c_47333,c_46922,c_46533,c_46531,c_46524,c_46078,c_45956,c_45950,c_45651,c_45649,c_35641,c_35629,c_35609,c_35608,c_35607,c_35605,c_35597,c_35596,c_35595,c_35594,c_35593,c_35592,c_35591,c_35541,c_35524,c_35518,c_28173,c_26467,c_26466,c_26308,c_23319,c_23318,c_21143,c_21042,c_19127,c_19126,c_19117,c_18802,c_18776,c_18669,c_18667,c_18665,c_18637,c_17428,c_16435,c_16380,c_16293,c_16184,c_16182,c_16179,c_15753,c_15748,c_15352,c_15214,c_14675,c_14592,c_14532,c_14501,c_14470,c_14440,c_14435,c_14401,c_14387,c_14289,c_14288,c_14279,c_14276,c_14193,c_13509,c_13444,c_13060,c_12740,c_12143,c_11793,c_11784,c_11782,c_11781,c_11772,c_11770,c_11766,c_11761,c_11780,c_11466,c_11463,c_6436,c_46539,c_54217,c_69954,c_3480,c_11799,c_3327,c_3140,c_64784,c_70438,c_45655,c_46930,c_1184,c_570,c_569,c_568,c_567,c_566,c_565,c_564,c_555,c_553,c_552,c_549,c_546,c_557]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP248-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/5.38 % Computer : n004.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Wed Sep 23 14:15:55 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/5.42 Running first-order theorem proving
% 0.16/5.43 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.16/5.44
% 0.16/5.44 % ======== iProver multi-core TPTP/SMT =========
% 0.16/5.44
% 0.16/5.44 % Detected problem language: tptp
% 0.16/5.45 % Proving...
% 15.76/8.29 % SZS status Started for theBenchmark.p
% 15.76/8.29 % SZS status Unsatisfiable for theBenchmark.p
% 15.76/8.29
% 15.76/8.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 15.76/8.29
% 15.76/8.29 % ------ iProver source info
% 15.76/8.29
% 15.76/8.29 % git: date: 2026-07-19 20:42:38 +0200
% 15.76/8.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 15.76/8.29 % git: non_committed_changes: false
% 15.76/8.29
% 15.76/8.29 % ------ Parsing...% successful
% 15.76/8.29
% 15.76/8.29
% 15.76/8.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 15.76/8.29
% 15.76/8.29 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 15.76/8.29
% 15.76/8.29 % ------ Preprocessing... gs_s sp: 6 0s gs_e snvd_s sp: 0 0s snvd_e %
% 15.76/8.29
% 15.76/8.29 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 15.76/8.29 % ------ Proving...
% 15.76/8.29 % ------ Problem Properties
% 15.76/8.29
% 15.76/8.29 %
% 15.76/8.29 % clauses 65
% 15.76/8.29 % conjectures 49
% 15.76/8.29 % EPR 43
% 15.76/8.29 % Horn 22
% 15.76/8.29 % unary 16
% 15.76/8.29 % binary 42
% 15.76/8.29 % lits 124
% 15.76/8.29 % lits eq 112
% 15.76/8.29 % fd_pure 0
% 15.76/8.29 % fd_pseudo 0
% 15.76/8.29 % fd_cond 0
% 15.76/8.29 % fd_pseudo_cond 0
% 15.76/8.29 % AC symbols 0
% 15.76/8.29
% 15.76/8.29 % ------ Schedule dynamic 5 is on
% 15.76/8.29
% 15.76/8.29 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 15.76/8.29
% 15.76/8.29
% 15.76/8.29 % ------
% 15.76/8.29 % Current options:
% 15.76/8.29 % ------
% 15.76/8.29
% 15.76/8.29
% 15.76/8.29 %
% 15.76/8.29
% 15.76/8.29 % ------ Proving...
% 15.76/8.29 %
% 15.76/8.29
% 15.76/8.29 % SZS status Unsatisfiable for theBenchmark.p
% 15.76/8.29
% 15.76/8.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 18.78/8.30
% 18.78/8.30
%------------------------------------------------------------------------------