%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV556-1.010 : TPTP v9.0.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n009.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:13 PM UTC 2025 % Result : Satisfiable 7.81s 2.85s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.01/0.13 % Problem : SWV556-1.010 : TPTP v9.0.0. Released v4.0.0. % 0.13/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.14/0.35 % Computer : n009.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.20/0.35 % CPULimit : 300 % 0.20/0.35 % WCLimit : 300 % 0.20/0.35 % DateTime : Wed Apr 9 04:02:11 EDT 2025 % 0.20/0.35 % CPUTime : % 7.81/2.85 % 7.81/2.85 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.81/2.85 % 7.81/2.85 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.81/2.86 %$ store > sk > select > #nlpp > i_83 > i9 > i8 > i7 > i6 > i5 > i4 > i3 > i2 > i10 > i1 > e_85 > e_84 > e_81 > e_79 > e_77 > e_75 > e_73 > e_71 > e_69 > e_67 > e_65 > e_63 > e_61 > e_59 > e_57 > e_55 > e_53 > e_51 > e_49 > e_47 > e_45 > e_43 > a_82 > a_80 > a_78 > a_76 > a_74 > a_72 > a_70 > a_68 > a_66 > a_64 > a_62 > a_60 > a_58 > a_56 > a_54 > a_52 > a_50 > a_48 > a_46 > a_44 > a2 > a1 % 7.81/2.86 % 7.81/2.86 %Foreground sorts: % 7.81/2.86 % 7.81/2.86 % 7.81/2.86 %Background operators: % 7.81/2.86 % 7.81/2.86 % 7.81/2.86 %Foreground operators: % 7.81/2.86 tff(a1, type, a1: $i). % 7.81/2.86 tff(a_54, type, a_54: $i). % 7.81/2.86 tff(a_56, type, a_56: $i). % 7.81/2.86 tff(e_73, type, e_73: $i). % 7.81/2.86 tff(a_52, type, a_52: $i). % 7.81/2.86 tff(a_46, type, a_46: $i). % 7.81/2.86 tff(e_63, type, e_63: $i). % 7.81/2.86 tff(e_79, type, e_79: $i). % 7.81/2.86 tff(a_78, type, a_78: $i). % 7.81/2.86 tff(a_76, type, a_76: $i). % 7.81/2.86 tff(e_81, type, e_81: $i). % 7.81/2.86 tff(a_80, type, a_80: $i). % 7.81/2.86 tff(store, type, store: ($i * $i * $i) > $i). % 7.81/2.86 tff(e_85, type, e_85: $i). % 7.81/2.86 tff(e_53, type, e_53: $i). % 7.81/2.86 tff(e_43, type, e_43: $i). % 7.81/2.86 tff(e_45, type, e_45: $i). % 7.81/2.86 tff(a_62, type, a_62: $i). % 7.81/2.86 tff(e_67, type, e_67: $i). % 7.81/2.86 tff(a_70, type, a_70: $i). % 7.81/2.86 tff(a_66, type, a_66: $i). % 7.81/2.86 tff(a_68, type, a_68: $i). % 7.81/2.86 tff(e_75, type, e_75: $i). % 7.81/2.86 tff(i_83, type, i_83: $i). % 7.81/2.86 tff(e_61, type, e_61: $i). % 7.81/2.86 tff(a_50, type, a_50: $i). % 7.81/2.86 tff(e_55, type, e_55: $i). % 7.81/2.86 tff(i10, type, i10: $i). % 7.81/2.86 tff(e_57, type, e_57: $i). % 7.81/2.86 tff(a2, type, a2: $i). % 7.81/2.86 tff(i8, type, i8: $i). % 7.81/2.86 tff(e_77, type, e_77: $i). % 7.81/2.86 tff(i9, type, i9: $i). % 7.81/2.86 tff(sk, type, sk: ($i * $i) > $i). % 7.81/2.86 tff(i7, type, i7: $i). % 7.81/2.86 tff(i1, type, i1: $i). % 7.81/2.86 tff(i2, type, i2: $i). % 7.81/2.86 tff(e_65, type, e_65: $i). % 7.81/2.86 tff(select, type, select: ($i * $i) > $i). % 7.81/2.86 tff(e_51, type, e_51: $i). % 7.81/2.86 tff(e_49, type, e_49: $i). % 7.81/2.86 tff(a_64, type, a_64: $i). % 7.81/2.86 tff(a_44, type, a_44: $i). % 7.81/2.86 tff(a_74, type, a_74: $i). % 7.81/2.86 tff(a_82, type, a_82: $i). % 7.81/2.86 tff(a_72, type, a_72: $i). % 7.81/2.86 tff(a_48, type, a_48: $i). % 7.81/2.86 tff(e_84, type, e_84: $i). % 7.81/2.86 tff(i5, type, i5: $i). % 7.81/2.86 tff(e_69, type, e_69: $i). % 7.81/2.86 tff(e_71, type, e_71: $i). % 7.81/2.86 tff(i4, type, i4: $i). % 7.81/2.86 tff(a_58, type, a_58: $i). % 7.81/2.86 tff(e_59, type, e_59: $i). % 7.81/2.86 tff(i3, type, i3: $i). % 7.81/2.86 tff(a_60, type, a_60: $i). % 7.81/2.86 tff(e_47, type, e_47: $i). % 7.81/2.86 tff(i6, type, i6: $i). % 7.81/2.86 % 7.81/2.86 %Saturated clause set: % 7.81/2.86 tff(c_4293, plain, (sk(a1, a2)=i1)). % 7.81/2.86 tff(c_4311, plain, (e_45!=e_43)). % 7.81/2.86 tff(c_4297, plain, (e_85=e_43)). % 7.81/2.86 tff(c_4296, plain, (e_84=e_45)). % 7.81/2.86 tff(c_4292, plain, (i_83=i1)). % 7.81/2.86 tff(c_4219, plain, (![J_96]: (select(a2, J_96)=select(a1, J_96) | i1=J_96 | i1=J_96 | i1=J_96 | i1=J_96 | i1=J_96 | i1=J_96 | i10=J_96 | i1=J_96 | i10=J_96 | i10=J_96 | i1=J_96 | i1=J_96 | i1=J_96 | i1=J_96 | i1=J_96 | i1=J_96 | i1=J_96 | i1=J_96 | i1=J_96 | i1=J_96))). % 7.81/2.86 tff(c_4192, plain, (![J_14]: (select(a_44, J_14)=select(a2, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i10=J_14 | i1=J_14 | i10=J_14 | i10=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 7.81/2.86 tff(c_4153, plain, (![J_14]: (select(a_46, J_14)=select(a_44, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i10=J_14 | i1=J_14 | i10=J_14 | i10=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 7.81/2.86 tff(c_4102, plain, (![J_93]: (select(a_48, J_93)=select(a_46, J_93) | i1=J_93 | i1=J_93 | i1=J_93 | i1=J_93 | i1=J_93 | i10=J_93 | i1=J_93 | i10=J_93 | i10=J_93 | i1=J_93 | i1=J_93 | i1=J_93 | i1=J_93 | i1=J_93 | i1=J_93 | i1=J_93 | i1=J_93))). % 7.81/2.86 tff(c_4075, plain, (![J_14]: (select(a_50, J_14)=select(a_48, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i10=J_14 | i1=J_14 | i10=J_14 | i10=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 7.81/2.86 tff(c_4036, plain, (![J_14]: (select(a_52, J_14)=select(a_50, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i10=J_14 | i1=J_14 | i10=J_14 | i10=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 7.81/2.86 tff(c_3985, plain, (![J_90]: (select(a_54, J_90)=select(a_52, J_90) | i1=J_90 | i1=J_90 | i1=J_90 | i1=J_90 | i10=J_90 | i1=J_90 | i10=J_90 | i10=J_90 | i1=J_90 | i1=J_90 | i1=J_90 | i1=J_90 | i1=J_90 | i1=J_90))). % 7.81/2.86 tff(c_3958, plain, (![J_14]: (select(a_56, J_14)=select(a_54, J_14) | i1=J_14 | i1=J_14 | i1=J_14 | i10=J_14 | i1=J_14 | i10=J_14 | i10=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 7.81/2.86 tff(c_3907, plain, (![J_88]: (select(a_58, J_88)=select(a_56, J_88) | i1=J_88 | i1=J_88 | i1=J_88 | i10=J_88 | i1=J_88 | i10=J_88 | i10=J_88 | i1=J_88 | i1=J_88 | i1=J_88 | i1=J_88 | i1=J_88))). % 7.81/2.86 tff(c_3877, plain, (![J_14]: (select(a_60, J_14)=select(a_58, J_14) | i1=J_14 | i1=J_14 | i10=J_14 | i1=J_14 | i10=J_14 | i10=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 7.81/2.86 tff(c_3841, plain, (![J_14]: (select(a_62, J_14)=select(a_60, J_14) | i1=J_14 | i1=J_14 | i10=J_14 | i1=J_14 | i10=J_14 | i10=J_14 | i1=J_14 | i1=J_14 | i1=J_14 | i1=J_14))). % 7.81/2.86 tff(c_3790, plain, (![J_85]: (select(a_64, J_85)=select(a_62, J_85) | i1=J_85 | i1=J_85 | i10=J_85 | i1=J_85 | i10=J_85 | i10=J_85 | i1=J_85 | i1=J_85 | i1=J_85))). % 7.81/2.86 tff(c_3760, plain, (![J_5]: (select(a_66, J_5)=select(a_64, J_5) | i1=J_5 | i10=J_5 | i1=J_5 | i10=J_5 | i10=J_5 | i1=J_5 | i1=J_5 | i1=J_5))). % 7.81/2.86 tff(c_3709, plain, (![J_83]: (select(a_68, J_83)=select(a_66, J_83) | i1=J_83 | i10=J_83 | i1=J_83 | i10=J_83 | i10=J_83 | i1=J_83 | i1=J_83))). % 7.81/2.86 tff(c_3682, plain, (![J_5]: (select(a_70, J_5)=select(a_68, J_5) | i10=J_5 | i1=J_5 | i10=J_5 | i10=J_5 | i1=J_5 | i1=J_5))). % 7.81/2.86 tff(c_3643, plain, (![J_14]: (select(a_72, J_14)=select(a_70, J_14) | i10=J_14 | i1=J_14 | i10=J_14 | i10=J_14 | i1=J_14))). % 7.81/2.86 tff(c_3613, plain, (![J_14]: (select(a_74, J_14)=select(a_72, J_14) | i10=J_14 | i1=J_14 | i10=J_14 | i10=J_14))). % 7.81/2.86 tff(c_3390, plain, (![J_77]: (select(a_76, J_77)=select(a_74, J_77) | i10=J_77 | i1=J_77 | i10=J_77))). % 7.81/2.86 tff(c_3582, plain, (select(a2, i10)=e_75)). % 7.81/2.86 tff(c_3569, plain, (select(a_46, i10)=e_75)). % 7.81/2.86 tff(c_3557, plain, (select(a_50, i10)=e_75)). % 7.81/2.86 tff(c_3542, plain, (select(a_54, i10)=e_75)). % 7.81/2.86 tff(c_3525, plain, (select(a_58, i10)=e_75)). % 7.81/2.86 tff(c_1520, plain, (![J_14]: (select(a_62, J_14)=select(a_58, J_14) | i1=J_14))). % 7.81/2.86 tff(c_3473, plain, (![J_5]: (select(a_72, J_5)=select(a_68, J_5) | i1=J_5))). % 7.81/2.86 tff(c_3463, plain, (select(a1, i10)=e_43)). % 7.81/2.86 tff(c_3450, plain, (select(a_44, i10)=e_43)). % 7.81/2.86 tff(c_3437, plain, (select(a_48, i10)=e_43)). % 7.81/2.86 tff(c_3424, plain, (select(a_52, i10)=e_43)). % 7.81/2.87 tff(c_3374, plain, (select(a_56, i10)=e_43)). % 7.81/2.87 tff(c_2968, plain, (![J_66]: (select(a_78, J_66)=select(a_76, J_66) | i1=J_66 | i10=J_66))). % 7.81/2.87 tff(c_3361, plain, (select(a_60, i10)=e_43)). % 7.81/2.87 tff(c_3345, plain, (select(a_64, i10)=e_43)). % 7.81/2.87 tff(c_3324, plain, (![J_5]: (select(a_68, J_5)=select(a_64, J_5) | i1=J_5))). % 7.81/2.87 tff(c_1274, plain, (![J_14]: (select(a_56, J_14)=select(a_52, J_14) | i1=J_14))). % 7.81/2.87 tff(c_1265, plain, (![J_14]: (select(a_58, J_14)=select(a_54, J_14) | i1=J_14))). % 7.81/2.87 tff(c_3276, plain, (select(a_62, i10)=e_75)). % 7.81/2.87 tff(c_3260, plain, (select(a_66, i10)=e_75)). % 7.81/2.87 tff(c_3239, plain, (![J_14]: (select(a_70, J_14)=select(a_66, J_14) | i1=J_14))). % 7.81/2.87 tff(c_527, plain, (![J_14]: (select(a_76, J_14)=select(a_72, J_14) | i10=J_14))). % 7.81/2.87 tff(c_3200, plain, (![J_14]: (select(a_54, J_14)=select(a_50, J_14) | i1=J_14))). % 7.81/2.87 tff(c_1277, plain, (![J_14]: (select(a_50, J_14)=select(a_46, J_14) | i1=J_14))). % 7.81/2.87 tff(c_3011, plain, (store(a_76, i1, e_43)=a_80)). % 7.81/2.87 tff(c_3150, plain, (![J_14]: (select(a_64, J_14)=select(a_60, J_14) | i1=J_14))). % 7.81/2.87 tff(c_3012, plain, (store(a_74, i10, e_43)=a_78)). % 7.81/2.87 tff(c_3010, plain, (select(a_68, i10)=e_43)). % 7.81/2.87 tff(c_3064, plain, (select(a_70, i10)=e_75)). % 7.81/2.87 tff(c_3109, plain, (![J_14]: (select(a_48, J_14)=select(a_44, J_14) | i1=J_14))). % 7.81/2.87 tff(c_3013, plain, (select(a_72, i10)=e_43)). % 7.81/2.87 tff(c_3016, plain, (select(a_78, i10)=e_43)). % 7.81/2.87 tff(c_3014, plain, (select(a_80, i1)=e_43)). % 7.81/2.87 tff(c_3041, plain, (![J_14]: (select(a_74, J_14)=select(a_70, J_14) | i1=J_14))). % 7.81/2.87 tff(c_3026, plain, (select(a_78, i1)=e_43)). % 7.81/2.87 tff(c_3015, plain, (e_79=e_43)). % 7.81/2.87 tff(c_3005, plain, (e_77=e_43)). % 7.81/2.87 tff(c_379, plain, (![J_14]: (select(a_80, J_14)=select(a_78, J_14) | i10=J_14))). % 7.81/2.87 tff(c_2935, plain, (i10!=i1)). % 7.81/2.87 tff(c_2936, plain, (![J_14]: (select(a_52, J_14)=select(a_48, J_14) | i1=J_14))). % 7.81/2.87 tff(c_1562, plain, (store(a_56, i1, e_43)=a_60)). % 7.81/2.87 tff(c_1767, plain, (store(a_70, i1, e_43)=a_74)). % 7.81/2.87 tff(c_1755, plain, (store(a_68, i1, e_45)=a_72)). % 7.81/2.87 tff(c_1743, plain, (store(a_66, i1, e_45)=a_70)). % 7.81/2.87 tff(c_1723, plain, (![J_14]: (select(a_60, J_14)=select(a_56, J_14) | i1=J_14))). % 7.81/2.87 tff(c_1711, plain, (store(a_64, i1, e_43)=a_68)). % 7.81/2.87 tff(c_1699, plain, (store(a_60, i1, e_45)=a_64)). % 7.81/2.87 tff(c_1687, plain, (store(a_62, i1, e_43)=a_66)). % 7.81/2.87 tff(c_1682, plain, (select(a_74, i1)=e_43)). % 7.81/2.87 tff(c_1677, plain, (select(a_72, i1)=e_45)). % 7.81/2.87 tff(c_1665, plain, (store(a_58, i1, e_45)=a_62)). % 7.81/2.87 tff(c_1660, plain, (select(a_70, i1)=e_45)). % 7.81/2.87 tff(c_1655, plain, (select(a_68, i1)=e_43)). % 7.81/2.87 tff(c_1650, plain, (select(a_64, i1)=e_45)). % 7.81/2.87 tff(c_1630, plain, (![J_14]: (select(a_66, J_14)=select(a_62, J_14) | i1=J_14))). % 7.81/2.87 tff(c_1625, plain, (select(a_66, i1)=e_43)). % 7.81/2.87 tff(c_1619, plain, (select(a_62, i1)=e_45)). % 7.81/2.87 tff(c_1555, plain, (e_71=e_45)). % 7.81/2.87 tff(c_1563, plain, (e_73=e_43)). % 7.81/2.87 tff(c_1606, plain, (select(a_60, i1)=e_43)). % 7.81/2.87 tff(c_1556, plain, (e_69=e_45)). % 7.81/2.87 tff(c_1564, plain, (e_67=e_43)). % 7.81/2.87 tff(c_1565, plain, (e_65=e_43)). % 7.81/2.87 tff(c_1574, plain, (![J_14]: (select(a_78, J_14)=select(a_74, J_14) | i10=J_14))). % 7.81/2.87 tff(c_1557, plain, (e_63=e_45)). % 7.81/2.87 tff(c_1527, plain, (e_59=e_43)). % 7.81/2.87 tff(c_1528, plain, (e_61=e_45)). % 7.81/2.87 tff(c_1513, plain, (i8=i1)). % 7.81/2.87 tff(c_1519, plain, (i6=i1)). % 7.81/2.87 tff(c_1514, plain, (i7=i1)). % 7.81/2.87 tff(c_1502, plain, (i5=i1)). % 7.81/2.87 tff(c_1460, plain, (store(a_54, i1, e_43)=a_58)). % 7.81/2.87 tff(c_1448, plain, (store(a_52, i1, e_45)=a_56)). % 7.81/2.87 tff(c_1435, plain, (store(a_48, i1, e_43)=a_52)). % 7.81/2.87 tff(c_1423, plain, (store(a_50, i1, e_45)=a_54)). % 7.81/2.87 tff(c_1411, plain, (store(a_44, i1, e_45)=a_48)). % 7.81/2.87 tff(c_415, plain, (![J_14]: (select(a_46, J_14)=select(a2, J_14) | i1=J_14))). % 7.81/2.87 tff(c_1387, plain, (select(a_58, i1)=e_43)). % 7.81/2.87 tff(c_1382, plain, (select(a_56, i1)=e_45)). % 7.81/2.87 tff(c_1377, plain, (select(a_54, i1)=e_45)). % 7.81/2.87 tff(c_1372, plain, (select(a_52, i1)=e_43)). % 7.81/2.87 tff(c_1303, plain, (select(a_50, i1)=e_43)). % 7.81/2.87 tff(c_1362, plain, (select(a_48, i1)=e_45)). % 7.81/2.87 tff(c_1307, plain, (e_55=e_45)). % 7.81/2.87 tff(c_1290, plain, (e_57=e_43)). % 7.81/2.87 tff(c_424, plain, (![J_14]: (select(a_80, J_14)=select(a_76, J_14) | i1=J_14))). % 7.81/2.87 tff(c_1275, plain, (i4=i1)). % 7.81/2.87 tff(c_1308, plain, (e_53=e_45)). % 7.81/2.87 tff(c_1276, plain, (i3=i1)). % 7.81/2.87 tff(c_1291, plain, (e_51=e_43)). % 7.81/2.87 tff(c_1285, plain, (e_47=e_45)). % 7.81/2.87 tff(c_1296, plain, (store(a_46, i1, e_43)=a_50)). % 7.81/2.87 tff(c_1284, plain, (e_49=e_43)). % 7.81/2.87 tff(c_1264, plain, (i2=i1)). % 7.81/2.87 tff(c_373, plain, (![J_14]: (select(a_44, J_14)=select(a1, J_14) | i1=J_14))). % 7.81/2.87 tff(c_531, plain, (store(a_72, i10, e_75)=a_76)). % 7.81/2.87 tff(c_581, plain, (store(a_78, i10, e_75)=a_80)). % 7.81/2.87 tff(c_580, plain, (select(a_80, i10)=e_75)). % 7.81/2.87 tff(c_532, plain, (select(a_74, i10)=e_75)). % 7.81/2.88 tff(c_550, plain, (e_81=e_75)). % 7.81/2.88 tff(c_529, plain, (select(a_76, i10)=e_75)). % 7.81/2.88 tff(c_525, plain, (i9=i10)). % 7.81/2.88 tff(c_326, plain, (select(a_46, i1)=e_45)). % 7.81/2.88 tff(c_284, plain, (select(a_44, i1)=e_43)). % 7.81/2.88 tff(c_4, plain, (![A_6, I_4, E_7, J_5]: (select(store(A_6, I_4, E_7), J_5)=select(A_6, J_5) | J_5=I_4))). % 7.81/2.88 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 7.81/2.88 tff(c_6, plain, (store(a1, i1, e_43)=a_44)). % 7.81/2.88 tff(c_8, plain, (store(a2, i1, e_45)=a_46)). % 7.81/2.88 tff(c_46, plain, (select(a2, i1)=e_43)). % 7.81/2.88 tff(c_48, plain, (select(a1, i1)=e_45)). % 7.81/2.88 tff(c_92, plain, (a_82=a_80)). % 7.81/2.88 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.81/2.88 %------------------------------------------------------------------------------