%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ANA018-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n010.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 : Fri Sep 25 12:55:04 PM UTC 2026
% Result : Unsatisfiable 8.48s 1.82s
% Output : Proof 8.48s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t13,axiom,
sFlat0 = v_x(v_xa),
introduced(definition) ).
cnf(t73,plain,
v_x(v_xa) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sFlat1 = c_HOL_Oabs(v_x(v_xa),t_b),
introduced(definition) ).
cnf(t68,plain,
c_HOL_Oabs(v_x(v_xa),t_b) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t250,plain,
c_HOL_Oabs(sFlat0,t_b) = sFlat1,
inference(step,[status(thm)],[t68,t73]) ).
cnf(t75,plain,
c_HOL_Oabs(sFlat0,t_b) = sFlat1,
inference(rw,[status(thm)],[t250]) ).
cnf(t86,plain,
c_HOL_Oabs(sFlat0,t_b) = sFlat1,
inference(orient,[status(thm)],[t75]) ).
cnf(f5,axiom,
( c_times(c_times(V_a,V_b,T_a),V_c,T_a) = c_times(V_a,c_times(V_b,V_c,T_a),T_a)
| ~ class_OrderedGroup_Osemigroup__mult(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Omult__ac__1_0) ).
fof(f5_nnf,plain,
! [T_a,V_a,V_b,V_c] :
( c_times(c_times(V_a,V_b,T_a),V_c,T_a) = c_times(V_a,c_times(V_b,V_c,T_a),T_a)
| ~ class_OrderedGroup_Osemigroup__mult(T_a) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [T_a,V_a,V_b,V_c] :
( c_times(c_times(V_a,V_b,T_a),V_c,T_a) = c_times(V_a,c_times(V_b,V_c,T_a),T_a)
| ~ class_OrderedGroup_Osemigroup__mult(T_a) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( c_times(c_times(X1,X2,X0),X3,X0) = c_times(X1,c_times(X2,X3,X0),X0)
| ~ class_OrderedGroup_Osemigroup__mult(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t11,plain,
ifeq(class_OrderedGroup_Osemigroup__mult(X1),true,c_times(c_times(X2,X3,X1),X4,X1),c_times(X2,c_times(X3,X4,X1),X1)) = c_times(X2,c_times(X3,X4,X1),X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t46,plain,
ifeq(class_OrderedGroup_Osemigroup__mult(X1),true,c_times(c_times(X2,X3,X1),X4,X1),c_times(X2,c_times(X3,X4,X1),X1)) = c_times(X2,c_times(X3,X4,X1),X1),
inference(orient,[status(thm)],[t11]) ).
cnf(f10,axiom,
( class_OrderedGroup_Osemigroup__mult(T)
| ~ class_Ring__and__Field_Oordered__idom(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oordered__idom_21) ).
fof(f10_nnf,plain,
! [T] :
( class_OrderedGroup_Osemigroup__mult(T)
| ~ class_Ring__and__Field_Oordered__idom(T) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [T] :
( class_OrderedGroup_Osemigroup__mult(T)
| ~ class_Ring__and__Field_Oordered__idom(T) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( class_OrderedGroup_Osemigroup__mult(X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t5,plain,
ifeq(class_Ring__and__Field_Oordered__idom(X1),true,class_OrderedGroup_Osemigroup__mult(X1),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t22,plain,
ifeq(class_Ring__and__Field_Oordered__idom(X1),true,class_OrderedGroup_Osemigroup__mult(X1),true) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(f4,negated_conjecture,
class_Ring__and__Field_Oordered__idom(t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tfree_tcs) ).
fof(f4_nnf,plain,
class_Ring__and__Field_Oordered__idom(t_b),
inference(nnf_transformation,[status(thm)],[f4]) ).
cnf(c4,plain,
class_Ring__and__Field_Oordered__idom(t_b),
inference(cnf_transformation,[status(esa)],[f4_nnf]) ).
cnf(t0,plain,
class_Ring__and__Field_Oordered__idom(t_b) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t40,plain,
class_Ring__and__Field_Oordered__idom(t_b) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t43,plain,
true = ifeq(true,true,class_OrderedGroup_Osemigroup__mult(t_b),true),
inference(cp,[status(thm)],[t22,t40]) ).
cnf(t2,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t20,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t253,plain,
true = class_OrderedGroup_Osemigroup__mult(t_b),
inference(step,[status(thm)],[t43,t20]) ).
cnf(t80,plain,
class_OrderedGroup_Osemigroup__mult(t_b) = true,
inference(orient,[status(thm)],[t253]) ).
cnf(t81,plain,
c_times(X1,c_times(X2,X3,t_b),t_b) = ifeq(true,true,c_times(c_times(X1,X2,t_b),X3,t_b),c_times(X1,c_times(X2,X3,t_b),t_b)),
inference(cp,[status(thm)],[t46,t80]) ).
cnf(t265,plain,
c_times(X1,c_times(X2,X3,t_b),t_b) = c_times(c_times(X1,X2,t_b),X3,t_b),
inference(step,[status(thm)],[t81,t20]) ).
cnf(t108,plain,
c_times(c_times(X1,X2,t_b),X3,t_b) = c_times(X1,c_times(X2,X3,t_b),t_b),
inference(orient,[status(thm)],[t265]) ).
cnf(t15,axiom,
sFlat2 = c_times(v_ca,v_c,t_b),
introduced(definition) ).
cnf(t53,plain,
c_times(v_ca,v_c,t_b) = sFlat2,
inference(orient,[status(thm)],[t15]) ).
cnf(t109,plain,
c_times(v_ca,c_times(v_c,X1,t_b),t_b) = c_times(sFlat2,X1,t_b),
inference(cp,[status(thm)],[t108,t53]) ).
cnf(t112,plain,
c_times(v_ca,c_times(v_c,X1,t_b),t_b) = c_times(sFlat2,X1,t_b),
inference(orient,[status(thm)],[t109]) ).
cnf(t16,axiom,
sFlat3 = v_g(v_xa),
introduced(definition) ).
cnf(t70,plain,
v_g(v_xa) = sFlat3,
inference(orient,[status(thm)],[t16]) ).
cnf(t17,axiom,
sFlat4 = c_HOL_Oabs(v_g(v_xa),t_b),
introduced(definition) ).
cnf(t65,plain,
c_HOL_Oabs(v_g(v_xa),t_b) = sFlat4,
inference(orient,[status(thm)],[t17]) ).
cnf(t249,plain,
c_HOL_Oabs(sFlat3,t_b) = sFlat4,
inference(step,[status(thm)],[t65,t70]) ).
cnf(t72,plain,
c_HOL_Oabs(sFlat3,t_b) = sFlat4,
inference(rw,[status(thm)],[t249]) ).
cnf(t85,plain,
c_HOL_Oabs(sFlat3,t_b) = sFlat4,
inference(orient,[status(thm)],[t72]) ).
cnf(t18,axiom,
sFlat5 = c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b),
introduced(definition) ).
cnf(t47,plain,
c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b) = sFlat5,
inference(orient,[status(thm)],[t18]) ).
cnf(t246,plain,
c_times(sFlat2,c_HOL_Oabs(v_g(v_xa),t_b),t_b) = sFlat5,
inference(step,[status(thm)],[t47,t53]) ).
cnf(t58,plain,
c_times(sFlat2,c_HOL_Oabs(v_g(v_xa),t_b),t_b) = sFlat5,
inference(rw,[status(thm)],[t246]) ).
cnf(t255,plain,
c_times(sFlat2,c_HOL_Oabs(sFlat3,t_b),t_b) = sFlat5,
inference(step,[status(thm)],[t58,t70]) ).
cnf(t256,plain,
c_times(sFlat2,sFlat4,t_b) = sFlat5,
inference(step,[status(thm)],[t255,t85]) ).
cnf(t87,plain,
c_times(sFlat2,sFlat4,t_b) = sFlat5,
inference(orient,[status(thm)],[t256]) ).
cnf(t19,axiom,
sFlat6 = c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b),
introduced(definition) ).
cnf(t247,plain,
sFlat6 = c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(sFlat2,c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b),
inference(step,[status(thm)],[t19,t53]) ).
cnf(t59,plain,
c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(sFlat2,c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b) = sFlat6,
inference(orient,[status(thm)],[t247]) ).
cnf(t248,plain,
c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(sFlat2,sFlat4,t_b),t_b) = sFlat6,
inference(step,[status(thm)],[t59,t65]) ).
cnf(t67,plain,
c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(sFlat2,sFlat4,t_b),t_b) = sFlat6,
inference(rw,[status(thm)],[t248]) ).
cnf(t266,plain,
c_lessequals(c_HOL_Oabs(sFlat0,t_b),c_times(sFlat2,sFlat4,t_b),t_b) = sFlat6,
inference(step,[status(thm)],[t67,t73]) ).
cnf(t267,plain,
c_lessequals(sFlat1,c_times(sFlat2,sFlat4,t_b),t_b) = sFlat6,
inference(step,[status(thm)],[t266,t86]) ).
cnf(t268,plain,
c_lessequals(sFlat1,sFlat5,t_b) = sFlat6,
inference(step,[status(thm)],[t267,t87]) ).
cnf(t115,plain,
c_lessequals(sFlat1,sFlat5,t_b) = sFlat6,
inference(orient,[status(thm)],[t268]) ).
cnf(f6,axiom,
( c_lessequals(V_x,V_z,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_z,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Orderings_Oorder__class_Oorder__trans_0) ).
fof(f6_nnf,plain,
! [T_a,V_y,V_z,V_x] :
( c_lessequals(V_x,V_z,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_z,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [T_a,V_y,V_z,V_x] :
( c_lessequals(V_x,V_z,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_z,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( c_lessequals(X3,X2,X0)
| ~ c_lessequals(X3,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t10,plain,
ifeq(class_Orderings_Oorder(X1),true,ifeq(c_lessequals(X2,X3,X1),true,ifeq(c_lessequals(X4,X2,X1),true,c_lessequals(X4,X3,X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t24,plain,
ifeq(class_Orderings_Oorder(X1),true,ifeq(c_lessequals(X2,X3,X1),true,ifeq(c_lessequals(X4,X2,X1),true,c_lessequals(X4,X3,X1),true),true),true) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t119,plain,
true = ifeq(class_Orderings_Oorder(t_b),true,ifeq(c_lessequals(X1,sFlat5,t_b),true,ifeq(c_lessequals(sFlat1,X1,t_b),true,sFlat6,true),true),true),
inference(cp,[status(thm)],[t24,t115]) ).
cnf(f9,axiom,
( class_Orderings_Oorder(T)
| ~ class_LOrder_Ojoin__semilorder(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_LOrder_Ojoin__semilorder_1) ).
fof(f9_nnf,plain,
! [T] :
( class_Orderings_Oorder(T)
| ~ class_LOrder_Ojoin__semilorder(T) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [T] :
( class_Orderings_Oorder(T)
| ~ class_LOrder_Ojoin__semilorder(T) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( class_Orderings_Oorder(X0)
| ~ class_LOrder_Ojoin__semilorder(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t3,plain,
ifeq(class_LOrder_Ojoin__semilorder(X1),true,class_Orderings_Oorder(X1),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t26,plain,
ifeq(class_LOrder_Ojoin__semilorder(X1),true,class_Orderings_Oorder(X1),true) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(f11,axiom,
( class_LOrder_Ojoin__semilorder(T)
| ~ class_Ring__and__Field_Oordered__idom(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oordered__idom_35) ).
fof(f11_nnf,plain,
! [T] :
( class_LOrder_Ojoin__semilorder(T)
| ~ class_Ring__and__Field_Oordered__idom(T) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [T] :
( class_LOrder_Ojoin__semilorder(T)
| ~ class_Ring__and__Field_Oordered__idom(T) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( class_LOrder_Ojoin__semilorder(X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t4,plain,
ifeq(class_Ring__and__Field_Oordered__idom(X1),true,class_LOrder_Ojoin__semilorder(X1),true) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t21,plain,
ifeq(class_Ring__and__Field_Oordered__idom(X1),true,class_LOrder_Ojoin__semilorder(X1),true) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t41,plain,
true = ifeq(true,true,class_LOrder_Ojoin__semilorder(t_b),true),
inference(cp,[status(thm)],[t21,t40]) ).
cnf(t251,plain,
true = class_LOrder_Ojoin__semilorder(t_b),
inference(step,[status(thm)],[t41,t20]) ).
cnf(t76,plain,
class_LOrder_Ojoin__semilorder(t_b) = true,
inference(orient,[status(thm)],[t251]) ).
cnf(t77,plain,
true = ifeq(true,true,class_Orderings_Oorder(t_b),true),
inference(cp,[status(thm)],[t26,t76]) ).
cnf(t254,plain,
true = class_Orderings_Oorder(t_b),
inference(step,[status(thm)],[t77,t20]) ).
cnf(t82,plain,
class_Orderings_Oorder(t_b) = true,
inference(orient,[status(thm)],[t254]) ).
cnf(t286,plain,
true = ifeq(true,true,ifeq(c_lessequals(X1,sFlat5,t_b),true,ifeq(c_lessequals(sFlat1,X1,t_b),true,sFlat6,true),true),true),
inference(step,[status(thm)],[t119,t82]) ).
cnf(t287,plain,
true = ifeq(c_lessequals(X1,sFlat5,t_b),true,ifeq(c_lessequals(sFlat1,X1,t_b),true,sFlat6,true),true),
inference(step,[status(thm)],[t286,t20]) ).
cnf(t155,plain,
ifeq(c_lessequals(X1,sFlat5,t_b),true,ifeq(c_lessequals(sFlat1,X1,t_b),true,sFlat6,true),true) = true,
inference(orient,[status(thm)],[t287]) ).
cnf(f8,axiom,
( c_lessequals(c_times(V_c,V_a,T_a),c_times(V_c,V_b,T_a),T_a)
| ~ c_lessequals(c_0,V_c,T_a)
| ~ c_lessequals(V_a,V_b,T_a)
| ~ class_Ring__and__Field_Opordered__semiring(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Ring__and__Field_Opordered__semiring_h57e6052f6a1e05b1) ).
fof(f8_nnf,plain,
! [T_a,V_a,V_b,V_c] :
( c_lessequals(c_times(V_c,V_a,T_a),c_times(V_c,V_b,T_a),T_a)
| ~ c_lessequals(c_0,V_c,T_a)
| ~ c_lessequals(V_a,V_b,T_a)
| ~ class_Ring__and__Field_Opordered__semiring(T_a) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [T_a,V_a,V_b,V_c] :
( c_lessequals(c_times(V_c,V_a,T_a),c_times(V_c,V_b,T_a),T_a)
| ~ c_lessequals(c_0,V_c,T_a)
| ~ c_lessequals(V_a,V_b,T_a)
| ~ class_Ring__and__Field_Opordered__semiring(T_a) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( c_lessequals(c_times(X3,X1,X0),c_times(X3,X2,X0),X0)
| ~ c_lessequals(c_0,X3,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Ring__and__Field_Opordered__semiring(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t12,plain,
ifeq(class_Ring__and__Field_Opordered__semiring(X1),true,ifeq(c_lessequals(X2,X3,X1),true,ifeq(c_lessequals(c_0,X4,X1),true,c_lessequals(c_times(X4,X2,X1),c_times(X4,X3,X1),X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t27,plain,
ifeq(class_Ring__and__Field_Opordered__semiring(X1),true,ifeq(c_lessequals(X2,X3,X1),true,ifeq(c_lessequals(c_0,X4,X1),true,c_lessequals(c_times(X4,X2,X1),c_times(X4,X3,X1),X1),true),true),true) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(f7,axiom,
( c_lessequals(V_x,V_y,T_a)
| ~ c_less(V_x,V_y,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Orderings_Oorder__less__imp__le_0) ).
fof(f7_nnf,plain,
! [T_a,V_x,V_y] :
( c_lessequals(V_x,V_y,T_a)
| ~ c_less(V_x,V_y,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [T_a,V_x,V_y] :
( c_lessequals(V_x,V_y,T_a)
| ~ c_less(V_x,V_y,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( c_lessequals(X1,X2,X0)
| ~ c_less(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t9,plain,
ifeq(class_Orderings_Oorder(X1),true,ifeq(c_less(X2,X3,X1),true,c_lessequals(X2,X3,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t25,plain,
ifeq(class_Orderings_Oorder(X1),true,ifeq(c_less(X2,X3,X1),true,c_lessequals(X2,X3,X1),true),true) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(f1,negated_conjecture,
c_less(c_0,v_ca,t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f1_nnf,plain,
c_less(c_0,v_ca,t_b),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
c_less(c_0,v_ca,t_b),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(t1,plain,
c_less(c_0,v_ca,t_b) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t44,plain,
c_less(c_0,v_ca,t_b) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t45,plain,
true = ifeq(class_Orderings_Oorder(t_b),true,ifeq(true,true,c_lessequals(c_0,v_ca,t_b),true),true),
inference(cp,[status(thm)],[t25,t44]) ).
cnf(t262,plain,
true = ifeq(true,true,ifeq(true,true,c_lessequals(c_0,v_ca,t_b),true),true),
inference(step,[status(thm)],[t45,t82]) ).
cnf(t263,plain,
true = ifeq(true,true,c_lessequals(c_0,v_ca,t_b),true),
inference(step,[status(thm)],[t262,t20]) ).
cnf(t264,plain,
true = c_lessequals(c_0,v_ca,t_b),
inference(step,[status(thm)],[t263,t20]) ).
cnf(t102,plain,
c_lessequals(c_0,v_ca,t_b) = true,
inference(orient,[status(thm)],[t264]) ).
cnf(t107,plain,
true = ifeq(class_Ring__and__Field_Opordered__semiring(t_b),true,ifeq(c_lessequals(X1,X2,t_b),true,ifeq(true,true,c_lessequals(c_times(v_ca,X1,t_b),c_times(v_ca,X2,t_b),t_b),true),true),true),
inference(cp,[status(thm)],[t27,t102]) ).
cnf(f12,axiom,
( class_Ring__and__Field_Opordered__semiring(T)
| ~ class_Ring__and__Field_Oordered__idom(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oordered__idom_42) ).
fof(f12_nnf,plain,
! [T] :
( class_Ring__and__Field_Opordered__semiring(T)
| ~ class_Ring__and__Field_Oordered__idom(T) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [T] :
( class_Ring__and__Field_Opordered__semiring(T)
| ~ class_Ring__and__Field_Oordered__idom(T) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( class_Ring__and__Field_Opordered__semiring(X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t6,plain,
ifeq(class_Ring__and__Field_Oordered__idom(X1),true,class_Ring__and__Field_Opordered__semiring(X1),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t23,plain,
ifeq(class_Ring__and__Field_Oordered__idom(X1),true,class_Ring__and__Field_Opordered__semiring(X1),true) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t42,plain,
true = ifeq(true,true,class_Ring__and__Field_Opordered__semiring(t_b),true),
inference(cp,[status(thm)],[t23,t40]) ).
cnf(t252,plain,
true = class_Ring__and__Field_Opordered__semiring(t_b),
inference(step,[status(thm)],[t42,t20]) ).
cnf(t78,plain,
class_Ring__and__Field_Opordered__semiring(t_b) = true,
inference(orient,[status(thm)],[t252]) ).
cnf(t295,plain,
true = ifeq(true,true,ifeq(c_lessequals(X1,X2,t_b),true,ifeq(true,true,c_lessequals(c_times(v_ca,X1,t_b),c_times(v_ca,X2,t_b),t_b),true),true),true),
inference(step,[status(thm)],[t107,t78]) ).
cnf(t296,plain,
true = ifeq(c_lessequals(X1,X2,t_b),true,ifeq(true,true,c_lessequals(c_times(v_ca,X1,t_b),c_times(v_ca,X2,t_b),t_b),true),true),
inference(step,[status(thm)],[t295,t20]) ).
cnf(t297,plain,
true = ifeq(c_lessequals(X1,X2,t_b),true,c_lessequals(c_times(v_ca,X1,t_b),c_times(v_ca,X2,t_b),t_b),true),
inference(step,[status(thm)],[t296,t20]) ).
cnf(t171,plain,
ifeq(c_lessequals(X1,X2,t_b),true,c_lessequals(c_times(v_ca,X1,t_b),c_times(v_ca,X2,t_b),t_b),true) = true,
inference(orient,[status(thm)],[t297]) ).
cnf(f0,negated_conjecture,
c_lessequals(c_HOL_Oabs(v_f(V_U),t_b),c_times(v_c,c_HOL_Oabs(v_g(V_U),t_b),t_b),t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f0_nnf,plain,
! [V_U] : c_lessequals(c_HOL_Oabs(v_f(V_U),t_b),c_times(v_c,c_HOL_Oabs(v_g(V_U),t_b),t_b),t_b),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [V_U] : c_lessequals(c_HOL_Oabs(v_f(V_U),t_b),c_times(v_c,c_HOL_Oabs(v_g(V_U),t_b),t_b),t_b),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
c_lessequals(c_HOL_Oabs(v_f(X0),t_b),c_times(v_c,c_HOL_Oabs(v_g(X0),t_b),t_b),t_b),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t7,plain,
c_lessequals(c_HOL_Oabs(v_f(X1),t_b),c_times(v_c,c_HOL_Oabs(v_g(X1),t_b),t_b),t_b) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t34,plain,
c_lessequals(c_HOL_Oabs(v_f(X1),t_b),c_times(v_c,c_HOL_Oabs(v_g(X1),t_b),t_b),t_b) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t71,plain,
true = c_lessequals(c_HOL_Oabs(v_f(v_xa),t_b),c_times(v_c,c_HOL_Oabs(sFlat3,t_b),t_b),t_b),
inference(cp,[status(thm)],[t34,t70]) ).
cnf(t278,plain,
true = c_lessequals(c_HOL_Oabs(v_f(v_xa),t_b),c_times(v_c,sFlat4,t_b),t_b),
inference(step,[status(thm)],[t71,t85]) ).
cnf(t131,plain,
c_lessequals(c_HOL_Oabs(v_f(v_xa),t_b),c_times(v_c,sFlat4,t_b),t_b) = true,
inference(orient,[status(thm)],[t278]) ).
cnf(t177,plain,
true = ifeq(true,true,c_lessequals(c_times(v_ca,c_HOL_Oabs(v_f(v_xa),t_b),t_b),c_times(v_ca,c_times(v_c,sFlat4,t_b),t_b),t_b),true),
inference(cp,[status(thm)],[t171,t131]) ).
cnf(t298,plain,
true = c_lessequals(c_times(v_ca,c_HOL_Oabs(v_f(v_xa),t_b),t_b),c_times(v_ca,c_times(v_c,sFlat4,t_b),t_b),t_b),
inference(step,[status(thm)],[t177,t20]) ).
cnf(t299,plain,
true = c_lessequals(c_times(v_ca,c_HOL_Oabs(v_f(v_xa),t_b),t_b),c_times(sFlat2,sFlat4,t_b),t_b),
inference(step,[status(thm)],[t298,t112]) ).
cnf(t300,plain,
true = c_lessequals(c_times(v_ca,c_HOL_Oabs(v_f(v_xa),t_b),t_b),sFlat5,t_b),
inference(step,[status(thm)],[t299,t87]) ).
cnf(t182,plain,
c_lessequals(c_times(v_ca,c_HOL_Oabs(v_f(v_xa),t_b),t_b),sFlat5,t_b) = true,
inference(orient,[status(thm)],[t300]) ).
cnf(t186,plain,
true = ifeq(true,true,ifeq(c_lessequals(sFlat1,c_times(v_ca,c_HOL_Oabs(v_f(v_xa),t_b),t_b),t_b),true,sFlat6,true),true),
inference(cp,[status(thm)],[t155,t182]) ).
cnf(t303,plain,
true = ifeq(c_lessequals(sFlat1,c_times(v_ca,c_HOL_Oabs(v_f(v_xa),t_b),t_b),t_b),true,sFlat6,true),
inference(step,[status(thm)],[t186,t20]) ).
cnf(f2,negated_conjecture,
c_lessequals(c_HOL_Oabs(v_x(V_U),t_b),c_times(v_ca,c_HOL_Oabs(v_f(V_U),t_b),t_b),t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f2_nnf,plain,
! [V_U] : c_lessequals(c_HOL_Oabs(v_x(V_U),t_b),c_times(v_ca,c_HOL_Oabs(v_f(V_U),t_b),t_b),t_b),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [V_U] : c_lessequals(c_HOL_Oabs(v_x(V_U),t_b),c_times(v_ca,c_HOL_Oabs(v_f(V_U),t_b),t_b),t_b),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
c_lessequals(c_HOL_Oabs(v_x(X0),t_b),c_times(v_ca,c_HOL_Oabs(v_f(X0),t_b),t_b),t_b),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t8,plain,
c_lessequals(c_HOL_Oabs(v_x(X1),t_b),c_times(v_ca,c_HOL_Oabs(v_f(X1),t_b),t_b),t_b) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t28,plain,
c_lessequals(c_HOL_Oabs(v_x(X1),t_b),c_times(v_ca,c_HOL_Oabs(v_f(X1),t_b),t_b),t_b) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t74,plain,
true = c_lessequals(c_HOL_Oabs(sFlat0,t_b),c_times(v_ca,c_HOL_Oabs(v_f(v_xa),t_b),t_b),t_b),
inference(cp,[status(thm)],[t28,t73]) ).
cnf(t279,plain,
true = c_lessequals(sFlat1,c_times(v_ca,c_HOL_Oabs(v_f(v_xa),t_b),t_b),t_b),
inference(step,[status(thm)],[t74,t86]) ).
cnf(t138,plain,
c_lessequals(sFlat1,c_times(v_ca,c_HOL_Oabs(v_f(v_xa),t_b),t_b),t_b) = true,
inference(orient,[status(thm)],[t279]) ).
cnf(t304,plain,
true = ifeq(true,true,sFlat6,true),
inference(step,[status(thm)],[t303,t138]) ).
cnf(t305,plain,
true = sFlat6,
inference(step,[status(thm)],[t304,t20]) ).
cnf(t193,plain,
true = sFlat6,
inference(orient,[status(thm)],[t305]) ).
cnf(f3,negated_conjecture,
~ c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f3_nnf,plain,
~ c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
~ c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
~ c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(goal_0,negated_conjecture,
c_lessequals(c_HOL_Oabs(v_x(v_xa),t_b),c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b) != true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(g0_0,plain,
c_lessequals(c_HOL_Oabs(sFlat0,t_b),c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b) != true,
inference(rw,[status(thm)],[goal_0,t73]) ).
cnf(g0_1,plain,
c_lessequals(sFlat1,c_times(c_times(v_ca,v_c,t_b),c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b) != true,
inference(rw,[status(thm)],[g0_0,t86]) ).
cnf(g0_2,plain,
c_lessequals(sFlat1,c_times(v_ca,c_times(v_c,c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b),t_b) != true,
inference(rw,[status(thm)],[g0_1,t108]) ).
cnf(g0_3,plain,
c_lessequals(sFlat1,c_times(sFlat2,c_HOL_Oabs(v_g(v_xa),t_b),t_b),t_b) != true,
inference(rw,[status(thm)],[g0_2,t112]) ).
cnf(g0_4,plain,
c_lessequals(sFlat1,c_times(sFlat2,c_HOL_Oabs(sFlat3,t_b),t_b),t_b) != true,
inference(rw,[status(thm)],[g0_3,t70]) ).
cnf(g0_5,plain,
c_lessequals(sFlat1,c_times(sFlat2,sFlat4,t_b),t_b) != true,
inference(rw,[status(thm)],[g0_4,t85]) ).
cnf(g0_6,plain,
c_lessequals(sFlat1,sFlat5,t_b) != true,
inference(rw,[status(thm)],[g0_5,t87]) ).
cnf(g0_7,plain,
sFlat6 != true,
inference(rw,[status(thm)],[g0_6,t115]) ).
cnf(g0_8,plain,
sFlat6 != sFlat6,
inference(rw,[status(thm)],[g0_7,t193]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ANA018-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.14/0.41 % Computer : n010.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Fri Sep 25 05:46:29 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.48/1.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.48/1.82 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------