%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU019+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:44:54 AM UTC 2026
% Result : Theorem 0.15s 10.75s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 4
% Syntax : Number of formulae : 44 ( 15 unt; 0 def)
% Number of atoms : 144 ( 45 equ)
% Maximal formula atoms : 23 ( 3 avg)
% Number of connectives : 165 ( 65 ~; 76 |; 18 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% Number of variables : 61 ( 2 sgn 22 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d8_funct_1,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
<=> ! [B,C] :
( ( apply(A,B) = apply(A,C)
& in(C,relation_dom(A))
& in(B,relation_dom(A)) )
=> B = C ) ) ),
file('theBenchmark.p',d8_funct_1) ).
fof(fc2_funct_1,axiom,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
file('theBenchmark.p',fc2_funct_1) ).
fof(t34_funct_1,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( B = identity_relation(A)
<=> ( ! [C] :
( in(C,A)
=> apply(B,C) = C )
& relation_dom(B) = A ) ) ),
file('theBenchmark.p',t34_funct_1) ).
fof(t52_funct_1,conjecture,
! [A] : one_to_one(identity_relation(A)),
file('theBenchmark.p',t52_funct_1) ).
fof(t52_funct_1_neg,negated_conjecture,
~ ! [A] : one_to_one(identity_relation(A)),
inference(assume_negation,[status(cth)],[t52_funct_1]) ).
fof(nnf_4,plain,
! [A] :
( ( ( ? [B,C] :
( C != B
& apply(A,C) = apply(A,B)
& in(C,relation_dom(A))
& in(B,relation_dom(A)) )
| one_to_one(A) )
& ( ! [X0,X1] :
( X1 = X0
| apply(A,X1) != apply(A,X0)
| ~ in(X1,relation_dom(A))
| ~ in(X0,relation_dom(A)) )
| ~ one_to_one(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d8_funct_1]) ).
fof(sk_d8_funct_1_sk,plain,
! [A] :
( ( ( ( sK1(A) != sK0(A)
& apply(A,sK1(A)) = apply(A,sK0(A))
& in(sK1(A),relation_dom(A))
& in(sK0(A),relation_dom(A)) )
| one_to_one(A) )
& ( ! [X0,X1] :
( X1 = X0
| apply(A,X1) != apply(A,X0)
| ~ in(X1,relation_dom(A))
| ~ in(X0,relation_dom(A)) )
| ~ one_to_one(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(B,sK0(A)),skolemize(C,sK1(A))],[nnf_4]) ).
fof(sk_d8_funct_1,plain,
( ! [VAR_0] :
( sK1(VAR_0) != sK0(VAR_0)
| one_to_one(VAR_0)
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0] :
( apply(VAR_0,sK1(VAR_0)) = apply(VAR_0,sK0(VAR_0))
| one_to_one(VAR_0)
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0] :
( in(sK1(VAR_0),relation_dom(VAR_0))
| one_to_one(VAR_0)
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0] :
( in(sK0(VAR_0),relation_dom(VAR_0))
| one_to_one(VAR_0)
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( VAR_2 = VAR_1
| apply(VAR_0,VAR_2) != apply(VAR_0,VAR_1)
| ~ in(VAR_2,relation_dom(VAR_0))
| ~ in(VAR_1,relation_dom(VAR_0))
| ~ one_to_one(VAR_0)
| ~ function(VAR_0)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d8_funct_1_sk]) ).
cnf(c_34,plain,
( in(sK0(A),relation_dom(A))
| one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_funct_1]) ).
cnf(c_35,plain,
( in(sK1(A),relation_dom(A))
| one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_funct_1]) ).
cnf(c_36,plain,
( apply(A,sK1(A)) = apply(A,sK0(A))
| one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_funct_1]) ).
cnf(c_37,plain,
( sK1(A) != sK0(A)
| one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_funct_1]) ).
cnf(c_38,plain,
function(identity_relation(A)),
inference(clausify,[status(thm)],[fc2_funct_1]) ).
cnf(c_40,plain,
( relation_dom(A) = B
| identity_relation(B) != A
| ~ function(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[t34_funct_1]) ).
cnf(c_41,plain,
( apply(A,C) = C
| ~ in(C,B)
| identity_relation(B) != A
| ~ function(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[t34_funct_1]) ).
cnf(c_55,plain,
( apply(identity_relation(A),C) = C
| ~ in(C,B)
| identity_relation(B) != identity_relation(A)
| ~ relation(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_41,c_38]) ).
cnf(c_58,plain,
( relation_dom(identity_relation(A)) = B
| identity_relation(B) != identity_relation(A)
| ~ relation(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_40,c_38]) ).
cnf(c_66,plain,
( in(sK0(identity_relation(A)),relation_dom(identity_relation(A)))
| one_to_one(identity_relation(A))
| ~ relation(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_38,c_34]) ).
cnf(c_67,plain,
( in(sK1(identity_relation(A)),relation_dom(identity_relation(A)))
| one_to_one(identity_relation(A))
| ~ relation(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_38,c_35]) ).
cnf(c_68,plain,
( apply(identity_relation(A),sK1(identity_relation(A))) = apply(identity_relation(A),sK0(identity_relation(A)))
| one_to_one(identity_relation(A))
| ~ relation(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_38,c_36]) ).
cnf(c_69,plain,
( sK1(identity_relation(A)) != sK0(identity_relation(A))
| one_to_one(identity_relation(A))
| ~ relation(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_38,c_37]) ).
fof(nnf_31,plain,
? [A] : ~ one_to_one(identity_relation(A)),
inference(fof_nnf,[status(thm)],[t52_funct_1_neg]) ).
fof(sk_t52_funct_1_neg,plain,
~ one_to_one(identity_relation(sK2)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(A,sK2)],[nnf_31]) ).
cnf(c_75,negated_conjecture,
~ one_to_one(identity_relation(sK2)),
inference(split_conjunct,[status(thm)],[sk_t52_funct_1_neg]) ).
cnf(c_100,plain,
relation(identity_relation(A)),
inference(clausify,[status(thm)],[fc2_funct_1]) ).
cnf(c_114,plain,
( sK1(identity_relation(A)) != sK0(identity_relation(A))
| one_to_one(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_100,c_69]) ).
cnf(c_115,plain,
( apply(identity_relation(A),sK1(identity_relation(A))) = apply(identity_relation(A),sK0(identity_relation(A)))
| one_to_one(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_100,c_68]) ).
cnf(c_116,plain,
( in(sK1(identity_relation(A)),relation_dom(identity_relation(A)))
| one_to_one(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_100,c_67]) ).
cnf(c_117,plain,
( in(sK0(identity_relation(A)),relation_dom(identity_relation(A)))
| one_to_one(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_100,c_66]) ).
cnf(c_119,plain,
( relation_dom(identity_relation(B)) = A
| identity_relation(A) != identity_relation(B) ),
inference(resolve,[status(thm)],[c_100,c_58]) ).
cnf(c_120,plain,
( apply(identity_relation(B),C) = C
| ~ in(C,A)
| identity_relation(A) != identity_relation(B) ),
inference(resolve,[status(thm)],[c_100,c_55]) ).
cnf(c_198,negated_conjecture,
sK1(identity_relation(sK2)) != sK0(identity_relation(sK2)),
inference(resolve,[status(thm)],[c_114,c_75]) ).
cnf(c_199,plain,
apply(identity_relation(sK2),sK1(identity_relation(sK2))) = apply(identity_relation(sK2),sK0(identity_relation(sK2))),
inference(resolve,[status(thm)],[c_115,c_75]) ).
cnf(c_216,plain,
relation_dom(identity_relation(A)) = A,
inference(xxres,[status(thm)],[c_119]) ).
cnf(c_236,plain,
( in(sK0(identity_relation(A)),A)
| one_to_one(identity_relation(A)) ),
inference(paramod,[status(thm)],[c_216,c_117]) ).
cnf(c_237,plain,
( in(sK1(identity_relation(A)),A)
| one_to_one(identity_relation(A)) ),
inference(paramod,[status(thm)],[c_216,c_116]) ).
cnf(c_238,plain,
( apply(identity_relation(B),A) = A
| ~ in(A,B) ),
inference(xxres,[status(thm)],[c_120]) ).
cnf(c_510,plain,
( one_to_one(identity_relation(A))
| apply(identity_relation(A),sK1(identity_relation(A))) = sK1(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_238,c_237]) ).
cnf(c_511,plain,
( one_to_one(identity_relation(A))
| apply(identity_relation(A),sK0(identity_relation(A))) = sK0(identity_relation(A)) ),
inference(resolve,[status(thm)],[c_238,c_236]) ).
cnf(c_2118,negated_conjecture,
apply(identity_relation(sK2),sK1(identity_relation(sK2))) = sK1(identity_relation(sK2)),
inference(resolve,[status(thm)],[c_510,c_75]) ).
cnf(c_2102,negated_conjecture,
apply(identity_relation(sK2),sK0(identity_relation(sK2))) = sK1(identity_relation(sK2)),
inference(paramod,[status(thm)],[c_199,c_2118]) ).
cnf(c_2119,negated_conjecture,
apply(identity_relation(sK2),sK0(identity_relation(sK2))) = sK0(identity_relation(sK2)),
inference(resolve,[status(thm)],[c_511,c_75]) ).
cnf(c_2120,negated_conjecture,
sK1(identity_relation(sK2)) = sK0(identity_relation(sK2)),
inference(paramod,[status(thm)],[c_2102,c_2119]) ).
cnf(c_2117,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_198,c_2120]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU019+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/10.38 % Computer : n019.cluster.edu
% 0.11/10.38 % Model : x86_64 x86_64
% 0.11/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.38 % Memory : 8046.5625MB
% 0.11/10.38 % OS : Linux 6.8.0-71-generic
% 0.11/10.38 % CPULimit : 300
% 0.11/10.38 % WCLimit : 300
% 0.11/10.38 % DateTime : Sat Sep 26 08:31:16 UTC 2026
% 0.11/10.38 % CPUTime :
% 0.11/10.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/10.39 % Process 857223 was started by sandbox2 on n019,
% 0.11/10.39 % Sat Sep 26 08:31:16 2026
% 0.11/10.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/10.40
% 0.15/10.40 % From the command line: assign(max_seconds, 300).
% 0.15/10.75
% 0.15/10.75 % given #500 (F,wt=29): 635 -in(f4(c4),f4(f4(powerset(empty_set)))). [ur(157,a,175,a,c,522,a)].
% 0.15/10.75
% 0.15/10.75 % SZS status Theorem for theBenchmark
% 0.15/10.75
% 0.15/10.75 % Proof 1 at 0.26 (+ 0.07) seconds.
% 0.15/10.75 % Length of proof is 35.
% 0.15/10.75 % Level of proof is 8.
% 0.15/10.75 % Maximum clause weight is 39.000.
% 0.15/10.75 % Given clauses 667.
% 0.15/10.75
% 0.15/10.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------