%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SET684+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 : n020.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:49 AM UTC 2026
% Result : Theorem 2.66s 0.72s
% Output : CNFRefutation 2.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 9
% Syntax : Number of formulae : 83 ( 17 unt; 0 def)
% Number of atoms : 389 ( 7 equ)
% Maximal formula atoms : 26 ( 4 avg)
% Number of connectives : 517 ( 211 ~; 198 |; 64 &)
% ( 5 <=>; 39 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 10 con; 0-5 aty)
% Number of variables : 214 ( 13 sgn 69 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(p1,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,binary_relation_type)
=> ! [E] :
( ilf_type(E,binary_relation_type)
=> ( member(ordered_pair(B,C),compose(D,E))
<=> ? [F] :
( member(ordered_pair(F,C),E)
& member(ordered_pair(B,F),D)
& ilf_type(F,set_type) ) ) ) ) ) ),
file('theBenchmark.p',p1) ).
fof(p2,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,set_type)
=> ! [F] :
( ilf_type(F,relation_type(B,C))
=> ( member(ordered_pair(D,E),F)
=> ( member(E,C)
& member(D,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)
& ~ empty(C) )
=> ( ilf_type(B,member_type(C))
<=> member(B,C) ) ) ),
file('theBenchmark.p',p7) ).
fof(p15,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( ilf_type(B,binary_relation_type)
<=> ( ilf_type(B,set_type)
& relation_like(B) ) ) ),
file('theBenchmark.p',p15) ).
fof(p26,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',p26) ).
fof(p27,axiom,
! [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))
=> ! [F] :
( ilf_type(F,relation_type(C,D))
=> compose5(B,C,D,E,F) = compose(E,F) ) ) ) ) ),
file('theBenchmark.p',p27) ).
fof(p29,axiom,
! [B] : ilf_type(B,set_type),
file('theBenchmark.p',p29) ).
fof(prove_relset_1_51,conjecture,
! [B] :
( ( ilf_type(B,set_type)
& ~ empty(B) )
=> ! [C] :
( ( ilf_type(C,set_type)
& ~ empty(C) )
=> ! [D] :
( ( ilf_type(D,set_type)
& ~ empty(D) )
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ! [F] :
( ilf_type(F,relation_type(C,D))
=> ! [G] :
( ilf_type(G,member_type(B))
=> ! [H] :
( ilf_type(H,member_type(D))
=> ( member(ordered_pair(G,H),compose5(B,C,D,E,F))
<=> ? [I] :
( member(ordered_pair(I,H),F)
& member(ordered_pair(G,I),E)
& ilf_type(I,member_type(C)) ) ) ) ) ) ) ) ) ),
file('theBenchmark.p',prove_relset_1_51) ).
fof(prove_relset_1_51_neg,negated_conjecture,
~ ! [B] :
( ( ilf_type(B,set_type)
& ~ empty(B) )
=> ! [C] :
( ( ilf_type(C,set_type)
& ~ empty(C) )
=> ! [D] :
( ( ilf_type(D,set_type)
& ~ empty(D) )
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ! [F] :
( ilf_type(F,relation_type(C,D))
=> ! [G] :
( ilf_type(G,member_type(B))
=> ! [H] :
( ilf_type(H,member_type(D))
=> ( member(ordered_pair(G,H),compose5(B,C,D,E,F))
<=> ? [I] :
( member(ordered_pair(I,H),F)
& member(ordered_pair(G,I),E)
& ilf_type(I,member_type(C)) ) ) ) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[prove_relset_1_51]) ).
cnf(c_31,plain,
( ~ relation_like(A)
| ilf_type(A,binary_relation_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p15]) ).
cnf(c_40,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)],[p26]) ).
cnf(c_41,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_40,c_31]) ).
fof(nnf_30,plain,
? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ? [G] :
( ? [H] :
( ( ! [I] :
( ~ member(ordered_pair(I,H),F)
| ~ member(ordered_pair(G,I),E)
| ~ ilf_type(I,member_type(C)) )
| ~ member(ordered_pair(G,H),compose5(B,C,D,E,F)) )
& ( ? [X0] :
( member(ordered_pair(X0,H),F)
& member(ordered_pair(G,X0),E)
& ilf_type(X0,member_type(C)) )
| member(ordered_pair(G,H),compose5(B,C,D,E,F)) )
& ilf_type(H,member_type(D)) )
& ilf_type(G,member_type(B)) )
& ilf_type(F,relation_type(C,D)) )
& ilf_type(E,relation_type(B,C)) )
& ilf_type(D,set_type)
& ~ empty(D) )
& ilf_type(C,set_type)
& ~ empty(C) )
& ilf_type(B,set_type)
& ~ empty(B) ),
inference(fof_nnf,[status(thm)],[prove_relset_1_51_neg]) ).
fof(sk_prove_relset_1_51_neg_sk,plain,
( ( ! [I] :
( ~ member(ordered_pair(I,sK1),sK6)
| ~ member(ordered_pair(sK0,I),sK5)
| ~ ilf_type(I,member_type(sK3)) )
| ~ member(ordered_pair(sK0,sK1),compose5(sK2,sK3,sK4,sK5,sK6)) )
& ( ( member(ordered_pair(sK7,sK1),sK6)
& member(ordered_pair(sK0,sK7),sK5)
& ilf_type(sK7,member_type(sK3)) )
| member(ordered_pair(sK0,sK1),compose5(sK2,sK3,sK4,sK5,sK6)) )
& ilf_type(sK1,member_type(sK4))
& ilf_type(sK0,member_type(sK2))
& ilf_type(sK6,relation_type(sK3,sK4))
& ilf_type(sK5,relation_type(sK2,sK3))
& ilf_type(sK4,set_type)
& ~ empty(sK4)
& ilf_type(sK3,set_type)
& ~ empty(sK3)
& ilf_type(sK2,set_type)
& ~ empty(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK0,sK1,sK7]),skolemize(B,sK2),skolemize(C,sK3),skolemize(D,sK4),skolemize(E,sK5),skolemize(F,sK6),skolemize(G,sK0),skolemize(H,sK1),skolemize(X0,sK7)],[nnf_30]) ).
fof(sk_prove_relset_1_51_neg,plain,
( ! [VAR_0] :
( ~ member(ordered_pair(VAR_0,sK1),sK6)
| ~ member(ordered_pair(sK0,VAR_0),sK5)
| ~ ilf_type(VAR_0,member_type(sK3))
| ~ member(ordered_pair(sK0,sK1),compose5(sK2,sK3,sK4,sK5,sK6)) )
& ( member(ordered_pair(sK7,sK1),sK6)
| member(ordered_pair(sK0,sK1),compose5(sK2,sK3,sK4,sK5,sK6)) )
& ( member(ordered_pair(sK0,sK7),sK5)
| member(ordered_pair(sK0,sK1),compose5(sK2,sK3,sK4,sK5,sK6)) )
& ( ilf_type(sK7,member_type(sK3))
| member(ordered_pair(sK0,sK1),compose5(sK2,sK3,sK4,sK5,sK6)) )
& ilf_type(sK1,member_type(sK4))
& ilf_type(sK0,member_type(sK2))
& ilf_type(sK6,relation_type(sK3,sK4))
& ilf_type(sK5,relation_type(sK2,sK3))
& ilf_type(sK4,set_type)
& ~ empty(sK4)
& ilf_type(sK3,set_type)
& ~ empty(sK3)
& ilf_type(sK2,set_type)
& ~ empty(sK2) ),
inference(cnf_transformation,[status(thm)],[sk_prove_relset_1_51_neg_sk]) ).
cnf(c_57,negated_conjecture,
( ~ member(ordered_pair(A,sK1),sK6)
| ~ member(ordered_pair(sK0,A),sK5)
| ~ ilf_type(A,member_type(sK3))
| ~ member(ordered_pair(sK0,sK1),compose5(sK2,sK3,sK4,sK5,sK6)) ),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_51_neg]) ).
cnf(c_58,negated_conjecture,
( member(ordered_pair(sK7,sK1),sK6)
| member(ordered_pair(sK0,sK1),compose5(sK2,sK3,sK4,sK5,sK6)) ),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_51_neg]) ).
cnf(c_59,negated_conjecture,
( member(ordered_pair(sK0,sK7),sK5)
| member(ordered_pair(sK0,sK1),compose5(sK2,sK3,sK4,sK5,sK6)) ),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_51_neg]) ).
cnf(c_63,negated_conjecture,
ilf_type(sK6,relation_type(sK3,sK4)),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_51_neg]) ).
cnf(c_64,negated_conjecture,
ilf_type(sK5,relation_type(sK2,sK3)),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_51_neg]) ).
cnf(c_68,negated_conjecture,
~ empty(sK3),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_51_neg]) ).
cnf(c_71,plain,
ilf_type(A,set_type),
inference(clausify,[status(thm)],[p29]) ).
cnf(c_74,plain,
( compose5(A,B,C,D,E) = compose(D,E)
| ~ ilf_type(E,relation_type(B,C))
| ~ ilf_type(D,relation_type(A,B))
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p27]) ).
cnf(c_2227,plain,
( compose5(D,A,B,C,E) = compose(C,E)
| ~ ilf_type(E,relation_type(A,B))
| ~ ilf_type(C,relation_type(D,A))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_71,c_74]) ).
cnf(c_2228,plain,
( compose5(C,D,A,B,E) = compose(B,E)
| ~ ilf_type(E,relation_type(D,A))
| ~ ilf_type(B,relation_type(C,D))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_71,c_2227]) ).
cnf(c_75,plain,
( compose5(B,C,E,A,D) = compose(A,D)
| ~ ilf_type(D,relation_type(C,E))
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_71,c_2228]) ).
cnf(c_115,plain,
( ~ member(A,B)
| ilf_type(A,member_type(B))
| ~ ilf_type(B,set_type)
| empty(B)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p7]) ).
cnf(c_2229,plain,
( ~ member(B,A)
| ilf_type(B,member_type(A))
| ~ ilf_type(A,set_type)
| empty(A) ),
inference(resolve,[status(thm)],[c_71,c_115]) ).
cnf(c_116,plain,
( ~ member(B,A)
| ilf_type(B,member_type(A))
| empty(A) ),
inference(resolve,[status(thm)],[c_71,c_2229]) ).
cnf(c_121,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_2230,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_71,c_121]) ).
cnf(c_122,plain,
( ilf_type(A,subset_type(cross_product(B,C)))
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_71,c_2230]) ).
cnf(c_130,plain,
( member(D,B)
| ~ member(ordered_pair(C,D),E)
| ~ ilf_type(E,relation_type(A,B))
| ~ ilf_type(D,set_type)
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p2]) ).
cnf(c_2231,plain,
( member(C,A)
| ~ member(ordered_pair(B,C),D)
| ~ ilf_type(D,relation_type(E,A))
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_71,c_130]) ).
cnf(c_2232,plain,
( member(B,E)
| ~ member(ordered_pair(A,B),C)
| ~ ilf_type(C,relation_type(D,E))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_71,c_2231]) ).
cnf(c_2233,plain,
( member(A,D)
| ~ member(ordered_pair(E,A),B)
| ~ ilf_type(B,relation_type(C,D))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_71,c_2232]) ).
cnf(c_131,plain,
( member(E,C)
| ~ member(ordered_pair(D,E),A)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_71,c_2233]) ).
fof(nnf_1,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ( ( ! [F] :
( ~ member(ordered_pair(F,C),E)
| ~ member(ordered_pair(B,F),D)
| ~ ilf_type(F,set_type) )
| member(ordered_pair(B,C),compose(D,E)) )
& ( ? [X0] :
( member(ordered_pair(X0,C),E)
& member(ordered_pair(B,X0),D)
& ilf_type(X0,set_type) )
| ~ member(ordered_pair(B,C),compose(D,E)) ) )
| ~ ilf_type(E,binary_relation_type) )
| ~ ilf_type(D,binary_relation_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(fof_nnf,[status(thm)],[p1]) ).
fof(sk_p1_sk,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ( ( ! [F] :
( ~ member(ordered_pair(F,C),E)
| ~ member(ordered_pair(B,F),D)
| ~ ilf_type(F,set_type) )
| member(ordered_pair(B,C),compose(D,E)) )
& ( ( member(ordered_pair(sK8(B,C,D,E),C),E)
& member(ordered_pair(B,sK8(B,C,D,E)),D)
& ilf_type(sK8(B,C,D,E),set_type) )
| ~ member(ordered_pair(B,C),compose(D,E)) ) )
| ~ ilf_type(E,binary_relation_type) )
| ~ ilf_type(D,binary_relation_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X0,sK8(B,C,D,E))],[nnf_1]) ).
fof(sk_p1,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ member(ordered_pair(VAR_4,VAR_1),VAR_3)
| ~ member(ordered_pair(VAR_0,VAR_4),VAR_2)
| ~ ilf_type(VAR_4,set_type)
| member(ordered_pair(VAR_0,VAR_1),compose(VAR_2,VAR_3))
| ~ ilf_type(VAR_3,binary_relation_type)
| ~ ilf_type(VAR_2,binary_relation_type)
| ~ ilf_type(VAR_1,set_type)
| ~ ilf_type(VAR_0,set_type) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( member(ordered_pair(sK8(VAR_0,VAR_1,VAR_2,VAR_3),VAR_1),VAR_3)
| ~ member(ordered_pair(VAR_0,VAR_1),compose(VAR_2,VAR_3))
| ~ ilf_type(VAR_3,binary_relation_type)
| ~ ilf_type(VAR_2,binary_relation_type)
| ~ ilf_type(VAR_1,set_type)
| ~ ilf_type(VAR_0,set_type) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( member(ordered_pair(VAR_0,sK8(VAR_0,VAR_1,VAR_2,VAR_3)),VAR_2)
| ~ member(ordered_pair(VAR_0,VAR_1),compose(VAR_2,VAR_3))
| ~ ilf_type(VAR_3,binary_relation_type)
| ~ ilf_type(VAR_2,binary_relation_type)
| ~ ilf_type(VAR_1,set_type)
| ~ ilf_type(VAR_0,set_type) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ilf_type(sK8(VAR_0,VAR_1,VAR_2,VAR_3),set_type)
| ~ member(ordered_pair(VAR_0,VAR_1),compose(VAR_2,VAR_3))
| ~ ilf_type(VAR_3,binary_relation_type)
| ~ ilf_type(VAR_2,binary_relation_type)
| ~ ilf_type(VAR_1,set_type)
| ~ ilf_type(VAR_0,set_type) ) ),
inference(cnf_transformation,[status(thm)],[sk_p1_sk]) ).
cnf(c_134,plain,
( ~ member(ordered_pair(E,B),D)
| ~ member(ordered_pair(A,E),C)
| ~ ilf_type(E,set_type)
| member(ordered_pair(A,B),compose(C,D))
| ~ ilf_type(D,binary_relation_type)
| ~ ilf_type(C,binary_relation_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(split_conjunct,[status(thm)],[sk_p1]) ).
cnf(c_2234,plain,
( ~ member(ordered_pair(E,A),C)
| ~ member(ordered_pair(D,E),B)
| ~ ilf_type(E,set_type)
| member(ordered_pair(D,A),compose(B,C))
| ~ ilf_type(C,binary_relation_type)
| ~ ilf_type(B,binary_relation_type)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_71,c_134]) ).
cnf(c_2235,plain,
( ~ member(ordered_pair(E,D),B)
| ~ member(ordered_pair(C,E),A)
| ~ ilf_type(E,set_type)
| member(ordered_pair(C,D),compose(A,B))
| ~ ilf_type(B,binary_relation_type)
| ~ ilf_type(A,binary_relation_type) ),
inference(resolve,[status(thm)],[c_71,c_2234]) ).
cnf(c_135,plain,
( ~ member(ordered_pair(E,D),B)
| ~ member(ordered_pair(C,E),A)
| member(ordered_pair(C,D),compose(A,B))
| ~ ilf_type(B,binary_relation_type)
| ~ ilf_type(A,binary_relation_type) ),
inference(resolve,[status(thm)],[c_71,c_2235]) ).
cnf(c_136,plain,
( member(ordered_pair(sK8(A,B,C,D),B),D)
| ~ member(ordered_pair(A,B),compose(C,D))
| ~ ilf_type(D,binary_relation_type)
| ~ ilf_type(C,binary_relation_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(split_conjunct,[status(thm)],[sk_p1]) ).
cnf(c_2236,plain,
( member(ordered_pair(sK8(D,A,B,C),A),C)
| ~ member(ordered_pair(D,A),compose(B,C))
| ~ ilf_type(C,binary_relation_type)
| ~ ilf_type(B,binary_relation_type)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_71,c_136]) ).
cnf(c_137,plain,
( member(ordered_pair(sK8(C,D,A,B),D),B)
| ~ member(ordered_pair(C,D),compose(A,B))
| ~ ilf_type(B,binary_relation_type)
| ~ ilf_type(A,binary_relation_type) ),
inference(resolve,[status(thm)],[c_71,c_2236]) ).
cnf(c_138,plain,
( member(ordered_pair(A,sK8(A,B,C,D)),C)
| ~ member(ordered_pair(A,B),compose(C,D))
| ~ ilf_type(D,binary_relation_type)
| ~ ilf_type(C,binary_relation_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(split_conjunct,[status(thm)],[sk_p1]) ).
cnf(c_2237,plain,
( member(ordered_pair(D,sK8(D,A,B,C)),B)
| ~ member(ordered_pair(D,A),compose(B,C))
| ~ ilf_type(C,binary_relation_type)
| ~ ilf_type(B,binary_relation_type)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_71,c_138]) ).
cnf(c_139,plain,
( member(ordered_pair(C,sK8(C,D,A,B)),A)
| ~ member(ordered_pair(C,D),compose(A,B))
| ~ ilf_type(B,binary_relation_type)
| ~ ilf_type(A,binary_relation_type) ),
inference(resolve,[status(thm)],[c_71,c_2237]) ).
cnf(c_2238,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_71,c_41]) ).
cnf(c_2239,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_71,c_2238]) ).
cnf(c_168,plain,
( ilf_type(A,binary_relation_type)
| ~ ilf_type(A,subset_type(cross_product(B,C))) ),
inference(resolve,[status(thm)],[c_71,c_2239]) ).
cnf(c_182,plain,
( compose5(sK2,sK3,B,sK5,A) = compose(sK5,A)
| ~ ilf_type(A,relation_type(sK3,B)) ),
inference(resolve,[status(thm)],[c_75,c_64]) ).
cnf(c_243,plain,
ilf_type(sK5,subset_type(cross_product(sK2,sK3))),
inference(resolve,[status(thm)],[c_122,c_64]) ).
cnf(c_244,plain,
ilf_type(sK6,subset_type(cross_product(sK3,sK4))),
inference(resolve,[status(thm)],[c_122,c_63]) ).
cnf(c_250,plain,
( member(B,sK3)
| ~ member(ordered_pair(A,B),sK5) ),
inference(resolve,[status(thm)],[c_131,c_64]) ).
cnf(c_268,plain,
( member(ordered_pair(sK0,sK1),compose5(sK2,sK3,sK4,sK5,sK6))
| ~ member(ordered_pair(B,sK7),A)
| member(ordered_pair(B,sK1),compose(A,sK6))
| ~ ilf_type(sK6,binary_relation_type)
| ~ ilf_type(A,binary_relation_type) ),
inference(resolve,[status(thm)],[c_135,c_58]) ).
cnf(c_370,plain,
compose5(sK2,sK3,sK4,sK5,sK6) = compose(sK5,sK6),
inference(resolve,[status(thm)],[c_182,c_63]) ).
cnf(c_391,plain,
( member(ordered_pair(sK0,sK1),compose(sK5,sK6))
| ~ member(ordered_pair(B,sK7),A)
| member(ordered_pair(B,sK1),compose(A,sK6))
| ~ ilf_type(sK6,binary_relation_type)
| ~ ilf_type(A,binary_relation_type) ),
inference(paramod,[status(thm)],[c_370,c_268]) ).
cnf(c_417,negated_conjecture,
( member(ordered_pair(sK0,sK7),sK5)
| member(ordered_pair(sK0,sK1),compose(sK5,sK6)) ),
inference(paramod,[status(thm)],[c_370,c_59]) ).
cnf(c_419,negated_conjecture,
( ~ member(ordered_pair(A,sK1),sK6)
| ~ member(ordered_pair(sK0,A),sK5)
| ~ ilf_type(A,member_type(sK3))
| ~ member(ordered_pair(sK0,sK1),compose(sK5,sK6)) ),
inference(paramod,[status(thm)],[c_370,c_57]) ).
cnf(c_420,plain,
( ~ member(ordered_pair(sK0,sK7),sK5)
| member(ordered_pair(sK0,sK1),compose(sK5,sK6))
| ~ ilf_type(sK6,binary_relation_type)
| ~ ilf_type(sK5,binary_relation_type) ),
inference(factor,[status(thm)],[c_391]) ).
cnf(c_560,plain,
ilf_type(sK5,binary_relation_type),
inference(resolve,[status(thm)],[c_243,c_168]) ).
cnf(c_564,plain,
( ~ member(ordered_pair(sK0,sK7),sK5)
| member(ordered_pair(sK0,sK1),compose(sK5,sK6))
| ~ ilf_type(sK6,binary_relation_type) ),
inference(resolve,[status(thm)],[c_560,c_420]) ).
cnf(c_770,plain,
ilf_type(sK6,binary_relation_type),
inference(resolve,[status(thm)],[c_244,c_168]) ).
cnf(c_773,plain,
( ~ member(ordered_pair(sK0,sK7),sK5)
| member(ordered_pair(sK0,sK1),compose(sK5,sK6)) ),
inference(resolve,[status(thm)],[c_770,c_564]) ).
cnf(c_2240,negated_conjecture,
( member(ordered_pair(sK0,sK1),compose(sK5,sK6))
| member(ordered_pair(sK0,sK1),compose(sK5,sK6)) ),
inference(resolve,[status(thm)],[c_773,c_417]) ).
cnf(c_1370,negated_conjecture,
member(ordered_pair(sK0,sK1),compose(sK5,sK6)),
inference(copy,[status(thm)],[c_2240]) ).
cnf(c_1373,negated_conjecture,
( ~ member(ordered_pair(A,sK1),sK6)
| ~ member(ordered_pair(sK0,A),sK5)
| ~ ilf_type(A,member_type(sK3)) ),
inference(resolve,[status(thm)],[c_1370,c_419]) ).
cnf(c_2241,plain,
( member(ordered_pair(sK0,sK8(sK0,sK1,sK5,sK6)),sK5)
| ~ ilf_type(sK6,binary_relation_type)
| ~ ilf_type(sK5,binary_relation_type) ),
inference(resolve,[status(thm)],[c_1370,c_139]) ).
cnf(c_2242,plain,
( member(ordered_pair(sK0,sK8(sK0,sK1,sK5,sK6)),sK5)
| ~ ilf_type(sK6,binary_relation_type) ),
inference(resolve,[status(thm)],[c_560,c_2241]) ).
cnf(c_1383,plain,
member(ordered_pair(sK0,sK8(sK0,sK1,sK5,sK6)),sK5),
inference(resolve,[status(thm)],[c_770,c_2242]) ).
cnf(c_2243,plain,
( member(ordered_pair(sK8(sK0,sK1,sK5,sK6),sK1),sK6)
| ~ ilf_type(sK6,binary_relation_type)
| ~ ilf_type(sK5,binary_relation_type) ),
inference(resolve,[status(thm)],[c_1370,c_137]) ).
cnf(c_2244,plain,
( member(ordered_pair(sK8(sK0,sK1,sK5,sK6),sK1),sK6)
| ~ ilf_type(sK6,binary_relation_type) ),
inference(resolve,[status(thm)],[c_560,c_2243]) ).
cnf(c_1384,plain,
member(ordered_pair(sK8(sK0,sK1,sK5,sK6),sK1),sK6),
inference(resolve,[status(thm)],[c_770,c_2244]) ).
cnf(c_2245,negated_conjecture,
( ~ member(ordered_pair(sK8(sK0,sK1,sK5,sK6),sK1),sK6)
| ~ ilf_type(sK8(sK0,sK1,sK5,sK6),member_type(sK3)) ),
inference(resolve,[status(thm)],[c_1383,c_1373]) ).
cnf(c_2200,negated_conjecture,
~ ilf_type(sK8(sK0,sK1,sK5,sK6),member_type(sK3)),
inference(resolve,[status(thm)],[c_1384,c_2245]) ).
cnf(c_2204,plain,
member(sK8(sK0,sK1,sK5,sK6),sK3),
inference(resolve,[status(thm)],[c_1383,c_250]) ).
cnf(c_2246,negated_conjecture,
( ~ member(A,sK3)
| ilf_type(A,member_type(sK3)) ),
inference(resolve,[status(thm)],[c_116,c_68]) ).
cnf(c_2247,negated_conjecture,
~ member(sK8(sK0,sK1,sK5,sK6),sK3),
inference(resolve,[status(thm)],[c_2246,c_2200]) ).
cnf(c_2226,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_2204,c_2247]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET684+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n020.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 26 08:05:50 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.35 % Process 1040186 was started by sandbox on n020,
% 0.07/0.35 % Sat Sep 26 08:05:50 2026
% 0.07/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.36
% 0.11/0.36 % From the command line: assign(max_seconds, 300).
% 2.66/0.72
% 2.66/0.72 % SZS status Theorem for theBenchmark
% 2.66/0.72
% 2.66/0.72 % Proof 1 at 0.29 (+ 0.06) seconds.
% 2.66/0.72 % Length of proof is 55.
% 2.66/0.72 % Level of proof is 12.
% 2.66/0.72 % Maximum clause weight is 38.000.
% 2.66/0.72 % Given clauses 287.
% 2.66/0.72
% 2.66/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------