%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU180+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 : n004.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:20 AM UTC 2026
% Result : Theorem 0.14s 10.83s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 9
% Syntax : Number of formulae : 49 ( 24 unt; 0 def)
% Number of atoms : 104 ( 32 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 97 ( 42 ~; 36 |; 6 &)
% ( 6 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 81 ( 8 sgn 24 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('theBenchmark.p',commutativity_k2_tarski) ).
fof(commutativity_k2_xboole_0,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('theBenchmark.p',commutativity_k2_xboole_0) ).
fof(d2_xboole_0,axiom,
! [A,B,C] :
( C = set_union2(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(D,B)
| in(D,A) ) ) ),
file('theBenchmark.p',d2_xboole_0) ).
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(d6_relat_1,axiom,
! [A] :
( relation(A)
=> relation_field(A) = set_union2(relation_dom(A),relation_rng(A)) ),
file('theBenchmark.p',d6_relat_1) ).
fof(t1_boole,axiom,
! [A] : set_union2(A,empty_set) = A,
file('theBenchmark.p',t1_boole) ).
fof(t30_relat_1,conjecture,
! [A,B,C] :
( relation(C)
=> ( in(ordered_pair(A,B),C)
=> ( in(B,relation_field(C))
& in(A,relation_field(C)) ) ) ),
file('theBenchmark.p',t30_relat_1) ).
fof(t30_relat_1_neg,negated_conjecture,
~ ! [A,B,C] :
( relation(C)
=> ( in(ordered_pair(A,B),C)
=> ( in(B,relation_field(C))
& in(A,relation_field(C)) ) ) ),
inference(assume_negation,[status(cth)],[t30_relat_1]) ).
fof(nnf_35,plain,
? [A,B,C] :
( ( ~ in(B,relation_field(C))
| ~ in(A,relation_field(C)) )
& in(ordered_pair(A,B),C)
& relation(C) ),
inference(fof_nnf,[status(thm)],[t30_relat_1_neg]) ).
fof(sk_t30_relat_1_neg,plain,
( ( ~ in(sK2,relation_field(sK1))
| ~ in(sK0,relation_field(sK1)) )
& in(ordered_pair(sK0,sK2),sK1)
& relation(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0,sK2]),skolemize(A,sK0),skolemize(B,sK2),skolemize(C,sK1)],[nnf_35]) ).
cnf(c_40,negated_conjecture,
( ~ in(sK2,relation_field(sK1))
| ~ in(sK0,relation_field(sK1)) ),
inference(split_conjunct,[status(thm)],[sk_t30_relat_1_neg]) ).
cnf(c_41,negated_conjecture,
in(ordered_pair(sK0,sK2),sK1),
inference(split_conjunct,[status(thm)],[sk_t30_relat_1_neg]) ).
cnf(c_42,negated_conjecture,
relation(sK1),
inference(split_conjunct,[status(thm)],[sk_t30_relat_1_neg]) ).
cnf(c_46,plain,
set_union2(A,empty_set) = A,
inference(clausify,[status(thm)],[t1_boole]) ).
cnf(c_59,plain,
( relation_field(A) = set_union2(relation_dom(A),relation_rng(A))
| ~ relation(A) ),
inference(clausify,[status(thm)],[d6_relat_1]) ).
cnf(c_60,plain,
( set_union2(relation_dom(A),relation_rng(A)) = relation_field(A)
| ~ relation(A) ),
inference(copy,[status(thm)],[c_59]) ).
cnf(c_61,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
cnf(c_66,plain,
( ~ in(ordered_pair(D,C),A)
| in(C,B)
| relation_rng(A) != B
| ~ relation(A) ),
inference(clausify,[status(thm)],[d5_relat_1]) ).
cnf(c_67,plain,
( ~ in(unordered_pair(unordered_pair(D,C),singleton(D)),A)
| in(C,B)
| relation_rng(A) != B
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_61,c_66]) ).
cnf(c_74,plain,
( ~ in(ordered_pair(C,D),A)
| in(C,B)
| relation_dom(A) != B
| ~ relation(A) ),
inference(clausify,[status(thm)],[d4_relat_1]) ).
cnf(c_75,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_61,c_74]) ).
cnf(c_81,plain,
( ~ in(D,B)
| in(D,C)
| set_union2(A,B) != C ),
inference(clausify,[status(thm)],[d2_xboole_0]) ).
cnf(c_82,plain,
( ~ in(D,A)
| in(D,C)
| set_union2(A,B) != C ),
inference(clausify,[status(thm)],[d2_xboole_0]) ).
cnf(c_84,plain,
set_union2(A,B) = set_union2(B,A),
inference(clausify,[status(thm)],[commutativity_k2_xboole_0]) ).
cnf(c_85,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_631,negated_conjecture,
in(unordered_pair(unordered_pair(sK0,sK2),singleton(sK0)),sK1),
inference(paramod,[status(thm)],[c_61,c_41]) ).
cnf(c_87,negated_conjecture,
in(unordered_pair(singleton(sK0),unordered_pair(sK0,sK2)),sK1),
inference(paramod,[status(thm)],[c_85,c_631]) ).
cnf(c_95,plain,
( ~ in(unordered_pair(singleton(C),unordered_pair(C,D)),A)
| in(C,B)
| relation_dom(A) != B
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_85,c_75]) ).
cnf(c_99,plain,
( ~ in(unordered_pair(singleton(D),unordered_pair(D,C)),A)
| in(C,B)
| relation_rng(A) != B
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_85,c_67]) ).
cnf(c_116,plain,
set_union2(relation_dom(sK1),relation_rng(sK1)) = relation_field(sK1),
inference(resolve,[status(thm)],[c_60,c_42]) ).
cnf(c_207,plain,
set_union2(empty_set,A) = A,
inference(paramod,[status(thm)],[c_84,c_46]) ).
cnf(c_632,negated_conjecture,
( in(sK0,A)
| relation_dom(sK1) != A
| ~ relation(sK1) ),
inference(resolve,[status(thm)],[c_95,c_87]) ).
cnf(c_249,negated_conjecture,
( in(sK0,A)
| relation_dom(sK1) != A ),
inference(resolve,[status(thm)],[c_42,c_632]) ).
cnf(c_633,negated_conjecture,
( in(sK2,A)
| relation_rng(sK1) != A
| ~ relation(sK1) ),
inference(resolve,[status(thm)],[c_99,c_87]) ).
cnf(c_265,negated_conjecture,
( in(sK2,A)
| relation_rng(sK1) != A ),
inference(resolve,[status(thm)],[c_42,c_633]) ).
cnf(c_634,plain,
A = set_union2(empty_set,A),
inference(copy,[status(thm)],[c_207]) ).
cnf(c_635,plain,
in(sK0,set_union2(empty_set,relation_dom(sK1))),
inference(resolve,[status(thm)],[c_249,c_634]) ).
cnf(c_320,plain,
in(sK0,relation_dom(sK1)),
inference(paramod,[status(thm)],[c_207,c_635]) ).
cnf(c_636,plain,
A = set_union2(empty_set,A),
inference(copy,[status(thm)],[c_207]) ).
cnf(c_637,plain,
in(sK2,set_union2(empty_set,relation_rng(sK1))),
inference(resolve,[status(thm)],[c_265,c_636]) ).
cnf(c_364,plain,
in(sK2,relation_rng(sK1)),
inference(paramod,[status(thm)],[c_207,c_637]) ).
cnf(c_499,plain,
( ~ in(A,relation_dom(sK1))
| in(A,relation_field(sK1)) ),
inference(resolve,[status(thm)],[c_116,c_82]) ).
cnf(c_592,plain,
in(sK0,relation_field(sK1)),
inference(resolve,[status(thm)],[c_499,c_320]) ).
cnf(c_599,negated_conjecture,
~ in(sK2,relation_field(sK1)),
inference(resolve,[status(thm)],[c_592,c_40]) ).
cnf(c_638,negated_conjecture,
( ~ in(sK2,B)
| set_union2(A,B) != relation_field(sK1) ),
inference(resolve,[status(thm)],[c_81,c_599]) ).
cnf(c_629,negated_conjecture,
set_union2(A,relation_rng(sK1)) != relation_field(sK1),
inference(resolve,[status(thm)],[c_638,c_364]) ).
cnf(c_630,plain,
$false,
inference(resolve,[status(thm)],[c_629,c_116]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU180+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.09/10.74 % Computer : n004.cluster.edu
% 0.09/10.74 % Model : x86_64 x86_64
% 0.09/10.74 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.74 % Memory : 8046.5625MB
% 0.09/10.74 % OS : Linux 6.8.0-71-generic
% 0.09/10.74 % CPULimit : 300
% 0.09/10.74 % WCLimit : 300
% 0.09/10.74 % DateTime : Sat Sep 26 08:45:32 UTC 2026
% 0.09/10.74 % CPUTime :
% 0.09/10.74 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/10.74 % Process 1277243 was started by sandbox on n004,
% 0.09/10.74 % Sat Sep 26 08:45:32 2026
% 0.09/10.74 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/10.75
% 0.09/10.75 % From the command line: assign(max_seconds, 300).
% 0.14/10.83
% 0.14/10.83 % SZS status Theorem for theBenchmark
% 0.14/10.83
% 0.14/10.83 % Proof 1 at 0.04 (+ 0.02) seconds.
% 0.14/10.83 % Length of proof is 38.
% 0.14/10.83 % Level of proof is 9.
% 0.14/10.83 % Maximum clause weight is 34.000.
% 0.14/10.83 % Given clauses 121.
% 0.14/10.83
% 0.14/10.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------