%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PUZ028-3 : 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 : n016.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.30s 4.19s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.21 % Problem : PUZ028-3 : TPTP v9.0.0. Released v1.1.0. % 0.11/0.22 % 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.42 % Computer : n016.cluster.edu % 0.13/0.42 % Model : x86_64 x86_64 % 0.13/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.42 % Memory : 8042.1875MB % 0.13/0.42 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.42 % CPULimit : 300 % 0.13/0.42 % WCLimit : 300 % 0.13/0.42 % DateTime : Tue Apr 8 17:10:54 EDT 2025 % 0.13/0.43 % CPUTime : % 12.30/4.19 % 12.30/4.19 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.30/4.19 % 12.30/4.19 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.30/4.20 %$ not_familiar > not_equal > familiar > person > #nlpp > n6 > n5 > n4 > n3 > n2 > n1 % 12.30/4.20 % 12.30/4.20 %Foreground sorts: % 12.30/4.20 % 12.30/4.20 % 12.30/4.20 %Background operators: % 12.30/4.20 % 12.30/4.20 % 12.30/4.20 %Foreground operators: % 12.30/4.20 tff(not_familiar, type, not_familiar: ($i * $i) > $o). % 12.30/4.20 tff(n3, type, n3: $i). % 12.30/4.20 tff(n1, type, n1: $i). % 12.30/4.20 tff(familiar, type, familiar: ($i * $i) > $o). % 12.30/4.20 tff(n6, type, n6: $i). % 12.30/4.20 tff(n4, type, n4: $i). % 12.30/4.20 tff(not_equal, type, not_equal: ($i * $i) > $o). % 12.30/4.20 tff(n2, type, n2: $i). % 12.30/4.20 tff(person, type, person: $i > $o). % 12.30/4.20 tff(n5, type, n5: $i). % 12.30/4.20 % 12.30/4.20 %Saturated clause set: % 12.30/4.20 tff(c_5000, plain, (~not_familiar(n3, n2))). % 12.30/4.20 tff(c_5002, plain, (~not_familiar(n5, n3))). % 12.30/4.20 tff(c_4979, plain, (~not_familiar(n5, n1))). % 12.30/4.20 tff(c_4941, plain, (~not_familiar(n5, n2))). % 12.30/4.20 tff(c_4943, plain, (~not_familiar(n1, n4))). % 12.30/4.20 tff(c_4938, plain, (~not_familiar(n3, n4))). % 12.30/4.20 tff(c_4922, plain, (~not_familiar(n1, n2))). % 12.30/4.20 tff(c_4913, plain, (~not_familiar(n2, n1))). % 12.30/4.20 tff(c_4906, plain, (~not_familiar(n6, n3))). % 12.30/4.20 tff(c_4897, plain, (~not_familiar(n6, n4))). % 12.30/4.20 tff(c_4892, plain, (~not_familiar(n6, n2))). % 12.30/4.20 tff(c_4885, plain, (~familiar(n1, n5))). % 12.30/4.20 tff(c_4884, plain, (not_familiar(n1, n5))). % 12.30/4.20 tff(c_4880, plain, (~familiar(n4, n1))). % 12.30/4.20 tff(c_4879, plain, (not_familiar(n4, n1))). % 12.30/4.21 tff(c_4788, plain, (familiar(n5, n2))). % 12.30/4.21 tff(c_4787, plain, (~familiar(n3, n6))). % 12.30/4.21 tff(c_4786, plain, (not_familiar(n3, n6))). % 12.30/4.21 tff(c_4712, plain, (~familiar(n2, n6))). % 12.30/4.21 tff(c_4711, plain, (not_familiar(n2, n6))). % 12.30/4.21 tff(c_4707, plain, (familiar(n6, n4))). % 12.30/4.21 tff(c_4704, plain, (~familiar(n2, n5))). % 12.30/4.21 tff(c_4703, plain, (not_familiar(n2, n5))). % 12.30/4.21 tff(c_4590, plain, (~familiar(n3, n5))). % 12.30/4.21 tff(c_4589, plain, (not_familiar(n3, n5))). % 12.30/4.21 tff(c_4474, plain, (~familiar(n1, n6))). % 12.30/4.21 tff(c_4473, plain, (not_familiar(n1, n6))). % 12.30/4.21 tff(c_4369, plain, (familiar(n6, n3))). % 12.30/4.21 tff(c_4368, plain, (familiar(n5, n3))). % 12.30/4.21 tff(c_4365, plain, (familiar(n3, n4))). % 12.30/4.21 tff(c_4364, plain, (~familiar(n4, n3))). % 12.30/4.21 tff(c_4363, plain, (not_familiar(n4, n3))). % 12.30/4.21 tff(c_4090, plain, (~familiar(n4, n6))). % 12.30/4.21 tff(c_4089, plain, (not_familiar(n4, n6))). % 12.30/4.21 tff(c_4010, plain, (familiar(n5, n6))). % 12.30/4.21 tff(c_4009, plain, (~familiar(n1, n3))). % 12.30/4.21 tff(c_4008, plain, (not_familiar(n1, n3))). % 12.30/4.21 tff(c_3704, plain, (familiar(n3, n2))). % 12.30/4.21 tff(c_3697, plain, (~familiar(n3, n1))). % 12.30/4.21 tff(c_3703, plain, (familiar(n6, n1))). % 12.30/4.21 tff(c_3696, plain, (not_familiar(n3, n1))). % 12.30/4.21 tff(c_3505, plain, (~familiar(n4, n2))). % 12.30/4.21 tff(c_3504, plain, (not_familiar(n4, n2))). % 12.30/4.21 tff(c_3506, plain, (~not_familiar(n5, n4))). % 12.30/4.21 tff(c_1461, plain, (familiar(n6, n2))). % 12.30/4.21 tff(c_1460, plain, (~familiar(n4, n5))). % 12.30/4.21 tff(c_1459, plain, (not_familiar(n4, n5))). % 12.30/4.21 tff(c_1216, plain, (familiar(n5, n4))). % 12.30/4.21 tff(c_1215, plain, (~not_familiar(n6, n5))). % 12.30/4.21 tff(c_1214, plain, (familiar(n2, n1))). % 12.30/4.21 tff(c_1213, plain, (familiar(n6, n5))). % 12.30/4.21 tff(c_1212, plain, (familiar(n2, n4))). % 12.30/4.21 tff(c_1211, plain, (familiar(n5, n1))). % 12.30/4.21 tff(c_1210, plain, (~not_familiar(n6, n1))). % 12.30/4.21 tff(c_1209, plain, (familiar(n1, n2))). % 12.30/4.21 tff(c_1208, plain, (familiar(n1, n4))). % 12.30/4.21 tff(c_1207, plain, (familiar(n2, n3))). % 12.30/4.21 tff(c_56, plain, (not_equal(n5, n2))). % 12.30/4.21 tff(c_64, plain, (not_equal(n6, n1))). % 12.30/4.21 tff(c_58, plain, (not_equal(n5, n3))). % 12.30/4.21 tff(c_30, plain, (not_equal(n2, n5))). % 12.30/4.21 tff(c_54, plain, (not_equal(n5, n1))). % 12.30/4.21 tff(c_66, plain, (not_equal(n6, n2))). % 12.30/4.21 tff(c_28, plain, (not_equal(n2, n4))). % 12.30/4.21 tff(c_48, plain, (not_equal(n4, n3))). % 12.30/4.21 tff(c_1076, plain, (~not_equal(n6, n6))). % 12.30/4.21 tff(c_70, plain, (not_equal(n6, n4))). % 12.30/4.21 tff(c_1098, plain, (~not_equal(n5, n5))). % 12.30/4.21 tff(c_62, plain, (not_equal(n5, n6))). % 12.30/4.21 tff(c_42, plain, (not_equal(n3, n6))). % 12.30/4.21 tff(c_68, plain, (not_equal(n6, n3))). % 12.30/4.21 tff(c_60, plain, (not_equal(n5, n4))). % 12.30/4.21 tff(c_664, plain, (~not_familiar(n2, n2))). % 12.30/4.21 tff(c_50, plain, (not_equal(n4, n5))). % 12.30/4.21 tff(c_1142, plain, (~not_equal(n3, n3))). % 12.30/4.21 tff(c_14, plain, (not_equal(n1, n2))). % 12.30/4.21 tff(c_18, plain, (not_equal(n1, n4))). % 12.30/4.21 tff(c_22, plain, (not_equal(n1, n6))). % 12.30/4.21 tff(c_836, plain, (~not_familiar(n4, n4))). % 12.30/4.21 tff(c_32, plain, (not_equal(n2, n6))). % 12.30/4.21 tff(c_16, plain, (not_equal(n1, n3))). % 12.30/4.21 tff(c_24, plain, (not_equal(n2, n1))). % 12.30/4.21 tff(c_1164, plain, (~not_equal(n2, n2))). % 12.30/4.21 tff(c_34, plain, (not_equal(n3, n1))). % 12.30/4.21 tff(c_578, plain, (~not_familiar(n1, n1))). % 12.30/4.21 tff(c_40, plain, (not_equal(n3, n5))). % 12.30/4.21 tff(c_1008, plain, (~not_familiar(n6, n6))). % 12.30/4.21 tff(c_26, plain, (not_equal(n2, n3))). % 12.30/4.21 tff(c_1186, plain, (~not_equal(n1, n1))). % 12.30/4.21 tff(c_44, plain, (not_equal(n4, n1))). % 12.30/4.21 tff(c_1120, plain, (~not_equal(n4, n4))). % 12.30/4.21 tff(c_38, plain, (not_equal(n3, n4))). % 12.30/4.21 tff(c_146, plain, (~familiar(n1, n1))). % 12.30/4.21 tff(c_318, plain, (~familiar(n3, n3))). % 12.30/4.21 tff(c_52, plain, (not_equal(n4, n6))). % 12.30/4.21 tff(c_46, plain, (not_equal(n4, n2))). % 12.30/4.21 tff(c_404, plain, (~familiar(n4, n4))). % 12.30/4.21 tff(c_20, plain, (not_equal(n1, n5))). % 12.30/4.21 tff(c_36, plain, (not_equal(n3, n2))). % 12.30/4.21 tff(c_490, plain, (~familiar(n5, n5))). % 12.30/4.21 tff(c_72, plain, (not_equal(n6, n5))). % 12.30/4.21 tff(c_576, plain, (~familiar(n6, n6))). % 12.30/4.21 tff(c_232, plain, (~familiar(n2, n2))). % 12.30/4.21 tff(c_922, plain, (~not_familiar(n5, n5))). % 12.30/4.21 tff(c_750, plain, (~not_familiar(n3, n3))). % 12.30/4.21 tff(c_2, plain, (person(n1))). % 12.30/4.21 tff(c_4, plain, (person(n2))). % 12.30/4.21 tff(c_6, plain, (person(n3))). % 12.30/4.22 tff(c_8, plain, (person(n4))). % 12.30/4.22 tff(c_10, plain, (person(n5))). % 12.30/4.22 tff(c_12, plain, (person(n6))). % 12.30/4.22 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.30/4.22 %------------------------------------------------------------------------------