%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU243+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 : n016.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 8.09s 1.63s
% Output : CNFRefutation 8.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 3
% Syntax : Number of formulae : 88 ( 10 unt; 0 def)
% Number of atoms : 335 ( 97 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 368 ( 121 ~; 205 |; 34 &)
% ( 4 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 92 ( 0 sgn 44 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d2_wellord1,axiom,
! [A] :
( relation(A)
=> ( well_founded_relation(A)
<=> ! [B] :
~ ( ! [C] :
~ ( disjoint(fiber(A,C),B)
& in(C,B) )
& B != empty_set
& subset(B,relation_field(A)) ) ) ),
file('theBenchmark.p',d2_wellord1) ).
fof(d3_wellord1,axiom,
! [A] :
( relation(A)
=> ! [B] :
( is_well_founded_in(A,B)
<=> ! [C] :
~ ( ! [D] :
~ ( disjoint(fiber(A,D),C)
& in(D,C) )
& C != empty_set
& subset(C,B) ) ) ),
file('theBenchmark.p',d3_wellord1) ).
fof(t5_wellord1,conjecture,
! [A] :
( relation(A)
=> ( well_founded_relation(A)
<=> is_well_founded_in(A,relation_field(A)) ) ),
file('theBenchmark.p',t5_wellord1) ).
fof(t5_wellord1_neg,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( well_founded_relation(A)
<=> is_well_founded_in(A,relation_field(A)) ) ),
inference(assume_negation,[status(cth)],[t5_wellord1]) ).
fof(nnf_36,plain,
? [A] :
( ( ~ is_well_founded_in(A,relation_field(A))
| ~ well_founded_relation(A) )
& ( is_well_founded_in(A,relation_field(A))
| well_founded_relation(A) )
& relation(A) ),
inference(fof_nnf,[status(thm)],[t5_wellord1_neg]) ).
fof(sk_t5_wellord1_neg,plain,
( ( ~ is_well_founded_in(sK0,relation_field(sK0))
| ~ well_founded_relation(sK0) )
& ( is_well_founded_in(sK0,relation_field(sK0))
| well_founded_relation(sK0) )
& relation(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_36]) ).
cnf(c_42,negated_conjecture,
relation(sK0),
inference(split_conjunct,[status(thm)],[sk_t5_wellord1_neg]) ).
fof(nnf_6,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ! [D] :
( ~ disjoint(fiber(A,D),C)
| ~ in(D,C) )
& C != empty_set
& subset(C,B) )
| is_well_founded_in(A,B) )
& ( ! [X0] :
( ? [X1] :
( disjoint(fiber(A,X1),X0)
& in(X1,X0) )
| X0 = empty_set
| ~ subset(X0,B) )
| ~ is_well_founded_in(A,B) ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d3_wellord1]) ).
fof(sk_d3_wellord1_sk,plain,
! [A] :
( ! [B] :
( ( ( ! [D] :
( ~ disjoint(fiber(A,D),sK1(A,B))
| ~ in(D,sK1(A,B)) )
& sK1(A,B) != empty_set
& subset(sK1(A,B),B) )
| is_well_founded_in(A,B) )
& ( ! [X0] :
( ( disjoint(fiber(A,sK2(A,B,X0)),X0)
& in(sK2(A,B,X0),X0) )
| X0 = empty_set
| ~ subset(X0,B) )
| ~ is_well_founded_in(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK1]),skolemize(X1,sK2(A,B,X0)),skolemize(C,sK1(A,B))],[nnf_6]) ).
fof(sk_d3_wellord1,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ disjoint(fiber(VAR_0,VAR_2),sK1(VAR_0,VAR_1))
| ~ in(VAR_2,sK1(VAR_0,VAR_1))
| is_well_founded_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( sK1(VAR_0,VAR_1) != empty_set
| is_well_founded_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( subset(sK1(VAR_0,VAR_1),VAR_1)
| is_well_founded_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( disjoint(fiber(VAR_0,sK2(VAR_0,VAR_1,VAR_2)),VAR_2)
| VAR_2 = empty_set
| ~ subset(VAR_2,VAR_1)
| ~ is_well_founded_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK2(VAR_0,VAR_1,VAR_2),VAR_2)
| VAR_2 = empty_set
| ~ subset(VAR_2,VAR_1)
| ~ is_well_founded_in(VAR_0,VAR_1)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d3_wellord1_sk]) ).
cnf(c_48,plain,
( ~ disjoint(fiber(A,C),sK1(A,B))
| ~ in(C,sK1(A,B))
| is_well_founded_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d3_wellord1]) ).
cnf(c_49,plain,
( sK1(A,B) != empty_set
| is_well_founded_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d3_wellord1]) ).
cnf(c_50,plain,
( subset(sK1(A,B),B)
| is_well_founded_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d3_wellord1]) ).
cnf(c_51,plain,
( disjoint(fiber(A,sK2(A,B,C)),C)
| C = empty_set
| ~ subset(C,B)
| ~ is_well_founded_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d3_wellord1]) ).
cnf(c_52,plain,
( in(sK2(A,B,C),C)
| C = empty_set
| ~ subset(C,B)
| ~ is_well_founded_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d3_wellord1]) ).
fof(nnf_5,plain,
! [A] :
( ( ( ? [B] :
( ! [C] :
( ~ disjoint(fiber(A,C),B)
| ~ in(C,B) )
& empty_set != B
& subset(B,relation_field(A)) )
| well_founded_relation(A) )
& ( ! [X0] :
( ? [X1] :
( disjoint(fiber(A,X1),X0)
& in(X1,X0) )
| empty_set = X0
| ~ subset(X0,relation_field(A)) )
| ~ well_founded_relation(A) ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d2_wellord1]) ).
fof(sk_d2_wellord1_sk,plain,
! [A] :
( ( ( ( ! [C] :
( ~ disjoint(fiber(A,C),sK3(A))
| ~ in(C,sK3(A)) )
& empty_set != sK3(A)
& subset(sK3(A),relation_field(A)) )
| well_founded_relation(A) )
& ( ! [X0] :
( ( disjoint(fiber(A,sK4(A,X0)),X0)
& in(sK4(A,X0),X0) )
| empty_set = X0
| ~ subset(X0,relation_field(A)) )
| ~ well_founded_relation(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK3]),skolemize(X1,sK4(A,X0)),skolemize(B,sK3(A))],[nnf_5]) ).
fof(sk_d2_wellord1,plain,
( ! [VAR_0,VAR_1] :
( ~ disjoint(fiber(VAR_0,VAR_1),sK3(VAR_0))
| ~ in(VAR_1,sK3(VAR_0))
| well_founded_relation(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0] :
( empty_set != sK3(VAR_0)
| well_founded_relation(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0] :
( subset(sK3(VAR_0),relation_field(VAR_0))
| well_founded_relation(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( disjoint(fiber(VAR_0,sK4(VAR_0,VAR_1)),VAR_1)
| empty_set = VAR_1
| ~ subset(VAR_1,relation_field(VAR_0))
| ~ well_founded_relation(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK4(VAR_0,VAR_1),VAR_1)
| empty_set = VAR_1
| ~ subset(VAR_1,relation_field(VAR_0))
| ~ well_founded_relation(VAR_0)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d2_wellord1_sk]) ).
cnf(c_53,plain,
( ~ disjoint(fiber(A,B),sK3(A))
| ~ in(B,sK3(A))
| well_founded_relation(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d2_wellord1]) ).
cnf(c_54,plain,
( empty_set != sK3(A)
| well_founded_relation(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d2_wellord1]) ).
cnf(c_55,plain,
( subset(sK3(A),relation_field(A))
| well_founded_relation(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d2_wellord1]) ).
cnf(c_56,plain,
( disjoint(fiber(A,sK4(A,B)),B)
| empty_set = B
| ~ subset(B,relation_field(A))
| ~ well_founded_relation(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d2_wellord1]) ).
cnf(c_57,plain,
( in(sK4(A,B),B)
| empty_set = B
| ~ subset(B,relation_field(A))
| ~ well_founded_relation(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d2_wellord1]) ).
cnf(c_58,negated_conjecture,
( ~ is_well_founded_in(sK0,relation_field(sK0))
| ~ well_founded_relation(sK0) ),
inference(split_conjunct,[status(thm)],[sk_t5_wellord1_neg]) ).
cnf(c_59,negated_conjecture,
( is_well_founded_in(sK0,relation_field(sK0))
| well_founded_relation(sK0) ),
inference(split_conjunct,[status(thm)],[sk_t5_wellord1_neg]) ).
cnf(c_93,negated_conjecture,
( ~ disjoint(fiber(sK0,B),sK1(sK0,A))
| ~ in(B,sK1(sK0,A))
| is_well_founded_in(sK0,A) ),
inference(resolve,[status(thm)],[c_48,c_42]) ).
cnf(c_97,negated_conjecture,
( sK1(sK0,A) != empty_set
| is_well_founded_in(sK0,A) ),
inference(resolve,[status(thm)],[c_49,c_42]) ).
cnf(c_101,negated_conjecture,
( subset(sK1(sK0,A),A)
| is_well_founded_in(sK0,A) ),
inference(resolve,[status(thm)],[c_50,c_42]) ).
cnf(c_108,negated_conjecture,
( disjoint(fiber(sK0,sK2(sK0,A,B)),B)
| B = empty_set
| ~ subset(B,A)
| ~ is_well_founded_in(sK0,A) ),
inference(resolve,[status(thm)],[c_51,c_42]) ).
cnf(c_109,negated_conjecture,
( disjoint(fiber(sK0,sK2(sK0,A,B)),B)
| empty_set = B
| ~ subset(B,A)
| ~ is_well_founded_in(sK0,A) ),
inference(copy,[status(thm)],[c_108]) ).
cnf(c_116,negated_conjecture,
( in(sK2(sK0,A,B),B)
| B = empty_set
| ~ subset(B,A)
| ~ is_well_founded_in(sK0,A) ),
inference(resolve,[status(thm)],[c_52,c_42]) ).
cnf(c_117,negated_conjecture,
( in(sK2(sK0,A,B),B)
| empty_set = B
| ~ subset(B,A)
| ~ is_well_founded_in(sK0,A) ),
inference(copy,[status(thm)],[c_116]) ).
cnf(c_121,negated_conjecture,
( ~ disjoint(fiber(sK0,A),sK3(sK0))
| ~ in(A,sK3(sK0))
| well_founded_relation(sK0) ),
inference(resolve,[status(thm)],[c_53,c_42]) ).
cnf(c_128,negated_conjecture,
( empty_set != sK3(sK0)
| well_founded_relation(sK0) ),
inference(resolve,[status(thm)],[c_54,c_42]) ).
cnf(c_129,negated_conjecture,
( sK3(sK0) != empty_set
| well_founded_relation(sK0) ),
inference(copy,[status(thm)],[c_128]) ).
cnf(c_133,negated_conjecture,
( subset(sK3(sK0),relation_field(sK0))
| well_founded_relation(sK0) ),
inference(resolve,[status(thm)],[c_55,c_42]) ).
cnf(c_137,negated_conjecture,
( disjoint(fiber(sK0,sK4(sK0,A)),A)
| empty_set = A
| ~ subset(A,relation_field(sK0))
| ~ well_founded_relation(sK0) ),
inference(resolve,[status(thm)],[c_56,c_42]) ).
cnf(c_141,negated_conjecture,
( in(sK4(sK0,A),A)
| empty_set = A
| ~ subset(A,relation_field(sK0))
| ~ well_founded_relation(sK0) ),
inference(resolve,[status(thm)],[c_57,c_42]) ).
cnf(c_172,plain,
( ~ well_founded_relation(sK0)
| subset(sK1(sK0,relation_field(sK0)),relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_101,c_58]) ).
cnf(c_3083,negated_conjecture,
( well_founded_relation(sK0)
| in(sK2(sK0,relation_field(sK0),A),A)
| empty_set = A
| ~ subset(A,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_117,c_59]) ).
cnf(c_3084,negated_conjecture,
( well_founded_relation(sK0)
| well_founded_relation(sK0)
| in(sK2(sK0,relation_field(sK0),sK3(sK0)),sK3(sK0))
| empty_set = sK3(sK0) ),
inference(resolve,[status(thm)],[c_3083,c_133]) ).
cnf(c_3085,negated_conjecture,
( well_founded_relation(sK0)
| well_founded_relation(sK0)
| in(sK2(sK0,relation_field(sK0),sK3(sK0)),sK3(sK0))
| sK3(sK0) = empty_set ),
inference(copy,[status(thm)],[c_3084]) ).
cnf(c_205,negated_conjecture,
( well_founded_relation(sK0)
| in(sK2(sK0,relation_field(sK0),sK3(sK0)),sK3(sK0))
| sK3(sK0) = empty_set ),
inference(copy,[status(thm)],[c_3085]) ).
cnf(c_3086,negated_conjecture,
( well_founded_relation(sK0)
| disjoint(fiber(sK0,sK2(sK0,relation_field(sK0),A)),A)
| empty_set = A
| ~ subset(A,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_109,c_59]) ).
cnf(c_3087,negated_conjecture,
( well_founded_relation(sK0)
| well_founded_relation(sK0)
| disjoint(fiber(sK0,sK2(sK0,relation_field(sK0),sK3(sK0))),sK3(sK0))
| empty_set = sK3(sK0) ),
inference(resolve,[status(thm)],[c_3086,c_133]) ).
cnf(c_3088,negated_conjecture,
( well_founded_relation(sK0)
| well_founded_relation(sK0)
| disjoint(fiber(sK0,sK2(sK0,relation_field(sK0),sK3(sK0))),sK3(sK0))
| sK3(sK0) = empty_set ),
inference(copy,[status(thm)],[c_3087]) ).
cnf(c_209,negated_conjecture,
( well_founded_relation(sK0)
| disjoint(fiber(sK0,sK2(sK0,relation_field(sK0),sK3(sK0))),sK3(sK0))
| sK3(sK0) = empty_set ),
inference(copy,[status(thm)],[c_3088]) ).
cnf(c_3089,negated_conjecture,
( well_founded_relation(sK0)
| sK3(sK0) = empty_set
| ~ disjoint(fiber(sK0,sK2(sK0,relation_field(sK0),sK3(sK0))),sK3(sK0))
| well_founded_relation(sK0) ),
inference(resolve,[status(thm)],[c_121,c_205]) ).
cnf(c_3090,negated_conjecture,
( well_founded_relation(sK0)
| sK3(sK0) = empty_set
| well_founded_relation(sK0)
| sK3(sK0) = empty_set
| well_founded_relation(sK0) ),
inference(resolve,[status(thm)],[c_3089,c_209]) ).
cnf(c_3091,negated_conjecture,
( well_founded_relation(sK0)
| sK3(sK0) = empty_set
| sK3(sK0) = empty_set
| well_founded_relation(sK0) ),
inference(copy,[status(thm)],[c_3090]) ).
cnf(c_3092,negated_conjecture,
( well_founded_relation(sK0)
| sK3(sK0) = empty_set
| well_founded_relation(sK0) ),
inference(copy,[status(thm)],[c_3091]) ).
cnf(c_869,negated_conjecture,
( sK3(sK0) = empty_set
| well_founded_relation(sK0) ),
inference(copy,[status(thm)],[c_3092]) ).
cnf(c_872,plain,
( subset(sK1(sK0,relation_field(sK0)),relation_field(sK0))
| sK3(sK0) = empty_set ),
inference(resolve,[status(thm)],[c_869,c_172]) ).
cnf(c_3093,negated_conjecture,
( sK3(sK0) = empty_set
| in(sK4(sK0,A),A)
| empty_set = A
| ~ subset(A,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_141,c_869]) ).
cnf(c_3094,negated_conjecture,
( sK3(sK0) = empty_set
| sK3(sK0) = empty_set
| in(sK4(sK0,sK1(sK0,relation_field(sK0))),sK1(sK0,relation_field(sK0)))
| empty_set = sK1(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_3093,c_872]) ).
cnf(c_3095,negated_conjecture,
( sK3(sK0) = empty_set
| sK3(sK0) = empty_set
| in(sK4(sK0,sK1(sK0,relation_field(sK0))),sK1(sK0,relation_field(sK0)))
| sK1(sK0,relation_field(sK0)) = empty_set ),
inference(copy,[status(thm)],[c_3094]) ).
cnf(c_892,negated_conjecture,
( sK3(sK0) = empty_set
| in(sK4(sK0,sK1(sK0,relation_field(sK0))),sK1(sK0,relation_field(sK0)))
| sK1(sK0,relation_field(sK0)) = empty_set ),
inference(copy,[status(thm)],[c_3095]) ).
cnf(c_3096,negated_conjecture,
( sK3(sK0) = empty_set
| disjoint(fiber(sK0,sK4(sK0,A)),A)
| empty_set = A
| ~ subset(A,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_137,c_869]) ).
cnf(c_3097,negated_conjecture,
( sK3(sK0) = empty_set
| sK3(sK0) = empty_set
| disjoint(fiber(sK0,sK4(sK0,sK1(sK0,relation_field(sK0)))),sK1(sK0,relation_field(sK0)))
| empty_set = sK1(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_3096,c_872]) ).
cnf(c_3098,negated_conjecture,
( sK3(sK0) = empty_set
| sK3(sK0) = empty_set
| disjoint(fiber(sK0,sK4(sK0,sK1(sK0,relation_field(sK0)))),sK1(sK0,relation_field(sK0)))
| sK1(sK0,relation_field(sK0)) = empty_set ),
inference(copy,[status(thm)],[c_3097]) ).
cnf(c_893,negated_conjecture,
( sK3(sK0) = empty_set
| disjoint(fiber(sK0,sK4(sK0,sK1(sK0,relation_field(sK0)))),sK1(sK0,relation_field(sK0)))
| sK1(sK0,relation_field(sK0)) = empty_set ),
inference(copy,[status(thm)],[c_3098]) ).
cnf(c_3099,negated_conjecture,
( sK3(sK0) = empty_set
| sK1(sK0,relation_field(sK0)) = empty_set
| ~ disjoint(fiber(sK0,sK4(sK0,sK1(sK0,relation_field(sK0)))),sK1(sK0,relation_field(sK0)))
| is_well_founded_in(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_93,c_892]) ).
cnf(c_3100,negated_conjecture,
( sK3(sK0) = empty_set
| sK1(sK0,relation_field(sK0)) = empty_set
| sK3(sK0) = empty_set
| sK1(sK0,relation_field(sK0)) = empty_set
| is_well_founded_in(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_3099,c_893]) ).
cnf(c_3101,negated_conjecture,
( sK3(sK0) = empty_set
| sK3(sK0) = empty_set
| sK1(sK0,relation_field(sK0)) = empty_set
| is_well_founded_in(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_3100]) ).
cnf(c_2917,negated_conjecture,
( sK3(sK0) = empty_set
| sK1(sK0,relation_field(sK0)) = empty_set
| is_well_founded_in(sK0,relation_field(sK0)) ),
inference(copy,[status(thm)],[c_3101]) ).
cnf(c_3102,negated_conjecture,
( sK3(sK0) = empty_set
| ~ is_well_founded_in(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_58,c_869]) ).
cnf(c_3103,negated_conjecture,
( sK3(sK0) = empty_set
| sK1(sK0,relation_field(sK0)) = empty_set
| sK3(sK0) = empty_set ),
inference(resolve,[status(thm)],[c_3102,c_2917]) ).
cnf(c_2935,negated_conjecture,
( sK1(sK0,relation_field(sK0)) = empty_set
| sK3(sK0) = empty_set ),
inference(copy,[status(thm)],[c_3103]) ).
cnf(c_2936,plain,
( is_well_founded_in(sK0,relation_field(sK0))
| sK3(sK0) = empty_set ),
inference(resolve,[status(thm)],[c_2935,c_97]) ).
cnf(c_3104,negated_conjecture,
( sK3(sK0) = empty_set
| ~ is_well_founded_in(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_58,c_869]) ).
cnf(c_3105,negated_conjecture,
( sK3(sK0) = empty_set
| sK3(sK0) = empty_set ),
inference(resolve,[status(thm)],[c_3104,c_2936]) ).
cnf(c_2958,negated_conjecture,
sK3(sK0) = empty_set,
inference(copy,[status(thm)],[c_3105]) ).
cnf(c_3106,negated_conjecture,
( empty_set != empty_set
| well_founded_relation(sK0) ),
inference(paramod,[status(thm)],[c_2958,c_129]) ).
cnf(c_2962,negated_conjecture,
well_founded_relation(sK0),
inference(copy,[status(thm)],[c_3106]) ).
cnf(c_2976,negated_conjecture,
subset(sK1(sK0,relation_field(sK0)),relation_field(sK0)),
inference(resolve,[status(thm)],[c_2962,c_172]) ).
cnf(c_2977,negated_conjecture,
( in(sK4(sK0,A),A)
| empty_set = A
| ~ subset(A,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_2962,c_141]) ).
cnf(c_2978,negated_conjecture,
( disjoint(fiber(sK0,sK4(sK0,A)),A)
| empty_set = A
| ~ subset(A,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_2962,c_137]) ).
cnf(c_2979,negated_conjecture,
~ is_well_founded_in(sK0,relation_field(sK0)),
inference(resolve,[status(thm)],[c_2962,c_58]) ).
cnf(c_2981,negated_conjecture,
sK1(sK0,relation_field(sK0)) != empty_set,
inference(resolve,[status(thm)],[c_97,c_2979]) ).
cnf(c_3107,negated_conjecture,
( in(sK4(sK0,sK1(sK0,relation_field(sK0))),sK1(sK0,relation_field(sK0)))
| empty_set = sK1(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_2977,c_2976]) ).
cnf(c_3108,negated_conjecture,
( in(sK4(sK0,sK1(sK0,relation_field(sK0))),sK1(sK0,relation_field(sK0)))
| sK1(sK0,relation_field(sK0)) = empty_set ),
inference(copy,[status(thm)],[c_3107]) ).
cnf(c_3002,negated_conjecture,
in(sK4(sK0,sK1(sK0,relation_field(sK0))),sK1(sK0,relation_field(sK0))),
inference(resolve,[status(thm)],[c_2981,c_3108]) ).
cnf(c_3109,negated_conjecture,
( disjoint(fiber(sK0,sK4(sK0,sK1(sK0,relation_field(sK0)))),sK1(sK0,relation_field(sK0)))
| empty_set = sK1(sK0,relation_field(sK0)) ),
inference(resolve,[status(thm)],[c_2978,c_2976]) ).
cnf(c_3110,negated_conjecture,
( disjoint(fiber(sK0,sK4(sK0,sK1(sK0,relation_field(sK0)))),sK1(sK0,relation_field(sK0)))
| sK1(sK0,relation_field(sK0)) = empty_set ),
inference(copy,[status(thm)],[c_3109]) ).
cnf(c_3070,negated_conjecture,
disjoint(fiber(sK0,sK4(sK0,sK1(sK0,relation_field(sK0)))),sK1(sK0,relation_field(sK0))),
inference(resolve,[status(thm)],[c_2981,c_3110]) ).
cnf(c_3111,negated_conjecture,
( ~ disjoint(fiber(sK0,A),sK1(sK0,relation_field(sK0)))
| ~ in(A,sK1(sK0,relation_field(sK0))) ),
inference(resolve,[status(thm)],[c_93,c_2979]) ).
cnf(c_3112,negated_conjecture,
~ disjoint(fiber(sK0,sK4(sK0,sK1(sK0,relation_field(sK0)))),sK1(sK0,relation_field(sK0))),
inference(resolve,[status(thm)],[c_3111,c_3002]) ).
cnf(c_3082,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3070,c_3112]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU243+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.10/0.57 % Computer : n016.cluster.edu
% 0.10/0.57 % Model : x86_64 x86_64
% 0.10/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.57 % Memory : 8046.5625MB
% 0.10/0.57 % OS : Linux 6.8.0-71-generic
% 0.10/0.57 % CPULimit : 300
% 0.10/0.57 % WCLimit : 300
% 0.10/0.57 % DateTime : Sat Sep 26 09:02:16 UTC 2026
% 0.10/0.58 % CPUTime :
% 0.10/0.58 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.58 % Process 493702 was started by sandbox on n016,
% 0.10/0.58 % Sat Sep 26 09:02:16 2026
% 0.10/0.58 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.59
% 0.10/0.59 % From the command line: assign(max_seconds, 300).
% 8.09/1.63
% 8.09/1.63 % given #500 (F,wt=55): 1042 -element(set_union2(set_union2(A,set_union2(c4,B)),C),set_union2(set_union2(A,set_union2(B,c4)),C)). [para(80(a,1),630(a,1,1,2))].
% 8.09/1.63
% 8.09/1.63 % given #1000 (T,wt=29): 2917 is_well_founded_in(c6,relation_field(c6)) | f4(c6,relation_field(c6)) = empty_set | f2(c6) = empty_set. [hyper(93,b,892,b,c,893,b),merge(d),merge(e)].
% 8.09/1.63
% 8.09/1.63 % SZS status Theorem for theBenchmark
% 8.09/1.63
% 8.09/1.63 % Proof 1 at 0.80 (+ 0.22) seconds.
% 8.09/1.63 % Length of proof is 49.
% 8.09/1.63 % Level of proof is 16.
% 8.09/1.63 % Maximum clause weight is 48.000.
% 8.09/1.63 % Given clauses 1043.
% 8.09/1.63
% 8.09/1.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------