%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SET889+1 : TPTP v8.1.0. Bugfixed v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n028.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:57 EDT 2022 % Result : Theorem 54.87s 33.69s % Output : Proof 61.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET889+1 : TPTP v8.1.0. Bugfixed v4.0.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n028.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 : 600 % 0.13/0.34 % DateTime : Sun Jul 10 04:21:12 EDT 2022 % 0.13/0.34 % CPUTime : % 0.65/0.66 ____ _ % 0.65/0.66 ___ / __ \_____(_)___ ________ __________ % 0.65/0.66 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.65/0.66 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.65/0.66 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.65/0.66 % 0.65/0.66 A Theorem Prover for First-Order Logic % 0.65/0.66 (ePrincess v.1.0) % 0.65/0.66 % 0.65/0.66 (c) Philipp Rümmer, 2009-2015 % 0.65/0.66 (c) Peter Backeman, 2014-2015 % 0.65/0.66 (contributions by Angelo Brillout, Peter Baumgartner) % 0.65/0.66 Free software under GNU Lesser General Public License (LGPL). % 0.65/0.66 Bug reports to peter@backeman.se % 0.65/0.66 % 0.65/0.66 For more information, visit http://user.uu.se/~petba168/breu/ % 0.65/0.66 % 0.65/0.66 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.74/0.71 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.50/0.96 Prover 0: Preprocessing ... % 1.83/1.13 Prover 0: Warning: ignoring some quantifiers % 1.99/1.15 Prover 0: Constructing countermodel ... % 2.70/1.36 Prover 0: gave up % 2.70/1.36 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 2.70/1.38 Prover 1: Preprocessing ... % 3.02/1.46 Prover 1: Warning: ignoring some quantifiers % 3.02/1.46 Prover 1: Constructing countermodel ... % 3.15/1.53 Prover 1: gave up % 3.15/1.53 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.36/1.55 Prover 2: Preprocessing ... % 3.45/1.61 Prover 2: Warning: ignoring some quantifiers % 3.45/1.61 Prover 2: Constructing countermodel ... % 3.99/1.68 Prover 2: gave up % 3.99/1.68 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.99/1.70 Prover 3: Preprocessing ... % 3.99/1.72 Prover 3: Warning: ignoring some quantifiers % 3.99/1.72 Prover 3: Constructing countermodel ... % 4.45/1.78 Prover 3: gave up % 4.45/1.78 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 4.45/1.79 Prover 4: Preprocessing ... % 4.75/1.85 Prover 4: Warning: ignoring some quantifiers % 4.75/1.85 Prover 4: Constructing countermodel ... % 5.38/2.04 Prover 4: gave up % 5.38/2.04 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 5.38/2.05 Prover 5: Preprocessing ... % 5.85/2.08 Prover 5: Warning: ignoring some quantifiers % 5.85/2.08 Prover 5: Constructing countermodel ... % 6.04/2.13 Prover 5: gave up % 6.04/2.13 Prover 6: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 6.04/2.13 Prover 6: Preprocessing ... % 6.23/2.16 Prover 6: Warning: ignoring some quantifiers % 6.23/2.17 Prover 6: Constructing countermodel ... % 6.23/2.21 Prover 6: gave up % 6.23/2.21 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximalOutermost -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 6.23/2.22 Prover 7: Preprocessing ... % 6.23/2.24 Prover 7: Proving ... % 28.37/12.94 Prover 8: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 28.37/12.96 Prover 8: Preprocessing ... % 28.77/13.00 Prover 8: Proving ... % 50.80/31.45 Prover 9: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=completeFrugal % 50.80/31.46 Prover 9: Preprocessing ... % 50.87/31.50 Prover 9: Proving ... % 54.87/33.69 Prover 9: proved (2236ms) % 54.87/33.69 Prover 7: stopped % 54.87/33.69 Prover 8: stopped % 54.87/33.69 % 54.87/33.69 % SZS status Theorem for theBenchmark % 54.87/33.69 % 54.87/33.69 Generating proof ... found it (size 80) % 61.62/37.47 % 61.62/37.47 % SZS output start Proof for theBenchmark % 61.62/37.47 Assumed formulas after preprocessing and simplification: % 61.62/37.47 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ( ~ (v4 = v3) & singleton(v1) = v2 & powerset(v2) = v3 & unordered_pair(v0, v2) = v4 & empty(v6) & empty(v0) & ~ empty(v5) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = v8 | v10 = v7 | ~ (unordered_pair(v7, v8) = v9) | ~ in(v10, v9)) & ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (unordered_pair(v10, v9) = v8) | ~ (unordered_pair(v10, v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v9 = v7 | v7 = v0 | ~ (singleton(v8) = v9) | ~ subset(v7, v9)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (singleton(v9) = v8) | ~ (singleton(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : (v8 = v7 | ~ (powerset(v9) = v8) | ~ (powerset(v9) = v7)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (unordered_pair(v7, v8) = v9) | in(v8, v9)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (unordered_pair(v7, v8) = v9) | in(v7, v9)) & ! [v7] : ! [v8] : ! [v9] : ( ~ (unordered_pair(v7, v8) = v9) | ! [v10] : (v10 = v9 | ? [v11] : ((v11 = v8 | v11 = v7 | in(v11, v10)) & ( ~ in(v11, v10) | ( ~ (v11 = v8) & ~ (v11 = v7)))))) & ! [v7] : ! [v8] : (v8 = v7 | ? [v9] : (( ~ in(v9, v8) | ~ in(v9, v7)) & (in(v9, v8) | in(v9, v7)))) & ! [v7] : ! [v8] : ( ~ subset(v8, v7) | ! [v9] : (in(v8, v9) | ? [v10] : ( ~ (v10 = v9) & powerset(v7) = v10))) & ! [v7] : ! [v8] : ( ~ in(v8, v7) | ~ in(v7, v8)) & ! [v7] : ! [v8] : ( ~ in(v8, v7) | ! [v9] : (subset(v8, v9) | ? [v10] : ( ~ (v10 = v7) & powerset(v9) = v10))) & ! [v7] : subset(v7, v7) & ! [v7] : ! [v8] : ? [v9] : ((v9 = v8 & powerset(v7) = v8) | (( ~ subset(v9, v7) | ~ in(v9, v8)) & (subset(v9, v7) | in(v9, v8)))) & ! [v7] : ! [v8] : ? [v9] : (singleton(v8) = v9 & (subset(v7, v9) | ( ~ (v9 = v7) & ~ (v7 = v0)))) & ! [v7] : ! [v8] : ? [v9] : (unordered_pair(v8, v7) = v9 & unordered_pair(v7, v8) = v9)) % 61.73/37.50 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 yields: % 61.73/37.50 | (1) ~ (all_0_2_2 = all_0_3_3) & singleton(all_0_5_5) = all_0_4_4 & powerset(all_0_4_4) = all_0_3_3 & unordered_pair(all_0_6_6, all_0_4_4) = all_0_2_2 & empty(all_0_0_0) & empty(all_0_6_6) & ~ empty(all_0_1_1) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | v3 = v0 | ~ (unordered_pair(v0, v1) = v2) | ~ in(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (unordered_pair(v3, v2) = v1) | ~ (unordered_pair(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | v0 = all_0_6_6 | ~ (singleton(v1) = v2) | ~ subset(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | in(v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | in(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | ! [v3] : (v3 = v2 | ? [v4] : ((v4 = v1 | v4 = v0 | in(v4, v3)) & ( ~ in(v4, v3) | ( ~ (v4 = v1) & ~ (v4 = v0)))))) & ! [v0] : ! [v1] : (v1 = v0 | ? [v2] : (( ~ in(v2, v1) | ~ in(v2, v0)) & (in(v2, v1) | in(v2, v0)))) & ! [v0] : ! [v1] : ( ~ subset(v1, v0) | ! [v2] : (in(v1, v2) | ? [v3] : ( ~ (v3 = v2) & powerset(v0) = v3))) & ! [v0] : ! [v1] : ( ~ in(v1, v0) | ~ in(v0, v1)) & ! [v0] : ! [v1] : ( ~ in(v1, v0) | ! [v2] : (subset(v1, v2) | ? [v3] : ( ~ (v3 = v0) & powerset(v2) = v3))) & ! [v0] : subset(v0, v0) & ! [v0] : ! [v1] : ? [v2] : ((v2 = v1 & powerset(v0) = v1) | (( ~ subset(v2, v0) | ~ in(v2, v1)) & (subset(v2, v0) | in(v2, v1)))) & ! [v0] : ! [v1] : ? [v2] : (singleton(v1) = v2 & (subset(v0, v2) | ( ~ (v2 = v0) & ~ (v0 = all_0_6_6)))) & ! [v0] : ! [v1] : ? [v2] : (unordered_pair(v1, v0) = v2 & unordered_pair(v0, v1) = v2) % 61.73/37.50 | % 61.73/37.50 | Applying alpha-rule on (1) yields: % 61.73/37.50 | (2) empty(all_0_0_0) % 61.73/37.50 | (3) ~ empty(all_0_1_1) % 61.73/37.50 | (4) ! [v0] : subset(v0, v0) % 61.73/37.50 | (5) ! [v0] : ! [v1] : (v1 = v0 | ? [v2] : (( ~ in(v2, v1) | ~ in(v2, v0)) & (in(v2, v1) | in(v2, v0)))) % 61.73/37.50 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (unordered_pair(v3, v2) = v1) | ~ (unordered_pair(v3, v2) = v0)) % 61.73/37.50 | (7) ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | ! [v3] : (v3 = v2 | ? [v4] : ((v4 = v1 | v4 = v0 | in(v4, v3)) & ( ~ in(v4, v3) | ( ~ (v4 = v1) & ~ (v4 = v0)))))) % 61.73/37.50 | (8) ! [v0] : ! [v1] : ? [v2] : (unordered_pair(v1, v0) = v2 & unordered_pair(v0, v1) = v2) % 61.73/37.51 | (9) ! [v0] : ! [v1] : ( ~ in(v1, v0) | ! [v2] : (subset(v1, v2) | ? [v3] : ( ~ (v3 = v0) & powerset(v2) = v3))) % 61.73/37.51 | (10) powerset(all_0_4_4) = all_0_3_3 % 61.73/37.51 | (11) empty(all_0_6_6) % 61.73/37.51 | (12) ~ (all_0_2_2 = all_0_3_3) % 61.73/37.51 | (13) ! [v0] : ! [v1] : ( ~ in(v1, v0) | ~ in(v0, v1)) % 61.73/37.51 | (14) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) % 61.73/37.51 | (15) ! [v0] : ! [v1] : ? [v2] : ((v2 = v1 & powerset(v0) = v1) | (( ~ subset(v2, v0) | ~ in(v2, v1)) & (subset(v2, v0) | in(v2, v1)))) % 61.73/37.51 | (16) ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | v0 = all_0_6_6 | ~ (singleton(v1) = v2) | ~ subset(v0, v2)) % 61.73/37.51 | (17) ! [v0] : ! [v1] : ? [v2] : (singleton(v1) = v2 & (subset(v0, v2) | ( ~ (v2 = v0) & ~ (v0 = all_0_6_6)))) % 61.73/37.51 | (18) singleton(all_0_5_5) = all_0_4_4 % 61.73/37.51 | (19) ! [v0] : ! [v1] : ( ~ subset(v1, v0) | ! [v2] : (in(v1, v2) | ? [v3] : ( ~ (v3 = v2) & powerset(v0) = v3))) % 61.73/37.51 | (20) ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | in(v1, v2)) % 61.73/37.51 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | v3 = v0 | ~ (unordered_pair(v0, v1) = v2) | ~ in(v3, v2)) % 61.73/37.51 | (22) unordered_pair(all_0_6_6, all_0_4_4) = all_0_2_2 % 61.73/37.51 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) % 61.73/37.51 | (24) ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | in(v0, v2)) % 61.73/37.51 | % 61.73/37.51 | Instantiating formula (20) with all_0_2_2, all_0_4_4, all_0_6_6 and discharging atoms unordered_pair(all_0_6_6, all_0_4_4) = all_0_2_2, yields: % 61.73/37.51 | (25) in(all_0_4_4, all_0_2_2) % 61.73/37.51 | % 61.73/37.51 | Instantiating formula (24) with all_0_2_2, all_0_4_4, all_0_6_6 and discharging atoms unordered_pair(all_0_6_6, all_0_4_4) = all_0_2_2, yields: % 61.73/37.51 | (26) in(all_0_6_6, all_0_2_2) % 61.73/37.51 | % 61.73/37.51 | Introducing new symbol ex_15_1_8 defined by: % 61.73/37.51 | (27) ex_15_1_8 = all_0_4_4 % 61.73/37.51 | % 61.73/37.51 | Introducing new symbol ex_15_0_7 defined by: % 61.73/37.51 | (28) ex_15_0_7 = all_0_2_2 % 61.73/37.51 | % 61.73/37.51 | Instantiating formula (15) with ex_15_0_7, ex_15_1_8 yields: % 61.73/37.51 | (29) ? [v0] : ((v0 = ex_15_0_7 & powerset(ex_15_1_8) = ex_15_0_7) | (( ~ subset(v0, ex_15_1_8) | ~ in(v0, ex_15_0_7)) & (subset(v0, ex_15_1_8) | in(v0, ex_15_0_7)))) % 61.73/37.51 | % 61.73/37.51 | Instantiating (29) with all_16_0_9 yields: % 61.73/37.51 | (30) (all_16_0_9 = ex_15_0_7 & powerset(ex_15_1_8) = ex_15_0_7) | (( ~ subset(all_16_0_9, ex_15_1_8) | ~ in(all_16_0_9, ex_15_0_7)) & (subset(all_16_0_9, ex_15_1_8) | in(all_16_0_9, ex_15_0_7))) % 61.73/37.51 | % 61.73/37.51 +-Applying beta-rule and splitting (30), into two cases. % 61.73/37.51 |-Branch one: % 61.73/37.51 | (31) all_16_0_9 = ex_15_0_7 & powerset(ex_15_1_8) = ex_15_0_7 % 61.73/37.51 | % 61.73/37.51 | Applying alpha-rule on (31) yields: % 61.73/37.51 | (32) all_16_0_9 = ex_15_0_7 % 61.73/37.51 | (33) powerset(ex_15_1_8) = ex_15_0_7 % 61.73/37.51 | % 61.73/37.51 | From (27)(28) and (33) follows: % 61.73/37.51 | (34) powerset(all_0_4_4) = all_0_2_2 % 61.73/37.51 | % 61.73/37.51 | Instantiating formula (14) with all_0_4_4, all_0_3_3, all_0_2_2 and discharging atoms powerset(all_0_4_4) = all_0_2_2, powerset(all_0_4_4) = all_0_3_3, yields: % 61.73/37.51 | (35) all_0_2_2 = all_0_3_3 % 61.73/37.51 | % 61.73/37.51 | Equations (35) can reduce 12 to: % 61.73/37.51 | (36) $false % 61.73/37.51 | % 61.73/37.51 |-The branch is then unsatisfiable % 61.73/37.51 |-Branch two: % 61.73/37.51 | (37) ( ~ subset(all_16_0_9, ex_15_1_8) | ~ in(all_16_0_9, ex_15_0_7)) & (subset(all_16_0_9, ex_15_1_8) | in(all_16_0_9, ex_15_0_7)) % 61.73/37.51 | % 61.73/37.51 | Applying alpha-rule on (37) yields: % 61.73/37.51 | (38) ~ subset(all_16_0_9, ex_15_1_8) | ~ in(all_16_0_9, ex_15_0_7) % 61.73/37.51 | (39) subset(all_16_0_9, ex_15_1_8) | in(all_16_0_9, ex_15_0_7) % 61.73/37.51 | % 61.73/37.51 +-Applying beta-rule and splitting (39), into two cases. % 61.73/37.51 |-Branch one: % 61.73/37.51 | (40) in(all_16_0_9, ex_15_0_7) % 61.73/37.51 | % 61.73/37.51 +-Applying beta-rule and splitting (38), into two cases. % 61.73/37.51 |-Branch one: % 61.73/37.51 | (41) ~ in(all_16_0_9, ex_15_0_7) % 61.73/37.51 | % 61.73/37.51 | Using (40) and (41) yields: % 61.73/37.51 | (42) $false % 61.73/37.51 | % 61.73/37.51 |-The branch is then unsatisfiable % 61.73/37.51 |-Branch two: % 61.73/37.51 | (43) ~ subset(all_16_0_9, ex_15_1_8) % 61.73/37.51 | % 61.73/37.51 | Instantiating formula (21) with all_16_0_9, all_0_2_2, all_0_4_4, all_0_6_6 and discharging atoms unordered_pair(all_0_6_6, all_0_4_4) = all_0_2_2, yields: % 61.73/37.52 | (44) all_16_0_9 = all_0_4_4 | all_16_0_9 = all_0_6_6 | ~ in(all_16_0_9, all_0_2_2) % 61.73/37.52 | % 61.73/37.52 +-Applying beta-rule and splitting (44), into two cases. % 61.73/37.52 |-Branch one: % 61.73/37.52 | (45) ~ in(all_16_0_9, all_0_2_2) % 61.73/37.52 | % 61.73/37.52 | From (28) and (40) follows: % 61.73/37.52 | (46) in(all_16_0_9, all_0_2_2) % 61.73/37.52 | % 61.73/37.52 | Using (46) and (45) yields: % 61.73/37.52 | (42) $false % 61.73/37.52 | % 61.73/37.52 |-The branch is then unsatisfiable % 61.73/37.52 |-Branch two: % 61.73/37.52 | (48) all_16_0_9 = all_0_4_4 | all_16_0_9 = all_0_6_6 % 61.73/37.52 | % 61.73/37.52 +-Applying beta-rule and splitting (48), into two cases. % 61.73/37.52 |-Branch one: % 61.73/37.52 | (49) all_16_0_9 = all_0_4_4 % 61.73/37.52 | % 61.73/37.52 | From (49) and (43) follows: % 61.73/37.52 | (50) ~ subset(all_0_4_4, ex_15_1_8) % 61.73/37.52 | % 61.73/37.52 | Introducing new symbol ex_65_1_22 defined by: % 61.73/37.52 | (51) ex_65_1_22 = all_16_0_9 % 61.73/37.52 | % 61.73/37.52 | Introducing new symbol ex_65_0_21 defined by: % 61.73/37.52 | (52) ex_65_0_21 = all_0_5_5 % 61.73/37.52 | % 61.73/37.52 | Instantiating formula (17) with ex_65_0_21, ex_65_1_22 yields: % 61.73/37.52 | (53) ? [v0] : (singleton(ex_65_0_21) = v0 & (subset(ex_65_1_22, v0) | ( ~ (v0 = ex_65_1_22) & ~ (ex_65_1_22 = all_0_6_6)))) % 61.73/37.52 | % 61.73/37.52 | Instantiating (53) with all_66_0_23 yields: % 61.73/37.52 | (54) singleton(ex_65_0_21) = all_66_0_23 & (subset(ex_65_1_22, all_66_0_23) | ( ~ (all_66_0_23 = ex_65_1_22) & ~ (ex_65_1_22 = all_0_6_6))) % 61.73/37.52 | % 61.73/37.52 | Applying alpha-rule on (54) yields: % 61.73/37.52 | (55) singleton(ex_65_0_21) = all_66_0_23 % 61.73/37.52 | (56) subset(ex_65_1_22, all_66_0_23) | ( ~ (all_66_0_23 = ex_65_1_22) & ~ (ex_65_1_22 = all_0_6_6)) % 61.73/37.52 | % 61.73/37.52 +-Applying beta-rule and splitting (56), into two cases. % 61.73/37.52 |-Branch one: % 61.73/37.52 | (57) subset(ex_65_1_22, all_66_0_23) % 61.73/37.52 | % 61.73/37.52 | Combining equations (49,51) yields a new equation: % 61.73/37.52 | (58) ex_65_1_22 = all_0_4_4 % 61.73/37.52 | % 61.73/37.52 | From (52) and (55) follows: % 61.73/37.52 | (59) singleton(all_0_5_5) = all_66_0_23 % 61.73/37.52 | % 61.73/37.52 | From (58) and (57) follows: % 61.73/37.52 | (60) subset(all_0_4_4, all_66_0_23) % 61.73/37.52 | % 61.73/37.52 | From (27) and (50) follows: % 61.73/37.52 | (61) ~ subset(all_0_4_4, all_0_4_4) % 61.73/37.52 | % 61.73/37.52 | Instantiating formula (23) with all_0_5_5, all_0_4_4, all_66_0_23 and discharging atoms singleton(all_0_5_5) = all_66_0_23, singleton(all_0_5_5) = all_0_4_4, yields: % 61.73/37.52 | (62) all_66_0_23 = all_0_4_4 % 61.73/37.52 | % 61.73/37.52 | From (62) and (60) follows: % 61.73/37.52 | (63) subset(all_0_4_4, all_0_4_4) % 61.73/37.52 | % 61.73/37.52 | Using (63) and (61) yields: % 61.73/37.52 | (42) $false % 61.73/37.52 | % 61.73/37.52 |-The branch is then unsatisfiable % 61.73/37.52 |-Branch two: % 61.73/37.52 | (65) ~ (all_66_0_23 = ex_65_1_22) & ~ (ex_65_1_22 = all_0_6_6) % 61.73/37.52 | % 61.73/37.52 | Applying alpha-rule on (65) yields: % 61.73/37.52 | (66) ~ (all_66_0_23 = ex_65_1_22) % 61.73/37.52 | (67) ~ (ex_65_1_22 = all_0_6_6) % 61.73/37.52 | % 61.73/37.52 | Combining equations (49,51) yields a new equation: % 61.73/37.52 | (58) ex_65_1_22 = all_0_4_4 % 61.73/37.52 | % 61.73/37.52 | Equations (58) can reduce 66 to: % 61.73/37.52 | (69) ~ (all_66_0_23 = all_0_4_4) % 61.73/37.52 | % 61.73/37.52 | From (52) and (55) follows: % 61.73/37.52 | (59) singleton(all_0_5_5) = all_66_0_23 % 61.73/37.52 | % 61.73/37.52 | Instantiating formula (23) with all_0_5_5, all_0_4_4, all_66_0_23 and discharging atoms singleton(all_0_5_5) = all_66_0_23, singleton(all_0_5_5) = all_0_4_4, yields: % 61.92/37.52 | (62) all_66_0_23 = all_0_4_4 % 61.92/37.52 | % 61.92/37.52 | Equations (62) can reduce 69 to: % 61.92/37.52 | (36) $false % 61.92/37.52 | % 61.92/37.52 |-The branch is then unsatisfiable % 61.92/37.52 |-Branch two: % 61.92/37.52 | (73) all_16_0_9 = all_0_6_6 % 61.92/37.52 | % 61.92/37.52 | From (73) and (43) follows: % 61.92/37.52 | (74) ~ subset(all_0_6_6, ex_15_1_8) % 61.92/37.52 | % 61.92/37.52 | Introducing new symbol ex_65_1_25 defined by: % 61.92/37.52 | (75) ex_65_1_25 = all_16_0_9 % 61.92/37.52 | % 61.92/37.52 | Introducing new symbol ex_65_0_24 defined by: % 61.92/37.52 | (76) ex_65_0_24 = all_0_5_5 % 61.92/37.52 | % 61.92/37.52 | Instantiating formula (17) with ex_65_0_24, ex_65_1_25 yields: % 61.92/37.52 | (77) ? [v0] : (singleton(ex_65_0_24) = v0 & (subset(ex_65_1_25, v0) | ( ~ (v0 = ex_65_1_25) & ~ (ex_65_1_25 = all_0_6_6)))) % 61.92/37.52 | % 61.92/37.52 | Instantiating (77) with all_66_0_26 yields: % 61.92/37.52 | (78) singleton(ex_65_0_24) = all_66_0_26 & (subset(ex_65_1_25, all_66_0_26) | ( ~ (all_66_0_26 = ex_65_1_25) & ~ (ex_65_1_25 = all_0_6_6))) % 61.92/37.52 | % 61.92/37.52 | Applying alpha-rule on (78) yields: % 61.92/37.52 | (79) singleton(ex_65_0_24) = all_66_0_26 % 61.92/37.52 | (80) subset(ex_65_1_25, all_66_0_26) | ( ~ (all_66_0_26 = ex_65_1_25) & ~ (ex_65_1_25 = all_0_6_6)) % 61.92/37.52 | % 61.92/37.52 +-Applying beta-rule and splitting (80), into two cases. % 61.92/37.52 |-Branch one: % 61.92/37.52 | (81) subset(ex_65_1_25, all_66_0_26) % 61.92/37.52 | % 61.92/37.52 | Combining equations (73,75) yields a new equation: % 61.92/37.52 | (82) ex_65_1_25 = all_0_6_6 % 61.92/37.52 | % 61.92/37.52 | From (76) and (79) follows: % 61.92/37.52 | (83) singleton(all_0_5_5) = all_66_0_26 % 61.92/37.52 | % 61.92/37.52 | From (82) and (81) follows: % 61.92/37.52 | (84) subset(all_0_6_6, all_66_0_26) % 61.92/37.52 | % 61.92/37.52 | From (27) and (74) follows: % 61.92/37.52 | (85) ~ subset(all_0_6_6, all_0_4_4) % 61.92/37.52 | % 61.92/37.52 | Instantiating formula (23) with all_0_5_5, all_0_4_4, all_66_0_26 and discharging atoms singleton(all_0_5_5) = all_66_0_26, singleton(all_0_5_5) = all_0_4_4, yields: % 61.92/37.52 | (86) all_66_0_26 = all_0_4_4 % 61.92/37.52 | % 61.92/37.52 | From (86) and (84) follows: % 61.92/37.52 | (87) subset(all_0_6_6, all_0_4_4) % 61.92/37.52 | % 61.92/37.52 | Using (87) and (85) yields: % 61.92/37.52 | (42) $false % 61.92/37.52 | % 61.92/37.52 |-The branch is then unsatisfiable % 61.92/37.52 |-Branch two: % 61.92/37.52 | (89) ~ (all_66_0_26 = ex_65_1_25) & ~ (ex_65_1_25 = all_0_6_6) % 61.92/37.52 | % 61.92/37.52 | Applying alpha-rule on (89) yields: % 61.92/37.52 | (90) ~ (all_66_0_26 = ex_65_1_25) % 61.92/37.52 | (91) ~ (ex_65_1_25 = all_0_6_6) % 61.92/37.52 | % 61.92/37.52 | Combining equations (73,75) yields a new equation: % 61.92/37.52 | (82) ex_65_1_25 = all_0_6_6 % 61.92/37.52 | % 61.92/37.52 | Equations (82) can reduce 91 to: % 61.92/37.52 | (36) $false % 61.92/37.52 | % 61.92/37.52 |-The branch is then unsatisfiable % 61.92/37.52 |-Branch two: % 61.92/37.52 | (41) ~ in(all_16_0_9, ex_15_0_7) % 61.92/37.52 | (95) subset(all_16_0_9, ex_15_1_8) % 61.92/37.53 | % 61.92/37.53 | Instantiating formula (16) with all_0_4_4, all_0_5_5, all_16_0_9 and discharging atoms singleton(all_0_5_5) = all_0_4_4, yields: % 61.92/37.53 | (96) all_16_0_9 = all_0_4_4 | all_16_0_9 = all_0_6_6 | ~ subset(all_16_0_9, all_0_4_4) % 61.92/37.53 | % 61.92/37.53 +-Applying beta-rule and splitting (96), into two cases. % 61.92/37.53 |-Branch one: % 61.92/37.53 | (97) ~ subset(all_16_0_9, all_0_4_4) % 61.92/37.53 | % 61.92/37.53 | From (27) and (95) follows: % 61.92/37.53 | (98) subset(all_16_0_9, all_0_4_4) % 61.92/37.53 | % 61.92/37.53 | Using (98) and (97) yields: % 61.92/37.53 | (42) $false % 61.92/37.53 | % 61.92/37.53 |-The branch is then unsatisfiable % 61.92/37.53 |-Branch two: % 61.92/37.53 | (48) all_16_0_9 = all_0_4_4 | all_16_0_9 = all_0_6_6 % 61.92/37.53 | % 61.92/37.53 +-Applying beta-rule and splitting (48), into two cases. % 61.92/37.53 |-Branch one: % 61.92/37.53 | (49) all_16_0_9 = all_0_4_4 % 61.92/37.53 | % 61.92/37.53 | From (49) and (41) follows: % 61.92/37.53 | (102) ~ in(all_0_4_4, ex_15_0_7) % 61.92/37.53 | % 61.92/37.53 | From (28) and (102) follows: % 61.92/37.53 | (103) ~ in(all_0_4_4, all_0_2_2) % 61.92/37.53 | % 61.92/37.53 | Using (25) and (103) yields: % 61.92/37.53 | (42) $false % 61.92/37.53 | % 61.92/37.53 |-The branch is then unsatisfiable % 61.92/37.53 |-Branch two: % 61.92/37.53 | (73) all_16_0_9 = all_0_6_6 % 61.92/37.53 | % 61.92/37.53 | From (73) and (41) follows: % 61.92/37.53 | (106) ~ in(all_0_6_6, ex_15_0_7) % 61.92/37.53 | % 61.92/37.53 | From (28) and (106) follows: % 61.92/37.53 | (107) ~ in(all_0_6_6, all_0_2_2) % 61.92/37.53 | % 61.92/37.53 | Using (26) and (107) yields: % 61.92/37.53 | (42) $false % 61.92/37.53 | % 61.92/37.53 |-The branch is then unsatisfiable % 61.92/37.53 % SZS output end Proof for theBenchmark % 61.92/37.53 % 61.92/37.53 36857ms %------------------------------------------------------------------------------