%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP282-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 : n017.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:43 PM UTC 2026
% Result : Unsatisfiable 54.55s 10.53s
% Output : CNFRefutation 54.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 52
% Syntax : Number of formulae : 446 ( 143 unt; 14 def)
% Number of atoms : 1577 ( 829 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 609 ( 184 ~; 425 |; 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 : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 106 ( 0 sgn 106 !; 0 ?; 79 :)
% 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_c8,sk_c9) = sk_c7
| multiply(sk_c9,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c7 = multiply(sk_c8,sk_c9)
| multiply(sk_c9,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c9
| multiply(sk_c9,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c9 = multiply(sk_c8,sk_c7)
| multiply(sk_c9,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( inverse(sk_c9) = sk_c7
| multiply(sk_c9,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c7 = inverse(sk_c9)
| multiply(sk_c9,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( inverse(sk_c4) = sk_c9
| multiply(sk_c9,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c9 = inverse(sk_c4)
| multiply(sk_c9,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c9
| multiply(sk_c9,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c9 = multiply(sk_c4,sk_c7)
| multiply(sk_c9,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c9,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c7 = multiply(sk_c5,sk_c6)
| multiply(sk_c9,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( inverse(sk_c5) = sk_c6
| multiply(sk_c9,sk_c8) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c6 = inverse(sk_c5)
| multiply(sk_c9,sk_c8) = sk_c7 ),
inference(reorient_equations,[],[f17]) ).
fof(f23,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c9 = multiply(sk_c8,sk_c7)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c9) = sk_c7
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c7 = inverse(sk_c9)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( inverse(sk_c4) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f28,plain,
( sk_c9 = inverse(sk_c4)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f30,plain,
( sk_c9 = multiply(sk_c4,sk_c7)
| sk_c8 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f29]) ).
fof(f39,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c9 = multiply(sk_c8,sk_c7)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( inverse(sk_c9) = sk_c7
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f42,plain,
( sk_c7 = inverse(sk_c9)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( inverse(sk_c4) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f44,plain,
( sk_c9 = inverse(sk_c4)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c9 = multiply(sk_c4,sk_c7)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f45]) ).
fof(f53,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c7
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c7 = multiply(sk_c8,sk_c9)
| sk_c8 = multiply(sk_c9,sk_c3) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c9 = multiply(sk_c8,sk_c7)
| sk_c8 = multiply(sk_c9,sk_c3) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( inverse(sk_c9) = sk_c7
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f58,plain,
( sk_c7 = inverse(sk_c9)
| sk_c8 = multiply(sk_c9,sk_c3) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( inverse(sk_c4) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c9 = inverse(sk_c4)
| sk_c8 = multiply(sk_c9,sk_c3) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c9
| multiply(sk_c9,sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c9 = multiply(sk_c4,sk_c7)
| sk_c8 = multiply(sk_c9,sk_c3) ),
inference(reorient_equations,[],[f61]) ).
fof(f71,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f72,plain,
( sk_c9 = multiply(sk_c8,sk_c7)
| sk_c3 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c9) = sk_c7
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f74,plain,
( sk_c7 = inverse(sk_c9)
| sk_c3 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( inverse(sk_c4) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c9 = inverse(sk_c4)
| sk_c3 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
( sk_c9 = multiply(sk_c4,sk_c7)
| sk_c3 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f77]) ).
fof(f85,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c7
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f86,plain,
( sk_c7 = multiply(sk_c8,sk_c9)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c8,sk_c7) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c9 = multiply(sk_c8,sk_c7)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( inverse(sk_c9) = sk_c7
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f90,plain,
( sk_c7 = inverse(sk_c9)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,negated_conjecture,
( inverse(sk_c4) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f92,plain,
( sk_c9 = inverse(sk_c4)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f91]) ).
fof(f93,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c9
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f94,plain,
( sk_c9 = multiply(sk_c4,sk_c7)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f93]) ).
fof(f95,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f96,plain,
( sk_c7 = multiply(sk_c5,sk_c6)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f95]) ).
fof(f97,negated_conjecture,
( inverse(sk_c5) = sk_c6
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f98,plain,
( sk_c6 = inverse(sk_c5)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f97]) ).
fof(f99,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c7
| inverse(sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f100,plain,
( sk_c7 = multiply(sk_c6,sk_c9)
| sk_c9 = inverse(sk_c2) ),
inference(reorient_equations,[],[f99]) ).
fof(f101,negated_conjecture,
! [X2,X3,X0,X1,X4,X5] :
( multiply(X5,sk_c9) != sk_c7
| inverse(X4) != X5
| multiply(X4,X5) != sk_c7
| multiply(X3,sk_c7) != sk_c9
| inverse(X3) != sk_c9
| inverse(sk_c9) != sk_c7
| multiply(sk_c8,sk_c7) != sk_c9
| multiply(sk_c8,sk_c9) != sk_c7
| inverse(X2) != sk_c9
| multiply(X2,sk_c9) != X1
| multiply(sk_c9,X1) != sk_c8
| inverse(X0) != sk_c9
| multiply(X0,sk_c9) != sk_c8
| multiply(sk_c9,sk_c8) != sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_49) ).
fof(f102,plain,
! [X2,X3,X0,X1,X4,X5] :
( sk_c7 != multiply(X5,sk_c9)
| inverse(X4) != X5
| sk_c7 != multiply(X4,X5)
| sk_c9 != multiply(X3,sk_c7)
| sk_c9 != inverse(X3)
| sk_c7 != inverse(sk_c9)
| sk_c9 != multiply(sk_c8,sk_c7)
| sk_c7 != multiply(sk_c8,sk_c9)
| sk_c9 != inverse(X2)
| multiply(X2,sk_c9) != X1
| sk_c8 != multiply(sk_c9,X1)
| inverse(X0) != sk_c9
| sk_c8 != multiply(X0,sk_c9)
| multiply(sk_c9,sk_c8) != sk_c7 ),
inference(reorient_equations,[],[f101]) ).
fof(f103,plain,
! [X2,X3,X0,X4,X5] :
( sk_c7 != multiply(X5,sk_c9)
| inverse(X4) != X5
| sk_c7 != multiply(X4,X5)
| sk_c9 != multiply(X3,sk_c7)
| sk_c9 != inverse(X3)
| sk_c7 != inverse(sk_c9)
| sk_c9 != multiply(sk_c8,sk_c7)
| sk_c7 != multiply(sk_c8,sk_c9)
| sk_c9 != inverse(X2)
| sk_c8 != multiply(sk_c9,multiply(X2,sk_c9))
| inverse(X0) != sk_c9
| sk_c8 != multiply(X0,sk_c9)
| multiply(sk_c9,sk_c8) != sk_c7 ),
inference(equality_resolution,[],[f102]) ).
fof(f104,plain,
! [X2,X3,X0,X4] :
( sk_c7 != multiply(inverse(X4),sk_c9)
| sk_c7 != multiply(X4,inverse(X4))
| sk_c9 != multiply(X3,sk_c7)
| sk_c9 != inverse(X3)
| sk_c7 != inverse(sk_c9)
| sk_c9 != multiply(sk_c8,sk_c7)
| sk_c7 != multiply(sk_c8,sk_c9)
| sk_c9 != inverse(X2)
| sk_c8 != multiply(sk_c9,multiply(X2,sk_c9))
| inverse(X0) != sk_c9
| sk_c8 != multiply(X0,sk_c9)
| multiply(sk_c9,sk_c8) != sk_c7 ),
inference(equality_resolution,[],[f103]) ).
tcf(c_101,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_102,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_104,negated_conjecture,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( multiply(sk_c9,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_105,negated_conjecture,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( multiply(sk_c9,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c9) = sk_c7 )
| ( multiply(sk_c9,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c9,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_108,negated_conjecture,
( ( multiply(sk_c4,sk_c7) = sk_c9 )
| ( multiply(sk_c9,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_109,negated_conjecture,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c9,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c5) = sk_c6 )
| ( multiply(sk_c9,sk_c8) = sk_c7 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_113,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c9) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_116,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c4,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_128,negated_conjecture,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( multiply(sk_c9,sk_c3) = sk_c8 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_129,negated_conjecture,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( multiply(sk_c9,sk_c3) = sk_c8 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c9) = sk_c7 )
| ( multiply(sk_c9,sk_c3) = sk_c8 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c9,sk_c3) = sk_c8 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_132,negated_conjecture,
( ( multiply(sk_c4,sk_c7) = sk_c9 )
| ( multiply(sk_c9,sk_c3) = sk_c8 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_137,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c3 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c9) = sk_c7 )
| ( multiply(sk_c2,sk_c9) = sk_c3 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c4) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c3 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_140,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c3 )
| ( multiply(sk_c4,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_145,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_148,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c4,sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_150,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_152,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(sk_c9) != sk_c7 )
| ( inverse(X2) != sk_c9 )
| ( inverse(X1) != sk_c9 )
| ( inverse(X0) != sk_c9 )
| ( multiply(sk_c8,sk_c7) != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c7 )
| ( multiply(sk_c9,sk_c8) != sk_c7 )
| ( multiply(X1,sk_c7) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 )
| ( multiply(inverse(X3),sk_c9) != sk_c7 )
| ( multiply(X3,inverse(X3)) != sk_c7 )
| ( multiply(sk_c9,multiply(X2,sk_c9)) != sk_c8 ) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_597,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_152]) ).
tcf(c_598,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c9) != sk_c7 )
| ( multiply(X0,inverse(X0)) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_152]) ).
tcf(c_599,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c7) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_152]) ).
tcf(c_600,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c9 )
| ( multiply(sk_c9,multiply(X0,sk_c9)) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_152]) ).
tcf(c_601,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c9) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c7 )
| ( multiply(sk_c9,sk_c8) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_152]) ).
tcf(c_602,definition,
iPr_def_14 = multiply(sk_c9,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_603,definition,
iPr_def_15 = multiply(sk_c8,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_604,definition,
iPr_def_16 = multiply(sk_c8,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_605,definition,
iPr_def_17 = inverse(sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_606,definition,
iPr_def_18 = multiply(sk_c6,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_607,definition,
iPr_def_19 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_608,definition,
iPr_def_20 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_609,definition,
iPr_def_21 = multiply(sk_c5,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_610,definition,
iPr_def_22 = multiply(sk_c4,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_611,definition,
iPr_def_23 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_612,definition,
iPr_def_24 = multiply(sk_c2,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_613,definition,
iPr_def_25 = multiply(sk_c9,sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_614,definition,
iPr_def_26 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_615,definition,
iPr_def_27 = multiply(sk_c1,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_616,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_17 != sk_c7 )
| ( iPr_def_16 != sk_c9 )
| ( iPr_def_15 != sk_c7 )
| ( iPr_def_14 != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_601,c_605,c_604,c_603,c_602]) ).
tcf(c_617,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c9 )
| ( multiply(sk_c9,multiply(X0,sk_c9)) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_600]) ).
tcf(c_618,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c7) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_599]) ).
tcf(c_619,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c9) != sk_c7 )
| ( multiply(X0,inverse(X0)) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_598]) ).
tcf(c_620,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_597]) ).
tcf(c_621,negated_conjecture,
( ( iPr_def_19 = sk_c9 )
| ( iPr_def_18 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_151,c_607,c_606]) ).
tcf(c_622,negated_conjecture,
( ( iPr_def_20 = sk_c6 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_150,c_608]) ).
tcf(c_623,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_149,c_609]) ).
tcf(c_624,negated_conjecture,
( ( iPr_def_22 = sk_c9 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_148,c_610]) ).
tcf(c_625,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_147,c_611]) ).
tcf(c_626,negated_conjecture,
( ( iPr_def_19 = sk_c9 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_146]) ).
tcf(c_627,negated_conjecture,
( ( iPr_def_19 = sk_c9 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_145]) ).
tcf(c_628,negated_conjecture,
( ( iPr_def_19 = sk_c9 )
| ( iPr_def_15 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_144]) ).
tcf(c_632,negated_conjecture,
( ( iPr_def_24 = sk_c3 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_140]) ).
tcf(c_633,negated_conjecture,
( ( iPr_def_24 = sk_c3 )
| ( iPr_def_23 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_139]) ).
tcf(c_634,negated_conjecture,
( ( iPr_def_24 = sk_c3 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_138]) ).
tcf(c_635,negated_conjecture,
( ( iPr_def_24 = sk_c3 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_640,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_132]) ).
tcf(c_641,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_23 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_642,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_643,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_644,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_15 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_128]) ).
tcf(c_648,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_649,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_23 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_650,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_651,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_656,negated_conjecture,
( ( iPr_def_27 = sk_c8 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_657,negated_conjecture,
( ( iPr_def_27 = sk_c8 )
| ( iPr_def_23 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_115]) ).
tcf(c_658,negated_conjecture,
( ( iPr_def_27 = sk_c8 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_659,negated_conjecture,
( ( iPr_def_27 = sk_c8 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_662,negated_conjecture,
( ( iPr_def_20 = sk_c6 )
| ( iPr_def_14 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_663,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_14 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_664,negated_conjecture,
( ( iPr_def_22 = sk_c9 )
| ( iPr_def_14 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_665,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_14 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_666,negated_conjecture,
( ( iPr_def_17 = sk_c7 )
| ( iPr_def_14 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_667,negated_conjecture,
( ( iPr_def_16 = sk_c9 )
| ( iPr_def_14 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_668,negated_conjecture,
( ( iPr_def_15 = sk_c7 )
| ( iPr_def_14 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_104]) ).
tcf(c_669,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_670,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_675,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_669]) ).
tcf(c_1032,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_19,sk_c8) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_627,c_602]) ).
tcf(c_1139,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_19,sk_c3) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_627,c_613]) ).
tcf(c_1144,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c9,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_634,c_613]) ).
tcf(c_1145,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c9,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_633,c_613]) ).
tcf(c_1146,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(sk_c9,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_632,c_613]) ).
tcf(c_1172,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_19) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_627,c_615]) ).
tcf(c_1181,plain,
multiply(iPr_def_17,sk_c9) = identity,
inference(superposition,[status(thm)],[c_605,c_102]) ).
tcf(c_1182,plain,
multiply(iPr_def_23,sk_c4) = identity,
inference(superposition,[status(thm)],[c_611,c_102]) ).
tcf(c_1183,plain,
multiply(iPr_def_20,sk_c5) = identity,
inference(superposition,[status(thm)],[c_608,c_102]) ).
tcf(c_1184,plain,
multiply(iPr_def_26,sk_c1) = identity,
inference(superposition,[status(thm)],[c_614,c_102]) ).
tcf(c_1185,plain,
multiply(iPr_def_19,sk_c2) = identity,
inference(superposition,[status(thm)],[c_607,c_102]) ).
tcf(c_1221,plain,
! [X0: $i,X1: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_1235,plain,
! [X0: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != sk_c7 )
| ( X0 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1221]) ).
tcf(c_1236,plain,
sk_c7 = sk_c7,
inference(instantiation,[status(thm)],[c_669]) ).
tcf(c_1243,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_25,sk_c7) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_640,c_604]) ).
tcf(c_1257,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c7 )
| ( sk_c7 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_1259,plain,
( ( sk_c7 = iPr_def_15 )
| ( iPr_def_15 != sk_c7 )
| ( sk_c7 != sk_c7 ) ),
inference(instantiation,[status(thm)],[c_1235]) ).
tcf(c_1268,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_25,sk_c7) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_641,c_604]) ).
tcf(c_1283,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c9,iPr_def_25) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_642,c_602]) ).
tcf(c_1294,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_25,sk_c7) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_643,c_604]) ).
tcf(c_1296,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c9,iPr_def_25) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_643,c_602]) ).
tcf(c_1417,plain,
( ( sk_c9 = iPr_def_22 )
| ( inverse(iPr_def_26) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_648,c_605]) ).
tcf(c_1418,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_26,sk_c8) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_648,c_602]) ).
tcf(c_1449,plain,
! [X0: $i] :
( ( sk_c7 = X0 )
| ( sk_c7 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1221]) ).
tcf(c_1450,plain,
( ( sk_c7 = sk_c9 )
| ( sk_c7 != iPr_def_14 )
| ( sk_c9 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1449]) ).
tcf(c_1470,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_649,c_615]) ).
tcf(c_1474,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c8,iPr_def_26) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_649,c_603]) ).
tcf(c_1475,plain,
( ( sk_c9 = iPr_def_23 )
| ( inverse(iPr_def_26) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_649,c_605]) ).
tcf(c_1476,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_26,sk_c8) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_649,c_602]) ).
tcf(c_1534,plain,
( ( sk_c9 = iPr_def_26 )
| ( multiply(sk_c4,iPr_def_17) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_650,c_610]) ).
tcf(c_1569,plain,
( ( sk_c9 = iPr_def_16 )
| ( inverse(iPr_def_26) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_651,c_605]) ).
tcf(c_1570,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_26,sk_c8) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_651,c_602]) ).
tcf(c_1814,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c9,iPr_def_27) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_657,c_602]) ).
tcf(c_2044,plain,
( ( sk_c7 = iPr_def_14 )
| ( multiply(sk_c5,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_662,c_609]) ).
tcf(c_2110,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(sk_c4,iPr_def_14) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_664,c_610]) ).
tcf(c_2185,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c4,iPr_def_14) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_665,c_610]) ).
tcf(c_2302,plain,
( ( sk_c7 = iPr_def_14 )
| ( multiply(sk_c4,iPr_def_17) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_666,c_610]) ).
tcf(c_2479,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c7 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_668,c_666]) ).
tcf(c_2482,plain,
( ( iPr_def_15 = iPr_def_21 )
| ( sk_c7 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_668,c_663]) ).
tcf(c_2487,plain,
( ( sk_c7 = iPr_def_14 )
| ( multiply(sk_c4,iPr_def_15) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_668,c_610]) ).
tcf(c_2545,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_16 )
| ( inverse(sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_604,c_618]) ).
tcf(c_2547,plain,
( ~ iPr_def_12
| ( sk_c9 != sk_c7 )
| ( inverse(identity) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_101,c_618]) ).
tcf(c_2715,plain,
( ~ iPr_def_10
| ( sk_c8 != iPr_def_27 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_615,c_620]) ).
tcf(c_2736,plain,
( ~ iPr_def_10
| ( sk_c8 != iPr_def_27 )
| ( sk_c9 != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_2715,c_614]) ).
tcf(c_2958,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 = iPr_def_19 )
| ( iPr_def_14 != iPr_def_15 )
| ( sk_c7 != iPr_def_17 )
| ( sk_c7 != iPr_def_15 )
| ( sk_c9 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_628,c_616]) ).
tcf(c_3417,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c8,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_602,c_103]) ).
tcf(c_3418,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c9,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_603,c_103]) ).
tcf(c_3419,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c7,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_604,c_103]) ).
tcf(c_3421,plain,
! [X0: $i] : multiply(sk_c5,multiply(sk_c6,X0)) = multiply(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_609,c_103]) ).
tcf(c_3422,plain,
! [X0: $i] : multiply(sk_c6,multiply(sk_c9,X0)) = multiply(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_606,c_103]) ).
tcf(c_3423,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c9,X0)) = multiply(iPr_def_27,X0),
inference(superposition,[status(thm)],[c_615,c_103]) ).
tcf(c_3425,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c9,X0)) = multiply(iPr_def_24,X0),
inference(superposition,[status(thm)],[c_612,c_103]) ).
tcf(c_3427,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_102,c_103]) ).
tcf(c_3429,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c9,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1181,c_103]) ).
tcf(c_3430,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1182,c_103]) ).
tcf(c_3431,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1183,c_103]) ).
tcf(c_3432,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1184,c_103]) ).
tcf(c_3433,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1185,c_103]) ).
tcf(c_3439,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3433,c_101]) ).
tcf(c_3440,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3432,c_101]) ).
tcf(c_3441,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3431,c_101]) ).
tcf(c_3442,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3430,c_101]) ).
tcf(c_3443,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c9,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3429,c_101]) ).
tcf(c_4290,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_15 = X0 )
| ( iPr_def_15 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_6227,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(sk_c4,iPr_def_14) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_2479,c_610]) ).
tcf(c_6430,plain,
( ( iPr_def_15 = iPr_def_21 )
| ( multiply(sk_c4,iPr_def_14) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_2482,c_610]) ).
tcf(c_6722,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_19,iPr_def_27) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_659,c_1032]) ).
tcf(c_6729,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_19,iPr_def_25) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_643,c_1032]) ).
tcf(c_6886,plain,
multiply(iPr_def_19,iPr_def_24) = sk_c9,
inference(superposition,[status(thm)],[c_612,c_3439]) ).
tcf(c_6889,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(iPr_def_24,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_6886,c_103]) ).
tcf(c_6891,plain,
multiply(iPr_def_26,iPr_def_27) = sk_c9,
inference(superposition,[status(thm)],[c_615,c_3440]) ).
tcf(c_6904,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(iPr_def_27,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_6891,c_103]) ).
tcf(c_6906,plain,
multiply(iPr_def_20,iPr_def_21) = sk_c6,
inference(superposition,[status(thm)],[c_609,c_3441]) ).
tcf(c_6919,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(iPr_def_21,X0)) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_6906,c_103]) ).
tcf(c_6921,plain,
multiply(iPr_def_23,iPr_def_22) = sk_c7,
inference(superposition,[status(thm)],[c_610,c_3442]) ).
tcf(c_6934,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(iPr_def_22,X0)) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_6921,c_103]) ).
tcf(c_7931,plain,
multiply(iPr_def_17,iPr_def_14) = sk_c8,
inference(superposition,[status(thm)],[c_602,c_3443]) ).
tcf(c_7932,plain,
multiply(iPr_def_17,iPr_def_25) = sk_c3,
inference(superposition,[status(thm)],[c_613,c_3443]) ).
tcf(c_8137,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(iPr_def_14,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_7931,c_103]) ).
tcf(c_8139,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(iPr_def_25,X0)) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_7932,c_103]) ).
tcf(c_8762,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_19,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_635,c_1139]) ).
tcf(c_8770,plain,
( ( sk_c9 = iPr_def_25 )
| ( sk_c9 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_8762,c_6886]) ).
tcf(c_9286,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_8770,c_612]) ).
tcf(c_9288,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c8,iPr_def_25) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_8770,c_603]) ).
tcf(c_10038,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_26,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_649,c_1145]) ).
tcf(c_10126,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_26,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_648,c_1146]) ).
tcf(c_11724,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c8,sk_c9) )
| ( X1 != X0 )
| ( multiply(sk_c8,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_11725,plain,
( ( sk_c9 = multiply(sk_c8,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c8,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_11724]) ).
tcf(c_12191,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_25,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_664,c_1243]) ).
tcf(c_12398,plain,
! [X0: $i] :
( ( iPr_def_15 = X0 )
| ( iPr_def_15 != multiply(sk_c8,sk_c9) )
| ( X0 != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_4290]) ).
tcf(c_12399,plain,
( ( iPr_def_15 = sk_c9 )
| ( iPr_def_15 != multiply(sk_c8,sk_c9) )
| ( sk_c9 != multiply(sk_c8,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_12398]) ).
tcf(c_12602,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_25,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_665,c_1268]) ).
tcf(c_13592,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_25,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_667,c_1294]) ).
tcf(c_15301,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_656,c_1418]) ).
tcf(c_15312,plain,
( ( sk_c9 = iPr_def_22 )
| ( sk_c9 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_15301,c_6891]) ).
tcf(c_15871,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1470,c_3440]) ).
tcf(c_15872,plain,
( ( sk_c9 = iPr_def_26 )
| ( sk_c9 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_15871,c_6891]) ).
tcf(c_16106,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_27,iPr_def_26) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_657,c_1474]) ).
tcf(c_16163,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_657,c_1476]) ).
tcf(c_16175,plain,
( ( sk_c9 = iPr_def_23 )
| ( sk_c9 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_16163,c_6891]) ).
tcf(c_16237,plain,
( ( sk_c9 = iPr_def_26 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_1534,c_3442]) ).
tcf(c_16238,plain,
( ( sk_c7 = iPr_def_17 )
| ( sk_c9 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_16237,c_6921]) ).
tcf(c_16296,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_16175,c_15312]) ).
tcf(c_17034,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_659,c_1570]) ).
tcf(c_17048,plain,
( ( sk_c9 = iPr_def_16 )
| ( sk_c9 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_17034,c_6891]) ).
tcf(c_17103,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_17048,c_16175]) ).
tcf(c_19624,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_17,iPr_def_14) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1814,c_3443]) ).
tcf(c_19625,plain,
( ( sk_c8 = iPr_def_27 )
| ( sk_c9 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_19624,c_7931]) ).
tcf(c_21289,plain,
! [X0: $i] :
( ( iPr_def_22 = iPr_def_23 )
| ( multiply(iPr_def_17,multiply(iPr_def_14,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_16296,c_3443]) ).
tcf(c_21312,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( multiply(iPr_def_17,iPr_def_14) = identity ) ),
inference(superposition,[status(thm)],[c_16296,c_1181]) ).
tcf(c_21339,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( sk_c8 = identity ) ),
inference(light_normalisation,[status(thm)],[c_21312,c_7931]) ).
tcf(c_21396,plain,
! [X0: $i] :
( ( iPr_def_22 = iPr_def_23 )
| ( multiply(sk_c8,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_21289,c_8137]) ).
tcf(c_21545,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( multiply(sk_c8,sk_c9) = sk_c9 ) ),
inference(instantiation,[status(thm)],[c_21396]) ).
tcf(c_22645,plain,
( ( sk_c7 = iPr_def_14 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2302,c_3442]) ).
tcf(c_22646,plain,
( ( sk_c7 = iPr_def_17 )
| ( sk_c7 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_22645,c_6921]) ).
tcf(c_22863,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_23 )
| ( multiply(iPr_def_17,multiply(iPr_def_14,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_17103,c_3443]) ).
tcf(c_22886,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( multiply(iPr_def_17,iPr_def_14) = identity ) ),
inference(superposition,[status(thm)],[c_17103,c_1181]) ).
tcf(c_22911,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( sk_c8 = identity ) ),
inference(light_normalisation,[status(thm)],[c_22886,c_7931]) ).
tcf(c_22974,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_23 )
| ( multiply(sk_c8,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_22863,c_8137]) ).
tcf(c_23129,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( multiply(sk_c8,sk_c9) = sk_c9 ) ),
inference(instantiation,[status(thm)],[c_22974]) ).
tcf(c_23917,plain,
( ( sk_c7 = iPr_def_14 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2487,c_3442]) ).
tcf(c_23918,plain,
( ( sk_c7 = iPr_def_15 )
| ( sk_c7 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_23917,c_6921]) ).
tcf(c_25308,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( identity = iPr_def_25 )
| ( sk_c7 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_21339,c_644]) ).
tcf(c_25315,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( multiply(identity,sk_c7) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_21339,c_604]) ).
tcf(c_26260,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( identity = iPr_def_25 )
| ( sk_c7 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_22911,c_644]) ).
tcf(c_27127,plain,
multiply(sk_c9,iPr_def_15) = multiply(iPr_def_14,sk_c9),
inference(superposition,[status(thm)],[c_603,c_3417]) ).
tcf(c_27128,plain,
multiply(sk_c9,iPr_def_16) = multiply(iPr_def_14,sk_c7),
inference(superposition,[status(thm)],[c_604,c_3417]) ).
tcf(c_27516,plain,
multiply(iPr_def_17,multiply(iPr_def_14,sk_c9)) = iPr_def_15,
inference(superposition,[status(thm)],[c_27127,c_3443]) ).
tcf(c_27693,plain,
multiply(iPr_def_17,multiply(iPr_def_14,sk_c7)) = iPr_def_16,
inference(superposition,[status(thm)],[c_27128,c_3443]) ).
tcf(c_27902,plain,
multiply(sk_c8,iPr_def_14) = multiply(iPr_def_15,sk_c8),
inference(superposition,[status(thm)],[c_602,c_3418]) ).
tcf(c_27903,plain,
multiply(sk_c8,iPr_def_25) = multiply(iPr_def_15,sk_c3),
inference(superposition,[status(thm)],[c_613,c_3418]) ).
tcf(c_27908,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c8,iPr_def_25) = multiply(iPr_def_15,iPr_def_24) ) ),
inference(superposition,[status(thm)],[c_1145,c_3418]) ).
tcf(c_27928,plain,
multiply(sk_c8,multiply(iPr_def_14,sk_c7)) = multiply(iPr_def_15,iPr_def_16),
inference(superposition,[status(thm)],[c_27128,c_3418]) ).
tcf(c_28372,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_15,iPr_def_25) = multiply(iPr_def_25,iPr_def_14) ) ),
inference(superposition,[status(thm)],[c_643,c_27902]) ).
tcf(c_28374,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_15,iPr_def_25) = multiply(iPr_def_25,iPr_def_14) ) ),
inference(superposition,[status(thm)],[c_641,c_27902]) ).
tcf(c_28375,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_15,iPr_def_25) = multiply(iPr_def_25,iPr_def_14) ) ),
inference(superposition,[status(thm)],[c_640,c_27902]) ).
tcf(c_28493,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_15,sk_c3) = multiply(iPr_def_27,iPr_def_25) ) ),
inference(superposition,[status(thm)],[c_659,c_27903]) ).
tcf(c_28877,plain,
multiply(sk_c5,iPr_def_18) = multiply(iPr_def_21,sk_c9),
inference(superposition,[status(thm)],[c_606,c_3421]) ).
tcf(c_28956,plain,
multiply(sk_c6,iPr_def_14) = multiply(iPr_def_18,sk_c8),
inference(superposition,[status(thm)],[c_602,c_3422]) ).
tcf(c_28982,plain,
multiply(sk_c6,multiply(iPr_def_14,sk_c7)) = multiply(iPr_def_18,iPr_def_16),
inference(superposition,[status(thm)],[c_27128,c_3422]) ).
tcf(c_29309,plain,
( ( sk_c7 = iPr_def_14 )
| ( multiply(iPr_def_18,sk_c8) = multiply(iPr_def_20,iPr_def_14) ) ),
inference(superposition,[status(thm)],[c_662,c_28956]) ).
tcf(c_29315,plain,
multiply(sk_c5,multiply(iPr_def_18,sk_c8)) = multiply(iPr_def_21,iPr_def_14),
inference(superposition,[status(thm)],[c_28956,c_3421]) ).
tcf(c_29363,plain,
multiply(sk_c1,iPr_def_14) = multiply(iPr_def_27,sk_c8),
inference(superposition,[status(thm)],[c_602,c_3423]) ).
tcf(c_29364,plain,
multiply(sk_c1,iPr_def_25) = multiply(iPr_def_27,sk_c3),
inference(superposition,[status(thm)],[c_613,c_3423]) ).
tcf(c_29374,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_14) = multiply(iPr_def_27,iPr_def_25) ) ),
inference(superposition,[status(thm)],[c_1296,c_3423]) ).
tcf(c_29892,plain,
multiply(sk_c2,iPr_def_14) = multiply(iPr_def_24,sk_c8),
inference(superposition,[status(thm)],[c_602,c_3425]) ).
tcf(c_29893,plain,
multiply(sk_c2,iPr_def_25) = multiply(iPr_def_24,sk_c3),
inference(superposition,[status(thm)],[c_613,c_3425]) ).
tcf(c_29919,plain,
multiply(sk_c2,multiply(iPr_def_14,sk_c7)) = multiply(iPr_def_24,iPr_def_16),
inference(superposition,[status(thm)],[c_27128,c_3425]) ).
tcf(c_31301,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_3427,c_101]) ).
tcf(c_31343,plain,
multiply(inverse(sk_c4),iPr_def_22) = sk_c7,
inference(superposition,[status(thm)],[c_610,c_31301]) ).
tcf(c_31349,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_101,c_31301]) ).
tcf(c_31350,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_102,c_31301]) ).
tcf(c_31445,plain,
multiply(inverse(iPr_def_17),identity) = sk_c9,
inference(superposition,[status(thm)],[c_1181,c_31301]) ).
tcf(c_31523,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(inverse(sk_c4),iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2185,c_31301]) ).
tcf(c_31524,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(inverse(sk_c4),iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2110,c_31301]) ).
tcf(c_31537,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_3443,c_31301]) ).
tcf(c_31538,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_3442,c_31301]) ).
tcf(c_31539,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_3441,c_31301]) ).
tcf(c_31540,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_3440,c_31301]) ).
tcf(c_31541,plain,
! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_3439,c_31301]) ).
tcf(c_31572,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(inverse(iPr_def_27),iPr_def_15) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_16106,c_31301]) ).
tcf(c_31581,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_31301,c_31301]) ).
tcf(c_36251,plain,
( ~ iPr_def_13
| ( inverse(inverse(identity)) != sk_c9 )
| ( multiply(sk_c9,sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_31349,c_617]) ).
tcf(c_36255,plain,
( ~ iPr_def_11
| ( inverse(inverse(identity)) != sk_c7 )
| ( multiply(inverse(inverse(identity)),sk_c9) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_31349,c_619]) ).
tcf(c_36271,plain,
multiply(sk_c9,identity) = sk_c9,
inference(demodulation,[status(thm)],[c_31445,c_31537]) ).
tcf(c_36316,plain,
multiply(sk_c8,sk_c9) = multiply(iPr_def_15,identity),
inference(superposition,[status(thm)],[c_36271,c_3418]) ).
tcf(c_36319,plain,
multiply(iPr_def_15,identity) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_36316,c_603]) ).
tcf(c_36681,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_31350,c_31581]) ).
tcf(c_36699,plain,
multiply(sk_c9,sk_c8) = multiply(iPr_def_14,identity),
inference(superposition,[status(thm)],[c_36681,c_3417]) ).
tcf(c_36706,plain,
multiply(sk_c8,sk_c7) = multiply(iPr_def_16,identity),
inference(superposition,[status(thm)],[c_36681,c_3419]) ).
tcf(c_36713,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_36681,c_31349]) ).
tcf(c_36716,plain,
multiply(iPr_def_16,identity) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_36706,c_604]) ).
tcf(c_36718,plain,
multiply(iPr_def_14,identity) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_36699,c_602]) ).
tcf(c_39585,plain,
( ~ iPr_def_10
| ( inverse(inverse(iPr_def_17)) != sk_c9 )
| ( multiply(sk_c9,sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_31537,c_620]) ).
tcf(c_39588,plain,
multiply(sk_c9,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_31537,c_102]) ).
tcf(c_39591,plain,
! [X0: $i] : multiply(sk_c9,multiply(iPr_def_17,X0)) = X0,
inference(superposition,[status(thm)],[c_31537,c_31301]) ).
tcf(c_39592,plain,
multiply(sk_c9,identity) = inverse(iPr_def_17),
inference(superposition,[status(thm)],[c_31537,c_36681]) ).
tcf(c_39654,plain,
multiply(sk_c1,identity) = multiply(iPr_def_27,iPr_def_17),
inference(superposition,[status(thm)],[c_39588,c_3423]) ).
tcf(c_39655,plain,
multiply(sk_c6,identity) = multiply(iPr_def_18,iPr_def_17),
inference(superposition,[status(thm)],[c_39588,c_3422]) ).
tcf(c_39656,plain,
multiply(sk_c8,identity) = multiply(iPr_def_15,iPr_def_17),
inference(superposition,[status(thm)],[c_39588,c_3418]) ).
tcf(c_39657,plain,
multiply(iPr_def_17,identity) = iPr_def_17,
inference(superposition,[status(thm)],[c_39588,c_3443]) ).
tcf(c_39798,plain,
inverse(iPr_def_17) = sk_c9,
inference(demodulation,[status(thm)],[c_39592,c_36681]) ).
tcf(c_40183,plain,
multiply(sk_c9,sk_c8) = iPr_def_14,
inference(superposition,[status(thm)],[c_7931,c_39591]) ).
tcf(c_40184,plain,
multiply(sk_c9,sk_c3) = iPr_def_25,
inference(superposition,[status(thm)],[c_7932,c_39591]) ).
tcf(c_41046,plain,
! [X0: $i] :
( ( iPr_def_15 = sk_c7 )
| ( iPr_def_15 != X0 )
| ( sk_c7 != X0 ) ),
inference(instantiation,[status(thm)],[c_1257]) ).
tcf(c_41047,plain,
( ( iPr_def_15 = sk_c7 )
| ( iPr_def_15 != sk_c9 )
| ( sk_c7 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_41046]) ).
tcf(c_43360,plain,
multiply(iPr_def_27,iPr_def_17) = sk_c1,
inference(demodulation,[status(thm)],[c_39654,c_36681]) ).
tcf(c_43370,plain,
multiply(inverse(iPr_def_27),sk_c1) = iPr_def_17,
inference(superposition,[status(thm)],[c_43360,c_31301]) ).
tcf(c_45401,plain,
multiply(iPr_def_18,iPr_def_17) = sk_c6,
inference(demodulation,[status(thm)],[c_39655,c_36681]) ).
tcf(c_45646,plain,
multiply(iPr_def_15,iPr_def_17) = sk_c8,
inference(demodulation,[status(thm)],[c_39656,c_36681]) ).
tcf(c_45647,plain,
multiply(inverse(iPr_def_15),sk_c8) = iPr_def_17,
inference(superposition,[status(thm)],[c_45646,c_31301]) ).
tcf(c_45668,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(inverse(iPr_def_15),iPr_def_27) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_658,c_45647]) ).
tcf(c_45669,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(inverse(iPr_def_15),iPr_def_27) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_657,c_45647]) ).
tcf(c_45675,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(inverse(iPr_def_15),iPr_def_25) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_642,c_45647]) ).
tcf(c_45680,plain,
multiply(inverse(inverse(iPr_def_15)),iPr_def_17) = sk_c8,
inference(superposition,[status(thm)],[c_45647,c_31301]) ).
tcf(c_46105,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(inverse(inverse(iPr_def_15)),iPr_def_17) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_45668,c_31301]) ).
tcf(c_46125,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(inverse(inverse(iPr_def_15)),iPr_def_17) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_45669,c_31301]) ).
tcf(c_46479,plain,
( ~ iPr_def_13
| ( inverse(inverse(iPr_def_23)) != sk_c9 )
| ( multiply(sk_c9,multiply(sk_c4,sk_c9)) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_31538,c_617]) ).
tcf(c_46480,plain,
( ~ iPr_def_10
| ( inverse(inverse(iPr_def_23)) != sk_c9 )
| ( multiply(sk_c4,sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_31538,c_620]) ).
tcf(c_46483,plain,
multiply(sk_c4,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_31538,c_102]) ).
tcf(c_46485,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_23)) != sk_c9 )
| ( multiply(sk_c4,sk_c7) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_31538,c_618]) ).
tcf(c_46486,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_23,X0)) = X0,
inference(superposition,[status(thm)],[c_31538,c_31301]) ).
tcf(c_46487,plain,
multiply(sk_c4,identity) = inverse(iPr_def_23),
inference(superposition,[status(thm)],[c_31538,c_36681]) ).
tcf(c_46496,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_22 )
| ( inverse(inverse(iPr_def_23)) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_46485,c_610]) ).
tcf(c_46524,plain,
inverse(iPr_def_23) = sk_c4,
inference(demodulation,[status(thm)],[c_46487,c_36681]) ).
tcf(c_46537,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_23,sk_c4) != sk_c7 )
| ( multiply(inverse(iPr_def_23),sk_c9) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_46524,c_619]) ).
tcf(c_46549,plain,
multiply(sk_c4,sk_c7) = iPr_def_22,
inference(superposition,[status(thm)],[c_6921,c_46486]) ).
tcf(c_46569,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(inverse(inverse(iPr_def_15)),iPr_def_17) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_45675,c_31301]) ).
tcf(c_47585,plain,
multiply(sk_c5,iPr_def_20) = identity,
inference(superposition,[status(thm)],[c_31539,c_102]) ).
tcf(c_47588,plain,
! [X0: $i] : multiply(sk_c5,multiply(iPr_def_20,X0)) = X0,
inference(superposition,[status(thm)],[c_31539,c_31301]) ).
tcf(c_47589,plain,
multiply(sk_c5,identity) = inverse(iPr_def_20),
inference(superposition,[status(thm)],[c_31539,c_36681]) ).
tcf(c_47602,plain,
( ( identity = iPr_def_21 )
| ( sk_c7 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_2044,c_47585]) ).
tcf(c_47695,plain,
inverse(iPr_def_20) = sk_c5,
inference(demodulation,[status(thm)],[c_47589,c_36681]) ).
tcf(c_47698,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_20,sk_c5) != sk_c7 )
| ( multiply(inverse(iPr_def_20),sk_c9) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_47695,c_619]) ).
tcf(c_47700,plain,
( ~ iPr_def_11
| ( sk_c7 != identity )
| ( multiply(sk_c5,sk_c9) != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_47698,c_1183,c_47695]) ).
tcf(c_47709,plain,
multiply(sk_c5,identity) = sk_c5,
inference(superposition,[status(thm)],[c_1183,c_47588]) ).
tcf(c_47710,plain,
multiply(sk_c5,sk_c6) = iPr_def_21,
inference(superposition,[status(thm)],[c_6906,c_47588]) ).
tcf(c_50886,plain,
( ~ iPr_def_13
| ( inverse(inverse(iPr_def_26)) != sk_c9 )
| ( multiply(sk_c9,multiply(sk_c1,sk_c9)) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_31540,c_617]) ).
tcf(c_50890,plain,
multiply(sk_c1,iPr_def_26) = identity,
inference(superposition,[status(thm)],[c_31540,c_102]) ).
tcf(c_50892,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_26)) != sk_c9 )
| ( multiply(sk_c1,sk_c7) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_31540,c_618]) ).
tcf(c_50893,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_26,X0)) = X0,
inference(superposition,[status(thm)],[c_31540,c_31301]) ).
tcf(c_50894,plain,
multiply(sk_c1,identity) = inverse(iPr_def_26),
inference(superposition,[status(thm)],[c_31540,c_36681]) ).
tcf(c_51152,plain,
inverse(iPr_def_26) = sk_c1,
inference(demodulation,[status(thm)],[c_50894,c_36681]) ).
tcf(c_51161,plain,
( ( sk_c1 = iPr_def_17 )
| ( sk_c9 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1569,c_51152]) ).
tcf(c_51162,plain,
( ( sk_c1 = iPr_def_17 )
| ( sk_c9 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_1475,c_51152]) ).
tcf(c_51163,plain,
( ( sk_c1 = iPr_def_17 )
| ( sk_c9 = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_1417,c_51152]) ).
tcf(c_51244,plain,
multiply(sk_c1,sk_c9) = iPr_def_27,
inference(superposition,[status(thm)],[c_6891,c_50893]) ).
tcf(c_51248,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_10126,c_50893]) ).
tcf(c_51249,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_10038,c_50893]) ).
tcf(c_51265,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_27,sk_c3) = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_51249,c_29364]) ).
tcf(c_51268,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_27,sk_c3) = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_51248,c_29364]) ).
tcf(c_55325,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_17,iPr_def_14) = multiply(iPr_def_27,sk_c8) ) ),
inference(superposition,[status(thm)],[c_51161,c_29363]) ).
tcf(c_55332,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_17,iPr_def_19) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_51161,c_1172]) ).
tcf(c_55524,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(inverse(iPr_def_27),iPr_def_17) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_51162,c_43370]) ).
tcf(c_55530,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_17,iPr_def_25) = multiply(iPr_def_27,sk_c3) ) ),
inference(superposition,[status(thm)],[c_51162,c_29364]) ).
tcf(c_55531,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_17,iPr_def_14) = multiply(iPr_def_27,sk_c8) ) ),
inference(superposition,[status(thm)],[c_51162,c_29363]) ).
tcf(c_55541,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_17,sk_c9) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_51162,c_615]) ).
tcf(c_55542,plain,
( ( sk_c9 = iPr_def_23 )
| ( inverse(iPr_def_17) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_51162,c_614]) ).
tcf(c_55789,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_17,iPr_def_25) = multiply(iPr_def_27,sk_c3) ) ),
inference(superposition,[status(thm)],[c_51163,c_29364]) ).
tcf(c_56813,plain,
multiply(sk_c2,iPr_def_19) = identity,
inference(superposition,[status(thm)],[c_31541,c_102]) ).
tcf(c_56816,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_19,X0)) = X0,
inference(superposition,[status(thm)],[c_31541,c_31301]) ).
tcf(c_56817,plain,
multiply(sk_c2,identity) = inverse(iPr_def_19),
inference(superposition,[status(thm)],[c_31541,c_36681]) ).
tcf(c_57674,plain,
inverse(iPr_def_19) = sk_c2,
inference(demodulation,[status(thm)],[c_56817,c_36681]) ).
tcf(c_57728,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_6722,c_56816]) ).
tcf(c_57729,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_6729,c_56816]) ).
tcf(c_57730,plain,
multiply(sk_c2,sk_c9) = iPr_def_24,
inference(superposition,[status(thm)],[c_6886,c_56816]) ).
tcf(c_57735,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_57729,c_29892]) ).
tcf(c_57738,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_57728,c_29892]) ).
tcf(c_75654,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(inverse(sk_c4),iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_6227,c_31301]) ).
tcf(c_75886,plain,
( ( iPr_def_15 = iPr_def_21 )
| ( multiply(inverse(sk_c4),iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_6430,c_31301]) ).
tcf(c_79667,plain,
multiply(sk_c9,identity) = multiply(iPr_def_19,iPr_def_24),
inference(superposition,[status(thm)],[c_36681,c_6889]) ).
tcf(c_79707,plain,
multiply(sk_c9,identity) = multiply(iPr_def_26,iPr_def_27),
inference(superposition,[status(thm)],[c_36681,c_6904]) ).
tcf(c_80858,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( sk_c7 = iPr_def_15 ) ),
inference(global_subsumption_just,[status(thm)],[c_25308,c_675,c_603,c_1236,c_1259,c_1450,c_11725,c_12399,c_16296,c_21545,c_23918,c_41047]) ).
tcf(c_82610,plain,
multiply(sk_c6,identity) = multiply(iPr_def_20,iPr_def_21),
inference(superposition,[status(thm)],[c_36681,c_6919]) ).
tcf(c_82614,plain,
multiply(sk_c6,identity) = sk_c6,
inference(light_normalisation,[status(thm)],[c_82610,c_6906]) ).
tcf(c_82623,plain,
multiply(sk_c7,identity) = multiply(iPr_def_23,iPr_def_22),
inference(superposition,[status(thm)],[c_36681,c_6934]) ).
tcf(c_82628,plain,
multiply(sk_c7,identity) = sk_c7,
inference(light_normalisation,[status(thm)],[c_82623,c_6921]) ).
tcf(c_82644,plain,
multiply(sk_c8,identity) = multiply(iPr_def_17,iPr_def_14),
inference(superposition,[status(thm)],[c_36681,c_8137]) ).
tcf(c_82648,plain,
multiply(sk_c8,identity) = sk_c8,
inference(light_normalisation,[status(thm)],[c_82644,c_7931]) ).
tcf(c_82667,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(sk_c3,iPr_def_14) = multiply(iPr_def_17,iPr_def_16) ) ),
inference(superposition,[status(thm)],[c_12602,c_8139]) ).
tcf(c_82672,plain,
multiply(sk_c3,identity) = multiply(iPr_def_17,iPr_def_25),
inference(superposition,[status(thm)],[c_36681,c_8139]) ).
tcf(c_82681,plain,
multiply(sk_c3,identity) = sk_c3,
inference(light_normalisation,[status(thm)],[c_82672,c_7932]) ).
tcf(c_83629,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_24,sk_c3) = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_9286,c_29893]) ).
tcf(c_83655,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c9,sk_c3) = multiply(iPr_def_19,iPr_def_24) ) ),
inference(superposition,[status(thm)],[c_83629,c_6889]) ).
tcf(c_85433,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( sk_c7 = iPr_def_15 ) ),
inference(global_subsumption_just,[status(thm)],[c_26260,c_675,c_603,c_1236,c_1259,c_1450,c_11725,c_12399,c_17103,c_23129,c_23918,c_41047]) ).
tcf(c_85514,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_16 = iPr_def_23 )
| ( iPr_def_14 != iPr_def_15 )
| ( sk_c7 != iPr_def_17 )
| ( sk_c7 != iPr_def_15 )
| ( sk_c9 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_85433,c_616]) ).
tcf(c_86817,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_15,sk_c3) = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_9288,c_27903]) ).
tcf(c_131474,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_15,iPr_def_25) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_28372,c_13592]) ).
tcf(c_131999,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_17,multiply(iPr_def_15,iPr_def_25)) = multiply(sk_c3,iPr_def_14) ) ),
inference(superposition,[status(thm)],[c_28374,c_8139]) ).
tcf(c_132001,plain,
( ( sk_c9 = iPr_def_23 )
| ( multiply(iPr_def_15,iPr_def_25) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_28374,c_12602]) ).
tcf(c_132036,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_15,iPr_def_25) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_28375,c_12191]) ).
tcf(c_138384,plain,
( ( sk_c7 = iPr_def_14 )
| ( multiply(sk_c5,multiply(iPr_def_18,sk_c8)) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_29309,c_47588]) ).
tcf(c_138385,plain,
( ( sk_c7 = iPr_def_14 )
| ( multiply(iPr_def_21,iPr_def_14) = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_138384,c_29315]) ).
tcf(c_148317,plain,
( ~ iPr_def_12
| ( sk_c9 != identity )
| ( sk_c9 != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_2547,c_36713]) ).
tcf(c_149775,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( sk_c7 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_25315,c_101]) ).
tcf(c_149829,plain,
( ( iPr_def_22 = iPr_def_23 )
| ( iPr_def_15 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_149775,c_80858]) ).
tcf(c_150357,plain,
( ( iPr_def_15 = iPr_def_16 )
| ( multiply(iPr_def_22,iPr_def_22) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_149829,c_6921]) ).
tcf(c_150359,plain,
( ( iPr_def_15 = iPr_def_16 )
| ( multiply(iPr_def_22,sk_c4) = identity ) ),
inference(superposition,[status(thm)],[c_149829,c_1182]) ).
tcf(c_151678,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_150359,c_150357,c_148317,c_138385,c_132036,c_131999,c_132001,c_131474,c_86817,c_85514,c_83655,c_82681,c_82672,c_82667,c_82648,c_82644,c_82628,c_82623,c_82614,c_82610,c_79707,c_79667,c_75886,c_75654,c_57738,c_57735,c_57730,c_57674,c_56813,c_55789,c_55542,c_55531,c_55530,c_55524,c_55541,c_55332,c_55325,c_51268,c_51265,c_51244,c_51152,c_50892,c_50886,c_50890,c_47710,c_47709,c_47700,c_47695,c_47602,c_47585,c_46569,c_46549,c_46537,c_46524,c_46496,c_46480,c_46479,c_46483,c_46125,c_46105,c_45680,c_45669,c_45647,c_45646,c_45401,c_43360,c_40184,c_40183,c_39798,c_39657,c_39585,c_39592,c_39588,c_36718,c_36716,c_36706,c_36713,c_36319,c_36255,c_36251,c_31572,c_31524,c_31523,c_31343,c_29919,c_29892,c_29374,c_29363,c_28982,c_28877,c_28493,c_27928,c_27908,c_27903,c_27693,c_27516,c_27128,c_22646,c_19625,c_16238,c_16175,c_15872,c_15871,c_2958,c_2736,c_2545,c_1283,c_1182,c_1181,c_1144,c_628,c_627,c_626,c_625,c_624,c_623,c_622,c_621,c_616,c_614,c_611,c_605]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP282-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n017.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 14:16:45 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/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.10/0.44
% 0.10/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.44
% 0.10/0.44 % Detected problem language: tptp
% 0.10/0.45 % Proving...
% 54.55/10.53 % SZS status Started for theBenchmark.p
% 54.55/10.53 % SZS status Unsatisfiable for theBenchmark.p
% 54.55/10.53
% 54.55/10.53 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 54.55/10.53
% 54.55/10.53 % ------ iProver source info
% 54.55/10.53
% 54.55/10.53 % git: date: 2026-07-19 20:42:38 +0200
% 54.55/10.53 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 54.55/10.53 % git: non_committed_changes: false
% 54.55/10.53
% 54.55/10.53 % ------ Parsing...% successful
% 54.55/10.53
% 54.55/10.53
% 54.55/10.53 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 54.55/10.53
% 54.55/10.53 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 54.55/10.53
% 54.55/10.53 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 54.55/10.53
% 54.55/10.53 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 54.55/10.53 % ------ Proving...
% 54.55/10.53 % ------ Problem Properties
% 54.55/10.53
% 54.55/10.53 %
% 54.55/10.53 % clauses 70
% 54.55/10.53 % conjectures 53
% 54.55/10.53 % EPR 49
% 54.55/10.53 % Horn 21
% 54.55/10.53 % unary 17
% 54.55/10.53 % binary 48
% 54.55/10.53 % lits 133
% 54.55/10.53 % lits eq 125
% 54.55/10.53 % fd_pure 0
% 54.55/10.53 % fd_pseudo 0
% 54.55/10.53 % fd_cond 0
% 54.55/10.53 % fd_pseudo_cond 0
% 54.55/10.53 % AC symbols 0
% 54.55/10.53
% 54.55/10.53 % ------ Schedule dynamic 5 is on
% 54.55/10.53
% 54.55/10.53 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 54.55/10.53
% 54.55/10.53
% 54.55/10.53 % ------
% 54.55/10.53 % Current options:
% 54.55/10.53 % ------
% 54.55/10.53
% 54.55/10.53
% 54.55/10.53 %
% 54.55/10.53
% 54.55/10.53 % ------ Proving...
% 54.55/10.53 %
% 54.55/10.53
% 54.55/10.53 % SZS status Unsatisfiable for theBenchmark.p
% 54.55/10.53
% 54.55/10.53 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 54.55/10.55
% 54.55/10.55
%------------------------------------------------------------------------------