%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP266-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n014.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:38 PM UTC 2026
% Result : Unsatisfiable 10.73s 2.76s
% Output : CNFRefutation 10.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 57
% Syntax : Number of formulae : 407 ( 114 unt; 14 def)
% Number of atoms : 1366 ( 779 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 646 ( 222 ~; 424 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 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 : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 117 ( 0 sgn 117 !; 0 ?; 82 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c5,sk_c11)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c5)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f11,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c9 = inverse(sk_c6)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c9,sk_c8) = sk_c10
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c10 = multiply(sk_c9,sk_c8)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( inverse(sk_c7) = sk_c9
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c9 = inverse(sk_c7)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c10 = multiply(sk_c5,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c11 = inverse(sk_c5)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f21]) ).
fof(f25,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c9 = inverse(sk_c6)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( multiply(sk_c9,sk_c8) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f28,plain,
( sk_c10 = multiply(sk_c9,sk_c8)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f30,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f29]) ).
fof(f37,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c9 = inverse(sk_c6)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( multiply(sk_c9,sk_c8) = sk_c10
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f42,plain,
( sk_c10 = multiply(sk_c9,sk_c8)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f44,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c7) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c9 = inverse(sk_c7)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f45]) ).
fof(f51,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c9,sk_c8) = sk_c10
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c10 = multiply(sk_c9,sk_c8)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f58,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( inverse(sk_c7) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c9 = inverse(sk_c7)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f59]) ).
fof(f67,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c10,sk_c4) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f68,plain,
( sk_c9 = inverse(sk_c6)
| sk_c9 = multiply(sk_c10,sk_c4) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( multiply(sk_c9,sk_c8) = sk_c10
| multiply(sk_c10,sk_c4) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f70,plain,
( sk_c10 = multiply(sk_c9,sk_c8)
| sk_c9 = multiply(sk_c10,sk_c4) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| multiply(sk_c10,sk_c4) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f72,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| sk_c9 = multiply(sk_c10,sk_c4) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c7) = sk_c9
| multiply(sk_c10,sk_c4) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f74,plain,
( sk_c9 = inverse(sk_c7)
| sk_c9 = multiply(sk_c10,sk_c4) ),
inference(reorient_equations,[],[f73]) ).
fof(f79,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| multiply(sk_c3,sk_c10) = sk_c4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_38) ).
fof(f80,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| sk_c4 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f79]) ).
fof(f81,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c3,sk_c10) = sk_c4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_39) ).
fof(f82,plain,
( sk_c9 = inverse(sk_c6)
| sk_c4 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
( multiply(sk_c9,sk_c8) = sk_c10
| multiply(sk_c3,sk_c10) = sk_c4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_40) ).
fof(f84,plain,
( sk_c10 = multiply(sk_c9,sk_c8)
| sk_c4 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| multiply(sk_c3,sk_c10) = sk_c4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f86,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| sk_c4 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( inverse(sk_c7) = sk_c9
| multiply(sk_c3,sk_c10) = sk_c4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c9 = inverse(sk_c7)
| sk_c4 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f90,plain,
( sk_c10 = multiply(sk_c5,sk_c11)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f92,plain,
( sk_c11 = inverse(sk_c5)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f91]) ).
fof(f93,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f94,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f93]) ).
fof(f95,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f96,plain,
( sk_c9 = inverse(sk_c6)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f95]) ).
fof(f97,negated_conjecture,
( multiply(sk_c9,sk_c8) = sk_c10
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f98,plain,
( sk_c10 = multiply(sk_c9,sk_c8)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f97]) ).
fof(f99,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c8
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f100,plain,
( sk_c8 = multiply(sk_c7,sk_c9)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f99]) ).
fof(f101,negated_conjecture,
( inverse(sk_c7) = sk_c9
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_49) ).
fof(f102,plain,
( sk_c9 = inverse(sk_c7)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f101]) ).
fof(f103,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( inverse(X7) != sk_c9
| multiply(X7,sk_c9) != X6
| multiply(sk_c9,X6) != sk_c10
| inverse(X5) != sk_c9
| multiply(X5,sk_c9) != sk_c10
| inverse(X4) != sk_c11
| multiply(X4,sk_c11) != sk_c10
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != X2
| multiply(sk_c10,X2) != sk_c9
| inverse(X1) != sk_c9
| multiply(X1,sk_c9) != sk_c10
| inverse(X0) != sk_c11
| multiply(X0,sk_c11) != sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_50) ).
fof(f104,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( sk_c9 != inverse(X7)
| multiply(X7,sk_c9) != X6
| sk_c10 != multiply(sk_c9,X6)
| sk_c9 != inverse(X5)
| sk_c10 != multiply(X5,sk_c9)
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c10 != inverse(X3)
| multiply(X3,sk_c10) != X2
| sk_c9 != multiply(sk_c10,X2)
| sk_c9 != inverse(X1)
| sk_c10 != multiply(X1,sk_c9)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(reorient_equations,[],[f103]) ).
fof(f105,plain,
! [X3,X0,X1,X6,X7,X4,X5] :
( sk_c9 != inverse(X7)
| multiply(X7,sk_c9) != X6
| sk_c10 != multiply(sk_c9,X6)
| sk_c9 != inverse(X5)
| sk_c10 != multiply(X5,sk_c9)
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(sk_c10,multiply(X3,sk_c10))
| sk_c9 != inverse(X1)
| sk_c10 != multiply(X1,sk_c9)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(equality_resolution,[],[f104]) ).
fof(f106,plain,
! [X3,X0,X1,X7,X4,X5] :
( sk_c9 != inverse(X7)
| sk_c10 != multiply(sk_c9,multiply(X7,sk_c9))
| sk_c9 != inverse(X5)
| sk_c10 != multiply(X5,sk_c9)
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(sk_c10,multiply(X3,sk_c10))
| sk_c9 != inverse(X1)
| sk_c10 != multiply(X1,sk_c9)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(equality_resolution,[],[f105]) ).
tcf(c_102,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_103,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_105,negated_conjecture,
( ( multiply(sk_c5,sk_c11) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_109,negated_conjecture,
( ( multiply(sk_c9,sk_c8) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_110,negated_conjecture,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_112,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_121,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c6,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_123,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_124,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_137,negated_conjecture,
( ( multiply(sk_c9,sk_c8) = sk_c10 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_138,negated_conjecture,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_142,negated_conjecture,
( ( multiply(sk_c3,sk_c10) = sk_c4 )
| ( multiply(sk_c6,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_143,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c3,sk_c10) = sk_c4 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_144,negated_conjecture,
( ( multiply(sk_c3,sk_c10) = sk_c4 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_145,negated_conjecture,
( ( multiply(sk_c3,sk_c10) = sk_c4 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c3,sk_c10) = sk_c4 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_148,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c6,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_150,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_152,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_153,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_154,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(X5) != sk_c10 )
| ( inverse(X4) != sk_c9 )
| ( inverse(X3) != sk_c9 )
| ( inverse(X2) != sk_c9 )
| ( inverse(X1) != sk_c11 )
| ( inverse(X0) != sk_c11 )
| ( multiply(X4,sk_c9) != sk_c10 )
| ( multiply(X3,sk_c9) != sk_c10 )
| ( multiply(X1,sk_c11) != sk_c10 )
| ( multiply(X0,sk_c11) != sk_c10 )
| ( multiply(sk_c9,multiply(X2,sk_c9)) != sk_c10 )
| ( multiply(sk_c10,multiply(X5,sk_c10)) != sk_c9 ) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_607,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_154]) ).
tcf(c_608,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_154]) ).
tcf(c_609,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(sk_c9,multiply(X0,sk_c9)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_154]) ).
tcf(c_610,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_154]) ).
tcf(c_611,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_154]) ).
tcf(c_612,definition,
iPr_def_14 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_613,definition,
iPr_def_15 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_614,definition,
iPr_def_16 = multiply(sk_c7,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_615,definition,
iPr_def_17 = multiply(sk_c9,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_616,definition,
iPr_def_18 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_617,definition,
iPr_def_19 = multiply(sk_c6,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_618,definition,
iPr_def_20 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_619,definition,
iPr_def_21 = multiply(sk_c5,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_620,definition,
iPr_def_22 = multiply(sk_c3,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_621,definition,
iPr_def_23 = multiply(sk_c10,sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_622,definition,
iPr_def_24 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_623,definition,
iPr_def_25 = multiply(sk_c2,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_624,definition,
iPr_def_26 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_625,definition,
iPr_def_27 = multiply(sk_c1,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_626,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_611]) ).
tcf(c_627,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_610]) ).
tcf(c_629,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(sk_c9,multiply(X0,sk_c9)) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_609]) ).
tcf(c_630,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_608]) ).
tcf(c_632,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_607]) ).
tcf(c_633,negated_conjecture,
( ( iPr_def_15 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_153,c_613,c_612]) ).
tcf(c_634,negated_conjecture,
( ( iPr_def_16 = sk_c8 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_152,c_614]) ).
tcf(c_635,negated_conjecture,
( ( iPr_def_17 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_151,c_615]) ).
tcf(c_636,negated_conjecture,
( ( iPr_def_18 = sk_c9 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_150,c_616]) ).
tcf(c_637,negated_conjecture,
( ( iPr_def_19 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_149,c_617]) ).
tcf(c_638,negated_conjecture,
( ( iPr_def_20 = sk_c11 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_148,c_618]) ).
tcf(c_639,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_147,c_619]) ).
tcf(c_640,negated_conjecture,
( ( iPr_def_22 = sk_c4 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_146,c_620]) ).
tcf(c_641,negated_conjecture,
( ( iPr_def_22 = sk_c4 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_145]) ).
tcf(c_642,negated_conjecture,
( ( iPr_def_22 = sk_c4 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_144]) ).
tcf(c_643,negated_conjecture,
( ( iPr_def_22 = sk_c4 )
| ( iPr_def_18 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_143]) ).
tcf(c_644,negated_conjecture,
( ( iPr_def_22 = sk_c4 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_647,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_139,c_621]) ).
tcf(c_648,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_138]) ).
tcf(c_649,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_650,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_18 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_654,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_132,c_622]) ).
tcf(c_655,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_656,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_657,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_18 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_658,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_128]) ).
tcf(c_661,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_125,c_623]) ).
tcf(c_662,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_663,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_664,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_18 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_665,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_669,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_670,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_671,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_18 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_115]) ).
tcf(c_673,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_674,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_675,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_111,c_625]) ).
tcf(c_676,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_677,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_678,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_18 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_680,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_681,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_682,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_683,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_993,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_633,c_636]) ).
tcf(c_1071,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c7,iPr_def_23) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_647,c_614]) ).
tcf(c_1110,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c10,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_644,c_621]) ).
tcf(c_1111,plain,
( ( sk_c9 = iPr_def_18 )
| ( multiply(sk_c10,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_643,c_621]) ).
tcf(c_1113,plain,
( ( sk_c8 = iPr_def_16 )
| ( multiply(sk_c10,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_641,c_621]) ).
tcf(c_1114,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c10,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_640,c_621]) ).
tcf(c_1135,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_647,c_623]) ).
tcf(c_1147,plain,
multiply(iPr_def_20,sk_c5) = identity,
inference(superposition,[status(thm)],[c_618,c_103]) ).
tcf(c_1148,plain,
multiply(iPr_def_18,sk_c6) = identity,
inference(superposition,[status(thm)],[c_616,c_103]) ).
tcf(c_1149,plain,
multiply(iPr_def_14,sk_c7) = identity,
inference(superposition,[status(thm)],[c_612,c_103]) ).
tcf(c_1150,plain,
multiply(iPr_def_26,sk_c1) = identity,
inference(superposition,[status(thm)],[c_624,c_103]) ).
tcf(c_1151,plain,
multiply(iPr_def_24,sk_c2) = identity,
inference(superposition,[status(thm)],[c_622,c_103]) ).
tcf(c_1152,plain,
multiply(iPr_def_15,sk_c3) = identity,
inference(superposition,[status(thm)],[c_613,c_103]) ).
tcf(c_1157,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c9,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_648,c_615]) ).
tcf(c_1297,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c2,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_654,c_623]) ).
tcf(c_1299,plain,
( ( iPr_def_23 = iPr_def_24 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_654,c_647]) ).
tcf(c_1341,plain,
( ( sk_c9 = iPr_def_24 )
| ( multiply(sk_c9,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_655,c_615]) ).
tcf(c_1427,plain,
( ( sk_c9 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_657,c_623]) ).
tcf(c_1472,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_658,c_623]) ).
tcf(c_1602,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_14,sk_c8) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_661,c_615]) ).
tcf(c_1679,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_1685,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(sk_c9,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_662,c_615]) ).
tcf(c_1746,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(sk_c2,iPr_def_18) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_664,c_623]) ).
tcf(c_1824,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c3,iPr_def_25) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_665,c_620]) ).
tcf(c_1845,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_24 )
| ( iPr_def_24 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_1934,plain,
( ( sk_c11 = iPr_def_26 )
| ( multiply(sk_c9,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_669,c_615]) ).
tcf(c_1987,plain,
( ( sk_c9 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_671,c_625]) ).
tcf(c_2065,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_673,c_625]) ).
tcf(c_2104,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_674,c_625]) ).
tcf(c_2159,plain,
( ( sk_c10 = iPr_def_27 )
| ( multiply(iPr_def_14,sk_c8) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_675,c_615]) ).
tcf(c_2209,plain,
iPr_def_14 = iPr_def_14,
inference(instantiation,[status(thm)],[c_682]) ).
tcf(c_2216,plain,
iPr_def_18 = iPr_def_18,
inference(instantiation,[status(thm)],[c_682]) ).
tcf(c_2228,plain,
iPr_def_24 = iPr_def_24,
inference(instantiation,[status(thm)],[c_682]) ).
tcf(c_2365,plain,
( ( sk_c10 = iPr_def_27 )
| ( multiply(sk_c6,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_678,c_617]) ).
tcf(c_2542,plain,
( ( sk_c10 = iPr_def_27 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_680,c_625]) ).
tcf(c_2617,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_681,c_620]) ).
tcf(c_2702,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_19 )
| ( inverse(sk_c6) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_617,c_630]) ).
tcf(c_2704,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_25 )
| ( inverse(sk_c2) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_623,c_630]) ).
tcf(c_2726,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_24 )
| ( sk_c10 != iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_2704,c_622]) ).
tcf(c_2734,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_18 )
| ( sk_c10 != iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_2702,c_616]) ).
tcf(c_2856,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_2859,plain,
! [X0: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1679]) ).
tcf(c_2862,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_18 = X0 )
| ( iPr_def_18 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_2873,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_27 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_625,c_632]) ).
tcf(c_2874,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_21 )
| ( inverse(sk_c5) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_619,c_632]) ).
tcf(c_2891,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_21 )
| ( sk_c11 != iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_2874,c_618]) ).
tcf(c_2895,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_27 )
| ( sk_c11 != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_2873,c_624]) ).
tcf(c_2976,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_24 = X0 )
| ( iPr_def_24 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_2999,plain,
( ~ iPr_def_13
| ( inverse(identity) != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_102,c_627]) ).
tcf(c_3000,plain,
( ~ iPr_def_13
| ( inverse(inverse(sk_c10)) != sk_c10 )
| ( multiply(sk_c10,identity) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_103,c_627]) ).
tcf(c_3133,plain,
( ~ iPr_def_12
| ( inverse(sk_c6) != sk_c9 )
| ( multiply(sk_c9,iPr_def_19) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_617,c_629]) ).
tcf(c_3134,plain,
( ~ iPr_def_12
| ( inverse(sk_c7) != sk_c9 )
| ( multiply(sk_c9,iPr_def_16) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_614,c_629]) ).
tcf(c_3135,plain,
( ~ iPr_def_12
| ( inverse(sk_c2) != sk_c9 )
| ( multiply(sk_c9,iPr_def_25) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_623,c_629]) ).
tcf(c_3137,plain,
( ~ iPr_def_12
| ( inverse(inverse(sk_c9)) != sk_c9 )
| ( multiply(sk_c9,identity) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_103,c_629]) ).
tcf(c_3157,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_24 )
| ( multiply(sk_c9,iPr_def_25) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_3135,c_622]) ).
tcf(c_3161,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_14 )
| ( multiply(sk_c9,iPr_def_16) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_3134,c_612]) ).
tcf(c_3165,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_18 )
| ( multiply(sk_c9,iPr_def_19) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_3133,c_616]) ).
tcf(c_3363,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c8,X0)) = multiply(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_615,c_104]) ).
tcf(c_3367,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c10,X0)) = multiply(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_620,c_104]) ).
tcf(c_3369,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_103,c_104]) ).
tcf(c_3371,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1147,c_104]) ).
tcf(c_3372,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1148,c_104]) ).
tcf(c_3373,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1149,c_104]) ).
tcf(c_3374,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1150,c_104]) ).
tcf(c_3375,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1151,c_104]) ).
tcf(c_3376,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1152,c_104]) ).
tcf(c_3382,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3376,c_102]) ).
tcf(c_3383,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3375,c_102]) ).
tcf(c_3384,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3374,c_102]) ).
tcf(c_3385,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3373,c_102]) ).
tcf(c_3386,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3372,c_102]) ).
tcf(c_3387,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3371,c_102]) ).
tcf(c_3443,plain,
multiply(iPr_def_15,sk_c3) = identity,
inference(superposition,[status(thm)],[c_613,c_103]) ).
tcf(c_3931,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_3934,plain,
( ( iPr_def_18 = iPr_def_14 )
| ( iPr_def_18 != sk_c9 )
| ( iPr_def_14 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2859]) ).
tcf(c_4973,plain,
! [X0: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_2856]) ).
tcf(c_5070,plain,
multiply(iPr_def_15,iPr_def_22) = sk_c10,
inference(superposition,[status(thm)],[c_620,c_3382]) ).
tcf(c_5077,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(iPr_def_22,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_5070,c_104]) ).
tcf(c_5079,plain,
multiply(iPr_def_24,iPr_def_25) = sk_c9,
inference(superposition,[status(thm)],[c_623,c_3383]) ).
tcf(c_5082,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(iPr_def_25,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_5079,c_104]) ).
tcf(c_5084,plain,
multiply(iPr_def_26,iPr_def_27) = sk_c11,
inference(superposition,[status(thm)],[c_625,c_3384]) ).
tcf(c_5094,plain,
! [X0: $i] :
( ( iPr_def_18 = X0 )
| ( iPr_def_18 != iPr_def_18 )
| ( X0 != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_2862]) ).
tcf(c_5098,plain,
multiply(iPr_def_14,iPr_def_16) = sk_c9,
inference(superposition,[status(thm)],[c_614,c_3385]) ).
tcf(c_5131,plain,
! [X0: $i] :
( ( iPr_def_24 = X0 )
| ( iPr_def_24 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_2976]) ).
tcf(c_5324,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_14,iPr_def_16) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1071,c_3385]) ).
tcf(c_5325,plain,
( ( sk_c9 = iPr_def_23 )
| ( sk_c9 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_5324,c_5098]) ).
tcf(c_5425,plain,
multiply(iPr_def_18,iPr_def_19) = sk_c9,
inference(superposition,[status(thm)],[c_617,c_3386]) ).
tcf(c_5439,plain,
multiply(iPr_def_20,iPr_def_21) = sk_c11,
inference(superposition,[status(thm)],[c_619,c_3387]) ).
tcf(c_6553,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( sk_c9 = iPr_def_18 )
| ( multiply(iPr_def_15,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_993,c_1111]) ).
tcf(c_6572,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( sk_c9 = iPr_def_18 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_6553,c_5070]) ).
tcf(c_6814,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_15,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_993,c_1114]) ).
tcf(c_6827,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_6814,c_5070]) ).
tcf(c_7815,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1297,c_3383]) ).
tcf(c_7816,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c9 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_7815,c_5079]) ).
tcf(c_8055,plain,
( ( sk_c9 = iPr_def_18 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1427,c_3383]) ).
tcf(c_8056,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c9 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_8055,c_5079]) ).
tcf(c_8153,plain,
! [X0: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2856]) ).
tcf(c_8299,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1472,c_3383]) ).
tcf(c_8300,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c10 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_8299,c_5079]) ).
tcf(c_8764,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_14,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_662,c_1602]) ).
tcf(c_8769,plain,
( ( sk_c9 = iPr_def_17 )
| ( sk_c10 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_8764,c_5098]) ).
tcf(c_9010,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_3931]) ).
tcf(c_9011,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != iPr_def_14 )
| ( sk_c10 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_9010]) ).
tcf(c_9389,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_1746,c_3383]) ).
tcf(c_9390,plain,
( ( sk_c9 = iPr_def_18 )
| ( sk_c10 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_9389,c_5079]) ).
tcf(c_9661,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(iPr_def_15,iPr_def_22) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1824,c_3382]) ).
tcf(c_9662,plain,
( ( sk_c10 = iPr_def_25 )
| ( sk_c10 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_9661,c_5070]) ).
tcf(c_10140,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2065,c_3384]) ).
tcf(c_10141,plain,
( ( sk_c11 = iPr_def_26 )
| ( sk_c11 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_10140,c_5084]) ).
tcf(c_10162,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2104,c_3384]) ).
tcf(c_10163,plain,
( ( sk_c10 = iPr_def_21 )
| ( sk_c11 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_10162,c_5084]) ).
tcf(c_10365,plain,
( ( sk_c10 = iPr_def_27 )
| ( multiply(iPr_def_14,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_676,c_2159]) ).
tcf(c_10372,plain,
( ( sk_c9 = iPr_def_17 )
| ( sk_c10 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_10365,c_5098]) ).
tcf(c_11139,plain,
( ( sk_c10 = iPr_def_27 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_2542,c_3384]) ).
tcf(c_11140,plain,
( ( sk_c10 = iPr_def_27 )
| ( sk_c11 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_11139,c_5084]) ).
tcf(c_11186,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(iPr_def_15,iPr_def_22) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2617,c_3382]) ).
tcf(c_11187,plain,
( ( sk_c10 = iPr_def_27 )
| ( sk_c10 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_11186,c_5070]) ).
tcf(c_12443,plain,
multiply(sk_c3,iPr_def_23) = multiply(iPr_def_22,sk_c4),
inference(superposition,[status(thm)],[c_621,c_3367]) ).
tcf(c_12654,plain,
multiply(iPr_def_15,multiply(iPr_def_22,sk_c4)) = iPr_def_23,
inference(superposition,[status(thm)],[c_12443,c_3382]) ).
tcf(c_14100,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_3369,c_102]) ).
tcf(c_14110,plain,
multiply(inverse(sk_c9),iPr_def_17) = sk_c8,
inference(superposition,[status(thm)],[c_615,c_14100]) ).
tcf(c_14112,plain,
multiply(inverse(sk_c2),iPr_def_25) = sk_c9,
inference(superposition,[status(thm)],[c_623,c_14100]) ).
tcf(c_14113,plain,
multiply(inverse(sk_c10),iPr_def_23) = sk_c4,
inference(superposition,[status(thm)],[c_621,c_14100]) ).
tcf(c_14115,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_102,c_14100]) ).
tcf(c_14116,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_103,c_14100]) ).
tcf(c_14197,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(inverse(sk_c2),iPr_def_25) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1135,c_14100]) ).
tcf(c_14294,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_3387,c_14100]) ).
tcf(c_14295,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_3386,c_14100]) ).
tcf(c_14296,plain,
! [X0: $i] : multiply(inverse(iPr_def_14),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_3385,c_14100]) ).
tcf(c_14297,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_3384,c_14100]) ).
tcf(c_14298,plain,
! [X0: $i] : multiply(inverse(iPr_def_24),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_3383,c_14100]) ).
tcf(c_14299,plain,
! [X0: $i] : multiply(inverse(iPr_def_15),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_3382,c_14100]) ).
tcf(c_14365,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_14100,c_14100]) ).
tcf(c_15733,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_14116,c_14365]) ).
tcf(c_15751,plain,
multiply(sk_c9,sk_c8) = multiply(iPr_def_17,identity),
inference(superposition,[status(thm)],[c_15733,c_3363]) ).
tcf(c_15753,plain,
multiply(sk_c9,identity) = multiply(iPr_def_24,iPr_def_25),
inference(superposition,[status(thm)],[c_15733,c_5082]) ).
tcf(c_15755,plain,
multiply(sk_c10,identity) = multiply(iPr_def_15,iPr_def_22),
inference(superposition,[status(thm)],[c_15733,c_5077]) ).
tcf(c_15763,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_15733,c_14115]) ).
tcf(c_15765,plain,
multiply(sk_c10,identity) = sk_c10,
inference(light_normalisation,[status(thm)],[c_15755,c_5070]) ).
tcf(c_15767,plain,
multiply(sk_c9,identity) = sk_c9,
inference(light_normalisation,[status(thm)],[c_15753,c_5079]) ).
tcf(c_15769,plain,
multiply(iPr_def_17,identity) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_15751,c_615]) ).
tcf(c_15781,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_2726,c_2734,c_2726,c_9390,c_9662]) ).
tcf(c_15783,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_15781,c_2734,c_8056,c_8300,c_15781]) ).
tcf(c_15785,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_626,c_15783]) ).
tcf(c_16566,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_21 ) ),
inference(global_subsumption_just,[status(thm)],[c_2891,c_2895,c_2891,c_10141,c_11140]) ).
tcf(c_16568,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_16566,c_2895,c_10163,c_11187,c_16566]) ).
tcf(c_16570,plain,
( iPr_def_13
| iPr_def_12 ),
inference(backward_subsumption_resolution,[status(thm)],[c_15785,c_16568]) ).
tcf(c_18410,plain,
multiply(sk_c5,iPr_def_20) = identity,
inference(superposition,[status(thm)],[c_14294,c_103]) ).
tcf(c_18415,plain,
! [X0: $i] : multiply(sk_c5,multiply(iPr_def_20,X0)) = X0,
inference(superposition,[status(thm)],[c_14294,c_14100]) ).
tcf(c_19205,plain,
multiply(sk_c5,sk_c11) = iPr_def_21,
inference(superposition,[status(thm)],[c_5439,c_18415]) ).
tcf(c_19666,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( iPr_def_18 != iPr_def_14 )
| ( iPr_def_14 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_4973]) ).
tcf(c_19667,plain,
( ( iPr_def_14 = sk_c9 )
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c9 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_4973]) ).
tcf(c_19695,plain,
multiply(sk_c6,iPr_def_18) = identity,
inference(superposition,[status(thm)],[c_14295,c_103]) ).
tcf(c_19701,plain,
multiply(sk_c6,identity) = inverse(iPr_def_18),
inference(superposition,[status(thm)],[c_14295,c_15733]) ).
tcf(c_19710,plain,
( ( identity = iPr_def_19 )
| ( sk_c10 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_2365,c_19695]) ).
tcf(c_19923,plain,
( ( identity = iPr_def_19 )
| ( multiply(iPr_def_27,sk_c4) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_19710,c_621]) ).
tcf(c_20021,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_3443,c_104]) ).
tcf(c_20027,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_20021,c_102]) ).
tcf(c_20243,plain,
inverse(iPr_def_18) = sk_c6,
inference(demodulation,[status(thm)],[c_19701,c_15733]) ).
tcf(c_20773,plain,
multiply(sk_c7,identity) = inverse(iPr_def_14),
inference(superposition,[status(thm)],[c_14296,c_15733]) ).
tcf(c_21370,plain,
inverse(iPr_def_14) = sk_c7,
inference(demodulation,[status(thm)],[c_20773,c_15733]) ).
tcf(c_23637,plain,
multiply(sk_c1,iPr_def_26) = identity,
inference(superposition,[status(thm)],[c_14297,c_103]) ).
tcf(c_23642,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_26,X0)) = X0,
inference(superposition,[status(thm)],[c_14297,c_14100]) ).
tcf(c_23653,plain,
( ( identity = iPr_def_27 )
| ( sk_c9 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_1987,c_23637]) ).
tcf(c_24342,plain,
( ( identity = iPr_def_27 )
| ( multiply(sk_c6,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_23653,c_617]) ).
tcf(c_24351,plain,
( ( identity = iPr_def_27 )
| ( identity = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_24342,c_19695]) ).
tcf(c_24444,plain,
multiply(sk_c1,sk_c11) = iPr_def_27,
inference(superposition,[status(thm)],[c_5084,c_23642]) ).
tcf(c_25038,plain,
( ( iPr_def_24 = iPr_def_23 )
| ( iPr_def_24 != iPr_def_24 )
| ( iPr_def_23 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_5131]) ).
tcf(c_25250,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_23 != sk_c9 )
| ( iPr_def_14 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_8153]) ).
tcf(c_25282,plain,
( ( iPr_def_18 = sk_c9 )
| ( iPr_def_18 != iPr_def_18 )
| ( sk_c9 != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_5094]) ).
tcf(c_25550,plain,
! [X0: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1679]) ).
tcf(c_25551,plain,
( ( sk_c10 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_23 )
| ( sk_c10 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_25550]) ).
tcf(c_25576,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_3931]) ).
tcf(c_25577,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != iPr_def_24 )
| ( sk_c10 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_25576]) ).
tcf(c_25808,plain,
! [X0: $i] :
( ( identity = iPr_def_19 )
| ( multiply(iPr_def_27,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_24351,c_102]) ).
tcf(c_26747,plain,
multiply(sk_c2,iPr_def_24) = identity,
inference(superposition,[status(thm)],[c_14298,c_103]) ).
tcf(c_26752,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_24,X0)) = X0,
inference(superposition,[status(thm)],[c_14298,c_14100]) ).
tcf(c_26753,plain,
multiply(sk_c2,identity) = inverse(iPr_def_24),
inference(superposition,[status(thm)],[c_14298,c_15733]) ).
tcf(c_26776,plain,
( ( identity = iPr_def_25 )
| ( sk_c9 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_1427,c_26747]) ).
tcf(c_26778,plain,
( ( identity = iPr_def_25 )
| ( sk_c9 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1297,c_26747]) ).
tcf(c_26845,plain,
inverse(iPr_def_24) = sk_c2,
inference(demodulation,[status(thm)],[c_26753,c_15733]) ).
tcf(c_26867,plain,
multiply(sk_c2,identity) = sk_c2,
inference(superposition,[status(thm)],[c_1151,c_26752]) ).
tcf(c_28286,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( identity = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_26778,c_26776]) ).
tcf(c_28927,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( inverse(iPr_def_25) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_28286,c_15763]) ).
tcf(c_28947,plain,
multiply(sk_c3,iPr_def_15) = identity,
inference(superposition,[status(thm)],[c_14299,c_103]) ).
tcf(c_28952,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_15,X0)) = X0,
inference(superposition,[status(thm)],[c_14299,c_14100]) ).
tcf(c_28953,plain,
multiply(sk_c3,identity) = inverse(iPr_def_15),
inference(superposition,[status(thm)],[c_14299,c_15733]) ).
tcf(c_29008,plain,
multiply(iPr_def_15,identity) = iPr_def_15,
inference(superposition,[status(thm)],[c_28947,c_3382]) ).
tcf(c_29275,plain,
multiply(iPr_def_15,iPr_def_22) = sk_c10,
inference(superposition,[status(thm)],[c_620,c_20027]) ).
tcf(c_29630,plain,
inverse(iPr_def_15) = sk_c3,
inference(demodulation,[status(thm)],[c_28953,c_15733]) ).
tcf(c_29634,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm)],[c_1152,c_28952]) ).
tcf(c_29643,plain,
multiply(sk_c3,sk_c10) = iPr_def_22,
inference(superposition,[status(thm)],[c_5070,c_28952]) ).
tcf(c_37151,plain,
( ( identity = iPr_def_19 )
| ( sk_c4 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_25808,c_19923]) ).
tcf(c_39093,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( identity = iPr_def_19 )
| ( sk_c9 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_37151,c_643]) ).
tcf(c_39793,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( identity = iPr_def_19 )
| ( multiply(sk_c6,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_39093,c_617]) ).
tcf(c_39804,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( identity = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_39793,c_19695]) ).
tcf(c_42167,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_633,c_636]) ).
tcf(c_42485,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( multiply(iPr_def_15,sk_c4) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_42167,c_621]) ).
tcf(c_42571,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_15,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_640,c_42485]) ).
tcf(c_42572,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_42571,c_29275]) ).
tcf(c_49552,plain,
! [X0: $i] :
( ( X0 = iPr_def_24 )
| ( iPr_def_24 != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1845]) ).
tcf(c_49553,plain,
( ( sk_c10 = iPr_def_24 )
| ( iPr_def_24 != iPr_def_23 )
| ( sk_c10 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_49552]) ).
tcf(c_51993,plain,
( ~ iPr_def_13
| ( sk_c10 != identity )
| ( multiply(sk_c10,sk_c10) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_2999,c_15763]) ).
tcf(c_53339,plain,
( ~ iPr_def_13
| ( sk_c10 != sk_c9 )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_3000,c_15733]) ).
tcf(c_53391,plain,
( ( iPr_def_14 = iPr_def_18 )
| ~ iPr_def_13
| ( sk_c10 != sk_c9 )
| ( inverse(inverse(iPr_def_15)) != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_993,c_53339]) ).
tcf(c_53437,plain,
( ( iPr_def_14 = iPr_def_18 )
| ~ iPr_def_13
| ( sk_c10 != sk_c9 ) ),
inference(ground_joinability,[status(thm)],[c_53391,c_613,c_29630]) ).
tcf(c_53678,plain,
( ~ iPr_def_12
| ( sk_c10 != sk_c9 )
| ( inverse(inverse(sk_c9)) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_3137,c_15733]) ).
tcf(c_53723,plain,
( ( sk_c9 = iPr_def_18 )
| ~ iPr_def_12
| ( sk_c10 != sk_c9 )
| ( inverse(inverse(iPr_def_24)) != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_657,c_53678]) ).
tcf(c_53725,plain,
( ( sk_c9 = iPr_def_14 )
| ~ iPr_def_12
| ( sk_c10 != sk_c9 )
| ( inverse(inverse(iPr_def_24)) != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_654,c_53678]) ).
tcf(c_53757,plain,
( ( sk_c9 = iPr_def_14 )
| ~ iPr_def_12
| ( sk_c10 != sk_c9 ) ),
inference(ground_joinability,[status(thm)],[c_53725,c_622,c_26845]) ).
tcf(c_53765,plain,
( ( sk_c9 = iPr_def_18 )
| ~ iPr_def_12
| ( sk_c10 != sk_c9 ) ),
inference(ground_joinability,[status(thm)],[c_53723,c_622,c_26845]) ).
tcf(c_54814,plain,
( ( iPr_def_14 = iPr_def_18 )
| ( sk_c9 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_42572,c_1299,c_2228,c_6827,c_7816,c_16570,c_25038,c_25577,c_49553,c_53437,c_53757]) ).
tcf(c_54816,plain,
iPr_def_14 = iPr_def_18,
inference(global_subsumption_just,[status(thm)],[c_54814,c_650,c_2209,c_2216,c_3934,c_6572,c_9011,c_16570,c_19666,c_19667,c_25250,c_25282,c_25551,c_53437,c_53765,c_54814]) ).
tcf(c_56575,plain,
iPr_def_14 = iPr_def_18,
inference(global_subsumption_just,[status(thm)],[c_28927,c_54816]) ).
tcf(c_56601,plain,
inverse(iPr_def_14) = sk_c6,
inference(demodulation,[status(thm)],[c_20243,c_56575]) ).
tcf(c_56655,plain,
multiply(iPr_def_14,iPr_def_19) = sk_c9,
inference(demodulation,[status(thm)],[c_5425,c_56575]) ).
tcf(c_56675,plain,
sk_c6 = sk_c7,
inference(demodulation,[status(thm)],[c_21370,c_56601]) ).
tcf(c_56694,plain,
multiply(sk_c6,sk_c9) = iPr_def_16,
inference(demodulation,[status(thm)],[c_614,c_56675]) ).
tcf(c_56697,plain,
iPr_def_16 = iPr_def_19,
inference(demodulation,[status(thm)],[c_617,c_56694]) ).
tcf(c_56829,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(sk_c10,iPr_def_22) = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_1110,c_56697]) ).
tcf(c_60288,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_56829,c_56697,c_56655,c_56575,c_53757,c_53339,c_51993,c_39804,c_29643,c_29634,c_29630,c_29008,c_28947,c_26867,c_26845,c_24444,c_23637,c_19205,c_18410,c_16570,c_15769,c_15767,c_15765,c_15755,c_15753,c_15751,c_14197,c_14113,c_14112,c_14110,c_12654,c_12443,c_10372,c_8769,c_5325,c_3165,c_3161,c_3157,c_1934,c_1685,c_1341,c_1157,c_1114,c_1113,c_678,c_677,c_676,c_670,c_663,c_656,c_649,c_642,c_639,c_638,c_637,c_636,c_635,c_634,c_622,c_613]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP266-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n014.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 14:18:33 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 10.73/2.76 % SZS status Started for theBenchmark.p
% 10.73/2.76 % SZS status Unsatisfiable for theBenchmark.p
% 10.73/2.76
% 10.73/2.76 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.73/2.76
% 10.73/2.76 % ------ iProver source info
% 10.73/2.76
% 10.73/2.76 % git: date: 2026-07-19 20:42:38 +0200
% 10.73/2.76 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.73/2.76 % git: non_committed_changes: false
% 10.73/2.76
% 10.73/2.76 % ------ Parsing...% successful
% 10.73/2.76
% 10.73/2.76
% 10.73/2.76 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 10.73/2.76
% 10.73/2.76 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 10.73/2.76
% 10.73/2.76 % ------ Preprocessing... gs_s sp: 6 0s gs_e snvd_s sp: 0 0s snvd_e %
% 10.73/2.76
% 10.73/2.76 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 10.73/2.76 % ------ Proving...
% 10.73/2.76 % ------ Problem Properties
% 10.73/2.76
% 10.73/2.76 %
% 10.73/2.76 % clauses 71
% 10.73/2.76 % conjectures 54
% 10.73/2.76 % EPR 50
% 10.73/2.76 % Horn 21
% 10.73/2.76 % unary 17
% 10.73/2.76 % binary 49
% 10.73/2.76 % lits 131
% 10.73/2.76 % lits eq 123
% 10.73/2.76 % fd_pure 0
% 10.73/2.76 % fd_pseudo 0
% 10.73/2.76 % fd_cond 0
% 10.73/2.76 % fd_pseudo_cond 0
% 10.73/2.76 % AC symbols 0
% 10.73/2.76
% 10.73/2.76 % ------ Schedule dynamic 5 is on
% 10.73/2.76
% 10.73/2.76 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 10.73/2.76
% 10.73/2.76
% 10.73/2.76 % ------
% 10.73/2.76 % Current options:
% 10.73/2.76 % ------
% 10.73/2.76
% 10.73/2.76
% 10.73/2.76 %
% 10.73/2.76
% 10.73/2.76 % ------ Proving...
% 10.73/2.76 %
% 10.73/2.76
% 10.73/2.76 % SZS status Unsatisfiable for theBenchmark.p
% 10.73/2.76
% 10.73/2.76 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.73/2.77
% 10.73/2.77
%------------------------------------------------------------------------------