%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT356+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:02:55 PM UTC 2026
% Result : Theorem 0.19s 1.01s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 9
% Syntax : Number of formulae : 83 ( 13 unt; 0 def)
% Number of atoms : 609 ( 53 equ)
% Maximal formula atoms : 25 ( 7 avg)
% Number of connectives : 920 ( 394 ~; 394 |; 109 &)
% ( 4 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-4 aty)
% Number of variables : 69 ( 68 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l1_orders_2(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ( k2_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A)
& k1_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l1_orders_2(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ( k2_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A)
& k1_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f34,axiom,
! [A] :
( l1_orders_2(A)
=> ( v2_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( ( v17_waybel_0(C,A,B)
& v3_lattice3(B)
& v3_lattice3(A) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(D) )
=> ( D = k1_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(C) )
=> ( ( v18_waybel_0(C,B,A)
& v3_lattice3(B)
& v3_lattice3(A) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(D) )
=> ( D = k2_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,D,C),A,B) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A] :
( l1_struct_0(A)
=> ( m2_relset_1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(k7_grcat_1(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [A] :
( l1_orders_2(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [A] :
( l1_orders_2(A)
=> ( v23_waybel_0(k7_grcat_1(A),A,A)
& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(k7_grcat_1(A))
& v1_relat_1(k7_grcat_1(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f93,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ( v8_waybel_1(k7_grcat_1(A),A)
& v7_waybel_1(k7_grcat_1(A),A)
& v6_waybel_1(k7_grcat_1(A),A)
& v23_waybel_0(k7_grcat_1(A),A,A)
& v22_waybel_0(k7_grcat_1(A),A,A)
& v21_waybel_0(k7_grcat_1(A),A,A)
& v20_waybel_0(k7_grcat_1(A),A,A)
& v19_waybel_0(k7_grcat_1(A),A,A)
& v18_waybel_0(k7_grcat_1(A),A,A)
& v17_waybel_0(k7_grcat_1(A),A,A)
& v5_orders_3(k7_grcat_1(A),A,A)
& v11_quantal1(k7_grcat_1(A))
& v1_partfun1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& ~ v1_xboole_0(k7_grcat_1(A))
& v2_funct_1(k7_grcat_1(A))
& v1_funct_1(k7_grcat_1(A))
& v1_relat_1(k7_grcat_1(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> v3_waybel_1(k1_waybel_1(A,A,k7_grcat_1(A),k7_grcat_1(A)),A,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,plain,
? [A] :
( ( k2_waybel34(A,A,k7_grcat_1(A)) != k7_grcat_1(A)
| k1_waybel34(A,A,k7_grcat_1(A)) != k7_grcat_1(A) )
& l1_orders_2(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)],[f2]) ).
fof(f133,plain,
( ( k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl)) != k7_grcat_1(sK0_skl)
| k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl)) != k7_grcat_1(sK0_skl) )
& l1_orders_2(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]),skolemize(A,sK0_skl)],[f132]) ).
fof(f134,plain,
v2_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
v3_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f136,plain,
v4_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f137,plain,
v1_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f138,plain,
v2_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f139,plain,
v3_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f140,plain,
l1_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f141,plain,
( k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl)) != k7_grcat_1(sK0_skl)
| k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl)) != k7_grcat_1(sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f282,plain,
! [A] :
( ~ v3_struct_0(A)
| ~ v2_lattice3(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f283,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f339,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( D = k1_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) )
| ~ m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(D) )
| ~ v17_waybel_0(C,A,B)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B) )
| ~ l1_orders_2(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)],[f49]) ).
fof(f340,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ~ v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
| D = k1_waybel34(A,B,C) )
& ( v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
| D != k1_waybel34(A,B,C) ) )
| ~ m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(D) )
| ~ v17_waybel_0(C,A,B)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B) )
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(NNF_transformation,[status(thm)],[f339]) ).
fof(f342,plain,
! [X0,X1,X2,X3] :
( ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| X3 = k1_waybel34(X0,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f343,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( D = k2_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,D,C),A,B) )
| ~ m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(D) )
| ~ v18_waybel_0(C,B,A)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B) )
| ~ l1_orders_2(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)],[f50]) ).
fof(f344,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ~ v3_waybel_1(k1_waybel_1(A,B,D,C),A,B)
| D = k2_waybel34(A,B,C) )
& ( v3_waybel_1(k1_waybel_1(A,B,D,C),A,B)
| D != k2_waybel34(A,B,C) ) )
| ~ m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(D) )
| ~ v18_waybel_0(C,B,A)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B) )
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(NNF_transformation,[status(thm)],[f343]) ).
fof(f346,plain,
! [X0,X1,X2,X3] :
( ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| X3 = k2_waybel34(X0,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f358,plain,
! [A] :
( ( m2_relset_1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(k7_grcat_1(A)) )
| ~ l1_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f360,plain,
! [X0] :
( v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f361,plain,
! [X0] :
( m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f362,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f363,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f445,plain,
! [A] :
( ( v23_waybel_0(k7_grcat_1(A),A,A)
& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(k7_grcat_1(A))
& v1_relat_1(k7_grcat_1(A)) )
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f89]) ).
fof(f447,plain,
! [X0] :
( v1_funct_1(k7_grcat_1(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f468,plain,
! [A] :
( ( v8_waybel_1(k7_grcat_1(A),A)
& v7_waybel_1(k7_grcat_1(A),A)
& v6_waybel_1(k7_grcat_1(A),A)
& v23_waybel_0(k7_grcat_1(A),A,A)
& v22_waybel_0(k7_grcat_1(A),A,A)
& v21_waybel_0(k7_grcat_1(A),A,A)
& v20_waybel_0(k7_grcat_1(A),A,A)
& v19_waybel_0(k7_grcat_1(A),A,A)
& v18_waybel_0(k7_grcat_1(A),A,A)
& v17_waybel_0(k7_grcat_1(A),A,A)
& v5_orders_3(k7_grcat_1(A),A,A)
& v11_quantal1(k7_grcat_1(A))
& v1_partfun1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& ~ v1_xboole_0(k7_grcat_1(A))
& v2_funct_1(k7_grcat_1(A))
& v1_funct_1(k7_grcat_1(A))
& v1_relat_1(k7_grcat_1(A)) )
| ~ l1_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f93]) ).
fof(f477,plain,
! [X0] :
( v17_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f468]) ).
fof(f478,plain,
! [X0] :
( v18_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f468]) ).
fof(f693,plain,
! [A] :
( v3_waybel_1(k1_waybel_1(A,A,k7_grcat_1(A),k7_grcat_1(A)),A,A)
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f129]) ).
fof(f694,plain,
! [X0] :
( v3_waybel_1(k1_waybel_1(X0,X0,k7_grcat_1(X0),k7_grcat_1(X0)),X0,X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f693]) ).
fof(f907,plain,
( v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f477,f134]) ).
fof(f909,plain,
( v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f907,f140]) ).
fof(f911,plain,
( v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f478,f134]) ).
fof(f913,plain,
( v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f911,f140]) ).
fof(f921,plain,
( ~ v2_lattice3(sK0_skl)
| ~ l1_orders_2(sK0_skl)
| v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f909,f283]) ).
fof(f923,plain,
( ~ v2_lattice3(sK0_skl)
| v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f921,f140]) ).
fof(f925,plain,
( ~ v2_lattice3(sK0_skl)
| ~ l1_orders_2(sK0_skl)
| v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f913,f283]) ).
fof(f927,plain,
( ~ v2_lattice3(sK0_skl)
| v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f925,f140]) ).
fof(f929,plain,
v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f923,f138]) ).
fof(f935,plain,
v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f927,f138]) ).
fof(f1785,plain,
! [X0] :
( k7_grcat_1(X0) = k2_waybel34(X0,X0,k7_grcat_1(X0))
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k7_grcat_1(X0))
| ~ v18_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k7_grcat_1(X0))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f694,f346]) ).
fof(f1786,plain,
! [X0] :
( k7_grcat_1(X0) = k1_waybel34(X0,X0,k7_grcat_1(X0))
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k7_grcat_1(X0))
| ~ v17_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k7_grcat_1(X0))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f694,f342]) ).
fof(f1787,plain,
! [X0] :
( k7_grcat_1(X0) = k2_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v18_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k7_grcat_1(X0))
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1785]) ).
fof(f1788,plain,
! [X0] :
( k7_grcat_1(X0) = k2_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v18_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k7_grcat_1(X0))
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1787,f283]) ).
fof(f1789,plain,
! [X0] :
( k7_grcat_1(X0) = k1_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v17_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k7_grcat_1(X0))
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1786]) ).
fof(f1790,plain,
! [X0] :
( k7_grcat_1(X0) = k1_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v17_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k7_grcat_1(X0))
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1789,f283]) ).
fof(f1814,plain,
! [X0] :
( k7_grcat_1(X0) = k2_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v18_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1788,f447]) ).
fof(f1815,plain,
! [X0] :
( ~ l1_struct_0(X0)
| k7_grcat_1(X0) = k2_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v18_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f1814,f360]) ).
fof(f1817,plain,
! [X0] :
( ~ l1_struct_0(X0)
| k7_grcat_1(X0) = k2_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v18_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1815,f361]) ).
fof(f1819,plain,
! [X0] :
( k7_grcat_1(X0) = k1_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v17_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1790,f447]) ).
fof(f1820,plain,
! [X0] :
( ~ l1_struct_0(X0)
| k7_grcat_1(X0) = k1_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v17_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f1819,f360]) ).
fof(f1822,plain,
! [X0] :
( ~ l1_struct_0(X0)
| k7_grcat_1(X0) = k1_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v17_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1820,f361]) ).
fof(f1881,plain,
! [X0] :
( k7_grcat_1(X0) = k2_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v18_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1817,f363]) ).
fof(f1883,plain,
( k7_grcat_1(sK0_skl) = k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1881,f134]) ).
fof(f1885,plain,
( k7_grcat_1(sK0_skl) = k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1883,f140]) ).
fof(f1886,plain,
! [X0] :
( k7_grcat_1(X0) = k1_waybel34(X0,X0,k7_grcat_1(X0))
| ~ v17_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1822,f363]) ).
fof(f1888,plain,
( k7_grcat_1(sK0_skl) = k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1886,f134]) ).
fof(f1890,plain,
( k7_grcat_1(sK0_skl) = k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1888,f140]) ).
fof(f2112,plain,
( k7_grcat_1(sK0_skl) = k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1885,f135]) ).
fof(f2113,plain,
( k7_grcat_1(sK0_skl) = k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl) ),
inference(resolution,[status(thm)],[f2112,f136]) ).
fof(f2114,plain,
( k7_grcat_1(sK0_skl) = k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2113,f137]) ).
fof(f2115,plain,
( k7_grcat_1(sK0_skl) = k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v18_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2114,f138]) ).
fof(f2116,plain,
( k7_grcat_1(sK0_skl) = k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v3_lattice3(sK0_skl) ),
inference(resolution,[status(thm)],[f2115,f935]) ).
fof(f2118,plain,
k7_grcat_1(sK0_skl) = k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f2116,f139]) ).
fof(f2130,plain,
( k7_grcat_1(sK0_skl) != k7_grcat_1(sK0_skl)
| k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl)) != k7_grcat_1(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f2118,f141]) ).
fof(f2147,plain,
k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl)) != k7_grcat_1(sK0_skl),
inference(trivial_equality_resolution,[status(thm)],[f2130]) ).
fof(f2506,plain,
( k7_grcat_1(sK0_skl) = k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1890,f135]) ).
fof(f2507,plain,
( k7_grcat_1(sK0_skl) = k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl) ),
inference(resolution,[status(thm)],[f2506,f136]) ).
fof(f2508,plain,
( k7_grcat_1(sK0_skl) = k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v2_lattice3(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2507,f137]) ).
fof(f2509,plain,
( k7_grcat_1(sK0_skl) = k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v17_waybel_0(k7_grcat_1(sK0_skl),sK0_skl,sK0_skl)
| ~ v3_lattice3(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2508,f138]) ).
fof(f2510,plain,
( k7_grcat_1(sK0_skl) = k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))
| ~ v3_lattice3(sK0_skl) ),
inference(resolution,[status(thm)],[f2509,f929]) ).
fof(f2512,plain,
k7_grcat_1(sK0_skl) = k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f2510,f139]) ).
fof(f2527,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2512,f2147]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT356+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.63 % Computer : n016.cluster.edu
% 0.15/0.63 % Model : x86_64 x86_64
% 0.15/0.63 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.63 % Memory : 8046.5625MB
% 0.15/0.63 % OS : Linux 6.8.0-71-generic
% 0.15/0.63 % CPULimit : 300
% 0.15/0.63 % WCLimit : 300
% 0.15/0.63 % DateTime : Sun Sep 20 23:53:08 UTC 2026
% 0.15/0.63 % CPUTime :
% 0.19/0.66 % Drodi V4.1.1
% 0.19/1.01 % Refutation found
% 0.19/1.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/1.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.19/1.04 % Elapsed time: 0.393876 seconds
% 0.19/1.04 % CPU time: 2.803740 seconds
% 0.19/1.04 % Total memory used: 151.269 MB
% 0.19/1.04 % Net memory used: 150.192 MB
%------------------------------------------------------------------------------