%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU210+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:45:25 AM UTC 2026
% Result : Theorem 1.76s 0.70s
% Output : CNFRefutation 1.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of formulae : 83 ( 36 unt; 0 def)
% Number of atoms : 210 ( 39 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 218 ( 91 ~; 83 |; 32 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-3 aty)
% Number of variables : 137 ( 5 sgn 65 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('theBenchmark.p',commutativity_k2_tarski) ).
fof(d3_tarski,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('theBenchmark.p',d3_tarski) ).
fof(d5_relat_1,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) ) ),
file('theBenchmark.p',d5_relat_1) ).
fof(d5_tarski,axiom,
! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
file('theBenchmark.p',d5_tarski) ).
fof(existence_m1_subset_1,axiom,
! [A] :
? [B] : element(B,A),
file('theBenchmark.p',existence_m1_subset_1) ).
fof(rc1_relat_1,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('theBenchmark.p',rc1_relat_1) ).
fof(rc1_xboole_0,axiom,
? [A] : empty(A),
file('theBenchmark.p',rc1_xboole_0) ).
fof(reflexivity_r1_tarski,axiom,
! [A,B] : subset(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(t166_relat_1,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('theBenchmark.p',t166_relat_1) ).
fof(t2_subset,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t3_subset,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t5_subset,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('theBenchmark.p',t5_subset) ).
fof(t6_boole,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('theBenchmark.p',t6_boole) ).
fof(t174_relat_1,conjecture,
! [A,B] :
( relation(B)
=> ~ ( relation_inverse_image(B,A) = empty_set
& subset(A,relation_rng(B))
& A != empty_set ) ),
file('theBenchmark.p',t174_relat_1) ).
fof(t174_relat_1_neg,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> ~ ( relation_inverse_image(B,A) = empty_set
& subset(A,relation_rng(B))
& A != empty_set ) ),
inference(assume_negation,[status(cth)],[t174_relat_1]) ).
fof(nnf_5,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ! [D] : ~ in(ordered_pair(D,C),A)
| ~ in(C,B) )
& ( ? [X3] : in(ordered_pair(X3,C),A)
| in(C,B) ) )
| relation_rng(A) = B )
& ( ! [X0] :
( ( ! [X2] : ~ in(ordered_pair(X2,X0),A)
| in(X0,B) )
& ( ? [X1] : in(ordered_pair(X1,X0),A)
| ~ in(X0,B) ) )
| relation_rng(A) != B ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d5_relat_1]) ).
fof(sk_d5_relat_1_sk,plain,
! [A] :
( ! [B] :
( ( ( ( ! [D] : ~ in(ordered_pair(D,sK7(A,B)),A)
| ~ in(sK7(A,B),B) )
& ( in(ordered_pair(sK8(A,B),sK7(A,B)),A)
| in(sK7(A,B),B) ) )
| relation_rng(A) = B )
& ( ! [X0] :
( ( ! [X2] : ~ in(ordered_pair(X2,X0),A)
| in(X0,B) )
& ( in(ordered_pair(sK0(A,B,X0),X0),A)
| ~ in(X0,B) ) )
| relation_rng(A) != B ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK7,sK8]),skolemize(X1,sK0(A,B,X0)),skolemize(C,sK7(A,B)),skolemize(X3,sK8(A,B))],[nnf_5]) ).
fof(sk_d5_relat_1,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ in(ordered_pair(VAR_2,sK7(VAR_0,VAR_1)),VAR_0)
| ~ in(sK7(VAR_0,VAR_1),VAR_1)
| relation_rng(VAR_0) = VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(sK8(VAR_0,VAR_1),sK7(VAR_0,VAR_1)),VAR_0)
| in(sK7(VAR_0,VAR_1),VAR_1)
| relation_rng(VAR_0) = VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(ordered_pair(VAR_3,VAR_2),VAR_0)
| in(VAR_2,VAR_1)
| relation_rng(VAR_0) != VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(ordered_pair(sK0(VAR_0,VAR_1,VAR_2),VAR_2),VAR_0)
| ~ in(VAR_2,VAR_1)
| relation_rng(VAR_0) != VAR_1
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d5_relat_1_sk]) ).
cnf(c_40,plain,
( in(ordered_pair(sK0(A,B,C),C),A)
| ~ in(C,B)
| relation_rng(A) != B
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d5_relat_1]) ).
cnf(c_53,plain,
( ~ in(D,C)
| ~ in(ordered_pair(B,D),A)
| ~ in(D,relation_rng(A))
| in(B,relation_inverse_image(A,C))
| ~ relation(A) ),
inference(clausify,[status(thm)],[t166_relat_1]) ).
fof(nnf_39,plain,
? [A,B] :
( relation_inverse_image(B,A) = empty_set
& subset(A,relation_rng(B))
& empty_set != A
& relation(B) ),
inference(fof_nnf,[status(thm)],[t174_relat_1_neg]) ).
fof(sk_t174_relat_1_neg,plain,
( relation_inverse_image(sK1,sK2) = empty_set
& subset(sK2,relation_rng(sK1))
& empty_set != sK2
& relation(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(A,sK2),skolemize(B,sK1)],[nnf_39]) ).
cnf(c_54,negated_conjecture,
relation(sK1),
inference(split_conjunct,[status(thm)],[sk_t174_relat_1_neg]) ).
cnf(c_55,plain,
( ~ subset(A,B)
| element(A,powerset(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_56,negated_conjecture,
subset(sK2,relation_rng(sK1)),
inference(split_conjunct,[status(thm)],[sk_t174_relat_1_neg]) ).
cnf(c_58,plain,
subset(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
fof(nnf_4,plain,
! [A,B] :
( ( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ( ! [X3] :
( in(X3,B)
| ~ in(X3,A) )
| ~ subset(A,B) ) ),
inference(fof_nnf,[status(thm)],[d3_tarski]) ).
fof(sk_d3_tarski_sk,plain,
! [A,B] :
( ( ( ~ in(sK3(A,B),B)
& in(sK3(A,B),A) )
| subset(A,B) )
& ( ! [X3] :
( in(X3,B)
| ~ in(X3,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(C,sK3(A,B))],[nnf_4]) ).
fof(sk_d3_tarski,plain,
( ! [VAR_0,VAR_1] :
( ~ in(sK3(VAR_0,VAR_1),VAR_1)
| subset(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( in(sK3(VAR_0,VAR_1),VAR_0)
| subset(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(VAR_2,VAR_1)
| ~ in(VAR_2,VAR_0)
| ~ subset(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_d3_tarski_sk]) ).
cnf(c_60,plain,
( in(sK3(A,B),A)
| subset(A,B) ),
inference(split_conjunct,[status(thm)],[sk_d3_tarski]) ).
cnf(c_61,plain,
( in(C,B)
| ~ in(C,A)
| ~ subset(A,B) ),
inference(split_conjunct,[status(thm)],[sk_d3_tarski]) ).
cnf(c_62,negated_conjecture,
( in(A,relation_rng(sK1))
| ~ in(A,sK2) ),
inference(resolve,[status(thm)],[c_61,c_56]) ).
cnf(c_66,plain,
( element(A,powerset(B))
| in(sK3(A,B),A) ),
inference(resolve,[status(thm)],[c_60,c_55]) ).
cnf(c_68,plain,
element(A,powerset(A)),
inference(resolve,[status(thm)],[c_58,c_55]) ).
cnf(c_71,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_72,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
fof(nnf_15,plain,
! [A] :
? [B] : element(B,A),
inference(fof_nnf,[status(thm)],[existence_m1_subset_1]) ).
fof(sk_existence_m1_subset_1,plain,
! [A] : element(sK4(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(B,sK4(A))],[nnf_15]) ).
cnf(c_73,plain,
element(sK4(A),A),
inference(split_conjunct,[status(thm)],[sk_existence_m1_subset_1]) ).
fof(nnf_23,plain,
? [A] :
( relation(A)
& empty(A) ),
inference(fof_nnf,[status(thm)],[rc1_relat_1]) ).
fof(sk_rc1_relat_1,plain,
( relation(sK5)
& empty(sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(A,sK5)],[nnf_23]) ).
cnf(c_81,plain,
empty(sK5),
inference(split_conjunct,[status(thm)],[sk_rc1_relat_1]) ).
fof(nnf_25,plain,
? [A] : empty(A),
inference(fof_nnf,[status(thm)],[rc1_xboole_0]) ).
fof(sk_rc1_xboole_0,plain,
empty(sK6),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(A,sK6)],[nnf_25]) ).
cnf(c_84,plain,
empty(sK6),
inference(split_conjunct,[status(thm)],[sk_rc1_xboole_0]) ).
cnf(c_90,plain,
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
cnf(c_92,plain,
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t5_subset]) ).
cnf(c_93,plain,
( empty_set = A
| ~ empty(A) ),
inference(clausify,[status(thm)],[t6_boole]) ).
cnf(c_96,negated_conjecture,
empty_set != sK2,
inference(split_conjunct,[status(thm)],[sk_t174_relat_1_neg]) ).
cnf(c_97,negated_conjecture,
sK2 != empty_set,
inference(copy,[status(thm)],[c_96]) ).
cnf(c_98,negated_conjecture,
relation_inverse_image(sK1,sK2) = empty_set,
inference(split_conjunct,[status(thm)],[sk_t174_relat_1_neg]) ).
cnf(c_99,negated_conjecture,
empty_set = relation_inverse_image(sK1,sK2),
inference(copy,[status(thm)],[c_98]) ).
cnf(c_170,negated_conjecture,
( ~ in(C,B)
| ~ in(ordered_pair(A,C),sK1)
| ~ in(C,relation_rng(sK1))
| in(A,relation_inverse_image(sK1,B)) ),
inference(resolve,[status(thm)],[c_54,c_53]) ).
cnf(c_171,negated_conjecture,
( ~ in(C,B)
| ~ in(unordered_pair(unordered_pair(A,C),singleton(A)),sK1)
| ~ in(C,relation_rng(sK1))
| in(A,relation_inverse_image(sK1,B)) ),
inference(paramod,[status(thm)],[c_72,c_170]) ).
cnf(c_183,negated_conjecture,
( in(ordered_pair(sK0(sK1,A,B),B),sK1)
| ~ in(B,A)
| relation_rng(sK1) != A ),
inference(resolve,[status(thm)],[c_54,c_40]) ).
cnf(c_1320,negated_conjecture,
( in(unordered_pair(unordered_pair(sK0(sK1,A,B),B),singleton(sK0(sK1,A,B))),sK1)
| ~ in(B,A)
| relation_rng(sK1) != A ),
inference(paramod,[status(thm)],[c_72,c_183]) ).
cnf(c_184,negated_conjecture,
( in(unordered_pair(unordered_pair(B,sK0(sK1,A,B)),singleton(sK0(sK1,A,B))),sK1)
| ~ in(B,A)
| relation_rng(sK1) != A ),
inference(paramod,[status(thm)],[c_71,c_1320]) ).
cnf(c_1321,negated_conjecture,
sK2 != relation_inverse_image(sK1,sK2),
inference(paramod,[status(thm)],[c_99,c_97]) ).
cnf(c_186,negated_conjecture,
relation_inverse_image(sK1,sK2) != sK2,
inference(copy,[status(thm)],[c_1321]) ).
cnf(c_187,plain,
( relation_inverse_image(sK1,sK2) = A
| ~ empty(A) ),
inference(paramod,[status(thm)],[c_99,c_93]) ).
cnf(c_207,plain,
( in(sK4(A),A)
| empty(A) ),
inference(resolve,[status(thm)],[c_90,c_73]) ).
cnf(c_222,plain,
( ~ element(B,powerset(sK5))
| ~ in(A,B) ),
inference(resolve,[status(thm)],[c_92,c_81]) ).
cnf(c_1322,plain,
( ~ empty(B)
| ~ in(A,B) ),
inference(resolve,[status(thm)],[c_92,c_68]) ).
cnf(c_231,plain,
~ in(A,sK5),
inference(resolve,[status(thm)],[c_1322,c_81]) ).
cnf(c_315,plain,
( ~ in(C,B)
| ~ in(unordered_pair(unordered_pair(C,A),singleton(A)),sK1)
| ~ in(C,relation_rng(sK1))
| in(A,relation_inverse_image(sK1,B)) ),
inference(paramod,[status(thm)],[c_71,c_171]) ).
cnf(c_350,plain,
relation_inverse_image(sK1,sK2) = sK6,
inference(resolve,[status(thm)],[c_187,c_84]) ).
cnf(c_1323,plain,
relation_inverse_image(sK1,sK2) = sK5,
inference(resolve,[status(thm)],[c_187,c_81]) ).
cnf(c_351,plain,
sK6 = sK5,
inference(paramod,[status(thm)],[c_350,c_1323]) ).
cnf(c_352,negated_conjecture,
~ empty(sK2),
inference(resolve,[status(thm)],[c_187,c_186]) ).
cnf(c_359,plain,
relation_inverse_image(sK1,sK2) = sK5,
inference(paramod,[status(thm)],[c_351,c_350]) ).
cnf(c_742,plain,
( empty(A)
| ~ element(A,powerset(sK5)) ),
inference(resolve,[status(thm)],[c_222,c_207]) ).
cnf(c_747,plain,
( in(sK3(A,sK5),A)
| empty(A) ),
inference(resolve,[status(thm)],[c_742,c_66]) ).
cnf(c_751,plain,
~ element(sK2,powerset(sK5)),
inference(resolve,[status(thm)],[c_742,c_352]) ).
cnf(c_1324,negated_conjecture,
( in(sK3(sK2,sK5),relation_rng(sK1))
| empty(sK2) ),
inference(resolve,[status(thm)],[c_747,c_62]) ).
cnf(c_800,negated_conjecture,
in(sK3(sK2,sK5),relation_rng(sK1)),
inference(resolve,[status(thm)],[c_352,c_1324]) ).
cnf(c_1325,negated_conjecture,
( in(unordered_pair(unordered_pair(sK3(sK2,sK5),sK0(sK1,relation_rng(sK1),sK3(sK2,sK5))),singleton(sK0(sK1,relation_rng(sK1),sK3(sK2,sK5)))),sK1)
| relation_rng(sK1) != relation_rng(sK1) ),
inference(resolve,[status(thm)],[c_800,c_184]) ).
cnf(c_819,negated_conjecture,
in(unordered_pair(unordered_pair(sK3(sK2,sK5),sK0(sK1,relation_rng(sK1),sK3(sK2,sK5))),singleton(sK0(sK1,relation_rng(sK1),sK3(sK2,sK5)))),sK1),
inference(copy,[status(thm)],[c_1325]) ).
cnf(c_872,plain,
in(sK3(sK2,sK5),sK2),
inference(resolve,[status(thm)],[c_751,c_66]) ).
cnf(c_1326,plain,
( ~ in(unordered_pair(unordered_pair(sK3(sK2,sK5),A),singleton(A)),sK1)
| ~ in(sK3(sK2,sK5),relation_rng(sK1))
| in(A,relation_inverse_image(sK1,sK2)) ),
inference(resolve,[status(thm)],[c_315,c_872]) ).
cnf(c_1327,plain,
( ~ in(unordered_pair(unordered_pair(sK3(sK2,sK5),A),singleton(A)),sK1)
| ~ in(sK3(sK2,sK5),relation_rng(sK1))
| in(A,sK5) ),
inference(paramod,[status(thm)],[c_359,c_1326]) ).
cnf(c_1328,plain,
( ~ in(unordered_pair(unordered_pair(sK3(sK2,sK5),A),singleton(A)),sK1)
| ~ in(sK3(sK2,sK5),relation_rng(sK1)) ),
inference(resolve,[status(thm)],[c_231,c_1327]) ).
cnf(c_1318,plain,
~ in(unordered_pair(unordered_pair(sK3(sK2,sK5),A),singleton(A)),sK1),
inference(resolve,[status(thm)],[c_800,c_1328]) ).
cnf(c_1319,plain,
$false,
inference(resolve,[status(thm)],[c_1318,c_819]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU210+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n006.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sat Sep 26 08:50:41 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.15/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.38 % Process 857322 was started by sandbox on n006,
% 0.15/0.38 % Sat Sep 26 08:50:41 2026
% 0.15/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/0.39
% 0.15/0.39 % From the command line: assign(max_seconds, 300).
% 1.76/0.70
% 1.76/0.70 % SZS status Theorem for theBenchmark
% 1.76/0.70
% 1.76/0.70 % Proof 1 at 0.18 (+ 0.05) seconds.
% 1.76/0.70 % Length of proof is 59.
% 1.76/0.70 % Level of proof is 8.
% 1.76/0.70 % Maximum clause weight is 52.000.
% 1.76/0.70 % Given clauses 285.
% 1.76/0.70
% 1.76/0.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------