%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SET894+1 : TPTP v8.1.0. Bugfixed v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%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 : 600s % DateTime : Tue Jul 19 00:22:59 EDT 2022 % Result : Theorem 151.44s 111.00s % Output : Proof 224.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SET894+1 : TPTP v8.1.0. Bugfixed v4.0.0. % 0.11/0.12 % Command : ePrincess-casc -timeout=%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 : 600 % 0.12/0.33 % DateTime : Sun Jul 10 16:42:44 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.57 ____ _ % 0.18/0.57 ___ / __ \_____(_)___ ________ __________ % 0.18/0.57 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.18/0.57 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.18/0.57 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.18/0.57 % 0.18/0.57 A Theorem Prover for First-Order Logic % 0.18/0.57 (ePrincess v.1.0) % 0.18/0.57 % 0.18/0.57 (c) Philipp Rümmer, 2009-2015 % 0.18/0.57 (c) Peter Backeman, 2014-2015 % 0.18/0.57 (contributions by Angelo Brillout, Peter Baumgartner) % 0.18/0.57 Free software under GNU Lesser General Public License (LGPL). % 0.18/0.57 Bug reports to peter@backeman.se % 0.18/0.57 % 0.18/0.57 For more information, visit http://user.uu.se/~petba168/breu/ % 0.18/0.57 % 0.18/0.57 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.66/0.62 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.39/0.89 Prover 0: Preprocessing ... % 1.93/1.09 Prover 0: Warning: ignoring some quantifiers % 1.93/1.11 Prover 0: Constructing countermodel ... % 3.05/1.43 Prover 0: gave up % 3.05/1.44 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 3.05/1.46 Prover 1: Preprocessing ... % 3.66/1.52 Prover 1: Warning: ignoring some quantifiers % 3.66/1.53 Prover 1: Constructing countermodel ... % 4.08/1.61 Prover 1: gave up % 4.08/1.61 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 4.08/1.62 Prover 2: Preprocessing ... % 4.08/1.68 Prover 2: Warning: ignoring some quantifiers % 4.08/1.69 Prover 2: Constructing countermodel ... % 13.08/3.87 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 13.08/3.89 Prover 3: Preprocessing ... % 13.71/3.94 Prover 3: Warning: ignoring some quantifiers % 13.71/3.94 Prover 3: Constructing countermodel ... % 14.09/4.02 Prover 3: gave up % 14.09/4.02 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 14.09/4.03 Prover 4: Preprocessing ... % 14.09/4.07 Prover 4: Warning: ignoring some quantifiers % 14.09/4.07 Prover 4: Constructing countermodel ... % 17.87/5.05 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 17.87/5.07 Prover 5: Preprocessing ... % 18.38/5.12 Prover 5: Warning: ignoring some quantifiers % 18.38/5.12 Prover 5: Constructing countermodel ... % 43.66/20.63 Prover 5: stopped % 43.84/20.83 Prover 6: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 43.84/20.85 Prover 6: Preprocessing ... % 43.84/20.88 Prover 6: Warning: ignoring some quantifiers % 43.84/20.88 Prover 6: Constructing countermodel ... % 139.86/106.76 Prover 6: stopped % 140.04/106.97 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximalOutermost -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 140.04/106.98 Prover 7: Preprocessing ... % 140.25/107.01 Prover 7: Proving ... % 151.44/111.00 Prover 7: proved (4037ms) % 151.44/111.00 Prover 2: stopped % 151.44/111.00 Prover 4: stopped % 151.44/111.00 % 151.44/111.00 % SZS status Theorem for theBenchmark % 151.44/111.00 % 151.44/111.00 Generating proof ... found it (size 56) % 224.86/170.13 % 224.86/170.13 % SZS output start Proof for theBenchmark % 224.86/170.14 Assumed formulas after preprocessing and simplification: % 224.86/170.14 | (0) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (cartesian_product2(v2, v3) = v5) | ~ (ordered_pair(v0, v1) = v4) | ~ in(v4, v5) | (in(v1, v3) & in(v0, v2))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (cartesian_product2(v2, v3) = v5) | ~ (ordered_pair(v0, v1) = v4) | ~ in(v1, v3) | ~ in(v0, v2) | in(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (singleton(v0) = v3) | ~ (unordered_pair(v2, v3) = v4) | ~ (unordered_pair(v0, v1) = v2) | ordered_pair(v0, v1) = v4) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (cartesian_product2(v3, v2) = v1) | ~ (cartesian_product2(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ordered_pair(v3, v2) = v1) | ~ (ordered_pair(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (unordered_pair(v3, v2) = v1) | ~ (unordered_pair(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (cartesian_product2(v0, v1) = v2) | ! [v3] : (v3 = v2 | ? [v4] : (( ~ in(v4, v3) | ! [v5] : ! [v6] : ( ~ in(v6, v1) | ~ in(v5, v0) | ? [v7] : ( ~ (v7 = v4) & ordered_pair(v5, v6) = v7))) & (in(v4, v3) | ? [v5] : ? [v6] : (ordered_pair(v5, v6) = v4 & in(v6, v1) & in(v5, v0)))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (cartesian_product2(v0, v1) = v2) | ( ! [v3] : ( ~ in(v3, v2) | ? [v4] : ? [v5] : (ordered_pair(v4, v5) = v3 & in(v5, v1) & in(v4, v0))) & ! [v3] : (in(v3, v2) | ! [v4] : ! [v5] : ( ~ in(v5, v1) | ~ in(v4, v0) | ? [v6] : ( ~ (v6 = v3) & ordered_pair(v4, v5) = v6))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (ordered_pair(v0, v1) = v2) | ~ empty(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | unordered_pair(v1, v0) = v2) & ! [v0] : ! [v1] : (v1 = v0 | ? [v2] : (( ~ in(v2, v1) | ~ in(v2, v0)) & (in(v2, v1) | in(v2, v0)))) & ! [v0] : ! [v1] : ( ~ (singleton(v0) = v1) | ! [v2] : (v2 = v1 | ? [v3] : (( ~ (v3 = v0) | ~ in(v0, v2)) & (v3 = v0 | in(v3, v2))))) & ! [v0] : ! [v1] : ( ~ (singleton(v0) = v1) | (in(v0, v1) & ! [v2] : (v2 = v0 | ~ in(v2, v1)))) & ! [v0] : ! [v1] : ( ~ in(v1, v0) | ~ in(v0, v1)) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = v4) & cartesian_product2(v2, v3) = v4 & ordered_pair(v0, v1) = v5 & singleton(v5) = v6 & singleton(v1) = v3 & singleton(v0) = v2) & ? [v0] : ~ empty(v0) & ? [v0] : empty(v0) % 224.86/170.16 | Applying alpha-rule on (0) yields: % 224.86/170.16 | (1) ! [v0] : ! [v1] : ( ~ in(v1, v0) | ~ in(v0, v1)) % 224.86/170.16 | (2) ! [v0] : ! [v1] : ( ~ (singleton(v0) = v1) | (in(v0, v1) & ! [v2] : (v2 = v0 | ~ in(v2, v1)))) % 224.86/170.16 | (3) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = v4) & cartesian_product2(v2, v3) = v4 & ordered_pair(v0, v1) = v5 & singleton(v5) = v6 & singleton(v1) = v3 & singleton(v0) = v2) % 224.86/170.16 | (4) ! [v0] : ! [v1] : ( ~ (singleton(v0) = v1) | ! [v2] : (v2 = v1 | ? [v3] : (( ~ (v3 = v0) | ~ in(v0, v2)) & (v3 = v0 | in(v3, v2))))) % 224.86/170.16 | (5) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) % 224.86/170.16 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (cartesian_product2(v3, v2) = v1) | ~ (cartesian_product2(v3, v2) = v0)) % 224.86/170.16 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (cartesian_product2(v2, v3) = v5) | ~ (ordered_pair(v0, v1) = v4) | ~ in(v4, v5) | (in(v1, v3) & in(v0, v2))) % 224.86/170.16 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (unordered_pair(v3, v2) = v1) | ~ (unordered_pair(v3, v2) = v0)) % 224.86/170.16 | (9) ! [v0] : ! [v1] : ! [v2] : ( ~ (ordered_pair(v0, v1) = v2) | ~ empty(v2)) % 224.86/170.16 | (10) ? [v0] : empty(v0) % 224.86/170.16 | (11) ! [v0] : ! [v1] : (v1 = v0 | ? [v2] : (( ~ in(v2, v1) | ~ in(v2, v0)) & (in(v2, v1) | in(v2, v0)))) % 224.86/170.16 | (12) ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | unordered_pair(v1, v0) = v2) % 224.86/170.16 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (singleton(v0) = v3) | ~ (unordered_pair(v2, v3) = v4) | ~ (unordered_pair(v0, v1) = v2) | ordered_pair(v0, v1) = v4) % 224.86/170.16 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ordered_pair(v3, v2) = v1) | ~ (ordered_pair(v3, v2) = v0)) % 224.86/170.17 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (cartesian_product2(v2, v3) = v5) | ~ (ordered_pair(v0, v1) = v4) | ~ in(v1, v3) | ~ in(v0, v2) | in(v4, v5)) % 224.86/170.17 | (16) ? [v0] : ~ empty(v0) % 224.86/170.17 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ (cartesian_product2(v0, v1) = v2) | ( ! [v3] : ( ~ in(v3, v2) | ? [v4] : ? [v5] : (ordered_pair(v4, v5) = v3 & in(v5, v1) & in(v4, v0))) & ! [v3] : (in(v3, v2) | ! [v4] : ! [v5] : ( ~ in(v5, v1) | ~ in(v4, v0) | ? [v6] : ( ~ (v6 = v3) & ordered_pair(v4, v5) = v6))))) % 224.86/170.17 | (18) ! [v0] : ! [v1] : ! [v2] : ( ~ (cartesian_product2(v0, v1) = v2) | ! [v3] : (v3 = v2 | ? [v4] : (( ~ in(v4, v3) | ! [v5] : ! [v6] : ( ~ in(v6, v1) | ~ in(v5, v0) | ? [v7] : ( ~ (v7 = v4) & ordered_pair(v5, v6) = v7))) & (in(v4, v3) | ? [v5] : ? [v6] : (ordered_pair(v5, v6) = v4 & in(v6, v1) & in(v5, v0)))))) % 224.86/170.17 | % 224.86/170.17 | Instantiating (3) with all_3_0_1, all_3_1_2, all_3_2_3, all_3_3_4, all_3_4_5, all_3_5_6, all_3_6_7 yields: % 224.86/170.17 | (19) ~ (all_3_0_1 = all_3_2_3) & cartesian_product2(all_3_4_5, all_3_3_4) = all_3_2_3 & ordered_pair(all_3_6_7, all_3_5_6) = all_3_1_2 & singleton(all_3_1_2) = all_3_0_1 & singleton(all_3_5_6) = all_3_3_4 & singleton(all_3_6_7) = all_3_4_5 % 224.86/170.17 | % 224.86/170.17 | Applying alpha-rule on (19) yields: % 224.86/170.17 | (20) ~ (all_3_0_1 = all_3_2_3) % 224.86/170.17 | (21) singleton(all_3_6_7) = all_3_4_5 % 224.86/170.17 | (22) singleton(all_3_5_6) = all_3_3_4 % 224.86/170.17 | (23) singleton(all_3_1_2) = all_3_0_1 % 224.86/170.17 | (24) cartesian_product2(all_3_4_5, all_3_3_4) = all_3_2_3 % 224.86/170.17 | (25) ordered_pair(all_3_6_7, all_3_5_6) = all_3_1_2 % 224.86/170.17 | % 224.86/170.17 | Instantiating formula (17) with all_3_2_3, all_3_3_4, all_3_4_5 and discharging atoms cartesian_product2(all_3_4_5, all_3_3_4) = all_3_2_3, yields: % 224.86/170.17 | (26) ! [v0] : ( ~ in(v0, all_3_2_3) | ? [v1] : ? [v2] : (ordered_pair(v1, v2) = v0 & in(v2, all_3_3_4) & in(v1, all_3_4_5))) & ! [v0] : (in(v0, all_3_2_3) | ! [v1] : ! [v2] : ( ~ in(v2, all_3_3_4) | ~ in(v1, all_3_4_5) | ? [v3] : ( ~ (v3 = v0) & ordered_pair(v1, v2) = v3))) % 224.86/170.17 | % 224.86/170.17 | Applying alpha-rule on (26) yields: % 224.86/170.17 | (27) ! [v0] : ( ~ in(v0, all_3_2_3) | ? [v1] : ? [v2] : (ordered_pair(v1, v2) = v0 & in(v2, all_3_3_4) & in(v1, all_3_4_5))) % 224.86/170.17 | (28) ! [v0] : (in(v0, all_3_2_3) | ! [v1] : ! [v2] : ( ~ in(v2, all_3_3_4) | ~ in(v1, all_3_4_5) | ? [v3] : ( ~ (v3 = v0) & ordered_pair(v1, v2) = v3))) % 224.86/170.17 | % 224.86/170.17 | Instantiating formula (2) with all_3_0_1, all_3_1_2 and discharging atoms singleton(all_3_1_2) = all_3_0_1, yields: % 224.86/170.17 | (29) in(all_3_1_2, all_3_0_1) & ! [v0] : (v0 = all_3_1_2 | ~ in(v0, all_3_0_1)) % 224.86/170.17 | % 224.86/170.17 | Applying alpha-rule on (29) yields: % 224.86/170.17 | (30) in(all_3_1_2, all_3_0_1) % 224.86/170.17 | (31) ! [v0] : (v0 = all_3_1_2 | ~ in(v0, all_3_0_1)) % 224.86/170.17 | % 224.86/170.17 | Instantiating formula (2) with all_3_3_4, all_3_5_6 and discharging atoms singleton(all_3_5_6) = all_3_3_4, yields: % 224.86/170.17 | (32) in(all_3_5_6, all_3_3_4) & ! [v0] : (v0 = all_3_5_6 | ~ in(v0, all_3_3_4)) % 224.86/170.17 | % 224.86/170.17 | Applying alpha-rule on (32) yields: % 224.86/170.17 | (33) in(all_3_5_6, all_3_3_4) % 224.86/170.17 | (34) ! [v0] : (v0 = all_3_5_6 | ~ in(v0, all_3_3_4)) % 224.86/170.17 | % 224.86/170.17 | Instantiating formula (2) with all_3_4_5, all_3_6_7 and discharging atoms singleton(all_3_6_7) = all_3_4_5, yields: % 224.86/170.17 | (35) in(all_3_6_7, all_3_4_5) & ! [v0] : (v0 = all_3_6_7 | ~ in(v0, all_3_4_5)) % 224.86/170.17 | % 224.86/170.17 | Applying alpha-rule on (35) yields: % 224.86/170.17 | (36) in(all_3_6_7, all_3_4_5) % 224.86/170.17 | (37) ! [v0] : (v0 = all_3_6_7 | ~ in(v0, all_3_4_5)) % 224.86/170.17 | % 224.86/170.17 | Instantiating formula (15) with all_3_2_3, all_3_1_2, all_3_3_4, all_3_4_5, all_3_5_6, all_3_6_7 and discharging atoms cartesian_product2(all_3_4_5, all_3_3_4) = all_3_2_3, ordered_pair(all_3_6_7, all_3_5_6) = all_3_1_2, in(all_3_5_6, all_3_3_4), in(all_3_6_7, all_3_4_5), yields: % 224.86/170.17 | (38) in(all_3_1_2, all_3_2_3) % 224.86/170.17 | % 224.86/170.17 | Introducing new symbol ex_100_1_20 defined by: % 224.86/170.17 | (39) ex_100_1_20 = all_3_0_1 % 224.86/170.17 | % 224.86/170.17 | Introducing new symbol ex_100_0_19 defined by: % 224.86/170.17 | (40) ex_100_0_19 = all_3_2_3 % 224.86/170.17 | % 224.86/170.17 | Instantiating formula (11) with ex_100_0_19, ex_100_1_20 yields: % 224.86/170.17 | (41) ex_100_0_19 = ex_100_1_20 | ? [v0] : (( ~ in(v0, ex_100_0_19) | ~ in(v0, ex_100_1_20)) & (in(v0, ex_100_0_19) | in(v0, ex_100_1_20))) % 224.86/170.17 | % 224.86/170.17 +-Applying beta-rule and splitting (41), into two cases. % 224.86/170.17 |-Branch one: % 224.86/170.17 | (42) ex_100_0_19 = ex_100_1_20 % 224.86/170.17 | % 224.86/170.17 | Combining equations (42,40) yields a new equation: % 224.86/170.17 | (43) ex_100_1_20 = all_3_2_3 % 224.86/170.17 | % 224.86/170.17 | Simplifying 43 yields: % 224.86/170.17 | (44) ex_100_1_20 = all_3_2_3 % 224.86/170.17 | % 224.86/170.17 | Combining equations (44,39) yields a new equation: % 224.86/170.17 | (45) all_3_0_1 = all_3_2_3 % 224.86/170.17 | % 224.86/170.17 | Equations (45) can reduce 20 to: % 224.86/170.17 | (46) $false % 224.86/170.17 | % 224.86/170.18 |-The branch is then unsatisfiable % 224.86/170.18 |-Branch two: % 224.86/170.18 | (47) ? [v0] : (( ~ in(v0, ex_100_0_19) | ~ in(v0, ex_100_1_20)) & (in(v0, ex_100_0_19) | in(v0, ex_100_1_20))) % 224.86/170.18 | % 224.86/170.18 | Instantiating (47) with all_103_0_21 yields: % 224.86/170.18 | (48) ( ~ in(all_103_0_21, ex_100_0_19) | ~ in(all_103_0_21, ex_100_1_20)) & (in(all_103_0_21, ex_100_0_19) | in(all_103_0_21, ex_100_1_20)) % 224.86/170.18 | % 224.86/170.18 | Applying alpha-rule on (48) yields: % 224.86/170.18 | (49) ~ in(all_103_0_21, ex_100_0_19) | ~ in(all_103_0_21, ex_100_1_20) % 224.86/170.18 | (50) in(all_103_0_21, ex_100_0_19) | in(all_103_0_21, ex_100_1_20) % 224.86/170.18 | % 224.86/170.18 +-Applying beta-rule and splitting (49), into two cases. % 224.86/170.18 |-Branch one: % 224.86/170.18 | (51) ~ in(all_103_0_21, ex_100_0_19) % 224.86/170.18 | % 224.86/170.18 +-Applying beta-rule and splitting (50), into two cases. % 224.86/170.18 |-Branch one: % 224.86/170.18 | (52) in(all_103_0_21, ex_100_0_19) % 224.86/170.18 | % 224.86/170.18 | Using (52) and (51) yields: % 224.86/170.18 | (53) $false % 224.86/170.18 | % 224.86/170.18 |-The branch is then unsatisfiable % 224.86/170.18 |-Branch two: % 224.86/170.18 | (54) in(all_103_0_21, ex_100_1_20) % 224.86/170.18 | % 224.86/170.18 | Instantiating formula (31) with all_103_0_21 yields: % 224.86/170.18 | (55) all_103_0_21 = all_3_1_2 | ~ in(all_103_0_21, all_3_0_1) % 224.86/170.18 | % 224.86/170.18 +-Applying beta-rule and splitting (55), into two cases. % 224.86/170.18 |-Branch one: % 224.86/170.18 | (56) ~ in(all_103_0_21, all_3_0_1) % 224.86/170.18 | % 224.86/170.18 | From (39) and (54) follows: % 224.86/170.18 | (57) in(all_103_0_21, all_3_0_1) % 224.86/170.18 | % 224.86/170.18 | Using (57) and (56) yields: % 224.86/170.18 | (53) $false % 224.86/170.18 | % 224.86/170.18 |-The branch is then unsatisfiable % 224.86/170.18 |-Branch two: % 224.86/170.18 | (59) all_103_0_21 = all_3_1_2 % 224.86/170.18 | % 224.86/170.18 | From (59) and (51) follows: % 224.86/170.18 | (60) ~ in(all_3_1_2, ex_100_0_19) % 224.86/170.18 | % 224.86/170.18 | From (40) and (60) follows: % 224.86/170.18 | (61) ~ in(all_3_1_2, all_3_2_3) % 224.86/170.18 | % 224.86/170.18 | Using (38) and (61) yields: % 224.86/170.18 | (53) $false % 224.86/170.18 | % 224.86/170.18 |-The branch is then unsatisfiable % 224.86/170.18 |-Branch two: % 224.86/170.18 | (52) in(all_103_0_21, ex_100_0_19) % 224.86/170.18 | (64) ~ in(all_103_0_21, ex_100_1_20) % 224.86/170.18 | % 224.86/170.18 | Instantiating formula (31) with all_103_0_21 yields: % 224.86/170.18 | (55) all_103_0_21 = all_3_1_2 | ~ in(all_103_0_21, all_3_0_1) % 224.86/170.18 | % 224.86/170.18 | Instantiating formula (27) with all_103_0_21 yields: % 224.86/170.18 | (66) ~ in(all_103_0_21, all_3_2_3) | ? [v0] : ? [v1] : (ordered_pair(v0, v1) = all_103_0_21 & in(v1, all_3_3_4) & in(v0, all_3_4_5)) % 224.86/170.18 | % 224.86/170.18 +-Applying beta-rule and splitting (55), into two cases. % 224.86/170.18 |-Branch one: % 224.86/170.18 | (56) ~ in(all_103_0_21, all_3_0_1) % 224.86/170.18 | % 224.86/170.18 +-Applying beta-rule and splitting (66), into two cases. % 224.86/170.18 |-Branch one: % 224.86/170.18 | (68) ~ in(all_103_0_21, all_3_2_3) % 224.86/170.18 | % 224.86/170.18 | From (40) and (52) follows: % 224.86/170.18 | (69) in(all_103_0_21, all_3_2_3) % 224.86/170.18 | % 224.86/170.18 | Using (69) and (68) yields: % 224.86/170.18 | (53) $false % 224.86/170.18 | % 224.86/170.18 |-The branch is then unsatisfiable % 224.86/170.18 |-Branch two: % 224.86/170.18 | (71) ? [v0] : ? [v1] : (ordered_pair(v0, v1) = all_103_0_21 & in(v1, all_3_3_4) & in(v0, all_3_4_5)) % 224.86/170.18 | % 224.86/170.18 | Instantiating (71) with all_146_0_37, all_146_1_38 yields: % 224.86/170.18 | (72) ordered_pair(all_146_1_38, all_146_0_37) = all_103_0_21 & in(all_146_0_37, all_3_3_4) & in(all_146_1_38, all_3_4_5) % 224.86/170.18 | % 224.86/170.18 | Applying alpha-rule on (72) yields: % 224.86/170.18 | (73) ordered_pair(all_146_1_38, all_146_0_37) = all_103_0_21 % 224.86/170.18 | (74) in(all_146_0_37, all_3_3_4) % 224.86/170.18 | (75) in(all_146_1_38, all_3_4_5) % 224.86/170.18 | % 224.86/170.18 | Instantiating formula (34) with all_146_0_37 and discharging atoms in(all_146_0_37, all_3_3_4), yields: % 224.86/170.18 | (76) all_146_0_37 = all_3_5_6 % 224.86/170.18 | % 224.86/170.18 | Instantiating formula (37) with all_146_1_38 and discharging atoms in(all_146_1_38, all_3_4_5), yields: % 224.86/170.18 | (77) all_146_1_38 = all_3_6_7 % 224.86/170.18 | % 224.86/170.18 | From (77)(76) and (73) follows: % 224.86/170.18 | (78) ordered_pair(all_3_6_7, all_3_5_6) = all_103_0_21 % 224.86/170.18 | % 224.86/170.18 | Instantiating formula (14) with all_3_6_7, all_3_5_6, all_103_0_21, all_3_1_2 and discharging atoms ordered_pair(all_3_6_7, all_3_5_6) = all_103_0_21, ordered_pair(all_3_6_7, all_3_5_6) = all_3_1_2, yields: % 224.86/170.18 | (59) all_103_0_21 = all_3_1_2 % 224.86/170.18 | % 224.86/170.18 | From (59) and (56) follows: % 224.86/170.18 | (80) ~ in(all_3_1_2, all_3_0_1) % 224.86/170.18 | % 224.86/170.18 | Using (30) and (80) yields: % 224.86/170.18 | (53) $false % 224.86/170.18 | % 224.86/170.18 |-The branch is then unsatisfiable % 224.86/170.18 |-Branch two: % 224.86/170.18 | (59) all_103_0_21 = all_3_1_2 % 224.86/170.18 | % 224.86/170.18 | From (59) and (64) follows: % 224.86/170.18 | (83) ~ in(all_3_1_2, ex_100_1_20) % 224.86/170.18 | % 224.86/170.18 | From (39) and (83) follows: % 224.86/170.18 | (80) ~ in(all_3_1_2, all_3_0_1) % 224.86/170.18 | % 224.86/170.18 | Using (30) and (80) yields: % 224.86/170.18 | (53) $false % 224.86/170.18 | % 224.86/170.18 |-The branch is then unsatisfiable % 224.86/170.18 % SZS output end Proof for theBenchmark % 224.86/170.18 % 224.86/170.18 169602ms %------------------------------------------------------------------------------