%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU344+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 02:20:14 PM UTC 2026
% Result : Theorem 0.14s 0.44s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 8
% Syntax : Number of formulae : 51 ( 12 unt; 0 def)
% Number of atoms : 149 ( 34 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 163 ( 65 ~; 64 |; 18 &)
% ( 4 <=>; 11 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 71 ( 65 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [A] :
( ( join_semilatt_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( below(A,B,C)
<=> join(A,B,C) = C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( latt_str(boole_lattice(A))
& strict_latt_str(boole_lattice(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A] :
( latt_str(A)
=> ( join_semilatt_str(A)
& meet_semilatt_str(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [A,B] :
( subset(A,B)
=> set_union2(A,B) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [A,B] :
( element(B,the_carrier(boole_lattice(A)))
=> ! [C] :
( element(C,the_carrier(boole_lattice(A)))
=> ( meet(boole_lattice(A),B,C) = set_intersection2(B,C)
& join(boole_lattice(A),B,C) = set_union2(B,C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,conjecture,
! [A,B] :
( element(B,the_carrier(boole_lattice(A)))
=> ! [C] :
( element(C,the_carrier(boole_lattice(A)))
=> ( below(boole_lattice(A),B,C)
<=> subset(B,C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,negated_conjecture,
~ ! [A,B] :
( element(B,the_carrier(boole_lattice(A)))
=> ! [C] :
( element(C,the_carrier(boole_lattice(A)))
=> ( below(boole_lattice(A),B,C)
<=> subset(B,C) ) ) ),
inference(negated_conjecture,[status(cth)],[f73]) ).
fof(f81,axiom,
! [A,B] : subset(A,set_union2(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( below(A,B,C)
<=> join(A,B,C) = C )
| ~ element(C,the_carrier(A)) )
| ~ element(B,the_carrier(A)) )
| ~ join_semilatt_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f100,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( join(A,B,C) != C
| below(A,B,C) )
& ( join(A,B,C) = C
| ~ below(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ element(B,the_carrier(A)) )
| ~ join_semilatt_str(A)
| empty_carrier(A) ),
inference(NNF_transformation,[status(thm)],[f99]) ).
fof(f101,plain,
! [X0,X1,X2] :
( join(X0,X1,X2) = X2
| ~ below(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f102,plain,
! [X0,X1,X2] :
( join(X0,X1,X2) != X2
| below(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f107,plain,
( ! [A] : latt_str(boole_lattice(A))
& ! [A] : strict_latt_str(boole_lattice(A)) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f109,plain,
! [X0] : latt_str(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f120,plain,
! [A] :
( ( join_semilatt_str(A)
& meet_semilatt_str(A) )
| ~ latt_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f122,plain,
! [X0] :
( join_semilatt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f147,plain,
( ! [A] : strict_latt_str(boole_lattice(A))
& ! [A] : ~ empty_carrier(boole_lattice(A)) ),
inference(miniscoping,[status(thm)],[f44]) ).
fof(f148,plain,
! [X0] : ~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f208,plain,
! [A,B] :
( set_union2(A,B) = B
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f209,plain,
! [X0,X1] :
( set_union2(X0,X1) = X1
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f211,plain,
! [A,B] :
( ! [C] :
( ( meet(boole_lattice(A),B,C) = set_intersection2(B,C)
& join(boole_lattice(A),B,C) = set_union2(B,C) )
| ~ element(C,the_carrier(boole_lattice(A))) )
| ~ element(B,the_carrier(boole_lattice(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f70]) ).
fof(f212,plain,
! [X0,X1,X2] :
( join(boole_lattice(X1),X0,X2) = set_union2(X0,X2)
| ~ element(X2,the_carrier(boole_lattice(X1)))
| ~ element(X0,the_carrier(boole_lattice(X1))) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f217,plain,
? [A,B] :
( ? [C] :
( ( below(boole_lattice(A),B,C)
<~> subset(B,C) )
& element(C,the_carrier(boole_lattice(A))) )
& element(B,the_carrier(boole_lattice(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f74]) ).
fof(f218,plain,
? [A,B] :
( ? [C] :
( ( ~ subset(B,C)
| ~ below(boole_lattice(A),B,C) )
& ( subset(B,C)
| below(boole_lattice(A),B,C) )
& element(C,the_carrier(boole_lattice(A))) )
& element(B,the_carrier(boole_lattice(A))) ),
inference(NNF_transformation,[status(thm)],[f217]) ).
fof(f219,plain,
( ( ~ subset(sK16_skl,sK17_skl)
| ~ below(boole_lattice(sK15_skl),sK16_skl,sK17_skl) )
& ( subset(sK16_skl,sK17_skl)
| below(boole_lattice(sK15_skl),sK16_skl,sK17_skl) )
& element(sK17_skl,the_carrier(boole_lattice(sK15_skl)))
& element(sK16_skl,the_carrier(boole_lattice(sK15_skl))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(A,sK15_skl),skolemize(B,sK16_skl),skolemize(C,sK17_skl)],[f218]) ).
fof(f220,plain,
element(sK16_skl,the_carrier(boole_lattice(sK15_skl))),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f221,plain,
element(sK17_skl,the_carrier(boole_lattice(sK15_skl))),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f222,plain,
( subset(sK16_skl,sK17_skl)
| below(boole_lattice(sK15_skl),sK16_skl,sK17_skl) ),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f223,plain,
( ~ subset(sK16_skl,sK17_skl)
| ~ below(boole_lattice(sK15_skl),sK16_skl,sK17_skl) ),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f241,plain,
! [X0,X1] : subset(X0,set_union2(X0,X1)),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f245,plain,
( below(boole_lattice(sK15_skl),sK16_skl,sK17_skl)
| set_union2(sK16_skl,sK17_skl) = sK17_skl ),
inference(resolution,[status(thm)],[f209,f222]) ).
fof(f322,plain,
! [X0,X1,X2] :
( join(boole_lattice(X0),X1,X2) != X2
| below(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ join_semilatt_str(boole_lattice(X0)) ),
inference(resolution,[status(thm)],[f148,f102]) ).
fof(f323,plain,
! [X0,X1,X2] :
( join(boole_lattice(X0),X1,X2) = X2
| ~ below(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ join_semilatt_str(boole_lattice(X0)) ),
inference(resolution,[status(thm)],[f148,f101]) ).
fof(f442,plain,
! [X0] : join_semilatt_str(boole_lattice(X0)),
inference(resolution,[status(thm)],[f122,f109]) ).
fof(f448,plain,
! [X0,X1,X2] :
( join(boole_lattice(X1),X0,X2) = X2
| ~ below(boole_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(boole_lattice(X1)))
| ~ element(X0,the_carrier(boole_lattice(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[f323,f442]) ).
fof(f449,plain,
! [X0,X1,X2] :
( join(boole_lattice(X1),X0,X2) != X2
| below(boole_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(boole_lattice(X1)))
| ~ element(X0,the_carrier(boole_lattice(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[f322,f442]) ).
fof(f495,plain,
( set_union2(sK16_skl,sK17_skl) = sK17_skl
| join(boole_lattice(sK15_skl),sK16_skl,sK17_skl) = sK17_skl
| ~ element(sK17_skl,the_carrier(boole_lattice(sK15_skl)))
| ~ element(sK16_skl,the_carrier(boole_lattice(sK15_skl))) ),
inference(resolution,[status(thm)],[f448,f245]) ).
fof(f496,plain,
( set_union2(sK16_skl,sK17_skl) = sK17_skl
| join(boole_lattice(sK15_skl),sK16_skl,sK17_skl) = sK17_skl
| ~ element(sK17_skl,the_carrier(boole_lattice(sK15_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f495,f220]) ).
fof(f543,plain,
( set_union2(sK16_skl,sK17_skl) = sK17_skl
| join(boole_lattice(sK15_skl),sK16_skl,sK17_skl) = sK17_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f496,f221]) ).
fof(f546,plain,
( ~ subset(sK16_skl,sK17_skl)
| join(boole_lattice(sK15_skl),sK16_skl,sK17_skl) != sK17_skl
| ~ element(sK17_skl,the_carrier(boole_lattice(sK15_skl)))
| ~ element(sK16_skl,the_carrier(boole_lattice(sK15_skl))) ),
inference(resolution,[status(thm)],[f449,f223]) ).
fof(f548,plain,
( ~ subset(sK16_skl,sK17_skl)
| join(boole_lattice(sK15_skl),sK16_skl,sK17_skl) != sK17_skl
| ~ element(sK17_skl,the_carrier(boole_lattice(sK15_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f546,f220]) ).
fof(f582,plain,
( ~ subset(sK16_skl,sK17_skl)
| join(boole_lattice(sK15_skl),sK16_skl,sK17_skl) != sK17_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f548,f221]) ).
fof(f1160,plain,
! [X0] :
( join(boole_lattice(sK15_skl),X0,sK17_skl) = set_union2(X0,sK17_skl)
| ~ element(X0,the_carrier(boole_lattice(sK15_skl))) ),
inference(resolution,[status(thm)],[f212,f221]) ).
fof(f1180,plain,
join(boole_lattice(sK15_skl),sK16_skl,sK17_skl) = set_union2(sK16_skl,sK17_skl),
inference(resolution,[status(thm)],[f1160,f220]) ).
fof(f1577,plain,
( ~ subset(sK16_skl,sK17_skl)
| set_union2(sK16_skl,sK17_skl) != sK17_skl ),
inference(backward_demodulation,[status(thm)],[f1180,f582]) ).
fof(f1578,plain,
( set_union2(sK16_skl,sK17_skl) = sK17_skl
| set_union2(sK16_skl,sK17_skl) = sK17_skl ),
inference(backward_demodulation,[status(thm)],[f1180,f543]) ).
fof(f1589,plain,
~ subset(sK16_skl,sK17_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1577,f209]) ).
fof(f1590,plain,
set_union2(sK16_skl,sK17_skl) = sK17_skl,
inference(duplicate_literals_removal,[status(thm)],[f1578]) ).
fof(f1621,plain,
subset(sK16_skl,sK17_skl),
inference(paramodulation,[status(thm)],[f1590,f241]) ).
fof(f1637,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1621,f1589]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU344+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:15:45 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 0.14/0.44 % Refutation found
% 0.14/0.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.48 % Elapsed time: 0.097091 seconds
% 0.14/0.48 % CPU time: 0.403708 seconds
% 0.14/0.48 % Total memory used: 90.341 MB
% 0.14/0.48 % Net memory used: 90.100 MB
%------------------------------------------------------------------------------