%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : LAT351+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 10:34:35 PM UTC 2025
% Result : Theorem 32.02s 4.34s
% Output : CNFRefutation 32.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 15
% Syntax : Number of formulae : 215 ( 159 unt; 0 def)
% Number of atoms : 633 ( 10 equ)
% Maximal formula atoms : 21 ( 2 avg)
% Number of connectives : 696 ( 278 ~; 267 |; 130 &)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 3 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 : 59 ( 13 sgn 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t18_waybel22,plain,
! [A,B] :
( ( v2_orders_2(B)
& v3_orders_2(B)
& v4_orders_2(B)
& v1_lattice3(B)
& v2_lattice3(B)
& v3_lattice3(B)
& v3_waybel_3(B)
& l1_orders_2(B) )
=> ! [C] :
( ( r1_waybel22(B,C)
& k1_card_1(C) = k1_card_1(A) )
=> r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_waybel22) ).
fof(t18_waybel22_negated,plain,
~ ! [A,B] :
( ( v2_orders_2(B)
& v3_orders_2(B)
& v4_orders_2(B)
& v1_lattice3(B)
& v2_lattice3(B)
& v3_lattice3(B)
& v3_waybel_3(B)
& l1_orders_2(B) )
=> ! [C] :
( ( r1_waybel22(B,C)
& k1_card_1(C) = k1_card_1(A) )
=> r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))) ) ),
inference(negate_conjecture,[status(cth)],[t18_waybel22]) ).
cnf(0,plain,
v2_orders_2(sK2),
inference(cnf,[status(esa)],[t18_waybel22_negated]) ).
cnf(l0,plain,
v2_orders_2(sK2),
inference(instantiation,[status(thm)],[0]) ).
fof(t17_waybel22,plain,
! [A] :
( ( v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v3_lattice3(A)
& v3_waybel_3(A)
& l1_orders_2(A) )
=> ! [B] :
( ( v2_orders_2(B)
& v3_orders_2(B)
& v4_orders_2(B)
& v1_lattice3(B)
& v2_lattice3(B)
& v3_lattice3(B)
& v3_waybel_3(B)
& l1_orders_2(B) )
=> ! [C,D] :
( ( r1_waybel22(A,C)
& r1_waybel22(B,D)
& k1_card_1(C) = k1_card_1(D) )
=> r5_waybel_1(A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_waybel22) ).
cnf(334,plain,
( ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X0)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ r1_waybel22(X0,X2)
| ~ r1_waybel22(X1,X3)
| k1_card_1(X2) != k1_card_1(X3)
| ~ v2_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v2_lattice3(X1)
| r5_waybel_1(X0,X1) ),
inference(cnf,[status(esa)],[t17_waybel22]) ).
cnf(l1,plain,
( ~ v3_lattice3(sK2)
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| ~ v3_waybel_3(sK2)
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| ~ l1_orders_2(sK2)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| ~ r1_waybel22(sK2,sK3)
| ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))),k1_waybel22(sK1))
| k1_card_1(sK3) != k1_card_1(k1_waybel22(sK1))
| ~ v2_orders_2(sK2)
| ~ v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| ~ v3_orders_2(sK2)
| ~ v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| ~ v4_orders_2(sK2)
| ~ v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| ~ v1_lattice3(sK2)
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| ~ v2_lattice3(sK2)
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| r5_waybel_1(sK2,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1)))) ),
inference(instantiation,[status(thm)],[334]) ).
cnf(5,plain,
v3_lattice3(sK2),
inference(cnf,[status(esa)],[t18_waybel22_negated]) ).
cnf(l5,plain,
v3_lattice3(sK2),
inference(instantiation,[status(thm)],[5]) ).
cnf(4,plain,
v2_lattice3(sK2),
inference(cnf,[status(esa)],[t18_waybel22_negated]) ).
cnf(l511,plain,
v2_lattice3(sK2),
inference(instantiation,[status(thm)],[4]) ).
fof(fc1_waybel22,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v2_yellow_0(A)
& v2_lattice3(A)
& l1_orders_2(A) )
=> ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(A)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(A)))
& v2_yellow_0(k2_yellow_1(k9_waybel_0(A)))
& v3_yellow_0(k2_yellow_1(k9_waybel_0(A)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(A)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(A)))
& v1_lattice3(k2_yellow_1(k9_waybel_0(A)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(A)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(A)))
& v3_waybel_3(k2_yellow_1(k9_waybel_0(A))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_waybel22) ).
cnf(171,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| v3_waybel_3(k2_yellow_1(k9_waybel_0(X0)))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc1_waybel22]) ).
cnf(l19,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v2_yellow_0(k3_yellow_1(sK1))
| v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[171]) ).
cnf(6,plain,
v3_waybel_3(sK2),
inference(cnf,[status(esa)],[t18_waybel22_negated]) ).
cnf(l6,plain,
v3_waybel_3(sK2),
inference(instantiation,[status(thm)],[6]) ).
cnf(8,plain,
r1_waybel22(sK2,sK3),
inference(cnf,[status(esa)],[t18_waybel22_negated]) ).
cnf(l4,plain,
r1_waybel22(sK2,sK3),
inference(instantiation,[status(thm)],[8]) ).
cnf(168,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| v1_lattice3(k2_yellow_1(k9_waybel_0(X0)))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc1_waybel22]) ).
cnf(l530,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v2_yellow_0(k3_yellow_1(sK1))
| v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[168]) ).
cnf(7,plain,
l1_orders_2(sK2),
inference(cnf,[status(esa)],[t18_waybel22_negated]) ).
cnf(l39,plain,
l1_orders_2(sK2),
inference(instantiation,[status(thm)],[7]) ).
fof(cc12_waybel_0,plain,
! [A] :
( l1_orders_2(A)
=> ( ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v1_yellow_0(A)
& v24_waybel_0(A) )
=> ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v3_lattice3(A)
& v1_yellow_0(A)
& v2_yellow_0(A)
& v3_yellow_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc12_waybel_0) ).
cnf(16,plain,
( ~ l1_orders_2(X0)
| ~ v1_yellow_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v24_waybel_0(X0)
| v2_lattice3(X0)
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[cc12_waybel_0]) ).
cnf(l192,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v1_yellow_0(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v1_lattice3(k3_yellow_1(sK1))
| ~ v24_waybel_0(k3_yellow_1(sK1))
| v2_lattice3(k3_yellow_1(sK1))
| v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[16]) ).
fof(cc9_waybel_0,plain,
! [A] :
( l1_orders_2(A)
=> ( ( v2_orders_2(A)
& v1_lattice3(A)
& v24_waybel_0(A) )
=> ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v1_lattice3(A)
& v2_yellow_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc9_waybel_0) ).
cnf(79,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0)
| ~ v24_waybel_0(X0) ),
inference(cnf,[status(esa)],[cc9_waybel_0]) ).
cnf(l448,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v1_lattice3(k3_yellow_1(sK1))
| ~ v3_struct_0(k3_yellow_1(sK1))
| ~ v24_waybel_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[79]) ).
fof(cc1_waybel_8,plain,
! [A] :
( l1_orders_2(A)
=> ( ( v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v2_waybel_8(A) )
=> ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v2_yellow_0(A)
& v24_waybel_0(A)
& v2_waybel_3(A)
& v3_waybel_3(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_waybel_8) ).
cnf(28,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v2_waybel_8(X0)
| v2_yellow_0(X0) ),
inference(cnf,[status(esa)],[cc1_waybel_8]) ).
cnf(l383,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v1_lattice3(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v2_waybel_8(k3_yellow_1(sK1))
| v2_yellow_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[28]) ).
fof(fc2_waybel16,plain,
! [A] :
( ( v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v2_lattice3(A)
& v2_yellow_0(A)
& l1_orders_2(A) )
=> ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(A)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(A)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(A)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(A)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(A)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(A)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(A))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_waybel16) ).
cnf(181,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| v2_orders_2(k2_yellow_1(k9_waybel_0(X0))) ),
inference(cnf,[status(esa)],[fc2_waybel16]) ).
cnf(l512,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v2_yellow_0(k3_yellow_1(sK1))
| v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1)))) ),
inference(instantiation,[status(thm)],[181]) ).
fof(fc14_waybel_8,plain,
! [A] :
( ~ v3_struct_0(k3_yellow_1(A))
& v1_orders_2(k3_yellow_1(A))
& v2_orders_2(k3_yellow_1(A))
& v3_orders_2(k3_yellow_1(A))
& v4_orders_2(k3_yellow_1(A))
& v1_lattice3(k3_yellow_1(A))
& v2_lattice3(k3_yellow_1(A))
& v3_lattice3(k3_yellow_1(A))
& v1_yellow_0(k3_yellow_1(A))
& v2_yellow_0(k3_yellow_1(A))
& v3_yellow_0(k3_yellow_1(A))
& v24_waybel_0(k3_yellow_1(A))
& v25_waybel_0(k3_yellow_1(A))
& v2_waybel_1(k3_yellow_1(A))
& v9_waybel_1(k3_yellow_1(A))
& v10_waybel_1(k3_yellow_1(A))
& v11_waybel_1(k3_yellow_1(A))
& v2_waybel_3(k3_yellow_1(A))
& v3_waybel_3(k3_yellow_1(A))
& v1_waybel_8(k3_yellow_1(A))
& v2_waybel_8(k3_yellow_1(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc14_waybel_8) ).
cnf(143,plain,
v24_waybel_0(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l396,plain,
v24_waybel_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[143]) ).
cnf(l620,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v1_yellow_0(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v1_lattice3(k3_yellow_1(sK1))
| ~ v24_waybel_0(k3_yellow_1(sK1))
| v2_lattice3(k3_yellow_1(sK1))
| v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(136,plain,
v4_orders_2(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l621,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l402,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(134,plain,
v2_orders_2(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l859,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
fof(dt_k3_yellow_1,plain,
! [A] :
( v1_orders_2(k3_yellow_1(A))
& l1_orders_2(k3_yellow_1(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_yellow_1) ).
cnf(92,plain,
l1_orders_2(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[dt_k3_yellow_1]) ).
cnf(l579,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l452,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(140,plain,
v1_yellow_0(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l251,plain,
v1_yellow_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[140]) ).
cnf(80,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v24_waybel_0(X0)
| v2_yellow_0(X0) ),
inference(cnf,[status(esa)],[cc9_waybel_0]) ).
cnf(l1470,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v1_lattice3(k3_yellow_1(sK1))
| ~ v24_waybel_0(k3_yellow_1(sK1))
| v2_yellow_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[80]) ).
cnf(137,plain,
v1_lattice3(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l451,plain,
v1_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[137]) ).
cnf(135,plain,
v3_orders_2(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l401,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l449,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l863,plain,
v24_waybel_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[143]) ).
fof(cc2_lattice3,plain,
! [A] :
( l1_orders_2(A)
=> ( v2_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattice3) ).
cnf(41,plain,
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf,[status(esa)],[cc2_lattice3]) ).
cnf(l1630,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l935,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(152,plain,
v2_waybel_8(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l403,plain,
v2_waybel_8(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[152]) ).
cnf(l216,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l695,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
fof(cc1_yellow_0,plain,
! [A] :
( l1_orders_2(A)
=> ( ( ~ v3_struct_0(A)
& v3_lattice3(A) )
=> ( ~ v3_struct_0(A)
& v1_lattice3(A)
& v2_lattice3(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_yellow_0) ).
cnf(33,plain,
( ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_lattice3(X0)
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[cc1_yellow_0]) ).
cnf(l545,plain,
( ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| v3_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1)))) ),
inference(instantiation,[status(thm)],[33]) ).
fof(cc13_waybel_0,plain,
! [A] :
( l1_orders_2(A)
=> ( ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v4_orders_2(A)
& v25_waybel_0(A) )
=> ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v4_orders_2(A)
& v2_lattice3(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc13_waybel_0) ).
cnf(20,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v25_waybel_0(X0)
| v2_lattice3(X0)
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[cc13_waybel_0]) ).
cnf(l937,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v25_waybel_0(k3_yellow_1(sK1))
| v2_lattice3(k3_yellow_1(sK1))
| v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l399,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l384,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l1471,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(132,plain,
~ v3_struct_0(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l951,plain,
~ v3_struct_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[132]) ).
cnf(l945,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l1625,plain,
v24_waybel_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[143]) ).
cnf(185,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| v3_lattice3(k2_yellow_1(k9_waybel_0(X0))) ),
inference(cnf,[status(esa)],[fc2_waybel16]) ).
cnf(l606,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v2_yellow_0(k3_yellow_1(sK1))
| v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1)))) ),
inference(instantiation,[status(thm)],[185]) ).
cnf(170,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc1_waybel22]) ).
cnf(l244,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v2_yellow_0(k3_yellow_1(sK1))
| v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[170]) ).
fof(dt_k2_yellow_1,plain,
! [A] :
( v1_orders_2(k2_yellow_1(A))
& l1_orders_2(k2_yellow_1(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yellow_1) ).
cnf(90,plain,
l1_orders_2(k2_yellow_1(X0)),
inference(cnf,[status(esa)],[dt_k2_yellow_1]) ).
cnf(l625,plain,
l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1)))),
inference(instantiation,[status(thm)],[90]) ).
cnf(l247,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l473,plain,
~ v3_struct_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[132]) ).
cnf(l1689,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l615,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l410,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l195,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(138,plain,
v2_lattice3(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l1666,plain,
v2_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[138]) ).
cnf(l811,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l3,plain,
l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1)))),
inference(instantiation,[status(thm)],[90]) ).
cnf(l583,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l398,plain,
v2_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[138]) ).
cnf(l29,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l266,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l1665,plain,
~ v3_struct_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[132]) ).
cnf(l942,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l939,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(144,plain,
v25_waybel_0(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l943,plain,
v25_waybel_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(182,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| v3_orders_2(k2_yellow_1(k9_waybel_0(X0))) ),
inference(cnf,[status(esa)],[fc2_waybel16]) ).
cnf(l509,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v2_yellow_0(k3_yellow_1(sK1))
| v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1)))) ),
inference(instantiation,[status(thm)],[182]) ).
cnf(l194,plain,
v1_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[137]) ).
cnf(l748,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l400,plain,
v1_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[137]) ).
cnf(l814,plain,
v1_yellow_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[140]) ).
cnf(1,plain,
v3_orders_2(sK2),
inference(cnf,[status(esa)],[t18_waybel22_negated]) ).
cnf(l522,plain,
v3_orders_2(sK2),
inference(instantiation,[status(thm)],[1]) ).
cnf(l450,plain,
v24_waybel_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[143]) ).
cnf(l813,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(141,plain,
v2_yellow_0(k3_yellow_1(X0)),
inference(cnf,[status(esa)],[fc14_waybel_8]) ).
cnf(l539,plain,
v2_yellow_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[141]) ).
cnf(l860,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l1651,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v1_lattice3(k3_yellow_1(sK1))
| ~ v3_struct_0(k3_yellow_1(sK1))
| ~ v24_waybel_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l1681,plain,
v1_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1679,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(183,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| v4_orders_2(k2_yellow_1(k9_waybel_0(X0))) ),
inference(cnf,[status(esa)],[fc2_waybel16]) ).
cnf(l548,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v2_yellow_0(k3_yellow_1(sK1))
| v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1)))) ),
inference(instantiation,[status(thm)],[183]) ).
cnf(l510,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v1_yellow_0(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v1_lattice3(k3_yellow_1(sK1))
| ~ v24_waybel_0(k3_yellow_1(sK1))
| v2_lattice3(k3_yellow_1(sK1))
| v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l295,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l31,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l1010,plain,
v1_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[137]) ).
cnf(l515,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l526,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(32,plain,
( ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| v1_lattice3(X0)
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[cc1_yellow_0]) ).
cnf(l518,plain,
( ~ v3_lattice3(sK2)
| ~ l1_orders_2(sK2)
| v1_lattice3(sK2)
| v3_struct_0(sK2) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l747,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l793,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l536,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l812,plain,
v1_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[137]) ).
cnf(l193,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l1632,plain,
~ v3_struct_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[132]) ).
cnf(l578,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l787,plain,
v2_yellow_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[141]) ).
cnf(l741,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(2,plain,
v4_orders_2(sK2),
inference(cnf,[status(esa)],[t18_waybel22_negated]) ).
cnf(l562,plain,
v4_orders_2(sK2),
inference(instantiation,[status(thm)],[2]) ).
cnf(l870,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l1678,plain,
v24_waybel_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[143]) ).
cnf(l594,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l250,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l569,plain,
v3_lattice3(sK2),
inference(instantiation,[status(thm)],[5]) ).
cnf(l634,plain,
( ~ l1_orders_2(sK2)
| ~ v2_lattice3(sK2)
| ~ v3_struct_0(sK2) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(10,plain,
~ r5_waybel_1(sK2,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1)))),
inference(cnf,[status(esa)],[t18_waybel22_negated]) ).
cnf(l513,plain,
~ r5_waybel_1(sK2,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1)))),
inference(instantiation,[status(thm)],[10]) ).
cnf(18,plain,
( ~ l1_orders_2(X0)
| ~ v1_yellow_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v24_waybel_0(X0)
| v2_yellow_0(X0)
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[cc12_waybel_0]) ).
cnf(l734,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v1_yellow_0(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v1_lattice3(k3_yellow_1(sK1))
| ~ v24_waybel_0(k3_yellow_1(sK1))
| v2_yellow_0(k3_yellow_1(sK1))
| v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1626,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l853,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l776,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l580,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l613,plain,
v2_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[138]) ).
cnf(l623,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l563,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l857,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l742,plain,
v1_yellow_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[140]) ).
cnf(l756,plain,
v2_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[138]) ).
cnf(l590,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l283,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l869,plain,
v24_waybel_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[143]) ).
cnf(l521,plain,
l1_orders_2(sK2),
inference(instantiation,[status(thm)],[7]) ).
cnf(l334,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v1_lattice3(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v2_waybel_8(k3_yellow_1(sK1))
| v2_yellow_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l341,plain,
v2_waybel_8(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[152]) ).
cnf(l833,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l346,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l849,plain,
~ v3_struct_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[132]) ).
cnf(l868,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l854,plain,
v24_waybel_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[143]) ).
cnf(l647,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l989,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l342,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l846,plain,
v1_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[137]) ).
fof(t16_waybel22,plain,
! [A] : r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))),k1_waybel22(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t16_waybel22) ).
cnf(333,plain,
r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),k1_waybel22(X0)),
inference(cnf,[status(esa)],[t16_waybel22]) ).
cnf(l2,plain,
r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))),k1_waybel22(sK1)),
inference(instantiation,[status(thm)],[333]) ).
cnf(l988,plain,
v1_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1692,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l728,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l365,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l838,plain,
v1_yellow_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[140]) ).
cnf(l300,plain,
v2_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[138]) ).
cnf(l847,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l850,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v1_yellow_0(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v1_lattice3(k3_yellow_1(sK1))
| ~ v24_waybel_0(k3_yellow_1(sK1))
| v2_yellow_0(k3_yellow_1(sK1))
| v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(158,plain,
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc1_waybel22]) ).
cnf(l605,plain,
( ~ l1_orders_2(k3_yellow_1(sK1))
| ~ v2_orders_2(k3_yellow_1(sK1))
| ~ v3_orders_2(k3_yellow_1(sK1))
| ~ v4_orders_2(k3_yellow_1(sK1))
| ~ v2_lattice3(k3_yellow_1(sK1))
| ~ v2_yellow_0(k3_yellow_1(sK1))
| ~ v3_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1))))
| v3_struct_0(k3_yellow_1(sK1)) ),
inference(instantiation,[status(thm)],[158]) ).
cnf(l339,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l995,plain,
v2_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[138]) ).
cnf(l746,plain,
v2_yellow_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[141]) ).
cnf(l1627,plain,
v1_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[137]) ).
cnf(l862,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(l918,plain,
v24_waybel_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[143]) ).
cnf(l889,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l851,plain,
v1_yellow_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[140]) ).
cnf(l751,plain,
~ v3_struct_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[132]) ).
cnf(l724,plain,
v2_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[134]) ).
cnf(l736,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l892,plain,
v1_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[137]) ).
cnf(l888,plain,
v3_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[135]) ).
cnf(l777,plain,
v2_lattice3(sK2),
inference(instantiation,[status(thm)],[4]) ).
cnf(l661,plain,
l1_orders_2(sK2),
inference(instantiation,[status(thm)],[7]) ).
cnf(l891,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l778,plain,
v2_lattice3(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[138]) ).
cnf(l919,plain,
~ v3_struct_0(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[132]) ).
cnf(9,plain,
k1_card_1(sK3) = k1_card_1(sK1),
inference(cnf,[status(esa)],[t18_waybel22_negated]) ).
cnf(l253,plain,
k1_card_1(sK3) = k1_card_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
fof(t10_waybel22,plain,
! [A] : k1_card_1(k1_waybel22(A)) = k1_card_1(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_waybel22) ).
cnf(332,plain,
k1_card_1(k1_waybel22(X0)) = k1_card_1(X0),
inference(cnf,[status(esa)],[t10_waybel22]) ).
cnf(l315,plain,
k1_card_1(k1_waybel22(sK1)) = k1_card_1(sK1),
inference(instantiation,[status(thm)],[332]) ).
cnf(l925,plain,
v4_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[136]) ).
cnf(l721,plain,
l1_orders_2(k3_yellow_1(sK1)),
inference(instantiation,[status(thm)],[92]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l5,l511,l19,l6,l4,l530,l39,l192,l448,l383,l512,l396,l620,l621,l402,l859,l579,l452,l251,l1470,l451,l401,l449,l863,l1630,l935,l403,l216,l695,l545,l937,l399,l384,l1471,l951,l945,l1625,l606,l244,l625,l247,l473,l1689,l615,l410,l195,l1666,l811,l3,l583,l398,l29,l266,l1665,l942,l939,l943,l509,l194,l748,l400,l814,l522,l450,l813,l539,l860,l1651,l1681,l1679,l548,l510,l295,l31,l1010,l515,l526,l518,l747,l793,l536,l812,l193,l1632,l578,l787,l741,l562,l870,l1678,l594,l250,l569,l634,l513,l734,l1626,l853,l776,l580,l613,l623,l563,l857,l742,l756,l590,l283,l869,l521,l334,l341,l833,l346,l849,l868,l854,l647,l989,l342,l846,l2,l988,l1692,l728,l365,l838,l300,l847,l850,l605,l339,l995,l746,l1627,l862,l918,l889,l851,l751,l724,l736,l892,l888,l777,l661,l891,l778,l919,l253,l315,l925,l721]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : LAT351+1 : TPTP v9.0.0. Released v3.4.0.
% 0.03/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Jul 21 01:08:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.35 % launching worker at depth: 9
% 0.19/0.40 % launching worker at depth: 10
% 4.22/0.91 % launching worker at depth: 11
% 32.02/4.34 % SZS status Theorem for theBenchmark
% 32.02/4.34 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------