%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP246-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n001.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:27 PM UTC 2026
% Result : Unsatisfiable 25.51s 5.31s
% Output : CNFRefutation 25.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 50
% Syntax : Number of formulae : 400 ( 110 unt; 14 def)
% Number of atoms : 1320 ( 722 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 610 ( 210 ~; 400 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 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 : 21 ( 19 usr; 20 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 104 ( 0 sgn 104 !; 0 ?; 75 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c4,sk_c11) = sk_c10
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c4,sk_c11)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c4) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c4)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c5,sk_c10) = sk_c9
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f22,negated_conjecture,
( multiply(sk_c4,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f23,plain,
( sk_c10 = multiply(sk_c4,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
( inverse(sk_c4) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c11 = inverse(sk_c4)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f24]) ).
fof(f28,negated_conjecture,
( inverse(sk_c5) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f29,plain,
( sk_c10 = inverse(sk_c5)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f28]) ).
fof(f30,negated_conjecture,
( inverse(sk_c6) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f31,plain,
( sk_c11 = inverse(sk_c6)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f32]) ).
fof(f42,negated_conjecture,
( inverse(sk_c4) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_20) ).
fof(f43,plain,
( sk_c11 = inverse(sk_c4)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f42]) ).
fof(f44,negated_conjecture,
( multiply(sk_c5,sk_c10) = sk_c9
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f45,plain,
( multiply(sk_c5,sk_c10) = sk_c9
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
( inverse(sk_c5) = sk_c10
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f47,plain,
( sk_c10 = inverse(sk_c5)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f46]) ).
fof(f48,negated_conjecture,
( inverse(sk_c6) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_23) ).
fof(f49,plain,
( sk_c11 = inverse(sk_c6)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f48]) ).
fof(f50,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f51,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f50]) ).
fof(f54,negated_conjecture,
( inverse(sk_c7) = sk_c8
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f55,plain,
( sk_c8 = inverse(sk_c7)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f54]) ).
fof(f56,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c10
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_27) ).
fof(f57,plain,
( sk_c10 = multiply(sk_c8,sk_c9)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f56]) ).
fof(f60,negated_conjecture,
( inverse(sk_c4) = sk_c11
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_29) ).
fof(f61,plain,
( sk_c11 = inverse(sk_c4)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f60]) ).
fof(f62,negated_conjecture,
( multiply(sk_c5,sk_c10) = sk_c9
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f63,plain,
( multiply(sk_c5,sk_c10) = sk_c9
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f62]) ).
fof(f64,negated_conjecture,
( inverse(sk_c5) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f65,plain,
( sk_c10 = inverse(sk_c5)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f64]) ).
fof(f66,negated_conjecture,
( inverse(sk_c6) = sk_c11
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f67,plain,
( sk_c11 = inverse(sk_c6)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f66]) ).
fof(f68,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_33) ).
fof(f69,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f68]) ).
fof(f74,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f75,plain,
( sk_c10 = multiply(sk_c8,sk_c9)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f74]) ).
fof(f78,negated_conjecture,
( inverse(sk_c4) = sk_c11
| inverse(sk_c3) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_38) ).
fof(f79,plain,
( sk_c11 = inverse(sk_c4)
| sk_c11 = inverse(sk_c3) ),
inference(reorient_equations,[],[f78]) ).
fof(f80,negated_conjecture,
( multiply(sk_c5,sk_c10) = sk_c9
| inverse(sk_c3) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_39) ).
fof(f81,plain,
( multiply(sk_c5,sk_c10) = sk_c9
| sk_c11 = inverse(sk_c3) ),
inference(reorient_equations,[],[f80]) ).
fof(f82,negated_conjecture,
( inverse(sk_c5) = sk_c10
| inverse(sk_c3) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_40) ).
fof(f83,plain,
( sk_c10 = inverse(sk_c5)
| sk_c11 = inverse(sk_c3) ),
inference(reorient_equations,[],[f82]) ).
fof(f84,negated_conjecture,
( inverse(sk_c6) = sk_c11
| inverse(sk_c3) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_41) ).
fof(f85,plain,
( sk_c11 = inverse(sk_c6)
| sk_c11 = inverse(sk_c3) ),
inference(reorient_equations,[],[f84]) ).
fof(f86,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| inverse(sk_c3) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_42) ).
fof(f87,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c11 = inverse(sk_c3) ),
inference(reorient_equations,[],[f86]) ).
fof(f94,negated_conjecture,
( multiply(sk_c4,sk_c11) = sk_c10
| multiply(sk_c3,sk_c9) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_46) ).
fof(f95,plain,
( sk_c10 = multiply(sk_c4,sk_c11)
| sk_c11 = multiply(sk_c3,sk_c9) ),
inference(reorient_equations,[],[f94]) ).
fof(f96,negated_conjecture,
( inverse(sk_c4) = sk_c11
| multiply(sk_c3,sk_c9) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_47) ).
fof(f97,plain,
( sk_c11 = inverse(sk_c4)
| sk_c11 = multiply(sk_c3,sk_c9) ),
inference(reorient_equations,[],[f96]) ).
fof(f98,negated_conjecture,
( multiply(sk_c5,sk_c10) = sk_c9
| multiply(sk_c3,sk_c9) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_48) ).
fof(f99,plain,
( multiply(sk_c5,sk_c10) = sk_c9
| sk_c11 = multiply(sk_c3,sk_c9) ),
inference(reorient_equations,[],[f98]) ).
fof(f100,negated_conjecture,
( inverse(sk_c5) = sk_c10
| multiply(sk_c3,sk_c9) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_49) ).
fof(f101,plain,
( sk_c10 = inverse(sk_c5)
| sk_c11 = multiply(sk_c3,sk_c9) ),
inference(reorient_equations,[],[f100]) ).
fof(f102,negated_conjecture,
( inverse(sk_c6) = sk_c11
| multiply(sk_c3,sk_c9) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_50) ).
fof(f103,plain,
( sk_c11 = inverse(sk_c6)
| sk_c11 = multiply(sk_c3,sk_c9) ),
inference(reorient_equations,[],[f102]) ).
fof(f104,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| multiply(sk_c3,sk_c9) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_51) ).
fof(f105,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c11 = multiply(sk_c3,sk_c9) ),
inference(reorient_equations,[],[f104]) ).
fof(f112,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X7,sk_c9) != sk_c10
| inverse(X6) != X7
| multiply(X6,X7) != sk_c10
| multiply(X5,sk_c10) != sk_c11
| inverse(X5) != sk_c11
| inverse(X4) != sk_c10
| multiply(X4,sk_c10) != sk_c9
| inverse(X3) != sk_c11
| multiply(X3,sk_c11) != sk_c10
| multiply(X2,sk_c9) != sk_c11
| inverse(X2) != sk_c11
| inverse(X1) != sk_c10
| multiply(X1,sk_c10) != sk_c9
| inverse(X0) != sk_c11
| multiply(X0,sk_c11) != sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_55) ).
fof(f113,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( sk_c10 != multiply(X7,sk_c9)
| inverse(X6) != X7
| sk_c10 != multiply(X6,X7)
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c10 != inverse(X4)
| sk_c9 != multiply(X4,sk_c10)
| sk_c11 != inverse(X3)
| sk_c10 != multiply(X3,sk_c11)
| sk_c11 != multiply(X2,sk_c9)
| sk_c11 != inverse(X2)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(reorient_equations,[],[f112]) ).
fof(f114,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( sk_c10 != multiply(inverse(X6),sk_c9)
| sk_c10 != multiply(X6,inverse(X6))
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c10 != inverse(X4)
| sk_c9 != multiply(X4,sk_c10)
| sk_c11 != inverse(X3)
| sk_c10 != multiply(X3,sk_c11)
| sk_c11 != multiply(X2,sk_c9)
| sk_c11 != inverse(X2)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(equality_resolution,[],[f113]) ).
tcf(c_107,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_108,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_110,negated_conjecture,
( ( multiply(sk_c4,sk_c11) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_112,negated_conjecture,
( ( multiply(sk_c5,sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_120,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c5) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c6) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c5,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c5) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c6) = sk_c11 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_133,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_135,negated_conjecture,
( ( inverse(sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c5,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_140,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c5) = sk_c10 ) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c6) = sk_c11 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_145,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c8,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_148,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c5,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c5) = sk_c10 ) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_150,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c6) = sk_c11 ) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_155,negated_conjecture,
( ( multiply(sk_c3,sk_c9) = sk_c11 )
| ( multiply(sk_c4,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_156,negated_conjecture,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c3,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_157,negated_conjecture,
( ( multiply(sk_c3,sk_c9) = sk_c11 )
| ( multiply(sk_c5,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_158,negated_conjecture,
( ( inverse(sk_c5) = sk_c10 )
| ( multiply(sk_c3,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_159,negated_conjecture,
( ( inverse(sk_c6) = sk_c11 )
| ( multiply(sk_c3,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_160,negated_conjecture,
( ( multiply(sk_c3,sk_c9) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_164,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( inverse(X6) != sk_c10 )
| ( inverse(X5) != sk_c10 )
| ( inverse(X3) != sk_c11 )
| ( inverse(X2) != sk_c11 )
| ( inverse(X1) != sk_c11 )
| ( inverse(X0) != sk_c11 )
| ( multiply(X6,sk_c10) != sk_c9 )
| ( multiply(X5,sk_c10) != sk_c9 )
| ( multiply(X3,sk_c11) != sk_c10 )
| ( multiply(X2,sk_c9) != sk_c11 )
| ( multiply(X1,sk_c10) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 )
| ( multiply(inverse(X4),sk_c9) != sk_c10 )
| ( multiply(X4,inverse(X4)) != sk_c10 ) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_665,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c9) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_164]) ).
tcf(c_666,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_164]) ).
tcf(c_667,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_164]) ).
tcf(c_668,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_164]) ).
tcf(c_669,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( multiply(inverse(X0),sk_c9) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_164]) ).
tcf(c_670,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_164]) ).
tcf(c_671,definition,
iPr_def_15 = multiply(sk_c8,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_672,definition,
iPr_def_16 = multiply(sk_c3,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_673,definition,
iPr_def_17 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_675,definition,
iPr_def_19 = multiply(sk_c6,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_676,definition,
iPr_def_20 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_677,definition,
iPr_def_21 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_678,definition,
iPr_def_22 = multiply(sk_c5,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_679,definition,
iPr_def_23 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_680,definition,
iPr_def_24 = multiply(sk_c4,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_681,definition,
iPr_def_25 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_682,definition,
iPr_def_26 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_683,definition,
iPr_def_27 = multiply(sk_c2,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_684,definition,
iPr_def_28 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_685,definition,
iPr_def_29 = multiply(sk_c1,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_686,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_670]) ).
tcf(c_687,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( multiply(inverse(X0),sk_c9) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_669]) ).
tcf(c_690,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_668]) ).
tcf(c_691,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_667]) ).
tcf(c_692,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_666]) ).
tcf(c_693,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c9) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_665]) ).
tcf(c_697,negated_conjecture,
( ( iPr_def_19 = sk_c11 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_160,c_675]) ).
tcf(c_698,negated_conjecture,
( ( iPr_def_20 = sk_c11 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_159,c_676]) ).
tcf(c_699,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_158,c_677]) ).
tcf(c_700,negated_conjecture,
( ( iPr_def_22 = sk_c9 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_157,c_678]) ).
tcf(c_701,negated_conjecture,
( ( iPr_def_23 = sk_c11 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_156,c_679]) ).
tcf(c_702,negated_conjecture,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_155,c_680]) ).
tcf(c_706,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_151]) ).
tcf(c_707,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_150]) ).
tcf(c_708,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_149]) ).
tcf(c_709,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_148]) ).
tcf(c_710,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_23 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_147]) ).
tcf(c_712,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_145,c_682]) ).
tcf(c_715,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_716,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_717,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_140]) ).
tcf(c_718,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_139]) ).
tcf(c_719,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_23 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_138]) ).
tcf(c_721,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_136,c_683]) ).
tcf(c_722,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_17 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_135]) ).
tcf(c_724,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_133]) ).
tcf(c_725,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_132]) ).
tcf(c_726,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_727,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_728,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_23 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_733,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_19 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_734,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_735,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_737,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_23 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_738,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_24 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_745,negated_conjecture,
( ( iPr_def_29 = sk_c10 )
| ( iPr_def_22 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_746,negated_conjecture,
( ( iPr_def_29 = sk_c10 )
| ( iPr_def_23 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_111]) ).
tcf(c_747,negated_conjecture,
( ( iPr_def_29 = sk_c10 )
| ( iPr_def_24 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_1367,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(sk_c3,iPr_def_22) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_700,c_672]) ).
tcf(c_1413,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_707,c_685]) ).
tcf(c_1414,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_706,c_685]) ).
tcf(c_1418,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_701,c_685]) ).
tcf(c_1420,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_698,c_685]) ).
tcf(c_1421,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_19) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_697,c_685]) ).
tcf(c_1459,plain,
multiply(iPr_def_23,sk_c4) = identity,
inference(superposition,[status(thm)],[c_679,c_108]) ).
tcf(c_1460,plain,
multiply(iPr_def_21,sk_c5) = identity,
inference(superposition,[status(thm)],[c_677,c_108]) ).
tcf(c_1461,plain,
multiply(iPr_def_20,sk_c6) = identity,
inference(superposition,[status(thm)],[c_676,c_108]) ).
tcf(c_1462,plain,
multiply(iPr_def_17,sk_c7) = identity,
inference(superposition,[status(thm)],[c_673,c_108]) ).
tcf(c_1463,plain,
multiply(iPr_def_28,sk_c1) = identity,
inference(superposition,[status(thm)],[c_684,c_108]) ).
tcf(c_1464,plain,
multiply(iPr_def_26,sk_c2) = identity,
inference(superposition,[status(thm)],[c_682,c_108]) ).
tcf(c_1465,plain,
multiply(iPr_def_25,sk_c3) = identity,
inference(superposition,[status(thm)],[c_681,c_108]) ).
tcf(c_1504,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(sk_c3,iPr_def_22) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_709,c_672]) ).
tcf(c_1521,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_710,c_685]) ).
tcf(c_1585,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_712,c_683]) ).
tcf(c_1744,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_716,c_685]) ).
tcf(c_1832,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_717,c_683]) ).
tcf(c_1845,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(sk_c3,iPr_def_22) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_718,c_672]) ).
tcf(c_1890,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_719,c_685]) ).
tcf(c_1992,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_721,c_672]) ).
tcf(c_2020,plain,
( ( sk_c9 = iPr_def_27 )
| ( multiply(iPr_def_17,sk_c9) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_722,c_671]) ).
tcf(c_2065,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_724,c_672]) ).
tcf(c_2096,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_725,c_672]) ).
tcf(c_2127,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_726,c_672]) ).
tcf(c_2164,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_727,c_672]) ).
tcf(c_2199,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(sk_c8,iPr_def_27) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_728,c_671]) ).
tcf(c_2501,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_733,c_685]) ).
tcf(c_2505,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( sk_c11 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_733,c_706]) ).
tcf(c_2650,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c1,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_734,c_685]) ).
tcf(c_2774,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_735,c_685]) ).
tcf(c_2776,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( sk_c10 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_735,c_708]) ).
tcf(c_2989,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( sk_c11 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_737,c_710]) ).
tcf(c_2990,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_737,c_685]) ).
tcf(c_2991,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(sk_c4,iPr_def_28) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_737,c_680]) ).
tcf(c_3117,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(sk_c1,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_738,c_685]) ).
tcf(c_3826,plain,
( ( sk_c10 = iPr_def_29 )
| ( multiply(sk_c1,iPr_def_23) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_746,c_685]) ).
tcf(c_4007,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(sk_c2,iPr_def_29) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_747,c_683]) ).
tcf(c_4037,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_108,c_109]) ).
tcf(c_4039,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1459,c_109]) ).
tcf(c_4040,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1460,c_109]) ).
tcf(c_4041,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1461,c_109]) ).
tcf(c_4042,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1462,c_109]) ).
tcf(c_4043,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1463,c_109]) ).
tcf(c_4044,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1464,c_109]) ).
tcf(c_4045,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1465,c_109]) ).
tcf(c_4047,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4045,c_107]) ).
tcf(c_4048,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4044,c_107]) ).
tcf(c_4049,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4043,c_107]) ).
tcf(c_4050,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4042,c_107]) ).
tcf(c_4051,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4041,c_107]) ).
tcf(c_4052,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4040,c_107]) ).
tcf(c_4053,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4039,c_107]) ).
tcf(c_4728,plain,
( ~ iPr_def_13
| ( sk_c9 != iPr_def_22 )
| ( inverse(sk_c5) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_678,c_690]) ).
tcf(c_4730,plain,
( ~ iPr_def_13
| ( sk_c9 != iPr_def_27 )
| ( inverse(sk_c2) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_683,c_690]) ).
tcf(c_4747,plain,
( ~ iPr_def_13
| ( sk_c9 != iPr_def_27 )
| ( sk_c10 != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_4730,c_682]) ).
tcf(c_4755,plain,
( ~ iPr_def_13
| ( sk_c9 != iPr_def_22 )
| ( sk_c10 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_4728,c_677]) ).
tcf(c_4909,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_19 )
| ( inverse(sk_c6) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_675,c_691]) ).
tcf(c_4931,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_20 )
| ( sk_c11 != iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_4909,c_676]) ).
tcf(c_5036,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_29 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_685,c_692]) ).
tcf(c_5037,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_24 )
| ( inverse(sk_c4) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_680,c_692]) ).
tcf(c_5074,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_24 )
| ( sk_c11 != iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_5037,c_679]) ).
tcf(c_5078,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_29 )
| ( sk_c11 != iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_5036,c_684]) ).
tcf(c_5318,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_16 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_672,c_693]) ).
tcf(c_5338,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_25 )
| ( sk_c11 != iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_5318,c_681]) ).
tcf(c_5418,plain,
( ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 )
| ( multiply(sk_c3,sk_c9) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_5475,plain,
( ~ iPr_def_10
| ( inverse(sk_c4) != sk_c11 )
| ( multiply(sk_c4,sk_c9) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_5491,plain,
( ~ iPr_def_14
| ( inverse(identity) != sk_c10 )
| ( multiply(inverse(identity),sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_107,c_687]) ).
tcf(c_5496,plain,
( ~ iPr_def_14
| ( multiply(sk_c7,iPr_def_17) != sk_c10 )
| ( multiply(inverse(sk_c7),sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_673,c_687]) ).
tcf(c_5498,plain,
( ~ iPr_def_14
| ( multiply(sk_c2,iPr_def_26) != sk_c10 )
| ( multiply(inverse(sk_c2),sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_682,c_687]) ).
tcf(c_5507,plain,
( ~ iPr_def_14
| ( multiply(iPr_def_26,sk_c9) != sk_c10 )
| ( multiply(sk_c2,iPr_def_26) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_5498,c_682]) ).
tcf(c_5515,plain,
( ~ iPr_def_14
| ( multiply(iPr_def_17,sk_c9) != sk_c10 )
| ( multiply(sk_c7,iPr_def_17) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_5496,c_673]) ).
tcf(c_6985,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( multiply(sk_c5,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_2776,c_678]) ).
tcf(c_7251,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_2989,c_680]) ).
tcf(c_9038,plain,
multiply(iPr_def_25,iPr_def_16) = sk_c9,
inference(superposition,[status(thm)],[c_672,c_4047]) ).
tcf(c_9063,plain,
multiply(iPr_def_26,iPr_def_27) = sk_c10,
inference(superposition,[status(thm)],[c_683,c_4048]) ).
tcf(c_9097,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(iPr_def_27,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_9063,c_109]) ).
tcf(c_9302,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(iPr_def_25,iPr_def_16) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_1367,c_4047]) ).
tcf(c_9303,plain,
( ( sk_c9 = iPr_def_22 )
| ( sk_c11 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_9302,c_9038]) ).
tcf(c_9479,plain,
multiply(iPr_def_28,iPr_def_29) = sk_c11,
inference(superposition,[status(thm)],[c_685,c_4049]) ).
tcf(c_9482,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(iPr_def_29,X0)) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_9479,c_109]) ).
tcf(c_9530,plain,
multiply(iPr_def_20,iPr_def_19) = sk_c10,
inference(superposition,[status(thm)],[c_675,c_4051]) ).
tcf(c_9535,plain,
multiply(iPr_def_21,iPr_def_22) = sk_c10,
inference(superposition,[status(thm)],[c_678,c_4052]) ).
tcf(c_9538,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(iPr_def_22,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_9535,c_109]) ).
tcf(c_9811,plain,
multiply(iPr_def_23,iPr_def_24) = sk_c11,
inference(superposition,[status(thm)],[c_680,c_4053]) ).
tcf(c_9897,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(iPr_def_24,X0)) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_9811,c_109]) ).
tcf(c_10048,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1413,c_4049]) ).
tcf(c_10049,plain,
( ( sk_c11 = iPr_def_25 )
| ( sk_c11 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_10048,c_9479]) ).
tcf(c_10076,plain,
( ( sk_c11 = iPr_def_19 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1414,c_4049]) ).
tcf(c_10077,plain,
( ( sk_c11 = iPr_def_25 )
| ( sk_c11 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_10076,c_9479]) ).
tcf(c_10144,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1418,c_4049]) ).
tcf(c_10145,plain,
( ( sk_c11 = iPr_def_23 )
| ( sk_c11 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_10144,c_9479]) ).
tcf(c_10168,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_1420,c_4049]) ).
tcf(c_10169,plain,
( ( sk_c11 = iPr_def_20 )
| ( sk_c11 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_10168,c_9479]) ).
tcf(c_10180,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1421,c_4049]) ).
tcf(c_10181,plain,
( ( sk_c11 = iPr_def_19 )
| ( sk_c11 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_10180,c_9479]) ).
tcf(c_10314,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(iPr_def_25,iPr_def_16) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_1504,c_4047]) ).
tcf(c_10315,plain,
( ( sk_c9 = iPr_def_22 )
| ( sk_c11 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_10314,c_9038]) ).
tcf(c_10346,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1521,c_4049]) ).
tcf(c_10347,plain,
( ( sk_c11 = iPr_def_25 )
| ( sk_c11 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_10346,c_9479]) ).
tcf(c_10713,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_1744,c_4049]) ).
tcf(c_10714,plain,
( ( sk_c10 = iPr_def_26 )
| ( sk_c11 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_10713,c_9479]) ).
tcf(c_10735,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1832,c_4048]) ).
tcf(c_10736,plain,
( ( sk_c10 = iPr_def_26 )
| ( sk_c10 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_10735,c_9063]) ).
tcf(c_10767,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(iPr_def_25,iPr_def_16) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_1845,c_4047]) ).
tcf(c_10768,plain,
( ( sk_c9 = iPr_def_22 )
| ( sk_c10 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_10767,c_9038]) ).
tcf(c_10793,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1890,c_4049]) ).
tcf(c_10794,plain,
( ( sk_c10 = iPr_def_26 )
| ( sk_c11 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_10793,c_9479]) ).
tcf(c_10929,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_25,iPr_def_16) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1992,c_4047]) ).
tcf(c_10930,plain,
( ( sk_c9 = iPr_def_27 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_10929,c_9038]) ).
tcf(c_11359,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(iPr_def_25,iPr_def_16) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2127,c_4047]) ).
tcf(c_11360,plain,
( ( sk_c9 = iPr_def_27 )
| ( sk_c10 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_11359,c_9038]) ).
tcf(c_11417,plain,
( ( sk_c9 = iPr_def_22 )
| ( multiply(iPr_def_25,iPr_def_16) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2164,c_4047]) ).
tcf(c_11418,plain,
( ( sk_c9 = iPr_def_27 )
| ( sk_c9 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_11417,c_9038]) ).
tcf(c_12142,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2990,c_4049]) ).
tcf(c_12143,plain,
( ( sk_c11 = iPr_def_28 )
| ( sk_c11 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_12142,c_9479]) ).
tcf(c_12194,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_3117,c_4049]) ).
tcf(c_12195,plain,
( ( sk_c10 = iPr_def_24 )
| ( sk_c11 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_12194,c_9479]) ).
tcf(c_12620,plain,
( ( sk_c10 = iPr_def_29 )
| ( multiply(iPr_def_28,iPr_def_29) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_3826,c_4049]) ).
tcf(c_12621,plain,
( ( sk_c10 = iPr_def_29 )
| ( sk_c11 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_12620,c_9479]) ).
tcf(c_12651,plain,
( ( sk_c10 = iPr_def_24 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_4007,c_4048]) ).
tcf(c_12652,plain,
( ( sk_c10 = iPr_def_29 )
| ( sk_c10 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_12651,c_9063]) ).
tcf(c_18018,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_4037,c_107]) ).
tcf(c_18028,plain,
multiply(inverse(sk_c5),iPr_def_22) = sk_c10,
inference(superposition,[status(thm)],[c_678,c_18018]) ).
tcf(c_18034,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_107,c_18018]) ).
tcf(c_18035,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_108,c_18018]) ).
tcf(c_18036,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_109,c_18018]) ).
tcf(c_18199,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_4053,c_18018]) ).
tcf(c_18200,plain,
! [X0: $i] : multiply(inverse(iPr_def_21),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_4052,c_18018]) ).
tcf(c_18201,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_4051,c_18018]) ).
tcf(c_18202,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_4050,c_18018]) ).
tcf(c_18203,plain,
! [X0: $i] : multiply(inverse(iPr_def_28),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_4049,c_18018]) ).
tcf(c_18204,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_4048,c_18018]) ).
tcf(c_18205,plain,
! [X0: $i] : multiply(inverse(iPr_def_25),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_4047,c_18018]) ).
tcf(c_18274,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_18018,c_18018]) ).
tcf(c_18824,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_18035,c_18274]) ).
tcf(c_18836,plain,
multiply(sk_c11,identity) = multiply(iPr_def_28,iPr_def_29),
inference(superposition,[status(thm)],[c_18824,c_9482]) ).
tcf(c_18839,plain,
multiply(sk_c11,identity) = multiply(iPr_def_23,iPr_def_24),
inference(superposition,[status(thm)],[c_18824,c_9897]) ).
tcf(c_18840,plain,
multiply(sk_c10,identity) = multiply(iPr_def_21,iPr_def_22),
inference(superposition,[status(thm)],[c_18824,c_9538]) ).
tcf(c_18849,plain,
multiply(sk_c10,identity) = multiply(iPr_def_26,iPr_def_27),
inference(superposition,[status(thm)],[c_18824,c_9097]) ).
tcf(c_18858,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_18824,c_18034]) ).
tcf(c_18860,plain,
multiply(sk_c10,identity) = sk_c10,
inference(light_normalisation,[status(thm)],[c_18849,c_9063]) ).
tcf(c_18870,plain,
multiply(sk_c11,identity) = sk_c11,
inference(light_normalisation,[status(thm)],[c_18839,c_9811]) ).
tcf(c_18904,plain,
multiply(sk_c4,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_18199,c_108]) ).
tcf(c_18905,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_23)) != sk_c11 )
| ( multiply(sk_c4,sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_18199,c_691]) ).
tcf(c_18907,plain,
( ~ iPr_def_10
| ( inverse(inverse(iPr_def_23)) != sk_c11 )
| ( multiply(sk_c4,sk_c9) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_18199,c_693]) ).
tcf(c_18909,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_23,X0)) = X0,
inference(superposition,[status(thm)],[c_18199,c_18018]) ).
tcf(c_18910,plain,
multiply(sk_c4,identity) = inverse(iPr_def_23),
inference(superposition,[status(thm)],[c_18199,c_18824]) ).
tcf(c_18927,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( identity = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_7251,c_18904]) ).
tcf(c_18947,plain,
inverse(iPr_def_23) = sk_c4,
inference(demodulation,[status(thm)],[c_18910,c_18824]) ).
tcf(c_19662,plain,
multiply(sk_c4,sk_c11) = iPr_def_24,
inference(superposition,[status(thm)],[c_9811,c_18909]) ).
tcf(c_19784,plain,
multiply(sk_c5,iPr_def_21) = identity,
inference(superposition,[status(thm)],[c_18200,c_108]) ).
tcf(c_19789,plain,
! [X0: $i] : multiply(sk_c5,multiply(iPr_def_21,X0)) = X0,
inference(superposition,[status(thm)],[c_18200,c_18018]) ).
tcf(c_19810,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( identity = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_6985,c_19784]) ).
tcf(c_20068,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( iPr_def_22 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_19810,c_18927]) ).
tcf(c_20092,plain,
multiply(sk_c5,sk_c10) = iPr_def_22,
inference(superposition,[status(thm)],[c_9535,c_19789]) ).
tcf(c_20350,plain,
! [X0: $i] : multiply(sk_c6,multiply(iPr_def_20,X0)) = X0,
inference(superposition,[status(thm)],[c_18201,c_18018]) ).
tcf(c_20351,plain,
multiply(sk_c6,identity) = inverse(iPr_def_20),
inference(superposition,[status(thm)],[c_18201,c_18824]) ).
tcf(c_20619,plain,
inverse(iPr_def_20) = sk_c6,
inference(demodulation,[status(thm)],[c_20351,c_18824]) ).
tcf(c_20629,plain,
multiply(sk_c6,sk_c10) = iPr_def_19,
inference(superposition,[status(thm)],[c_9530,c_20350]) ).
tcf(c_20911,plain,
multiply(sk_c7,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_18202,c_108]) ).
tcf(c_23564,plain,
multiply(sk_c1,iPr_def_28) = identity,
inference(superposition,[status(thm)],[c_18203,c_108]) ).
tcf(c_23565,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_28)) != sk_c11 )
| ( multiply(sk_c1,sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_18203,c_691]) ).
tcf(c_23569,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_28,X0)) = X0,
inference(superposition,[status(thm)],[c_18203,c_18018]) ).
tcf(c_23570,plain,
multiply(sk_c1,identity) = inverse(iPr_def_28),
inference(superposition,[status(thm)],[c_18203,c_18824]) ).
tcf(c_23641,plain,
( ( identity = iPr_def_29 )
| ( sk_c10 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_3117,c_23564]) ).
tcf(c_23642,plain,
( ( identity = iPr_def_29 )
| ( sk_c11 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_2990,c_23564]) ).
tcf(c_23643,plain,
( ( identity = iPr_def_29 )
| ( sk_c10 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_2774,c_23564]) ).
tcf(c_23644,plain,
( ( identity = iPr_def_29 )
| ( sk_c11 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_2650,c_23564]) ).
tcf(c_23645,plain,
( ( identity = iPr_def_29 )
| ( sk_c11 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_2501,c_23564]) ).
tcf(c_23783,plain,
multiply(iPr_def_28,identity) = iPr_def_28,
inference(superposition,[status(thm)],[c_23564,c_4049]) ).
tcf(c_24115,plain,
inverse(iPr_def_28) = sk_c1,
inference(demodulation,[status(thm)],[c_23570,c_18824]) ).
tcf(c_24122,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( inverse(iPr_def_25) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_20068,c_24115]) ).
tcf(c_24383,plain,
( ( identity = iPr_def_29 )
| ( multiply(sk_c5,iPr_def_24) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_23641,c_678]) ).
tcf(c_24781,plain,
( ( identity = iPr_def_29 )
| ( multiply(sk_c5,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_23643,c_678]) ).
tcf(c_24787,plain,
( ( identity = iPr_def_29 )
| ( identity = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_24781,c_19784]) ).
tcf(c_24900,plain,
multiply(sk_c1,identity) = sk_c1,
inference(superposition,[status(thm)],[c_1463,c_23569]) ).
tcf(c_24901,plain,
multiply(sk_c1,sk_c11) = iPr_def_29,
inference(superposition,[status(thm)],[c_9479,c_23569]) ).
tcf(c_25203,plain,
( ( identity = iPr_def_29 )
| ( multiply(sk_c1,iPr_def_20) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_23644,c_685]) ).
tcf(c_25339,plain,
( ( iPr_def_19 = iPr_def_23 )
| ( identity = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_23645,c_23642]) ).
tcf(c_25390,plain,
( ( identity = iPr_def_29 )
| ( multiply(sk_c1,iPr_def_19) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_23645,c_685]) ).
tcf(c_27194,plain,
multiply(sk_c2,iPr_def_26) = identity,
inference(superposition,[status(thm)],[c_18204,c_108]) ).
tcf(c_27199,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_26,X0)) = X0,
inference(superposition,[status(thm)],[c_18204,c_18018]) ).
tcf(c_27226,plain,
( ( identity = iPr_def_27 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1585,c_27194]) ).
tcf(c_27831,plain,
multiply(sk_c2,identity) = sk_c2,
inference(superposition,[status(thm)],[c_1464,c_27199]) ).
tcf(c_27832,plain,
multiply(sk_c2,sk_c10) = iPr_def_27,
inference(superposition,[status(thm)],[c_9063,c_27199]) ).
tcf(c_28691,plain,
( ( identity = iPr_def_27 )
| ( multiply(sk_c6,iPr_def_15) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_27226,c_675]) ).
tcf(c_30313,plain,
( ( identity = iPr_def_29 )
| ( multiply(inverse(sk_c5),iPr_def_22) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_24383,c_18018]) ).
tcf(c_37153,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_25,X0)) = X0,
inference(superposition,[status(thm)],[c_18205,c_18018]) ).
tcf(c_37154,plain,
multiply(sk_c3,identity) = inverse(iPr_def_25),
inference(superposition,[status(thm)],[c_18205,c_18824]) ).
tcf(c_37662,plain,
inverse(iPr_def_25) = sk_c3,
inference(demodulation,[status(thm)],[c_37154,c_18824]) ).
tcf(c_37726,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm)],[c_1465,c_37153]) ).
tcf(c_37727,plain,
multiply(sk_c3,sk_c9) = iPr_def_16,
inference(superposition,[status(thm)],[c_9038,c_37153]) ).
tcf(c_39007,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( sk_c1 = sk_c3 ) ),
inference(light_normalisation,[status(thm)],[c_24122,c_37662]) ).
tcf(c_39034,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( multiply(sk_c1,sk_c9) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_39007,c_672]) ).
tcf(c_43029,plain,
( ( iPr_def_22 = iPr_def_24 )
| ~ iPr_def_10
| ( sk_c11 != iPr_def_16 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_39034,c_693]) ).
tcf(c_43034,plain,
( ( iPr_def_22 = iPr_def_24 )
| ~ iPr_def_10
| ( sk_c11 != iPr_def_28 )
| ( sk_c11 != iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_43029,c_684]) ).
tcf(c_58733,plain,
( ~ iPr_def_13
| ( sk_c9 != iPr_def_27 ) ),
inference(global_subsumption_just,[status(thm)],[c_4747,c_4755,c_4747,c_10736,c_10768]) ).
tcf(c_58735,plain,
~ iPr_def_13,
inference(global_subsumption_just,[status(thm)],[c_58733,c_4755,c_11360,c_11418,c_58733]) ).
tcf(c_58737,plain,
( iPr_def_14
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_686,c_58735]) ).
tcf(c_59427,plain,
( ( identity = iPr_def_29 )
| ~ iPr_def_12
| ( iPr_def_19 != iPr_def_23 )
| ( sk_c11 != iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_23642,c_4931]) ).
tcf(c_59461,plain,
( ( iPr_def_25 = iPr_def_28 )
| ~ iPr_def_12
| ( sk_c11 != iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_2505,c_4931]) ).
tcf(c_59477,plain,
( ( sk_c10 = iPr_def_26 )
| ~ iPr_def_12
| ( sk_c11 != iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_715,c_4931]) ).
tcf(c_59835,plain,
( ( sk_c10 = iPr_def_26 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_59477,c_10714,c_59477]) ).
tcf(c_59847,plain,
( ~ iPr_def_14
| ( sk_c10 != identity )
| ( multiply(identity,sk_c9) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_5491,c_18858]) ).
tcf(c_59848,plain,
( ~ iPr_def_14
| ( sk_c10 != identity )
| ( sk_c10 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_59847,c_107]) ).
tcf(c_60643,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_5074,c_5078,c_5074,c_12143,c_12621]) ).
tcf(c_60645,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_60643,c_5078,c_12195,c_12652,c_60643]) ).
tcf(c_60647,plain,
( iPr_def_14
| iPr_def_12
| iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_58737,c_60645]) ).
tcf(c_60823,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_23 )
| ( multiply(sk_c4,sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_18905,c_679,c_18947]) ).
tcf(c_61174,plain,
( ~ iPr_def_10
| ( multiply(sk_c4,sk_c9) != sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_18907,c_147,c_156,c_5418,c_5475]) ).
tcf(c_61194,plain,
( ( sk_c10 = iPr_def_29 )
| ~ iPr_def_10
| ( multiply(sk_c4,iPr_def_22) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_745,c_61174]) ).
tcf(c_61197,plain,
( ( sk_c11 = iPr_def_23 )
| ~ iPr_def_10
| ( multiply(sk_c4,iPr_def_27) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_728,c_61174]) ).
tcf(c_61198,plain,
( ( sk_c9 = iPr_def_22 )
| ~ iPr_def_10
| ( multiply(sk_c4,iPr_def_27) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_727,c_61174]) ).
tcf(c_61200,plain,
( ( sk_c11 = iPr_def_20 )
| ~ iPr_def_10
| ( multiply(sk_c4,iPr_def_27) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_725,c_61174]) ).
tcf(c_61201,plain,
( ( sk_c11 = iPr_def_19 )
| ~ iPr_def_10
| ( multiply(sk_c4,iPr_def_27) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_724,c_61174]) ).
tcf(c_61205,plain,
( ( sk_c11 = iPr_def_25 )
| ~ iPr_def_10
| ( multiply(sk_c4,iPr_def_22) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_709,c_61174]) ).
tcf(c_61206,plain,
( ( sk_c11 = iPr_def_16 )
| ~ iPr_def_10
| ( multiply(sk_c4,iPr_def_22) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_700,c_61174]) ).
tcf(c_61301,plain,
( ( multiply(sk_c4,iPr_def_22) != sk_c11 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_61194,c_5338,c_61206,c_61205]) ).
tcf(c_61302,plain,
( ~ iPr_def_10
| ( multiply(sk_c4,iPr_def_22) != sk_c11 ) ),
inference(renaming,[status(thm)],[c_61301]) ).
tcf(c_61313,plain,
( ( sk_c11 = iPr_def_23 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_61197,c_5338,c_10145,c_10347]) ).
tcf(c_62458,plain,
( ( sk_c9 = iPr_def_22 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_61198,c_5338,c_9303,c_10315]) ).
tcf(c_62466,plain,
( ( sk_c11 = iPr_def_20 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_61200,c_5338,c_10049,c_10169]) ).
tcf(c_62472,plain,
( ( sk_c11 = iPr_def_19 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_61201,c_5338,c_10077,c_10181]) ).
tcf(c_63590,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_28 )
| ( multiply(sk_c1,sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_23565,c_684,c_24115]) ).
tcf(c_64782,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c1)),multiply(X0,iPr_def_29)) = sk_c11,
inference(superposition,[status(thm)],[c_24901,c_18036]) ).
tcf(c_64784,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c4)),multiply(X0,iPr_def_24)) = sk_c11,
inference(superposition,[status(thm)],[c_19662,c_18036]) ).
tcf(c_64788,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_19)) = sk_c10,
inference(superposition,[status(thm)],[c_20629,c_18036]) ).
tcf(c_64792,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c8)),multiply(X0,iPr_def_15)) = sk_c9,
inference(superposition,[status(thm)],[c_671,c_18036]) ).
tcf(c_64849,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_23 )
| ( multiply(inverse(multiply(X0,sk_c1)),multiply(X0,iPr_def_29)) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1521,c_18036]) ).
tcf(c_64871,plain,
! [X0: $i] :
( ( identity = iPr_def_29 )
| ( multiply(inverse(multiply(X0,sk_c1)),multiply(X0,iPr_def_29)) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_25203,c_18036]) ).
tcf(c_64877,plain,
! [X0: $i] :
( ( identity = iPr_def_29 )
| ( multiply(inverse(multiply(X0,sk_c1)),multiply(X0,iPr_def_29)) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_25390,c_18036]) ).
tcf(c_64919,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_23 )
| ( multiply(inverse(multiply(X0,sk_c8)),multiply(X0,iPr_def_15)) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2199,c_18036]) ).
tcf(c_64929,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_23 )
| ( multiply(inverse(multiply(X0,sk_c4)),multiply(X0,iPr_def_24)) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2991,c_18036]) ).
tcf(c_65030,plain,
! [X0: $i] :
( ( identity = iPr_def_27 )
| ( multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_19)) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_28691,c_18036]) ).
tcf(c_72503,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_65030,c_64929,c_64919,c_64877,c_64871,c_64849,c_64792,c_64788,c_64784,c_64782,c_63590,c_62472,c_62466,c_62458,c_61313,c_61302,c_61174,c_60823,c_60647,c_59848,c_59847,c_59835,c_59461,c_59427,c_43034,c_37727,c_37726,c_37662,c_30313,c_27832,c_27831,c_27194,c_25339,c_24900,c_24787,c_24115,c_23783,c_23644,c_23642,c_20911,c_20629,c_20619,c_20351,c_20092,c_19784,c_19662,c_18910,c_18904,c_18870,c_18860,c_18849,c_18840,c_18836,c_18028,c_12621,c_12143,c_10930,c_10794,c_10049,c_5515,c_5507,c_4931,c_2096,c_2065,c_2020,c_1464,c_747,c_702,c_701,c_700,c_699,c_698,c_697,c_681,c_676]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP246-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.37 % Computer : n001.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 14:21:05 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.43 % Proving...
% 25.51/5.31 % SZS status Started for theBenchmark.p
% 25.51/5.31 % SZS status Unsatisfiable for theBenchmark.p
% 25.51/5.31
% 25.51/5.31 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 25.51/5.31
% 25.51/5.31 % ------ iProver source info
% 25.51/5.31
% 25.51/5.31 % git: date: 2026-07-19 20:42:38 +0200
% 25.51/5.31 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 25.51/5.31 % git: non_committed_changes: false
% 25.51/5.31
% 25.51/5.31 % ------ Parsing...% successful
% 25.51/5.31
% 25.51/5.31
% 25.51/5.31 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 25.51/5.31
% 25.51/5.31 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 25.51/5.31
% 25.51/5.31 % ------ Preprocessing... gs_s sp: 7 0s gs_e snvd_s sp: 0 0s snvd_e %
% 25.51/5.31
% 25.51/5.31 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 25.51/5.31 % ------ Proving...
% 25.51/5.31 % ------ Problem Properties
% 25.51/5.31
% 25.51/5.31 %
% 25.51/5.31 % clauses 78
% 25.51/5.31 % conjectures 60
% 25.51/5.31 % EPR 55
% 25.51/5.31 % Horn 23
% 25.51/5.31 % unary 18
% 25.51/5.31 % binary 54
% 25.51/5.31 % lits 146
% 25.51/5.31 % lits eq 136
% 25.51/5.31 % fd_pure 0
% 25.51/5.31 % fd_pseudo 0
% 25.51/5.31 % fd_cond 0
% 25.51/5.31 % fd_pseudo_cond 0
% 25.51/5.31 % AC symbols 0
% 25.51/5.31
% 25.51/5.31 % ------ Schedule dynamic 5 is on
% 25.51/5.31
% 25.51/5.31 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 25.51/5.31
% 25.51/5.31
% 25.51/5.31 % ------
% 25.51/5.31 % Current options:
% 25.51/5.31 % ------
% 25.51/5.31
% 25.51/5.31
% 25.51/5.31 %
% 25.51/5.31
% 25.51/5.31 % ------ Proving...
% 25.51/5.31 %
% 25.51/5.31
% 25.51/5.31 % SZS status Unsatisfiable for theBenchmark.p
% 25.51/5.31
% 25.51/5.31 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 25.51/5.32
% 25.51/5.32
%------------------------------------------------------------------------------