%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU350+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 : 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:48 PM UTC 2026
% Result : Theorem 16.12s 2.71s
% Output : Proof 16.12s
% 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(f58,conjecture,
! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(poset_of_lattice(B)))
=> ( relstr_set_smaller(poset_of_lattice(B),A,C)
<=> latt_element_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_lattice3) ).
fof(f58_neg,negated_conjecture,
~ ! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(poset_of_lattice(B)))
=> ( relstr_set_smaller(poset_of_lattice(B),A,C)
<=> latt_element_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) ),
inference(negated_conjecture,[status(cth)],[f58]) ).
fof(f58_nnf,plain,
? [A,B] :
( ? [C] :
( ( ( latt_element_smaller(B,cast_to_el_of_lattice(B,C),A)
& ~ relstr_set_smaller(poset_of_lattice(B),A,C) )
| ( ~ latt_element_smaller(B,cast_to_el_of_lattice(B,C),A)
& relstr_set_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)],[f58_neg]) ).
fof(f58_sk,plain,
( ( ( latt_element_smaller(sk17,cast_to_el_of_lattice(sk17,sk18),sk16)
& ~ relstr_set_smaller(poset_of_lattice(sk17),sk16,sk18) )
| ( ~ latt_element_smaller(sk17,cast_to_el_of_lattice(sk17,sk18),sk16)
& relstr_set_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])],[f58_nnf]) ).
cnf(c101,plain,
lattice(sk17),
inference(cnf_transformation,[status(esa)],[f58_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,c101]) ).
cnf(c102,plain,
latt_str(sk17),
inference(cnf_transformation,[status(esa)],[f58_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,c102]) ).
cnf(c103,plain,
element(sk18,the_carrier(poset_of_lattice(sk17))),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(p150,plain,
( cast_to_el_of_lattice(sk17,sk18) = sk18
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p149,c103]) ).
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,c101]) ).
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,c102]) ).
cnf(p208,plain,
( element(cast_to_el_of_lattice(sk17,sk18),the_carrier(sk17))
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p204,c103]) ).
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,c101]) ).
cnf(p146,plain,
( cast_to_el_of_LattPOSet(sk17,X0) = X0
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p145,c102]) ).
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(f57,axiom,
! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(B))
=> ( latt_element_smaller(B,C,A)
<=> relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_lattice3) ).
fof(f57_nnf,plain,
! [A,B] :
( ! [C] :
( ( ( ~ relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| latt_element_smaller(B,C,A) )
& ( relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| ~ latt_element_smaller(B,C,A) ) )
| ~ element(C,the_carrier(B)) )
| ~ latt_str(B)
| ~ lattice(B)
| empty_carrier(B) ),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
! [B,C,A] :
( ( ( ~ relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| latt_element_smaller(B,C,A) )
& ( relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| ~ latt_element_smaller(B,C,A) ) )
| ~ element(C,the_carrier(B))
| ~ latt_str(B)
| ~ lattice(B)
| empty_carrier(B) ),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c99,plain,
( ~ relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| latt_element_smaller(X1,X2,X0)
| ~ element(X2,the_carrier(X1))
| ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p451,plain,
( ~ relstr_set_smaller(poset_of_lattice(sk17),X1,cast_to_el_of_LattPOSet(sk17,X0))
| latt_element_smaller(sk17,X0,X1)
| ~ element(X0,the_carrier(sk17))
| ~ latt_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c99,c101]) ).
cnf(p1405,plain,
( ~ relstr_set_smaller(poset_of_lattice(sk17),X1,cast_to_el_of_LattPOSet(sk17,X0))
| latt_element_smaller(sk17,X0,X1)
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p451,c102]) ).
cnf(p2813,plain,
( empty_carrier(sk17)
| ~ relstr_set_smaller(poset_of_lattice(sk17),X0,cast_to_el_of_LattPOSet(sk17,sk18))
| latt_element_smaller(sk17,sk18,X0)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p1405,p219]) ).
cnf(p2888,plain,
( ~ relstr_set_smaller(poset_of_lattice(sk17),X0,cast_to_el_of_LattPOSet(sk17,sk18))
| latt_element_smaller(sk17,sk18,X0)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2813]) ).
cnf(p2889,plain,
( ~ relstr_set_smaller(poset_of_lattice(sk17),X0,sk18)
| latt_element_smaller(sk17,sk18,X0)
| empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(superposition,[status(thm)],[p222,p2888]) ).
cnf(p2892,plain,
( ~ relstr_set_smaller(poset_of_lattice(sk17),X0,sk18)
| latt_element_smaller(sk17,sk18,X0)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2889]) ).
cnf(c105,plain,
( latt_element_smaller(sk17,cast_to_el_of_lattice(sk17,sk18),sk16)
| relstr_set_smaller(poset_of_lattice(sk17),sk16,sk18) ),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(p152,plain,
( latt_element_smaller(sk17,sk18,sk16)
| relstr_set_smaller(poset_of_lattice(sk17),sk16,sk18)
| empty_carrier(sk17) ),
inference(superposition,[status(thm)],[p150,c105]) ).
cnf(p2893,plain,
( latt_element_smaller(sk17,sk18,sk16)
| empty_carrier(sk17)
| latt_element_smaller(sk17,sk18,sk16)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p2892,p152]) ).
cnf(p2895,plain,
( empty_carrier(sk17)
| latt_element_smaller(sk17,sk18,sk16)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2893]) ).
cnf(p2896,plain,
( latt_element_smaller(sk17,sk18,sk16)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2895]) ).
cnf(c98,plain,
( relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_element_smaller(X1,X2,X0)
| ~ element(X2,the_carrier(X1))
| ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p448,plain,
( relstr_set_smaller(poset_of_lattice(sk17),X1,cast_to_el_of_LattPOSet(sk17,X0))
| ~ latt_element_smaller(sk17,X0,X1)
| ~ element(X0,the_carrier(sk17))
| ~ latt_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c98,c101]) ).
cnf(p1395,plain,
( relstr_set_smaller(poset_of_lattice(sk17),X1,cast_to_el_of_LattPOSet(sk17,X0))
| ~ latt_element_smaller(sk17,X0,X1)
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p448,c102]) ).
cnf(p2732,plain,
( empty_carrier(sk17)
| relstr_set_smaller(poset_of_lattice(sk17),X0,cast_to_el_of_LattPOSet(sk17,sk18))
| ~ latt_element_smaller(sk17,sk18,X0)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p1395,p219]) ).
cnf(p2808,plain,
( relstr_set_smaller(poset_of_lattice(sk17),X0,cast_to_el_of_LattPOSet(sk17,sk18))
| ~ latt_element_smaller(sk17,sk18,X0)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2732]) ).
cnf(p2899,plain,
( relstr_set_smaller(poset_of_lattice(sk17),sk16,cast_to_el_of_LattPOSet(sk17,sk18))
| empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p2896,p2808]) ).
cnf(p2905,plain,
( relstr_set_smaller(poset_of_lattice(sk17),sk16,cast_to_el_of_LattPOSet(sk17,sk18))
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2899]) ).
cnf(p2907,plain,
( relstr_set_smaller(poset_of_lattice(sk17),sk16,sk18)
| empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(superposition,[status(thm)],[p222,p2905]) ).
cnf(p2908,plain,
( relstr_set_smaller(poset_of_lattice(sk17),sk16,sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2907]) ).
cnf(c106,plain,
( ~ relstr_set_smaller(poset_of_lattice(sk17),sk16,sk18)
| ~ latt_element_smaller(sk17,cast_to_el_of_lattice(sk17,sk18),sk16) ),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(p153,plain,
( ~ relstr_set_smaller(poset_of_lattice(sk17),sk16,sk18)
| ~ latt_element_smaller(sk17,sk18,sk16)
| empty_carrier(sk17) ),
inference(superposition,[status(thm)],[p150,c106]) ).
cnf(p2897,plain,
( ~ relstr_set_smaller(poset_of_lattice(sk17),sk16,sk18)
| empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p2896,p153]) ).
cnf(p2900,plain,
( ~ relstr_set_smaller(poset_of_lattice(sk17),sk16,sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p2897]) ).
cnf(p2909,plain,
( empty_carrier(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p2908,p2900]) ).
cnf(p2910,plain,
empty_carrier(sk17),
inference(factoring,[status(thm)],[p2909]) ).
cnf(c100,plain,
~ empty_carrier(sk17),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(p2913,plain,
$false,
inference(resolution,[status(thm)],[p2910,c100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU350+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.19/0.44 % Computer : n009.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Thu Sep 24 13:48:15 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.44 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 16.12/2.71 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.12/2.71 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------