%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV866-1 : TPTP v9.2.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n026.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:34 PM UTC 2026
% Result : Unsatisfiable 0.25s 1.62s
% Output : CNFRefutation 0.25s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 42)
% 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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cls_evaln__elim__cases_I4_J_0) ).
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/sandbox2/benchmark/theBenchmark.p',cls_evaln_OSemi_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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cls_evalc__elim__cases_I4_J_0) ).
cnf(cls_eval__eq_1,axiom,
( c_Natural_Oevalc(X1,X2,X3)
| ~ c_Natural_Oevaln(X1,X2,X4,X3) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cls_evaln_OSkip_0) ).
cnf(cls_com__det_0,axiom,
( X1 = X2
| ~ c_Natural_Oevalc(X3,X4,X1)
| ~ c_Natural_Oevalc(X3,X4,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com__det_0) ).
cnf(cls_evalc__elim__cases_I1_J_0,axiom,
( X1 = X2
| ~ c_Natural_Oevalc(c_Com_Ocom_OSKIP,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_evalc__elim__cases_I1_J_0) ).
cnf(cls_conjecture_2,negated_conjecture,
~ c_Natural_Oevalc(v_c,v_Z,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
cnf(cls_evalc_OSkip_0,axiom,
c_Natural_Oevalc(c_Com_Ocom_OSKIP,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_evalc_OSkip_0) ).
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/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I3_J_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/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I3_J_1) ).
cnf(cls_com_Osimps_I13_J_0,axiom,
c_Com_Ocom_OSemi(X1,X2) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I12_J_0) ).
cnf(cls_single__stateE_0,axiom,
( v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X1) != X1
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_single__stateE_0) ).
cnf(cls_state__not__singleton__def_1,axiom,
( c_Hoare__Mirabelle_Ostate__not__singleton
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_state__not__singleton__def_1) ).
cnf(cls_state__not__singleton__def_0,axiom,
( v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__1 != v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__2
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_state__not__singleton__def_0) ).
cnf(cls_state__not__singleton__def__raw_0,axiom,
( v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__raw__1 != v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__raw__2
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_state__not__singleton__def__raw_0) ).
cnf(cls_conjecture_1,negated_conjecture,
X1 = v_s_H,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(cls_conjecture_0,negated_conjecture,
c_Hoare__Mirabelle_Ostate__not__singleton,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(i_0_26,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_27,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_28,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_29,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_30,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_31,axiom,
( c_Natural_Oevalc(X1,X2,X3)
| ~ c_Natural_Oevaln(X1,X2,X4,X3) ),
cls_eval__eq_1,
[final] ).
cnf(i_0_32,axiom,
( c_Natural_Oevalc(X1,X2,X3)
| ~ c_Natural_Oevaln(X1,X2,X4,X3) ),
cls_evaln__evalc_0,
[final] ).
cnf(i_0_33,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_34,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_35,axiom,
( X1 = X2
| ~ c_Natural_Oevaln(c_Com_Ocom_OSKIP,X2,X3,X1) ),
cls_evaln__elim__cases_I1_J_0,
[final] ).
cnf(i_0_36,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_37,axiom,
c_Natural_Oevaln(c_Com_Ocom_OSKIP,X1,X2,X1),
cls_evaln_OSkip_0,
[final] ).
cnf(i_0_38,axiom,
( X1 = X2
| ~ c_Natural_Oevalc(X3,X4,X1)
| ~ c_Natural_Oevalc(X3,X4,X2) ),
cls_com__det_0,
[final] ).
cnf(i_0_39,axiom,
( X1 = X2
| ~ c_Natural_Oevalc(c_Com_Ocom_OSKIP,X2,X1) ),
cls_evalc__elim__cases_I1_J_0,
[final] ).
cnf(i_0_40,negated_conjecture,
~ c_Natural_Oevalc(v_c,v_Z,X1),
cls_conjecture_2,
[final] ).
cnf(i_0_41,axiom,
c_Natural_Oevalc(c_Com_Ocom_OSKIP,X1,X1),
cls_evalc_OSkip_0,
[final] ).
cnf(i_0_42,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_43,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_44,axiom,
c_Com_Ocom_OSemi(X1,X2) != c_Com_Ocom_OSKIP,
cls_com_Osimps_I13_J_0,
[final] ).
cnf(i_0_45,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X1,X2),
cls_com_Osimps_I12_J_0,
[final] ).
cnf(i_0_46,axiom,
( v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X1) != X1
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
cls_single__stateE_0,
[final] ).
cnf(i_0_47,axiom,
( c_Hoare__Mirabelle_Ostate__not__singleton
| X1 = X2 ),
cls_state__not__singleton__def_1,
[final] ).
cnf(i_0_48,axiom,
( v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__1 != v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__2
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
cls_state__not__singleton__def_0,
[final] ).
cnf(i_0_49,axiom,
( v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__raw__1 != v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__raw__2
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
cls_state__not__singleton__def__raw_0,
[final] ).
cnf(i_0_50,negated_conjecture,
X1 = v_s_H,
cls_conjecture_1,
[final] ).
cnf(i_0_51,negated_conjecture,
c_Hoare__Mirabelle_Ostate__not__singleton,
cls_conjecture_0,
[final] ).
cnf(i_0_52,axiom,
X1 = X1 ).
cnf(i_0_53,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_54,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_55,axiom,
( X1 != X2
| c_Com_Ocom_OSemi(X1,X3) = c_Com_Ocom_OSemi(X2,X3) ) ).
cnf(i_0_56,axiom,
( X1 != X2
| c_Com_Ocom_OSemi(X3,X1) = c_Com_Ocom_OSemi(X3,X2) ) ).
cnf(i_0_57,axiom,
( X1 != X2
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X1) = v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X2) ) ).
cnf(i_0_58,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X1,X3,X4,X5)
| c_Natural_Oevaln(X2,X3,X4,X5) ) ).
cnf(i_0_59,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X1,X4,X5)
| c_Natural_Oevaln(X3,X2,X4,X5) ) ).
cnf(i_0_60,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X4,X1,X5)
| c_Natural_Oevaln(X3,X4,X2,X5) ) ).
cnf(i_0_61,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X4,X5,X1)
| c_Natural_Oevaln(X3,X4,X5,X2) ) ).
cnf(i_0_62,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X1,X3,X4)
| c_Natural_Oevalc(X2,X3,X4) ) ).
cnf(i_0_63,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X3,X1,X4)
| c_Natural_Oevalc(X3,X2,X4) ) ).
cnf(i_0_64,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X3,X4,X1)
| c_Natural_Oevalc(X3,X4,X2) ) ).
cnf(i_0_52_001,axiom,
X1 = X1 ).
cnf(i_0_53_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_54_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_55_004,axiom,
( X1 != X2
| c_Com_Ocom_OSemi(X1,X3) = c_Com_Ocom_OSemi(X2,X3) ) ).
cnf(i_0_56_005,axiom,
( X1 != X2
| c_Com_Ocom_OSemi(X3,X1) = c_Com_Ocom_OSemi(X3,X2) ) ).
cnf(i_0_57_006,axiom,
( X1 != X2
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X1) = v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X2) ) ).
cnf(i_0_58_007,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X1,X3,X4,X5)
| c_Natural_Oevaln(X2,X3,X4,X5) ) ).
cnf(i_0_59_008,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X1,X4,X5)
| c_Natural_Oevaln(X3,X2,X4,X5) ) ).
cnf(i_0_60_009,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X4,X1,X5)
| c_Natural_Oevaln(X3,X4,X2,X5) ) ).
cnf(i_0_61_010,axiom,
( X1 != X2
| ~ c_Natural_Oevaln(X3,X4,X5,X1)
| c_Natural_Oevaln(X3,X4,X5,X2) ) ).
cnf(i_0_62_011,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X1,X3,X4)
| c_Natural_Oevalc(X2,X3,X4) ) ).
cnf(i_0_63_012,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X3,X1,X4)
| c_Natural_Oevalc(X3,X2,X4) ) ).
cnf(i_0_64_013,axiom,
( X1 != X2
| ~ c_Natural_Oevalc(X3,X4,X1)
| c_Natural_Oevalc(X3,X4,X2) ) ).
cnf(i_0_65,plain,
X1 = X1,
inference(equality_inference,[],[42]) ).
cnf(i_0_66,plain,
X1 = X1,
inference(equality_inference,[],[43]) ).
cnf(i_0_67,plain,
$false,
inference(scs_inference,[],[i_0_50,i_0_51,i_0_46]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV866-1 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n026.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 06:04:38 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 0.25/1.62 % Version : CSE_E---1.7
% 0.25/1.62 % Problem : theBenchmark.p
% 0.25/1.62 % SZS status Unsatisfiable for theBenchmark.p
% 0.25/1.62 % SZS output start CNFRefutation
% See solution above
% 0.25/1.63 % Total time : 1.273s
%------------------------------------------------------------------------------