%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SET667+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Sun Sep 27 08:36:46 AM UTC 2026
% Result : Theorem 227.34s 55.33s
% Output : CNFRefutation 227.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 10
% Syntax : Number of formulae : 73 ( 14 unt; 0 def)
% Number of atoms : 255 ( 10 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 303 ( 121 ~; 121 |; 24 &)
% ( 3 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 153 ( 12 sgn 46 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(p1,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,binary_relation_type)
=> ( member(ordered_pair(B,C),D)
=> ( member(C,range_of(D))
& member(B,domain_of(D)) ) ) ) ) ),
file('theBenchmark.p',p1) ).
fof(p2,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( member(C,B)
<=> member(ordered_pair(C,C),identity_relation_of(B)) ) ) ),
file('theBenchmark.p',p2) ).
fof(p5,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( ! [E] :
( ilf_type(E,relation_type(B,C))
=> ilf_type(E,subset_type(cross_product(B,C))) )
& ! [D] :
( ilf_type(D,subset_type(cross_product(B,C)))
=> ilf_type(D,relation_type(B,C)) ) ) ) ),
file('theBenchmark.p',p5) ).
fof(p7,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( subset(B,C)
<=> ! [D] :
( ilf_type(D,set_type)
=> ( member(D,B)
=> member(D,C) ) ) ) ) ),
file('theBenchmark.p',p7) ).
fof(p13,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( ilf_type(B,binary_relation_type)
<=> ( ilf_type(B,set_type)
& relation_like(B) ) ) ),
file('theBenchmark.p',p13) ).
fof(p24,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,subset_type(cross_product(B,C)))
=> relation_like(D) ) ) ),
file('theBenchmark.p',p24) ).
fof(p27,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('theBenchmark.p',p27) ).
fof(p29,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('theBenchmark.p',p29) ).
fof(p31,axiom,
! [B] : ilf_type(B,set_type),
file('theBenchmark.p',p31) ).
fof(prove_relset_1_30,conjecture,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ( subset(identity_relation_of(D),E)
=> ( subset(D,range(B,C,E))
& subset(D,domain(B,C,E)) ) ) ) ) ) ),
file('theBenchmark.p',prove_relset_1_30) ).
fof(prove_relset_1_30_neg,negated_conjecture,
~ ! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ( subset(identity_relation_of(D),E)
=> ( subset(D,range(B,C,E))
& subset(D,domain(B,C,E)) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[prove_relset_1_30]) ).
cnf(c_33,plain,
( ~ relation_like(A)
| ilf_type(A,binary_relation_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p13]) ).
cnf(c_41,plain,
( relation_like(C)
| ~ ilf_type(C,subset_type(cross_product(A,B)))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p24]) ).
cnf(c_47,plain,
( ilf_type(C,binary_relation_type)
| ~ ilf_type(C,set_type)
| ~ ilf_type(C,subset_type(cross_product(A,B)))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_41,c_33]) ).
fof(nnf_32,plain,
? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ( ~ subset(D,range(B,C,E))
| ~ subset(D,domain(B,C,E)) )
& subset(identity_relation_of(D),E)
& ilf_type(E,relation_type(B,C)) )
& ilf_type(D,set_type) )
& ilf_type(C,set_type) )
& ilf_type(B,set_type) ),
inference(fof_nnf,[status(thm)],[prove_relset_1_30_neg]) ).
fof(sk_prove_relset_1_30_neg,plain,
( ( ~ subset(sK0,range(sK1,sK2,sK3))
| ~ subset(sK0,domain(sK1,sK2,sK3)) )
& subset(identity_relation_of(sK0),sK3)
& ilf_type(sK3,relation_type(sK1,sK2))
& ilf_type(sK0,set_type)
& ilf_type(sK2,set_type)
& ilf_type(sK1,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK0,sK3]),skolemize(B,sK1),skolemize(C,sK2),skolemize(D,sK0),skolemize(E,sK3)],[nnf_32]) ).
cnf(c_59,negated_conjecture,
( ~ subset(sK0,range(sK1,sK2,sK3))
| ~ subset(sK0,domain(sK1,sK2,sK3)) ),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_30_neg]) ).
cnf(c_60,negated_conjecture,
subset(identity_relation_of(sK0),sK3),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_30_neg]) ).
cnf(c_61,negated_conjecture,
ilf_type(sK3,relation_type(sK1,sK2)),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_30_neg]) ).
cnf(c_65,plain,
ilf_type(A,set_type),
inference(clausify,[status(thm)],[p31]) ).
cnf(c_68,plain,
( range(A,B,C) = range_of(C)
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p29]) ).
cnf(c_22643,plain,
( range(C,A,B) = range_of(B)
| ~ ilf_type(B,relation_type(C,A))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_65,c_68]) ).
cnf(c_69,plain,
( range(B,C,A) = range_of(A)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_65,c_22643]) ).
cnf(c_72,plain,
( domain(A,B,C) = domain_of(C)
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p27]) ).
cnf(c_22644,plain,
( domain(C,A,B) = domain_of(B)
| ~ ilf_type(B,relation_type(C,A))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_65,c_72]) ).
cnf(c_73,plain,
( domain(B,C,A) = domain_of(A)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_65,c_22644]) ).
fof(nnf_7,plain,
! [B] :
( ! [C] :
( ( ( ? [D] :
( ~ member(D,C)
& member(D,B)
& ilf_type(D,set_type) )
| subset(B,C) )
& ( ! [X0] :
( member(X0,C)
| ~ member(X0,B)
| ~ ilf_type(X0,set_type) )
| ~ subset(B,C) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(fof_nnf,[status(thm)],[p7]) ).
fof(sk_p7_sk,plain,
! [B] :
( ! [C] :
( ( ( ( ~ member(sK4(B,C),C)
& member(sK4(B,C),B)
& ilf_type(sK4(B,C),set_type) )
| subset(B,C) )
& ( ! [X0] :
( member(X0,C)
| ~ member(X0,B)
| ~ ilf_type(X0,set_type) )
| ~ subset(B,C) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(D,sK4(B,C))],[nnf_7]) ).
fof(sk_p7,plain,
( ! [VAR_0,VAR_1] :
( ~ member(sK4(VAR_0,VAR_1),VAR_1)
| subset(VAR_0,VAR_1)
| ~ ilf_type(VAR_1,set_type)
| ~ ilf_type(VAR_0,set_type) )
& ! [VAR_0,VAR_1] :
( member(sK4(VAR_0,VAR_1),VAR_0)
| subset(VAR_0,VAR_1)
| ~ ilf_type(VAR_1,set_type)
| ~ ilf_type(VAR_0,set_type) )
& ! [VAR_0,VAR_1] :
( ilf_type(sK4(VAR_0,VAR_1),set_type)
| subset(VAR_0,VAR_1)
| ~ ilf_type(VAR_1,set_type)
| ~ ilf_type(VAR_0,set_type) )
& ! [VAR_0,VAR_1,VAR_2] :
( member(VAR_2,VAR_1)
| ~ member(VAR_2,VAR_0)
| ~ ilf_type(VAR_2,set_type)
| ~ subset(VAR_0,VAR_1)
| ~ ilf_type(VAR_1,set_type)
| ~ ilf_type(VAR_0,set_type) ) ),
inference(cnf_transformation,[status(thm)],[sk_p7_sk]) ).
cnf(c_111,plain,
( ~ member(sK4(A,B),B)
| subset(A,B)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(split_conjunct,[status(thm)],[sk_p7]) ).
cnf(c_22645,plain,
( ~ member(sK4(B,A),A)
| subset(B,A)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_65,c_111]) ).
cnf(c_112,plain,
( ~ member(sK4(A,B),B)
| subset(A,B) ),
inference(resolve,[status(thm)],[c_65,c_22645]) ).
cnf(c_113,plain,
( member(sK4(A,B),A)
| subset(A,B)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(split_conjunct,[status(thm)],[sk_p7]) ).
cnf(c_22646,plain,
( member(sK4(B,A),B)
| subset(B,A)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_65,c_113]) ).
cnf(c_114,plain,
( member(sK4(A,B),A)
| subset(A,B) ),
inference(resolve,[status(thm)],[c_65,c_22646]) ).
cnf(c_116,plain,
( member(C,B)
| ~ member(C,A)
| ~ ilf_type(C,set_type)
| ~ subset(A,B)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(split_conjunct,[status(thm)],[sk_p7]) ).
cnf(c_22647,plain,
( member(C,A)
| ~ member(C,B)
| ~ ilf_type(C,set_type)
| ~ subset(B,A)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_65,c_116]) ).
cnf(c_22648,plain,
( member(C,B)
| ~ member(C,A)
| ~ ilf_type(C,set_type)
| ~ subset(A,B) ),
inference(resolve,[status(thm)],[c_65,c_22647]) ).
cnf(c_117,plain,
( member(C,B)
| ~ member(C,A)
| ~ subset(A,B) ),
inference(resolve,[status(thm)],[c_65,c_22648]) ).
cnf(c_120,plain,
( ilf_type(C,subset_type(cross_product(A,B)))
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p5]) ).
cnf(c_22649,plain,
( ilf_type(B,subset_type(cross_product(C,A)))
| ~ ilf_type(B,relation_type(C,A))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_65,c_120]) ).
cnf(c_121,plain,
( ilf_type(A,subset_type(cross_product(B,C)))
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_65,c_22649]) ).
cnf(c_133,plain,
( member(ordered_pair(B,B),identity_relation_of(A))
| ~ member(B,A)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p2]) ).
cnf(c_22650,plain,
( member(ordered_pair(A,A),identity_relation_of(B))
| ~ member(A,B)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_65,c_133]) ).
cnf(c_134,plain,
( member(ordered_pair(A,A),identity_relation_of(B))
| ~ member(A,B) ),
inference(resolve,[status(thm)],[c_65,c_22650]) ).
cnf(c_135,plain,
( member(B,range_of(C))
| ~ member(ordered_pair(A,B),C)
| ~ ilf_type(C,binary_relation_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p1]) ).
cnf(c_22651,plain,
( member(A,range_of(B))
| ~ member(ordered_pair(C,A),B)
| ~ ilf_type(B,binary_relation_type)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_65,c_135]) ).
cnf(c_136,plain,
( member(C,range_of(A))
| ~ member(ordered_pair(B,C),A)
| ~ ilf_type(A,binary_relation_type) ),
inference(resolve,[status(thm)],[c_65,c_22651]) ).
cnf(c_137,plain,
( member(A,domain_of(C))
| ~ member(ordered_pair(A,B),C)
| ~ ilf_type(C,binary_relation_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p1]) ).
cnf(c_22652,plain,
( member(C,domain_of(B))
| ~ member(ordered_pair(C,A),B)
| ~ ilf_type(B,binary_relation_type)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_65,c_137]) ).
cnf(c_138,plain,
( member(B,domain_of(A))
| ~ member(ordered_pair(B,C),A)
| ~ ilf_type(A,binary_relation_type) ),
inference(resolve,[status(thm)],[c_65,c_22652]) ).
cnf(c_22653,plain,
( ilf_type(B,binary_relation_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(B,subset_type(cross_product(C,A)))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_65,c_47]) ).
cnf(c_22654,plain,
( ilf_type(A,binary_relation_type)
| ~ ilf_type(A,set_type)
| ~ ilf_type(A,subset_type(cross_product(B,C))) ),
inference(resolve,[status(thm)],[c_65,c_22653]) ).
cnf(c_165,plain,
( ilf_type(A,binary_relation_type)
| ~ ilf_type(A,subset_type(cross_product(B,C))) ),
inference(resolve,[status(thm)],[c_65,c_22654]) ).
cnf(c_169,plain,
range(sK1,sK2,sK3) = range_of(sK3),
inference(resolve,[status(thm)],[c_69,c_61]) ).
cnf(c_171,negated_conjecture,
( ~ subset(sK0,range_of(sK3))
| ~ subset(sK0,domain(sK1,sK2,sK3)) ),
inference(paramod,[status(thm)],[c_169,c_59]) ).
cnf(c_173,plain,
domain(sK1,sK2,sK3) = domain_of(sK3),
inference(resolve,[status(thm)],[c_73,c_61]) ).
cnf(c_175,negated_conjecture,
( ~ subset(sK0,range_of(sK3))
| ~ subset(sK0,domain_of(sK3)) ),
inference(paramod,[status(thm)],[c_173,c_171]) ).
cnf(c_207,plain,
( member(A,sK3)
| ~ member(A,identity_relation_of(sK0)) ),
inference(resolve,[status(thm)],[c_117,c_60]) ).
cnf(c_217,plain,
ilf_type(sK3,subset_type(cross_product(sK1,sK2))),
inference(resolve,[status(thm)],[c_121,c_61]) ).
cnf(c_227,plain,
( subset(A,B)
| member(ordered_pair(sK4(A,B),sK4(A,B)),identity_relation_of(A)) ),
inference(resolve,[status(thm)],[c_134,c_114]) ).
cnf(c_503,plain,
ilf_type(sK3,binary_relation_type),
inference(resolve,[status(thm)],[c_217,c_165]) ).
cnf(c_506,plain,
( member(A,domain_of(sK3))
| ~ member(ordered_pair(A,B),sK3) ),
inference(resolve,[status(thm)],[c_503,c_138]) ).
cnf(c_507,plain,
( member(B,range_of(sK3))
| ~ member(ordered_pair(A,B),sK3) ),
inference(resolve,[status(thm)],[c_503,c_136]) ).
cnf(c_964,plain,
( member(ordered_pair(sK4(sK0,A),sK4(sK0,A)),sK3)
| subset(sK0,A) ),
inference(resolve,[status(thm)],[c_227,c_207]) ).
cnf(c_22351,plain,
( member(sK4(sK0,A),range_of(sK3))
| subset(sK0,A) ),
inference(resolve,[status(thm)],[c_964,c_507]) ).
cnf(c_22655,plain,
( subset(sK0,range_of(sK3))
| subset(sK0,range_of(sK3)) ),
inference(resolve,[status(thm)],[c_22351,c_112]) ).
cnf(c_22411,plain,
subset(sK0,range_of(sK3)),
inference(copy,[status(thm)],[c_22655]) ).
cnf(c_22423,negated_conjecture,
~ subset(sK0,domain_of(sK3)),
inference(resolve,[status(thm)],[c_22411,c_175]) ).
cnf(c_22634,plain,
member(ordered_pair(sK4(sK0,domain_of(sK3)),sK4(sK0,domain_of(sK3))),sK3),
inference(resolve,[status(thm)],[c_22423,c_964]) ).
cnf(c_22636,negated_conjecture,
~ member(sK4(sK0,domain_of(sK3)),domain_of(sK3)),
inference(resolve,[status(thm)],[c_112,c_22423]) ).
cnf(c_22641,plain,
~ member(ordered_pair(sK4(sK0,domain_of(sK3)),A),sK3),
inference(resolve,[status(thm)],[c_506,c_22636]) ).
cnf(c_22642,plain,
$false,
inference(resolve,[status(thm)],[c_22641,c_22634]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET667+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.43 % Computer : n009.cluster.edu
% 0.10/0.43 % Model : x86_64 x86_64
% 0.10/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.43 % Memory : 8046.5625MB
% 0.10/0.43 % OS : Linux 6.8.0-71-generic
% 0.10/0.43 % CPULimit : 300
% 0.10/0.43 % WCLimit : 300
% 0.10/0.43 % DateTime : Sat Sep 26 08:04:15 UTC 2026
% 0.10/0.43 % CPUTime :
% 0.10/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.44 % Process 3780796 was started by sandbox on n009,
% 0.10/0.44 % Sat Sep 26 08:04:15 2026
% 0.10/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.45
% 0.10/0.45 % From the command line: assign(max_seconds, 300).
% 227.34/55.33
% 227.34/55.33 % given #500 (A,wt=57): 345 member(A,power_set(power_set(B))) | member(f10(f6(A,power_set(B))),f6(A,power_set(B))) | ordered_pair(f8(f6(A,power_set(B)),f6(f6(A,power_set(B)),B)),f9(f6(A,power_set(B)),f6(f6(A,power_set(B)),B))) = f6(f6(A,power_set(B)),B). [resolve(182,a,160,b)].
% 227.34/55.33
% 227.34/55.33 % given #1000 (T,wt=12): 13732 empty(f11(power_set(A))) | -empty(A). [resolve(491,a,78,b)].
% 227.34/55.33
% 227.34/55.33 % given #1500 (F,wt=22): 10794 -empty(range_of(identity_relation_of(range_of(identity_relation_of(identity_relation_of(identity_relation_of(c4))))))). [ur(7934,a,8273,a)].
% 227.34/55.33
% 227.34/55.33 % given #2000 (A,wt=30): 835 subset(identity_relation_of(A),f1(B,C)) | member(ordered_pair(f3(identity_relation_of(A),f1(B,C)),f4(identity_relation_of(A),f1(B,C))),identity_relation_of(A)). [resolve(220,a,791,a)].
% 227.34/55.33
% 227.34/55.33 % SZS status Theorem for theBenchmark
% 227.34/55.33
% 227.34/55.33 % Proof 1 at 4.48 (+ 1.95) seconds.
% 227.34/55.33 % Length of proof is 54.
% 227.34/55.33 % Level of proof is 11.
% 227.34/55.33 % Maximum clause weight is 24.000.
% 227.34/55.33 % Given clauses 2412.
% 227.34/55.33
% 227.34/55.33 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------