%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP260-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:32:37 PM UTC 2026
% Result : Unsatisfiable 41.45s 8.39s
% Output : CNFRefutation 41.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 60
% Syntax : Number of formulae : 450 ( 136 unt; 15 def)
% Number of atoms : 1542 ( 881 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 778 ( 291 ~; 487 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 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 : 20 ( 18 usr; 19 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 155 ( 0 sgn 155 !; 0 ?; 120 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c3)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c10 = inverse(sk_c4)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f10]) ).
fof(f16,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f17,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f16]) ).
fof(f18,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,negated_conjecture,
( inverse(sk_c6) = sk_c8
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f20,plain,
( sk_c8 = inverse(sk_c6)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f22,plain,
( sk_c6 = multiply(sk_c7,sk_c8)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f24,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f29,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f32,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f34,plain,
( sk_c8 = inverse(sk_c5)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f33]) ).
fof(f37,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f38,plain,
( inverse(sk_c7) = sk_c6
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f37]) ).
fof(f41,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f42,plain,
( sk_c6 = multiply(sk_c7,sk_c8)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c11 = inverse(sk_c3)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f48,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c10 = inverse(sk_c4)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f52,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f54,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f53]) ).
fof(f57,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f58,plain,
( inverse(sk_c7) = sk_c6
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f57]) ).
fof(f61,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_30) ).
fof(f62,plain,
( sk_c6 = multiply(sk_c7,sk_c8)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f64,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f68,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f72,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f74,plain,
( sk_c8 = inverse(sk_c5)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f73]) ).
fof(f77,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_38) ).
fof(f78,plain,
( inverse(sk_c7) = sk_c6
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f77]) ).
fof(f81,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_40) ).
fof(f82,plain,
( sk_c6 = multiply(sk_c7,sk_c8)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f84,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f86,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f88,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f90,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f92,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f91]) ).
fof(f93,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f94,plain,
( sk_c8 = inverse(sk_c5)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f93]) ).
fof(f97,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f98,plain,
( inverse(sk_c7) = sk_c6
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f97]) ).
fof(f101,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c6
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_50) ).
fof(f102,plain,
( sk_c6 = multiply(sk_c7,sk_c8)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f101]) ).
fof(f103,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| multiply(X5,sk_c10) != sk_c11
| inverse(X4) != X5
| multiply(X4,X5) != sk_c11
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != sk_c9
| inverse(X2) != sk_c11
| multiply(X2,sk_c11) != sk_c10
| multiply(sk_c9,sk_c11) != sk_c10
| inverse(X1) != sk_c10
| multiply(X1,sk_c10) != sk_c9
| inverse(X0) != sk_c11
| multiply(X0,sk_c11) != sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_51) ).
fof(f104,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c10 != multiply(sk_c9,sk_c11)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(reorient_equations,[],[f103]) ).
fof(f105,plain,
! [X2,X3,X0,X1,X6,X7,X4] :
( multiply(X6,inverse(X4)) != X7
| inverse(X4) != inverse(X7)
| inverse(X6) != X7
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c10 != multiply(sk_c9,sk_c11)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(equality_resolution,[],[f104]) ).
fof(f106,plain,
! [X2,X3,X0,X1,X6,X4] :
( inverse(X6) != multiply(X6,inverse(X4))
| inverse(X4) != inverse(inverse(X6))
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c10 != multiply(sk_c9,sk_c11)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(equality_resolution,[],[f105]) ).
tcf(c_103,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_104,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_106,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_108,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_112,negated_conjecture,
( ( multiply(sk_c8,sk_c10) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_115,negated_conjecture,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_120,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_128,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_135,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_140,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_143,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_145,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_146,negated_conjecture,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_148,negated_conjecture,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_150,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_153,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_155,negated_conjecture,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_156,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(X5) != sk_c10 )
| ( inverse(X4) != sk_c10 )
| ( inverse(X3) != sk_c11 )
| ( inverse(X2) != sk_c11 )
| ( multiply(sk_c9,sk_c11) != sk_c10 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(X5,sk_c10) != sk_c9 )
| ( multiply(X4,sk_c10) != sk_c9 )
| ( multiply(X3,sk_c11) != sk_c10 )
| ( multiply(X2,sk_c11) != sk_c10 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_621,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_156]) ).
tcf(c_622,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_156]) ).
tcf(c_623,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_156]) ).
tcf(c_624,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c9,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_156]) ).
tcf(c_625,definition,
iPr_def_13 = multiply(sk_c9,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_626,definition,
iPr_def_14 = multiply(sk_c7,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_627,definition,
iPr_def_15 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_628,definition,
iPr_def_16 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_629,definition,
iPr_def_17 = multiply(sk_c8,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_630,definition,
iPr_def_18 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_631,definition,
iPr_def_19 = multiply(sk_c5,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_632,definition,
iPr_def_20 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_633,definition,
iPr_def_21 = multiply(sk_c4,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_634,definition,
iPr_def_22 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_635,definition,
iPr_def_23 = multiply(sk_c3,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_636,definition,
iPr_def_24 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_637,definition,
iPr_def_25 = multiply(sk_c2,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_638,definition,
iPr_def_26 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_639,definition,
iPr_def_27 = multiply(sk_c1,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_640,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_13 != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_624,c_625]) ).
tcf(c_641,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_623]) ).
tcf(c_644,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_622]) ).
tcf(c_645,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_621]) ).
tcf(c_646,negated_conjecture,
( ( iPr_def_14 = sk_c6 )
| ( iPr_def_13 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_155,c_626]) ).
tcf(c_648,negated_conjecture,
( ( iPr_def_16 = sk_c6 )
| ( iPr_def_13 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_153,c_628]) ).
tcf(c_650,negated_conjecture,
( ( iPr_def_18 = sk_c8 )
| ( iPr_def_13 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_151,c_630]) ).
tcf(c_651,negated_conjecture,
( ( iPr_def_19 = sk_c11 )
| ( iPr_def_13 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_150,c_631]) ).
tcf(c_652,negated_conjecture,
( ( iPr_def_20 = sk_c10 )
| ( iPr_def_13 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_149,c_632]) ).
tcf(c_653,negated_conjecture,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_13 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_148,c_633]) ).
tcf(c_654,negated_conjecture,
( ( iPr_def_22 = sk_c11 )
| ( iPr_def_13 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_147,c_634]) ).
tcf(c_655,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_13 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_146,c_635]) ).
tcf(c_656,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_14 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_145,c_636]) ).
tcf(c_658,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_16 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_143]) ).
tcf(c_660,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_661,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_140]) ).
tcf(c_662,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_20 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_139]) ).
tcf(c_664,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_665,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_666,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_14 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_135,c_637]) ).
tcf(c_668,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_16 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_133]) ).
tcf(c_670,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_671,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_672,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_20 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_673,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_21 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_128]) ).
tcf(c_674,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_675,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_676,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_14 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_125,c_638]) ).
tcf(c_678,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_16 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_680,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_681,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_682,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_20 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_684,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_685,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_686,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_14 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_115,c_639]) ).
tcf(c_687,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_15 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_688,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_16 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_689,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_692,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_20 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_693,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_21 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_694,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_695,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_696,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_697,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1006,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c10 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_646,c_648]) ).
tcf(c_1115,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c10 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_658,c_656]) ).
tcf(c_1179,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(sk_c5,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_660,c_631]) ).
tcf(c_1192,plain,
( ( sk_c10 = iPr_def_13 )
| ( multiply(sk_c4,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_652,c_633]) ).
tcf(c_1227,plain,
multiply(iPr_def_22,sk_c3) = identity,
inference(superposition,[status(thm)],[c_634,c_104]) ).
tcf(c_1228,plain,
multiply(iPr_def_20,sk_c4) = identity,
inference(superposition,[status(thm)],[c_632,c_104]) ).
tcf(c_1229,plain,
multiply(iPr_def_18,sk_c5) = identity,
inference(superposition,[status(thm)],[c_630,c_104]) ).
tcf(c_1230,plain,
multiply(iPr_def_16,sk_c7) = identity,
inference(superposition,[status(thm)],[c_628,c_104]) ).
tcf(c_1231,plain,
multiply(iPr_def_15,sk_c6) = identity,
inference(superposition,[status(thm)],[c_627,c_104]) ).
tcf(c_1232,plain,
multiply(iPr_def_26,sk_c1) = identity,
inference(superposition,[status(thm)],[c_638,c_104]) ).
tcf(c_1233,plain,
multiply(iPr_def_24,sk_c2) = identity,
inference(superposition,[status(thm)],[c_636,c_104]) ).
tcf(c_1258,plain,
! [X0: $i] :
( ( iPr_def_13 = sk_c10 )
| ( iPr_def_13 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1265,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_662,c_637]) ).
tcf(c_1270,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_20 )
| ( iPr_def_13 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_662,c_640]) ).
tcf(c_1288,plain,
( ( iPr_def_13 = sk_c10 )
| ( iPr_def_13 != iPr_def_13 )
| ( sk_c10 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1258]) ).
tcf(c_1289,plain,
iPr_def_13 = iPr_def_13,
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_1307,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( sk_c10 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_664,c_661]) ).
tcf(c_1324,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1326,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_1329,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1367,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1329]) ).
tcf(c_1403,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_20 )
| ( iPr_def_20 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1367]) ).
tcf(c_1407,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_24 )
| ( iPr_def_24 != inverse(sk_c2) )
| ( inverse(X0) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1367]) ).
tcf(c_1446,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c9 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_668,c_666]) ).
tcf(c_1479,plain,
( ( sk_c9 = iPr_def_25 )
| ( multiply(sk_c5,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_670,c_631]) ).
tcf(c_1500,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(iPr_def_25,sk_c11) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_671,c_625]) ).
tcf(c_1635,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != iPr_def_20 )
| ( inverse(X0) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_1324]) ).
tcf(c_1665,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c11 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_678,c_676]) ).
tcf(c_1727,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != iPr_def_24 )
| ( inverse(X0) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1324]) ).
tcf(c_1745,plain,
( ( sk_c11 = iPr_def_26 )
| ( multiply(sk_c5,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_680,c_631]) ).
tcf(c_1832,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_682,c_639]) ).
tcf(c_1936,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_684,c_639]) ).
tcf(c_1994,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_685,c_639]) ).
tcf(c_2119,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c10 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_688,c_686]) ).
tcf(c_2347,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_692,c_637]) ).
tcf(c_2459,plain,
( ( inverse(sk_c4) = iPr_def_20 )
| ( iPr_def_20 != inverse(sk_c4) )
| ( inverse(sk_c4) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1403]) ).
tcf(c_2460,plain,
inverse(sk_c4) = inverse(sk_c4),
inference(instantiation,[status(thm)],[c_1326]) ).
tcf(c_2486,plain,
( ( sk_c10 = iPr_def_27 )
| ( multiply(sk_c1,iPr_def_22) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_694,c_639]) ).
tcf(c_2542,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_695,c_637]) ).
tcf(c_2572,plain,
( ( inverse(sk_c2) = iPr_def_24 )
| ( iPr_def_24 != inverse(sk_c2) )
| ( inverse(sk_c2) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1407]) ).
tcf(c_2573,plain,
inverse(sk_c2) = inverse(sk_c2),
inference(instantiation,[status(thm)],[c_1326]) ).
tcf(c_2604,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_27 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_639,c_644]) ).
tcf(c_2605,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_23 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_635,c_644]) ).
tcf(c_2629,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_23 )
| ( sk_c11 != iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_2605,c_634]) ).
tcf(c_2633,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_27 )
| ( sk_c11 != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_2604,c_638]) ).
tcf(c_2869,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c11,X0)) = multiply(iPr_def_27,X0),
inference(superposition,[status(thm)],[c_639,c_105]) ).
tcf(c_2870,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c11,X0)) = multiply(iPr_def_23,X0),
inference(superposition,[status(thm)],[c_635,c_105]) ).
tcf(c_2873,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c10,X0)) = multiply(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_629,c_105]) ).
tcf(c_2874,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c8,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_626,c_105]) ).
tcf(c_2875,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c10,X0)) = multiply(iPr_def_25,X0),
inference(superposition,[status(thm)],[c_637,c_105]) ).
tcf(c_2876,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c11,X0)) = multiply(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_625,c_105]) ).
tcf(c_2878,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_104,c_105]) ).
tcf(c_2880,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1227,c_105]) ).
tcf(c_2881,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1228,c_105]) ).
tcf(c_2882,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1229,c_105]) ).
tcf(c_2883,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1230,c_105]) ).
tcf(c_2884,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1231,c_105]) ).
tcf(c_2885,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1232,c_105]) ).
tcf(c_2886,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1233,c_105]) ).
tcf(c_2889,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2886,c_103]) ).
tcf(c_2890,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2885,c_103]) ).
tcf(c_2891,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2884,c_103]) ).
tcf(c_2892,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2883,c_103]) ).
tcf(c_2893,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2882,c_103]) ).
tcf(c_2894,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2881,c_103]) ).
tcf(c_2895,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2880,c_103]) ).
tcf(c_3143,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( sk_c10 != iPr_def_20 )
| ( inverse(sk_c4) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_1635]) ).
tcf(c_3233,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( sk_c10 != iPr_def_24 )
| ( inverse(sk_c2) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1727]) ).
tcf(c_3299,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_21 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_633,c_645]) ).
tcf(c_3301,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_25 )
| ( inverse(sk_c2) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_637,c_645]) ).
tcf(c_3318,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_25 )
| ( sk_c10 != iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_3301,c_636]) ).
tcf(c_3325,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_21 )
| ( sk_c10 != iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_3299,c_632]) ).
tcf(c_3428,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_103,c_641]) ).
tcf(c_3713,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( iPr_def_13 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1115,c_1006]) ).
tcf(c_3716,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1115,c_637]) ).
tcf(c_3962,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1307,c_637]) ).
tcf(c_4081,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_25,sk_c11) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_1446,c_625]) ).
tcf(c_4123,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1665,c_639]) ).
tcf(c_4216,plain,
( ( iPr_def_24 = iPr_def_27 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_2119,c_1115]) ).
tcf(c_4223,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( iPr_def_13 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2119,c_1006]) ).
tcf(c_4226,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_2119,c_637]) ).
tcf(c_5030,plain,
multiply(iPr_def_24,iPr_def_25) = sk_c10,
inference(superposition,[status(thm)],[c_637,c_2889]) ).
tcf(c_5044,plain,
multiply(iPr_def_26,iPr_def_27) = sk_c11,
inference(superposition,[status(thm)],[c_639,c_2890]) ).
tcf(c_5056,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(iPr_def_27,X0)) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_5044,c_105]) ).
tcf(c_5131,plain,
multiply(iPr_def_16,iPr_def_14) = sk_c8,
inference(superposition,[status(thm)],[c_626,c_2892]) ).
tcf(c_5157,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(iPr_def_14,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_5131,c_105]) ).
tcf(c_5159,plain,
multiply(iPr_def_18,iPr_def_19) = sk_c8,
inference(superposition,[status(thm)],[c_631,c_2893]) ).
tcf(c_5492,plain,
multiply(iPr_def_20,iPr_def_21) = sk_c10,
inference(superposition,[status(thm)],[c_633,c_2894]) ).
tcf(c_5507,plain,
multiply(iPr_def_22,iPr_def_23) = sk_c11,
inference(superposition,[status(thm)],[c_635,c_2895]) ).
tcf(c_5522,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(iPr_def_23,X0)) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_5507,c_105]) ).
tcf(c_5652,plain,
( ~ iPr_def_10
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(sk_c4,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_645]) ).
tcf(c_5701,plain,
( ~ iPr_def_10
| ( inverse(sk_c2) != sk_c10 )
| ( multiply(sk_c2,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_645]) ).
tcf(c_6324,plain,
( ( sk_c10 = iPr_def_13 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_1192,c_2894]) ).
tcf(c_6325,plain,
( ( sk_c10 = iPr_def_20 )
| ( sk_c10 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_6324,c_5492]) ).
tcf(c_6554,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1265,c_2889]) ).
tcf(c_6555,plain,
( ( sk_c10 = iPr_def_24 )
| ( sk_c10 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_6554,c_5030]) ).
tcf(c_7492,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(iPr_def_25,iPr_def_26) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_681,c_1500]) ).
tcf(c_8635,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1832,c_2890]) ).
tcf(c_8636,plain,
( ( sk_c10 = iPr_def_20 )
| ( sk_c11 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_8635,c_5044]) ).
tcf(c_8729,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1936,c_2890]) ).
tcf(c_8730,plain,
( ( sk_c11 = iPr_def_26 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_8729,c_5044]) ).
tcf(c_8774,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1994,c_2890]) ).
tcf(c_8775,plain,
( ( sk_c10 = iPr_def_23 )
| ( sk_c11 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_8774,c_5044]) ).
tcf(c_9482,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2347,c_2889]) ).
tcf(c_9483,plain,
( ( sk_c10 = iPr_def_27 )
| ( sk_c10 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_9482,c_5030]) ).
tcf(c_9590,plain,
( ( sk_c10 = iPr_def_27 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_2486,c_2890]) ).
tcf(c_9591,plain,
( ( sk_c10 = iPr_def_27 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_9590,c_5044]) ).
tcf(c_9643,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2542,c_2889]) ).
tcf(c_9644,plain,
( ( sk_c10 = iPr_def_27 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_9643,c_5030]) ).
tcf(c_10952,plain,
( iPr_def_12
| ( sk_c10 = iPr_def_20 ) ),
inference(global_subsumption_just,[status(thm)],[c_1270,c_129,c_128,c_636,c_640,c_1288,c_1289,c_2572,c_2573,c_2633,c_3233,c_5652,c_5701,c_6325,c_6555,c_8636,c_9483]) ).
tcf(c_11973,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_25,iPr_def_26) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_1665,c_4081]) ).
tcf(c_13151,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_2878,c_103]) ).
tcf(c_13176,plain,
multiply(inverse(sk_c9),iPr_def_13) = sk_c11,
inference(superposition,[status(thm)],[c_625,c_13151]) ).
tcf(c_13177,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_103,c_13151]) ).
tcf(c_13178,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_104,c_13151]) ).
tcf(c_13179,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_105,c_13151]) ).
tcf(c_13368,plain,
! [X0: $i] : multiply(inverse(iPr_def_22),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_2895,c_13151]) ).
tcf(c_13369,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_2894,c_13151]) ).
tcf(c_13370,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_2893,c_13151]) ).
tcf(c_13372,plain,
! [X0: $i] : multiply(inverse(iPr_def_15),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_2891,c_13151]) ).
tcf(c_13373,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_2890,c_13151]) ).
tcf(c_13374,plain,
! [X0: $i] : multiply(inverse(iPr_def_24),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_2889,c_13151]) ).
tcf(c_13409,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_13151,c_13151]) ).
tcf(c_14320,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_13178,c_13409]) ).
tcf(c_14332,plain,
multiply(sk_c11,identity) = multiply(iPr_def_26,iPr_def_27),
inference(superposition,[status(thm)],[c_14320,c_5056]) ).
tcf(c_14333,plain,
multiply(sk_c9,sk_c11) = multiply(iPr_def_13,identity),
inference(superposition,[status(thm)],[c_14320,c_2876]) ).
tcf(c_14336,plain,
multiply(sk_c11,identity) = multiply(iPr_def_22,iPr_def_23),
inference(superposition,[status(thm)],[c_14320,c_5522]) ).
tcf(c_14338,plain,
multiply(sk_c2,sk_c10) = multiply(iPr_def_25,identity),
inference(superposition,[status(thm)],[c_14320,c_2875]) ).
tcf(c_14339,plain,
multiply(sk_c8,sk_c10) = multiply(iPr_def_17,identity),
inference(superposition,[status(thm)],[c_14320,c_2873]) ).
tcf(c_14353,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_14320,c_13177]) ).
tcf(c_14360,plain,
multiply(iPr_def_17,identity) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_14339,c_629]) ).
tcf(c_14361,plain,
multiply(iPr_def_25,identity) = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_14338,c_637]) ).
tcf(c_14363,plain,
multiply(sk_c11,identity) = sk_c11,
inference(light_normalisation,[status(thm)],[c_14336,c_5507]) ).
tcf(c_14366,plain,
multiply(iPr_def_13,identity) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_14333,c_625]) ).
tcf(c_14371,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_23 ) ),
inference(global_subsumption_just,[status(thm)],[c_2629,c_2633,c_2629,c_8730,c_9591]) ).
tcf(c_14373,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_14371,c_2633,c_8775,c_9644,c_14371]) ).
tcf(c_14381,plain,
( iPr_def_12
| iPr_def_10
| ( sk_c10 != iPr_def_13 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_640,c_14373]) ).
tcf(c_14404,plain,
multiply(identity,identity) = identity,
inference(superposition,[status(thm)],[c_14353,c_104]) ).
tcf(c_14432,plain,
( iPr_def_12
| ( sk_c10 != iPr_def_13 ) ),
inference(global_subsumption_just,[status(thm)],[c_14381,c_138,c_128,c_632,c_2459,c_2460,c_3143,c_5652,c_5701,c_10952,c_14381]) ).
tcf(c_14461,plain,
( iPr_def_12
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1006,c_14432]) ).
tcf(c_14790,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_25 ) ),
inference(global_subsumption_just,[status(thm)],[c_3318,c_139,c_138,c_129,c_128,c_5652,c_5701]) ).
tcf(c_14804,plain,
( ( sk_c10 = iPr_def_23 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_675,c_14790]) ).
tcf(c_14806,plain,
( ( sk_c9 = iPr_def_21 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_673,c_14790]) ).
tcf(c_14807,plain,
( ( sk_c10 = iPr_def_20 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_672,c_14790]) ).
tcf(c_14893,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_14804,c_3325,c_14807,c_14806]) ).
tcf(c_15611,plain,
multiply(sk_c3,iPr_def_22) = identity,
inference(superposition,[status(thm)],[c_13368,c_104]) ).
tcf(c_15613,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_22,X0)) = X0,
inference(superposition,[status(thm)],[c_13368,c_13151]) ).
tcf(c_15614,plain,
multiply(sk_c3,identity) = inverse(iPr_def_22),
inference(superposition,[status(thm)],[c_13368,c_14320]) ).
tcf(c_16405,plain,
inverse(iPr_def_22) = sk_c3,
inference(demodulation,[status(thm)],[c_15614,c_14320]) ).
tcf(c_16418,plain,
multiply(sk_c3,sk_c11) = iPr_def_23,
inference(superposition,[status(thm)],[c_5507,c_15613]) ).
tcf(c_17096,plain,
multiply(sk_c4,iPr_def_20) = identity,
inference(superposition,[status(thm)],[c_13369,c_104]) ).
tcf(c_17097,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(inverse(inverse(iPr_def_20))) != inverse(X0) )
| ( multiply(sk_c4,inverse(X0)) != inverse(inverse(iPr_def_20)) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_13369,c_641]) ).
tcf(c_17098,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_20,X0)) = X0,
inference(superposition,[status(thm)],[c_13369,c_13151]) ).
tcf(c_17099,plain,
multiply(sk_c4,identity) = inverse(iPr_def_20),
inference(superposition,[status(thm)],[c_13369,c_14320]) ).
tcf(c_17488,plain,
inverse(iPr_def_20) = sk_c4,
inference(demodulation,[status(thm)],[c_17099,c_14320]) ).
tcf(c_17501,plain,
multiply(sk_c4,sk_c10) = iPr_def_21,
inference(superposition,[status(thm)],[c_5492,c_17098]) ).
tcf(c_18183,plain,
multiply(sk_c5,iPr_def_18) = identity,
inference(superposition,[status(thm)],[c_13370,c_104]) ).
tcf(c_18185,plain,
! [X0: $i] : multiply(sk_c5,multiply(iPr_def_18,X0)) = X0,
inference(superposition,[status(thm)],[c_13370,c_13151]) ).
tcf(c_18193,plain,
( ( identity = iPr_def_19 )
| ( sk_c11 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_1745,c_18183]) ).
tcf(c_18194,plain,
( ( identity = iPr_def_19 )
| ( sk_c9 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_1479,c_18183]) ).
tcf(c_18196,plain,
( ( identity = iPr_def_19 )
| ( sk_c10 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_1179,c_18183]) ).
tcf(c_18825,plain,
( ( identity = iPr_def_19 )
| ( multiply(iPr_def_25,sk_c11) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_18194,c_625]) ).
tcf(c_18851,plain,
multiply(sk_c5,sk_c8) = iPr_def_19,
inference(superposition,[status(thm)],[c_5159,c_18185]) ).
tcf(c_19313,plain,
( ( identity = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_18196,c_637]) ).
tcf(c_21668,plain,
multiply(sk_c6,iPr_def_15) = identity,
inference(superposition,[status(thm)],[c_13372,c_104]) ).
tcf(c_21693,plain,
multiply(iPr_def_15,identity) = iPr_def_15,
inference(superposition,[status(thm)],[c_21668,c_2891]) ).
tcf(c_23475,plain,
multiply(sk_c1,iPr_def_26) = identity,
inference(superposition,[status(thm)],[c_13373,c_104]) ).
tcf(c_23476,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(inverse(inverse(iPr_def_26))) != inverse(X0) )
| ( multiply(sk_c1,inverse(X0)) != inverse(inverse(iPr_def_26)) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_13373,c_641]) ).
tcf(c_23477,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_26,X0)) = X0,
inference(superposition,[status(thm)],[c_13373,c_13151]) ).
tcf(c_23478,plain,
multiply(sk_c1,identity) = inverse(iPr_def_26),
inference(superposition,[status(thm)],[c_13373,c_14320]) ).
tcf(c_23486,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( identity = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_4123,c_23475]) ).
tcf(c_23514,plain,
multiply(iPr_def_26,identity) = iPr_def_26,
inference(superposition,[status(thm)],[c_23475,c_2890]) ).
tcf(c_23644,plain,
inverse(iPr_def_26) = sk_c1,
inference(demodulation,[status(thm)],[c_23478,c_14320]) ).
tcf(c_24183,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_27) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_23486,c_14353]) ).
tcf(c_24510,plain,
multiply(sk_c1,identity) = sk_c1,
inference(superposition,[status(thm)],[c_1232,c_23477]) ).
tcf(c_24511,plain,
multiply(sk_c1,sk_c11) = iPr_def_27,
inference(superposition,[status(thm)],[c_5044,c_23477]) ).
tcf(c_26810,plain,
multiply(sk_c2,iPr_def_24) = identity,
inference(superposition,[status(thm)],[c_13374,c_104]) ).
tcf(c_26811,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(inverse(inverse(iPr_def_24))) != inverse(X0) )
| ( multiply(sk_c2,inverse(X0)) != inverse(inverse(iPr_def_24)) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_13374,c_641]) ).
tcf(c_26812,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_24,X0)) = X0,
inference(superposition,[status(thm)],[c_13374,c_13151]) ).
tcf(c_26813,plain,
multiply(sk_c2,identity) = inverse(iPr_def_24),
inference(superposition,[status(thm)],[c_13374,c_14320]) ).
tcf(c_26833,plain,
( ( identity = iPr_def_25 )
| ( identity = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_19313,c_26810]) ).
tcf(c_26836,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( identity = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_3962,c_26810]) ).
tcf(c_26839,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( identity = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_3716,c_26810]) ).
tcf(c_27032,plain,
inverse(iPr_def_24) = sk_c2,
inference(demodulation,[status(thm)],[c_26813,c_14320]) ).
tcf(c_27042,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_13) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_3713,c_27032]) ).
tcf(c_27083,plain,
multiply(sk_c2,sk_c10) = iPr_def_25,
inference(superposition,[status(thm)],[c_5030,c_26812]) ).
tcf(c_27317,plain,
! [X0: $i] :
( ( identity = iPr_def_19 )
| ( multiply(iPr_def_25,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_26833,c_103]) ).
tcf(c_27795,plain,
! [X0: $i] :
( ( iPr_def_19 = iPr_def_22 )
| ( multiply(iPr_def_25,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_26836,c_103]) ).
tcf(c_28339,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_25,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_26839,c_103]) ).
tcf(c_36416,plain,
( ( identity = iPr_def_19 )
| ( sk_c11 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_27317,c_18825]) ).
tcf(c_38459,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( iPr_def_13 = iPr_def_26 )
| ( sk_c11 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_27795,c_7492]) ).
tcf(c_39224,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c11 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_28339,c_4081]) ).
tcf(c_39890,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( identity = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_36416,c_18193]) ).
tcf(c_42758,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( iPr_def_13 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_39224,c_1665]) ).
tcf(c_48560,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_13) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_42758,c_23644]) ).
tcf(c_50155,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_13) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_4223,c_24183]) ).
tcf(c_50156,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_24) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_4216,c_24183]) ).
tcf(c_50160,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c2 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_50156,c_27032]) ).
tcf(c_51630,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != identity )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_3428,c_14353]) ).
tcf(c_51681,plain,
( ~ iPr_def_12
| ( inverse(sk_c1) != identity )
| ( multiply(sk_c1,iPr_def_26) != sk_c11 )
| ( multiply(inverse(sk_c1),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_638,c_51630]) ).
tcf(c_51698,plain,
( ~ iPr_def_12
| ( inverse(iPr_def_24) != identity )
| ( multiply(iPr_def_24,sk_c2) != sk_c11 )
| ( multiply(inverse(iPr_def_24),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_27032,c_51630]) ).
tcf(c_51717,plain,
( ~ iPr_def_12
| ( sk_c2 != identity )
| ( sk_c11 != iPr_def_25 )
| ( sk_c11 != identity ) ),
inference(light_normalisation,[status(thm)],[c_51698,c_1233,c_27032,c_27083]) ).
tcf(c_51762,plain,
( ~ iPr_def_12
| ( identity != iPr_def_26 )
| ( sk_c11 != identity )
| ( multiply(iPr_def_26,sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_51681,c_638,c_23475]) ).
tcf(c_56468,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c4 )
| ( multiply(sk_c4,inverse(X0)) != iPr_def_20 )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_17097,c_632,c_17488]) ).
tcf(c_56521,plain,
( ~ iPr_def_12
| ( inverse(sk_c6) != sk_c4 )
| ( multiply(sk_c6,iPr_def_15) != sk_c11 )
| ( multiply(sk_c4,inverse(sk_c6)) != iPr_def_20 )
| ( multiply(inverse(sk_c6),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_627,c_56468]) ).
tcf(c_56621,plain,
( ~ iPr_def_12
| ( sk_c4 != iPr_def_15 )
| ( sk_c11 != identity )
| ( multiply(iPr_def_15,sk_c10) != sk_c11 )
| ( multiply(sk_c4,iPr_def_15) != iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_56521,c_627,c_21668]) ).
tcf(c_65833,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c1 )
| ( multiply(sk_c1,inverse(X0)) != iPr_def_26 )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_23476,c_638,c_23644]) ).
tcf(c_65888,plain,
( ~ iPr_def_12
| ( inverse(sk_c2) != sk_c1 )
| ( multiply(sk_c2,iPr_def_24) != sk_c11 )
| ( multiply(sk_c1,inverse(sk_c2)) != iPr_def_26 )
| ( multiply(inverse(sk_c2),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_636,c_65833]) ).
tcf(c_65981,plain,
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( sk_c1 != iPr_def_24 )
| ( multiply(iPr_def_24,sk_c10) != sk_c11 )
| ( multiply(sk_c1,iPr_def_24) != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_65888,c_636,c_26810]) ).
tcf(c_70997,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c2 )
| ( multiply(sk_c2,inverse(X0)) != iPr_def_24 )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_26811,c_636,c_27032]) ).
tcf(c_81346,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c9)),multiply(X0,iPr_def_13)) = sk_c11,
inference(superposition,[status(thm)],[c_625,c_13179]) ).
tcf(c_92011,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c1 = sk_c2 ) ),
inference(superposition,[status(thm)],[c_48560,c_27042]) ).
tcf(c_92696,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c1 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_92011,c_50160]) ).
tcf(c_92817,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_24) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_92696,c_638]) ).
tcf(c_92818,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c2 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_92817,c_27032]) ).
tcf(c_93080,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_92818,c_4226]) ).
tcf(c_93103,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c11 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_93080,c_5044]) ).
tcf(c_96161,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(sk_c9,iPr_def_25) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_93103,c_625]) ).
tcf(c_98641,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c2 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_50155,c_27042]) ).
tcf(c_108545,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_108558,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_108569,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_108600,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_108602,plain,
( ( sk_c11 = multiply(iPr_def_25,iPr_def_26) )
| ( sk_c11 != iPr_def_13 )
| ( multiply(iPr_def_25,iPr_def_26) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_108558]) ).
tcf(c_108612,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(X0,X1) )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_108772,plain,
! [X0: $i] :
( ( multiply(iPr_def_25,iPr_def_26) = X0 )
| ( X0 != iPr_def_13 )
| ( multiply(iPr_def_25,iPr_def_26) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_108600]) ).
tcf(c_108797,plain,
! [X0: $i] :
( ( X0 = multiply(iPr_def_25,iPr_def_26) )
| ( X0 != iPr_def_13 )
| ( multiply(iPr_def_25,iPr_def_26) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_108612]) ).
tcf(c_108867,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(iPr_def_25,iPr_def_26) )
| ( X1 != X0 )
| ( multiply(iPr_def_25,iPr_def_26) != X0 ) ),
inference(instantiation,[status(thm)],[c_108612]) ).
tcf(c_108875,plain,
( ( sk_c11 = identity )
| ( identity != multiply(iPr_def_25,iPr_def_26) )
| ( sk_c11 != multiply(iPr_def_25,iPr_def_26) ) ),
inference(instantiation,[status(thm)],[c_108545]) ).
tcf(c_109602,plain,
! [X0: $i] :
( ( identity = multiply(iPr_def_25,iPr_def_26) )
| ( identity != X0 )
| ( multiply(iPr_def_25,iPr_def_26) != X0 ) ),
inference(instantiation,[status(thm)],[c_108867]) ).
tcf(c_109603,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != multiply(iPr_def_25,iPr_def_26) )
| ( X0 != multiply(iPr_def_25,iPr_def_26) ) ),
inference(instantiation,[status(thm)],[c_108569]) ).
tcf(c_110132,plain,
! [X0: $i,X1: $i] :
( ( multiply(iPr_def_25,iPr_def_26) = multiply(X0,X1) )
| ( multiply(iPr_def_25,iPr_def_26) != iPr_def_13 )
| ( multiply(X0,X1) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_108772]) ).
tcf(c_110664,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c11) )
| ( X0 != iPr_def_27 )
| ( multiply(sk_c1,sk_c11) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_108612]) ).
tcf(c_110665,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c11) = X0 )
| ( X0 != iPr_def_27 )
| ( multiply(sk_c1,sk_c11) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_108600]) ).
tcf(c_115105,plain,
( ( identity = multiply(sk_c1,sk_c11) )
| ( identity != iPr_def_27 )
| ( multiply(sk_c1,sk_c11) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_110664]) ).
tcf(c_115107,plain,
( ( identity = multiply(iPr_def_25,iPr_def_26) )
| ( identity != multiply(sk_c1,sk_c11) )
| ( multiply(iPr_def_25,iPr_def_26) != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_109602]) ).
tcf(c_115284,plain,
( ( multiply(sk_c1,sk_c11) = iPr_def_13 )
| ( iPr_def_13 != iPr_def_27 )
| ( multiply(sk_c1,sk_c11) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_110665]) ).
tcf(c_115285,plain,
( ( multiply(iPr_def_25,iPr_def_26) = multiply(sk_c1,sk_c11) )
| ( multiply(iPr_def_25,iPr_def_26) != iPr_def_13 )
| ( multiply(sk_c1,sk_c11) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_110132]) ).
tcf(c_127299,plain,
( ( sk_c2 = identity )
| ( identity != multiply(iPr_def_25,iPr_def_26) )
| ( sk_c2 != multiply(iPr_def_25,iPr_def_26) ) ),
inference(instantiation,[status(thm)],[c_109603]) ).
tcf(c_134548,plain,
( ( sk_c2 = multiply(iPr_def_25,iPr_def_26) )
| ( sk_c2 != iPr_def_13 )
| ( multiply(iPr_def_25,iPr_def_26) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_108797]) ).
tcf(c_151842,plain,
iPr_def_14 = iPr_def_16,
inference(global_subsumption_just,[status(thm)],[c_96161,c_4223,c_11973,c_14461,c_23486,c_24511,c_39224,c_51717,c_93103,c_98641,c_108602,c_108875,c_115105,c_115107,c_115284,c_115285,c_127299,c_134548]) ).
tcf(c_151900,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(iPr_def_14,X0)) = multiply(sk_c8,X0),
inference(demodulation,[status(thm)],[c_5157,c_151842]) ).
tcf(c_151919,plain,
multiply(iPr_def_14,iPr_def_14) = sk_c8,
inference(demodulation,[status(thm)],[c_5131,c_151842]) ).
tcf(c_152975,plain,
multiply(sk_c8,identity) = multiply(iPr_def_14,iPr_def_14),
inference(superposition,[status(thm)],[c_14320,c_151900]) ).
tcf(c_152986,plain,
multiply(sk_c8,iPr_def_14) = multiply(iPr_def_14,sk_c8),
inference(superposition,[status(thm)],[c_151919,c_151900]) ).
tcf(c_153035,plain,
multiply(inverse(identity),multiply(inverse(sk_c9),iPr_def_13)) = sk_c11,
inference(superposition,[status(thm)],[c_104,c_81346]) ).
tcf(c_153085,plain,
multiply(inverse(multiply(inverse(iPr_def_13),sk_c9)),identity) = sk_c11,
inference(superposition,[status(thm)],[c_104,c_81346]) ).
tcf(c_153156,plain,
multiply(identity,sk_c11) = sk_c11,
inference(light_normalisation,[status(thm)],[c_153035,c_13176,c_14353]) ).
tcf(c_154322,plain,
multiply(sk_c7,multiply(iPr_def_14,sk_c8)) = multiply(iPr_def_14,iPr_def_14),
inference(superposition,[status(thm)],[c_152986,c_2874]) ).
tcf(c_154324,plain,
multiply(sk_c7,multiply(iPr_def_14,sk_c8)) = sk_c8,
inference(light_normalisation,[status(thm)],[c_154322,c_151919]) ).
tcf(c_155284,plain,
inverse(multiply(inverse(iPr_def_13),sk_c9)) = sk_c11,
inference(demodulation,[status(thm)],[c_153085,c_14320]) ).
tcf(c_155339,plain,
( ~ iPr_def_12
| ( inverse(multiply(inverse(iPr_def_13),sk_c9)) != sk_c2 )
| ( multiply(multiply(inverse(iPr_def_13),sk_c9),sk_c11) != sk_c11 )
| ( multiply(sk_c2,inverse(multiply(inverse(iPr_def_13),sk_c9))) != iPr_def_24 )
| ( multiply(inverse(multiply(inverse(iPr_def_13),sk_c9)),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_155284,c_70997]) ).
tcf(c_155359,plain,
multiply(sk_c11,multiply(inverse(iPr_def_13),sk_c9)) = identity,
inference(superposition,[status(thm)],[c_155284,c_104]) ).
tcf(c_155462,plain,
( ~ iPr_def_12
| ( sk_c11 != sk_c2 )
| ( multiply(sk_c2,sk_c11) != iPr_def_24 )
| ( multiply(sk_c11,sk_c10) != sk_c11 )
| ( multiply(multiply(inverse(iPr_def_13),sk_c9),sk_c11) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_155339,c_155284]) ).
tcf(c_156779,plain,
multiply(inverse(sk_c11),identity) = multiply(inverse(iPr_def_13),sk_c9),
inference(superposition,[status(thm)],[c_155359,c_13151]) ).
tcf(c_156782,plain,
multiply(inverse(multiply(sk_c11,inverse(iPr_def_13))),identity) = sk_c9,
inference(superposition,[status(thm)],[c_155359,c_13179]) ).
tcf(c_156784,plain,
multiply(iPr_def_13,multiply(inverse(iPr_def_13),sk_c9)) = multiply(sk_c9,identity),
inference(superposition,[status(thm)],[c_155359,c_2876]) ).
tcf(c_156785,plain,
multiply(iPr_def_23,multiply(inverse(iPr_def_13),sk_c9)) = multiply(sk_c3,identity),
inference(superposition,[status(thm)],[c_155359,c_2870]) ).
tcf(c_156786,plain,
multiply(iPr_def_27,multiply(inverse(iPr_def_13),sk_c9)) = multiply(sk_c1,identity),
inference(superposition,[status(thm)],[c_155359,c_2869]) ).
tcf(c_159563,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_156786,c_156785,c_156784,c_156782,c_156779,c_155462,c_154324,c_154322,c_152975,c_65981,c_56621,c_51762,c_39890,c_38459,c_27083,c_27032,c_26810,c_24511,c_24510,c_23644,c_23514,c_23475,c_21693,c_18851,c_18183,c_17501,c_17488,c_17099,c_17096,c_16418,c_16405,c_15614,c_15611,c_14893,c_14373,c_14366,c_14363,c_14361,c_14360,c_14339,c_14333,c_14332,c_14353,c_153156,c_14404,c_695,c_694,c_693,c_692,c_689,c_687,c_685,c_684,c_675,c_674,c_665,c_664,c_655,c_654,c_653,c_652,c_651,c_650,c_640,c_638,c_634,c_632]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP260-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 14:17:42 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 41.45/8.39 % SZS status Started for theBenchmark.p
% 41.45/8.39 % SZS status Unsatisfiable for theBenchmark.p
% 41.45/8.39
% 41.45/8.39 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 41.45/8.39
% 41.45/8.39 % ------ iProver source info
% 41.45/8.39
% 41.45/8.39 % git: date: 2026-07-19 20:42:38 +0200
% 41.45/8.39 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 41.45/8.39 % git: non_committed_changes: false
% 41.45/8.39
% 41.45/8.39 % ------ Parsing...% successful
% 41.45/8.39
% 41.45/8.39
% 41.45/8.39 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 41.45/8.39
% 41.45/8.39 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 41.45/8.39
% 41.45/8.39 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 41.45/8.39
% 41.45/8.39 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 41.45/8.39 % ------ Proving...
% 41.45/8.39 % ------ Problem Properties
% 41.45/8.39
% 41.45/8.39 %
% 41.45/8.39 % clauses 72
% 41.45/8.39 % conjectures 54
% 41.45/8.39 % EPR 51
% 41.45/8.39 % Horn 21
% 41.45/8.39 % unary 18
% 41.45/8.39 % binary 50
% 41.45/8.39 % lits 133
% 41.45/8.39 % lits eq 127
% 41.45/8.40 % fd_pure 0
% 41.45/8.40 % fd_pseudo 0
% 41.45/8.40 % fd_cond 0
% 41.45/8.40 % fd_pseudo_cond 0
% 41.45/8.40 % AC symbols 0
% 41.45/8.40
% 41.45/8.40 % ------ Schedule dynamic 5 is on
% 41.45/8.40
% 41.45/8.40 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 41.45/8.40
% 41.45/8.40
% 41.45/8.40 % ------
% 41.45/8.40 % Current options:
% 41.45/8.40 % ------
% 41.45/8.40
% 41.45/8.40
% 41.45/8.40 %
% 41.45/8.40
% 41.45/8.40 % ------ Proving...
% 41.45/8.40 %
% 41.45/8.40
% 41.45/8.40 % SZS status Unsatisfiable for theBenchmark.p
% 41.45/8.40
% 41.45/8.40 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 41.45/8.40
% 41.45/8.40
%------------------------------------------------------------------------------