%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU291+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 : n006.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:36 PM UTC 2026
% Result : Theorem 17.39s 2.69s
% Output : Proof 17.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 13
% Syntax : Number of formulae : 109 ( 32 unt; 0 def)
% Number of atoms : 275 ( 84 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 262 ( 96 ~; 105 |; 40 &)
% ( 4 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-3 aty)
% Number of variables : 124 ( 2 sgn 89 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f41,axiom,
! [A,B,C,D] :
( relation_of2_as_subset(D,C,A)
=> ( subset(A,B)
=> relation_of2_as_subset(D,C,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_relset_1) ).
fof(f41_nnf,plain,
! [A,B,C,D] :
( relation_of2_as_subset(D,C,B)
| ~ subset(A,B)
| ~ relation_of2_as_subset(D,C,A) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [D,C,A,B] :
( relation_of2_as_subset(D,C,B)
| ~ subset(A,B)
| ~ relation_of2_as_subset(D,C,A) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c73,plain,
( relation_of2_as_subset(X3,X2,X1)
| ~ subset(X0,X1)
| ~ relation_of2_as_subset(X3,X2,X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
fof(f51,conjecture,
! [A,B,C,D] :
( ( relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) )
=> ( subset(B,C)
=> ( ( relation_of2_as_subset(D,A,C)
& quasi_total(D,A,C)
& function(D) )
| ( A != empty_set
& B = empty_set ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_funct_2) ).
fof(f51_neg,negated_conjecture,
~ ! [A,B,C,D] :
( ( relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) )
=> ( subset(B,C)
=> ( ( relation_of2_as_subset(D,A,C)
& quasi_total(D,A,C)
& function(D) )
| ( A != empty_set
& B = empty_set ) ) ) ),
inference(negated_conjecture,[status(cth)],[f51]) ).
fof(f51_nnf,plain,
? [A,B,C,D] :
( ( ~ relation_of2_as_subset(D,A,C)
| ~ quasi_total(D,A,C)
| ~ function(D) )
& ( A = empty_set
| B != empty_set )
& subset(B,C)
& relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) ),
inference(nnf_transformation,[status(thm)],[f51_neg]) ).
fof(f51_sk,plain,
( ( ~ relation_of2_as_subset(sk20,sk17,sk19)
| ~ quasi_total(sk20,sk17,sk19)
| ~ function(sk20) )
& ( sk17 = empty_set
| sk18 != empty_set )
& subset(sk18,sk19)
& relation_of2_as_subset(sk20,sk17,sk18)
& quasi_total(sk20,sk17,sk18)
& function(sk20) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk17,sk18,sk19,sk20])],[f51_nnf]) ).
cnf(c86,plain,
relation_of2_as_subset(sk20,sk17,sk18),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p227,plain,
( relation_of2_as_subset(sk20,sk17,X0)
| ~ subset(sk18,X0) ),
inference(resolution,[status(thm)],[c73,c86]) ).
cnf(c87,plain,
subset(sk18,sk19),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p229,plain,
relation_of2_as_subset(sk20,sk17,sk19),
inference(resolution,[status(thm)],[p227,c87]) ).
fof(f39,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f39_nnf,plain,
! [A,B,C] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [C,A,B] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c70,plain,
( relation_of2(X2,X0,X1)
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p237,plain,
relation_of2(sk20,sk17,sk19),
inference(resolution,[status(thm)],[p229,c70]) ).
fof(f38,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> relation_dom_as_subset(A,B,C) = relation_dom(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_relset_1) ).
fof(f38_nnf,plain,
! [A,B,C] :
( relation_dom_as_subset(A,B,C) = relation_dom(C)
| ~ relation_of2(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [C,A,B] :
( relation_dom_as_subset(A,B,C) = relation_dom(C)
| ~ relation_of2(C,A,B) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c69,plain,
( relation_dom_as_subset(X0,X1,X2) = relation_dom(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p240,plain,
relation_dom_as_subset(sk17,sk19,sk20) = relation_dom(sk20),
inference(resolution,[status(thm)],[p237,c69]) ).
fof(f5,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> ( ( B = empty_set
=> ( ( quasi_total(C,A,B)
<=> C = empty_set )
| A = empty_set ) )
& ( ( B = empty_set
=> A = empty_set )
=> ( quasi_total(C,A,B)
<=> A = relation_dom_as_subset(A,B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_funct_2) ).
fof(f5_nnf,plain,
! [A,B,C] :
( ( ( ( ( C != empty_set
| quasi_total(C,A,B) )
& ( C = empty_set
| ~ quasi_total(C,A,B) ) )
| A = empty_set
| B != empty_set )
& ( ( ( A != relation_dom_as_subset(A,B,C)
| quasi_total(C,A,B) )
& ( A = relation_dom_as_subset(A,B,C)
| ~ quasi_total(C,A,B) ) )
| ( A != empty_set
& B = empty_set ) ) )
| ~ relation_of2_as_subset(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [C,A,B] :
( ( ( ( ( C != empty_set
| quasi_total(C,A,B) )
& ( C = empty_set
| ~ quasi_total(C,A,B) ) )
| A = empty_set
| B != empty_set )
& ( ( ( A != relation_dom_as_subset(A,B,C)
| quasi_total(C,A,B) )
& ( A = relation_dom_as_subset(A,B,C)
| ~ quasi_total(C,A,B) ) )
| ( A != empty_set
& B = empty_set ) ) )
| ~ relation_of2_as_subset(C,A,B) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c8,plain,
( X0 != relation_dom_as_subset(X0,X1,X2)
| quasi_total(X2,X0,X1)
| X1 = empty_set
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p231,plain,
( sk17 != relation_dom_as_subset(sk17,sk19,sk20)
| quasi_total(sk20,sk17,sk19)
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p229,c8]) ).
cnf(p242,plain,
( sk17 != relation_dom(sk20)
| quasi_total(sk20,sk17,sk19)
| sk19 = empty_set ),
inference(demodulation,[status(thm)],[p240,p231]) ).
cnf(p214,plain,
relation_of2(sk20,sk17,sk18),
inference(resolution,[status(thm)],[c70,c86]) ).
cnf(p217,plain,
relation_dom_as_subset(sk17,sk18,sk20) = relation_dom(sk20),
inference(resolution,[status(thm)],[p214,c69]) ).
cnf(c7,plain,
( X0 = relation_dom_as_subset(X0,X1,X2)
| ~ quasi_total(X2,X0,X1)
| X1 = empty_set
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p102,plain,
( sk17 = relation_dom_as_subset(sk17,sk18,sk20)
| ~ quasi_total(sk20,sk17,sk18)
| sk18 = empty_set ),
inference(resolution,[status(thm)],[c7,c86]) ).
cnf(c85,plain,
quasi_total(sk20,sk17,sk18),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p103,plain,
( sk17 = relation_dom_as_subset(sk17,sk18,sk20)
| sk18 = empty_set ),
inference(resolution,[status(thm)],[p102,c85]) ).
cnf(p218,plain,
( sk17 = relation_dom(sk20)
| sk18 = empty_set ),
inference(demodulation,[status(thm)],[p217,p103]) ).
cnf(p245,plain,
( sk18 = empty_set
| quasi_total(sk20,sk17,sk19)
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p242,p218]) ).
cnf(c89,plain,
( ~ relation_of2_as_subset(sk20,sk17,sk19)
| ~ quasi_total(sk20,sk17,sk19)
| ~ function(sk20) ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(c84,plain,
function(sk20),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p91,plain,
( ~ relation_of2_as_subset(sk20,sk17,sk19)
| ~ quasi_total(sk20,sk17,sk19) ),
inference(resolution,[status(thm)],[c89,c84]) ).
cnf(p255,plain,
( ~ relation_of2_as_subset(sk20,sk17,sk19)
| sk18 = empty_set
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p245,p91]) ).
cnf(p268,plain,
( sk18 = empty_set
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p255,p229]) ).
cnf(p269,plain,
( subset(sk18,empty_set)
| sk18 = empty_set ),
inference(superposition,[status(thm)],[p268,c87]) ).
fof(f45,axiom,
! [A] :
( subset(A,empty_set)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_xboole_1) ).
fof(f45_nnf,plain,
! [A] :
( A = empty_set
| ~ subset(A,empty_set) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [A] :
( A = empty_set
| ~ subset(A,empty_set) ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c78,plain,
( X0 = empty_set
| ~ subset(X0,empty_set) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p281,plain,
( sk18 = empty_set
| sk18 = empty_set ),
inference(resolution,[status(thm)],[p269,c78]) ).
cnf(p287,plain,
sk18 = empty_set,
inference(factoring,[status(thm)],[p281]) ).
cnf(c88,plain,
( sk17 = empty_set
| sk18 != empty_set ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p291,plain,
( sk17 = empty_set
| empty_set != empty_set ),
inference(demodulation,[status(thm)],[p287,c88]) ).
cnf(p329,plain,
sk17 = empty_set,
inference(equality_resolution,[status(thm)],[p291]) ).
fof(f44,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f44_nnf,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c76,plain,
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
fof(f10,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> element(relation_dom_as_subset(A,B,C),powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_relset_1) ).
fof(f10_nnf,plain,
! [A,B,C] :
( element(relation_dom_as_subset(A,B,C),powerset(A))
| ~ relation_of2(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [C,A,B] :
( element(relation_dom_as_subset(A,B,C),powerset(A))
| ~ relation_of2(C,A,B) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c17,plain,
( element(relation_dom_as_subset(X0,X1,X2),powerset(X0))
| ~ relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p216,plain,
element(relation_dom_as_subset(sk17,sk18,sk20),powerset(sk17)),
inference(resolution,[status(thm)],[p214,c17]) ).
cnf(p220,plain,
element(relation_dom(sk20),powerset(sk17)),
inference(demodulation,[status(thm)],[p217,p216]) ).
cnf(p261,plain,
subset(relation_dom(sk20),sk17),
inference(resolution,[status(thm)],[c76,p220]) ).
cnf(p344,plain,
subset(relation_dom(sk20),empty_set),
inference(demodulation,[status(thm)],[p329,p261]) ).
cnf(p369,plain,
relation_dom(sk20) = empty_set,
inference(resolution,[status(thm)],[p344,c78]) ).
fof(f22,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_dom(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_relat_1) ).
fof(f22_nnf,plain,
! [A] :
( ~ empty(relation_dom(A))
| ~ relation(A)
| empty(A) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [A] :
( ~ empty(relation_dom(A))
| ~ relation(A)
| empty(A) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c32,plain,
( ~ empty(relation_dom(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
fof(f13,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f13_nnf,plain,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [C,A,B] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c20,plain,
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p121,plain,
element(sk20,powerset(cartesian_product2(sk17,sk18))),
inference(resolution,[status(thm)],[c20,c86]) ).
fof(f3,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f3_nnf,plain,
! [A,B,C] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [C,A,B] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( relation(X2)
| ~ element(X2,powerset(cartesian_product2(X0,X1))) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p122,plain,
relation(sk20),
inference(resolution,[status(thm)],[p121,c3]) ).
cnf(p161,plain,
( ~ empty(relation_dom(sk20))
| empty(sk20) ),
inference(resolution,[status(thm)],[c32,p122]) ).
cnf(p370,plain,
( ~ empty(empty_set)
| empty(sk20) ),
inference(demodulation,[status(thm)],[p369,p161]) ).
fof(f17,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc12_relat_1) ).
fof(f17_nnf,plain,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c24,plain,
empty(empty_set),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p381,plain,
empty(sk20),
inference(resolution,[status(thm)],[p370,c24]) ).
fof(f48,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(f48_nnf,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c81,plain,
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p383,plain,
sk20 = empty_set,
inference(resolution,[status(thm)],[p381,c81]) ).
cnf(p338,plain,
( empty_set != relation_dom(sk20)
| quasi_total(sk20,empty_set,sk19)
| sk19 = empty_set ),
inference(demodulation,[status(thm)],[p329,p242]) ).
cnf(p372,plain,
( empty_set != empty_set
| quasi_total(sk20,empty_set,sk19)
| sk19 = empty_set ),
inference(demodulation,[status(thm)],[p369,p338]) ).
cnf(p402,plain,
( empty_set != empty_set
| quasi_total(empty_set,empty_set,sk19)
| sk19 = empty_set ),
inference(demodulation,[status(thm)],[p383,p372]) ).
cnf(p426,plain,
( quasi_total(empty_set,empty_set,sk19)
| sk19 = empty_set ),
inference(equality_resolution,[status(thm)],[p402]) ).
cnf(p330,plain,
( ~ relation_of2_as_subset(sk20,empty_set,sk19)
| ~ quasi_total(sk20,empty_set,sk19) ),
inference(demodulation,[status(thm)],[p329,p91]) ).
cnf(p384,plain,
( ~ relation_of2_as_subset(empty_set,empty_set,sk19)
| ~ quasi_total(empty_set,empty_set,sk19) ),
inference(demodulation,[status(thm)],[p383,p330]) ).
cnf(p429,plain,
( ~ relation_of2_as_subset(empty_set,empty_set,sk19)
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p426,p384]) ).
cnf(p332,plain,
relation_of2_as_subset(sk20,empty_set,sk19),
inference(demodulation,[status(thm)],[p329,p229]) ).
cnf(p385,plain,
relation_of2_as_subset(empty_set,empty_set,sk19),
inference(demodulation,[status(thm)],[p383,p332]) ).
cnf(p430,plain,
sk19 = empty_set,
inference(resolution,[status(thm)],[p429,p385]) ).
cnf(p432,plain,
( ~ relation_of2_as_subset(empty_set,empty_set,empty_set)
| ~ quasi_total(empty_set,empty_set,empty_set) ),
inference(demodulation,[status(thm)],[p430,p384]) ).
cnf(p288,plain,
quasi_total(sk20,sk17,empty_set),
inference(demodulation,[status(thm)],[p287,c85]) ).
cnf(p349,plain,
quasi_total(sk20,empty_set,empty_set),
inference(demodulation,[status(thm)],[p329,p288]) ).
cnf(p390,plain,
quasi_total(empty_set,empty_set,empty_set),
inference(demodulation,[status(thm)],[p383,p349]) ).
cnf(p433,plain,
~ relation_of2_as_subset(empty_set,empty_set,empty_set),
inference(resolution,[status(thm)],[p432,p390]) ).
cnf(p289,plain,
relation_of2_as_subset(sk20,sk17,empty_set),
inference(demodulation,[status(thm)],[p287,c86]) ).
cnf(p350,plain,
relation_of2_as_subset(sk20,empty_set,empty_set),
inference(demodulation,[status(thm)],[p329,p289]) ).
cnf(p391,plain,
relation_of2_as_subset(empty_set,empty_set,empty_set),
inference(demodulation,[status(thm)],[p383,p350]) ).
cnf(p435,plain,
$false,
inference(resolution,[status(thm)],[p433,p391]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU291+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.35 % Computer : n006.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 13:33:56 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 17.39/2.69 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.39/2.69 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------