%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PUZ028-2 : TPTP v9.0.0. Bugfixed v1.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 : n004.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:04 PM UTC 2025 % Result : Satisfiable 5.49s 2.74s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : PUZ028-2 : TPTP v9.0.0. Bugfixed v1.2.0. % 0.09/0.11 % 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.10/0.31 % Computer : n004.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.31 % CPULimit : 300 % 0.15/0.31 % WCLimit : 300 % 0.15/0.31 % DateTime : Tue Apr 8 17:09:52 EDT 2025 % 0.15/0.31 % CPUTime : % 5.49/2.74 % 5.49/2.74 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.49/2.74 % 5.49/2.74 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.49/2.75 %$ not_familiar > not_equal > familiar > person > #nlpp > n6 > n5 > n4 > n3 > n2 > n1 % 5.49/2.75 % 5.49/2.75 %Foreground sorts: % 5.49/2.75 % 5.49/2.75 % 5.49/2.75 %Background operators: % 5.49/2.75 % 5.49/2.75 % 5.49/2.75 %Foreground operators: % 5.49/2.75 tff(not_familiar, type, not_familiar: ($i * $i) > $o). % 5.49/2.75 tff(n3, type, n3: $i). % 5.49/2.75 tff(n1, type, n1: $i). % 5.49/2.75 tff(familiar, type, familiar: ($i * $i) > $o). % 5.49/2.75 tff(n6, type, n6: $i). % 5.49/2.75 tff(n4, type, n4: $i). % 5.49/2.75 tff(not_equal, type, not_equal: ($i * $i) > $o). % 5.49/2.75 tff(n2, type, n2: $i). % 5.49/2.75 tff(person, type, person: $i > $o). % 5.49/2.75 tff(n5, type, n5: $i). % 5.49/2.75 % 5.49/2.75 %Saturated clause set: % 5.49/2.76 tff(c_788, plain, (![Y_25]: (~not_equal(Y_25, n5) | familiar(Y_25, n5) | ~not_equal(n3, Y_25) | ~person(Y_25) | familiar(n3, Y_25)))). % 5.49/2.76 tff(c_772, plain, (~not_equal(n4, n4))). % 5.49/2.76 tff(c_757, plain, (![Y_25]: (~not_equal(Y_25, n2) | familiar(Y_25, n2) | ~not_equal(n4, Y_25) | ~person(Y_25) | familiar(n4, Y_25)))). % 5.49/2.76 tff(c_727, plain, (![Y_25]: (~not_equal(Y_25, n1) | familiar(Y_25, n1) | ~not_equal(n2, Y_25) | ~person(Y_25) | familiar(n2, Y_25)))). % 5.49/2.76 tff(c_697, plain, (![Y_25]: (~not_equal(Y_25, n4) | familiar(Y_25, n4) | ~not_equal(n3, Y_25) | ~person(Y_25) | familiar(n3, Y_25)))). % 5.49/2.76 tff(c_685, plain, (~not_equal(n2, n2))). % 5.49/2.76 tff(c_666, plain, (![Y_25]: (~not_equal(Y_25, n4) | familiar(Y_25, n4) | ~not_equal(n2, Y_25) | ~person(Y_25) | familiar(n2, Y_25)))). % 5.49/2.76 tff(c_665, plain, (~familiar(n6, n6))). % 5.49/2.76 tff(c_648, plain, (~familiar(n1, n1))). % 5.49/2.76 tff(c_649, plain, (![X2_4]: (~familiar(X2_4, n1) | ~familiar(n6, X2_4)))). % 5.49/2.76 tff(c_643, plain, (familiar(n1, n6))). % 5.49/2.76 tff(c_614, plain, (![Y_25]: (~not_equal(Y_25, n6) | familiar(Y_25, n6) | ~not_equal(n5, Y_25) | ~person(Y_25) | familiar(n5, Y_25)))). % 5.49/2.76 tff(c_585, plain, (![Y_25]: (~not_equal(Y_25, n1) | familiar(Y_25, n1) | ~not_equal(n5, Y_25) | ~person(Y_25) | familiar(n5, Y_25)))). % 5.49/2.76 tff(c_555, plain, (![Y_25]: (~not_equal(Y_25, n1) | familiar(Y_25, n1) | ~not_equal(n4, Y_25) | ~person(Y_25) | familiar(n4, Y_25)))). % 5.49/2.76 tff(c_528, plain, (![Y_25]: (~not_equal(Y_25, n1) | familiar(Y_25, n1) | ~not_equal(n3, Y_25) | ~person(Y_25) | familiar(n3, Y_25)))). % 5.49/2.76 tff(c_520, plain, (![X2_4]: (~familiar(X2_4, n2) | ~familiar(n1, X2_4)))). % 5.49/2.76 tff(c_517, plain, (familiar(n2, n1))). % 5.49/2.76 tff(c_487, plain, (![Y_25]: (~not_equal(Y_25, n6) | familiar(Y_25, n6) | ~not_equal(n2, Y_25) | ~person(Y_25) | familiar(n2, Y_25)))). % 5.49/2.76 tff(c_457, plain, (![Y_25]: (~not_equal(Y_25, n6) | familiar(Y_25, n6) | ~not_equal(n4, Y_25) | ~person(Y_25) | familiar(n4, Y_25)))). % 5.49/2.76 tff(c_449, plain, (![X2_4]: (~familiar(X2_4, n4) | ~familiar(n1, X2_4)))). % 5.49/2.76 tff(c_446, plain, (familiar(n4, n1))). % 5.49/2.76 tff(c_435, plain, (![X2_4]: (~familiar(X2_4, n5) | ~familiar(n1, X2_4)))). % 5.49/2.76 tff(c_432, plain, (familiar(n5, n1))). % 5.49/2.76 tff(c_401, plain, (![Y_25]: (~not_equal(Y_25, n2) | familiar(Y_25, n2) | ~not_equal(n3, Y_25) | ~person(Y_25) | familiar(n3, Y_25)))). % 5.49/2.77 tff(c_398, plain, (![X2_4]: (~familiar(X2_4, n3) | ~familiar(n5, X2_4)))). % 5.49/2.77 tff(c_397, plain, (~familiar(n2, n3))). % 5.49/2.77 tff(c_395, plain, (~familiar(n4, n3))). % 5.49/2.77 tff(c_386, plain, (familiar(n3, n5))). % 5.49/2.77 tff(c_385, plain, (~familiar(n4, n4))). % 5.49/2.77 tff(c_384, plain, (~familiar(n4, n2))). % 5.49/2.77 tff(c_378, plain, (![X2_4]: (~familiar(X2_4, n5) | ~familiar(n4, X2_4)))). % 5.49/2.77 tff(c_369, plain, (familiar(n5, n4))). % 5.49/2.77 tff(c_368, plain, (~familiar(n6, n5))). % 5.49/2.77 tff(c_361, plain, (![X2_4]: (~familiar(X2_4, n2) | ~familiar(n6, X2_4)))). % 5.49/2.77 tff(c_360, plain, (~familiar(n1, n2))). % 5.49/2.77 tff(c_355, plain, (familiar(n2, n6))). % 5.49/2.77 tff(c_333, plain, (![X2_4]: (~familiar(X2_4, n3) | ~familiar(n2, X2_4)))). % 5.49/2.77 tff(c_351, plain, (~familiar(n6, n4))). % 5.49/2.77 tff(c_350, plain, (~familiar(n6, n2))). % 5.49/2.77 tff(c_337, plain, (![X2_4]: (~familiar(X2_4, n3) | ~familiar(n1, X2_4)))). % 5.49/2.77 tff(c_344, plain, (![X2_4]: (~familiar(X2_4, n5) | ~familiar(n6, X2_4)))). % 5.49/2.77 tff(c_343, plain, (~familiar(n1, n5))). % 5.49/2.77 tff(c_338, plain, (familiar(n5, n6))). % 5.49/2.77 tff(c_334, plain, (familiar(n3, n1))). % 5.49/2.77 tff(c_327, plain, (familiar(n3, n2))). % 5.49/2.77 tff(c_326, plain, (~familiar(n2, n4))). % 5.49/2.77 tff(c_325, plain, (~familiar(n2, n2))). % 5.49/2.77 tff(c_319, plain, (![X2_4]: (~familiar(X2_4, n5) | ~familiar(n2, X2_4)))). % 5.49/2.77 tff(c_318, plain, (~familiar(n5, n5))). % 5.49/2.77 tff(c_313, plain, (familiar(n5, n2))). % 5.49/2.77 tff(c_286, plain, (![Y_25]: (~not_equal(Y_25, n6) | familiar(Y_25, n6) | ~not_equal(n3, Y_25) | ~person(Y_25) | familiar(n3, Y_25)))). % 5.49/2.77 tff(c_285, plain, (~familiar(n6, n3))). % 5.49/2.77 tff(c_281, plain, (![X2_4]: (~familiar(X2_4, n4) | ~familiar(n6, X2_4)))). % 5.49/2.77 tff(c_280, plain, (~familiar(n1, n4))). % 5.49/2.77 tff(c_275, plain, (familiar(n4, n6))). % 5.49/2.77 tff(c_274, plain, (~familiar(n1, n3))). % 5.49/2.77 tff(c_270, plain, (![X2_4]: (~familiar(X2_4, n6) | ~familiar(n1, X2_4)))). % 5.49/2.77 tff(c_267, plain, (familiar(n6, n1))). % 5.49/2.77 tff(c_265, plain, (![X2_4]: (~familiar(X2_4, n3) | ~familiar(n6, X2_4)))). % 5.49/2.77 tff(c_262, plain, (familiar(n3, n6))). % 5.49/2.77 tff(c_260, plain, (![X2_4]: (~familiar(X2_4, n2) | ~familiar(n5, X2_4)))). % 5.49/2.77 tff(c_257, plain, (familiar(n2, n5))). % 5.49/2.77 tff(c_255, plain, (![X2_4]: (~familiar(X2_4, n3) | ~familiar(n4, X2_4)))). % 5.49/2.77 tff(c_254, plain, (~familiar(n5, n3))). % 5.49/2.77 tff(c_249, plain, (familiar(n3, n4))). % 5.49/2.77 tff(c_247, plain, (![X2_4]: (~familiar(X2_4, n4) | ~familiar(n5, X2_4)))). % 5.49/2.77 tff(c_244, plain, (familiar(n4, n5))). % 5.49/2.77 tff(c_92, plain, (![Y_22, X_1, Y_2]: (~not_equal(Y_22, X_1) | familiar(Y_22, X_1) | ~not_equal(Y_2, Y_22) | ~person(Y_22) | familiar(Y_2, Y_22) | ~not_equal(X_1, Y_2) | ~person(Y_2) | ~person(X_1) | familiar(X_1, Y_2)))). % 5.49/2.77 tff(c_88, plain, (![Y_19, X_1, Y_2]: (~not_familiar(Y_19, X_1) | ~not_equal(Y_2, Y_19) | ~person(Y_19) | familiar(Y_2, Y_19) | ~not_equal(X_1, Y_2) | ~person(Y_2) | ~person(X_1) | familiar(X_1, Y_2)))). % 5.49/2.78 tff(c_84, plain, (![X2_7, X_15, Y_16]: (~not_familiar(X2_7, X_15) | ~not_familiar(Y_16, X2_7) | ~not_equal(X_15, Y_16) | ~person(Y_16) | ~person(X_15) | familiar(X_15, Y_16)))). % 5.49/2.78 tff(c_74, plain, (![X_1, Y_2]: (~not_equal(X_1, Y_2) | ~person(Y_2) | ~person(X_1) | not_familiar(X_1, Y_2) | familiar(X_1, Y_2)))). % 5.49/2.78 tff(c_78, plain, (![X3_8, X1_6, X2_7]: (~not_familiar(X3_8, X1_6) | ~not_familiar(X2_7, X3_8) | ~not_familiar(X1_6, X2_7)))). % 5.49/2.78 tff(c_76, plain, (![X3_5, X1_3, X2_4]: (~familiar(X3_5, X1_3) | ~familiar(X2_4, X3_5) | ~familiar(X1_3, X2_4)))). % 5.49/2.78 tff(c_50, plain, (not_equal(n4, n5))). % 5.49/2.78 tff(c_72, plain, (not_equal(n6, n5))). % 5.49/2.78 tff(c_64, plain, (not_equal(n6, n1))). % 5.49/2.78 tff(c_70, plain, (not_equal(n6, n4))). % 5.49/2.78 tff(c_28, plain, (not_equal(n2, n4))). % 5.49/2.78 tff(c_52, plain, (not_equal(n4, n6))). % 5.49/2.78 tff(c_38, plain, (not_equal(n3, n4))). % 5.49/2.78 tff(c_30, plain, (not_equal(n2, n5))). % 5.49/2.78 tff(c_42, plain, (not_equal(n3, n6))). % 5.49/2.78 tff(c_54, plain, (not_equal(n5, n1))). % 5.49/2.78 tff(c_46, plain, (not_equal(n4, n2))). % 5.49/2.78 tff(c_58, plain, (not_equal(n5, n3))). % 5.49/2.78 tff(c_32, plain, (not_equal(n2, n6))). % 5.49/2.78 tff(c_36, plain, (not_equal(n3, n2))). % 5.49/2.78 tff(c_34, plain, (not_equal(n3, n1))). % 5.49/2.78 tff(c_56, plain, (not_equal(n5, n2))). % 5.49/2.78 tff(c_44, plain, (not_equal(n4, n1))). % 5.49/2.78 tff(c_14, plain, (not_equal(n1, n2))). % 5.49/2.78 tff(c_40, plain, (not_equal(n3, n5))). % 5.49/2.78 tff(c_60, plain, (not_equal(n5, n4))). % 5.49/2.78 tff(c_26, plain, (not_equal(n2, n3))). % 5.49/2.78 tff(c_24, plain, (not_equal(n2, n1))). % 5.49/2.78 tff(c_22, plain, (not_equal(n1, n6))). % 5.49/2.78 tff(c_20, plain, (not_equal(n1, n5))). % 5.49/2.78 tff(c_18, plain, (not_equal(n1, n4))). % 5.49/2.78 tff(c_66, plain, (not_equal(n6, n2))). % 5.49/2.78 tff(c_48, plain, (not_equal(n4, n3))). % 5.49/2.78 tff(c_16, plain, (not_equal(n1, n3))). % 5.49/2.78 tff(c_62, plain, (not_equal(n5, n6))). % 5.49/2.78 tff(c_68, plain, (not_equal(n6, n3))). % 5.49/2.78 tff(c_4, plain, (person(n2))). % 5.49/2.78 tff(c_6, plain, (person(n3))). % 5.49/2.78 tff(c_8, plain, (person(n4))). % 5.49/2.78 tff(c_10, plain, (person(n5))). % 5.49/2.78 tff(c_2, plain, (person(n1))). % 5.49/2.78 tff(c_12, plain, (person(n6))). % 5.49/2.78 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.49/2.78 %------------------------------------------------------------------------------