%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEU146+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n023.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 08:46:57 EDT 2022 % Result : Theorem 9.68s 3.02s % Output : Proof 11.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SEU146+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n023.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 : Sat Jun 18 23:07:34 EDT 2022 % 0.12/0.33 % CPUTime : % 0.57/0.58 ____ _ % 0.57/0.58 ___ / __ \_____(_)___ ________ __________ % 0.57/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.57/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.57/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.57/0.58 % 0.57/0.58 A Theorem Prover for First-Order Logic % 0.57/0.59 (ePrincess v.1.0) % 0.57/0.59 % 0.57/0.59 (c) Philipp Rümmer, 2009-2015 % 0.57/0.59 (c) Peter Backeman, 2014-2015 % 0.57/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.57/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.57/0.59 Bug reports to peter@backeman.se % 0.57/0.59 % 0.57/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.57/0.59 % 0.57/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.75/0.66 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.44/0.93 Prover 0: Preprocessing ... % 1.68/1.06 Prover 0: Warning: ignoring some quantifiers % 1.68/1.07 Prover 0: Constructing countermodel ... % 2.33/1.23 Prover 0: gave up % 2.33/1.23 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 2.35/1.25 Prover 1: Preprocessing ... % 2.61/1.33 Prover 1: Constructing countermodel ... % 2.83/1.40 Prover 1: gave up % 2.83/1.40 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.83/1.42 Prover 2: Preprocessing ... % 3.23/1.48 Prover 2: Warning: ignoring some quantifiers % 3.23/1.49 Prover 2: Constructing countermodel ... % 3.55/1.57 Prover 2: gave up % 3.55/1.57 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.55/1.58 Prover 3: Preprocessing ... % 3.55/1.60 Prover 3: Warning: ignoring some quantifiers % 3.55/1.60 Prover 3: Constructing countermodel ... % 3.97/1.64 Prover 3: gave up % 3.97/1.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 3.97/1.65 Prover 4: Preprocessing ... % 4.27/1.70 Prover 4: Warning: ignoring some quantifiers % 4.27/1.70 Prover 4: Constructing countermodel ... % 9.14/2.88 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 9.14/2.89 Prover 5: Preprocessing ... % 9.40/2.95 Prover 5: Constructing countermodel ... % 9.68/3.02 Prover 5: proved (138ms) % 9.68/3.02 Prover 4: stopped % 9.68/3.02 % 9.68/3.02 No countermodel exists, formula is valid % 9.68/3.02 % SZS status Theorem for theBenchmark % 9.68/3.02 % 9.68/3.02 Generating proof ... found it (size 109) % 11.05/3.28 % 11.05/3.28 % SZS output start Proof for theBenchmark % 11.05/3.29 Assumed formulas after preprocessing and simplification: % 11.05/3.29 | (0) empty(empty_set) = 0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (set_difference(v1, v3) = v4) | ~ (singleton(v2) = v3) | ~ (subset(v0, v4) = v5) | ? [v6] : ? [v7] : (subset(v0, v1) = v6 & in(v2, v0) = v7 & ( ~ (v6 = 0) | v7 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = 0 | ~ (set_difference(v1, v4) = v5) | ~ (singleton(v2) = v4) | ~ (in(v2, v0) = v3) | ? [v6] : ? [v7] : (subset(v0, v5) = v7 & subset(v0, v1) = v6 & ( ~ (v6 = 0) | v7 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (singleton(v0) = v2) | ~ (subset(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & in(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subset(v0, v1) = 0) | ~ (in(v2, v0) = v3) | ? [v4] : ? [v5] : (set_difference(v1, v4) = v5 & singleton(v2) = v4 & subset(v0, v5) = 0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (set_difference(v3, v2) = v1) | ~ (set_difference(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (singleton(v2) = v3) | ~ (subset(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (set_difference(v1, v3) = v5 & subset(v0, v5) = v6 & in(v2, v0) = v4 & (v6 = 0 | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : (v2 = empty_set | ~ (set_difference(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & subset(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ( ~ (v3 = empty_set) & set_difference(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & singleton(v0) = v3 & subset(v3, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (singleton(v0) = v2) | ~ (subset(v2, v1) = 0) | in(v0, v1) = 0) & ! [v0] : ! [v1] : (v1 = v0 | ~ (subset(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subset(v0, v1) = v2)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (subset(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subset(v1, v0) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(empty_set, v0) = v1)) & ! [v0] : ! [v1] : ( ~ (set_difference(v0, v1) = empty_set) | subset(v0, v1) = 0) & ! [v0] : ! [v1] : ( ~ (subset(v0, v1) = 0) | set_difference(v0, v1) = empty_set) & ! [v0] : ! [v1] : ( ~ (in(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v0, v1) = v2)) & ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v1, v0) = v2)) & ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : (singleton(v0) = v2 & subset(v2, v1) = 0)) & ! [v0] : (v0 = empty_set | ~ (subset(v0, empty_set) = 0)) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : (singleton(v1) = v2 & subset(v0, v2) = v3 & ((v3 = 0 & ~ (v2 = v0) & ~ (v0 = empty_set)) | ( ~ (v3 = 0) & (v2 = v0 | v0 = empty_set)))) & ? [v0] : ? [v1] : ( ~ (v1 = 0) & empty(v0) = v1) & ? [v0] : empty(v0) = 0 % 11.05/3.32 | Applying alpha-rule on (0) yields: % 11.05/3.32 | (1) ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) % 11.05/3.32 | (2) ? [v0] : ? [v1] : ( ~ (v1 = 0) & empty(v0) = v1) % 11.05/3.32 | (3) ! [v0] : ! [v1] : ( ~ (subset(v0, v1) = 0) | set_difference(v0, v1) = empty_set) % 11.05/3.32 | (4) ! [v0] : ! [v1] : ( ~ (set_difference(v0, v1) = empty_set) | subset(v0, v1) = 0) % 11.05/3.32 | (5) ! [v0] : ! [v1] : (v1 = v0 | ~ (subset(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & subset(v1, v0) = v2)) % 11.05/3.32 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) % 11.05/3.32 | (7) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v1, v0) = v2)) % 11.05/3.32 | (8) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (singleton(v1) = v2 & subset(v0, v2) = v3 & ((v3 = 0 & ~ (v2 = v0) & ~ (v0 = empty_set)) | ( ~ (v3 = 0) & (v2 = v0 | v0 = empty_set)))) % 11.05/3.33 | (9) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ( ~ (v3 = empty_set) & set_difference(v0, v1) = v3)) % 11.05/3.33 | (10) ! [v0] : ! [v1] : ! [v2] : (v2 = empty_set | ~ (set_difference(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & subset(v0, v1) = v3)) % 11.05/3.33 | (11) ! [v0] : ! [v1] : ! [v2] : ( ~ (singleton(v0) = v2) | ~ (subset(v2, v1) = 0) | in(v0, v1) = 0) % 11.05/3.33 | (12) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : (singleton(v0) = v2 & subset(v2, v1) = 0)) % 11.05/3.33 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = 0 | ~ (set_difference(v1, v4) = v5) | ~ (singleton(v2) = v4) | ~ (in(v2, v0) = v3) | ? [v6] : ? [v7] : (subset(v0, v5) = v7 & subset(v0, v1) = v6 & ( ~ (v6 = 0) | v7 = 0))) % 11.05/3.33 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subset(v0, v1) = 0) | ~ (in(v2, v0) = v3) | ? [v4] : ? [v5] : (set_difference(v1, v4) = v5 & singleton(v2) = v4 & subset(v0, v5) = 0)) % 11.05/3.33 | (15) ! [v0] : ! [v1] : (v1 = v0 | ~ (subset(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & subset(v0, v1) = v2)) % 11.05/3.33 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (set_difference(v3, v2) = v1) | ~ (set_difference(v3, v2) = v0)) % 11.05/3.33 | (17) ! [v0] : (v0 = empty_set | ~ (subset(v0, empty_set) = 0)) % 11.05/3.33 | (18) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & singleton(v0) = v3 & subset(v3, v1) = v4)) % 11.05/3.33 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (singleton(v2) = v3) | ~ (subset(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (set_difference(v1, v3) = v5 & subset(v0, v5) = v6 & in(v2, v0) = v4 & (v6 = 0 | v4 = 0))) % 11.05/3.33 | (20) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) % 11.05/3.33 | (21) empty(empty_set) = 0 % 11.05/3.33 | (22) ! [v0] : ! [v1] : ( ~ (in(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v0, v1) = v2)) % 11.05/3.33 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) % 11.05/3.33 | (24) ? [v0] : empty(v0) = 0 % 11.05/3.33 | (25) ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(empty_set, v0) = v1)) % 11.05/3.33 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (set_difference(v1, v3) = v4) | ~ (singleton(v2) = v3) | ~ (subset(v0, v4) = v5) | ? [v6] : ? [v7] : (subset(v0, v1) = v6 & in(v2, v0) = v7 & ( ~ (v6 = 0) | v7 = 0))) % 11.05/3.33 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) % 11.05/3.33 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (singleton(v0) = v2) | ~ (subset(v2, v1) = v3) | ? [v4] : ( ~ (v4 = 0) & in(v0, v1) = v4)) % 11.05/3.33 | % 11.05/3.33 | Instantiating (8) with all_6_0_3, all_6_1_4, all_6_2_5, all_6_3_6 yields: % 11.05/3.33 | (29) singleton(all_6_2_5) = all_6_1_4 & subset(all_6_3_6, all_6_1_4) = all_6_0_3 & ((all_6_0_3 = 0 & ~ (all_6_1_4 = all_6_3_6) & ~ (all_6_3_6 = empty_set)) | ( ~ (all_6_0_3 = 0) & (all_6_1_4 = all_6_3_6 | all_6_3_6 = empty_set))) % 11.05/3.33 | % 11.05/3.33 | Applying alpha-rule on (29) yields: % 11.05/3.33 | (30) singleton(all_6_2_5) = all_6_1_4 % 11.05/3.33 | (31) subset(all_6_3_6, all_6_1_4) = all_6_0_3 % 11.05/3.33 | (32) (all_6_0_3 = 0 & ~ (all_6_1_4 = all_6_3_6) & ~ (all_6_3_6 = empty_set)) | ( ~ (all_6_0_3 = 0) & (all_6_1_4 = all_6_3_6 | all_6_3_6 = empty_set)) % 11.05/3.33 | % 11.05/3.34 | Instantiating formula (1) with all_6_0_3, all_6_3_6 yields: % 11.05/3.34 | (33) all_6_0_3 = 0 | ~ (subset(all_6_3_6, all_6_3_6) = all_6_0_3) % 11.05/3.34 | % 11.05/3.34 | Instantiating formula (25) with all_6_0_3, all_6_1_4 yields: % 11.05/3.34 | (34) all_6_0_3 = 0 | ~ (subset(empty_set, all_6_1_4) = all_6_0_3) % 11.05/3.34 | % 11.05/3.34 | Instantiating formula (19) with all_6_1_4, all_6_2_5, all_6_1_4, all_6_3_6 and discharging atoms singleton(all_6_2_5) = all_6_1_4, yields: % 11.05/3.34 | (35) ~ (subset(all_6_3_6, all_6_1_4) = 0) | ? [v0] : ? [v1] : ? [v2] : (set_difference(all_6_1_4, all_6_1_4) = v1 & subset(all_6_3_6, v1) = v2 & in(all_6_2_5, all_6_3_6) = v0 & (v2 = 0 | v0 = 0)) % 11.05/3.34 | % 11.05/3.34 | Instantiating formula (15) with all_6_3_6, all_6_1_4 yields: % 11.05/3.34 | (36) all_6_1_4 = all_6_3_6 | ~ (subset(all_6_3_6, all_6_1_4) = 0) | ? [v0] : ( ~ (v0 = 0) & subset(all_6_1_4, all_6_3_6) = v0) % 11.05/3.34 | % 11.05/3.34 | Instantiating formula (3) with all_6_1_4, all_6_3_6 yields: % 11.05/3.34 | (37) ~ (subset(all_6_3_6, all_6_1_4) = 0) | set_difference(all_6_3_6, all_6_1_4) = empty_set % 11.05/3.34 | % 11.05/3.34 | Instantiating formula (9) with all_6_0_3, all_6_1_4, all_6_3_6 and discharging atoms subset(all_6_3_6, all_6_1_4) = all_6_0_3, yields: % 11.05/3.34 | (38) all_6_0_3 = 0 | ? [v0] : ( ~ (v0 = empty_set) & set_difference(all_6_3_6, all_6_1_4) = v0) % 11.05/3.34 | % 11.05/3.34 +-Applying beta-rule and splitting (37), into two cases. % 11.05/3.34 |-Branch one: % 11.05/3.34 | (39) ~ (subset(all_6_3_6, all_6_1_4) = 0) % 11.05/3.34 | % 11.05/3.34 | Using (31) and (39) yields: % 11.05/3.34 | (40) ~ (all_6_0_3 = 0) % 11.05/3.34 | % 11.05/3.34 +-Applying beta-rule and splitting (33), into two cases. % 11.05/3.34 |-Branch one: % 11.05/3.34 | (41) ~ (subset(all_6_3_6, all_6_3_6) = all_6_0_3) % 11.05/3.34 | % 11.05/3.34 +-Applying beta-rule and splitting (34), into two cases. % 11.05/3.34 |-Branch one: % 11.05/3.34 | (42) ~ (subset(empty_set, all_6_1_4) = all_6_0_3) % 11.05/3.34 | % 11.05/3.34 +-Applying beta-rule and splitting (38), into two cases. % 11.05/3.34 |-Branch one: % 11.05/3.34 | (43) all_6_0_3 = 0 % 11.05/3.34 | % 11.05/3.34 | Equations (43) can reduce 40 to: % 11.05/3.34 | (44) $false % 11.05/3.34 | % 11.05/3.34 |-The branch is then unsatisfiable % 11.05/3.34 |-Branch two: % 11.05/3.34 | (40) ~ (all_6_0_3 = 0) % 11.05/3.34 | (46) ? [v0] : ( ~ (v0 = empty_set) & set_difference(all_6_3_6, all_6_1_4) = v0) % 11.05/3.34 | % 11.05/3.34 | Using (31) and (41) yields: % 11.05/3.34 | (47) ~ (all_6_1_4 = all_6_3_6) % 11.05/3.34 | % 11.05/3.34 | Using (31) and (42) yields: % 11.05/3.34 | (48) ~ (all_6_3_6 = empty_set) % 11.05/3.34 | % 11.05/3.34 +-Applying beta-rule and splitting (32), into two cases. % 11.05/3.34 |-Branch one: % 11.05/3.34 | (49) all_6_0_3 = 0 & ~ (all_6_1_4 = all_6_3_6) & ~ (all_6_3_6 = empty_set) % 11.05/3.34 | % 11.05/3.34 | Applying alpha-rule on (49) yields: % 11.05/3.34 | (43) all_6_0_3 = 0 % 11.05/3.34 | (47) ~ (all_6_1_4 = all_6_3_6) % 11.05/3.34 | (48) ~ (all_6_3_6 = empty_set) % 11.05/3.34 | % 11.05/3.34 | Equations (43) can reduce 40 to: % 11.05/3.34 | (44) $false % 11.05/3.34 | % 11.05/3.34 |-The branch is then unsatisfiable % 11.05/3.34 |-Branch two: % 11.05/3.34 | (54) ~ (all_6_0_3 = 0) & (all_6_1_4 = all_6_3_6 | all_6_3_6 = empty_set) % 11.05/3.34 | % 11.05/3.34 | Applying alpha-rule on (54) yields: % 11.05/3.34 | (40) ~ (all_6_0_3 = 0) % 11.05/3.34 | (56) all_6_1_4 = all_6_3_6 | all_6_3_6 = empty_set % 11.05/3.34 | % 11.05/3.34 +-Applying beta-rule and splitting (56), into two cases. % 11.05/3.34 |-Branch one: % 11.05/3.34 | (57) all_6_3_6 = empty_set % 11.05/3.34 | % 11.05/3.34 | Equations (57) can reduce 48 to: % 11.05/3.34 | (44) $false % 11.05/3.34 | % 11.05/3.34 |-The branch is then unsatisfiable % 11.05/3.34 |-Branch two: % 11.05/3.34 | (48) ~ (all_6_3_6 = empty_set) % 11.05/3.34 | (60) all_6_1_4 = all_6_3_6 % 11.05/3.34 | % 11.05/3.34 | Equations (60) can reduce 47 to: % 11.05/3.34 | (44) $false % 11.05/3.34 | % 11.05/3.34 |-The branch is then unsatisfiable % 11.05/3.34 |-Branch two: % 11.05/3.34 | (62) subset(empty_set, all_6_1_4) = all_6_0_3 % 11.05/3.34 | (43) all_6_0_3 = 0 % 11.05/3.34 | % 11.05/3.34 | Equations (43) can reduce 40 to: % 11.05/3.34 | (44) $false % 11.05/3.34 | % 11.05/3.34 |-The branch is then unsatisfiable % 11.05/3.34 |-Branch two: % 11.05/3.34 | (65) subset(all_6_3_6, all_6_3_6) = all_6_0_3 % 11.05/3.34 | (43) all_6_0_3 = 0 % 11.05/3.34 | % 11.05/3.34 | Equations (43) can reduce 40 to: % 11.05/3.34 | (44) $false % 11.05/3.34 | % 11.05/3.34 |-The branch is then unsatisfiable % 11.05/3.34 |-Branch two: % 11.05/3.34 | (68) subset(all_6_3_6, all_6_1_4) = 0 % 11.05/3.34 | (69) set_difference(all_6_3_6, all_6_1_4) = empty_set % 11.05/3.34 | % 11.05/3.34 +-Applying beta-rule and splitting (38), into two cases. % 11.05/3.34 |-Branch one: % 11.05/3.34 | (43) all_6_0_3 = 0 % 11.05/3.34 | % 11.05/3.34 | From (43) and (31) follows: % 11.05/3.34 | (68) subset(all_6_3_6, all_6_1_4) = 0 % 11.05/3.34 | % 11.05/3.34 +-Applying beta-rule and splitting (35), into two cases. % 11.05/3.34 |-Branch one: % 11.05/3.34 | (39) ~ (subset(all_6_3_6, all_6_1_4) = 0) % 11.05/3.34 | % 11.05/3.34 | Using (68) and (39) yields: % 11.05/3.34 | (73) $false % 11.05/3.34 | % 11.05/3.34 |-The branch is then unsatisfiable % 11.05/3.34 |-Branch two: % 11.05/3.34 | (68) subset(all_6_3_6, all_6_1_4) = 0 % 11.05/3.34 | (75) ? [v0] : ? [v1] : ? [v2] : (set_difference(all_6_1_4, all_6_1_4) = v1 & subset(all_6_3_6, v1) = v2 & in(all_6_2_5, all_6_3_6) = v0 & (v2 = 0 | v0 = 0)) % 11.05/3.34 | % 11.05/3.34 | Instantiating (75) with all_22_0_8, all_22_1_9, all_22_2_10 yields: % 11.05/3.34 | (76) set_difference(all_6_1_4, all_6_1_4) = all_22_1_9 & subset(all_6_3_6, all_22_1_9) = all_22_0_8 & in(all_6_2_5, all_6_3_6) = all_22_2_10 & (all_22_0_8 = 0 | all_22_2_10 = 0) % 11.05/3.35 | % 11.05/3.35 | Applying alpha-rule on (76) yields: % 11.05/3.35 | (77) set_difference(all_6_1_4, all_6_1_4) = all_22_1_9 % 11.05/3.35 | (78) subset(all_6_3_6, all_22_1_9) = all_22_0_8 % 11.05/3.35 | (79) in(all_6_2_5, all_6_3_6) = all_22_2_10 % 11.05/3.35 | (80) all_22_0_8 = 0 | all_22_2_10 = 0 % 11.05/3.35 | % 11.05/3.35 +-Applying beta-rule and splitting (32), into two cases. % 11.05/3.35 |-Branch one: % 11.05/3.35 | (49) all_6_0_3 = 0 & ~ (all_6_1_4 = all_6_3_6) & ~ (all_6_3_6 = empty_set) % 11.05/3.35 | % 11.05/3.35 | Applying alpha-rule on (49) yields: % 11.05/3.35 | (43) all_6_0_3 = 0 % 11.05/3.35 | (47) ~ (all_6_1_4 = all_6_3_6) % 11.05/3.35 | (48) ~ (all_6_3_6 = empty_set) % 11.05/3.35 | % 11.05/3.35 +-Applying beta-rule and splitting (36), into two cases. % 11.05/3.35 |-Branch one: % 11.05/3.35 | (39) ~ (subset(all_6_3_6, all_6_1_4) = 0) % 11.05/3.35 | % 11.05/3.35 | Using (68) and (39) yields: % 11.05/3.35 | (73) $false % 11.05/3.35 | % 11.05/3.35 |-The branch is then unsatisfiable % 11.05/3.35 |-Branch two: % 11.05/3.35 | (68) subset(all_6_3_6, all_6_1_4) = 0 % 11.05/3.35 | (88) all_6_1_4 = all_6_3_6 | ? [v0] : ( ~ (v0 = 0) & subset(all_6_1_4, all_6_3_6) = v0) % 11.05/3.35 | % 11.05/3.35 +-Applying beta-rule and splitting (88), into two cases. % 11.05/3.35 |-Branch one: % 11.05/3.35 | (60) all_6_1_4 = all_6_3_6 % 11.05/3.35 | % 11.05/3.35 | Equations (60) can reduce 47 to: % 11.05/3.35 | (44) $false % 11.05/3.35 | % 11.05/3.35 |-The branch is then unsatisfiable % 11.05/3.35 |-Branch two: % 11.05/3.35 | (47) ~ (all_6_1_4 = all_6_3_6) % 11.05/3.35 | (92) ? [v0] : ( ~ (v0 = 0) & subset(all_6_1_4, all_6_3_6) = v0) % 11.05/3.35 | % 11.05/3.35 | Instantiating (92) with all_36_0_11 yields: % 11.05/3.35 | (93) ~ (all_36_0_11 = 0) & subset(all_6_1_4, all_6_3_6) = all_36_0_11 % 11.05/3.35 | % 11.05/3.35 | Applying alpha-rule on (93) yields: % 11.05/3.35 | (94) ~ (all_36_0_11 = 0) % 11.05/3.35 | (95) subset(all_6_1_4, all_6_3_6) = all_36_0_11 % 11.05/3.35 | % 11.05/3.35 | Instantiating formula (17) with all_6_3_6 yields: % 11.05/3.35 | (96) all_6_3_6 = empty_set | ~ (subset(all_6_3_6, empty_set) = 0) % 11.05/3.35 | % 11.05/3.35 | Instantiating formula (10) with all_22_1_9, all_6_1_4, all_6_1_4 and discharging atoms set_difference(all_6_1_4, all_6_1_4) = all_22_1_9, yields: % 11.05/3.35 | (97) all_22_1_9 = empty_set | ? [v0] : ( ~ (v0 = 0) & subset(all_6_1_4, all_6_1_4) = v0) % 11.05/3.35 | % 11.05/3.35 | Instantiating formula (28) with all_36_0_11, all_6_1_4, all_6_3_6, all_6_2_5 and discharging atoms singleton(all_6_2_5) = all_6_1_4, subset(all_6_1_4, all_6_3_6) = all_36_0_11, yields: % 11.05/3.35 | (98) all_36_0_11 = 0 | ? [v0] : ( ~ (v0 = 0) & in(all_6_2_5, all_6_3_6) = v0) % 11.05/3.35 | % 11.05/3.35 | Instantiating formula (26) with all_22_0_8, all_22_1_9, all_6_1_4, all_6_2_5, all_6_1_4, all_6_3_6 and discharging atoms set_difference(all_6_1_4, all_6_1_4) = all_22_1_9, singleton(all_6_2_5) = all_6_1_4, subset(all_6_3_6, all_22_1_9) = all_22_0_8, yields: % 11.05/3.35 | (99) all_22_0_8 = 0 | ? [v0] : ? [v1] : (subset(all_6_3_6, all_6_1_4) = v0 & in(all_6_2_5, all_6_3_6) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 11.05/3.35 | % 11.05/3.35 | Instantiating formula (19) with all_6_1_4, all_6_2_5, all_22_1_9, all_6_3_6 and discharging atoms singleton(all_6_2_5) = all_6_1_4, yields: % 11.05/3.35 | (100) ~ (subset(all_6_3_6, all_22_1_9) = 0) | ? [v0] : ? [v1] : ? [v2] : (set_difference(all_22_1_9, all_6_1_4) = v1 & subset(all_6_3_6, v1) = v2 & in(all_6_2_5, all_6_3_6) = v0 & (v2 = 0 | v0 = 0)) % 11.05/3.35 | % 11.05/3.35 | Instantiating formula (3) with all_22_1_9, all_6_3_6 yields: % 11.05/3.35 | (101) ~ (subset(all_6_3_6, all_22_1_9) = 0) | set_difference(all_6_3_6, all_22_1_9) = empty_set % 11.05/3.35 | % 11.05/3.35 | Instantiating formula (22) with all_6_2_5, all_6_3_6 yields: % 11.05/3.35 | (102) ~ (in(all_6_2_5, all_6_3_6) = 0) | ? [v0] : ( ~ (v0 = 0) & in(all_6_3_6, all_6_2_5) = v0) % 11.05/3.35 | % 11.05/3.35 | Instantiating formula (12) with all_6_3_6, all_6_2_5 yields: % 11.05/3.35 | (103) ~ (in(all_6_2_5, all_6_3_6) = 0) | ? [v0] : (singleton(all_6_2_5) = v0 & subset(v0, all_6_3_6) = 0) % 11.05/3.35 | % 11.05/3.35 +-Applying beta-rule and splitting (96), into two cases. % 11.05/3.35 |-Branch one: % 11.05/3.35 | (104) ~ (subset(all_6_3_6, empty_set) = 0) % 11.05/3.35 | % 11.05/3.35 +-Applying beta-rule and splitting (98), into two cases. % 11.05/3.35 |-Branch one: % 11.05/3.35 | (105) all_36_0_11 = 0 % 11.05/3.35 | % 11.05/3.35 | Equations (105) can reduce 94 to: % 11.05/3.35 | (44) $false % 11.05/3.35 | % 11.05/3.35 |-The branch is then unsatisfiable % 11.05/3.35 |-Branch two: % 11.05/3.35 | (94) ~ (all_36_0_11 = 0) % 11.05/3.35 | (108) ? [v0] : ( ~ (v0 = 0) & in(all_6_2_5, all_6_3_6) = v0) % 11.05/3.35 | % 11.05/3.35 | Instantiating (108) with all_53_0_12 yields: % 11.05/3.35 | (109) ~ (all_53_0_12 = 0) & in(all_6_2_5, all_6_3_6) = all_53_0_12 % 11.05/3.35 | % 11.05/3.35 | Applying alpha-rule on (109) yields: % 11.05/3.35 | (110) ~ (all_53_0_12 = 0) % 11.05/3.35 | (111) in(all_6_2_5, all_6_3_6) = all_53_0_12 % 11.05/3.35 | % 11.05/3.35 +-Applying beta-rule and splitting (99), into two cases. % 11.05/3.35 |-Branch one: % 11.05/3.35 | (112) all_22_0_8 = 0 % 11.05/3.35 | % 11.05/3.35 | From (112) and (78) follows: % 11.05/3.35 | (113) subset(all_6_3_6, all_22_1_9) = 0 % 11.05/3.35 | % 11.05/3.35 +-Applying beta-rule and splitting (100), into two cases. % 11.05/3.35 |-Branch one: % 11.05/3.35 | (114) ~ (subset(all_6_3_6, all_22_1_9) = 0) % 11.05/3.35 | % 11.05/3.35 | Using (113) and (114) yields: % 11.05/3.35 | (73) $false % 11.05/3.35 | % 11.05/3.35 |-The branch is then unsatisfiable % 11.05/3.35 |-Branch two: % 11.05/3.35 | (113) subset(all_6_3_6, all_22_1_9) = 0 % 11.05/3.36 | (117) ? [v0] : ? [v1] : ? [v2] : (set_difference(all_22_1_9, all_6_1_4) = v1 & subset(all_6_3_6, v1) = v2 & in(all_6_2_5, all_6_3_6) = v0 & (v2 = 0 | v0 = 0)) % 11.05/3.36 | % 11.05/3.36 +-Applying beta-rule and splitting (101), into two cases. % 11.05/3.36 |-Branch one: % 11.05/3.36 | (114) ~ (subset(all_6_3_6, all_22_1_9) = 0) % 11.05/3.36 | % 11.05/3.36 | Using (113) and (114) yields: % 11.05/3.36 | (73) $false % 11.05/3.36 | % 11.05/3.36 |-The branch is then unsatisfiable % 11.05/3.36 |-Branch two: % 11.05/3.36 | (113) subset(all_6_3_6, all_22_1_9) = 0 % 11.05/3.36 | (121) set_difference(all_6_3_6, all_22_1_9) = empty_set % 11.05/3.36 | % 11.05/3.36 | Using (113) and (104) yields: % 11.05/3.36 | (122) ~ (all_22_1_9 = empty_set) % 11.05/3.36 | % 11.05/3.36 +-Applying beta-rule and splitting (97), into two cases. % 11.05/3.36 |-Branch one: % 11.05/3.36 | (123) all_22_1_9 = empty_set % 11.05/3.36 | % 11.05/3.36 | Equations (123) can reduce 122 to: % 11.05/3.36 | (44) $false % 11.05/3.36 | % 11.05/3.36 |-The branch is then unsatisfiable % 11.05/3.36 |-Branch two: % 11.05/3.36 | (122) ~ (all_22_1_9 = empty_set) % 11.05/3.36 | (126) ? [v0] : ( ~ (v0 = 0) & subset(all_6_1_4, all_6_1_4) = v0) % 11.05/3.36 | % 11.05/3.36 | Instantiating (126) with all_93_0_17 yields: % 11.05/3.36 | (127) ~ (all_93_0_17 = 0) & subset(all_6_1_4, all_6_1_4) = all_93_0_17 % 11.05/3.36 | % 11.05/3.36 | Applying alpha-rule on (127) yields: % 11.05/3.36 | (128) ~ (all_93_0_17 = 0) % 11.05/3.36 | (129) subset(all_6_1_4, all_6_1_4) = all_93_0_17 % 11.05/3.36 | % 11.05/3.36 | Instantiating formula (1) with all_93_0_17, all_6_1_4 and discharging atoms subset(all_6_1_4, all_6_1_4) = all_93_0_17, yields: % 11.05/3.36 | (130) all_93_0_17 = 0 % 11.05/3.36 | % 11.05/3.36 | Equations (130) can reduce 128 to: % 11.05/3.36 | (44) $false % 11.05/3.36 | % 11.05/3.36 |-The branch is then unsatisfiable % 11.05/3.36 |-Branch two: % 11.05/3.36 | (132) ~ (all_22_0_8 = 0) % 11.05/3.36 | (133) ? [v0] : ? [v1] : (subset(all_6_3_6, all_6_1_4) = v0 & in(all_6_2_5, all_6_3_6) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 11.05/3.36 | % 11.05/3.36 | Instantiating (133) with all_64_0_21, all_64_1_22 yields: % 11.05/3.36 | (134) subset(all_6_3_6, all_6_1_4) = all_64_1_22 & in(all_6_2_5, all_6_3_6) = all_64_0_21 & ( ~ (all_64_1_22 = 0) | all_64_0_21 = 0) % 11.05/3.36 | % 11.05/3.36 | Applying alpha-rule on (134) yields: % 11.05/3.36 | (135) subset(all_6_3_6, all_6_1_4) = all_64_1_22 % 11.05/3.36 | (136) in(all_6_2_5, all_6_3_6) = all_64_0_21 % 11.05/3.36 | (137) ~ (all_64_1_22 = 0) | all_64_0_21 = 0 % 11.05/3.36 | % 11.05/3.36 +-Applying beta-rule and splitting (80), into two cases. % 11.05/3.36 |-Branch one: % 11.05/3.36 | (112) all_22_0_8 = 0 % 11.05/3.36 | % 11.05/3.36 | Equations (112) can reduce 132 to: % 11.05/3.36 | (44) $false % 11.05/3.36 | % 11.05/3.36 |-The branch is then unsatisfiable % 11.05/3.36 |-Branch two: % 11.05/3.36 | (132) ~ (all_22_0_8 = 0) % 11.05/3.36 | (141) all_22_2_10 = 0 % 11.05/3.36 | % 11.05/3.36 | From (141) and (79) follows: % 11.05/3.36 | (142) in(all_6_2_5, all_6_3_6) = 0 % 11.05/3.36 | % 11.05/3.36 +-Applying beta-rule and splitting (102), into two cases. % 11.05/3.36 |-Branch one: % 11.05/3.36 | (143) ~ (in(all_6_2_5, all_6_3_6) = 0) % 11.05/3.36 | % 11.05/3.36 | Using (142) and (143) yields: % 11.05/3.36 | (73) $false % 11.05/3.36 | % 11.05/3.36 |-The branch is then unsatisfiable % 11.05/3.36 |-Branch two: % 11.05/3.36 | (142) in(all_6_2_5, all_6_3_6) = 0 % 11.05/3.36 | (146) ? [v0] : ( ~ (v0 = 0) & in(all_6_3_6, all_6_2_5) = v0) % 11.05/3.36 | % 11.05/3.36 +-Applying beta-rule and splitting (103), into two cases. % 11.05/3.36 |-Branch one: % 11.05/3.36 | (143) ~ (in(all_6_2_5, all_6_3_6) = 0) % 11.05/3.36 | % 11.05/3.36 | Using (142) and (143) yields: % 11.05/3.36 | (73) $false % 11.05/3.36 | % 11.05/3.36 |-The branch is then unsatisfiable % 11.05/3.36 |-Branch two: % 11.05/3.36 | (142) in(all_6_2_5, all_6_3_6) = 0 % 11.05/3.36 | (150) ? [v0] : (singleton(all_6_2_5) = v0 & subset(v0, all_6_3_6) = 0) % 11.05/3.36 | % 11.05/3.36 | Instantiating formula (6) with all_6_2_5, all_6_3_6, all_53_0_12, all_64_0_21 and discharging atoms in(all_6_2_5, all_6_3_6) = all_64_0_21, in(all_6_2_5, all_6_3_6) = all_53_0_12, yields: % 11.05/3.36 | (151) all_64_0_21 = all_53_0_12 % 11.05/3.36 | % 11.05/3.36 | Instantiating formula (6) with all_6_2_5, all_6_3_6, 0, all_64_0_21 and discharging atoms in(all_6_2_5, all_6_3_6) = all_64_0_21, in(all_6_2_5, all_6_3_6) = 0, yields: % 11.05/3.36 | (152) all_64_0_21 = 0 % 11.05/3.36 | % 11.05/3.36 | Combining equations (151,152) yields a new equation: % 11.05/3.36 | (153) all_53_0_12 = 0 % 11.05/3.36 | % 11.05/3.36 | Simplifying 153 yields: % 11.05/3.36 | (154) all_53_0_12 = 0 % 11.05/3.37 | % 11.05/3.37 | Equations (154) can reduce 110 to: % 11.05/3.37 | (44) $false % 11.05/3.37 | % 11.05/3.37 |-The branch is then unsatisfiable % 11.05/3.37 |-Branch two: % 11.05/3.37 | (156) subset(all_6_3_6, empty_set) = 0 % 11.05/3.37 | (57) all_6_3_6 = empty_set % 11.05/3.37 | % 11.05/3.37 | Equations (57) can reduce 48 to: % 11.05/3.37 | (44) $false % 11.05/3.37 | % 11.05/3.37 |-The branch is then unsatisfiable % 11.05/3.37 |-Branch two: % 11.05/3.37 | (54) ~ (all_6_0_3 = 0) & (all_6_1_4 = all_6_3_6 | all_6_3_6 = empty_set) % 11.05/3.37 | % 11.05/3.37 | Applying alpha-rule on (54) yields: % 11.05/3.37 | (40) ~ (all_6_0_3 = 0) % 11.05/3.37 | (56) all_6_1_4 = all_6_3_6 | all_6_3_6 = empty_set % 11.05/3.37 | % 11.05/3.37 | Equations (43) can reduce 40 to: % 11.05/3.37 | (44) $false % 11.05/3.37 | % 11.05/3.37 |-The branch is then unsatisfiable % 11.05/3.37 |-Branch two: % 11.05/3.37 | (40) ~ (all_6_0_3 = 0) % 11.05/3.37 | (46) ? [v0] : ( ~ (v0 = empty_set) & set_difference(all_6_3_6, all_6_1_4) = v0) % 11.05/3.37 | % 11.05/3.37 +-Applying beta-rule and splitting (35), into two cases. % 11.05/3.37 |-Branch one: % 11.05/3.37 | (39) ~ (subset(all_6_3_6, all_6_1_4) = 0) % 11.05/3.37 | % 11.05/3.37 | Using (68) and (39) yields: % 11.05/3.37 | (73) $false % 11.05/3.37 | % 11.05/3.37 |-The branch is then unsatisfiable % 11.05/3.37 |-Branch two: % 11.05/3.37 | (68) subset(all_6_3_6, all_6_1_4) = 0 % 11.05/3.37 | (75) ? [v0] : ? [v1] : ? [v2] : (set_difference(all_6_1_4, all_6_1_4) = v1 & subset(all_6_3_6, v1) = v2 & in(all_6_2_5, all_6_3_6) = v0 & (v2 = 0 | v0 = 0)) % 11.05/3.37 | % 11.05/3.37 | Instantiating formula (27) with all_6_3_6, all_6_1_4, 0, all_6_0_3 and discharging atoms subset(all_6_3_6, all_6_1_4) = all_6_0_3, subset(all_6_3_6, all_6_1_4) = 0, yields: % 11.05/3.37 | (43) all_6_0_3 = 0 % 11.05/3.37 | % 11.05/3.37 | Equations (43) can reduce 40 to: % 11.05/3.37 | (44) $false % 11.05/3.37 | % 11.05/3.37 |-The branch is then unsatisfiable % 11.05/3.37 % SZS output end Proof for theBenchmark % 11.05/3.37 % 11.05/3.37 2767ms %------------------------------------------------------------------------------