%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU206+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 : n019.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:24 AM UTC 2026
% Result : Theorem 243.49s 32.37s
% Output : CNFRefutation 243.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 5
% Syntax : Number of formulae : 49 ( 9 unt; 0 def)
% Number of atoms : 211 ( 54 equ)
% Maximal formula atoms : 26 ( 4 avg)
% Number of connectives : 261 ( 99 ~; 124 |; 27 &)
% ( 6 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 1 con; 0-4 aty)
% Number of variables : 143 ( 6 sgn 71 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d13_relat_1,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = relation_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) ) ) ) ),
file('theBenchmark.p',d13_relat_1) ).
fof(d4_relat_1,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) ) ),
file('theBenchmark.p',d4_relat_1) ).
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(t146_relat_1,conjecture,
! [A] :
( relation(A)
=> relation_image(A,relation_dom(A)) = relation_rng(A) ),
file('theBenchmark.p',t146_relat_1) ).
fof(t146_relat_1_neg,negated_conjecture,
~ ! [A] :
( relation(A)
=> relation_image(A,relation_dom(A)) = relation_rng(A) ),
inference(assume_negation,[status(cth)],[t146_relat_1]) ).
fof(nnf_5,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| ~ in(D,C) )
& ( ? [X3] :
( in(X3,B)
& in(ordered_pair(X3,D),A) )
| in(D,C) ) )
| relation_image(A,B) = C )
& ( ! [X0] :
( ( ! [X2] :
( ~ in(X2,B)
| ~ in(ordered_pair(X2,X0),A) )
| in(X0,C) )
& ( ? [X1] :
( in(X1,B)
& in(ordered_pair(X1,X0),A) )
| ~ in(X0,C) ) )
| relation_image(A,B) != C ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d13_relat_1]) ).
fof(sk_d13_relat_1_sk,plain,
! [A] :
( ! [B,C] :
( ( ( ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,sK4(A,B,C)),A) )
| ~ in(sK4(A,B,C),C) )
& ( ( in(sK5(A,B,C),B)
& in(ordered_pair(sK5(A,B,C),sK4(A,B,C)),A) )
| in(sK4(A,B,C),C) ) )
| relation_image(A,B) = C )
& ( ! [X0] :
( ( ! [X2] :
( ~ in(X2,B)
| ~ in(ordered_pair(X2,X0),A) )
| in(X0,C) )
& ( ( in(sK0(A,B,C,X0),B)
& in(ordered_pair(sK0(A,B,C,X0),X0),A) )
| ~ in(X0,C) ) )
| relation_image(A,B) != C ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK4,sK5]),skolemize(X1,sK0(A,B,C,X0)),skolemize(D,sK4(A,B,C)),skolemize(X3,sK5(A,B,C))],[nnf_5]) ).
fof(sk_d13_relat_1,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_3,VAR_1)
| ~ in(ordered_pair(VAR_3,sK4(VAR_0,VAR_1,VAR_2)),VAR_0)
| ~ in(sK4(VAR_0,VAR_1,VAR_2),VAR_2)
| relation_image(VAR_0,VAR_1) = VAR_2
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK5(VAR_0,VAR_1,VAR_2),VAR_1)
| in(sK4(VAR_0,VAR_1,VAR_2),VAR_2)
| relation_image(VAR_0,VAR_1) = VAR_2
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(ordered_pair(sK5(VAR_0,VAR_1,VAR_2),sK4(VAR_0,VAR_1,VAR_2)),VAR_0)
| in(sK4(VAR_0,VAR_1,VAR_2),VAR_2)
| relation_image(VAR_0,VAR_1) = VAR_2
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ in(VAR_4,VAR_1)
| ~ in(ordered_pair(VAR_4,VAR_3),VAR_0)
| in(VAR_3,VAR_2)
| relation_image(VAR_0,VAR_1) != VAR_2
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( in(sK0(VAR_0,VAR_1,VAR_2,VAR_3),VAR_1)
| ~ in(VAR_3,VAR_2)
| relation_image(VAR_0,VAR_1) != VAR_2
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( in(ordered_pair(sK0(VAR_0,VAR_1,VAR_2,VAR_3),VAR_3),VAR_0)
| ~ in(VAR_3,VAR_2)
| relation_image(VAR_0,VAR_1) != VAR_2
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d13_relat_1_sk]) ).
cnf(c_46,plain,
( in(ordered_pair(sK0(A,B,C,D),D),A)
| ~ in(D,C)
| relation_image(A,B) != C
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d13_relat_1]) ).
cnf(c_49,plain,
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A)
| in(D,C)
| relation_image(A,B) != C
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d13_relat_1]) ).
cnf(c_54,plain,
( ~ in(ordered_pair(C,D),A)
| in(C,B)
| relation_dom(A) != B
| ~ relation(A) ),
inference(clausify,[status(thm)],[d4_relat_1]) ).
fof(nnf_8,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,sK1(A,B)),A)
| ~ in(sK1(A,B),B) )
& ( in(ordered_pair(sK2(A,B),sK1(A,B)),A)
| in(sK1(A,B),B) ) )
| relation_rng(A) = B )
& ( ! [X0] :
( ( ! [X2] : ~ in(ordered_pair(X2,X0),A)
| in(X0,B) )
& ( in(ordered_pair(sK9(A,B,X0),X0),A)
| ~ in(X0,B) ) )
| relation_rng(A) != B ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK1,sK2]),skolemize(X1,sK9(A,B,X0)),skolemize(C,sK1(A,B)),skolemize(X3,sK2(A,B))],[nnf_8]) ).
fof(sk_d5_relat_1,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ in(ordered_pair(VAR_2,sK1(VAR_0,VAR_1)),VAR_0)
| ~ in(sK1(VAR_0,VAR_1),VAR_1)
| relation_rng(VAR_0) = VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(sK2(VAR_0,VAR_1),sK1(VAR_0,VAR_1)),VAR_0)
| in(sK1(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(sK9(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_59,plain,
( in(ordered_pair(sK2(A,B),sK1(A,B)),A)
| in(sK1(A,B),B)
| relation_rng(A) = B
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d5_relat_1]) ).
cnf(c_60,plain,
( ~ in(ordered_pair(C,sK1(A,B)),A)
| ~ in(sK1(A,B),B)
| relation_rng(A) = B
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d5_relat_1]) ).
fof(nnf_45,plain,
? [A] :
( relation_rng(A) != relation_image(A,relation_dom(A))
& relation(A) ),
inference(fof_nnf,[status(thm)],[t146_relat_1_neg]) ).
fof(sk_t146_relat_1_neg,plain,
( relation_rng(sK3) != relation_image(sK3,relation_dom(sK3))
& relation(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(A,sK3)],[nnf_45]) ).
cnf(c_69,negated_conjecture,
relation(sK3),
inference(split_conjunct,[status(thm)],[sk_t146_relat_1_neg]) ).
cnf(c_70,negated_conjecture,
( in(ordered_pair(sK0(sK3,A,B,C),C),sK3)
| ~ in(C,B)
| relation_image(sK3,A) != B ),
inference(resolve,[status(thm)],[c_69,c_46]) ).
cnf(c_72,negated_conjecture,
( ~ in(D,A)
| ~ in(ordered_pair(D,C),sK3)
| in(C,B)
| relation_image(sK3,A) != B ),
inference(resolve,[status(thm)],[c_69,c_49]) ).
cnf(c_77,negated_conjecture,
( ~ in(ordered_pair(B,C),sK3)
| in(B,A)
| relation_dom(sK3) != A ),
inference(resolve,[status(thm)],[c_69,c_54]) ).
cnf(c_82,negated_conjecture,
( in(ordered_pair(sK2(sK3,A),sK1(sK3,A)),sK3)
| in(sK1(sK3,A),A)
| relation_rng(sK3) = A ),
inference(resolve,[status(thm)],[c_69,c_59]) ).
cnf(c_83,negated_conjecture,
( ~ in(ordered_pair(B,sK1(sK3,A)),sK3)
| ~ in(sK1(sK3,A),A)
| relation_rng(sK3) = A ),
inference(resolve,[status(thm)],[c_69,c_60]) ).
cnf(c_181,negated_conjecture,
relation_rng(sK3) != relation_image(sK3,relation_dom(sK3)),
inference(split_conjunct,[status(thm)],[sk_t146_relat_1_neg]) ).
cnf(c_182,negated_conjecture,
relation_image(sK3,relation_dom(sK3)) != relation_rng(sK3),
inference(copy,[status(thm)],[c_181]) ).
cnf(c_209,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
cnf(c_292,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(B,sK1(sK3,A)),singleton(B)),sK3)
| ~ in(sK1(sK3,A),A)
| relation_rng(sK3) = A ),
inference(paramod,[status(thm)],[c_209,c_83]) ).
cnf(c_293,negated_conjecture,
( in(unordered_pair(unordered_pair(sK2(sK3,A),sK1(sK3,A)),singleton(sK2(sK3,A))),sK3)
| in(sK1(sK3,A),A)
| relation_rng(sK3) = A ),
inference(paramod,[status(thm)],[c_209,c_82]) ).
cnf(c_298,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(B,C),singleton(B)),sK3)
| in(B,A)
| relation_dom(sK3) != A ),
inference(paramod,[status(thm)],[c_209,c_77]) ).
cnf(c_302,negated_conjecture,
( ~ in(D,A)
| ~ in(unordered_pair(unordered_pair(D,C),singleton(D)),sK3)
| in(C,B)
| relation_image(sK3,A) != B ),
inference(paramod,[status(thm)],[c_209,c_72]) ).
cnf(c_303,negated_conjecture,
( in(unordered_pair(unordered_pair(sK0(sK3,A,B,C),C),singleton(sK0(sK3,A,B,C))),sK3)
| ~ in(C,B)
| relation_image(sK3,A) != B ),
inference(paramod,[status(thm)],[c_209,c_70]) ).
cnf(c_9466,plain,
( ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),sK3)
| in(A,relation_dom(sK3)) ),
inference(xxres,[status(thm)],[c_298]) ).
cnf(c_576,negated_conjecture,
( in(sK1(sK3,A),A)
| relation_rng(sK3) = A
| in(sK2(sK3,A),relation_dom(sK3)) ),
inference(resolve,[status(thm)],[c_9466,c_293]) ).
cnf(c_603,plain,
( in(unordered_pair(unordered_pair(sK0(sK3,B,relation_image(sK3,B),A),A),singleton(sK0(sK3,B,relation_image(sK3,B),A))),sK3)
| ~ in(A,relation_image(sK3,B)) ),
inference(xxres,[status(thm)],[c_303]) ).
cnf(c_9467,plain,
( ~ in(C,B)
| ~ in(unordered_pair(unordered_pair(C,A),singleton(C)),sK3)
| in(A,relation_image(sK3,B)) ),
inference(xxres,[status(thm)],[c_302]) ).
cnf(c_9468,negated_conjecture,
( in(sK1(sK3,A),A)
| relation_rng(sK3) = A
| ~ in(sK2(sK3,A),B)
| in(sK1(sK3,A),relation_image(sK3,B)) ),
inference(resolve,[status(thm)],[c_9467,c_293]) ).
cnf(c_9469,negated_conjecture,
( in(sK1(sK3,A),A)
| relation_rng(sK3) = A
| in(sK1(sK3,A),A)
| relation_rng(sK3) = A
| in(sK1(sK3,A),relation_image(sK3,relation_dom(sK3))) ),
inference(resolve,[status(thm)],[c_9468,c_576]) ).
cnf(c_9470,negated_conjecture,
( in(sK1(sK3,A),A)
| in(sK1(sK3,A),A)
| relation_rng(sK3) = A
| in(sK1(sK3,A),relation_image(sK3,relation_dom(sK3))) ),
inference(copy,[status(thm)],[c_9469]) ).
cnf(c_5237,negated_conjecture,
( in(sK1(sK3,A),A)
| relation_rng(sK3) = A
| in(sK1(sK3,A),relation_image(sK3,relation_dom(sK3))) ),
inference(copy,[status(thm)],[c_9470]) ).
cnf(c_9471,plain,
( relation_rng(sK3) = relation_image(sK3,relation_dom(sK3))
| in(sK1(sK3,relation_image(sK3,relation_dom(sK3))),relation_image(sK3,relation_dom(sK3))) ),
inference(factor,[status(thm)],[c_5237]) ).
cnf(c_9472,plain,
( relation_image(sK3,relation_dom(sK3)) = relation_rng(sK3)
| in(sK1(sK3,relation_image(sK3,relation_dom(sK3))),relation_image(sK3,relation_dom(sK3))) ),
inference(copy,[status(thm)],[c_9471]) ).
cnf(c_5242,negated_conjecture,
in(sK1(sK3,relation_image(sK3,relation_dom(sK3))),relation_image(sK3,relation_dom(sK3))),
inference(resolve,[status(thm)],[c_182,c_9472]) ).
cnf(c_9473,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(A,sK1(sK3,relation_image(sK3,relation_dom(sK3)))),singleton(A)),sK3)
| relation_rng(sK3) = relation_image(sK3,relation_dom(sK3)) ),
inference(resolve,[status(thm)],[c_5242,c_292]) ).
cnf(c_9474,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(A,sK1(sK3,relation_image(sK3,relation_dom(sK3)))),singleton(A)),sK3)
| relation_image(sK3,relation_dom(sK3)) = relation_rng(sK3) ),
inference(copy,[status(thm)],[c_9473]) ).
cnf(c_9452,negated_conjecture,
~ in(unordered_pair(unordered_pair(A,sK1(sK3,relation_image(sK3,relation_dom(sK3)))),singleton(A)),sK3),
inference(resolve,[status(thm)],[c_182,c_9474]) ).
cnf(c_9475,plain,
in(unordered_pair(unordered_pair(sK0(sK3,relation_dom(sK3),relation_image(sK3,relation_dom(sK3)),sK1(sK3,relation_image(sK3,relation_dom(sK3)))),sK1(sK3,relation_image(sK3,relation_dom(sK3)))),singleton(sK0(sK3,relation_dom(sK3),relation_image(sK3,relation_dom(sK3)),sK1(sK3,relation_image(sK3,relation_dom(sK3)))))),sK3),
inference(resolve,[status(thm)],[c_603,c_5242]) ).
cnf(c_9465,plain,
$false,
inference(resolve,[status(thm)],[c_9452,c_9475]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU206+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.11/0.36 % Computer : n019.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sat Sep 26 08:49:33 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.36 % Process 896019 was started by sandbox on n019,
% 0.11/0.36 % Sat Sep 26 08:49:33 2026
% 0.11/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 243.49/32.37
% 243.49/32.37 % given #500 (W,wt=10): 2545 in(A,B) | -in(powerset(A),f4(powerset(A),B)). [resolve(708,b,217,b)].
% 243.49/32.37
% 243.49/32.37 % SZS status Theorem for theBenchmark
% 243.49/32.37
% 243.49/32.37 % Proof 1 at 6.24 (+ 1.39) seconds.
% 243.49/32.37 % Length of proof is 30.
% 243.49/32.37 % Level of proof is 8.
% 243.49/32.37 % Maximum clause weight is 27.000.
% 243.49/32.37 % Given clauses 919.
% 243.49/32.37
% 243.49/32.37 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------