%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SET995+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 : n002.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:37:25 AM UTC 2026
% Result : Theorem 2.37s 0.73s
% Output : CNFRefutation 2.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 4
% Syntax : Number of formulae : 63 ( 22 unt; 0 def)
% Number of atoms : 237 ( 86 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 300 ( 126 ~; 129 |; 30 &)
% ( 4 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 56 ( 0 sgn 23 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d1_tarski,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('theBenchmark.p',d1_tarski) ).
fof(d5_funct_1,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) ) ) ) ),
file('theBenchmark.p',d5_funct_1) ).
fof(t9_funct_1,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( ( ! [C] :
( in(C,relation_dom(A))
=> apply(A,C) = apply(B,C) )
& relation_dom(A) = relation_dom(B) )
=> A = B ) ) ),
file('theBenchmark.p',t9_funct_1) ).
fof(t17_funct_1,conjecture,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( ( relation_rng(C) = singleton(A)
& relation_rng(B) = singleton(A)
& relation_dom(B) = relation_dom(C) )
=> B = C ) ) ),
file('theBenchmark.p',t17_funct_1) ).
fof(t17_funct_1_neg,negated_conjecture,
~ ! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( ( relation_rng(C) = singleton(A)
& relation_rng(B) = singleton(A)
& relation_dom(B) = relation_dom(C) )
=> B = C ) ) ),
inference(assume_negation,[status(cth)],[t17_funct_1]) ).
cnf(c_41,plain,
( C = A
| ~ in(C,B)
| singleton(A) != B ),
inference(clausify,[status(thm)],[d1_tarski]) ).
cnf(c_47,plain,
( apply(A,D) != C
| ~ in(D,relation_dom(A))
| in(C,B)
| relation_rng(A) != B
| ~ function(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[d5_funct_1]) ).
fof(nnf_32,plain,
! [A] :
( ! [B] :
( B = A
| ? [C] :
( apply(B,C) != apply(A,C)
& in(C,relation_dom(A)) )
| relation_dom(B) != relation_dom(A)
| ~ function(B)
| ~ relation(B) )
| ~ function(A)
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[t9_funct_1]) ).
fof(sk_t9_funct_1_sk,plain,
! [A] :
( ! [B] :
( B = A
| ( apply(B,sK0(A,B)) != apply(A,sK0(A,B))
& in(sK0(A,B),relation_dom(A)) )
| relation_dom(B) != relation_dom(A)
| ~ function(B)
| ~ relation(B) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(C,sK0(A,B))],[nnf_32]) ).
fof(sk_t9_funct_1,plain,
( ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| apply(VAR_1,sK0(VAR_0,VAR_1)) != apply(VAR_0,sK0(VAR_0,VAR_1))
| relation_dom(VAR_1) != relation_dom(VAR_0)
| ~ function(VAR_1)
| ~ relation(VAR_1)
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| in(sK0(VAR_0,VAR_1),relation_dom(VAR_0))
| relation_dom(VAR_1) != relation_dom(VAR_0)
| ~ function(VAR_1)
| ~ relation(VAR_1)
| ~ function(VAR_0)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_t9_funct_1_sk]) ).
cnf(c_83,plain,
( B = A
| in(sK0(A,B),relation_dom(A))
| relation_dom(B) != relation_dom(A)
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_t9_funct_1]) ).
cnf(c_84,plain,
( B = A
| apply(B,sK0(A,B)) != apply(A,sK0(A,B))
| relation_dom(B) != relation_dom(A)
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_t9_funct_1]) ).
fof(nnf_33,plain,
? [A,B] :
( ? [C] :
( C != B
& relation_rng(C) = singleton(A)
& relation_rng(B) = singleton(A)
& relation_dom(C) = relation_dom(B)
& function(C)
& relation(C) )
& function(B)
& relation(B) ),
inference(fof_nnf,[status(thm)],[t17_funct_1_neg]) ).
fof(sk_t17_funct_1_neg,plain,
( sK2 != sK1
& relation_rng(sK2) = singleton(sK3)
& relation_rng(sK1) = singleton(sK3)
& relation_dom(sK2) = relation_dom(sK1)
& function(sK2)
& relation(sK2)
& function(sK1)
& relation(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(A,sK3),skolemize(B,sK1),skolemize(C,sK2)],[nnf_33]) ).
cnf(c_85,negated_conjecture,
relation(sK1),
inference(split_conjunct,[status(thm)],[sk_t17_funct_1_neg]) ).
cnf(c_86,negated_conjecture,
function(sK1),
inference(split_conjunct,[status(thm)],[sk_t17_funct_1_neg]) ).
cnf(c_87,negated_conjecture,
relation(sK2),
inference(split_conjunct,[status(thm)],[sk_t17_funct_1_neg]) ).
cnf(c_88,negated_conjecture,
function(sK2),
inference(split_conjunct,[status(thm)],[sk_t17_funct_1_neg]) ).
cnf(c_89,negated_conjecture,
relation_dom(sK2) = relation_dom(sK1),
inference(split_conjunct,[status(thm)],[sk_t17_funct_1_neg]) ).
cnf(c_90,negated_conjecture,
relation_rng(sK1) = singleton(sK3),
inference(split_conjunct,[status(thm)],[sk_t17_funct_1_neg]) ).
cnf(c_91,negated_conjecture,
singleton(sK3) = relation_rng(sK1),
inference(copy,[status(thm)],[c_90]) ).
cnf(c_92,negated_conjecture,
relation_rng(sK2) = singleton(sK3),
inference(split_conjunct,[status(thm)],[sk_t17_funct_1_neg]) ).
cnf(c_93,negated_conjecture,
relation_rng(sK2) = relation_rng(sK1),
inference(paramod,[status(thm)],[c_91,c_92]) ).
cnf(c_94,negated_conjecture,
sK2 != sK1,
inference(split_conjunct,[status(thm)],[sk_t17_funct_1_neg]) ).
cnf(c_109,plain,
( ~ in(C,relation_dom(A))
| in(apply(A,C),B)
| relation_rng(A) != B
| ~ function(A)
| ~ relation(A) ),
inference(xxres,[status(thm)],[c_47]) ).
cnf(c_1198,plain,
( B = A
| apply(B,sK0(A,B)) != apply(A,sK0(A,B))
| relation_dom(A) != relation_dom(B)
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(copy,[status(thm)],[c_84]) ).
cnf(c_1199,negated_conjecture,
( sK1 = sK2
| apply(sK1,sK0(sK2,sK1)) != apply(sK2,sK0(sK2,sK1))
| ~ function(sK1)
| ~ relation(sK1)
| ~ function(sK2)
| ~ relation(sK2) ),
inference(resolve,[status(thm)],[c_89,c_1198]) ).
cnf(c_1200,negated_conjecture,
( sK1 = sK2
| apply(sK2,sK0(sK2,sK1)) != apply(sK1,sK0(sK2,sK1))
| ~ function(sK1)
| ~ relation(sK1)
| ~ function(sK2)
| ~ relation(sK2) ),
inference(copy,[status(thm)],[c_1199]) ).
cnf(c_1201,negated_conjecture,
( sK2 = sK1
| apply(sK2,sK0(sK2,sK1)) != apply(sK1,sK0(sK2,sK1))
| ~ function(sK1)
| ~ relation(sK1)
| ~ function(sK2)
| ~ relation(sK2) ),
inference(copy,[status(thm)],[c_1200]) ).
cnf(c_1202,negated_conjecture,
( sK2 = sK1
| apply(sK2,sK0(sK2,sK1)) != apply(sK1,sK0(sK2,sK1))
| ~ function(sK1)
| ~ relation(sK1)
| ~ function(sK2) ),
inference(resolve,[status(thm)],[c_87,c_1201]) ).
cnf(c_1203,negated_conjecture,
( sK2 = sK1
| apply(sK2,sK0(sK2,sK1)) != apply(sK1,sK0(sK2,sK1))
| ~ function(sK1)
| ~ relation(sK1) ),
inference(resolve,[status(thm)],[c_88,c_1202]) ).
cnf(c_1204,negated_conjecture,
( sK2 = sK1
| apply(sK2,sK0(sK2,sK1)) != apply(sK1,sK0(sK2,sK1))
| ~ function(sK1) ),
inference(resolve,[status(thm)],[c_85,c_1203]) ).
cnf(c_1205,negated_conjecture,
( sK2 = sK1
| apply(sK2,sK0(sK2,sK1)) != apply(sK1,sK0(sK2,sK1)) ),
inference(resolve,[status(thm)],[c_86,c_1204]) ).
cnf(c_256,negated_conjecture,
apply(sK2,sK0(sK2,sK1)) != apply(sK1,sK0(sK2,sK1)),
inference(resolve,[status(thm)],[c_94,c_1205]) ).
cnf(c_1206,plain,
( B = A
| in(sK0(A,B),relation_dom(A))
| relation_dom(A) != relation_dom(B)
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(copy,[status(thm)],[c_83]) ).
cnf(c_1207,negated_conjecture,
( sK1 = sK2
| in(sK0(sK2,sK1),relation_dom(sK2))
| ~ function(sK1)
| ~ relation(sK1)
| ~ function(sK2)
| ~ relation(sK2) ),
inference(resolve,[status(thm)],[c_89,c_1206]) ).
cnf(c_1208,negated_conjecture,
( sK1 = sK2
| in(sK0(sK2,sK1),relation_dom(sK1))
| ~ function(sK1)
| ~ relation(sK1)
| ~ function(sK2)
| ~ relation(sK2) ),
inference(paramod,[status(thm)],[c_89,c_1207]) ).
cnf(c_1209,negated_conjecture,
( sK2 = sK1
| in(sK0(sK2,sK1),relation_dom(sK1))
| ~ function(sK1)
| ~ relation(sK1)
| ~ function(sK2)
| ~ relation(sK2) ),
inference(copy,[status(thm)],[c_1208]) ).
cnf(c_1210,negated_conjecture,
( sK2 = sK1
| in(sK0(sK2,sK1),relation_dom(sK1))
| ~ function(sK1)
| ~ relation(sK1)
| ~ function(sK2) ),
inference(resolve,[status(thm)],[c_87,c_1209]) ).
cnf(c_1211,negated_conjecture,
( sK2 = sK1
| in(sK0(sK2,sK1),relation_dom(sK1))
| ~ function(sK1)
| ~ relation(sK1) ),
inference(resolve,[status(thm)],[c_88,c_1210]) ).
cnf(c_1212,negated_conjecture,
( sK2 = sK1
| in(sK0(sK2,sK1),relation_dom(sK1))
| ~ function(sK1) ),
inference(resolve,[status(thm)],[c_85,c_1211]) ).
cnf(c_1213,negated_conjecture,
( sK2 = sK1
| in(sK0(sK2,sK1),relation_dom(sK1)) ),
inference(resolve,[status(thm)],[c_86,c_1212]) ).
cnf(c_257,negated_conjecture,
in(sK0(sK2,sK1),relation_dom(sK1)),
inference(resolve,[status(thm)],[c_94,c_1213]) ).
cnf(c_1214,negated_conjecture,
( A = sK3
| ~ in(A,relation_rng(sK1)) ),
inference(resolve,[status(thm)],[c_91,c_41]) ).
cnf(c_259,negated_conjecture,
( sK3 = A
| ~ in(A,relation_rng(sK1)) ),
inference(copy,[status(thm)],[c_1214]) ).
cnf(c_1215,negated_conjecture,
( ~ in(A,relation_dom(sK2))
| in(apply(sK2,A),relation_rng(sK1))
| ~ function(sK2)
| ~ relation(sK2) ),
inference(resolve,[status(thm)],[c_109,c_93]) ).
cnf(c_1216,negated_conjecture,
( ~ in(A,relation_dom(sK1))
| in(apply(sK2,A),relation_rng(sK1))
| ~ function(sK2)
| ~ relation(sK2) ),
inference(paramod,[status(thm)],[c_89,c_1215]) ).
cnf(c_1217,negated_conjecture,
( ~ in(A,relation_dom(sK1))
| in(apply(sK2,A),relation_rng(sK1))
| ~ function(sK2) ),
inference(resolve,[status(thm)],[c_87,c_1216]) ).
cnf(c_711,negated_conjecture,
( ~ in(A,relation_dom(sK1))
| in(apply(sK2,A),relation_rng(sK1)) ),
inference(resolve,[status(thm)],[c_88,c_1217]) ).
cnf(c_1218,negated_conjecture,
relation_rng(sK1) = relation_rng(sK2),
inference(copy,[status(thm)],[c_93]) ).
cnf(c_1219,negated_conjecture,
( ~ in(A,relation_dom(sK1))
| in(apply(sK1,A),relation_rng(sK2))
| ~ function(sK1)
| ~ relation(sK1) ),
inference(resolve,[status(thm)],[c_109,c_1218]) ).
cnf(c_1220,negated_conjecture,
( ~ in(A,relation_dom(sK1))
| in(apply(sK1,A),relation_rng(sK1))
| ~ function(sK1)
| ~ relation(sK1) ),
inference(paramod,[status(thm)],[c_93,c_1219]) ).
cnf(c_1221,negated_conjecture,
( ~ in(A,relation_dom(sK1))
| in(apply(sK1,A),relation_rng(sK1))
| ~ function(sK1) ),
inference(resolve,[status(thm)],[c_85,c_1220]) ).
cnf(c_712,negated_conjecture,
( ~ in(A,relation_dom(sK1))
| in(apply(sK1,A),relation_rng(sK1)) ),
inference(resolve,[status(thm)],[c_86,c_1221]) ).
cnf(c_794,plain,
in(apply(sK2,sK0(sK2,sK1)),relation_rng(sK1)),
inference(resolve,[status(thm)],[c_711,c_257]) ).
cnf(c_799,plain,
in(apply(sK1,sK0(sK2,sK1)),relation_rng(sK1)),
inference(resolve,[status(thm)],[c_712,c_257]) ).
cnf(c_1222,plain,
sK3 = apply(sK2,sK0(sK2,sK1)),
inference(resolve,[status(thm)],[c_794,c_259]) ).
cnf(c_1185,plain,
apply(sK2,sK0(sK2,sK1)) = sK3,
inference(copy,[status(thm)],[c_1222]) ).
cnf(c_1223,negated_conjecture,
sK3 != apply(sK1,sK0(sK2,sK1)),
inference(paramod,[status(thm)],[c_1185,c_256]) ).
cnf(c_1186,negated_conjecture,
apply(sK1,sK0(sK2,sK1)) != sK3,
inference(copy,[status(thm)],[c_1223]) ).
cnf(c_1224,plain,
sK3 = apply(sK1,sK0(sK2,sK1)),
inference(resolve,[status(thm)],[c_799,c_259]) ).
cnf(c_1225,plain,
apply(sK1,sK0(sK2,sK1)) = sK3,
inference(copy,[status(thm)],[c_1224]) ).
cnf(c_1197,plain,
$false,
inference(resolve,[status(thm)],[c_1186,c_1225]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET995+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.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 08:32:21 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 1261928 was started by sandbox2 on n002,
% 0.13/0.36 % Sat Sep 26 08:32:21 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 2.37/0.73
% 2.37/0.73 % SZS status Theorem for theBenchmark
% 2.37/0.73
% 2.37/0.73 % Proof 1 at 0.21 (+ 0.06) seconds.
% 2.37/0.73 % Length of proof is 29.
% 2.37/0.73 % Level of proof is 8.
% 2.37/0.73 % Maximum clause weight is 42.000.
% 2.37/0.73 % Given clauses 327.
% 2.37/0.73
% 2.37/0.73 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------