%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : SWV918-10 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n027.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 : 600s % DateTime : Wed Jul 20 20:48:13 EDT 2022 % Result : Unknown 10.21s 10.23s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.13 % Problem : SWV918-10 : TPTP v8.1.0. Released v7.3.0. % 0.09/0.14 % Command : moca.sh %s % 0.14/0.35 % Computer : n027.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Thu Jun 16 00:19:35 EDT 2022 % 0.14/0.35 % CPUTime : % 10.21/10.23 % SZS status Satisfiable % 10.21/10.23 % SZS output start Proof % 10.21/10.23 The input problem is satisfiable because % 10.21/10.23 % 10.21/10.23 [1] the following set of Horn clauses is satisfiable: % 10.21/10.23 % 10.21/10.23 ifeq2(A, A, B, C) = B % 10.21/10.23 ifeq(A, A, B, C) = B % 10.21/10.23 c_COMBI(V_P, T_a) = V_P % 10.21/10.23 ifeq(c_Conform_Ohconf(V_P, V_h, T_a), true, c_Exceptions_Opreallocated(V_h), true) = true % 10.21/10.23 c_Conform_Ohconf(v_P, v_ha____, tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)), tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) = true % 10.21/10.23 c_COMBI(v_P, t_a) = v_P % 10.21/10.23 v_h_Ha____ = c_Fun_Ofun__upd(v_ha____, v_a____, c_Option_Ooption_OSome(c_Pair(v_C____, c_Objects_Oinit__fields(v_FDTs____), tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval))), tc_prod(tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval)))), tc_nat, tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval))))) % 10.21/10.23 c_Conform_Ooconf(v_P, v_ha____, c_Pair(v_C____, c_Objects_Oinit__fields(v_FDTs____), tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval))), tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)), tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) = true % 10.21/10.23 hAPP(v_ha____, v_a____) = c_Option_Ooption_ONone(tc_prod(tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval)))) % 10.21/10.23 c_Conform_Ohconf(v_P, v_h_Ha____, tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)), tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) = true ==> \bottom % 10.21/10.23 c_fequal(V_x, V_x, T_a) = true % 10.21/10.23 ifeq2(c_fequal(V_X, V_Y, T_a), true, V_X, V_Y) = V_Y % 10.21/10.23 % 10.21/10.23 This holds because % 10.21/10.23 % 10.21/10.23 [2] the following E does not entail the following G (Claessen-Smallbone's transformation (2018)): % 10.21/10.23 % 10.21/10.23 E: % 10.21/10.23 c_COMBI(V_P, T_a) = V_P % 10.21/10.23 c_COMBI(v_P, t_a) = v_P % 10.21/10.23 c_Conform_Ohconf(v_P, v_ha____, tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)), tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) = true % 10.21/10.23 c_Conform_Ooconf(v_P, v_ha____, c_Pair(v_C____, c_Objects_Oinit__fields(v_FDTs____), tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval))), tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)), tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) = true % 10.21/10.23 c_fequal(V_x, V_x, T_a) = true % 10.21/10.23 f1(c_Conform_Ohconf(v_P, v_h_Ha____, tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)), tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))) = false__ % 10.21/10.23 f1(true) = true__ % 10.21/10.23 hAPP(v_ha____, v_a____) = c_Option_Ooption_ONone(tc_prod(tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval)))) % 10.21/10.23 ifeq(A, A, B, C) = B % 10.21/10.23 ifeq(c_Conform_Ohconf(V_P, V_h, T_a), true, c_Exceptions_Opreallocated(V_h), true) = true % 10.21/10.23 ifeq2(A, A, B, C) = B % 10.21/10.23 ifeq2(c_fequal(V_X, V_Y, T_a), true, V_X, V_Y) = V_Y % 10.21/10.23 v_h_Ha____ = c_Fun_Ofun__upd(v_ha____, v_a____, c_Option_Ooption_OSome(c_Pair(v_C____, c_Objects_Oinit__fields(v_FDTs____), tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval))), tc_prod(tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval)))), tc_nat, tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval))))) % 10.21/10.23 G: % 10.21/10.23 true__ = false__ % 10.21/10.23 % 10.21/10.23 This holds because % 10.21/10.23 % 10.21/10.23 [3] the following ground-complete ordered TRS entails E but does not entail G: % 10.21/10.23 % 10.21/10.23 % 10.21/10.23 c_COMBI(V_P, T_a) -> V_P % 10.21/10.23 c_Conform_Ohconf(v_P, v_ha____, tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)), tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) -> c_Exceptions_Opreallocated(v_ha____) % 10.21/10.23 c_Conform_Ooconf(v_P, v_ha____, c_Pair(v_C____, c_Objects_Oinit__fields(v_FDTs____), tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval))), tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)), tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) -> c_Exceptions_Opreallocated(v_ha____) % 10.21/10.23 c_Fun_Ofun__upd(v_ha____, v_a____, c_Option_Ooption_OSome(c_Pair(v_C____, c_Objects_Oinit__fields(v_FDTs____), tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval))), tc_prod(tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval)))), tc_nat, tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval))))) -> v_h_Ha____ % 10.21/10.23 c_Option_Ooption_ONone(tc_prod(tc_List_Olist(tc_String_Ochar), tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar), tc_List_Olist(tc_String_Ochar)), tc_Option_Ooption(tc_Value_Oval)))) -> hAPP(v_ha____, v_a____) % 10.21/10.23 c_fequal(V_x, V_x, T_a) -> c_Exceptions_Opreallocated(v_ha____) % 10.21/10.23 f1(c_Conform_Ohconf(v_P, v_h_Ha____, tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)), tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))) -> false__ % 10.21/10.23 f1(c_Exceptions_Opreallocated(v_ha____)) -> true__ % 10.21/10.23 ifeq(A, A, B, C) -> B % 10.21/10.23 ifeq(c_Conform_Ohconf(Y0, Y1, Y2), c_Exceptions_Opreallocated(v_ha____), c_Exceptions_Opreallocated(Y1), c_Exceptions_Opreallocated(v_ha____)) -> c_Exceptions_Opreallocated(v_ha____) % 10.21/10.23 ifeq2(A, A, B, C) -> B % 10.21/10.23 ifeq2(c_fequal(Y0, Y1, Y2), c_Exceptions_Opreallocated(v_ha____), Y0, Y1) -> Y1 % 10.21/10.23 true -> c_Exceptions_Opreallocated(v_ha____) % 10.21/10.23 with the LPO induced by % 10.21/10.23 ifeq > c_Option_Ooption_OSome > v_h_Ha____ > tc_nat > t_a > c_Fun_Ofun__upd > f1 > c_fequal > c_Option_Ooption_ONone > hAPP > v_a____ > ifeq2 > c_Conform_Ohconf > true > c_Conform_Ooconf > c_Exceptions_Opreallocated > c_Pair > v_ha____ > tc_Option_Ooption > c_Objects_Oinit__fields > v_P > v_C____ > v_FDTs____ > tc_Value_Oval > c_COMBI > tc_Expr_Oexp > tc_List_Olist > tc_prod > tc_String_Ochar > tc_fun > false__ > true__ % 10.21/10.23 % 10.21/10.23 % SZS output end Proof % 10.21/10.23 %------------------------------------------------------------------------------