%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU241+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 : n018.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.23s 0.61s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 6
% Syntax : Number of formulae : 100 ( 13 unt; 0 def)
% Number of atoms : 356 ( 100 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 414 ( 158 ~; 210 |; 33 &)
% ( 4 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 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 : 115 ( 5 sgn 46 !; 5 ?)
% 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_2,axiom,
! [A] :
( relation(A)
=> ( antisymmetric(A)
<=> is_antisymmetric_in(A,relation_field(A)) ) ),
file('theBenchmark.p',d12_relat_2) ).
fof(d4_relat_2,axiom,
! [A] :
( relation(A)
=> ! [B] :
( is_antisymmetric_in(A,B)
<=> ! [C,D] :
( ( in(ordered_pair(D,C),A)
& in(ordered_pair(C,D),A)
& in(D,B)
& in(C,B) )
=> C = D ) ) ),
file('theBenchmark.p',d4_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(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(l3_wellord1,conjecture,
! [A] :
( relation(A)
=> ( antisymmetric(A)
<=> ! [B,C] :
( ( in(ordered_pair(C,B),A)
& in(ordered_pair(B,C),A) )
=> B = C ) ) ),
file('theBenchmark.p',l3_wellord1) ).
fof(l3_wellord1_neg,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( antisymmetric(A)
<=> ! [B,C] :
( ( in(ordered_pair(C,B),A)
& in(ordered_pair(B,C),A) )
=> B = C ) ) ),
inference(assume_negation,[status(cth)],[l3_wellord1]) ).
fof(nnf_36,plain,
? [A] :
( ( ? [B,C] :
( C != B
& in(ordered_pair(C,B),A)
& in(ordered_pair(B,C),A) )
| ~ antisymmetric(A) )
& ( ! [X0,X1] :
( X1 = X0
| ~ in(ordered_pair(X1,X0),A)
| ~ in(ordered_pair(X0,X1),A) )
| antisymmetric(A) )
& relation(A) ),
inference(fof_nnf,[status(thm)],[l3_wellord1_neg]) ).
fof(sk_l3_wellord1_neg_sk,plain,
( ( ( sK4 != sK3
& in(ordered_pair(sK4,sK3),sK0)
& in(ordered_pair(sK3,sK4),sK0) )
| ~ antisymmetric(sK0) )
& ( ! [X0,X1] :
( X1 = X0
| ~ in(ordered_pair(X1,X0),sK0)
| ~ in(ordered_pair(X0,X1),sK0) )
| antisymmetric(sK0) )
& relation(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK3,sK4]),skolemize(A,sK0),skolemize(B,sK3),skolemize(C,sK4)],[nnf_36]) ).
fof(sk_l3_wellord1_neg,plain,
( ( sK4 != sK3
| ~ antisymmetric(sK0) )
& ( in(ordered_pair(sK4,sK3),sK0)
| ~ antisymmetric(sK0) )
& ( in(ordered_pair(sK3,sK4),sK0)
| ~ antisymmetric(sK0) )
& ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| ~ in(ordered_pair(VAR_1,VAR_0),sK0)
| ~ in(ordered_pair(VAR_0,VAR_1),sK0)
| antisymmetric(sK0) )
& relation(sK0) ),
inference(cnf_transformation,[status(thm)],[sk_l3_wellord1_neg_sk]) ).
cnf(c_42,negated_conjecture,
relation(sK0),
inference(split_conjunct,[status(thm)],[sk_l3_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_7,plain,
! [A] :
( ! [B] :
( ( ? [C,D] :
( D != C
& in(ordered_pair(D,C),A)
& in(ordered_pair(C,D),A)
& in(D,B)
& in(C,B) )
| is_antisymmetric_in(A,B) )
& ( ! [X0,X1] :
( X1 = X0
| ~ in(ordered_pair(X1,X0),A)
| ~ in(ordered_pair(X0,X1),A)
| ~ in(X1,B)
| ~ in(X0,B) )
| ~ is_antisymmetric_in(A,B) ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d4_relat_2]) ).
fof(sk_d4_relat_2_sk,plain,
! [A] :
( ! [B] :
( ( ( sK1(A,B) != sK2(A,B)
& in(ordered_pair(sK1(A,B),sK2(A,B)),A)
& in(ordered_pair(sK2(A,B),sK1(A,B)),A)
& in(sK1(A,B),B)
& in(sK2(A,B),B) )
| is_antisymmetric_in(A,B) )
& ( ! [X0,X1] :
( X1 = X0
| ~ in(ordered_pair(X1,X0),A)
| ~ in(ordered_pair(X0,X1),A)
| ~ in(X1,B)
| ~ in(X0,B) )
| ~ is_antisymmetric_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_7]) ).
fof(sk_d4_relat_2,plain,
( ! [VAR_0,VAR_1] :
( sK1(VAR_0,VAR_1) != sK2(VAR_0,VAR_1)
| is_antisymmetric_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1)),VAR_0)
| is_antisymmetric_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_antisymmetric_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK1(VAR_0,VAR_1),VAR_1)
| is_antisymmetric_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK2(VAR_0,VAR_1),VAR_1)
| is_antisymmetric_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_3 = VAR_2
| ~ in(ordered_pair(VAR_3,VAR_2),VAR_0)
| ~ in(ordered_pair(VAR_2,VAR_3),VAR_0)
| ~ in(VAR_3,VAR_1)
| ~ in(VAR_2,VAR_1)
| ~ is_antisymmetric_in(VAR_0,VAR_1)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d4_relat_2_sk]) ).
cnf(c_50,plain,
( sK1(A,B) != sK2(A,B)
| is_antisymmetric_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d4_relat_2]) ).
cnf(c_51,plain,
( in(ordered_pair(sK1(A,B),sK2(A,B)),A)
| is_antisymmetric_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d4_relat_2]) ).
cnf(c_52,plain,
( in(ordered_pair(sK2(A,B),sK1(A,B)),A)
| is_antisymmetric_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d4_relat_2]) ).
cnf(c_55,plain,
( D = C
| ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B)
| ~ is_antisymmetric_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d4_relat_2]) ).
cnf(c_56,plain,
( ~ is_antisymmetric_in(A,relation_field(A))
| antisymmetric(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[d12_relat_2]) ).
cnf(c_57,plain,
( is_antisymmetric_in(A,relation_field(A))
| ~ antisymmetric(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[d12_relat_2]) ).
cnf(c_62,negated_conjecture,
( is_antisymmetric_in(sK0,relation_field(sK0))
| ~ antisymmetric(sK0) ),
inference(resolve,[status(thm)],[c_57,c_42]) ).
cnf(c_66,negated_conjecture,
( ~ is_antisymmetric_in(sK0,relation_field(sK0))
| antisymmetric(sK0) ),
inference(resolve,[status(thm)],[c_56,c_42]) ).
cnf(c_70,negated_conjecture,
( C = B
| ~ in(ordered_pair(C,B),sK0)
| ~ in(ordered_pair(B,C),sK0)
| ~ in(C,A)
| ~ in(B,A)
| ~ is_antisymmetric_in(sK0,A) ),
inference(resolve,[status(thm)],[c_55,c_42]) ).
cnf(c_82,negated_conjecture,
( in(ordered_pair(sK2(sK0,A),sK1(sK0,A)),sK0)
| is_antisymmetric_in(sK0,A) ),
inference(resolve,[status(thm)],[c_52,c_42]) ).
cnf(c_86,negated_conjecture,
( in(ordered_pair(sK1(sK0,A),sK2(sK0,A)),sK0)
| is_antisymmetric_in(sK0,A) ),
inference(resolve,[status(thm)],[c_51,c_42]) ).
cnf(c_90,negated_conjecture,
( sK1(sK0,A) != sK2(sK0,A)
| is_antisymmetric_in(sK0,A) ),
inference(resolve,[status(thm)],[c_50,c_42]) ).
cnf(c_108,negated_conjecture,
( in(A,relation_field(sK0))
| ~ in(ordered_pair(A,B),sK0) ),
inference(resolve,[status(thm)],[c_45,c_42]) ).
cnf(c_109,negated_conjecture,
( in(B,relation_field(sK0))
| ~ in(ordered_pair(A,B),sK0) ),
inference(resolve,[status(thm)],[c_44,c_42]) ).
cnf(c_111,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_113,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
cnf(c_114,plain,
ordered_pair(A,B) = unordered_pair(singleton(A),unordered_pair(A,B)),
inference(paramod,[status(thm)],[c_111,c_113]) ).
cnf(c_128,negated_conjecture,
( B = A
| ~ in(ordered_pair(B,A),sK0)
| ~ in(ordered_pair(A,B),sK0)
| antisymmetric(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l3_wellord1_neg]) ).
cnf(c_699,negated_conjecture,
( B = A
| ~ in(ordered_pair(B,A),sK0)
| ~ in(unordered_pair(singleton(A),unordered_pair(A,B)),sK0)
| antisymmetric(sK0) ),
inference(paramod,[status(thm)],[c_114,c_128]) ).
cnf(c_129,negated_conjecture,
( B = A
| ~ in(unordered_pair(singleton(B),unordered_pair(B,A)),sK0)
| ~ in(unordered_pair(singleton(A),unordered_pair(A,B)),sK0)
| antisymmetric(sK0) ),
inference(paramod,[status(thm)],[c_114,c_699]) ).
cnf(c_130,negated_conjecture,
( in(ordered_pair(sK3,sK4),sK0)
| ~ antisymmetric(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l3_wellord1_neg]) ).
cnf(c_131,negated_conjecture,
( in(unordered_pair(singleton(sK3),unordered_pair(sK3,sK4)),sK0)
| ~ antisymmetric(sK0) ),
inference(paramod,[status(thm)],[c_114,c_130]) ).
cnf(c_132,negated_conjecture,
( in(ordered_pair(sK4,sK3),sK0)
| ~ antisymmetric(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l3_wellord1_neg]) ).
cnf(c_700,negated_conjecture,
( in(unordered_pair(singleton(sK4),unordered_pair(sK4,sK3)),sK0)
| ~ antisymmetric(sK0) ),
inference(paramod,[status(thm)],[c_114,c_132]) ).
cnf(c_133,negated_conjecture,
( in(unordered_pair(singleton(sK4),unordered_pair(sK3,sK4)),sK0)
| ~ antisymmetric(sK0) ),
inference(paramod,[status(thm)],[c_111,c_700]) ).
cnf(c_134,negated_conjecture,
( sK4 != sK3
| ~ antisymmetric(sK0) ),
inference(split_conjunct,[status(thm)],[sk_l3_wellord1_neg]) ).
cnf(c_136,negated_conjecture,
( in(B,relation_field(sK0))
| ~ in(unordered_pair(singleton(A),unordered_pair(A,B)),sK0) ),
inference(paramod,[status(thm)],[c_114,c_109]) ).
cnf(c_137,negated_conjecture,
( in(A,relation_field(sK0))
| ~ in(unordered_pair(singleton(A),unordered_pair(A,B)),sK0) ),
inference(paramod,[status(thm)],[c_114,c_108]) ).
cnf(c_701,negated_conjecture,
( in(unordered_pair(singleton(sK1(sK0,A)),unordered_pair(sK1(sK0,A),sK2(sK0,A))),sK0)
| is_antisymmetric_in(sK0,A) ),
inference(paramod,[status(thm)],[c_114,c_86]) ).
cnf(c_147,negated_conjecture,
( in(unordered_pair(singleton(sK1(sK0,A)),unordered_pair(sK2(sK0,A),sK1(sK0,A))),sK0)
| is_antisymmetric_in(sK0,A) ),
inference(paramod,[status(thm)],[c_111,c_701]) ).
cnf(c_151,negated_conjecture,
( in(unordered_pair(singleton(sK2(sK0,A)),unordered_pair(sK2(sK0,A),sK1(sK0,A))),sK0)
| is_antisymmetric_in(sK0,A) ),
inference(paramod,[status(thm)],[c_114,c_82]) ).
cnf(c_702,negated_conjecture,
( C = B
| ~ in(ordered_pair(C,B),sK0)
| ~ in(unordered_pair(singleton(B),unordered_pair(B,C)),sK0)
| ~ in(C,A)
| ~ in(B,A)
| ~ is_antisymmetric_in(sK0,A) ),
inference(paramod,[status(thm)],[c_114,c_70]) ).
cnf(c_155,negated_conjecture,
( C = B
| ~ in(unordered_pair(singleton(C),unordered_pair(C,B)),sK0)
| ~ in(unordered_pair(singleton(B),unordered_pair(B,C)),sK0)
| ~ in(C,A)
| ~ in(B,A)
| ~ is_antisymmetric_in(sK0,A) ),
inference(paramod,[status(thm)],[c_114,c_702]) ).
cnf(c_197,plain,
( antisymmetric(sK0)
| in(unordered_pair(singleton(sK1(sK0,relation_field(sK0))),unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0)))),sK0) ),
inference(resolve,[status(thm)],[c_147,c_66]) ).
cnf(c_200,plain,
( antisymmetric(sK0)
| in(unordered_pair(singleton(sK2(sK0,relation_field(sK0))),unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0)))),sK0) ),
inference(resolve,[status(thm)],[c_151,c_66]) ).
cnf(c_703,negated_conjecture,
( sK2(sK0,relation_field(sK0)) = sK1(sK0,relation_field(sK0))
| ~ in(unordered_pair(singleton(sK1(sK0,relation_field(sK0))),unordered_pair(sK1(sK0,relation_field(sK0)),sK2(sK0,relation_field(sK0)))),sK0)
| antisymmetric(sK0)
| antisymmetric(sK0) ),
inference(resolve,[status(thm)],[c_200,c_129]) ).
cnf(c_704,negated_conjecture,
( sK2(sK0,relation_field(sK0)) = sK1(sK0,relation_field(sK0))
| ~ in(unordered_pair(singleton(sK1(sK0,relation_field(sK0))),unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0)))),sK0)
| antisymmetric(sK0)
| antisymmetric(sK0) ),
inference(paramod,[status(thm)],[c_111,c_703]) ).
cnf(c_705,negated_conjecture,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| ~ in(unordered_pair(singleton(sK1(sK0,relation_field(sK0))),unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0)))),sK0)
| antisymmetric(sK0)
| antisymmetric(sK0) ),
inference(copy,[status(thm)],[c_704]) ).
cnf(c_306,negated_conjecture,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| ~ in(unordered_pair(singleton(sK1(sK0,relation_field(sK0))),unordered_pair(sK2(sK0,relation_field(sK0)),sK1(sK0,relation_field(sK0)))),sK0)
| antisymmetric(sK0) ),
inference(copy,[status(thm)],[c_705]) ).
cnf(c_706,plain,
( antisymmetric(sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| antisymmetric(sK0) ),
inference(resolve,[status(thm)],[c_306,c_197]) ).
cnf(c_404,plain,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| antisymmetric(sK0) ),
inference(copy,[status(thm)],[c_706]) ).
cnf(c_405,plain,
( sK4 != sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_404,c_134]) ).
cnf(c_406,plain,
( in(unordered_pair(singleton(sK4),unordered_pair(sK3,sK4)),sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_404,c_133]) ).
cnf(c_407,plain,
( in(unordered_pair(singleton(sK3),unordered_pair(sK3,sK4)),sK0)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_404,c_131]) ).
cnf(c_408,plain,
( is_antisymmetric_in(sK0,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_404,c_62]) ).
cnf(c_707,negated_conjecture,
( sK3 = sK4
| ~ in(unordered_pair(singleton(sK4),unordered_pair(sK4,sK3)),sK0)
| ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_407,c_155]) ).
cnf(c_708,negated_conjecture,
( sK3 = sK4
| ~ in(unordered_pair(singleton(sK4),unordered_pair(sK3,sK4)),sK0)
| ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(paramod,[status(thm)],[c_111,c_707]) ).
cnf(c_442,negated_conjecture,
( sK4 = sK3
| ~ in(unordered_pair(singleton(sK4),unordered_pair(sK3,sK4)),sK0)
| ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_708]) ).
cnf(c_446,plain,
( in(sK3,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_407,c_137]) ).
cnf(c_447,plain,
( in(sK4,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_407,c_136]) ).
cnf(c_709,plain,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| sK4 = sK3
| ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_442,c_406]) ).
cnf(c_497,plain,
( sK4 = sK3
| ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_709]) ).
cnf(c_710,plain,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| sK4 = sK3
| ~ in(sK3,relation_field(sK0))
| ~ in(sK4,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_497,c_408]) ).
cnf(c_498,plain,
( sK4 = sK3
| ~ in(sK3,relation_field(sK0))
| ~ in(sK4,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_710]) ).
cnf(c_711,plain,
( sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0))
| sK4 = sK3
| ~ in(sK3,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_498,c_447]) ).
cnf(c_505,plain,
( sK4 = sK3
| ~ in(sK3,relation_field(sK0))
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_711]) ).
cnf(c_712,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_505,c_446]) ).
cnf(c_507,plain,
( sK4 = sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_712]) ).
cnf(c_520,plain,
( is_antisymmetric_in(sK0,relation_field(sK0))
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_507,c_90]) ).
cnf(c_523,plain,
( antisymmetric(sK0)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_520,c_66]) ).
cnf(c_525,plain,
( in(unordered_pair(singleton(sK4),unordered_pair(sK3,sK4)),sK0)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_523,c_133]) ).
cnf(c_526,plain,
( in(unordered_pair(singleton(sK3),unordered_pair(sK3,sK4)),sK0)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_523,c_131]) ).
cnf(c_713,negated_conjecture,
( sK3 = sK4
| ~ in(unordered_pair(singleton(sK4),unordered_pair(sK4,sK3)),sK0)
| ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_526,c_155]) ).
cnf(c_714,negated_conjecture,
( sK3 = sK4
| ~ in(unordered_pair(singleton(sK4),unordered_pair(sK3,sK4)),sK0)
| ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK4 = sK3 ),
inference(paramod,[status(thm)],[c_111,c_713]) ).
cnf(c_715,negated_conjecture,
( sK4 = sK3
| ~ in(unordered_pair(singleton(sK4),unordered_pair(sK3,sK4)),sK0)
| ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_714]) ).
cnf(c_554,negated_conjecture,
( ~ in(unordered_pair(singleton(sK4),unordered_pair(sK3,sK4)),sK0)
| ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_715]) ).
cnf(c_558,plain,
( in(sK3,relation_field(sK0))
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_526,c_137]) ).
cnf(c_559,plain,
( in(sK4,relation_field(sK0))
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_526,c_136]) ).
cnf(c_716,plain,
( sK4 = sK3
| ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_554,c_525]) ).
cnf(c_642,plain,
( ~ in(sK3,A)
| ~ in(sK4,A)
| ~ is_antisymmetric_in(sK0,A)
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_716]) ).
cnf(c_717,plain,
( sK4 = sK3
| ~ in(sK3,relation_field(sK0))
| ~ in(sK4,relation_field(sK0))
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_642,c_520]) ).
cnf(c_643,plain,
( ~ in(sK3,relation_field(sK0))
| ~ in(sK4,relation_field(sK0))
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_717]) ).
cnf(c_718,plain,
( sK4 = sK3
| ~ in(sK3,relation_field(sK0))
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_643,c_559]) ).
cnf(c_650,plain,
( ~ in(sK3,relation_field(sK0))
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_718]) ).
cnf(c_719,plain,
( sK4 = sK3
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_650,c_558]) ).
cnf(c_652,plain,
sK4 = sK3,
inference(copy,[status(thm)],[c_719]) ).
cnf(c_720,plain,
( sK3 != sK3
| sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)) ),
inference(paramod,[status(thm)],[c_652,c_405]) ).
cnf(c_667,plain,
sK1(sK0,relation_field(sK0)) = sK2(sK0,relation_field(sK0)),
inference(copy,[status(thm)],[c_720]) ).
cnf(c_721,negated_conjecture,
( sK3 != sK3
| ~ antisymmetric(sK0) ),
inference(paramod,[status(thm)],[c_652,c_134]) ).
cnf(c_668,negated_conjecture,
~ antisymmetric(sK0),
inference(copy,[status(thm)],[c_721]) ).
cnf(c_688,negated_conjecture,
~ is_antisymmetric_in(sK0,relation_field(sK0)),
inference(resolve,[status(thm)],[c_668,c_66]) ).
cnf(c_722,negated_conjecture,
sK1(sK0,relation_field(sK0)) != sK2(sK0,relation_field(sK0)),
inference(resolve,[status(thm)],[c_90,c_688]) ).
cnf(c_723,negated_conjecture,
sK2(sK0,relation_field(sK0)) != sK2(sK0,relation_field(sK0)),
inference(paramod,[status(thm)],[c_667,c_722]) ).
cnf(c_698,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_723]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU241+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n018.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sat Sep 26 08:59:36 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.46 % Process 52009 was started by sandbox on n018,
% 0.19/0.46 % Sat Sep 26 08:59:36 2026
% 0.19/0.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.19/0.47
% 0.19/0.47 % From the command line: assign(max_seconds, 300).
% 0.23/0.61
% 0.23/0.61 % SZS status Theorem for theBenchmark
% 0.23/0.61
% 0.23/0.61 % Proof 1 at 0.09 (+ 0.03) seconds.
% 0.23/0.61 % Length of proof is 68.
% 0.23/0.61 % Level of proof is 23.
% 0.23/0.61 % Maximum clause weight is 55.000.
% 0.23/0.61 % Given clauses 230.
% 0.23/0.61
% 0.23/0.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------