%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT351+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 : Sun Sep 27 07:50:21 AM UTC 2026
% Result : Theorem 9.15s 1.58s
% Output : CNFRefutation 9.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 9
% Syntax : Number of formulae : 108 ( 34 unt; 0 def)
% Number of atoms : 593 ( 30 equ)
% Maximal formula atoms : 21 ( 5 avg)
% Number of connectives : 859 ( 374 ~; 369 |; 107 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 26 ( 24 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-1 aty)
% Number of variables : 132 ( 15 sgn 17 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(dt_k2_yellow_1,axiom,
! [A] :
( l1_orders_2(k2_yellow_1(A))
& v1_orders_2(k2_yellow_1(A)) ),
file('theBenchmark.p',dt_k2_yellow_1) ).
fof(dt_k3_yellow_1,axiom,
! [A] :
( l1_orders_2(k3_yellow_1(A))
& v1_orders_2(k3_yellow_1(A)) ),
file('theBenchmark.p',dt_k3_yellow_1) ).
fof(fc14_waybel_8,axiom,
! [A] :
( v2_waybel_8(k3_yellow_1(A))
& v1_waybel_8(k3_yellow_1(A))
& v3_waybel_3(k3_yellow_1(A))
& v2_waybel_3(k3_yellow_1(A))
& v11_waybel_1(k3_yellow_1(A))
& v10_waybel_1(k3_yellow_1(A))
& v9_waybel_1(k3_yellow_1(A))
& v2_waybel_1(k3_yellow_1(A))
& v25_waybel_0(k3_yellow_1(A))
& v24_waybel_0(k3_yellow_1(A))
& v3_yellow_0(k3_yellow_1(A))
& v2_yellow_0(k3_yellow_1(A))
& v1_yellow_0(k3_yellow_1(A))
& v3_lattice3(k3_yellow_1(A))
& v2_lattice3(k3_yellow_1(A))
& v1_lattice3(k3_yellow_1(A))
& v4_orders_2(k3_yellow_1(A))
& v3_orders_2(k3_yellow_1(A))
& v2_orders_2(k3_yellow_1(A))
& v1_orders_2(k3_yellow_1(A))
& ~ v3_struct_0(k3_yellow_1(A)) ),
file('theBenchmark.p',fc14_waybel_8) ).
fof(fc1_waybel22,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v2_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ( v3_waybel_3(k2_yellow_1(k9_waybel_0(A)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(A)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(A)))
& v1_lattice3(k2_yellow_1(k9_waybel_0(A)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(A)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(A)))
& v3_yellow_0(k2_yellow_1(k9_waybel_0(A)))
& v2_yellow_0(k2_yellow_1(k9_waybel_0(A)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(A)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(A)))
& ~ v3_struct_0(k2_yellow_1(k9_waybel_0(A))) ) ),
file('theBenchmark.p',fc1_waybel22) ).
fof(fc2_waybel16,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_yellow_0(A)
& v2_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ( v25_waybel_0(k2_yellow_1(k9_waybel_0(A)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(A)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(A)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(A)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(A)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(A)))
& ~ v3_struct_0(k2_yellow_1(k9_waybel_0(A))) ) ),
file('theBenchmark.p',fc2_waybel16) ).
fof(t10_waybel22,axiom,
! [A] : k1_card_1(k1_waybel22(A)) = k1_card_1(A),
file('theBenchmark.p',t10_waybel22) ).
fof(t16_waybel22,axiom,
! [A] : r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))),k1_waybel22(A)),
file('theBenchmark.p',t16_waybel22) ).
fof(t17_waybel22,axiom,
! [A] :
( ( l1_orders_2(A)
& v3_waybel_3(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v3_waybel_3(B)
& v3_lattice3(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C,D] :
( ( k1_card_1(C) = k1_card_1(D)
& r1_waybel22(B,D)
& r1_waybel22(A,C) )
=> r5_waybel_1(A,B) ) ) ),
file('theBenchmark.p',t17_waybel22) ).
fof(t18_waybel22,conjecture,
! [A,B] :
( ( l1_orders_2(B)
& v3_waybel_3(B)
& v3_lattice3(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( k1_card_1(C) = k1_card_1(A)
& r1_waybel22(B,C) )
=> r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))) ) ),
file('theBenchmark.p',t18_waybel22) ).
fof(t18_waybel22_neg,negated_conjecture,
~ ! [A,B] :
( ( l1_orders_2(B)
& v3_waybel_3(B)
& v3_lattice3(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( k1_card_1(C) = k1_card_1(A)
& r1_waybel22(B,C) )
=> r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))) ) ),
inference(assume_negation,[status(cth)],[t18_waybel22]) ).
cnf(c_334,plain,
l1_orders_2(k2_yellow_1(A)),
inference(clausify,[status(thm)],[dt_k2_yellow_1]) ).
cnf(c_335,plain,
l1_orders_2(k3_yellow_1(A)),
inference(clausify,[status(thm)],[dt_k3_yellow_1]) ).
cnf(c_362,plain,
~ v3_struct_0(k3_yellow_1(A)),
inference(clausify,[status(thm)],[fc14_waybel_8]) ).
cnf(c_363,plain,
v2_orders_2(k3_yellow_1(A)),
inference(clausify,[status(thm)],[fc14_waybel_8]) ).
cnf(c_364,plain,
v3_orders_2(k3_yellow_1(A)),
inference(clausify,[status(thm)],[fc14_waybel_8]) ).
cnf(c_365,plain,
v4_orders_2(k3_yellow_1(A)),
inference(clausify,[status(thm)],[fc14_waybel_8]) ).
cnf(c_367,plain,
v2_lattice3(k3_yellow_1(A)),
inference(clausify,[status(thm)],[fc14_waybel_8]) ).
cnf(c_369,plain,
v2_yellow_0(k3_yellow_1(A)),
inference(clausify,[status(thm)],[fc14_waybel_8]) ).
cnf(c_382,plain,
( v1_lattice3(k2_yellow_1(k9_waybel_0(A)))
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v2_yellow_0(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_waybel22]) ).
cnf(c_385,plain,
( v3_waybel_3(k2_yellow_1(k9_waybel_0(A)))
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v2_yellow_0(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_waybel22]) ).
cnf(c_391,plain,
( v2_orders_2(k2_yellow_1(k9_waybel_0(A)))
| ~ l1_orders_2(A)
| ~ v2_yellow_0(A)
| ~ v2_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(clausify,[status(thm)],[fc2_waybel16]) ).
cnf(c_392,plain,
( v3_orders_2(k2_yellow_1(k9_waybel_0(A)))
| ~ l1_orders_2(A)
| ~ v2_yellow_0(A)
| ~ v2_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(clausify,[status(thm)],[fc2_waybel16]) ).
cnf(c_393,plain,
( v4_orders_2(k2_yellow_1(k9_waybel_0(A)))
| ~ l1_orders_2(A)
| ~ v2_yellow_0(A)
| ~ v2_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(clausify,[status(thm)],[fc2_waybel16]) ).
cnf(c_394,plain,
( v2_lattice3(k2_yellow_1(k9_waybel_0(A)))
| ~ l1_orders_2(A)
| ~ v2_yellow_0(A)
| ~ v2_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(clausify,[status(thm)],[fc2_waybel16]) ).
cnf(c_395,plain,
( v3_lattice3(k2_yellow_1(k9_waybel_0(A)))
| ~ l1_orders_2(A)
| ~ v2_yellow_0(A)
| ~ v2_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(clausify,[status(thm)],[fc2_waybel16]) ).
cnf(c_500,plain,
k1_card_1(k1_waybel22(A)) = k1_card_1(A),
inference(clausify,[status(thm)],[t10_waybel22]) ).
cnf(c_501,plain,
r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))),k1_waybel22(A)),
inference(clausify,[status(thm)],[t16_waybel22]) ).
cnf(c_502,plain,
( r5_waybel_1(A,B)
| k1_card_1(D) != k1_card_1(C)
| ~ r1_waybel22(B,D)
| ~ r1_waybel22(A,C)
| ~ l1_orders_2(B)
| ~ v3_waybel_3(B)
| ~ v3_lattice3(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(clausify,[status(thm)],[t17_waybel22]) ).
fof(nnf_120,plain,
? [A,B] :
( ? [C] :
( ~ r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
& k1_card_1(A) = k1_card_1(C)
& r1_waybel22(B,C) )
& l1_orders_2(B)
& v3_waybel_3(B)
& v3_lattice3(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) ),
inference(fof_nnf,[status(thm)],[t18_waybel22_neg]) ).
fof(sk_t18_waybel22_neg,plain,
( ~ r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK2))))
& k1_card_1(sK2) = k1_card_1(sK1)
& r1_waybel22(sK0,sK1)
& l1_orders_2(sK0)
& v3_waybel_3(sK0)
& v3_lattice3(sK0)
& v2_lattice3(sK0)
& v1_lattice3(sK0)
& v4_orders_2(sK0)
& v3_orders_2(sK0)
& v2_orders_2(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(A,sK2),skolemize(B,sK0),skolemize(C,sK1)],[nnf_120]) ).
cnf(c_512,negated_conjecture,
v2_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_513,negated_conjecture,
v3_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_514,negated_conjecture,
v4_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_515,negated_conjecture,
v1_lattice3(sK0),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_516,negated_conjecture,
v2_lattice3(sK0),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_517,negated_conjecture,
v3_lattice3(sK0),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_518,negated_conjecture,
v3_waybel_3(sK0),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_519,negated_conjecture,
l1_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_520,negated_conjecture,
r1_waybel22(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_521,negated_conjecture,
k1_card_1(sK2) = k1_card_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_522,negated_conjecture,
k1_card_1(sK1) = k1_card_1(sK2),
inference(copy,[status(thm)],[c_521]) ).
cnf(c_523,negated_conjecture,
~ r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK2)))),
inference(split_conjunct,[status(thm)],[sk_t18_waybel22_neg]) ).
cnf(c_5676,plain,
( v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A))
| ~ v2_orders_2(k3_yellow_1(A))
| v3_struct_0(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_382,c_369]) ).
cnf(c_5677,plain,
( v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A))
| ~ v2_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_362,c_5676]) ).
cnf(c_5678,plain,
( v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_363,c_5677]) ).
cnf(c_5679,plain,
( v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_364,c_5678]) ).
cnf(c_5680,plain,
( v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_365,c_5679]) ).
cnf(c_5681,plain,
( v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_367,c_5680]) ).
cnf(c_676,plain,
v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))),
inference(resolve,[status(thm)],[c_335,c_5681]) ).
cnf(c_5682,plain,
( v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A))
| ~ v2_orders_2(k3_yellow_1(A))
| v3_struct_0(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_385,c_369]) ).
cnf(c_5683,plain,
( v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A))
| ~ v2_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_362,c_5682]) ).
cnf(c_5684,plain,
( v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_363,c_5683]) ).
cnf(c_5685,plain,
( v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_364,c_5684]) ).
cnf(c_5686,plain,
( v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_365,c_5685]) ).
cnf(c_5687,plain,
( v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_367,c_5686]) ).
cnf(c_677,plain,
v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))),
inference(resolve,[status(thm)],[c_335,c_5687]) ).
cnf(c_5688,plain,
( v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A))
| ~ v2_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_391,c_369]) ).
cnf(c_5689,plain,
( v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_363,c_5688]) ).
cnf(c_5690,plain,
( v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_364,c_5689]) ).
cnf(c_5691,plain,
( v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_365,c_5690]) ).
cnf(c_5692,plain,
( v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_367,c_5691]) ).
cnf(c_680,plain,
v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))),
inference(resolve,[status(thm)],[c_335,c_5692]) ).
cnf(c_5693,plain,
( v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A))
| ~ v2_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_392,c_369]) ).
cnf(c_5694,plain,
( v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_363,c_5693]) ).
cnf(c_5695,plain,
( v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_364,c_5694]) ).
cnf(c_5696,plain,
( v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_365,c_5695]) ).
cnf(c_5697,plain,
( v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_367,c_5696]) ).
cnf(c_681,plain,
v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))),
inference(resolve,[status(thm)],[c_335,c_5697]) ).
cnf(c_5698,plain,
( v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A))
| ~ v2_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_393,c_369]) ).
cnf(c_5699,plain,
( v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_363,c_5698]) ).
cnf(c_5700,plain,
( v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_364,c_5699]) ).
cnf(c_5701,plain,
( v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_365,c_5700]) ).
cnf(c_5702,plain,
( v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_367,c_5701]) ).
cnf(c_682,plain,
v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))),
inference(resolve,[status(thm)],[c_335,c_5702]) ).
cnf(c_5703,plain,
( v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A))
| ~ v2_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_394,c_369]) ).
cnf(c_5704,plain,
( v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_363,c_5703]) ).
cnf(c_5705,plain,
( v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_364,c_5704]) ).
cnf(c_5706,plain,
( v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_365,c_5705]) ).
cnf(c_5707,plain,
( v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_367,c_5706]) ).
cnf(c_683,plain,
v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))),
inference(resolve,[status(thm)],[c_335,c_5707]) ).
cnf(c_5708,plain,
( v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A))
| ~ v2_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_395,c_369]) ).
cnf(c_5709,plain,
( v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A))
| ~ v3_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_363,c_5708]) ).
cnf(c_5710,plain,
( v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A))
| ~ v4_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_364,c_5709]) ).
cnf(c_5711,plain,
( v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A))
| ~ v2_lattice3(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_365,c_5710]) ).
cnf(c_5712,plain,
( v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| ~ l1_orders_2(k3_yellow_1(A)) ),
inference(resolve,[status(thm)],[c_367,c_5711]) ).
cnf(c_684,plain,
v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))),
inference(resolve,[status(thm)],[c_335,c_5712]) ).
cnf(c_5713,plain,
( r5_waybel_1(A,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(k1_waybel22(B)) != k1_card_1(C)
| ~ r1_waybel22(A,C)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(resolve,[status(thm)],[c_502,c_501]) ).
cnf(c_5714,plain,
( r5_waybel_1(A,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(C)
| ~ r1_waybel22(A,C)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(paramod,[status(thm)],[c_500,c_5713]) ).
cnf(c_5715,plain,
( r5_waybel_1(A,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(C)
| ~ r1_waybel22(A,C)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(resolve,[status(thm)],[c_680,c_5714]) ).
cnf(c_5716,plain,
( r5_waybel_1(A,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(C)
| ~ r1_waybel22(A,C)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(resolve,[status(thm)],[c_681,c_5715]) ).
cnf(c_5717,plain,
( r5_waybel_1(A,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(C)
| ~ r1_waybel22(A,C)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(resolve,[status(thm)],[c_682,c_5716]) ).
cnf(c_5718,plain,
( r5_waybel_1(A,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(C)
| ~ r1_waybel22(A,C)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(resolve,[status(thm)],[c_676,c_5717]) ).
cnf(c_5719,plain,
( r5_waybel_1(A,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(C)
| ~ r1_waybel22(A,C)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(resolve,[status(thm)],[c_683,c_5718]) ).
cnf(c_5720,plain,
( r5_waybel_1(A,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(C)
| ~ r1_waybel22(A,C)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(resolve,[status(thm)],[c_684,c_5719]) ).
cnf(c_5721,plain,
( r5_waybel_1(A,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(C)
| ~ r1_waybel22(A,C)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(resolve,[status(thm)],[c_677,c_5720]) ).
cnf(c_874,plain,
( r5_waybel_1(A,k2_yellow_1(k9_waybel_0(k3_yellow_1(C))))
| k1_card_1(C) != k1_card_1(B)
| ~ r1_waybel22(A,B)
| ~ l1_orders_2(A)
| ~ v3_waybel_3(A)
| ~ v3_lattice3(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(resolve,[status(thm)],[c_334,c_5721]) ).
cnf(c_5722,negated_conjecture,
( r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(A)
| ~ r1_waybel22(sK0,A)
| ~ l1_orders_2(sK0)
| ~ v3_waybel_3(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_874,c_512]) ).
cnf(c_5723,negated_conjecture,
( r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(A)
| ~ r1_waybel22(sK0,A)
| ~ l1_orders_2(sK0)
| ~ v3_waybel_3(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_5722,c_513]) ).
cnf(c_5724,negated_conjecture,
( r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(A)
| ~ r1_waybel22(sK0,A)
| ~ l1_orders_2(sK0)
| ~ v3_waybel_3(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_5723,c_514]) ).
cnf(c_5725,negated_conjecture,
( r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(A)
| ~ r1_waybel22(sK0,A)
| ~ l1_orders_2(sK0)
| ~ v3_waybel_3(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_5724,c_515]) ).
cnf(c_5726,negated_conjecture,
( r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(A)
| ~ r1_waybel22(sK0,A)
| ~ l1_orders_2(sK0)
| ~ v3_waybel_3(sK0)
| ~ v3_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_5725,c_516]) ).
cnf(c_5727,negated_conjecture,
( r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(A)
| ~ r1_waybel22(sK0,A)
| ~ l1_orders_2(sK0)
| ~ v3_waybel_3(sK0) ),
inference(resolve,[status(thm)],[c_5726,c_517]) ).
cnf(c_5728,negated_conjecture,
( r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(A)
| ~ r1_waybel22(sK0,A)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_5727,c_518]) ).
cnf(c_5729,negated_conjecture,
( r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(B))))
| k1_card_1(B) != k1_card_1(A)
| ~ r1_waybel22(sK0,A) ),
inference(resolve,[status(thm)],[c_5728,c_519]) ).
cnf(c_5730,negated_conjecture,
( r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
| k1_card_1(A) != k1_card_1(sK1) ),
inference(resolve,[status(thm)],[c_5729,c_520]) ).
cnf(c_5731,negated_conjecture,
k1_card_1(sK2) = k1_card_1(sK1),
inference(copy,[status(thm)],[c_522]) ).
cnf(c_5732,negated_conjecture,
r5_waybel_1(sK0,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK2)))),
inference(resolve,[status(thm)],[c_5730,c_5731]) ).
cnf(c_5675,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_523,c_5732]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT351+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/0.29 % Computer : n012.cluster.edu
% 0.04/0.29 % Model : x86_64 x86_64
% 0.04/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.29 % Memory : 8046.5625MB
% 0.04/0.29 % OS : Linux 6.8.0-71-generic
% 0.04/0.29 % CPULimit : 300
% 0.04/0.29 % WCLimit : 300
% 0.04/0.29 % DateTime : Fri Sep 25 21:11:20 UTC 2026
% 0.04/0.29 % CPUTime :
% 0.04/0.30 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.04/0.30 % Process 3035126 was started by sandbox2 on n012,
% 0.04/0.30 % Fri Sep 25 21:11:20 2026
% 0.04/0.30 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.04/0.33
% 0.04/0.33 % From the command line: assign(max_seconds, 300).
% 9.15/1.58
% 9.15/1.58 % given #500 (T,wt=18): 2160 c11 != c4 | u1_orders_2(c11) = u1_orders_2(c4). [para(538(a,1),1395(a,1)),flip(a)].
% 9.15/1.58
% 9.15/1.58 % given #1000 (F,wt=23): 4620 -r2_hidden(k1_zfmisc_1(u1_struct_0(c13)),k5_waybel_0(c13,f10(c13))). [resolve(4043,a,313,b)].
% 9.15/1.58
% 9.15/1.58 % SZS status Theorem for theBenchmark
% 9.15/1.58
% 9.15/1.58 % Proof 1 at 1.03 (+ 0.19) seconds.
% 9.15/1.58 % Length of proof is 48.
% 9.15/1.58 % Level of proof is 4.
% 9.15/1.58 % Maximum clause weight is 56.000.
% 9.15/1.58 % Given clauses 1198.
% 9.15/1.58
% 9.15/1.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------