%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET661+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.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:43:45 PM UTC 2026
% Result : Theorem 141.81s 23.37s
% Output : Proof 141.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 6
% Syntax : Number of formulae : 47 ( 13 unt; 0 def)
% Number of atoms : 129 ( 44 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 148 ( 66 ~; 56 |; 8 &)
% ( 0 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-3 aty)
% Number of variables : 85 ( 1 sgn 45 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f35,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ilf_type(inverse3(B,C,D),relation_type(C,B)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p36) ).
fof(f35_nnf,plain,
! [B] :
( ! [C] :
( ! [D] :
( ilf_type(inverse3(B,C,D),relation_type(C,B))
| ~ ilf_type(D,relation_type(B,C)) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [B,C,D] :
( ilf_type(inverse3(B,C,D),relation_type(C,B))
| ~ ilf_type(D,relation_type(B,C))
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c72,plain,
( ilf_type(inverse3(X0,X1,X2),relation_type(X1,X0))
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
fof(f36,axiom,
! [B] : ilf_type(B,set_type),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p37) ).
fof(f36_nnf,plain,
! [B] : ilf_type(B,set_type),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [B] : ilf_type(B,set_type),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c73,plain,
ilf_type(X0,set_type),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p599,plain,
( ilf_type(inverse3(X2,X0,X1),relation_type(X0,X2))
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c72,c73]) ).
cnf(p2327,plain,
( ilf_type(inverse3(X1,X2,X0),relation_type(X2,X1))
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(resolution,[status(thm)],[p599,c73]) ).
fof(f37,conjecture,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ( range(C,B,inverse3(B,C,D)) = domain(B,C,D)
& domain(C,B,inverse3(B,C,D)) = range(B,C,D) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_relset_1_24) ).
fof(f37_neg,negated_conjecture,
~ ! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ( range(C,B,inverse3(B,C,D)) = domain(B,C,D)
& domain(C,B,inverse3(B,C,D)) = range(B,C,D) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f37]) ).
fof(f37_nnf,plain,
? [B] :
( ? [C] :
( ? [D] :
( ( range(C,B,inverse3(B,C,D)) != domain(B,C,D)
| domain(C,B,inverse3(B,C,D)) != range(B,C,D) )
& ilf_type(D,relation_type(B,C)) )
& ilf_type(C,set_type) )
& ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f37_neg]) ).
fof(f37_sk,plain,
( ( range(sk15,sk14,inverse3(sk14,sk15,sk16)) != domain(sk14,sk15,sk16)
| domain(sk15,sk14,inverse3(sk14,sk15,sk16)) != range(sk14,sk15,sk16) )
& ilf_type(sk16,relation_type(sk14,sk15))
& ilf_type(sk15,set_type)
& ilf_type(sk14,set_type) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14,sk15,sk16])],[f37_nnf]) ).
cnf(c76,plain,
ilf_type(sk16,relation_type(sk14,sk15)),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p29448,plain,
ilf_type(inverse(sk16),relation_type(sk15,sk14)),
inference(resolution,[status(thm)],[p2327,c76]) ).
fof(f32,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> range(B,C,D) = range_of(D) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p33) ).
fof(f32_nnf,plain,
! [B] :
( ! [C] :
( ! [D] :
( range(B,C,D) = range_of(D)
| ~ ilf_type(D,relation_type(B,C)) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [B,C,D] :
( range(B,C,D) = range_of(D)
| ~ ilf_type(D,relation_type(B,C))
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c69,plain,
( range(X0,X1,X2) = range_of(X2)
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p536,plain,
( range(X2,X0,X1) = range_of(X1)
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c69,c73]) ).
cnf(p2179,plain,
( range(X1,X2,X0) = range_of(X0)
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(resolution,[status(thm)],[p536,c73]) ).
cnf(p29456,plain,
range(sk15,sk14,inverse(sk16)) = domain_of(sk16),
inference(resolution,[status(thm)],[p29448,p2179]) ).
fof(f30,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> domain(B,C,D) = domain_of(D) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p31) ).
fof(f30_nnf,plain,
! [B] :
( ! [C] :
( ! [D] :
( domain(B,C,D) = domain_of(D)
| ~ ilf_type(D,relation_type(B,C)) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [B,C,D] :
( domain(B,C,D) = domain_of(D)
| ~ ilf_type(D,relation_type(B,C))
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c67,plain,
( domain(X0,X1,X2) = domain_of(X2)
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p528,plain,
( domain(X2,X0,X1) = domain_of(X1)
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c67,c73]) ).
cnf(p2147,plain,
( domain(X1,X2,X0) = domain_of(X0)
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(resolution,[status(thm)],[p528,c73]) ).
cnf(p29453,plain,
domain(sk15,sk14,inverse(sk16)) = range_of(sk16),
inference(resolution,[status(thm)],[p29448,p2147]) ).
fof(f34,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> inverse3(B,C,D) = inverse(D) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p35) ).
fof(f34_nnf,plain,
! [B] :
( ! [C] :
( ! [D] :
( inverse3(B,C,D) = inverse(D)
| ~ ilf_type(D,relation_type(B,C)) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [B,C,D] :
( inverse3(B,C,D) = inverse(D)
| ~ ilf_type(D,relation_type(B,C))
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c71,plain,
( inverse3(X0,X1,X2) = inverse(X2)
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p570,plain,
( inverse3(X2,X0,X1) = inverse(X1)
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c71,c73]) ).
cnf(p2291,plain,
( inverse3(X1,X2,X0) = inverse(X0)
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(resolution,[status(thm)],[p570,c73]) ).
cnf(p29337,plain,
inverse3(sk14,sk15,sk16) = inverse(sk16),
inference(resolution,[status(thm)],[p2291,c76]) ).
cnf(p28639,plain,
range(sk14,sk15,sk16) = range_of(sk16),
inference(resolution,[status(thm)],[p2179,c76]) ).
cnf(p28246,plain,
domain(sk14,sk15,sk16) = domain_of(sk16),
inference(resolution,[status(thm)],[p2147,c76]) ).
cnf(c77,plain,
( range(sk15,sk14,inverse3(sk14,sk15,sk16)) != domain(sk14,sk15,sk16)
| domain(sk15,sk14,inverse3(sk14,sk15,sk16)) != range(sk14,sk15,sk16) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p28247,plain,
( range(sk15,sk14,inverse3(sk14,sk15,sk16)) != domain_of(sk16)
| domain(sk15,sk14,inverse3(sk14,sk15,sk16)) != range(sk14,sk15,sk16) ),
inference(demodulation,[status(thm)],[p28246,c77]) ).
cnf(p28640,plain,
( range(sk15,sk14,inverse3(sk14,sk15,sk16)) != domain_of(sk16)
| domain(sk15,sk14,inverse3(sk14,sk15,sk16)) != range_of(sk16) ),
inference(demodulation,[status(thm)],[p28639,p28247]) ).
cnf(p29338,plain,
( range(sk15,sk14,inverse(sk16)) != domain_of(sk16)
| domain(sk15,sk14,inverse(sk16)) != range_of(sk16) ),
inference(demodulation,[status(thm)],[p29337,p28640]) ).
cnf(p29454,plain,
( range(sk15,sk14,inverse(sk16)) != domain_of(sk16)
| range_of(sk16) != range_of(sk16) ),
inference(demodulation,[status(thm)],[p29453,p29338]) ).
cnf(p29457,plain,
( domain_of(sk16) != domain_of(sk16)
| range_of(sk16) != range_of(sk16) ),
inference(demodulation,[status(thm)],[p29456,p29454]) ).
cnf(p29614,plain,
domain_of(sk16) != domain_of(sk16),
inference(equality_resolution,[status(thm)],[p29457]) ).
cnf(p29616,plain,
$false,
inference(equality_resolution,[status(thm)],[p29614]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET661+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n016.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Thu Sep 24 11:41:05 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 141.81/23.37 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 141.81/23.37 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------