%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : MSC019+1 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n017.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 : Thu Aug 31 09:26:48 EDT 2023 % Result : Theorem 19.90s 3.36s % Output : Proof 25.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : MSC019+1 : TPTP v8.1.2. Released v4.0.0. % 0.10/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n017.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Aug 24 13:12:39 EDT 2023 % 0.13/0.34 % CPUTime : % 0.19/0.60 ________ _____ % 0.19/0.60 ___ __ \_________(_)________________________________ % 0.19/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.60 % 0.19/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.60 (2023-06-19) % 0.19/0.60 % 0.19/0.60 (c) Philipp Rümmer, 2009-2023 % 0.19/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.60 Amanda Stjerna. % 0.19/0.60 Free software under BSD-3-Clause. % 0.19/0.60 % 0.19/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.60 % 0.19/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.62 Running up to 7 provers in parallel. % 0.19/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.47/1.46 Prover 1: Preprocessing ... % 5.47/1.46 Prover 4: Preprocessing ... % 5.47/1.49 Prover 2: Preprocessing ... % 5.47/1.49 Prover 6: Preprocessing ... % 5.47/1.49 Prover 3: Preprocessing ... % 5.47/1.49 Prover 0: Preprocessing ... % 5.47/1.50 Prover 5: Preprocessing ... % 8.63/1.95 Prover 2: Constructing countermodel ... % 8.63/1.95 Prover 5: Constructing countermodel ... % 10.62/2.17 Prover 3: Constructing countermodel ... % 10.62/2.18 Prover 0: Proving ... % 10.62/2.18 Prover 6: Constructing countermodel ... % 14.57/2.70 Prover 4: Constructing countermodel ... % 14.57/2.71 Prover 1: Constructing countermodel ... % 19.63/3.36 Prover 3: proved (2733ms) % 19.90/3.36 % 19.90/3.36 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 19.90/3.36 % 19.90/3.36 Prover 6: stopped % 19.90/3.36 Prover 5: stopped % 19.90/3.36 Prover 2: stopped % 19.90/3.39 Prover 0: stopped % 19.90/3.39 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 19.90/3.39 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 19.90/3.39 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 19.90/3.39 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 19.90/3.39 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 21.44/3.61 Prover 8: Preprocessing ... % 21.44/3.61 Prover 10: Preprocessing ... % 21.44/3.63 Prover 7: Preprocessing ... % 21.44/3.64 Prover 13: Preprocessing ... % 22.70/3.78 Prover 11: Preprocessing ... % 22.70/3.87 Prover 1: Found proof (size 18) % 22.70/3.87 Prover 1: proved (3242ms) % 22.70/3.87 Prover 4: stopped % 22.70/3.89 Prover 11: stopped % 22.70/3.90 Prover 7: Constructing countermodel ... % 23.83/3.97 Prover 10: Constructing countermodel ... % 24.34/3.97 Prover 13: Constructing countermodel ... % 24.34/3.98 Prover 7: stopped % 24.34/4.03 Prover 10: stopped % 24.34/4.03 Prover 13: stopped % 24.34/4.05 Prover 8: Warning: ignoring some quantifiers % 24.34/4.06 Prover 8: Constructing countermodel ... % 24.98/4.09 Prover 8: stopped % 24.98/4.10 % 24.98/4.10 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 24.98/4.10 % 24.98/4.10 % SZS output start Proof for theBenchmark % 25.12/4.13 Assumptions after simplification: % 25.12/4.13 --------------------------------- % 25.12/4.13 % 25.12/4.13 (axiom1) % 25.15/4.16 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 25.15/4.16 (s_contains(v0, v2) = v3) | ~ (s_contains(v0, v1) = 0) | ~ $i(v2) | ~ % 25.15/4.16 $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_contains(v1, v2) = v4)) % 25.15/4.16 % 25.15/4.16 (kb18) % 25.15/4.16 s_contains(s_g019, s_g013) = 0 & $i(s_g013) & $i(s_g019) % 25.15/4.16 % 25.15/4.16 (kb451) % 25.15/4.16 s_contains(s_g419, s_g013) = 0 & $i(s_g419) & $i(s_g013) % 25.15/4.16 % 25.15/4.16 (kb74) % 25.15/4.16 s_contains(s_g013, s_MX) = 0 & $i(s_MX) & $i(s_g013) % 25.15/4.16 % 25.15/4.16 (mexico_in_america_1) % 25.15/4.16 $i(s_MX) & $i(s_g019) & ? [v0: int] : ( ~ (v0 = 0) & s_contains(s_g019, s_MX) % 25.15/4.16 = v0) % 25.15/4.16 % 25.15/4.16 (function-axioms) % 25.15/4.16 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 25.15/4.16 [v3: $i] : (v1 = v0 | ~ (s_partOf(v3, v2) = v1) | ~ (s_partOf(v3, v2) = v0)) % 25.15/4.16 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 25.15/4.16 [v3: $i] : (v1 = v0 | ~ (s_contains(v3, v2) = v1) | ~ (s_contains(v3, v2) = % 25.15/4.16 v0)) % 25.15/4.16 % 25.15/4.16 Further assumptions not needed in the proof: % 25.15/4.16 -------------------------------------------- % 25.15/4.16 axiom2, axiom3, kb0, kb1, kb10, kb100, kb101, kb102, kb103, kb104, kb105, kb106, % 25.15/4.16 kb107, kb108, kb109, kb11, kb110, kb111, kb112, kb113, kb114, kb115, kb116, % 25.15/4.16 kb117, kb118, kb119, kb12, kb120, kb121, kb122, kb123, kb124, kb125, kb126, % 25.15/4.16 kb127, kb128, kb129, kb13, kb130, kb131, kb132, kb133, kb134, kb135, kb136, % 25.15/4.16 kb137, kb138, kb139, kb14, kb140, kb141, kb142, kb143, kb144, kb145, kb146, % 25.15/4.16 kb147, kb148, kb149, kb15, kb150, kb151, kb152, kb153, kb154, kb155, kb156, % 25.15/4.16 kb157, kb158, kb159, kb16, kb160, kb161, kb162, kb163, kb164, kb165, kb166, % 25.15/4.16 kb167, kb168, kb169, kb17, kb170, kb171, kb172, kb173, kb174, kb175, kb176, % 25.15/4.16 kb177, kb178, kb179, kb180, kb181, kb182, kb183, kb184, kb185, kb186, kb187, % 25.15/4.16 kb188, kb189, kb19, kb190, kb191, kb192, kb193, kb194, kb195, kb196, kb197, % 25.15/4.16 kb198, kb199, kb2, kb20, kb200, kb201, kb202, kb203, kb204, kb205, kb206, kb207, % 25.15/4.16 kb208, kb209, kb21, kb210, kb211, kb212, kb213, kb214, kb215, kb216, kb217, % 25.15/4.16 kb218, kb219, kb22, kb220, kb221, kb222, kb223, kb224, kb225, kb226, kb227, % 25.15/4.16 kb228, kb229, kb23, kb230, kb231, kb232, kb233, kb234, kb235, kb236, kb237, % 25.15/4.16 kb238, kb239, kb24, kb240, kb241, kb242, kb243, kb244, kb245, kb246, kb247, % 25.15/4.16 kb248, kb249, kb25, kb250, kb251, kb252, kb253, kb254, kb255, kb256, kb257, % 25.15/4.16 kb258, kb259, kb26, kb260, kb261, kb262, kb263, kb264, kb265, kb266, kb267, % 25.15/4.16 kb268, kb269, kb27, kb270, kb271, kb272, kb273, kb274, kb275, kb276, kb277, % 25.15/4.16 kb278, kb279, kb28, kb280, kb281, kb282, kb283, kb284, kb285, kb286, kb287, % 25.15/4.16 kb288, kb289, kb29, kb290, kb291, kb292, kb293, kb294, kb295, kb296, kb297, % 25.15/4.16 kb298, kb299, kb3, kb30, kb300, kb301, kb302, kb303, kb304, kb305, kb306, kb307, % 25.15/4.16 kb308, kb309, kb31, kb310, kb311, kb312, kb313, kb314, kb315, kb316, kb317, % 25.15/4.16 kb318, kb319, kb32, kb320, kb321, kb322, kb323, kb324, kb325, kb326, kb327, % 25.15/4.16 kb328, kb329, kb33, kb330, kb331, kb332, kb333, kb334, kb335, kb336, kb337, % 25.15/4.16 kb338, kb339, kb34, kb340, kb341, kb342, kb343, kb344, kb345, kb346, kb347, % 25.15/4.16 kb348, kb349, kb35, kb350, kb351, kb352, kb353, kb354, kb355, kb356, kb357, % 25.15/4.16 kb358, kb359, kb36, kb360, kb361, kb362, kb363, kb364, kb365, kb366, kb367, % 25.15/4.16 kb368, kb369, kb37, kb370, kb371, kb372, kb373, kb374, kb375, kb376, kb377, % 25.15/4.16 kb378, kb379, kb38, kb380, kb381, kb382, kb383, kb384, kb385, kb386, kb387, % 25.15/4.16 kb388, kb389, kb39, kb390, kb391, kb392, kb393, kb394, kb395, kb396, kb397, % 25.15/4.17 kb398, kb399, kb4, kb40, kb400, kb401, kb402, kb403, kb404, kb405, kb406, kb407, % 25.15/4.17 kb408, kb409, kb41, kb410, kb411, kb412, kb413, kb414, kb415, kb416, kb417, % 25.15/4.17 kb418, kb419, kb42, kb420, kb421, kb422, kb423, kb424, kb425, kb426, kb427, % 25.15/4.17 kb428, kb429, kb43, kb430, kb431, kb432, kb433, kb434, kb435, kb436, kb437, % 25.15/4.17 kb438, kb439, kb44, kb440, kb441, kb442, kb443, kb444, kb445, kb446, kb447, % 25.15/4.17 kb448, kb449, kb45, kb450, kb452, kb453, kb454, kb455, kb456, kb457, kb458, % 25.15/4.17 kb459, kb46, kb460, kb461, kb462, kb463, kb464, kb465, kb466, kb467, kb468, % 25.15/4.17 kb469, kb47, kb470, kb471, kb472, kb473, kb474, kb475, kb476, kb477, kb478, % 25.15/4.17 kb479, kb48, kb480, kb481, kb482, kb483, kb484, kb485, kb486, kb487, kb488, % 25.15/4.17 kb489, kb49, kb490, kb491, kb492, kb493, kb494, kb495, kb496, kb497, kb498, % 25.15/4.17 kb499, kb5, kb50, kb500, kb501, kb502, kb503, kb504, kb505, kb506, kb507, kb508, % 25.15/4.17 kb509, kb51, kb510, kb511, kb512, kb513, kb514, kb515, kb516, kb517, kb518, % 25.15/4.17 kb519, kb52, kb520, kb521, kb522, kb523, kb524, kb525, kb526, kb527, kb528, % 25.15/4.17 kb529, kb53, kb530, kb531, kb532, kb533, kb534, kb535, kb536, kb537, kb538, % 25.15/4.17 kb539, kb54, kb540, kb541, kb542, kb543, kb544, kb545, kb546, kb547, kb548, % 25.15/4.17 kb549, kb55, kb550, kb551, kb552, kb553, kb554, kb555, kb556, kb557, kb558, % 25.15/4.17 kb559, kb56, kb560, kb561, kb562, kb563, kb564, kb565, kb566, kb567, kb568, % 25.15/4.17 kb569, kb57, kb570, kb571, kb572, kb573, kb574, kb575, kb576, kb577, kb578, % 25.15/4.17 kb579, kb58, kb580, kb581, kb582, kb583, kb584, kb585, kb586, kb587, kb588, % 25.15/4.17 kb589, kb59, kb590, kb591, kb592, kb593, kb594, kb595, kb596, kb597, kb598, % 25.15/4.17 kb599, kb6, kb60, kb61, kb62, kb63, kb64, kb65, kb66, kb67, kb68, kb69, kb7, % 25.15/4.17 kb70, kb71, kb72, kb73, kb75, kb76, kb77, kb78, kb79, kb8, kb80, kb81, kb82, % 25.15/4.17 kb83, kb84, kb85, kb86, kb87, kb88, kb89, kb9, kb90, kb91, kb92, kb93, kb94, % 25.15/4.17 kb95, kb96, kb97, kb98, kb99 % 25.15/4.17 % 25.15/4.17 Those formulas are unsatisfiable: % 25.15/4.17 --------------------------------- % 25.15/4.17 % 25.15/4.17 Begin of proof % 25.15/4.17 | % 25.15/4.17 | ALPHA: (kb18) implies: % 25.15/4.17 | (1) s_contains(s_g019, s_g013) = 0 % 25.15/4.17 | % 25.15/4.17 | ALPHA: (kb74) implies: % 25.15/4.17 | (2) s_contains(s_g013, s_MX) = 0 % 25.15/4.17 | % 25.15/4.17 | ALPHA: (kb451) implies: % 25.15/4.17 | (3) $i(s_g013) % 25.15/4.17 | % 25.15/4.17 | ALPHA: (mexico_in_america_1) implies: % 25.15/4.17 | (4) $i(s_g019) % 25.15/4.17 | (5) $i(s_MX) % 25.15/4.17 | (6) ? [v0: int] : ( ~ (v0 = 0) & s_contains(s_g019, s_MX) = v0) % 25.15/4.17 | % 25.15/4.17 | ALPHA: (function-axioms) implies: % 25.15/4.17 | (7) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 25.15/4.17 | ! [v3: $i] : (v1 = v0 | ~ (s_contains(v3, v2) = v1) | ~ % 25.15/4.17 | (s_contains(v3, v2) = v0)) % 25.15/4.17 | % 25.15/4.17 | DELTA: instantiating (6) with fresh symbol all_7_0 gives: % 25.15/4.17 | (8) ~ (all_7_0 = 0) & s_contains(s_g019, s_MX) = all_7_0 % 25.15/4.17 | % 25.15/4.17 | ALPHA: (8) implies: % 25.15/4.17 | (9) ~ (all_7_0 = 0) % 25.15/4.17 | (10) s_contains(s_g019, s_MX) = all_7_0 % 25.15/4.17 | % 25.15/4.17 | GROUND_INST: instantiating (axiom1) with s_g019, s_g013, s_MX, all_7_0, % 25.15/4.17 | simplifying with (1), (3), (4), (5), (10) gives: % 25.15/4.17 | (11) all_7_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & s_contains(s_g013, s_MX) = % 25.15/4.17 | v0) % 25.15/4.17 | % 25.15/4.17 | BETA: splitting (11) gives: % 25.15/4.17 | % 25.15/4.17 | Case 1: % 25.15/4.17 | | % 25.15/4.17 | | (12) all_7_0 = 0 % 25.15/4.17 | | % 25.15/4.17 | | REDUCE: (9), (12) imply: % 25.15/4.18 | | (13) $false % 25.15/4.18 | | % 25.15/4.18 | | CLOSE: (13) is inconsistent. % 25.15/4.18 | | % 25.15/4.18 | Case 2: % 25.15/4.18 | | % 25.15/4.18 | | (14) ? [v0: int] : ( ~ (v0 = 0) & s_contains(s_g013, s_MX) = v0) % 25.15/4.18 | | % 25.15/4.18 | | DELTA: instantiating (14) with fresh symbol all_22_0 gives: % 25.15/4.18 | | (15) ~ (all_22_0 = 0) & s_contains(s_g013, s_MX) = all_22_0 % 25.15/4.18 | | % 25.15/4.18 | | ALPHA: (15) implies: % 25.15/4.18 | | (16) ~ (all_22_0 = 0) % 25.15/4.18 | | (17) s_contains(s_g013, s_MX) = all_22_0 % 25.15/4.18 | | % 25.15/4.18 | | GROUND_INST: instantiating (7) with 0, all_22_0, s_MX, s_g013, simplifying % 25.15/4.18 | | with (2), (17) gives: % 25.15/4.18 | | (18) all_22_0 = 0 % 25.15/4.18 | | % 25.15/4.18 | | REDUCE: (16), (18) imply: % 25.15/4.18 | | (19) $false % 25.15/4.18 | | % 25.15/4.18 | | CLOSE: (19) is inconsistent. % 25.15/4.18 | | % 25.15/4.18 | End of split % 25.15/4.18 | % 25.15/4.18 End of proof % 25.15/4.18 % SZS output end Proof for theBenchmark % 25.15/4.18 % 25.15/4.18 3574ms %------------------------------------------------------------------------------