%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP224-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 : n020.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:31:51 PM UTC 2026
% Result : Unsatisfiable 58.12s 8.92s
% Output : CNFRefutation 58.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 49
% Syntax : Number of formulae : 416 ( 170 unt; 15 def)
% Number of atoms : 1292 ( 720 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 551 ( 192 ~; 359 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 2 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 22 ( 20 usr; 21 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 143 ( 0 sgn 143 !; 0 ?; 98 :)
% 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(f11,negated_conjecture,
( inverse(sk_c6) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c11 = inverse(sk_c6)
| inverse(sk_c1) = sk_c11 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| inverse(sk_c1) = sk_c11 ),
inference(reorient_equations,[],[f13]) ).
fof(f21,negated_conjecture,
( inverse(sk_c9) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c10 = inverse(sk_c9)
| inverse(sk_c1) = sk_c11 ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c10 = multiply(sk_c9,sk_c11)
| inverse(sk_c1) = sk_c11 ),
inference(reorient_equations,[],[f23]) ).
fof(f31,negated_conjecture,
( inverse(sk_c6) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c11 = inverse(sk_c6)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f33]) ).
fof(f41,negated_conjecture,
( inverse(sk_c9) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f42,plain,
( sk_c10 = inverse(sk_c9)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f44,plain,
( sk_c10 = multiply(sk_c9,sk_c11)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c11
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c11 = multiply(sk_c4,sk_c5)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( inverse(sk_c4) = sk_c5
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f48,plain,
( sk_c5 = inverse(sk_c4)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f47]) ).
fof(f55,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( inverse(sk_c7) = sk_c8
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f58,plain,
( sk_c8 = inverse(sk_c7)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c10
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c10 = multiply(sk_c8,sk_c11)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( inverse(sk_c9) = sk_c10
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c10 = inverse(sk_c9)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c10
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c10 = multiply(sk_c9,sk_c11)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c11 = multiply(sk_c4,sk_c5)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( inverse(sk_c4) = sk_c5
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f68,plain,
( sk_c5 = inverse(sk_c4)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f67]) ).
fof(f75,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
( inverse(sk_c7) = sk_c8
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
( sk_c8 = inverse(sk_c7)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f77]) ).
fof(f81,negated_conjecture,
( inverse(sk_c9) = sk_c10
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_39) ).
fof(f82,plain,
( sk_c10 = inverse(sk_c9)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c10
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_40) ).
fof(f84,plain,
( sk_c10 = multiply(sk_c9,sk_c11)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f86,plain,
( sk_c11 = multiply(sk_c4,sk_c5)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( inverse(sk_c4) = sk_c5
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c5 = inverse(sk_c4)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f87]) ).
fof(f91,negated_conjecture,
( inverse(sk_c6) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f92,plain,
( sk_c11 = inverse(sk_c6)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f91]) ).
fof(f93,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f94,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f93]) ).
fof(f95,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f96,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f95]) ).
fof(f97,negated_conjecture,
( inverse(sk_c7) = sk_c8
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f98,plain,
( sk_c8 = inverse(sk_c7)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f97]) ).
fof(f99,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f100,plain,
( sk_c10 = multiply(sk_c8,sk_c11)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f99]) ).
fof(f101,negated_conjecture,
( inverse(sk_c9) = sk_c10
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_49) ).
fof(f102,plain,
( sk_c10 = inverse(sk_c9)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f101]) ).
fof(f103,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_50) ).
fof(f104,plain,
( sk_c10 = multiply(sk_c9,sk_c11)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f103]) ).
fof(f105,negated_conjecture,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X8,sk_c11) != sk_c10
| inverse(X8) != sk_c10
| multiply(X7,sk_c11) != sk_c10
| inverse(X6) != X7
| multiply(X6,X7) != sk_c10
| multiply(X5,sk_c10) != sk_c11
| inverse(X5) != sk_c11
| multiply(X4,sk_c10) != sk_c11
| inverse(X3) != X4
| multiply(X3,X4) != sk_c11
| inverse(X2) != sk_c11
| multiply(X2,sk_c11) != X1
| multiply(sk_c11,X1) != sk_c10
| multiply(X0,sk_c10) != sk_c11
| inverse(X0) != sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_51) ).
fof(f106,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( sk_c10 != multiply(X8,sk_c11)
| sk_c10 != inverse(X8)
| sk_c10 != multiply(X7,sk_c11)
| inverse(X6) != X7
| sk_c10 != multiply(X6,X7)
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c11 != multiply(X4,sk_c10)
| inverse(X3) != X4
| sk_c11 != multiply(X3,X4)
| sk_c11 != inverse(X2)
| multiply(X2,sk_c11) != X1
| sk_c10 != multiply(sk_c11,X1)
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11 ),
inference(reorient_equations,[],[f105]) ).
fof(f107,plain,
! [X2,X3,X0,X8,X6,X7,X4,X5] :
( sk_c10 != multiply(X8,sk_c11)
| sk_c10 != inverse(X8)
| sk_c10 != multiply(X7,sk_c11)
| inverse(X6) != X7
| sk_c10 != multiply(X6,X7)
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c11 != multiply(X4,sk_c10)
| inverse(X3) != X4
| sk_c11 != multiply(X3,X4)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(sk_c11,multiply(X2,sk_c11))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11 ),
inference(equality_resolution,[],[f106]) ).
fof(f108,plain,
! [X2,X3,X0,X8,X6,X7,X5] :
( sk_c10 != multiply(X8,sk_c11)
| sk_c10 != inverse(X8)
| sk_c10 != multiply(X7,sk_c11)
| inverse(X6) != X7
| sk_c10 != multiply(X6,X7)
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c11 != multiply(inverse(X3),sk_c10)
| sk_c11 != multiply(X3,inverse(X3))
| sk_c11 != inverse(X2)
| sk_c10 != multiply(sk_c11,multiply(X2,sk_c11))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11 ),
inference(equality_resolution,[],[f107]) ).
fof(f109,plain,
! [X2,X3,X0,X8,X6,X5] :
( sk_c10 != multiply(X8,sk_c11)
| sk_c10 != inverse(X8)
| sk_c10 != multiply(inverse(X6),sk_c11)
| sk_c10 != multiply(X6,inverse(X6))
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c11 != multiply(inverse(X3),sk_c10)
| sk_c11 != multiply(X3,inverse(X3))
| sk_c11 != inverse(X2)
| sk_c10 != multiply(sk_c11,multiply(X2,sk_c11))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11 ),
inference(equality_resolution,[],[f108]) ).
tcf(c_103,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_104,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c6) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c9) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c6) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c6,sk_c10) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c9) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_125,negated_conjecture,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c4,sk_c5) = sk_c11 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_131,negated_conjecture,
( ( multiply(sk_c7,sk_c8) = sk_c10 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c7) = sk_c8 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_133,negated_conjecture,
( ( multiply(sk_c8,sk_c11) = sk_c10 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c9) = sk_c10 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_135,negated_conjecture,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_141,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c9) = sk_c10 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_145,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c4) = sk_c5 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c6) = sk_c11 ) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_150,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_152,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_153,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c8,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_154,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_155,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_156,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(X5) != sk_c10 )
| ( inverse(X3) != sk_c11 )
| ( inverse(X2) != sk_c11 )
| ( inverse(X0) != sk_c11 )
| ( multiply(X5,sk_c11) != sk_c10 )
| ( multiply(X2,sk_c10) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 )
| ( multiply(inverse(X4),sk_c11) != sk_c10 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X4,inverse(X4)) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(sk_c11,multiply(X3,sk_c11)) != sk_c10 ) ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_617,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_156]) ).
tcf(c_618,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c11) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_156]) ).
tcf(c_619,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_156]) ).
tcf(c_620,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_156]) ).
tcf(c_621,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c11 )
| ( multiply(sk_c11,multiply(X0,sk_c11)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_156]) ).
tcf(c_622,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_156]) ).
tcf(c_623,definition,
iPr_def_15 = multiply(sk_c9,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_624,definition,
iPr_def_16 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_625,definition,
iPr_def_17 = inverse(sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_626,definition,
iPr_def_18 = multiply(sk_c8,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_627,definition,
iPr_def_19 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_628,definition,
iPr_def_20 = multiply(sk_c7,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_629,definition,
iPr_def_21 = multiply(sk_c6,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_630,definition,
iPr_def_22 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_631,definition,
iPr_def_23 = multiply(sk_c5,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_632,definition,
iPr_def_24 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_633,definition,
iPr_def_25 = multiply(sk_c4,sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_634,definition,
iPr_def_26 = multiply(sk_c2,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_635,definition,
iPr_def_27 = multiply(sk_c11,sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_636,definition,
iPr_def_28 = multiply(sk_c1,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_637,definition,
iPr_def_29 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_638,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_622]) ).
tcf(c_639,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c11 )
| ( multiply(sk_c11,multiply(X0,sk_c11)) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_621]) ).
tcf(c_640,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_620]) ).
tcf(c_641,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_619]) ).
tcf(c_643,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c11) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_618]) ).
tcf(c_644,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_617]) ).
tcf(c_645,negated_conjecture,
( ( iPr_def_16 = sk_c11 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_155,c_624,c_623]) ).
tcf(c_646,negated_conjecture,
( ( iPr_def_17 = sk_c10 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_154,c_625]) ).
tcf(c_647,negated_conjecture,
( ( iPr_def_18 = sk_c10 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_153,c_626]) ).
tcf(c_648,negated_conjecture,
( ( iPr_def_19 = sk_c8 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_152,c_627]) ).
tcf(c_649,negated_conjecture,
( ( iPr_def_20 = sk_c10 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_151,c_628]) ).
tcf(c_650,negated_conjecture,
( ( iPr_def_21 = sk_c11 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_150,c_629]) ).
tcf(c_651,negated_conjecture,
( ( iPr_def_22 = sk_c11 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_149,c_630]) ).
tcf(c_653,negated_conjecture,
( ( iPr_def_24 = sk_c5 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_147,c_632]) ).
tcf(c_654,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_16 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_146,c_633]) ).
tcf(c_655,negated_conjecture,
( ( iPr_def_26 = sk_c3 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_145,c_634]) ).
tcf(c_656,negated_conjecture,
( ( iPr_def_26 = sk_c3 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_144]) ).
tcf(c_658,negated_conjecture,
( ( iPr_def_26 = sk_c3 )
| ( iPr_def_19 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_659,negated_conjecture,
( ( iPr_def_26 = sk_c3 )
| ( iPr_def_20 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_663,negated_conjecture,
( ( iPr_def_26 = sk_c3 )
| ( iPr_def_24 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_664,negated_conjecture,
( ( iPr_def_26 = sk_c3 )
| ( iPr_def_25 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_665,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_135,c_635]) ).
tcf(c_666,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_134]) ).
tcf(c_667,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_133]) ).
tcf(c_668,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_19 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_132]) ).
tcf(c_669,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_20 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_673,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_24 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_674,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_25 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_675,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_125,c_636]) ).
tcf(c_676,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_680,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_21 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_681,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_685,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_115,c_637]) ).
tcf(c_686,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_17 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_690,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_21 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_691,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_1144,plain,
( ( sk_c3 = iPr_def_26 )
| ( multiply(sk_c7,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_658,c_628]) ).
tcf(c_1145,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(sk_c7,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_648,c_628]) ).
tcf(c_1177,plain,
( ( sk_c11 = iPr_def_16 )
| ( multiply(sk_c4,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_653,c_633]) ).
tcf(c_1196,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(sk_c11,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_659,c_635]) ).
tcf(c_1198,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(sk_c11,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_656,c_635]) ).
tcf(c_1199,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c11,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_655,c_635]) ).
tcf(c_1228,plain,
multiply(iPr_def_29,sk_c1) = identity,
inference(superposition,[status(thm)],[c_637,c_104]) ).
tcf(c_1229,plain,
multiply(iPr_def_24,sk_c4) = identity,
inference(superposition,[status(thm)],[c_632,c_104]) ).
tcf(c_1230,plain,
multiply(iPr_def_22,sk_c6) = identity,
inference(superposition,[status(thm)],[c_630,c_104]) ).
tcf(c_1231,plain,
multiply(iPr_def_19,sk_c7) = identity,
inference(superposition,[status(thm)],[c_627,c_104]) ).
tcf(c_1232,plain,
multiply(iPr_def_17,sk_c9) = identity,
inference(superposition,[status(thm)],[c_625,c_104]) ).
tcf(c_1233,plain,
multiply(iPr_def_16,sk_c2) = identity,
inference(superposition,[status(thm)],[c_624,c_104]) ).
tcf(c_1259,plain,
( ( sk_c3 = iPr_def_26 )
| ( multiply(sk_c4,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_663,c_633]) ).
tcf(c_1269,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(sk_c11,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_664,c_635]) ).
tcf(c_1283,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_665,c_629]) ).
tcf(c_1322,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_666,c_629]) ).
tcf(c_1388,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_667,c_629]) ).
tcf(c_1415,plain,
( ( sk_c10 = iPr_def_27 )
| ( multiply(sk_c7,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_668,c_628]) ).
tcf(c_1431,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_669,c_629]) ).
tcf(c_1588,plain,
( ( sk_c10 = iPr_def_27 )
| ( multiply(sk_c4,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_673,c_633]) ).
tcf(c_1604,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_674,c_629]) ).
tcf(c_1667,plain,
( ( sk_c11 = iPr_def_28 )
| ( multiply(sk_c1,iPr_def_15) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_675,c_636]) ).
tcf(c_1750,plain,
( ( sk_c11 = iPr_def_28 )
| ( multiply(sk_c1,iPr_def_17) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_676,c_636]) ).
tcf(c_1752,plain,
( ( sk_c11 = iPr_def_28 )
| ( multiply(sk_c6,iPr_def_17) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_676,c_629]) ).
tcf(c_2018,plain,
( ( sk_c11 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_680,c_634]) ).
tcf(c_2063,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_681,c_634]) ).
tcf(c_2252,plain,
( ( sk_c11 = iPr_def_29 )
| ( multiply(sk_c1,iPr_def_15) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_685,c_636]) ).
tcf(c_2384,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c11 = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_686,c_685]) ).
tcf(c_2396,plain,
( ( sk_c11 = iPr_def_29 )
| ( multiply(sk_c1,iPr_def_17) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_686,c_636]) ).
tcf(c_2809,plain,
( ( sk_c11 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_29) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_690,c_634]) ).
tcf(c_2906,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_29) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_691,c_634]) ).
tcf(c_3131,plain,
( ~ iPr_def_13
| ( sk_c10 != iPr_def_18 )
| ( inverse(sk_c8) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_626,c_640]) ).
tcf(c_3132,plain,
( ~ iPr_def_13
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_623,c_640]) ).
tcf(c_3155,plain,
( ~ iPr_def_13
| ( sk_c10 != iPr_def_17 )
| ( sk_c10 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_3132,c_625]) ).
tcf(c_3282,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_21 )
| ( inverse(sk_c6) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_629,c_644]) ).
tcf(c_3283,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_28 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_636,c_644]) ).
tcf(c_3309,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_29 )
| ( sk_c11 != iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_3283,c_637]) ).
tcf(c_3313,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_22 )
| ( sk_c11 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_3282,c_630]) ).
tcf(c_3586,plain,
! [X0: $i] : multiply(sk_c6,multiply(sk_c10,X0)) = multiply(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_629,c_105]) ).
tcf(c_3587,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c8,X0)) = multiply(iPr_def_20,X0),
inference(superposition,[status(thm)],[c_628,c_105]) ).
tcf(c_3590,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c10,X0)) = multiply(iPr_def_28,X0),
inference(superposition,[status(thm)],[c_636,c_105]) ).
tcf(c_3594,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_104,c_105]) ).
tcf(c_3596,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1228,c_105]) ).
tcf(c_3597,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1229,c_105]) ).
tcf(c_3598,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1230,c_105]) ).
tcf(c_3599,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1231,c_105]) ).
tcf(c_3600,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c9,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1232,c_105]) ).
tcf(c_3601,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1233,c_105]) ).
tcf(c_3605,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3601,c_103]) ).
tcf(c_3606,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c9,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3600,c_103]) ).
tcf(c_3607,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3599,c_103]) ).
tcf(c_3608,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3598,c_103]) ).
tcf(c_3609,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3597,c_103]) ).
tcf(c_3610,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3596,c_103]) ).
tcf(c_4616,plain,
( ~ iPr_def_14
| ( inverse(identity) != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_103,c_639]) ).
tcf(c_4617,plain,
( ~ iPr_def_14
| ( multiply(sk_c11,identity) != sk_c10 )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_104,c_639]) ).
tcf(c_4890,plain,
( ~ iPr_def_11
| ( inverse(identity) != sk_c10 )
| ( multiply(inverse(identity),sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_103,c_643]) ).
tcf(c_6289,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(sk_c9,iPr_def_29) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2384,c_623]) ).
tcf(c_8411,plain,
multiply(iPr_def_16,iPr_def_26) = sk_c11,
inference(superposition,[status(thm)],[c_634,c_3605]) ).
tcf(c_8427,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(iPr_def_26,X0)) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_8411,c_105]) ).
tcf(c_8429,plain,
multiply(iPr_def_17,iPr_def_15) = sk_c11,
inference(superposition,[status(thm)],[c_623,c_3606]) ).
tcf(c_8445,plain,
multiply(iPr_def_19,iPr_def_20) = sk_c8,
inference(superposition,[status(thm)],[c_628,c_3607]) ).
tcf(c_8455,plain,
multiply(iPr_def_22,iPr_def_21) = sk_c10,
inference(superposition,[status(thm)],[c_629,c_3608]) ).
tcf(c_8458,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(iPr_def_21,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_8455,c_105]) ).
tcf(c_8803,plain,
multiply(iPr_def_24,iPr_def_25) = sk_c5,
inference(superposition,[status(thm)],[c_633,c_3609]) ).
tcf(c_8808,plain,
multiply(iPr_def_29,iPr_def_28) = sk_c10,
inference(superposition,[status(thm)],[c_636,c_3610]) ).
tcf(c_8811,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(iPr_def_28,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_8808,c_105]) ).
tcf(c_12248,plain,
( ( sk_c11 = iPr_def_28 )
| ( multiply(iPr_def_29,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_1667,c_3610]) ).
tcf(c_12249,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c11 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_12248,c_8808]) ).
tcf(c_12466,plain,
( ( sk_c11 = iPr_def_28 )
| ( multiply(iPr_def_29,iPr_def_28) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_1750,c_3610]) ).
tcf(c_12467,plain,
( ( sk_c10 = iPr_def_17 )
| ( sk_c11 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_12466,c_8808]) ).
tcf(c_13083,plain,
( ( sk_c11 = iPr_def_21 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2018,c_3605]) ).
tcf(c_13084,plain,
( ( sk_c11 = iPr_def_28 )
| ( sk_c11 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_13083,c_8411]) ).
tcf(c_13290,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2063,c_3605]) ).
tcf(c_13291,plain,
( ( sk_c11 = iPr_def_28 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_13290,c_8411]) ).
tcf(c_14348,plain,
( ( sk_c11 = iPr_def_29 )
| ( multiply(iPr_def_29,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2252,c_3610]) ).
tcf(c_14349,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c11 = iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_14348,c_8808]) ).
tcf(c_14404,plain,
( ( sk_c11 = iPr_def_29 )
| ( multiply(iPr_def_29,iPr_def_28) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2396,c_3610]) ).
tcf(c_14405,plain,
( ( sk_c10 = iPr_def_17 )
| ( sk_c11 = iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_14404,c_8808]) ).
tcf(c_14980,plain,
( ( sk_c11 = iPr_def_21 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_2809,c_3605]) ).
tcf(c_14981,plain,
( ( sk_c11 = iPr_def_29 )
| ( sk_c11 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_14980,c_8411]) ).
tcf(c_15252,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_2906,c_3605]) ).
tcf(c_15253,plain,
( ( sk_c11 = iPr_def_29 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_15252,c_8411]) ).
tcf(c_17120,plain,
multiply(sk_c7,iPr_def_18) = multiply(iPr_def_20,sk_c11),
inference(superposition,[status(thm)],[c_626,c_3587]) ).
tcf(c_21628,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_3594,c_103]) ).
tcf(c_21636,plain,
multiply(inverse(sk_c5),iPr_def_23) = sk_c10,
inference(superposition,[status(thm)],[c_631,c_21628]) ).
tcf(c_21642,plain,
multiply(inverse(sk_c11),iPr_def_27) = sk_c3,
inference(superposition,[status(thm)],[c_635,c_21628]) ).
tcf(c_21644,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_103,c_21628]) ).
tcf(c_21645,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_104,c_21628]) ).
tcf(c_21646,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_105,c_21628]) ).
tcf(c_21911,plain,
! [X0: $i] : multiply(inverse(iPr_def_29),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_3610,c_21628]) ).
tcf(c_21912,plain,
! [X0: $i] : multiply(inverse(iPr_def_24),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_3609,c_21628]) ).
tcf(c_21913,plain,
! [X0: $i] : multiply(inverse(iPr_def_22),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_3608,c_21628]) ).
tcf(c_21914,plain,
! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_3607,c_21628]) ).
tcf(c_21915,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_3606,c_21628]) ).
tcf(c_21916,plain,
! [X0: $i] : multiply(inverse(iPr_def_16),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_3605,c_21628]) ).
tcf(c_21921,plain,
multiply(inverse(iPr_def_16),sk_c11) = iPr_def_26,
inference(superposition,[status(thm)],[c_8411,c_21628]) ).
tcf(c_21952,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_21628,c_21628]) ).
tcf(c_23329,plain,
( ~ iPr_def_12
| ( inverse(inverse(identity)) != sk_c11 )
| ( multiply(inverse(inverse(identity)),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_21644,c_641]) ).
tcf(c_23444,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_21645,c_21952]) ).
tcf(c_23471,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_23444,c_21644]) ).
tcf(c_23484,plain,
multiply(sk_c11,identity) = multiply(iPr_def_16,iPr_def_26),
inference(superposition,[status(thm)],[c_23444,c_8427]) ).
tcf(c_23487,plain,
multiply(sk_c11,identity) = sk_c11,
inference(light_normalisation,[status(thm)],[c_23484,c_8411]) ).
tcf(c_23505,plain,
multiply(identity,identity) = identity,
inference(superposition,[status(thm)],[c_23471,c_104]) ).
tcf(c_23535,plain,
multiply(sk_c10,identity) = multiply(iPr_def_22,iPr_def_21),
inference(superposition,[status(thm)],[c_23444,c_8458]) ).
tcf(c_23538,plain,
multiply(sk_c10,identity) = sk_c10,
inference(light_normalisation,[status(thm)],[c_23535,c_8455]) ).
tcf(c_23589,plain,
multiply(sk_c10,identity) = multiply(iPr_def_29,iPr_def_28),
inference(superposition,[status(thm)],[c_23444,c_8811]) ).
tcf(c_24080,plain,
( ( sk_c11 = iPr_def_29 )
| ~ iPr_def_13
| ( sk_c10 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_685,c_3155]) ).
tcf(c_24084,plain,
( ( sk_c11 = iPr_def_28 )
| ~ iPr_def_13
| ( sk_c10 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_675,c_3155]) ).
tcf(c_24199,plain,
( ( sk_c11 = iPr_def_29 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_24080,c_14405,c_24080]) ).
tcf(c_24205,plain,
( ( sk_c11 = iPr_def_28 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_24084,c_12467,c_24084]) ).
tcf(c_24236,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_29 ) ),
inference(global_subsumption_just,[status(thm)],[c_3309,c_3313,c_3309,c_13084,c_13291]) ).
tcf(c_24238,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_24236,c_3313,c_14981,c_15253,c_24236]) ).
tcf(c_24240,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_638,c_24238]) ).
tcf(c_24281,plain,
multiply(sk_c1,iPr_def_29) = identity,
inference(superposition,[status(thm)],[c_21911,c_104]) ).
tcf(c_24286,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_29,X0)) = X0,
inference(superposition,[status(thm)],[c_21911,c_21628]) ).
tcf(c_24287,plain,
multiply(sk_c1,identity) = inverse(iPr_def_29),
inference(superposition,[status(thm)],[c_21911,c_23444]) ).
tcf(c_24518,plain,
multiply(iPr_def_29,identity) = iPr_def_29,
inference(superposition,[status(thm)],[c_24281,c_3610]) ).
tcf(c_24585,plain,
inverse(iPr_def_29) = sk_c1,
inference(demodulation,[status(thm)],[c_24287,c_23444]) ).
tcf(c_24715,plain,
multiply(sk_c1,sk_c10) = iPr_def_28,
inference(superposition,[status(thm)],[c_8808,c_24286]) ).
tcf(c_24982,plain,
multiply(sk_c4,iPr_def_24) = identity,
inference(superposition,[status(thm)],[c_21912,c_104]) ).
tcf(c_24987,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_24,X0)) = X0,
inference(superposition,[status(thm)],[c_21912,c_21628]) ).
tcf(c_25003,plain,
( ( identity = iPr_def_25 )
| ( sk_c10 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_1588,c_24982]) ).
tcf(c_25004,plain,
( ( identity = iPr_def_25 )
| ( sk_c3 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_1259,c_24982]) ).
tcf(c_25005,plain,
( ( identity = iPr_def_25 )
| ( sk_c11 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1177,c_24982]) ).
tcf(c_26945,plain,
( ( identity = iPr_def_25 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_25003,c_629]) ).
tcf(c_27018,plain,
( ( identity = iPr_def_25 )
| ( multiply(sk_c11,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_25004,c_635]) ).
tcf(c_27128,plain,
multiply(sk_c4,sk_c5) = iPr_def_25,
inference(superposition,[status(thm)],[c_8803,c_24987]) ).
tcf(c_30694,plain,
! [X0: $i] : multiply(sk_c6,multiply(iPr_def_22,X0)) = X0,
inference(superposition,[status(thm)],[c_21913,c_21628]) ).
tcf(c_30695,plain,
multiply(sk_c6,identity) = inverse(iPr_def_22),
inference(superposition,[status(thm)],[c_21913,c_23444]) ).
tcf(c_33044,plain,
inverse(iPr_def_22) = sk_c6,
inference(demodulation,[status(thm)],[c_30695,c_23444]) ).
tcf(c_33048,plain,
( ~ iPr_def_12
| ( multiply(iPr_def_22,sk_c6) != sk_c11 )
| ( multiply(inverse(iPr_def_22),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_33044,c_641]) ).
tcf(c_33050,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_21 )
| ( sk_c11 != identity ) ),
inference(light_normalisation,[status(thm)],[c_33048,c_629,c_1230,c_33044]) ).
tcf(c_33061,plain,
multiply(sk_c6,sk_c10) = iPr_def_21,
inference(superposition,[status(thm)],[c_8455,c_30694]) ).
tcf(c_34192,plain,
( ( identity = iPr_def_25 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_25005,c_27018]) ).
tcf(c_34252,plain,
( ( identity = iPr_def_25 )
| ( sk_c11 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_34192,c_8411]) ).
tcf(c_34673,plain,
( ( iPr_def_16 = iPr_def_27 )
| ( identity = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_34252,c_25005]) ).
tcf(c_38087,plain,
multiply(sk_c7,iPr_def_19) = identity,
inference(superposition,[status(thm)],[c_21914,c_104]) ).
tcf(c_38092,plain,
! [X0: $i] : multiply(sk_c7,multiply(iPr_def_19,X0)) = X0,
inference(superposition,[status(thm)],[c_21914,c_21628]) ).
tcf(c_38093,plain,
multiply(sk_c7,identity) = inverse(iPr_def_19),
inference(superposition,[status(thm)],[c_21914,c_23444]) ).
tcf(c_38108,plain,
( ( identity = iPr_def_20 )
| ( sk_c10 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_1415,c_38087]) ).
tcf(c_38109,plain,
( ( identity = iPr_def_20 )
| ( sk_c11 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1145,c_38087]) ).
tcf(c_38110,plain,
( ( identity = iPr_def_20 )
| ( sk_c3 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_1144,c_38087]) ).
tcf(c_40989,plain,
( ( identity = iPr_def_20 )
| ( multiply(sk_c6,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_38108,c_629]) ).
tcf(c_41179,plain,
( ( identity = iPr_def_20 )
| ( multiply(iPr_def_16,sk_c3) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_38109,c_635]) ).
tcf(c_41571,plain,
inverse(iPr_def_19) = sk_c7,
inference(demodulation,[status(thm)],[c_38093,c_23444]) ).
tcf(c_41595,plain,
multiply(sk_c7,sk_c8) = iPr_def_20,
inference(superposition,[status(thm)],[c_8445,c_38092]) ).
tcf(c_44053,plain,
multiply(sk_c9,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_21915,c_104]) ).
tcf(c_44058,plain,
! [X0: $i] : multiply(sk_c9,multiply(iPr_def_17,X0)) = X0,
inference(superposition,[status(thm)],[c_21915,c_21628]) ).
tcf(c_44059,plain,
multiply(sk_c9,identity) = inverse(iPr_def_17),
inference(superposition,[status(thm)],[c_21915,c_23444]) ).
tcf(c_44079,plain,
multiply(iPr_def_17,identity) = iPr_def_17,
inference(superposition,[status(thm)],[c_44053,c_3606]) ).
tcf(c_44082,plain,
inverse(iPr_def_17) = sk_c9,
inference(demodulation,[status(thm)],[c_44059,c_23444]) ).
tcf(c_44085,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_17,sk_c9) != sk_c10 )
| ( multiply(inverse(iPr_def_17),sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_44082,c_643]) ).
tcf(c_44092,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_15 )
| ( sk_c10 != identity ) ),
inference(light_normalisation,[status(thm)],[c_44085,c_623,c_1232,c_44082]) ).
tcf(c_44096,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm)],[c_1232,c_44058]) ).
tcf(c_44097,plain,
multiply(sk_c9,sk_c11) = iPr_def_15,
inference(superposition,[status(thm)],[c_8429,c_44058]) ).
tcf(c_44165,plain,
( ( identity = iPr_def_20 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_38110,c_41179]) ).
tcf(c_44178,plain,
( ( identity = iPr_def_20 )
| ( sk_c11 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_44165,c_8411]) ).
tcf(c_44309,plain,
( ( iPr_def_16 = iPr_def_27 )
| ( identity = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_44178,c_38109]) ).
tcf(c_44658,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( iPr_def_16 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_44309,c_34673]) ).
tcf(c_45954,plain,
multiply(sk_c2,iPr_def_16) = identity,
inference(superposition,[status(thm)],[c_21916,c_104]) ).
tcf(c_45959,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_16,X0)) = X0,
inference(superposition,[status(thm)],[c_21916,c_21628]) ).
tcf(c_45960,plain,
multiply(sk_c2,identity) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_21916,c_23444]) ).
tcf(c_46022,plain,
multiply(iPr_def_16,identity) = iPr_def_16,
inference(superposition,[status(thm)],[c_45954,c_3605]) ).
tcf(c_46025,plain,
inverse(iPr_def_16) = sk_c2,
inference(demodulation,[status(thm)],[c_45960,c_23444]) ).
tcf(c_46028,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_16,sk_c2) != sk_c10 )
| ( multiply(inverse(iPr_def_16),sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_46025,c_643]) ).
tcf(c_46029,plain,
( ~ iPr_def_12
| ( multiply(iPr_def_16,sk_c2) != sk_c11 )
| ( multiply(inverse(iPr_def_16),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_46025,c_641]) ).
tcf(c_46039,plain,
multiply(sk_c2,identity) = sk_c2,
inference(superposition,[status(thm)],[c_1233,c_45959]) ).
tcf(c_46054,plain,
multiply(sk_c2,sk_c11) = iPr_def_26,
inference(superposition,[status(thm)],[c_8411,c_45959]) ).
tcf(c_64963,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c5)),multiply(X0,iPr_def_23)) = sk_c10,
inference(superposition,[status(thm)],[c_631,c_21646]) ).
tcf(c_64964,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_21)) = sk_c10,
inference(superposition,[status(thm)],[c_33061,c_21646]) ).
tcf(c_64968,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c8)),multiply(X0,iPr_def_18)) = sk_c11,
inference(superposition,[status(thm)],[c_626,c_21646]) ).
tcf(c_64973,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c11)),multiply(X0,iPr_def_27)) = sk_c3,
inference(superposition,[status(thm)],[c_635,c_21646]) ).
tcf(c_65071,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_22)),multiply(X0,identity)) = sk_c6,
inference(superposition,[status(thm)],[c_1230,c_21646]) ).
tcf(c_65073,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_17)),multiply(X0,identity)) = sk_c9,
inference(superposition,[status(thm)],[c_1232,c_21646]) ).
tcf(c_65074,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_16)),multiply(X0,identity)) = sk_c2,
inference(superposition,[status(thm)],[c_1233,c_21646]) ).
tcf(c_65095,plain,
! [X0: $i] :
( ( identity = iPr_def_20 )
| ( multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_21)) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_40989,c_21646]) ).
tcf(c_65096,plain,
! [X0: $i] :
( ( identity = iPr_def_25 )
| ( multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_21)) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_26945,c_21646]) ).
tcf(c_65097,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_25 )
| ( multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_21)) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1604,c_21646]) ).
tcf(c_65101,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_20 )
| ( multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_21)) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1431,c_21646]) ).
tcf(c_65102,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_18 )
| ( multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_21)) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1388,c_21646]) ).
tcf(c_65103,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_17 )
| ( multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_21)) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1322,c_21646]) ).
tcf(c_65104,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_15 )
| ( multiply(inverse(multiply(X0,sk_c6)),multiply(X0,iPr_def_21)) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1283,c_21646]) ).
tcf(c_65216,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c2)),multiply(X0,identity)) = iPr_def_16,
inference(superposition,[status(thm)],[c_45954,c_21646]) ).
tcf(c_65300,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c1)),multiply(X0,identity)) = iPr_def_29,
inference(superposition,[status(thm)],[c_24281,c_21646]) ).
tcf(c_65302,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c9)),multiply(X0,identity)) = iPr_def_17,
inference(superposition,[status(thm)],[c_44053,c_21646]) ).
tcf(c_65453,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c9)),X0) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_65302,c_23444]) ).
tcf(c_65455,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c1)),X0) = iPr_def_29,
inference(light_normalisation,[status(thm)],[c_65300,c_23444]) ).
tcf(c_65456,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c2)),X0) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_65216,c_23444]) ).
tcf(c_65457,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_16)),X0) = sk_c2,
inference(light_normalisation,[status(thm)],[c_65074,c_23444]) ).
tcf(c_65458,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_17)),X0) = sk_c9,
inference(light_normalisation,[status(thm)],[c_65073,c_23444]) ).
tcf(c_65460,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_22)),X0) = sk_c6,
inference(light_normalisation,[status(thm)],[c_65071,c_23444]) ).
tcf(c_71265,plain,
multiply(inverse(identity),iPr_def_17) = iPr_def_17,
inference(superposition,[status(thm)],[c_1232,c_65453]) ).
tcf(c_71302,plain,
multiply(identity,iPr_def_17) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_71265,c_23471]) ).
tcf(c_72790,plain,
multiply(inverse(identity),multiply(inverse(sk_c5),iPr_def_23)) = sk_c10,
inference(superposition,[status(thm)],[c_104,c_64963]) ).
tcf(c_72831,plain,
multiply(inverse(multiply(inverse(iPr_def_23),sk_c5)),identity) = sk_c10,
inference(superposition,[status(thm)],[c_104,c_64963]) ).
tcf(c_72877,plain,
multiply(identity,sk_c10) = sk_c10,
inference(light_normalisation,[status(thm)],[c_72790,c_21636,c_23471]) ).
tcf(c_73817,plain,
multiply(inverse(identity),iPr_def_29) = iPr_def_29,
inference(superposition,[status(thm)],[c_1228,c_65455]) ).
tcf(c_73864,plain,
multiply(identity,iPr_def_29) = iPr_def_29,
inference(light_normalisation,[status(thm)],[c_73817,c_23471]) ).
tcf(c_73976,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,multiply(X1,sk_c2))),multiply(X0,X1)) = iPr_def_16,
inference(superposition,[status(thm)],[c_105,c_65456]) ).
tcf(c_73977,plain,
multiply(inverse(identity),iPr_def_16) = iPr_def_16,
inference(superposition,[status(thm)],[c_1233,c_65456]) ).
tcf(c_74027,plain,
( ~ iPr_def_13
| ( sk_c10 != iPr_def_16 )
| ( inverse(inverse(multiply(sk_c11,sk_c2))) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_65456,c_640]) ).
tcf(c_74034,plain,
multiply(inverse(iPr_def_16),inverse(multiply(sk_c2,sk_c2))) = iPr_def_16,
inference(superposition,[status(thm)],[c_65456,c_65456]) ).
tcf(c_74035,plain,
multiply(identity,iPr_def_16) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_73977,c_23471]) ).
tcf(c_74037,plain,
multiply(sk_c2,inverse(multiply(sk_c2,sk_c2))) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_74034,c_46025]) ).
tcf(c_74149,plain,
inverse(multiply(inverse(iPr_def_23),sk_c5)) = sk_c10,
inference(demodulation,[status(thm)],[c_72831,c_23444]) ).
tcf(c_74163,plain,
multiply(sk_c10,multiply(inverse(iPr_def_23),sk_c5)) = identity,
inference(superposition,[status(thm)],[c_74149,c_104]) ).
tcf(c_74247,plain,
multiply(iPr_def_28,multiply(inverse(iPr_def_23),sk_c5)) = multiply(sk_c1,identity),
inference(superposition,[status(thm)],[c_74163,c_3590]) ).
tcf(c_74248,plain,
multiply(iPr_def_21,multiply(inverse(iPr_def_23),sk_c5)) = multiply(sk_c6,identity),
inference(superposition,[status(thm)],[c_74163,c_3586]) ).
tcf(c_74438,plain,
multiply(inverse(multiply(inverse(iPr_def_18),sk_c8)),identity) = sk_c11,
inference(superposition,[status(thm)],[c_104,c_64968]) ).
tcf(c_74815,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,multiply(X1,iPr_def_16))),multiply(X0,X1)) = sk_c2,
inference(superposition,[status(thm)],[c_105,c_65457]) ).
tcf(c_74816,plain,
multiply(inverse(identity),sk_c2) = sk_c2,
inference(superposition,[status(thm)],[c_45954,c_65457]) ).
tcf(c_74891,plain,
multiply(inverse(sk_c2),inverse(multiply(iPr_def_16,iPr_def_16))) = sk_c2,
inference(superposition,[status(thm)],[c_65457,c_65457]) ).
tcf(c_74896,plain,
multiply(inverse(sk_c2),inverse(multiply(sk_c9,iPr_def_16))) = iPr_def_17,
inference(superposition,[status(thm)],[c_65457,c_65453]) ).
tcf(c_74899,plain,
multiply(identity,sk_c2) = sk_c2,
inference(light_normalisation,[status(thm)],[c_74816,c_23471]) ).
tcf(c_74903,plain,
multiply(iPr_def_16,inverse(multiply(sk_c9,iPr_def_16))) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_74896,c_624]) ).
tcf(c_74905,plain,
multiply(iPr_def_16,inverse(multiply(iPr_def_16,iPr_def_16))) = sk_c2,
inference(light_normalisation,[status(thm)],[c_74891,c_624]) ).
tcf(c_75283,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,multiply(X1,iPr_def_17))),multiply(X0,X1)) = sk_c9,
inference(superposition,[status(thm)],[c_105,c_65458]) ).
tcf(c_75346,plain,
multiply(inverse(sk_c9),inverse(multiply(sk_c2,iPr_def_17))) = iPr_def_16,
inference(superposition,[status(thm)],[c_65458,c_65456]) ).
tcf(c_75349,plain,
multiply(iPr_def_17,inverse(multiply(sk_c2,iPr_def_17))) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_75346,c_625]) ).
tcf(c_76335,plain,
inverse(multiply(inverse(iPr_def_18),sk_c8)) = sk_c11,
inference(demodulation,[status(thm)],[c_74438,c_23444]) ).
tcf(c_76349,plain,
multiply(sk_c11,multiply(inverse(iPr_def_18),sk_c8)) = identity,
inference(superposition,[status(thm)],[c_76335,c_104]) ).
tcf(c_76563,plain,
( ( sk_c11 = iPr_def_21 )
| ( multiply(iPr_def_28,multiply(inverse(iPr_def_18),sk_c8)) = identity ) ),
inference(superposition,[status(thm)],[c_680,c_76349]) ).
tcf(c_76579,plain,
multiply(inverse(sk_c11),identity) = multiply(inverse(iPr_def_18),sk_c8),
inference(superposition,[status(thm)],[c_76349,c_21628]) ).
tcf(c_77240,plain,
multiply(inverse(multiply(inverse(iPr_def_27),sk_c11)),identity) = sk_c3,
inference(superposition,[status(thm)],[c_104,c_64973]) ).
tcf(c_78404,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,multiply(X1,iPr_def_22))),multiply(X0,X1)) = sk_c6,
inference(superposition,[status(thm)],[c_105,c_65460]) ).
tcf(c_78455,plain,
( ~ iPr_def_13
| ( sk_c10 != sk_c6 )
| ( inverse(inverse(multiply(sk_c11,iPr_def_22))) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_65460,c_640]) ).
tcf(c_79222,plain,
inverse(multiply(inverse(iPr_def_27),sk_c11)) = sk_c3,
inference(demodulation,[status(thm)],[c_77240,c_23444]) ).
tcf(c_79286,plain,
( ~ iPr_def_11
| ( multiply(multiply(inverse(iPr_def_27),sk_c11),sk_c3) != sk_c10 )
| ( multiply(inverse(multiply(inverse(iPr_def_27),sk_c11)),sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_79222,c_643]) ).
tcf(c_79288,plain,
multiply(sk_c3,multiply(inverse(iPr_def_27),sk_c11)) = identity,
inference(superposition,[status(thm)],[c_79222,c_104]) ).
tcf(c_79396,plain,
( ~ iPr_def_11
| ( multiply(sk_c3,sk_c11) != sk_c10 )
| ( multiply(multiply(inverse(iPr_def_27),sk_c11),sk_c3) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_79286,c_79222]) ).
tcf(c_79712,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(iPr_def_26,multiply(inverse(iPr_def_27),sk_c11)) = identity ) ),
inference(superposition,[status(thm)],[c_656,c_79288]) ).
tcf(c_79713,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_26,multiply(inverse(iPr_def_27),sk_c11)) = identity ) ),
inference(superposition,[status(thm)],[c_655,c_79288]) ).
tcf(c_96165,plain,
( ( sk_c11 = iPr_def_21 )
| ( multiply(sk_c10,multiply(inverse(iPr_def_18),sk_c8)) = multiply(iPr_def_29,identity) ) ),
inference(superposition,[status(thm)],[c_76563,c_8811]) ).
tcf(c_140172,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c2)),multiply(X0,iPr_def_16)) = inverse(multiply(sk_c2,sk_c2)),
inference(superposition,[status(thm)],[c_74037,c_21646]) ).
tcf(c_140173,plain,
inverse(multiply(sk_c2,sk_c2)) = multiply(iPr_def_16,iPr_def_16),
inference(superposition,[status(thm)],[c_74037,c_3605]) ).
tcf(c_141624,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(sk_c11,multiply(inverse(iPr_def_27),sk_c11)) = multiply(iPr_def_16,identity) ) ),
inference(superposition,[status(thm)],[c_79712,c_8427]) ).
tcf(c_143946,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c11,multiply(inverse(iPr_def_27),sk_c11)) = multiply(iPr_def_16,identity) ) ),
inference(superposition,[status(thm)],[c_79713,c_8427]) ).
tcf(c_154366,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_16)),multiply(X0,iPr_def_17)) = inverse(multiply(sk_c9,iPr_def_16)),
inference(superposition,[status(thm)],[c_74903,c_21646]) ).
tcf(c_154367,plain,
inverse(multiply(sk_c9,iPr_def_16)) = multiply(sk_c2,iPr_def_17),
inference(superposition,[status(thm)],[c_74903,c_45959]) ).
tcf(c_154581,plain,
inverse(multiply(iPr_def_16,iPr_def_16)) = multiply(sk_c2,sk_c2),
inference(superposition,[status(thm)],[c_74905,c_45959]) ).
tcf(c_157052,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(inverse(multiply(sk_c11,multiply(iPr_def_26,sk_c2))),iPr_def_27) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1199,c_73976]) ).
tcf(c_157053,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(inverse(multiply(sk_c11,multiply(iPr_def_26,sk_c2))),iPr_def_27) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1198,c_73976]) ).
tcf(c_161274,plain,
inverse(multiply(sk_c2,iPr_def_17)) = multiply(sk_c9,iPr_def_16),
inference(superposition,[status(thm)],[c_75349,c_44058]) ).
tcf(c_163217,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(multiply(X0,sk_c2)),multiply(X0,iPr_def_16))),iPr_def_16) = sk_c2,
inference(superposition,[status(thm)],[c_65456,c_74815]) ).
tcf(c_163374,plain,
multiply(multiply(sk_c2,sk_c2),iPr_def_16) = sk_c2,
inference(light_normalisation,[status(thm)],[c_163217,c_140172,c_140173,c_154581]) ).
tcf(c_170469,plain,
( ( sk_c11 = iPr_def_28 )
| ( multiply(inverse(multiply(sk_c6,multiply(iPr_def_17,iPr_def_17))),iPr_def_21) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_1752,c_75283]) ).
tcf(c_170663,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(inverse(multiply(sk_c9,multiply(iPr_def_29,iPr_def_17))),iPr_def_15) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_6289,c_75283]) ).
tcf(c_170927,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(multiply(X0,iPr_def_16)),multiply(X0,iPr_def_17))),sk_c2) = sk_c9,
inference(superposition,[status(thm)],[c_65457,c_75283]) ).
tcf(c_171086,plain,
multiply(multiply(sk_c9,iPr_def_16),sk_c2) = sk_c9,
inference(light_normalisation,[status(thm)],[c_170927,c_154366,c_154367,c_161274]) ).
tcf(c_180027,plain,
( ~ iPr_def_14
| ( sk_c11 != identity )
| ( multiply(sk_c11,sk_c11) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_4616,c_23471]) ).
tcf(c_181307,plain,
( ~ iPr_def_11
| ( sk_c10 != identity )
| ( multiply(identity,sk_c11) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_4890,c_23471]) ).
tcf(c_181308,plain,
( ~ iPr_def_11
| ( sk_c10 != identity )
| ( sk_c11 != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_181307,c_103]) ).
tcf(c_182972,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(inverse(multiply(iPr_def_26,multiply(multiply(inverse(iPr_def_27),sk_c11),iPr_def_22))),identity) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_79713,c_78404]) ).
tcf(c_182973,plain,
( ( sk_c10 = iPr_def_17 )
| ( multiply(inverse(multiply(iPr_def_26,multiply(multiply(inverse(iPr_def_27),sk_c11),iPr_def_22))),identity) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_79712,c_78404]) ).
tcf(c_189370,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_182973,c_182972,c_181308,c_180027,c_171086,c_170663,c_170469,c_163374,c_157053,c_157052,c_154581,c_154367,c_143946,c_141624,c_140173,c_96165,c_79396,c_79288,c_78455,c_76579,c_74248,c_74247,c_74027,c_65104,c_65103,c_65102,c_65101,c_65097,c_65096,c_65095,c_64964,c_46054,c_46039,c_46029,c_46028,c_46025,c_46022,c_45954,c_44658,c_44097,c_44096,c_44092,c_44079,c_41595,c_41571,c_38093,c_38087,c_33061,c_33050,c_33044,c_30695,c_27128,c_24982,c_24715,c_24585,c_24518,c_24287,c_24281,c_24240,c_24205,c_24199,c_23589,c_23538,c_23535,c_23487,c_23484,c_23471,c_23329,c_21921,c_21642,c_17120,c_14349,c_12249,c_4617,c_74035,c_72877,c_23505,c_3155,c_3131,c_74899,c_73864,c_71302,c_1269,c_1233,c_1196,c_654,c_653,c_651,c_650,c_649,c_648,c_647,c_646,c_645,c_637,c_630,c_625,c_624]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP224-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n020.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 14:12:18 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 58.12/8.92 % SZS status Started for theBenchmark.p
% 58.12/8.92 % SZS status Unsatisfiable for theBenchmark.p
% 58.12/8.92
% 58.12/8.92 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 58.12/8.92
% 58.12/8.92 % ------ iProver source info
% 58.12/8.92
% 58.12/8.92 % git: date: 2026-07-19 20:42:38 +0200
% 58.12/8.92 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 58.12/8.92 % git: non_committed_changes: false
% 58.12/8.92
% 58.12/8.92 % ------ Parsing...% successful
% 58.12/8.92
% 58.12/8.92
% 58.12/8.92 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 58.12/8.92
% 58.12/8.92 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 58.12/8.92
% 58.12/8.92 % ------ Preprocessing... gs_s sp: 6 0s gs_e snvd_s sp: 0 0s snvd_e %
% 58.12/8.92
% 58.12/8.92 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 58.12/8.92 % ------ Proving...
% 58.12/8.92 % ------ Problem Properties
% 58.12/8.92
% 58.12/8.92 %
% 58.12/8.92 % clauses 74
% 58.12/8.92 % conjectures 56
% 58.12/8.92 % EPR 51
% 58.12/8.92 % Horn 23
% 58.12/8.92 % unary 18
% 58.12/8.92 % binary 50
% 58.12/8.92 % lits 138
% 58.12/8.92 % lits eq 128
% 58.12/8.92 % fd_pure 0
% 58.12/8.92 % fd_pseudo 0
% 58.12/8.92 % fd_cond 0
% 58.12/8.92 % fd_pseudo_cond 0
% 58.12/8.92 % AC symbols 0
% 58.12/8.92
% 58.12/8.92 % ------ Schedule dynamic 5 is on
% 58.12/8.92
% 58.12/8.92 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 58.12/8.92
% 58.12/8.92
% 58.12/8.92 % ------
% 58.12/8.92 % Current options:
% 58.12/8.92 % ------
% 58.12/8.92
% 58.12/8.92
% 58.12/8.92 %
% 58.12/8.92
% 58.12/8.92 % ------ Proving...
% 58.12/8.92 %
% 58.12/8.92
% 58.12/8.92 % SZS status Unsatisfiable for theBenchmark.p
% 58.12/8.92
% 58.12/8.92 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 58.12/8.93
% 58.12/8.93
%------------------------------------------------------------------------------