%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP326-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 : n016.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:51 PM UTC 2026
% Result : Unsatisfiable 5.43s 2.17s
% Output : CNFRefutation 9.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 35
% Syntax : Number of formulae : 308 ( 97 unt; 10 def)
% Number of atoms : 1089 ( 555 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 438 ( 147 ~; 291 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 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 : 15 ( 13 usr; 14 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 72 ( 0 sgn 72 !; 0 ?; 55 :)
% 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_c6,sk_c7) = sk_c5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,negated_conjecture,
( inverse(sk_c6) = sk_c5
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f7,plain,
( sk_c5 = inverse(sk_c6)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f6]) ).
fof(f8,negated_conjecture,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f9,plain,
( sk_c6 = multiply(sk_c7,sk_c5)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f8]) ).
fof(f10,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c7 = inverse(sk_c4)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c7 = multiply(sk_c4,sk_c6)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c6) = sk_c5
| inverse(sk_c1) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c5 = inverse(sk_c6)
| sk_c6 = inverse(sk_c1) ),
inference(reorient_equations,[],[f14]) ).
fof(f16,negated_conjecture,
( multiply(sk_c7,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f17,plain,
( sk_c6 = multiply(sk_c7,sk_c5)
| sk_c6 = inverse(sk_c1) ),
inference(reorient_equations,[],[f16]) ).
fof(f18,negated_conjecture,
( inverse(sk_c4) = sk_c7
| inverse(sk_c1) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,plain,
( sk_c7 = inverse(sk_c4)
| sk_c6 = inverse(sk_c1) ),
inference(reorient_equations,[],[f18]) ).
fof(f20,negated_conjecture,
( multiply(sk_c4,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_9) ).
fof(f21,plain,
( sk_c7 = multiply(sk_c4,sk_c6)
| sk_c6 = inverse(sk_c1) ),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
( inverse(sk_c6) = sk_c5
| multiply(sk_c7,sk_c3) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f23,plain,
( sk_c5 = inverse(sk_c6)
| sk_c6 = multiply(sk_c7,sk_c3) ),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c7,sk_c3) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c6 = multiply(sk_c7,sk_c5)
| sk_c6 = multiply(sk_c7,sk_c3) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c7,sk_c3) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c7 = inverse(sk_c4)
| sk_c6 = multiply(sk_c7,sk_c3) ),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c7,sk_c3) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f29,plain,
( sk_c7 = multiply(sk_c4,sk_c6)
| sk_c6 = multiply(sk_c7,sk_c3) ),
inference(reorient_equations,[],[f28]) ).
fof(f30,negated_conjecture,
( inverse(sk_c6) = sk_c5
| multiply(sk_c2,sk_c7) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f31,plain,
( sk_c5 = inverse(sk_c6)
| sk_c3 = multiply(sk_c2,sk_c7) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c2,sk_c7) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c6 = multiply(sk_c7,sk_c5)
| sk_c3 = multiply(sk_c2,sk_c7) ),
inference(reorient_equations,[],[f32]) ).
fof(f34,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f35,plain,
( sk_c7 = inverse(sk_c4)
| sk_c3 = multiply(sk_c2,sk_c7) ),
inference(reorient_equations,[],[f34]) ).
fof(f36,negated_conjecture,
( multiply(sk_c4,sk_c6) = sk_c7
| multiply(sk_c2,sk_c7) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f37,plain,
( sk_c7 = multiply(sk_c4,sk_c6)
| sk_c3 = multiply(sk_c2,sk_c7) ),
inference(reorient_equations,[],[f36]) ).
fof(f38,negated_conjecture,
( inverse(sk_c6) = sk_c5
| inverse(sk_c2) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_18) ).
fof(f39,plain,
( sk_c5 = inverse(sk_c6)
| sk_c7 = inverse(sk_c2) ),
inference(reorient_equations,[],[f38]) ).
fof(f40,negated_conjecture,
( multiply(sk_c7,sk_c5) = sk_c6
| inverse(sk_c2) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_19) ).
fof(f41,plain,
( sk_c6 = multiply(sk_c7,sk_c5)
| sk_c7 = inverse(sk_c2) ),
inference(reorient_equations,[],[f40]) ).
fof(f42,negated_conjecture,
( inverse(sk_c4) = sk_c7
| inverse(sk_c2) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_20) ).
fof(f43,plain,
( sk_c7 = inverse(sk_c4)
| sk_c7 = inverse(sk_c2) ),
inference(reorient_equations,[],[f42]) ).
fof(f44,negated_conjecture,
( multiply(sk_c4,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f45,plain,
( sk_c7 = multiply(sk_c4,sk_c6)
| sk_c7 = inverse(sk_c2) ),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
! [X2,X3,X0,X1] :
( multiply(X3,sk_c6) != sk_c7
| inverse(X3) != sk_c7
| multiply(sk_c7,sk_c5) != sk_c6
| inverse(sk_c6) != sk_c5
| inverse(X2) != sk_c7
| multiply(X2,sk_c7) != X1
| multiply(sk_c7,X1) != sk_c6
| inverse(X0) != sk_c6
| multiply(X0,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f47,plain,
! [X2,X3,X0,X1] :
( sk_c7 != multiply(X3,sk_c6)
| sk_c7 != inverse(X3)
| sk_c6 != multiply(sk_c7,sk_c5)
| sk_c5 != inverse(sk_c6)
| sk_c7 != inverse(X2)
| multiply(X2,sk_c7) != X1
| sk_c6 != multiply(sk_c7,X1)
| inverse(X0) != sk_c6
| sk_c7 != multiply(X0,sk_c6)
| multiply(sk_c6,sk_c7) != sk_c5 ),
inference(reorient_equations,[],[f46]) ).
fof(f48,plain,
! [X2,X3,X0] :
( sk_c7 != multiply(X3,sk_c6)
| sk_c7 != inverse(X3)
| sk_c6 != multiply(sk_c7,sk_c5)
| sk_c5 != inverse(sk_c6)
| sk_c7 != inverse(X2)
| sk_c6 != multiply(sk_c7,multiply(X2,sk_c7))
| inverse(X0) != sk_c6
| sk_c7 != multiply(X0,sk_c6)
| multiply(sk_c6,sk_c7) != sk_c5 ),
inference(equality_resolution,[],[f47]) ).
tcf(c_74,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_75,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_77,negated_conjecture,
multiply(sk_c6,sk_c7) = sk_c5,
inference(cnf_transformation,[],[f5]) ).
tcf(c_78,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_79,negated_conjecture,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_80,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_81,negated_conjecture,
( ( multiply(sk_c4,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_82,negated_conjecture,
( ( inverse(sk_c1) = sk_c6 )
| ( inverse(sk_c6) = sk_c5 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_83,negated_conjecture,
( ( inverse(sk_c1) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_84,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( inverse(sk_c1) = sk_c6 ) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_85,negated_conjecture,
( ( inverse(sk_c1) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_86,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c7,sk_c3) = sk_c6 ) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_87,negated_conjecture,
( ( multiply(sk_c7,sk_c3) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_88,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c7,sk_c3) = sk_c6 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_89,negated_conjecture,
( ( multiply(sk_c4,sk_c6) = sk_c7 )
| ( multiply(sk_c7,sk_c3) = sk_c6 ) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_90,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c2,sk_c7) = sk_c3 ) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_91,negated_conjecture,
( ( multiply(sk_c2,sk_c7) = sk_c3 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_92,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c2,sk_c7) = sk_c3 ) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_93,negated_conjecture,
( ( multiply(sk_c2,sk_c7) = sk_c3 )
| ( multiply(sk_c4,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_94,negated_conjecture,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c6) = sk_c5 ) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_95,negated_conjecture,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_96,negated_conjecture,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c4) = sk_c7 ) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_97,negated_conjecture,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c4,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_98,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(sk_c6) != sk_c5 )
| ( inverse(X2) != sk_c7 )
| ( inverse(X1) != sk_c7 )
| ( inverse(X0) != sk_c6 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( multiply(X2,sk_c6) != sk_c7 )
| ( multiply(X0,sk_c6) != sk_c7 )
| ( multiply(sk_c7,multiply(X1,sk_c7)) != sk_c6 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(sk_c6) != sk_c5 )
| ( inverse(X2) != sk_c7 )
| ( inverse(X1) != sk_c7 )
| ( inverse(X0) != sk_c6 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( multiply(sk_c7,multiply(X1,sk_c7)) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 )
| ( multiply(X2,sk_c6) != sk_c7 ) ),
inference(global_subsumption_just,[status(thm)],[c_98,c_77,c_98]) ).
tcf(c_104,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(sk_c6) != sk_c5 )
| ( inverse(X2) != sk_c7 )
| ( inverse(X1) != sk_c6 )
| ( inverse(X0) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( multiply(X2,sk_c6) != sk_c7 )
| ( multiply(X1,sk_c6) != sk_c7 )
| ( multiply(sk_c7,multiply(X0,sk_c7)) != sk_c6 ) ),
inference(renaming,[status(thm)],[c_103]) ).
tcf(c_308,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_104]) ).
tcf(c_309,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_104]) ).
tcf(c_310,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c7 )
| ( multiply(sk_c7,multiply(X0,sk_c7)) != sk_c6 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_104]) ).
tcf(c_311,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c6) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c6 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_104]) ).
tcf(c_312,definition,
iPr_def_13 = multiply(sk_c7,sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_313,definition,
iPr_def_14 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_314,definition,
iPr_def_15 = multiply(sk_c4,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_315,definition,
iPr_def_16 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_316,definition,
iPr_def_17 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_317,definition,
iPr_def_18 = multiply(sk_c2,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_318,definition,
iPr_def_19 = multiply(sk_c7,sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_319,definition,
iPr_def_20 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_320,definition,
iPr_def_21 = multiply(sk_c1,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_321,definition,
iPr_def_22 = multiply(sk_c6,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_322,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != sk_c5 )
| ( iPr_def_13 != sk_c6 ) ),
inference(demodulation,[status(thm)],[c_311,c_313,c_312]) ).
tcf(c_323,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c7 )
| ( multiply(sk_c7,multiply(X0,sk_c7)) != sk_c6 ) ),
inference(demodulation,[status(thm)],[c_310]) ).
tcf(c_324,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_309]) ).
tcf(c_325,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_308]) ).
tcf(c_326,negated_conjecture,
( ( iPr_def_16 = sk_c7 )
| ( iPr_def_15 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_97,c_315,c_314]) ).
tcf(c_327,negated_conjecture,
( ( iPr_def_17 = sk_c7 )
| ( iPr_def_16 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_96,c_316]) ).
tcf(c_328,negated_conjecture,
( ( iPr_def_16 = sk_c7 )
| ( iPr_def_13 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_95]) ).
tcf(c_329,negated_conjecture,
( ( iPr_def_16 = sk_c7 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_94]) ).
tcf(c_330,negated_conjecture,
( ( iPr_def_18 = sk_c3 )
| ( iPr_def_15 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_93,c_317]) ).
tcf(c_331,negated_conjecture,
( ( iPr_def_18 = sk_c3 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_92]) ).
tcf(c_332,negated_conjecture,
( ( iPr_def_18 = sk_c3 )
| ( iPr_def_13 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_91]) ).
tcf(c_333,negated_conjecture,
( ( iPr_def_18 = sk_c3 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_90]) ).
tcf(c_334,negated_conjecture,
( ( iPr_def_19 = sk_c6 )
| ( iPr_def_15 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_89,c_318]) ).
tcf(c_335,negated_conjecture,
( ( iPr_def_19 = sk_c6 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_88]) ).
tcf(c_336,negated_conjecture,
( ( iPr_def_19 = sk_c6 )
| ( iPr_def_13 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_87]) ).
tcf(c_337,negated_conjecture,
( ( iPr_def_19 = sk_c6 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_86]) ).
tcf(c_338,negated_conjecture,
( ( iPr_def_20 = sk_c6 )
| ( iPr_def_15 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_85,c_319]) ).
tcf(c_339,negated_conjecture,
( ( iPr_def_20 = sk_c6 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_84]) ).
tcf(c_340,negated_conjecture,
( ( iPr_def_20 = sk_c6 )
| ( iPr_def_13 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_83]) ).
tcf(c_341,negated_conjecture,
( ( iPr_def_20 = sk_c6 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_82]) ).
tcf(c_342,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_15 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_81,c_320]) ).
tcf(c_343,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_17 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_80]) ).
tcf(c_344,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_13 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_79]) ).
tcf(c_345,negated_conjecture,
( ( iPr_def_21 = sk_c7 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_78]) ).
tcf(c_346,negated_conjecture,
iPr_def_22 = sk_c5,
inference(demodulation,[status(thm)],[c_77,c_321]) ).
tcf(c_526,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( sk_c7 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_329,c_346]) ).
tcf(c_547,plain,
multiply(sk_c7,iPr_def_22) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_312,c_346]) ).
tcf(c_565,plain,
( ( sk_c7 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_16) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_326,c_317]) ).
tcf(c_572,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(iPr_def_16,sk_c3) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_526,c_318]) ).
tcf(c_574,plain,
( ( sk_c7 = iPr_def_15 )
| ( multiply(iPr_def_16,sk_c3) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_326,c_318]) ).
tcf(c_590,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( sk_c3 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_333,c_346]) ).
tcf(c_597,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(sk_c7,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_590,c_318]) ).
tcf(c_645,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( sk_c6 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_337,c_346]) ).
tcf(c_654,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( inverse(iPr_def_19) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_645,c_313]) ).
tcf(c_708,plain,
( ( sk_c7 = iPr_def_17 )
| ( inverse(iPr_def_20) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_339,c_313]) ).
tcf(c_744,plain,
( ( sk_c6 = iPr_def_13 )
| ( inverse(iPr_def_20) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_340,c_313]) ).
tcf(c_772,plain,
( ( sk_c6 = iPr_def_13 )
| ( multiply(sk_c1,iPr_def_19) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_336,c_320]) ).
tcf(c_773,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(sk_c1,iPr_def_19) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_335,c_320]) ).
tcf(c_814,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_20,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_339,c_321]) ).
tcf(c_815,plain,
( ( sk_c7 = iPr_def_15 )
| ( multiply(iPr_def_20,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_338,c_321]) ).
tcf(c_854,plain,
multiply(iPr_def_14,sk_c6) = identity,
inference(superposition,[status(thm)],[c_313,c_75]) ).
tcf(c_855,plain,
multiply(iPr_def_17,sk_c4) = identity,
inference(superposition,[status(thm)],[c_316,c_75]) ).
tcf(c_856,plain,
multiply(iPr_def_20,sk_c1) = identity,
inference(superposition,[status(thm)],[c_319,c_75]) ).
tcf(c_857,plain,
multiply(iPr_def_16,sk_c2) = identity,
inference(superposition,[status(thm)],[c_315,c_75]) ).
tcf(c_868,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( sk_c6 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_341,c_346]) ).
tcf(c_880,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(iPr_def_20,sk_c7) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_868,c_321]) ).
tcf(c_951,plain,
( ( sk_c6 = iPr_def_13 )
| ( multiply(iPr_def_14,iPr_def_20) = identity ) ),
inference(superposition,[status(thm)],[c_340,c_854]) ).
tcf(c_954,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(iPr_def_14,iPr_def_19) = identity ) ),
inference(superposition,[status(thm)],[c_645,c_854]) ).
tcf(c_1006,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_21,sk_c3) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_343,c_318]) ).
tcf(c_1052,plain,
( ( sk_c7 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_13) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_344,c_320]) ).
tcf(c_1117,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( sk_c7 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_345,c_346]) ).
tcf(c_1153,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != iPr_def_22 )
| ( sk_c6 != iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_322,c_346]) ).
tcf(c_1176,plain,
( ~ iPr_def_11
| ( sk_c7 != iPr_def_15 )
| ( inverse(sk_c4) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_314,c_324]) ).
tcf(c_1179,plain,
( ~ iPr_def_11
| ( sk_c7 != identity )
| ( inverse(iPr_def_14) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_854,c_324]) ).
tcf(c_1196,plain,
( ~ iPr_def_11
| ( sk_c7 != iPr_def_17 )
| ( sk_c7 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_1176,c_316]) ).
tcf(c_1327,plain,
( ~ iPr_def_10
| ( sk_c6 != sk_c7 )
| ( inverse(identity) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_74,c_325]) ).
tcf(c_1329,plain,
( ~ iPr_def_10
| ( sk_c7 != identity )
| ( inverse(iPr_def_14) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_854,c_325]) ).
tcf(c_1663,plain,
! [X0: $i] : multiply(sk_c6,multiply(sk_c7,X0)) = multiply(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_321,c_76]) ).
tcf(c_1664,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c6,X0)) = multiply(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_320,c_76]) ).
tcf(c_1665,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c6,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_314,c_76]) ).
tcf(c_1666,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c3,X0)) = multiply(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_318,c_76]) ).
tcf(c_1667,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c7,X0)) = multiply(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_317,c_76]) ).
tcf(c_1669,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_75,c_76]) ).
tcf(c_1671,plain,
! [X0: $i] : multiply(sk_c7,multiply(iPr_def_22,X0)) = multiply(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_547,c_76]) ).
tcf(c_1672,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_854,c_76]) ).
tcf(c_1673,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_855,c_76]) ).
tcf(c_1674,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_856,c_76]) ).
tcf(c_1675,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_857,c_76]) ).
tcf(c_1680,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_1675,c_74]) ).
tcf(c_1681,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_1674,c_74]) ).
tcf(c_1682,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_1673,c_74]) ).
tcf(c_1683,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_1672,c_74]) ).
tcf(c_2098,plain,
multiply(iPr_def_16,iPr_def_18) = sk_c7,
inference(superposition,[status(thm)],[c_317,c_1680]) ).
tcf(c_2106,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(iPr_def_18,X0)) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_2098,c_76]) ).
tcf(c_2189,plain,
multiply(iPr_def_20,iPr_def_21) = sk_c6,
inference(superposition,[status(thm)],[c_320,c_1681]) ).
tcf(c_2192,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(iPr_def_21,X0)) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_2189,c_76]) ).
tcf(c_2199,plain,
multiply(iPr_def_17,iPr_def_15) = sk_c6,
inference(superposition,[status(thm)],[c_314,c_1682]) ).
tcf(c_2202,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(iPr_def_15,X0)) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_2199,c_76]) ).
tcf(c_2204,plain,
multiply(iPr_def_14,iPr_def_22) = sk_c7,
inference(superposition,[status(thm)],[c_321,c_1683]) ).
tcf(c_2280,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(iPr_def_22,X0)) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_2204,c_76]) ).
tcf(c_2429,plain,
( ( sk_c7 = iPr_def_15 )
| ( multiply(iPr_def_16,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_330,c_574]) ).
tcf(c_2431,plain,
( ( sk_c7 = iPr_def_19 )
| ( sk_c7 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_2429,c_2098]) ).
tcf(c_3195,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(iPr_def_16,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_590,c_572]) ).
tcf(c_3200,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( sk_c7 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_3195,c_2098]) ).
tcf(c_3237,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(sk_c6,iPr_def_19) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_3200,c_321]) ).
tcf(c_3399,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(iPr_def_21,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1117,c_597]) ).
tcf(c_3698,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_343,c_814]) ).
tcf(c_3705,plain,
( ( sk_c7 = iPr_def_17 )
| ( sk_c6 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_3698,c_2189]) ).
tcf(c_3776,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_14,iPr_def_22) = identity ) ),
inference(superposition,[status(thm)],[c_3705,c_854]) ).
tcf(c_3781,plain,
( ( iPr_def_20 = iPr_def_22 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_3705,c_339]) ).
tcf(c_3785,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_3705,c_335]) ).
tcf(c_3802,plain,
( ( sk_c7 = iPr_def_17 )
| ( sk_c7 = identity ) ),
inference(light_normalisation,[status(thm)],[c_3776,c_2204]) ).
tcf(c_4001,plain,
( ( iPr_def_20 = iPr_def_22 )
| ( multiply(sk_c6,iPr_def_17) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_3781,c_321]) ).
tcf(c_4185,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( multiply(sk_c6,iPr_def_17) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_3785,c_321]) ).
tcf(c_4264,plain,
( ( sk_c7 = iPr_def_15 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_342,c_815]) ).
tcf(c_4269,plain,
( ( sk_c7 = iPr_def_15 )
| ~ iPr_def_12
| ( inverse(iPr_def_20) != sk_c7 )
| ( multiply(sk_c7,iPr_def_22) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_815,c_323]) ).
tcf(c_4272,plain,
( ( sk_c7 = iPr_def_15 )
| ( sk_c6 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_4264,c_2189]) ).
tcf(c_4710,plain,
( ( sk_c7 = iPr_def_15 )
| ( multiply(iPr_def_14,iPr_def_22) = identity ) ),
inference(superposition,[status(thm)],[c_4272,c_854]) ).
tcf(c_4720,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( sk_c7 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4272,c_334]) ).
tcf(c_4736,plain,
( ( sk_c7 = iPr_def_15 )
| ( sk_c7 = identity ) ),
inference(light_normalisation,[status(thm)],[c_4710,c_2204]) ).
tcf(c_5038,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( multiply(iPr_def_15,iPr_def_22) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_4720,c_547]) ).
tcf(c_5216,plain,
( ( identity = iPr_def_21 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_3802,c_343]) ).
tcf(c_5219,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(identity,sk_c3) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_3802,c_318]) ).
tcf(c_5221,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(identity,iPr_def_22) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_3802,c_547]) ).
tcf(c_5478,plain,
( ( identity = iPr_def_19 )
| ( sk_c7 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4736,c_2431]) ).
tcf(c_5486,plain,
( ( identity = iPr_def_21 )
| ( sk_c7 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4736,c_342]) ).
tcf(c_5493,plain,
( ( identity = iPr_def_16 )
| ( sk_c7 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4736,c_326]) ).
tcf(c_5975,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( identity = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_5486,c_5216]) ).
tcf(c_6130,plain,
( ( identity = iPr_def_16 )
| ( multiply(iPr_def_15,iPr_def_22) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_5493,c_547]) ).
tcf(c_6496,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_1117,c_880]) ).
tcf(c_6504,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( sk_c6 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_6496,c_2189]) ).
tcf(c_6698,plain,
( ( identity = iPr_def_19 )
| ( multiply(iPr_def_15,iPr_def_22) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_5478,c_547]) ).
tcf(c_6957,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(iPr_def_14,iPr_def_22) = identity ) ),
inference(superposition,[status(thm)],[c_6504,c_854]) ).
tcf(c_6983,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( sk_c7 = identity ) ),
inference(light_normalisation,[status(thm)],[c_6957,c_2204]) ).
tcf(c_7342,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( identity = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_6983,c_3200]) ).
tcf(c_7703,plain,
( ( sk_c7 = iPr_def_21 )
| ( multiply(iPr_def_20,iPr_def_21) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_1052,c_1681]) ).
tcf(c_7704,plain,
( ( sk_c7 = iPr_def_21 )
| ( sk_c6 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_7703,c_2189]) ).
tcf(c_8170,plain,
multiply(sk_c6,iPr_def_19) = multiply(iPr_def_22,sk_c3),
inference(superposition,[status(thm)],[c_318,c_1663]) ).
tcf(c_8171,plain,
multiply(sk_c6,iPr_def_13) = multiply(iPr_def_22,iPr_def_22),
inference(superposition,[status(thm)],[c_547,c_1663]) ).
tcf(c_8414,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(iPr_def_20,iPr_def_19) = multiply(iPr_def_22,sk_c3) ) ),
inference(superposition,[status(thm)],[c_868,c_8170]) ).
tcf(c_8415,plain,
( ( sk_c6 = iPr_def_13 )
| ( multiply(iPr_def_20,iPr_def_19) = multiply(iPr_def_22,sk_c3) ) ),
inference(superposition,[status(thm)],[c_340,c_8170]) ).
tcf(c_8416,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_20,iPr_def_19) = multiply(iPr_def_22,sk_c3) ) ),
inference(superposition,[status(thm)],[c_339,c_8170]) ).
tcf(c_8417,plain,
( ( sk_c7 = iPr_def_15 )
| ( multiply(iPr_def_20,iPr_def_19) = multiply(iPr_def_22,sk_c3) ) ),
inference(superposition,[status(thm)],[c_338,c_8170]) ).
tcf(c_8424,plain,
multiply(iPr_def_14,multiply(iPr_def_22,sk_c3)) = iPr_def_19,
inference(superposition,[status(thm)],[c_8170,c_1683]) ).
tcf(c_8546,plain,
multiply(iPr_def_14,multiply(iPr_def_22,iPr_def_22)) = iPr_def_13,
inference(superposition,[status(thm)],[c_8171,c_1683]) ).
tcf(c_8714,plain,
multiply(sk_c1,multiply(iPr_def_22,sk_c3)) = multiply(iPr_def_21,iPr_def_19),
inference(superposition,[status(thm)],[c_8170,c_1664]) ).
tcf(c_8876,plain,
multiply(sk_c4,iPr_def_22) = multiply(iPr_def_15,sk_c7),
inference(superposition,[status(thm)],[c_321,c_1665]) ).
tcf(c_9190,plain,
multiply(sk_c2,iPr_def_13) = multiply(iPr_def_18,iPr_def_22),
inference(superposition,[status(thm)],[c_547,c_1667]) ).
tcf(c_12636,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1669,c_74]) ).
tcf(c_12656,plain,
multiply(inverse(sk_c6),iPr_def_22) = sk_c7,
inference(superposition,[status(thm)],[c_321,c_12636]) ).
tcf(c_12661,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_74,c_12636]) ).
tcf(c_12662,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_75,c_12636]) ).
tcf(c_12664,plain,
multiply(inverse(sk_c7),iPr_def_13) = iPr_def_22,
inference(superposition,[status(thm)],[c_547,c_12636]) ).
tcf(c_12760,plain,
! [X0: $i] : multiply(inverse(iPr_def_14),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_1683,c_12636]) ).
tcf(c_12761,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_1682,c_12636]) ).
tcf(c_12762,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_1681,c_12636]) ).
tcf(c_12763,plain,
! [X0: $i] : multiply(inverse(iPr_def_16),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_1680,c_12636]) ).
tcf(c_12802,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_12636,c_12636]) ).
tcf(c_13792,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_12662,c_12802]) ).
tcf(c_13804,plain,
multiply(sk_c7,identity) = multiply(iPr_def_14,iPr_def_22),
inference(superposition,[status(thm)],[c_13792,c_2280]) ).
tcf(c_13805,plain,
multiply(sk_c7,iPr_def_22) = multiply(iPr_def_13,identity),
inference(superposition,[status(thm)],[c_13792,c_1671]) ).
tcf(c_13812,plain,
multiply(sk_c6,identity) = multiply(iPr_def_17,iPr_def_15),
inference(superposition,[status(thm)],[c_13792,c_2202]) ).
tcf(c_13816,plain,
multiply(sk_c7,sk_c3) = multiply(iPr_def_19,identity),
inference(superposition,[status(thm)],[c_13792,c_1666]) ).
tcf(c_13817,plain,
multiply(sk_c7,identity) = multiply(iPr_def_16,iPr_def_18),
inference(superposition,[status(thm)],[c_13792,c_2106]) ).
tcf(c_13826,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_13792,c_12661]) ).
tcf(c_13827,plain,
multiply(sk_c7,identity) = sk_c7,
inference(light_normalisation,[status(thm)],[c_13817,c_2098]) ).
tcf(c_13828,plain,
multiply(iPr_def_19,identity) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_13816,c_318]) ).
tcf(c_13835,plain,
multiply(iPr_def_13,identity) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_13805,c_547]) ).
tcf(c_13859,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( inverse(iPr_def_19) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_7342,c_13826]) ).
tcf(c_15722,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(iPr_def_22,sk_c3) = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_3237,c_8170]) ).
tcf(c_15892,plain,
multiply(sk_c6,iPr_def_14) = identity,
inference(superposition,[status(thm)],[c_12760,c_75]) ).
tcf(c_15895,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_14)) != sk_c7 )
| ( multiply(sk_c7,multiply(sk_c6,sk_c7)) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_12760,c_323]) ).
tcf(c_15896,plain,
! [X0: $i] : multiply(sk_c6,multiply(iPr_def_14,X0)) = X0,
inference(superposition,[status(thm)],[c_12760,c_12636]) ).
tcf(c_15897,plain,
multiply(sk_c6,identity) = inverse(iPr_def_14),
inference(superposition,[status(thm)],[c_12760,c_13792]) ).
tcf(c_15904,plain,
( ~ iPr_def_12
| ( sk_c6 != iPr_def_13 )
| ( inverse(inverse(iPr_def_14)) != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_15895,c_321,c_547]) ).
tcf(c_15995,plain,
multiply(sk_c4,identity) = multiply(iPr_def_15,iPr_def_14),
inference(superposition,[status(thm)],[c_15892,c_1665]) ).
tcf(c_15996,plain,
multiply(sk_c1,identity) = multiply(iPr_def_21,iPr_def_14),
inference(superposition,[status(thm)],[c_15892,c_1664]) ).
tcf(c_16065,plain,
inverse(iPr_def_14) = sk_c6,
inference(demodulation,[status(thm)],[c_15897,c_13792]) ).
tcf(c_16088,plain,
! [X0: $i] :
( ( sk_c6 = iPr_def_13 )
| ( multiply(iPr_def_19,multiply(iPr_def_14,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_336,c_15896]) ).
tcf(c_16097,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(sk_c6,identity) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_954,c_15896]) ).
tcf(c_16104,plain,
multiply(sk_c6,sk_c7) = iPr_def_22,
inference(superposition,[status(thm)],[c_2204,c_15896]) ).
tcf(c_17138,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( multiply(sk_c6,iPr_def_18) = multiply(iPr_def_20,iPr_def_19) ) ),
inference(superposition,[status(thm)],[c_3399,c_2192]) ).
tcf(c_17222,plain,
multiply(iPr_def_15,iPr_def_14) = sk_c4,
inference(demodulation,[status(thm)],[c_15995,c_13792]) ).
tcf(c_17288,plain,
multiply(iPr_def_21,iPr_def_14) = sk_c1,
inference(demodulation,[status(thm)],[c_15996,c_13792]) ).
tcf(c_17309,plain,
( ( sk_c6 = iPr_def_13 )
| ( multiply(iPr_def_20,iPr_def_19) = multiply(iPr_def_22,iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_332,c_8415]) ).
tcf(c_17373,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_20,iPr_def_19) = multiply(iPr_def_22,iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_331,c_8416]) ).
tcf(c_18709,plain,
( ( iPr_def_20 = iPr_def_22 )
| ( multiply(inverse(sk_c6),iPr_def_22) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_4001,c_12636]) ).
tcf(c_18731,plain,
( ~ iPr_def_10
| ( inverse(inverse(iPr_def_17)) != sk_c6 )
| ( multiply(sk_c4,sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_12761,c_325]) ).
tcf(c_18732,plain,
( ~ iPr_def_11
| ( inverse(inverse(iPr_def_17)) != sk_c7 )
| ( multiply(sk_c4,sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_12761,c_324]) ).
tcf(c_18733,plain,
multiply(sk_c4,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_12761,c_75]) ).
tcf(c_18736,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_17)) != sk_c7 )
| ( multiply(sk_c7,multiply(sk_c4,sk_c7)) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_12761,c_323]) ).
tcf(c_18737,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_17,X0)) = X0,
inference(superposition,[status(thm)],[c_12761,c_12636]) ).
tcf(c_18738,plain,
multiply(sk_c4,identity) = inverse(iPr_def_17),
inference(superposition,[status(thm)],[c_12761,c_13792]) ).
tcf(c_18743,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_15 )
| ( inverse(inverse(iPr_def_17)) != sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_18731,c_314]) ).
tcf(c_19519,plain,
inverse(iPr_def_17) = sk_c4,
inference(demodulation,[status(thm)],[c_18738,c_13792]) ).
tcf(c_19530,plain,
multiply(sk_c4,sk_c6) = iPr_def_15,
inference(superposition,[status(thm)],[c_2199,c_18737]) ).
tcf(c_19591,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_20)) != sk_c7 )
| ( multiply(sk_c7,multiply(sk_c1,sk_c7)) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_12762,c_323]) ).
tcf(c_19593,plain,
multiply(sk_c1,identity) = inverse(iPr_def_20),
inference(superposition,[status(thm)],[c_12762,c_13792]) ).
tcf(c_22559,plain,
( ( sk_c6 = iPr_def_13 )
| ( multiply(iPr_def_19,identity) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_951,c_16088]) ).
tcf(c_22717,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( multiply(inverse(sk_c6),iPr_def_22) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_4185,c_12636]) ).
tcf(c_22793,plain,
inverse(iPr_def_20) = sk_c1,
inference(demodulation,[status(thm)],[c_19593,c_13792]) ).
tcf(c_22796,plain,
( ( sk_c1 = iPr_def_14 )
| ( sk_c6 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_744,c_22793]) ).
tcf(c_22797,plain,
( ( sk_c1 = iPr_def_14 )
| ( sk_c7 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_708,c_22793]) ).
tcf(c_23202,plain,
( ( sk_c6 = iPr_def_13 )
| ( multiply(iPr_def_14,multiply(iPr_def_20,iPr_def_19)) = multiply(sk_c7,iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_17309,c_2280]) ).
tcf(c_23285,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_14,multiply(iPr_def_20,iPr_def_19)) = multiply(sk_c7,iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_17373,c_2280]) ).
tcf(c_24261,plain,
( ( sk_c6 = iPr_def_13 )
| ( multiply(iPr_def_14,iPr_def_19) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_22796,c_772]) ).
tcf(c_24265,plain,
( ( sk_c6 = iPr_def_13 )
| ( inverse(iPr_def_14) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_22796,c_319]) ).
tcf(c_24287,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_14,iPr_def_19) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_22797,c_773]) ).
tcf(c_24723,plain,
( ~ iPr_def_11
| ( inverse(iPr_def_14) != sk_c7 ) ),
inference(global_subsumption_just,[status(thm)],[c_1179,c_1196,c_1179,c_3802,c_4736]) ).
tcf(c_24725,plain,
( ~ iPr_def_11
| ( sk_c6 != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_24723,c_16065]) ).
tcf(c_24751,plain,
( ( sk_c6 = iPr_def_13 )
| ~ iPr_def_11
| ( sk_c7 != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_336,c_24725]) ).
tcf(c_24752,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_11
| ( sk_c7 != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_335,c_24725]) ).
tcf(c_24753,plain,
( ( sk_c7 = iPr_def_15 )
| ~ iPr_def_11
| ( sk_c7 != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_334,c_24725]) ).
tcf(c_25045,plain,
multiply(sk_c2,iPr_def_16) = identity,
inference(superposition,[status(thm)],[c_12763,c_75]) ).
tcf(c_25048,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_16)) != sk_c7 )
| ( multiply(sk_c7,multiply(sk_c2,sk_c7)) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_12763,c_323]) ).
tcf(c_25049,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_16,X0)) = X0,
inference(superposition,[status(thm)],[c_12763,c_12636]) ).
tcf(c_25050,plain,
multiply(sk_c2,identity) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_12763,c_13792]) ).
tcf(c_25057,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_16)) != sk_c7 )
| ( multiply(sk_c7,iPr_def_18) != sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_25048,c_317]) ).
tcf(c_25062,plain,
( ( identity = iPr_def_18 )
| ( sk_c7 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_565,c_25045]) ).
tcf(c_25095,plain,
inverse(iPr_def_16) = sk_c2,
inference(demodulation,[status(thm)],[c_25050,c_13792]) ).
tcf(c_25104,plain,
multiply(sk_c2,sk_c7) = iPr_def_18,
inference(superposition,[status(thm)],[c_2098,c_25049]) ).
tcf(c_25562,plain,
( ( sk_c7 != iPr_def_19 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_24751,c_1196,c_24753,c_24752]) ).
tcf(c_25563,plain,
( ~ iPr_def_11
| ( sk_c7 != iPr_def_19 ) ),
inference(renaming,[status(thm)],[c_25562]) ).
tcf(c_25585,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_11
| ( identity != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_3802,c_25563]) ).
tcf(c_25595,plain,
( ( sk_c7 = iPr_def_15 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_2431,c_25563]) ).
tcf(c_25881,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( identity = iPr_def_18 )
| ( sk_c7 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_25062,c_327]) ).
tcf(c_26990,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( identity = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_16) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_25881,c_317]) ).
tcf(c_26999,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( identity = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_26990,c_25045]) ).
tcf(c_27004,plain,
( ~ iPr_def_10
| ( sk_c6 != identity )
| ( sk_c6 != sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_1327,c_13826]) ).
tcf(c_27260,plain,
( ( iPr_def_18 = iPr_def_21 )
| ( iPr_def_15 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_26999,c_5975]) ).
tcf(c_27946,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(iPr_def_18,iPr_def_14) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_27260,c_17288]) ).
tcf(c_28423,plain,
( ~ iPr_def_10
| ( sk_c7 != identity ) ),
inference(ground_joinability,[status(thm)],[c_1329,c_16065]) ).
tcf(c_28447,plain,
( ( sk_c7 = iPr_def_15 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_4736,c_28423]) ).
tcf(c_28449,plain,
( ( sk_c7 = iPr_def_17 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_3802,c_28423]) ).
tcf(c_28839,plain,
( ( sk_c3 = iPr_def_19 )
| ( sk_c7 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_5219,c_74]) ).
tcf(c_28859,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_20,iPr_def_19) = multiply(iPr_def_22,iPr_def_19) ) ),
inference(superposition,[status(thm)],[c_28839,c_8416]) ).
tcf(c_28875,plain,
( ( sk_c7 = iPr_def_17 )
| ( multiply(iPr_def_21,iPr_def_19) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_28839,c_1006]) ).
tcf(c_28883,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c7 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_28839,c_331]) ).
tcf(c_29520,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_28875,c_28859,c_28883,c_28449,c_28447,c_27946,c_27004,c_25595,c_25585,c_25104,c_25095,c_25057,c_25045,c_24287,c_24265,c_24261,c_23285,c_23202,c_22793,c_22717,c_22559,c_19591,c_19530,c_19519,c_18743,c_18736,c_18732,c_18733,c_18709,c_17222,c_17138,c_16104,c_16097,c_16065,c_15904,c_15897,c_15892,c_15722,c_13859,c_13835,c_13828,c_13827,c_13817,c_13812,c_13805,c_13804,c_12664,c_12656,c_9190,c_8876,c_8714,c_8546,c_8424,c_8414,c_8417,c_8416,c_8415,c_7704,c_6698,c_6130,c_5221,c_5038,c_4269,c_1196,c_1153,c_654,c_346,c_343,c_339,c_329,c_328,c_327,c_326,c_319,c_316,c_315,c_313]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP326-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.08/0.36 % Computer : n016.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Wed Sep 23 14:33:26 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 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.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.42 % Detected problem language: tptp
% 0.14/0.43 % Proving...
% 5.43/2.17 % SZS status Started for theBenchmark.p
% 5.43/2.17 % SZS status Unsatisfiable for theBenchmark.p
% 5.43/2.17
% 5.43/2.17 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 5.43/2.17
% 5.43/2.17 % ------ iProver source info
% 5.43/2.17
% 5.43/2.17 % git: date: 2026-07-19 20:42:38 +0200
% 5.43/2.17 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 5.43/2.17 % git: non_committed_changes: false
% 5.43/2.17
% 5.43/2.17 % ------ Parsing...% successful
% 5.43/2.17
% 5.43/2.17
% 5.43/2.17 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 5.43/2.17
% 5.43/2.17 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 5.43/2.17
% 5.43/2.17 % ------ Preprocessing... gs_s sp: 3 0s gs_e snvd_s sp: 0 0s snvd_e %
% 5.43/2.17
% 5.43/2.17 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 5.43/2.17 % ------ Proving...
% 5.43/2.17 % ------ Problem Properties
% 5.43/2.17
% 5.43/2.17 %
% 5.43/2.17 % clauses 38
% 5.43/2.17 % conjectures 25
% 5.43/2.17 % EPR 22
% 5.43/2.17 % Horn 17
% 5.43/2.17 % unary 14
% 5.43/2.17 % binary 20
% 5.43/2.17 % lits 68
% 5.43/2.17 % lits eq 62
% 5.43/2.17 % fd_pure 0
% 5.43/2.17 % fd_pseudo 0
% 5.43/2.17 % fd_cond 0
% 5.43/2.17 % fd_pseudo_cond 0
% 5.43/2.17 % AC symbols 0
% 5.43/2.17
% 5.43/2.17 % ------ Schedule dynamic 5 is on
% 5.43/2.17
% 5.43/2.17 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 5.43/2.17
% 5.43/2.17
% 5.43/2.17 % ------
% 5.43/2.17 % Current options:
% 5.43/2.17 % ------
% 5.43/2.17
% 5.43/2.17
% 5.43/2.17 %
% 5.43/2.17
% 5.43/2.17 % ------ Proving...
% 5.43/2.17 %
% 5.43/2.17
% 5.43/2.17 % SZS status Unsatisfiable for theBenchmark.p
% 5.43/2.17
% 5.43/2.17 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 9.88/2.17
% 9.88/2.17
%------------------------------------------------------------------------------