%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV888-1 : TPTP v9.2.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:27:39 PM UTC 2026
% Result : Unsatisfiable 0.27s 1.63s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 78)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_evaln__elim__cases_I4_J_1,axiom,
( c_Natural_Oevaln(X1,c_Natural_Osko__Natural__Xevaln__elim__cases__4__1(X2,X1,X3,X4,X5),X3,X5)
| ~ c_Natural_Oevaln(c_Com_Ocom_OSemi(X2,X1),X4,X3,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln__elim__cases_I4_J_1) ).
cnf(cls_evaln__elim__cases_I4_J_0,axiom,
( c_Natural_Oevaln(X1,X2,X3,c_Natural_Osko__Natural__Xevaln__elim__cases__4__1(X1,X4,X3,X2,X5))
| ~ c_Natural_Oevaln(c_Com_Ocom_OSemi(X1,X4),X2,X3,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln__elim__cases_I4_J_0) ).
cnf(cls_evaln__elim__cases_I6_J_1,axiom,
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X3,X2,X4),X4)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X1),X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln__elim__cases_I6_J_1) ).
cnf(cls_evaln_OSemi_0,axiom,
( c_Natural_Oevaln(c_Com_Ocom_OSemi(X1,X2),X3,X4,X5)
| ~ c_Natural_Oevaln(X2,X6,X4,X5)
| ~ c_Natural_Oevaln(X1,X3,X4,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln_OSemi_0) ).
cnf(cls_evaln__elim__cases_I6_J_0,axiom,
( X1 = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X2,X1,X3,X4))
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X2),X3,X1,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln__elim__cases_I6_J_0) ).
cnf(cls_evaln_OBody_0,axiom,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(X1),X2,c_Suc(X3),X4)
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln_OBody_0) ).
cnf(cls_evalc__elim__cases_I4_J_1,axiom,
( c_Natural_Oevalc(X1,c_Natural_Osko__Natural__Xevalc__elim__cases__4__1(X2,X1,X3,X4),X4)
| ~ c_Natural_Oevalc(c_Com_Ocom_OSemi(X2,X1),X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evalc__elim__cases_I4_J_1) ).
cnf(cls_evalc__elim__cases_I4_J_0,axiom,
( c_Natural_Oevalc(X1,X2,c_Natural_Osko__Natural__Xevalc__elim__cases__4__1(X1,X3,X2,X4))
| ~ c_Natural_Oevalc(c_Com_Ocom_OSemi(X1,X3),X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evalc__elim__cases_I4_J_0) ).
cnf(cls_evaln__Suc_0,axiom,
( c_Natural_Oevaln(X1,X2,c_Suc(X3),X4)
| ~ c_Natural_Oevaln(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln__Suc_0) ).
cnf(cls_eval__eq_1,axiom,
( c_Natural_Oevalc(X1,X2,X3)
| ~ c_Natural_Oevaln(X1,X2,X4,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_eval__eq_1) ).
cnf(cls_evaln__evalc_0,axiom,
( c_Natural_Oevalc(X1,X2,X3)
| ~ c_Natural_Oevaln(X1,X2,X4,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln__evalc_0) ).
cnf(cls_evalc__evaln_0,axiom,
( c_Natural_Oevaln(X1,X2,c_Natural_Osko__Natural__Xevalc__evaln__1__1(X1,X2,X3),X3)
| ~ c_Natural_Oevalc(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evalc__evaln_0) ).
cnf(cls_eval__eq_0,axiom,
( c_Natural_Oevaln(X1,X2,c_Natural_Osko__Natural__Xeval__eq__1__1(X1,X2,X3),X3)
| ~ c_Natural_Oevalc(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_eval__eq_0) ).
cnf(cls_evaln__elim__cases_I1_J_0,axiom,
( X1 = X2
| ~ c_Natural_Oevaln(c_Com_Ocom_OSKIP,X2,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln__elim__cases_I1_J_0) ).
cnf(cls_evalc_OSemi_0,axiom,
( c_Natural_Oevalc(c_Com_Ocom_OSemi(X1,X2),X3,X4)
| ~ c_Natural_Oevalc(X2,X5,X4)
| ~ c_Natural_Oevalc(X1,X3,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evalc_OSemi_0) ).
cnf(cls_evaln_OSkip_0,axiom,
c_Natural_Oevaln(c_Com_Ocom_OSKIP,X1,X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evaln_OSkip_0) ).
cnf(cls_evalc_OBody_0,axiom,
( c_Natural_Oevalc(c_Com_Ocom_OBODY(X1),X2,X3)
| ~ c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evalc_OBody_0) ).
cnf(cls_evalc__elim__cases_I6_J_0,axiom,
( c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3)
| ~ c_Natural_Oevalc(c_Com_Ocom_OBODY(X1),X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evalc__elim__cases_I6_J_0) ).
cnf(cls_com__det_0,axiom,
( X1 = X2
| ~ c_Natural_Oevalc(X3,X4,X1)
| ~ c_Natural_Oevalc(X3,X4,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com__det_0) ).
cnf(cls_conjecture_1,negated_conjecture,
~ c_Natural_Oevalc(c_Com_Ocom_OBODY(v_pn),v_x,v_xa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(cls_evalc__elim__cases_I1_J_0,axiom,
( X1 = X2
| ~ c_Natural_Oevalc(c_Com_Ocom_OSKIP,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evalc__elim__cases_I1_J_0) ).
cnf(cls_conjecture_0,negated_conjecture,
c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_x,v_xa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(cls_evalc_OSkip_0,axiom,
c_Natural_Oevalc(c_Com_Ocom_OSKIP,X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evalc_OSkip_0) ).
cnf(cls_WTs__elim__cases_I4_J_0,axiom,
( c_Com_OWT(X1)
| ~ c_Com_OWT(c_Com_Ocom_OSemi(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WTs__elim__cases_I4_J_0) ).
cnf(cls_WTs__elim__cases_I4_J_1,axiom,
( c_Com_OWT(X1)
| ~ c_Com_OWT(c_Com_Ocom_OSemi(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WTs__elim__cases_I4_J_1) ).
cnf(cls_com_Osimps_I3_J_0,axiom,
( X1 = X3
| c_Com_Ocom_OSemi(X1,X2) != c_Com_Ocom_OSemi(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I3_J_0) ).
cnf(cls_option_Oinject_0,axiom,
( X1 = X3
| c_Option_Ooption_OSome(X1,X2) != c_Option_Ooption_OSome(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Oinject_0) ).
cnf(cls_com_Osimps_I3_J_1,axiom,
( X2 = X4
| c_Com_Ocom_OSemi(X1,X2) != c_Com_Ocom_OSemi(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I3_J_1) ).
cnf(cls_option_Oexhaust_0,axiom,
( X1 = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(X1,X2),X2)
| X1 = c_Option_Ooption_ONone(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Oexhaust_0) ).
cnf(cls_not__Some__eq_0,axiom,
( X1 = c_Option_Ooption_ONone(X2)
| X1 = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(X1,X2),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Some__eq_0) ).
cnf(cls_not__None__eq_0,axiom,
( X1 = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(X1,X2),X2)
| X1 = c_Option_Ooption_ONone(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__None__eq_0) ).
cnf(cls_option_Onchotomy_0,axiom,
( X1 = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(X1,X2),X2)
| X1 = c_Option_Ooption_ONone(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Onchotomy_0) ).
cnf(cls_WT_OSemi_0,axiom,
( c_Com_OWT(c_Com_Ocom_OSemi(X1,X2))
| ~ c_Com_OWT(X2)
| ~ c_Com_OWT(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WT_OSemi_0) ).
cnf(cls_the_Osimps_0,axiom,
c_Option_Othe(c_Option_Ooption_OSome(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_the_Osimps_0) ).
cnf(cls_WTs__elim__cases_I7_J_0,axiom,
( c_Com_Obody(X1) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(X1),tc_Com_Ocom)
| ~ c_Com_OWT(c_Com_Ocom_OBODY(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WTs__elim__cases_I7_J_0) ).
cnf(cls_WT__bodiesD_0,axiom,
( c_Com_OWT(X2)
| c_Com_Obody(X1) != c_Option_Ooption_OSome(X2,tc_Com_Ocom)
| ~ c_Com_OWT__bodies ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WT__bodiesD_0) ).
cnf(cls_com_Osimps_I48_J_0,axiom,
c_Com_Ocom_OSemi(X1,X2) != c_Com_Ocom_OBODY(X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I48_J_0) ).
cnf(cls_not__None__eq_1,axiom,
c_Option_Ooption_OSome(X1,X2) != c_Option_Ooption_ONone(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__None__eq_1) ).
cnf(cls_option_Osimps_I3_J_0,axiom,
c_Option_Ooption_OSome(X1,X2) != c_Option_Ooption_ONone(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Osimps_I3_J_0) ).
cnf(cls_com_Osimps_I49_J_0,axiom,
c_Com_Ocom_OBODY(X1) != c_Com_Ocom_OSemi(X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I49_J_0) ).
cnf(cls_not__Some__eq_1,axiom,
c_Option_Ooption_ONone(X1) != c_Option_Ooption_OSome(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Some__eq_1) ).
cnf(cls_option_Osimps_I2_J_0,axiom,
c_Option_Ooption_ONone(X1) != c_Option_Ooption_OSome(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Osimps_I2_J_0) ).
cnf(cls_com_Osimps_I13_J_0,axiom,
c_Com_Ocom_OSemi(X1,X2) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I13_J_0) ).
cnf(cls_com_Osimps_I12_J_0,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I12_J_0) ).
cnf(cls_WT_OBody_0,axiom,
( c_Com_OWT(c_Com_Ocom_OBODY(X1))
| c_Com_Obody(X1) = c_Option_Ooption_ONone(tc_Com_Ocom) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WT_OBody_0) ).
cnf(cls_com_Osimps_I6_J_0,axiom,
( X1 = X2
| c_Com_Ocom_OBODY(X1) != c_Com_Ocom_OBODY(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I6_J_0) ).
cnf(cls_nat_Oinject_0,axiom,
( X1 = X2
| c_Suc(X1) != c_Suc(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Oinject_0) ).
cnf(cls_Suc__inject_0,axiom,
( X1 = X2
| c_Suc(X1) != c_Suc(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__inject_0) ).
cnf(cls_Suc__n__not__n_0,axiom,
c_Suc(X1) != X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
cnf(cls_n__not__Suc__n_0,axiom,
X1 != c_Suc(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
cnf(cls_com_Osimps_I19_J_0,axiom,
c_Com_Ocom_OBODY(X1) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I19_J_0) ).
cnf(cls_com_Osimps_I18_J_0,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I18_J_0) ).
cnf(cls_WT_OSkip_0,axiom,
c_Com_OWT(c_Com_Ocom_OSKIP),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WT_OSkip_0) ).
cnf(i_0_53,axiom,
( c_Natural_Oevaln(X1,c_Natural_Osko__Natural__Xevaln__elim__cases__4__1(X2,X1,X3,X4,X5),X3,X5)
| ~ c_Natural_Oevaln(c_Com_Ocom_OSemi(X2,X1),X4,X3,X5) ),
cls_evaln__elim__cases_I4_J_1,
[final] ).
cnf(i_0_54,axiom,
( c_Natural_Oevaln(X1,X2,X3,c_Natural_Osko__Natural__Xevaln__elim__cases__4__1(X1,X4,X3,X2,X5))
| ~ c_Natural_Oevaln(c_Com_Ocom_OSemi(X1,X4),X2,X3,X5) ),
cls_evaln__elim__cases_I4_J_0,
[final] ).
cnf(i_0_55,axiom,
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X1,X3,X2,X4),X4)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X1),X2,X3,X4) ),
cls_evaln__elim__cases_I6_J_1,
[final] ).
cnf(i_0_56,axiom,
( c_Natural_Oevaln(c_Com_Ocom_OSemi(X1,X2),X3,X4,X5)
| ~ c_Natural_Oevaln(X2,X6,X4,X5)
| ~ c_Natural_Oevaln(X1,X3,X4,X6) ),
cls_evaln_OSemi_0,
[final] ).
cnf(i_0_57,axiom,
( X1 = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X2,X1,X3,X4))
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X2),X3,X1,X4) ),
cls_evaln__elim__cases_I6_J_0,
[final] ).
cnf(i_0_58,axiom,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(X1),X2,c_Suc(X3),X4)
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3,X4) ),
cls_evaln_OBody_0,
[final] ).
cnf(i_0_59,axiom,
( c_Natural_Oevalc(X1,c_Natural_Osko__Natural__Xevalc__elim__cases__4__1(X2,X1,X3,X4),X4)
| ~ c_Natural_Oevalc(c_Com_Ocom_OSemi(X2,X1),X3,X4) ),
cls_evalc__elim__cases_I4_J_1,
[final] ).
cnf(i_0_60,axiom,
( c_Natural_Oevalc(X1,X2,c_Natural_Osko__Natural__Xevalc__elim__cases__4__1(X1,X3,X2,X4))
| ~ c_Natural_Oevalc(c_Com_Ocom_OSemi(X1,X3),X2,X4) ),
cls_evalc__elim__cases_I4_J_0,
[final] ).
cnf(i_0_61,axiom,
( c_Natural_Oevaln(X1,X2,c_Suc(X3),X4)
| ~ c_Natural_Oevaln(X1,X2,X3,X4) ),
cls_evaln__Suc_0,
[final] ).
cnf(i_0_62,axiom,
( c_Natural_Oevalc(X1,X2,X3)
| ~ c_Natural_Oevaln(X1,X2,X4,X3) ),
cls_eval__eq_1,
[final] ).
cnf(i_0_63,axiom,
( c_Natural_Oevalc(X1,X2,X3)
| ~ c_Natural_Oevaln(X1,X2,X4,X3) ),
cls_evaln__evalc_0,
[final] ).
cnf(i_0_64,axiom,
( c_Natural_Oevaln(X1,X2,c_Natural_Osko__Natural__Xevalc__evaln__1__1(X1,X2,X3),X3)
| ~ c_Natural_Oevalc(X1,X2,X3) ),
cls_evalc__evaln_0,
[final] ).
cnf(i_0_65,axiom,
( c_Natural_Oevaln(X1,X2,c_Natural_Osko__Natural__Xeval__eq__1__1(X1,X2,X3),X3)
| ~ c_Natural_Oevalc(X1,X2,X3) ),
cls_eval__eq_0,
[final] ).
cnf(i_0_66,axiom,
( X1 = X2
| ~ c_Natural_Oevaln(c_Com_Ocom_OSKIP,X2,X3,X1) ),
cls_evaln__elim__cases_I1_J_0,
[final] ).
cnf(i_0_67,axiom,
( c_Natural_Oevalc(c_Com_Ocom_OSemi(X1,X2),X3,X4)
| ~ c_Natural_Oevalc(X2,X5,X4)
| ~ c_Natural_Oevalc(X1,X3,X5) ),
cls_evalc_OSemi_0,
[final] ).
cnf(i_0_68,axiom,
c_Natural_Oevaln(c_Com_Ocom_OSKIP,X1,X2,X1),
cls_evaln_OSkip_0,
[final] ).
cnf(i_0_69,axiom,
( c_Natural_Oevalc(c_Com_Ocom_OBODY(X1),X2,X3)
| ~ c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3) ),
cls_evalc_OBody_0,
[final] ).
cnf(i_0_70,axiom,
( c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom),X2,X3)
| ~ c_Natural_Oevalc(c_Com_Ocom_OBODY(X1),X2,X3) ),
cls_evalc__elim__cases_I6_J_0,
[final] ).
cnf(i_0_71,axiom,
( X1 = X2
| ~ c_Natural_Oevalc(X3,X4,X1)
| ~ c_Natural_Oevalc(X3,X4,X2) ),
cls_com__det_0,
[final] ).
cnf(i_0_72,negated_conjecture,
~ c_Natural_Oevalc(c_Com_Ocom_OBODY(v_pn),v_x,v_xa),
cls_conjecture_1,
[final] ).
cnf(i_0_73,axiom,
( X1 = X2
| ~ c_Natural_Oevalc(c_Com_Ocom_OSKIP,X2,X1) ),
cls_evalc__elim__cases_I1_J_0,
[final] ).
cnf(i_0_74,negated_conjecture,
c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_x,v_xa),
cls_conjecture_0,
[final] ).
cnf(i_0_75,axiom,
c_Natural_Oevalc(c_Com_Ocom_OSKIP,X1,X1),
cls_evalc_OSkip_0,
[final] ).
cnf(i_0_76,axiom,
( c_Com_OWT(X1)
| ~ c_Com_OWT(c_Com_Ocom_OSemi(X1,X2)) ),
cls_WTs__elim__cases_I4_J_0,
[final] ).
cnf(i_0_77,axiom,
( c_Com_OWT(X1)
| ~ c_Com_OWT(c_Com_Ocom_OSemi(X2,X1)) ),
cls_WTs__elim__cases_I4_J_1,
[final] ).
cnf(i_0_78,axiom,
( X1 = X3
| c_Com_Ocom_OSemi(X1,X2) != c_Com_Ocom_OSemi(X3,X4) ),
cls_com_Osimps_I3_J_0,
[final] ).
cnf(i_0_79,axiom,
( X1 = X3
| c_Option_Ooption_OSome(X1,X2) != c_Option_Ooption_OSome(X3,X2) ),
cls_option_Oinject_0,
[final] ).
cnf(i_0_80,axiom,
( X2 = X4
| c_Com_Ocom_OSemi(X1,X2) != c_Com_Ocom_OSemi(X3,X4) ),
cls_com_Osimps_I3_J_1,
[final] ).
cnf(i_0_81,axiom,
( X1 = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(X1,X2),X2)
| X1 = c_Option_Ooption_ONone(X2) ),
cls_option_Oexhaust_0,
[final] ).
cnf(i_0_82,axiom,
( X1 = c_Option_Ooption_ONone(X2)
| X1 = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(X1,X2),X2) ),
cls_not__Some__eq_0,
[final] ).
cnf(i_0_83,axiom,
( X1 = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(X1,X2),X2)
| X1 = c_Option_Ooption_ONone(X2) ),
cls_not__None__eq_0,
[final] ).
cnf(i_0_84,axiom,
( X1 = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(X1,X2),X2)
| X1 = c_Option_Ooption_ONone(X2) ),
cls_option_Onchotomy_0,
[final] ).
cnf(i_0_85,axiom,
( c_Com_OWT(c_Com_Ocom_OSemi(X1,X2))
| ~ c_Com_OWT(X2)
| ~ c_Com_OWT(X1) ),
cls_WT_OSemi_0,
[final] ).
cnf(i_0_86,axiom,
c_Option_Othe(c_Option_Ooption_OSome(X1,X2),X2) = X1,
cls_the_Osimps_0,
[final] ).
cnf(i_0_87,axiom,
( c_Com_Obody(X1) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(X1),tc_Com_Ocom)
| ~ c_Com_OWT(c_Com_Ocom_OBODY(X1)) ),
cls_WTs__elim__cases_I7_J_0,
[final] ).
cnf(i_0_88,axiom,
( c_Com_OWT(X2)
| c_Com_Obody(X1) != c_Option_Ooption_OSome(X2,tc_Com_Ocom)
| ~ c_Com_OWT__bodies ),
cls_WT__bodiesD_0,
[final] ).
cnf(i_0_89,axiom,
c_Com_Ocom_OSemi(X1,X2) != c_Com_Ocom_OBODY(X3),
cls_com_Osimps_I48_J_0,
[final] ).
cnf(i_0_90,axiom,
c_Option_Ooption_OSome(X1,X2) != c_Option_Ooption_ONone(X2),
cls_not__None__eq_1,
[final] ).
cnf(i_0_91,axiom,
c_Option_Ooption_OSome(X1,X2) != c_Option_Ooption_ONone(X2),
cls_option_Osimps_I3_J_0,
[final] ).
cnf(i_0_92,axiom,
c_Com_Ocom_OBODY(X1) != c_Com_Ocom_OSemi(X2,X3),
cls_com_Osimps_I49_J_0,
[final] ).
cnf(i_0_93,axiom,
c_Option_Ooption_ONone(X1) != c_Option_Ooption_OSome(X2,X1),
cls_not__Some__eq_1,
[final] ).
cnf(i_0_94,axiom,
c_Option_Ooption_ONone(X1) != c_Option_Ooption_OSome(X2,X1),
cls_option_Osimps_I2_J_0,
[final] ).
cnf(i_0_95,axiom,
c_Com_Ocom_OSemi(X1,X2) != c_Com_Ocom_OSKIP,
cls_com_Osimps_I13_J_0,
[final] ).
cnf(i_0_96,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X1,X2),
cls_com_Osimps_I12_J_0,
[final] ).
cnf(i_0_97,axiom,
( c_Com_OWT(c_Com_Ocom_OBODY(X1))
| c_Com_Obody(X1) = c_Option_Ooption_ONone(tc_Com_Ocom) ),
cls_WT_OBody_0,
[final] ).
cnf(i_0_98,axiom,
( X1 = X2
| c_Com_Ocom_OBODY(X1) != c_Com_Ocom_OBODY(X2) ),
cls_com_Osimps_I6_J_0,
[final] ).
cnf(i_0_99,axiom,
( X1 = X2
| c_Suc(X1) != c_Suc(X2) ),
cls_nat_Oinject_0,
[final] ).
cnf(i_0_100,axiom,
( X1 = X2
| c_Suc(X1) != c_Suc(X2) ),
cls_Suc__inject_0,
[final] ).
cnf(i_0_101,axiom,
c_Suc(X1) != X1,
cls_Suc__n__not__n_0,
[final] ).
cnf(i_0_102,axiom,
X1 != c_Suc(X1),
cls_n__not__Suc__n_0,
[final] ).
cnf(i_0_103,axiom,
c_Com_Ocom_OBODY(X1) != c_Com_Ocom_OSKIP,
cls_com_Osimps_I19_J_0,
[final] ).
cnf(i_0_104,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(X1),
cls_com_Osimps_I18_J_0,
[final] ).
cnf(i_0_105,axiom,
c_Com_OWT(c_Com_Ocom_OSKIP),
cls_WT_OSkip_0,
[final] ).
cnf(i_0_106,axiom,
X1 = X1 ).
cnf(i_0_107,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_108,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_109,axiom,
( X1 != X2
| c_Option_Ooption_OSome(X1,X3) = c_Option_Ooption_OSome(X2,X3) ) ).
cnf(i_0_110,axiom,
( X1 != X2
| c_Option_Ooption_OSome(X3,X1) = c_Option_Ooption_OSome(X3,X2) ) ).
cnf(i_0_111,axiom,
( X1 != X2
| c_Option_Ooption_ONone(X1) = c_Option_Ooption_ONone(X2) ) ).
cnf(i_0_112,axiom,
( X1 != X2
| c_Com_Ocom_OSemi(X1,X3) = c_Com_Ocom_OSemi(X2,X3) ) ).
cnf(i_0_113,axiom,
( X1 != X2
| c_Com_Ocom_OSemi(X3,X1) = c_Com_Ocom_OSemi(X3,X2) ) ).
cnf(i_0_114,axiom,
( X1 != X2
| c_Option_Othe(X1,X3) = c_Option_Othe(X2,X3) ) ).
cnf(i_0_115,axiom,
( X1 != X2
| c_Option_Othe(X3,X1) = c_Option_Othe(X3,X2) ) ).
cnf(i_0_116,axiom,
( X1 != X2
| c_Com_Obody(X1) = c_Com_Obody(X2) ) ).
cnf(i_0_117,axiom,
( X1 != X2
| c_Com_Ocom_OBODY(X1) = c_Com_Ocom_OBODY(X2) ) ).
cnf(i_0_118,axiom,
( X1 != X2
| c_Suc(X1) = c_Suc(X2) ) ).
cnf(i_0_119,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X1,X3,X4,X5)
| c_Natural_Oevaln(X2,X3,X4,X5) ) ).
cnf(i_0_120,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X1,X4,X5)
| c_Natural_Oevaln(X3,X2,X4,X5) ) ).
cnf(i_0_121,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X4,X1,X5)
| c_Natural_Oevaln(X3,X4,X2,X5) ) ).
cnf(i_0_122,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X4,X5,X1)
| c_Natural_Oevaln(X3,X4,X5,X2) ) ).
cnf(i_0_123,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X1,X3,X4)
| c_Natural_Oevalc(X2,X3,X4) ) ).
cnf(i_0_124,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X3,X1,X4)
| c_Natural_Oevalc(X3,X2,X4) ) ).
cnf(i_0_125,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X3,X4,X1)
| c_Natural_Oevalc(X3,X4,X2) ) ).
cnf(i_0_126,axiom,
( X1 != X2
| ~ c_Com_OWT(X1)
| c_Com_OWT(X2) ) ).
cnf(i_0_106_001,axiom,
X1 = X1 ).
cnf(i_0_107_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_108_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_109_004,axiom,
( X1 != X2
| c_Option_Ooption_OSome(X1,X3) = c_Option_Ooption_OSome(X2,X3) ) ).
cnf(i_0_110_005,axiom,
( X1 != X2
| c_Option_Ooption_OSome(X3,X1) = c_Option_Ooption_OSome(X3,X2) ) ).
cnf(i_0_111_006,axiom,
( X1 != X2
| c_Option_Ooption_ONone(X1) = c_Option_Ooption_ONone(X2) ) ).
cnf(i_0_112_007,axiom,
( X1 != X2
| c_Com_Ocom_OSemi(X1,X3) = c_Com_Ocom_OSemi(X2,X3) ) ).
cnf(i_0_113_008,axiom,
( X1 != X2
| c_Com_Ocom_OSemi(X3,X1) = c_Com_Ocom_OSemi(X3,X2) ) ).
cnf(i_0_114_009,axiom,
( X1 != X2
| c_Option_Othe(X1,X3) = c_Option_Othe(X2,X3) ) ).
cnf(i_0_115_010,axiom,
( X1 != X2
| c_Option_Othe(X3,X1) = c_Option_Othe(X3,X2) ) ).
cnf(i_0_116_011,axiom,
( X1 != X2
| c_Com_Obody(X1) = c_Com_Obody(X2) ) ).
cnf(i_0_117_012,axiom,
( X1 != X2
| c_Com_Ocom_OBODY(X1) = c_Com_Ocom_OBODY(X2) ) ).
cnf(i_0_118_013,axiom,
( X1 != X2
| c_Suc(X1) = c_Suc(X2) ) ).
cnf(i_0_119_014,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X1,X3,X4,X5)
| c_Natural_Oevaln(X2,X3,X4,X5) ) ).
cnf(i_0_120_015,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X1,X4,X5)
| c_Natural_Oevaln(X3,X2,X4,X5) ) ).
cnf(i_0_121_016,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X4,X1,X5)
| c_Natural_Oevaln(X3,X4,X2,X5) ) ).
cnf(i_0_122_017,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X4,X5,X1)
| c_Natural_Oevaln(X3,X4,X5,X2) ) ).
cnf(i_0_123_018,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X1,X3,X4)
| c_Natural_Oevalc(X2,X3,X4) ) ).
cnf(i_0_124_019,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X3,X1,X4)
| c_Natural_Oevalc(X3,X2,X4) ) ).
cnf(i_0_125_020,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X3,X4,X1)
| c_Natural_Oevalc(X3,X4,X2) ) ).
cnf(i_0_126_021,axiom,
( X1 != X2
| ~ c_Com_OWT(X1)
| c_Com_OWT(X2) ) ).
cnf(i_0_127,plain,
X1 = X1,
inference(equality_inference,[],[78]) ).
cnf(i_0_128,plain,
X1 = X1,
inference(equality_inference,[],[79]) ).
cnf(i_0_129,plain,
X1 = X1,
inference(equality_inference,[],[80]) ).
cnf(i_0_130,plain,
X1 = X1,
inference(equality_inference,[],[98]) ).
cnf(i_0_131,plain,
X1 = X1,
inference(equality_inference,[],[100]) ).
cnf(i_0_132,plain,
$false,
inference(scs_inference,[],[i_0_72,i_0_74,i_0_69]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.13 % Problem : SWV888-1 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.34 % Computer : n028.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 06:07:15 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 0.27/1.63 % Version : CSE_E---1.7
% 0.27/1.63 % Problem : theBenchmark.p
% 0.27/1.63 % SZS status Unsatisfiable for theBenchmark.p
% 0.27/1.63 % SZS output start CNFRefutation
% See solution above
% 0.27/1.65 % Total time : 1.276s
%------------------------------------------------------------------------------