%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV904-1 : TPTP v8.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 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 : Mon Jun 24 16:48:52 EDT 2024 % Result : Unsatisfiable 0.49s 0.62s % Output : CNFRefutation 0.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SWV904-1 : TPTP v8.2.0. Released v4.1.0. % 0.06/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n026.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Thu Jun 20 18:51:09 EDT 2024 % 0.10/0.32 % CPUTime : % 0.49/0.58 start to proof:theBenchmark % 0.49/0.61 %------------------------------------------- % 0.49/0.61 % File :CSE---1.7 % 0.49/0.61 % Problem :theBenchmark % 0.49/0.61 % Transform :cnf % 0.49/0.61 % Format :tptp:raw % 0.49/0.61 % Command :java -jar mcs_scs.jar %d %s % 0.49/0.61 % 0.49/0.61 % Result :Theorem 0.000000s % 0.49/0.61 % Output :CNFRefutation 0.000000s % 0.49/0.61 %------------------------------------------- % 0.49/0.61 %------------------------------------------------------------------------------ % 0.49/0.61 % File : SWV904-1 : TPTP v8.2.0. Released v4.1.0. % 0.49/0.61 % Domain : Software Verification % 0.49/0.61 % Problem : Hoare logic with procedures 450_1 % 0.49/0.61 % Version : Especial. % 0.49/0.61 % English : Completeness is taken relative to completeness of the underlying % 0.49/0.61 % logic. Two versions of completeness proof: nested single recursion % 0.49/0.61 % and simultaneous recursion in call rule. % 0.49/0.61 % 0.49/0.61 % Refs : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.49/0.61 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.49/0.61 % Source : [Nip10] % 0.49/0.61 % Names : Hoare-450_1 [Nip10] % 0.49/0.61 % 0.49/0.61 % Status : Unsatisfiable % 0.49/0.61 % Rating : 0.00 v5.5.0, 0.05 v5.4.0, 0.10 v5.3.0, 0.06 v5.2.0, 0.00 v5.1.0, 0.06 v5.0.0, 0.07 v4.1.0 % 0.49/0.61 % Syntax : Number of clauses : 29 ( 15 unt; 2 nHn; 27 RR) % 0.49/0.61 % Number of literals : 45 ( 25 equ; 28 neg) % 0.49/0.61 % Maximal clause size : 3 ( 1 avg) % 0.49/0.61 % Maximal term depth : 3 ( 1 avg) % 0.49/0.61 % Number of predicates : 4 ( 3 usr; 2 prp; 0-2 aty) % 0.49/0.61 % Number of functors : 14 ( 14 usr; 7 con; 0-2 aty) % 0.49/0.61 % Number of variables : 46 ( 25 sgn) % 0.49/0.61 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.49/0.61 % 0.49/0.61 % Comments : % 0.49/0.61 %------------------------------------------------------------------------------ % 0.49/0.62 cnf(cls_option_Osimps_I2_J_0,axiom, % 0.49/0.62 c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_not__Some__eq_1,axiom, % 0.49/0.62 c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_option_Osimps_I3_J_0,axiom, % 0.49/0.62 c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_not__None__eq_1,axiom, % 0.49/0.62 c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_WT_OBody_0,axiom, % 0.49/0.62 ( c_Com_OWT(c_Com_Ocom_OBODY(V_pn)) % 0.49/0.62 | c_Com_Obody(V_pn) = c_Option_Ooption_ONone(tc_Com_Ocom) ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_com_Osimps_I19_J_0,axiom, % 0.49/0.62 c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP ). % 0.49/0.62 % 0.49/0.62 cnf(cls_com_Osimps_I49_J_0,axiom, % 0.49/0.62 c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_com_Osimps_I48_J_0,axiom, % 0.49/0.62 c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_com_Osimps_I6_J_0,axiom, % 0.49/0.62 ( c_Com_Ocom_OBODY(V_pname) != c_Com_Ocom_OBODY(V_pname_H) % 0.49/0.62 | V_pname = V_pname_H ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_com_Osimps_I18_J_0,axiom, % 0.49/0.62 c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_WTs__elim__cases_I7_J_0,axiom, % 0.49/0.62 ( c_Com_Obody(V_P) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(V_P),tc_Com_Ocom) % 0.49/0.62 | ~ c_Com_OWT(c_Com_Ocom_OBODY(V_P)) ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_com_Osimps_I3_J_1,axiom, % 0.49/0.62 ( c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H) % 0.49/0.62 | V_com2 = V_com2_H ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_com_Osimps_I3_J_0,axiom, % 0.49/0.62 ( c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H) % 0.49/0.62 | V_com1 = V_com1_H ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_option_Oinject_0,axiom, % 0.49/0.62 ( c_Option_Ooption_OSome(V_a,T_a) != c_Option_Ooption_OSome(V_a_H,T_a) % 0.49/0.62 | V_a = V_a_H ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_com_Osimps_I13_J_0,axiom, % 0.49/0.62 c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP ). % 0.49/0.62 % 0.49/0.62 cnf(cls_com_Osimps_I12_J_0,axiom, % 0.49/0.62 c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_WT__bodiesD_0,axiom, % 0.49/0.62 ( c_Com_Obody(V_pn) != c_Option_Ooption_OSome(V_b,tc_Com_Ocom) % 0.49/0.62 | ~ c_Com_OWT__bodies % 0.49/0.62 | c_Com_OWT(V_b) ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_WT_OSemi_0,axiom, % 0.49/0.62 ( c_Com_OWT(c_Com_Ocom_OSemi(V_c0,V_c1)) % 0.49/0.62 | ~ c_Com_OWT(V_c1) % 0.49/0.62 | ~ c_Com_OWT(V_c0) ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_WTs__elim__cases_I4_J_0,axiom, % 0.49/0.62 ( c_Com_OWT(V_c1) % 0.49/0.62 | ~ c_Com_OWT(c_Com_Ocom_OSemi(V_c1,V_c2)) ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_WTs__elim__cases_I4_J_1,axiom, % 0.49/0.62 ( c_Com_OWT(V_c2) % 0.49/0.62 | ~ c_Com_OWT(c_Com_Ocom_OSemi(V_c1,V_c2)) ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_state__not__singleton__def__raw_0,axiom, % 0.49/0.62 ( v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__raw__1 != v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__raw__2 % 0.49/0.62 | ~ c_Hoare__Mirabelle_Ostate__not__singleton ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_state__not__singleton__def_1,axiom, % 0.49/0.62 ( c_Hoare__Mirabelle_Ostate__not__singleton % 0.49/0.62 | V_x = V_xa ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_single__stateE_0,axiom, % 0.49/0.62 ( v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t) != V_t % 0.49/0.62 | ~ c_Hoare__Mirabelle_Ostate__not__singleton ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_WT_OSkip_0,axiom, % 0.49/0.62 c_Com_OWT(c_Com_Ocom_OSKIP) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_state__not__singleton__def_0,axiom, % 0.49/0.62 ( v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__1 != v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__2 % 0.49/0.62 | ~ c_Hoare__Mirabelle_Ostate__not__singleton ) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_conjecture_0,negated_conjecture, % 0.49/0.62 c_Hoare__Mirabelle_Ostate__not__singleton ). % 0.49/0.62 % 0.49/0.62 cnf(cls_conjecture_1,negated_conjecture, % 0.49/0.62 c_Com_OWT__bodies ). % 0.49/0.62 % 0.49/0.62 cnf(cls_conjecture_2,negated_conjecture, % 0.49/0.62 c_Com_OWT(v_c) ). % 0.49/0.62 % 0.49/0.62 cnf(cls_conjecture_3,negated_conjecture, % 0.49/0.62 ~ c_Hoare__Mirabelle_Ostate__not__singleton ). % 0.49/0.62 % 0.49/0.62 %------------------------------------------------------------------------------ % 0.49/0.62 %------------------------------------------- % 0.49/0.62 % Proof found % 0.49/0.62 % SZS status Theorem for theBenchmark % 0.49/0.62 % SZS output start Proof % 0.49/0.62 %ClaNum:44(EqnAxiom:15) % 0.49/0.62 %VarNum:52(SingletonVarNum:34) % 0.49/0.62 %MaxLitNum:3 % 0.49/0.62 %MaxfuncDepth:2 % 0.49/0.62 %SharedTerms:17 % 0.49/0.62 %goalClause: 16 17 19 20 % 0.49/0.62 %singleGoalClaCount:4 % 0.49/0.62 [16]P1(a5000) % 0.49/0.62 [17]P3(a5000) % 0.49/0.62 [18]P2(a1) % 0.49/0.62 [19]P2(a4) % 0.49/0.62 [20]~P3(a5000) % 0.49/0.62 [22]~E(f2(x221),a1) % 0.49/0.62 [24]~E(f5(x241,x242),a1) % 0.49/0.62 [29]~E(f6(x291,x292),f7(x292)) % 0.49/0.62 [27]~E(f2(x271),f5(x272,x273)) % 0.49/0.62 [30]~E(f5(x301,x302),f2(x303)) % 0.49/0.62 [36]E(f3(x361),f7(a9))+P2(f2(x361)) % 0.49/0.62 [38]~P2(f2(x381))+E(f6(f8(x381),a9),f3(x381)) % 0.49/0.62 [35]E(x351,x352)+~E(f2(x351),f2(x352)) % 0.49/0.62 [43]P2(x431)+~P2(f5(x432,x431)) % 0.49/0.62 [44]P2(x441)+~P2(f5(x441,x442)) % 0.49/0.62 [41]E(x411,x412)+~E(f6(x411,x413),f6(x412,x413)) % 0.49/0.62 [40]E(x401,x402)+~E(f5(x403,x401),f5(x404,x402)) % 0.49/0.62 [42]E(x421,x422)+~E(f5(x421,x423),f5(x422,x424)) % 0.49/0.62 [37]P2(x371)+~E(f3(x372),f6(x371,a9))+~P1(a5000) % 0.49/0.62 [39]~P2(x392)+~P2(x391)+P2(f5(x391,x392)) % 0.49/0.62 %EqnAxiom % 0.49/0.62 [1]E(x11,x11) % 0.49/0.62 [2]E(x22,x21)+~E(x21,x22) % 0.49/0.62 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.49/0.62 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.49/0.62 [5]~E(x51,x52)+E(f5(x51,x53),f5(x52,x53)) % 0.49/0.62 [6]~E(x61,x62)+E(f5(x63,x61),f5(x63,x62)) % 0.49/0.62 [7]~E(x71,x72)+E(f3(x71),f3(x72)) % 0.49/0.62 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83)) % 0.49/0.62 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92)) % 0.49/0.62 [10]~E(x101,x102)+E(f7(x101),f7(x102)) % 0.49/0.62 [11]~E(x111,x112)+E(f8(x111),f8(x112)) % 0.49/0.62 [12]~E(x121,x122)+E(f12(x121),f12(x122)) % 0.49/0.62 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 0.49/0.62 [14]~P3(x141)+P3(x142)+~E(x141,x142) % 0.49/0.62 [15]~P2(x151)+P2(x152)+~E(x151,x152) % 0.49/0.62 % 0.49/0.62 %------------------------------------------- % 0.49/0.62 cnf(49,plain, % 0.49/0.62 ($false), % 0.49/0.62 inference(scs_inference,[],[17,20]), % 0.49/0.62 ['proof']). % 0.49/0.62 % SZS output end Proof % 0.49/0.62 % Total time :0.000000s %------------------------------------------------------------------------------