%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP317-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 : n009.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:49 PM UTC 2026
% Result : Unsatisfiable 47.18s 7.24s
% Output : CNFRefutation 47.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 43
% Syntax : Number of formulae : 414 ( 45 unt; 0 def)
% Number of atoms : 1004 ( 937 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 982 ( 392 ~; 590 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 154 ( 0 sgn 154 !; 0 ?; 131 :)
% 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(f7,negated_conjecture,
( inverse(sk_c8) = sk_c7
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c7 = inverse(sk_c8)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c8 = inverse(sk_c5)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c8,sk_c9) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c9 = inverse(sk_c6)
| multiply(sk_c8,sk_c9) = sk_c7 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c9 = multiply(sk_c8,sk_c7)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( inverse(sk_c8) = sk_c7
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c7 = inverse(sk_c8)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f19]) ).
fof(f23,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c8 = inverse(sk_c5)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f28,plain,
( sk_c9 = inverse(sk_c6)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f30,plain,
( sk_c9 = multiply(sk_c8,sk_c7)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( inverse(sk_c8) = sk_c7
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c7 = inverse(sk_c8)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f36,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f35]) ).
fof(f37,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f39]) ).
fof(f45,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c9,sk_c7) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c8 = multiply(sk_c9,sk_c7) ),
inference(reorient_equations,[],[f45]) ).
fof(f49,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c9,sk_c7) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_23) ).
fof(f50,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c8 = multiply(sk_c9,sk_c7) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c9,sk_c7) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c9 = inverse(sk_c6)
| sk_c8 = multiply(sk_c9,sk_c7) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c9
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c9 = multiply(sk_c8,sk_c7)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( inverse(sk_c8) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c7 = inverse(sk_c8)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_27) ).
fof(f58,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = multiply(sk_c2,sk_c8) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c9
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c9 = multiply(sk_c8,sk_c7)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( inverse(sk_c8) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f68,plain,
( sk_c7 = inverse(sk_c8)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_33) ).
fof(f70,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f72,plain,
( sk_c8 = inverse(sk_c5)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_35) ).
fof(f74,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c9 = inverse(sk_c6)
| sk_c8 = inverse(sk_c2) ),
inference(reorient_equations,[],[f75]) ).
fof(f83,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c4) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_40) ).
fof(f84,plain,
( sk_c8 = inverse(sk_c5)
| inverse(sk_c4) = sk_c3 ),
inference(reorient_equations,[],[f83]) ).
fof(f87,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c4) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c9 = inverse(sk_c6)
| inverse(sk_c4) = sk_c3 ),
inference(reorient_equations,[],[f87]) ).
fof(f95,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_46) ).
fof(f96,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = inverse(sk_c3) ),
inference(reorient_equations,[],[f95]) ).
fof(f99,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_48) ).
fof(f100,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = inverse(sk_c3) ),
inference(reorient_equations,[],[f99]) ).
fof(f113,negated_conjecture,
! [X2,X3,X0,X1,X4,X5] :
( inverse(X5) != sk_c9
| multiply(X5,sk_c9) != sk_c7
| inverse(X4) != sk_c8
| multiply(X4,sk_c8) != sk_c9
| inverse(sk_c8) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c9
| multiply(X2,sk_c9) != X3
| inverse(X3) != sk_c9
| inverse(X2) != X3
| inverse(X1) != sk_c8
| multiply(X1,sk_c8) != sk_c9
| multiply(sk_c9,sk_c7) != sk_c8
| inverse(X0) != sk_c9
| multiply(X0,sk_c9) != sk_c8
| multiply(sk_c8,sk_c9) != sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_55) ).
fof(f114,plain,
! [X2,X3,X0,X1,X4,X5] :
( sk_c9 != inverse(X5)
| sk_c7 != multiply(X5,sk_c9)
| sk_c8 != inverse(X4)
| sk_c9 != multiply(X4,sk_c8)
| sk_c7 != inverse(sk_c8)
| sk_c9 != multiply(sk_c8,sk_c7)
| multiply(X2,sk_c9) != X3
| sk_c9 != inverse(X3)
| inverse(X2) != X3
| sk_c8 != inverse(X1)
| sk_c9 != multiply(X1,sk_c8)
| sk_c8 != multiply(sk_c9,sk_c7)
| inverse(X0) != sk_c9
| sk_c8 != multiply(X0,sk_c9)
| multiply(sk_c8,sk_c9) != sk_c7 ),
inference(reorient_equations,[],[f113]) ).
fof(f115,plain,
! [X2,X0,X1,X4,X5] :
( sk_c9 != inverse(X5)
| sk_c7 != multiply(X5,sk_c9)
| sk_c8 != inverse(X4)
| sk_c9 != multiply(X4,sk_c8)
| sk_c7 != inverse(sk_c8)
| sk_c9 != multiply(sk_c8,sk_c7)
| inverse(X2) != multiply(X2,sk_c9)
| sk_c9 != inverse(inverse(X2))
| sk_c8 != inverse(X1)
| sk_c9 != multiply(X1,sk_c8)
| sk_c8 != multiply(sk_c9,sk_c7)
| inverse(X0) != sk_c9
| sk_c8 != multiply(X0,sk_c9)
| multiply(sk_c8,sk_c9) != sk_c7 ),
inference(equality_resolution,[],[f114]) ).
tcf(c_107,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_108,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_112,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_114,negated_conjecture,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_116,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_132,negated_conjecture,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_134,negated_conjecture,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_135,negated_conjecture,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_138,negated_conjecture,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_140,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_143,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_145,negated_conjecture,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c4) = sk_c3 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c4) = sk_c3 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_155,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_164,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c8) != sk_c7 )
| ( inverse(X4) != sk_c9 )
| ( inverse(X3) != sk_c8 )
| ( inverse(X2) != sk_c8 )
| ( inverse(X1) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( multiply(sk_c8,sk_c7) != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c7 )
| ( inverse(inverse(X0)) != sk_c9 )
| ( multiply(X4,sk_c9) != sk_c7 )
| ( multiply(X3,sk_c8) != sk_c9 )
| ( multiply(X2,sk_c8) != sk_c9 )
| ( multiply(X1,sk_c9) != sk_c8 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_665,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_164]) ).
tcf(c_666,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_164]) ).
tcf(c_667,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_164]) ).
tcf(c_668,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != sk_c9 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_164]) ).
tcf(c_669,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c8) != sk_c7 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( multiply(sk_c8,sk_c7) != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_164]) ).
tcf(c_670,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_671,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_672,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_673,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_676,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_678,plain,
( ~ iPr_def_11
| ( inverse(sk_c9) != sk_c9 )
| ( multiply(sk_c9,sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_961,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( sk_c8 != X0 )
| ( multiply(sk_c9,sk_c7) != X0 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_964,plain,
! [X0: $i,X1: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_965,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != sk_c8 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_964]) ).
tcf(c_966,plain,
sk_c8 = sk_c8,
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_972,plain,
( ( sk_c8 = multiply(identity,sk_c8) )
| ( sk_c8 != sk_c8 )
| ( multiply(identity,sk_c8) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_965]) ).
tcf(c_973,plain,
multiply(identity,sk_c8) = sk_c8,
inference(instantiation,[status(thm)],[c_107]) ).
tcf(c_975,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_976,plain,
( ( sk_c9 = sk_c8 )
| ( sk_c9 != sk_c9 )
| ( sk_c8 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_975]) ).
tcf(c_981,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( sk_c8 != multiply(identity,sk_c8) )
| ( multiply(sk_c9,sk_c7) != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_961]) ).
tcf(c_982,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != multiply(identity,sk_c8) )
| ( X0 != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_964]) ).
tcf(c_990,plain,
! [X0: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != multiply(identity,sk_c8) )
| ( X0 != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_975]) ).
tcf(c_992,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c7) = inverse(sk_c5) )
| ( inverse(sk_c5) != X0 )
| ( multiply(sk_c9,sk_c7) != X0 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_996,plain,
( ( multiply(sk_c9,sk_c7) = multiply(identity,sk_c8) )
| ( sk_c7 != sk_c8 )
| ( sk_c9 != identity ) ),
inference(instantiation,[status(thm)],[c_672]) ).
tcf(c_1001,plain,
( ( sk_c8 = multiply(sk_c9,sk_c7) )
| ( sk_c8 != sk_c8 )
| ( multiply(sk_c9,sk_c7) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_965]) ).
tcf(c_1002,plain,
! [X0: $i] :
( ( inverse(sk_c8) = sk_c7 )
| ( sk_c7 != X0 )
| ( inverse(sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1011,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,sk_c8) )
| ( X1 != X0 )
| ( multiply(identity,sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1013,plain,
! [X0: $i,X1: $i] :
( ( sk_c8 = multiply(X0,X1) )
| ( sk_c8 != multiply(identity,sk_c8) )
| ( multiply(X0,X1) != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_982]) ).
tcf(c_1036,plain,
! [X0: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != multiply(sk_c9,sk_c7) )
| ( X0 != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_975]) ).
tcf(c_1037,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != multiply(sk_c9,sk_c7) )
| ( X0 != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_964]) ).
tcf(c_1038,plain,
( ( sk_c8 = sk_c9 )
| ( sk_c9 != multiply(sk_c9,sk_c7) )
| ( sk_c8 != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_1037]) ).
tcf(c_1063,plain,
! [X0: $i,X1: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1067,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c7) = inverse(sk_c5) )
| ( inverse(sk_c5) != inverse(X0) )
| ( multiply(sk_c9,sk_c7) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_992]) ).
tcf(c_1068,plain,
! [X0: $i] :
( ( inverse(sk_c5) = inverse(X0) )
| ( sk_c5 != X0 ) ),
inference(instantiation,[status(thm)],[c_673]) ).
tcf(c_1069,plain,
( ( multiply(sk_c9,sk_c7) = inverse(sk_c5) )
| ( inverse(sk_c5) != inverse(sk_c9) )
| ( multiply(sk_c9,sk_c7) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1067]) ).
tcf(c_1070,plain,
( ( inverse(sk_c5) = inverse(sk_c9) )
| ( sk_c5 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1068]) ).
tcf(c_1076,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,sk_c8) = X1 )
| ( X1 != X0 )
| ( multiply(identity,sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1077,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(identity,sk_c8) )
| ( X2 != multiply(X0,X1) )
| ( multiply(identity,sk_c8) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_1011]) ).
tcf(c_1115,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_1117,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1204,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_108,c_109]) ).
tcf(c_1256,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c5) )
| ( X1 != X0 )
| ( inverse(sk_c5) != X0 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1287,plain,
! [X0: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != sk_c7 )
| ( X0 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_1288,plain,
sk_c7 = sk_c7,
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_1289,plain,
( ( sk_c7 = sk_c9 )
| ( sk_c7 != sk_c7 )
| ( sk_c9 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1287]) ).
tcf(c_1306,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c7) = inverse(X1) )
| ( inverse(X1) != X0 )
| ( multiply(sk_c9,sk_c7) != X0 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1307,plain,
( ( multiply(sk_c9,sk_c7) = inverse(sk_c9) )
| ( inverse(sk_c9) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1306]) ).
tcf(c_1309,plain,
! [X0: $i,X1: $i] :
( ( sk_c5 = X0 )
| ( sk_c5 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1383,plain,
! [X0: $i] :
( ( multiply(identity,sk_c8) = X0 )
| ( X0 != sk_c8 )
| ( multiply(identity,sk_c8) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1076]) ).
tcf(c_1395,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1497,plain,
( ( sk_c7 = inverse(sk_c8) )
| ( sk_c7 != sk_c7 )
| ( inverse(sk_c8) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1287]) ).
tcf(c_1499,plain,
( ( sk_c7 = multiply(identity,sk_c7) )
| ( sk_c7 != sk_c7 )
| ( multiply(identity,sk_c7) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1287]) ).
tcf(c_1500,plain,
multiply(identity,sk_c7) = sk_c7,
inference(instantiation,[status(thm)],[c_107]) ).
tcf(c_1502,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c7 )
| ( sk_c7 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1951,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c9) = X0 )
| ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_671,c_116]) ).
tcf(c_1953,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c9) = X0 )
| ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_671,c_120]) ).
tcf(c_2009,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_671,c_670]) ).
tcf(c_2023,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c9,sk_c7) )
| ( X1 != X0 )
| ( multiply(sk_c9,sk_c7) != X0 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_2024,plain,
( ( sk_c9 = multiply(sk_c9,sk_c7) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2023]) ).
tcf(c_2025,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c8 )
| ( sk_c8 != multiply(sk_c9,sk_c7) )
| ( multiply(X0,X1) != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_1036]) ).
tcf(c_2026,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c9,sk_c7) )
| ( X1 != sk_c7 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_672]) ).
tcf(c_2027,plain,
( ( multiply(sk_c9,sk_c9) = sk_c8 )
| ( sk_c8 != multiply(sk_c9,sk_c7) )
| ( multiply(sk_c9,sk_c9) != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_2025]) ).
tcf(c_2028,plain,
( ( multiply(sk_c9,sk_c9) = multiply(sk_c9,sk_c7) )
| ( sk_c9 != sk_c7 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2026]) ).
tcf(c_2075,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c7) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c9,sk_c7) != X0 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_2077,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c7) = multiply(X0,X1) )
| ( sk_c7 != X1 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_672]) ).
tcf(c_2118,plain,
( ( sk_c8 = multiply(sk_c9,sk_c7) )
| ( sk_c8 != multiply(identity,sk_c8) )
| ( multiply(sk_c9,sk_c7) != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1013]) ).
tcf(c_2250,plain,
( ( multiply(identity,sk_c8) = multiply(sk_c9,sk_c7) )
| ( multiply(identity,sk_c8) != sk_c8 )
| ( multiply(sk_c9,sk_c7) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1383]) ).
tcf(c_2285,plain,
! [X0: $i] :
( ( sk_c5 = X0 )
| ( sk_c5 != sk_c5 )
| ( X0 != sk_c5 ) ),
inference(instantiation,[status(thm)],[c_1309]) ).
tcf(c_2286,plain,
sk_c5 = sk_c5,
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_2440,plain,
( ~ iPr_def_10
| ( inverse(sk_c5) != sk_c8 )
| ( multiply(sk_c5,sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_2441,plain,
( ( multiply(identity,sk_c8) = inverse(sk_c5) )
| ( inverse(sk_c5) != sk_c8 )
| ( multiply(identity,sk_c8) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1383]) ).
tcf(c_2447,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c5) )
| ( X0 != sk_c8 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1256]) ).
tcf(c_2521,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1395]) ).
tcf(c_2522,plain,
( ( identity = sk_c9 )
| ( identity != identity )
| ( sk_c9 != identity ) ),
inference(instantiation,[status(thm)],[c_2521]) ).
tcf(c_2573,plain,
! [X0: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != multiply(sk_c6,sk_c9) )
| ( X0 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_2574,plain,
( ( sk_c7 = sk_c9 )
| ( sk_c7 != multiply(sk_c6,sk_c9) )
| ( sk_c9 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_2573]) ).
tcf(c_2661,plain,
! [X0: $i] :
( ( multiply(identity,sk_c8) = X0 )
| ( X0 != inverse(sk_c5) )
| ( multiply(identity,sk_c8) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_1076]) ).
tcf(c_2754,plain,
! [X0: $i] :
( ( X0 = sk_c7 )
| ( sk_c7 != inverse(sk_c8) )
| ( X0 != inverse(sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1502]) ).
tcf(c_2756,plain,
! [X0: $i] :
( ( X0 = sk_c7 )
| ( sk_c7 != multiply(sk_c6,sk_c9) )
| ( X0 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1502]) ).
tcf(c_2757,plain,
( ( sk_c9 = sk_c7 )
| ( sk_c7 != multiply(sk_c6,sk_c9) )
| ( sk_c9 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_2756]) ).
tcf(c_3096,plain,
( ( inverse(sk_c2) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c5) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_142,c_665]) ).
tcf(c_3099,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c2) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_136,c_665]) ).
tcf(c_3102,plain,
( ( inverse(sk_c5) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c2) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_137,c_665]) ).
tcf(c_3120,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_120,c_666]) ).
tcf(c_3133,plain,
( ~ iPr_def_11
| ( sk_c8 != identity )
| ( inverse(inverse(sk_c9)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_108,c_666]) ).
tcf(c_3142,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ~ iPr_def_12
| ( inverse(sk_c6) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_132,c_667]) ).
tcf(c_3146,plain,
( ( inverse(sk_c2) = sk_c8 )
| ~ iPr_def_12
| ( inverse(sk_c6) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_144,c_667]) ).
tcf(c_3147,plain,
( ( inverse(sk_c1) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c6) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_126,c_667]) ).
tcf(c_3151,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_12
| ( sk_c8 != sk_c7 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_121,c_667]) ).
tcf(c_3161,plain,
( ~ iPr_def_12
| ( sk_c7 != identity )
| ( inverse(inverse(sk_c9)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_108,c_667]) ).
tcf(c_3212,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1204,c_107]) ).
tcf(c_3268,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_108,c_3212]) ).
tcf(c_3284,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_3212,c_3212]) ).
tcf(c_3387,plain,
( ( inverse(sk_c2) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c5) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_665,c_142]) ).
tcf(c_3418,plain,
! [X0: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != multiply(identity,sk_c7) )
| ( X0 != multiply(identity,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_3562,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_3284,c_108]) ).
tcf(c_3628,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_666,c_120]) ).
tcf(c_3684,plain,
( ( inverse(sk_c2) = sk_c8 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_3387,c_143,c_2440,c_3102,c_3096,c_3099]) ).
tcf(c_3686,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_3684,c_2440,c_3102,c_3099,c_3684]) ).
tcf(c_3744,plain,
( ( sk_c7 = multiply(sk_c6,sk_c9) )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2009,c_126]) ).
tcf(c_3748,plain,
( ( sk_c7 = multiply(sk_c6,sk_c9) )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(resolution,[status(thm)],[c_2009,c_114]) ).
tcf(c_3749,plain,
( ( sk_c7 = multiply(sk_c6,sk_c9) )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_2009,c_132]) ).
tcf(c_3812,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c7) = multiply(X0,sk_c7) )
| ( sk_c7 != sk_c7 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_2077]) ).
tcf(c_4087,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_127,c_3562]) ).
tcf(c_4089,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_123,c_3562]) ).
tcf(c_4090,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_145,c_3562]) ).
tcf(c_4092,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_141,c_3562]) ).
tcf(c_4173,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_3268,c_3284]) ).
tcf(c_4182,plain,
! [X0: $i] : multiply(X0,identity) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_4173,c_3284]) ).
tcf(c_4183,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4182,c_4173]) ).
tcf(c_4185,plain,
( ~ iPr_def_12
| ( sk_c7 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3161,c_4183]) ).
tcf(c_4186,plain,
( ~ iPr_def_11
| ( sk_c8 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3133,c_4183]) ).
tcf(c_4278,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_4087,c_121]) ).
tcf(c_4290,plain,
( ( sk_c8 = identity )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_4278,c_3562]) ).
tcf(c_4387,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_4089,c_117]) ).
tcf(c_4473,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_4090,c_139]) ).
tcf(c_4577,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c8) )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_673]) ).
tcf(c_4579,plain,
( ( inverse(sk_c9) = inverse(sk_c8) )
| ( sk_c9 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_4577]) ).
tcf(c_4769,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c6,sk_c9) )
| ( X1 != X0 )
| ( multiply(sk_c6,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_4794,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_4092,c_135]) ).
tcf(c_5141,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_4183,c_108]) ).
tcf(c_5343,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_120,c_666]) ).
tcf(c_5364,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ~ iPr_def_12
| ( inverse(sk_c6) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_132,c_667]) ).
tcf(c_5369,plain,
( ( inverse(sk_c1) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c6) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_126,c_667]) ).
tcf(c_5387,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_127,c_5141]) ).
tcf(c_5391,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_143,c_5141]) ).
tcf(c_5574,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( X0 != sk_c9 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(light_normalisation,[status(thm)],[c_668,c_4183]) ).
tcf(c_5825,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_5387,c_121]) ).
tcf(c_5836,plain,
( ( sk_c8 = identity )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_5825,c_5141]) ).
tcf(c_5838,plain,
( ( sk_c8 = identity )
| ( multiply(sk_c9,sk_c6) = identity ) ),
inference(superposition,[status(thm)],[c_5825,c_108]) ).
tcf(c_5848,plain,
! [X0: $i] :
( ( sk_c8 = identity )
| ( multiply(sk_c9,multiply(sk_c6,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_5838,c_109]) ).
tcf(c_5859,plain,
( ( sk_c7 = identity )
| ( sk_c8 = identity )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_5836,c_114]) ).
tcf(c_5862,plain,
( ( sk_c7 = identity )
| ( sk_c8 = identity )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_5836,c_144]) ).
tcf(c_5863,plain,
( ( sk_c7 = identity )
| ( sk_c8 = identity )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_5836,c_126]) ).
tcf(c_5977,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_5391,c_137]) ).
tcf(c_5984,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_5977,c_5141]) ).
tcf(c_6066,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_5984,c_130]) ).
tcf(c_6067,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_5984,c_112]) ).
tcf(c_6070,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_5984,c_142]) ).
tcf(c_6071,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_5984,c_124]) ).
tcf(c_6125,plain,
( ( sk_c9 = identity )
| ~ iPr_def_13
| ( sk_c8 != sk_c9 )
| ( inverse(sk_c8) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_6067,c_5574]) ).
tcf(c_6350,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c7) = X0 )
| ( X0 != sk_c8 )
| ( multiply(sk_c9,sk_c7) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_2075]) ).
tcf(c_6356,plain,
( ( multiply(sk_c9,sk_c7) = sk_c9 )
| ( sk_c9 != sk_c8 )
| ( multiply(sk_c9,sk_c7) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_6350]) ).
tcf(c_6385,plain,
( ( inverse(sk_c1) = sk_c9 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_5369,c_127,c_3147]) ).
tcf(c_6904,plain,
! [X0: $i] :
( ( X0 = multiply(identity,sk_c8) )
| ( X0 != multiply(sk_c9,sk_c7) )
| ( multiply(identity,sk_c8) != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_1077]) ).
tcf(c_7030,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_5343,c_126,c_3120]) ).
tcf(c_7471,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_5364,c_133,c_3142]) ).
tcf(c_8060,plain,
! [X0: $i] :
( ( sk_c8 = identity )
| ( multiply(sk_c9,multiply(sk_c6,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_5848,c_107]) ).
tcf(c_8068,plain,
( ( sk_c8 = identity )
| ( multiply(sk_c9,sk_c7) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_132,c_8060]) ).
tcf(c_8745,plain,
( ~ iPr_def_12
| ( inverse(sk_c6) != sk_c9 )
| ( multiply(sk_c6,sk_c9) != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_667]) ).
tcf(c_9029,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_3628,c_7030]) ).
tcf(c_9039,plain,
( ( sk_c7 = multiply(sk_c6,sk_c9) )
| ~ iPr_def_11 ),
inference(resolution,[status(thm)],[c_9029,c_2009]) ).
tcf(c_10359,plain,
( ( multiply(sk_c9,sk_c7) = multiply(identity,sk_c7) )
| ( sk_c7 != sk_c7 )
| ( sk_c9 != identity ) ),
inference(instantiation,[status(thm)],[c_3812]) ).
tcf(c_10360,plain,
( ( sk_c7 = multiply(sk_c9,sk_c7) )
| ( sk_c7 != multiply(identity,sk_c7) )
| ( multiply(sk_c9,sk_c7) != multiply(identity,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_3418]) ).
tcf(c_10987,plain,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ~ iPr_def_12
| ( sk_c7 != sk_c8 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_1951,c_667]) ).
tcf(c_11130,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ~ iPr_def_12
| ( sk_c7 != sk_c8 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_1953,c_667]) ).
tcf(c_11272,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_151,c_4183]) ).
tcf(c_11273,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_149,c_4183]) ).
tcf(c_11275,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c9) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_157,c_4183]) ).
tcf(c_11278,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_4183,c_108]) ).
tcf(c_11415,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_115,c_667]) ).
tcf(c_11443,plain,
( ( inverse(sk_c9) = sk_c3 )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_11275,c_11278]) ).
tcf(c_11446,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_125,c_11278]) ).
tcf(c_11447,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_123,c_11278]) ).
tcf(c_11500,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( X0 != sk_c9 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(light_normalisation,[status(thm)],[c_668,c_4183]) ).
tcf(c_11552,plain,
( ( sk_c9 = sk_c4 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_11272,c_157]) ).
tcf(c_11560,plain,
( ( sk_c9 = sk_c4 )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_11552,c_11278]) ).
tcf(c_11569,plain,
( ( sk_c9 = sk_c4 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_11273,c_155]) ).
tcf(c_11576,plain,
( ( sk_c9 = sk_c4 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_11569,c_11278]) ).
tcf(c_11689,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1204,c_107]) ).
tcf(c_11761,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(sk_c2),sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_139,c_11689]) ).
tcf(c_11762,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(inverse(sk_c2),sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_137,c_11689]) ).
tcf(c_11763,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(inverse(sk_c2),sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_135,c_11689]) ).
tcf(c_11850,plain,
( ( sk_c7 = identity )
| ( sk_c9 = sk_c4 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_11560,c_132]) ).
tcf(c_11851,plain,
( ( sk_c7 = identity )
| ( sk_c9 = sk_c4 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_11560,c_114]) ).
tcf(c_11874,plain,
( ( sk_c9 = identity )
| ( sk_c9 = sk_c4 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_11576,c_142]) ).
tcf(c_11920,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_11446,c_119]) ).
tcf(c_11931,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c8) = sk_c5 ) ),
inference(superposition,[status(thm)],[c_11920,c_4183]) ).
tcf(c_11946,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_11447,c_117]) ).
tcf(c_12023,plain,
( ( sk_c7 = sk_c5 )
| ( sk_c8 = identity ) ),
inference(superposition,[status(thm)],[c_11931,c_11946]) ).
tcf(c_12398,plain,
( ( sk_c7 = identity )
| ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c9) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_11443,c_144]) ).
tcf(c_12399,plain,
( ( sk_c7 = identity )
| ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c9) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_11443,c_126]) ).
tcf(c_12842,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_145,c_11761]) ).
tcf(c_12857,plain,
( ( sk_c8 = sk_c7 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_12842,c_115]) ).
tcf(c_12874,plain,
( ( sk_c8 = sk_c7 )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_12857,c_11278]) ).
tcf(c_12881,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_143,c_11762]) ).
tcf(c_12896,plain,
( ( sk_c8 = sk_c7 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_12881,c_113]) ).
tcf(c_13053,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_141,c_11763]) ).
tcf(c_13068,plain,
( ( sk_c8 = sk_c7 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_13053,c_111]) ).
tcf(c_13102,plain,
( ( sk_c8 = sk_c7 )
| ( multiply(sk_c8,sk_c7) = identity ) ),
inference(superposition,[status(thm)],[c_13068,c_11278]) ).
tcf(c_13397,plain,
! [X0: $i] :
( ( sk_c8 = identity )
| ( identity != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_1117]) ).
tcf(c_13400,plain,
( ( sk_c8 = identity )
| ( identity != sk_c9 )
| ( sk_c8 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_13397]) ).
tcf(c_13426,plain,
! [X0: $i] :
( ( sk_c7 = identity )
| ( identity != X0 )
| ( sk_c7 != X0 ) ),
inference(instantiation,[status(thm)],[c_1117]) ).
tcf(c_13427,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( sk_c7 != identity )
| ( inverse(sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_1002]) ).
tcf(c_13428,plain,
( ( sk_c7 = identity )
| ( identity != sk_c9 )
| ( sk_c7 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_13426]) ).
tcf(c_13792,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_11415,c_127,c_3147,c_3151,c_12857]) ).
tcf(c_14493,plain,
( ( multiply(identity,sk_c8) = multiply(sk_c9,sk_c7) )
| ( multiply(identity,sk_c8) != inverse(sk_c5) )
| ( multiply(sk_c9,sk_c7) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_2661]) ).
tcf(c_16281,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c6,sk_c9) )
| ( X0 != identity )
| ( multiply(sk_c6,sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_4769]) ).
tcf(c_16283,plain,
( ( sk_c9 = multiply(sk_c6,sk_c9) )
| ( sk_c9 != identity )
| ( multiply(sk_c6,sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_16281]) ).
tcf(c_16722,plain,
( ( sk_c7 != sk_c8 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_10987,c_6385,c_8745,c_11130,c_13792]) ).
tcf(c_16723,plain,
( ~ iPr_def_12
| ( sk_c7 != sk_c8 ) ),
inference(renaming,[status(thm)],[c_16722]) ).
tcf(c_18488,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_964]) ).
tcf(c_18489,plain,
( ( sk_c8 = sk_c9 )
| ( sk_c9 != identity )
| ( sk_c8 != identity ) ),
inference(instantiation,[status(thm)],[c_18488]) ).
tcf(c_20389,plain,
! [X0: $i] :
( ( identity = sk_c8 )
| ( identity != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_1395]) ).
tcf(c_20397,plain,
( ( identity = inverse(sk_c5) )
| ( identity != sk_c8 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_2447]) ).
tcf(c_20405,plain,
( ( identity = sk_c8 )
| ( identity != sk_c9 )
| ( sk_c8 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_20389]) ).
tcf(c_20657,plain,
( ( sk_c7 = inverse(sk_c5) )
| ( sk_c7 != sk_c8 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_2447]) ).
tcf(c_20658,plain,
( ( sk_c7 = identity )
| ( identity != inverse(sk_c5) )
| ( sk_c7 != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_13426]) ).
tcf(c_20725,plain,
( ( sk_c7 = sk_c8 )
| ( sk_c7 != sk_c7 )
| ( sk_c8 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1287]) ).
tcf(c_21024,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(global_subsumption_just,[status(thm)],[c_11874,c_6070]) ).
tcf(c_21035,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c2,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_21024,c_11278]) ).
tcf(c_21108,plain,
( ( sk_c8 = sk_c7 )
| ( sk_c7 != sk_c8 )
| ( sk_c8 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_965]) ).
tcf(c_21152,plain,
! [X0: $i] :
( ( sk_c7 = sk_c8 )
| ( sk_c7 != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_975]) ).
tcf(c_21153,plain,
( ( sk_c7 = sk_c8 )
| ( sk_c7 != sk_c9 )
| ( sk_c8 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_21152]) ).
tcf(c_21286,plain,
( ( sk_c8 = sk_c7 )
| ( sk_c7 != multiply(identity,sk_c8) )
| ( sk_c8 != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_982]) ).
tcf(c_21339,plain,
( ( sk_c7 = sk_c8 )
| ( sk_c7 != multiply(identity,sk_c8) )
| ( sk_c8 != multiply(identity,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_990]) ).
tcf(c_21524,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c7 )
| ( sk_c7 != inverse(sk_c8) )
| ( inverse(X0) != inverse(sk_c8) ) ),
inference(instantiation,[status(thm)],[c_2754]) ).
tcf(c_21526,plain,
( ( inverse(sk_c9) = sk_c7 )
| ( sk_c7 != inverse(sk_c8) )
| ( inverse(sk_c9) != inverse(sk_c8) ) ),
inference(instantiation,[status(thm)],[c_21524]) ).
tcf(c_22183,plain,
( ( sk_c5 = sk_c7 )
| ( sk_c5 != sk_c5 )
| ( sk_c7 != sk_c5 ) ),
inference(instantiation,[status(thm)],[c_2285]) ).
tcf(c_22493,plain,
! [X0: $i] :
( ( sk_c5 = X0 )
| ( sk_c5 != sk_c7 )
| ( X0 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1309]) ).
tcf(c_22494,plain,
( ( sk_c5 = sk_c9 )
| ( sk_c5 != sk_c7 )
| ( sk_c9 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_22493]) ).
tcf(c_23174,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_21035,c_138]) ).
tcf(c_23176,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_21035,c_134]) ).
tcf(c_23202,plain,
( ( sk_c9 = identity )
| ~ iPr_def_12
| ( inverse(sk_c6) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_23174,c_667]) ).
tcf(c_23203,plain,
( ( sk_c9 = identity )
| ~ iPr_def_11
| ( sk_c8 != sk_c7 )
| ( inverse(sk_c6) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_23174,c_666]) ).
tcf(c_23238,plain,
( ( sk_c9 = identity )
| ( sk_c8 = sk_c7 ) ),
inference(superposition,[status(thm)],[c_23176,c_13102]) ).
tcf(c_23253,plain,
( ( sk_c9 = identity )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_23202,c_13792,c_23202]) ).
tcf(c_23257,plain,
( ( sk_c7 = identity )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(global_subsumption_just,[status(thm)],[c_11850,c_966,c_972,c_973,c_981,c_996,c_1115,c_1288,c_2522,c_2574,c_3749,c_6066,c_12874,c_13428,c_16283,c_20725]) ).
tcf(c_23272,plain,
( ( sk_c7 = identity )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(global_subsumption_just,[status(thm)],[c_11851,c_113,c_1115,c_1288,c_2522,c_2574,c_3748,c_5859,c_6067,c_12874,c_13428,c_16283,c_18489,c_20405,c_20397,c_20657,c_20658,c_20725]) ).
tcf(c_23282,plain,
( ( sk_c7 = identity )
| ~ iPr_def_13
| ( sk_c8 != sk_c9 )
| ( inverse(sk_c8) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_23272,c_11500]) ).
tcf(c_23787,plain,
( ( sk_c7 = multiply(identity,sk_c8) )
| ( sk_c7 != multiply(sk_c9,sk_c7) )
| ( multiply(identity,sk_c8) != multiply(sk_c9,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_6904]) ).
tcf(c_23824,plain,
( ( sk_c7 = identity )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(global_subsumption_just,[status(thm)],[c_12398,c_145,c_141,c_140,c_669,c_3146,c_3686,c_4186,c_5862,c_6070,c_18489,c_23257,c_23272,c_23282]) ).
tcf(c_23933,plain,
( ( sk_c7 = identity )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_12399,c_143,c_125,c_123,c_122,c_669,c_966,c_972,c_973,c_1115,c_1288,c_1499,c_1500,c_2250,c_2440,c_2522,c_2574,c_3102,c_3096,c_3099,c_3744,c_4186,c_5863,c_5859,c_6071,c_7471,c_10359,c_10360,c_12874,c_13428,c_16283,c_16723,c_18489,c_20405,c_20397,c_20657,c_20658,c_20725,c_21339,c_23253,c_23257,c_23282,c_23787]) ).
tcf(c_24045,plain,
~ iPr_def_12,
inference(global_subsumption_just,[status(thm)],[c_4185,c_966,c_972,c_973,c_1288,c_1499,c_1500,c_2250,c_7471,c_10359,c_10360,c_16723,c_21339,c_23253,c_23787]) ).
tcf(c_24047,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c8) != sk_c7 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( multiply(sk_c8,sk_c7) != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_669,c_24045]) ).
tcf(c_24212,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_4183,c_108]) ).
tcf(c_24242,negated_conjecture,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_665,c_143,c_2440,c_3102,c_3096,c_3099]) ).
tcf(c_24244,plain,
( iPr_def_13
| iPr_def_11
| ( inverse(sk_c8) != sk_c7 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( multiply(sk_c8,sk_c7) != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_24047,c_24242]) ).
tcf(c_24248,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_127,c_24212]) ).
tcf(c_24250,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_123,c_24212]) ).
tcf(c_24251,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_145,c_24212]) ).
tcf(c_24262,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_24212,c_107]) ).
tcf(c_24263,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_24212,c_109]) ).
tcf(c_24264,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_24212,c_109]) ).
tcf(c_24303,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_24263,c_107]) ).
tcf(c_24307,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(superposition,[status(thm)],[c_108,c_24303]) ).
tcf(c_24315,plain,
! [X0: $i] :
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c1,multiply(sk_c9,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_123,c_24303]) ).
tcf(c_24361,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_120,c_666]) ).
tcf(c_24377,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( X0 != sk_c9 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(light_normalisation,[status(thm)],[c_668,c_4183]) ).
tcf(c_24405,plain,
( ~ iPr_def_13
| ( sk_c9 != identity )
| ( inverse(identity) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_107,c_24377]) ).
tcf(c_24625,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_24248,c_121]) ).
tcf(c_24634,plain,
( ( sk_c8 = identity )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_24625,c_24212]) ).
tcf(c_24673,plain,
( ( sk_c8 = identity )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_24250,c_117]) ).
tcf(c_24682,plain,
( ( sk_c8 = identity )
| ( multiply(sk_c8,sk_c7) = identity ) ),
inference(superposition,[status(thm)],[c_24673,c_24212]) ).
tcf(c_24717,plain,
( ( sk_c7 = identity )
| ( sk_c8 = identity )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_24634,c_132]) ).
tcf(c_24721,plain,
( ( sk_c7 = identity )
| ( sk_c8 = identity )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_24634,c_144]) ).
tcf(c_24722,plain,
( ( sk_c7 = identity )
| ( sk_c8 = identity )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_24634,c_126]) ).
tcf(c_24769,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_24251,c_139]) ).
tcf(c_24777,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c9) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_24769,c_4183]) ).
tcf(c_24853,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( multiply(sk_c9,multiply(sk_c6,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_24777,c_24303]) ).
tcf(c_25217,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c1,multiply(sk_c9,inverse(sk_c8))) = identity ) ),
inference(superposition,[status(thm)],[c_117,c_24264]) ).
tcf(c_25736,plain,
( ~ iPr_def_13
| ( sk_c9 != identity ) ),
inference(light_normalisation,[status(thm)],[c_24405,c_24262]) ).
tcf(c_25831,plain,
( ( sk_c7 = identity )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(global_subsumption_just,[status(thm)],[c_24721,c_23824]) ).
tcf(c_25836,plain,
( ( sk_c7 = identity )
| ( multiply(sk_c2,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_25831,c_24212]) ).
tcf(c_25840,plain,
( ( sk_c7 = identity )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_24722,c_23933]) ).
tcf(c_25845,plain,
( ( sk_c7 = identity )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_25840,c_24212]) ).
tcf(c_25964,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_24361,c_126,c_3120]) ).
tcf(c_25976,plain,
( ( sk_c7 = identity )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(global_subsumption_just,[status(thm)],[c_24717,c_23257]) ).
tcf(c_26298,plain,
( ( sk_c7 = identity )
| ( sk_c9 = identity )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_25836,c_138]) ).
tcf(c_26299,plain,
( ( sk_c7 = identity )
| ( sk_c9 = identity )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_25836,c_136]) ).
tcf(c_26317,plain,
( ( sk_c7 = identity )
| ( sk_c8 = identity )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_25845,c_120]) ).
tcf(c_27143,plain,
( ( inverse(sk_c8) = identity )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_25217,c_24315]) ).
tcf(c_27610,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( sk_c9 = identity ) ),
inference(global_subsumption_just,[status(thm)],[c_26298,c_23174]) ).
tcf(c_27611,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(renaming,[status(thm)],[c_27610]) ).
tcf(c_27624,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c9,sk_c7) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_27611,c_24853]) ).
tcf(c_27627,plain,
sk_c9 = identity,
inference(global_subsumption_just,[status(thm)],[c_26299,c_676,c_669,c_966,c_1001,c_1038,c_2024,c_3686,c_4473,c_4794,c_6067,c_6066,c_6125,c_23176,c_23203,c_23238,c_24045,c_27624]) ).
tcf(c_27676,plain,
( ( sk_c9 = sk_c7 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_25976,c_27627]) ).
tcf(c_27689,plain,
( ~ iPr_def_13
| ( sk_c9 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_25736,c_27627]) ).
tcf(c_27734,plain,
( ( sk_c8 = sk_c9 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_24682,c_27627]) ).
tcf(c_27756,plain,
! [X0: $i] : multiply(X0,sk_c9) = X0,
inference(demodulation,[status(thm)],[c_24307,c_27627]) ).
tcf(c_27758,plain,
inverse(sk_c9) = sk_c9,
inference(demodulation,[status(thm)],[c_24262,c_27627]) ).
tcf(c_27769,plain,
! [X0: $i] : multiply(sk_c9,X0) = X0,
inference(demodulation,[status(thm)],[c_107,c_27627]) ).
tcf(c_27770,plain,
~ iPr_def_13,
inference(equality_resolution_simp,[status(thm)],[c_27689]) ).
tcf(c_27779,plain,
( ( sk_c9 = sk_c7 )
| ( sk_c8 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_27676,c_27769]) ).
tcf(c_27855,plain,
( iPr_def_11
| ( inverse(sk_c8) != sk_c7 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( multiply(sk_c8,sk_c7) != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_24244,c_27770]) ).
tcf(c_27856,plain,
( iPr_def_11
| ( sk_c8 != sk_c7 )
| ( inverse(sk_c8) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_27855,c_27756,c_27769]) ).
tcf(c_27869,plain,
( ( sk_c7 = identity )
| ( sk_c8 = identity ) ),
inference(global_subsumption_just,[status(thm)],[c_26317,c_143,c_676,c_678,c_669,c_966,c_972,c_973,c_996,c_1001,c_1038,c_1069,c_1070,c_1115,c_1289,c_1288,c_1307,c_1499,c_1500,c_2024,c_2027,c_2028,c_2118,c_2250,c_2286,c_2440,c_2441,c_2522,c_2757,c_3102,c_3096,c_3099,c_4290,c_4387,c_4473,c_4794,c_6067,c_6066,c_6125,c_7471,c_8068,c_9039,c_10359,c_10360,c_12023,c_12896,c_13400,c_14493,c_16283,c_16723,c_18489,c_20725,c_21108,c_21153,c_21286,c_21339,c_22183,c_22494,c_23176,c_23203,c_23238,c_23253,c_23787,c_27624,c_27758,c_27779,c_27734,c_27856]) ).
tcf(c_27871,plain,
( ( sk_c9 = sk_c7 )
| ( sk_c8 = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_27869,c_27627]) ).
tcf(c_27923,plain,
( ( sk_c8 = sk_c7 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_115,c_27756]) ).
tcf(c_27926,plain,
( ( sk_c7 = sk_c6 )
| ~ iPr_def_11 ),
inference(demodulation,[status(thm)],[c_25964,c_27756]) ).
tcf(c_28011,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_27926,c_143,c_676,c_678,c_669,c_966,c_972,c_973,c_996,c_1001,c_1038,c_1069,c_1070,c_1115,c_1289,c_1288,c_1307,c_1499,c_1500,c_2024,c_2027,c_2028,c_2118,c_2250,c_2286,c_2440,c_2441,c_2522,c_2757,c_3102,c_3096,c_3099,c_4186,c_4290,c_4387,c_4473,c_4794,c_6067,c_6066,c_6125,c_7471,c_8068,c_9039,c_10359,c_10360,c_12023,c_12896,c_13400,c_14493,c_16283,c_16723,c_18489,c_20725,c_21108,c_21153,c_21286,c_21339,c_22183,c_22494,c_23176,c_23203,c_23238,c_23253,c_23787,c_27624,c_27758,c_27779,c_27734,c_27856]) ).
tcf(c_28013,plain,
( ( sk_c8 != sk_c7 )
| ( inverse(sk_c8) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_27856,c_28011]) ).
tcf(c_28022,plain,
sk_c8 = sk_c7,
inference(global_subsumption_just,[status(thm)],[c_27923,c_966,c_972,c_973,c_1069,c_1070,c_1289,c_1288,c_1307,c_1499,c_1500,c_2250,c_2286,c_2441,c_8068,c_10359,c_10360,c_12023,c_12896,c_14493,c_18489,c_21108,c_21153,c_21286,c_22183,c_22494,c_23787,c_27627,c_27758,c_27779]) ).
tcf(c_28025,plain,
sk_c8 = sk_c9,
inference(demodulation,[status(thm)],[c_27871,c_28022]) ).
tcf(c_28054,plain,
( ( inverse(sk_c8) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_28013,c_28022]) ).
tcf(c_28080,plain,
( ( inverse(sk_c9) != sk_c7 )
| ( multiply(sk_c9,sk_c7) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_28054,c_28025]) ).
tcf(c_28126,plain,
sk_c9 = sk_c7,
inference(demodulation,[status(thm)],[c_28022,c_28025]) ).
tcf(c_28136,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_28126,c_28080,c_28025,c_28022,c_27627,c_27143,c_21526,c_20725,c_13427,c_13428,c_6356,c_4579,c_2522,c_1497,c_1288,c_1289,c_1115,c_996,c_981,c_976,c_973,c_972,c_966,c_676]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP317-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.10/0.35 % Computer : n009.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 14:27:13 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/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.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.42 % Proving...
% 47.18/7.24 % SZS status Started for theBenchmark.p
% 47.18/7.24 % SZS status Unsatisfiable for theBenchmark.p
% 47.18/7.24
% 47.18/7.24 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 47.18/7.24
% 47.18/7.24 % ------ iProver source info
% 47.18/7.24
% 47.18/7.24 % git: date: 2026-07-19 20:42:38 +0200
% 47.18/7.24 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 47.18/7.24 % git: non_committed_changes: false
% 47.18/7.24
% 47.18/7.24 % ------ Parsing...% successful
% 47.18/7.24
% 47.18/7.24
% 47.18/7.24 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 47.18/7.24
% 47.18/7.24 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 47.18/7.24
% 47.18/7.24 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 47.18/7.24
% 47.18/7.24 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 47.18/7.24 % ------ Proving...
% 47.18/7.24 % ------ Problem Properties
% 47.18/7.24
% 47.18/7.24 %
% 47.18/7.24 % clauses 62
% 47.18/7.24 % conjectures 59
% 47.18/7.24 % EPR 0
% 47.18/7.24 % Horn 7
% 47.18/7.24 % unary 3
% 47.18/7.24 % binary 54
% 47.18/7.24 % lits 131
% 47.18/7.24 % lits eq 123
% 47.18/7.24 % fd_pure 0
% 47.18/7.24 % fd_pseudo 0
% 47.18/7.24 % fd_cond 0
% 47.18/7.24 % fd_pseudo_cond 0
% 47.18/7.24 % AC symbols 0
% 47.18/7.24
% 47.18/7.24 % ------ Input Options Time Limit: Unbounded
% 47.18/7.24
% 47.18/7.24
% 47.18/7.24 % ------
% 47.18/7.24 % Current options:
% 47.18/7.24 % ------
% 47.18/7.24
% 47.18/7.24
% 47.18/7.24 %
% 47.18/7.24
% 47.18/7.24 % ------ Proving...
% 47.18/7.24 %
% 47.18/7.24
% 47.18/7.24 % SZS status Unsatisfiable for theBenchmark.p
% 47.18/7.24
% 47.18/7.24 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 47.18/7.25
% 47.18/7.25
%------------------------------------------------------------------------------