%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : AGT002+1 : 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:18 EDT 2023 % Result : Theorem 17.22s 3.19s % Output : Proof 34.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : AGT002+1 : TPTP v8.1.2. Bugfixed v3.1.0. % 0.00/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.31 % Computer : n029.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.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Sun Aug 27 17:39:26 EDT 2023 % 0.10/0.32 % CPUTime : % 0.16/0.61 ________ _____ % 0.16/0.61 ___ __ \_________(_)________________________________ % 0.16/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.61 % 0.16/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.61 (2023-06-19) % 0.16/0.61 % 0.16/0.61 (c) Philipp Rümmer, 2009-2023 % 0.16/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.62 Amanda Stjerna. % 0.16/0.62 Free software under BSD-3-Clause. % 0.16/0.62 % 0.16/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.62 % 0.16/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.16/0.63 Running up to 7 provers in parallel. % 0.16/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.16/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.16/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.16/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.16/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.16/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.16/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 9.01/2.21 Prover 4: Preprocessing ... % 9.01/2.27 Prover 1: Preprocessing ... % 9.82/2.29 Prover 5: Preprocessing ... % 9.82/2.29 Prover 0: Preprocessing ... % 9.82/2.29 Prover 2: Preprocessing ... % 9.82/2.29 Prover 6: Preprocessing ... % 9.82/2.31 Prover 3: Preprocessing ... % 16.98/3.14 Prover 2: Constructing countermodel ... % 17.22/3.19 Prover 2: proved (2544ms) % 17.22/3.19 % 17.22/3.19 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.22/3.19 % 17.22/3.20 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 18.56/3.35 Prover 5: Constructing countermodel ... % 18.56/3.35 Prover 5: stopped % 18.56/3.35 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 19.59/3.48 Prover 7: Preprocessing ... % 19.59/3.48 Prover 3: Constructing countermodel ... % 19.59/3.49 Prover 3: stopped % 19.59/3.50 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 19.59/3.50 Prover 6: Constructing countermodel ... % 19.59/3.51 Prover 6: stopped % 19.59/3.52 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 20.42/3.60 Prover 8: Preprocessing ... % 22.79/3.94 Prover 10: Preprocessing ... % 22.79/3.95 Prover 11: Preprocessing ... % 25.64/4.32 Prover 0: Constructing countermodel ... % 25.64/4.33 Prover 0: stopped % 25.64/4.35 Prover 7: Warning: ignoring some quantifiers % 25.64/4.35 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 26.32/4.52 Prover 1: Constructing countermodel ... % 26.32/4.53 Prover 7: Constructing countermodel ... % 26.32/4.59 Prover 13: Preprocessing ... % 28.62/4.73 Prover 4: Constructing countermodel ... % 28.62/4.74 Prover 10: Warning: ignoring some quantifiers % 29.30/4.80 Prover 10: Constructing countermodel ... % 29.30/4.84 Prover 7: Found proof (size 4) % 29.30/4.84 Prover 7: proved (1644ms) % 30.16/4.92 Prover 1: stopped % 30.16/4.95 Prover 10: stopped % 30.16/4.96 Prover 4: stopped % 30.16/4.98 Prover 8: Warning: ignoring some quantifiers % 30.82/5.01 Prover 8: Constructing countermodel ... % 31.39/5.12 Prover 8: stopped % 31.90/5.24 Prover 13: Warning: ignoring some quantifiers % 31.90/5.27 Prover 13: Constructing countermodel ... % 32.80/5.38 Prover 13: stopped % 33.41/5.54 Prover 11: Constructing countermodel ... % 33.71/5.66 Prover 11: stopped % 33.71/5.66 % 33.71/5.66 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.71/5.66 % 33.71/5.66 % SZS output start Proof for theBenchmark % 34.01/5.69 Assumptions after simplification: % 34.01/5.69 --------------------------------- % 34.01/5.69 % 34.01/5.69 (event_213) % 34.01/5.70 $i(sufferterragovernment) & $i(christiansufferterrahumanitarianorganization) & % 34.01/5.70 $i(n6) & $i(towna) & ~ % 34.01/5.70 accept_team(christiansufferterrahumanitarianorganization, % 34.01/5.70 sufferterragovernment, towna, n6) % 34.01/5.70 % 34.01/5.70 (query_2) % 34.01/5.70 $i(sufferterragovernment) & $i(christiansufferterrahumanitarianorganization) & % 34.01/5.70 $i(n6) & $i(towna) & accept_team(christiansufferterrahumanitarianorganization, % 34.01/5.70 sufferterragovernment, towna, n6) % 34.01/5.70 % 34.01/5.70 Further assumptions not needed in the proof: % 34.01/5.70 -------------------------------------------- % 34.01/5.71 a1_1, a1_2, a1_3, a1_4, a1_5, a1_6, a1_7, a2_1, a2_10, a2_11, a2_12, a2_13, % 34.01/5.71 a2_2, a2_3, a2_4, a2_5, a2_6, a2_7, a2_8, a2_9, event_1, event_10, event_100, % 34.01/5.71 event_101, event_102, event_103, event_104, event_105, event_106, event_107, % 34.01/5.71 event_108, event_109, event_11, event_110, event_111, event_112, event_113, % 34.01/5.71 event_114, event_115, event_116, event_117, event_118, event_119, event_12, % 34.01/5.71 event_120, event_121, event_122, event_123, event_124, event_125, event_126, % 34.01/5.71 event_127, event_128, event_129, event_13, event_130, event_131, event_132, % 34.01/5.71 event_133, event_134, event_135, event_136, event_137, event_138, event_139, % 34.01/5.71 event_14, event_140, event_141, event_142, event_143, event_144, event_145, % 34.01/5.71 event_146, event_147, event_148, event_149, event_15, event_150, event_151, % 34.01/5.71 event_152, event_153, event_154, event_155, event_156, event_157, event_158, % 34.01/5.71 event_159, event_16, event_160, event_161, event_162, event_163, event_164, % 34.01/5.71 event_165, event_166, event_167, event_168, event_169, event_17, event_170, % 34.01/5.71 event_171, event_172, event_173, event_174, event_175, event_176, event_177, % 34.01/5.71 event_178, event_179, event_18, event_180, event_181, event_182, event_183, % 34.01/5.71 event_184, event_185, event_186, event_187, event_188, event_189, event_19, % 34.01/5.71 event_190, event_191, event_192, event_193, event_194, event_195, event_196, % 34.01/5.71 event_197, event_198, event_199, event_2, event_20, event_200, event_201, % 34.01/5.71 event_202, event_203, event_204, event_205, event_206, event_207, event_208, % 34.01/5.71 event_209, event_21, event_210, event_211, event_212, event_214, event_215, % 34.01/5.71 event_216, event_217, event_218, event_219, event_22, event_220, event_221, % 34.01/5.71 event_222, event_223, event_224, event_225, event_226, event_227, event_228, % 34.01/5.71 event_229, event_23, event_230, event_231, event_232, event_233, event_234, % 34.01/5.71 event_235, event_236, event_237, event_238, event_239, event_24, event_240, % 34.01/5.71 event_241, event_242, event_243, event_244, event_245, event_246, event_247, % 34.01/5.71 event_248, event_249, event_25, event_26, event_27, event_28, event_29, event_3, % 34.01/5.71 event_30, event_31, event_32, event_33, event_34, event_35, event_36, event_37, % 34.01/5.71 event_38, event_39, event_4, event_40, event_41, event_42, event_43, event_44, % 34.01/5.71 event_45, event_46, event_47, event_48, event_49, event_5, event_50, event_51, % 34.01/5.71 event_52, event_53, event_54, event_55, event_56, event_57, event_58, event_59, % 34.01/5.71 event_6, event_60, event_61, event_62, event_63, event_64, event_65, event_66, % 34.01/5.71 event_67, event_68, event_69, event_7, event_70, event_71, event_72, event_73, % 34.01/5.71 event_74, event_75, event_76, event_77, event_78, event_79, event_8, event_80, % 34.01/5.71 event_81, event_82, event_83, event_84, event_85, event_86, event_87, event_88, % 34.01/5.71 event_89, event_9, event_90, event_91, event_92, event_93, event_94, event_95, % 34.01/5.71 event_96, event_97, event_98, event_99, less_entry_point_neg_neg, % 34.01/5.71 less_entry_point_neg_pos, less_entry_point_pos_pos, less_or_equal, % 34.01/5.71 less_property, less_successor, rdn0, rdn1, rdn10, rdn100, rdn101, rdn102, % 34.01/5.71 rdn103, rdn104, rdn105, rdn106, rdn107, rdn108, rdn109, rdn11, rdn110, rdn111, % 34.01/5.71 rdn112, rdn113, rdn114, rdn115, rdn116, rdn117, rdn118, rdn119, rdn12, rdn120, % 34.01/5.71 rdn121, rdn122, rdn123, rdn124, rdn125, rdn126, rdn127, rdn13, rdn14, rdn15, % 34.01/5.71 rdn16, rdn17, rdn18, rdn19, rdn2, rdn20, rdn21, rdn22, rdn23, rdn24, rdn25, % 34.01/5.71 rdn26, rdn27, rdn28, rdn29, rdn3, rdn30, rdn31, rdn32, rdn33, rdn34, rdn35, % 34.01/5.71 rdn36, rdn37, rdn38, rdn39, rdn4, rdn40, rdn41, rdn42, rdn43, rdn44, rdn45, % 34.01/5.71 rdn46, rdn47, rdn48, rdn49, rdn5, rdn50, rdn51, rdn52, rdn53, rdn54, rdn55, % 34.01/5.71 rdn56, rdn57, rdn58, rdn59, rdn6, rdn60, rdn61, rdn62, rdn63, rdn64, rdn65, % 34.01/5.71 rdn66, rdn67, rdn68, rdn69, rdn7, rdn70, rdn71, rdn72, rdn73, rdn74, rdn75, % 34.01/5.71 rdn76, rdn77, rdn78, rdn79, rdn8, rdn80, rdn81, rdn82, rdn83, rdn84, rdn85, % 34.01/5.71 rdn86, rdn87, rdn88, rdn89, rdn9, rdn90, rdn91, rdn92, rdn93, rdn94, rdn95, % 34.01/5.71 rdn96, rdn97, rdn98, rdn99, rdn_digit1, rdn_digit2, rdn_digit3, rdn_digit4, % 34.01/5.71 rdn_digit5, rdn_digit6, rdn_digit7, rdn_digit8, rdn_digit9, % 34.01/5.71 rdn_extra_digits_positive_less, rdn_non_zero_by_digit, % 34.01/5.71 rdn_non_zero_by_structure, rdn_positive_less01, rdn_positive_less12, % 34.01/5.71 rdn_positive_less23, rdn_positive_less34, rdn_positive_less45, % 34.01/5.71 rdn_positive_less56, rdn_positive_less67, rdn_positive_less78, % 34.01/5.71 rdn_positive_less89, rdn_positive_less_multi_digit_high, % 34.01/5.71 rdn_positive_less_multi_digit_low, rdn_positive_less_transitivity, rdnn1, % 34.01/5.71 rdnn10, rdnn100, rdnn101, rdnn102, rdnn103, rdnn104, rdnn105, rdnn106, rdnn107, % 34.01/5.71 rdnn108, rdnn109, rdnn11, rdnn110, rdnn111, rdnn112, rdnn113, rdnn114, rdnn115, % 34.01/5.71 rdnn116, rdnn117, rdnn118, rdnn119, rdnn12, rdnn120, rdnn121, rdnn122, rdnn123, % 34.01/5.71 rdnn124, rdnn125, rdnn126, rdnn127, rdnn128, rdnn13, rdnn14, rdnn15, rdnn16, % 34.01/5.71 rdnn17, rdnn18, rdnn19, rdnn2, rdnn20, rdnn21, rdnn22, rdnn23, rdnn24, rdnn25, % 34.01/5.71 rdnn26, rdnn27, rdnn28, rdnn29, rdnn3, rdnn30, rdnn31, rdnn32, rdnn33, rdnn34, % 34.01/5.71 rdnn35, rdnn36, rdnn37, rdnn38, rdnn39, rdnn4, rdnn40, rdnn41, rdnn42, rdnn43, % 34.01/5.71 rdnn44, rdnn45, rdnn46, rdnn47, rdnn48, rdnn49, rdnn5, rdnn50, rdnn51, rdnn52, % 34.01/5.71 rdnn53, rdnn54, rdnn55, rdnn56, rdnn57, rdnn58, rdnn59, rdnn6, rdnn60, rdnn61, % 34.01/5.71 rdnn62, rdnn63, rdnn64, rdnn65, rdnn66, rdnn67, rdnn68, rdnn69, rdnn7, rdnn70, % 34.01/5.71 rdnn71, rdnn72, rdnn73, rdnn74, rdnn75, rdnn76, rdnn77, rdnn78, rdnn79, rdnn8, % 34.01/5.71 rdnn80, rdnn81, rdnn82, rdnn83, rdnn84, rdnn85, rdnn86, rdnn87, rdnn88, rdnn89, % 34.01/5.71 rdnn9, rdnn90, rdnn91, rdnn92, rdnn93, rdnn94, rdnn95, rdnn96, rdnn97, rdnn98, % 34.01/5.71 rdnn99 % 34.01/5.71 % 34.01/5.71 Those formulas are unsatisfiable: % 34.01/5.71 --------------------------------- % 34.01/5.71 % 34.01/5.71 Begin of proof % 34.01/5.71 | % 34.01/5.71 | ALPHA: (event_213) implies: % 34.01/5.71 | (1) ~ accept_team(christiansufferterrahumanitarianorganization, % 34.01/5.71 | sufferterragovernment, towna, n6) % 34.01/5.71 | % 34.01/5.71 | ALPHA: (query_2) implies: % 34.01/5.71 | (2) accept_team(christiansufferterrahumanitarianorganization, % 34.01/5.71 | sufferterragovernment, towna, n6) % 34.01/5.71 | % 34.01/5.72 | PRED_UNIFY: (1), (2) imply: % 34.01/5.72 | (3) $false % 34.01/5.72 | % 34.01/5.72 | CLOSE: (3) is inconsistent. % 34.01/5.72 | % 34.01/5.72 End of proof % 34.01/5.72 % SZS output end Proof for theBenchmark % 34.01/5.72 % 34.01/5.72 5102ms %------------------------------------------------------------------------------