%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SET579+3 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n010.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:20:24 EDT 2022 % Result : Theorem 68.01s 41.25s % Output : Proof 81.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SET579+3 : TPTP v8.1.0. Released v2.2.0. % 0.03/0.14 % Command : ePrincess-casc -timeout=%d %s % 0.15/0.35 % Computer : n010.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 600 % 0.15/0.35 % DateTime : Mon Jul 11 04:29:00 EDT 2022 % 0.15/0.36 % CPUTime : % 0.47/0.62 ____ _ % 0.47/0.62 ___ / __ \_____(_)___ ________ __________ % 0.47/0.62 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.47/0.62 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.47/0.62 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.47/0.62 % 0.47/0.62 A Theorem Prover for First-Order Logic % 0.47/0.62 (ePrincess v.1.0) % 0.47/0.62 % 0.47/0.62 (c) Philipp Rümmer, 2009-2015 % 0.47/0.62 (c) Peter Backeman, 2014-2015 % 0.47/0.62 (contributions by Angelo Brillout, Peter Baumgartner) % 0.47/0.62 Free software under GNU Lesser General Public License (LGPL). % 0.47/0.62 Bug reports to peter@backeman.se % 0.47/0.62 % 0.47/0.62 For more information, visit http://user.uu.se/~petba168/breu/ % 0.47/0.62 % 0.47/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.69/0.67 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.34/0.92 Prover 0: Preprocessing ... % 1.63/1.04 Prover 0: Warning: ignoring some quantifiers % 1.76/1.06 Prover 0: Constructing countermodel ... % 2.14/1.17 Prover 0: gave up % 2.14/1.18 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 2.14/1.19 Prover 1: Preprocessing ... % 2.46/1.26 Prover 1: Constructing countermodel ... % 2.56/1.29 Prover 1: gave up % 2.56/1.29 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.56/1.30 Prover 2: Preprocessing ... % 2.90/1.37 Prover 2: Warning: ignoring some quantifiers % 2.90/1.38 Prover 2: Constructing countermodel ... % 2.90/1.41 Prover 2: gave up % 2.90/1.41 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.90/1.42 Prover 3: Preprocessing ... % 3.18/1.44 Prover 3: Warning: ignoring some quantifiers % 3.18/1.44 Prover 3: Constructing countermodel ... % 3.18/1.46 Prover 3: gave up % 3.18/1.46 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 3.36/1.47 Prover 4: Preprocessing ... % 3.69/1.54 Prover 4: Warning: ignoring some quantifiers % 3.69/1.55 Prover 4: Constructing countermodel ... % 5.07/1.87 Prover 4: gave up % 5.07/1.87 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 5.07/1.88 Prover 5: Preprocessing ... % 5.07/1.91 Prover 5: Constructing countermodel ... % 5.43/1.93 Prover 5: gave up % 5.43/1.93 Prover 6: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 5.43/1.94 Prover 6: Preprocessing ... % 5.43/1.96 Prover 6: Warning: ignoring some quantifiers % 5.43/1.97 Prover 6: Constructing countermodel ... % 5.65/1.98 Prover 6: gave up % 5.65/1.98 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximalOutermost -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 5.65/1.99 Prover 7: Preprocessing ... % 5.65/2.00 Prover 7: Proving ... % 29.98/12.80 Prover 8: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 29.98/12.82 Prover 8: Preprocessing ... % 30.16/12.85 Prover 8: Constructing countermodel ... % 30.16/12.86 Prover 8: gave up % 30.16/12.86 Prover 9: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=completeFrugal % 30.16/12.87 Prover 9: Preprocessing ... % 30.42/12.90 Prover 9: Proving ... % 56.62/32.83 Prover 10: Options: -triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 56.62/32.84 Prover 10: Preprocessing ... % 56.62/32.85 Prover 10: Warning: ignoring some quantifiers % 56.62/32.86 Prover 10: Constructing countermodel ... % 56.73/32.87 Prover 10: gave up % 56.73/32.87 Prover 11: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 56.73/32.88 Prover 11: Preprocessing ... % 56.73/32.89 Prover 11: Warning: ignoring some quantifiers % 56.73/32.89 Prover 11: Constructing countermodel ... % 56.73/32.91 Prover 11: gave up % 56.73/32.91 Prover 12: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 56.73/32.92 Prover 12: Preprocessing ... % 57.04/32.94 Prover 12: Constructing countermodel ... % 57.04/32.95 Prover 12: gave up % 57.04/32.95 Prover 13: Options: -triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 57.04/32.95 Prover 13: Preprocessing ... % 57.04/32.96 Prover 13: Warning: ignoring some quantifiers % 57.04/32.96 Prover 13: Constructing countermodel ... % 57.18/32.98 Prover 13: gave up % 57.18/32.98 Prover 14: Options: -triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 57.18/32.99 Prover 14: Preprocessing ... % 57.18/32.99 Prover 14: Warning: ignoring some quantifiers % 57.18/32.99 Prover 14: Constructing countermodel ... % 57.18/33.00 Prover 14: gave up % 57.18/33.00 Prover 15: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 57.18/33.01 Prover 15: Preprocessing ... % 57.18/33.02 Prover 15: Constructing countermodel ... % 57.47/33.03 Prover 15: gave up % 57.47/33.03 Prover 16: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 57.47/33.03 Prover 16: Preprocessing ... % 57.47/33.05 Prover 16: Constructing countermodel ... % 57.47/33.05 Prover 16: gave up % 57.47/33.05 Prover 17: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 57.47/33.06 Prover 17: Preprocessing ... % 57.57/33.06 Prover 17: Warning: ignoring some quantifiers % 57.57/33.06 Prover 17: Constructing countermodel ... % 57.57/33.07 Prover 17: gave up % 57.57/33.07 Prover 18: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximalOutermost -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 57.57/33.08 Prover 18: Preprocessing ... % 57.57/33.08 Prover 18: Warning: ignoring some quantifiers % 57.57/33.08 Prover 18: Constructing countermodel ... % 57.57/33.09 Prover 18: gave up % 57.57/33.09 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 57.57/33.09 Prover 19: Preprocessing ... % 57.57/33.11 Prover 19: Constructing countermodel ... % 57.57/33.11 Prover 19: gave up % 61.74/36.14 Prover 9: stopped % 68.01/41.25 Prover 7: proved (17347ms) % 68.01/41.25 % 68.01/41.25 % SZS status Theorem for theBenchmark % 68.01/41.25 % 68.01/41.25 Generating proof ... found it (size 98) % 81.41/51.15 % 81.41/51.15 % SZS output start Proof for theBenchmark % 81.41/51.15 Assumed formulas after preprocessing and simplification: % 81.41/51.15 | (0) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (difference(v3, v2) = v1) | ~ (difference(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (difference(v0, v1) = v3) | ~ member(v2, v3) | (member(v2, v0) & ~ member(v2, v1))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (difference(v0, v1) = v3) | ~ member(v2, v0) | member(v2, v3) | member(v2, v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ subset(v1, v0) | ~ subset(v0, v1)) & ! [v0] : ! [v1] : ( ~ subset(v0, v1) | ! [v2] : ( ~ member(v2, v0) | member(v2, v1))) & ! [v0] : ! [v1] : (subset(v0, v1) | ? [v2] : (member(v2, v0) & ~ member(v2, v1))) & ! [v0] : subset(v0, v0) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = v0) & difference(v1, v2) = v3 & ! [v4] : ( ~ member(v4, v1) | member(v4, v2) | member(v4, v0)) & ! [v4] : ( ~ member(v4, v0) | (member(v4, v1) & ~ member(v4, v2)))) % 81.41/51.17 | Applying alpha-rule on (0) yields: % 81.41/51.17 | (1) ! [v0] : subset(v0, v0) % 81.41/51.17 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (difference(v3, v2) = v1) | ~ (difference(v3, v2) = v0)) % 81.41/51.17 | (3) ! [v0] : ! [v1] : ( ~ subset(v0, v1) | ! [v2] : ( ~ member(v2, v0) | member(v2, v1))) % 81.41/51.17 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (difference(v0, v1) = v3) | ~ member(v2, v0) | member(v2, v3) | member(v2, v1)) % 81.41/51.17 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (difference(v0, v1) = v3) | ~ member(v2, v3) | (member(v2, v0) & ~ member(v2, v1))) % 81.41/51.17 | (6) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = v0) & difference(v1, v2) = v3 & ! [v4] : ( ~ member(v4, v1) | member(v4, v2) | member(v4, v0)) & ! [v4] : ( ~ member(v4, v0) | (member(v4, v1) & ~ member(v4, v2)))) % 81.57/51.17 | (7) ! [v0] : ! [v1] : (v1 = v0 | ~ subset(v1, v0) | ~ subset(v0, v1)) % 81.57/51.17 | (8) ! [v0] : ! [v1] : (subset(v0, v1) | ? [v2] : (member(v2, v0) & ~ member(v2, v1))) % 81.57/51.17 | % 81.57/51.17 | Instantiating (6) with all_1_0_0, all_1_1_1, all_1_2_2, all_1_3_3 yields: % 81.57/51.17 | (9) ~ (all_1_0_0 = all_1_3_3) & difference(all_1_2_2, all_1_1_1) = all_1_0_0 & ! [v0] : ( ~ member(v0, all_1_2_2) | member(v0, all_1_1_1) | member(v0, all_1_3_3)) & ! [v0] : ( ~ member(v0, all_1_3_3) | (member(v0, all_1_2_2) & ~ member(v0, all_1_1_1))) % 81.57/51.17 | % 81.57/51.17 | Applying alpha-rule on (9) yields: % 81.57/51.17 | (10) ~ (all_1_0_0 = all_1_3_3) % 81.57/51.17 | (11) difference(all_1_2_2, all_1_1_1) = all_1_0_0 % 81.57/51.17 | (12) ! [v0] : ( ~ member(v0, all_1_2_2) | member(v0, all_1_1_1) | member(v0, all_1_3_3)) % 81.57/51.17 | (13) ! [v0] : ( ~ member(v0, all_1_3_3) | (member(v0, all_1_2_2) & ~ member(v0, all_1_1_1))) % 81.57/51.17 | % 81.57/51.17 | Introducing new symbol ex_10_1_5 defined by: % 81.57/51.17 | (14) ex_10_1_5 = all_1_0_0 % 81.57/51.17 | % 81.57/51.17 | Introducing new symbol ex_10_0_4 defined by: % 81.57/51.17 | (15) ex_10_0_4 = all_1_3_3 % 81.57/51.17 | % 81.57/51.17 | Instantiating formula (8) with ex_10_0_4, ex_10_1_5 yields: % 81.57/51.17 | (16) subset(ex_10_1_5, ex_10_0_4) | ? [v0] : (member(v0, ex_10_1_5) & ~ member(v0, ex_10_0_4)) % 81.57/51.17 | % 81.57/51.17 +-Applying beta-rule and splitting (16), into two cases. % 81.57/51.17 |-Branch one: % 81.57/51.17 | (17) subset(ex_10_1_5, ex_10_0_4) % 81.57/51.17 | % 81.57/51.17 | Instantiating formula (3) with ex_10_0_4, ex_10_1_5 and discharging atoms subset(ex_10_1_5, ex_10_0_4), yields: % 81.57/51.17 | (18) ! [v0] : ( ~ member(v0, ex_10_1_5) | member(v0, ex_10_0_4)) % 81.57/51.17 | % 81.57/51.17 | Introducing new symbol ex_29_1_9 defined by: % 81.57/51.17 | (19) ex_29_1_9 = all_1_3_3 % 81.57/51.17 | % 81.57/51.17 | Introducing new symbol ex_29_0_8 defined by: % 81.57/51.17 | (20) ex_29_0_8 = all_1_0_0 % 81.57/51.17 | % 81.57/51.17 | Instantiating formula (8) with ex_29_0_8, ex_29_1_9 yields: % 81.57/51.17 | (21) subset(ex_29_1_9, ex_29_0_8) | ? [v0] : (member(v0, ex_29_1_9) & ~ member(v0, ex_29_0_8)) % 81.57/51.17 | % 81.57/51.17 +-Applying beta-rule and splitting (21), into two cases. % 81.57/51.17 |-Branch one: % 81.57/51.17 | (22) subset(ex_29_1_9, ex_29_0_8) % 81.57/51.17 | % 81.57/51.17 | Instantiating formula (7) with ex_29_0_8, ex_29_1_9 and discharging atoms subset(ex_29_1_9, ex_29_0_8), yields: % 81.57/51.17 | (23) ex_29_0_8 = ex_29_1_9 | ~ subset(ex_29_0_8, ex_29_1_9) % 81.57/51.17 | % 81.57/51.17 +-Applying beta-rule and splitting (23), into two cases. % 81.57/51.17 |-Branch one: % 81.57/51.17 | (24) ~ subset(ex_29_0_8, ex_29_1_9) % 81.57/51.17 | % 81.57/51.17 | From (14)(15) and (17) follows: % 81.57/51.17 | (25) subset(all_1_0_0, all_1_3_3) % 81.57/51.17 | % 81.57/51.17 | From (20)(19) and (24) follows: % 81.57/51.18 | (26) ~ subset(all_1_0_0, all_1_3_3) % 81.57/51.18 | % 81.57/51.18 | Using (25) and (26) yields: % 81.57/51.18 | (27) $false % 81.57/51.18 | % 81.57/51.18 |-The branch is then unsatisfiable % 81.57/51.18 |-Branch two: % 81.57/51.18 | (28) ex_29_0_8 = ex_29_1_9 % 81.57/51.18 | % 81.57/51.18 | Combining equations (28,20) yields a new equation: % 81.57/51.18 | (29) ex_29_1_9 = all_1_0_0 % 81.57/51.18 | % 81.57/51.18 | Simplifying 29 yields: % 81.57/51.18 | (30) ex_29_1_9 = all_1_0_0 % 81.57/51.18 | % 81.57/51.18 | Combining equations (30,19) yields a new equation: % 81.57/51.18 | (31) all_1_0_0 = all_1_3_3 % 81.57/51.18 | % 81.57/51.18 | Simplifying 31 yields: % 81.57/51.18 | (32) all_1_0_0 = all_1_3_3 % 81.57/51.18 | % 81.57/51.18 | Equations (32) can reduce 10 to: % 81.57/51.18 | (33) $false % 81.57/51.18 | % 81.57/51.18 |-The branch is then unsatisfiable % 81.57/51.18 |-Branch two: % 81.57/51.18 | (34) ? [v0] : (member(v0, ex_29_1_9) & ~ member(v0, ex_29_0_8)) % 81.57/51.18 | % 81.57/51.18 | Instantiating (34) with all_31_0_10 yields: % 81.57/51.18 | (35) member(all_31_0_10, ex_29_1_9) & ~ member(all_31_0_10, ex_29_0_8) % 81.57/51.18 | % 81.57/51.18 | Applying alpha-rule on (35) yields: % 81.57/51.18 | (36) member(all_31_0_10, ex_29_1_9) % 81.57/51.18 | (37) ~ member(all_31_0_10, ex_29_0_8) % 81.57/51.18 | % 81.57/51.18 | Instantiating formula (5) with all_1_0_0, all_31_0_10, all_1_1_1, all_1_2_2 and discharging atoms difference(all_1_2_2, all_1_1_1) = all_1_0_0, yields: % 81.57/51.18 | (38) ~ member(all_31_0_10, all_1_0_0) | (member(all_31_0_10, all_1_2_2) & ~ member(all_31_0_10, all_1_1_1)) % 81.57/51.18 | % 81.57/51.18 | Instantiating formula (4) with all_1_0_0, all_31_0_10, all_1_1_1, all_1_2_2 and discharging atoms difference(all_1_2_2, all_1_1_1) = all_1_0_0, yields: % 81.57/51.18 | (39) ~ member(all_31_0_10, all_1_2_2) | member(all_31_0_10, all_1_0_0) | member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 | Instantiating formula (18) with all_31_0_10 yields: % 81.57/51.18 | (40) ~ member(all_31_0_10, ex_10_1_5) | member(all_31_0_10, ex_10_0_4) % 81.57/51.18 | % 81.57/51.18 | Instantiating formula (13) with all_31_0_10 yields: % 81.57/51.18 | (41) ~ member(all_31_0_10, all_1_3_3) | (member(all_31_0_10, all_1_2_2) & ~ member(all_31_0_10, all_1_1_1)) % 81.57/51.18 | % 81.57/51.18 +-Applying beta-rule and splitting (40), into two cases. % 81.57/51.18 |-Branch one: % 81.57/51.18 | (42) ~ member(all_31_0_10, ex_10_1_5) % 81.57/51.18 | % 81.57/51.18 +-Applying beta-rule and splitting (39), into two cases. % 81.57/51.18 |-Branch one: % 81.57/51.18 | (43) ~ member(all_31_0_10, all_1_2_2) % 81.57/51.18 | % 81.57/51.18 +-Applying beta-rule and splitting (41), into two cases. % 81.57/51.18 |-Branch one: % 81.57/51.18 | (44) ~ member(all_31_0_10, all_1_3_3) % 81.57/51.18 | % 81.57/51.18 | From (19) and (36) follows: % 81.57/51.18 | (45) member(all_31_0_10, all_1_3_3) % 81.57/51.18 | % 81.57/51.18 | Using (45) and (44) yields: % 81.57/51.18 | (27) $false % 81.57/51.18 | % 81.57/51.18 |-The branch is then unsatisfiable % 81.57/51.18 |-Branch two: % 81.57/51.18 | (47) member(all_31_0_10, all_1_2_2) & ~ member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 | Applying alpha-rule on (47) yields: % 81.57/51.18 | (48) member(all_31_0_10, all_1_2_2) % 81.57/51.18 | (49) ~ member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 | Using (48) and (43) yields: % 81.57/51.18 | (27) $false % 81.57/51.18 | % 81.57/51.18 |-The branch is then unsatisfiable % 81.57/51.18 |-Branch two: % 81.57/51.18 | (51) member(all_31_0_10, all_1_0_0) | member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 +-Applying beta-rule and splitting (38), into two cases. % 81.57/51.18 |-Branch one: % 81.57/51.18 | (52) ~ member(all_31_0_10, all_1_0_0) % 81.57/51.18 | % 81.57/51.18 +-Applying beta-rule and splitting (51), into two cases. % 81.57/51.18 |-Branch one: % 81.57/51.18 | (53) member(all_31_0_10, all_1_0_0) % 81.57/51.18 | % 81.57/51.18 | Using (53) and (52) yields: % 81.57/51.18 | (27) $false % 81.57/51.18 | % 81.57/51.18 |-The branch is then unsatisfiable % 81.57/51.18 |-Branch two: % 81.57/51.18 | (55) member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 +-Applying beta-rule and splitting (41), into two cases. % 81.57/51.18 |-Branch one: % 81.57/51.18 | (44) ~ member(all_31_0_10, all_1_3_3) % 81.57/51.18 | % 81.57/51.18 | From (19) and (36) follows: % 81.57/51.18 | (45) member(all_31_0_10, all_1_3_3) % 81.57/51.18 | % 81.57/51.18 | Using (45) and (44) yields: % 81.57/51.18 | (27) $false % 81.57/51.18 | % 81.57/51.18 |-The branch is then unsatisfiable % 81.57/51.18 |-Branch two: % 81.57/51.18 | (47) member(all_31_0_10, all_1_2_2) & ~ member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 | Applying alpha-rule on (47) yields: % 81.57/51.18 | (48) member(all_31_0_10, all_1_2_2) % 81.57/51.18 | (49) ~ member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 | Using (55) and (49) yields: % 81.57/51.18 | (27) $false % 81.57/51.18 | % 81.57/51.18 |-The branch is then unsatisfiable % 81.57/51.18 |-Branch two: % 81.57/51.18 | (53) member(all_31_0_10, all_1_0_0) % 81.57/51.18 | (47) member(all_31_0_10, all_1_2_2) & ~ member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 | From (14) and (42) follows: % 81.57/51.18 | (52) ~ member(all_31_0_10, all_1_0_0) % 81.57/51.18 | % 81.57/51.18 | Using (53) and (52) yields: % 81.57/51.18 | (27) $false % 81.57/51.18 | % 81.57/51.18 |-The branch is then unsatisfiable % 81.57/51.18 |-Branch two: % 81.57/51.18 | (67) member(all_31_0_10, ex_10_0_4) % 81.57/51.18 | % 81.57/51.18 +-Applying beta-rule and splitting (39), into two cases. % 81.57/51.18 |-Branch one: % 81.57/51.18 | (43) ~ member(all_31_0_10, all_1_2_2) % 81.57/51.18 | % 81.57/51.18 +-Applying beta-rule and splitting (41), into two cases. % 81.57/51.18 |-Branch one: % 81.57/51.18 | (44) ~ member(all_31_0_10, all_1_3_3) % 81.57/51.18 | % 81.57/51.18 | From (15) and (67) follows: % 81.57/51.18 | (45) member(all_31_0_10, all_1_3_3) % 81.57/51.18 | % 81.57/51.18 | Using (45) and (44) yields: % 81.57/51.18 | (27) $false % 81.57/51.18 | % 81.57/51.18 |-The branch is then unsatisfiable % 81.57/51.18 |-Branch two: % 81.57/51.18 | (47) member(all_31_0_10, all_1_2_2) & ~ member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 | Applying alpha-rule on (47) yields: % 81.57/51.18 | (48) member(all_31_0_10, all_1_2_2) % 81.57/51.18 | (49) ~ member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 | Using (48) and (43) yields: % 81.57/51.18 | (27) $false % 81.57/51.18 | % 81.57/51.18 |-The branch is then unsatisfiable % 81.57/51.18 |-Branch two: % 81.57/51.18 | (51) member(all_31_0_10, all_1_0_0) | member(all_31_0_10, all_1_1_1) % 81.57/51.18 | % 81.57/51.18 +-Applying beta-rule and splitting (38), into two cases. % 81.57/51.18 |-Branch one: % 81.57/51.18 | (52) ~ member(all_31_0_10, all_1_0_0) % 81.57/51.18 | % 81.57/51.18 +-Applying beta-rule and splitting (51), into two cases. % 81.57/51.18 |-Branch one: % 81.57/51.18 | (53) member(all_31_0_10, all_1_0_0) % 81.57/51.19 | % 81.57/51.19 | Using (53) and (52) yields: % 81.57/51.19 | (27) $false % 81.57/51.19 | % 81.57/51.19 |-The branch is then unsatisfiable % 81.57/51.19 |-Branch two: % 81.57/51.19 | (55) member(all_31_0_10, all_1_1_1) % 81.57/51.19 | % 81.57/51.19 +-Applying beta-rule and splitting (41), into two cases. % 81.57/51.19 |-Branch one: % 81.57/51.19 | (44) ~ member(all_31_0_10, all_1_3_3) % 81.57/51.19 | % 81.57/51.19 | From (15) and (67) follows: % 81.57/51.19 | (45) member(all_31_0_10, all_1_3_3) % 81.57/51.19 | % 81.57/51.19 | Using (45) and (44) yields: % 81.57/51.19 | (27) $false % 81.57/51.19 | % 81.57/51.19 |-The branch is then unsatisfiable % 81.57/51.19 |-Branch two: % 81.57/51.19 | (47) member(all_31_0_10, all_1_2_2) & ~ member(all_31_0_10, all_1_1_1) % 81.57/51.19 | % 81.57/51.19 | Applying alpha-rule on (47) yields: % 81.57/51.19 | (48) member(all_31_0_10, all_1_2_2) % 81.57/51.19 | (49) ~ member(all_31_0_10, all_1_1_1) % 81.57/51.19 | % 81.57/51.19 | Using (55) and (49) yields: % 81.57/51.19 | (27) $false % 81.57/51.19 | % 81.57/51.19 |-The branch is then unsatisfiable % 81.57/51.19 |-Branch two: % 81.57/51.19 | (53) member(all_31_0_10, all_1_0_0) % 81.57/51.19 | (47) member(all_31_0_10, all_1_2_2) & ~ member(all_31_0_10, all_1_1_1) % 81.57/51.19 | % 81.57/51.19 | From (20) and (37) follows: % 81.57/51.19 | (52) ~ member(all_31_0_10, all_1_0_0) % 81.57/51.19 | % 81.57/51.19 | Using (53) and (52) yields: % 81.57/51.19 | (27) $false % 81.57/51.19 | % 81.57/51.19 |-The branch is then unsatisfiable % 81.57/51.19 |-Branch two: % 81.57/51.19 | (92) ? [v0] : (member(v0, ex_10_1_5) & ~ member(v0, ex_10_0_4)) % 81.57/51.19 | % 81.57/51.19 | Instantiating (92) with all_12_0_6 yields: % 81.57/51.19 | (93) member(all_12_0_6, ex_10_1_5) & ~ member(all_12_0_6, ex_10_0_4) % 81.57/51.19 | % 81.57/51.19 | Applying alpha-rule on (93) yields: % 81.57/51.19 | (94) member(all_12_0_6, ex_10_1_5) % 81.57/51.19 | (95) ~ member(all_12_0_6, ex_10_0_4) % 81.57/51.19 | % 81.57/51.19 | Instantiating formula (5) with all_1_0_0, all_12_0_6, all_1_1_1, all_1_2_2 and discharging atoms difference(all_1_2_2, all_1_1_1) = all_1_0_0, yields: % 81.57/51.19 | (96) ~ member(all_12_0_6, all_1_0_0) | (member(all_12_0_6, all_1_2_2) & ~ member(all_12_0_6, all_1_1_1)) % 81.57/51.19 | % 81.57/51.19 | Instantiating formula (12) with all_12_0_6 yields: % 81.57/51.19 | (97) ~ member(all_12_0_6, all_1_2_2) | member(all_12_0_6, all_1_1_1) | member(all_12_0_6, all_1_3_3) % 81.57/51.19 | % 81.57/51.19 +-Applying beta-rule and splitting (97), into two cases. % 81.57/51.19 |-Branch one: % 81.57/51.19 | (98) ~ member(all_12_0_6, all_1_2_2) % 81.57/51.19 | % 81.57/51.19 +-Applying beta-rule and splitting (96), into two cases. % 81.57/51.19 |-Branch one: % 81.57/51.19 | (99) ~ member(all_12_0_6, all_1_0_0) % 81.57/51.19 | % 81.57/51.19 | From (14) and (94) follows: % 81.57/51.19 | (100) member(all_12_0_6, all_1_0_0) % 81.57/51.19 | % 81.57/51.19 | Using (100) and (99) yields: % 81.57/51.19 | (27) $false % 81.57/51.19 | % 81.57/51.19 |-The branch is then unsatisfiable % 81.57/51.19 |-Branch two: % 81.57/51.19 | (102) member(all_12_0_6, all_1_2_2) & ~ member(all_12_0_6, all_1_1_1) % 81.57/51.19 | % 81.57/51.19 | Applying alpha-rule on (102) yields: % 81.57/51.19 | (103) member(all_12_0_6, all_1_2_2) % 81.57/51.19 | (104) ~ member(all_12_0_6, all_1_1_1) % 81.57/51.19 | % 81.57/51.19 | Using (103) and (98) yields: % 81.57/51.19 | (27) $false % 81.57/51.19 | % 81.57/51.19 |-The branch is then unsatisfiable % 81.57/51.19 |-Branch two: % 81.57/51.19 | (106) member(all_12_0_6, all_1_1_1) | member(all_12_0_6, all_1_3_3) % 81.57/51.19 | % 81.57/51.19 +-Applying beta-rule and splitting (106), into two cases. % 81.57/51.19 |-Branch one: % 81.57/51.19 | (107) member(all_12_0_6, all_1_1_1) % 81.57/51.19 | % 81.57/51.19 +-Applying beta-rule and splitting (96), into two cases. % 81.57/51.19 |-Branch one: % 81.57/51.19 | (99) ~ member(all_12_0_6, all_1_0_0) % 81.57/51.19 | % 81.57/51.19 | From (14) and (94) follows: % 81.57/51.19 | (100) member(all_12_0_6, all_1_0_0) % 81.57/51.19 | % 81.57/51.19 | Using (100) and (99) yields: % 81.57/51.19 | (27) $false % 81.57/51.19 | % 81.57/51.19 |-The branch is then unsatisfiable % 81.57/51.19 |-Branch two: % 81.57/51.19 | (102) member(all_12_0_6, all_1_2_2) & ~ member(all_12_0_6, all_1_1_1) % 81.57/51.19 | % 81.57/51.19 | Applying alpha-rule on (102) yields: % 81.57/51.19 | (103) member(all_12_0_6, all_1_2_2) % 81.57/51.19 | (104) ~ member(all_12_0_6, all_1_1_1) % 81.57/51.19 | % 81.57/51.19 | Using (107) and (104) yields: % 81.57/51.19 | (27) $false % 81.57/51.19 | % 81.57/51.19 |-The branch is then unsatisfiable % 81.57/51.19 |-Branch two: % 81.57/51.19 | (115) member(all_12_0_6, all_1_3_3) % 81.57/51.19 | % 81.57/51.19 | From (15) and (95) follows: % 81.57/51.19 | (116) ~ member(all_12_0_6, all_1_3_3) % 81.57/51.19 | % 81.57/51.19 | Using (115) and (116) yields: % 81.57/51.19 | (27) $false % 81.57/51.19 | % 81.57/51.19 |-The branch is then unsatisfiable % 81.57/51.19 % SZS output end Proof for theBenchmark % 81.57/51.19 % 81.57/51.19 50564ms %------------------------------------------------------------------------------