%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV821-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.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 03:14:06 PM UTC 2026
% Result : Unsatisfiable 60.60s 8.30s
% Output : Proof 60.60s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t63,axiom,
sF2 = hBOOL(hAPP(hAPP(v_P,v_x),v_xa)),
introduced(definition) ).
cnf(t61,axiom,
sF0 = hAPP(v_P,v_x),
introduced(definition) ).
cnf(t76,plain,
hAPP(v_P,v_x) = sF0,
inference(orient,[status(thm)],[t61]) ).
cnf(t373,plain,
sF2 = hBOOL(hAPP(sF0,v_xa)),
inference(step,[status(thm)],[t63,t76]) ).
cnf(t62,axiom,
sF1 = hAPP(hAPP(v_P,v_x),v_xa),
introduced(definition) ).
cnf(t367,plain,
sF1 = hAPP(sF0,v_xa),
inference(step,[status(thm)],[t62,t76]) ).
cnf(t95,plain,
hAPP(sF0,v_xa) = sF1,
inference(orient,[status(thm)],[t367]) ).
cnf(t374,plain,
sF2 = hBOOL(sF1),
inference(step,[status(thm)],[t373,t95]) ).
cnf(f1264,negated_conjecture,
hBOOL(hAPP(hAPP(v_P,v_x),v_xa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1264_nnf,plain,
hBOOL(hAPP(hAPP(v_P,v_x),v_xa)),
inference(nnf_transformation,[status(thm)],[f1264]) ).
cnf(c1264,plain,
hBOOL(hAPP(hAPP(v_P,v_x),v_xa)),
inference(cnf_transformation,[status(esa)],[f1264_nnf]) ).
cnf(t26,plain,
hBOOL(hAPP(hAPP(v_P,v_x),v_xa)) = true,
inference(equality_encoding,[status(esa)],[c1264]) ).
cnf(t369,plain,
hBOOL(hAPP(sF0,v_xa)) = true,
inference(step,[status(thm)],[t26,t76]) ).
cnf(t370,plain,
hBOOL(sF1) = true,
inference(step,[status(thm)],[t369,t95]) ).
cnf(t103,plain,
hBOOL(sF1) = true,
inference(orient,[status(thm)],[t370]) ).
cnf(t375,plain,
sF2 = true,
inference(step,[status(thm)],[t374,t103]) ).
cnf(t113,plain,
true = sF2,
inference(orient,[status(thm)],[t375]) ).
cnf(t66,axiom,
sF5 = hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)),
introduced(definition) ).
cnf(t64,axiom,
sF3 = hAPP(v_Q,v_x),
introduced(definition) ).
cnf(t77,plain,
hAPP(v_Q,v_x) = sF3,
inference(orient,[status(thm)],[t64]) ).
cnf(t384,plain,
sF5 = hBOOL(hAPP(sF3,v_xb)),
inference(step,[status(thm)],[t66,t77]) ).
cnf(t65,axiom,
sF4 = hAPP(hAPP(v_Q,v_x),v_xb),
introduced(definition) ).
cnf(t368,plain,
sF4 = hAPP(sF3,v_xb),
inference(step,[status(thm)],[t65,t77]) ).
cnf(t96,plain,
hAPP(sF3,v_xb) = sF4,
inference(orient,[status(thm)],[t368]) ).
cnf(t385,plain,
sF5 = hBOOL(sF4),
inference(step,[status(thm)],[t384,t96]) ).
cnf(f1266,negated_conjecture,
~ hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f1266_nnf,plain,
~ hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)),
inference(nnf_transformation,[status(thm)],[f1266]) ).
fof(f1266_sk,plain,
~ hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)),
inference(skolemisation,[status(esa)],[f1266_nnf]) ).
cnf(c1266,plain,
~ hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)),
inference(cnf_transformation,[status(esa)],[f1266_sk]) ).
cnf(t27,plain,
hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)) = false,
inference(equality_encoding,[status(esa)],[c1266]) ).
cnf(t371,plain,
hBOOL(hAPP(sF3,v_xb)) = false,
inference(step,[status(thm)],[t27,t77]) ).
cnf(t372,plain,
hBOOL(sF4) = false,
inference(step,[status(thm)],[t371,t96]) ).
cnf(t104,plain,
hBOOL(sF4) = false,
inference(orient,[status(thm)],[t372]) ).
cnf(t386,plain,
sF5 = false,
inference(step,[status(thm)],[t385,t104]) ).
cnf(t128,plain,
false = sF5,
inference(orient,[status(thm)],[t386]) ).
cnf(f1218,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f1218_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f1218]) ).
fof(f1218_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f1218_nnf]) ).
cnf(c1218,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f1218_sk]) ).
cnf(t18,plain,
eq(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(X1)) = false,
inference(equality_encoding,[status(esa)],[c1218]) ).
cnf(t68,axiom,
sF7 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition) ).
cnf(t72,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = sF7,
inference(orient,[status(thm)],[t68]) ).
cnf(t365,plain,
eq(sF7,c_Suc(X1)) = false,
inference(step,[status(thm)],[t18,t72]) ).
cnf(t92,plain,
eq(sF7,c_Suc(X1)) = false,
inference(orient,[status(thm)],[t365]) ).
cnf(t411,plain,
eq(sF7,c_Suc(X1)) = sF5,
inference(step,[status(thm)],[t92,t128]) ).
cnf(t153,plain,
eq(sF7,c_Suc(X1)) = sF5,
inference(orient,[status(thm)],[t411]) ).
cnf(f1250,axiom,
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(V_P),V_s,V_n,V_s1)
| V_n = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(V_P,V_n,V_s,V_s1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_evaln__elim__cases_I6_J_0) ).
fof(f1250_nnf,plain,
! [V_n,V_P,V_s,V_s1] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(V_P),V_s,V_n,V_s1)
| V_n = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(V_P,V_n,V_s,V_s1)) ),
inference(nnf_transformation,[status(thm)],[f1250]) ).
fof(f1250_sk,plain,
! [V_n,V_P,V_s,V_s1] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(V_P),V_s,V_n,V_s1)
| V_n = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(V_P,V_n,V_s,V_s1)) ),
inference(skolemisation,[status(esa)],[f1250_nnf]) ).
cnf(c1250,plain,
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X1),X2,X0,X3)
| X0 = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X0,X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f1250_sk]) ).
cnf(t58,plain,
ifeq(c_Natural_Oevaln(c_Com_Ocom_OBODY(X1),X2,X3,X4),true,X3,c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X3,X2,X4))) = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X3,X2,X4)),
inference(equality_encoding,[status(esa)],[c1250]) ).
cnf(t498,plain,
ifeq(c_Natural_Oevaln(c_Com_Ocom_OBODY(X1),X2,X3,X4),sF2,X3,c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X3,X2,X4))) = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X3,X2,X4)),
inference(step,[status(thm)],[t58,t113]) ).
cnf(t261,plain,
ifeq(c_Natural_Oevaln(c_Com_Ocom_OBODY(X1),X2,X3,X4),sF2,X3,c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X3,X2,X4))) = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X3,X2,X4)),
inference(orient,[status(thm)],[t498]) ).
cnf(t67,axiom,
sF6 = c_Com_Ocom_OBODY(v_pn),
introduced(definition) ).
cnf(t71,plain,
c_Com_Ocom_OBODY(v_pn) = sF6,
inference(orient,[status(thm)],[t67]) ).
cnf(t262,plain,
c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,X1,X2,X3)) = ifeq(c_Natural_Oevaln(sF6,X2,X1,X3),sF2,X1,c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,X1,X2,X3))),
inference(cp,[status(thm)],[t261,t71]) ).
cnf(t263,plain,
ifeq(c_Natural_Oevaln(sF6,X1,X2,X3),sF2,X2,c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,X2,X1,X3))) = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,X2,X1,X3)),
inference(orient,[status(thm)],[t262]) ).
cnf(f1265,negated_conjecture,
c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_HOL_Ozero__class_Ozero(tc_nat),v_xb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1265_nnf,plain,
c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_HOL_Ozero__class_Ozero(tc_nat),v_xb),
inference(nnf_transformation,[status(thm)],[f1265]) ).
cnf(c1265,plain,
c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_HOL_Ozero__class_Ozero(tc_nat),v_xb),
inference(cnf_transformation,[status(esa)],[f1265_nnf]) ).
cnf(t34,plain,
c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_HOL_Ozero__class_Ozero(tc_nat),v_xb) = true,
inference(equality_encoding,[status(esa)],[c1265]) ).
cnf(t437,plain,
c_Natural_Oevaln(sF6,v_xa,c_HOL_Ozero__class_Ozero(tc_nat),v_xb) = true,
inference(step,[status(thm)],[t34,t71]) ).
cnf(t438,plain,
c_Natural_Oevaln(sF6,v_xa,sF7,v_xb) = true,
inference(step,[status(thm)],[t437,t72]) ).
cnf(t439,plain,
c_Natural_Oevaln(sF6,v_xa,sF7,v_xb) = sF2,
inference(step,[status(thm)],[t438,t113]) ).
cnf(t179,plain,
c_Natural_Oevaln(sF6,v_xa,sF7,v_xb) = sF2,
inference(orient,[status(thm)],[t439]) ).
cnf(t264,plain,
c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,sF7,v_xa,v_xb)) = ifeq(sF2,sF2,sF7,c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,sF7,v_xa,v_xb))),
inference(cp,[status(thm)],[t263,t179]) ).
cnf(t22,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t94,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t22]) ).
cnf(t499,plain,
c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,sF7,v_xa,v_xb)) = sF7,
inference(step,[status(thm)],[t264,t94]) ).
cnf(t274,plain,
c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,sF7,v_xa,v_xb)) = sF7,
inference(orient,[status(thm)],[t499]) ).
cnf(t278,plain,
sF5 = eq(sF7,sF7),
inference(cp,[status(thm)],[t153,t274]) ).
cnf(t3,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t73,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t376,plain,
eq(X1,X1) = sF2,
inference(step,[status(thm)],[t73,t113]) ).
cnf(t114,plain,
eq(X1,X1) = sF2,
inference(orient,[status(thm)],[t376]) ).
cnf(t500,plain,
sF5 = sF2,
inference(step,[status(thm)],[t278,t114]) ).
cnf(t287,plain,
sF5 = sF2,
inference(orient,[status(thm)],[t500]) ).
cnf(t537,plain,
false = sF2,
inference(step,[status(thm)],[t128,t287]) ).
cnf(t324,plain,
false = sF2,
inference(orient,[status(thm)],[t537]) ).
cnf(f324,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__one__less__zero_0) ).
fof(f324_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f324]) ).
fof(f324_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f324_nnf]) ).
cnf(c324,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f324_sk]) ).
cnf(f331,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__sum__squares__lt__zero_0) ).
fof(f331_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f331]) ).
fof(f331_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f331_nnf]) ).
cnf(c331,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Otimes__class_Otimes(X2,X2,X0),X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f331_sk]) ).
cnf(f370,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f370_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f370]) ).
fof(f370_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f370_nnf]) ).
cnf(c370,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f370_sk]) ).
cnf(f372,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f372_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f372]) ).
fof(f372_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f372_nnf]) ).
cnf(c372,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f372_sk]) ).
cnf(f374,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f374_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f374]) ).
fof(f374_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f374_nnf]) ).
cnf(c374,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f374_sk]) ).
cnf(f376,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f376_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f376]) ).
fof(f376_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f376_nnf]) ).
cnf(c376,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f376_sk]) ).
cnf(f495,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f495_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f495]) ).
fof(f495_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f495_nnf]) ).
cnf(c495,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f495_sk]) ).
cnf(f496,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f496_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f496]) ).
fof(f496_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f496_nnf]) ).
cnf(c496,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f496_sk]) ).
cnf(f497,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f497_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f497]) ).
fof(f497_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f497_nnf]) ).
cnf(c497,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f497_sk]) ).
cnf(f498,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f498_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f498]) ).
fof(f498_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f498_nnf]) ).
cnf(c498,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f498_sk]) ).
cnf(f499,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f499_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f499]) ).
fof(f499_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f499_nnf]) ).
cnf(c499,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f499_sk]) ).
cnf(f516,axiom,
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__one__le__zero_0) ).
fof(f516_nnf,plain,
! [T_a] :
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f516]) ).
fof(f516_sk,plain,
! [T_a] :
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f516_nnf]) ).
cnf(c516,plain,
( ~ c_lessequals(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f516_sk]) ).
cnf(f605,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__square__less__zero_0) ).
fof(f605_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f605]) ).
fof(f605_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f605_nnf]) ).
cnf(c605,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f605_sk]) ).
cnf(f609,axiom,
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq__eq_1) ).
fof(f609_nnf,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f609]) ).
fof(f609_sk,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f609_nnf]) ).
cnf(c609,plain,
( ~ c_lessequals(c_Suc(X1),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f609_sk]) ).
cnf(f666,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_abs__not__less__zero_0) ).
fof(f666_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(nnf_transformation,[status(thm)],[f666]) ).
fof(f666_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(skolemisation,[status(esa)],[f666_nnf]) ).
cnf(c666,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(X0) ),
inference(cnf_transformation,[status(esa)],[f666_sk]) ).
cnf(f729,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I13_J_0) ).
fof(f729_nnf,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f729]) ).
fof(f729_sk,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f729_nnf]) ).
cnf(c729,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f729_sk]) ).
cnf(f753,axiom,
~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f753_nnf,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f753]) ).
fof(f753_sk,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f753_nnf]) ).
cnf(c753,plain,
~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f753_sk]) ).
cnf(f778,axiom,
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_of__nat__less__0__iff_0) ).
fof(f778_nnf,plain,
! [T_a,V_m] :
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f778]) ).
fof(f778_sk,plain,
! [T_a,V_m] :
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f778_nnf]) ).
cnf(c778,plain,
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f778_sk]) ).
cnf(f824,axiom,
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f824_nnf,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f824]) ).
fof(f824_sk,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f824_nnf]) ).
cnf(c824,plain,
( ~ c_HOL_Oord__class_Oless(X1,c_Suc(X0),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f824_sk]) ).
cnf(f877,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__add__less1_0) ).
fof(f877_nnf,plain,
! [V_i,V_j] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f877]) ).
fof(f877_sk,plain,
! [V_i,V_j] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f877_nnf]) ).
cnf(c877,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f877_sk]) ).
cnf(f878,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__add__less2_0) ).
fof(f878_nnf,plain,
! [V_j,V_i] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f878]) ).
fof(f878_sk,plain,
! [V_j,V_i] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f878_nnf]) ).
cnf(c878,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat),
inference(cnf_transformation,[status(esa)],[f878_sk]) ).
cnf(f903,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f903_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f903]) ).
fof(f903_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f903_nnf]) ).
cnf(c903,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f903_sk]) ).
cnf(f904,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f904_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f904]) ).
fof(f904_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f904_nnf]) ).
cnf(c904,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f904_sk]) ).
cnf(f906,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__less__abs__iff_0) ).
fof(f906_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(nnf_transformation,[status(thm)],[f906]) ).
fof(f906_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(skolemisation,[status(esa)],[f906_nnf]) ).
cnf(c906,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(X0),X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(X0) ),
inference(cnf_transformation,[status(esa)],[f906_sk]) ).
cnf(f980,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sum__squares__gt__zero__iff_0) ).
fof(f980_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f980]) ).
fof(f980_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f980_nnf]) ).
cnf(c980,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f980_sk]) ).
cnf(f1055,axiom,
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f1055_nnf,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f1055]) ).
fof(f1055_sk,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f1055_nnf]) ).
cnf(c1055,plain,
( c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f1055_sk]) ).
cnf(f1156,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I12_J_0) ).
fof(f1156_nnf,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f1156]) ).
fof(f1156_sk,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f1156_nnf]) ).
cnf(c1156,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f1156_sk]) ).
cnf(f1158,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f1158_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f1158]) ).
fof(f1158_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f1158_nnf]) ).
cnf(c1158,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f1158_sk]) ).
cnf(f1159,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f1159_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f1159]) ).
fof(f1159_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f1159_nnf]) ).
cnf(c1159,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f1159_sk]) ).
cnf(f1162,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f1162_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f1162]) ).
fof(f1162_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f1162_nnf]) ).
cnf(c1162,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f1162_sk]) ).
cnf(f1163,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f1163_nnf,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f1163]) ).
fof(f1163_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f1163_nnf]) ).
cnf(c1163,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f1163_sk]) ).
cnf(f1173,axiom,
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f1173_nnf,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f1173]) ).
fof(f1173_sk,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f1173_nnf]) ).
cnf(c1173,plain,
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f1173_sk]) ).
cnf(f1198,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
fof(f1198_nnf,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f1198]) ).
fof(f1198_sk,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f1198_nnf]) ).
cnf(c1198,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f1198_sk]) ).
cnf(f1200,axiom,
c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__neq__Zero_0) ).
fof(f1200_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f1200]) ).
fof(f1200_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f1200_nnf]) ).
cnf(c1200,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f1200_sk]) ).
cnf(f1201,axiom,
c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
fof(f1201_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f1201]) ).
fof(f1201_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f1201_nnf]) ).
cnf(c1201,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f1201_sk]) ).
cnf(f1219,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f1219_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f1219]) ).
fof(f1219_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f1219_nnf]) ).
cnf(c1219,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f1219_sk]) ).
cnf(f1224,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f1224_nnf,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f1224]) ).
fof(f1224_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f1224_nnf]) ).
cnf(c1224,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f1224_sk]) ).
cnf(f1225,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f1225_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f1225]) ).
fof(f1225_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f1225_nnf]) ).
cnf(c1225,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f1225_sk]) ).
cnf(f1251,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I19_J_0) ).
fof(f1251_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f1251]) ).
fof(f1251_sk,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f1251_nnf]) ).
cnf(c1251,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f1251_sk]) ).
cnf(f1252,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I49_J_0) ).
fof(f1252_nnf,plain,
! [V_pname_H,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f1252]) ).
fof(f1252_sk,plain,
! [V_pname_H,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f1252_nnf]) ).
cnf(c1252,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSemi(X1,X2),
inference(cnf_transformation,[status(esa)],[f1252_sk]) ).
cnf(f1253,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I48_J_0) ).
fof(f1253_nnf,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f1253]) ).
fof(f1253_sk,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f1253_nnf]) ).
cnf(c1253,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f1253_sk]) ).
cnf(f1254,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I18_J_0) ).
fof(f1254_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f1254]) ).
fof(f1254_sk,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f1254_nnf]) ).
cnf(c1254,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(X0),
inference(cnf_transformation,[status(esa)],[f1254_sk]) ).
cnf(f1258,axiom,
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_power__eq__0__iff_1) ).
fof(f1258_nnf,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f1258]) ).
fof(f1258_sk,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f1258_nnf]) ).
cnf(c1258,plain,
( c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Power_Opower(X0)
| ~ class_Ring__and__Field_Omult__zero(X0)
| ~ class_Ring__and__Field_Ono__zero__divisors(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f1258_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c324,c331,c370,c372,c374,c376,c495,c496,c497,c498,c499,c516,c605,c609,c666,c729,c753,c778,c824,c877,c878,c903,c904,c906,c980,c1055,c1156,c1158,c1159,c1162,c1163,c1173,c1198,c1200,c1201,c1218,c1219,c1224,c1225,c1251,c1252,c1253,c1254,c1258,c1266]) ).
cnf(g0_0,plain,
sF2 != false,
inference(rw,[status(thm)],[goal_0,t113]) ).
cnf(g0_1,plain,
sF2 != sF2,
inference(rw,[status(thm)],[g0_0,t324]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV821-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.18/0.44 % Computer : n013.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Thu Sep 24 21:06:36 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 60.60/8.30 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 60.60/8.30 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------