%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU096+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.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:50:56 PM UTC 2026
% Result : Theorem 23.63s 9.04s
% Output : Proof 23.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 3
% Syntax : Number of formulae : 25 ( 9 unt; 0 def)
% Number of atoms : 71 ( 7 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 74 ( 28 ~; 24 |; 15 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 26 ( 0 sgn 16 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f52,conjecture,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( ( finite(relation_inverse_image(B,A))
& subset(A,relation_rng(B)) )
=> finite(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t27_finset_1) ).
fof(f52_neg,negated_conjecture,
~ ! [A,B] :
( ( function(B)
& relation(B) )
=> ( ( finite(relation_inverse_image(B,A))
& subset(A,relation_rng(B)) )
=> finite(A) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f52_nnf,plain,
? [A,B] :
( ~ finite(A)
& finite(relation_inverse_image(B,A))
& subset(A,relation_rng(B))
& function(B)
& relation(B) ),
inference(nnf_transformation,[status(thm)],[f52_neg]) ).
fof(f52_sk,plain,
( ~ finite(sk26)
& finite(relation_inverse_image(sk27,sk26))
& subset(sk26,relation_rng(sk27))
& function(sk27)
& relation(sk27) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk26,sk27])],[f52_nnf]) ).
cnf(c136,plain,
relation(sk27),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
fof(f49,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( subset(A,relation_rng(B))
=> relation_image(B,relation_inverse_image(B,A)) = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t147_funct_1) ).
fof(f49_nnf,plain,
! [A,B] :
( relation_image(B,relation_inverse_image(B,A)) = A
| ~ subset(A,relation_rng(B))
| ~ function(B)
| ~ relation(B) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [B,A] :
( relation_image(B,relation_inverse_image(B,A)) = A
| ~ subset(A,relation_rng(B))
| ~ function(B)
| ~ relation(B) ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c133,plain,
( relation_image(X1,relation_inverse_image(X1,X0)) = X0
| ~ subset(X0,relation_rng(X1))
| ~ function(X1)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p294,plain,
( relation_image(sk27,relation_inverse_image(sk27,X0)) = X0
| ~ subset(X0,relation_rng(sk27))
| ~ function(sk27) ),
inference(resolution,[status(thm)],[c136,c133]) ).
cnf(c137,plain,
function(sk27),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p378,plain,
( relation_image(sk27,relation_inverse_image(sk27,X0)) = X0
| ~ subset(X0,relation_rng(sk27)) ),
inference(resolution,[status(thm)],[p294,c137]) ).
cnf(c138,plain,
subset(sk26,relation_rng(sk27)),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p529,plain,
relation_image(sk27,relation_inverse_image(sk27,sk26)) = sk26,
inference(resolution,[status(thm)],[p378,c138]) ).
fof(f14,axiom,
! [A,B] :
( ( finite(B)
& function(A)
& relation(A) )
=> finite(relation_image(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc13_finset_1) ).
fof(f14_nnf,plain,
! [A,B] :
( finite(relation_image(A,B))
| ~ finite(B)
| ~ function(A)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [A,B] :
( finite(relation_image(A,B))
| ~ finite(B)
| ~ function(A)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c29,plain,
( finite(relation_image(X0,X1))
| ~ finite(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p291,plain,
( finite(relation_image(sk27,X0))
| ~ finite(X0)
| ~ function(sk27) ),
inference(resolution,[status(thm)],[c136,c29]) ).
cnf(p377,plain,
( finite(relation_image(sk27,X0))
| ~ finite(X0) ),
inference(resolution,[status(thm)],[p291,c137]) ).
cnf(c139,plain,
finite(relation_inverse_image(sk27,sk26)),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p522,plain,
finite(relation_image(sk27,relation_inverse_image(sk27,sk26))),
inference(resolution,[status(thm)],[p377,c139]) ).
cnf(p530,plain,
finite(sk26),
inference(demodulation,[status(thm)],[p529,p522]) ).
cnf(c140,plain,
~ finite(sk26),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1314,plain,
$false,
inference(resolution,[status(thm)],[p530,c140]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU096+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.59 % Computer : n013.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 12:43:26 UTC 2026
% 0.11/5.60 % CPUTime :
% 0.15/5.60 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 23.63/9.04 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.63/9.04 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------