%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : AGT002+2 : TPTP v8.1.2. Bugfixed v3.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%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 Aug 30 15:55:19 EDT 2023 % Result : Theorem 15.53s 2.88s % Output : Proof 32.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : AGT002+2 : TPTP v8.1.2. Bugfixed v3.1.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n029.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Aug 27 17:20:26 EDT 2023 % 0.19/0.34 % CPUTime : % 0.19/0.61 ________ _____ % 0.19/0.61 ___ __ \_________(_)________________________________ % 0.19/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.61 % 0.19/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.61 (2023-06-19) % 0.19/0.61 % 0.19/0.61 (c) Philipp Rümmer, 2009-2023 % 0.19/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.61 Amanda Stjerna. % 0.19/0.61 Free software under BSD-3-Clause. % 0.19/0.61 % 0.19/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.61 % 0.19/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.62 Running up to 7 provers in parallel. % 0.19/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.62/2.04 Prover 4: Preprocessing ... % 9.62/2.04 Prover 1: Preprocessing ... % 9.62/2.07 Prover 6: Preprocessing ... % 9.62/2.07 Prover 2: Preprocessing ... % 9.62/2.07 Prover 5: Preprocessing ... % 9.62/2.07 Prover 3: Preprocessing ... % 9.62/2.07 Prover 0: Preprocessing ... % 14.88/2.83 Prover 2: Constructing countermodel ... % 15.53/2.87 Prover 2: proved (2232ms) % 15.53/2.87 % 15.53/2.88 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.53/2.88 % 15.53/2.88 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 15.83/2.89 Prover 5: Constructing countermodel ... % 15.83/2.89 Prover 5: stopped % 15.83/2.91 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 15.83/3.04 Prover 6: Constructing countermodel ... % 15.83/3.05 Prover 3: Constructing countermodel ... % 15.83/3.05 Prover 3: stopped % 15.83/3.06 Prover 6: stopped % 15.83/3.07 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 15.83/3.08 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 18.52/3.25 Prover 7: Preprocessing ... % 18.75/3.30 Prover 8: Preprocessing ... % 19.13/3.39 Prover 10: Preprocessing ... % 20.06/3.47 Prover 11: Preprocessing ... % 20.77/3.57 Prover 0: Constructing countermodel ... % 20.77/3.57 Prover 0: stopped % 20.77/3.57 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 22.48/3.81 Prover 13: Preprocessing ... % 25.74/4.25 Prover 10: Warning: ignoring some quantifiers % 25.74/4.30 Prover 1: Constructing countermodel ... % 25.74/4.31 Prover 10: Constructing countermodel ... % 25.74/4.35 Prover 7: Warning: ignoring some quantifiers % 26.47/4.38 Prover 7: Constructing countermodel ... % 28.01/4.53 Prover 4: Constructing countermodel ... % 29.15/4.71 Prover 7: Found proof (size 4) % 29.15/4.71 Prover 10: Found proof (size 4) % 29.15/4.71 Prover 7: proved (1838ms) % 29.15/4.71 Prover 10: proved (1642ms) % 29.67/4.76 Prover 4: stopped % 29.87/4.77 Prover 8: Warning: ignoring some quantifiers % 29.87/4.77 Prover 1: stopped % 29.87/4.78 Prover 8: Constructing countermodel ... % 29.87/4.79 Prover 13: Warning: ignoring some quantifiers % 29.87/4.82 Prover 13: Constructing countermodel ... % 30.89/4.93 Prover 8: stopped % 30.89/4.97 Prover 13: stopped % 31.97/5.19 Prover 11: Constructing countermodel ... % 32.21/5.30 Prover 11: stopped % 32.21/5.30 % 32.21/5.30 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.21/5.30 % 32.21/5.31 % SZS output start Proof for theBenchmark % 32.50/5.36 Assumptions after simplification: % 32.50/5.36 --------------------------------- % 32.50/5.36 % 32.50/5.36 (event_213) % 32.72/5.37 $i(sufferterragovernment) & $i(christiansufferterrahumanitarianorganization) & % 32.72/5.37 $i(n6) & $i(towna) & ~ % 32.72/5.37 accept_team(christiansufferterrahumanitarianorganization, % 32.72/5.37 sufferterragovernment, towna, n6) % 32.72/5.37 % 32.72/5.37 (query_2) % 32.72/5.37 $i(sufferterragovernment) & $i(christiansufferterrahumanitarianorganization) & % 32.72/5.37 $i(n6) & $i(towna) & accept_team(christiansufferterrahumanitarianorganization, % 32.72/5.37 sufferterragovernment, towna, n6) % 32.72/5.37 % 32.72/5.37 Further assumptions not needed in the proof: % 32.72/5.37 -------------------------------------------- % 32.72/5.37 a1_1, a1_2, a1_3, a1_4, a1_5, a1_6, a1_7, a2_1, a2_10, a2_11, a2_12, a2_13, % 32.72/5.37 a2_2, a2_3, a2_4, a2_5, a2_6, a2_7, a2_8, a2_9, deduced_1, deduced_10, % 32.72/5.38 deduced_100, deduced_101, deduced_102, deduced_103, deduced_104, deduced_105, % 32.72/5.38 deduced_106, deduced_107, deduced_108, deduced_109, deduced_11, deduced_110, % 32.72/5.38 deduced_111, deduced_112, deduced_113, deduced_114, deduced_115, deduced_116, % 32.72/5.38 deduced_117, deduced_118, deduced_119, deduced_12, deduced_120, deduced_121, % 32.72/5.38 deduced_122, deduced_123, deduced_124, deduced_125, deduced_126, deduced_127, % 32.72/5.38 deduced_128, deduced_129, deduced_13, deduced_130, deduced_131, deduced_132, % 32.72/5.38 deduced_133, deduced_134, deduced_135, deduced_136, deduced_137, deduced_138, % 32.72/5.38 deduced_139, deduced_14, deduced_140, deduced_141, deduced_142, deduced_143, % 32.72/5.38 deduced_144, deduced_145, deduced_146, deduced_147, deduced_148, deduced_149, % 32.72/5.38 deduced_15, deduced_150, deduced_151, deduced_152, deduced_153, deduced_154, % 32.72/5.38 deduced_155, deduced_156, deduced_157, deduced_158, deduced_159, deduced_16, % 32.72/5.38 deduced_160, deduced_161, deduced_162, deduced_163, deduced_164, deduced_165, % 32.72/5.38 deduced_166, deduced_167, deduced_168, deduced_169, deduced_17, deduced_170, % 32.72/5.38 deduced_171, deduced_172, deduced_173, deduced_174, deduced_175, deduced_176, % 32.72/5.38 deduced_177, deduced_178, deduced_179, deduced_18, deduced_180, deduced_181, % 32.72/5.38 deduced_182, deduced_183, deduced_184, deduced_185, deduced_186, deduced_187, % 32.72/5.38 deduced_188, deduced_189, deduced_19, deduced_190, deduced_191, deduced_192, % 32.72/5.38 deduced_193, deduced_194, deduced_195, deduced_196, deduced_197, deduced_198, % 32.72/5.38 deduced_199, deduced_2, deduced_20, deduced_200, deduced_201, deduced_202, % 32.72/5.38 deduced_203, deduced_204, deduced_205, deduced_206, deduced_207, deduced_208, % 32.72/5.38 deduced_209, deduced_21, deduced_210, deduced_211, deduced_212, deduced_213, % 32.72/5.38 deduced_214, deduced_215, deduced_216, deduced_217, deduced_218, deduced_219, % 32.72/5.38 deduced_22, deduced_220, deduced_221, deduced_222, deduced_223, deduced_224, % 32.72/5.38 deduced_225, deduced_226, deduced_227, deduced_228, deduced_229, deduced_23, % 32.72/5.38 deduced_230, deduced_231, deduced_232, deduced_233, deduced_234, deduced_235, % 32.72/5.38 deduced_236, deduced_237, deduced_238, deduced_239, deduced_24, deduced_240, % 32.72/5.38 deduced_241, deduced_242, deduced_243, deduced_244, deduced_245, deduced_246, % 32.72/5.38 deduced_247, deduced_248, deduced_249, deduced_25, deduced_250, deduced_251, % 32.72/5.38 deduced_252, deduced_253, deduced_254, deduced_255, deduced_256, deduced_257, % 32.72/5.38 deduced_258, deduced_259, deduced_26, deduced_260, deduced_261, deduced_262, % 32.72/5.38 deduced_263, deduced_264, deduced_265, deduced_266, deduced_267, deduced_268, % 32.72/5.38 deduced_269, deduced_27, deduced_270, deduced_271, deduced_272, deduced_273, % 32.72/5.38 deduced_274, deduced_275, deduced_276, deduced_277, deduced_278, deduced_279, % 32.72/5.38 deduced_28, deduced_280, deduced_281, deduced_282, deduced_283, deduced_284, % 32.72/5.38 deduced_285, deduced_286, deduced_287, deduced_288, deduced_289, deduced_29, % 32.72/5.38 deduced_290, deduced_291, deduced_292, deduced_293, deduced_294, deduced_295, % 32.72/5.38 deduced_296, deduced_297, deduced_298, deduced_299, deduced_3, deduced_30, % 32.72/5.38 deduced_300, deduced_301, deduced_302, deduced_303, deduced_304, deduced_305, % 32.72/5.38 deduced_306, deduced_307, deduced_308, deduced_309, deduced_31, deduced_310, % 32.72/5.38 deduced_311, deduced_312, deduced_313, deduced_314, deduced_315, deduced_316, % 32.72/5.38 deduced_317, deduced_318, deduced_319, deduced_32, deduced_320, deduced_321, % 32.72/5.38 deduced_322, deduced_323, deduced_324, deduced_325, deduced_326, deduced_327, % 32.72/5.38 deduced_328, deduced_329, deduced_33, deduced_330, deduced_331, deduced_332, % 32.72/5.38 deduced_333, deduced_334, deduced_335, deduced_336, deduced_337, deduced_338, % 32.72/5.38 deduced_339, deduced_34, deduced_340, deduced_341, deduced_342, deduced_343, % 32.72/5.38 deduced_344, deduced_345, deduced_346, deduced_347, deduced_348, deduced_349, % 32.72/5.38 deduced_35, deduced_350, deduced_351, deduced_352, deduced_353, deduced_354, % 32.72/5.38 deduced_355, deduced_356, deduced_357, deduced_358, deduced_359, deduced_36, % 32.72/5.38 deduced_360, deduced_361, deduced_362, deduced_363, deduced_364, deduced_365, % 32.72/5.38 deduced_366, deduced_367, deduced_37, deduced_38, deduced_39, deduced_4, % 32.72/5.38 deduced_40, deduced_41, deduced_42, deduced_43, deduced_44, deduced_45, % 32.72/5.38 deduced_46, deduced_47, deduced_48, deduced_49, deduced_5, deduced_50, % 32.72/5.38 deduced_51, deduced_52, deduced_53, deduced_54, deduced_55, deduced_56, % 32.72/5.38 deduced_57, deduced_58, deduced_59, deduced_6, deduced_60, deduced_61, % 32.72/5.38 deduced_62, deduced_63, deduced_64, deduced_65, deduced_66, deduced_67, % 32.72/5.38 deduced_68, deduced_69, deduced_7, deduced_70, deduced_71, deduced_72, % 32.72/5.38 deduced_73, deduced_74, deduced_75, deduced_76, deduced_77, deduced_78, % 32.72/5.38 deduced_79, deduced_8, deduced_80, deduced_81, deduced_82, deduced_83, % 32.72/5.38 deduced_84, deduced_85, deduced_86, deduced_87, deduced_88, deduced_89, % 32.72/5.38 deduced_9, deduced_90, deduced_91, deduced_92, deduced_93, deduced_94, % 32.72/5.38 deduced_95, deduced_96, deduced_97, deduced_98, deduced_99, event_1, event_10, % 32.72/5.38 event_100, event_101, event_102, event_103, event_104, event_105, event_106, % 32.72/5.38 event_107, event_108, event_109, event_11, event_110, event_111, event_112, % 32.72/5.38 event_113, event_114, event_115, event_116, event_117, event_118, event_119, % 32.72/5.38 event_12, event_120, event_121, event_122, event_123, event_124, event_125, % 32.72/5.38 event_126, event_127, event_128, event_129, event_13, event_130, event_131, % 32.72/5.38 event_132, event_133, event_134, event_135, event_136, event_137, event_138, % 32.72/5.38 event_139, event_14, event_140, event_141, event_142, event_143, event_144, % 32.72/5.38 event_145, event_146, event_147, event_148, event_149, event_15, event_150, % 32.72/5.38 event_151, event_152, event_153, event_154, event_155, event_156, event_157, % 32.72/5.38 event_158, event_159, event_16, event_160, event_161, event_162, event_163, % 32.72/5.38 event_164, event_165, event_166, event_167, event_168, event_169, event_17, % 32.72/5.38 event_170, event_171, event_172, event_173, event_174, event_175, event_176, % 32.72/5.38 event_177, event_178, event_179, event_18, event_180, event_181, event_182, % 32.72/5.38 event_183, event_184, event_185, event_186, event_187, event_188, event_189, % 32.72/5.38 event_19, event_190, event_191, event_192, event_193, event_194, event_195, % 32.72/5.38 event_196, event_197, event_198, event_199, event_2, event_20, event_200, % 32.72/5.38 event_201, event_202, event_203, event_204, event_205, event_206, event_207, % 32.72/5.38 event_208, event_209, event_21, event_210, event_211, event_212, event_214, % 32.72/5.38 event_215, event_216, event_217, event_218, event_219, event_22, event_220, % 32.72/5.38 event_221, event_222, event_223, event_224, event_225, event_226, event_227, % 32.72/5.38 event_228, event_229, event_23, event_230, event_231, event_232, event_233, % 32.72/5.38 event_234, event_235, event_236, event_237, event_238, event_239, event_24, % 32.72/5.38 event_240, event_241, event_242, event_243, event_244, event_245, event_246, % 32.72/5.38 event_247, event_248, event_249, event_25, event_26, event_27, event_28, % 32.72/5.38 event_29, event_3, event_30, event_31, event_32, event_33, event_34, event_35, % 32.72/5.38 event_36, event_37, event_38, event_39, event_4, event_40, event_41, event_42, % 32.72/5.38 event_43, event_44, event_45, event_46, event_47, event_48, event_49, event_5, % 32.72/5.38 event_50, event_51, event_52, event_53, event_54, event_55, event_56, event_57, % 32.72/5.38 event_58, event_59, event_6, event_60, event_61, event_62, event_63, event_64, % 32.72/5.38 event_65, event_66, event_67, event_68, event_69, event_7, event_70, event_71, % 32.72/5.38 event_72, event_73, event_74, event_75, event_76, event_77, event_78, event_79, % 32.72/5.38 event_8, event_80, event_81, event_82, event_83, event_84, event_85, event_86, % 32.72/5.38 event_87, event_88, event_89, event_9, event_90, event_91, event_92, event_93, % 32.72/5.38 event_94, event_95, event_96, event_97, event_98, event_99, % 32.72/5.38 less_entry_point_neg_neg, less_entry_point_neg_pos, less_entry_point_pos_pos, % 32.72/5.38 less_or_equal, less_property, less_successor, rdn0, rdn1, rdn10, rdn100, rdn101, % 32.72/5.38 rdn102, rdn103, rdn104, rdn105, rdn106, rdn107, rdn108, rdn109, rdn11, rdn110, % 32.72/5.38 rdn111, rdn112, rdn113, rdn114, rdn115, rdn116, rdn117, rdn118, rdn119, rdn12, % 32.72/5.38 rdn120, rdn121, rdn122, rdn123, rdn124, rdn125, rdn126, rdn127, rdn13, rdn14, % 32.72/5.38 rdn15, rdn16, rdn17, rdn18, rdn19, rdn2, rdn20, rdn21, rdn22, rdn23, rdn24, % 32.72/5.38 rdn25, rdn26, rdn27, rdn28, rdn29, rdn3, rdn30, rdn31, rdn32, rdn33, rdn34, % 32.72/5.38 rdn35, rdn36, rdn37, rdn38, rdn39, rdn4, rdn40, rdn41, rdn42, rdn43, rdn44, % 32.72/5.38 rdn45, rdn46, rdn47, rdn48, rdn49, rdn5, rdn50, rdn51, rdn52, rdn53, rdn54, % 32.72/5.38 rdn55, rdn56, rdn57, rdn58, rdn59, rdn6, rdn60, rdn61, rdn62, rdn63, rdn64, % 32.72/5.38 rdn65, rdn66, rdn67, rdn68, rdn69, rdn7, rdn70, rdn71, rdn72, rdn73, rdn74, % 32.72/5.38 rdn75, rdn76, rdn77, rdn78, rdn79, rdn8, rdn80, rdn81, rdn82, rdn83, rdn84, % 32.72/5.38 rdn85, rdn86, rdn87, rdn88, rdn89, rdn9, rdn90, rdn91, rdn92, rdn93, rdn94, % 32.72/5.38 rdn95, rdn96, rdn97, rdn98, rdn99, rdn_digit1, rdn_digit2, rdn_digit3, % 32.72/5.38 rdn_digit4, rdn_digit5, rdn_digit6, rdn_digit7, rdn_digit8, rdn_digit9, % 32.72/5.38 rdn_extra_digits_positive_less, rdn_non_zero_by_digit, % 32.72/5.38 rdn_non_zero_by_structure, rdn_positive_less01, rdn_positive_less12, % 32.72/5.38 rdn_positive_less23, rdn_positive_less34, rdn_positive_less45, % 32.72/5.38 rdn_positive_less56, rdn_positive_less67, rdn_positive_less78, % 32.72/5.38 rdn_positive_less89, rdn_positive_less_multi_digit_high, % 32.72/5.38 rdn_positive_less_multi_digit_low, rdn_positive_less_transitivity, rdnn1, % 32.72/5.38 rdnn10, rdnn100, rdnn101, rdnn102, rdnn103, rdnn104, rdnn105, rdnn106, rdnn107, % 32.72/5.38 rdnn108, rdnn109, rdnn11, rdnn110, rdnn111, rdnn112, rdnn113, rdnn114, rdnn115, % 32.72/5.38 rdnn116, rdnn117, rdnn118, rdnn119, rdnn12, rdnn120, rdnn121, rdnn122, rdnn123, % 32.72/5.38 rdnn124, rdnn125, rdnn126, rdnn127, rdnn128, rdnn13, rdnn14, rdnn15, rdnn16, % 32.72/5.38 rdnn17, rdnn18, rdnn19, rdnn2, rdnn20, rdnn21, rdnn22, rdnn23, rdnn24, rdnn25, % 32.72/5.38 rdnn26, rdnn27, rdnn28, rdnn29, rdnn3, rdnn30, rdnn31, rdnn32, rdnn33, rdnn34, % 32.72/5.38 rdnn35, rdnn36, rdnn37, rdnn38, rdnn39, rdnn4, rdnn40, rdnn41, rdnn42, rdnn43, % 32.72/5.38 rdnn44, rdnn45, rdnn46, rdnn47, rdnn48, rdnn49, rdnn5, rdnn50, rdnn51, rdnn52, % 32.72/5.38 rdnn53, rdnn54, rdnn55, rdnn56, rdnn57, rdnn58, rdnn59, rdnn6, rdnn60, rdnn61, % 32.72/5.38 rdnn62, rdnn63, rdnn64, rdnn65, rdnn66, rdnn67, rdnn68, rdnn69, rdnn7, rdnn70, % 32.72/5.38 rdnn71, rdnn72, rdnn73, rdnn74, rdnn75, rdnn76, rdnn77, rdnn78, rdnn79, rdnn8, % 32.72/5.38 rdnn80, rdnn81, rdnn82, rdnn83, rdnn84, rdnn85, rdnn86, rdnn87, rdnn88, rdnn89, % 32.72/5.38 rdnn9, rdnn90, rdnn91, rdnn92, rdnn93, rdnn94, rdnn95, rdnn96, rdnn97, rdnn98, % 32.72/5.38 rdnn99 % 32.72/5.38 % 32.72/5.38 Those formulas are unsatisfiable: % 32.72/5.38 --------------------------------- % 32.72/5.38 % 32.72/5.38 Begin of proof % 32.72/5.38 | % 32.72/5.38 | ALPHA: (event_213) implies: % 32.72/5.39 | (1) ~ accept_team(christiansufferterrahumanitarianorganization, % 32.72/5.39 | sufferterragovernment, towna, n6) % 32.72/5.39 | % 32.72/5.39 | ALPHA: (query_2) implies: % 32.72/5.39 | (2) accept_team(christiansufferterrahumanitarianorganization, % 32.72/5.39 | sufferterragovernment, towna, n6) % 32.72/5.39 | % 32.72/5.39 | PRED_UNIFY: (1), (2) imply: % 32.72/5.39 | (3) $false % 32.72/5.39 | % 32.72/5.39 | CLOSE: (3) is inconsistent. % 32.72/5.39 | % 32.72/5.39 End of proof % 32.72/5.39 % SZS output end Proof for theBenchmark % 32.72/5.39 % 32.72/5.39 4779ms %------------------------------------------------------------------------------