%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PUZ028-4 : TPTP v9.0.0. Released v1.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 : 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 : Wed Apr 9 08:25:05 PM UTC 2025 % Result : Satisfiable 12.36s 4.40s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.18 % Problem : PUZ028-4 : TPTP v9.0.0. Released v1.1.0. % 0.12/0.19 % 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.13/0.41 % Computer : n026.cluster.edu % 0.13/0.41 % Model : x86_64 x86_64 % 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.41 % Memory : 8042.1875MB % 0.13/0.41 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.41 % CPULimit : 300 % 0.13/0.41 % WCLimit : 300 % 0.13/0.41 % DateTime : Tue Apr 8 17:10:53 EDT 2025 % 0.13/0.41 % CPUTime : % 12.36/4.40 % 12.36/4.40 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.36/4.40 % 12.36/4.40 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.36/4.41 %$ not_familiar > familiar > #nlpp > n6 > n5 > n4 > n3 > n2 > n1 % 12.36/4.41 % 12.36/4.41 %Foreground sorts: % 12.36/4.41 % 12.36/4.41 % 12.36/4.41 %Background operators: % 12.36/4.41 % 12.36/4.41 % 12.36/4.41 %Foreground operators: % 12.36/4.41 tff(not_familiar, type, not_familiar: ($i * $i) > $o). % 12.36/4.41 tff(n3, type, n3: $i). % 12.36/4.41 tff(n1, type, n1: $i). % 12.36/4.41 tff(familiar, type, familiar: ($i * $i) > $o). % 12.36/4.41 tff(n6, type, n6: $i). % 12.36/4.41 tff(n4, type, n4: $i). % 12.36/4.41 tff(n2, type, n2: $i). % 12.36/4.41 tff(n5, type, n5: $i). % 12.36/4.41 % 12.36/4.41 %Saturated clause set: % 12.36/4.41 tff(c_12799, plain, (~not_familiar(n5, n1))). % 12.36/4.41 tff(c_12790, plain, (~not_familiar(n4, n2))). % 12.36/4.41 tff(c_12755, plain, (~not_familiar(n1, n3))). % 12.36/4.41 tff(c_12753, plain, (~not_familiar(n6, n5))). % 12.36/4.41 tff(c_12744, plain, (~not_familiar(n4, n3))). % 12.36/4.42 tff(c_12729, plain, (~not_familiar(n5, n4))). % 12.36/4.42 tff(c_12672, plain, (~not_familiar(n1, n2))). % 12.36/4.42 tff(c_12663, plain, (~not_familiar(n6, n4))). % 12.36/4.42 tff(c_12658, plain, (~not_familiar(n6, n3))). % 12.36/4.42 tff(c_12646, plain, (~not_familiar(n6, n1))). % 12.36/4.42 tff(c_12643, plain, (~not_familiar(n5, n3))). % 12.36/4.42 tff(c_12640, plain, (~not_familiar(n5, n2))). % 12.36/4.42 tff(c_12631, plain, (familiar(n5, n3))). % 12.36/4.42 tff(c_12633, plain, (~not_familiar(n6, n2))). % 12.36/4.42 tff(c_12630, plain, (~familiar(n2, n4))). % 12.36/4.42 tff(c_12629, plain, (not_familiar(n2, n4))). % 12.36/4.42 tff(c_12566, plain, (familiar(n6, n3))). % 12.36/4.42 tff(c_12565, plain, (familiar(n3, n2))). % 12.36/4.42 tff(c_12564, plain, (~familiar(n3, n4))). % 12.36/4.42 tff(c_12563, plain, (not_familiar(n3, n4))). % 12.36/4.42 tff(c_12500, plain, (~familiar(n2, n1))). % 12.36/4.42 tff(c_12499, plain, (not_familiar(n2, n1))). % 12.36/4.42 tff(c_12439, plain, (familiar(n5, n2))). % 12.36/4.42 tff(c_12438, plain, (~familiar(n1, n6))). % 12.36/4.42 tff(c_12437, plain, (not_familiar(n1, n6))). % 12.36/4.42 tff(c_12406, plain, (~familiar(n3, n5))). % 12.36/4.42 tff(c_12405, plain, (not_familiar(n3, n5))). % 12.36/4.42 tff(c_12004, plain, (familiar(n6, n2))). % 12.36/4.42 tff(c_12003, plain, (~familiar(n4, n1))). % 12.36/4.42 tff(c_12002, plain, (not_familiar(n4, n1))). % 12.36/4.42 tff(c_11330, plain, (familiar(n4, n2))). % 12.36/4.42 tff(c_11329, plain, (~familiar(n3, n6))). % 12.36/4.42 tff(c_11328, plain, (not_familiar(n3, n6))). % 12.36/4.42 tff(c_9965, plain, (~familiar(n2, n6))). % 12.36/4.42 tff(c_9964, plain, (not_familiar(n2, n6))). % 12.36/4.42 tff(c_8932, plain, (~familiar(n4, n5))). % 12.36/4.42 tff(c_8931, plain, (not_familiar(n4, n5))). % 12.36/4.42 tff(c_7977, plain, (~familiar(n2, n5))). % 12.36/4.42 tff(c_7976, plain, (not_familiar(n2, n5))). % 12.36/4.42 tff(c_7267, plain, (~familiar(n4, n6))). % 12.36/4.42 tff(c_7266, plain, (not_familiar(n4, n6))). % 12.36/4.42 tff(c_7268, plain, (familiar(n2, n3))). % 12.36/4.42 tff(c_7210, plain, (familiar(n5, n1))). % 12.36/4.42 tff(c_7208, plain, (~familiar(n3, n1))). % 12.36/4.42 tff(c_7209, plain, (familiar(n6, n4))). % 12.36/4.42 tff(c_7207, plain, (not_familiar(n3, n1))). % 12.36/4.42 tff(c_6263, plain, (familiar(n5, n4))). % 12.36/4.42 tff(c_6262, plain, (familiar(n4, n3))). % 12.36/4.42 tff(c_6261, plain, (~familiar(n5, n6))). % 12.36/4.42 tff(c_6260, plain, (not_familiar(n5, n6))). % 12.36/4.42 tff(c_546, plain, (familiar(n6, n1))). % 12.36/4.42 tff(c_545, plain, (familiar(n1, n5))). % 12.36/4.42 tff(c_544, plain, (familiar(n1, n4))). % 12.36/4.42 tff(c_543, plain, (familiar(n1, n3))). % 12.36/4.42 tff(c_542, plain, (familiar(n1, n2))). % 12.36/4.42 tff(c_541, plain, (familiar(n6, n5))). % 12.36/4.42 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.36/4.42 %------------------------------------------------------------------------------