%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU248+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 : n012.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:34 AM UTC 2026
% Result : Theorem 44.24s 6.72s
% Output : CNFRefutation 44.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 7
% Syntax : Number of formulae : 46 ( 13 unt; 0 def)
% Number of atoms : 158 ( 25 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 195 ( 83 ~; 82 |; 18 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 2 con; 0-3 aty)
% Number of variables : 132 ( 16 sgn 56 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('theBenchmark.p',commutativity_k2_tarski) ).
fof(d12_relat_1,axiom,
! [A,B] :
( relation(B)
=> ! [C] :
( relation(C)
=> ( C = relation_rng_restriction(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ( in(ordered_pair(D,E),B)
& in(E,A) ) ) ) ) ),
file('theBenchmark.p',d12_relat_1) ).
fof(d3_tarski,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('theBenchmark.p',d3_tarski) ).
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_tarski,axiom,
! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
file('theBenchmark.p',d5_tarski) ).
fof(dt_k8_relat_1,axiom,
! [A,B] :
( relation(B)
=> relation(relation_rng_restriction(A,B)) ),
file('theBenchmark.p',dt_k8_relat_1) ).
fof(l29_wellord1,conjecture,
! [A,B] :
( relation(B)
=> subset(relation_dom(relation_rng_restriction(A,B)),relation_dom(B)) ),
file('theBenchmark.p',l29_wellord1) ).
fof(l29_wellord1_neg,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> subset(relation_dom(relation_rng_restriction(A,B)),relation_dom(B)) ),
inference(assume_negation,[status(cth)],[l29_wellord1]) ).
fof(nnf_34,plain,
? [A,B] :
( ~ subset(relation_dom(relation_rng_restriction(A,B)),relation_dom(B))
& relation(B) ),
inference(fof_nnf,[status(thm)],[l29_wellord1_neg]) ).
fof(sk_l29_wellord1_neg,plain,
( ~ subset(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1))
& relation(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_34]) ).
cnf(c_35,negated_conjecture,
~ subset(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1)),
inference(split_conjunct,[status(thm)],[sk_l29_wellord1_neg]) ).
cnf(c_36,negated_conjecture,
relation(sK1),
inference(split_conjunct,[status(thm)],[sk_l29_wellord1_neg]) ).
cnf(c_61,plain,
( relation(relation_rng_restriction(B,A))
| ~ relation(A) ),
inference(clausify,[status(thm)],[dt_k8_relat_1]) ).
cnf(c_62,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
fof(nnf_7,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ! [D] : ~ in(ordered_pair(C,D),A)
| ~ in(C,B) )
& ( ? [X3] : in(ordered_pair(C,X3),A)
| in(C,B) ) )
| relation_dom(A) = B )
& ( ! [X0] :
( ( ! [X2] : ~ in(ordered_pair(X0,X2),A)
| in(X0,B) )
& ( ? [X1] : in(ordered_pair(X0,X1),A)
| ~ in(X0,B) ) )
| relation_dom(A) != B ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d4_relat_1]) ).
fof(sk_d4_relat_1_sk,plain,
! [A] :
( ! [B] :
( ( ( ( ! [D] : ~ in(ordered_pair(sK4(A,B),D),A)
| ~ in(sK4(A,B),B) )
& ( in(ordered_pair(sK4(A,B),sK5(A,B)),A)
| in(sK4(A,B),B) ) )
| relation_dom(A) = B )
& ( ! [X0] :
( ( ! [X2] : ~ in(ordered_pair(X0,X2),A)
| in(X0,B) )
& ( in(ordered_pair(X0,sK2(A,B,X0)),A)
| ~ in(X0,B) ) )
| relation_dom(A) != B ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK4,sK5]),skolemize(X1,sK2(A,B,X0)),skolemize(C,sK4(A,B)),skolemize(X3,sK5(A,B))],[nnf_7]) ).
fof(sk_d4_relat_1,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ in(ordered_pair(sK4(VAR_0,VAR_1),VAR_2),VAR_0)
| ~ in(sK4(VAR_0,VAR_1),VAR_1)
| relation_dom(VAR_0) = VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1)),VAR_0)
| in(sK4(VAR_0,VAR_1),VAR_1)
| relation_dom(VAR_0) = VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(ordered_pair(VAR_2,VAR_3),VAR_0)
| in(VAR_2,VAR_1)
| relation_dom(VAR_0) != VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(ordered_pair(VAR_2,sK2(VAR_0,VAR_1,VAR_2)),VAR_0)
| ~ in(VAR_2,VAR_1)
| relation_dom(VAR_0) != VAR_1
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d4_relat_1_sk]) ).
cnf(c_67,plain,
( ~ in(ordered_pair(C,D),A)
| in(C,B)
| relation_dom(A) != B
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d4_relat_1]) ).
cnf(c_68,plain,
( ~ in(unordered_pair(unordered_pair(C,D),singleton(C)),A)
| in(C,B)
| relation_dom(A) != B
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_62,c_67]) ).
cnf(c_69,plain,
( in(ordered_pair(C,sK2(A,B,C)),A)
| ~ in(C,B)
| relation_dom(A) != B
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d4_relat_1]) ).
cnf(c_70,plain,
( in(unordered_pair(unordered_pair(C,sK2(A,B,C)),singleton(C)),A)
| ~ in(C,B)
| relation_dom(A) != B
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_62,c_69]) ).
fof(nnf_6,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_6]) ).
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_71,plain,
( ~ in(sK3(A,B),B)
| subset(A,B) ),
inference(split_conjunct,[status(thm)],[sk_d3_tarski]) ).
cnf(c_72,plain,
( in(sK3(A,B),A)
| subset(A,B) ),
inference(split_conjunct,[status(thm)],[sk_d3_tarski]) ).
cnf(c_82,plain,
( in(ordered_pair(D,E),A)
| ~ in(ordered_pair(D,E),B)
| relation_rng_restriction(C,A) != B
| ~ relation(B)
| ~ relation(A) ),
inference(clausify,[status(thm)],[d12_relat_1]) ).
cnf(c_13067,plain,
( in(ordered_pair(D,E),A)
| ~ in(unordered_pair(unordered_pair(D,E),singleton(D)),B)
| relation_rng_restriction(C,A) != B
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_62,c_82]) ).
cnf(c_83,plain,
( in(unordered_pair(unordered_pair(D,E),singleton(D)),A)
| ~ in(unordered_pair(unordered_pair(D,E),singleton(D)),B)
| relation_rng_restriction(C,A) != B
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_62,c_13067]) ).
cnf(c_86,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_96,plain,
( in(unordered_pair(singleton(C),unordered_pair(C,sK2(A,B,C))),A)
| ~ in(C,B)
| relation_dom(A) != B
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_86,c_70]) ).
cnf(c_118,plain,
relation(relation_rng_restriction(A,sK1)),
inference(resolve,[status(thm)],[c_61,c_36]) ).
cnf(c_128,plain,
( ~ in(unordered_pair(unordered_pair(B,C),singleton(B)),A)
| in(B,relation_dom(A))
| ~ relation(A) ),
inference(xxres,[status(thm)],[c_68]) ).
cnf(c_129,negated_conjecture,
~ in(sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1)),relation_dom(sK1)),
inference(resolve,[status(thm)],[c_71,c_35]) ).
cnf(c_131,plain,
in(sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1)),relation_dom(relation_rng_restriction(sK0,sK1))),
inference(resolve,[status(thm)],[c_72,c_35]) ).
cnf(c_161,plain,
( in(unordered_pair(unordered_pair(D,E),singleton(D)),A)
| ~ in(unordered_pair(singleton(D),unordered_pair(D,E)),B)
| relation_rng_restriction(C,A) != B
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_86,c_83]) ).
cnf(c_202,plain,
( in(unordered_pair(singleton(B),unordered_pair(B,sK2(A,relation_dom(A),B))),A)
| ~ in(B,relation_dom(A))
| ~ relation(A) ),
inference(xxres,[status(thm)],[c_96]) ).
cnf(c_13068,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),sK1)
| in(A,relation_dom(sK1)) ),
inference(resolve,[status(thm)],[c_128,c_36]) ).
cnf(c_471,negated_conjecture,
~ in(unordered_pair(unordered_pair(sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1)),A),singleton(sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1)))),sK1),
inference(resolve,[status(thm)],[c_13068,c_129]) ).
cnf(c_13069,plain,
( in(unordered_pair(singleton(sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1))),unordered_pair(sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1)),sK2(relation_rng_restriction(sK0,sK1),relation_dom(relation_rng_restriction(sK0,sK1)),sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1))))),relation_rng_restriction(sK0,sK1))
| ~ relation(relation_rng_restriction(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_202,c_131]) ).
cnf(c_2689,plain,
in(unordered_pair(singleton(sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1))),unordered_pair(sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1)),sK2(relation_rng_restriction(sK0,sK1),relation_dom(relation_rng_restriction(sK0,sK1)),sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1))))),relation_rng_restriction(sK0,sK1)),
inference(resolve,[status(thm)],[c_118,c_13069]) ).
cnf(c_13070,negated_conjecture,
( in(unordered_pair(unordered_pair(C,D),singleton(C)),sK1)
| ~ in(unordered_pair(singleton(C),unordered_pair(C,D)),A)
| relation_rng_restriction(B,sK1) != A
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_161,c_36]) ).
cnf(c_13071,negated_conjecture,
( in(unordered_pair(unordered_pair(C,D),singleton(C)),sK1)
| ~ in(unordered_pair(singleton(C),unordered_pair(C,D)),relation_rng_restriction(B,sK1))
| relation_rng_restriction(A,sK1) != relation_rng_restriction(B,sK1) ),
inference(resolve,[status(thm)],[c_13070,c_118]) ).
cnf(c_13072,plain,
( in(unordered_pair(unordered_pair(A,B),singleton(A)),sK1)
| ~ in(unordered_pair(singleton(A),unordered_pair(A,B)),relation_rng_restriction(C,sK1)) ),
inference(xxres,[status(thm)],[c_13071]) ).
cnf(c_13065,plain,
~ in(unordered_pair(singleton(sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1))),unordered_pair(sK3(relation_dom(relation_rng_restriction(sK0,sK1)),relation_dom(sK1)),A)),relation_rng_restriction(B,sK1)),
inference(resolve,[status(thm)],[c_13072,c_471]) ).
cnf(c_13066,plain,
$false,
inference(resolve,[status(thm)],[c_13065,c_2689]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU248+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Sat Sep 26 08:58:19 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/0.30 % Process 205853 was started by sandbox on n012,
% 0.03/0.30 % Sat Sep 26 08:58:19 2026
% 0.03/0.30 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.03/0.30
% 0.03/0.30 % From the command line: assign(max_seconds, 300).
% 44.24/6.72
% 44.24/6.72 % given #500 (W,wt=23): 2370 relation_rng_restriction(A,c5) = empty_set | -subset(A,B) | in(f3(A,empty_set),B). [resolve(2260,b,73,b)].
% 44.24/6.72
% 44.24/6.72 % given #1000 (F,wt=37): 7151 -in(unordered_pair(singleton(A),unordered_pair(B,A)),relation_rng_restriction(f7(powerset(B)),c1)). [para(86(a,1),1340(a,1))].
% 44.24/6.72
% 44.24/6.72 % SZS status Theorem for theBenchmark
% 44.24/6.72
% 44.24/6.72 % Proof 1 at 5.94 (+ 0.28) seconds.
% 44.24/6.72 % Length of proof is 31.
% 44.24/6.72 % Level of proof is 6.
% 44.24/6.72 % Maximum clause weight is 76.000.
% 44.24/6.72 % Given clauses 1101.
% 44.24/6.72
% 44.24/6.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------