%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU371+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 : 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 02:20:19 PM UTC 2026
% Result : Theorem 0.12s 0.45s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 11
% Syntax : Number of formulae : 57 ( 26 unt; 0 def)
% Number of atoms : 165 ( 45 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 159 ( 51 ~; 49 |; 55 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 23 ( 21 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-2 aty)
% Number of variables : 78 ( 76 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f19,axiom,
! [A] :
( rel_str(A)
=> bottom_of_relstr(A) = join_on_relstr(A,empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] : boole_POSet(A) = poset_of_lattice(boole_lattice(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] :
( latt_str(boole_lattice(A))
& strict_latt_str(boole_lattice(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A] :
( rel_str(boole_POSet(A))
& strict_rel_str(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [A] :
( complete_latt_str(boole_lattice(A))
& boolean_lattstr(boole_lattice(A))
& complemented_lattstr(boole_lattice(A))
& bounded_lattstr(boole_lattice(A))
& upper_bounded_semilattstr(boole_lattice(A))
& lower_bounded_semilattstr(boole_lattice(A))
& modular_lattstr(boole_lattice(A))
& distributive_lattstr(boole_lattice(A))
& lattice(boole_lattice(A))
& join_absorbing(boole_lattice(A))
& meet_absorbing(boole_lattice(A))
& meet_associative(boole_lattice(A))
& meet_commutative(boole_lattice(A))
& join_associative(boole_lattice(A))
& join_commutative(boole_lattice(A))
& strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f103,conjecture,
! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,negated_conjecture,
~ ! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set,
inference(negated_conjecture,[status(cth)],[f103]) ).
fof(f106,axiom,
! [A] :
( ( latt_str(A)
& complete_latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ! [B] :
( meet_of_latt_set(A,B) = meet_on_relstr(poset_of_lattice(A),B)
& join_of_latt_set(A,B) = join_on_relstr(poset_of_lattice(A),B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [A] :
( bottom_of_semilattstr(boole_lattice(A)) = empty_set
& lower_bounded_semilattstr(boole_lattice(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,axiom,
! [A] :
( ( latt_str(A)
& complete_latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ( bottom_of_semilattstr(A) = join_of_latt_set(A,empty_set)
& latt_str(A)
& lower_bounded_semilattstr(A)
& lattice(A)
& ~ empty_carrier(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,plain,
! [A] :
( bottom_of_relstr(A) = join_on_relstr(A,empty_set)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f193,plain,
! [X0] :
( bottom_of_relstr(X0) = join_on_relstr(X0,empty_set)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f198,plain,
! [X0] : boole_POSet(X0) = poset_of_lattice(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f211,plain,
( ! [A] : latt_str(boole_lattice(A))
& ! [A] : strict_latt_str(boole_lattice(A)) ),
inference(miniscoping,[status(thm)],[f27]) ).
fof(f213,plain,
! [X0] : latt_str(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f234,plain,
( ! [A] : rel_str(boole_POSet(A))
& ! [A] : strict_rel_str(boole_POSet(A)) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f236,plain,
! [X0] : rel_str(boole_POSet(X0)),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f278,plain,
( ! [A] : complete_latt_str(boole_lattice(A))
& ! [A] : boolean_lattstr(boole_lattice(A))
& ! [A] : complemented_lattstr(boole_lattice(A))
& ! [A] : bounded_lattstr(boole_lattice(A))
& ! [A] : upper_bounded_semilattstr(boole_lattice(A))
& ! [A] : lower_bounded_semilattstr(boole_lattice(A))
& ! [A] : modular_lattstr(boole_lattice(A))
& ! [A] : distributive_lattstr(boole_lattice(A))
& ! [A] : lattice(boole_lattice(A))
& ! [A] : join_absorbing(boole_lattice(A))
& ! [A] : meet_absorbing(boole_lattice(A))
& ! [A] : meet_associative(boole_lattice(A))
& ! [A] : meet_commutative(boole_lattice(A))
& ! [A] : join_associative(boole_lattice(A))
& ! [A] : join_commutative(boole_lattice(A))
& ! [A] : strict_latt_str(boole_lattice(A))
& ! [A] : ~ empty_carrier(boole_lattice(A)) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f279,plain,
! [X0] : ~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f287,plain,
! [X0] : lattice(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f295,plain,
! [X0] : complete_latt_str(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f502,plain,
empty(sK16_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f88]) ).
fof(f503,plain,
empty(sK16_skl),
inference(cnf_transformation,[status(thm)],[f502]) ).
fof(f575,plain,
? [A] : bottom_of_relstr(boole_POSet(A)) != empty_set,
inference(pre_NNF_transformation,[status(thm)],[f104]) ).
fof(f576,plain,
bottom_of_relstr(boole_POSet(sK28_skl)) != empty_set,
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl]),skolemize(A,sK28_skl)],[f575]) ).
fof(f577,plain,
bottom_of_relstr(boole_POSet(sK28_skl)) != empty_set,
inference(cnf_transformation,[status(thm)],[f576]) ).
fof(f580,plain,
! [A] :
( ! [B] :
( meet_of_latt_set(A,B) = meet_on_relstr(poset_of_lattice(A),B)
& join_of_latt_set(A,B) = join_on_relstr(poset_of_lattice(A),B) )
| ~ latt_str(A)
| ~ complete_latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f106]) ).
fof(f581,plain,
! [A] :
( ( ! [B] : meet_of_latt_set(A,B) = meet_on_relstr(poset_of_lattice(A),B)
& ! [B] : join_of_latt_set(A,B) = join_on_relstr(poset_of_lattice(A),B) )
| ~ latt_str(A)
| ~ complete_latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(miniscoping,[status(thm)],[f580]) ).
fof(f582,plain,
! [X0,X1] :
( join_of_latt_set(X0,X1) = join_on_relstr(poset_of_lattice(X0),X1)
| ~ latt_str(X0)
| ~ complete_latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f581]) ).
fof(f591,plain,
( ! [A] : bottom_of_semilattstr(boole_lattice(A)) = empty_set
& ! [A] : lower_bounded_semilattstr(boole_lattice(A)) ),
inference(miniscoping,[status(thm)],[f109]) ).
fof(f593,plain,
! [X0] : bottom_of_semilattstr(boole_lattice(X0)) = empty_set,
inference(cnf_transformation,[status(thm)],[f591]) ).
fof(f601,plain,
! [A] :
( ( bottom_of_semilattstr(A) = join_of_latt_set(A,empty_set)
& latt_str(A)
& lower_bounded_semilattstr(A)
& lattice(A)
& ~ empty_carrier(A) )
| ~ latt_str(A)
| ~ complete_latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f112]) ).
fof(f606,plain,
! [X0] :
( bottom_of_semilattstr(X0) = join_of_latt_set(X0,empty_set)
| ~ latt_str(X0)
| ~ complete_latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f601]) ).
fof(f610,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f114]) ).
fof(f611,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f610]) ).
fof(f619,plain,
! [X0] : bottom_of_relstr(boole_POSet(X0)) = join_on_relstr(boole_POSet(X0),empty_set),
inference(resolution,[status(thm)],[f236,f193]) ).
fof(f816,plain,
sK16_skl = empty_set,
inference(resolution,[status(thm)],[f503,f611]) ).
fof(f820,plain,
! [X0] : bottom_of_relstr(boole_POSet(X0)) = join_on_relstr(boole_POSet(X0),sK16_skl),
inference(backward_demodulation,[status(thm)],[f816,f619]) ).
fof(f825,plain,
bottom_of_relstr(boole_POSet(sK28_skl)) != sK16_skl,
inference(backward_demodulation,[status(thm)],[f816,f577]) ).
fof(f994,plain,
! [X0] : bottom_of_semilattstr(boole_lattice(X0)) = sK16_skl,
inference(forward_demodulation,[status(thm)],[f816,f593]) ).
fof(f1112,plain,
! [X0,X1] :
( join_of_latt_set(boole_lattice(X0),X1) = join_on_relstr(poset_of_lattice(boole_lattice(X0)),X1)
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(resolution,[status(thm)],[f582,f295]) ).
fof(f1113,plain,
! [X0,X1] :
( join_of_latt_set(boole_lattice(X0),X1) = join_on_relstr(boole_POSet(X0),X1)
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(forward_demodulation,[status(thm)],[f198,f1112]) ).
fof(f1114,plain,
! [X0,X1] :
( join_of_latt_set(boole_lattice(X0),X1) = join_on_relstr(boole_POSet(X0),X1)
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1113,f279]) ).
fof(f1115,plain,
! [X0,X1] :
( join_of_latt_set(boole_lattice(X0),X1) = join_on_relstr(boole_POSet(X0),X1)
| ~ latt_str(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1114,f287]) ).
fof(f1116,plain,
! [X0,X1] : join_of_latt_set(boole_lattice(X0),X1) = join_on_relstr(boole_POSet(X0),X1),
inference(resolution,[status(thm)],[f1115,f213]) ).
fof(f1148,plain,
! [X0] : bottom_of_relstr(boole_POSet(X0)) = join_of_latt_set(boole_lattice(X0),sK16_skl),
inference(backward_demodulation,[status(thm)],[f1116,f820]) ).
fof(f1171,plain,
! [X0] :
( bottom_of_semilattstr(X0) = join_of_latt_set(X0,sK16_skl)
| ~ latt_str(X0)
| ~ complete_latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(forward_demodulation,[status(thm)],[f816,f606]) ).
fof(f1172,plain,
! [X0] :
( bottom_of_semilattstr(boole_lattice(X0)) = join_of_latt_set(boole_lattice(X0),sK16_skl)
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(resolution,[status(thm)],[f1171,f295]) ).
fof(f1173,plain,
! [X0] :
( sK16_skl = join_of_latt_set(boole_lattice(X0),sK16_skl)
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(forward_demodulation,[status(thm)],[f994,f1172]) ).
fof(f1174,plain,
! [X0] :
( sK16_skl = bottom_of_relstr(boole_POSet(X0))
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(forward_demodulation,[status(thm)],[f1148,f1173]) ).
fof(f1175,plain,
! [X0] :
( sK16_skl = bottom_of_relstr(boole_POSet(X0))
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1174,f279]) ).
fof(f1176,plain,
! [X0] :
( sK16_skl = bottom_of_relstr(boole_POSet(X0))
| ~ latt_str(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1175,f287]) ).
fof(f1177,plain,
! [X0] : sK16_skl = bottom_of_relstr(boole_POSet(X0)),
inference(resolution,[status(thm)],[f1176,f213]) ).
fof(f1178,plain,
sK16_skl != sK16_skl,
inference(backward_demodulation,[status(thm)],[f1177,f825]) ).
fof(f1184,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f1178]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU371+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n005.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 06:15:49 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 0.12/0.45 % Refutation found
% 0.12/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.47 % Elapsed time: 0.089551 seconds
% 0.12/0.47 % CPU time: 0.370614 seconds
% 0.12/0.47 % Total memory used: 122.503 MB
% 0.12/0.47 % Net memory used: 122.102 MB
%------------------------------------------------------------------------------