%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU240+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 : n003.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 0.22s 0.67s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 6
% Syntax : Number of formulae : 75 ( 15 unt; 0 def)
% Number of atoms : 282 ( 4 equ)
% Maximal formula atoms : 26 ( 3 avg)
% Number of connectives : 341 ( 134 ~; 157 |; 37 &)
% ( 4 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 141 ( 5 sgn 57 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('theBenchmark.p',commutativity_k2_tarski) ).
fof(d16_relat_2,axiom,
! [A] :
( relation(A)
=> ( transitive(A)
<=> is_transitive_in(A,relation_field(A)) ) ),
file('theBenchmark.p',d16_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(d8_relat_2,axiom,
! [A] :
( relation(A)
=> ! [B] :
( is_transitive_in(A,B)
<=> ! [C,D,E] :
( ( in(ordered_pair(D,E),A)
& in(ordered_pair(C,D),A)
& in(E,B)
& in(D,B)
& in(C,B) )
=> in(ordered_pair(C,E),A) ) ) ),
file('theBenchmark.p',d8_relat_2) ).
fof(t30_relat_1,axiom,
! [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(l2_wellord1,conjecture,
! [A] :
( relation(A)
=> ( transitive(A)
<=> ! [B,C,D] :
( ( in(ordered_pair(C,D),A)
& in(ordered_pair(B,C),A) )
=> in(ordered_pair(B,D),A) ) ) ),
file('theBenchmark.p',l2_wellord1) ).
fof(l2_wellord1_neg,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( transitive(A)
<=> ! [B,C,D] :
( ( in(ordered_pair(C,D),A)
& in(ordered_pair(B,C),A) )
=> in(ordered_pair(B,D),A) ) ) ),
inference(assume_negation,[status(cth)],[l2_wellord1]) ).
fof(nnf_36,plain,
? [A] :
( ( ? [B,C,D] :
( ~ in(ordered_pair(B,D),A)
& in(ordered_pair(C,D),A)
& in(ordered_pair(B,C),A) )
| ~ transitive(A) )
& ( ! [X0,X1,X2] :
( in(ordered_pair(X0,X2),A)
| ~ in(ordered_pair(X1,X2),A)
| ~ in(ordered_pair(X0,X1),A) )
| transitive(A) )
& relation(A) ),
inference(fof_nnf,[status(thm)],[l2_wellord1_neg]) ).
fof(sk_l2_wellord1_neg_sk,plain,
( ( ( ~ in(ordered_pair(sK4,sK6),sK0)
& in(ordered_pair(sK5,sK6),sK0)
& in(ordered_pair(sK4,sK5),sK0) )
| ~ transitive(sK0) )
& ( ! [X0,X1,X2] :
( in(ordered_pair(X0,X2),sK0)
| ~ in(ordered_pair(X1,X2),sK0)
| ~ in(ordered_pair(X0,X1),sK0) )
| transitive(sK0) )
& relation(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK4,sK5,sK6]),skolemize(A,sK0),skolemize(B,sK4),skolemize(C,sK5),skolemize(D,sK6)],[nnf_36]) ).
fof(sk_l2_wellord1_neg,plain,
( ( ~ in(ordered_pair(sK4,sK6),sK0)
| ~ transitive(sK0) )
& ( in(ordered_pair(sK5,sK6),sK0)
| ~ transitive(sK0) )
& ( in(ordered_pair(sK4,sK5),sK0)
| ~ transitive(sK0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(ordered_pair(VAR_0,VAR_2),sK0)
| ~ in(ordered_pair(VAR_1,VAR_2),sK0)
| ~ in(ordered_pair(VAR_0,VAR_1),sK0)
| transitive(sK0) )
& relation(sK0) ),
inference(cnf_transformation,[status(thm)],[sk_l2_wellord1_neg_sk]) ).
cnf(c_42,negated_conjecture,
relation(sK0),
inference(split_conjunct,[status(thm)],[sk_l2_wellord1_neg]) ).
cnf(c_44,plain,
( in(C,relation_field(A))
| ~ in(ordered_pair(B,C),A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[t30_relat_1]) ).
cnf(c_45,plain,
( in(B,relation_field(A))
| ~ in(ordered_pair(B,C),A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[t30_relat_1]) ).
fof(nnf_9,plain,
! [A] :
( ! [B] :
( ( ? [C,D,E] :
( ~ in(ordered_pair(C,E),A)
& in(ordered_pair(D,E),A)
& in(ordered_pair(C,D),A)
& in(E,B)
& in(D,B)
& in(C,B) )
| is_transitive_in(A,B) )
& ( ! [X0,X1,X2] :
( in(ordered_pair(X0,X2),A)
| ~ in(ordered_pair(X1,X2),A)
| ~ in(ordered_pair(X0,X1),A)
| ~ in(X2,B)
| ~ in(X1,B)
| ~ in(X0,B) )
| ~ is_transitive_in(A,B) ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d8_relat_2]) ).
fof(sk_d8_relat_2_sk,plain,
! [A] :
( ! [B] :
( ( ( ~ in(ordered_pair(sK1(A,B),sK2(A,B)),A)
& in(ordered_pair(sK3(A,B),sK2(A,B)),A)
& in(ordered_pair(sK1(A,B),sK3(A,B)),A)
& in(sK2(A,B),B)
& in(sK3(A,B),B)
& in(sK1(A,B),B) )
| is_transitive_in(A,B) )
& ( ! [X0,X1,X2] :
( in(ordered_pair(X0,X2),A)
| ~ in(ordered_pair(X1,X2),A)
| ~ in(ordered_pair(X0,X1),A)
| ~ in(X2,B)
| ~ in(X1,B)
| ~ in(X0,B) )
| ~ is_transitive_in(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK3,sK2]),skolemize(C,sK1(A,B)),skolemize(D,sK3(A,B)),skolemize(E,sK2(A,B))],[nnf_9]) ).
fof(sk_d8_relat_2,plain,
( ! [VAR_0,VAR_1] :
( ~ in(ordered_pair(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1)),VAR_0)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(sK3(VAR_0,VAR_1),sK2(VAR_0,VAR_1)),VAR_0)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(sK1(VAR_0,VAR_1),sK3(VAR_0,VAR_1)),VAR_0)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK2(VAR_0,VAR_1),VAR_1)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK3(VAR_0,VAR_1),VAR_1)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK1(VAR_0,VAR_1),VAR_1)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( in(ordered_pair(VAR_2,VAR_4),VAR_0)
| ~ in(ordered_pair(VAR_3,VAR_4),VAR_0)
| ~ in(ordered_pair(VAR_2,VAR_3),VAR_0)
| ~ in(VAR_4,VAR_1)
| ~ in(VAR_3,VAR_1)
| ~ in(VAR_2,VAR_1)
| ~ is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d8_relat_2_sk]) ).
cnf(c_49,plain,
( ~ in(ordered_pair(sK1(A,B),sK2(A,B)),A)
| is_transitive_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_2]) ).
cnf(c_50,plain,
( in(ordered_pair(sK3(A,B),sK2(A,B)),A)
| is_transitive_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_2]) ).
cnf(c_51,plain,
( in(ordered_pair(sK1(A,B),sK3(A,B)),A)
| is_transitive_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_2]) ).
cnf(c_55,plain,
( in(ordered_pair(C,E),A)
| ~ in(ordered_pair(D,E),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(E,B)
| ~ in(D,B)
| ~ in(C,B)
| ~ is_transitive_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_2]) ).
cnf(c_57,plain,
( ~ is_transitive_in(A,relation_field(A))
| transitive(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[d16_relat_2]) ).
cnf(c_58,plain,
( is_transitive_in(A,relation_field(A))
| ~ transitive(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[d16_relat_2]) ).
cnf(c_63,negated_conjecture,
( is_transitive_in(sK0,relation_field(sK0))
| ~ transitive(sK0) ),
inference(resolve,[status(thm)],[c_58,c_42]) ).
cnf(c_67,negated_conjecture,
( ~ is_transitive_in(sK0,relation_field(sK0))
| transitive(sK0) ),
inference(resolve,[status(thm)],[c_57,c_42]) ).
cnf(c_79,negated_conjecture,
( in(ordered_pair(B,D),sK0)
| ~ in(ordered_pair(C,D),sK0)
| ~ in(ordered_pair(B,C),sK0)
| ~ in(D,A)
| ~ in(C,A)
| ~ in(B,A)
| ~ is_transitive_in(sK0,A) ),
inference(resolve,[status(thm)],[c_55,c_42]) ).
cnf(c_95,negated_conjecture,
( in(ordered_pair(sK1(sK0,A),sK3(sK0,A)),sK0)
| is_transitive_in(sK0,A) ),
inference(resolve,[status(thm)],[c_51,c_42]) ).
cnf(c_99,negated_conjecture,
( in(ordered_pair(sK3(sK0,A),sK2(sK0,A)),sK0)
| is_transitive_in(sK0,A) ),
inference(resolve,[status(thm)],[c_50,c_42]) ).
cnf(c_103,negated_conjecture,
( ~ in(ordered_pair(sK1(sK0,A),sK2(sK0,A)),sK0)
| is_transitive_in(sK0,A) ),
inference(resolve,[status(thm)],[c_49,c_42]) ).
cnf(c_113,negated_conjecture,
( in(A,relation_field(sK0))
| ~ in(ordered_pair(A,B),sK0) ),
inference(resolve,[status(thm)],[c_45,c_42]) ).
cnf(c_114,negated_conjecture,
( in(B,relation_field(sK0))
| ~ in(ordered_pair(A,B),sK0) ),
inference(resolve,[status(thm)],[c_44,c_42]) ).
cnf(c_116,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_118,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
cnf(c_132,negated_conjecture,
( in(ordered_pair(A,C),sK0)
| ~ in(ordered_pair(B,C),sK0)
| ~ in(ordered_pair(A,B),sK0)
| transitive(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l2_wellord1_neg]) ).
cnf(c_688,negated_conjecture,
( in(ordered_pair(A,C),sK0)
| ~ in(ordered_pair(B,C),sK0)
| ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),sK0)
| transitive(sK0) ),
inference(paramod,[status(thm)],[c_118,c_132]) ).
cnf(c_689,negated_conjecture,
( in(ordered_pair(A,C),sK0)
| ~ in(unordered_pair(unordered_pair(B,C),singleton(B)),sK0)
| ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),sK0)
| transitive(sK0) ),
inference(paramod,[status(thm)],[c_118,c_688]) ).
cnf(c_133,negated_conjecture,
( in(unordered_pair(unordered_pair(A,C),singleton(A)),sK0)
| ~ in(unordered_pair(unordered_pair(B,C),singleton(B)),sK0)
| ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),sK0)
| transitive(sK0) ),
inference(paramod,[status(thm)],[c_118,c_689]) ).
cnf(c_134,negated_conjecture,
( in(ordered_pair(sK4,sK5),sK0)
| ~ transitive(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l2_wellord1_neg]) ).
cnf(c_135,negated_conjecture,
( in(unordered_pair(unordered_pair(sK4,sK5),singleton(sK4)),sK0)
| ~ transitive(sK0) ),
inference(paramod,[status(thm)],[c_118,c_134]) ).
cnf(c_136,negated_conjecture,
( in(ordered_pair(sK5,sK6),sK0)
| ~ transitive(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l2_wellord1_neg]) ).
cnf(c_137,negated_conjecture,
( in(unordered_pair(unordered_pair(sK5,sK6),singleton(sK5)),sK0)
| ~ transitive(sK0) ),
inference(paramod,[status(thm)],[c_118,c_136]) ).
cnf(c_138,negated_conjecture,
( ~ in(ordered_pair(sK4,sK6),sK0)
| ~ transitive(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l2_wellord1_neg]) ).
cnf(c_139,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(sK4,sK6),singleton(sK4)),sK0)
| ~ transitive(sK0) ),
inference(paramod,[status(thm)],[c_118,c_138]) ).
cnf(c_153,negated_conjecture,
( in(B,relation_field(sK0))
| ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),sK0) ),
inference(paramod,[status(thm)],[c_118,c_114]) ).
cnf(c_154,negated_conjecture,
( in(A,relation_field(sK0))
| ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),sK0) ),
inference(paramod,[status(thm)],[c_118,c_113]) ).
cnf(c_164,negated_conjecture,
( ~ in(unordered_pair(unordered_pair(sK1(sK0,A),sK2(sK0,A)),singleton(sK1(sK0,A))),sK0)
| is_transitive_in(sK0,A) ),
inference(paramod,[status(thm)],[c_118,c_103]) ).
cnf(c_168,negated_conjecture,
( in(unordered_pair(unordered_pair(sK3(sK0,A),sK2(sK0,A)),singleton(sK3(sK0,A))),sK0)
| is_transitive_in(sK0,A) ),
inference(paramod,[status(thm)],[c_118,c_99]) ).
cnf(c_172,negated_conjecture,
( in(unordered_pair(unordered_pair(sK1(sK0,A),sK3(sK0,A)),singleton(sK1(sK0,A))),sK0)
| is_transitive_in(sK0,A) ),
inference(paramod,[status(thm)],[c_118,c_95]) ).
cnf(c_690,negated_conjecture,
( in(ordered_pair(B,D),sK0)
| ~ in(ordered_pair(C,D),sK0)
| ~ in(unordered_pair(unordered_pair(B,C),singleton(B)),sK0)
| ~ in(D,A)
| ~ in(C,A)
| ~ in(B,A)
| ~ is_transitive_in(sK0,A) ),
inference(paramod,[status(thm)],[c_118,c_79]) ).
cnf(c_691,negated_conjecture,
( in(ordered_pair(B,D),sK0)
| ~ in(unordered_pair(unordered_pair(C,D),singleton(C)),sK0)
| ~ in(unordered_pair(unordered_pair(B,C),singleton(B)),sK0)
| ~ in(D,A)
| ~ in(C,A)
| ~ in(B,A)
| ~ is_transitive_in(sK0,A) ),
inference(paramod,[status(thm)],[c_118,c_690]) ).
cnf(c_176,negated_conjecture,
( in(unordered_pair(unordered_pair(B,D),singleton(B)),sK0)
| ~ in(unordered_pair(unordered_pair(C,D),singleton(C)),sK0)
| ~ in(unordered_pair(unordered_pair(B,C),singleton(B)),sK0)
| ~ in(D,A)
| ~ in(C,A)
| ~ in(B,A)
| ~ is_transitive_in(sK0,A) ),
inference(paramod,[status(thm)],[c_118,c_691]) ).
cnf(c_231,plain,
( in(unordered_pair(unordered_pair(A,C),singleton(A)),sK0)
| ~ in(unordered_pair(unordered_pair(B,C),singleton(B)),sK0)
| ~ in(unordered_pair(singleton(A),unordered_pair(A,B)),sK0)
| transitive(sK0) ),
inference(paramod,[status(thm)],[c_116,c_133]) ).
cnf(c_290,plain,
( transitive(sK0)
| in(unordered_pair(unordered_pair(sK3(sK0,relation_field(sK0)),sK2(sK0,relation_field(sK0))),singleton(sK3(sK0,relation_field(sK0)))),sK0) ),
inference(resolve,[status(thm)],[c_168,c_67]) ).
cnf(c_302,plain,
( transitive(sK0)
| in(unordered_pair(unordered_pair(sK1(sK0,relation_field(sK0)),sK3(sK0,relation_field(sK0))),singleton(sK1(sK0,relation_field(sK0)))),sK0) ),
inference(resolve,[status(thm)],[c_172,c_67]) ).
cnf(c_692,plain,
( in(unordered_pair(unordered_pair(A,sK2(sK0,relation_field(sK0))),singleton(A)),sK0)
| ~ in(unordered_pair(singleton(A),unordered_pair(A,sK3(sK0,relation_field(sK0)))),sK0)
| transitive(sK0)
| transitive(sK0) ),
inference(resolve,[status(thm)],[c_290,c_231]) ).
cnf(c_693,plain,
( in(unordered_pair(unordered_pair(A,sK2(sK0,relation_field(sK0))),singleton(A)),sK0)
| ~ in(unordered_pair(unordered_pair(A,sK3(sK0,relation_field(sK0))),singleton(A)),sK0)
| transitive(sK0)
| transitive(sK0) ),
inference(paramod,[status(thm)],[c_116,c_692]) ).
cnf(c_560,plain,
( in(unordered_pair(unordered_pair(A,sK2(sK0,relation_field(sK0))),singleton(A)),sK0)
| ~ in(unordered_pair(unordered_pair(A,sK3(sK0,relation_field(sK0))),singleton(A)),sK0)
| transitive(sK0) ),
inference(copy,[status(thm)],[c_693]) ).
cnf(c_694,plain,
( transitive(sK0)
| in(unordered_pair(unordered_pair(sK1(sK0,relation_field(sK0)),sK2(sK0,relation_field(sK0))),singleton(sK1(sK0,relation_field(sK0)))),sK0)
| transitive(sK0) ),
inference(resolve,[status(thm)],[c_560,c_302]) ).
cnf(c_593,plain,
( in(unordered_pair(unordered_pair(sK1(sK0,relation_field(sK0)),sK2(sK0,relation_field(sK0))),singleton(sK1(sK0,relation_field(sK0)))),sK0)
| transitive(sK0) ),
inference(copy,[status(thm)],[c_694]) ).
cnf(c_620,plain,
( is_transitive_in(sK0,relation_field(sK0))
| transitive(sK0) ),
inference(resolve,[status(thm)],[c_593,c_164]) ).
cnf(c_695,negated_conjecture,
( transitive(sK0)
| transitive(sK0) ),
inference(resolve,[status(thm)],[c_620,c_67]) ).
cnf(c_623,negated_conjecture,
transitive(sK0),
inference(copy,[status(thm)],[c_695]) ).
cnf(c_624,negated_conjecture,
~ in(unordered_pair(unordered_pair(sK4,sK6),singleton(sK4)),sK0),
inference(resolve,[status(thm)],[c_623,c_139]) ).
cnf(c_625,negated_conjecture,
in(unordered_pair(unordered_pair(sK5,sK6),singleton(sK5)),sK0),
inference(resolve,[status(thm)],[c_623,c_137]) ).
cnf(c_626,negated_conjecture,
in(unordered_pair(unordered_pair(sK4,sK5),singleton(sK4)),sK0),
inference(resolve,[status(thm)],[c_623,c_135]) ).
cnf(c_627,negated_conjecture,
is_transitive_in(sK0,relation_field(sK0)),
inference(resolve,[status(thm)],[c_623,c_63]) ).
cnf(c_654,plain,
in(sK5,relation_field(sK0)),
inference(resolve,[status(thm)],[c_625,c_154]) ).
cnf(c_655,plain,
in(sK6,relation_field(sK0)),
inference(resolve,[status(thm)],[c_625,c_153]) ).
cnf(c_685,plain,
in(sK4,relation_field(sK0)),
inference(resolve,[status(thm)],[c_626,c_154]) ).
cnf(c_696,negated_conjecture,
( in(unordered_pair(unordered_pair(A,C),singleton(A)),sK0)
| ~ in(unordered_pair(unordered_pair(B,C),singleton(B)),sK0)
| ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),sK0)
| ~ in(C,relation_field(sK0))
| ~ in(B,relation_field(sK0))
| ~ in(A,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_176,c_627]) ).
cnf(c_697,negated_conjecture,
( in(unordered_pair(unordered_pair(A,B),singleton(A)),sK0)
| ~ in(unordered_pair(unordered_pair(sK5,B),singleton(sK5)),sK0)
| ~ in(unordered_pair(unordered_pair(A,sK5),singleton(A)),sK0)
| ~ in(B,relation_field(sK0))
| ~ in(A,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_696,c_654]) ).
cnf(c_698,negated_conjecture,
( in(unordered_pair(unordered_pair(A,sK6),singleton(A)),sK0)
| ~ in(unordered_pair(unordered_pair(sK5,sK6),singleton(sK5)),sK0)
| ~ in(unordered_pair(unordered_pair(A,sK5),singleton(A)),sK0)
| ~ in(A,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_697,c_655]) ).
cnf(c_699,negated_conjecture,
( in(unordered_pair(unordered_pair(sK4,sK6),singleton(sK4)),sK0)
| ~ in(unordered_pair(unordered_pair(sK5,sK6),singleton(sK5)),sK0)
| ~ in(sK4,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_698,c_626]) ).
cnf(c_700,negated_conjecture,
( in(unordered_pair(unordered_pair(sK4,sK6),singleton(sK4)),sK0)
| ~ in(sK4,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_699,c_625]) ).
cnf(c_701,negated_conjecture,
~ in(sK4,relation_field(sK0)),
inference(resolve,[status(thm)],[c_700,c_624]) ).
cnf(c_687,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_685,c_701]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU240+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n003.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sat Sep 26 08:59:09 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.44 % Process 2502019 was started by sandbox on n003,
% 0.16/0.44 % Sat Sep 26 08:59:09 2026
% 0.16/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.16/0.45
% 0.16/0.45 % From the command line: assign(max_seconds, 300).
% 0.22/0.67
% 0.22/0.67 % SZS status Theorem for theBenchmark
% 0.22/0.67
% 0.22/0.67 % Proof 1 at 0.16 (+ 0.04) seconds.
% 0.22/0.67 % Length of proof is 54.
% 0.22/0.67 % Level of proof is 11.
% 0.22/0.67 % Maximum clause weight is 36.000.
% 0.22/0.67 % Given clauses 235.
% 0.22/0.67
% 0.22/0.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------