%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SCT071-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:27 AM UTC 2026
% Result : Unsatisfiable 85.47s 17.25s
% Output : CNFRefutation 85.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of formulae : 29 ( 16 unt; 0 def)
% Number of atoms : 44 ( 13 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 36 ( 21 ~; 15 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 2 prp; 0-5 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-4 aty)
% Number of variables : 47 ( 4 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_conjecture_0,axiom,
~ v_thesis____,
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_243,plain,
~ v_thesis____,
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
fof(cls_that_0,axiom,
! [VAR_0] :
( v_thesis____
| ~ c_Fun_Oinj__on(VAR_0,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi,tc_nat)
| c_Set_Oimage(VAR_0,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi,tc_nat) != c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Finite__Set_Ocard(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),tc_nat) ),
file('theBenchmark.p',cls_that_0) ).
cnf(c_247,plain,
( v_thesis____
| ~ c_Fun_Oinj__on(A,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi,tc_nat)
| c_Set_Oimage(A,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi,tc_nat) != c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Finite__Set_Ocard(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),tc_nat) ),
inference(clausify,[status(thm)],[cls_that_0]) ).
cnf(c_248,plain,
( ~ c_Fun_Oinj__on(A,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi,tc_nat)
| c_Set_Oimage(A,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi,tc_nat) != c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Finite__Set_Ocard(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),tc_nat) ),
inference(resolve,[status(thm)],[c_243,c_247]) ).
fof(cls_atLeast0LessThan_0,axiom,
! [VAR_0] : c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),VAR_0,tc_nat) = c_SetInterval_Oord__class_OlessThan(VAR_0,tc_nat),
file('theBenchmark.p',cls_atLeast0LessThan_0) ).
cnf(c_259,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),A,tc_nat) = c_SetInterval_Oord__class_OlessThan(A,tc_nat),
inference(clausify,[status(thm)],[cls_atLeast0LessThan_0]) ).
fof(cls_finite__indi_0,axiom,
c_Finite__Set_Ofinite(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),
file('theBenchmark.p',cls_finite__indi_0) ).
cnf(c_281,plain,
c_Finite__Set_Ofinite(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),
inference(clausify,[status(thm)],[cls_finite__indi_0]) ).
fof(cls_ex__bij__betw__finite__nat_0,axiom,
! [VAR_0,VAR_1] :
( ~ c_Finite__Set_Ofinite(VAR_0,VAR_1)
| c_Fun_Obij__betw(c_List_Osko__SetInterval__Xex__bij__betw__finite__nat__1__1(VAR_0,VAR_1),VAR_0,c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Finite__Set_Ocard(VAR_0,VAR_1),tc_nat),VAR_1,tc_nat) ),
file('theBenchmark.p',cls_ex__bij__betw__finite__nat_0) ).
cnf(c_299,plain,
( ~ c_Finite__Set_Ofinite(A,B)
| c_Fun_Obij__betw(c_List_Osko__SetInterval__Xex__bij__betw__finite__nat__1__1(A,B),A,c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Finite__Set_Ocard(A,B),tc_nat),B,tc_nat) ),
inference(clausify,[status(thm)],[cls_ex__bij__betw__finite__nat_0]) ).
cnf(c_300,plain,
( ~ c_Finite__Set_Ofinite(A,B)
| c_Fun_Obij__betw(c_List_Osko__SetInterval__Xex__bij__betw__finite__nat__1__1(A,B),A,c_SetInterval_Oord__class_OlessThan(c_Finite__Set_Ocard(A,B),tc_nat),B,tc_nat) ),
inference(paramod,[status(thm)],[c_259,c_299]) ).
fof(cls_bij__betw__def_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ c_Fun_Obij__betw(VAR_0,VAR_1,VAR_4,VAR_2,VAR_3)
| c_Fun_Oinj__on(VAR_0,VAR_1,VAR_2,VAR_3) ),
file('theBenchmark.p',cls_bij__betw__def_0) ).
cnf(c_301,plain,
( ~ c_Fun_Obij__betw(A,B,E,C,D)
| c_Fun_Oinj__on(A,B,C,D) ),
inference(clausify,[status(thm)],[cls_bij__betw__def_0]) ).
fof(cls_Int__UNIV__left_0,axiom,
! [VAR_0,VAR_1] : c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Otop__class_Otop(tc_fun(VAR_0,tc_bool)),VAR_1,tc_fun(VAR_0,tc_bool)) = VAR_1,
file('theBenchmark.p',cls_Int__UNIV__left_0) ).
cnf(c_425,plain,
c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool)) = B,
inference(clausify,[status(thm)],[cls_Int__UNIV__left_0]) ).
fof(cls_bij__betw__def_1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ c_Fun_Obij__betw(VAR_0,VAR_1,VAR_4,VAR_2,VAR_3)
| c_Set_Oimage(VAR_0,VAR_1,VAR_2,VAR_3) = VAR_4 ),
file('theBenchmark.p',cls_bij__betw__def_1) ).
cnf(c_455,plain,
( ~ c_Fun_Obij__betw(A,B,E,C,D)
| c_Set_Oimage(A,B,C,D) = E ),
inference(clausify,[status(thm)],[cls_bij__betw__def_1]) ).
fof(cls_finite__Int_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ c_Finite__Set_Ofinite(VAR_0,VAR_2)
| c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(VAR_0,VAR_1,tc_fun(VAR_2,tc_bool)),VAR_2) ),
file('theBenchmark.p',cls_finite__Int_0) ).
cnf(c_474,plain,
( ~ c_Finite__Set_Ofinite(A,C)
| c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(A,B,tc_fun(C,tc_bool)),C) ),
inference(clausify,[status(thm)],[cls_finite__Int_0]) ).
cnf(c_939,plain,
( ~ c_Fun_Oinj__on(A,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi,tc_nat)
| c_Set_Oimage(A,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi,tc_nat) != c_SetInterval_Oord__class_OlessThan(c_Finite__Set_Ocard(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),tc_nat) ),
inference(paramod,[status(thm)],[c_259,c_248]) ).
cnf(c_24224,plain,
c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),A,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),
inference(resolve,[status(thm)],[c_474,c_281]) ).
cnf(c_1411,plain,
c_Finite__Set_Ofinite(A,tc_Arrow__Order__Mirabelle_Oindi),
inference(paramod,[status(thm)],[c_425,c_24224]) ).
cnf(c_3085,plain,
c_Fun_Obij__betw(c_List_Osko__SetInterval__Xex__bij__betw__finite__nat__1__1(A,tc_Arrow__Order__Mirabelle_Oindi),A,c_SetInterval_Oord__class_OlessThan(c_Finite__Set_Ocard(A,tc_Arrow__Order__Mirabelle_Oindi),tc_nat),tc_Arrow__Order__Mirabelle_Oindi,tc_nat),
inference(resolve,[status(thm)],[c_1411,c_300]) ).
cnf(c_24219,plain,
c_Set_Oimage(c_List_Osko__SetInterval__Xex__bij__betw__finite__nat__1__1(A,tc_Arrow__Order__Mirabelle_Oindi),A,tc_Arrow__Order__Mirabelle_Oindi,tc_nat) = c_SetInterval_Oord__class_OlessThan(c_Finite__Set_Ocard(A,tc_Arrow__Order__Mirabelle_Oindi),tc_nat),
inference(resolve,[status(thm)],[c_3085,c_455]) ).
cnf(c_24221,plain,
c_Fun_Oinj__on(c_List_Osko__SetInterval__Xex__bij__betw__finite__nat__1__1(A,tc_Arrow__Order__Mirabelle_Oindi),A,tc_Arrow__Order__Mirabelle_Oindi,tc_nat),
inference(resolve,[status(thm)],[c_3085,c_301]) ).
cnf(c_24225,plain,
c_Set_Oimage(c_List_Osko__SetInterval__Xex__bij__betw__finite__nat__1__1(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi,tc_nat) != c_SetInterval_Oord__class_OlessThan(c_Finite__Set_Ocard(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),tc_nat),
inference(resolve,[status(thm)],[c_24221,c_939]) ).
cnf(c_24226,plain,
c_SetInterval_Oord__class_OlessThan(c_Finite__Set_Ocard(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),tc_nat) != c_SetInterval_Oord__class_OlessThan(c_Finite__Set_Ocard(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi),tc_nat),
inference(paramod,[status(thm)],[c_24219,c_24225]) ).
cnf(c_24223,plain,
$false,
inference(copy,[status(thm)],[c_24226]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT071-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n026.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sat Sep 26 06:27:31 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.38 % Process 306388 was started by sandbox on n026,
% 0.09/5.38 % Sat Sep 26 06:27:31 2026
% 0.09/5.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/5.41
% 0.14/5.41 % From the command line: assign(max_seconds, 300).
% 85.47/17.25
% 85.47/17.25 % given #500 (I,wt=9): 811 c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool)) # tptp_name(cls_empty__subsetI_0) # clausal_fof(1). [assumption].
% 85.47/17.25
% 85.47/17.25 % given #1000 (T,wt=9): 1547 c_Lattices_Olower__semilattice__class_Oinf(A,c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_nat),tc_nat) = A. [resolve(542,a,225,a)].
% 85.47/17.25
% 85.47/17.25 % given #1500 (F,wt=11): 11808 c_Suc(c_Lattices_Oupper__semilattice__class_Osup(A,c_Lattices_Oupper__semilattice__class_Osup(c_Suc(B),C,tc_nat),tc_nat)) != B. [para(138(a,1),11727(a,1,1))].
% 85.47/17.25
% 85.47/17.25 % given #2000 (T,wt=11): 4842 hBOOL(c_in(A,c_Set_Oinsert(B,c_SetInterval_Oord__class_OlessThan(c_Suc(A),tc_nat),tc_nat),tc_nat)). [resolve(2274,a,380,b)].
% 85.47/17.25
% 85.47/17.25 % given #2500 (F,wt=13): 19157 -c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(c_Suc(c_Suc(c_Suc(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_nat)))),C,tc_nat),B,tc_nat). [para(6908(a,1),16451(a,2))].
% 85.47/17.25
% 85.47/17.25 % given #3000 (T,wt=12): 3084 c_lessequals(c_Finite__Set_Ocard(c_Set_Oimage(A,B,tc_Arrow__Order__Mirabelle_Oindi,C),C),c_Finite__Set_Ocard(B,tc_Arrow__Order__Mirabelle_Oindi),tc_nat). [resolve(1411,a,419,b)].
% 85.47/17.25
% 85.47/17.25 % SZS status Unsatisfiable for theBenchmark
% 85.47/17.25
% 85.47/17.25 % Proof 1 at 9.23 (+ 2.49) seconds.
% 85.47/17.25 % Length of proof is 17.
% 85.47/17.25 % Level of proof is 4.
% 85.47/17.25 % Maximum clause weight is 27.000.
% 85.47/17.25 % Given clauses 3007.
% 85.47/17.25
% 85.47/17.25 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------