%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU242+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:33 AM UTC 2026
% Result : Theorem 1.94s 0.65s
% Output : CNFRefutation 1.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 5
% Syntax : Number of formulae : 102 ( 12 unt; 0 def)
% Number of atoms : 390 ( 101 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 428 ( 140 ~; 235 |; 45 &)
% ( 4 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 98 ( 0 sgn 43 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('theBenchmark.p',commutativity_k2_tarski) ).
fof(d14_relat_2,axiom,
! [A] :
( relation(A)
=> ( connected(A)
<=> is_connected_in(A,relation_field(A)) ) ),
file('theBenchmark.p',d14_relat_2) ).
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_2,axiom,
! [A] :
( relation(A)
=> ! [B] :
( is_connected_in(A,B)
<=> ! [C,D] :
~ ( ~ in(ordered_pair(D,C),A)
& ~ in(ordered_pair(C,D),A)
& C != D
& in(D,B)
& in(C,B) ) ) ),
file('theBenchmark.p',d6_relat_2) ).
fof(l4_wellord1,conjecture,
! [A] :
( relation(A)
=> ( connected(A)
<=> ! [B,C] :
~ ( ~ in(ordered_pair(C,B),A)
& ~ in(ordered_pair(B,C),A)
& B != C
& in(C,relation_field(A))
& in(B,relation_field(A)) ) ) ),
file('theBenchmark.p',l4_wellord1) ).
fof(l4_wellord1_neg,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( connected(A)
<=> ! [B,C] :
~ ( ~ in(ordered_pair(C,B),A)
& ~ in(ordered_pair(B,C),A)
& B != C
& in(C,relation_field(A))
& in(B,relation_field(A)) ) ) ),
inference(assume_negation,[status(cth)],[l4_wellord1]) ).
fof(nnf_35,plain,
? [A] :
( ( ? [B,C] :
( ~ in(ordered_pair(C,B),A)
& ~ in(ordered_pair(B,C),A)
& C != B
& in(C,relation_field(A))
& in(B,relation_field(A)) )
| ~ connected(A) )
& ( ! [X0,X1] :
( in(ordered_pair(X1,X0),A)
| in(ordered_pair(X0,X1),A)
| X1 = X0
| ~ in(X1,relation_field(A))
| ~ in(X0,relation_field(A)) )
| connected(A) )
& relation(A) ),
inference(fof_nnf,[status(thm)],[l4_wellord1_neg]) ).
fof(sk_l4_wellord1_neg_sk,plain,
( ( ( ~ in(ordered_pair(sK4,sK3),sK0)
& ~ in(ordered_pair(sK3,sK4),sK0)
& sK4 != sK3
& in(sK4,relation_field(sK0))
& in(sK3,relation_field(sK0)) )
| ~ connected(sK0) )
& ( ! [X0,X1] :
( in(ordered_pair(X1,X0),sK0)
| in(ordered_pair(X0,X1),sK0)
| X1 = X0
| ~ in(X1,relation_field(sK0))
| ~ in(X0,relation_field(sK0)) )
| connected(sK0) )
& relation(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK3,sK4]),skolemize(A,sK0),skolemize(B,sK3),skolemize(C,sK4)],[nnf_35]) ).
fof(sk_l4_wellord1_neg,plain,
( ( ~ in(ordered_pair(sK4,sK3),sK0)
| ~ connected(sK0) )
& ( ~ in(ordered_pair(sK3,sK4),sK0)
| ~ connected(sK0) )
& ( sK4 != sK3
| ~ connected(sK0) )
& ( in(sK4,relation_field(sK0))
| ~ connected(sK0) )
& ( in(sK3,relation_field(sK0))
| ~ connected(sK0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(VAR_1,VAR_0),sK0)
| in(ordered_pair(VAR_0,VAR_1),sK0)
| VAR_1 = VAR_0
| ~ in(VAR_1,relation_field(sK0))
| ~ in(VAR_0,relation_field(sK0))
| connected(sK0) )
& relation(sK0) ),
inference(cnf_transformation,[status(thm)],[sk_l4_wellord1_neg_sk]) ).
cnf(c_41,negated_conjecture,
relation(sK0),
inference(split_conjunct,[status(thm)],[sk_l4_wellord1_neg]) ).
fof(nnf_9,plain,
! [A] :
( ! [B] :
( ( ? [C,D] :
( ~ in(ordered_pair(D,C),A)
& ~ in(ordered_pair(C,D),A)
& D != C
& in(D,B)
& in(C,B) )
| is_connected_in(A,B) )
& ( ! [X0,X1] :
( in(ordered_pair(X1,X0),A)
| in(ordered_pair(X0,X1),A)
| X1 = X0
| ~ in(X1,B)
| ~ in(X0,B) )
| ~ is_connected_in(A,B) ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d6_relat_2]) ).
fof(sk_d6_relat_2_sk,plain,
! [A] :
( ! [B] :
( ( ( ~ in(ordered_pair(sK1(A,B),sK2(A,B)),A)
& ~ in(ordered_pair(sK2(A,B),sK1(A,B)),A)
& sK1(A,B) != sK2(A,B)
& in(sK1(A,B),B)
& in(sK2(A,B),B) )
| is_connected_in(A,B) )
& ( ! [X0,X1] :
( in(ordered_pair(X1,X0),A)
| in(ordered_pair(X0,X1),A)
| X1 = X0
| ~ in(X1,B)
| ~ in(X0,B) )
| ~ is_connected_in(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK1]),skolemize(C,sK2(A,B)),skolemize(D,sK1(A,B))],[nnf_9]) ).
fof(sk_d6_relat_2,plain,
( ! [VAR_0,VAR_1] :
( ~ in(ordered_pair(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1)),VAR_0)
| is_connected_in(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)
| is_connected_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( sK1(VAR_0,VAR_1) != sK2(VAR_0,VAR_1)
| is_connected_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK1(VAR_0,VAR_1),VAR_1)
| is_connected_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK2(VAR_0,VAR_1),VAR_1)
| is_connected_in(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(ordered_pair(VAR_2,VAR_3),VAR_0)
| VAR_3 = VAR_2
| ~ in(VAR_3,VAR_1)
| ~ in(VAR_2,VAR_1)
| ~ is_connected_in(VAR_0,VAR_1)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d6_relat_2_sk]) ).
cnf(c_46,plain,
( ~ in(ordered_pair(sK1(A,B),sK2(A,B)),A)
| is_connected_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d6_relat_2]) ).
cnf(c_47,plain,
( ~ in(ordered_pair(sK2(A,B),sK1(A,B)),A)
| is_connected_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d6_relat_2]) ).
cnf(c_48,plain,
( sK1(A,B) != sK2(A,B)
| is_connected_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d6_relat_2]) ).
cnf(c_49,plain,
( in(sK1(A,B),B)
| is_connected_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d6_relat_2]) ).
cnf(c_50,plain,
( in(sK2(A,B),B)
| is_connected_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d6_relat_2]) ).
cnf(c_51,plain,
( in(ordered_pair(D,C),A)
| in(ordered_pair(C,D),A)
| D = C
| ~ in(D,B)
| ~ in(C,B)
| ~ is_connected_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d6_relat_2]) ).
cnf(c_53,plain,
( ~ is_connected_in(A,relation_field(A))
| connected(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[d14_relat_2]) ).
cnf(c_54,plain,
( is_connected_in(A,relation_field(A))
| ~ connected(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[d14_relat_2]) ).
cnf(c_59,negated_conjecture,
( is_connected_in(sK0,relation_field(sK0))
| ~ connected(sK0) ),
inference(resolve,[status(thm)],[c_54,c_41]) ).
cnf(c_63,negated_conjecture,
( ~ is_connected_in(sK0,relation_field(sK0))
| connected(sK0) ),
inference(resolve,[status(thm)],[c_53,c_41]) ).
cnf(c_75,negated_conjecture,
( in(ordered_pair(C,B),sK0)
| in(ordered_pair(B,C),sK0)
| C = B
| ~ in(C,A)
| ~ in(B,A)
| ~ is_connected_in(sK0,A) ),
inference(resolve,[status(thm)],[c_51,c_41]) ).
cnf(c_79,negated_conjecture,
( in(sK2(sK0,A),A)
| is_connected_in(sK0,A) ),
inference(resolve,[status(thm)],[c_50,c_41]) ).
cnf(c_83,negated_conjecture,
( in(sK1(sK0,A),A)
| is_connected_in(sK0,A) ),
inference(resolve,[status(thm)],[c_49,c_41]) ).
cnf(c_87,negated_conjecture,
( sK1(sK0,A) != sK2(sK0,A)
| is_connected_in(sK0,A) ),
inference(resolve,[status(thm)],[c_48,c_41]) ).
cnf(c_91,negated_conjecture,
( ~ in(ordered_pair(sK2(sK0,A),sK1(sK0,A)),sK0)
| is_connected_in(sK0,A) ),
inference(resolve,[status(thm)],[c_47,c_41]) ).
cnf(c_95,negated_conjecture,
( ~ in(ordered_pair(sK1(sK0,A),sK2(sK0,A)),sK0)
| is_connected_in(sK0,A) ),
inference(resolve,[status(thm)],[c_46,c_41]) ).
cnf(c_100,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_102,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
cnf(c_116,negated_conjecture,
( in(ordered_pair(B,A),sK0)
| in(ordered_pair(A,B),sK0)
| B = A
| ~ in(B,relation_field(sK0))
| ~ in(A,relation_field(sK0))
| connected(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l4_wellord1_neg]) ).
cnf(c_1742,negated_conjecture,
( in(ordered_pair(B,A),sK0)
| in(unordered_pair(unordered_pair(A,B),singleton(A)),sK0)
| B = A
| ~ in(B,relation_field(sK0))
| ~ in(A,relation_field(sK0))
| connected(sK0) ),
inference(paramod,[status(thm)],[c_102,c_116]) ).
cnf(c_117,negated_conjecture,
( in(unordered_pair(unordered_pair(B,A),singleton(B)),sK0)
| in(unordered_pair(unordered_pair(A,B),singleton(A)),sK0)
| B = A
| ~ in(B,relation_field(sK0))
| ~ in(A,relation_field(sK0))
| connected(sK0) ),
inference(paramod,[status(thm)],[c_102,c_1742]) ).
cnf(c_118,negated_conjecture,
( in(sK3,relation_field(sK0))
| ~ connected(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l4_wellord1_neg]) ).
cnf(c_119,negated_conjecture,
( in(sK4,relation_field(sK0))
| ~ connected(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l4_wellord1_neg]) ).
cnf(c_120,negated_conjecture,
( sK4 != sK3
| ~ connected(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l4_wellord1_neg]) ).
cnf(c_121,negated_conjecture,
( ~ in(ordered_pair(sK3,sK4),sK0)
| ~ connected(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l4_wellord1_neg]) ).
cnf(c_122,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| ~ connected(sK0) ),
inference(paramod,[status(thm)],[c_102,c_121]) ).
cnf(c_123,negated_conjecture,
( ~ in(ordered_pair(sK4,sK3),sK0)
| ~ connected(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l4_wellord1_neg]) ).
cnf(c_1743,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(sK4,sK3),singleton(sK4)),sK0)
| ~ connected(sK0) ),
inference(paramod,[status(thm)],[c_102,c_123]) ).
cnf(c_124,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK4)),sK0)
| ~ connected(sK0) ),
inference(paramod,[status(thm)],[c_100,c_1743]) ).
cnf(c_1744,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(sK1(sK0,A),sK2(sK0,A)),singleton(sK1(sK0,A))),sK0)
| is_connected_in(sK0,A) ),
inference(paramod,[status(thm)],[c_102,c_95]) ).
cnf(c_129,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(sK2(sK0,A),sK1(sK0,A)),singleton(sK1(sK0,A))),sK0)
| is_connected_in(sK0,A) ),
inference(paramod,[status(thm)],[c_100,c_1744]) ).
cnf(c_133,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(sK2(sK0,A),sK1(sK0,A)),singleton(sK2(sK0,A))),sK0)
| is_connected_in(sK0,A) ),
inference(paramod,[status(thm)],[c_102,c_91]) ).
cnf(c_1745,negated_conjecture,
( in(ordered_pair(C,B),sK0)
| in(unordered_pair(unordered_pair(B,C),singleton(B)),sK0)
| C = B
| ~ in(C,A)
| ~ in(B,A)
| ~ is_connected_in(sK0,A) ),
inference(paramod,[status(thm)],[c_102,c_75]) ).
cnf(c_137,negated_conjecture,
( in(unordered_pair(unordered_pair(C,B),singleton(C)),sK0)
| in(unordered_pair(unordered_pair(B,C),singleton(B)),sK0)
| C = B
| ~ in(C,A)
| ~ in(B,A)
| ~ is_connected_in(sK0,A) ),
inference(paramod,[status(thm)],[c_102,c_1745]) ).
cnf(c_138,plain,
( connected(sK0)
| in(sK2(sK0,relation_field(sK0)),relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_79,c_63]) ).
cnf(c_142,plain,
( connected(sK0)
| in(sK1(sK0,relation_field(sK0)),relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_83,c_63]) ).
cnf(c_1746,negated_conjecture,
( in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),A),singleton(sK2(sK0,relation_field(sK0)))),sK0)
| in(unordered_pair(unordered_pair(A,sK2(sK0,relation_field(sK0))),singleton(A)),sK0)
| sK2(sK0,relation_field(sK0)) = A
| ~ in(A,relation_field(sK0))
| connected(sK0)
| connected(sK0) ),
inference(resolve,[status(thm)],[c_138,c_117]) ).
cnf(c_191,negated_conjecture,
( in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),A),singleton(sK2(sK0,relation_field(sK0)))),sK0)
| in(unordered_pair(unordered_pair(A,sK2(sK0,relation_field(sK0))),singleton(A)),sK0)
| sK2(sK0,relation_field(sK0)) = A
| ~ in(A,relation_field(sK0))
| connected(sK0) ),
inference(copy,[status(thm)],[c_1746]) ).
cnf(c_1747,plain,
( connected(sK0)
| in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0))),singleton(sK2(sK0,relation_field(sK0)))),sK0)
| in(unordered_pair(unordered_pair(sK1(sK0,relation_field(sK0)),sK2(sK0,relation_field(sK0))),singleton(sK1(sK0,relation_field(sK0)))),sK0)
| sK2(sK0,relation_field(sK0)) = sK1(sK0,relation_field(sK0))
| connected(sK0) ),
inference(resolve,[status(thm)],[c_191,c_142]) ).
cnf(c_1748,plain,
( connected(sK0)
| in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0))),singleton(sK2(sK0,relation_field(sK0)))),sK0)
| in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0))),singleton(sK1(sK0,relation_field(sK0)))),sK0)
| sK2(sK0,relation_field(sK0)) = sK1(sK0,relation_field(sK0))
| connected(sK0) ),
inference(paramod,[status(thm)],[c_100,c_1747]) ).
cnf(c_1749,plain,
( connected(sK0)
| in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0))),singleton(sK2(sK0,relation_field(sK0)))),sK0)
| in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0))),singleton(sK1(sK0,relation_field(sK0)))),sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| connected(sK0) ),
inference(copy,[status(thm)],[c_1748]) ).
cnf(c_427,plain,
( in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0))),singleton(sK2(sK0,relation_field(sK0)))),sK0)
| in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0))),singleton(sK1(sK0,relation_field(sK0)))),sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| connected(sK0) ),
inference(copy,[status(thm)],[c_1749]) ).
cnf(c_1217,plain,
( is_connected_in(sK0,relation_field(sK0))
| in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0))),singleton(sK2(sK0,relation_field(sK0)))),sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| connected(sK0) ),
inference(resolve,[status(thm)],[c_427,c_129]) ).
cnf(c_1750,negated_conjecture,
( connected(sK0)
| in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0))),singleton(sK2(sK0,relation_field(sK0)))),sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| connected(sK0) ),
inference(resolve,[status(thm)],[c_1217,c_63]) ).
cnf(c_1232,negated_conjecture,
( in(unordered_pair(unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0))),singleton(sK2(sK0,relation_field(sK0)))),sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| connected(sK0) ),
inference(copy,[status(thm)],[c_1750]) ).
cnf(c_1239,plain,
( is_connected_in(sK0,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| connected(sK0) ),
inference(resolve,[status(thm)],[c_1232,c_133]) ).
cnf(c_1751,negated_conjecture,
( connected(sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| connected(sK0) ),
inference(resolve,[status(thm)],[c_1239,c_63]) ).
cnf(c_1242,negated_conjecture,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| connected(sK0) ),
inference(copy,[status(thm)],[c_1751]) ).
cnf(c_1243,plain,
( ~ in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK4)),sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1242,c_124]) ).
cnf(c_1244,plain,
( ~ in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1242,c_122]) ).
cnf(c_1245,plain,
( sK4 != sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1242,c_120]) ).
cnf(c_1246,plain,
( in(sK4,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1242,c_119]) ).
cnf(c_1247,plain,
( in(sK3,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1242,c_118]) ).
cnf(c_1248,plain,
( is_connected_in(sK0,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1242,c_59]) ).
cnf(c_1270,plain,
( in(unordered_pair(unordered_pair(sK4,A),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(A,sK4),singleton(A)),sK0)
| sK4 = A
| ~ in(A,relation_field(sK0))
| ~ is_connected_in(sK0,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1246,c_137]) ).
cnf(c_1752,plain,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| in(unordered_pair(unordered_pair(sK4,A),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(A,sK4),singleton(A)),sK0)
| sK4 = A
| ~ in(A,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1270,c_1248]) ).
cnf(c_1441,plain,
( in(unordered_pair(unordered_pair(sK4,A),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(A,sK4),singleton(A)),sK0)
| sK4 = A
| ~ in(A,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_1752]) ).
cnf(c_1753,plain,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| in(unordered_pair(unordered_pair(sK4,sK3),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK4 = sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1441,c_1247]) ).
cnf(c_1754,plain,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK4 = sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(paramod,[status(thm)],[c_100,c_1753]) ).
cnf(c_1455,plain,
( in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK4 = sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_1754]) ).
cnf(c_1755,plain,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK4 = sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1455,c_1243]) ).
cnf(c_1457,plain,
( in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK4 = sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_1755]) ).
cnf(c_1756,plain,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| sK4 = sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_1457,c_1244]) ).
cnf(c_1458,plain,
( sK4 = sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_1756]) ).
cnf(c_1459,plain,
( is_connected_in(sK0,relation_field(sK0))
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1458,c_87]) ).
cnf(c_1463,plain,
( in(unordered_pair(unordered_pair(B,A),singleton(B)),sK0)
| in(unordered_pair(unordered_pair(A,B),singleton(A)),sK0)
| B = A
| ~ in(B,relation_field(sK0))
| ~ in(A,relation_field(sK0))
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1459,c_137]) ).
cnf(c_1464,plain,
( connected(sK0)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1459,c_63]) ).
cnf(c_1757,plain,
( in(unordered_pair(unordered_pair(sK4,sK3),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| ~ in(sK4,relation_field(sK0))
| ~ in(sK3,relation_field(sK0))
| sK4 = sK3 ),
inference(factor,[status(thm)],[c_1463]) ).
cnf(c_1465,plain,
( in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| ~ in(sK4,relation_field(sK0))
| ~ in(sK3,relation_field(sK0))
| sK4 = sK3 ),
inference(paramod,[status(thm)],[c_100,c_1757]) ).
cnf(c_1472,plain,
( ~ in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK4)),sK0)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1464,c_124]) ).
cnf(c_1473,plain,
( ~ in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1464,c_122]) ).
cnf(c_1474,plain,
( in(sK4,relation_field(sK0))
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1464,c_119]) ).
cnf(c_1475,plain,
( in(sK3,relation_field(sK0))
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1464,c_118]) ).
cnf(c_1758,plain,
( sK4 = sK3
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| ~ in(sK4,relation_field(sK0))
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1465,c_1475]) ).
cnf(c_1583,plain,
( in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| ~ in(sK4,relation_field(sK0))
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_1758]) ).
cnf(c_1759,plain,
( sK4 = sK3
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1583,c_1474]) ).
cnf(c_1585,plain,
( in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK4)),sK0)
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_1759]) ).
cnf(c_1760,plain,
( sK4 = sK3
| in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1585,c_1472]) ).
cnf(c_1586,plain,
( in(unordered_pair(unordered_pair(sK3,sK4),singleton(sK3)),sK0)
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_1760]) ).
cnf(c_1761,plain,
( sK4 = sK3
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_1586,c_1473]) ).
cnf(c_1587,plain,
sK4 = sK3,
inference(copy,[status(thm)],[c_1761]) ).
cnf(c_1762,plain,
( sK3 != sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(paramod,[status(thm)],[c_1587,c_1245]) ).
cnf(c_1592,plain,
sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)),
inference(copy,[status(thm)],[c_1762]) ).
cnf(c_1763,negated_conjecture,
( sK3 != sK3
| ~ connected(sK0) ),
inference(paramod,[status(thm)],[c_1587,c_120]) ).
cnf(c_1594,negated_conjecture,
~ connected(sK0),
inference(copy,[status(thm)],[c_1763]) ).
cnf(c_1672,negated_conjecture,
~ is_connected_in(sK0,relation_field(sK0)),
inference(resolve,[status(thm)],[c_1594,c_63]) ).
cnf(c_1764,negated_conjecture,
sK1(sK0,relation_field(sK0)) != sK2(sK0,relation_field(sK0)),
inference(resolve,[status(thm)],[c_87,c_1672]) ).
cnf(c_1765,negated_conjecture,
sK2(sK0,relation_field(sK0)) != sK2(sK0,relation_field(sK0)),
inference(paramod,[status(thm)],[c_1592,c_1764]) ).
cnf(c_1741,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_1765]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU242+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n001.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 09:03:28 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 1439906 was started by sandbox2 on n001,
% 0.11/0.37 % Sat Sep 26 09:03:28 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 1.94/0.65
% 1.94/0.65 % given #500 (A,wt=88): 444 f2(c1,relation_field(c1)) = f1(c1,relation_field(c1)) | connected(c1) | -in(A,relation_field(c1)) | f2(empty_set,relation_field(c1)) = A | in(unordered_pair(unordered_pair(A,f2(empty_set,relation_field(c1))),singleton(A)),c6) | in(unordered_pair(unordered_pair(f2(empty_set,relation_field(c1)),A),singleton(f2(empty_set,relation_field(c1)))),c6) | in(f2(c6,relation_field(c1)),relation_field(c1)). [resolve(404,c,186,b)].
% 1.94/0.65
% 1.94/0.65 % SZS status Theorem for theBenchmark
% 1.94/0.65
% 1.94/0.65 % Proof 1 at 0.21 (+ 0.06) seconds.
% 1.94/0.65 % Length of proof is 71.
% 1.94/0.65 % Level of proof is 25.
% 1.94/0.65 % Maximum clause weight is 80.000.
% 1.94/0.65 % Given clauses 544.
% 1.94/0.65
% 1.94/0.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------