%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV879-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 09:09:16 AM UTC 2026
% Result : Unsatisfiable 32.53s 5.26s
% Output : CNFRefutation 32.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 11
% Syntax : Number of formulae : 40 ( 22 unt; 0 def)
% Number of atoms : 65 ( 12 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 54 ( 29 ~; 25 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 2 con; 0-4 aty)
% Number of variables : 81 ( 14 sgn 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clsarity_nat__Orderings_Olinorder,axiom,
class_Orderings_Olinorder(tc_nat),
file('theBenchmark.p',clsarity_nat__Orderings_Olinorder) ).
cnf(c_23,plain,
class_Orderings_Olinorder(tc_nat),
inference(clausify,[status(thm)],[clsarity_nat__Orderings_Olinorder]) ).
fof(cls_Max__ge_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ c_Finite__Set_Ofinite(VAR_2,VAR_0)
| ~ hBOOL(c_in(VAR_1,VAR_2,VAR_0))
| c_lessequals(VAR_1,hAPP(c_Finite__Set_Olinorder__class_OMax(VAR_0),VAR_2),VAR_0)
| ~ class_Orderings_Olinorder(VAR_0) ),
file('theBenchmark.p',cls_Max__ge_0) ).
cnf(c_31,plain,
( ~ c_Finite__Set_Ofinite(C,A)
| ~ hBOOL(c_in(B,C,A))
| c_lessequals(B,hAPP(c_Finite__Set_Olinorder__class_OMax(A),C),A)
| ~ class_Orderings_Olinorder(A) ),
inference(clausify,[status(thm)],[cls_Max__ge_0]) ).
fof(cls_min__max_Osup__assoc_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( hAPP(hAPP(c_Orderings_Oord__class_Omax(VAR_0),hAPP(hAPP(c_Orderings_Oord__class_Omax(VAR_0),VAR_1),VAR_2)),VAR_3) = hAPP(hAPP(c_Orderings_Oord__class_Omax(VAR_0),VAR_1),hAPP(hAPP(c_Orderings_Oord__class_Omax(VAR_0),VAR_2),VAR_3))
| ~ class_Orderings_Olinorder(VAR_0) ),
file('theBenchmark.p',cls_min__max_Osup__assoc_0) ).
cnf(c_45,plain,
( hAPP(hAPP(c_Orderings_Oord__class_Omax(A),hAPP(hAPP(c_Orderings_Oord__class_Omax(A),B),C)),D) = hAPP(hAPP(c_Orderings_Oord__class_Omax(A),B),hAPP(hAPP(c_Orderings_Oord__class_Omax(A),C),D))
| ~ class_Orderings_Olinorder(A) ),
inference(clausify,[status(thm)],[cls_min__max_Osup__assoc_0]) ).
fof(cls_le__maxI2_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_lessequals(VAR_1,hAPP(hAPP(c_Orderings_Oord__class_Omax(VAR_0),VAR_2),VAR_1),VAR_0)
| ~ class_Orderings_Olinorder(VAR_0) ),
file('theBenchmark.p',cls_le__maxI2_0) ).
cnf(c_107,plain,
( c_lessequals(B,hAPP(hAPP(c_Orderings_Oord__class_Omax(A),C),B),A)
| ~ class_Orderings_Olinorder(A) ),
inference(clausify,[status(thm)],[cls_le__maxI2_0]) ).
fof(cls_sup__max_0,axiom,
! [VAR_0] :
( c_Lattices_Oupper__semilattice__class_Osup(VAR_0) = c_Orderings_Oord__class_Omax(VAR_0)
| ~ class_Lattices_Oupper__semilattice(VAR_0)
| ~ class_Orderings_Olinorder(VAR_0) ),
file('theBenchmark.p',cls_sup__max_0) ).
cnf(c_138,plain,
( c_Lattices_Oupper__semilattice__class_Osup(A) = c_Orderings_Oord__class_Omax(A)
| ~ class_Lattices_Oupper__semilattice(A)
| ~ class_Orderings_Olinorder(A) ),
inference(clausify,[status(thm)],[cls_sup__max_0]) ).
cnf(c_216,plain,
( c_Lattices_Oupper__semilattice__class_Osup(tc_nat) = c_Orderings_Oord__class_Omax(tc_nat)
| ~ class_Lattices_Oupper__semilattice(tc_nat) ),
inference(resolve,[status(thm)],[c_23,c_138]) ).
cnf(c_217,plain,
( c_Orderings_Oord__class_Omax(tc_nat) = c_Lattices_Oupper__semilattice__class_Osup(tc_nat)
| ~ class_Lattices_Oupper__semilattice(tc_nat) ),
inference(copy,[status(thm)],[c_216]) ).
cnf(c_239,plain,
c_lessequals(A,hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),B),A),tc_nat),
inference(resolve,[status(thm)],[c_23,c_107]) ).
cnf(c_297,plain,
hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),A),B)),C) = hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),A),hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),B),C)),
inference(resolve,[status(thm)],[c_23,c_45]) ).
cnf(c_318,plain,
( ~ c_Finite__Set_Ofinite(B,tc_nat)
| ~ hBOOL(c_in(A,B,tc_nat))
| c_lessequals(A,hAPP(c_Finite__Set_Olinorder__class_OMax(tc_nat),B),tc_nat) ),
inference(resolve,[status(thm)],[c_23,c_31]) ).
fof(clsarity_bool__Finite__Set_Ofinite_Ofinite,axiom,
class_Finite__Set_Ofinite_Ofinite(tc_bool),
file('theBenchmark.p',clsarity_bool__Finite__Set_Ofinite_Ofinite) ).
cnf(c_357,plain,
class_Finite__Set_Ofinite_Ofinite(tc_bool),
inference(clausify,[status(thm)],[clsarity_bool__Finite__Set_Ofinite_Ofinite]) ).
fof(clsarity_nat__Lattices_Oupper__semilattice,axiom,
class_Lattices_Oupper__semilattice(tc_nat),
file('theBenchmark.p',clsarity_nat__Lattices_Oupper__semilattice) ).
cnf(c_371,plain,
class_Lattices_Oupper__semilattice(tc_nat),
inference(clausify,[status(thm)],[clsarity_nat__Lattices_Oupper__semilattice]) ).
fof(cls_finite_0,axiom,
! [VAR_0,VAR_1] :
( c_Finite__Set_Ofinite(VAR_1,VAR_0)
| ~ class_Finite__Set_Ofinite_Ofinite(VAR_0) ),
file('theBenchmark.p',cls_finite_0) ).
cnf(c_391,plain,
( c_Finite__Set_Ofinite(B,A)
| ~ class_Finite__Set_Ofinite_Ofinite(A) ),
inference(clausify,[status(thm)],[cls_finite_0]) ).
fof(cls_finite__imageI_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ c_Finite__Set_Ofinite(VAR_1,VAR_2)
| c_Finite__Set_Ofinite(c_Set_Oimage(VAR_0,VAR_1,VAR_2,VAR_3),VAR_3) ),
file('theBenchmark.p',cls_finite__imageI_0) ).
cnf(c_419,plain,
( ~ c_Finite__Set_Ofinite(B,C)
| c_Finite__Set_Ofinite(c_Set_Oimage(A,B,C,D),D) ),
inference(clausify,[status(thm)],[cls_finite__imageI_0]) ).
fof(cls_rangeI_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : hBOOL(c_in(hAPP(VAR_0,VAR_1),c_Set_Oimage(VAR_0,c_Orderings_Otop__class_Otop(tc_fun(VAR_2,tc_bool)),VAR_2,VAR_3),VAR_3)),
file('theBenchmark.p',cls_rangeI_0) ).
cnf(c_475,plain,
hBOOL(c_in(hAPP(A,B),c_Set_Oimage(A,c_Orderings_Otop__class_Otop(tc_fun(C,tc_bool)),C,D),D)),
inference(clausify,[status(thm)],[cls_rangeI_0]) ).
fof(cls_not__less__eq__eq_1,axiom,
! [VAR_0,VAR_1] :
( ~ c_lessequals(c_Suc(VAR_1),VAR_0,tc_nat)
| ~ c_lessequals(VAR_0,VAR_1,tc_nat) ),
file('theBenchmark.p',cls_not__less__eq__eq_1) ).
cnf(c_811,plain,
( ~ c_lessequals(c_Suc(B),A,tc_nat)
| ~ c_lessequals(A,B,tc_nat) ),
inference(clausify,[status(thm)],[cls_not__less__eq__eq_1]) ).
cnf(c_1037,plain,
c_Orderings_Oord__class_Omax(tc_nat) = c_Lattices_Oupper__semilattice__class_Osup(tc_nat),
inference(resolve,[status(thm)],[c_371,c_217]) ).
cnf(c_18887,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),A),B)),C) = hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),A),hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),B),C)),
inference(paramod,[status(thm)],[c_1037,c_297]) ).
cnf(c_18888,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),A),B)),C) = hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),A),hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),B),C)),
inference(paramod,[status(thm)],[c_1037,c_18887]) ).
cnf(c_18889,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),A),B)),C) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),A),hAPP(hAPP(c_Orderings_Oord__class_Omax(tc_nat),B),C)),
inference(paramod,[status(thm)],[c_1037,c_18888]) ).
cnf(c_1148,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),A),B)),C) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),B),C)),
inference(paramod,[status(thm)],[c_1037,c_18889]) ).
cnf(c_1161,plain,
c_lessequals(A,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),B),A),tc_nat),
inference(paramod,[status(thm)],[c_1037,c_239]) ).
cnf(c_1261,plain,
c_Finite__Set_Ofinite(A,tc_bool),
inference(resolve,[status(thm)],[c_391,c_357]) ).
cnf(c_1312,plain,
( ~ c_Finite__Set_Ofinite(c_Set_Oimage(A,c_Orderings_Otop__class_Otop(tc_fun(C,tc_bool)),C,tc_nat),tc_nat)
| c_lessequals(hAPP(A,B),hAPP(c_Finite__Set_Olinorder__class_OMax(tc_nat),c_Set_Oimage(A,c_Orderings_Otop__class_Otop(tc_fun(C,tc_bool)),C,tc_nat)),tc_nat) ),
inference(resolve,[status(thm)],[c_475,c_318]) ).
cnf(c_4615,plain,
~ c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),A),c_Suc(B)),B,tc_nat),
inference(resolve,[status(thm)],[c_1161,c_811]) ).
cnf(c_4732,plain,
c_Finite__Set_Ofinite(c_Set_Oimage(A,B,tc_bool,C),C),
inference(resolve,[status(thm)],[c_1261,c_419]) ).
cnf(c_6821,plain,
~ c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_nat),B),c_Suc(C))),C,tc_nat),
inference(paramod,[status(thm)],[c_1148,c_4615]) ).
cnf(c_18885,plain,
c_lessequals(hAPP(A,B),hAPP(c_Finite__Set_Olinorder__class_OMax(tc_nat),c_Set_Oimage(A,c_Orderings_Otop__class_Otop(tc_fun(tc_bool,tc_bool)),tc_bool,tc_nat)),tc_nat),
inference(resolve,[status(thm)],[c_1312,c_4732]) ).
cnf(c_18886,plain,
$false,
inference(resolve,[status(thm)],[c_18885,c_6821]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV879-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.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 15:06:44 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 445508 was started by sandbox2 on n009,
% 0.09/0.36 % Sat Sep 26 15:06:44 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 32.53/5.26
% 32.53/5.26 % given #500 (I,wt=22): 968 c_lessequals(A,B,tc_fun(C,tc_bool)) | -c_HOL_Oord__class_Oless(A,B,tc_fun(C,tc_bool)) # tptp_name(cls_psubset__eq_0) # clausal_fof(1). [assumption].
% 32.53/5.26
% 32.53/5.26 % given #1000 (W,wt=20): 9032 c_Complete__Lattice_OInf__class_OInf(v_U,tc_bool) = v_x | c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_bool),v_x,tc_bool). [resolve(6196,a,5263,b)].
% 32.53/5.26
% 32.53/5.26 % given #1500 (F,wt=25): 16481 c_Set_Oimage(A,v_G,B,C) != c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)). [para(16208(a,1),4834(a,1,2))].
% 32.53/5.26
% 32.53/5.26 % SZS status Unsatisfiable for theBenchmark
% 32.53/5.26
% 32.53/5.26 % Proof 1 at 4.07 (+ 0.69) seconds.
% 32.53/5.26 % Length of proof is 26.
% 32.53/5.26 % Level of proof is 7.
% 32.53/5.26 % Maximum clause weight is 65.000.
% 32.53/5.26 % Given clauses 1794.
% 32.53/5.26
% 32.53/5.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------