%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SCT159+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:28:34 AM UTC 2026
% Result : Theorem 179.66s 29.53s
% Output : CNFRefutation 179.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 7
% Syntax : Number of formulae : 23 ( 12 unt; 0 def)
% Number of atoms : 51 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 46 ( 18 ~; 17 |; 6 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-4 aty)
% Number of variables : 57 ( 7 sgn 28 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_finite__imageI,axiom,
! [V_h_2,T_b,V_Fa_2,T_a] :
( c_Finite__Set_Ofinite(T_a,V_Fa_2)
=> c_Finite__Set_Ofinite(T_b,c_Set_Oimage(T_a,T_b,V_h_2,V_Fa_2)) ),
file('theBenchmark.p',fact_finite__imageI) ).
fof(fact_finite__subset,axiom,
! [V_B_2,V_A_2,T_a] :
( c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,tc_HOL_Obool),V_A_2,V_B_2)
=> ( c_Finite__Set_Ofinite(T_a,V_B_2)
=> c_Finite__Set_Ofinite(T_a,V_A_2) ) ),
file('theBenchmark.p',fact_finite__subset) ).
fof(fact_finite__nat__set__iff__bounded__le,axiom,
! [V_N_2] :
( c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)
<=> ? [B_m] :
! [B_x] :
( c_member(tc_Nat_Onat,B_x,V_N_2)
=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_x,B_m) ) ),
file('theBenchmark.p',fact_finite__nat__set__iff__bounded__le) ).
fof(fact_subset__UNIV,axiom,
! [V_A_2,T_a] : c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,tc_HOL_Obool),V_A_2,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool))),
file('theBenchmark.p',fact_subset__UNIV) ).
fof(fact_rangeI,axiom,
! [T_b,V_x_2,V_f_2,T_a] : c_member(T_a,hAPP(V_f_2,V_x_2),c_Set_Oimage(T_b,T_a,V_f_2,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_HOL_Obool)))),
file('theBenchmark.p',fact_rangeI) ).
fof(fact_Suc__n__not__le__n,axiom,
! [V_n] : ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_Nat_OSuc,V_n),V_n),
file('theBenchmark.p',fact_Suc__n__not__le__n) ).
fof(fact_finite__indi,axiom,
c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool))),
file('theBenchmark.p',fact_finite__indi) ).
cnf(c_739,plain,
c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool))),
inference(clausify,[status(thm)],[fact_finite__indi]) ).
cnf(c_740,plain,
( c_Finite__Set_Ofinite(C,c_Set_Oimage(A,C,D,B))
| ~ c_Finite__Set_Ofinite(A,B) ),
inference(clausify,[status(thm)],[fact_finite__imageI]) ).
cnf(c_805,plain,
( c_Finite__Set_Ofinite(A,B)
| ~ c_Finite__Set_Ofinite(A,C)
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(A,tc_HOL_Obool),B,C) ),
inference(clausify,[status(thm)],[fact_finite__subset]) ).
fof(nnf_137,plain,
! [V_N_2] :
( ( ! [B_m] :
? [B_x] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_x,B_m)
& c_member(tc_Nat_Onat,B_x,V_N_2) )
| c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2) )
& ( ? [X0] :
! [X1] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X0)
| ~ c_member(tc_Nat_Onat,X1,V_N_2) )
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2) ) ),
inference(fof_nnf,[status(thm)],[fact_finite__nat__set__iff__bounded__le]) ).
fof(sk_fact_finite__nat__set__iff__bounded__le_sk,plain,
! [V_N_2] :
( ( ! [B_m] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK1(V_N_2,B_m),B_m)
& c_member(tc_Nat_Onat,sK1(V_N_2,B_m),V_N_2) )
| c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2) )
& ( ! [X1] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,sK0(V_N_2))
| ~ c_member(tc_Nat_Onat,X1,V_N_2) )
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0(V_N_2)),skolemize(B_x,sK1(V_N_2,B_m))],[nnf_137]) ).
fof(sk_fact_finite__nat__set__iff__bounded__le,plain,
( ! [VAR_0,VAR_1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK1(VAR_0,VAR_1),VAR_1)
| c_Finite__Set_Ofinite(tc_Nat_Onat,VAR_0) )
& ! [VAR_0,VAR_1] :
( c_member(tc_Nat_Onat,sK1(VAR_0,VAR_1),VAR_0)
| c_Finite__Set_Ofinite(tc_Nat_Onat,VAR_0) )
& ! [VAR_0,VAR_1] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,VAR_1,sK0(VAR_0))
| ~ c_member(tc_Nat_Onat,VAR_1,VAR_0)
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact_finite__nat__set__iff__bounded__le_sk]) ).
cnf(c_870,plain,
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B,sK0(A))
| ~ c_member(tc_Nat_Onat,B,A)
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,A) ),
inference(split_conjunct,[status(thm)],[sk_fact_finite__nat__set__iff__bounded__le]) ).
cnf(c_893,plain,
c_Orderings_Oord__class_Oless__eq(tc_fun(A,tc_HOL_Obool),B,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool))),
inference(clausify,[status(thm)],[fact_subset__UNIV]) ).
cnf(c_907,plain,
c_member(A,hAPP(B,C),c_Set_Oimage(D,A,B,c_Orderings_Otop__class_Otop(tc_fun(D,tc_HOL_Obool)))),
inference(clausify,[status(thm)],[fact_rangeI]) ).
cnf(c_929,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_Nat_OSuc,A),A),
inference(clausify,[status(thm)],[fact_Suc__n__not__le__n]) ).
cnf(c_13234,plain,
( c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,A)
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool),A,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool))) ),
inference(resolve,[status(thm)],[c_805,c_739]) ).
cnf(c_2799,plain,
c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,A),
inference(resolve,[status(thm)],[c_893,c_13234]) ).
cnf(c_2813,plain,
c_Finite__Set_Ofinite(A,c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi,A,B,C)),
inference(resolve,[status(thm)],[c_2799,c_740]) ).
cnf(c_13235,plain,
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,sK0(c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi,tc_Nat_Onat,B,C)))
| ~ c_member(tc_Nat_Onat,A,c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi,tc_Nat_Onat,B,C)) ),
inference(resolve,[status(thm)],[c_870,c_2813]) ).
cnf(c_13232,plain,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(A,B),sK0(c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi,tc_Nat_Onat,A,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool))))),
inference(resolve,[status(thm)],[c_13235,c_907]) ).
cnf(c_13233,plain,
$false,
inference(resolve,[status(thm)],[c_13232,c_929]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT159+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/5.45 % Computer : n008.cluster.edu
% 0.18/5.45 % Model : x86_64 x86_64
% 0.18/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.45 % Memory : 8046.5625MB
% 0.18/5.45 % OS : Linux 6.8.0-71-generic
% 0.18/5.45 % CPULimit : 300
% 0.18/5.45 % WCLimit : 300
% 0.18/5.45 % DateTime : Sat Sep 26 06:34:45 UTC 2026
% 0.18/5.46 % CPUTime :
% 0.18/5.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/5.46 % Process 2990197 was started by sandbox2 on n008,
% 0.18/5.46 % Sat Sep 26 06:34:45 2026
% 0.18/5.46 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.23/5.63
% 0.23/5.63 % From the command line: assign(max_seconds, 300).
% 0.23/5.63
% 0.23/5.63 % SInE: 355 to sos, 177 to usable, of 532 axioms (tolerance 2.00, depth 0 fixpoint).
% 179.66/29.53
% 179.66/29.53 % given #500 (F,wt=33): 3874 -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Nat_Onat_Onat__size(c_Nat_Osize__class_Osize(tc_Nat_Onat,hAPP(c_Nat_OSuc,A))),c_Nat_Onat_Onat__size(c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat)))). [para(1194(a,1),3870(a,2,1))].
% 179.66/29.53
% 179.66/29.53 % SZS status Theorem for theBenchmark
% 179.66/29.53
% 179.66/29.53 % Proof 1 at 6.33 (+ 1.14) seconds.
% 179.66/29.53 % Length of proof is 17.
% 179.66/29.53 % Level of proof is 5.
% 179.66/29.53 % Maximum clause weight is 222.000.
% 179.66/29.53 % Given clauses 860.
% 179.66/29.53
% 179.66/29.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------