%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP251-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 : n012.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:28 PM UTC 2026
% Result : Unsatisfiable 7.97s 6.53s
% Output : CNFRefutation 7.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 47
% Syntax : Number of formulae : 338 ( 92 unt; 13 def)
% Number of atoms : 1097 ( 616 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 512 ( 173 ~; 339 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 2 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 : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 81 ( 0 sgn 81 !; 0 ?; 55 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c10 = inverse(sk_c4)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c8 = inverse(sk_c5)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c9 = inverse(sk_c6)
| multiply(sk_c1,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c8 = inverse(sk_c5)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f31,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c9 = inverse(sk_c6)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f31]) ).
fof(f37,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c8 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f37]) ).
fof(f45,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c9 = inverse(sk_c6)
| sk_c8 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f45]) ).
fof(f51,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f51]) ).
fof(f59,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c9 = inverse(sk_c3) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c10 = inverse(sk_c4)
| sk_c9 = inverse(sk_c3) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = inverse(sk_c3) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f68,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = inverse(sk_c3) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| inverse(sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_33) ).
fof(f70,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c9 = inverse(sk_c3) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f72,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c9 = inverse(sk_c3) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_35) ).
fof(f74,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = inverse(sk_c3) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
( sk_c10 = inverse(sk_c4)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f77]) ).
fof(f79,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_38) ).
fof(f80,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f79]) ).
fof(f81,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_39) ).
fof(f82,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
( multiply(sk_c9,sk_c7) = sk_c8
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_40) ).
fof(f84,plain,
( sk_c8 = multiply(sk_c9,sk_c7)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_41) ).
fof(f86,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
! [X2,X3,X0,X1,X6,X4,X5] :
( inverse(X6) != sk_c9
| multiply(X6,sk_c9) != X5
| multiply(sk_c9,X5) != sk_c8
| inverse(X4) != sk_c8
| multiply(X4,sk_c8) != sk_c9
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != sk_c9
| multiply(X2,sk_c8) != sk_c9
| inverse(X2) != sk_c9
| inverse(X1) != sk_c9
| multiply(X1,sk_c9) != sk_c8
| inverse(X0) != sk_c10
| multiply(X0,sk_c10) != sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_43) ).
fof(f90,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( sk_c9 != inverse(X6)
| multiply(X6,sk_c9) != X5
| sk_c8 != multiply(sk_c9,X5)
| sk_c8 != inverse(X4)
| sk_c9 != multiply(X4,sk_c8)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c9 != multiply(X2,sk_c8)
| sk_c9 != inverse(X2)
| sk_c9 != inverse(X1)
| sk_c8 != multiply(X1,sk_c9)
| inverse(X0) != sk_c10
| sk_c9 != multiply(X0,sk_c10) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,plain,
! [X2,X3,X0,X1,X6,X4] :
( sk_c9 != inverse(X6)
| sk_c8 != multiply(sk_c9,multiply(X6,sk_c9))
| sk_c8 != inverse(X4)
| sk_c9 != multiply(X4,sk_c8)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c9 != multiply(X2,sk_c8)
| sk_c9 != inverse(X2)
| sk_c9 != inverse(X1)
| sk_c8 != multiply(X1,sk_c9)
| inverse(X0) != sk_c10
| sk_c9 != multiply(X0,sk_c10) ),
inference(equality_resolution,[],[f90]) ).
tcf(c_95,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_96,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_98,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_99,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_100,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_101,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_102,negated_conjecture,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_103,negated_conjecture,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_104,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_105,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_114,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_118,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_133,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c3,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_135,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_137,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_138,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c3,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_140,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(X5) != sk_c9 )
| ( inverse(X4) != sk_c9 )
| ( inverse(X3) != sk_c9 )
| ( inverse(X2) != sk_c8 )
| ( inverse(X1) != sk_c10 )
| ( inverse(X0) != sk_c10 )
| ( multiply(X5,sk_c9) != sk_c8 )
| ( multiply(X3,sk_c8) != sk_c9 )
| ( multiply(X2,sk_c8) != sk_c9 )
| ( multiply(X1,sk_c10) != sk_c9 )
| ( multiply(X0,sk_c10) != sk_c9 )
| ( multiply(sk_c9,multiply(X4,sk_c9)) != sk_c8 ) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_537,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_140]) ).
tcf(c_538,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_140]) ).
tcf(c_539,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_140]) ).
tcf(c_540,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_140]) ).
tcf(c_541,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c9 )
| ( multiply(sk_c9,multiply(X0,sk_c9)) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_140]) ).
tcf(c_542,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_140]) ).
tcf(c_543,definition,
iPr_def_15 = multiply(sk_c3,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_544,definition,
iPr_def_16 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_545,definition,
iPr_def_17 = multiply(sk_c6,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_546,definition,
iPr_def_18 = multiply(sk_c9,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_547,definition,
iPr_def_19 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_548,definition,
iPr_def_20 = multiply(sk_c5,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_549,definition,
iPr_def_21 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_550,definition,
iPr_def_22 = multiply(sk_c4,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_551,definition,
iPr_def_23 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_552,definition,
iPr_def_24 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_553,definition,
iPr_def_25 = multiply(sk_c2,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_554,definition,
iPr_def_26 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_555,definition,
iPr_def_27 = multiply(sk_c1,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_556,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_542]) ).
tcf(c_557,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c9 )
| ( multiply(sk_c9,multiply(X0,sk_c9)) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_541]) ).
tcf(c_558,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_540]) ).
tcf(c_560,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_539]) ).
tcf(c_561,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_538]) ).
tcf(c_562,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_537]) ).
tcf(c_563,negated_conjecture,
( ( iPr_def_16 = sk_c9 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_139,c_544,c_543]) ).
tcf(c_564,negated_conjecture,
( ( iPr_def_17 = sk_c7 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_138,c_545]) ).
tcf(c_565,negated_conjecture,
( ( iPr_def_18 = sk_c8 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_137,c_546]) ).
tcf(c_566,negated_conjecture,
( ( iPr_def_19 = sk_c8 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_136,c_547]) ).
tcf(c_567,negated_conjecture,
( ( iPr_def_20 = sk_c9 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_135,c_548]) ).
tcf(c_568,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_134,c_549]) ).
tcf(c_569,negated_conjecture,
( ( iPr_def_22 = sk_c9 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_133,c_550]) ).
tcf(c_570,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_132,c_551]) ).
tcf(c_571,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_572,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_573,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_19 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_574,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_128]) ).
tcf(c_575,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_576,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_577,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_125,c_552]) ).
tcf(c_581,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_584,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_118,c_553]) ).
tcf(c_588,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_591,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_111,c_554]) ).
tcf(c_594,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_19 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_595,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_596,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_597,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_598,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_104,c_555]) ).
tcf(c_599,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_103]) ).
tcf(c_600,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_18 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_102]) ).
tcf(c_601,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_19 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_101]) ).
tcf(c_602,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_100]) ).
tcf(c_603,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_99]) ).
tcf(c_604,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_98]) ).
tcf(c_896,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c9 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_565,c_566]) ).
tcf(c_983,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c9 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_573,c_572]) ).
tcf(c_984,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c3,iPr_def_19) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_573,c_543]) ).
tcf(c_1080,plain,
( ( sk_c9 = iPr_def_15 )
| ( multiply(iPr_def_16,sk_c7) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_563,c_546]) ).
tcf(c_1081,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c9,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_571,c_546]) ).
tcf(c_1113,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c4,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_575,c_550]) ).
tcf(c_1114,plain,
( ( sk_c9 = iPr_def_15 )
| ( multiply(sk_c4,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_568,c_550]) ).
tcf(c_1120,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_576,c_553]) ).
tcf(c_1121,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_574,c_553]) ).
tcf(c_1122,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_570,c_553]) ).
tcf(c_1124,plain,
( ( sk_c9 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_20) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_567,c_553]) ).
tcf(c_1154,plain,
multiply(iPr_def_21,sk_c4) = identity,
inference(superposition,[status(thm)],[c_549,c_96]) ).
tcf(c_1155,plain,
multiply(iPr_def_19,sk_c5) = identity,
inference(superposition,[status(thm)],[c_547,c_96]) ).
tcf(c_1156,plain,
multiply(iPr_def_16,sk_c6) = identity,
inference(superposition,[status(thm)],[c_544,c_96]) ).
tcf(c_1157,plain,
multiply(iPr_def_26,sk_c1) = identity,
inference(superposition,[status(thm)],[c_554,c_96]) ).
tcf(c_1158,plain,
multiply(iPr_def_24,sk_c2) = identity,
inference(superposition,[status(thm)],[c_552,c_96]) ).
tcf(c_1159,plain,
multiply(iPr_def_23,sk_c3) = identity,
inference(superposition,[status(thm)],[c_551,c_96]) ).
tcf(c_1344,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c5,iPr_def_25) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_584,c_548]) ).
tcf(c_1512,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(sk_c5,iPr_def_25) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_588,c_548]) ).
tcf(c_1638,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_591,c_555]) ).
tcf(c_1726,plain,
( ( sk_c8 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_594,c_555]) ).
tcf(c_1765,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_595,c_555]) ).
tcf(c_1804,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_596,c_555]) ).
tcf(c_1843,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_597,c_555]) ).
tcf(c_1887,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_598,c_553]) ).
tcf(c_1949,plain,
( ( sk_c9 = iPr_def_27 )
| ( multiply(sk_c9,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_599,c_546]) ).
tcf(c_2028,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c9 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_601,c_600]) ).
tcf(c_2035,plain,
( ( sk_c9 = iPr_def_27 )
| ( multiply(sk_c5,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_601,c_548]) ).
tcf(c_2115,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_602,c_545]) ).
tcf(c_2213,plain,
( ( sk_c9 = iPr_def_27 )
| ( multiply(sk_c1,iPr_def_21) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_603,c_555]) ).
tcf(c_2214,plain,
( ( sk_c9 = iPr_def_27 )
| ( multiply(sk_c4,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_603,c_550]) ).
tcf(c_2269,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_604,c_553]) ).
tcf(c_2852,plain,
( ~ iPr_def_13
| ( sk_c8 != iPr_def_17 )
| ( inverse(sk_c6) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_545,c_558]) ).
tcf(c_2853,plain,
( ~ iPr_def_13
| ( sk_c8 != iPr_def_25 )
| ( inverse(sk_c2) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_553,c_558]) ).
tcf(c_2855,plain,
( ~ iPr_def_13
| ( sk_c8 != identity )
| ( inverse(inverse(sk_c9)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_96,c_558]) ).
tcf(c_2875,plain,
( ~ iPr_def_13
| ( sk_c8 != iPr_def_25 )
| ( sk_c9 != iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_2853,c_552]) ).
tcf(c_2879,plain,
( ~ iPr_def_13
| ( sk_c8 != iPr_def_17 )
| ( sk_c9 != iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_2852,c_544]) ).
tcf(c_3033,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_20 )
| ( inverse(sk_c5) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_548,c_560]) ).
tcf(c_3034,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_15 )
| ( inverse(sk_c3) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_543,c_560]) ).
tcf(c_3053,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_23 )
| ( sk_c9 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_3034,c_551]) ).
tcf(c_3057,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_20 )
| ( sk_c9 != iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_3033,c_547]) ).
tcf(c_3190,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_27 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_555,c_561]) ).
tcf(c_3191,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_22 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_550,c_561]) ).
tcf(c_3208,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_22 )
| ( sk_c10 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_3191,c_549]) ).
tcf(c_3212,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_27 )
| ( sk_c10 != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_3190,c_554]) ).
tcf(c_3298,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_20 )
| ( inverse(sk_c5) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_548,c_562]) ).
tcf(c_3299,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_15 )
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_543,c_562]) ).
tcf(c_3322,plain,
( ~ iPr_def_10
| ( sk_c8 != iPr_def_19 )
| ( sk_c9 != iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_3298,c_547]) ).
tcf(c_3458,plain,
( ~ iPr_def_14
| ( inverse(sk_c6) != sk_c9 )
| ( multiply(sk_c9,iPr_def_17) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_545,c_557]) ).
tcf(c_3485,plain,
( ~ iPr_def_14
| ( sk_c9 != iPr_def_16 )
| ( multiply(sk_c9,iPr_def_17) != sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_3458,c_544]) ).
tcf(c_3743,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_983,c_553]) ).
tcf(c_4103,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c7,X0)) = multiply(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_546,c_97]) ).
tcf(c_4104,plain,
! [X0: $i] : multiply(sk_c6,multiply(sk_c9,X0)) = multiply(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_545,c_97]) ).
tcf(c_4108,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_96,c_97]) ).
tcf(c_4111,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1154,c_97]) ).
tcf(c_4112,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1155,c_97]) ).
tcf(c_4113,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1156,c_97]) ).
tcf(c_4114,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1157,c_97]) ).
tcf(c_4115,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1158,c_97]) ).
tcf(c_4116,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1159,c_97]) ).
tcf(c_4123,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4116,c_95]) ).
tcf(c_4124,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4115,c_95]) ).
tcf(c_4125,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4114,c_95]) ).
tcf(c_4126,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4113,c_95]) ).
tcf(c_4127,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4112,c_95]) ).
tcf(c_4128,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4111,c_95]) ).
tcf(c_5871,plain,
multiply(iPr_def_23,iPr_def_15) = sk_c8,
inference(superposition,[status(thm)],[c_543,c_4123]) ).
tcf(c_5883,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(iPr_def_15,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_5871,c_97]) ).
tcf(c_5885,plain,
multiply(iPr_def_24,iPr_def_25) = sk_c9,
inference(superposition,[status(thm)],[c_553,c_4124]) ).
tcf(c_5888,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(iPr_def_25,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_5885,c_97]) ).
tcf(c_5963,plain,
multiply(iPr_def_26,iPr_def_27) = sk_c10,
inference(superposition,[status(thm)],[c_555,c_4125]) ).
tcf(c_5976,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_23,iPr_def_15) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_984,c_4123]) ).
tcf(c_5977,plain,
( ( sk_c8 = iPr_def_19 )
| ( sk_c9 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_5976,c_5871]) ).
tcf(c_6360,plain,
multiply(iPr_def_16,iPr_def_17) = sk_c9,
inference(superposition,[status(thm)],[c_545,c_4126]) ).
tcf(c_6384,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(iPr_def_17,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_6360,c_97]) ).
tcf(c_6396,plain,
multiply(iPr_def_19,iPr_def_20) = sk_c8,
inference(superposition,[status(thm)],[c_548,c_4127]) ).
tcf(c_6399,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(iPr_def_20,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_6396,c_97]) ).
tcf(c_6401,plain,
multiply(iPr_def_21,iPr_def_22) = sk_c10,
inference(superposition,[status(thm)],[c_550,c_4128]) ).
tcf(c_6511,plain,
( ( sk_c9 = iPr_def_15 )
| ( multiply(iPr_def_16,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_564,c_1080]) ).
tcf(c_6513,plain,
( ( sk_c9 = iPr_def_18 )
| ( sk_c9 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_6511,c_6360]) ).
tcf(c_8173,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1121,c_4124]) ).
tcf(c_8174,plain,
( ( sk_c9 = iPr_def_23 )
| ( sk_c9 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_8173,c_5885]) ).
tcf(c_8215,plain,
( ( sk_c9 = iPr_def_15 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_1124,c_4124]) ).
tcf(c_8216,plain,
( ( sk_c9 = iPr_def_20 )
| ( sk_c9 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_8215,c_5885]) ).
tcf(c_8666,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_19,iPr_def_20) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1344,c_4127]) ).
tcf(c_8667,plain,
( ( sk_c8 = iPr_def_25 )
| ( sk_c9 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_8666,c_6396]) ).
tcf(c_8894,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(iPr_def_19,iPr_def_20) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1512,c_4127]) ).
tcf(c_8895,plain,
( ( sk_c8 = iPr_def_25 )
| ( sk_c9 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_8894,c_6396]) ).
tcf(c_9431,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1804,c_4125]) ).
tcf(c_9432,plain,
( ( sk_c10 = iPr_def_26 )
| ( sk_c10 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_9431,c_5963]) ).
tcf(c_9686,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1843,c_4125]) ).
tcf(c_9687,plain,
( ( sk_c9 = iPr_def_22 )
| ( sk_c10 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_9686,c_5963]) ).
tcf(c_9717,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1887,c_4124]) ).
tcf(c_9718,plain,
( ( sk_c9 = iPr_def_27 )
| ( sk_c9 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_9717,c_5885]) ).
tcf(c_9890,plain,
( ( sk_c9 = iPr_def_27 )
| ( multiply(iPr_def_19,iPr_def_20) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_2035,c_4127]) ).
tcf(c_9891,plain,
( ( sk_c8 = iPr_def_19 )
| ( sk_c9 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_9890,c_6396]) ).
tcf(c_10291,plain,
( ( sk_c9 = iPr_def_27 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_2213,c_4125]) ).
tcf(c_10292,plain,
( ( sk_c9 = iPr_def_27 )
| ( sk_c10 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_10291,c_5963]) ).
tcf(c_10322,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2269,c_4124]) ).
tcf(c_10323,plain,
( ( sk_c9 = iPr_def_27 )
| ( sk_c9 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_10322,c_5885]) ).
tcf(c_11980,plain,
multiply(sk_c6,iPr_def_18) = multiply(iPr_def_17,sk_c7),
inference(superposition,[status(thm)],[c_546,c_4104]) ).
tcf(c_15389,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_4108,c_95]) ).
tcf(c_15400,plain,
multiply(inverse(sk_c6),iPr_def_17) = sk_c9,
inference(superposition,[status(thm)],[c_545,c_15389]) ).
tcf(c_15401,plain,
multiply(inverse(sk_c2),iPr_def_25) = sk_c9,
inference(superposition,[status(thm)],[c_553,c_15389]) ).
tcf(c_15402,plain,
multiply(inverse(sk_c3),iPr_def_15) = sk_c8,
inference(superposition,[status(thm)],[c_543,c_15389]) ).
tcf(c_15403,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_95,c_15389]) ).
tcf(c_15404,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_96,c_15389]) ).
tcf(c_15459,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(inverse(sk_c9),iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_1081,c_15389]) ).
tcf(c_15477,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( multiply(inverse(sk_c2),iPr_def_25) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_3743,c_15389]) ).
tcf(c_15478,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(inverse(sk_c2),iPr_def_25) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1122,c_15389]) ).
tcf(c_15479,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(inverse(sk_c2),iPr_def_25) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1121,c_15389]) ).
tcf(c_15480,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(inverse(sk_c2),iPr_def_25) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1120,c_15389]) ).
tcf(c_15503,plain,
multiply(inverse(iPr_def_23),identity) = sk_c3,
inference(superposition,[status(thm)],[c_1159,c_15389]) ).
tcf(c_15536,plain,
( ( sk_c9 = iPr_def_20 )
| ( multiply(inverse(sk_c6),iPr_def_17) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2115,c_15389]) ).
tcf(c_15567,plain,
! [X0: $i] : multiply(inverse(iPr_def_21),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_4128,c_15389]) ).
tcf(c_15568,plain,
! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_4127,c_15389]) ).
tcf(c_15569,plain,
! [X0: $i] : multiply(inverse(iPr_def_16),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_4126,c_15389]) ).
tcf(c_15570,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_4125,c_15389]) ).
tcf(c_15573,plain,
multiply(inverse(iPr_def_23),sk_c8) = iPr_def_15,
inference(superposition,[status(thm)],[c_5871,c_15389]) ).
tcf(c_15601,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_15389,c_15389]) ).
tcf(c_16429,plain,
( ~ iPr_def_14
| ( inverse(inverse(identity)) != sk_c9 )
| ( multiply(sk_c9,sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_15403,c_557]) ).
tcf(c_16448,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_15404,c_15601]) ).
tcf(c_16460,plain,
multiply(sk_c8,identity) = multiply(iPr_def_19,iPr_def_20),
inference(superposition,[status(thm)],[c_16448,c_6399]) ).
tcf(c_16463,plain,
multiply(sk_c9,sk_c7) = multiply(iPr_def_18,identity),
inference(superposition,[status(thm)],[c_16448,c_4103]) ).
tcf(c_16464,plain,
multiply(sk_c9,identity) = multiply(iPr_def_16,iPr_def_17),
inference(superposition,[status(thm)],[c_16448,c_6384]) ).
tcf(c_16467,plain,
multiply(sk_c9,identity) = multiply(iPr_def_24,iPr_def_25),
inference(superposition,[status(thm)],[c_16448,c_5888]) ).
tcf(c_16468,plain,
multiply(sk_c8,identity) = multiply(iPr_def_23,iPr_def_15),
inference(superposition,[status(thm)],[c_16448,c_5883]) ).
tcf(c_16475,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_16448,c_15403]) ).
tcf(c_16476,plain,
multiply(sk_c8,identity) = sk_c8,
inference(light_normalisation,[status(thm)],[c_16468,c_5871]) ).
tcf(c_16477,plain,
multiply(sk_c9,identity) = sk_c9,
inference(light_normalisation,[status(thm)],[c_16467,c_5885]) ).
tcf(c_16481,plain,
multiply(iPr_def_18,identity) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_16463,c_546]) ).
tcf(c_16493,plain,
multiply(identity,identity) = identity,
inference(superposition,[status(thm)],[c_16475,c_96]) ).
tcf(c_18782,plain,
( ( sk_c9 = iPr_def_20 )
| ~ iPr_def_13
| ( sk_c8 != iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_581,c_2875]) ).
tcf(c_18783,plain,
( ( sk_c9 = iPr_def_16 )
| ~ iPr_def_13
| ( sk_c8 != iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_577,c_2875]) ).
tcf(c_19053,plain,
( ( sk_c9 = iPr_def_20 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_18782,c_8895,c_18782]) ).
tcf(c_19059,plain,
( ( sk_c9 = iPr_def_16 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_18783,c_8667,c_18783]) ).
tcf(c_19755,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_3057,c_3057,c_3053,c_8174,c_8216]) ).
tcf(c_19783,plain,
( ( sk_c9 = iPr_def_15 )
| ~ iPr_def_12
| ( iPr_def_18 != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_6513,c_19755]) ).
tcf(c_19809,plain,
( ( sk_c9 = iPr_def_15 )
| ~ iPr_def_12
| ( iPr_def_19 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_569,c_19755]) ).
tcf(c_20243,plain,
( ( sk_c9 = iPr_def_15 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_19809,c_896,c_19783]) ).
tcf(c_20249,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_23 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3053,c_20243]) ).
tcf(c_20355,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_22 ) ),
inference(global_subsumption_just,[status(thm)],[c_3208,c_3212,c_3208,c_9432,c_10292]) ).
tcf(c_20357,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_20355,c_3212,c_9687,c_10323,c_20355]) ).
tcf(c_20359,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_556,c_20357]) ).
tcf(c_20412,plain,
multiply(sk_c4,iPr_def_21) = identity,
inference(superposition,[status(thm)],[c_15567,c_96]) ).
tcf(c_20419,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_21,X0)) = X0,
inference(superposition,[status(thm)],[c_15567,c_15389]) ).
tcf(c_20433,plain,
( ( identity = iPr_def_22 )
| ( sk_c9 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_2214,c_20412]) ).
tcf(c_20436,plain,
( ( identity = iPr_def_22 )
| ( sk_c9 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1114,c_20412]) ).
tcf(c_20437,plain,
( ( identity = iPr_def_22 )
| ( sk_c9 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_1113,c_20412]) ).
tcf(c_21232,plain,
multiply(sk_c4,sk_c10) = iPr_def_22,
inference(superposition,[status(thm)],[c_6401,c_20419]) ).
tcf(c_21308,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( identity = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_20436,c_20433]) ).
tcf(c_21763,plain,
( ( identity = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_20437,c_553]) ).
tcf(c_22192,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_27 )
| ( multiply(iPr_def_22,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_21308,c_95]) ).
tcf(c_22352,plain,
multiply(sk_c5,iPr_def_19) = identity,
inference(superposition,[status(thm)],[c_15568,c_96]) ).
tcf(c_22355,plain,
( ~ iPr_def_10
| ( inverse(inverse(iPr_def_19)) != sk_c8 )
| ( multiply(sk_c5,sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_15568,c_562]) ).
tcf(c_22360,plain,
multiply(sk_c5,identity) = inverse(iPr_def_19),
inference(superposition,[status(thm)],[c_15568,c_16448]) ).
tcf(c_22368,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_20 )
| ( inverse(inverse(iPr_def_19)) != sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_22355,c_548]) ).
tcf(c_22375,plain,
( ( identity = iPr_def_20 )
| ( sk_c9 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_2035,c_22352]) ).
tcf(c_22430,plain,
multiply(iPr_def_19,identity) = iPr_def_19,
inference(superposition,[status(thm)],[c_22352,c_4127]) ).
tcf(c_23265,plain,
inverse(iPr_def_19) = sk_c5,
inference(demodulation,[status(thm)],[c_22360,c_16448]) ).
tcf(c_23813,plain,
( ( identity = iPr_def_22 )
| ( multiply(inverse(sk_c2),iPr_def_25) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_21763,c_15389]) ).
tcf(c_24476,plain,
( ( iPr_def_15 = iPr_def_27 )
| ~ iPr_def_12
| ( sk_c9 != sk_c8 )
| ( inverse(iPr_def_22) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_22192,c_560]) ).
tcf(c_24477,plain,
( ( iPr_def_15 = iPr_def_27 )
| ~ iPr_def_14
| ( inverse(iPr_def_22) != sk_c9 )
| ( multiply(sk_c9,sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_22192,c_557]) ).
tcf(c_24478,plain,
( ( iPr_def_15 = iPr_def_27 )
| ~ iPr_def_13
| ( sk_c9 != sk_c8 )
| ( inverse(iPr_def_22) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_22192,c_558]) ).
tcf(c_24954,plain,
multiply(sk_c6,iPr_def_16) = identity,
inference(superposition,[status(thm)],[c_15569,c_96]) ).
tcf(c_24958,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_16)) != sk_c9 )
| ( multiply(sk_c6,sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_15569,c_560]) ).
tcf(c_24961,plain,
! [X0: $i] : multiply(sk_c6,multiply(iPr_def_16,X0)) = X0,
inference(superposition,[status(thm)],[c_15569,c_15389]) ).
tcf(c_24962,plain,
multiply(sk_c6,identity) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_15569,c_16448]) ).
tcf(c_25121,plain,
inverse(iPr_def_16) = sk_c6,
inference(demodulation,[status(thm)],[c_24962,c_16448]) ).
tcf(c_25596,plain,
multiply(sk_c6,identity) = sk_c6,
inference(superposition,[status(thm)],[c_1156,c_24961]) ).
tcf(c_25597,plain,
multiply(sk_c6,sk_c9) = iPr_def_17,
inference(superposition,[status(thm)],[c_6360,c_24961]) ).
tcf(c_26634,plain,
multiply(sk_c1,iPr_def_26) = identity,
inference(superposition,[status(thm)],[c_15570,c_96]) ).
tcf(c_26655,plain,
( ( identity = iPr_def_27 )
| ( sk_c9 = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_1843,c_26634]) ).
tcf(c_26656,plain,
( ( identity = iPr_def_27 )
| ( sk_c10 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_1804,c_26634]) ).
tcf(c_26657,plain,
( ( identity = iPr_def_27 )
| ( sk_c9 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_1765,c_26634]) ).
tcf(c_26658,plain,
( ( identity = iPr_def_27 )
| ( sk_c8 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1726,c_26634]) ).
tcf(c_26660,plain,
( ( identity = iPr_def_27 )
| ( sk_c9 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1638,c_26634]) ).
tcf(c_28710,plain,
( ( identity = iPr_def_27 )
| ( sk_c9 = iPr_def_27 )
| ( multiply(iPr_def_22,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_26655,c_1949]) ).
tcf(c_29014,plain,
( ( identity = iPr_def_27 )
| ( multiply(sk_c4,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_26656,c_550]) ).
tcf(c_29015,plain,
( ( identity = iPr_def_27 )
| ( identity = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_29014,c_20412]) ).
tcf(c_29084,plain,
( ( iPr_def_20 = iPr_def_22 )
| ( identity = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_26657,c_26655]) ).
tcf(c_29467,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_29084,c_29015,c_28710,c_26660,c_26658,c_26657,c_26655,c_25597,c_25596,c_25121,c_24958,c_24954,c_24478,c_24477,c_24476,c_23813,c_23265,c_22430,c_22375,c_22368,c_21232,c_20412,c_20359,c_20249,c_19059,c_19053,c_16481,c_16477,c_16476,c_16464,c_16463,c_16460,c_16475,c_16429,c_15573,c_15536,c_15503,c_15480,c_15479,c_15478,c_15477,c_15459,c_15402,c_15401,c_15400,c_11980,c_9891,c_9718,c_5977,c_3485,c_3322,c_3299,c_2879,c_2855,c_16493,c_2028,c_569,c_568,c_567,c_566,c_565,c_564,c_563,c_551,c_547,c_544]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP251-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.04/5.32 % Computer : n012.cluster.edu
% 0.04/5.32 % Model : x86_64 x86_64
% 0.04/5.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.32 % Memory : 8046.5625MB
% 0.04/5.32 % OS : Linux 6.8.0-71-generic
% 0.04/5.32 % CPULimit : 300
% 0.04/5.32 % WCLimit : 300
% 0.04/5.32 % DateTime : Wed Sep 23 14:15:45 UTC 2026
% 0.04/5.33 % CPUTime :
% 0.04/5.33 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.04/5.35 Running first-order theorem proving
% 0.04/5.35 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.04/5.35
% 0.04/5.35 % ======== iProver multi-core TPTP/SMT =========
% 0.04/5.35
% 0.04/5.35 % Detected problem language: tptp
% 0.04/5.36 % Proving...
% 7.97/6.53 % SZS status Started for theBenchmark.p
% 7.97/6.53 % SZS status Unsatisfiable for theBenchmark.p
% 7.97/6.53
% 7.97/6.53 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.97/6.53
% 7.97/6.53 % ------ iProver source info
% 7.97/6.53
% 7.97/6.53 % git: date: 2026-07-19 20:42:38 +0200
% 7.97/6.53 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.97/6.53 % git: non_committed_changes: false
% 7.97/6.53
% 7.97/6.53 % ------ Parsing...% successful
% 7.97/6.53
% 7.97/6.53
% 7.97/6.53 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 7.97/6.53
% 7.97/6.53 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 7.97/6.53
% 7.97/6.53 % ------ Preprocessing... gs_s sp: 6 0s gs_e snvd_s sp: 0 0s snvd_e %
% 7.97/6.53
% 7.97/6.53 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 7.97/6.53 % ------ Proving...
% 7.97/6.53 % ------ Problem Properties
% 7.97/6.53
% 7.97/6.53 %
% 7.97/6.53 % clauses 64
% 7.97/6.53 % conjectures 48
% 7.97/6.53 % EPR 43
% 7.97/6.53 % Horn 21
% 7.97/6.53 % unary 16
% 7.97/6.53 % binary 42
% 7.97/6.53 % lits 120
% 7.97/6.53 % lits eq 110
% 7.97/6.53 % fd_pure 0
% 7.97/6.53 % fd_pseudo 0
% 7.97/6.53 % fd_cond 0
% 7.97/6.53 % fd_pseudo_cond 0
% 7.97/6.53 % AC symbols 0
% 7.97/6.53
% 7.97/6.53 % ------ Schedule dynamic 5 is on
% 7.97/6.53
% 7.97/6.53 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 7.97/6.53
% 7.97/6.53
% 7.97/6.53 % ------
% 7.97/6.53 % Current options:
% 7.97/6.53 % ------
% 7.97/6.53
% 7.97/6.53
% 7.97/6.53 %
% 7.97/6.53
% 7.97/6.53 % ------ Proving...
% 7.97/6.53 %
% 7.97/6.53
% 7.97/6.53 % SZS status Unsatisfiable for theBenchmark.p
% 7.97/6.53
% 7.97/6.53 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.97/6.53
% 7.97/6.53
%------------------------------------------------------------------------------