%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU348+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n004.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:48 PM UTC 2026
% Result : Theorem 19.28s 3.24s
% Output : Proof 19.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 5
% Syntax : Number of formulae : 63 ( 6 unt; 0 def)
% Number of atoms : 238 ( 15 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 265 ( 90 ~; 134 |; 27 &)
% ( 3 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 68 ( 0 sgn 33 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(poset_of_lattice(A)))
=> cast_to_el_of_lattice(A,B) = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_lattice3) ).
fof(f7_nnf,plain,
! [A] :
( ! [B] :
( cast_to_el_of_lattice(A,B) = B
| ~ element(B,the_carrier(poset_of_lattice(A))) )
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B] :
( cast_to_el_of_lattice(A,B) = B
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c14,plain,
( cast_to_el_of_lattice(X0,X1) = X1
| ~ element(X1,the_carrier(poset_of_lattice(X0)))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
fof(f57,conjecture,
! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(poset_of_lattice(B)))
=> ( relstr_element_smaller(poset_of_lattice(B),A,C)
<=> latt_set_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_lattice3) ).
fof(f57_neg,negated_conjecture,
~ ! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(poset_of_lattice(B)))
=> ( relstr_element_smaller(poset_of_lattice(B),A,C)
<=> latt_set_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) ),
inference(negated_conjecture,[status(cth)],[f57]) ).
fof(f57_nnf,plain,
? [A,B] :
( ? [C] :
( ( ( latt_set_smaller(B,cast_to_el_of_lattice(B,C),A)
& ~ relstr_element_smaller(poset_of_lattice(B),A,C) )
| ( ~ latt_set_smaller(B,cast_to_el_of_lattice(B,C),A)
& relstr_element_smaller(poset_of_lattice(B),A,C) ) )
& element(C,the_carrier(poset_of_lattice(B))) )
& latt_str(B)
& lattice(B)
& ~ empty_carrier(B) ),
inference(nnf_transformation,[status(thm)],[f57_neg]) ).
fof(f57_sk,plain,
( ( ( latt_set_smaller(sk17,cast_to_el_of_lattice(sk17,sk18),sk16)
& ~ relstr_element_smaller(poset_of_lattice(sk17),sk16,sk18) )
| ( ~ latt_set_smaller(sk17,cast_to_el_of_lattice(sk17,sk18),sk16)
& relstr_element_smaller(poset_of_lattice(sk17),sk16,sk18) ) )
& element(sk18,the_carrier(poset_of_lattice(sk17)))
& latt_str(sk17)
& lattice(sk17)
& ~ empty_carrier(sk17) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk16,sk17,sk18])],[f57_nnf]) ).
cnf(c100,plain,
lattice(sk17),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p148,plain,
( cast_to_el_of_lattice(sk17,X0) = X0
| ~ element(X0,the_carrier(poset_of_lattice(sk17)))
| ~ latt_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c14,c100]) ).
cnf(c101,plain,
latt_str(sk17),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p149,plain,
( cast_to_el_of_lattice(sk17,X0) = X0
| ~ element(X0,the_carrier(poset_of_lattice(sk17)))
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p148,c101]) ).
cnf(c102,plain,
element(sk18,the_carrier(poset_of_lattice(sk17))),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p150,plain,
( cast_to_el_of_lattice(sk17,sk18) = sk18
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p149,c102]) ).
fof(f15,axiom,
! [A,B] :
( ( element(B,the_carrier(poset_of_lattice(A)))
& latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> element(cast_to_el_of_lattice(A,B),the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattice3) ).
fof(f15_nnf,plain,
! [A,B] :
( element(cast_to_el_of_lattice(A,B),the_carrier(A))
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A,B] :
( element(cast_to_el_of_lattice(A,B),the_carrier(A))
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c31,plain,
( element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| ~ element(X1,the_carrier(poset_of_lattice(X0)))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p196,plain,
( element(cast_to_el_of_lattice(sk17,X0),the_carrier(sk17))
| ~ element(X0,the_carrier(poset_of_lattice(sk17)))
| ~ latt_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c31,c100]) ).
cnf(p204,plain,
( element(cast_to_el_of_lattice(sk17,X0),the_carrier(sk17))
| ~ element(X0,the_carrier(poset_of_lattice(sk17)))
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p196,c101]) ).
cnf(p208,plain,
( element(cast_to_el_of_lattice(sk17,sk18),the_carrier(sk17))
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p204,c102]) ).
cnf(p213,plain,
( element(sk18,the_carrier(sk17))
| empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(superposition,[status(thm)],[p150,p208]) ).
cnf(p219,plain,
( element(sk18,the_carrier(sk17))
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p213]) ).
fof(f6,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> cast_to_el_of_LattPOSet(A,B) = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_lattice3) ).
fof(f6_nnf,plain,
! [A] :
( ! [B] :
( cast_to_el_of_LattPOSet(A,B) = B
| ~ element(B,the_carrier(A)) )
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B] :
( cast_to_el_of_LattPOSet(A,B) = B
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c13,plain,
( cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ element(X1,the_carrier(X0))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p145,plain,
( cast_to_el_of_LattPOSet(sk17,X0) = X0
| ~ element(X0,the_carrier(sk17))
| ~ latt_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c13,c100]) ).
cnf(p146,plain,
( cast_to_el_of_LattPOSet(sk17,X0) = X0
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p145,c101]) ).
cnf(p220,plain,
( cast_to_el_of_LattPOSet(sk17,sk18) = sk18
| empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p219,p146]) ).
cnf(p222,plain,
( cast_to_el_of_LattPOSet(sk17,sk18) = sk18
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p220]) ).
fof(f56,axiom,
! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(B))
=> ( latt_set_smaller(B,C,A)
<=> relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_lattice3) ).
fof(f56_nnf,plain,
! [A,B] :
( ! [C] :
( ( ( ~ relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| latt_set_smaller(B,C,A) )
& ( relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| ~ latt_set_smaller(B,C,A) ) )
| ~ element(C,the_carrier(B)) )
| ~ latt_str(B)
| ~ lattice(B)
| empty_carrier(B) ),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
! [B,C,A] :
( ( ( ~ relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| latt_set_smaller(B,C,A) )
& ( relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| ~ latt_set_smaller(B,C,A) ) )
| ~ element(C,the_carrier(B))
| ~ latt_str(B)
| ~ lattice(B)
| empty_carrier(B) ),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c98,plain,
( ~ relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| latt_set_smaller(X1,X2,X0)
| ~ element(X2,the_carrier(X1))
| ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1) ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(p416,plain,
( ~ relstr_element_smaller(poset_of_lattice(sk17),X1,cast_to_el_of_LattPOSet(sk17,X0))
| latt_set_smaller(sk17,X0,X1)
| ~ element(X0,the_carrier(sk17))
| ~ latt_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c98,c100]) ).
cnf(p1301,plain,
( ~ relstr_element_smaller(poset_of_lattice(sk17),X1,cast_to_el_of_LattPOSet(sk17,X0))
| latt_set_smaller(sk17,X0,X1)
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p416,c101]) ).
cnf(p2783,plain,
( empty_carrier(sk17)
| ~ relstr_element_smaller(poset_of_lattice(sk17),X0,cast_to_el_of_LattPOSet(sk17,sk18))
| latt_set_smaller(sk17,sk18,X0)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p1301,p219]) ).
cnf(p2857,plain,
( ~ relstr_element_smaller(poset_of_lattice(sk17),X0,cast_to_el_of_LattPOSet(sk17,sk18))
| latt_set_smaller(sk17,sk18,X0)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2783]) ).
cnf(p2859,plain,
( ~ relstr_element_smaller(poset_of_lattice(sk17),X0,sk18)
| latt_set_smaller(sk17,sk18,X0)
| empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(superposition,[status(thm)],[p222,p2857]) ).
cnf(p2860,plain,
( ~ relstr_element_smaller(poset_of_lattice(sk17),X0,sk18)
| latt_set_smaller(sk17,sk18,X0)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2859]) ).
cnf(c104,plain,
( latt_set_smaller(sk17,cast_to_el_of_lattice(sk17,sk18),sk16)
| relstr_element_smaller(poset_of_lattice(sk17),sk16,sk18) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p153,plain,
( latt_set_smaller(sk17,sk18,sk16)
| relstr_element_smaller(poset_of_lattice(sk17),sk16,sk18)
| empty_carrier(sk17) ),
inference(superposition,[status(thm)],[p150,c104]) ).
cnf(p2861,plain,
( latt_set_smaller(sk17,sk18,sk16)
| empty_carrier(sk17)
| latt_set_smaller(sk17,sk18,sk16)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p2860,p153]) ).
cnf(p2863,plain,
( empty_carrier(sk17)
| latt_set_smaller(sk17,sk18,sk16)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2861]) ).
cnf(p2865,plain,
( latt_set_smaller(sk17,sk18,sk16)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2863]) ).
cnf(c97,plain,
( relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_set_smaller(X1,X2,X0)
| ~ element(X2,the_carrier(X1))
| ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1) ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(p411,plain,
( relstr_element_smaller(poset_of_lattice(sk17),X1,cast_to_el_of_LattPOSet(sk17,X0))
| ~ latt_set_smaller(sk17,X0,X1)
| ~ element(X0,the_carrier(sk17))
| ~ latt_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c97,c100]) ).
cnf(p1293,plain,
( relstr_element_smaller(poset_of_lattice(sk17),X1,cast_to_el_of_LattPOSet(sk17,X0))
| ~ latt_set_smaller(sk17,X0,X1)
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p411,c101]) ).
cnf(p2651,plain,
( empty_carrier(sk17)
| relstr_element_smaller(poset_of_lattice(sk17),X0,cast_to_el_of_LattPOSet(sk17,sk18))
| ~ latt_set_smaller(sk17,sk18,X0)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p1293,p219]) ).
cnf(p2725,plain,
( relstr_element_smaller(poset_of_lattice(sk17),X0,cast_to_el_of_LattPOSet(sk17,sk18))
| ~ latt_set_smaller(sk17,sk18,X0)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2651]) ).
cnf(p2868,plain,
( relstr_element_smaller(poset_of_lattice(sk17),sk16,cast_to_el_of_LattPOSet(sk17,sk18))
| empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p2865,p2725]) ).
cnf(p2875,plain,
( relstr_element_smaller(poset_of_lattice(sk17),sk16,cast_to_el_of_LattPOSet(sk17,sk18))
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2868]) ).
cnf(p2876,plain,
( relstr_element_smaller(poset_of_lattice(sk17),sk16,sk18)
| empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(superposition,[status(thm)],[p222,p2875]) ).
cnf(p2877,plain,
( relstr_element_smaller(poset_of_lattice(sk17),sk16,sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2876]) ).
cnf(c105,plain,
( ~ relstr_element_smaller(poset_of_lattice(sk17),sk16,sk18)
| ~ latt_set_smaller(sk17,cast_to_el_of_lattice(sk17,sk18),sk16) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p154,plain,
( ~ relstr_element_smaller(poset_of_lattice(sk17),sk16,sk18)
| ~ latt_set_smaller(sk17,sk18,sk16)
| empty_carrier(sk17) ),
inference(superposition,[status(thm)],[p150,c105]) ).
cnf(p2866,plain,
( ~ relstr_element_smaller(poset_of_lattice(sk17),sk16,sk18)
| empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p2865,p154]) ).
cnf(p2869,plain,
( ~ relstr_element_smaller(poset_of_lattice(sk17),sk16,sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2866]) ).
cnf(p2878,plain,
( empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p2877,p2869]) ).
cnf(p2879,plain,
empty_carrier(sk17),
inference(factoring,[status(thm)],[p2878]) ).
cnf(c99,plain,
~ empty_carrier(sk17),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p2880,plain,
$false,
inference(resolution,[status(thm)],[p2879,c99]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU348+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.40 % Computer : n004.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Thu Sep 24 13:47:36 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 19.28/3.24 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.28/3.24 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------