%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV824-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 : n002.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:08 PM UTC 2026
% Result : Unsatisfiable 9.63s 2.04s
% Output : Proof 9.63s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t105,axiom,
sF0 = v_fun1(v_x,v_xa),
introduced(definition) ).
cnf(f670,negated_conjecture,
v_fun1(v_x,v_xa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f670_nnf,plain,
v_fun1(v_x,v_xa),
inference(nnf_transformation,[status(thm)],[f670]) ).
cnf(c670,plain,
v_fun1(v_x,v_xa),
inference(cnf_transformation,[status(esa)],[f670_nnf]) ).
cnf(t4,plain,
v_fun1(v_x,v_xa) = true,
inference(equality_encoding,[status(esa)],[c670]) ).
cnf(t117,plain,
v_fun1(v_x,v_xa) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t896,plain,
sF0 = true,
inference(step,[status(thm)],[t105,t117]) ).
cnf(t119,plain,
true = sF0,
inference(orient,[status(thm)],[t896]) ).
cnf(t106,axiom,
sF1 = v_fun2(v_x,v_xb),
introduced(definition) ).
cnf(f672,negated_conjecture,
~ v_fun2(v_x,v_xb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f672_nnf,plain,
~ v_fun2(v_x,v_xb),
inference(nnf_transformation,[status(thm)],[f672]) ).
fof(f672_sk,plain,
~ v_fun2(v_x,v_xb),
inference(skolemisation,[status(esa)],[f672_nnf]) ).
cnf(c672,plain,
~ v_fun2(v_x,v_xb),
inference(cnf_transformation,[status(esa)],[f672_sk]) ).
cnf(t5,plain,
v_fun2(v_x,v_xb) = false,
inference(equality_encoding,[status(esa)],[c672]) ).
cnf(t118,plain,
v_fun2(v_x,v_xb) = false,
inference(orient,[status(thm)],[t5]) ).
cnf(t901,plain,
sF1 = false,
inference(step,[status(thm)],[t106,t118]) ).
cnf(t124,plain,
false = sF1,
inference(orient,[status(thm)],[t901]) ).
cnf(f673,negated_conjecture,
( ~ v_fun1(V_Z,V_s)
| ~ c_Natural_Oevaln(v_com,V_s,c_Suc(v_n),V_s_H)
| v_fun2(V_Z,V_s_H) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f673_nnf,plain,
! [V_Z,V_s_H,V_s] :
( ~ v_fun1(V_Z,V_s)
| ~ c_Natural_Oevaln(v_com,V_s,c_Suc(v_n),V_s_H)
| v_fun2(V_Z,V_s_H) ),
inference(nnf_transformation,[status(thm)],[f673]) ).
fof(f673_sk,plain,
! [V_Z,V_s_H,V_s] :
( ~ v_fun1(V_Z,V_s)
| ~ c_Natural_Oevaln(v_com,V_s,c_Suc(v_n),V_s_H)
| v_fun2(V_Z,V_s_H) ),
inference(skolemisation,[status(esa)],[f673_nnf]) ).
cnf(c673,plain,
( ~ v_fun1(X0,X2)
| ~ c_Natural_Oevaln(v_com,X2,c_Suc(v_n),X1)
| v_fun2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f673_sk]) ).
cnf(t87,plain,
ifeq(c_Natural_Oevaln(v_com,X1,c_Suc(v_n),X2),true,ifeq(v_fun1(X3,X1),true,v_fun2(X3,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c673]) ).
cnf(t109,axiom,
sF4 = c_Suc(v_n),
introduced(definition) ).
cnf(t113,plain,
c_Suc(v_n) = sF4,
inference(orient,[status(thm)],[t109]) ).
cnf(t1139,plain,
ifeq(c_Natural_Oevaln(v_com,X1,sF4,X2),true,ifeq(v_fun1(X3,X1),true,v_fun2(X3,X2),true),true) = true,
inference(step,[status(thm)],[t87,t113]) ).
cnf(t110,axiom,
sF5(X1,X2) = c_Natural_Oevaln(v_com,X1,c_Suc(v_n),X2),
introduced(definition) ).
cnf(t939,plain,
sF5(X1,X2) = c_Natural_Oevaln(v_com,X1,sF4,X2),
inference(step,[status(thm)],[t110,t113]) ).
cnf(t178,plain,
c_Natural_Oevaln(v_com,X1,sF4,X2) = sF5(X1,X2),
inference(orient,[status(thm)],[t939]) ).
cnf(t1140,plain,
ifeq(sF5(X1,X2),true,ifeq(v_fun1(X3,X1),true,v_fun2(X3,X2),true),true) = true,
inference(step,[status(thm)],[t1139,t178]) ).
cnf(t1141,plain,
ifeq(sF5(X1,X2),sF0,ifeq(v_fun1(X3,X1),true,v_fun2(X3,X2),true),true) = true,
inference(step,[status(thm)],[t1140,t119]) ).
cnf(t1142,plain,
ifeq(sF5(X1,X2),sF0,ifeq(v_fun1(X3,X1),sF0,v_fun2(X3,X2),true),true) = true,
inference(step,[status(thm)],[t1141,t119]) ).
cnf(t1143,plain,
ifeq(sF5(X1,X2),sF0,ifeq(v_fun1(X3,X1),sF0,v_fun2(X3,X2),sF0),true) = true,
inference(step,[status(thm)],[t1142,t119]) ).
cnf(t111,axiom,
sF6(X1,X2,X3) = ifeq(v_fun1(X1,X2),true,v_fun2(X1,X3),true),
introduced(definition) ).
cnf(t971,plain,
sF6(X1,X2,X3) = ifeq(v_fun1(X1,X2),sF0,v_fun2(X1,X3),true),
inference(step,[status(thm)],[t111,t119]) ).
cnf(t972,plain,
sF6(X1,X2,X3) = ifeq(v_fun1(X1,X2),sF0,v_fun2(X1,X3),sF0),
inference(step,[status(thm)],[t971,t119]) ).
cnf(t233,plain,
ifeq(v_fun1(X1,X2),sF0,v_fun2(X1,X3),sF0) = sF6(X1,X2,X3),
inference(orient,[status(thm)],[t972]) ).
cnf(t1144,plain,
ifeq(sF5(X1,X2),sF0,sF6(X3,X1,X2),true) = true,
inference(step,[status(thm)],[t1143,t233]) ).
cnf(t1145,plain,
ifeq(sF5(X1,X2),sF0,sF6(X3,X1,X2),sF0) = true,
inference(step,[status(thm)],[t1144,t119]) ).
cnf(t1146,plain,
ifeq(sF5(X1,X2),sF0,sF6(X3,X1,X2),sF0) = sF0,
inference(step,[status(thm)],[t1145,t119]) ).
cnf(t775,plain,
ifeq(sF5(X1,X2),sF0,sF6(X3,X1,X2),sF0) = sF0,
inference(orient,[status(thm)],[t1146]) ).
cnf(f635,axiom,
( ~ c_Natural_Oevaln(V_c,V_s,V_n,V_s_H)
| c_Natural_Oevaln(V_c,V_s,c_Suc(V_n),V_s_H) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_evaln__Suc_0) ).
fof(f635_nnf,plain,
! [V_c,V_s,V_n,V_s_H] :
( ~ c_Natural_Oevaln(V_c,V_s,V_n,V_s_H)
| c_Natural_Oevaln(V_c,V_s,c_Suc(V_n),V_s_H) ),
inference(nnf_transformation,[status(thm)],[f635]) ).
fof(f635_sk,plain,
! [V_c,V_s,V_n,V_s_H] :
( ~ c_Natural_Oevaln(V_c,V_s,V_n,V_s_H)
| c_Natural_Oevaln(V_c,V_s,c_Suc(V_n),V_s_H) ),
inference(skolemisation,[status(esa)],[f635_nnf]) ).
cnf(c635,plain,
( ~ c_Natural_Oevaln(X0,X1,X2,X3)
| c_Natural_Oevaln(X0,X1,c_Suc(X2),X3) ),
inference(cnf_transformation,[status(esa)],[f635_sk]) ).
cnf(t78,plain,
ifeq(c_Natural_Oevaln(X1,X2,X3,X4),true,c_Natural_Oevaln(X1,X2,c_Suc(X3),X4),true) = true,
inference(equality_encoding,[status(esa)],[c635]) ).
cnf(t1044,plain,
ifeq(c_Natural_Oevaln(X1,X2,X3,X4),sF0,c_Natural_Oevaln(X1,X2,c_Suc(X3),X4),true) = true,
inference(step,[status(thm)],[t78,t119]) ).
cnf(t1045,plain,
ifeq(c_Natural_Oevaln(X1,X2,X3,X4),sF0,c_Natural_Oevaln(X1,X2,c_Suc(X3),X4),sF0) = true,
inference(step,[status(thm)],[t1044,t119]) ).
cnf(t1046,plain,
ifeq(c_Natural_Oevaln(X1,X2,X3,X4),sF0,c_Natural_Oevaln(X1,X2,c_Suc(X3),X4),sF0) = sF0,
inference(step,[status(thm)],[t1045,t119]) ).
cnf(t477,plain,
ifeq(c_Natural_Oevaln(X1,X2,X3,X4),sF0,c_Natural_Oevaln(X1,X2,c_Suc(X3),X4),sF0) = sF0,
inference(orient,[status(thm)],[t1046]) ).
cnf(f671,negated_conjecture,
c_Natural_Oevaln(v_com,v_xa,v_n,v_xb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f671_nnf,plain,
c_Natural_Oevaln(v_com,v_xa,v_n,v_xb),
inference(nnf_transformation,[status(thm)],[f671]) ).
cnf(c671,plain,
c_Natural_Oevaln(v_com,v_xa,v_n,v_xb),
inference(cnf_transformation,[status(esa)],[f671_nnf]) ).
cnf(t17,plain,
c_Natural_Oevaln(v_com,v_xa,v_n,v_xb) = true,
inference(equality_encoding,[status(esa)],[c671]) ).
cnf(t914,plain,
c_Natural_Oevaln(v_com,v_xa,v_n,v_xb) = sF0,
inference(step,[status(thm)],[t17,t119]) ).
cnf(t145,plain,
c_Natural_Oevaln(v_com,v_xa,v_n,v_xb) = sF0,
inference(orient,[status(thm)],[t914]) ).
cnf(t479,plain,
sF0 = ifeq(sF0,sF0,c_Natural_Oevaln(v_com,v_xa,c_Suc(v_n),v_xb),sF0),
inference(cp,[status(thm)],[t477,t145]) ).
cnf(t25,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t157,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t25]) ).
cnf(t1047,plain,
sF0 = c_Natural_Oevaln(v_com,v_xa,c_Suc(v_n),v_xb),
inference(step,[status(thm)],[t479,t157]) ).
cnf(t1048,plain,
sF0 = c_Natural_Oevaln(v_com,v_xa,sF4,v_xb),
inference(step,[status(thm)],[t1047,t113]) ).
cnf(t1049,plain,
sF0 = sF5(v_xa,v_xb),
inference(step,[status(thm)],[t1048,t178]) ).
cnf(t481,plain,
sF5(v_xa,v_xb) = sF0,
inference(orient,[status(thm)],[t1049]) ).
cnf(t777,plain,
sF0 = ifeq(sF0,sF0,sF6(X1,v_xa,v_xb),sF0),
inference(cp,[status(thm)],[t775,t481]) ).
cnf(t1147,plain,
sF0 = sF6(X1,v_xa,v_xb),
inference(step,[status(thm)],[t777,t157]) ).
cnf(t778,plain,
sF6(X1,v_xa,v_xb) = sF0,
inference(orient,[status(thm)],[t1147]) ).
cnf(t899,plain,
v_fun1(v_x,v_xa) = sF0,
inference(step,[status(thm)],[t117,t119]) ).
cnf(t122,plain,
v_fun1(v_x,v_xa) = sF0,
inference(orient,[status(thm)],[t899]) ).
cnf(t234,plain,
sF6(v_x,v_xa,X1) = ifeq(sF0,sF0,v_fun2(v_x,X1),sF0),
inference(cp,[status(thm)],[t233,t122]) ).
cnf(t973,plain,
sF6(v_x,v_xa,X1) = v_fun2(v_x,X1),
inference(step,[status(thm)],[t234,t157]) ).
cnf(t236,plain,
sF6(v_x,v_xa,X1) = v_fun2(v_x,X1),
inference(orient,[status(thm)],[t973]) ).
cnf(t779,plain,
sF0 = v_fun2(v_x,v_xb),
inference(cp,[status(thm)],[t778,t236]) ).
cnf(t904,plain,
v_fun2(v_x,v_xb) = sF1,
inference(step,[status(thm)],[t118,t124]) ).
cnf(t127,plain,
v_fun2(v_x,v_xb) = sF1,
inference(orient,[status(thm)],[t904]) ).
cnf(t1148,plain,
sF0 = sF1,
inference(step,[status(thm)],[t779,t127]) ).
cnf(t780,plain,
sF1 = sF0,
inference(orient,[status(thm)],[t1148]) ).
cnf(t1151,plain,
false = sF0,
inference(step,[status(thm)],[t124,t780]) ).
cnf(t783,plain,
false = sF0,
inference(orient,[status(thm)],[t1151]) ).
cnf(f84,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(f84_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)],[f84]) ).
fof(f84_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)],[f84_nnf]) ).
cnf(c84,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSemi(X1,X2),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(f116,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(f116_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)],[f116]) ).
fof(f116_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f116_nnf]) ).
cnf(c116,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f116_sk]) ).
cnf(f187,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(f187_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)],[f187]) ).
fof(f187_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)],[f187_nnf]) ).
cnf(c187,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)],[f187_sk]) ).
cnf(f217,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(f217_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)],[f217]) ).
fof(f217_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f217_nnf]) ).
cnf(c217,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f217_sk]) ).
cnf(f233,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(f233_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)],[f233]) ).
fof(f233_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)],[f233_nnf]) ).
cnf(c233,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f233_sk]) ).
cnf(f236,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(f236_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)],[f236]) ).
fof(f236_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)],[f236_nnf]) ).
cnf(c236,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(f238,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(f238_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)],[f238]) ).
fof(f238_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)],[f238_nnf]) ).
cnf(c238,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
cnf(f240,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(f240_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)],[f240]) ).
fof(f240_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)],[f240_nnf]) ).
cnf(c240,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f240_sk]) ).
cnf(f242,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(f242_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)],[f242]) ).
fof(f242_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)],[f242_nnf]) ).
cnf(c242,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f242_sk]) ).
cnf(f323,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(f323_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f323]) ).
fof(f323_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f323_nnf]) ).
cnf(c323,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f323_sk]) ).
cnf(f324,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(f324_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f324]) ).
fof(f324_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f324_nnf]) ).
cnf(c324,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f324_sk]) ).
cnf(f325,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(f325_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)],[f325]) ).
fof(f325_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)],[f325_nnf]) ).
cnf(c325,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f325_sk]) ).
cnf(f326,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(f326_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)],[f326]) ).
fof(f326_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)],[f326_nnf]) ).
cnf(c326,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f326_sk]) ).
cnf(f327,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(f327_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)],[f327]) ).
fof(f327_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)],[f327_nnf]) ).
cnf(c327,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f327_sk]) ).
cnf(f384,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(f384_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)],[f384]) ).
fof(f384_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)],[f384_nnf]) ).
cnf(c384,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f384_sk]) ).
cnf(f385,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(f385_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)],[f385]) ).
fof(f385_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)],[f385_nnf]) ).
cnf(c385,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)],[f385_sk]) ).
cnf(f404,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(f404_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)],[f404]) ).
fof(f404_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)],[f404_nnf]) ).
cnf(c404,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f404_sk]) ).
cnf(f405,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(f405_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)],[f405]) ).
fof(f405_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)],[f405_nnf]) ).
cnf(c405,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat),
inference(cnf_transformation,[status(esa)],[f405_sk]) ).
cnf(f420,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(f420_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)],[f420]) ).
fof(f420_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)],[f420_nnf]) ).
cnf(c420,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)],[f420_sk]) ).
cnf(f477,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(f477_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f477]) ).
fof(f477_sk,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f477_nnf]) ).
cnf(c477,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(X0),
inference(cnf_transformation,[status(esa)],[f477_sk]) ).
cnf(f500,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(f500_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)],[f500]) ).
fof(f500_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)],[f500_nnf]) ).
cnf(c500,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)],[f500_sk]) ).
cnf(f551,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(f551_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f551]) ).
fof(f551_sk,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f551_nnf]) ).
cnf(c551,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f551_sk]) ).
cnf(f610,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(f610_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)],[f610]) ).
fof(f610_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)],[f610_nnf]) ).
cnf(c610,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f610_sk]) ).
cnf(f611,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(f611_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)],[f611]) ).
fof(f611_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)],[f611_nnf]) ).
cnf(c611,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)],[f611_sk]) ).
cnf(f612,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(f612_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)],[f612]) ).
fof(f612_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)],[f612_nnf]) ).
cnf(c612,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)],[f612_sk]) ).
cnf(f615,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(f615_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)],[f615]) ).
fof(f615_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)],[f615_nnf]) ).
cnf(c615,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)],[f615_sk]) ).
cnf(f616,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(f616_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)],[f616]) ).
fof(f616_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)],[f616_nnf]) ).
cnf(c616,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)],[f616_sk]) ).
cnf(f624,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f624_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f624]) ).
fof(f624_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f624_nnf]) ).
cnf(c624,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f624_sk]) ).
cnf(f625,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f625_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f625]) ).
fof(f625_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f625_nnf]) ).
cnf(c625,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f625_sk]) ).
cnf(f626,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(f626_nnf,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f626]) ).
fof(f626_sk,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f626_nnf]) ).
cnf(c626,plain,
~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f626_sk]) ).
cnf(f632,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(f632_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f632]) ).
fof(f632_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f632_nnf]) ).
cnf(c632,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f632_sk]) ).
cnf(f633,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(f633_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f633]) ).
fof(f633_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f633_nnf]) ).
cnf(c633,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f633_sk]) ).
cnf(f645,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(f645_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f645]) ).
fof(f645_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f645_nnf]) ).
cnf(c645,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f645_sk]) ).
cnf(f646,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(f646_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f646]) ).
fof(f646_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f646_nnf]) ).
cnf(c646,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f646_sk]) ).
cnf(f654,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(f654_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)],[f654]) ).
fof(f654_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)],[f654_nnf]) ).
cnf(c654,plain,
( ~ c_lessequals(c_Suc(X1),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f654_sk]) ).
cnf(f662,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(f662_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)],[f662]) ).
fof(f662_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)],[f662_nnf]) ).
cnf(c662,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)],[f662_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c84,c116,c187,c217,c233,c236,c238,c240,c242,c323,c324,c325,c326,c327,c384,c385,c404,c405,c420,c477,c500,c551,c610,c611,c612,c615,c616,c624,c625,c626,c632,c633,c645,c646,c654,c662,c672]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t119]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t783]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV824-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.59 % Computer : n002.cluster.edu
% 0.12/0.59 % Model : x86_64 x86_64
% 0.12/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.59 % Memory : 8046.5625MB
% 0.12/0.59 % OS : Linux 6.8.0-71-generic
% 0.12/0.59 % CPULimit : 300
% 0.12/0.59 % WCLimit : 300
% 0.12/0.59 % DateTime : Thu Sep 24 21:10:06 UTC 2026
% 0.12/0.59 % CPUTime :
% 0.12/0.59 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 9.63/2.04 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.63/2.04 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------