%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU371+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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 : Sun Sep 27 08:46:07 AM UTC 2026
% Result : Theorem 4.99s 1.19s
% Output : CNFRefutation 4.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 9
% Syntax : Number of formulae : 43 ( 17 unt; 0 def)
% Number of atoms : 127 ( 35 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 127 ( 43 ~; 45 |; 35 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 25 ( 23 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 2 con; 0-2 aty)
% Number of variables : 46 ( 7 sgn 11 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d11_yellow_0,axiom,
! [A] :
( rel_str(A)
=> bottom_of_relstr(A) = join_on_relstr(A,empty_set) ),
file('theBenchmark.p',d11_yellow_0) ).
fof(d2_yellow_1,axiom,
! [A] : boole_POSet(A) = poset_of_lattice(boole_lattice(A)),
file('theBenchmark.p',d2_yellow_1) ).
fof(dt_k1_lattice3,axiom,
! [A] :
( latt_str(boole_lattice(A))
& strict_latt_str(boole_lattice(A)) ),
file('theBenchmark.p',dt_k1_lattice3) ).
fof(dt_k3_lattice3,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ( rel_str(poset_of_lattice(A))
& antisymmetric_relstr(poset_of_lattice(A))
& transitive_relstr(poset_of_lattice(A))
& reflexive_relstr(poset_of_lattice(A))
& strict_rel_str(poset_of_lattice(A)) ) ),
file('theBenchmark.p',dt_k3_lattice3) ).
fof(fc1_knaster,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('theBenchmark.p',fc1_knaster) ).
fof(t29_yellow_0,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('theBenchmark.p',t29_yellow_0) ).
fof(t3_lattice3,axiom,
! [A] :
( bottom_of_semilattstr(boole_lattice(A)) = empty_set
& lower_bounded_semilattstr(boole_lattice(A)) ),
file('theBenchmark.p',t3_lattice3) ).
fof(t50_lattice3,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('theBenchmark.p',t50_lattice3) ).
fof(t18_yellow_1,conjecture,
! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set,
file('theBenchmark.p',t18_yellow_1) ).
fof(t18_yellow_1_neg,negated_conjecture,
~ ! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set,
inference(assume_negation,[status(cth)],[t18_yellow_1]) ).
cnf(c_116,plain,
( join_on_relstr(A,empty_set) = bottom_of_relstr(A)
| ~ rel_str(A) ),
inference(clausify,[status(thm)],[d11_yellow_0]) ).
cnf(c_128,plain,
( rel_str(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[dt_k3_lattice3]) ).
cnf(c_146,plain,
( 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(clausify,[status(thm)],[t29_yellow_0]) ).
cnf(c_149,plain,
( bottom_of_semilattstr(A) = join_of_latt_set(A,empty_set)
| ~ latt_str(A)
| ~ complete_latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[t50_lattice3]) ).
cnf(c_152,plain,
( join_on_relstr(poset_of_lattice(A),empty_set) = bottom_of_relstr(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(resolve,[status(thm)],[c_128,c_116]) ).
cnf(c_228,plain,
latt_str(boole_lattice(A)),
inference(clausify,[status(thm)],[dt_k1_lattice3]) ).
cnf(c_847,plain,
( join_on_relstr(poset_of_lattice(boole_lattice(A)),empty_set) = bottom_of_relstr(poset_of_lattice(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_228,c_152]) ).
cnf(c_850,plain,
( bottom_of_semilattstr(boole_lattice(A)) = join_of_latt_set(boole_lattice(A),empty_set)
| ~ complete_latt_str(boole_lattice(A))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_228,c_149]) ).
cnf(c_851,plain,
( join_of_latt_set(boole_lattice(A),empty_set) = bottom_of_semilattstr(boole_lattice(A))
| ~ complete_latt_str(boole_lattice(A))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(copy,[status(thm)],[c_850]) ).
cnf(c_854,plain,
( join_of_latt_set(boole_lattice(A),B) = join_on_relstr(poset_of_lattice(boole_lattice(A)),B)
| ~ complete_latt_str(boole_lattice(A))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_228,c_146]) ).
cnf(c_855,plain,
( join_on_relstr(poset_of_lattice(boole_lattice(A)),B) = join_of_latt_set(boole_lattice(A),B)
| ~ complete_latt_str(boole_lattice(A))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(copy,[status(thm)],[c_854]) ).
cnf(c_1190,plain,
boole_POSet(A) = poset_of_lattice(boole_lattice(A)),
inference(clausify,[status(thm)],[d2_yellow_1]) ).
cnf(c_1198,plain,
~ empty_carrier(boole_lattice(A)),
inference(clausify,[status(thm)],[fc1_knaster]) ).
cnf(c_1205,plain,
lattice(boole_lattice(A)),
inference(clausify,[status(thm)],[fc1_knaster]) ).
cnf(c_1212,plain,
complete_latt_str(boole_lattice(A)),
inference(clausify,[status(thm)],[fc1_knaster]) ).
cnf(c_1356,plain,
bottom_of_semilattstr(boole_lattice(A)) = empty_set,
inference(clausify,[status(thm)],[t3_lattice3]) ).
fof(nnf_114,plain,
? [A] : bottom_of_relstr(boole_POSet(A)) != empty_set,
inference(fof_nnf,[status(thm)],[t18_yellow_1_neg]) ).
fof(sk_t18_yellow_1_neg,plain,
bottom_of_relstr(boole_POSet(sK0)) != empty_set,
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_114]) ).
cnf(c_1362,negated_conjecture,
bottom_of_relstr(boole_POSet(sK0)) != empty_set,
inference(split_conjunct,[status(thm)],[sk_t18_yellow_1_neg]) ).
cnf(c_1363,negated_conjecture,
bottom_of_relstr(poset_of_lattice(boole_lattice(sK0))) != empty_set,
inference(paramod,[status(thm)],[c_1190,c_1362]) ).
cnf(c_1900,plain,
( join_on_relstr(poset_of_lattice(boole_lattice(A)),B) = join_of_latt_set(boole_lattice(A),B)
| ~ complete_latt_str(boole_lattice(A))
| ~ lattice(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_1198,c_855]) ).
cnf(c_1901,plain,
( join_on_relstr(poset_of_lattice(boole_lattice(A)),B) = join_of_latt_set(boole_lattice(A),B)
| ~ complete_latt_str(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_1205,c_1900]) ).
cnf(c_1893,plain,
join_on_relstr(poset_of_lattice(boole_lattice(A)),B) = join_of_latt_set(boole_lattice(A),B),
inference(resolve,[status(thm)],[c_1212,c_1901]) ).
cnf(c_1902,plain,
( join_of_latt_set(boole_lattice(A),empty_set) = empty_set
| ~ complete_latt_str(boole_lattice(A))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(paramod,[status(thm)],[c_1356,c_851]) ).
cnf(c_1903,plain,
( join_of_latt_set(boole_lattice(A),empty_set) = empty_set
| ~ complete_latt_str(boole_lattice(A))
| ~ lattice(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_1198,c_1902]) ).
cnf(c_1904,plain,
( join_of_latt_set(boole_lattice(A),empty_set) = empty_set
| ~ complete_latt_str(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_1205,c_1903]) ).
cnf(c_1895,plain,
join_of_latt_set(boole_lattice(A),empty_set) = empty_set,
inference(resolve,[status(thm)],[c_1212,c_1904]) ).
cnf(c_1905,plain,
( join_of_latt_set(boole_lattice(A),empty_set) = bottom_of_relstr(poset_of_lattice(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(paramod,[status(thm)],[c_1893,c_847]) ).
cnf(c_1906,plain,
( empty_set = bottom_of_relstr(poset_of_lattice(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(paramod,[status(thm)],[c_1895,c_1905]) ).
cnf(c_1907,plain,
( bottom_of_relstr(poset_of_lattice(boole_lattice(A))) = empty_set
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(copy,[status(thm)],[c_1906]) ).
cnf(c_1908,plain,
( bottom_of_relstr(poset_of_lattice(boole_lattice(A))) = empty_set
| ~ lattice(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_1198,c_1907]) ).
cnf(c_1898,plain,
bottom_of_relstr(poset_of_lattice(boole_lattice(A))) = empty_set,
inference(resolve,[status(thm)],[c_1205,c_1908]) ).
cnf(c_1899,plain,
$false,
inference(resolve,[status(thm)],[c_1898,c_1363]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU371+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n008.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 : Sat Sep 26 09:21:54 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 3296398 was started by sandbox2 on n008,
% 0.09/0.37 % Sat Sep 26 09:21:54 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.40
% 0.09/0.40 % From the command line: assign(max_seconds, 300).
% 4.99/1.19
% 4.99/1.19 % SZS status Theorem for theBenchmark
% 4.99/1.19
% 4.99/1.19 % Proof 1 at 0.75 (+ 0.03) seconds.
% 4.99/1.19 % Length of proof is 31.
% 4.99/1.19 % Level of proof is 6.
% 4.99/1.19 % Maximum clause weight is 39.000.
% 4.99/1.19 % Given clauses 0.
% 4.99/1.19
% 4.99/1.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------