%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PLA029+2 : TPTP v9.0.0. Released v2.5.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 : n013.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:23:05 PM UTC 2025 % Result : Satisfiable 4.22s 1.96s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : PLA029+2 : TPTP v9.0.0. Released v2.5.0. % 0.03/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 : n013.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 16:35:32 EDT 2025 % 0.12/0.33 % CPUTime : % 4.22/1.96 % 4.22/1.96 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.22/1.96 % 4.22/1.96 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.22/1.97 %$ on > source > object > neq > destination > clear > time > nonfixed > fixed > a_block > #nlpp > s % 4.22/1.97 % 4.22/1.97 %Foreground sorts: % 4.22/1.97 % 4.22/1.97 % 4.22/1.97 %Background operators: % 4.22/1.97 % 4.22/1.97 % 4.22/1.97 %Foreground operators: % 4.22/1.97 tff(a_block, type, a_block: $i > $o). % 4.22/1.97 tff(time, type, time: $i > $o). % 4.22/1.97 tff(s, type, s: $i > $i). % 4.22/1.97 tff(destination, type, destination: ($i * $i) > $o). % 4.22/1.97 tff(on, type, on: ($i * $i * $i) > $o). % 4.22/1.97 tff(nonfixed, type, nonfixed: $i > $o). % 4.22/1.97 tff(clear, type, clear: ($i * $i) > $o). % 4.22/1.97 tff(fixed, type, fixed: $i > $o). % 4.22/1.97 tff(object, type, object: ($i * $i) > $o). % 4.22/1.97 tff(neq, type, neq: ($i * $i) > $o). % 4.22/1.97 tff(source, type, source: ($i * $i) > $o). % 4.22/1.97 % 4.22/1.97 %Saturated clause set: % 4.22/1.97 tff(c_342, plain, (![V_24, I_23, W_26]: (object(V_24, s(I_23)) | ~time(s(I_23)) | ~source(V_24, s(s(I_23))) | ~object(W_26, s(s(I_23))) | ~neq(W_26, V_24) | ~a_block(V_24) | ~nonfixed(W_26) | ~on(V_24, W_26, I_23) | object(V_24, I_23) | ~time(I_23) | ~neq(V_24, W_26) | ~a_block(W_26) | ~nonfixed(V_24)))). % 4.22/1.97 tff(c_343, plain, (![X_2, I_1, Z_4]: (object(X_2, s(I_1)) | ~time(s(I_1)) | ~source(X_2, s(s(I_1))) | ~object(Z_4, s(s(I_1))) | ~neq(Z_4, X_2) | ~a_block(X_2) | ~nonfixed(Z_4) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.97 tff(c_305, plain, (![V_24, I_23, W_26]: (object(V_24, s(I_23)) | ~destination(V_24, s(I_23)) | ~object(W_26, s(I_23)) | ~time(s(I_23)) | ~neq(W_26, V_24) | ~a_block(V_24) | ~nonfixed(W_26) | ~on(V_24, W_26, I_23) | object(V_24, I_23) | ~time(I_23) | ~neq(V_24, W_26) | ~a_block(W_26) | ~nonfixed(V_24)))). % 4.22/1.97 tff(c_306, plain, (![X_2, I_1, Z_4]: (object(X_2, s(I_1)) | ~destination(X_2, s(I_1)) | ~object(Z_4, s(I_1)) | ~time(s(I_1)) | ~neq(Z_4, X_2) | ~a_block(X_2) | ~nonfixed(Z_4) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.97 tff(c_316, plain, (![W_26, X_208, V_24, I_23]: (~neq(W_26, X_208) | ~neq(V_24, X_208) | ~nonfixed(W_26) | ~source(W_26, s(I_23)) | ~object(X_208, s(I_23)) | ~neq(X_208, W_26) | ~nonfixed(X_208) | ~on(V_24, W_26, I_23) | object(V_24, I_23) | ~time(I_23) | ~neq(V_24, W_26) | ~a_block(W_26) | ~nonfixed(V_24)))). % 4.22/1.97 tff(c_357, plain, (![Y_16, V_246, X_14, I_245]: (~neq(Y_16, V_246) | ~neq(X_14, V_246) | ~nonfixed(Y_16) | ~on(V_246, Y_16, I_245) | object(V_246, I_245) | ~time(I_245) | ~neq(V_246, Y_16) | ~nonfixed(V_246) | ~source(Y_16, s(I_245)) | ~object(X_14, s(I_245)) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.97 tff(c_317, plain, (![Z_4, X_208, X_2, I_1]: (~neq(Z_4, X_208) | ~neq(X_2, X_208) | ~nonfixed(Z_4) | ~source(Z_4, s(I_1)) | ~object(X_208, s(I_1)) | ~neq(X_208, Z_4) | ~nonfixed(X_208) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.97 tff(c_330, plain, (![Y_16, X_216, X_14, I_215]: (~neq(Y_16, X_216) | ~neq(X_14, X_216) | ~nonfixed(Y_16) | ~destination(Y_16, I_215) | ~object(X_216, I_215) | ~time(I_215) | ~neq(X_216, Y_16) | ~nonfixed(X_216) | ~source(Y_16, s(I_215)) | ~object(X_14, s(I_215)) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.97 tff(c_356, plain, (![Z_4, V_246, X_2, I_1]: (~neq(Z_4, V_246) | ~neq(X_2, V_246) | ~nonfixed(Z_4) | ~on(V_246, Z_4, I_1) | object(V_246, I_1) | ~neq(V_246, Z_4) | ~nonfixed(V_246) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.97 tff(c_328, plain, (![W_26, X_216, V_24, I_23]: (~neq(W_26, X_216) | ~neq(V_24, X_216) | ~nonfixed(W_26) | ~destination(W_26, I_23) | ~object(X_216, I_23) | ~neq(X_216, W_26) | ~nonfixed(X_216) | ~on(V_24, W_26, I_23) | object(V_24, I_23) | ~time(I_23) | ~neq(V_24, W_26) | ~a_block(W_26) | ~nonfixed(V_24)))). % 4.22/1.97 tff(c_218, plain, (![X_164, W_26, I_23, V_24]: (~on(X_164, W_26, s(I_23)) | ~neq(W_26, V_24) | ~neq(X_164, V_24) | ~neq(X_164, W_26) | ~nonfixed(W_26) | ~nonfixed(X_164) | ~on(V_24, W_26, I_23) | object(V_24, I_23) | ~time(I_23) | ~neq(V_24, W_26) | ~a_block(W_26) | ~nonfixed(V_24)))). % 4.22/1.97 tff(c_255, plain, (![W_26, Y_184, I_23, V_24]: (~neq(W_26, Y_184) | ~source(Y_184, s(I_23)) | ~object(V_24, s(I_23)) | ~neq(V_24, Y_184) | ~a_block(Y_184) | ~on(V_24, W_26, I_23) | object(V_24, I_23) | ~time(I_23) | ~neq(V_24, W_26) | ~a_block(W_26) | ~nonfixed(V_24)))). % 4.22/1.97 tff(c_294, plain, (![Y_16, W_198, X_14, I_197]: (~neq(Y_16, W_198) | ~on(X_14, W_198, I_197) | object(X_14, I_197) | ~time(I_197) | ~neq(X_14, W_198) | ~a_block(W_198) | ~source(Y_16, s(I_197)) | ~object(X_14, s(I_197)) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.97 tff(c_271, plain, (![Y_16, X_14, I_187]: (~on(Y_16, X_14, I_187) | object(Y_16, I_187) | ~time(I_187) | ~neq(Y_16, X_14) | ~a_block(X_14) | ~nonfixed(Y_16) | ~source(Y_16, s(I_187)) | ~object(X_14, s(I_187)) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.98 tff(c_329, plain, (![Z_4, X_216, X_2, I_1]: (~neq(Z_4, X_216) | ~neq(X_2, X_216) | ~nonfixed(Z_4) | ~object(X_216, I_1) | ~neq(X_216, Z_4) | ~nonfixed(X_216) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.98 tff(c_256, plain, (![Z_4, Y_184, I_1, X_2]: (~neq(Z_4, Y_184) | ~source(Y_184, s(I_1)) | ~object(X_2, s(I_1)) | ~neq(X_2, Y_184) | ~a_block(Y_184) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.98 tff(c_282, plain, (![Y_16, Z_191, I_190, X_14]: (~neq(Y_16, Z_191) | ~destination(Z_191, I_190) | ~object(X_14, I_190) | ~time(I_190) | ~neq(X_14, Z_191) | ~a_block(Z_191) | ~source(Y_16, s(I_190)) | ~object(X_14, s(I_190)) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.98 tff(c_189, plain, (![X_2, I_1, Z_4]: (~source(X_2, s(I_1)) | ~object(Z_4, s(I_1)) | ~neq(Z_4, X_2) | ~a_block(X_2) | ~nonfixed(Z_4) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.98 tff(c_219, plain, (![X_164, Z_4, I_1, X_2]: (~on(X_164, Z_4, s(I_1)) | ~neq(Z_4, X_2) | ~neq(X_164, X_2) | ~neq(X_164, Z_4) | ~nonfixed(Z_4) | ~nonfixed(X_164) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.98 tff(c_318, plain, (![Y_16, X_208, X_14, I_13]: (~neq(Y_16, X_208) | ~neq(X_14, X_208) | ~nonfixed(Y_16) | ~object(X_208, I_13) | ~neq(X_208, Y_16) | ~nonfixed(X_208) | ~source(Y_16, I_13) | ~object(X_14, I_13) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.98 tff(c_220, plain, (![X_164, Y_16, I_13, X_14]: (~on(X_164, Y_16, I_13) | ~neq(Y_16, X_14) | ~neq(X_164, X_14) | ~neq(X_164, Y_16) | ~nonfixed(Y_16) | ~nonfixed(X_164) | ~source(Y_16, I_13) | ~object(X_14, I_13) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.98 tff(c_208, plain, (![V_24, I_23, W_26]: (object(V_24, s(I_23)) | ~source(W_26, s(I_23)) | ~time(s(I_23)) | ~nonfixed(W_26) | ~on(V_24, W_26, I_23) | object(V_24, I_23) | ~time(I_23) | ~neq(V_24, W_26) | ~a_block(W_26) | ~nonfixed(V_24)))). % 4.22/1.98 tff(c_270, plain, (![Z_4, X_2, I_1]: (~on(Z_4, X_2, I_1) | object(Z_4, I_1) | ~neq(Z_4, X_2) | ~a_block(X_2) | ~nonfixed(Z_4) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.98 tff(c_228, plain, (![V_24, Y_168, I_23, W_26]: (~on(V_24, Y_168, s(I_23)) | ~neq(Y_168, W_26) | ~neq(V_24, Y_168) | ~a_block(Y_168) | ~on(V_24, W_26, I_23) | object(V_24, I_23) | ~time(I_23) | ~neq(V_24, W_26) | ~a_block(W_26) | ~nonfixed(V_24)))). % 4.22/1.98 tff(c_209, plain, (![X_2, I_1, Z_4]: (object(X_2, s(I_1)) | ~source(Z_4, s(I_1)) | ~time(s(I_1)) | ~nonfixed(Z_4) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.98 tff(c_229, plain, (![X_2, Y_168, I_1, Z_4]: (~on(X_2, Y_168, s(I_1)) | ~neq(Y_168, Z_4) | ~neq(X_2, Y_168) | ~a_block(Y_168) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.22/1.98 tff(c_174, plain, (![W_150, V_149, I_151]: (~on(W_150, V_149, s(I_151)) | ~neq(W_150, V_149) | ~a_block(V_149) | ~on(V_149, W_150, I_151) | object(V_149, I_151) | ~time(I_151) | ~neq(V_149, W_150) | ~a_block(W_150) | ~nonfixed(V_149)))). % 4.22/1.98 tff(c_230, plain, (![X_14, Y_168, I_13, Y_16]: (~on(X_14, Y_168, I_13) | ~neq(Y_168, Y_16) | ~neq(X_14, Y_168) | ~a_block(Y_168) | ~source(Y_16, I_13) | ~object(X_14, I_13) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.98 tff(c_113, plain, (![Z_132, X_131, I_133]: (~on(Z_132, X_131, s(I_133)) | ~neq(Z_132, X_131) | ~a_block(X_131) | ~destination(Z_132, I_133) | ~object(X_131, I_133) | ~time(I_133) | ~neq(X_131, Z_132) | ~a_block(Z_132) | ~nonfixed(X_131)))). % 4.22/1.98 tff(c_138, plain, (![X_14, Y_16, I_145]: (on(X_14, Y_16, I_145) | object(X_14, I_145) | ~time(I_145) | ~source(Y_16, s(I_145)) | ~object(X_14, s(I_145)) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.98 tff(c_148, plain, (![X_14, Y_16, I_148]: (on(X_14, Y_16, I_148) | destination(Y_16, I_148) | ~time(I_148) | ~source(Y_16, s(I_148)) | ~object(X_14, s(I_148)) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.98 tff(c_128, plain, (![Y_16, I_142, X_14]: (~source(Y_16, I_142) | ~object(X_14, I_142) | ~time(I_142) | ~source(Y_16, s(I_142)) | ~object(X_14, s(I_142)) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.22/1.98 tff(c_44, plain, (![X_70, Z_76, I_69, Y_74]: (~on(X_70, Z_76, I_69) | ~on(X_70, Y_74, I_69) | ~neq(Y_74, Z_76) | ~neq(X_70, Z_76) | ~a_block(Z_76) | ~neq(X_70, Y_74) | ~a_block(Y_74) | ~nonfixed(X_70)))). % 4.22/1.98 tff(c_42, plain, (![Z_68, Y_66, I_61, X_62]: (~on(Z_68, Y_66, I_61) | ~on(X_62, Y_66, I_61) | ~neq(Y_66, Z_68) | ~neq(X_62, Z_68) | ~nonfixed(Z_68) | ~neq(X_62, Y_66) | ~nonfixed(Y_66) | ~nonfixed(X_62)))). % 4.22/1.98 tff(c_197, plain, (![V_157, Y_10, I_9]: (~on(V_157, Y_10, I_9) | object(V_157, I_9) | ~neq(V_157, Y_10) | ~a_block(Y_10) | ~nonfixed(V_157) | ~source(Y_10, I_9) | ~time(I_9) | ~nonfixed(Y_10)))). % 4.22/1.98 tff(c_175, plain, (![W_150, I_151, V_149]: (~clear(W_150, s(I_151)) | ~nonfixed(W_150) | ~on(V_149, W_150, I_151) | object(V_149, I_151) | ~time(I_151) | ~neq(V_149, W_150) | ~a_block(W_150) | ~nonfixed(V_149)))). % 4.22/1.98 tff(c_95, plain, (![Y_126, X_125, I_127]: (~on(Y_126, X_125, I_127) | ~neq(Y_126, X_125) | ~a_block(X_125) | ~source(Y_126, I_127) | ~object(X_125, I_127) | ~neq(X_125, Y_126) | ~a_block(Y_126) | ~nonfixed(X_125)))). % 4.22/1.98 tff(c_18, plain, (![V_24, W_26, I_23]: (on(V_24, W_26, s(I_23)) | ~on(V_24, W_26, I_23) | object(V_24, I_23) | ~time(I_23) | ~neq(V_24, W_26) | ~a_block(W_26) | ~nonfixed(V_24)))). % 4.22/1.98 tff(c_24, plain, (![V_34, W_36, I_33]: (~on(V_34, W_36, s(I_33)) | on(V_34, W_36, I_33) | destination(W_36, I_33) | ~time(I_33) | ~neq(V_34, W_36) | ~a_block(W_36) | ~nonfixed(V_34)))). % 4.22/1.98 tff(c_22, plain, (![V_30, W_32, I_29]: (~on(V_30, W_32, s(I_29)) | on(V_30, W_32, I_29) | object(V_30, I_29) | ~time(I_29) | ~neq(V_30, W_32) | ~a_block(W_32) | ~nonfixed(V_30)))). % 4.22/1.98 tff(c_4, plain, (![X_6, Y_8, I_5]: (~on(X_6, Y_8, s(I_5)) | ~source(Y_8, I_5) | ~object(X_6, I_5) | ~time(I_5) | ~neq(X_6, Y_8) | ~a_block(Y_8) | ~nonfixed(X_6)))). % 4.22/1.98 tff(c_96, plain, (![Y_126, I_127, X_125]: (~clear(Y_126, I_127) | ~nonfixed(Y_126) | ~source(Y_126, I_127) | ~object(X_125, I_127) | ~neq(X_125, Y_126) | ~a_block(Y_126) | ~nonfixed(X_125)))). % 4.50/1.98 tff(c_115, plain, (![X_131, Z_132, I_133]: (~fixed(X_131) | ~destination(Z_132, I_133) | ~object(X_131, I_133) | ~time(I_133) | ~neq(X_131, Z_132) | ~a_block(Z_132) | ~nonfixed(X_131)))). % 4.50/1.98 tff(c_2, plain, (![X_2, Z_4, I_1]: (on(X_2, Z_4, s(I_1)) | ~destination(Z_4, I_1) | ~object(X_2, I_1) | ~time(I_1) | ~neq(X_2, Z_4) | ~a_block(Z_4) | ~nonfixed(X_2)))). % 4.50/1.98 tff(c_97, plain, (![X_125, Y_126, I_127]: (~fixed(X_125) | ~source(Y_126, I_127) | ~object(X_125, I_127) | ~neq(X_125, Y_126) | ~a_block(Y_126) | ~nonfixed(X_125)))). % 4.50/1.98 tff(c_10, plain, (![X_14, Y_16, I_13]: (on(X_14, Y_16, I_13) | ~source(Y_16, I_13) | ~object(X_14, I_13) | ~neq(X_14, Y_16) | ~a_block(Y_16) | ~nonfixed(X_14)))). % 4.50/1.98 tff(c_38, plain, (![Y_58, X_56, I_55]: (~on(Y_58, X_56, I_55) | ~on(X_56, Y_58, I_55) | ~neq(X_56, Y_58) | ~a_block(Y_58) | ~a_block(X_56)))). % 4.50/1.98 tff(c_20, plain, (![W_28, I_27]: (~clear(W_28, s(I_27)) | clear(W_28, I_27) | source(W_28, I_27) | ~time(I_27) | ~nonfixed(W_28)))). % 4.50/1.98 tff(c_16, plain, (![W_22, I_21]: (clear(W_22, s(I_21)) | ~clear(W_22, I_21) | destination(W_22, I_21) | ~time(I_21) | ~nonfixed(W_22)))). % 4.50/1.98 tff(c_28, plain, (![Y2_44, I_41, Y1_42]: (~source(Y2_44, I_41) | ~source(Y1_42, I_41) | ~neq(Y1_42, Y2_44) | ~a_block(Y2_44) | ~a_block(Y1_42)))). % 4.50/1.98 tff(c_30, plain, (![Z2_48, I_45, Z1_46]: (~destination(Z2_48, I_45) | ~destination(Z1_46, I_45) | ~neq(Z1_46, Z2_48) | ~a_block(Z2_48) | ~a_block(Z1_46)))). % 4.50/1.98 tff(c_26, plain, (![X2_40, I_37, X1_38]: (~object(X2_40, I_37) | ~object(X1_38, I_37) | ~neq(X1_38, X2_40) | ~a_block(X2_40) | ~nonfixed(X1_38)))). % 4.50/1.98 tff(c_62, plain, (![Y_105, I_106]: (~destination(Y_105, I_106) | ~source(Y_105, I_106) | ~time(I_106) | ~nonfixed(Y_105)))). % 4.50/1.98 tff(c_6, plain, (![Y_10, I_9]: (clear(Y_10, s(I_9)) | ~source(Y_10, I_9) | ~time(I_9) | ~nonfixed(Y_10)))). % 4.50/1.98 tff(c_46, plain, (![Y_80, I_77, X_78]: (~clear(Y_80, I_77) | ~on(X_78, Y_80, I_77) | ~nonfixed(Y_80) | ~nonfixed(X_78)))). % 4.50/1.98 tff(c_8, plain, (![Z_12, I_11]: (~clear(Z_12, s(I_11)) | ~destination(Z_12, I_11) | ~time(I_11) | ~nonfixed(Z_12)))). % 4.50/1.98 tff(c_36, plain, (![Y_54, I_53]: (~destination(Y_54, I_53) | ~source(Y_54, I_53) | ~a_block(Y_54)))). % 4.50/1.98 tff(c_12, plain, (![X_18, I_17]: (clear(X_18, I_17) | ~object(X_18, I_17) | ~nonfixed(X_18)))). % 4.50/1.98 tff(c_14, plain, (![Z_20, I_19]: (clear(Z_20, I_19) | ~destination(Z_20, I_19) | ~nonfixed(Z_20)))). % 4.50/1.98 tff(c_32, plain, (![X_50, I_49]: (~source(X_50, I_49) | ~object(X_50, I_49) | ~nonfixed(X_50)))). % 4.50/1.98 tff(c_34, plain, (![X_52, I_51]: (~destination(X_52, I_51) | ~object(X_52, I_51) | ~nonfixed(X_52)))). % 4.50/1.98 tff(c_48, plain, (![Y_84, X_82, I_81]: (~on(Y_84, X_82, I_81) | ~fixed(Y_84) | ~a_block(X_82)))). % 4.50/1.98 tff(c_40, plain, (![X_60, I_59]: (~on(X_60, X_60, I_59) | ~a_block(X_60)))). % 4.50/1.98 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.50/1.98 %------------------------------------------------------------------------------