%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP356-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 : n015.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:20 PM UTC 2026
% Result : Unsatisfiable 10.69s 2.72s
% Output : CNFRefutation 10.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 47
% Syntax : Number of formulae : 601 ( 150 unt; 11 def)
% Number of atoms : 2362 (1116 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 1062 ( 388 ~; 674 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 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 : 17 ( 15 usr; 16 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 147 ( 0 sgn 147 !; 0 ?; 127 :)
% 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_c7) = sk_c6
| multiply(sk_c7,sk_c6) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c6 = multiply(sk_c8,sk_c7)
| multiply(sk_c7,sk_c6) = sk_c8 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( multiply(sk_c3,sk_c8) = sk_c7
| multiply(sk_c7,sk_c6) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c7 = multiply(sk_c3,sk_c8)
| multiply(sk_c7,sk_c6) = sk_c8 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( inverse(sk_c3) = sk_c8
| multiply(sk_c7,sk_c6) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c8 = inverse(sk_c3)
| multiply(sk_c7,sk_c6) = sk_c8 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c7,sk_c6) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c7 = multiply(sk_c8,sk_c5)
| multiply(sk_c7,sk_c6) = sk_c8 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c4,sk_c8) = sk_c5
| multiply(sk_c7,sk_c6) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c5 = multiply(sk_c4,sk_c8)
| multiply(sk_c7,sk_c6) = sk_c8 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( inverse(sk_c4) = sk_c8
| multiply(sk_c7,sk_c6) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c8 = inverse(sk_c4)
| multiply(sk_c7,sk_c6) = sk_c8 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c6 = multiply(sk_c8,sk_c7)
| sk_c8 = multiply(sk_c1,sk_c7) ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( multiply(sk_c3,sk_c8) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c7 = multiply(sk_c3,sk_c8)
| sk_c8 = multiply(sk_c1,sk_c7) ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( inverse(sk_c3) = sk_c8
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c8 = inverse(sk_c3)
| sk_c8 = multiply(sk_c1,sk_c7) ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c7 = multiply(sk_c8,sk_c5)
| sk_c8 = multiply(sk_c1,sk_c7) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(sk_c4,sk_c8) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c5 = multiply(sk_c4,sk_c8)
| sk_c8 = multiply(sk_c1,sk_c7) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( inverse(sk_c4) = sk_c8
| multiply(sk_c1,sk_c7) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f28,plain,
( sk_c8 = inverse(sk_c4)
| sk_c8 = multiply(sk_c1,sk_c7) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f30,plain,
( sk_c6 = multiply(sk_c8,sk_c7)
| sk_c7 = inverse(sk_c1) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( multiply(sk_c3,sk_c8) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c7 = multiply(sk_c3,sk_c8)
| sk_c7 = inverse(sk_c1) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( inverse(sk_c3) = sk_c8
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c8 = inverse(sk_c3)
| sk_c7 = inverse(sk_c1) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( multiply(sk_c8,sk_c5) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f36,plain,
( sk_c7 = multiply(sk_c8,sk_c5)
| sk_c7 = inverse(sk_c1) ),
inference(reorient_equations,[],[f35]) ).
fof(f37,negated_conjecture,
( multiply(sk_c4,sk_c8) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c5 = multiply(sk_c4,sk_c8)
| sk_c7 = inverse(sk_c1) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( inverse(sk_c4) = sk_c8
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c8 = inverse(sk_c4)
| sk_c7 = inverse(sk_c1) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c6
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_19) ).
fof(f42,plain,
( sk_c6 = multiply(sk_c8,sk_c7)
| sk_c6 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( multiply(sk_c3,sk_c8) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_20) ).
fof(f44,plain,
( sk_c7 = multiply(sk_c3,sk_c8)
| sk_c6 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c3) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c8 = inverse(sk_c3)
| sk_c6 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( multiply(sk_c8,sk_c5) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f48,plain,
( sk_c7 = multiply(sk_c8,sk_c5)
| sk_c6 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f47]) ).
fof(f51,negated_conjecture,
( inverse(sk_c4) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c8 = inverse(sk_c4)
| sk_c6 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c6
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c6 = multiply(sk_c8,sk_c7)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c3,sk_c8) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c7 = multiply(sk_c3,sk_c8)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( inverse(sk_c3) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_27) ).
fof(f58,plain,
( sk_c8 = inverse(sk_c3)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( multiply(sk_c8,sk_c5) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c7 = multiply(sk_c8,sk_c5)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( multiply(sk_c4,sk_c8) = sk_c5
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c5 = multiply(sk_c4,sk_c8)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( inverse(sk_c4) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c8 = inverse(sk_c4)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
! [X2,X3,X0,X1,X4] :
( inverse(X4) != sk_c8
| multiply(X4,sk_c8) != X3
| multiply(sk_c8,X3) != sk_c7
| inverse(X2) != sk_c8
| multiply(X2,sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c6
| inverse(X1) != sk_c8
| multiply(X1,sk_c8) != sk_c6
| inverse(X0) != sk_c7
| multiply(X0,sk_c7) != sk_c8
| multiply(sk_c7,sk_c6) != sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
! [X2,X3,X0,X1,X4] :
( sk_c8 != inverse(X4)
| multiply(X4,sk_c8) != X3
| sk_c7 != multiply(sk_c8,X3)
| sk_c8 != inverse(X2)
| sk_c7 != multiply(X2,sk_c8)
| sk_c6 != multiply(sk_c8,sk_c7)
| sk_c8 != inverse(X1)
| sk_c6 != multiply(X1,sk_c8)
| inverse(X0) != sk_c7
| sk_c8 != multiply(X0,sk_c7)
| multiply(sk_c7,sk_c6) != sk_c8 ),
inference(reorient_equations,[],[f65]) ).
fof(f67,plain,
! [X2,X0,X1,X4] :
( sk_c8 != inverse(X4)
| sk_c7 != multiply(sk_c8,multiply(X4,sk_c8))
| sk_c8 != inverse(X2)
| sk_c7 != multiply(X2,sk_c8)
| sk_c6 != multiply(sk_c8,sk_c7)
| sk_c8 != inverse(X1)
| sk_c6 != multiply(X1,sk_c8)
| inverse(X0) != sk_c7
| sk_c8 != multiply(X0,sk_c7)
| multiply(sk_c7,sk_c6) != sk_c8 ),
inference(equality_resolution,[],[f66]) ).
tcf(c_83,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_84,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_86,negated_conjecture,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c7,sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_87,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_88,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c7,sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_89,negated_conjecture,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_90,negated_conjecture,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( multiply(sk_c7,sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_91,negated_conjecture,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c7,sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_92,negated_conjecture,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_93,negated_conjecture,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_94,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_95,negated_conjecture,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_96,negated_conjecture,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_97,negated_conjecture,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_98,negated_conjecture,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_99,negated_conjecture,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_100,negated_conjecture,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_101,negated_conjecture,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_102,negated_conjecture,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_103,negated_conjecture,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_104,negated_conjecture,
( ( multiply(sk_c2,sk_c8) = sk_c6 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_105,negated_conjecture,
( ( multiply(sk_c2,sk_c8) = sk_c6 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_107,negated_conjecture,
( ( multiply(sk_c2,sk_c8) = sk_c6 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_112,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_116,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(X3) != sk_c8 )
| ( inverse(X2) != sk_c8 )
| ( inverse(X1) != sk_c8 )
| ( inverse(X0) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c8 )
| ( multiply(X3,sk_c8) != sk_c6 )
| ( multiply(X2,sk_c8) != sk_c7 )
| ( multiply(X0,sk_c7) != sk_c8 )
| ( multiply(sk_c8,multiply(X1,sk_c8)) != sk_c7 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_117,plain,
multiply(identity,sk_c8) = sk_c8,
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_409,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_116]) ).
tcf(c_410,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_116]) ).
tcf(c_411,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c6 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_116]) ).
tcf(c_412,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c8 )
| ( multiply(sk_c8,multiply(X0,sk_c8)) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_116]) ).
tcf(c_413,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c8,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_116]) ).
tcf(c_414,definition,
iPr_def_14 = multiply(sk_c7,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_415,definition,
iPr_def_15 = multiply(sk_c8,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_416,definition,
iPr_def_16 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_417,definition,
iPr_def_17 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_418,definition,
iPr_def_18 = multiply(sk_c4,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_419,definition,
iPr_def_19 = multiply(sk_c8,sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_420,definition,
iPr_def_20 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_421,definition,
iPr_def_21 = multiply(sk_c3,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_422,definition,
iPr_def_22 = multiply(sk_c2,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_423,definition,
iPr_def_23 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_424,definition,
iPr_def_24 = multiply(sk_c1,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_425,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 != sk_c6 )
| ( iPr_def_14 != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_413,c_415,c_414]) ).
tcf(c_426,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c8 )
| ( multiply(sk_c8,multiply(X0,sk_c8)) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_412]) ).
tcf(c_427,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c6 ) ),
inference(demodulation,[status(thm)],[c_411]) ).
tcf(c_428,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_410]) ).
tcf(c_429,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_409]) ).
tcf(c_430,negated_conjecture,
( ( iPr_def_17 = sk_c8 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_115,c_417,c_416]) ).
tcf(c_431,negated_conjecture,
( ( iPr_def_18 = sk_c5 )
| ( iPr_def_17 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_114,c_418]) ).
tcf(c_432,negated_conjecture,
( ( iPr_def_19 = sk_c7 )
| ( iPr_def_17 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_113,c_419]) ).
tcf(c_433,negated_conjecture,
( ( iPr_def_20 = sk_c8 )
| ( iPr_def_17 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_112,c_420]) ).
tcf(c_434,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_17 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_111,c_421]) ).
tcf(c_435,negated_conjecture,
( ( iPr_def_17 = sk_c8 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_436,negated_conjecture,
( ( iPr_def_22 = sk_c6 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_109,c_422]) ).
tcf(c_438,negated_conjecture,
( ( iPr_def_22 = sk_c6 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_439,negated_conjecture,
( ( iPr_def_22 = sk_c6 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_440,negated_conjecture,
( ( iPr_def_22 = sk_c6 )
| ( iPr_def_21 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_441,negated_conjecture,
( ( iPr_def_22 = sk_c6 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_104]) ).
tcf(c_442,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_103,c_423]) ).
tcf(c_443,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_18 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_102]) ).
tcf(c_444,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_101]) ).
tcf(c_445,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_100]) ).
tcf(c_446,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_21 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_99]) ).
tcf(c_447,negated_conjecture,
( ( iPr_def_23 = sk_c7 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_98]) ).
tcf(c_448,negated_conjecture,
( ( iPr_def_24 = sk_c8 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_97,c_424]) ).
tcf(c_449,negated_conjecture,
( ( iPr_def_24 = sk_c8 )
| ( iPr_def_18 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_96]) ).
tcf(c_450,negated_conjecture,
( ( iPr_def_24 = sk_c8 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_95]) ).
tcf(c_451,negated_conjecture,
( ( iPr_def_24 = sk_c8 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_94]) ).
tcf(c_452,negated_conjecture,
( ( iPr_def_24 = sk_c8 )
| ( iPr_def_21 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_93]) ).
tcf(c_453,negated_conjecture,
( ( iPr_def_24 = sk_c8 )
| ( iPr_def_15 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_92]) ).
tcf(c_454,negated_conjecture,
( ( iPr_def_16 = sk_c8 )
| ( iPr_def_14 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_91]) ).
tcf(c_455,negated_conjecture,
( ( iPr_def_18 = sk_c5 )
| ( iPr_def_14 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_90]) ).
tcf(c_456,negated_conjecture,
( ( iPr_def_19 = sk_c7 )
| ( iPr_def_14 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_89]) ).
tcf(c_457,negated_conjecture,
( ( iPr_def_20 = sk_c8 )
| ( iPr_def_14 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_88]) ).
tcf(c_458,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_14 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_87]) ).
tcf(c_459,negated_conjecture,
( ( iPr_def_15 = sk_c6 )
| ( iPr_def_14 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_86]) ).
tcf(c_460,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_461,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_462,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_466,plain,
sk_c8 = sk_c8,
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_696,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( sk_c8 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_432,c_434]) ).
tcf(c_719,plain,
( ( sk_c8 = iPr_def_16 )
| ( multiply(sk_c7,iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_436,c_414]) ).
tcf(c_729,plain,
( ( sk_c8 = iPr_def_17 )
| ( multiply(iPr_def_20,sk_c7) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_433,c_415]) ).
tcf(c_747,plain,
( ( sk_c8 = iPr_def_17 )
| ( multiply(iPr_def_20,sk_c5) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_433,c_419]) ).
tcf(c_764,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c7,iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_438,c_414]) ).
tcf(c_776,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(sk_c7,iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_439,c_414]) ).
tcf(c_788,plain,
( ( sk_c7 = iPr_def_21 )
| ( multiply(sk_c7,iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_440,c_414]) ).
tcf(c_831,plain,
( ( sk_c7 = iPr_def_23 )
| ( multiply(sk_c8,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_443,c_419]) ).
tcf(c_880,plain,
( ( sk_c8 = iPr_def_17 )
| ( multiply(sk_c2,iPr_def_20) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_433,c_422]) ).
tcf(c_886,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_445,c_424]) ).
tcf(c_887,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_444,c_424]) ).
tcf(c_888,plain,
( ( sk_c8 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_442,c_424]) ).
tcf(c_901,plain,
! [X0: $i] :
( ( iPr_def_14 = sk_c8 )
| ( iPr_def_14 != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_902,plain,
( ( iPr_def_14 = sk_c8 )
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c8 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_901]) ).
tcf(c_903,plain,
iPr_def_14 = iPr_def_14,
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_904,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_906,plain,
multiply(iPr_def_20,sk_c3) = identity,
inference(superposition,[status(thm)],[c_420,c_84]) ).
tcf(c_907,plain,
multiply(iPr_def_16,sk_c4) = identity,
inference(superposition,[status(thm)],[c_416,c_84]) ).
tcf(c_908,plain,
multiply(iPr_def_23,sk_c1) = identity,
inference(superposition,[status(thm)],[c_423,c_84]) ).
tcf(c_909,plain,
multiply(iPr_def_17,sk_c2) = identity,
inference(superposition,[status(thm)],[c_417,c_84]) ).
tcf(c_910,plain,
! [X0: $i] :
( ( sk_c8 = iPr_def_14 )
| ( iPr_def_14 != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_911,plain,
( ( sk_c8 = iPr_def_14 )
| ( iPr_def_14 != sk_c8 )
| ( sk_c8 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_910]) ).
tcf(c_918,plain,
( ( sk_c7 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_446,c_424]) ).
tcf(c_936,plain,
! [X0: $i] :
( ( sk_c8 = multiply(sk_c7,sk_c6) )
| ( sk_c8 != X0 )
| ( multiply(sk_c7,sk_c6) != X0 ) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_945,plain,
( ( sk_c8 = iPr_def_14 )
| ( iPr_def_14 != multiply(sk_c7,sk_c6) )
| ( sk_c8 != multiply(sk_c7,sk_c6) ) ),
inference(instantiation,[status(thm)],[c_910]) ).
tcf(c_956,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( sk_c6 = iPr_def_15 )
| ( sk_c7 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_447,c_441]) ).
tcf(c_981,plain,
! [X0: $i,X1: $i] :
( ( sk_c8 = multiply(sk_c7,sk_c6) )
| ( sk_c8 != multiply(X0,X1) )
| ( multiply(sk_c7,sk_c6) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_936]) ).
tcf(c_982,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c7,sk_c6) = multiply(X0,X1) )
| ( sk_c6 != X1 )
| ( sk_c7 != X0 ) ),
inference(instantiation,[status(thm)],[c_462]) ).
tcf(c_983,plain,
( ( sk_c8 = multiply(sk_c7,sk_c6) )
| ( sk_c8 != multiply(sk_c8,sk_c8) )
| ( multiply(sk_c7,sk_c6) != multiply(sk_c8,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_981]) ).
tcf(c_984,plain,
( ( multiply(sk_c7,sk_c6) = multiply(sk_c8,sk_c8) )
| ( sk_c6 != sk_c8 )
| ( sk_c7 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_982]) ).
tcf(c_997,plain,
( ( iPr_def_17 = iPr_def_24 )
| ( sk_c8 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_448,c_430]) ).
tcf(c_1026,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(sk_c8,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_449,c_419]) ).
tcf(c_1032,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_1049,plain,
( ( sk_c8 = iPr_def_24 )
| ( multiply(iPr_def_19,sk_c6) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_450,c_414]) ).
tcf(c_1083,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_451,c_421]) ).
tcf(c_1126,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( sk_c8 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_452,c_450]) ).
tcf(c_1155,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c8 = multiply(X0,X1) )
| ( sk_c8 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_1158,plain,
sk_c7 = sk_c7,
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_1160,plain,
! [X0: $i,X1: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_1175,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c7 )
| ( sk_c7 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_1225,plain,
( ( sk_c8 = iPr_def_14 )
| ( multiply(iPr_def_16,sk_c5) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_454,c_419]) ).
tcf(c_1297,plain,
( ( sk_c8 = iPr_def_14 )
| ( multiply(sk_c1,iPr_def_19) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_456,c_424]) ).
tcf(c_1330,plain,
( ( iPr_def_16 = iPr_def_20 )
| ( sk_c8 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_457,c_454]) ).
tcf(c_1334,plain,
( ( sk_c8 = iPr_def_14 )
| ( multiply(sk_c3,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_457,c_421]) ).
tcf(c_1337,plain,
( ( sk_c8 = iPr_def_14 )
| ( multiply(iPr_def_20,sk_c7) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_457,c_415]) ).
tcf(c_1385,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( sk_c8 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_458,c_456]) ).
tcf(c_1388,plain,
( ( sk_c8 = iPr_def_14 )
| ( multiply(sk_c1,iPr_def_21) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_458,c_424]) ).
tcf(c_1417,plain,
! [X0: $i] :
( ( iPr_def_14 = sk_c7 )
| ( iPr_def_14 != X0 )
| ( sk_c7 != X0 ) ),
inference(instantiation,[status(thm)],[c_904]) ).
tcf(c_1437,plain,
! [X0: $i] :
( ( sk_c7 = iPr_def_14 )
| ( iPr_def_14 != X0 )
| ( sk_c7 != X0 ) ),
inference(instantiation,[status(thm)],[c_1032]) ).
tcf(c_1450,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( sk_c8 = iPr_def_14 )
| ( sk_c6 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_459,c_441]) ).
tcf(c_1486,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_17) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_696,c_422]) ).
tcf(c_1532,plain,
sk_c6 = sk_c6,
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_1651,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( multiply(iPr_def_24,sk_c5) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1126,c_419]) ).
tcf(c_1653,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( multiply(iPr_def_24,sk_c7) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_1126,c_415]) ).
tcf(c_1672,plain,
! [X0: $i,X1: $i] :
( ( sk_c6 = X0 )
| ( sk_c6 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_1674,plain,
! [X0: $i] :
( ( sk_c6 = iPr_def_14 )
| ( iPr_def_14 != X0 )
| ( sk_c6 != X0 ) ),
inference(instantiation,[status(thm)],[c_1032]) ).
tcf(c_1727,plain,
( ( iPr_def_16 = iPr_def_20 )
| ( iPr_def_14 = iPr_def_17 )
| ( sk_c8 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1330,c_430]) ).
tcf(c_1795,plain,
! [X0: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != sk_c7 )
| ( X0 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1160]) ).
tcf(c_1805,plain,
! [X0: $i] :
( ( sk_c8 = multiply(identity,X0) )
| ( sk_c8 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_1155]) ).
tcf(c_1806,plain,
( ( sk_c8 = multiply(identity,sk_c8) )
| ( sk_c8 != sk_c8 )
| ( multiply(identity,sk_c8) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1805]) ).
tcf(c_1813,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sk_c8 = multiply(X0,X1) )
| ( sk_c8 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_1155]) ).
tcf(c_1939,plain,
( ~ iPr_def_12
| ( sk_c6 != iPr_def_22 )
| ( inverse(sk_c2) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_422,c_427]) ).
tcf(c_1940,plain,
( ~ iPr_def_12
| ( sk_c6 != sk_c8 )
| ( inverse(identity) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_83,c_427]) ).
tcf(c_1941,plain,
( ~ iPr_def_12
| ( sk_c6 != identity )
| ( inverse(inverse(sk_c8)) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_84,c_427]) ).
tcf(c_1955,plain,
( ~ iPr_def_12
| ( sk_c8 != iPr_def_17 )
| ( sk_c6 != iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_1939,c_417]) ).
tcf(c_2068,plain,
( ~ iPr_def_11
| ( sk_c8 != iPr_def_15 )
| ( inverse(sk_c8) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_415,c_428]) ).
tcf(c_2070,plain,
( ~ iPr_def_11
| ( sk_c7 != sk_c8 )
| ( inverse(identity) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_83,c_428]) ).
tcf(c_2184,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_21 )
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_421,c_429]) ).
tcf(c_2187,plain,
( ~ iPr_def_10
| ( sk_c7 != sk_c8 )
| ( inverse(identity) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_83,c_429]) ).
tcf(c_2188,plain,
( ~ iPr_def_10
| ( sk_c7 != identity )
| ( inverse(inverse(sk_c8)) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_84,c_429]) ).
tcf(c_2210,plain,
( ~ iPr_def_10
| ( sk_c8 != iPr_def_20 )
| ( sk_c7 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_2184,c_420]) ).
tcf(c_2327,plain,
( ~ iPr_def_13
| ( inverse(inverse(sk_c8)) != sk_c8 )
| ( multiply(sk_c8,identity) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_84,c_426]) ).
tcf(c_2485,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( iPr_def_14 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1385,c_1126]) ).
tcf(c_2681,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_2683,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_2688,plain,
! [X0: $i] :
( ( iPr_def_14 = identity )
| ( iPr_def_14 != X0 )
| ( identity != X0 ) ),
inference(instantiation,[status(thm)],[c_904]) ).
tcf(c_2789,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c8,X0)) = multiply(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_421,c_85]) ).
tcf(c_2791,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c8,X0)) = multiply(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_418,c_85]) ).
tcf(c_2792,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c7,X0)) = multiply(iPr_def_24,X0),
inference(superposition,[status(thm)],[c_424,c_85]) ).
tcf(c_2793,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c8,X0)) = multiply(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_422,c_85]) ).
tcf(c_2795,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_84,c_85]) ).
tcf(c_2799,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_906,c_85]) ).
tcf(c_2800,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_907,c_85]) ).
tcf(c_2801,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_908,c_85]) ).
tcf(c_2802,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_909,c_85]) ).
tcf(c_2808,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2802,c_83]) ).
tcf(c_2809,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2801,c_83]) ).
tcf(c_2810,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2800,c_83]) ).
tcf(c_2811,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2799,c_83]) ).
tcf(c_2956,plain,
multiply(iPr_def_23,iPr_def_24) = sk_c7,
inference(superposition,[status(thm)],[c_424,c_2809]) ).
tcf(c_3047,plain,
( ( sk_c8 = iPr_def_16 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_442,c_719]) ).
tcf(c_3151,plain,
( ( sk_c8 = iPr_def_17 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_434,c_729]) ).
tcf(c_3373,plain,
! [X0: $i] :
( ( sk_c6 = X0 )
| ( sk_c6 != sk_c6 )
| ( X0 != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_1672]) ).
tcf(c_3597,plain,
multiply(iPr_def_16,iPr_def_18) = sk_c8,
inference(superposition,[status(thm)],[c_418,c_2810]) ).
tcf(c_3620,plain,
multiply(iPr_def_20,iPr_def_21) = sk_c8,
inference(superposition,[status(thm)],[c_421,c_2811]) ).
tcf(c_3636,plain,
( ( sk_c8 = iPr_def_17 )
| ( multiply(iPr_def_20,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_431,c_747]) ).
tcf(c_3685,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c8 = multiply(X0,X1) )
| ( sk_c8 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_1813]) ).
tcf(c_3686,plain,
( ( sk_c8 = multiply(sk_c8,sk_c8) )
| ( sk_c8 != multiply(identity,sk_c8) )
| ( multiply(sk_c8,sk_c8) != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_3685]) ).
tcf(c_3777,plain,
( ( iPr_def_14 = sk_c7 )
| ( iPr_def_14 != iPr_def_19 )
| ( sk_c7 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1417]) ).
tcf(c_3778,plain,
( ( sk_c7 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_19 )
| ( sk_c7 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1437]) ).
tcf(c_3781,plain,
! [X0: $i] :
( ( X0 = sk_c7 )
| ( sk_c7 != iPr_def_19 )
| ( X0 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1175]) ).
tcf(c_3782,plain,
! [X0: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != iPr_def_19 )
| ( X0 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1160]) ).
tcf(c_3783,plain,
( ( sk_c7 = sk_c8 )
| ( sk_c8 != iPr_def_19 )
| ( sk_c7 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_3782]) ).
tcf(c_3784,plain,
( ( sk_c8 = sk_c7 )
| ( sk_c8 != iPr_def_19 )
| ( sk_c7 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_3781]) ).
tcf(c_3789,plain,
! [X0: $i] :
( ( X0 = sk_c7 )
| ( sk_c7 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1175]) ).
tcf(c_3790,plain,
! [X0: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1160]) ).
tcf(c_3869,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_444,c_764]) ).
tcf(c_3907,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_445,c_776]) ).
tcf(c_4314,plain,
( ( sk_c7 = iPr_def_23 )
| ( iPr_def_23 != sk_c7 )
| ( sk_c7 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1795]) ).
tcf(c_4627,plain,
( ( sk_c8 = iPr_def_20 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_886,c_2809]) ).
tcf(c_4628,plain,
( ( sk_c8 = iPr_def_20 )
| ( sk_c7 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_4627,c_2956]) ).
tcf(c_4639,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_887,c_2809]) ).
tcf(c_4640,plain,
( ( sk_c7 = iPr_def_23 )
| ( sk_c7 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_4639,c_2956]) ).
tcf(c_4688,plain,
( ( sk_c7 = iPr_def_21 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_918,c_2809]) ).
tcf(c_4689,plain,
( ( sk_c7 = iPr_def_23 )
| ( sk_c7 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_4688,c_2956]) ).
tcf(c_5320,plain,
! [X0: $i] :
( ( identity = iPr_def_14 )
| ( iPr_def_14 != X0 )
| ( identity != X0 ) ),
inference(instantiation,[status(thm)],[c_1032]) ).
tcf(c_5939,plain,
( ( sk_c8 = iPr_def_14 )
| ( multiply(iPr_def_16,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_455,c_1225]) ).
tcf(c_5945,plain,
( ( sk_c8 = iPr_def_19 )
| ( sk_c8 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_5939,c_3597]) ).
tcf(c_6133,plain,
( ( sk_c8 = iPr_def_14 )
| ( multiply(sk_c2,iPr_def_16) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_454,c_422]) ).
tcf(c_7084,plain,
( ( sk_c8 = iPr_def_14 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1297,c_2809]) ).
tcf(c_7085,plain,
( ( sk_c8 = iPr_def_14 )
| ( sk_c7 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_7084,c_2956]) ).
tcf(c_7199,plain,
( ( sk_c8 = iPr_def_14 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_458,c_1337]) ).
tcf(c_7211,plain,
( ( sk_c8 = iPr_def_15 )
| ( sk_c8 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_7199,c_3620]) ).
tcf(c_7275,plain,
( ( iPr_def_15 = iPr_def_20 )
| ( sk_c8 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_7211,c_457]) ).
tcf(c_7556,plain,
( ( iPr_def_15 = iPr_def_20 )
| ( multiply(iPr_def_14,sk_c7) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_7275,c_415]) ).
tcf(c_7939,plain,
( ( sk_c6 = iPr_def_15 )
| ( iPr_def_15 != sk_c6 )
| ( sk_c6 != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_3373]) ).
tcf(c_8130,plain,
( ( sk_c8 = iPr_def_14 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_1388,c_2809]) ).
tcf(c_8131,plain,
( ( sk_c8 = iPr_def_14 )
| ( sk_c7 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_8130,c_2956]) ).
tcf(c_8783,plain,
( ( sk_c8 = iPr_def_17 )
| ( sk_c8 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_3151,c_3620]) ).
tcf(c_9692,plain,
( ( sk_c7 = iPr_def_23 )
| ( sk_c6 = iPr_def_15 ) ),
inference(global_subsumption_just,[status(thm)],[c_956,c_447,c_1158,c_1532,c_4314,c_7939]) ).
tcf(c_9693,plain,
( ( sk_c6 = iPr_def_15 )
| ( sk_c7 = iPr_def_23 ) ),
inference(renaming,[status(thm)],[c_9692]) ).
tcf(c_10186,plain,
( ( iPr_def_14 = identity )
| ( iPr_def_14 != sk_c7 )
| ( identity != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_2688]) ).
tcf(c_10699,plain,
multiply(sk_c1,iPr_def_14) = multiply(iPr_def_24,sk_c6),
inference(superposition,[status(thm)],[c_414,c_2792]) ).
tcf(c_10910,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = multiply(identity,X2) )
| ( X1 != X2 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_462]) ).
tcf(c_10911,plain,
( ( multiply(sk_c8,sk_c8) = multiply(identity,sk_c8) )
| ( sk_c8 != identity )
| ( sk_c8 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_10910]) ).
tcf(c_11184,plain,
( ( sk_c6 = iPr_def_15 )
| ( sk_c8 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_1450,c_466,c_459,c_911,c_1532,c_7939]) ).
tcf(c_11185,plain,
( ( sk_c8 = iPr_def_14 )
| ( sk_c6 = iPr_def_15 ) ),
inference(renaming,[status(thm)],[c_11184]) ).
tcf(c_12113,plain,
! [X0: $i] :
( ( sk_c6 = X0 )
| ( sk_c6 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1672]) ).
tcf(c_12116,plain,
( ( sk_c6 = sk_c8 )
| ( sk_c8 != iPr_def_15 )
| ( sk_c6 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_12113]) ).
tcf(c_12120,plain,
( ( sk_c6 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_15 )
| ( sk_c6 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1674]) ).
tcf(c_13013,plain,
( ( iPr_def_16 = iPr_def_20 )
| ( iPr_def_14 = iPr_def_17 )
| ( sk_c8 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1727,c_457]) ).
tcf(c_13021,plain,
( ( iPr_def_16 = iPr_def_20 )
| ( iPr_def_14 = iPr_def_17 )
| ( sk_c8 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_1727,c_433]) ).
tcf(c_13236,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != sk_c7 )
| ( X0 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_2683]) ).
tcf(c_13239,plain,
( ( sk_c8 = identity )
| ( identity != sk_c7 )
| ( sk_c8 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_13236]) ).
tcf(c_13892,plain,
( ( iPr_def_15 = iPr_def_20 )
| ~ iPr_def_11
| ( sk_c8 != iPr_def_15 )
| ( inverse(iPr_def_14) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_7556,c_428]) ).
tcf(c_18059,plain,
( ( identity = sk_c7 )
| ( identity != iPr_def_21 )
| ( sk_c7 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_3789]) ).
tcf(c_19302,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_2795,c_83]) ).
tcf(c_19307,plain,
multiply(inverse(sk_c7),iPr_def_14) = sk_c6,
inference(superposition,[status(thm)],[c_414,c_19302]) ).
tcf(c_19314,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_83,c_19302]) ).
tcf(c_19315,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_84,c_19302]) ).
tcf(c_19466,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_2811,c_19302]) ).
tcf(c_19467,plain,
! [X0: $i] : multiply(inverse(iPr_def_16),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_2810,c_19302]) ).
tcf(c_19468,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_2809,c_19302]) ).
tcf(c_19469,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_2808,c_19302]) ).
tcf(c_19526,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_19302,c_19302]) ).
tcf(c_21078,plain,
( ( sk_c7 = identity )
| ( identity != iPr_def_21 )
| ( sk_c7 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_3790]) ).
tcf(c_22078,plain,
( ( identity = iPr_def_14 )
| ( iPr_def_14 != identity )
| ( identity != identity ) ),
inference(instantiation,[status(thm)],[c_5320]) ).
tcf(c_22483,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_19315,c_19526]) ).
tcf(c_22509,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_22483,c_19314]) ).
tcf(c_22574,plain,
( ( sk_c8 = iPr_def_16 )
| ~ iPr_def_12
| ( sk_c6 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_430,c_1955]) ).
tcf(c_23158,plain,
( ( sk_c8 = iPr_def_16 )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_436,c_22574]) ).
tcf(c_26775,plain,
multiply(sk_c3,iPr_def_20) = identity,
inference(superposition,[status(thm)],[c_19466,c_84]) ).
tcf(c_26782,plain,
multiply(sk_c3,identity) = inverse(iPr_def_20),
inference(superposition,[status(thm)],[c_19466,c_22483]) ).
tcf(c_26798,plain,
( ( identity = iPr_def_21 )
| ( sk_c8 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1334,c_26775]) ).
tcf(c_27048,plain,
sk_c8 = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_13013,c_117,c_466,c_414,c_945,c_983,c_984,c_1806,c_3686,c_3783,c_3784,c_5945,c_7085,c_7211,c_8131,c_10911,c_11185,c_12116,c_13239,c_18059,c_26798]) ).
tcf(c_27070,plain,
( ( iPr_def_14 = iPr_def_16 )
| ~ iPr_def_12 ),
inference(demodulation,[status(thm)],[c_23158,c_27048]) ).
tcf(c_27130,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_14,X0)) = multiply(iPr_def_22,X0),
inference(demodulation,[status(thm)],[c_2793,c_27048]) ).
tcf(c_27132,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_14,X0)) = multiply(iPr_def_18,X0),
inference(demodulation,[status(thm)],[c_2791,c_27048]) ).
tcf(c_27134,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_14,X0)) = multiply(iPr_def_21,X0),
inference(demodulation,[status(thm)],[c_2789,c_27048]) ).
tcf(c_27147,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_3907,c_27048]) ).
tcf(c_27148,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( multiply(iPr_def_20,iPr_def_18) = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_3636,c_27048]) ).
tcf(c_27151,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_8783,c_27048]) ).
tcf(c_27152,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_3047,c_27048]) ).
tcf(c_27187,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_1083,c_27048]) ).
tcf(c_27189,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( multiply(iPr_def_19,sk_c6) = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1049,c_27048]) ).
tcf(c_27192,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( multiply(iPr_def_14,iPr_def_18) = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1026,c_27048]) ).
tcf(c_27204,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_888,c_27048]) ).
tcf(c_27205,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_886,c_27048]) ).
tcf(c_27207,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( multiply(sk_c2,iPr_def_20) = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_880,c_27048]) ).
tcf(c_27214,plain,
( ( sk_c7 = iPr_def_23 )
| ( multiply(iPr_def_14,iPr_def_18) = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_831,c_27048]) ).
tcf(c_27217,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( multiply(sk_c7,iPr_def_22) = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_776,c_27048]) ).
tcf(c_27223,plain,
multiply(iPr_def_16,iPr_def_18) = iPr_def_14,
inference(demodulation,[status(thm)],[c_3597,c_27048]) ).
tcf(c_27231,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(sk_c7,iPr_def_22) = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_719,c_27048]) ).
tcf(c_27236,plain,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != iPr_def_14 )
| ( multiply(X0,iPr_def_14) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_429,c_27048]) ).
tcf(c_27237,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_428,c_27048]) ).
tcf(c_27238,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != iPr_def_14 )
| ( multiply(X0,iPr_def_14) != sk_c6 ) ),
inference(demodulation,[status(thm)],[c_427,c_27048]) ).
tcf(c_27239,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c6 != iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_425,c_27048]) ).
tcf(c_27241,plain,
( ( iPr_def_17 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_997,c_27048]) ).
tcf(c_27249,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( sk_c6 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_453,c_27048]) ).
tcf(c_27251,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_451,c_27048]) ).
tcf(c_27252,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( sk_c7 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_450,c_27048]) ).
tcf(c_27254,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_448,c_27048]) ).
tcf(c_27255,plain,
multiply(sk_c2,iPr_def_14) = iPr_def_22,
inference(demodulation,[status(thm)],[c_422,c_27048]) ).
tcf(c_27256,plain,
multiply(sk_c3,iPr_def_14) = iPr_def_21,
inference(demodulation,[status(thm)],[c_421,c_27048]) ).
tcf(c_27257,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( sk_c7 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_445,c_27048]) ).
tcf(c_27258,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c7 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_442,c_27048]) ).
tcf(c_27259,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( sk_c6 = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_439,c_27048]) ).
tcf(c_27261,plain,
multiply(sk_c4,iPr_def_14) = iPr_def_18,
inference(demodulation,[status(thm)],[c_418,c_27048]) ).
tcf(c_27262,plain,
multiply(iPr_def_14,sk_c7) = iPr_def_15,
inference(demodulation,[status(thm)],[c_415,c_27048]) ).
tcf(c_27263,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c6 = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_436,c_27048]) ).
tcf(c_27264,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( sk_c6 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_435,c_27048]) ).
tcf(c_27265,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( sk_c7 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_434,c_27048]) ).
tcf(c_27266,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( iPr_def_14 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_433,c_27048]) ).
tcf(c_27267,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( sk_c7 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_432,c_27048]) ).
tcf(c_27269,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_430,c_27048]) ).
tcf(c_27471,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c6 != iPr_def_15 ) ),
inference(equality_resolution_simp,[status(thm)],[c_27239]) ).
tcf(c_27781,plain,
inverse(iPr_def_20) = sk_c3,
inference(demodulation,[status(thm)],[c_26782,c_22483]) ).
tcf(c_27875,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( inverse(iPr_def_14) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_27266,c_27781]) ).
tcf(c_27877,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( multiply(sk_c3,iPr_def_14) = identity ) ),
inference(superposition,[status(thm)],[c_27266,c_26775]) ).
tcf(c_27884,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( identity = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_27877,c_27256]) ).
tcf(c_27971,plain,
( ( iPr_def_16 = iPr_def_20 )
| ( iPr_def_14 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_13021,c_27048]) ).
tcf(c_28174,plain,
( ~ iPr_def_12
| ( identity != iPr_def_14 )
| ( sk_c6 != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_1940,c_22509,c_27048]) ).
tcf(c_28184,plain,
( ( iPr_def_14 = iPr_def_17 )
| ~ iPr_def_12
| ( iPr_def_14 != iPr_def_15 )
| ( identity != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_27264,c_28174]) ).
tcf(c_28213,plain,
( ~ iPr_def_11
| ( iPr_def_14 != iPr_def_15 )
| ( inverse(iPr_def_14) != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_2068,c_27048]) ).
tcf(c_28223,plain,
( ~ iPr_def_11
| ( sk_c7 != iPr_def_14 )
| ( sk_c7 != identity ) ),
inference(light_normalisation,[status(thm)],[c_2070,c_22509,c_27048]) ).
tcf(c_28233,plain,
( ( iPr_def_14 = iPr_def_17 )
| ~ iPr_def_11
| ( iPr_def_14 != iPr_def_19 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm)],[c_27267,c_28223]) ).
tcf(c_28275,plain,
( ~ iPr_def_10
| ( identity != iPr_def_14 )
| ( sk_c7 != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_2187,c_22509,c_27048]) ).
tcf(c_28293,plain,
( ( sk_c7 = iPr_def_21 )
| ~ iPr_def_10
| ( iPr_def_14 != iPr_def_23 )
| ( identity != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_446,c_28275]) ).
tcf(c_28294,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_10
| ( iPr_def_14 != iPr_def_23 )
| ( identity != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_444,c_28275]) ).
tcf(c_28485,plain,
( ~ iPr_def_12
| ( sk_c6 != identity )
| ( inverse(inverse(iPr_def_14)) != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_1941,c_27048]) ).
tcf(c_28624,plain,
multiply(sk_c4,iPr_def_16) = identity,
inference(superposition,[status(thm)],[c_19467,c_84]) ).
tcf(c_28627,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_16,X0)) = X0,
inference(superposition,[status(thm)],[c_19467,c_19302]) ).
tcf(c_28644,plain,
( ~ iPr_def_10
| ( sk_c7 != identity )
| ( inverse(inverse(iPr_def_14)) != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_2188,c_27048]) ).
tcf(c_28750,plain,
multiply(sk_c1,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_19468,c_84]) ).
tcf(c_28754,plain,
multiply(sk_c1,identity) = inverse(iPr_def_23),
inference(superposition,[status(thm)],[c_19468,c_22483]) ).
tcf(c_28755,plain,
( ( identity = iPr_def_24 )
| ( sk_c7 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_918,c_28750]) ).
tcf(c_28756,plain,
( ( identity = iPr_def_24 )
| ( sk_c7 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_887,c_28750]) ).
tcf(c_28769,plain,
inverse(iPr_def_23) = sk_c1,
inference(demodulation,[status(thm)],[c_28754,c_22483]) ).
tcf(c_28885,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( identity = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_28756,c_28755]) ).
tcf(c_29075,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( inverse(iPr_def_24) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_28885,c_22509]) ).
tcf(c_29077,plain,
! [X0: $i] :
( ( iPr_def_19 = iPr_def_21 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_28885,c_83]) ).
tcf(c_29094,plain,
multiply(sk_c2,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_19469,c_84]) ).
tcf(c_29097,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_17,X0)) = X0,
inference(superposition,[status(thm)],[c_19469,c_19302]) ).
tcf(c_29098,plain,
multiply(sk_c2,identity) = inverse(iPr_def_17),
inference(superposition,[status(thm)],[c_19469,c_22483]) ).
tcf(c_29104,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( identity = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_1486,c_29094]) ).
tcf(c_29133,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_14) = identity ) ),
inference(superposition,[status(thm)],[c_27269,c_29094]) ).
tcf(c_29139,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( identity = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_29133,c_27255]) ).
tcf(c_29177,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( iPr_def_19 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_29104,c_28885]) ).
tcf(c_29211,plain,
inverse(iPr_def_17) = sk_c2,
inference(demodulation,[status(thm)],[c_29098,c_22483]) ).
tcf(c_29262,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_22) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_29139,c_22509]) ).
tcf(c_29292,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( iPr_def_14 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_29177,c_2485]) ).
tcf(c_29532,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 = iPr_def_16 )
| ( iPr_def_15 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_27263,c_27471]) ).
tcf(c_29533,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 = iPr_def_20 )
| ( iPr_def_15 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_27259,c_27471]) ).
tcf(c_29535,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c7 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_9693,c_27471]) ).
tcf(c_29537,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c6 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_441,c_27471]) ).
tcf(c_29595,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 != iPr_def_22 ) ),
inference(global_subsumption_just,[status(thm)],[c_29537,c_27471,c_29537]) ).
tcf(c_29608,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_19 = iPr_def_21 )
| ( iPr_def_14 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_29292,c_29595]) ).
tcf(c_29642,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( multiply(iPr_def_16,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_27971,c_27148]) ).
tcf(c_29650,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( iPr_def_14 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_29642,c_27223]) ).
tcf(c_29726,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( sk_c7 = iPr_def_23 ) ),
inference(global_subsumption_just,[status(thm)],[c_29535,c_2210,c_4628,c_4689,c_29535]) ).
tcf(c_29768,plain,
( ( iPr_def_14 = iPr_def_17 )
| ~ iPr_def_10
| ( sk_c7 != identity )
| ( inverse(sk_c3) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_27875,c_28644]) ).
tcf(c_29788,plain,
( ( iPr_def_14 = iPr_def_17 )
| ~ iPr_def_10
| ( iPr_def_14 != iPr_def_20 )
| ( sk_c7 != identity ) ),
inference(light_normalisation,[status(thm)],[c_29768,c_420]) ).
tcf(c_30187,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( inverse(iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2485,c_29075]) ).
tcf(c_31049,plain,
sk_c8 = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_6133,c_117,c_466,c_414,c_945,c_983,c_984,c_1806,c_3686,c_3783,c_3784,c_5945,c_7085,c_7211,c_8131,c_10911,c_11185,c_12116,c_13239,c_18059,c_26798]) ).
tcf(c_31115,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c6 != iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_425,c_31049]) ).
tcf(c_31140,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( sk_c6 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_435,c_31049]) ).
tcf(c_31276,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c6 != iPr_def_15 ) ),
inference(equality_resolution_simp,[status(thm)],[c_31115]) ).
tcf(c_31606,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_31140,c_31276]) ).
tcf(c_31659,plain,
( iPr_def_13
| ( iPr_def_14 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_31606,c_2681,c_3777,c_10186,c_18059,c_21078,c_22078,c_27264,c_27266,c_27265,c_27267,c_27151,c_27471,c_27884,c_28184,c_28233,c_29650,c_29788]) ).
tcf(c_32576,plain,
( ( iPr_def_19 = iPr_def_21 )
| ~ iPr_def_11
| ( iPr_def_14 != iPr_def_15 )
| ( sk_c7 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_30187,c_28213]) ).
tcf(c_33089,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( identity = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_27204,c_28750]) ).
tcf(c_33101,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_33089,c_29139]) ).
tcf(c_33182,plain,
( ( iPr_def_17 = iPr_def_22 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_33101,c_27241]) ).
tcf(c_33184,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_33101,c_27254]) ).
tcf(c_33228,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_17) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_33182,c_29262]) ).
tcf(c_33246,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c2 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_33228,c_29211]) ).
tcf(c_33336,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( sk_c7 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_432,c_31049]) ).
tcf(c_33343,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( iPr_def_14 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_433,c_31049]) ).
tcf(c_33392,negated_conjecture,
iPr_def_14 = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_455,c_117,c_466,c_414,c_902,c_903,c_945,c_983,c_984,c_1806,c_3686,c_3783,c_3784,c_5945,c_7085,c_7211,c_8131,c_10911,c_11185,c_12116,c_13239,c_18059,c_26798]) ).
tcf(c_33455,plain,
multiply(iPr_def_20,sk_c3) = identity,
inference(superposition,[status(thm)],[c_420,c_84]) ).
tcf(c_33458,plain,
multiply(iPr_def_17,sk_c2) = identity,
inference(superposition,[status(thm)],[c_417,c_84]) ).
tcf(c_33463,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( multiply(iPr_def_19,sk_c6) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_33336,c_414]) ).
tcf(c_33730,plain,
multiply(sk_c3,iPr_def_14) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_421,c_33392]) ).
tcf(c_33899,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_428,c_33392]) ).
tcf(c_33909,plain,
( ~ iPr_def_11
| ( iPr_def_14 != iPr_def_24 )
| ( inverse(sk_c1) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_424,c_33899]) ).
tcf(c_33917,plain,
! [X0: $i] :
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,iPr_def_23) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_444,c_33899]) ).
tcf(c_33927,plain,
( ~ iPr_def_11
| ( iPr_def_14 != iPr_def_24 )
| ( sk_c7 != iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_33909,c_423]) ).
tcf(c_33974,plain,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != iPr_def_14 )
| ( multiply(X0,iPr_def_14) != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_429,c_33392]) ).
tcf(c_33987,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_21 )
| ( inverse(sk_c3) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_33730,c_33974]) ).
tcf(c_33993,plain,
( ~ iPr_def_10
| ( iPr_def_14 != iPr_def_20 )
| ( sk_c7 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_33987,c_420]) ).
tcf(c_34007,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != iPr_def_14 )
| ( multiply(iPr_def_14,multiply(X0,iPr_def_14)) != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_426,c_33392]) ).
tcf(c_34058,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_17 )
| ( multiply(iPr_def_19,multiply(sk_c6,X0)) = multiply(iPr_def_14,X0) ) ),
inference(superposition,[status(thm)],[c_33463,c_85]) ).
tcf(c_34114,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_33455,c_85]) ).
tcf(c_34115,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_34114,c_83]) ).
tcf(c_34322,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_33458,c_85]) ).
tcf(c_34323,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_34322,c_83]) ).
tcf(c_34330,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_17 )
| ( multiply(iPr_def_14,multiply(sk_c3,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_33343,c_34115]) ).
tcf(c_35000,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_33917,c_4640,c_27252,c_33927]) ).
tcf(c_35770,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_17 )
| ( sk_c7 = iPr_def_23 )
| ( multiply(iPr_def_19,multiply(iPr_def_15,X0)) = multiply(iPr_def_14,X0) ) ),
inference(superposition,[status(thm)],[c_447,c_34058]) ).
tcf(c_35820,plain,
( ( iPr_def_14 = iPr_def_17 )
| ~ iPr_def_13
| ( sk_c7 != iPr_def_14 )
| ( inverse(sk_c3) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_34330,c_34007]) ).
tcf(c_35835,plain,
( ( iPr_def_14 = iPr_def_17 )
| ~ iPr_def_13
| ( iPr_def_14 != iPr_def_20 )
| ( sk_c7 != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_35820,c_420]) ).
tcf(c_35845,plain,
iPr_def_14 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_35770,c_3778,c_27266,c_27267,c_29650,c_31659,c_35835]) ).
tcf(c_35859,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c2,X0)) = X0,
inference(demodulation,[status(thm)],[c_34323,c_35845]) ).
tcf(c_35868,plain,
inverse(sk_c2) = iPr_def_14,
inference(demodulation,[status(thm)],[c_417,c_35845]) ).
tcf(c_35921,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_14 )
| ( inverse(sk_c2) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_35859,c_34007]) ).
tcf(c_35922,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_14 ) ),
inference(ground_joinability,[status(thm)],[c_35921,c_35868]) ).
tcf(c_36654,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( identity = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_27205,c_28750]) ).
tcf(c_36692,plain,
iPr_def_14 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_27207,c_35845]) ).
tcf(c_36716,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_14,X0)) = X0,
inference(demodulation,[status(thm)],[c_29097,c_36692]) ).
tcf(c_36717,plain,
inverse(iPr_def_14) = sk_c2,
inference(demodulation,[status(thm)],[c_29211,c_36692]) ).
tcf(c_36718,plain,
multiply(sk_c2,iPr_def_14) = identity,
inference(demodulation,[status(thm)],[c_29094,c_36692]) ).
tcf(c_36746,plain,
multiply(iPr_def_14,sk_c2) = identity,
inference(demodulation,[status(thm)],[c_909,c_36692]) ).
tcf(c_36747,plain,
inverse(sk_c2) = iPr_def_14,
inference(demodulation,[status(thm)],[c_417,c_36692]) ).
tcf(c_36748,plain,
identity = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_36718,c_27255]) ).
tcf(c_36763,plain,
! [X0: $i] : multiply(iPr_def_22,X0) = X0,
inference(demodulation,[status(thm)],[c_27130,c_36716]) ).
tcf(c_36767,plain,
( ~ iPr_def_10
| ( sk_c7 != identity )
| ( inverse(sk_c2) != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_28644,c_36717]) ).
tcf(c_36768,plain,
( ~ iPr_def_12
| ( sk_c6 != identity )
| ( inverse(sk_c2) != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_28485,c_36717]) ).
tcf(c_36775,plain,
( ~ iPr_def_12
| ( sk_c6 != identity ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_36768,c_36747]) ).
tcf(c_36778,plain,
( ~ iPr_def_10
| ( sk_c7 != identity ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_36767,c_36747]) ).
tcf(c_36781,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_36654,c_36748]) ).
tcf(c_36786,plain,
multiply(sk_c1,iPr_def_23) = iPr_def_22,
inference(demodulation,[status(thm)],[c_28750,c_36748]) ).
tcf(c_36787,plain,
multiply(sk_c4,iPr_def_16) = iPr_def_22,
inference(demodulation,[status(thm)],[c_28624,c_36748]) ).
tcf(c_36791,plain,
( ~ iPr_def_12
| ( iPr_def_14 != iPr_def_22 )
| ( sk_c6 != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_28174,c_36748]) ).
tcf(c_36792,plain,
multiply(sk_c3,iPr_def_20) = iPr_def_22,
inference(demodulation,[status(thm)],[c_26775,c_36748]) ).
tcf(c_36793,plain,
inverse(iPr_def_22) = iPr_def_22,
inference(demodulation,[status(thm)],[c_22509,c_36748]) ).
tcf(c_36794,plain,
! [X0: $i] : multiply(X0,iPr_def_22) = X0,
inference(demodulation,[status(thm)],[c_22483,c_36748]) ).
tcf(c_36797,plain,
multiply(iPr_def_20,sk_c3) = iPr_def_22,
inference(demodulation,[status(thm)],[c_906,c_36748]) ).
tcf(c_36801,plain,
( ( sk_c7 = iPr_def_21 )
| ( sk_c7 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_788,c_36794]) ).
tcf(c_36802,plain,
( ( sk_c7 = iPr_def_19 )
| ( sk_c7 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_764,c_36794]) ).
tcf(c_36806,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_27152,c_36794]) ).
tcf(c_36807,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_14 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_27147,c_36794]) ).
tcf(c_36809,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( sk_c7 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_3869,c_36794]) ).
tcf(c_36858,plain,
multiply(iPr_def_14,sk_c2) = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_36746,c_36748]) ).
tcf(c_36861,plain,
multiply(sk_c3,iPr_def_22) = multiply(iPr_def_21,sk_c2),
inference(superposition,[status(thm)],[c_36858,c_27134]) ).
tcf(c_36971,plain,
multiply(inverse(iPr_def_20),iPr_def_22) = sk_c3,
inference(superposition,[status(thm)],[c_36797,c_19302]) ).
tcf(c_36974,plain,
multiply(iPr_def_21,sk_c2) = sk_c3,
inference(light_normalisation,[status(thm)],[c_36971,c_27781,c_36861]) ).
tcf(c_37092,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( multiply(sk_c3,iPr_def_22) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_36781,c_27187]) ).
tcf(c_37100,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( iPr_def_14 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_36781,c_27251]) ).
tcf(c_37123,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( sk_c3 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_37092,c_36861,c_36974]) ).
tcf(c_37268,plain,
( ~ iPr_def_12
| ( sk_c6 != iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_36775,c_36748]) ).
tcf(c_37279,plain,
( ( iPr_def_14 = iPr_def_20 )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_27259,c_37268]) ).
tcf(c_37283,plain,
( ( sk_c6 = iPr_def_15 )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_441,c_37268]) ).
tcf(c_37383,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_36778,c_36748]) ).
tcf(c_37393,plain,
( ( iPr_def_14 = iPr_def_20 )
| ~ iPr_def_10
| ( iPr_def_22 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_27257,c_37383]) ).
tcf(c_37394,plain,
( ( iPr_def_14 = iPr_def_24 )
| ~ iPr_def_10
| ( iPr_def_19 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_27252,c_37383]) ).
tcf(c_37398,plain,
( ( sk_c7 = iPr_def_21 )
| ~ iPr_def_10
| ( iPr_def_22 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_446,c_37383]) ).
tcf(c_37430,plain,
( ( iPr_def_22 != iPr_def_23 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_37398,c_33993,c_37398,c_37393]) ).
tcf(c_37431,plain,
( ~ iPr_def_10
| ( iPr_def_22 != iPr_def_23 ) ),
inference(renaming,[status(thm)],[c_37430]) ).
tcf(c_37603,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( sk_c7 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_27217,c_36794]) ).
tcf(c_37620,plain,
( ( iPr_def_14 = iPr_def_20 )
| ~ iPr_def_10
| ( iPr_def_14 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_37603,c_37383]) ).
tcf(c_37676,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c2 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_33246,c_36692]) ).
tcf(c_37993,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( sk_c7 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_36802,c_36801]) ).
tcf(c_38168,plain,
( ( iPr_def_14 = iPr_def_16 )
| ~ iPr_def_10
| ( iPr_def_14 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_36806,c_37431]) ).
tcf(c_38178,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_14) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_36806,c_28769]) ).
tcf(c_38185,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c1 = sk_c2 ) ),
inference(light_normalisation,[status(thm)],[c_38178,c_36717]) ).
tcf(c_38340,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( inverse(iPr_def_14) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_36807,c_28769]) ).
tcf(c_38347,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( sk_c1 = sk_c2 ) ),
inference(light_normalisation,[status(thm)],[c_38340,c_36717]) ).
tcf(c_38736,plain,
( ( iPr_def_14 = iPr_def_23 )
| ~ iPr_def_10
| ( iPr_def_19 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_36809,c_37383]) ).
tcf(c_38991,plain,
( ~ iPr_def_13
| ( multiply(sk_c8,identity) != sk_c7 ) ),
inference(ground_joinability,[status(thm)],[c_2327,c_27048,c_36747,c_36717]) ).
tcf(c_38992,plain,
( ~ iPr_def_13
| ( multiply(iPr_def_14,iPr_def_22) != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_38991,c_27048,c_36748]) ).
tcf(c_38993,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_38992,c_36794]) ).
tcf(c_39002,plain,
( ( sk_c7 = iPr_def_14 )
| ~ iPr_def_13
| ( iPr_def_14 != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_36802,c_38993]) ).
tcf(c_39004,plain,
( ( iPr_def_14 = iPr_def_20 )
| ~ iPr_def_13 ),
inference(superposition,[status(thm)],[c_37603,c_38993]) ).
tcf(c_39009,plain,
( ( iPr_def_14 = iPr_def_24 )
| ~ iPr_def_13
| ( iPr_def_14 != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_27252,c_38993]) ).
tcf(c_39178,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c7 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_27231,c_36794]) ).
tcf(c_39199,plain,
( ( iPr_def_14 = iPr_def_16 )
| ~ iPr_def_13 ),
inference(superposition,[status(thm)],[c_39178,c_38993]) ).
tcf(c_39374,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( inverse(iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_37100,c_36793]) ).
tcf(c_39376,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( sk_c2 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_39374,c_36717]) ).
tcf(c_39602,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( inverse(iPr_def_21) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_37123,c_420]) ).
tcf(c_39722,plain,
( ( iPr_def_19 = iPr_def_21 )
| ~ iPr_def_13 ),
inference(superposition,[status(thm)],[c_37993,c_38993]) ).
tcf(c_39728,plain,
( ( iPr_def_19 = iPr_def_21 )
| ~ iPr_def_10
| ( iPr_def_14 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_37993,c_37383]) ).
tcf(c_39741,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( multiply(inverse(iPr_def_14),iPr_def_14) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_37993,c_19307]) ).
tcf(c_39763,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( sk_c6 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_39741,c_27255,c_36717]) ).
tcf(c_39877,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( sk_c5 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_29077,c_1651]) ).
tcf(c_39880,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( sk_c7 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_29077,c_1653]) ).
tcf(c_40024,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c1 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_38185,c_37676]) ).
tcf(c_40289,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( sk_c1 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_39376,c_38347]) ).
tcf(c_40667,plain,
( ( iPr_def_19 = iPr_def_21 )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_39763,c_37268]) ).
tcf(c_41111,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( iPr_def_18 = iPr_def_19 )
| ( sk_c7 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_39877,c_443]) ).
tcf(c_41158,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_39880,c_37993]) ).
tcf(c_41274,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_14,sk_c7) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_40024,c_424]) ).
tcf(c_41279,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_41274,c_27262]) ).
tcf(c_41298,plain,
iPr_def_19 = iPr_def_21,
inference(global_subsumption_just,[status(thm)],[c_41111,c_29292,c_29608,c_32576,c_37993,c_39722,c_39728,c_40667,c_41158]) ).
tcf(c_41309,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( inverse(iPr_def_19) = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_39602,c_41298]) ).
tcf(c_41332,plain,
multiply(sk_c3,iPr_def_14) = iPr_def_19,
inference(demodulation,[status(thm)],[c_27256,c_41298]) ).
tcf(c_41374,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_19 )
| ( inverse(sk_c3) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_41332,c_27236]) ).
tcf(c_41377,plain,
( ~ iPr_def_10
| ( iPr_def_14 != iPr_def_20 )
| ( sk_c7 != iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_41374,c_420]) ).
tcf(c_41401,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_41279,c_33101]) ).
tcf(c_41483,plain,
( ( iPr_def_14 = iPr_def_20 )
| ( multiply(iPr_def_14,sk_c7) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_40289,c_424]) ).
tcf(c_41488,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_41483,c_27262]) ).
tcf(c_41623,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( iPr_def_14 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_41488,c_36781]) ).
tcf(c_41694,plain,
iPr_def_14 = iPr_def_20,
inference(global_subsumption_just,[status(thm)],[c_41309,c_27257,c_27251,c_29533,c_33927,c_37100,c_37279,c_37620,c_39004,c_41623]) ).
tcf(c_41710,plain,
multiply(sk_c3,iPr_def_14) = iPr_def_22,
inference(demodulation,[status(thm)],[c_36792,c_41694]) ).
tcf(c_41724,plain,
iPr_def_19 = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_41710,c_41332]) ).
tcf(c_41751,plain,
! [X0: $i] : multiply(X0,iPr_def_19) = X0,
inference(demodulation,[status(thm)],[c_36794,c_41724]) ).
tcf(c_41752,plain,
! [X0: $i] : multiply(iPr_def_19,X0) = X0,
inference(demodulation,[status(thm)],[c_36763,c_41724]) ).
tcf(c_41754,plain,
multiply(sk_c4,iPr_def_16) = iPr_def_19,
inference(demodulation,[status(thm)],[c_36787,c_41724]) ).
tcf(c_41755,plain,
multiply(sk_c1,iPr_def_23) = iPr_def_19,
inference(demodulation,[status(thm)],[c_36786,c_41724]) ).
tcf(c_41757,plain,
inverse(iPr_def_19) = iPr_def_19,
inference(demodulation,[status(thm)],[c_36793,c_41724]) ).
tcf(c_41758,plain,
identity = iPr_def_19,
inference(demodulation,[status(thm)],[c_36748,c_41724]) ).
tcf(c_41762,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 != iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_29595,c_41724]) ).
tcf(c_41765,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c6 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_27263,c_41724]) ).
tcf(c_41767,plain,
( ( sk_c6 = iPr_def_19 )
| ( sk_c7 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_438,c_41724]) ).
tcf(c_41788,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( sk_c6 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_27189,c_41752]) ).
tcf(c_41984,plain,
( ( identity != iPr_def_14 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_28293,c_27257,c_27251,c_28294,c_29533,c_33927,c_37100,c_37279,c_37620,c_38736,c_39004,c_41377,c_41623,c_41724]) ).
tcf(c_41985,plain,
( ~ iPr_def_10
| ( identity != iPr_def_14 ) ),
inference(renaming,[status(thm)],[c_41984]) ).
tcf(c_42075,plain,
( ~ iPr_def_11
| ( sk_c7 != iPr_def_14 )
| ( inverse(iPr_def_19) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_41752,c_27237]) ).
tcf(c_42078,plain,
( ~ iPr_def_12
| ( sk_c6 != iPr_def_14 )
| ( inverse(iPr_def_19) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_41752,c_27238]) ).
tcf(c_42082,plain,
( ~ iPr_def_12
| ( iPr_def_14 != iPr_def_19 )
| ( sk_c6 != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_42078,c_41757]) ).
tcf(c_42086,plain,
( ~ iPr_def_11
| ( sk_c7 != iPr_def_19 )
| ( sk_c7 != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_42075,c_41757]) ).
tcf(c_42296,plain,
iPr_def_14 = iPr_def_16,
inference(global_subsumption_just,[status(thm)],[c_41765,c_27070,c_27258,c_27254,c_29532,c_33184,c_33927,c_38168,c_39199,c_41401]) ).
tcf(c_42299,plain,
multiply(sk_c4,iPr_def_14) = iPr_def_19,
inference(demodulation,[status(thm)],[c_41754,c_42296]) ).
tcf(c_42311,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_14,X0)) = X0,
inference(demodulation,[status(thm)],[c_28627,c_42296]) ).
tcf(c_42315,plain,
multiply(iPr_def_14,iPr_def_18) = iPr_def_14,
inference(demodulation,[status(thm)],[c_27223,c_42296]) ).
tcf(c_42320,plain,
iPr_def_18 = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_42299,c_27261]) ).
tcf(c_42321,plain,
! [X0: $i] : multiply(iPr_def_18,X0) = X0,
inference(demodulation,[status(thm)],[c_27132,c_42311]) ).
tcf(c_42324,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c7 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_27214,c_42315]) ).
tcf(c_42325,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_27192,c_42315]) ).
tcf(c_42336,plain,
multiply(sk_c1,iPr_def_23) = iPr_def_18,
inference(demodulation,[status(thm)],[c_41755,c_42320]) ).
tcf(c_42338,plain,
! [X0: $i] : multiply(X0,iPr_def_18) = X0,
inference(demodulation,[status(thm)],[c_41751,c_42320]) ).
tcf(c_42339,plain,
inverse(iPr_def_18) = iPr_def_18,
inference(demodulation,[status(thm)],[c_41757,c_42320]) ).
tcf(c_42344,plain,
( ( sk_c6 = iPr_def_18 )
| ( sk_c7 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_41767,c_42320]) ).
tcf(c_42346,plain,
identity = iPr_def_18,
inference(demodulation,[status(thm)],[c_41758,c_42320]) ).
tcf(c_42347,plain,
iPr_def_18 = iPr_def_22,
inference(demodulation,[status(thm)],[c_41724,c_42320]) ).
tcf(c_42432,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_13892,c_3778,c_33927,c_35000,c_42086,c_42325,c_42324]) ).
tcf(c_42435,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c7 = iPr_def_23 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_29726,c_42432]) ).
tcf(c_42668,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( sk_c7 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_42324,c_42320]) ).
tcf(c_42712,plain,
iPr_def_14 = iPr_def_24,
inference(global_subsumption_just,[status(thm)],[c_42325,c_27249,c_27471,c_37394,c_39009,c_41724,c_41788,c_42082,c_42325,c_42432]) ).
tcf(c_42719,plain,
multiply(sk_c1,iPr_def_14) = multiply(iPr_def_14,sk_c6),
inference(demodulation,[status(thm)],[c_10699,c_42712]) ).
tcf(c_42722,plain,
multiply(sk_c1,sk_c7) = iPr_def_14,
inference(demodulation,[status(thm)],[c_424,c_42712]) ).
tcf(c_42725,plain,
( ( sk_c7 = iPr_def_23 )
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_42435,c_3778,c_4640,c_29726,c_33927,c_35000,c_35922,c_42086,c_42325,c_42324]) ).
tcf(c_42726,plain,
( iPr_def_12
| ( sk_c7 = iPr_def_23 ) ),
inference(renaming,[status(thm)],[c_42725]) ).
tcf(c_42770,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_42668,c_42722]) ).
tcf(c_42779,plain,
iPr_def_14 = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_42770,c_42336]) ).
tcf(c_42782,plain,
! [X0: $i] : multiply(X0,iPr_def_14) = X0,
inference(demodulation,[status(thm)],[c_42338,c_42779]) ).
tcf(c_42788,plain,
! [X0: $i] : multiply(iPr_def_14,X0) = X0,
inference(demodulation,[status(thm)],[c_42321,c_42779]) ).
tcf(c_42789,plain,
inverse(iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_42339,c_42779]) ).
tcf(c_42793,plain,
iPr_def_14 = iPr_def_22,
inference(demodulation,[status(thm)],[c_42347,c_42779]) ).
tcf(c_42794,plain,
identity = iPr_def_14,
inference(demodulation,[status(thm)],[c_42346,c_42779]) ).
tcf(c_42795,plain,
iPr_def_14 = iPr_def_19,
inference(demodulation,[status(thm)],[c_42320,c_42779]) ).
tcf(c_42812,plain,
sk_c7 = iPr_def_15,
inference(demodulation,[status(thm)],[c_27262,c_42788]) ).
tcf(c_42827,plain,
( iPr_def_12
| ( iPr_def_15 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_42726,c_42812]) ).
tcf(c_42835,plain,
( ( iPr_def_15 = iPr_def_23 )
| ( sk_c6 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_447,c_42812]) ).
tcf(c_42874,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c6 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_42344,c_42779,c_42812]) ).
tcf(c_42885,plain,
( ( iPr_def_15 = iPr_def_23 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_42874,c_42835]) ).
tcf(c_42919,plain,
sk_c6 = sk_c1,
inference(demodulation,[status(thm)],[c_42719,c_42782,c_42788]) ).
tcf(c_42923,plain,
inverse(sk_c6) = iPr_def_23,
inference(demodulation,[status(thm)],[c_423,c_42919]) ).
tcf(c_42943,plain,
( ( iPr_def_15 != iPr_def_19 )
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_41762,c_3778,c_33927,c_35000,c_35922,c_39002,c_41762,c_41985,c_42086,c_42325,c_42324,c_42795,c_42794]) ).
tcf(c_42944,plain,
( iPr_def_12
| ( iPr_def_15 != iPr_def_19 ) ),
inference(renaming,[status(thm)],[c_42943]) ).
tcf(c_42945,plain,
( iPr_def_12
| ( iPr_def_14 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_42944,c_42795]) ).
tcf(c_42959,plain,
iPr_def_15 = iPr_def_23,
inference(global_subsumption_just,[status(thm)],[c_42827,c_12120,c_36791,c_42793,c_42827,c_42835,c_42885]) ).
tcf(c_42988,plain,
inverse(sk_c6) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_42923,c_42959]) ).
tcf(c_42990,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( inverse(iPr_def_14) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_42874,c_42988]) ).
tcf(c_42992,plain,
iPr_def_14 = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_42990,c_42789]) ).
tcf(c_42994,plain,
iPr_def_12,
inference(backward_subsumption_resolution,[status(thm)],[c_42945,c_42992]) ).
tcf(c_43000,plain,
( ( sk_c6 = iPr_def_14 )
| ~ iPr_def_12 ),
inference(demodulation,[status(thm)],[c_37283,c_42992]) ).
tcf(c_43001,plain,
sk_c6 = iPr_def_14,
inference(forward_subsumption_resolution,[status(thm)],[c_43000,c_42994]) ).
tcf(c_43004,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_43001,c_42994,c_42793,c_36791]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP356-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 : n015.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.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Wed Sep 23 14:36:54 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.41
% 0.11/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.41
% 0.11/0.41 % Detected problem language: tptp
% 0.11/0.42 % Proving...
% 10.69/2.72 % SZS status Started for theBenchmark.p
% 10.69/2.72 % SZS status Unsatisfiable for theBenchmark.p
% 10.69/2.72
% 10.69/2.72 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.69/2.72
% 10.69/2.72 % ------ iProver source info
% 10.69/2.72
% 10.69/2.72 % git: date: 2026-07-19 20:42:38 +0200
% 10.69/2.72 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.69/2.72 % git: non_committed_changes: false
% 10.69/2.72
% 10.69/2.72 % ------ Parsing...% successful
% 10.69/2.72
% 10.69/2.72
% 10.69/2.72 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 10.69/2.72
% 10.69/2.72 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 10.69/2.72
% 10.69/2.72 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 10.69/2.72
% 10.69/2.72 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 10.69/2.72 % ------ Proving...
% 10.69/2.72 % ------ Problem Properties
% 10.69/2.72
% 10.69/2.72 %
% 10.69/2.72 % clauses 49
% 10.69/2.72 % conjectures 35
% 10.69/2.72 % EPR 31
% 10.69/2.72 % Horn 18
% 10.69/2.72 % unary 14
% 10.69/2.72 % binary 30
% 10.69/2.72 % lits 92
% 10.69/2.72 % lits eq 84
% 10.69/2.72 % fd_pure 0
% 10.69/2.72 % fd_pseudo 0
% 10.69/2.72 % fd_cond 0
% 10.69/2.72 % fd_pseudo_cond 0
% 10.69/2.72 % AC symbols 0
% 10.69/2.72
% 10.69/2.72 % ------ Schedule dynamic 5 is on
% 10.69/2.72
% 10.69/2.72 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 10.69/2.72
% 10.69/2.72
% 10.69/2.72 % ------
% 10.69/2.72 % Current options:
% 10.69/2.72 % ------
% 10.69/2.72
% 10.69/2.72
% 10.69/2.72 %
% 10.69/2.72
% 10.69/2.72 % ------ Proving...
% 10.69/2.72 %
% 10.69/2.72
% 10.69/2.72 % SZS status Unsatisfiable for theBenchmark.p
% 10.69/2.72
% 10.69/2.72 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.69/2.74
% 10.69/2.74
%------------------------------------------------------------------------------