%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP243-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 : n008.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:26 PM UTC 2026
% Result : Unsatisfiable 26.28s 4.30s
% Output : CNFRefutation 26.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 69
% Syntax : Number of formulae : 514 ( 112 unt; 16 def)
% Number of atoms : 1729 ( 961 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 754 ( 214 ~; 540 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 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 : 23 ( 21 usr; 22 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 116 ( 0 sgn 116 !; 0 ?; 77 :)
% 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,
( inverse(sk_c6) = sk_c12
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c12 = inverse(sk_c6)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c12 = multiply(sk_c6,sk_c11)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( inverse(sk_c7) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c11 = inverse(sk_c7)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( inverse(sk_c8) = sk_c9
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c9 = inverse(sk_c8)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c11 = multiply(sk_c9,sk_c10)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( inverse(sk_c6) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c12 = inverse(sk_c6)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( multiply(sk_c6,sk_c11) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c12 = multiply(sk_c6,sk_c11)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( inverse(sk_c7) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c11 = inverse(sk_c7)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f28,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( inverse(sk_c8) = sk_c9
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f30,plain,
( sk_c9 = inverse(sk_c8)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c11 = multiply(sk_c9,sk_c10)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f31]) ).
fof(f37,negated_conjecture,
( inverse(sk_c7) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c11 = inverse(sk_c7)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f42,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( inverse(sk_c8) = sk_c9
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f44,plain,
( sk_c9 = inverse(sk_c8)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c11 = multiply(sk_c9,sk_c10)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f45]) ).
fof(f51,negated_conjecture,
( inverse(sk_c7) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c11 = inverse(sk_c7)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( inverse(sk_c8) = sk_c9
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f58,plain,
( sk_c9 = inverse(sk_c8)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c11 = multiply(sk_c9,sk_c10)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( inverse(sk_c6) = sk_c12
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c12 = inverse(sk_c6)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( multiply(sk_c6,sk_c11) = sk_c12
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c12 = multiply(sk_c6,sk_c11)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c7) = sk_c11
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c11 = inverse(sk_c7)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f68,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f70,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f69]) ).
fof(f73,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c11
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f74,plain,
( sk_c11 = multiply(sk_c9,sk_c10)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( inverse(sk_c6) = sk_c12
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c12 = inverse(sk_c6)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
( multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
( sk_c12 = multiply(sk_c6,sk_c11)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f77]) ).
fof(f79,negated_conjecture,
( inverse(sk_c7) = sk_c11
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_38) ).
fof(f80,plain,
( sk_c11 = inverse(sk_c7)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f79]) ).
fof(f81,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_39) ).
fof(f82,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_40) ).
fof(f84,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( inverse(sk_c8) = sk_c9
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f86,plain,
( sk_c9 = inverse(sk_c8)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c11
| multiply(sk_c3,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c11 = multiply(sk_c9,sk_c10)
| sk_c12 = multiply(sk_c3,sk_c11) ),
inference(reorient_equations,[],[f87]) ).
fof(f93,negated_conjecture,
( inverse(sk_c7) = sk_c11
| multiply(sk_c4,sk_c5) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f94,plain,
( sk_c11 = inverse(sk_c7)
| sk_c11 = multiply(sk_c4,sk_c5) ),
inference(reorient_equations,[],[f93]) ).
fof(f97,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c4,sk_c5) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f98,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c11 = multiply(sk_c4,sk_c5) ),
inference(reorient_equations,[],[f97]) ).
fof(f99,negated_conjecture,
( inverse(sk_c8) = sk_c9
| multiply(sk_c4,sk_c5) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f100,plain,
( sk_c9 = inverse(sk_c8)
| sk_c11 = multiply(sk_c4,sk_c5) ),
inference(reorient_equations,[],[f99]) ).
fof(f107,negated_conjecture,
( inverse(sk_c7) = sk_c11
| inverse(sk_c4) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_52) ).
fof(f108,plain,
( sk_c11 = inverse(sk_c7)
| sk_c5 = inverse(sk_c4) ),
inference(reorient_equations,[],[f107]) ).
fof(f111,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| inverse(sk_c4) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_54) ).
fof(f112,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c5 = inverse(sk_c4) ),
inference(reorient_equations,[],[f111]) ).
fof(f117,negated_conjecture,
( inverse(sk_c6) = sk_c12
| multiply(sk_c5,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_57) ).
fof(f118,plain,
( sk_c12 = inverse(sk_c6)
| sk_c11 = multiply(sk_c5,sk_c10) ),
inference(reorient_equations,[],[f117]) ).
fof(f119,negated_conjecture,
( multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c5,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_58) ).
fof(f120,plain,
( sk_c12 = multiply(sk_c6,sk_c11)
| sk_c11 = multiply(sk_c5,sk_c10) ),
inference(reorient_equations,[],[f119]) ).
fof(f121,negated_conjecture,
( inverse(sk_c7) = sk_c11
| multiply(sk_c5,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_59) ).
fof(f122,plain,
( sk_c11 = inverse(sk_c7)
| sk_c11 = multiply(sk_c5,sk_c10) ),
inference(reorient_equations,[],[f121]) ).
fof(f123,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| multiply(sk_c5,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_60) ).
fof(f124,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| sk_c11 = multiply(sk_c5,sk_c10) ),
inference(reorient_equations,[],[f123]) ).
fof(f125,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c5,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_61) ).
fof(f126,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c11 = multiply(sk_c5,sk_c10) ),
inference(reorient_equations,[],[f125]) ).
fof(f127,negated_conjecture,
( inverse(sk_c8) = sk_c9
| multiply(sk_c5,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_62) ).
fof(f128,plain,
( sk_c9 = inverse(sk_c8)
| sk_c11 = multiply(sk_c5,sk_c10) ),
inference(reorient_equations,[],[f127]) ).
fof(f129,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c11
| multiply(sk_c5,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_63) ).
fof(f130,plain,
( sk_c11 = multiply(sk_c9,sk_c10)
| sk_c11 = multiply(sk_c5,sk_c10) ),
inference(reorient_equations,[],[f129]) ).
fof(f131,negated_conjecture,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X8,sk_c10) != sk_c11
| inverse(X7) != X8
| multiply(X7,X8) != sk_c11
| multiply(X6,sk_c10) != sk_c11
| inverse(X6) != sk_c11
| multiply(X5,sk_c11) != sk_c12
| inverse(X5) != sk_c12
| multiply(X4,sk_c10) != sk_c11
| inverse(X3) != X4
| multiply(X3,X4) != sk_c11
| multiply(X2,sk_c11) != sk_c12
| inverse(X2) != sk_c12
| inverse(X1) != sk_c11
| multiply(X1,sk_c11) != sk_c10
| inverse(X0) != sk_c12
| multiply(X0,sk_c12) != sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_64) ).
fof(f132,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( sk_c11 != multiply(X8,sk_c10)
| inverse(X7) != X8
| sk_c11 != multiply(X7,X8)
| sk_c11 != multiply(X6,sk_c10)
| sk_c11 != inverse(X6)
| sk_c12 != multiply(X5,sk_c11)
| sk_c12 != inverse(X5)
| sk_c11 != multiply(X4,sk_c10)
| inverse(X3) != X4
| sk_c11 != multiply(X3,X4)
| sk_c12 != multiply(X2,sk_c11)
| sk_c12 != inverse(X2)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(X1,sk_c11)
| inverse(X0) != sk_c12
| sk_c11 != multiply(X0,sk_c12) ),
inference(reorient_equations,[],[f131]) ).
fof(f133,plain,
! [X2,X3,X0,X1,X8,X6,X7,X5] :
( sk_c11 != multiply(X8,sk_c10)
| inverse(X7) != X8
| sk_c11 != multiply(X7,X8)
| sk_c11 != multiply(X6,sk_c10)
| sk_c11 != inverse(X6)
| sk_c12 != multiply(X5,sk_c11)
| sk_c12 != inverse(X5)
| sk_c11 != multiply(inverse(X3),sk_c10)
| sk_c11 != multiply(X3,inverse(X3))
| sk_c12 != multiply(X2,sk_c11)
| sk_c12 != inverse(X2)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(X1,sk_c11)
| inverse(X0) != sk_c12
| sk_c11 != multiply(X0,sk_c12) ),
inference(equality_resolution,[],[f132]) ).
fof(f134,plain,
! [X2,X3,X0,X1,X6,X7,X5] :
( sk_c11 != multiply(inverse(X7),sk_c10)
| sk_c11 != multiply(X7,inverse(X7))
| sk_c11 != multiply(X6,sk_c10)
| sk_c11 != inverse(X6)
| sk_c12 != multiply(X5,sk_c11)
| sk_c12 != inverse(X5)
| sk_c11 != multiply(inverse(X3),sk_c10)
| sk_c11 != multiply(X3,inverse(X3))
| sk_c12 != multiply(X2,sk_c11)
| sk_c12 != inverse(X2)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(X1,sk_c11)
| inverse(X0) != sk_c12
| sk_c11 != multiply(X0,sk_c12) ),
inference(equality_resolution,[],[f133]) ).
tcf(c_116,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_117,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c6,sk_c11) = sk_c12 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c7) = sk_c11 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_122,negated_conjecture,
( ( multiply(sk_c7,sk_c10) = sk_c11 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_123,negated_conjecture,
( ( multiply(sk_c8,sk_c9) = sk_c11 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c8) = sk_c9 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_125,negated_conjecture,
( ( multiply(sk_c9,sk_c10) = sk_c11 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c6) = sk_c12 )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c6,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c7) = sk_c11 )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c8,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c8) = sk_c9 )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_135,negated_conjecture,
( ( inverse(sk_c7) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_137,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c10 )
| ( multiply(sk_c8,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c8) = sk_c9 )
| ( multiply(sk_c2,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_139,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c7) = sk_c11 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_143,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c8,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_145,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( inverse(sk_c6) = sk_c12 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_148,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( multiply(sk_c6,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( inverse(sk_c7) = sk_c11 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_150,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( multiply(sk_c8,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_153,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_154,negated_conjecture,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(sk_c3,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_155,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c12 )
| ( multiply(sk_c6,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_156,negated_conjecture,
( ( inverse(sk_c7) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_157,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c12 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_158,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c12 )
| ( multiply(sk_c8,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_159,negated_conjecture,
( ( inverse(sk_c8) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_160,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c12 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_163,negated_conjecture,
( ( inverse(sk_c7) = sk_c11 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_165,negated_conjecture,
( ( multiply(sk_c4,sk_c5) = sk_c11 )
| ( multiply(sk_c8,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_166,negated_conjecture,
( ( inverse(sk_c8) = sk_c9 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_170,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c7) = sk_c11 ) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_172,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c8,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_175,negated_conjecture,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(sk_c5,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_176,negated_conjecture,
( ( multiply(sk_c5,sk_c10) = sk_c11 )
| ( multiply(sk_c6,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_177,negated_conjecture,
( ( inverse(sk_c7) = sk_c11 )
| ( multiply(sk_c5,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_178,negated_conjecture,
( ( multiply(sk_c5,sk_c10) = sk_c11 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_179,negated_conjecture,
( ( multiply(sk_c5,sk_c10) = sk_c11 )
| ( multiply(sk_c8,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_180,negated_conjecture,
( ( inverse(sk_c8) = sk_c9 )
| ( multiply(sk_c5,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_181,negated_conjecture,
( ( multiply(sk_c5,sk_c10) = sk_c11 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_182,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( inverse(X6) != sk_c11 )
| ( inverse(X5) != sk_c11 )
| ( inverse(X2) != sk_c12 )
| ( inverse(X1) != sk_c12 )
| ( inverse(X0) != sk_c12 )
| ( multiply(X6,sk_c11) != sk_c10 )
| ( multiply(X5,sk_c10) != sk_c11 )
| ( multiply(X2,sk_c11) != sk_c12 )
| ( multiply(X1,sk_c11) != sk_c12 )
| ( multiply(X0,sk_c12) != sk_c11 )
| ( multiply(inverse(X4),sk_c10) != sk_c11 )
| ( multiply(inverse(X3),sk_c10) != sk_c11 )
| ( multiply(X4,inverse(X4)) != sk_c11 )
| ( multiply(X3,inverse(X3)) != sk_c11 ) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_755,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c11) != sk_c12 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_182]) ).
tcf(c_756,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c12) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_182]) ).
tcf(c_757,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_182]) ).
tcf(c_758,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_182]) ).
tcf(c_759,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_182]) ).
tcf(c_760,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_182]) ).
tcf(c_761,definition,
iPr_def_15 = multiply(sk_c9,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_762,definition,
iPr_def_16 = multiply(sk_c5,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_763,definition,
iPr_def_17 = inverse(sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_764,definition,
iPr_def_18 = multiply(sk_c8,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_765,definition,
iPr_def_19 = multiply(sk_c7,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_766,definition,
iPr_def_20 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_767,definition,
iPr_def_21 = multiply(sk_c6,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_768,definition,
iPr_def_22 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_769,definition,
iPr_def_23 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_770,definition,
iPr_def_24 = multiply(sk_c4,sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_771,definition,
iPr_def_25 = multiply(sk_c3,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_772,definition,
iPr_def_26 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_773,definition,
iPr_def_27 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_774,definition,
iPr_def_28 = multiply(sk_c2,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_775,definition,
iPr_def_29 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_776,definition,
iPr_def_30 = multiply(sk_c1,sk_c12),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_777,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_760]) ).
tcf(c_779,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_759]) ).
tcf(c_780,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_758]) ).
tcf(c_781,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_757]) ).
tcf(c_782,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c12) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_756]) ).
tcf(c_784,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c11) != sk_c12 ) ),
inference(demodulation,[status(thm)],[c_755]) ).
tcf(c_785,negated_conjecture,
( ( iPr_def_16 = sk_c11 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_181,c_762,c_761]) ).
tcf(c_786,negated_conjecture,
( ( iPr_def_17 = sk_c9 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_180,c_763]) ).
tcf(c_787,negated_conjecture,
( ( iPr_def_18 = sk_c11 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_179,c_764]) ).
tcf(c_788,negated_conjecture,
( ( iPr_def_19 = sk_c11 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_178,c_765]) ).
tcf(c_789,negated_conjecture,
( ( iPr_def_20 = sk_c11 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_177,c_766]) ).
tcf(c_790,negated_conjecture,
( ( iPr_def_21 = sk_c12 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_176,c_767]) ).
tcf(c_791,negated_conjecture,
( ( iPr_def_22 = sk_c12 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_175,c_768]) ).
tcf(c_794,negated_conjecture,
( ( iPr_def_23 = sk_c5 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_172]) ).
tcf(c_796,negated_conjecture,
( ( iPr_def_23 = sk_c5 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_170]) ).
tcf(c_800,negated_conjecture,
( ( iPr_def_24 = sk_c11 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_166]) ).
tcf(c_801,negated_conjecture,
( ( iPr_def_24 = sk_c11 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_165]) ).
tcf(c_803,negated_conjecture,
( ( iPr_def_24 = sk_c11 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_163]) ).
tcf(c_806,negated_conjecture,
( ( iPr_def_25 = sk_c12 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_160,c_771]) ).
tcf(c_807,negated_conjecture,
( ( iPr_def_25 = sk_c12 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_159]) ).
tcf(c_808,negated_conjecture,
( ( iPr_def_25 = sk_c12 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_158]) ).
tcf(c_809,negated_conjecture,
( ( iPr_def_25 = sk_c12 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_157]) ).
tcf(c_810,negated_conjecture,
( ( iPr_def_25 = sk_c12 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_156]) ).
tcf(c_811,negated_conjecture,
( ( iPr_def_25 = sk_c12 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_155]) ).
tcf(c_812,negated_conjecture,
( ( iPr_def_25 = sk_c12 )
| ( iPr_def_22 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_154]) ).
tcf(c_813,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_153,c_772]) ).
tcf(c_815,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_151]) ).
tcf(c_816,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_150]) ).
tcf(c_817,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_149]) ).
tcf(c_818,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_148]) ).
tcf(c_819,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_22 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_147]) ).
tcf(c_820,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_146,c_773]) ).
tcf(c_821,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_145]) ).
tcf(c_822,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_144]) ).
tcf(c_823,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_143]) ).
tcf(c_824,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_827,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_139,c_774]) ).
tcf(c_828,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_138]) ).
tcf(c_829,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_830,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_831,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_135]) ).
tcf(c_834,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_132,c_775]) ).
tcf(c_835,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_836,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_837,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_838,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_128]) ).
tcf(c_839,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_840,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_22 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_841,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_125,c_776]) ).
tcf(c_842,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_843,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_844,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_845,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_846,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_847,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_22 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_1330,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(iPr_def_23,sk_c10) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_794,c_762]) ).
tcf(c_1347,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(sk_c8,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_786,c_764]) ).
tcf(c_1367,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_796,c_770]) ).
tcf(c_1369,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_794,c_770]) ).
tcf(c_1422,plain,
multiply(iPr_def_22,sk_c6) = identity,
inference(superposition,[status(thm)],[c_768,c_117]) ).
tcf(c_1423,plain,
multiply(iPr_def_20,sk_c7) = identity,
inference(superposition,[status(thm)],[c_766,c_117]) ).
tcf(c_1424,plain,
multiply(iPr_def_17,sk_c8) = identity,
inference(superposition,[status(thm)],[c_763,c_117]) ).
tcf(c_1425,plain,
multiply(iPr_def_29,sk_c1) = identity,
inference(superposition,[status(thm)],[c_775,c_117]) ).
tcf(c_1426,plain,
multiply(iPr_def_27,sk_c2) = identity,
inference(superposition,[status(thm)],[c_773,c_117]) ).
tcf(c_1427,plain,
multiply(iPr_def_26,sk_c3) = identity,
inference(superposition,[status(thm)],[c_772,c_117]) ).
tcf(c_1428,plain,
multiply(iPr_def_23,sk_c4) = identity,
inference(superposition,[status(thm)],[c_769,c_117]) ).
tcf(c_1433,plain,
( ( sk_c11 = iPr_def_24 )
| ( multiply(sk_c8,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_800,c_764]) ).
tcf(c_1447,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_24) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_801,c_774]) ).
tcf(c_1513,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_24) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_803,c_774]) ).
tcf(c_1581,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_806,c_776]) ).
tcf(c_1616,plain,
( ( sk_c12 = iPr_def_25 )
| ( multiply(sk_c8,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_807,c_764]) ).
tcf(c_1632,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_808,c_776]) ).
tcf(c_1682,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_809,c_776]) ).
tcf(c_1709,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_810,c_776]) ).
tcf(c_1736,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_811,c_776]) ).
tcf(c_1770,plain,
( ( sk_c12 = iPr_def_22 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_812,c_776]) ).
tcf(c_1817,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_813,c_776]) ).
tcf(c_1898,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_815,c_776]) ).
tcf(c_1951,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_816,c_776]) ).
tcf(c_2007,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_817,c_776]) ).
tcf(c_2054,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_818,c_776]) ).
tcf(c_2123,plain,
( ( sk_c12 = iPr_def_22 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_819,c_776]) ).
tcf(c_2221,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(sk_c8,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_821,c_764]) ).
tcf(c_2242,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_822,c_774]) ).
tcf(c_2303,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_823,c_774]) ).
tcf(c_2367,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_824,c_774]) ).
tcf(c_2604,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(sk_c7,iPr_def_28) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_827,c_765]) ).
tcf(c_2617,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(sk_c8,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_828,c_764]) ).
tcf(c_2633,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c7,iPr_def_28) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_829,c_765]) ).
tcf(c_2635,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c9,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_829,c_761]) ).
tcf(c_2653,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c7,iPr_def_28) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_830,c_765]) ).
tcf(c_2655,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c9,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_830,c_761]) ).
tcf(c_2672,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c7,iPr_def_28) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_831,c_765]) ).
tcf(c_2674,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c9,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_831,c_761]) ).
tcf(c_2763,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_834,c_776]) ).
tcf(c_2835,plain,
( ( sk_c12 = iPr_def_29 )
| ( multiply(sk_c8,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_835,c_764]) ).
tcf(c_2888,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_836,c_776]) ).
tcf(c_3017,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_837,c_776]) ).
tcf(c_3145,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_838,c_776]) ).
tcf(c_3492,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_841,c_774]) ).
tcf(c_3564,plain,
( ( sk_c11 = iPr_def_30 )
| ( multiply(sk_c8,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_842,c_764]) ).
tcf(c_3597,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_843,c_774]) ).
tcf(c_3683,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_844,c_774]) ).
tcf(c_3685,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c6,iPr_def_30) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_844,c_767]) ).
tcf(c_3777,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_845,c_774]) ).
tcf(c_3871,plain,
( ( sk_c11 = iPr_def_30 )
| ( multiply(sk_c1,iPr_def_21) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_846,c_776]) ).
tcf(c_4026,plain,
( ( sk_c11 = iPr_def_30 )
| ( multiply(sk_c1,iPr_def_22) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_847,c_776]) ).
tcf(c_4132,plain,
( ~ iPr_def_14
| ( sk_c10 != iPr_def_28 )
| ( inverse(sk_c2) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_774,c_779]) ).
tcf(c_4135,plain,
( ~ iPr_def_14
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_117,c_779]) ).
tcf(c_4159,plain,
( ~ iPr_def_14
| ( sk_c10 != iPr_def_28 )
| ( sk_c11 != iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_4132,c_773]) ).
tcf(c_4307,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_19 )
| ( inverse(sk_c7) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_765,c_781]) ).
tcf(c_4310,plain,
( ~ iPr_def_12
| ( sk_c11 != sk_c10 )
| ( inverse(identity) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_116,c_781]) ).
tcf(c_4327,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_20 )
| ( sk_c11 != iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_4307,c_766]) ).
tcf(c_4397,plain,
( ~ iPr_def_11
| ( sk_c11 != iPr_def_30 )
| ( inverse(sk_c1) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_776,c_782]) ).
tcf(c_4399,plain,
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( inverse(inverse(sk_c12)) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_117,c_782]) ).
tcf(c_4429,plain,
( ~ iPr_def_11
| ( sk_c11 != iPr_def_30 )
| ( sk_c12 != iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_4397,c_775]) ).
tcf(c_4754,plain,
( ~ iPr_def_10
| ( sk_c12 != iPr_def_21 )
| ( inverse(sk_c6) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_767,c_784]) ).
tcf(c_4756,plain,
( ~ iPr_def_10
| ( sk_c12 != iPr_def_25 )
| ( inverse(sk_c3) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_771,c_784]) ).
tcf(c_4778,plain,
( ~ iPr_def_10
| ( sk_c12 != iPr_def_26 )
| ( sk_c12 != iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_4756,c_772]) ).
tcf(c_4786,plain,
( ~ iPr_def_10
| ( sk_c12 != iPr_def_22 )
| ( sk_c12 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_4754,c_768]) ).
tcf(c_5052,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c10,X0)) = multiply(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_765,c_118]) ).
tcf(c_5054,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c10,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_761,c_118]) ).
tcf(c_5057,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c5,X0)) = multiply(iPr_def_24,X0),
inference(superposition,[status(thm)],[c_770,c_118]) ).
tcf(c_5060,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_117,c_118]) ).
tcf(c_5062,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1422,c_118]) ).
tcf(c_5063,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1423,c_118]) ).
tcf(c_5064,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c8,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1424,c_118]) ).
tcf(c_5065,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1425,c_118]) ).
tcf(c_5066,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1426,c_118]) ).
tcf(c_5067,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1427,c_118]) ).
tcf(c_5068,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1428,c_118]) ).
tcf(c_5074,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_5068,c_116]) ).
tcf(c_5075,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_5067,c_116]) ).
tcf(c_5076,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_5066,c_116]) ).
tcf(c_5077,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_5065,c_116]) ).
tcf(c_5078,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c8,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_5064,c_116]) ).
tcf(c_5079,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_5063,c_116]) ).
tcf(c_5080,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_5062,c_116]) ).
tcf(c_6318,plain,
( ~ iPr_def_13
| ( multiply(sk_c2,iPr_def_27) != sk_c11 )
| ( multiply(inverse(sk_c2),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_773,c_780]) ).
tcf(c_6332,plain,
( ~ iPr_def_13
| ( multiply(iPr_def_27,sk_c10) != sk_c11 )
| ( multiply(sk_c2,iPr_def_27) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_6318,c_773]) ).
tcf(c_15439,plain,
multiply(iPr_def_26,iPr_def_25) = sk_c11,
inference(superposition,[status(thm)],[c_771,c_5075]) ).
tcf(c_15442,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(iPr_def_25,X0)) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_15439,c_118]) ).
tcf(c_15444,plain,
multiply(iPr_def_27,iPr_def_28) = sk_c11,
inference(superposition,[status(thm)],[c_774,c_5076]) ).
tcf(c_15447,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(iPr_def_28,X0)) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_15444,c_118]) ).
tcf(c_15449,plain,
multiply(iPr_def_29,iPr_def_30) = sk_c12,
inference(superposition,[status(thm)],[c_776,c_5077]) ).
tcf(c_15828,plain,
multiply(iPr_def_17,iPr_def_18) = sk_c9,
inference(superposition,[status(thm)],[c_764,c_5078]) ).
tcf(c_15834,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(iPr_def_18,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_15828,c_118]) ).
tcf(c_15848,plain,
multiply(iPr_def_20,iPr_def_19) = sk_c10,
inference(superposition,[status(thm)],[c_765,c_5079]) ).
tcf(c_15851,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(iPr_def_19,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_15848,c_118]) ).
tcf(c_15853,plain,
multiply(iPr_def_22,iPr_def_21) = sk_c11,
inference(superposition,[status(thm)],[c_767,c_5080]) ).
tcf(c_16764,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1581,c_5077]) ).
tcf(c_16765,plain,
( ( sk_c11 = iPr_def_15 )
| ( sk_c12 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_16764,c_15449]) ).
tcf(c_16822,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1632,c_5077]) ).
tcf(c_16823,plain,
( ( sk_c11 = iPr_def_18 )
| ( sk_c12 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_16822,c_15449]) ).
tcf(c_16834,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1682,c_5077]) ).
tcf(c_16835,plain,
( ( sk_c11 = iPr_def_19 )
| ( sk_c12 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_16834,c_15449]) ).
tcf(c_16902,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1709,c_5077]) ).
tcf(c_16903,plain,
( ( sk_c11 = iPr_def_20 )
| ( sk_c12 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_16902,c_15449]) ).
tcf(c_16914,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1736,c_5077]) ).
tcf(c_16915,plain,
( ( sk_c12 = iPr_def_25 )
| ( sk_c12 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_16914,c_15449]) ).
tcf(c_17038,plain,
( ( sk_c12 = iPr_def_22 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1770,c_5077]) ).
tcf(c_17039,plain,
( ( sk_c12 = iPr_def_25 )
| ( sk_c12 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_17038,c_15449]) ).
tcf(c_17057,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1817,c_5077]) ).
tcf(c_17058,plain,
( ( sk_c11 = iPr_def_15 )
| ( sk_c12 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_17057,c_15449]) ).
tcf(c_17152,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1898,c_5077]) ).
tcf(c_17153,plain,
( ( sk_c11 = iPr_def_18 )
| ( sk_c12 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_17152,c_15449]) ).
tcf(c_17171,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1951,c_5077]) ).
tcf(c_17172,plain,
( ( sk_c11 = iPr_def_19 )
| ( sk_c12 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_17171,c_15449]) ).
tcf(c_17190,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2007,c_5077]) ).
tcf(c_17191,plain,
( ( sk_c11 = iPr_def_20 )
| ( sk_c12 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_17190,c_15449]) ).
tcf(c_17223,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2054,c_5077]) ).
tcf(c_17224,plain,
( ( sk_c12 = iPr_def_26 )
| ( sk_c12 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_17223,c_15449]) ).
tcf(c_17255,plain,
( ( sk_c12 = iPr_def_22 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2123,c_5077]) ).
tcf(c_17256,plain,
( ( sk_c12 = iPr_def_26 )
| ( sk_c12 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_17255,c_15449]) ).
tcf(c_17934,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_20,iPr_def_19) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2604,c_5079]) ).
tcf(c_17935,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c11 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_17934,c_15848]) ).
tcf(c_18031,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(iPr_def_20,iPr_def_19) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2633,c_5079]) ).
tcf(c_18032,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c11 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_18031,c_15848]) ).
tcf(c_18128,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(iPr_def_20,iPr_def_19) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2653,c_5079]) ).
tcf(c_18129,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c11 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_18128,c_15848]) ).
tcf(c_18263,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(iPr_def_20,iPr_def_19) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2672,c_5079]) ).
tcf(c_18264,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c11 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_18263,c_15848]) ).
tcf(c_18601,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_2763,c_5077]) ).
tcf(c_18602,plain,
( ( sk_c11 = iPr_def_15 )
| ( sk_c12 = iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_18601,c_15449]) ).
tcf(c_18794,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_2888,c_5077]) ).
tcf(c_18795,plain,
( ( sk_c11 = iPr_def_18 )
| ( sk_c12 = iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_18794,c_15449]) ).
tcf(c_18820,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_3017,c_5077]) ).
tcf(c_18821,plain,
( ( sk_c11 = iPr_def_19 )
| ( sk_c12 = iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_18820,c_15449]) ).
tcf(c_18846,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_3145,c_5077]) ).
tcf(c_18847,plain,
( ( sk_c11 = iPr_def_20 )
| ( sk_c12 = iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_18846,c_15449]) ).
tcf(c_18925,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3492,c_5076]) ).
tcf(c_18926,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c11 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_18925,c_15444]) ).
tcf(c_19061,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3597,c_5076]) ).
tcf(c_19062,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c11 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_19061,c_15444]) ).
tcf(c_19105,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3683,c_5076]) ).
tcf(c_19106,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c11 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_19105,c_15444]) ).
tcf(c_19149,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3777,c_5076]) ).
tcf(c_19150,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c11 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_19149,c_15444]) ).
tcf(c_19189,plain,
( ( sk_c11 = iPr_def_30 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_3871,c_5077]) ).
tcf(c_19190,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c12 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_19189,c_15449]) ).
tcf(c_19201,plain,
( ( sk_c11 = iPr_def_30 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_4026,c_5077]) ).
tcf(c_19202,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c12 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_19201,c_15449]) ).
tcf(c_20683,plain,
multiply(sk_c4,iPr_def_16) = multiply(iPr_def_24,sk_c10),
inference(superposition,[status(thm)],[c_762,c_5057]) ).
tcf(c_26854,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_5060,c_116]) ).
tcf(c_26871,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_116,c_26854]) ).
tcf(c_26872,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_117,c_26854]) ).
tcf(c_26873,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_118,c_26854]) ).
tcf(c_27094,plain,
! [X0: $i] : multiply(inverse(iPr_def_22),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_5080,c_26854]) ).
tcf(c_27095,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_5079,c_26854]) ).
tcf(c_27096,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_5078,c_26854]) ).
tcf(c_27097,plain,
! [X0: $i] : multiply(inverse(iPr_def_29),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_5077,c_26854]) ).
tcf(c_27098,plain,
! [X0: $i] : multiply(inverse(iPr_def_27),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_5076,c_26854]) ).
tcf(c_27100,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_5074,c_26854]) ).
tcf(c_27150,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_26854,c_26854]) ).
tcf(c_29578,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_26872,c_27150]) ).
tcf(c_29596,plain,
multiply(sk_c10,identity) = multiply(iPr_def_20,iPr_def_19),
inference(superposition,[status(thm)],[c_29578,c_15851]) ).
tcf(c_29600,plain,
multiply(sk_c9,identity) = multiply(iPr_def_17,iPr_def_18),
inference(superposition,[status(thm)],[c_29578,c_15834]) ).
tcf(c_29602,plain,
multiply(sk_c11,identity) = multiply(iPr_def_27,iPr_def_28),
inference(superposition,[status(thm)],[c_29578,c_15447]) ).
tcf(c_29603,plain,
multiply(sk_c11,identity) = multiply(iPr_def_26,iPr_def_25),
inference(superposition,[status(thm)],[c_29578,c_15442]) ).
tcf(c_29613,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_29578,c_26871]) ).
tcf(c_29616,plain,
multiply(sk_c11,identity) = sk_c11,
inference(light_normalisation,[status(thm)],[c_29603,c_15439]) ).
tcf(c_29619,plain,
multiply(sk_c9,identity) = sk_c9,
inference(light_normalisation,[status(thm)],[c_29600,c_15828]) ).
tcf(c_29623,plain,
multiply(sk_c10,identity) = sk_c10,
inference(light_normalisation,[status(thm)],[c_29596,c_15848]) ).
tcf(c_30190,plain,
multiply(identity,identity) = identity,
inference(superposition,[status(thm)],[c_29613,c_117]) ).
tcf(c_31095,plain,
( ( sk_c11 = iPr_def_20 )
| ~ iPr_def_14
| ( sk_c10 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_824,c_4159]) ).
tcf(c_31096,plain,
( ( sk_c11 = iPr_def_19 )
| ~ iPr_def_14
| ( sk_c10 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_823,c_4159]) ).
tcf(c_31097,plain,
( ( sk_c11 = iPr_def_18 )
| ~ iPr_def_14
| ( sk_c10 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_822,c_4159]) ).
tcf(c_31098,plain,
( ( sk_c11 = iPr_def_15 )
| ~ iPr_def_14
| ( sk_c10 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_820,c_4159]) ).
tcf(c_31608,plain,
( ( sk_c11 = iPr_def_20 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_31095,c_18264,c_31095]) ).
tcf(c_31614,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c11 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_777,c_31608]) ).
tcf(c_31620,plain,
( ( sk_c11 = iPr_def_19 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_31096,c_18129,c_31096]) ).
tcf(c_31626,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c11 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_777,c_31620]) ).
tcf(c_31647,plain,
( ( sk_c11 = iPr_def_18 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_31097,c_18032,c_31097]) ).
tcf(c_31653,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c11 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_777,c_31647]) ).
tcf(c_31659,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c11 = iPr_def_20 ) ),
inference(global_subsumption_just,[status(thm)],[c_31614,c_777,c_4429,c_4778,c_16903,c_17191,c_18264,c_18847,c_19150,c_31095]) ).
tcf(c_31667,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c11 = iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_31626,c_777,c_4429,c_4778,c_16835,c_17172,c_18129,c_18821,c_19106,c_31096]) ).
tcf(c_31675,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c11 = iPr_def_18 ) ),
inference(global_subsumption_just,[status(thm)],[c_31653,c_777,c_4429,c_4778,c_16823,c_17153,c_18795,c_19062,c_31647]) ).
tcf(c_31683,plain,
( ( sk_c11 = iPr_def_15 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_31098,c_17935,c_31098]) ).
tcf(c_31689,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c11 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_777,c_31683]) ).
tcf(c_31695,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c11 = iPr_def_15 ) ),
inference(global_subsumption_just,[status(thm)],[c_31689,c_777,c_4429,c_4778,c_16765,c_17058,c_17935,c_18602,c_18926,c_31098]) ).
tcf(c_33099,plain,
( ( sk_c12 = iPr_def_22 )
| ~ iPr_def_11
| ( sk_c11 != iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_840,c_4429]) ).
tcf(c_33100,plain,
( ( sk_c12 = iPr_def_21 )
| ~ iPr_def_11
| ( sk_c11 != iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_839,c_4429]) ).
tcf(c_33267,plain,
( ( sk_c12 = iPr_def_22 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_33099,c_19202,c_33099]) ).
tcf(c_33273,plain,
( ( sk_c12 = iPr_def_21 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_33100,c_19190,c_33100]) ).
tcf(c_33457,plain,
( ~ iPr_def_10
| ( sk_c12 != iPr_def_26 ) ),
inference(global_subsumption_just,[status(thm)],[c_4778,c_4786,c_4778,c_16915,c_17039]) ).
tcf(c_33459,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_33457,c_4786,c_17224,c_17256,c_33457]) ).
tcf(c_33461,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_777,c_33459]) ).
tcf(c_38457,plain,
multiply(sk_c6,iPr_def_22) = identity,
inference(superposition,[status(thm)],[c_27094,c_117]) ).
tcf(c_38461,plain,
! [X0: $i] : multiply(sk_c6,multiply(iPr_def_22,X0)) = X0,
inference(superposition,[status(thm)],[c_27094,c_26854]) ).
tcf(c_38462,plain,
multiply(sk_c6,identity) = inverse(iPr_def_22),
inference(superposition,[status(thm)],[c_27094,c_29578]) ).
tcf(c_40348,plain,
multiply(iPr_def_22,identity) = iPr_def_22,
inference(superposition,[status(thm)],[c_38457,c_5080]) ).
tcf(c_40357,plain,
inverse(iPr_def_22) = sk_c6,
inference(demodulation,[status(thm)],[c_38462,c_29578]) ).
tcf(c_40367,plain,
multiply(sk_c6,sk_c11) = iPr_def_21,
inference(superposition,[status(thm)],[c_15853,c_38461]) ).
tcf(c_40462,plain,
multiply(sk_c7,iPr_def_20) = identity,
inference(superposition,[status(thm)],[c_27095,c_117]) ).
tcf(c_40463,plain,
( ~ iPr_def_14
| ( inverse(inverse(iPr_def_20)) != sk_c11 )
| ( multiply(sk_c7,sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_27095,c_779]) ).
tcf(c_40467,plain,
multiply(sk_c7,identity) = inverse(iPr_def_20),
inference(superposition,[status(thm)],[c_27095,c_29578]) ).
tcf(c_40535,plain,
inverse(iPr_def_20) = sk_c7,
inference(demodulation,[status(thm)],[c_40467,c_29578]) ).
tcf(c_40538,plain,
( ~ iPr_def_13
| ( multiply(iPr_def_20,sk_c7) != sk_c11 )
| ( multiply(inverse(iPr_def_20),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_40535,c_780]) ).
tcf(c_40540,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_19 )
| ( sk_c11 != identity ) ),
inference(light_normalisation,[status(thm)],[c_40538,c_765,c_1423,c_40535]) ).
tcf(c_40574,plain,
multiply(sk_c8,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_27096,c_117]) ).
tcf(c_40578,plain,
! [X0: $i] : multiply(sk_c8,multiply(iPr_def_17,X0)) = X0,
inference(superposition,[status(thm)],[c_27096,c_26854]) ).
tcf(c_40592,plain,
( ( identity = iPr_def_18 )
| ( sk_c11 = iPr_def_30 ) ),
inference(demodulation,[status(thm)],[c_3564,c_40574]) ).
tcf(c_40593,plain,
( ( identity = iPr_def_18 )
| ( sk_c12 = iPr_def_29 ) ),
inference(demodulation,[status(thm)],[c_2835,c_40574]) ).
tcf(c_40594,plain,
( ( identity = iPr_def_18 )
| ( sk_c10 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_2617,c_40574]) ).
tcf(c_40595,plain,
( ( identity = iPr_def_18 )
| ( sk_c11 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_2221,c_40574]) ).
tcf(c_40597,plain,
( ( identity = iPr_def_18 )
| ( sk_c12 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_1616,c_40574]) ).
tcf(c_40598,plain,
( ( identity = iPr_def_18 )
| ( sk_c11 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_1433,c_40574]) ).
tcf(c_40599,plain,
( ( identity = iPr_def_18 )
| ( sk_c11 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1347,c_40574]) ).
tcf(c_41320,plain,
( ( identity = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_40593,c_776]) ).
tcf(c_41463,plain,
( ( identity = iPr_def_18 )
| ( multiply(sk_c9,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_40594,c_761]) ).
tcf(c_41517,plain,
multiply(sk_c8,sk_c9) = iPr_def_18,
inference(superposition,[status(thm)],[c_15828,c_40578]) ).
tcf(c_41673,plain,
( ( iPr_def_27 = iPr_def_30 )
| ( identity = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_40595,c_40592]) ).
tcf(c_41747,plain,
( ( identity = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_40595,c_774]) ).
tcf(c_42434,plain,
( ( iPr_def_25 = iPr_def_29 )
| ( identity = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_40597,c_40593]) ).
tcf(c_42435,plain,
( ( identity = iPr_def_18 )
| ~ iPr_def_11
| ( iPr_def_25 != iPr_def_29 )
| ( sk_c11 != iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_40597,c_4429]) ).
tcf(c_42607,plain,
( ( iPr_def_24 = iPr_def_27 )
| ( identity = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_40598,c_40595]) ).
tcf(c_42985,plain,
( ( iPr_def_16 = iPr_def_24 )
| ( identity = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_40599,c_40598]) ).
tcf(c_42986,plain,
( ( iPr_def_16 = iPr_def_27 )
| ( identity = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_40599,c_40595]) ).
tcf(c_42987,plain,
( ( iPr_def_16 = iPr_def_30 )
| ( identity = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_40599,c_40592]) ).
tcf(c_43772,plain,
( ( iPr_def_16 = iPr_def_27 )
| ( inverse(iPr_def_18) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_42986,c_29613]) ).
tcf(c_43926,plain,
( ( iPr_def_16 = iPr_def_30 )
| ( inverse(iPr_def_18) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_42987,c_29613]) ).
tcf(c_43993,plain,
multiply(sk_c1,iPr_def_29) = identity,
inference(superposition,[status(thm)],[c_27097,c_117]) ).
tcf(c_44047,plain,
( ( identity = iPr_def_30 )
| ( identity = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_41320,c_43993]) ).
tcf(c_44051,plain,
( ( identity = iPr_def_30 )
| ( sk_c11 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_3017,c_43993]) ).
tcf(c_45363,plain,
( ( identity = iPr_def_30 )
| ~ iPr_def_12
| ( sk_c11 != iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_44051,c_4327]) ).
tcf(c_47446,plain,
multiply(sk_c2,iPr_def_27) = identity,
inference(superposition,[status(thm)],[c_27098,c_117]) ).
tcf(c_47450,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_27,X0)) = X0,
inference(superposition,[status(thm)],[c_27098,c_26854]) ).
tcf(c_47487,plain,
( ( identity = iPr_def_28 )
| ( identity = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_41747,c_47446]) ).
tcf(c_47489,plain,
( ( identity = iPr_def_28 )
| ( sk_c11 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_2367,c_47446]) ).
tcf(c_47490,plain,
( ( identity = iPr_def_28 )
| ( sk_c11 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_2303,c_47446]) ).
tcf(c_47491,plain,
( ( identity = iPr_def_28 )
| ( sk_c11 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_2242,c_47446]) ).
tcf(c_47773,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( identity = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_47487,c_44047]) ).
tcf(c_48347,plain,
multiply(sk_c2,sk_c11) = iPr_def_28,
inference(superposition,[status(thm)],[c_15444,c_47450]) ).
tcf(c_48587,plain,
( ( identity = iPr_def_28 )
| ~ iPr_def_12
| ( sk_c11 != iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_47490,c_4327]) ).
tcf(c_49688,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( inverse(iPr_def_18) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_47773,c_29613]) ).
tcf(c_69530,plain,
multiply(sk_c4,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_27100,c_117]) ).
tcf(c_69534,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_23,X0)) = X0,
inference(superposition,[status(thm)],[c_27100,c_26854]) ).
tcf(c_69535,plain,
multiply(sk_c4,identity) = inverse(iPr_def_23),
inference(superposition,[status(thm)],[c_27100,c_29578]) ).
tcf(c_69550,plain,
( ( identity = iPr_def_24 )
| ( sk_c11 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_1369,c_69530]) ).
tcf(c_69552,plain,
( ( identity = iPr_def_24 )
| ( sk_c11 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_1367,c_69530]) ).
tcf(c_69603,plain,
inverse(iPr_def_23) = sk_c4,
inference(demodulation,[status(thm)],[c_69535,c_29578]) ).
tcf(c_69606,plain,
( ~ iPr_def_13
| ( multiply(iPr_def_23,sk_c4) != sk_c11 )
| ( multiply(inverse(iPr_def_23),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_69603,c_780]) ).
tcf(c_69608,plain,
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( multiply(sk_c4,sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_69606,c_1428,c_69603]) ).
tcf(c_70986,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c4,iPr_def_16) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_1330,c_69534]) ).
tcf(c_71034,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(iPr_def_24,sk_c10) = sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_70986,c_20683]) ).
tcf(c_73498,plain,
( ( iPr_def_16 = iPr_def_27 )
| ( multiply(iPr_def_18,iPr_def_18) = identity ) ),
inference(superposition,[status(thm)],[c_43772,c_117]) ).
tcf(c_73738,plain,
( ( iPr_def_16 = iPr_def_30 )
| ( multiply(iPr_def_18,iPr_def_18) = identity ) ),
inference(superposition,[status(thm)],[c_43926,c_117]) ).
tcf(c_82643,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( multiply(iPr_def_18,iPr_def_18) = identity ) ),
inference(superposition,[status(thm)],[c_49688,c_117]) ).
tcf(c_105436,plain,
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( sk_c11 != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_4310,c_29613]) ).
tcf(c_105482,plain,
( ( identity = iPr_def_18 )
| ~ iPr_def_12
| ( identity != iPr_def_30 )
| ( sk_c11 != sk_c10 ) ),
inference(superposition,[status(thm)],[c_40592,c_105436]) ).
tcf(c_105552,plain,
( ( sk_c11 = iPr_def_18 )
| ~ iPr_def_12
| ( identity != iPr_def_24 )
| ( sk_c11 != sk_c10 ) ),
inference(superposition,[status(thm)],[c_801,c_105436]) ).
tcf(c_107373,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_21)) = sk_c11,
inference(superposition,[status(thm)],[c_40367,c_26873]) ).
tcf(c_107379,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c9)),multiply(X0,iPr_def_15)) = sk_c10,
inference(superposition,[status(thm)],[c_761,c_26873]) ).
tcf(c_107380,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c2)),multiply(X0,iPr_def_28)) = sk_c11,
inference(superposition,[status(thm)],[c_48347,c_26873]) ).
tcf(c_107494,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_20 )
| ( multiply(inverse(multiply(X0,sk_c2)),multiply(X0,iPr_def_28)) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1513,c_26873]) ).
tcf(c_107496,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_18 )
| ( multiply(inverse(multiply(X0,sk_c2)),multiply(X0,iPr_def_28)) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1447,c_26873]) ).
tcf(c_107600,plain,
! [X0: $i] :
( ( identity = iPr_def_18 )
| ( multiply(inverse(multiply(X0,sk_c9)),multiply(X0,iPr_def_15)) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_41463,c_26873]) ).
tcf(c_107603,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_20 )
| ( multiply(inverse(multiply(X0,sk_c9)),multiply(X0,iPr_def_15)) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2674,c_26873]) ).
tcf(c_107604,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_19 )
| ( multiply(inverse(multiply(X0,sk_c9)),multiply(X0,iPr_def_15)) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2655,c_26873]) ).
tcf(c_107605,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_18 )
| ( multiply(inverse(multiply(X0,sk_c9)),multiply(X0,iPr_def_15)) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2635,c_26873]) ).
tcf(c_107623,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_19 )
| ( multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_21)) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3685,c_26873]) ).
tcf(c_107715,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c7)),multiply(X0,identity)) = iPr_def_20,
inference(superposition,[status(thm)],[c_40462,c_26873]) ).
tcf(c_107853,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c7)),X0) = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_107715,c_29578]) ).
tcf(c_119900,plain,
multiply(inverse(multiply(inverse(iPr_def_15),sk_c9)),identity) = sk_c10,
inference(superposition,[status(thm)],[c_117,c_107379]) ).
tcf(c_121303,plain,
( ~ iPr_def_11
| ( sk_c11 != iPr_def_20 )
| ( inverse(inverse(multiply(sk_c12,sk_c7))) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_107853,c_782]) ).
tcf(c_121310,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_20 )
| ( inverse(inverse(multiply(sk_c10,sk_c7))) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_107853,c_781]) ).
tcf(c_121703,plain,
inverse(multiply(inverse(iPr_def_15),sk_c9)) = sk_c10,
inference(demodulation,[status(thm)],[c_119900,c_29578]) ).
tcf(c_121722,plain,
( ~ iPr_def_13
| ( multiply(multiply(inverse(iPr_def_15),sk_c9),sk_c10) != sk_c11 )
| ( multiply(inverse(multiply(inverse(iPr_def_15),sk_c9)),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_121703,c_780]) ).
tcf(c_121723,plain,
multiply(sk_c10,multiply(inverse(iPr_def_15),sk_c9)) = identity,
inference(superposition,[status(thm)],[c_121703,c_117]) ).
tcf(c_121744,plain,
( ~ iPr_def_13
| ( multiply(sk_c10,sk_c10) != sk_c11 )
| ( multiply(multiply(inverse(iPr_def_15),sk_c9),sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_121722,c_121703]) ).
tcf(c_122033,plain,
multiply(iPr_def_15,multiply(inverse(iPr_def_15),sk_c9)) = multiply(sk_c9,identity),
inference(superposition,[status(thm)],[c_121723,c_5054]) ).
tcf(c_122034,plain,
multiply(iPr_def_19,multiply(inverse(iPr_def_15),sk_c9)) = multiply(sk_c7,identity),
inference(superposition,[status(thm)],[c_121723,c_5052]) ).
tcf(c_147986,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_122034,c_122033,c_121744,c_121310,c_121303,c_107623,c_107605,c_107604,c_107603,c_107600,c_107496,c_107494,c_107380,c_107379,c_107373,c_105552,c_105482,c_105436,c_82643,c_73738,c_73498,c_71034,c_69608,c_69552,c_69550,c_48587,c_48347,c_47491,c_47489,c_47446,c_45363,c_44047,c_42985,c_42607,c_42435,c_42434,c_41673,c_41517,c_40574,c_40540,c_40535,c_40463,c_40467,c_40462,c_40367,c_40357,c_40348,c_38462,c_33461,c_33273,c_33267,c_31695,c_31675,c_31667,c_31659,c_29623,c_29619,c_29616,c_29602,c_29596,c_29613,c_20683,c_6332,c_4399,c_4327,c_4135,c_30190,c_3564,c_791,c_790,c_789,c_788,c_787,c_786,c_785,c_768,c_766]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP243-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.09/0.35 % Computer : n008.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 14:15:29 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 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.14/0.40
% 0.14/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.40
% 0.14/0.40 % Detected problem language: tptp
% 0.14/0.41 % Proving...
% 26.28/4.30 % SZS status Started for theBenchmark.p
% 26.28/4.30 % SZS status Unsatisfiable for theBenchmark.p
% 26.28/4.30
% 26.28/4.30 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 26.28/4.30
% 26.28/4.30 % ------ iProver source info
% 26.28/4.30
% 26.28/4.30 % git: date: 2026-07-19 20:42:38 +0200
% 26.28/4.30 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 26.28/4.30 % git: non_committed_changes: false
% 26.28/4.30
% 26.28/4.30 % ------ Parsing...% successful
% 26.28/4.30
% 26.28/4.30
% 26.28/4.30 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 26.28/4.30
% 26.28/4.30 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 26.28/4.30
% 26.28/4.30 % ------ Preprocessing... gs_s sp: 7 0s gs_e snvd_s sp: 0 0s snvd_e %
% 26.28/4.30
% 26.28/4.30 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 26.28/4.30 % ------ Proving...
% 26.28/4.30 % ------ Problem Properties
% 26.28/4.30
% 26.28/4.30 %
% 26.28/4.30 % clauses 88
% 26.28/4.30 % conjectures 69
% 26.28/4.30 % EPR 64
% 26.28/4.30 % Horn 24
% 26.28/4.30 % unary 19
% 26.28/4.30 % binary 63
% 26.28/4.30 % lits 165
% 26.28/4.30 % lits eq 155
% 26.28/4.30 % fd_pure 0
% 26.28/4.30 % fd_pseudo 0
% 26.28/4.30 % fd_cond 0
% 26.28/4.30 % fd_pseudo_cond 0
% 26.28/4.30 % AC symbols 0
% 26.28/4.30
% 26.28/4.30 % ------ Schedule dynamic 5 is on
% 26.28/4.30
% 26.28/4.30 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 26.28/4.30
% 26.28/4.30
% 26.28/4.30 % ------
% 26.28/4.30 % Current options:
% 26.28/4.30 % ------
% 26.28/4.30
% 26.28/4.30
% 26.28/4.30 %
% 26.28/4.30
% 26.28/4.30 % ------ Proving...
% 26.28/4.30 %
% 26.28/4.30
% 26.28/4.30 % SZS status Unsatisfiable for theBenchmark.p
% 26.28/4.30
% 26.28/4.30 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 26.28/4.31
% 26.28/4.31
%------------------------------------------------------------------------------