%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT301+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 : n009.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:37 PM UTC 2026
% Result : Theorem 0.17s 0.63s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 51
% Syntax : Number of formulae : 204 ( 41 unt; 29 def)
% Number of atoms : 629 ( 19 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 658 ( 233 ~; 245 |; 122 &)
% ( 33 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 56 ( 54 usr; 30 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-2 aty)
% Number of variables : 85 ( 77 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v13_lattices(A)
=> r2_hidden(k5_lattices(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v13_lattices(A)
=> r2_hidden(k5_lattices(A),B) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f13,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> k7_filter_2(A,B) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A] :
( l1_lattices(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_lattice4(B,A)
=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,axiom,
? [A] :
( v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
? [A] :
( v1_funct_1(A)
& v1_xboole_0(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
? [A] :
( v3_lattices(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
? [A] :
( ~ v3_struct_0(A)
& l1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
? [A] :
( v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
? [A] :
( v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k15_filter_2(A,B) = k7_filter_2(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( ( l3_lattices(A)
& v14_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> r2_hidden(k6_lattices(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
<=> v14_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,axiom,
! [A] :
( ( l3_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k5_lattices(A) = k6_lattices(k1_lattice2(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,plain,
? [A] :
( ? [B] :
( ~ r2_hidden(k5_lattices(A),B)
& v13_lattices(A)
& m2_filter_2(B,A) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f91,plain,
( ~ r2_hidden(k5_lattices(sK0_skl),sK1_skl)
& v13_lattices(sK0_skl)
& m2_filter_2(sK1_skl,sK0_skl)
& l3_lattices(sK0_skl)
& v10_lattices(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f90]) ).
fof(f92,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f94,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f95,plain,
m2_filter_2(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f96,plain,
v13_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f97,plain,
~ r2_hidden(k5_lattices(sK0_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f131,plain,
! [A] :
( ! [B] :
( k7_filter_2(A,B) = B
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f132,plain,
! [X0,X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f136,plain,
! [A,B] :
( m1_filter_2(k15_filter_2(A,B),k1_lattice2(A))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f137,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f138,plain,
! [A] :
( ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f140,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f147,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f148,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f151,plain,
! [A] :
( ( l2_lattices(A)
& l1_lattices(A) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f152,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f160,plain,
! [A] :
( ! [B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
| ~ m2_filter_2(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f162,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f163,plain,
! [A] :
( ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ m2_lattice4(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f164,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f203,plain,
! [A] :
( ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f204,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f208,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f239,plain,
! [A] :
( ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f59]) ).
fof(f248,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f253,plain,
( v15_lattices(sK13_skl)
& v14_lattices(sK13_skl)
& v13_lattices(sK13_skl)
& v10_lattices(sK13_skl)
& v9_lattices(sK13_skl)
& v8_lattices(sK13_skl)
& v7_lattices(sK13_skl)
& v6_lattices(sK13_skl)
& v5_lattices(sK13_skl)
& v4_lattices(sK13_skl)
& v3_lattices(sK13_skl)
& ~ v3_struct_0(sK13_skl)
& l3_lattices(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f61]) ).
fof(f264,plain,
v13_lattices(sK13_skl),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f280,plain,
( v1_funct_1(sK18_skl)
& v1_xboole_0(sK18_skl)
& v1_relat_1(sK18_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f66]) ).
fof(f282,plain,
v1_xboole_0(sK18_skl),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f293,plain,
( v3_lattices(sK22_skl)
& l3_lattices(sK22_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(A,sK22_skl)],[f70]) ).
fof(f294,plain,
l3_lattices(sK22_skl),
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f296,plain,
( ~ v3_struct_0(sK23_skl)
& l1_struct_0(sK23_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(A,sK23_skl)],[f71]) ).
fof(f298,plain,
~ v3_struct_0(sK23_skl),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f303,plain,
( v3_lattices(sK25_skl)
& ~ v3_struct_0(sK25_skl)
& l3_lattices(sK25_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(A,sK25_skl)],[f73]) ).
fof(f304,plain,
l3_lattices(sK25_skl),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f305,plain,
~ v3_struct_0(sK25_skl),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f307,plain,
( v10_lattices(sK26_skl)
& v9_lattices(sK26_skl)
& v8_lattices(sK26_skl)
& v7_lattices(sK26_skl)
& v6_lattices(sK26_skl)
& v5_lattices(sK26_skl)
& v4_lattices(sK26_skl)
& v3_lattices(sK26_skl)
& ~ v3_struct_0(sK26_skl)
& l3_lattices(sK26_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(A,sK26_skl)],[f74]) ).
fof(f308,plain,
l3_lattices(sK26_skl),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f309,plain,
~ v3_struct_0(sK26_skl),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f317,plain,
v10_lattices(sK26_skl),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f318,plain,
! [A,B] :
( k15_filter_2(A,B) = k7_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f319,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f320,plain,
! [A] :
( ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f321,plain,
! [A] :
( ! [B] :
( ( ~ m1_filter_0(B,A)
| m1_filter_2(B,A) )
& ( m1_filter_0(B,A)
| ~ m1_filter_2(B,A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f320]) ).
fof(f322,plain,
! [A] :
( ( ! [B] :
( ~ m1_filter_0(B,A)
| m1_filter_2(B,A) )
& ! [B] :
( m1_filter_0(B,A)
| ~ m1_filter_2(B,A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(miniscoping,[status(thm)],[f321]) ).
fof(f323,plain,
! [X0,X1] :
( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f331,plain,
! [A] :
( ! [B] :
( r2_hidden(k6_lattices(A),B)
| ~ l3_lattices(A)
| ~ v14_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f332,plain,
! [X0,X1] :
( r2_hidden(k6_lattices(X0),X1)
| ~ l3_lattices(X0)
| ~ v14_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f347,plain,
! [A] :
( ( v13_lattices(A)
<=> v14_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f348,plain,
! [A] :
( ( ( ~ v14_lattices(k1_lattice2(A))
| v13_lattices(A) )
& ( v14_lattices(k1_lattice2(A))
| ~ v13_lattices(A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f347]) ).
fof(f349,plain,
! [X0] :
( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f353,plain,
! [A] :
( k5_lattices(A) = k6_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v13_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f87]) ).
fof(f354,plain,
! [X0] :
( k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v13_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f353]) ).
fof(f362,plain,
! [X0,X1] :
( r2_hidden(k6_lattices(X0),X1)
| ~ v14_lattices(X0)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f332]) ).
fof(f372,definition,
( sQ2_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f373,plain,
( ~ sQ2_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f372]) ).
fof(f375,definition,
( sQ3_spl
<=> v10_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f377,plain,
( sQ3_spl
| ~ v10_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f375]) ).
fof(f387,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f377,f93]) ).
fof(f388,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f387]) ).
fof(f389,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f373,f92]) ).
fof(f390,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f389]) ).
fof(f402,definition,
( sQ8_spl
<=> l3_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f404,plain,
( sQ8_spl
| ~ l3_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f402]) ).
fof(f409,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f404,f94]) ).
fof(f410,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f409]) ).
fof(f501,plain,
( k5_lattices(sK0_skl) = k6_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f354,f96]) ).
fof(f509,definition,
( sQ30_spl
<=> k5_lattices(sK0_skl) = k6_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f510,plain,
( ~ sQ30_spl
| k5_lattices(sK0_skl) = k6_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f509]) ).
fof(f512,plain,
( sQ30_spl
| ~ sQ8_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f501,f372,f375,f402,f509]) ).
fof(f523,plain,
( m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f137,f95]) ).
fof(f524,definition,
( sQ32_spl
<=> m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f525,plain,
( ~ sQ32_spl
| m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f524]) ).
fof(f527,plain,
( sQ32_spl
| ~ sQ8_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f523,f372,f375,f402,f524]) ).
fof(f532,definition,
( sQ33_spl
<=> l3_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f534,plain,
( sQ33_spl
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f532]) ).
fof(f541,plain,
l3_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f140,f94]) ).
fof(f542,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f541,f534]) ).
fof(f543,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f542]) ).
fof(f544,plain,
l3_lattices(k1_lattice2(k1_lattice2(sK0_skl))),
inference(resolution,[status(thm)],[f541,f140]) ).
fof(f553,definition,
( sQ35_spl
<=> v3_struct_0(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( ~ sQ35_spl
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,definition,
( sQ36_spl
<=> v10_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f583,plain,
l3_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0_skl)))),
inference(resolution,[status(thm)],[f544,f140]) ).
fof(f636,plain,
l1_lattices(sK0_skl),
inference(resolution,[status(thm)],[f152,f94]) ).
fof(f642,plain,
l1_struct_0(sK0_skl),
inference(resolution,[status(thm)],[f636,f148]) ).
fof(f655,definition,
( sQ55_spl
<=> l3_lattices(k1_lattice2(k1_lattice2(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f657,plain,
( sQ55_spl
| ~ l3_lattices(k1_lattice2(k1_lattice2(sK0_skl))) ),
inference(component_clause,[status(thm)],[f655]) ).
fof(f662,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f544]) ).
fof(f663,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f662]) ).
fof(f688,plain,
( m2_lattice4(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f162,f95]) ).
fof(f689,definition,
( sQ61_spl
<=> m2_lattice4(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f690,plain,
( ~ sQ61_spl
| m2_lattice4(sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f692,plain,
( sQ61_spl
| ~ sQ8_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f688,f372,f375,f402,f689]) ).
fof(f693,plain,
( ~ sQ61_spl
| m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f690,f164]) ).
fof(f694,definition,
( sQ62_spl
<=> m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f695,plain,
( ~ sQ62_spl
| m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
inference(component_clause,[status(thm)],[f694]) ).
fof(f697,plain,
( ~ sQ61_spl
| sQ62_spl
| ~ sQ8_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f693,f372,f375,f402,f694,f689]) ).
fof(f713,plain,
( ~ sQ62_spl
| k7_filter_2(sK0_skl,sK1_skl) = sK1_skl
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f695,f132]) ).
fof(f719,definition,
( sQ67_spl
<=> k7_filter_2(sK0_skl,sK1_skl) = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f720,plain,
( ~ sQ67_spl
| k7_filter_2(sK0_skl,sK1_skl) = sK1_skl ),
inference(component_clause,[status(thm)],[f719]) ).
fof(f722,plain,
( ~ sQ62_spl
| sQ67_spl
| ~ sQ8_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f713,f372,f375,f402,f719,f694]) ).
fof(f723,definition,
( sQ68_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f724,plain,
( ~ sQ68_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
inference(component_clause,[status(thm)],[f723]) ).
fof(f731,plain,
( ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f724,f208]) ).
fof(f732,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f731]) ).
fof(f775,definition,
( sQ78_spl
<=> l3_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f777,plain,
( sQ78_spl
| ~ l3_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f775]) ).
fof(f782,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f777,f583]) ).
fof(f783,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f782]) ).
fof(f785,definition,
( sQ80_spl
<=> v13_lattices(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f787,plain,
( sQ80_spl
| ~ v13_lattices(sK13_skl) ),
inference(component_clause,[status(thm)],[f785]) ).
fof(f792,plain,
( sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f787,f264]) ).
fof(f793,plain,
sQ80_spl,
inference(contradiction_clause,[status(thm)],[f792]) ).
fof(f836,definition,
( sQ86_spl
<=> v1_xboole_0(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f838,plain,
( sQ86_spl
| ~ v1_xboole_0(sK18_skl) ),
inference(component_clause,[status(thm)],[f836]) ).
fof(f843,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f838,f282]) ).
fof(f844,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f843]) ).
fof(f1056,plain,
( ~ sQ35_spl
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f204,f554]) ).
fof(f1058,plain,
( ~ sQ35_spl
| ~ sQ8_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1056,f372,f402,f553]) ).
fof(f1061,definition,
( sQ125_spl
<=> l1_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1063,plain,
( sQ125_spl
| ~ l1_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f1061]) ).
fof(f1065,plain,
( sQ125_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1063,f642]) ).
fof(f1066,plain,
sQ125_spl,
inference(contradiction_clause,[status(thm)],[f1065]) ).
fof(f1319,definition,
( sQ173_spl
<=> l3_lattices(sK22_skl) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f1321,plain,
( sQ173_spl
| ~ l3_lattices(sK22_skl) ),
inference(component_clause,[status(thm)],[f1319]) ).
fof(f1326,plain,
( sQ173_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1321,f294]) ).
fof(f1327,plain,
sQ173_spl,
inference(contradiction_clause,[status(thm)],[f1326]) ).
fof(f1438,definition,
( sQ196_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f1439,plain,
( ~ sQ196_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f1438]) ).
fof(f1445,plain,
( ~ sQ196_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1439,f208]) ).
fof(f1446,plain,
~ sQ196_spl,
inference(contradiction_clause,[status(thm)],[f1445]) ).
fof(f1467,definition,
( sQ198_spl
<=> v3_struct_0(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f1468,plain,
( ~ sQ198_spl
| v3_struct_0(sK25_skl) ),
inference(component_clause,[status(thm)],[f1467]) ).
fof(f1513,plain,
( ~ sQ198_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1468,f305]) ).
fof(f1514,plain,
~ sQ198_spl,
inference(contradiction_clause,[status(thm)],[f1513]) ).
fof(f1668,definition,
( sQ234_spl
<=> l3_lattices(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f1670,plain,
( sQ234_spl
| ~ l3_lattices(sK25_skl) ),
inference(component_clause,[status(thm)],[f1668]) ).
fof(f1675,plain,
( sQ234_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1670,f304]) ).
fof(f1676,plain,
sQ234_spl,
inference(contradiction_clause,[status(thm)],[f1675]) ).
fof(f1696,definition,
( sQ236_spl
<=> v3_struct_0(sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f1697,plain,
( ~ sQ236_spl
| v3_struct_0(sK26_skl) ),
inference(component_clause,[status(thm)],[f1696]) ).
fof(f1699,definition,
( sQ237_spl
<=> v10_lattices(sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f1701,plain,
( sQ237_spl
| ~ v10_lattices(sK26_skl) ),
inference(component_clause,[status(thm)],[f1699]) ).
fof(f1758,plain,
( sQ237_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1701,f317]) ).
fof(f1759,plain,
sQ237_spl,
inference(contradiction_clause,[status(thm)],[f1758]) ).
fof(f1760,plain,
( ~ sQ236_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1697,f309]) ).
fof(f1761,plain,
~ sQ236_spl,
inference(contradiction_clause,[status(thm)],[f1760]) ).
fof(f1842,plain,
( v10_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f248,f94]) ).
fof(f1869,plain,
( sQ36_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1842,f372,f375,f556]) ).
fof(f1918,definition,
( sQ278_spl
<=> l3_lattices(sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f1920,plain,
( sQ278_spl
| ~ l3_lattices(sK26_skl) ),
inference(component_clause,[status(thm)],[f1918]) ).
fof(f1925,plain,
( sQ278_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1920,f308]) ).
fof(f1926,plain,
sQ278_spl,
inference(contradiction_clause,[status(thm)],[f1925]) ).
fof(f2052,definition,
( sQ298_spl
<=> v3_struct_0(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition]) ).
fof(f2053,plain,
( ~ sQ298_spl
| v3_struct_0(sK23_skl) ),
inference(component_clause,[status(thm)],[f2052]) ).
fof(f2078,plain,
( ~ sQ298_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2053,f298]) ).
fof(f2079,plain,
~ sQ298_spl,
inference(contradiction_clause,[status(thm)],[f2078]) ).
fof(f2084,plain,
( k15_filter_2(sK0_skl,sK1_skl) = k7_filter_2(sK0_skl,sK1_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f319,f95]) ).
fof(f2093,definition,
( sQ307_spl
<=> k15_filter_2(sK0_skl,sK1_skl) = k7_filter_2(sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f2094,plain,
( ~ sQ307_spl
| k15_filter_2(sK0_skl,sK1_skl) = k7_filter_2(sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f2093]) ).
fof(f2096,plain,
( sQ307_spl
| ~ sQ8_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2084,f372,f375,f402,f2093]) ).
fof(f2102,plain,
( ~ sQ32_spl
| ~ sQ307_spl
| ~ sQ67_spl
| m1_filter_2(sK1_skl,k1_lattice2(sK0_skl)) ),
inference(backward_demodulation,[status(thm)],[f2104,f525]) ).
fof(f2104,plain,
( ~ sQ307_spl
| ~ sQ67_spl
| k15_filter_2(sK0_skl,sK1_skl) = sK1_skl ),
inference(forward_demodulation,[status(thm)],[f720,f2094]) ).
fof(f2120,plain,
( ~ sQ32_spl
| ~ sQ307_spl
| ~ sQ67_spl
| m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f2102,f323]) ).
fof(f2123,definition,
( sQ310_spl
<=> m1_filter_0(sK1_skl,k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f2124,plain,
( ~ sQ310_spl
| m1_filter_0(sK1_skl,k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2123]) ).
fof(f2126,plain,
( ~ sQ32_spl
| ~ sQ307_spl
| ~ sQ67_spl
| sQ310_spl
| ~ sQ33_spl
| ~ sQ36_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f2120,f553,f556,f532,f2123,f719,f2093,f524]) ).
fof(f2156,definition,
( sQ316_spl
<=> v14_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition]) ).
fof(f2218,plain,
( ~ sQ310_spl
| r2_hidden(k6_lattices(k1_lattice2(sK0_skl)),sK1_skl)
| ~ v14_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f2124,f362]) ).
fof(f2222,definition,
( sQ327_spl
<=> r2_hidden(k6_lattices(k1_lattice2(sK0_skl)),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition]) ).
fof(f2223,plain,
( ~ sQ327_spl
| r2_hidden(k6_lattices(k1_lattice2(sK0_skl)),sK1_skl) ),
inference(component_clause,[status(thm)],[f2222]) ).
fof(f2225,plain,
( ~ sQ310_spl
| sQ327_spl
| ~ sQ316_spl
| ~ sQ33_spl
| ~ sQ36_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f2218,f553,f556,f532,f2156,f2222,f2123]) ).
fof(f2243,plain,
( v14_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f349,f96]) ).
fof(f2248,plain,
( sQ316_spl
| ~ sQ8_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2243,f372,f375,f402,f2156]) ).
fof(f2250,plain,
( ~ sQ327_spl
| ~ sQ30_spl
| r2_hidden(k5_lattices(sK0_skl),sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f510,f2223]) ).
fof(f2251,plain,
( ~ sQ327_spl
| ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2250,f97]) ).
fof(f2252,plain,
( ~ sQ327_spl
| ~ sQ30_spl ),
inference(contradiction_clause,[status(thm)],[f2251]) ).
fof(f2253,plain,
$false,
inference(sat_refutation,[status(thm)],[f388,f390,f410,f512,f527,f543,f663,f692,f697,f722,f732,f783,f793,f844,f1058,f1066,f1327,f1446,f1514,f1676,f1759,f1761,f1869,f1926,f2079,f2096,f2126,f2225,f2248,f2252]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT301+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n009.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 20 23:30:42 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.48 % Drodi V4.1.1
% 0.17/0.63 % Refutation found
% 0.17/0.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.17/0.67 % Elapsed time: 0.214941 seconds
% 0.17/0.67 % CPU time: 1.038700 seconds
% 0.17/0.67 % Total memory used: 94.451 MB
% 0.17/0.67 % Net memory used: 93.989 MB
%------------------------------------------------------------------------------