%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV686-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 : 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:08:57 AM UTC 2026
% Result : Unsatisfiable 102.11s 14.09s
% Output : CNFRefutation 102.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 13
% Syntax : Number of formulae : 43 ( 29 unt; 0 def)
% Number of atoms : 63 ( 9 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 48 ( 28 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 1 con; 0-5 aty)
% Number of variables : 118 ( 41 sgn 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom,
class_Ring__and__Field_Oordered__semidom(tc_nat),
file('theBenchmark.p',clsarity_nat__Ring__and__Field_Oordered__semidom) ).
cnf(c_1,plain,
class_Ring__and__Field_Oordered__semidom(tc_nat),
inference(clausify,[status(thm)],[clsarity_nat__Ring__and__Field_Oordered__semidom]) ).
fof(cls_of__nat__0__less__iff_1,axiom,
! [VAR_0,VAR_1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),VAR_1,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(VAR_0),c_Nat_Osemiring__1__class_Oof__nat(VAR_1,VAR_0),VAR_0)
| ~ class_Ring__and__Field_Oordered__semidom(VAR_0) ),
file('theBenchmark.p',cls_of__nat__0__less__iff_1) ).
cnf(c_7,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),B,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Nat_Osemiring__1__class_Oof__nat(B,A),A)
| ~ class_Ring__and__Field_Oordered__semidom(A) ),
inference(clausify,[status(thm)],[cls_of__nat__0__less__iff_1]) ).
fof(cls_less__add__one_0,axiom,
! [VAR_0,VAR_1] :
( c_HOL_Oord__class_Oless(VAR_1,hAPP(hAPP(c_HOL_Oplus__class_Oplus(VAR_0),VAR_1),c_HOL_Oone__class_Oone(VAR_0)),VAR_0)
| ~ class_Ring__and__Field_Oordered__semidom(VAR_0) ),
file('theBenchmark.p',cls_less__add__one_0) ).
cnf(c_10,plain,
( c_HOL_Oord__class_Oless(B,hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),B),c_HOL_Oone__class_Oone(A)),A)
| ~ class_Ring__and__Field_Oordered__semidom(A) ),
inference(clausify,[status(thm)],[cls_less__add__one_0]) ).
fof(clsarity_nat__Ring__and__Field_Ocomm__semiring__1,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_nat),
file('theBenchmark.p',clsarity_nat__Ring__and__Field_Ocomm__semiring__1) ).
cnf(c_111,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_nat),
inference(clausify,[status(thm)],[clsarity_nat__Ring__and__Field_Ocomm__semiring__1]) ).
fof(cls_class__semiring_Oadd__0_0,axiom,
! [VAR_0,VAR_1] :
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(VAR_0),c_HOL_Ozero__class_Ozero(VAR_0)),VAR_1) = VAR_1
| ~ class_Ring__and__Field_Ocomm__semiring__1(VAR_0) ),
file('theBenchmark.p',cls_class__semiring_Oadd__0_0) ).
cnf(c_138,plain,
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),c_HOL_Ozero__class_Ozero(A)),B) = B
| ~ class_Ring__and__Field_Ocomm__semiring__1(A) ),
inference(clausify,[status(thm)],[cls_class__semiring_Oadd__0_0]) ).
fof(cls_add__strict__right__mono_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ c_HOL_Oord__class_Oless(VAR_1,VAR_3,VAR_0)
| c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(VAR_0),VAR_1),VAR_2),hAPP(hAPP(c_HOL_Oplus__class_Oplus(VAR_0),VAR_3),VAR_2),VAR_0)
| ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(VAR_0) ),
file('theBenchmark.p',cls_add__strict__right__mono_0) ).
cnf(c_345,plain,
( ~ c_HOL_Oord__class_Oless(B,D,A)
| c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),B),C),hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),D),C),A)
| ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(A) ),
inference(clausify,[status(thm)],[cls_add__strict__right__mono_0]) ).
fof(clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add,axiom,
class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat),
file('theBenchmark.p',clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add) ).
cnf(c_346,plain,
class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat),
inference(clausify,[status(thm)],[clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add]) ).
fof(clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat),
file('theBenchmark.p',clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le) ).
cnf(c_349,plain,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat),
inference(clausify,[status(thm)],[clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le]) ).
fof(cls_add__less__cancel__right_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(VAR_0),VAR_1),VAR_3),hAPP(hAPP(c_HOL_Oplus__class_Oplus(VAR_0),VAR_2),VAR_3),VAR_0)
| c_HOL_Oord__class_Oless(VAR_1,VAR_2,VAR_0)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(VAR_0) ),
file('theBenchmark.p',cls_add__less__cancel__right_0) ).
cnf(c_351,plain,
( ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),B),D),hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),C),D),A)
| c_HOL_Oord__class_Oless(B,C,A)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(A) ),
inference(clausify,[status(thm)],[cls_add__less__cancel__right_0]) ).
cnf(c_376,plain,
( ~ c_HOL_Oord__class_Oless(A,C,tc_nat)
| c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),B),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),C),B),tc_nat) ),
inference(resolve,[status(thm)],[c_345,c_346]) ).
cnf(c_462,plain,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),A) = A,
inference(resolve,[status(thm)],[c_138,c_111]) ).
fof(cls_COMBI__def_0,axiom,
! [VAR_0,VAR_1] : hAPP(c_COMBI(VAR_0),VAR_1) = VAR_1,
file('theBenchmark.p',cls_COMBI__def_0) ).
cnf(c_612,plain,
hAPP(c_COMBI(A),B) = B,
inference(clausify,[status(thm)],[cls_COMBI__def_0]) ).
fof(cls_gr__implies__not0_0,axiom,
! [VAR_0] : ~ c_HOL_Oord__class_Oless(VAR_0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('theBenchmark.p',cls_gr__implies__not0_0) ).
cnf(c_631,plain,
~ c_HOL_Oord__class_Oless(A,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(clausify,[status(thm)],[cls_gr__implies__not0_0]) ).
fof(cls_COMBB__def_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] : hAPP(hAPP(hAPP(c_COMBB(VAR_0,VAR_1,VAR_2),VAR_3),VAR_4),VAR_5) = hAPP(VAR_3,hAPP(VAR_4,VAR_5)),
file('theBenchmark.p',cls_COMBB__def_0) ).
cnf(c_687,plain,
hAPP(hAPP(hAPP(c_COMBB(A,B,C),D),E),F) = hAPP(D,hAPP(E,F)),
inference(clausify,[status(thm)],[cls_COMBB__def_0]) ).
fof(cls_COMBS__def_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] : hAPP(c_COMBS(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4),VAR_5) = hAPP(hAPP(VAR_0,VAR_5),hAPP(VAR_1,VAR_5)),
file('theBenchmark.p',cls_COMBS__def_0) ).
cnf(c_689,plain,
hAPP(c_COMBS(A,B,C,D,E),F) = hAPP(hAPP(A,F),hAPP(B,F)),
inference(clausify,[status(thm)],[cls_COMBS__def_0]) ).
cnf(c_713,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),A,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osemiring__1__class_Oof__nat(A,tc_nat),tc_nat) ),
inference(resolve,[status(thm)],[c_1,c_7]) ).
cnf(c_716,plain,
c_HOL_Oord__class_Oless(A,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),c_HOL_Oone__class_Oone(tc_nat)),tc_nat),
inference(resolve,[status(thm)],[c_1,c_10]) ).
cnf(c_838,plain,
( ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),C),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),B),C),tc_nat)
| c_HOL_Oord__class_Oless(A,B,tc_nat) ),
inference(resolve,[status(thm)],[c_349,c_351]) ).
cnf(c_14950,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osemiring__1__class_Oof__nat(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oone__class_Oone(tc_nat)),tc_nat),tc_nat),
inference(resolve,[status(thm)],[c_716,c_713]) ).
cnf(c_2450,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),
inference(paramod,[status(thm)],[c_462,c_14950]) ).
cnf(c_14951,plain,
( ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),B),B,tc_nat)
| c_HOL_Oord__class_Oless(A,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(paramod,[status(thm)],[c_462,c_838]) ).
cnf(c_3039,plain,
~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),B),B,tc_nat),
inference(resolve,[status(thm)],[c_631,c_14951]) ).
cnf(c_3666,plain,
~ c_HOL_Oord__class_Oless(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),A,B,C,D),E),hAPP(A,E),tc_nat),
inference(paramod,[status(thm)],[c_689,c_3039]) ).
cnf(c_4034,plain,
~ c_HOL_Oord__class_Oless(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),c_COMBS(A,B,C,D,E),F,V6,V7),V8),hAPP(hAPP(A,V8),hAPP(B,V8)),tc_nat),
inference(paramod,[status(thm)],[c_689,c_3666]) ).
cnf(c_14952,plain,
c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),A),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Oone__class_Oone(tc_nat),tc_nat)),A),tc_nat),
inference(resolve,[status(thm)],[c_2450,c_376]) ).
cnf(c_6774,plain,
c_HOL_Oord__class_Oless(A,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Oone__class_Oone(tc_nat),tc_nat)),A),tc_nat),
inference(paramod,[status(thm)],[c_462,c_14952]) ).
cnf(c_9190,plain,
~ c_HOL_Oord__class_Oless(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),c_COMBS(c_COMBI(A),B,C,D,E),F,V6,V7),V8),hAPP(V8,hAPP(B,V8)),tc_nat),
inference(paramod,[status(thm)],[c_612,c_4034]) ).
cnf(c_14919,plain,
~ c_HOL_Oord__class_Oless(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),c_COMBS(c_COMBI(A),c_COMBI(B),C,D,E),F,V6,V7),V8),hAPP(V8,V8),tc_nat),
inference(paramod,[status(thm)],[c_612,c_9190]) ).
cnf(c_14948,plain,
~ c_HOL_Oord__class_Oless(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),c_COMBS(c_COMBI(A),c_COMBI(B),C,D,E),F,V6,V7),hAPP(hAPP(c_COMBB(V8,V9,V10),V11),V12)),hAPP(V11,hAPP(V12,hAPP(hAPP(c_COMBB(V8,V9,V10),V11),V12))),tc_nat),
inference(paramod,[status(thm)],[c_687,c_14919]) ).
cnf(c_14949,plain,
$false,
inference(resolve,[status(thm)],[c_14948,c_6774]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV686-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 14:46:45 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 420730 was started by sandbox on n009,
% 0.09/0.37 % Sat Sep 26 14:46:45 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.40
% 0.09/0.40 % From the command line: assign(max_seconds, 300).
% 102.11/14.09
% 102.11/14.09 % given #500 (W,wt=20): 4558 c_HOL_Oord__class_Oless(A,c_Suc(v_n),tc_nat) | -c_HOL_Oord__class_Oless(c_Suc(A),v_i,tc_nat). [resolve(3758,b,835,b)].
% 102.11/14.09
% 102.11/14.09 % SZS status Unsatisfiable for theBenchmark
% 102.11/14.09
% 102.11/14.09 % Proof 1 at 4.74 (+ 0.80) seconds.
% 102.11/14.09 % Length of proof is 27.
% 102.11/14.09 % Level of proof is 8.
% 102.11/14.09 % Maximum clause weight is 77.000.
% 102.11/14.09 % Given clauses 853.
% 102.11/14.09
% 102.11/14.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------