%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU304+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 : n003.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:45:45 AM UTC 2026
% Result : Theorem 1.62s 0.70s
% Output : CNFRefutation 1.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 7
% Syntax : Number of formulae : 60 ( 21 unt; 0 def)
% Number of atoms : 192 ( 37 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 215 ( 83 ~; 82 |; 32 &)
% ( 2 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 77 ( 0 sgn 22 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k4_lattices,axiom,
! [A,B,C] :
( ( element(C,the_carrier(A))
& element(B,the_carrier(A))
& meet_semilatt_str(A)
& meet_commutative(A)
& ~ empty_carrier(A) )
=> meet_commut(A,B,C) = meet_commut(A,C,B) ),
file('theBenchmark.p',commutativity_k4_lattices) ).
fof(d3_lattices,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('theBenchmark.p',d3_lattices) ).
fof(d8_lattices,axiom,
! [A] :
( ( latt_str(A)
& ~ empty_carrier(A) )
=> ( meet_absorbing(A)
<=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> join(A,meet(A,B,C),C) = C ) ) ) ),
file('theBenchmark.p',d8_lattices) ).
fof(dt_k2_lattices,axiom,
! [A,B,C] :
( ( element(C,the_carrier(A))
& element(B,the_carrier(A))
& meet_semilatt_str(A)
& ~ empty_carrier(A) )
=> element(meet(A,B,C),the_carrier(A)) ),
file('theBenchmark.p',dt_k2_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( latt_str(A)
=> ( join_semilatt_str(A)
& meet_semilatt_str(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(redefinition_k4_lattices,axiom,
! [A,B,C] :
( ( element(C,the_carrier(A))
& element(B,the_carrier(A))
& meet_semilatt_str(A)
& meet_commutative(A)
& ~ empty_carrier(A) )
=> meet_commut(A,B,C) = meet(A,B,C) ),
file('theBenchmark.p',redefinition_k4_lattices) ).
fof(t23_lattices,conjecture,
! [A] :
( ( latt_str(A)
& meet_absorbing(A)
& meet_commutative(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> below(A,meet_commut(A,B,C),B) ) ) ),
file('theBenchmark.p',t23_lattices) ).
fof(t23_lattices_neg,negated_conjecture,
~ ! [A] :
( ( latt_str(A)
& meet_absorbing(A)
& meet_commutative(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> below(A,meet_commut(A,B,C),B) ) ) ),
inference(assume_negation,[status(cth)],[t23_lattices]) ).
cnf(c_55,plain,
( meet(A,B,C) = meet_commut(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ meet_semilatt_str(A)
| ~ meet_commutative(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[redefinition_k4_lattices]) ).
fof(nnf_50,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ below(A,meet_commut(A,B,C),B)
& element(C,the_carrier(A)) )
& element(B,the_carrier(A)) )
& latt_str(A)
& meet_absorbing(A)
& meet_commutative(A)
& ~ empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[t23_lattices_neg]) ).
fof(sk_t23_lattices_neg,plain,
( ~ below(sK0,meet_commut(sK0,sK1,sK2),sK1)
& element(sK2,the_carrier(sK0))
& element(sK1,the_carrier(sK0))
& latt_str(sK0)
& meet_absorbing(sK0)
& meet_commutative(sK0)
& ~ empty_carrier(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2)],[nnf_50]) ).
cnf(c_56,negated_conjecture,
meet_commutative(sK0),
inference(split_conjunct,[status(thm)],[sk_t23_lattices_neg]) ).
cnf(c_58,plain,
( meet_commut(A,C,B) = meet_commut(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ meet_semilatt_str(A)
| ~ meet_commutative(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[commutativity_k4_lattices]) ).
cnf(c_59,plain,
( join_semilatt_str(A)
| ~ latt_str(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_62,plain,
( 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(clausify,[status(thm)],[d3_lattices]) ).
cnf(c_69,negated_conjecture,
latt_str(sK0),
inference(split_conjunct,[status(thm)],[sk_t23_lattices_neg]) ).
cnf(c_72,plain,
( join(A,B,C) != C
| below(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| empty_carrier(A)
| ~ latt_str(A) ),
inference(resolve,[status(thm)],[c_59,c_62]) ).
cnf(c_79,plain,
( meet_semilatt_str(A)
| ~ latt_str(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_83,plain,
( join(A,meet(A,B,C),C) = C
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ meet_absorbing(A)
| ~ latt_str(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[d8_lattices]) ).
cnf(c_129,negated_conjecture,
( join(sK0,meet(sK0,A,B),B) = B
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| ~ meet_absorbing(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_83,c_69]) ).
cnf(c_137,negated_conjecture,
meet_semilatt_str(sK0),
inference(resolve,[status(thm)],[c_79,c_69]) ).
cnf(c_147,negated_conjecture,
( join(sK0,A,B) != B
| below(sK0,A,B)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_69,c_72]) ).
cnf(c_149,negated_conjecture,
( meet_commut(sK0,B,A) = meet_commut(sK0,A,B)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| ~ meet_semilatt_str(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_58,c_56]) ).
cnf(c_150,negated_conjecture,
( meet_commut(sK0,B,A) = meet_commut(sK0,A,B)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_137,c_149]) ).
cnf(c_153,negated_conjecture,
( meet(sK0,A,B) = meet_commut(sK0,A,B)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| ~ meet_semilatt_str(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_55,c_56]) ).
cnf(c_900,negated_conjecture,
( meet_commut(sK0,A,B) = meet(sK0,A,B)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| ~ meet_semilatt_str(sK0)
| empty_carrier(sK0) ),
inference(copy,[status(thm)],[c_153]) ).
cnf(c_154,negated_conjecture,
( meet_commut(sK0,A,B) = meet(sK0,A,B)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_137,c_900]) ).
cnf(c_158,plain,
( element(meet(A,B,C),the_carrier(A))
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ meet_semilatt_str(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[dt_k2_lattices]) ).
cnf(c_172,negated_conjecture,
~ empty_carrier(sK0),
inference(split_conjunct,[status(thm)],[sk_t23_lattices_neg]) ).
cnf(c_173,negated_conjecture,
meet_absorbing(sK0),
inference(split_conjunct,[status(thm)],[sk_t23_lattices_neg]) ).
cnf(c_174,negated_conjecture,
element(sK1,the_carrier(sK0)),
inference(split_conjunct,[status(thm)],[sk_t23_lattices_neg]) ).
cnf(c_175,negated_conjecture,
element(sK2,the_carrier(sK0)),
inference(split_conjunct,[status(thm)],[sk_t23_lattices_neg]) ).
cnf(c_176,negated_conjecture,
~ below(sK0,meet_commut(sK0,sK1,sK2),sK1),
inference(split_conjunct,[status(thm)],[sk_t23_lattices_neg]) ).
cnf(c_223,negated_conjecture,
( meet_commut(sK0,A,B) = meet(sK0,A,B)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_172,c_154]) ).
cnf(c_225,negated_conjecture,
( meet_commut(sK0,B,A) = meet_commut(sK0,A,B)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_172,c_150]) ).
cnf(c_227,negated_conjecture,
( join(sK0,A,B) != B
| below(sK0,A,B)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_172,c_147]) ).
cnf(c_901,negated_conjecture,
( join(sK0,meet(sK0,A,B),B) = B
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| ~ meet_absorbing(sK0) ),
inference(resolve,[status(thm)],[c_172,c_129]) ).
cnf(c_230,negated_conjecture,
( join(sK0,meet(sK0,A,B),B) = B
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_173,c_901]) ).
cnf(c_902,negated_conjecture,
( element(meet(sK0,A,B),the_carrier(sK0))
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_158,c_137]) ).
cnf(c_903,negated_conjecture,
( element(meet(sK0,sK1,A),the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_902,c_174]) ).
cnf(c_904,negated_conjecture,
( element(meet(sK0,sK1,sK2),the_carrier(sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_903,c_175]) ).
cnf(c_356,negated_conjecture,
element(meet(sK0,sK1,sK2),the_carrier(sK0)),
inference(resolve,[status(thm)],[c_172,c_904]) ).
cnf(c_905,negated_conjecture,
( meet_commut(sK0,sK2,A) = meet(sK0,sK2,A)
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_223,c_175]) ).
cnf(c_471,negated_conjecture,
meet_commut(sK0,sK2,sK1) = meet(sK0,sK2,sK1),
inference(resolve,[status(thm)],[c_905,c_174]) ).
cnf(c_906,negated_conjecture,
( meet_commut(sK0,sK1,A) = meet(sK0,sK1,A)
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_223,c_174]) ).
cnf(c_473,negated_conjecture,
meet_commut(sK0,sK1,sK2) = meet(sK0,sK1,sK2),
inference(resolve,[status(thm)],[c_906,c_175]) ).
cnf(c_477,negated_conjecture,
~ below(sK0,meet(sK0,sK1,sK2),sK1),
inference(paramod,[status(thm)],[c_473,c_176]) ).
cnf(c_907,negated_conjecture,
( meet_commut(sK0,A,sK2) = meet_commut(sK0,sK2,A)
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_225,c_175]) ).
cnf(c_908,negated_conjecture,
meet_commut(sK0,sK1,sK2) = meet_commut(sK0,sK2,sK1),
inference(resolve,[status(thm)],[c_907,c_174]) ).
cnf(c_909,negated_conjecture,
meet(sK0,sK1,sK2) = meet_commut(sK0,sK2,sK1),
inference(paramod,[status(thm)],[c_473,c_908]) ).
cnf(c_910,negated_conjecture,
meet(sK0,sK1,sK2) = meet(sK0,sK2,sK1),
inference(paramod,[status(thm)],[c_471,c_909]) ).
cnf(c_487,negated_conjecture,
meet(sK0,sK2,sK1) = meet(sK0,sK1,sK2),
inference(copy,[status(thm)],[c_910]) ).
cnf(c_911,negated_conjecture,
( join(sK0,meet(sK0,sK2,A),A) = A
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_230,c_175]) ).
cnf(c_912,negated_conjecture,
join(sK0,meet(sK0,sK2,sK1),sK1) = sK1,
inference(resolve,[status(thm)],[c_911,c_174]) ).
cnf(c_538,negated_conjecture,
join(sK0,meet(sK0,sK1,sK2),sK1) = sK1,
inference(paramod,[status(thm)],[c_487,c_912]) ).
cnf(c_913,negated_conjecture,
( join(sK0,meet(sK0,sK1,sK2),A) != A
| below(sK0,meet(sK0,sK1,sK2),A)
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_227,c_356]) ).
cnf(c_914,negated_conjecture,
( join(sK0,meet(sK0,sK1,sK2),sK1) != sK1
| below(sK0,meet(sK0,sK1,sK2),sK1) ),
inference(resolve,[status(thm)],[c_913,c_174]) ).
cnf(c_915,negated_conjecture,
join(sK0,meet(sK0,sK1,sK2),sK1) != sK1,
inference(resolve,[status(thm)],[c_914,c_477]) ).
cnf(c_916,negated_conjecture,
sK1 != sK1,
inference(paramod,[status(thm)],[c_538,c_915]) ).
cnf(c_899,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_916]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU304+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n003.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sat Sep 26 09:10:38 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.46 % Process 2524445 was started by sandbox2 on n003,
% 0.18/0.46 % Sat Sep 26 09:10:38 2026
% 0.18/0.46 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.48
% 0.18/0.48 % From the command line: assign(max_seconds, 300).
% 1.62/0.70
% 1.62/0.70 % SZS status Theorem for theBenchmark
% 1.62/0.70
% 1.62/0.70 % Proof 1 at 0.17 (+ 0.04) seconds.
% 1.62/0.70 % Length of proof is 40.
% 1.62/0.70 % Level of proof is 8.
% 1.62/0.70 % Maximum clause weight is 36.000.
% 1.62/0.70 % Given clauses 148.
% 1.62/0.70
% 1.62/0.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------