%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU284+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 : n005.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:41 AM UTC 2026
% Result : Theorem 0.05s 0.48s
% Output : CNFRefutation 0.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 2
% Syntax : Number of formulae : 123 ( 10 unt; 0 def)
% Number of atoms : 510 ( 345 equ)
% Maximal formula atoms : 104 ( 4 avg)
% Number of connectives : 624 ( 237 ~; 321 |; 61 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 39 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 1 con; 0-2 aty)
% Number of variables : 210 ( 34 sgn 77 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(s2_funct_1__e16_22__wellord2__1,axiom,
! [A] :
( ( ! [B] :
~ ( ! [C] : C != singleton(B)
& in(B,A) )
& ! [B,C,D] :
( ( D = singleton(B)
& C = singleton(B)
& in(B,A) )
=> C = D ) )
=> ? [B] :
( ! [C] :
( in(C,A)
=> apply(B,C) = singleton(C) )
& relation_dom(B) = A
& function(B)
& relation(B) ) ),
file('theBenchmark.p',s2_funct_1__e16_22__wellord2__1) ).
fof(s3_funct_1__e16_22__wellord2,conjecture,
! [A] :
? [B] :
( ! [C] :
( in(C,A)
=> apply(B,C) = singleton(C) )
& relation_dom(B) = A
& function(B)
& relation(B) ),
file('theBenchmark.p',s3_funct_1__e16_22__wellord2) ).
fof(s3_funct_1__e16_22__wellord2_neg,negated_conjecture,
~ ! [A] :
? [B] :
( ! [C] :
( in(C,A)
=> apply(B,C) = singleton(C) )
& relation_dom(B) = A
& function(B)
& relation(B) ),
inference(assume_negation,[status(cth)],[s3_funct_1__e16_22__wellord2]) ).
fof(nnf_6,plain,
! [A] :
( ? [B] :
( ! [C] :
( singleton(C) = apply(B,C)
| ~ in(C,A) )
& relation_dom(B) = A
& function(B)
& relation(B) )
| ? [X2] :
( ! [X3] : singleton(X2) != X3
& in(X2,A) )
| ? [X0,X1,D] :
( D != X1
& singleton(X0) = D
& singleton(X0) = X1
& in(X0,A) ) ),
inference(fof_nnf,[status(thm)],[s2_funct_1__e16_22__wellord2__1]) ).
fof(sk_s2_funct_1__e16_22__wellord2__1_sk,plain,
! [A] :
( ( ! [C] :
( singleton(C) = apply(sK3(A),C)
| ~ in(C,A) )
& relation_dom(sK3(A)) = A
& function(sK3(A))
& relation(sK3(A)) )
| ( ! [X3] : singleton(sK2(A)) != X3
& in(sK2(A),A) )
| ( sK0(A) != sK1(A)
& singleton(sK4(A)) = sK0(A)
& singleton(sK4(A)) = sK1(A)
& in(sK4(A),A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK1,sK0,sK2,sK3]),skolemize(X0,sK4(A)),skolemize(X1,sK1(A)),skolemize(D,sK0(A)),skolemize(X2,sK2(A)),skolemize(B,sK3(A))],[nnf_6]) ).
fof(sk_s2_funct_1__e16_22__wellord2__1,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( singleton(VAR_2) = apply(sK3(VAR_0),VAR_2)
| ~ in(VAR_2,VAR_0)
| singleton(sK2(VAR_0)) != VAR_1
| sK0(VAR_0) != sK1(VAR_0) )
& ! [VAR_0,VAR_1] :
( relation_dom(sK3(VAR_0)) = VAR_0
| singleton(sK2(VAR_0)) != VAR_1
| sK0(VAR_0) != sK1(VAR_0) )
& ! [VAR_0,VAR_1] :
( function(sK3(VAR_0))
| singleton(sK2(VAR_0)) != VAR_1
| sK0(VAR_0) != sK1(VAR_0) )
& ! [VAR_0,VAR_1] :
( relation(sK3(VAR_0))
| singleton(sK2(VAR_0)) != VAR_1
| sK0(VAR_0) != sK1(VAR_0) )
& ! [VAR_0,VAR_1] :
( singleton(VAR_1) = apply(sK3(VAR_0),VAR_1)
| ~ in(VAR_1,VAR_0)
| in(sK2(VAR_0),VAR_0)
| sK0(VAR_0) != sK1(VAR_0) )
& ! [VAR_0] :
( relation_dom(sK3(VAR_0)) = VAR_0
| in(sK2(VAR_0),VAR_0)
| sK0(VAR_0) != sK1(VAR_0) )
& ! [VAR_0] :
( function(sK3(VAR_0))
| in(sK2(VAR_0),VAR_0)
| sK0(VAR_0) != sK1(VAR_0) )
& ! [VAR_0] :
( relation(sK3(VAR_0))
| in(sK2(VAR_0),VAR_0)
| sK0(VAR_0) != sK1(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(VAR_2) = apply(sK3(VAR_0),VAR_2)
| ~ in(VAR_2,VAR_0)
| singleton(sK2(VAR_0)) != VAR_1
| singleton(sK4(VAR_0)) = sK0(VAR_0) )
& ! [VAR_0,VAR_1] :
( relation_dom(sK3(VAR_0)) = VAR_0
| singleton(sK2(VAR_0)) != VAR_1
| singleton(sK4(VAR_0)) = sK0(VAR_0) )
& ! [VAR_0,VAR_1] :
( function(sK3(VAR_0))
| singleton(sK2(VAR_0)) != VAR_1
| singleton(sK4(VAR_0)) = sK0(VAR_0) )
& ! [VAR_0,VAR_1] :
( relation(sK3(VAR_0))
| singleton(sK2(VAR_0)) != VAR_1
| singleton(sK4(VAR_0)) = sK0(VAR_0) )
& ! [VAR_0,VAR_1] :
( singleton(VAR_1) = apply(sK3(VAR_0),VAR_1)
| ~ in(VAR_1,VAR_0)
| in(sK2(VAR_0),VAR_0)
| singleton(sK4(VAR_0)) = sK0(VAR_0) )
& ! [VAR_0] :
( relation_dom(sK3(VAR_0)) = VAR_0
| in(sK2(VAR_0),VAR_0)
| singleton(sK4(VAR_0)) = sK0(VAR_0) )
& ! [VAR_0] :
( function(sK3(VAR_0))
| in(sK2(VAR_0),VAR_0)
| singleton(sK4(VAR_0)) = sK0(VAR_0) )
& ! [VAR_0] :
( relation(sK3(VAR_0))
| in(sK2(VAR_0),VAR_0)
| singleton(sK4(VAR_0)) = sK0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(VAR_2) = apply(sK3(VAR_0),VAR_2)
| ~ in(VAR_2,VAR_0)
| singleton(sK2(VAR_0)) != VAR_1
| singleton(sK4(VAR_0)) = sK1(VAR_0) )
& ! [VAR_0,VAR_1] :
( relation_dom(sK3(VAR_0)) = VAR_0
| singleton(sK2(VAR_0)) != VAR_1
| singleton(sK4(VAR_0)) = sK1(VAR_0) )
& ! [VAR_0,VAR_1] :
( function(sK3(VAR_0))
| singleton(sK2(VAR_0)) != VAR_1
| singleton(sK4(VAR_0)) = sK1(VAR_0) )
& ! [VAR_0,VAR_1] :
( relation(sK3(VAR_0))
| singleton(sK2(VAR_0)) != VAR_1
| singleton(sK4(VAR_0)) = sK1(VAR_0) )
& ! [VAR_0,VAR_1] :
( singleton(VAR_1) = apply(sK3(VAR_0),VAR_1)
| ~ in(VAR_1,VAR_0)
| in(sK2(VAR_0),VAR_0)
| singleton(sK4(VAR_0)) = sK1(VAR_0) )
& ! [VAR_0] :
( relation_dom(sK3(VAR_0)) = VAR_0
| in(sK2(VAR_0),VAR_0)
| singleton(sK4(VAR_0)) = sK1(VAR_0) )
& ! [VAR_0] :
( function(sK3(VAR_0))
| in(sK2(VAR_0),VAR_0)
| singleton(sK4(VAR_0)) = sK1(VAR_0) )
& ! [VAR_0] :
( relation(sK3(VAR_0))
| in(sK2(VAR_0),VAR_0)
| singleton(sK4(VAR_0)) = sK1(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(VAR_2) = apply(sK3(VAR_0),VAR_2)
| ~ in(VAR_2,VAR_0)
| singleton(sK2(VAR_0)) != VAR_1
| in(sK4(VAR_0),VAR_0) )
& ! [VAR_0,VAR_1] :
( relation_dom(sK3(VAR_0)) = VAR_0
| singleton(sK2(VAR_0)) != VAR_1
| in(sK4(VAR_0),VAR_0) )
& ! [VAR_0,VAR_1] :
( function(sK3(VAR_0))
| singleton(sK2(VAR_0)) != VAR_1
| in(sK4(VAR_0),VAR_0) )
& ! [VAR_0,VAR_1] :
( relation(sK3(VAR_0))
| singleton(sK2(VAR_0)) != VAR_1
| in(sK4(VAR_0),VAR_0) )
& ! [VAR_0,VAR_1] :
( singleton(VAR_1) = apply(sK3(VAR_0),VAR_1)
| ~ in(VAR_1,VAR_0)
| in(sK2(VAR_0),VAR_0)
| in(sK4(VAR_0),VAR_0) )
& ! [VAR_0] :
( relation_dom(sK3(VAR_0)) = VAR_0
| in(sK2(VAR_0),VAR_0)
| in(sK4(VAR_0),VAR_0) )
& ! [VAR_0] :
( function(sK3(VAR_0))
| in(sK2(VAR_0),VAR_0)
| in(sK4(VAR_0),VAR_0) )
& ! [VAR_0] :
( relation(sK3(VAR_0))
| in(sK2(VAR_0),VAR_0)
| in(sK4(VAR_0),VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1_sk]) ).
cnf(c_31,plain,
( relation(sK3(A))
| singleton(sK2(A)) != B
| sK0(A) != sK1(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_33,plain,
( relation(sK3(A))
| singleton(sK2(A)) != B
| singleton(sK4(A)) = sK0(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_35,plain,
( relation(sK3(A))
| singleton(sK2(A)) != B
| singleton(sK4(A)) = sK1(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
fof(nnf_26,plain,
? [A] :
! [B] :
( ? [C] :
( singleton(C) != apply(B,C)
& in(C,A) )
| relation_dom(B) != A
| ~ function(B)
| ~ relation(B) ),
inference(fof_nnf,[status(thm)],[s3_funct_1__e16_22__wellord2_neg]) ).
fof(sk_s3_funct_1__e16_22__wellord2_neg_sk,plain,
! [B] :
( ( singleton(sK6(B)) != apply(B,sK6(B))
& in(sK6(B),sK5) )
| relation_dom(B) != sK5
| ~ function(B)
| ~ relation(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6]),skolemize(A,sK5),skolemize(C,sK6(B))],[nnf_26]) ).
fof(sk_s3_funct_1__e16_22__wellord2_neg,plain,
( ! [VAR_0] :
( singleton(sK6(VAR_0)) != apply(VAR_0,sK6(VAR_0))
| relation_dom(VAR_0) != sK5
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0] :
( in(sK6(VAR_0),sK5)
| relation_dom(VAR_0) != sK5
| ~ function(VAR_0)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_s3_funct_1__e16_22__wellord2_neg_sk]) ).
cnf(c_44,negated_conjecture,
( in(sK6(A),sK5)
| relation_dom(A) != sK5
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_s3_funct_1__e16_22__wellord2_neg]) ).
cnf(c_45,negated_conjecture,
( singleton(sK6(A)) != apply(A,sK6(A))
| relation_dom(A) != sK5
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_s3_funct_1__e16_22__wellord2_neg]) ).
cnf(c_57,negated_conjecture,
( singleton(sK2(A)) != B
| singleton(sK4(A)) = sK1(A)
| singleton(sK6(sK3(A))) != apply(sK3(A),sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(resolve,[status(thm)],[c_45,c_35]) ).
cnf(c_318,negated_conjecture,
( singleton(sK2(A)) != B
| singleton(sK4(A)) = sK1(A)
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_57]) ).
cnf(c_319,negated_conjecture,
( singleton(sK2(A)) != B
| sK1(A) = singleton(sK4(A))
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_318]) ).
cnf(c_58,negated_conjecture,
( sK1(A) = singleton(sK4(A))
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_319]) ).
cnf(c_61,negated_conjecture,
( singleton(sK2(A)) != B
| singleton(sK4(A)) = sK0(A)
| singleton(sK6(sK3(A))) != apply(sK3(A),sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(resolve,[status(thm)],[c_45,c_33]) ).
cnf(c_320,negated_conjecture,
( singleton(sK2(A)) != B
| singleton(sK4(A)) = sK0(A)
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_61]) ).
cnf(c_321,negated_conjecture,
( singleton(sK2(A)) != B
| sK0(A) = singleton(sK4(A))
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_320]) ).
cnf(c_62,negated_conjecture,
( sK0(A) = singleton(sK4(A))
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_321]) ).
cnf(c_65,negated_conjecture,
( singleton(sK2(A)) != B
| sK0(A) != sK1(A)
| singleton(sK6(sK3(A))) != apply(sK3(A),sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(resolve,[status(thm)],[c_45,c_31]) ).
cnf(c_322,negated_conjecture,
( singleton(sK2(A)) != B
| sK0(A) != sK1(A)
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_65]) ).
cnf(c_66,negated_conjecture,
( sK0(A) != sK1(A)
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_322]) ).
cnf(c_85,negated_conjecture,
( singleton(sK2(A)) != B
| singleton(sK4(A)) = sK1(A)
| in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(resolve,[status(thm)],[c_44,c_35]) ).
cnf(c_323,negated_conjecture,
( singleton(sK2(A)) != B
| sK1(A) = singleton(sK4(A))
| in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_85]) ).
cnf(c_86,negated_conjecture,
( sK1(A) = singleton(sK4(A))
| in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_323]) ).
cnf(c_89,negated_conjecture,
( singleton(sK2(A)) != B
| singleton(sK4(A)) = sK0(A)
| in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(resolve,[status(thm)],[c_44,c_33]) ).
cnf(c_324,negated_conjecture,
( singleton(sK2(A)) != B
| sK0(A) = singleton(sK4(A))
| in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_89]) ).
cnf(c_90,negated_conjecture,
( sK0(A) = singleton(sK4(A))
| in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_324]) ).
cnf(c_92,negated_conjecture,
( singleton(sK2(A)) != B
| sK0(A) != sK1(A)
| in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(resolve,[status(thm)],[c_44,c_31]) ).
cnf(c_93,negated_conjecture,
( sK0(A) != sK1(A)
| in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_92]) ).
cnf(c_130,plain,
( singleton(C) = apply(sK3(A),C)
| ~ in(C,A)
| singleton(sK2(A)) != B
| sK0(A) != sK1(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_325,plain,
( apply(sK3(A),C) = singleton(C)
| ~ in(C,A)
| singleton(sK2(A)) != B
| sK0(A) != sK1(A) ),
inference(copy,[status(thm)],[c_130]) ).
cnf(c_131,plain,
( apply(sK3(A),B) = singleton(B)
| ~ in(B,A)
| sK0(A) != sK1(A) ),
inference(copy,[status(thm)],[c_325]) ).
cnf(c_132,plain,
( relation_dom(sK3(A)) = A
| singleton(sK2(A)) != B
| sK0(A) != sK1(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_133,plain,
( relation_dom(sK3(A)) = A
| sK0(A) != sK1(A) ),
inference(copy,[status(thm)],[c_132]) ).
cnf(c_134,plain,
( function(sK3(A))
| singleton(sK2(A)) != B
| sK0(A) != sK1(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_135,plain,
( function(sK3(A))
| sK0(A) != sK1(A) ),
inference(copy,[status(thm)],[c_134]) ).
cnf(c_137,plain,
( singleton(C) = apply(sK3(A),C)
| ~ in(C,A)
| singleton(sK2(A)) != B
| singleton(sK4(A)) = sK0(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_326,plain,
( singleton(C) = apply(sK3(A),C)
| ~ in(C,A)
| singleton(sK2(A)) != B
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_137]) ).
cnf(c_327,plain,
( apply(sK3(A),C) = singleton(C)
| ~ in(C,A)
| singleton(sK2(A)) != B
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_326]) ).
cnf(c_138,plain,
( apply(sK3(A),B) = singleton(B)
| ~ in(B,A)
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_327]) ).
cnf(c_139,plain,
( relation_dom(sK3(A)) = A
| singleton(sK2(A)) != B
| singleton(sK4(A)) = sK0(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_328,plain,
( relation_dom(sK3(A)) = A
| singleton(sK2(A)) != B
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_139]) ).
cnf(c_140,plain,
( relation_dom(sK3(A)) = A
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_328]) ).
cnf(c_141,plain,
( function(sK3(A))
| singleton(sK2(A)) != B
| singleton(sK4(A)) = sK0(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_329,plain,
( function(sK3(A))
| singleton(sK2(A)) != B
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_141]) ).
cnf(c_142,plain,
( function(sK3(A))
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_329]) ).
cnf(c_146,plain,
( singleton(C) = apply(sK3(A),C)
| ~ in(C,A)
| singleton(sK2(A)) != B
| singleton(sK4(A)) = sK1(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_330,plain,
( singleton(C) = apply(sK3(A),C)
| ~ in(C,A)
| singleton(sK2(A)) != B
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_146]) ).
cnf(c_331,plain,
( apply(sK3(A),C) = singleton(C)
| ~ in(C,A)
| singleton(sK2(A)) != B
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_330]) ).
cnf(c_147,plain,
( apply(sK3(A),B) = singleton(B)
| ~ in(B,A)
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_331]) ).
cnf(c_148,plain,
( relation_dom(sK3(A)) = A
| singleton(sK2(A)) != B
| singleton(sK4(A)) = sK1(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_332,plain,
( relation_dom(sK3(A)) = A
| singleton(sK2(A)) != B
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_148]) ).
cnf(c_149,plain,
( relation_dom(sK3(A)) = A
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_332]) ).
cnf(c_150,plain,
( function(sK3(A))
| singleton(sK2(A)) != B
| singleton(sK4(A)) = sK1(A) ),
inference(split_conjunct,[status(thm)],[sk_s2_funct_1__e16_22__wellord2__1]) ).
cnf(c_333,plain,
( function(sK3(A))
| singleton(sK2(A)) != B
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_150]) ).
cnf(c_151,plain,
( function(sK3(A))
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_333]) ).
cnf(c_334,plain,
( relation_dom(sK3(A)) = A
| singleton(sK4(A)) != sK1(A)
| relation_dom(sK3(A)) = A ),
inference(paramod,[status(thm)],[c_140,c_133]) ).
cnf(c_335,plain,
( relation_dom(sK3(A)) = A
| sK1(A) != singleton(sK4(A))
| relation_dom(sK3(A)) = A ),
inference(copy,[status(thm)],[c_334]) ).
cnf(c_176,plain,
( sK1(A) != singleton(sK4(A))
| relation_dom(sK3(A)) = A ),
inference(copy,[status(thm)],[c_335]) ).
cnf(c_336,negated_conjecture,
( sK0(A) = singleton(sK4(A))
| in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| sK0(A) = singleton(sK4(A)) ),
inference(resolve,[status(thm)],[c_142,c_90]) ).
cnf(c_179,negated_conjecture,
( in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_336]) ).
cnf(c_337,negated_conjecture,
( sK0(A) = singleton(sK4(A))
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| sK0(A) = singleton(sK4(A)) ),
inference(resolve,[status(thm)],[c_142,c_62]) ).
cnf(c_182,negated_conjecture,
( apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_337]) ).
cnf(c_338,negated_conjecture,
( sK1(A) = singleton(sK4(A))
| in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| sK1(A) = singleton(sK4(A)) ),
inference(resolve,[status(thm)],[c_151,c_86]) ).
cnf(c_186,negated_conjecture,
( in(sK6(sK3(A)),sK5)
| relation_dom(sK3(A)) != sK5
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_338]) ).
cnf(c_339,negated_conjecture,
( sK1(A) = singleton(sK4(A))
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| sK1(A) = singleton(sK4(A)) ),
inference(resolve,[status(thm)],[c_151,c_58]) ).
cnf(c_189,negated_conjecture,
( apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| relation_dom(sK3(A)) != sK5
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_339]) ).
cnf(c_340,plain,
( relation_dom(sK3(A)) = A
| relation_dom(sK3(A)) = A ),
inference(resolve,[status(thm)],[c_176,c_149]) ).
cnf(c_212,plain,
relation_dom(sK3(A)) = A,
inference(copy,[status(thm)],[c_340]) ).
cnf(c_341,negated_conjecture,
( apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| A != sK5
| sK1(A) = singleton(sK4(A)) ),
inference(paramod,[status(thm)],[c_212,c_189]) ).
cnf(c_213,negated_conjecture,
( apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| sK5 != A
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_341]) ).
cnf(c_342,negated_conjecture,
( in(sK6(sK3(A)),sK5)
| A != sK5
| sK1(A) = singleton(sK4(A)) ),
inference(paramod,[status(thm)],[c_212,c_186]) ).
cnf(c_214,negated_conjecture,
( in(sK6(sK3(A)),sK5)
| sK5 != A
| sK1(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_342]) ).
cnf(c_343,negated_conjecture,
( apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| A != sK5
| sK0(A) = singleton(sK4(A)) ),
inference(paramod,[status(thm)],[c_212,c_182]) ).
cnf(c_215,negated_conjecture,
( apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| sK5 != A
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_343]) ).
cnf(c_344,negated_conjecture,
( in(sK6(sK3(A)),sK5)
| A != sK5
| sK0(A) = singleton(sK4(A)) ),
inference(paramod,[status(thm)],[c_212,c_179]) ).
cnf(c_216,negated_conjecture,
( in(sK6(sK3(A)),sK5)
| sK5 != A
| sK0(A) = singleton(sK4(A)) ),
inference(copy,[status(thm)],[c_344]) ).
cnf(c_345,negated_conjecture,
( sK0(A) != sK1(A)
| in(sK6(sK3(A)),sK5)
| A != sK5
| ~ function(sK3(A)) ),
inference(paramod,[status(thm)],[c_212,c_93]) ).
cnf(c_221,negated_conjecture,
( sK0(A) != sK1(A)
| in(sK6(sK3(A)),sK5)
| sK5 != A
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_345]) ).
cnf(c_346,negated_conjecture,
( sK0(A) != sK1(A)
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| A != sK5
| ~ function(sK3(A)) ),
inference(paramod,[status(thm)],[c_212,c_66]) ).
cnf(c_223,negated_conjecture,
( sK0(A) != sK1(A)
| apply(sK3(A),sK6(sK3(A))) != singleton(sK6(sK3(A)))
| sK5 != A
| ~ function(sK3(A)) ),
inference(copy,[status(thm)],[c_346]) ).
cnf(c_347,plain,
A = relation_dom(sK3(A)),
inference(copy,[status(thm)],[c_212]) ).
cnf(c_348,plain,
( in(sK6(sK3(relation_dom(sK3(sK5)))),sK5)
| sK1(relation_dom(sK3(sK5))) = singleton(sK4(relation_dom(sK3(sK5)))) ),
inference(resolve,[status(thm)],[c_214,c_347]) ).
cnf(c_349,plain,
( in(sK6(sK3(relation_dom(sK3(sK5)))),sK5)
| sK1(sK5) = singleton(sK4(relation_dom(sK3(sK5)))) ),
inference(paramod,[status(thm)],[c_212,c_348]) ).
cnf(c_350,plain,
( in(sK6(sK3(relation_dom(sK3(sK5)))),sK5)
| sK1(sK5) = singleton(sK4(sK5)) ),
inference(paramod,[status(thm)],[c_212,c_349]) ).
cnf(c_247,plain,
( in(sK6(sK3(sK5)),sK5)
| sK1(sK5) = singleton(sK4(sK5)) ),
inference(paramod,[status(thm)],[c_212,c_350]) ).
cnf(c_351,plain,
( apply(sK3(sK5),sK6(sK3(sK5))) = singleton(sK6(sK3(sK5)))
| sK1(sK5) = singleton(sK4(sK5))
| sK1(sK5) = singleton(sK4(sK5)) ),
inference(resolve,[status(thm)],[c_247,c_147]) ).
cnf(c_250,plain,
( apply(sK3(sK5),sK6(sK3(sK5))) = singleton(sK6(sK3(sK5)))
| sK1(sK5) = singleton(sK4(sK5)) ),
inference(copy,[status(thm)],[c_351]) ).
cnf(c_352,plain,
A = relation_dom(sK3(A)),
inference(copy,[status(thm)],[c_212]) ).
cnf(c_353,plain,
( in(sK6(sK3(relation_dom(sK3(sK5)))),sK5)
| sK0(relation_dom(sK3(sK5))) = singleton(sK4(relation_dom(sK3(sK5)))) ),
inference(resolve,[status(thm)],[c_216,c_352]) ).
cnf(c_354,plain,
( in(sK6(sK3(relation_dom(sK3(sK5)))),sK5)
| sK0(sK5) = singleton(sK4(relation_dom(sK3(sK5)))) ),
inference(paramod,[status(thm)],[c_212,c_353]) ).
cnf(c_355,plain,
( in(sK6(sK3(relation_dom(sK3(sK5)))),sK5)
| sK0(sK5) = singleton(sK4(sK5)) ),
inference(paramod,[status(thm)],[c_212,c_354]) ).
cnf(c_265,plain,
( in(sK6(sK3(sK5)),sK5)
| sK0(sK5) = singleton(sK4(sK5)) ),
inference(paramod,[status(thm)],[c_212,c_355]) ).
cnf(c_356,plain,
( apply(sK3(sK5),sK6(sK3(sK5))) = singleton(sK6(sK3(sK5)))
| sK0(sK5) = singleton(sK4(sK5))
| sK0(sK5) = singleton(sK4(sK5)) ),
inference(resolve,[status(thm)],[c_265,c_138]) ).
cnf(c_268,plain,
( apply(sK3(sK5),sK6(sK3(sK5))) = singleton(sK6(sK3(sK5)))
| sK0(sK5) = singleton(sK4(sK5)) ),
inference(copy,[status(thm)],[c_356]) ).
cnf(c_357,plain,
( sK5 != sK5
| sK1(sK5) = singleton(sK4(sK5))
| sK1(sK5) = singleton(sK4(sK5)) ),
inference(resolve,[status(thm)],[c_250,c_213]) ).
cnf(c_358,plain,
( sK1(sK5) = singleton(sK4(sK5))
| sK1(sK5) = singleton(sK4(sK5)) ),
inference(copy,[status(thm)],[c_357]) ).
cnf(c_283,plain,
sK1(sK5) = singleton(sK4(sK5)),
inference(copy,[status(thm)],[c_358]) ).
cnf(c_285,plain,
( function(sK3(sK5))
| sK0(sK5) != singleton(sK4(sK5)) ),
inference(paramod,[status(thm)],[c_283,c_135]) ).
cnf(c_359,plain,
( sK5 != sK5
| sK0(sK5) = singleton(sK4(sK5))
| sK0(sK5) = singleton(sK4(sK5)) ),
inference(resolve,[status(thm)],[c_268,c_215]) ).
cnf(c_360,plain,
( sK0(sK5) = singleton(sK4(sK5))
| sK0(sK5) = singleton(sK4(sK5)) ),
inference(copy,[status(thm)],[c_359]) ).
cnf(c_299,plain,
sK0(sK5) = singleton(sK4(sK5)),
inference(copy,[status(thm)],[c_360]) ).
cnf(c_361,plain,
( function(sK3(sK5))
| singleton(sK4(sK5)) != singleton(sK4(sK5)) ),
inference(paramod,[status(thm)],[c_299,c_285]) ).
cnf(c_301,plain,
function(sK3(sK5)),
inference(copy,[status(thm)],[c_361]) ).
cnf(c_362,negated_conjecture,
( sK0(sK5) != sK1(sK5)
| apply(sK3(sK5),sK6(sK3(sK5))) != singleton(sK6(sK3(sK5)))
| sK5 != sK5 ),
inference(resolve,[status(thm)],[c_301,c_223]) ).
cnf(c_363,negated_conjecture,
( singleton(sK4(sK5)) != sK1(sK5)
| apply(sK3(sK5),sK6(sK3(sK5))) != singleton(sK6(sK3(sK5)))
| sK5 != sK5 ),
inference(paramod,[status(thm)],[c_299,c_362]) ).
cnf(c_364,negated_conjecture,
( singleton(sK4(sK5)) != singleton(sK4(sK5))
| apply(sK3(sK5),sK6(sK3(sK5))) != singleton(sK6(sK3(sK5)))
| sK5 != sK5 ),
inference(paramod,[status(thm)],[c_283,c_363]) ).
cnf(c_365,negated_conjecture,
( singleton(sK4(sK5)) != singleton(sK4(sK5))
| apply(sK3(sK5),sK6(sK3(sK5))) != singleton(sK6(sK3(sK5))) ),
inference(copy,[status(thm)],[c_364]) ).
cnf(c_312,negated_conjecture,
apply(sK3(sK5),sK6(sK3(sK5))) != singleton(sK6(sK3(sK5))),
inference(copy,[status(thm)],[c_365]) ).
cnf(c_366,negated_conjecture,
( sK0(sK5) != sK1(sK5)
| in(sK6(sK3(sK5)),sK5)
| sK5 != sK5 ),
inference(resolve,[status(thm)],[c_301,c_221]) ).
cnf(c_367,negated_conjecture,
( singleton(sK4(sK5)) != sK1(sK5)
| in(sK6(sK3(sK5)),sK5)
| sK5 != sK5 ),
inference(paramod,[status(thm)],[c_299,c_366]) ).
cnf(c_368,negated_conjecture,
( singleton(sK4(sK5)) != singleton(sK4(sK5))
| in(sK6(sK3(sK5)),sK5)
| sK5 != sK5 ),
inference(paramod,[status(thm)],[c_283,c_367]) ).
cnf(c_369,negated_conjecture,
( singleton(sK4(sK5)) != singleton(sK4(sK5))
| in(sK6(sK3(sK5)),sK5) ),
inference(copy,[status(thm)],[c_368]) ).
cnf(c_314,negated_conjecture,
in(sK6(sK3(sK5)),sK5),
inference(copy,[status(thm)],[c_369]) ).
cnf(c_370,plain,
( apply(sK3(sK5),sK6(sK3(sK5))) = singleton(sK6(sK3(sK5)))
| sK0(sK5) != sK1(sK5) ),
inference(resolve,[status(thm)],[c_314,c_131]) ).
cnf(c_371,plain,
( apply(sK3(sK5),sK6(sK3(sK5))) = singleton(sK6(sK3(sK5)))
| singleton(sK4(sK5)) != sK1(sK5) ),
inference(paramod,[status(thm)],[c_299,c_370]) ).
cnf(c_372,plain,
( apply(sK3(sK5),sK6(sK3(sK5))) = singleton(sK6(sK3(sK5)))
| singleton(sK4(sK5)) != singleton(sK4(sK5)) ),
inference(paramod,[status(thm)],[c_283,c_371]) ).
cnf(c_373,plain,
apply(sK3(sK5),sK6(sK3(sK5))) = singleton(sK6(sK3(sK5))),
inference(copy,[status(thm)],[c_372]) ).
cnf(c_317,plain,
$false,
inference(resolve,[status(thm)],[c_312,c_373]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU284+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40 % Computer : n005.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sat Sep 26 09:04:47 UTC 2026
% 0.05/0.41 % CPUTime :
% 0.05/0.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.05/0.41 % Process 1786436 was started by sandbox2 on n005,
% 0.05/0.41 % Sat Sep 26 09:04:47 2026
% 0.05/0.41 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.05/0.42
% 0.05/0.42 % From the command line: assign(max_seconds, 300).
% 0.05/0.48
% 0.05/0.48 % SZS status Theorem for theBenchmark
% 0.05/0.48
% 0.05/0.48 % Proof 1 at 0.04 (+ 0.01) seconds.
% 0.05/0.48 % Length of proof is 60.
% 0.05/0.48 % Level of proof is 12.
% 0.05/0.48 % Maximum clause weight is 25.000.
% 0.05/0.48 % Given clauses 117.
% 0.05/0.48
% 0.05/0.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------