%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ANA007-1 : TPTP v9.3.1. Released v3.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 06:51:05 AM UTC 2026
% Result : Unsatisfiable 97.47s 14.07s
% Output : CNFRefutation 97.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 5
% Syntax : Number of formulae : 16 ( 9 unt; 0 def)
% Number of atoms : 23 ( 4 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 17 ( 10 ~; 7 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-3 aty)
% Number of variables : 16 ( 0 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_Ring__and__Field_Omult__cancel__right1_2,axiom,
! [VAR_0,VAR_1] :
( VAR_1 = c_times(c_1,VAR_1,VAR_0)
| ~ class_Ring__and__Field_Oordered__idom(VAR_0) ),
file('theBenchmark.p',cls_Ring__and__Field_Omult__cancel__right1_2) ).
cnf(c_2013,plain,
( B = c_times(c_1,B,A)
| ~ class_Ring__and__Field_Oordered__idom(A) ),
inference(clausify,[status(thm)],[cls_Ring__and__Field_Omult__cancel__right1_2]) ).
cnf(c_2014,plain,
( c_times(c_1,B,A) = B
| ~ class_Ring__and__Field_Oordered__idom(A) ),
inference(copy,[status(thm)],[c_2013]) ).
fof(cls_Orderings_Oorder__class_Oaxioms__1_0,axiom,
! [VAR_0,VAR_1] :
( c_lessequals(VAR_1,VAR_1,VAR_0)
| ~ class_Orderings_Oorder(VAR_0) ),
file('theBenchmark.p',cls_Orderings_Oorder__class_Oaxioms__1_0) ).
cnf(c_2432,plain,
( c_lessequals(B,B,A)
| ~ class_Orderings_Oorder(A) ),
inference(clausify,[status(thm)],[cls_Orderings_Oorder__class_Oaxioms__1_0]) ).
fof(clsrel_Ring__and__Field_Oordered__idom_44,axiom,
! [VAR_0] :
( class_Orderings_Oorder(VAR_0)
| ~ class_Ring__and__Field_Oordered__idom(VAR_0) ),
file('theBenchmark.p',clsrel_Ring__and__Field_Oordered__idom_44) ).
cnf(c_3032,plain,
( class_Orderings_Oorder(A)
| ~ class_Ring__and__Field_Oordered__idom(A) ),
inference(clausify,[status(thm)],[clsrel_Ring__and__Field_Oordered__idom_44]) ).
fof(cls_conjecture_0,axiom,
! [VAR_0] : ~ c_lessequals(c_HOL_Oabs(v_f(v_x(VAR_0)),t_b),c_times(VAR_0,c_HOL_Oabs(v_f(v_x(VAR_0)),t_b),t_b),t_b),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_3272,plain,
~ c_lessequals(c_HOL_Oabs(v_f(v_x(A)),t_b),c_times(A,c_HOL_Oabs(v_f(v_x(A)),t_b),t_b),t_b),
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
fof(tfree_tcs,axiom,
class_Ring__and__Field_Oordered__idom(t_b),
file('theBenchmark.p',tfree_tcs) ).
cnf(c_3273,plain,
class_Ring__and__Field_Oordered__idom(t_b),
inference(clausify,[status(thm)],[tfree_tcs]) ).
cnf(c_10189,plain,
class_Orderings_Oorder(t_b),
inference(resolve,[status(thm)],[c_3273,c_3032]) ).
cnf(c_10220,plain,
c_times(c_1,A,t_b) = A,
inference(resolve,[status(thm)],[c_3273,c_2014]) ).
cnf(c_11603,plain,
c_lessequals(A,A,t_b),
inference(resolve,[status(thm)],[c_10189,c_2432]) ).
cnf(c_18557,plain,
~ c_lessequals(c_HOL_Oabs(v_f(v_x(c_1)),t_b),c_HOL_Oabs(v_f(v_x(c_1)),t_b),t_b),
inference(paramod,[status(thm)],[c_10220,c_3272]) ).
cnf(c_18556,plain,
$false,
inference(resolve,[status(thm)],[c_11603,c_18557]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ANA007-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n008.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 22:04:09 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 457516 was started by sandbox2 on n008,
% 0.09/0.37 % Sat Sep 26 22:04:09 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.25/0.49
% 0.25/0.49 % From the command line: assign(max_seconds, 300).
% 97.47/14.07
% 97.47/14.07 % given #500 (I,wt=38): 868 -c_in(c_Pair(A,B,tc_List_Olist(C),tc_List_Olist(C)),c_List_Olex(D,C),tc_prod(tc_List_Olist(C),tc_List_Olist(C))) | c_in(c_Pair(c_List_Olist_OCons(E,A,C),c_List_Olist_OCons(E,B,C),tc_List_Olist(C),tc_List_Olist(C)),c_List_Olex(D,C),tc_prod(tc_List_Olist(C),tc_List_Olist(C))) # tptp_name(cls_List_OCons__in__lex_5) # clausal_fof(1). [assumption].
% 97.47/14.07
% 97.47/14.07 % given #1000 (I,wt=21): 1632 -class_Numeral_Onumber__ring(A) | -class_Ring__and__Field_Oordered__idom(A) | -c_IntDef_Oneg(c_Numeral_Onumber__of(c_Numeral_Obin__add(B,c_Numeral_Obin__mult(c_Numeral_OMin,C)),A),A) | -c_lessequals(c_Numeral_Onumber__of(C,A),c_Numeral_Onumber__of(B,A),A). [copy(1631),rewrite([1618(3)])].
% 97.47/14.07
% 97.47/14.07 % given #1500 (I,wt=8): 2307 -c_lessequals(A,c_emptyset,tc_set(B)) | c_emptyset = A. [copy(2306),flip(b)].
% 97.47/14.07
% 97.47/14.07 % given #2000 (I,wt=4): 2868 -class_Ring__and__Field_Ofield(A) | class_Ring__and__Field_Osemiring__0(A) # tptp_name(clsrel_Ring__and__Field_Ofield_19) # clausal_fof(1). [assumption].
% 97.47/14.07
% 97.47/14.07 % given #2500 (I,wt=8): 3372 c_times(c_1,A,B) = A | -class_Power_Orecpower(B). [resolve(128,a,109,b)].
% 97.47/14.07
% 97.47/14.07 % given #3000 (F,wt=14): 12677 c_minus(c_Datatype_Oo2s(c_Datatype_Ooption_OSome(c_0,tc_IntDef_Oint),tc_IntDef_Oint),c_uminus(c_IntDef_OInts,tc_set(tc_IntDef_Oint)),tc_set(tc_IntDef_Oint)) != c_emptyset. [para(448(a,1),12592(a,1,1))].
% 97.47/14.07
% 97.47/14.07 % given #3500 (T,wt=5): 13777 class_HOL_Oplus(tc_set(tc_set(tc_set(t_b)))). [resolve(12239,a,428,b)].
% 97.47/14.07
% 97.47/14.07 % SZS status Unsatisfiable for theBenchmark
% 97.47/14.07
% 97.47/14.07 % Proof 1 at 11.91 (+ 1.24) seconds.
% 97.47/14.07 % Length of proof is 10.
% 97.47/14.07 % Level of proof is 3.
% 97.47/14.07 % Maximum clause weight is 15.000.
% 97.47/14.07 % Given clauses 3805.
% 97.47/14.07
% 97.47/14.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------