%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV917-1 : TPTP v9.0.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n021.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 : Wed Apr 9 09:31:54 PM UTC 2025 % Result : Satisfiable 3.57s 1.96s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV917-1 : TPTP v9.0.0. Released v4.1.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.14/0.34 % Computer : n021.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Apr 9 04:56:59 EDT 2025 % 0.14/0.34 % CPUTime : % 3.57/1.96 % 3.57/1.96 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.57/1.96 % 3.57/1.96 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.57/1.96 %$ c_Option_Ois__none > tc_prod > tc_fun > hAPP > c_Option_Ooption_OSome > c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1 > c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1 > c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1 > c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1 > #nlpp > tc_Option_Ooption > tc_List_Olist > c_Option_Ooption_ONone > c_Objects_Onew__Addr > v_ha____ > v_a____ > tc_nat > tc_Value_Oval > tc_String_Ochar % 3.57/1.96 % 3.57/1.96 %Foreground sorts: % 3.57/1.96 % 3.57/1.96 % 3.57/1.96 %Background operators: % 3.57/1.96 % 3.57/1.96 % 3.57/1.96 %Foreground operators: % 3.57/1.96 tff(c_Objects_Onew__Addr, type, c_Objects_Onew__Addr: $i > $i). % 3.57/1.96 tff(c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1, type, c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1: ($i * $i) > $i). % 3.57/1.96 tff(c_Option_Ooption_OSome, type, c_Option_Ooption_OSome: ($i * $i) > $i). % 3.57/1.96 tff(v_ha____, type, v_ha____: $i). % 3.57/1.96 tff(tc_Option_Ooption, type, tc_Option_Ooption: $i > $i). % 3.57/1.96 tff(tc_prod, type, tc_prod: ($i * $i) > $i). % 3.57/1.96 tff(c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1, type, c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1: ($i * $i) > $i). % 3.57/1.96 tff(c_Option_Ois__none, type, c_Option_Ois__none: ($i * $i) > $o). % 3.57/1.96 tff(tc_List_Olist, type, tc_List_Olist: $i > $i). % 3.57/1.96 tff(tc_nat, type, tc_nat: $i). % 3.57/1.96 tff(tc_fun, type, tc_fun: ($i * $i) > $i). % 3.57/1.96 tff(hAPP, type, hAPP: ($i * $i) > $i). % 3.57/1.96 tff(c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1, type, c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1: ($i * $i) > $i). % 3.57/1.96 tff(tc_String_Ochar, type, tc_String_Ochar: $i). % 3.57/1.96 tff(v_a____, type, v_a____: $i). % 3.57/1.96 tff(tc_Value_Oval, type, tc_Value_Oval: $i). % 3.57/1.96 tff(c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1, type, c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1: ($i * $i) > $i). % 3.57/1.96 tff(c_Option_Ooption_ONone, type, c_Option_Ooption_ONone: $i > $i). % 3.57/1.96 % 3.57/1.96 %Saturated clause set: % 3.57/1.96 tff(c_756, plain, (c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(c_Objects_Onew__Addr(v_ha____), tc_nat)=v_a____)). % 3.57/1.97 tff(c_664, plain, (![V_a_H_7, T_a_36]: (c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(c_Option_Ooption_OSome(V_a_H_7, T_a_36), T_a_36)=V_a_H_7))). % 3.57/1.97 tff(c_154, plain, (![V_x_43, T_a_42, V_a_5]: (c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(V_x_43, T_a_42)=V_a_5 | c_Option_Ooption_OSome(V_a_5, T_a_42)!=V_x_43 | c_Option_Ooption_ONone(T_a_42)=V_x_43))). % 3.57/1.97 tff(c_79, plain, (![V_v_37, T_a_36, V_a_H_7]: (c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(V_v_37, T_a_36)=V_a_H_7 | c_Option_Ooption_OSome(V_a_H_7, T_a_36)!=V_v_37 | c_Option_Ooption_ONone(T_a_36)=V_v_37))). % 3.79/1.97 tff(c_486, plain, (![V_v_1, T_a_2]: (c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(V_v_1, T_a_2)=c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(V_v_1, T_a_2) | c_Option_Ooption_ONone(T_a_2)=V_v_1))). % 3.79/1.97 tff(c_389, plain, (![V_x_55, T_a_4]: (c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(V_x_55, T_a_4)=c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(V_x_55, T_a_4) | c_Option_Ooption_ONone(T_a_4)=V_x_55))). % 3.79/1.97 tff(c_393, plain, (![V_x_55, T_a_2]: (c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(V_x_55, T_a_2)=c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(V_x_55, T_a_2) | c_Option_Ooption_ONone(T_a_2)=V_x_55))). % 3.79/1.97 tff(c_248, plain, (![V_y_48, T_a_11]: (c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(V_y_48, T_a_11)=c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(V_y_48, T_a_11) | c_Option_Ooption_ONone(T_a_11)=V_y_48))). % 3.79/1.97 tff(c_249, plain, (![V_y_48, T_a_2]: (c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(V_y_48, T_a_2)=c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(V_y_48, T_a_2) | c_Option_Ooption_ONone(T_a_2)=V_y_48))). % 3.79/1.97 tff(c_348, plain, (![V_a_H_7, T_a_40]: (c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(c_Option_Ooption_OSome(V_a_H_7, T_a_40), T_a_40)=V_a_H_7))). % 3.79/1.97 tff(c_426, plain, (c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(c_Objects_Onew__Addr(v_ha____), tc_nat)=v_a____)). % 3.79/1.97 tff(c_377, plain, (![V_a_H_7, T_a_39]: (c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(c_Option_Ooption_OSome(V_a_H_7, T_a_39), T_a_39)=V_a_H_7))). % 3.79/1.97 tff(c_105, plain, (![V_x_38, T_a_39, V_a_H_7]: (c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(V_x_38, T_a_39)=V_a_H_7 | c_Option_Ooption_OSome(V_a_H_7, T_a_39)!=V_x_38 | c_Option_Ooption_ONone(T_a_39)=V_x_38))). % 3.79/1.97 tff(c_344, plain, (c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(c_Objects_Onew__Addr(v_ha____), tc_nat)=v_a____)). % 3.79/1.97 tff(c_245, plain, (![V_y_48, T_a_4]: (c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(V_y_48, T_a_4)=c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(V_y_48, T_a_4) | c_Option_Ooption_ONone(T_a_4)=V_y_48))). % 3.79/1.97 tff(c_282, plain, (c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(c_Objects_Onew__Addr(v_ha____), tc_nat)=v_a____)). % 3.79/1.97 tff(c_233, plain, (![V_a_H_7, T_a_40]: (c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(c_Option_Ooption_OSome(V_a_H_7, T_a_40), T_a_40)=V_a_H_7))). % 3.79/1.97 tff(c_131, plain, (![V_y_41, T_a_40, V_a_H_7]: (c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(V_y_41, T_a_40)=V_a_H_7 | c_Option_Ooption_OSome(V_a_H_7, T_a_40)!=V_y_41 | c_Option_Ooption_ONone(T_a_40)=V_y_41))). % 3.79/1.97 tff(c_73, plain, (![V_v_37]: (c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(V_v_37, tc_nat)=v_a____ | c_Objects_Onew__Addr(v_ha____)!=V_v_37 | c_Option_Ooption_ONone(tc_nat)=V_v_37))). % 3.79/1.97 tff(c_99, plain, (![V_x_38]: (c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(V_x_38, tc_nat)=v_a____ | c_Objects_Onew__Addr(v_ha____)!=V_x_38 | c_Option_Ooption_ONone(tc_nat)=V_x_38))). % 3.79/1.97 tff(c_151, plain, (![V_x_43]: (c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(V_x_43, tc_nat)=v_a____ | c_Objects_Onew__Addr(v_ha____)!=V_x_43 | c_Option_Ooption_ONone(tc_nat)=V_x_43))). % 3.79/1.97 tff(c_28, plain, (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____))). % 3.79/1.97 tff(c_125, plain, (![V_y_41]: (c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(V_y_41, tc_nat)=v_a____ | c_Objects_Onew__Addr(v_ha____)!=V_y_41 | c_Option_Ooption_ONone(tc_nat)=V_y_41))). % 3.79/1.97 tff(c_4, plain, (![T_a_4, V_x_3]: (c_Option_Ooption_ONone(T_a_4)=V_x_3 | c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(V_x_3, T_a_4), T_a_4)=V_x_3))). % 3.79/1.97 tff(c_12, plain, (![T_a_13, V_y_12]: (c_Option_Ooption_ONone(T_a_13)=V_y_12 | c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(V_y_12, T_a_13), T_a_13)=V_y_12))). % 3.79/1.97 tff(c_10, plain, (![V_x_10, T_a_11]: (c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(V_x_10, T_a_11), T_a_11)=V_x_10 | c_Option_Ooption_ONone(T_a_11)=V_x_10))). % 3.79/1.97 tff(c_2, plain, (![T_a_2, V_v_1]: (c_Option_Ooption_ONone(T_a_2)=V_v_1 | c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(V_v_1, T_a_2), T_a_2)=V_v_1))). % 3.79/1.97 tff(c_55, plain, (![V_a_33]: (v_a____=V_a_33 | c_Option_Ooption_OSome(V_a_33, tc_nat)!=c_Objects_Onew__Addr(v_ha____)))). % 3.79/1.97 tff(c_6, plain, (![V_a_H_7, V_a_5, T_a_6]: (V_a_H_7=V_a_5 | c_Option_Ooption_OSome(V_a_H_7, T_a_6)!=c_Option_Ooption_OSome(V_a_5, T_a_6)))). % 3.79/1.97 tff(c_41, plain, (c_Option_Ooption_ONone(tc_nat)!=c_Objects_Onew__Addr(v_ha____))). % 3.79/1.97 tff(c_24, plain, (![V_x_23, T_a_24]: (~c_Option_Ois__none(V_x_23, T_a_24) | c_Option_Ooption_ONone(T_a_24)=V_x_23))). % 3.79/1.97 tff(c_22, plain, (![V_a_H_22, T_a_21]: (c_Option_Ooption_OSome(V_a_H_22, T_a_21)!=c_Option_Ooption_ONone(T_a_21)))). % 3.79/1.97 tff(c_37, plain, (~c_Option_Ois__none(c_Objects_Onew__Addr(v_ha____), tc_nat))). % 3.79/1.97 tff(c_8, plain, (![V_x_8, T_a_9]: (~c_Option_Ois__none(c_Option_Ooption_OSome(V_x_8, T_a_9), T_a_9)))). % 3.79/1.97 tff(c_26, plain, (c_Option_Ooption_OSome(v_a____, tc_nat)=c_Objects_Onew__Addr(v_ha____))). % 3.79/1.97 tff(c_14, plain, (![T_a_14]: (c_Option_Ois__none(c_Option_Ooption_ONone(T_a_14), T_a_14)))). % 3.79/1.97 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.79/1.97 %------------------------------------------------------------------------------