%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PUZ066+1 : TPTP v9.0.0. Released v3.2.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 : n029.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 08:25:13 PM UTC 2025 % Result : Satisfiable 25.98s 9.80s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PUZ066+1 : TPTP v9.0.0. Released v3.2.0. % 0.07/0.12 % 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.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Apr 8 17:21:34 EDT 2025 % 0.12/0.33 % CPUTime : % 25.98/9.80 % 25.98/9.80 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.98/9.80 % 25.98/9.80 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.27/9.81 %$ ssP > ssA > #nlpp > n9 > n8 > n7 > n6 > n5 > n4 > n3 > n2 > n1 % 26.27/9.81 % 26.27/9.81 %Foreground sorts: % 26.27/9.81 % 26.27/9.81 % 26.27/9.81 %Background operators: % 26.27/9.81 % 26.27/9.81 % 26.27/9.81 %Foreground operators: % 26.27/9.81 tff(n8, type, n8: $i). % 26.27/9.81 tff(ssA, type, ssA: ($i * $i) > $i). % 26.27/9.81 tff(n9, type, n9: $i). % 26.27/9.81 tff(n3, type, n3: $i). % 26.27/9.81 tff(n1, type, n1: $i). % 26.27/9.81 tff(n7, type, n7: $i). % 26.27/9.81 tff(n6, type, n6: $i). % 26.27/9.81 tff(n4, type, n4: $i). % 26.27/9.81 tff(ssP, type, ssP: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 26.27/9.81 tff(n2, type, n2: $i). % 26.27/9.81 tff(n5, type, n5: $i). % 26.27/9.81 % 26.27/9.81 %Saturated clause set: % 26.27/9.81 tff(c_8280, plain, (ssP(n7, n6, n8, n2, n4, n3, n5, n1, n9, n5, n1, n3, n7, n6, n9, n8, n2, n4, n2, n4, n9, n1, n8, n5, n3, n7, n6, n6, n7, n5, n9, n2, n8, n4, n3, n1, n8, n3, n4, n5, n7, n1, n6, n9, n2, n1, n9, n2, n4, n3, n6, n7, n5, n8, n3, n2, n7, n8, n1, n4, n9, n6, n5, n9, n8, n1, n6, n5, n7, n2, n4, n3, n4, n5, n6, n3, n9, n2, n1, n8, n7))). % 26.27/9.81 tff(c_8213, plain, (ssA(n2, n6)=n9)). % 26.27/9.81 tff(c_8198, plain, (ssA(n9, n5)=n9)). % 26.27/9.81 tff(c_8147, plain, (ssA(n4, n6)=n8)). % 26.27/9.81 tff(c_8130, plain, (ssA(n3, n5)=n8)). % 26.27/9.81 tff(c_8115, plain, (ssA(n2, n9)=n4)). % 26.27/9.81 tff(c_8100, plain, (ssA(n9, n8)=n8)). % 26.27/9.81 tff(c_8085, plain, (ssA(n9, n2)=n5)). % 26.27/9.81 tff(c_8070, plain, (ssA(n1, n9)=n9)). % 26.27/9.81 tff(c_8043, plain, (ssA(n9, n6)=n2)). % 26.27/9.81 tff(c_8024, plain, (ssA(n8, n5)=n5)). % 26.27/9.81 tff(c_8005, plain, (ssA(n7, n9)=n5)). % 26.27/9.81 tff(c_7981, plain, (ssA(n3, n6)=n5)). % 26.27/9.81 tff(c_7905, plain, (ssA(n7, n6)=n4)). % 26.27/9.81 tff(c_7885, plain, (ssA(n4, n5)=n2)). % 26.27/9.81 tff(c_7867, plain, (ssA(n8, n2)=n8)). % 26.27/9.81 tff(c_7702, plain, (ssA(n2, n7)=n8)). % 26.27/9.81 tff(c_7686, plain, (ssA(n6, n8)=n5)). % 26.27/9.81 tff(c_7671, plain, (ssA(n1, n3)=n8)). % 26.27/9.81 tff(c_7653, plain, (ssA(n7, n2)=n2)). % 26.27/9.81 tff(c_7634, plain, (ssA(n7, n7)=n9)). % 26.27/9.81 tff(c_7582, plain, (ssA(n2, n8)=n2)). % 26.27/9.81 tff(c_7563, plain, (ssA(n8, n8)=n4)). % 26.27/9.81 tff(c_7546, plain, (ssA(n5, n8)=n9)). % 26.27/9.81 tff(c_7527, plain, (ssA(n4, n4)=n9)). % 26.27/9.81 tff(c_7511, plain, (ssA(n3, n3)=n9)). % 26.27/9.81 tff(c_7169, plain, (ssA(n5, n9)=n2)). % 26.27/9.81 tff(c_7150, plain, (ssA(n1, n5)=n4)). % 26.27/9.81 tff(c_7131, plain, (ssA(n6, n9)=n8)). % 26.27/9.81 tff(c_5863, plain, (ssA(n7, n4)=n8)). % 26.27/9.81 tff(c_4141, plain, (ssA(n3, n4)=n1)). % 26.27/9.81 tff(c_4385, plain, (ssA(n5, n6)=n1)). % 26.27/9.81 tff(c_4179, plain, (ssA(n1, n8)=n1)). % 26.27/9.81 tff(c_4183, plain, (ssA(n9, n7)=n1)). % 26.27/9.81 tff(c_4527, plain, (ssA(n7, n1)=n3)). % 26.27/9.81 tff(c_5393, plain, (ssA(n8, n6)=n7)). % 26.27/9.81 tff(c_5545, plain, (ssA(n6, n3)=n2)). % 26.27/9.81 tff(c_5435, plain, (ssA(n6, n5)=n3)). % 26.27/9.81 tff(c_5244, plain, (ssA(n3, n8)=n7)). % 26.27/9.81 tff(c_4994, plain, (ssA(n4, n7)=n4)). % 26.27/9.81 tff(c_5608, plain, (ssA(n3, n1)=n2)). % 26.27/9.81 tff(c_5118, plain, (ssA(n2, n4)=n7)). % 26.27/9.81 tff(c_4851, plain, (ssA(n4, n3)=n5)). % 26.27/9.82 tff(c_5030, plain, (ssA(n9, n4)=n3)). % 26.27/9.82 tff(c_5363, plain, (ssA(n5, n5)=n7)). % 26.27/9.82 tff(c_4880, plain, (ssA(n8, n4)=n6)). % 26.27/9.82 tff(c_2684, plain, (ssA(n4, n9)=n1)). % 26.27/9.82 tff(c_5634, plain, (ssA(n2, n1)=n5)). % 26.27/9.82 tff(c_5148, plain, (ssA(n8, n9)=n3)). % 26.27/9.82 tff(c_5178, plain, (ssA(n1, n6)=n3)). % 26.27/9.82 tff(c_2672, plain, (ssA(n1, n7)=n5)). % 26.27/9.82 tff(c_4800, plain, (ssA(n5, n7)=n6)). % 26.27/9.82 tff(c_4949, plain, (ssA(n6, n6)=n6)). % 26.27/9.82 tff(c_2696, plain, (ssA(n8, n1)=n9)). % 26.27/9.82 tff(c_5211, plain, (ssA(n6, n7)=n7)). % 26.27/9.82 tff(c_4809, plain, (ssA(n7, n3)=n7)). % 26.27/9.82 tff(c_2694, plain, (ssA(n7, n8)=n6)). % 26.27/9.82 tff(c_4736, plain, (ssA(n4, n1)=n6)). % 26.27/9.82 tff(c_2690, plain, (ssA(n6, n4)=n4)). % 26.27/9.82 tff(c_2682, plain, (ssA(n4, n8)=n3)). % 26.27/9.82 tff(c_4622, plain, (ssA(n3, n9)=n6)). % 26.27/9.82 tff(c_4733, plain, (ssA(n9, n3)=n6)). % 26.27/9.82 tff(c_2698, plain, (ssA(n8, n7)=n2)). % 26.27/9.82 tff(c_5334, plain, (ssA(n9, n9)=n7)). % 26.27/9.82 tff(c_2700, plain, (ssA(n9, n1)=n4)). % 26.27/9.82 tff(c_4565, plain, (ssA(n3, n7)=n3)). % 26.27/9.82 tff(c_2692, plain, (ssA(n7, n5)=n1)). % 26.27/9.82 tff(c_3955, plain, (ssA(n1, n1)=n7)). % 26.27/9.82 tff(c_2676, plain, (ssA(n2, n3)=n3)). % 26.27/9.82 tff(c_2678, plain, (ssA(n2, n5)=n6)). % 26.27/9.82 tff(c_4316, plain, (ssA(n6, n1)=n1)). % 26.27/9.82 tff(c_5486, plain, (ssA(n3, n2)=n4)). % 26.27/9.82 tff(c_2670, plain, (ssA(n1, n4)=n2)). % 26.27/9.82 tff(c_5510, plain, (ssA(n6, n2)=n9)). % 26.27/9.82 tff(c_2688, plain, (ssA(n5, n4)=n5)). % 26.27/9.82 tff(c_5527, plain, (ssA(n5, n3)=n4)). % 26.27/9.82 tff(c_5408, plain, (ssA(n5, n2)=n3)). % 26.27/9.82 tff(c_2674, plain, (ssA(n2, n2)=n1)). % 26.27/9.82 tff(c_2680, plain, (ssA(n4, n2)=n7)). % 26.27/9.82 tff(c_2668, plain, (ssA(n1, n2)=n6)). % 26.27/9.82 tff(c_2686, plain, (ssA(n5, n1)=n8)). % 26.27/9.82 tff(c_4297, plain, (ssA(n8, n3)=n1)). % 26.27/9.82 tff(c_3962, plain, (n7!=n5)). % 26.27/9.82 tff(c_3025, plain, (n6!=n1)). % 26.27/9.82 tff(c_3030, plain, (n6!=n3)). % 26.27/9.82 tff(c_28, plain, (n6!=n4)). % 26.27/9.82 tff(c_46, plain, (n8!=n2)). % 26.27/9.82 tff(c_10, plain, (n8!=n6)). % 26.27/9.82 tff(c_60, plain, (n8!=n1)). % 26.27/9.82 tff(c_56, plain, (n3!=n2)). % 26.27/9.82 tff(c_3577, plain, (n9!=n2)). % 26.27/9.82 tff(c_66, plain, (n5!=n1)). % 26.27/9.82 tff(c_2829, plain, (n3!=n1)). % 26.27/9.82 tff(c_2801, plain, (n9!=n4)). % 26.27/9.82 tff(c_42, plain, (n4!=n3)). % 26.27/9.82 tff(c_4033, plain, (n6!=n5)). % 26.27/9.82 tff(c_32, plain, (n9!=n3)). % 26.27/9.82 tff(c_14, plain, (n9!=n5)). % 26.27/9.82 tff(c_8, plain, (n9!=n6)). % 26.27/9.82 tff(c_3816, plain, (n7!=n3)). % 26.27/9.82 tff(c_3396, plain, (n7!=n1)). % 26.27/9.82 tff(c_3964, plain, (n7!=n4)). % 26.27/9.82 tff(c_34, plain, (n8!=n3)). % 26.27/9.82 tff(c_3726, plain, (n8!=n5)). % 26.27/9.82 tff(c_3487, plain, (n9!=n8)). % 26.27/9.82 tff(c_40, plain, (n5!=n3)). % 26.27/9.82 tff(c_3490, plain, (n8!=n4)). % 26.27/9.82 tff(c_3373, plain, (n7!=n6)). % 26.27/9.82 tff(c_58, plain, (n9!=n1)). % 26.27/9.82 tff(c_3958, plain, (n7!=n2)). % 26.27/9.82 tff(c_3959, plain, (n9!=n7)). % 26.27/9.82 tff(c_68, plain, (n4!=n1)). % 26.27/9.82 tff(c_3272, plain, (n4!=n2)). % 26.27/9.82 tff(c_72, plain, (n2!=n1)). % 26.27/9.82 tff(c_3171, plain, (n5!=n2)). % 26.27/9.82 tff(c_2914, plain, (n8!=n7)). % 26.27/9.82 tff(c_2882, plain, (n5!=n4)). % 26.27/9.82 tff(c_2725, plain, (n6!=n2)). % 26.27/9.82 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.27/9.82 %------------------------------------------------------------------------------