%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU344+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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 : Fri Sep 25 02:51:47 PM UTC 2026
% Result : Theorem 56.32s 7.68s
% Output : Proof 56.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 7
% Syntax : Number of formulae : 50 ( 11 unt; 0 def)
% Number of atoms : 143 ( 19 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 142 ( 49 ~; 61 |; 20 &)
% ( 3 <=>; 9 =>; 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 : 61 ( 4 sgn 36 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [A] :
( latt_str(A)
=> ( join_semilatt_str(A)
& meet_semilatt_str(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f29_nnf,plain,
! [A] :
( ( join_semilatt_str(A)
& meet_semilatt_str(A) )
| ~ latt_str(A) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [A] :
( ( join_semilatt_str(A)
& meet_semilatt_str(A) )
| ~ latt_str(A) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c33,plain,
( join_semilatt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
fof(f14,axiom,
! [A] :
( latt_str(boole_lattice(A))
& strict_latt_str(boole_lattice(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice3) ).
fof(f14_nnf,plain,
! [A] :
( latt_str(boole_lattice(A))
& strict_latt_str(boole_lattice(A)) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [A] :
( latt_str(boole_lattice(A))
& strict_latt_str(boole_lattice(A)) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c17,plain,
latt_str(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p150,plain,
join_semilatt_str(boole_lattice(X0)),
inference(resolution,[status(thm)],[c33,c17]) ).
fof(f9,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/sandbox/benchmark/theBenchmark.p',d3_lattices) ).
fof(f9_nnf,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)],[f9]) ).
fof(f9_sk,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(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c10,plain,
( 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(esa)],[f9_sk]) ).
cnf(p167,plain,
( 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)))
| empty_carrier(boole_lattice(X0)) ),
inference(resolution,[status(thm)],[p150,c10]) ).
fof(f72,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/sandbox/benchmark/theBenchmark.p',t2_lattice3) ).
fof(f72_neg,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)],[f72]) ).
fof(f72_nnf,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)],[f72_neg]) ).
fof(f72_sk,plain,
( ( ( subset(sk16,sk17)
& ~ below(boole_lattice(sk15),sk16,sk17) )
| ( ~ subset(sk16,sk17)
& below(boole_lattice(sk15),sk16,sk17) ) )
& element(sk17,the_carrier(boole_lattice(sk15)))
& element(sk16,the_carrier(boole_lattice(sk15))) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15,sk16,sk17])],[f72_nnf]) ).
cnf(c93,plain,
element(sk16,the_carrier(boole_lattice(sk15))),
inference(cnf_transformation,[status(esa)],[f72_sk]) ).
cnf(p734,plain,
( join(boole_lattice(sk15),sk16,X0) != X0
| below(boole_lattice(sk15),sk16,X0)
| ~ element(X0,the_carrier(boole_lattice(sk15)))
| empty_carrier(boole_lattice(sk15)) ),
inference(resolution,[status(thm)],[p167,c93]) ).
cnf(c94,plain,
element(sk17,the_carrier(boole_lattice(sk15))),
inference(cnf_transformation,[status(esa)],[f72_sk]) ).
cnf(p5888,plain,
( set_union2(sk16,sk17) != sk17
| below(boole_lattice(sk15),sk16,sk17)
| empty_carrier(boole_lattice(sk15)) ),
inference(resolution,[status(thm)],[p734,c94]) ).
cnf(c9,plain,
( 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(esa)],[f9_sk]) ).
cnf(p166,plain,
( 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)))
| empty_carrier(boole_lattice(X0)) ),
inference(resolution,[status(thm)],[p150,c9]) ).
cnf(p723,plain,
( join(boole_lattice(sk15),sk16,X0) = X0
| ~ below(boole_lattice(sk15),sk16,X0)
| ~ element(X0,the_carrier(boole_lattice(sk15)))
| empty_carrier(boole_lattice(sk15)) ),
inference(resolution,[status(thm)],[p166,c93]) ).
cnf(p726,plain,
( set_union2(sk16,sk17) = sk17
| ~ below(boole_lattice(sk15),sk16,sk17)
| empty_carrier(boole_lattice(sk15)) ),
inference(resolution,[status(thm)],[p723,c94]) ).
cnf(c96,plain,
( subset(sk16,sk17)
| below(boole_lattice(sk15),sk16,sk17) ),
inference(cnf_transformation,[status(esa)],[f72_sk]) ).
cnf(p728,plain,
( subset(sk16,sk17)
| set_union2(sk16,sk17) = sk17
| empty_carrier(boole_lattice(sk15)) ),
inference(resolution,[status(thm)],[p726,c96]) ).
fof(f79,axiom,
! [A,B] : subset(A,set_union2(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_xboole_1) ).
fof(f79_nnf,plain,
! [A,B] : subset(A,set_union2(A,B)),
inference(nnf_transformation,[status(thm)],[f79]) ).
fof(f79_sk,plain,
! [A,B] : subset(A,set_union2(A,B)),
inference(skolemisation,[status(esa)],[f79_nnf]) ).
cnf(c106,plain,
subset(X0,set_union2(X0,X1)),
inference(cnf_transformation,[status(esa)],[f79_sk]) ).
cnf(p730,plain,
( subset(sk16,sk17)
| subset(sk16,sk17)
| empty_carrier(boole_lattice(sk15)) ),
inference(superposition,[status(thm)],[p728,c106]) ).
cnf(p733,plain,
( subset(sk16,sk17)
| empty_carrier(boole_lattice(sk15)) ),
inference(factoring,[status(thm)],[p730]) ).
fof(f67,axiom,
! [A,B] :
( subset(A,B)
=> set_union2(A,B) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_xboole_1) ).
fof(f67_nnf,plain,
! [A,B] :
( set_union2(A,B) = B
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [A,B] :
( set_union2(A,B) = B
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c87,plain,
( set_union2(X0,X1) = X1
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(p739,plain,
( set_union2(sk16,sk17) = sk17
| empty_carrier(boole_lattice(sk15)) ),
inference(resolution,[status(thm)],[p733,c87]) ).
cnf(p5989,plain,
( empty_carrier(boole_lattice(sk15))
| below(boole_lattice(sk15),sk16,sk17)
| empty_carrier(boole_lattice(sk15)) ),
inference(resolution,[status(thm)],[p5888,p739]) ).
cnf(p5990,plain,
( below(boole_lattice(sk15),sk16,sk17)
| empty_carrier(boole_lattice(sk15)) ),
inference(factoring,[status(thm)],[p5989]) ).
cnf(c97,plain,
( ~ below(boole_lattice(sk15),sk16,sk17)
| ~ subset(sk16,sk17) ),
inference(cnf_transformation,[status(esa)],[f72_sk]) ).
cnf(p737,plain,
( ~ below(boole_lattice(sk15),sk16,sk17)
| empty_carrier(boole_lattice(sk15)) ),
inference(resolution,[status(thm)],[p733,c97]) ).
cnf(p5991,plain,
( empty_carrier(boole_lattice(sk15))
| empty_carrier(boole_lattice(sk15)) ),
inference(resolution,[status(thm)],[p5990,p737]) ).
cnf(p5992,plain,
empty_carrier(boole_lattice(sk15)),
inference(factoring,[status(thm)],[p5991]) ).
fof(f43,axiom,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice3) ).
fof(f43_nnf,plain,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c51,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p5995,plain,
$false,
inference(resolution,[status(thm)],[p5992,c51]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU344+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.37 % Computer : n009.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Thu Sep 24 13:46:58 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 56.32/7.68 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.32/7.68 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------