%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT351+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 : Thu Sep 24 01:02:53 PM UTC 2026
% Result : Theorem 0.13s 0.40s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 34
% Syntax : Number of formulae : 156 ( 42 unt; 23 def)
% Number of atoms : 648 ( 23 equ)
% Maximal formula atoms : 21 ( 4 avg)
% Number of connectives : 795 ( 303 ~; 297 |; 161 &)
% ( 23 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 49 ( 47 usr; 24 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-1 aty)
% Number of variables : 93 ( 87 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,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(negated_conjecture,[status(cth)],[f1]) ).
fof(f19,axiom,
! [A] :
( l1_orders_2(A)
=> ( v2_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A] : k1_waybel22(A) = a_1_0_waybel22(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [A] :
( l1_orders_2(k2_yellow_1(A))
& v1_orders_2(k2_yellow_1(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A] :
( l1_orders_2(k3_yellow_1(A))
& v1_orders_2(k3_yellow_1(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,axiom,
! [A] : k1_card_1(k1_waybel22(A)) = k1_card_1(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,axiom,
! [A] : r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))),k1_waybel22(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,plain,
? [A,B] :
( ? [C] :
( ~ r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
& k1_card_1(C) = k1_card_1(A)
& 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(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f124,plain,
? [B] :
( ? [A] :
( ~ r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))
& ? [C] :
( k1_card_1(C) = k1_card_1(A)
& 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(miniscoping,[status(thm)],[f123]) ).
fof(f125,plain,
( ~ r5_waybel_1(sK0_skl,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))
& k1_card_1(sK2_skl) = k1_card_1(sK1_skl)
& r1_waybel22(sK0_skl,sK2_skl)
& l1_orders_2(sK0_skl)
& v3_waybel_3(sK0_skl)
& v3_lattice3(sK0_skl)
& v2_lattice3(sK0_skl)
& v1_lattice3(sK0_skl)
& v4_orders_2(sK0_skl)
& v3_orders_2(sK0_skl)
& v2_orders_2(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(B,sK0_skl),skolemize(A,sK1_skl),skolemize(C,sK2_skl)],[f124]) ).
fof(f126,plain,
v2_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
v3_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f128,plain,
v4_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f129,plain,
v1_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f130,plain,
v2_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f131,plain,
v3_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f132,plain,
v3_waybel_3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f133,plain,
l1_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f134,plain,
r1_waybel22(sK0_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f135,plain,
k1_card_1(sK2_skl) = k1_card_1(sK1_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f136,plain,
~ r5_waybel_1(sK0_skl,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f210,plain,
! [A] :
( ~ v3_struct_0(A)
| ~ v2_lattice3(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f211,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f300,plain,
! [X0] : k1_waybel22(X0) = a_1_0_waybel22(X0),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f308,plain,
( ! [A] : l1_orders_2(k2_yellow_1(A))
& ! [A] : v1_orders_2(k2_yellow_1(A)) ),
inference(miniscoping,[status(thm)],[f42]) ).
fof(f310,plain,
! [X0] : l1_orders_2(k2_yellow_1(X0)),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f311,plain,
( ! [A] : l1_orders_2(k3_yellow_1(A))
& ! [A] : v1_orders_2(k3_yellow_1(A)) ),
inference(miniscoping,[status(thm)],[f44]) ).
fof(f313,plain,
! [X0] : l1_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f369,plain,
( ! [A] : v2_waybel_8(k3_yellow_1(A))
& ! [A] : v1_waybel_8(k3_yellow_1(A))
& ! [A] : v3_waybel_3(k3_yellow_1(A))
& ! [A] : v2_waybel_3(k3_yellow_1(A))
& ! [A] : v11_waybel_1(k3_yellow_1(A))
& ! [A] : v10_waybel_1(k3_yellow_1(A))
& ! [A] : v9_waybel_1(k3_yellow_1(A))
& ! [A] : v2_waybel_1(k3_yellow_1(A))
& ! [A] : v25_waybel_0(k3_yellow_1(A))
& ! [A] : v24_waybel_0(k3_yellow_1(A))
& ! [A] : v3_yellow_0(k3_yellow_1(A))
& ! [A] : v2_yellow_0(k3_yellow_1(A))
& ! [A] : v1_yellow_0(k3_yellow_1(A))
& ! [A] : v3_lattice3(k3_yellow_1(A))
& ! [A] : v2_lattice3(k3_yellow_1(A))
& ! [A] : v1_lattice3(k3_yellow_1(A))
& ! [A] : v4_orders_2(k3_yellow_1(A))
& ! [A] : v3_orders_2(k3_yellow_1(A))
& ! [A] : v2_orders_2(k3_yellow_1(A))
& ! [A] : v1_orders_2(k3_yellow_1(A))
& ! [A] : ~ v3_struct_0(k3_yellow_1(A)) ),
inference(miniscoping,[status(thm)],[f66]) ).
fof(f372,plain,
! [X0] : v2_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f373,plain,
! [X0] : v3_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f374,plain,
! [X0] : v4_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f376,plain,
! [X0] : v2_lattice3(k3_yellow_1(X0)),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f379,plain,
! [X0] : v2_yellow_0(k3_yellow_1(X0)),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f399,plain,
! [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))) )
| ~ 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(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f410,plain,
! [X0] :
( v1_lattice3(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f399]) ).
fof(f413,plain,
! [X0] :
( v3_waybel_3(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f399]) ).
fof(f423,plain,
! [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))) )
| ~ l1_orders_2(A)
| ~ v2_yellow_0(A)
| ~ v2_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f426,plain,
! [X0] :
( v2_orders_2(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f423]) ).
fof(f427,plain,
! [X0] :
( v3_orders_2(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f423]) ).
fof(f428,plain,
! [X0] :
( v4_orders_2(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f423]) ).
fof(f429,plain,
! [X0] :
( v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f423]) ).
fof(f430,plain,
! [X0] :
( v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f423]) ).
fof(f621,plain,
! [X0] : k1_card_1(k1_waybel22(X0)) = k1_card_1(X0),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f622,plain,
! [X0] : r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),k1_waybel22(X0)),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f623,plain,
! [A] :
( ! [B] :
( ! [C,D] :
( r5_waybel_1(A,B)
| k1_card_1(C) != k1_card_1(D)
| ~ 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(pre_NNF_transformation,[status(thm)],[f113]) ).
fof(f624,plain,
! [A] :
( ! [B] :
( r5_waybel_1(A,B)
| ! [C,D] :
( k1_card_1(C) != k1_card_1(D)
| ~ 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(miniscoping,[status(thm)],[f623]) ).
fof(f625,plain,
! [X0,X1,X2,X3] :
( r5_waybel_1(X0,X1)
| k1_card_1(X2) != k1_card_1(X3)
| ~ r1_waybel22(X1,X3)
| ~ r1_waybel22(X0,X2)
| ~ l1_orders_2(X1)
| ~ v3_waybel_3(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_waybel_3(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f624]) ).
fof(f687,plain,
! [X0] :
( v1_lattice3(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f410,f211]) ).
fof(f688,plain,
! [X0] :
( v3_waybel_3(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f413,f211]) ).
fof(f689,plain,
! [X0,X1] :
( k1_card_1(X0) != k1_card_1(X1)
| ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)
| ~ r1_waybel22(sK0_skl,X0)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))
| ~ v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))
| ~ v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))
| ~ v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))
| ~ l1_orders_2(sK0_skl)
| ~ v3_waybel_3(sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f625,f136]) ).
fof(f690,definition,
( sQ6_spl
<=> v2_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f692,plain,
( sQ6_spl
| ~ v2_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f693,definition,
( sQ7_spl
<=> v3_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f695,plain,
( sQ7_spl
| ~ v3_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f693]) ).
fof(f696,definition,
( sQ8_spl
<=> v4_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f698,plain,
( sQ8_spl
| ~ v4_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f696]) ).
fof(f699,definition,
( sQ9_spl
<=> v1_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f701,plain,
( sQ9_spl
| ~ v1_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f699]) ).
fof(f702,definition,
( sQ10_spl
<=> v2_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f704,plain,
( sQ10_spl
| ~ v2_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f702]) ).
fof(f705,definition,
( sQ11_spl
<=> v3_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f707,plain,
( sQ11_spl
| ~ v3_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f705]) ).
fof(f708,definition,
( sQ12_spl
<=> v3_waybel_3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f710,plain,
( sQ12_spl
| ~ v3_waybel_3(sK0_skl) ),
inference(component_clause,[status(thm)],[f708]) ).
fof(f711,definition,
( sQ13_spl
<=> l1_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f713,plain,
( sQ13_spl
| ~ l1_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f711]) ).
fof(f714,definition,
( sQ14_spl
<=> v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f716,plain,
( sQ14_spl
| ~ v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
inference(component_clause,[status(thm)],[f714]) ).
fof(f717,definition,
( sQ15_spl
<=> v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f719,plain,
( sQ15_spl
| ~ v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
inference(component_clause,[status(thm)],[f717]) ).
fof(f720,definition,
( sQ16_spl
<=> v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f722,plain,
( sQ16_spl
| ~ v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
inference(component_clause,[status(thm)],[f720]) ).
fof(f723,definition,
( sQ17_spl
<=> v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f725,plain,
( sQ17_spl
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
inference(component_clause,[status(thm)],[f723]) ).
fof(f726,definition,
( sQ18_spl
<=> v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f728,plain,
( sQ18_spl
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
inference(component_clause,[status(thm)],[f726]) ).
fof(f729,definition,
( sQ19_spl
<=> v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f731,plain,
( sQ19_spl
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
inference(component_clause,[status(thm)],[f729]) ).
fof(f732,definition,
( sQ20_spl
<=> v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f734,plain,
( sQ20_spl
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
inference(component_clause,[status(thm)],[f732]) ).
fof(f735,definition,
( sQ21_spl
<=> l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f737,plain,
( sQ21_spl
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl)))) ),
inference(component_clause,[status(thm)],[f735]) ).
fof(f738,definition,
! [X0,X1] :
( sQ22_spl
<=> ( k1_card_1(X0) != k1_card_1(X1)
| ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)
| ~ r1_waybel22(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f739,plain,
! [X0,X1] :
( ~ sQ22_spl
| k1_card_1(X0) != k1_card_1(X1)
| ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)
| ~ r1_waybel22(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f738]) ).
fof(f741,plain,
( sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f689,f690,f693,f696,f699,f702,f705,f708,f711,f714,f717,f720,f723,f726,f729,f732,f735,f738]) ).
fof(f742,plain,
! [X0] :
( ~ sQ22_spl
| k1_card_1(sK2_skl) != k1_card_1(X0)
| ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X0) ),
inference(resolution,[status(thm)],[f739,f134]) ).
fof(f743,plain,
( ~ sQ22_spl
| k1_card_1(sK2_skl) != k1_card_1(k1_waybel22(sK1_skl)) ),
inference(resolution,[status(thm)],[f742,f622]) ).
fof(f785,plain,
( ~ sQ22_spl
| k1_card_1(sK2_skl) != k1_card_1(a_1_0_waybel22(sK1_skl)) ),
inference(backward_demodulation,[status(thm)],[f300,f743]) ).
fof(f811,plain,
( ~ sQ22_spl
| k1_card_1(sK2_skl) != k1_card_1(sK1_skl) ),
inference(backward_demodulation,[status(thm)],[f812,f785]) ).
fof(f812,plain,
! [X0] : k1_card_1(a_1_0_waybel22(X0)) = k1_card_1(X0),
inference(forward_demodulation,[status(thm)],[f300,f621]) ).
fof(f814,plain,
( ~ sQ22_spl
| k1_card_1(sK2_skl) != k1_card_1(sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f135,f811]) ).
fof(f815,plain,
( ~ sQ22_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f814]) ).
fof(f816,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f815]) ).
fof(f817,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f737,f310]) ).
fof(f818,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f817]) ).
fof(f820,plain,
( sQ20_spl
| ~ l1_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_lattice3(k3_yellow_1(sK1_skl))
| ~ v2_yellow_0(k3_yellow_1(sK1_skl))
| ~ v4_orders_2(k3_yellow_1(sK1_skl))
| ~ v3_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_orders_2(k3_yellow_1(sK1_skl)) ),
inference(resolution,[status(thm)],[f734,f688]) ).
fof(f825,definition,
( sQ31_spl
<=> v2_orders_2(k3_yellow_1(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f827,plain,
( sQ31_spl
| ~ v2_orders_2(k3_yellow_1(sK1_skl)) ),
inference(component_clause,[status(thm)],[f825]) ).
fof(f828,definition,
( sQ32_spl
<=> v3_orders_2(k3_yellow_1(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f830,plain,
( sQ32_spl
| ~ v3_orders_2(k3_yellow_1(sK1_skl)) ),
inference(component_clause,[status(thm)],[f828]) ).
fof(f831,definition,
( sQ33_spl
<=> v4_orders_2(k3_yellow_1(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f833,plain,
( sQ33_spl
| ~ v4_orders_2(k3_yellow_1(sK1_skl)) ),
inference(component_clause,[status(thm)],[f831]) ).
fof(f834,definition,
( sQ34_spl
<=> v2_yellow_0(k3_yellow_1(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f836,plain,
( sQ34_spl
| ~ v2_yellow_0(k3_yellow_1(sK1_skl)) ),
inference(component_clause,[status(thm)],[f834]) ).
fof(f837,definition,
( sQ35_spl
<=> v2_lattice3(k3_yellow_1(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f839,plain,
( sQ35_spl
| ~ v2_lattice3(k3_yellow_1(sK1_skl)) ),
inference(component_clause,[status(thm)],[f837]) ).
fof(f840,definition,
( sQ36_spl
<=> l1_orders_2(k3_yellow_1(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f842,plain,
( sQ36_spl
| ~ l1_orders_2(k3_yellow_1(sK1_skl)) ),
inference(component_clause,[status(thm)],[f840]) ).
fof(f843,plain,
( sQ20_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f820,f825,f828,f831,f834,f837,f840,f732]) ).
fof(f860,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f842,f313]) ).
fof(f861,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f860]) ).
fof(f862,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f839,f376]) ).
fof(f863,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f862]) ).
fof(f864,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f836,f379]) ).
fof(f865,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f864]) ).
fof(f866,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f833,f374]) ).
fof(f867,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f866]) ).
fof(f868,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f830,f373]) ).
fof(f869,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f868]) ).
fof(f870,plain,
( sQ18_spl
| ~ l1_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_yellow_0(k3_yellow_1(sK1_skl))
| ~ v2_lattice3(k3_yellow_1(sK1_skl))
| ~ v4_orders_2(k3_yellow_1(sK1_skl))
| ~ v3_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_orders_2(k3_yellow_1(sK1_skl)) ),
inference(resolution,[status(thm)],[f728,f429]) ).
fof(f875,plain,
( sQ18_spl
| ~ sQ36_spl
| ~ sQ34_spl
| ~ sQ35_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f870,f825,f828,f831,f837,f834,f840,f726]) ).
fof(f892,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f827,f372]) ).
fof(f893,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f892]) ).
fof(f894,plain,
( sQ16_spl
| ~ l1_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_yellow_0(k3_yellow_1(sK1_skl))
| ~ v2_lattice3(k3_yellow_1(sK1_skl))
| ~ v4_orders_2(k3_yellow_1(sK1_skl))
| ~ v3_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_orders_2(k3_yellow_1(sK1_skl)) ),
inference(resolution,[status(thm)],[f722,f428]) ).
fof(f896,plain,
( sQ16_spl
| ~ sQ36_spl
| ~ sQ34_spl
| ~ sQ35_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f894,f825,f828,f831,f837,f834,f840,f720]) ).
fof(f898,plain,
( sQ14_spl
| ~ l1_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_yellow_0(k3_yellow_1(sK1_skl))
| ~ v2_lattice3(k3_yellow_1(sK1_skl))
| ~ v4_orders_2(k3_yellow_1(sK1_skl))
| ~ v3_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_orders_2(k3_yellow_1(sK1_skl)) ),
inference(resolution,[status(thm)],[f716,f426]) ).
fof(f899,plain,
( sQ14_spl
| ~ sQ36_spl
| ~ sQ34_spl
| ~ sQ35_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f898,f825,f828,f831,f837,f834,f840,f714]) ).
fof(f900,plain,
( sQ17_spl
| ~ l1_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_lattice3(k3_yellow_1(sK1_skl))
| ~ v2_yellow_0(k3_yellow_1(sK1_skl))
| ~ v4_orders_2(k3_yellow_1(sK1_skl))
| ~ v3_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_orders_2(k3_yellow_1(sK1_skl)) ),
inference(resolution,[status(thm)],[f725,f687]) ).
fof(f904,plain,
( sQ17_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f900,f825,f828,f831,f834,f837,f840,f723]) ).
fof(f917,plain,
( sQ15_spl
| ~ l1_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_yellow_0(k3_yellow_1(sK1_skl))
| ~ v2_lattice3(k3_yellow_1(sK1_skl))
| ~ v4_orders_2(k3_yellow_1(sK1_skl))
| ~ v3_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_orders_2(k3_yellow_1(sK1_skl)) ),
inference(resolution,[status(thm)],[f719,f427]) ).
fof(f919,plain,
( sQ15_spl
| ~ sQ36_spl
| ~ sQ34_spl
| ~ sQ35_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f917,f825,f828,f831,f837,f834,f840,f717]) ).
fof(f921,plain,
( sQ19_spl
| ~ l1_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_yellow_0(k3_yellow_1(sK1_skl))
| ~ v2_lattice3(k3_yellow_1(sK1_skl))
| ~ v4_orders_2(k3_yellow_1(sK1_skl))
| ~ v3_orders_2(k3_yellow_1(sK1_skl))
| ~ v2_orders_2(k3_yellow_1(sK1_skl)) ),
inference(resolution,[status(thm)],[f731,f430]) ).
fof(f926,plain,
( sQ19_spl
| ~ sQ36_spl
| ~ sQ34_spl
| ~ sQ35_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f921,f825,f828,f831,f837,f834,f840,f729]) ).
fof(f931,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f713,f133]) ).
fof(f932,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f931]) ).
fof(f933,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f710,f132]) ).
fof(f934,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f933]) ).
fof(f935,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f707,f131]) ).
fof(f936,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f935]) ).
fof(f937,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f704,f130]) ).
fof(f938,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f937]) ).
fof(f939,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f701,f129]) ).
fof(f940,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f939]) ).
fof(f941,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f698,f128]) ).
fof(f942,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f941]) ).
fof(f943,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f692,f126]) ).
fof(f944,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f943]) ).
fof(f945,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f695,f127]) ).
fof(f946,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f945]) ).
fof(f947,plain,
$false,
inference(sat_refutation,[status(thm)],[f741,f816,f818,f843,f861,f863,f865,f867,f869,f875,f893,f896,f899,f904,f919,f926,f932,f934,f936,f938,f940,f942,f944,f946]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT351+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n005.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 23:46:18 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.43 % Elapsed time: 0.071889 seconds
% 0.13/0.43 % CPU time: 0.213162 seconds
% 0.13/0.43 % Total memory used: 119.898 MB
% 0.13/0.43 % Net memory used: 119.701 MB
%------------------------------------------------------------------------------