%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU371+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:22:27 PM UTC 2026
% Result : Theorem 0.17s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU371+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n008.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 06:17:24 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 0.17/0.49 % Refutation found
% 0.17/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.49 fof(f19,axiom,(
% 0.17/0.49 (! [A] :( rel_str(A)=> bottom_of_relstr(A) = join_on_relstr(A,empty_set) ) )),
% 0.17/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f22,axiom,(
% 0.17/0.49 (! [A] : boole_POSet(A) = poset_of_lattice(boole_lattice(A)) )),
% 0.17/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f27,axiom,(
% 0.17/0.49 (! [A] :( strict_latt_str(boole_lattice(A))& latt_str(boole_lattice(A)) ) )),
% 0.17/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f36,axiom,(
% 0.17/0.49 (! [A] :( strict_rel_str(boole_POSet(A))& rel_str(boole_POSet(A)) ) )),
% 0.17/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f59,axiom,(
% 0.17/0.49 (! [A] :( ~ empty_carrier(boole_lattice(A))& strict_latt_str(boole_lattice(A))& join_commutative(boole_lattice(A))& join_associative(boole_lattice(A))& meet_commutative(boole_lattice(A))& meet_associative(boole_lattice(A))& meet_absorbing(boole_lattice(A))& join_absorbing(boole_lattice(A))& lattice(boole_lattice(A))& distributive_lattstr(boole_lattice(A))& modular_lattstr(boole_lattice(A))& lower_bounded_semilattstr(boole_lattice(A))& upper_bounded_semilattstr(boole_lattice(A))& bounded_lattstr(boole_lattice(A))& complemented_lattstr(boole_lattice(A))& boolean_lattstr(boole_lattice(A))& complete_latt_str(boole_lattice(A)) ) )),
% 0.17/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f103,conjecture,(
% 0.17/0.49 (! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set )),
% 0.17/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f104,negated_conjecture,(
% 0.17/0.49 ~((! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set ))),
% 0.17/0.49 inference(negated_conjecture,[status(cth)],[f103])).
% 0.17/0.49 fof(f106,axiom,(
% 0.17/0.49 (! [A] :( ( ~ empty_carrier(A)& lattice(A)& complete_latt_str(A)& latt_str(A) )=> (! [B] :( join_of_latt_set(A,B) = join_on_relstr(poset_of_lattice(A),B)& meet_of_latt_set(A,B) = meet_on_relstr(poset_of_lattice(A),B) ) )) )),
% 0.17/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f109,axiom,(
% 0.17/0.49 (! [A] :( lower_bounded_semilattstr(boole_lattice(A))& bottom_of_semilattstr(boole_lattice(A)) = empty_set ) )),
% 0.17/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f112,axiom,(
% 0.17/0.49 (! [A] :( ( ~ empty_carrier(A)& lattice(A)& complete_latt_str(A)& latt_str(A) )=> ( ~ empty_carrier(A)& lattice(A)& lower_bounded_semilattstr(A)& latt_str(A)& bottom_of_semilattstr(A) = join_of_latt_set(A,empty_set) ) ) )),
% 0.17/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f192,plain,(
% 0.17/0.49 ![A]: (~rel_str(A)|bottom_of_relstr(A)=join_on_relstr(A,empty_set))),
% 0.17/0.49 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.17/0.49 fof(f193,plain,(
% 0.17/0.49 ![X0]: (~rel_str(X0)|bottom_of_relstr(X0)=join_on_relstr(X0,empty_set))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f192])).
% 0.17/0.49 fof(f198,plain,(
% 0.17/0.49 ![X0]: (boole_POSet(X0)=poset_of_lattice(boole_lattice(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f22])).
% 0.17/0.49 fof(f211,plain,(
% 0.17/0.49 (![A]: strict_latt_str(boole_lattice(A)))&(![A]: latt_str(boole_lattice(A)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f27])).
% 0.17/0.49 fof(f213,plain,(
% 0.17/0.49 ![X0]: (latt_str(boole_lattice(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f211])).
% 0.17/0.49 fof(f234,plain,(
% 0.17/0.49 (![A]: strict_rel_str(boole_POSet(A)))&(![A]: rel_str(boole_POSet(A)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f36])).
% 0.17/0.49 fof(f236,plain,(
% 0.17/0.49 ![X0]: (rel_str(boole_POSet(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f234])).
% 0.17/0.49 fof(f278,plain,(
% 0.17/0.49 ((((((((((((((((![A]: ~empty_carrier(boole_lattice(A)))&(![A]: strict_latt_str(boole_lattice(A))))&(![A]: join_commutative(boole_lattice(A))))&(![A]: join_associative(boole_lattice(A))))&(![A]: meet_commutative(boole_lattice(A))))&(![A]: meet_associative(boole_lattice(A))))&(![A]: meet_absorbing(boole_lattice(A))))&(![A]: join_absorbing(boole_lattice(A))))&(![A]: lattice(boole_lattice(A))))&(![A]: distributive_lattstr(boole_lattice(A))))&(![A]: modular_lattstr(boole_lattice(A))))&(![A]: lower_bounded_semilattstr(boole_lattice(A))))&(![A]: upper_bounded_semilattstr(boole_lattice(A))))&(![A]: bounded_lattstr(boole_lattice(A))))&(![A]: complemented_lattstr(boole_lattice(A))))&(![A]: boolean_lattstr(boole_lattice(A))))&(![A]: complete_latt_str(boole_lattice(A)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f59])).
% 0.17/0.49 fof(f279,plain,(
% 0.17/0.49 ![X0]: (~empty_carrier(boole_lattice(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f278])).
% 0.17/0.49 fof(f287,plain,(
% 0.17/0.49 ![X0]: (lattice(boole_lattice(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f278])).
% 0.17/0.49 fof(f295,plain,(
% 0.17/0.49 ![X0]: (complete_latt_str(boole_lattice(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f278])).
% 0.17/0.49 fof(f575,plain,(
% 0.17/0.49 (?[A]: ~bottom_of_relstr(boole_POSet(A))=empty_set)),
% 0.17/0.49 inference(pre_NNF_transformation,[status(thm)],[f104])).
% 0.17/0.49 fof(f576,plain,(
% 0.17/0.49 ~bottom_of_relstr(boole_POSet(sK28_skl))=empty_set),
% 0.17/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl]),skolemize(A,sK28_skl)],[f575])).
% 0.17/0.49 fof(f577,plain,(
% 0.17/0.49 ~bottom_of_relstr(boole_POSet(sK28_skl))=empty_set),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f576])).
% 0.17/0.49 fof(f580,plain,(
% 0.17/0.49 ![A]: ((((empty_carrier(A)|~lattice(A))|~complete_latt_str(A))|~latt_str(A))|(![B]: (join_of_latt_set(A,B)=join_on_relstr(poset_of_lattice(A),B)&meet_of_latt_set(A,B)=meet_on_relstr(poset_of_lattice(A),B))))),
% 0.17/0.49 inference(pre_NNF_transformation,[status(thm)],[f106])).
% 0.17/0.49 fof(f581,plain,(
% 0.17/0.49 ![A]: ((((empty_carrier(A)|~lattice(A))|~complete_latt_str(A))|~latt_str(A))|((![B]: join_of_latt_set(A,B)=join_on_relstr(poset_of_lattice(A),B))&(![B]: meet_of_latt_set(A,B)=meet_on_relstr(poset_of_lattice(A),B))))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f580])).
% 0.17/0.49 fof(f582,plain,(
% 0.17/0.49 ![X0,X1]: (empty_carrier(X0)|~lattice(X0)|~complete_latt_str(X0)|~latt_str(X0)|join_of_latt_set(X0,X1)=join_on_relstr(poset_of_lattice(X0),X1))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f581])).
% 0.17/0.49 fof(f591,plain,(
% 0.17/0.49 (![A]: lower_bounded_semilattstr(boole_lattice(A)))&(![A]: bottom_of_semilattstr(boole_lattice(A))=empty_set)),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f109])).
% 0.17/0.49 fof(f593,plain,(
% 0.17/0.49 ![X0]: (bottom_of_semilattstr(boole_lattice(X0))=empty_set)),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f591])).
% 0.17/0.49 fof(f601,plain,(
% 0.17/0.49 ![A]: ((((empty_carrier(A)|~lattice(A))|~complete_latt_str(A))|~latt_str(A))|((((~empty_carrier(A)&lattice(A))&lower_bounded_semilattstr(A))&latt_str(A))&bottom_of_semilattstr(A)=join_of_latt_set(A,empty_set)))),
% 0.17/0.49 inference(pre_NNF_transformation,[status(thm)],[f112])).
% 0.17/0.49 fof(f606,plain,(
% 0.17/0.49 ![X0]: (empty_carrier(X0)|~lattice(X0)|~complete_latt_str(X0)|~latt_str(X0)|bottom_of_semilattstr(X0)=join_of_latt_set(X0,empty_set))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f601])).
% 0.17/0.49 fof(f619,plain,(
% 0.17/0.49 ![X0]: (bottom_of_relstr(boole_POSet(X0))=join_on_relstr(boole_POSet(X0),empty_set))),
% 0.17/0.49 inference(resolution,[status(thm)],[f236,f193])).
% 0.17/0.49 fof(f1022,plain,(
% 0.17/0.49 ![X0,X1]: (empty_carrier(boole_lattice(X0))|~lattice(boole_lattice(X0))|~latt_str(boole_lattice(X0))|join_of_latt_set(boole_lattice(X0),X1)=join_on_relstr(poset_of_lattice(boole_lattice(X0)),X1))),
% 0.17/0.49 inference(resolution,[status(thm)],[f582,f295])).
% 0.17/0.49 fof(f1023,plain,(
% 0.17/0.49 ![X0,X1]: (empty_carrier(boole_lattice(X0))|~lattice(boole_lattice(X0))|~latt_str(boole_lattice(X0))|join_of_latt_set(boole_lattice(X0),X1)=join_on_relstr(boole_POSet(X0),X1))),
% 0.17/0.49 inference(forward_demodulation,[status(thm)],[f198,f1022])).
% 0.17/0.49 fof(f1024,plain,(
% 0.17/0.49 ![X0,X1]: (~lattice(boole_lattice(X0))|~latt_str(boole_lattice(X0))|join_of_latt_set(boole_lattice(X0),X1)=join_on_relstr(boole_POSet(X0),X1))),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f1023,f279])).
% 0.17/0.49 fof(f1028,plain,(
% 0.17/0.49 ![X0,X1]: (~latt_str(boole_lattice(X0))|join_of_latt_set(boole_lattice(X0),X1)=join_on_relstr(boole_POSet(X0),X1))),
% 0.17/0.49 inference(resolution,[status(thm)],[f1024,f287])).
% 0.17/0.49 fof(f1031,plain,(
% 0.17/0.49 ![X0,X1]: (join_of_latt_set(boole_lattice(X0),X1)=join_on_relstr(boole_POSet(X0),X1))),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f1028,f213])).
% 0.17/0.49 fof(f1069,plain,(
% 0.17/0.49 ![X0]: (empty_carrier(boole_lattice(X0))|~lattice(boole_lattice(X0))|~latt_str(boole_lattice(X0))|bottom_of_semilattstr(boole_lattice(X0))=join_of_latt_set(boole_lattice(X0),empty_set))),
% 0.17/0.49 inference(resolution,[status(thm)],[f606,f295])).
% 0.17/0.49 fof(f1070,plain,(
% 0.17/0.49 ![X0]: (empty_carrier(boole_lattice(X0))|~lattice(boole_lattice(X0))|~latt_str(boole_lattice(X0))|empty_set=join_of_latt_set(boole_lattice(X0),empty_set))),
% 0.17/0.49 inference(forward_demodulation,[status(thm)],[f593,f1069])).
% 0.17/0.49 fof(f1071,plain,(
% 0.17/0.49 ![X0]: (empty_carrier(boole_lattice(X0))|~lattice(boole_lattice(X0))|~latt_str(boole_lattice(X0))|empty_set=join_on_relstr(boole_POSet(X0),empty_set))),
% 0.17/0.49 inference(forward_demodulation,[status(thm)],[f1031,f1070])).
% 0.17/0.49 fof(f1072,plain,(
% 0.17/0.49 ![X0]: (empty_carrier(boole_lattice(X0))|~lattice(boole_lattice(X0))|~latt_str(boole_lattice(X0))|empty_set=bottom_of_relstr(boole_POSet(X0)))),
% 0.17/0.49 inference(forward_demodulation,[status(thm)],[f619,f1071])).
% 0.17/0.49 fof(f1073,plain,(
% 0.17/0.49 ![X0]: (~lattice(boole_lattice(X0))|~latt_str(boole_lattice(X0))|empty_set=bottom_of_relstr(boole_POSet(X0)))),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f1072,f279])).
% 0.17/0.49 fof(f1087,plain,(
% 0.17/0.49 ![X0]: (~latt_str(boole_lattice(X0))|empty_set=bottom_of_relstr(boole_POSet(X0)))),
% 0.17/0.49 inference(resolution,[status(thm)],[f1073,f287])).
% 0.17/0.49 fof(f1088,plain,(
% 0.17/0.49 ~empty_set=empty_set),
% 0.17/0.49 inference(backward_demodulation,[status(thm)],[f1091,f577])).
% 0.17/0.49 fof(f1091,plain,(
% 0.17/0.49 ![X0]: (empty_set=bottom_of_relstr(boole_POSet(X0)))),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f1087,f213])).
% 0.17/0.49 fof(f1092,plain,(
% 0.17/0.49 $false),
% 0.17/0.49 inference(trivial_equality_resolution,[status(thm)],[f1088])).
% 0.17/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.52 % Elapsed time: 0.089095 seconds
% 0.17/0.52 % CPU time: 0.313847 seconds
% 0.17/0.52 % Total memory used: 78.659 MB
% 0.17/0.52 % Net memory used: 78.546 MB
%------------------------------------------------------------------------------