%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU210+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 : n026.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:20 PM UTC 2026
% Result : Theorem 63.65s 13.67s
% Output : Proof 63.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 26
% Syntax : Number of formulae : 258 ( 203 unt; 0 def)
% Number of atoms : 388 ( 188 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 244 ( 114 ~; 72 |; 46 &)
% ( 4 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 9 con; 0-4 aty)
% Number of variables : 252 ( 23 sgn 99 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f30,axiom,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_inverse_image(C,B))
<=> ? [D] :
( in(D,B)
& in(ordered_pair(A,D),C)
& in(D,relation_rng(C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t166_relat_1) ).
fof(f30_nnf,plain,
! [A,B,C] :
( ( ( ! [D] :
( ~ in(D,B)
| ~ in(ordered_pair(A,D),C)
| ~ in(D,relation_rng(C)) )
| in(A,relation_inverse_image(C,B)) )
& ( ? [D] :
( in(D,B)
& in(ordered_pair(A,D),C)
& in(D,relation_rng(C)) )
| ~ in(A,relation_inverse_image(C,B)) ) )
| ~ relation(C) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(D,B)
| ~ in(ordered_pair(A,D),C)
| ~ in(D,relation_rng(C))
| in(A,relation_inverse_image(C,B)) )
& ( ( in(sk11(A,B,C),B)
& in(ordered_pair(A,sk11(A,B,C)),C)
& in(sk11(A,B,C),relation_rng(C)) )
| ~ in(A,relation_inverse_image(C,B)) ) )
| ~ relation(C) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11])],[f30_nnf]) ).
cnf(c46,plain,
( ~ in(X3,X1)
| ~ in(ordered_pair(X0,X3),X2)
| ~ in(X3,relation_rng(X2))
| in(X0,relation_inverse_image(X2,X1))
| ~ relation(X2) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(t243,plain,
ifeq(relation(X1),true,ifeq(in(X2,relation_rng(X1)),true,ifeq(in(ordered_pair(X3,X2),X1),true,ifeq(in(X2,X4),true,in(X3,relation_inverse_image(X1,X4)),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c46]) ).
cnf(t351,plain,
ifeq(relation(X1),true,ifeq(in(X2,relation_rng(X1)),true,ifeq(in(ordered_pair(X3,X2),X1),true,ifeq(in(X2,X4),true,in(X3,relation_inverse_image(X1,X4)),true),true),true),true) = true,
inference(orient,[status(thm)],[t243]) ).
fof(f31,conjecture,
! [A,B] :
( relation(B)
=> ~ ( relation_inverse_image(B,A) = empty_set
& subset(A,relation_rng(B))
& A != empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t174_relat_1) ).
fof(f31_neg,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> ~ ( relation_inverse_image(B,A) = empty_set
& subset(A,relation_rng(B))
& A != empty_set ) ),
inference(negated_conjecture,[status(cth)],[f31]) ).
fof(f31_nnf,plain,
? [A,B] :
( relation_inverse_image(B,A) = empty_set
& subset(A,relation_rng(B))
& A != empty_set
& relation(B) ),
inference(nnf_transformation,[status(thm)],[f31_neg]) ).
fof(f31_sk,plain,
( relation_inverse_image(sk13,sk12) = empty_set
& subset(sk12,relation_rng(sk13))
& sk12 != empty_set
& relation(sk13) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk12,sk13])],[f31_nnf]) ).
cnf(c47,plain,
relation(sk13),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(t12,plain,
relation(sk13) = true,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(t400,plain,
relation(sk13) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t411,plain,
true = ifeq(true,true,ifeq(in(X1,relation_rng(sk13)),true,ifeq(in(ordered_pair(X2,X1),sk13),true,ifeq(in(X1,X3),true,in(X2,relation_inverse_image(sk13,X3)),true),true),true),true),
inference(cp,[status(thm)],[t351,t400]) ).
cnf(t95,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t95]) ).
cnf(t4657,plain,
true = ifeq(in(X1,relation_rng(sk13)),true,ifeq(in(ordered_pair(X2,X1),sk13),true,ifeq(in(X1,X3),true,in(X2,relation_inverse_image(sk13,X3)),true),true),true),
inference(step,[status(thm)],[t411,t256]) ).
cnf(t3676,plain,
ifeq(in(X1,relation_rng(sk13)),true,ifeq(in(ordered_pair(X2,X1),sk13),true,ifeq(in(X1,X3),true,in(X2,relation_inverse_image(sk13,X3)),true),true),true) = true,
inference(orient,[status(thm)],[t4657]) ).
fof(f33,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f33_nnf,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c52,plain,
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(hi35,axiom,
ifeq(element(X0,X1),true,or(empty(X1),in(X0,X1)),true) = true,
inference(equality_encoding,[status(esa)],[c52]) ).
fof(f14,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(f14_nnf,plain,
! [A] :
? [B] : element(B,A),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [A] : element(sk4(A),A),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4])],[f14_nnf]) ).
cnf(c21,plain,
element(sk4(X0),X0),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(hi11,axiom,
element(sk4(X0),X0) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t155,plain,
or(empty(X1),in(sk4(X1),X1)) = true,
inference(hyper_resolution,[status(thm)],[hi35,hi11]) ).
cnf(t372,plain,
or(empty(X1),in(sk4(X1),X1)) = true,
inference(orient,[status(thm)],[t155]) ).
cnf(t132,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t569,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t132]) ).
fof(f38,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f38_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c58,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(t181,plain,
or(not(in(X1,X2)),not(empty(X2))) = true,
inference(equality_encoding,[status(esa)],[c58]) ).
cnf(t387,plain,
or(not(in(X1,X2)),not(empty(X2))) = true,
inference(orient,[status(thm)],[t181]) ).
fof(f4,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_relat_1) ).
fof(f4_nnf,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] : in(ordered_pair(D,C),A)
& ~ in(C,B) )
| ( ! [D] : ~ in(ordered_pair(D,C),A)
& in(C,B) ) )
| B = relation_rng(A) )
& ( ! [C] :
( ( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ( ? [D] : in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C,D] :
( ( ( ( in(ordered_pair(sk3(A,B),sk2(A,B)),A)
& ~ in(sk2(A,B),B) )
| ( ~ in(ordered_pair(D,sk2(A,B)),A)
& in(sk2(A,B),B) )
| B = relation_rng(A) )
& ( ( ( ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ( in(ordered_pair(sk1(A,B,C),C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2,sk3])],[f4_nnf]) ).
cnf(c9,plain,
( in(ordered_pair(sk3(X0,X1),sk2(X0,X1)),X0)
| in(sk2(X0,X1),X1)
| X1 = relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t235,plain,
ifeq(relation(X1),true,or(eq(X2,relation_rng(X1)),or(in(sk2(X1,X2),X2),in(ordered_pair(sk3(X1,X2),sk2(X1,X2)),X1))),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t362,plain,
ifeq(relation(X1),true,or(eq(X2,relation_rng(X1)),or(in(sk2(X1,X2),X2),in(ordered_pair(sk3(X1,X2),sk2(X1,X2)),X1))),true) = true,
inference(orient,[status(thm)],[t235]) ).
fof(f22,axiom,
! [A] :
( empty(A)
=> ( relation(relation_rng(A))
& empty(relation_rng(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc8_relat_1) ).
fof(f22_nnf,plain,
! [A] :
( ( relation(relation_rng(A))
& empty(relation_rng(A)) )
| ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [A] :
( ( relation(relation_rng(A))
& empty(relation_rng(A)) )
| ~ empty(A) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c30,plain,
( empty(relation_rng(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(hi16,axiom,
ifeq(empty(X0),true,empty(relation_rng(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c30]) ).
fof(f23,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_relat_1) ).
fof(f23_nnf,plain,
? [A] :
( relation(A)
& empty(A) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
( relation(sk5)
& empty(sk5) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f23_nnf]) ).
cnf(c32,plain,
empty(sk5),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(hi18,axiom,
empty(sk5) = true,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(h7,plain,
empty(relation_rng(sk5)) = true,
inference(hyper_resolution,[status(thm)],[hi16,hi18]) ).
cnf(h43,plain,
empty(relation_rng(relation_rng(sk5))) = true,
inference(hyper_resolution,[status(thm)],[hi16,h7]) ).
cnf(h90,plain,
empty(relation_rng(relation_rng(relation_rng(sk5)))) = true,
inference(hyper_resolution,[status(thm)],[hi16,h43]) ).
cnf(h149,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(sk5))))) = true,
inference(hyper_resolution,[status(thm)],[hi16,h90]) ).
cnf(h224,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5)))))) = true,
inference(hyper_resolution,[status(thm)],[hi16,h149]) ).
cnf(h315,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5))))))) = true,
inference(hyper_resolution,[status(thm)],[hi16,h224]) ).
cnf(h422,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5)))))))) = true,
inference(hyper_resolution,[status(thm)],[hi16,h315]) ).
cnf(t214,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5))))))))) = true,
inference(hyper_resolution,[status(thm)],[hi16,h422]) ).
cnf(h545,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5))))))))) = true,
inference(hyper_resolution,[status(thm)],[hi16,h422]) ).
fof(f39,axiom,
! [A,B] :
~ ( empty(B)
& A != B
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
fof(f39_nnf,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c59,plain,
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(hi40,axiom,
ifeq(empty(X0),true,ifeq(empty(X1),true,X0,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c59]) ).
fof(f25,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
fof(f25_nnf,plain,
? [A] : empty(A),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
empty(sk7),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7])],[f25_nnf]) ).
cnf(c36,plain,
empty(sk7),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(hi22,axiom,
empty(sk7) = true,
inference(equality_encoding,[status(esa)],[c36]) ).
cnf(t210,plain,
relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5)))))))) = sk7,
inference(hyper_resolution,[status(thm)],[hi40,hi22,h545]) ).
cnf(t209,plain,
relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5)))))))) = sk5,
inference(hyper_resolution,[status(thm)],[hi40,hi18,h545]) ).
cnf(t263,plain,
relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5)))))))) = sk5,
inference(orient,[status(thm)],[t209]) ).
cnf(t4051,plain,
sk5 = sk7,
inference(step,[status(thm)],[t210,t263]) ).
cnf(t267,plain,
sk5 = sk7,
inference(orient,[status(thm)],[t4051]) ).
cnf(t4078,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7))))))))) = true,
inference(step,[status(thm)],[t214,t267]) ).
cnf(t75,plain,
relation_rng(relation_rng(relation_rng(sk5))) = sk5,
inference(hyper_resolution,[status(thm)],[hi40,hi18,h90]) ).
cnf(t4075,plain,
relation_rng(relation_rng(relation_rng(sk7))) = sk5,
inference(step,[status(thm)],[t75,t267]) ).
cnf(t113,plain,
relation_rng(relation_rng(relation_rng(sk5))) = relation_rng(sk5),
inference(hyper_resolution,[status(thm)],[hi40,h7,h90]) ).
cnf(t4072,plain,
relation_rng(relation_rng(relation_rng(sk7))) = relation_rng(sk5),
inference(step,[status(thm)],[t113,t267]) ).
cnf(t4073,plain,
relation_rng(relation_rng(relation_rng(sk7))) = relation_rng(sk7),
inference(step,[status(thm)],[t4072,t267]) ).
cnf(t297,plain,
relation_rng(relation_rng(relation_rng(sk7))) = relation_rng(sk7),
inference(orient,[status(thm)],[t4073]) ).
cnf(t4076,plain,
relation_rng(sk7) = sk5,
inference(step,[status(thm)],[t4075,t297]) ).
cnf(t4077,plain,
relation_rng(sk7) = sk7,
inference(step,[status(thm)],[t4076,t267]) ).
cnf(t302,plain,
relation_rng(sk7) = sk7,
inference(orient,[status(thm)],[t4077]) ).
cnf(t4079,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7)))))))) = true,
inference(step,[status(thm)],[t4078,t302]) ).
cnf(t4080,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7))))))) = true,
inference(step,[status(thm)],[t4079,t302]) ).
cnf(t4081,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7)))))) = true,
inference(step,[status(thm)],[t4080,t302]) ).
cnf(t4082,plain,
empty(relation_rng(relation_rng(relation_rng(relation_rng(sk7))))) = true,
inference(step,[status(thm)],[t4081,t302]) ).
cnf(t4083,plain,
empty(relation_rng(relation_rng(relation_rng(sk7)))) = true,
inference(step,[status(thm)],[t4082,t302]) ).
cnf(t4084,plain,
empty(relation_rng(relation_rng(sk7))) = true,
inference(step,[status(thm)],[t4083,t302]) ).
cnf(t4085,plain,
empty(relation_rng(sk7)) = true,
inference(step,[status(thm)],[t4084,t302]) ).
cnf(t4086,plain,
empty(sk7) = true,
inference(step,[status(thm)],[t4085,t302]) ).
cnf(t306,plain,
empty(sk7) = true,
inference(orient,[status(thm)],[t4086]) ).
cnf(t388,plain,
true = or(not(in(X1,sk7)),not(true)),
inference(cp,[status(thm)],[t387,t306]) ).
cnf(t10,plain,
not(true) = false,
introduced(definition) ).
cnf(t579,plain,
not(true) = false,
inference(orient,[status(thm)],[t10]) ).
cnf(t4180,plain,
true = or(not(in(X1,sk7)),false),
inference(step,[status(thm)],[t388,t579]) ).
cnf(t33,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t260,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t33]) ).
cnf(t4181,plain,
true = not(in(X1,sk7)),
inference(step,[status(thm)],[t4180,t260]) ).
cnf(t858,plain,
not(in(X1,sk7)) = true,
inference(orient,[status(thm)],[t4181]) ).
cnf(t859,plain,
false = ifeq(true,true,in(X1,sk7),false),
inference(cp,[status(thm)],[t569,t858]) ).
cnf(t4182,plain,
false = in(X1,sk7),
inference(step,[status(thm)],[t859,t256]) ).
cnf(t860,plain,
in(X1,sk7) = false,
inference(orient,[status(thm)],[t4182]) ).
cnf(t879,plain,
true = ifeq(relation(sk7),true,or(eq(X1,relation_rng(sk7)),or(in(sk2(sk7,X1),X1),false)),true),
inference(cp,[status(thm)],[t362,t860]) ).
cnf(c31,plain,
( relation(relation_rng(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(hi17,axiom,
ifeq(empty(X0),true,relation(relation_rng(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t206,plain,
relation(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5)))))))) = true,
inference(hyper_resolution,[status(thm)],[hi17,h315]) ).
cnf(t4114,plain,
relation(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7)))))))) = true,
inference(step,[status(thm)],[t206,t267]) ).
cnf(t4115,plain,
relation(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7))))))) = true,
inference(step,[status(thm)],[t4114,t302]) ).
cnf(t4116,plain,
relation(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7)))))) = true,
inference(step,[status(thm)],[t4115,t302]) ).
cnf(t4117,plain,
relation(relation_rng(relation_rng(relation_rng(relation_rng(sk7))))) = true,
inference(step,[status(thm)],[t4116,t302]) ).
cnf(t4118,plain,
relation(relation_rng(relation_rng(relation_rng(sk7)))) = true,
inference(step,[status(thm)],[t4117,t302]) ).
cnf(t4119,plain,
relation(relation_rng(relation_rng(sk7))) = true,
inference(step,[status(thm)],[t4118,t302]) ).
cnf(t4120,plain,
relation(relation_rng(sk7)) = true,
inference(step,[status(thm)],[t4119,t302]) ).
cnf(t4121,plain,
relation(sk7) = true,
inference(step,[status(thm)],[t4120,t302]) ).
cnf(t390,plain,
relation(sk7) = true,
inference(orient,[status(thm)],[t4121]) ).
cnf(t4257,plain,
true = ifeq(true,true,or(eq(X1,relation_rng(sk7)),or(in(sk2(sk7,X1),X1),false)),true),
inference(step,[status(thm)],[t879,t390]) ).
cnf(t4258,plain,
true = or(eq(X1,relation_rng(sk7)),or(in(sk2(sk7,X1),X1),false)),
inference(step,[status(thm)],[t4257,t256]) ).
cnf(t4259,plain,
true = or(eq(X1,sk7),or(in(sk2(sk7,X1),X1),false)),
inference(step,[status(thm)],[t4258,t302]) ).
cnf(t4260,plain,
true = or(eq(X1,sk7),in(sk2(sk7,X1),X1)),
inference(step,[status(thm)],[t4259,t260]) ).
cnf(t1216,plain,
or(eq(X1,sk7),in(sk2(sk7,X1),X1)) = true,
inference(orient,[status(thm)],[t4260]) ).
cnf(c48,plain,
sk12 != empty_set,
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(t32,plain,
eq(sk12,empty_set) = false,
inference(equality_encoding,[status(esa)],[c48]) ).
fof(f20,axiom,
( relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(f20_nnf,plain,
( relation(empty_set)
& empty(empty_set) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
( relation(empty_set)
& empty(empty_set) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c27,plain,
empty(empty_set),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(hi13,axiom,
empty(empty_set) = true,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t189,plain,
relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5))))))) = empty_set,
inference(hyper_resolution,[status(thm)],[hi40,hi13,h422]) ).
cnf(t4059,plain,
relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7))))))) = empty_set,
inference(step,[status(thm)],[t189,t267]) ).
cnf(t190,plain,
relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk5))))))) = sk5,
inference(hyper_resolution,[status(thm)],[hi40,hi18,h422]) ).
cnf(t4056,plain,
relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7))))))) = sk5,
inference(step,[status(thm)],[t190,t267]) ).
cnf(t4057,plain,
relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7))))))) = sk7,
inference(step,[status(thm)],[t4056,t267]) ).
cnf(t275,plain,
relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(relation_rng(sk7))))))) = sk7,
inference(orient,[status(thm)],[t4057]) ).
cnf(t4060,plain,
sk7 = empty_set,
inference(step,[status(thm)],[t4059,t275]) ).
cnf(t280,plain,
empty_set = sk7,
inference(orient,[status(thm)],[t4060]) ).
cnf(t4140,plain,
eq(sk12,sk7) = false,
inference(step,[status(thm)],[t32,t280]) ).
cnf(t577,plain,
eq(sk12,sk7) = false,
inference(orient,[status(thm)],[t4140]) ).
cnf(t1217,plain,
true = or(false,in(sk2(sk7,sk12),sk12)),
inference(cp,[status(thm)],[t1216,t577]) ).
cnf(t35,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t261,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t35]) ).
cnf(t4261,plain,
true = in(sk2(sk7,sk12),sk12),
inference(step,[status(thm)],[t1217,t261]) ).
cnf(t1218,plain,
in(sk2(sk7,sk12),sk12) = true,
inference(orient,[status(thm)],[t4261]) ).
cnf(t1220,plain,
true = or(not(true),not(empty(sk12))),
inference(cp,[status(thm)],[t387,t1218]) ).
cnf(t4262,plain,
true = or(false,not(empty(sk12))),
inference(step,[status(thm)],[t1220,t579]) ).
cnf(t4263,plain,
true = not(empty(sk12)),
inference(step,[status(thm)],[t4262,t261]) ).
cnf(t1236,plain,
not(empty(sk12)) = true,
inference(orient,[status(thm)],[t4263]) ).
cnf(t1237,plain,
false = ifeq(true,true,empty(sk12),false),
inference(cp,[status(thm)],[t569,t1236]) ).
cnf(t4264,plain,
false = empty(sk12),
inference(step,[status(thm)],[t1237,t256]) ).
cnf(t1238,plain,
empty(sk12) = false,
inference(orient,[status(thm)],[t4264]) ).
cnf(t1245,plain,
true = or(false,in(sk4(sk12),sk12)),
inference(cp,[status(thm)],[t372,t1238]) ).
cnf(t4265,plain,
true = in(sk4(sk12),sk12),
inference(step,[status(thm)],[t1245,t261]) ).
cnf(t1254,plain,
in(sk4(sk12),sk12) = true,
inference(orient,[status(thm)],[t4265]) ).
cnf(t3696,plain,
true = ifeq(in(sk4(sk12),relation_rng(sk13)),true,ifeq(in(ordered_pair(X1,sk4(sk12)),sk13),true,ifeq(true,true,in(X1,relation_inverse_image(sk13,sk12)),true),true),true),
inference(cp,[status(thm)],[t3676,t1254]) ).
cnf(t222,plain,
ifeq(element(X1,X2),true,or(empty(X2),in(X1,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c52]) ).
cnf(t364,plain,
ifeq(element(X1,X2),true,or(empty(X2),in(X1,X2)),true) = true,
inference(orient,[status(thm)],[t222]) ).
fof(f35,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f35_nnf,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c55,plain,
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(t228,plain,
ifeq(in(X1,X2),true,ifeq(element(X2,powerset(X3)),true,element(X1,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c55]) ).
cnf(t314,plain,
ifeq(in(X1,X2),true,ifeq(element(X2,powerset(X3)),true,element(X1,X3),true),true) = true,
inference(orient,[status(thm)],[t228]) ).
fof(f34,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f34_nnf,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c54,plain,
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(hi37,axiom,
ifeq(subset(X0,X1),true,element(X0,powerset(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(c49,plain,
subset(sk12,relation_rng(sk13)),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(hi32,negated_conjecture,
subset(sk12,relation_rng(sk13)) = true,
inference(equality_encoding,[status(esa)],[c49]) ).
cnf(t90,plain,
element(sk12,powerset(relation_rng(sk13))) = true,
inference(hyper_resolution,[status(thm)],[hi37,hi32]) ).
cnf(t441,plain,
element(sk12,powerset(relation_rng(sk13))) = true,
inference(orient,[status(thm)],[t90]) ).
cnf(t446,plain,
true = ifeq(in(X1,sk12),true,ifeq(true,true,element(X1,relation_rng(sk13)),true),true),
inference(cp,[status(thm)],[t314,t441]) ).
cnf(t4356,plain,
true = ifeq(in(X1,sk12),true,element(X1,relation_rng(sk13)),true),
inference(step,[status(thm)],[t446,t256]) ).
cnf(t1668,plain,
ifeq(in(X1,sk12),true,element(X1,relation_rng(sk13)),true) = true,
inference(orient,[status(thm)],[t4356]) ).
cnf(t1669,plain,
true = ifeq(true,true,element(sk4(sk12),relation_rng(sk13)),true),
inference(cp,[status(thm)],[t1668,t1254]) ).
cnf(t4357,plain,
true = element(sk4(sk12),relation_rng(sk13)),
inference(step,[status(thm)],[t1669,t256]) ).
cnf(t1671,plain,
element(sk4(sk12),relation_rng(sk13)) = true,
inference(orient,[status(thm)],[t4357]) ).
cnf(t1672,plain,
true = ifeq(true,true,or(empty(relation_rng(sk13)),in(sk4(sk12),relation_rng(sk13))),true),
inference(cp,[status(thm)],[t364,t1671]) ).
cnf(t4358,plain,
true = or(empty(relation_rng(sk13)),in(sk4(sk12),relation_rng(sk13))),
inference(step,[status(thm)],[t1672,t256]) ).
fof(f36,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f36_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c56,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(t226,plain,
or(not(in(X1,X2)),or(not(element(X2,powerset(X3))),not(empty(X3)))) = true,
inference(equality_encoding,[status(esa)],[c56]) ).
cnf(t384,plain,
or(not(in(X1,X2)),or(not(element(X2,powerset(X3))),not(empty(X3)))) = true,
inference(orient,[status(thm)],[t226]) ).
cnf(t1232,plain,
true = or(not(true),or(not(element(sk12,powerset(X1))),not(empty(X1)))),
inference(cp,[status(thm)],[t384,t1218]) ).
cnf(t4309,plain,
true = or(false,or(not(element(sk12,powerset(X1))),not(empty(X1)))),
inference(step,[status(thm)],[t1232,t579]) ).
cnf(t4310,plain,
true = or(not(element(sk12,powerset(X1))),not(empty(X1))),
inference(step,[status(thm)],[t4309,t261]) ).
cnf(t1461,plain,
or(not(element(sk12,powerset(X1))),not(empty(X1))) = true,
inference(orient,[status(thm)],[t4310]) ).
cnf(t1462,plain,
true = or(not(true),not(empty(relation_rng(sk13)))),
inference(cp,[status(thm)],[t1461,t441]) ).
cnf(t4311,plain,
true = or(false,not(empty(relation_rng(sk13)))),
inference(step,[status(thm)],[t1462,t579]) ).
cnf(t4312,plain,
true = not(empty(relation_rng(sk13))),
inference(step,[status(thm)],[t4311,t261]) ).
cnf(t1464,plain,
not(empty(relation_rng(sk13))) = true,
inference(orient,[status(thm)],[t4312]) ).
cnf(t1465,plain,
false = ifeq(true,true,empty(relation_rng(sk13)),false),
inference(cp,[status(thm)],[t569,t1464]) ).
cnf(t4313,plain,
false = empty(relation_rng(sk13)),
inference(step,[status(thm)],[t1465,t256]) ).
cnf(t1466,plain,
empty(relation_rng(sk13)) = false,
inference(orient,[status(thm)],[t4313]) ).
cnf(t4359,plain,
true = or(false,in(sk4(sk12),relation_rng(sk13))),
inference(step,[status(thm)],[t4358,t1466]) ).
cnf(t4360,plain,
true = in(sk4(sk12),relation_rng(sk13)),
inference(step,[status(thm)],[t4359,t261]) ).
cnf(t1674,plain,
in(sk4(sk12),relation_rng(sk13)) = true,
inference(orient,[status(thm)],[t4360]) ).
cnf(t4658,plain,
true = ifeq(true,true,ifeq(in(ordered_pair(X1,sk4(sk12)),sk13),true,ifeq(true,true,in(X1,relation_inverse_image(sk13,sk12)),true),true),true),
inference(step,[status(thm)],[t3696,t1674]) ).
cnf(t4659,plain,
true = ifeq(in(ordered_pair(X1,sk4(sk12)),sk13),true,ifeq(true,true,in(X1,relation_inverse_image(sk13,sk12)),true),true),
inference(step,[status(thm)],[t4658,t256]) ).
cnf(t4660,plain,
true = ifeq(in(ordered_pair(X1,sk4(sk12)),sk13),true,in(X1,relation_inverse_image(sk13,sk12)),true),
inference(step,[status(thm)],[t4659,t256]) ).
cnf(c50,plain,
relation_inverse_image(sk13,sk12) = empty_set,
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(t40,plain,
relation_inverse_image(sk13,sk12) = empty_set,
inference(equality_encoding,[status(esa)],[c50]) ).
cnf(t4126,plain,
relation_inverse_image(sk13,sk12) = sk7,
inference(step,[status(thm)],[t40,t280]) ).
cnf(t471,plain,
relation_inverse_image(sk13,sk12) = sk7,
inference(orient,[status(thm)],[t4126]) ).
cnf(t4661,plain,
true = ifeq(in(ordered_pair(X1,sk4(sk12)),sk13),true,in(X1,sk7),true),
inference(step,[status(thm)],[t4660,t471]) ).
cnf(t4662,plain,
true = ifeq(in(ordered_pair(X1,sk4(sk12)),sk13),true,false,true),
inference(step,[status(thm)],[t4661,t860]) ).
cnf(t3744,plain,
ifeq(in(ordered_pair(X1,sk4(sk12)),sk13),true,false,true) = true,
inference(orient,[status(thm)],[t4662]) ).
cnf(c6,plain,
( in(ordered_pair(sk1(X0,X1,X2),X2),X0)
| ~ in(X2,X1)
| X1 != relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t234,plain,
ifeq(relation(X1),true,ifeq(X2,relation_rng(X1),ifeq(in(X3,X2),true,in(ordered_pair(sk1(X1,X2,X3),X3),X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t345,plain,
ifeq(relation(X1),true,ifeq(X2,relation_rng(X1),ifeq(in(X3,X2),true,in(ordered_pair(sk1(X1,X2,X3),X3),X1),true),true),true) = true,
inference(orient,[status(thm)],[t234]) ).
cnf(t346,plain,
true = ifeq(relation(X1),true,ifeq(in(X2,relation_rng(X1)),true,in(ordered_pair(sk1(X1,relation_rng(X1),X2),X2),X1),true),true),
inference(cp,[status(thm)],[t345,t256]) ).
cnf(t1348,plain,
ifeq(relation(X1),true,ifeq(in(X2,relation_rng(X1)),true,in(ordered_pair(sk1(X1,relation_rng(X1),X2),X2),X1),true),true) = true,
inference(orient,[status(thm)],[t346]) ).
cnf(t1686,plain,
true = ifeq(relation(sk13),true,ifeq(true,true,in(ordered_pair(sk1(sk13,relation_rng(sk13),sk4(sk12)),sk4(sk12)),sk13),true),true),
inference(cp,[status(thm)],[t1348,t1674]) ).
cnf(t4461,plain,
true = ifeq(true,true,ifeq(true,true,in(ordered_pair(sk1(sk13,relation_rng(sk13),sk4(sk12)),sk4(sk12)),sk13),true),true),
inference(step,[status(thm)],[t1686,t400]) ).
cnf(t4462,plain,
true = ifeq(true,true,in(ordered_pair(sk1(sk13,relation_rng(sk13),sk4(sk12)),sk4(sk12)),sk13),true),
inference(step,[status(thm)],[t4461,t256]) ).
cnf(t4463,plain,
true = in(ordered_pair(sk1(sk13,relation_rng(sk13),sk4(sk12)),sk4(sk12)),sk13),
inference(step,[status(thm)],[t4462,t256]) ).
cnf(t2316,plain,
in(ordered_pair(sk1(sk13,relation_rng(sk13),sk4(sk12)),sk4(sk12)),sk13) = true,
inference(orient,[status(thm)],[t4463]) ).
cnf(t3745,plain,
true = ifeq(true,true,false,true),
inference(cp,[status(thm)],[t3744,t2316]) ).
cnf(t4663,plain,
true = false,
inference(step,[status(thm)],[t3745,t256]) ).
cnf(t3746,plain,
false = true,
inference(orient,[status(thm)],[t4663]) ).
fof(f0,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f0_nnf,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f15,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f15_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c22,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
fof(f17,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f17_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c24,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
fof(f18,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f18_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c25,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
fof(f19,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f19_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c26,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
fof(f26,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f26_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
( relation(sk8)
& ~ empty(sk8) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8])],[f26_nnf]) ).
cnf(c37,plain,
~ empty(sk8),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
fof(f28,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f28_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
~ empty(sk10),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk10])],[f28_nnf]) ).
cnf(c41,plain,
~ empty(sk10),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c22,c24,c25,c26,c37,c41,c48,c56,c58]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t3746]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU210+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/5.59 % Computer : n026.cluster.edu
% 0.11/5.59 % Model : x86_64 x86_64
% 0.11/5.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.59 % Memory : 8046.5625MB
% 0.11/5.59 % OS : Linux 6.8.0-71-generic
% 0.11/5.59 % CPULimit : 300
% 0.11/5.59 % WCLimit : 300
% 0.11/5.59 % DateTime : Thu Sep 24 13:14:30 UTC 2026
% 0.11/5.59 % CPUTime :
% 0.11/5.59 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 63.65/13.67 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.65/13.67 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------