%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM412+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:16:56 AM UTC 2026
% Result : Theorem 0.09s 0.42s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 5
% Syntax : Number of formulae : 32 ( 9 unt; 0 def)
% Number of atoms : 86 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 92 ( 38 ~; 33 |; 11 &)
% ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 40 ( 5 sgn 15 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d8_ordinal1,axiom,
! [A,B] :
( ( transfinite_sequence(B)
& function(B)
& relation(B) )
=> ( transfinite_sequence_of(B,A)
<=> subset(relation_rng(B),A) ) ),
file('theBenchmark.p',d8_ordinal1) ).
fof(dt_k2_ordinal1,axiom,
! [A,B] :
( ( ordinal(B)
& transfinite_sequence(A)
& function(A)
& relation(A) )
=> transfinite_sequence_of(tseq_dom_restriction(A,B),relation_rng(A)) ),
file('theBenchmark.p',dt_k2_ordinal1) ).
fof(dt_m1_ordinal1,axiom,
! [A,B] :
( transfinite_sequence_of(B,A)
=> ( transfinite_sequence(B)
& function(B)
& relation(B) ) ),
file('theBenchmark.p',dt_m1_ordinal1) ).
fof(t47_ordinal1,axiom,
! [A,B] :
( subset(A,B)
=> ! [C] :
( transfinite_sequence_of(C,A)
=> transfinite_sequence_of(C,B) ) ),
file('theBenchmark.p',t47_ordinal1) ).
fof(t48_ordinal1,conjecture,
! [A,B] :
( transfinite_sequence_of(B,A)
=> ! [C] :
( ordinal(C)
=> transfinite_sequence_of(tseq_dom_restriction(B,C),A) ) ),
file('theBenchmark.p',t48_ordinal1) ).
fof(t48_ordinal1_neg,negated_conjecture,
~ ! [A,B] :
( transfinite_sequence_of(B,A)
=> ! [C] :
( ordinal(C)
=> transfinite_sequence_of(tseq_dom_restriction(B,C),A) ) ),
inference(assume_negation,[status(cth)],[t48_ordinal1]) ).
cnf(c_52,plain,
( transfinite_sequence_of(tseq_dom_restriction(A,B),relation_rng(A))
| ~ ordinal(B)
| ~ transfinite_sequence(A)
| ~ function(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[dt_k2_ordinal1]) ).
fof(nnf_47,plain,
? [A,B] :
( ? [C] :
( ~ transfinite_sequence_of(tseq_dom_restriction(B,C),A)
& ordinal(C) )
& transfinite_sequence_of(B,A) ),
inference(fof_nnf,[status(thm)],[t48_ordinal1_neg]) ).
fof(sk_t48_ordinal1_neg,plain,
( ~ transfinite_sequence_of(tseq_dom_restriction(sK1,sK0),sK2)
& ordinal(sK0)
& transfinite_sequence_of(sK1,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK0]),skolemize(A,sK2),skolemize(B,sK1),skolemize(C,sK0)],[nnf_47]) ).
cnf(c_58,negated_conjecture,
ordinal(sK0),
inference(split_conjunct,[status(thm)],[sk_t48_ordinal1_neg]) ).
cnf(c_84,negated_conjecture,
( transfinite_sequence_of(tseq_dom_restriction(A,sK0),relation_rng(A))
| ~ transfinite_sequence(A)
| ~ function(A)
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_58,c_52]) ).
cnf(c_85,plain,
( transfinite_sequence(A)
| ~ transfinite_sequence_of(A,B) ),
inference(clausify,[status(thm)],[dt_m1_ordinal1]) ).
cnf(c_87,plain,
( subset(relation_rng(A),B)
| ~ transfinite_sequence_of(A,B)
| ~ transfinite_sequence(A)
| ~ function(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[d8_ordinal1]) ).
cnf(c_102,negated_conjecture,
~ transfinite_sequence_of(tseq_dom_restriction(sK1,sK0),sK2),
inference(split_conjunct,[status(thm)],[sk_t48_ordinal1_neg]) ).
cnf(c_103,negated_conjecture,
transfinite_sequence_of(sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t48_ordinal1_neg]) ).
cnf(c_109,plain,
( transfinite_sequence_of(C,B)
| ~ transfinite_sequence_of(C,A)
| ~ subset(A,B) ),
inference(clausify,[status(thm)],[t47_ordinal1]) ).
cnf(c_154,plain,
( function(A)
| ~ transfinite_sequence_of(A,B) ),
inference(clausify,[status(thm)],[dt_m1_ordinal1]) ).
cnf(c_155,plain,
( relation(A)
| ~ transfinite_sequence_of(A,B) ),
inference(clausify,[status(thm)],[dt_m1_ordinal1]) ).
cnf(c_195,negated_conjecture,
( transfinite_sequence_of(tseq_dom_restriction(A,sK0),relation_rng(A))
| ~ function(A)
| ~ relation(A)
| ~ transfinite_sequence_of(A,B) ),
inference(resolve,[status(thm)],[c_85,c_84]) ).
cnf(c_199,plain,
( ~ transfinite_sequence_of(A,C)
| subset(relation_rng(A),B)
| ~ transfinite_sequence_of(A,B)
| ~ function(A)
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_87,c_85]) ).
cnf(c_201,plain,
( subset(relation_rng(A),B)
| ~ transfinite_sequence_of(A,B)
| ~ function(A)
| ~ relation(A) ),
inference(factor,[status(thm)],[c_199]) ).
cnf(c_224,plain,
function(sK1),
inference(resolve,[status(thm)],[c_154,c_103]) ).
cnf(c_226,plain,
relation(sK1),
inference(resolve,[status(thm)],[c_155,c_103]) ).
cnf(c_376,negated_conjecture,
( transfinite_sequence_of(tseq_dom_restriction(sK1,sK0),relation_rng(sK1))
| ~ function(sK1)
| ~ relation(sK1) ),
inference(resolve,[status(thm)],[c_195,c_103]) ).
cnf(c_377,negated_conjecture,
( transfinite_sequence_of(tseq_dom_restriction(sK1,sK0),relation_rng(sK1))
| ~ function(sK1) ),
inference(resolve,[status(thm)],[c_226,c_376]) ).
cnf(c_302,negated_conjecture,
transfinite_sequence_of(tseq_dom_restriction(sK1,sK0),relation_rng(sK1)),
inference(resolve,[status(thm)],[c_224,c_377]) ).
cnf(c_378,negated_conjecture,
( subset(relation_rng(sK1),sK2)
| ~ function(sK1)
| ~ relation(sK1) ),
inference(resolve,[status(thm)],[c_201,c_103]) ).
cnf(c_379,negated_conjecture,
( subset(relation_rng(sK1),sK2)
| ~ function(sK1) ),
inference(resolve,[status(thm)],[c_226,c_378]) ).
cnf(c_313,negated_conjecture,
subset(relation_rng(sK1),sK2),
inference(resolve,[status(thm)],[c_224,c_379]) ).
cnf(c_380,plain,
( transfinite_sequence_of(A,sK2)
| ~ transfinite_sequence_of(A,relation_rng(sK1)) ),
inference(resolve,[status(thm)],[c_109,c_313]) ).
cnf(c_381,negated_conjecture,
~ transfinite_sequence_of(tseq_dom_restriction(sK1,sK0),relation_rng(sK1)),
inference(resolve,[status(thm)],[c_380,c_102]) ).
cnf(c_375,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_302,c_381]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM412+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.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 02:45:11 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 731548 was started by sandbox on n001,
% 0.09/0.36 % Sat Sep 26 02:45:11 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 0.09/0.42
% 0.09/0.42 % SZS status Theorem for theBenchmark
% 0.09/0.42
% 0.09/0.42 % Proof 1 at 0.03 (+ 0.01) seconds.
% 0.09/0.42 % Length of proof is 23.
% 0.09/0.42 % Level of proof is 5.
% 0.09/0.42 % Maximum clause weight is 14.000.
% 0.09/0.42 % Given clauses 139.
% 0.09/0.42
% 0.09/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------