%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEU269+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n012.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:48:20 EDT 2022 % Result : Theorem 7.52s 2.31s % Output : Proof 22.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU269+1 : TPTP v8.1.0. Released v3.3.0. % 0.11/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.33 % Computer : n012.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sun Jun 19 11:36:38 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.58 ____ _ % 0.19/0.58 ___ / __ \_____(_)___ ________ __________ % 0.19/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.19/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.19/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.19/0.58 % 0.19/0.58 A Theorem Prover for First-Order Logic % 0.19/0.58 (ePrincess v.1.0) % 0.19/0.58 % 0.19/0.58 (c) Philipp Rümmer, 2009-2015 % 0.19/0.58 (c) Peter Backeman, 2014-2015 % 0.19/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.19/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.19/0.58 Bug reports to peter@backeman.se % 0.19/0.58 % 0.19/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.19/0.58 % 0.19/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.66/0.93 Prover 0: Preprocessing ... % 2.56/1.20 Prover 0: Warning: ignoring some quantifiers % 2.56/1.22 Prover 0: Constructing countermodel ... % 3.65/1.47 Prover 0: gave up % 3.65/1.47 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 3.91/1.51 Prover 1: Preprocessing ... % 4.71/1.66 Prover 1: Warning: ignoring some quantifiers % 4.71/1.67 Prover 1: Constructing countermodel ... % 5.01/1.83 Prover 1: gave up % 5.01/1.83 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 5.45/1.86 Prover 2: Preprocessing ... % 6.07/2.00 Prover 2: Warning: ignoring some quantifiers % 6.07/2.01 Prover 2: Constructing countermodel ... % 7.52/2.30 Prover 2: proved (475ms) % 7.52/2.31 % 7.52/2.31 No countermodel exists, formula is valid % 7.52/2.31 % SZS status Theorem for theBenchmark % 7.52/2.31 % 7.52/2.31 Generating proof ... Warning: ignoring some quantifiers % 21.13/5.69 found it (size 275) % 21.13/5.69 % 21.13/5.69 % SZS output start Proof for theBenchmark % 21.13/5.69 Assumed formulas after preprocessing and simplification: % 21.13/5.69 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v8 = 0) & ~ (v5 = 0) & ~ (v2 = 0) & relation_empty_yielding(v3) = 0 & relation_empty_yielding(empty_set) = 0 & inclusion_relation(v0) = v1 & transitive(v1) = v2 & one_to_one(v9) = 0 & one_to_one(v6) = 0 & one_to_one(empty_set) = 0 & relation(v13) = 0 & relation(v10) = 0 & relation(v9) = 0 & relation(v6) = 0 & relation(v3) = 0 & relation(empty_set) = 0 & epsilon_transitive(v12) = 0 & epsilon_transitive(v9) = 0 & epsilon_transitive(v4) = 0 & epsilon_transitive(empty_set) = 0 & ordinal(v12) = 0 & ordinal(v9) = 0 & ordinal(v4) = 0 & ordinal(empty_set) = 0 & epsilon_connected(v12) = 0 & epsilon_connected(v9) = 0 & epsilon_connected(v4) = 0 & epsilon_connected(empty_set) = 0 & function(v13) = 0 & function(v10) = 0 & function(v9) = 0 & function(v6) = 0 & function(v3) = 0 & function(empty_set) = 0 & empty(v11) = 0 & empty(v10) = 0 & empty(v9) = 0 & empty(v7) = v8 & empty(v4) = v5 & empty(empty_set) = 0 & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : (v21 = 0 | ~ (ordered_pair(v17, v18) = v19) | ~ (ordered_pair(v16, v18) = v20) | ~ (is_transitive_in(v14, v15) = 0) | ~ (relation(v14) = 0) | ~ (in(v20, v14) = v21) | ~ (in(v19, v14) = 0) | ? [v22] : ? [v23] : (( ~ (v23 = 0) & ordered_pair(v16, v17) = v22 & in(v22, v14) = v23) | ( ~ (v22 = 0) & in(v18, v15) = v22) | ( ~ (v22 = 0) & in(v17, v15) = v22) | ( ~ (v22 = 0) & in(v16, v15) = v22))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : (v21 = 0 | ~ (ordered_pair(v16, v18) = v20) | ~ (ordered_pair(v16, v17) = v19) | ~ (is_transitive_in(v14, v15) = 0) | ~ (relation(v14) = 0) | ~ (in(v20, v14) = v21) | ~ (in(v19, v14) = 0) | ? [v22] : ? [v23] : (( ~ (v23 = 0) & ordered_pair(v17, v18) = v22 & in(v22, v14) = v23) | ( ~ (v22 = 0) & in(v18, v15) = v22) | ( ~ (v22 = 0) & in(v17, v15) = v22) | ( ~ (v22 = 0) & in(v16, v15) = v22))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v20 = 0 | ~ (ordered_pair(v16, v18) = v19) | ~ (is_transitive_in(v14, v15) = 0) | ~ (relation(v14) = 0) | ~ (in(v19, v14) = v20) | ~ (in(v17, v15) = 0) | ? [v21] : ? [v22] : (( ~ (v22 = 0) & ordered_pair(v17, v18) = v21 & in(v21, v14) = v22) | ( ~ (v22 = 0) & ordered_pair(v16, v17) = v21 & in(v21, v14) = v22) | ( ~ (v21 = 0) & in(v18, v15) = v21) | ( ~ (v21 = 0) & in(v16, v15) = v21))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (ordered_pair(v17, v18) = v20) | ~ (ordered_pair(v16, v17) = v19) | ~ (is_transitive_in(v14, v15) = 0) | ~ (relation(v14) = 0) | ~ (in(v20, v14) = 0) | ~ (in(v19, v14) = 0) | ? [v21] : ? [v22] : ((v22 = 0 & ordered_pair(v16, v18) = v21 & in(v21, v14) = 0) | ( ~ (v21 = 0) & in(v18, v15) = v21) | ( ~ (v21 = 0) & in(v17, v15) = v21) | ( ~ (v21 = 0) & in(v16, v15) = v21))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (inclusion_relation(v14) = v15) | ~ (subset(v17, v18) = v19) | ~ (relation_field(v15) = v16) | ? [v20] : ? [v21] : (( ~ (v20 = 0) & relation(v15) = v20) | ( ~ (v20 = 0) & in(v18, v14) = v20) | ( ~ (v20 = 0) & in(v17, v14) = v20) | (( ~ (v19 = 0) | (v21 = 0 & ordered_pair(v17, v18) = v20 & in(v20, v15) = 0)) & (v19 = 0 | ( ~ (v21 = 0) & ordered_pair(v17, v18) = v20 & in(v20, v15) = v21))))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (inclusion_relation(v14) = v15) | ~ (ordered_pair(v17, v18) = v19) | ~ (relation_field(v15) = v16) | ? [v20] : ? [v21] : (( ~ (v20 = 0) & relation(v15) = v20) | ( ~ (v20 = 0) & in(v18, v14) = v20) | ( ~ (v20 = 0) & in(v17, v14) = v20) | (((v21 = 0 & subset(v17, v18) = 0) | ( ~ (v20 = 0) & in(v19, v15) = v20)) & ((v20 = 0 & in(v19, v15) = 0) | ( ~ (v21 = 0) & subset(v17, v18) = v21))))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (ordered_pair(v17, v18) = v19) | ~ (is_transitive_in(v14, v15) = 0) | ~ (relation(v14) = 0) | ~ (in(v19, v14) = 0) | ~ (in(v16, v15) = 0) | ? [v20] : ? [v21] : ((v21 = 0 & ordered_pair(v16, v18) = v20 & in(v20, v14) = 0) | ( ~ (v21 = 0) & ordered_pair(v16, v17) = v20 & in(v20, v14) = v21) | ( ~ (v20 = 0) & in(v18, v15) = v20) | ( ~ (v20 = 0) & in(v17, v15) = v20))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (ordered_pair(v16, v17) = v19) | ~ (is_transitive_in(v14, v15) = 0) | ~ (relation(v14) = 0) | ~ (in(v19, v14) = 0) | ~ (in(v18, v15) = 0) | ? [v20] : ? [v21] : ((v21 = 0 & ordered_pair(v16, v18) = v20 & in(v20, v14) = 0) | ( ~ (v21 = 0) & ordered_pair(v17, v18) = v20 & in(v20, v14) = v21) | ( ~ (v20 = 0) & in(v17, v15) = v20) | ( ~ (v20 = 0) & in(v16, v15) = v20))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = 0 | ~ (powerset(v16) = v17) | ~ (element(v15, v17) = 0) | ~ (element(v14, v16) = v18) | ? [v19] : ( ~ (v19 = 0) & in(v14, v15) = v19)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (is_transitive_in(v14, v15) = 0) | ~ (relation(v14) = 0) | ~ (in(v18, v15) = 0) | ~ (in(v17, v15) = 0) | ~ (in(v16, v15) = 0) | ? [v19] : ? [v20] : ((v20 = 0 & ordered_pair(v16, v18) = v19 & in(v19, v14) = 0) | ( ~ (v20 = 0) & ordered_pair(v17, v18) = v19 & in(v19, v14) = v20) | ( ~ (v20 = 0) & ordered_pair(v16, v17) = v19 & in(v19, v14) = v20))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (powerset(v15) = v16) | ~ (element(v14, v16) = v17) | ? [v18] : ( ~ (v18 = 0) & subset(v14, v15) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (element(v14, v16) = v17) | ~ (in(v14, v15) = 0) | ? [v18] : ? [v19] : ( ~ (v19 = 0) & powerset(v16) = v18 & element(v15, v18) = v19)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (subset(v15, v16) = 0) | ~ (subset(v14, v16) = v17) | ? [v18] : ( ~ (v18 = 0) & subset(v14, v15) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (subset(v14, v16) = v17) | ~ (subset(v14, v15) = 0) | ? [v18] : ( ~ (v18 = 0) & subset(v15, v16) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (element(v17, v16) = v15) | ~ (element(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (subset(v17, v16) = v15) | ~ (subset(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (ordered_pair(v17, v16) = v15) | ~ (ordered_pair(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (is_transitive_in(v17, v16) = v15) | ~ (is_transitive_in(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (set_union2(v17, v16) = v15) | ~ (set_union2(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (unordered_pair(v17, v16) = v15) | ~ (unordered_pair(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (in(v17, v16) = v15) | ~ (in(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (powerset(v16) = v17) | ~ (element(v15, v17) = 0) | ~ (in(v14, v15) = 0) | element(v14, v16) = 0) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (powerset(v16) = v17) | ~ (element(v15, v17) = 0) | ~ (in(v14, v15) = 0) | ? [v18] : ( ~ (v18 = 0) & empty(v16) = v18)) & ! [v14] : ! [v15] : ! [v16] : (v16 = v15 | ~ (inclusion_relation(v14) = v16) | ~ (relation_field(v15) = v14) | ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : ((v20 = 0 & v19 = 0 & in(v18, v14) = 0 & in(v17, v14) = 0 & ((v23 = 0 & subset(v17, v18) = 0) | (v22 = 0 & ordered_pair(v17, v18) = v21 & in(v21, v15) = 0)) & (( ~ (v23 = 0) & subset(v17, v18) = v23) | ( ~ (v22 = 0) & ordered_pair(v17, v18) = v21 & in(v21, v15) = v22))) | ( ~ (v17 = 0) & relation(v15) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v16 = v14 | ~ (inclusion_relation(v14) = v15) | ~ (relation_field(v15) = v16) | ? [v17] : ( ~ (v17 = 0) & relation(v15) = v17)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (element(v14, v15) = v16) | ? [v17] : ( ~ (v17 = 0) & in(v14, v15) = v17)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (subset(v14, v15) = v16) | ? [v17] : ? [v18] : ( ~ (v18 = 0) & powerset(v15) = v17 & element(v14, v17) = v18)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (is_transitive_in(v14, v15) = v16) | ~ (relation(v14) = 0) | ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : ( ~ (v23 = 0) & ordered_pair(v18, v19) = v21 & ordered_pair(v17, v19) = v22 & ordered_pair(v17, v18) = v20 & in(v22, v14) = v23 & in(v21, v14) = 0 & in(v20, v14) = 0 & in(v19, v15) = 0 & in(v18, v15) = 0 & in(v17, v15) = 0)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (in(v14, v15) = v16) | ? [v17] : ((v17 = 0 & empty(v15) = 0) | ( ~ (v17 = 0) & element(v14, v15) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (powerset(v16) = v15) | ~ (powerset(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (relation_empty_yielding(v16) = v15) | ~ (relation_empty_yielding(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (relation_dom(v16) = v15) | ~ (relation_dom(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (relation_rng(v16) = v15) | ~ (relation_rng(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (singleton(v16) = v15) | ~ (singleton(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (inclusion_relation(v16) = v15) | ~ (inclusion_relation(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (relation_field(v16) = v15) | ~ (relation_field(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (transitive(v16) = v15) | ~ (transitive(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (one_to_one(v16) = v15) | ~ (one_to_one(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (relation(v16) = v15) | ~ (relation(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (epsilon_transitive(v16) = v15) | ~ (epsilon_transitive(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (ordinal(v16) = v15) | ~ (ordinal(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (epsilon_connected(v16) = v15) | ~ (epsilon_connected(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (function(v16) = v15) | ~ (function(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (empty(v16) = v15) | ~ (empty(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (powerset(v15) = v16) | ~ (element(v14, v16) = 0) | subset(v14, v15) = 0) & ! [v14] : ! [v15] : ! [v16] : ( ~ (inclusion_relation(v14) = v16) | ~ (relation(v15) = 0) | ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : ? [v24] : (( ~ (v16 = v15) | (v17 = v14 & relation_field(v15) = v14 & ! [v25] : ! [v26] : ! [v27] : ( ~ (subset(v25, v26) = v27) | ? [v28] : ? [v29] : (( ~ (v28 = 0) & in(v26, v14) = v28) | ( ~ (v28 = 0) & in(v25, v14) = v28) | (( ~ (v27 = 0) | (v29 = 0 & ordered_pair(v25, v26) = v28 & in(v28, v15) = 0)) & (v27 = 0 | ( ~ (v29 = 0) & ordered_pair(v25, v26) = v28 & in(v28, v15) = v29))))) & ! [v25] : ! [v26] : ! [v27] : ( ~ (ordered_pair(v25, v26) = v27) | ? [v28] : ? [v29] : (( ~ (v28 = 0) & in(v26, v14) = v28) | ( ~ (v28 = 0) & in(v25, v14) = v28) | (((v29 = 0 & subset(v25, v26) = 0) | ( ~ (v28 = 0) & in(v27, v15) = v28)) & ((v28 = 0 & in(v27, v15) = 0) | ( ~ (v29 = 0) & subset(v25, v26) = v29))))))) & (v16 = v15 | (v21 = 0 & v20 = 0 & in(v19, v14) = 0 & in(v18, v14) = 0 & ((v24 = 0 & subset(v18, v19) = 0) | (v23 = 0 & ordered_pair(v18, v19) = v22 & in(v22, v15) = 0)) & (( ~ (v24 = 0) & subset(v18, v19) = v24) | ( ~ (v23 = 0) & ordered_pair(v18, v19) = v22 & in(v22, v15) = v23))) | ( ~ (v17 = v14) & relation_field(v15) = v17)))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (subset(v15, v16) = 0) | ~ (subset(v14, v15) = 0) | subset(v14, v16) = 0) & ! [v14] : ! [v15] : ! [v16] : ( ~ (ordered_pair(v14, v15) = v16) | ? [v17] : ? [v18] : (singleton(v14) = v18 & unordered_pair(v17, v18) = v16 & unordered_pair(v14, v15) = v17)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (ordered_pair(v14, v15) = v16) | ? [v17] : ( ~ (v17 = 0) & empty(v16) = v17)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_union2(v15, v14) = v16) | set_union2(v14, v15) = v16) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_union2(v15, v14) = v16) | ? [v17] : ((v17 = 0 & empty(v14) = 0) | ( ~ (v17 = 0) & empty(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_union2(v14, v15) = v16) | set_union2(v15, v14) = v16) & ! [v14] : ! [v15] : ! [v16] : ( ~ (set_union2(v14, v15) = v16) | ? [v17] : ((v17 = 0 & empty(v14) = 0) | ( ~ (v17 = 0) & empty(v16) = v17))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (unordered_pair(v15, v14) = v16) | unordered_pair(v14, v15) = v16) & ! [v14] : ! [v15] : ! [v16] : ( ~ (unordered_pair(v14, v15) = v16) | unordered_pair(v15, v14) = v16) & ! [v14] : ! [v15] : ! [v16] : ( ~ (unordered_pair(v14, v15) = v16) | ? [v17] : ? [v18] : (singleton(v14) = v18 & ordered_pair(v14, v15) = v17 & unordered_pair(v16, v18) = v17)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (empty(v16) = 0) | ~ (in(v14, v15) = 0) | ? [v17] : ? [v18] : ( ~ (v18 = 0) & powerset(v16) = v17 & element(v15, v17) = v18)) & ! [v14] : ! [v15] : (v15 = v14 | ~ (set_union2(v14, v14) = v15)) & ! [v14] : ! [v15] : (v15 = v14 | ~ (set_union2(v14, empty_set) = v15)) & ! [v14] : ! [v15] : (v15 = v14 | ~ (empty(v15) = 0) | ~ (empty(v14) = 0)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (subset(v14, v14) = v15)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (ordinal(v14) = v15) | ? [v16] : (( ~ (v16 = 0) & epsilon_transitive(v14) = v16) | ( ~ (v16 = 0) & epsilon_connected(v14) = v16))) & ! [v14] : ! [v15] : (v15 = 0 | ~ (function(v14) = v15) | ? [v16] : ( ~ (v16 = 0) & empty(v14) = v16)) & ! [v14] : ! [v15] : ( ~ (element(v14, v15) = 0) | ? [v16] : ((v16 = 0 & empty(v15) = 0) | (v16 = 0 & in(v14, v15) = 0))) & ! [v14] : ! [v15] : ( ~ (relation_dom(v14) = v15) | ? [v16] : ? [v17] : ? [v18] : ((v18 = v16 & relation_rng(v14) = v17 & relation_field(v14) = v16 & set_union2(v15, v17) = v16) | ( ~ (v16 = 0) & relation(v14) = v16))) & ! [v14] : ! [v15] : ( ~ (relation_rng(v14) = v15) | ? [v16] : ? [v17] : ? [v18] : ((v18 = v16 & relation_dom(v14) = v17 & relation_field(v14) = v16 & set_union2(v17, v15) = v16) | ( ~ (v16 = 0) & relation(v14) = v16))) & ! [v14] : ! [v15] : ( ~ (inclusion_relation(v14) = v15) | relation(v15) = 0) & ! [v14] : ! [v15] : ( ~ (subset(v14, v15) = 0) | ? [v16] : (powerset(v15) = v16 & element(v14, v16) = 0)) & ! [v14] : ! [v15] : ( ~ (relation_field(v14) = v15) | ? [v16] : ? [v17] : ? [v18] : ((v18 = v15 & relation_dom(v14) = v16 & relation_rng(v14) = v17 & set_union2(v16, v17) = v15) | ( ~ (v16 = 0) & relation(v14) = v16))) & ! [v14] : ! [v15] : ( ~ (relation_field(v14) = v15) | ? [v16] : ? [v17] : (( ~ (v16 = 0) & relation(v14) = v16) | (((v17 = 0 & is_transitive_in(v14, v15) = 0) | ( ~ (v16 = 0) & transitive(v14) = v16)) & ((v16 = 0 & transitive(v14) = 0) | ( ~ (v17 = 0) & is_transitive_in(v14, v15) = v17))))) & ! [v14] : ! [v15] : ( ~ (transitive(v14) = v15) | ? [v16] : ? [v17] : (( ~ (v16 = 0) & relation(v14) = v16) | (( ~ (v15 = 0) | (v17 = 0 & relation_field(v14) = v16 & is_transitive_in(v14, v16) = 0)) & (v15 = 0 | ( ~ (v17 = 0) & relation_field(v14) = v16 & is_transitive_in(v14, v16) = v17))))) & ! [v14] : ! [v15] : ( ~ (one_to_one(v14) = v15) | ? [v16] : ? [v17] : ((v17 = 0 & v16 = 0 & v15 = 0 & relation(v14) = 0 & function(v14) = 0) | ( ~ (v16 = 0) & relation(v14) = v16) | ( ~ (v16 = 0) & function(v14) = v16) | ( ~ (v16 = 0) & empty(v14) = v16))) & ! [v14] : ! [v15] : ( ~ (epsilon_transitive(v14) = v15) | ? [v16] : ? [v17] : ((v17 = 0 & v16 = 0 & v15 = 0 & ordinal(v14) = 0 & epsilon_connected(v14) = 0) | ( ~ (v16 = 0) & empty(v14) = v16))) & ! [v14] : ! [v15] : ( ~ (epsilon_transitive(v14) = v15) | ? [v16] : ((v16 = 0 & v15 = 0 & epsilon_connected(v14) = 0) | ( ~ (v16 = 0) & ordinal(v14) = v16))) & ! [v14] : ! [v15] : ( ~ (ordinal(v14) = v15) | ? [v16] : ? [v17] : ((v17 = 0 & v16 = 0 & v15 = 0 & epsilon_transitive(v14) = 0 & epsilon_connected(v14) = 0) | ( ~ (v16 = 0) & empty(v14) = v16))) & ! [v14] : ! [v15] : ( ~ (epsilon_connected(v14) = v15) | ? [v16] : ? [v17] : ((v17 = 0 & v16 = 0 & v15 = 0 & epsilon_transitive(v14) = 0 & ordinal(v14) = 0) | ( ~ (v16 = 0) & empty(v14) = v16))) & ! [v14] : ! [v15] : ( ~ (epsilon_connected(v14) = v15) | ? [v16] : ((v16 = 0 & v15 = 0 & epsilon_transitive(v14) = 0) | ( ~ (v16 = 0) & ordinal(v14) = v16))) & ! [v14] : ! [v15] : ( ~ (in(v15, v14) = 0) | ? [v16] : ( ~ (v16 = 0) & in(v14, v15) = v16)) & ! [v14] : ! [v15] : ( ~ (in(v14, v15) = 0) | element(v14, v15) = 0) & ! [v14] : ! [v15] : ( ~ (in(v14, v15) = 0) | ? [v16] : ( ~ (v16 = 0) & empty(v15) = v16)) & ! [v14] : ! [v15] : ( ~ (in(v14, v15) = 0) | ? [v16] : ( ~ (v16 = 0) & in(v15, v14) = v16)) & ! [v14] : (v14 = empty_set | ~ (empty(v14) = 0)) & ! [v14] : ( ~ (relation(v14) = 0) | ? [v15] : ? [v16] : ? [v17] : (relation_dom(v14) = v16 & relation_rng(v14) = v17 & relation_field(v14) = v15 & set_union2(v16, v17) = v15)) & ! [v14] : ( ~ (relation(v14) = 0) | ? [v15] : ? [v16] : ? [v17] : (((v17 = 0 & relation_field(v14) = v16 & is_transitive_in(v14, v16) = 0) | ( ~ (v15 = 0) & transitive(v14) = v15)) & ((v15 = 0 & transitive(v14) = 0) | ( ~ (v17 = 0) & relation_field(v14) = v16 & is_transitive_in(v14, v16) = v17)))) & ! [v14] : ( ~ (relation(v14) = 0) | ? [v15] : ? [v16] : ((v16 = 0 & v15 = 0 & one_to_one(v14) = 0 & function(v14) = 0) | ( ~ (v15 = 0) & function(v14) = v15) | ( ~ (v15 = 0) & empty(v14) = v15))) & ! [v14] : ( ~ (epsilon_transitive(v14) = 0) | ? [v15] : ((v15 = 0 & ordinal(v14) = 0) | ( ~ (v15 = 0) & epsilon_connected(v14) = v15))) & ! [v14] : ( ~ (ordinal(v14) = 0) | (epsilon_transitive(v14) = 0 & epsilon_connected(v14) = 0)) & ! [v14] : ( ~ (epsilon_connected(v14) = 0) | ? [v15] : ((v15 = 0 & ordinal(v14) = 0) | ( ~ (v15 = 0) & epsilon_transitive(v14) = v15))) & ! [v14] : ( ~ (function(v14) = 0) | ? [v15] : ? [v16] : ((v16 = 0 & v15 = 0 & one_to_one(v14) = 0 & relation(v14) = 0) | ( ~ (v15 = 0) & relation(v14) = v15) | ( ~ (v15 = 0) & empty(v14) = v15))) & ! [v14] : ( ~ (empty(v14) = 0) | function(v14) = 0) & ! [v14] : ( ~ (empty(v14) = 0) | ? [v15] : ? [v16] : ? [v17] : ((v17 = 0 & v16 = 0 & v15 = 0 & one_to_one(v14) = 0 & relation(v14) = 0 & function(v14) = 0) | ( ~ (v15 = 0) & relation(v14) = v15) | ( ~ (v15 = 0) & function(v14) = v15))) & ! [v14] : ( ~ (empty(v14) = 0) | (epsilon_transitive(v14) = 0 & ordinal(v14) = 0 & epsilon_connected(v14) = 0)) & ? [v14] : ? [v15] : ? [v16] : element(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : subset(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : ordered_pair(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : is_transitive_in(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : set_union2(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : unordered_pair(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : in(v15, v14) = v16 & ? [v14] : ? [v15] : powerset(v14) = v15 & ? [v14] : ? [v15] : relation_empty_yielding(v14) = v15 & ? [v14] : ? [v15] : element(v15, v14) = 0 & ? [v14] : ? [v15] : relation_dom(v14) = v15 & ? [v14] : ? [v15] : relation_rng(v14) = v15 & ? [v14] : ? [v15] : singleton(v14) = v15 & ? [v14] : ? [v15] : inclusion_relation(v14) = v15 & ? [v14] : ? [v15] : relation_field(v14) = v15 & ? [v14] : ? [v15] : transitive(v14) = v15 & ? [v14] : ? [v15] : one_to_one(v14) = v15 & ? [v14] : ? [v15] : relation(v14) = v15 & ? [v14] : ? [v15] : epsilon_transitive(v14) = v15 & ? [v14] : ? [v15] : ordinal(v14) = v15 & ? [v14] : ? [v15] : epsilon_connected(v14) = v15 & ? [v14] : ? [v15] : function(v14) = v15 & ? [v14] : ? [v15] : empty(v14) = v15) % 21.71/5.78 | 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, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13 yields: % 21.71/5.78 | (1) ~ (all_0_5_5 = 0) & ~ (all_0_8_8 = 0) & ~ (all_0_11_11 = 0) & relation_empty_yielding(all_0_10_10) = 0 & relation_empty_yielding(empty_set) = 0 & inclusion_relation(all_0_13_13) = all_0_12_12 & transitive(all_0_12_12) = all_0_11_11 & one_to_one(all_0_4_4) = 0 & one_to_one(all_0_7_7) = 0 & one_to_one(empty_set) = 0 & relation(all_0_0_0) = 0 & relation(all_0_3_3) = 0 & relation(all_0_4_4) = 0 & relation(all_0_7_7) = 0 & relation(all_0_10_10) = 0 & relation(empty_set) = 0 & epsilon_transitive(all_0_1_1) = 0 & epsilon_transitive(all_0_4_4) = 0 & epsilon_transitive(all_0_9_9) = 0 & epsilon_transitive(empty_set) = 0 & ordinal(all_0_1_1) = 0 & ordinal(all_0_4_4) = 0 & ordinal(all_0_9_9) = 0 & ordinal(empty_set) = 0 & epsilon_connected(all_0_1_1) = 0 & epsilon_connected(all_0_4_4) = 0 & epsilon_connected(all_0_9_9) = 0 & epsilon_connected(empty_set) = 0 & function(all_0_0_0) = 0 & function(all_0_3_3) = 0 & function(all_0_4_4) = 0 & function(all_0_7_7) = 0 & function(all_0_10_10) = 0 & function(empty_set) = 0 & empty(all_0_2_2) = 0 & empty(all_0_3_3) = 0 & empty(all_0_4_4) = 0 & empty(all_0_6_6) = all_0_5_5 & empty(all_0_9_9) = all_0_8_8 & empty(empty_set) = 0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (ordered_pair(v3, v4) = v5) | ~ (ordered_pair(v2, v4) = v6) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v6, v0) = v7) | ~ (in(v5, v0) = 0) | ? [v8] : ? [v9] : (( ~ (v9 = 0) & ordered_pair(v2, v3) = v8 & in(v8, v0) = v9) | ( ~ (v8 = 0) & in(v4, v1) = v8) | ( ~ (v8 = 0) & in(v3, v1) = v8) | ( ~ (v8 = 0) & in(v2, v1) = v8))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (ordered_pair(v2, v4) = v6) | ~ (ordered_pair(v2, v3) = v5) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v6, v0) = v7) | ~ (in(v5, v0) = 0) | ? [v8] : ? [v9] : (( ~ (v9 = 0) & ordered_pair(v3, v4) = v8 & in(v8, v0) = v9) | ( ~ (v8 = 0) & in(v4, v1) = v8) | ( ~ (v8 = 0) & in(v3, v1) = v8) | ( ~ (v8 = 0) & in(v2, v1) = v8))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (ordered_pair(v2, v4) = v5) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v5, v0) = v6) | ~ (in(v3, v1) = 0) | ? [v7] : ? [v8] : (( ~ (v8 = 0) & ordered_pair(v3, v4) = v7 & in(v7, v0) = v8) | ( ~ (v8 = 0) & ordered_pair(v2, v3) = v7 & in(v7, v0) = v8) | ( ~ (v7 = 0) & in(v4, v1) = v7) | ( ~ (v7 = 0) & in(v2, v1) = v7))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (ordered_pair(v3, v4) = v6) | ~ (ordered_pair(v2, v3) = v5) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v6, v0) = 0) | ~ (in(v5, v0) = 0) | ? [v7] : ? [v8] : ((v8 = 0 & ordered_pair(v2, v4) = v7 & in(v7, v0) = 0) | ( ~ (v7 = 0) & in(v4, v1) = v7) | ( ~ (v7 = 0) & in(v3, v1) = v7) | ( ~ (v7 = 0) & in(v2, v1) = v7))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (inclusion_relation(v0) = v1) | ~ (subset(v3, v4) = v5) | ~ (relation_field(v1) = v2) | ? [v6] : ? [v7] : (( ~ (v6 = 0) & relation(v1) = v6) | ( ~ (v6 = 0) & in(v4, v0) = v6) | ( ~ (v6 = 0) & in(v3, v0) = v6) | (( ~ (v5 = 0) | (v7 = 0 & ordered_pair(v3, v4) = v6 & in(v6, v1) = 0)) & (v5 = 0 | ( ~ (v7 = 0) & ordered_pair(v3, v4) = v6 & in(v6, v1) = v7))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (inclusion_relation(v0) = v1) | ~ (ordered_pair(v3, v4) = v5) | ~ (relation_field(v1) = v2) | ? [v6] : ? [v7] : (( ~ (v6 = 0) & relation(v1) = v6) | ( ~ (v6 = 0) & in(v4, v0) = v6) | ( ~ (v6 = 0) & in(v3, v0) = v6) | (((v7 = 0 & subset(v3, v4) = 0) | ( ~ (v6 = 0) & in(v5, v1) = v6)) & ((v6 = 0 & in(v5, v1) = 0) | ( ~ (v7 = 0) & subset(v3, v4) = v7))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (ordered_pair(v3, v4) = v5) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v5, v0) = 0) | ~ (in(v2, v1) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & ordered_pair(v2, v4) = v6 & in(v6, v0) = 0) | ( ~ (v7 = 0) & ordered_pair(v2, v3) = v6 & in(v6, v0) = v7) | ( ~ (v6 = 0) & in(v4, v1) = v6) | ( ~ (v6 = 0) & in(v3, v1) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (ordered_pair(v2, v3) = v5) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v5, v0) = 0) | ~ (in(v4, v1) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & ordered_pair(v2, v4) = v6 & in(v6, v0) = 0) | ( ~ (v7 = 0) & ordered_pair(v3, v4) = v6 & in(v6, v0) = v7) | ( ~ (v6 = 0) & in(v3, v1) = v6) | ( ~ (v6 = 0) & in(v2, v1) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (element(v0, v2) = v4) | ? [v5] : ( ~ (v5 = 0) & in(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v4, v1) = 0) | ~ (in(v3, v1) = 0) | ~ (in(v2, v1) = 0) | ? [v5] : ? [v6] : ((v6 = 0 & ordered_pair(v2, v4) = v5 & in(v5, v0) = 0) | ( ~ (v6 = 0) & ordered_pair(v3, v4) = v5 & in(v5, v0) = v6) | ( ~ (v6 = 0) & ordered_pair(v2, v3) = v5 & in(v5, v0) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (powerset(v1) = v2) | ~ (element(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subset(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (element(v0, v2) = v3) | ~ (in(v0, v1) = 0) | ? [v4] : ? [v5] : ( ~ (v5 = 0) & powerset(v2) = v4 & element(v1, v4) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subset(v1, v2) = 0) | ~ (subset(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subset(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subset(v0, v2) = v3) | ~ (subset(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & subset(v1, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(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 | ~ (is_transitive_in(v3, v2) = v1) | ~ (is_transitive_in(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (set_union2(v3, v2) = v1) | ~ (set_union2(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (unordered_pair(v3, v2) = v1) | ~ (unordered_pair(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | element(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & empty(v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (inclusion_relation(v0) = v2) | ~ (relation_field(v1) = v0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ((v6 = 0 & v5 = 0 & in(v4, v0) = 0 & in(v3, v0) = 0 & ((v9 = 0 & subset(v3, v4) = 0) | (v8 = 0 & ordered_pair(v3, v4) = v7 & in(v7, v1) = 0)) & (( ~ (v9 = 0) & subset(v3, v4) = v9) | ( ~ (v8 = 0) & ordered_pair(v3, v4) = v7 & in(v7, v1) = v8))) | ( ~ (v3 = 0) & relation(v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ (inclusion_relation(v0) = v1) | ~ (relation_field(v1) = v2) | ? [v3] : ( ~ (v3 = 0) & relation(v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (element(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & in(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v1) = v3 & element(v0, v3) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (is_transitive_in(v0, v1) = v2) | ~ (relation(v0) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v9 = 0) & ordered_pair(v4, v5) = v7 & ordered_pair(v3, v5) = v8 & ordered_pair(v3, v4) = v6 & in(v8, v0) = v9 & in(v7, v0) = 0 & in(v6, v0) = 0 & in(v5, v1) = 0 & in(v4, v1) = 0 & in(v3, v1) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ((v3 = 0 & empty(v1) = 0) | ( ~ (v3 = 0) & element(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_empty_yielding(v2) = v1) | ~ (relation_empty_yielding(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_dom(v2) = v1) | ~ (relation_dom(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_rng(v2) = v1) | ~ (relation_rng(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (inclusion_relation(v2) = v1) | ~ (inclusion_relation(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_field(v2) = v1) | ~ (relation_field(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (transitive(v2) = v1) | ~ (transitive(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (one_to_one(v2) = v1) | ~ (one_to_one(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation(v2) = v1) | ~ (relation(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (epsilon_transitive(v2) = v1) | ~ (epsilon_transitive(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (ordinal(v2) = v1) | ~ (ordinal(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (epsilon_connected(v2) = v1) | ~ (epsilon_connected(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (function(v2) = v1) | ~ (function(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ (element(v0, v2) = 0) | subset(v0, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (inclusion_relation(v0) = v2) | ~ (relation(v1) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : (( ~ (v2 = v1) | (v3 = v0 & relation_field(v1) = v0 & ! [v11] : ! [v12] : ! [v13] : ( ~ (subset(v11, v12) = v13) | ? [v14] : ? [v15] : (( ~ (v14 = 0) & in(v12, v0) = v14) | ( ~ (v14 = 0) & in(v11, v0) = v14) | (( ~ (v13 = 0) | (v15 = 0 & ordered_pair(v11, v12) = v14 & in(v14, v1) = 0)) & (v13 = 0 | ( ~ (v15 = 0) & ordered_pair(v11, v12) = v14 & in(v14, v1) = v15))))) & ! [v11] : ! [v12] : ! [v13] : ( ~ (ordered_pair(v11, v12) = v13) | ? [v14] : ? [v15] : (( ~ (v14 = 0) & in(v12, v0) = v14) | ( ~ (v14 = 0) & in(v11, v0) = v14) | (((v15 = 0 & subset(v11, v12) = 0) | ( ~ (v14 = 0) & in(v13, v1) = v14)) & ((v14 = 0 & in(v13, v1) = 0) | ( ~ (v15 = 0) & subset(v11, v12) = v15))))))) & (v2 = v1 | (v7 = 0 & v6 = 0 & in(v5, v0) = 0 & in(v4, v0) = 0 & ((v10 = 0 & subset(v4, v5) = 0) | (v9 = 0 & ordered_pair(v4, v5) = v8 & in(v8, v1) = 0)) & (( ~ (v10 = 0) & subset(v4, v5) = v10) | ( ~ (v9 = 0) & ordered_pair(v4, v5) = v8 & in(v8, v1) = v9))) | ( ~ (v3 = v0) & relation_field(v1) = v3)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (subset(v1, v2) = 0) | ~ (subset(v0, v1) = 0) | subset(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (ordered_pair(v0, v1) = v2) | ? [v3] : ? [v4] : (singleton(v0) = v4 & unordered_pair(v3, v4) = v2 & unordered_pair(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (ordered_pair(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & empty(v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v1, v0) = v2) | set_union2(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v1, v0) = v2) | ? [v3] : ((v3 = 0 & empty(v0) = 0) | ( ~ (v3 = 0) & empty(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v0, v1) = v2) | set_union2(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v0, v1) = v2) | ? [v3] : ((v3 = 0 & empty(v0) = 0) | ( ~ (v3 = 0) & empty(v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v1, v0) = v2) | unordered_pair(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | unordered_pair(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | ? [v3] : ? [v4] : (singleton(v0) = v4 & ordered_pair(v0, v1) = v3 & unordered_pair(v2, v4) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (empty(v2) = 0) | ~ (in(v0, v1) = 0) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v2) = v3 & element(v1, v3) = v4)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (set_union2(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (set_union2(v0, empty_set) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (ordinal(v0) = v1) | ? [v2] : (( ~ (v2 = 0) & epsilon_transitive(v0) = v2) | ( ~ (v2 = 0) & epsilon_connected(v0) = v2))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (function(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v0) = v2)) & ! [v0] : ! [v1] : ( ~ (element(v0, v1) = 0) | ? [v2] : ((v2 = 0 & empty(v1) = 0) | (v2 = 0 & in(v0, v1) = 0))) & ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = v2 & relation_rng(v0) = v3 & relation_field(v0) = v2 & set_union2(v1, v3) = v2) | ( ~ (v2 = 0) & relation(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = v2 & relation_dom(v0) = v3 & relation_field(v0) = v2 & set_union2(v3, v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (inclusion_relation(v0) = v1) | relation(v1) = 0) & ! [v0] : ! [v1] : ( ~ (subset(v0, v1) = 0) | ? [v2] : (powerset(v1) = v2 & element(v0, v2) = 0)) & ! [v0] : ! [v1] : ( ~ (relation_field(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = v1 & relation_dom(v0) = v2 & relation_rng(v0) = v3 & set_union2(v2, v3) = v1) | ( ~ (v2 = 0) & relation(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_field(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v2 = 0) & relation(v0) = v2) | (((v3 = 0 & is_transitive_in(v0, v1) = 0) | ( ~ (v2 = 0) & transitive(v0) = v2)) & ((v2 = 0 & transitive(v0) = 0) | ( ~ (v3 = 0) & is_transitive_in(v0, v1) = v3))))) & ! [v0] : ! [v1] : ( ~ (transitive(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v2 = 0) & relation(v0) = v2) | (( ~ (v1 = 0) | (v3 = 0 & relation_field(v0) = v2 & is_transitive_in(v0, v2) = 0)) & (v1 = 0 | ( ~ (v3 = 0) & relation_field(v0) = v2 & is_transitive_in(v0, v2) = v3))))) & ! [v0] : ! [v1] : ( ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & v1 = 0 & relation(v0) = 0 & function(v0) = 0) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2) | ( ~ (v2 = 0) & empty(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (epsilon_transitive(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & v1 = 0 & ordinal(v0) = 0 & epsilon_connected(v0) = 0) | ( ~ (v2 = 0) & empty(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (epsilon_transitive(v0) = v1) | ? [v2] : ((v2 = 0 & v1 = 0 & epsilon_connected(v0) = 0) | ( ~ (v2 = 0) & ordinal(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (ordinal(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & v1 = 0 & epsilon_transitive(v0) = 0 & epsilon_connected(v0) = 0) | ( ~ (v2 = 0) & empty(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (epsilon_connected(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & v1 = 0 & epsilon_transitive(v0) = 0 & ordinal(v0) = 0) | ( ~ (v2 = 0) & empty(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (epsilon_connected(v0) = v1) | ? [v2] : ((v2 = 0 & v1 = 0 & epsilon_transitive(v0) = 0) | ( ~ (v2 = 0) & ordinal(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (in(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v0, v1) = v2)) & ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | element(v0, v1) = 0) & ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) & ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v1, v0) = v2)) & ! [v0] : (v0 = empty_set | ~ (empty(v0) = 0)) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : (relation_dom(v0) = v2 & relation_rng(v0) = v3 & relation_field(v0) = v1 & set_union2(v2, v3) = v1)) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : (((v3 = 0 & relation_field(v0) = v2 & is_transitive_in(v0, v2) = 0) | ( ~ (v1 = 0) & transitive(v0) = v1)) & ((v1 = 0 & transitive(v0) = 0) | ( ~ (v3 = 0) & relation_field(v0) = v2 & is_transitive_in(v0, v2) = v3)))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & one_to_one(v0) = 0 & function(v0) = 0) | ( ~ (v1 = 0) & function(v0) = v1) | ( ~ (v1 = 0) & empty(v0) = v1))) & ! [v0] : ( ~ (epsilon_transitive(v0) = 0) | ? [v1] : ((v1 = 0 & ordinal(v0) = 0) | ( ~ (v1 = 0) & epsilon_connected(v0) = v1))) & ! [v0] : ( ~ (ordinal(v0) = 0) | (epsilon_transitive(v0) = 0 & epsilon_connected(v0) = 0)) & ! [v0] : ( ~ (epsilon_connected(v0) = 0) | ? [v1] : ((v1 = 0 & ordinal(v0) = 0) | ( ~ (v1 = 0) & epsilon_transitive(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & one_to_one(v0) = 0 & relation(v0) = 0) | ( ~ (v1 = 0) & relation(v0) = v1) | ( ~ (v1 = 0) & empty(v0) = v1))) & ! [v0] : ( ~ (empty(v0) = 0) | function(v0) = 0) & ! [v0] : ( ~ (empty(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & v1 = 0 & one_to_one(v0) = 0 & relation(v0) = 0 & function(v0) = 0) | ( ~ (v1 = 0) & relation(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (empty(v0) = 0) | (epsilon_transitive(v0) = 0 & ordinal(v0) = 0 & epsilon_connected(v0) = 0)) & ? [v0] : ? [v1] : ? [v2] : element(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : subset(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : ordered_pair(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : is_transitive_in(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : set_union2(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : unordered_pair(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : in(v1, v0) = v2 & ? [v0] : ? [v1] : powerset(v0) = v1 & ? [v0] : ? [v1] : relation_empty_yielding(v0) = v1 & ? [v0] : ? [v1] : element(v1, v0) = 0 & ? [v0] : ? [v1] : relation_dom(v0) = v1 & ? [v0] : ? [v1] : relation_rng(v0) = v1 & ? [v0] : ? [v1] : singleton(v0) = v1 & ? [v0] : ? [v1] : inclusion_relation(v0) = v1 & ? [v0] : ? [v1] : relation_field(v0) = v1 & ? [v0] : ? [v1] : transitive(v0) = v1 & ? [v0] : ? [v1] : one_to_one(v0) = v1 & ? [v0] : ? [v1] : relation(v0) = v1 & ? [v0] : ? [v1] : epsilon_transitive(v0) = v1 & ? [v0] : ? [v1] : ordinal(v0) = v1 & ? [v0] : ? [v1] : epsilon_connected(v0) = v1 & ? [v0] : ? [v1] : function(v0) = v1 & ? [v0] : ? [v1] : empty(v0) = v1 % 21.71/5.82 | % 21.71/5.82 | Applying alpha-rule on (1) yields: % 21.71/5.82 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (ordered_pair(v2, v3) = v5) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v5, v0) = 0) | ~ (in(v4, v1) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & ordered_pair(v2, v4) = v6 & in(v6, v0) = 0) | ( ~ (v7 = 0) & ordered_pair(v3, v4) = v6 & in(v6, v0) = v7) | ( ~ (v6 = 0) & in(v3, v1) = v6) | ( ~ (v6 = 0) & in(v2, v1) = v6))) % 21.71/5.82 | (3) ! [v0] : ( ~ (empty(v0) = 0) | (epsilon_transitive(v0) = 0 & ordinal(v0) = 0 & epsilon_connected(v0) = 0)) % 21.71/5.82 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (ordered_pair(v2, v4) = v6) | ~ (ordered_pair(v2, v3) = v5) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v6, v0) = v7) | ~ (in(v5, v0) = 0) | ? [v8] : ? [v9] : (( ~ (v9 = 0) & ordered_pair(v3, v4) = v8 & in(v8, v0) = v9) | ( ~ (v8 = 0) & in(v4, v1) = v8) | ( ~ (v8 = 0) & in(v3, v1) = v8) | ( ~ (v8 = 0) & in(v2, v1) = v8))) % 21.71/5.82 | (5) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) % 21.71/5.82 | (6) ! [v0] : ! [v1] : (v1 = 0 | ~ (function(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v0) = v2)) % 21.71/5.82 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (ordered_pair(v2, v4) = v5) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v5, v0) = v6) | ~ (in(v3, v1) = 0) | ? [v7] : ? [v8] : (( ~ (v8 = 0) & ordered_pair(v3, v4) = v7 & in(v7, v0) = v8) | ( ~ (v8 = 0) & ordered_pair(v2, v3) = v7 & in(v7, v0) = v8) | ( ~ (v7 = 0) & in(v4, v1) = v7) | ( ~ (v7 = 0) & in(v2, v1) = v7))) % 21.71/5.82 | (8) ? [v0] : ? [v1] : relation_dom(v0) = v1 % 21.71/5.82 | (9) function(all_0_4_4) = 0 % 21.71/5.82 | (10) ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = v2 & relation_rng(v0) = v3 & relation_field(v0) = v2 & set_union2(v1, v3) = v2) | ( ~ (v2 = 0) & relation(v0) = v2))) % 21.71/5.82 | (11) empty(all_0_4_4) = 0 % 21.71/5.82 | (12) ordinal(all_0_1_1) = 0 % 21.71/5.82 | (13) relation(all_0_7_7) = 0 % 21.71/5.82 | (14) ? [v0] : ? [v1] : relation(v0) = v1 % 21.71/5.82 | (15) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ((v3 = 0 & empty(v1) = 0) | ( ~ (v3 = 0) & element(v0, v1) = v3))) % 21.71/5.82 | (16) ! [v0] : ! [v1] : ( ~ (epsilon_connected(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & v1 = 0 & epsilon_transitive(v0) = 0 & ordinal(v0) = 0) | ( ~ (v2 = 0) & empty(v0) = v2))) % 21.71/5.82 | (17) ? [v0] : ? [v1] : ? [v2] : subset(v1, v0) = v2 % 21.71/5.82 | (18) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (one_to_one(v2) = v1) | ~ (one_to_one(v2) = v0)) % 21.71/5.82 | (19) ? [v0] : ? [v1] : powerset(v0) = v1 % 21.71/5.82 | (20) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) % 21.71/5.82 | (21) inclusion_relation(all_0_13_13) = all_0_12_12 % 21.71/5.82 | (22) empty(empty_set) = 0 % 21.71/5.82 | (23) ! [v0] : ( ~ (ordinal(v0) = 0) | (epsilon_transitive(v0) = 0 & epsilon_connected(v0) = 0)) % 21.71/5.82 | (24) ? [v0] : ? [v1] : ? [v2] : in(v1, v0) = v2 % 21.71/5.82 | (25) relation(all_0_4_4) = 0 % 21.71/5.82 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subset(v1, v2) = 0) | ~ (subset(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subset(v0, v1) = v4)) % 21.71/5.82 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) % 21.71/5.82 | (28) epsilon_connected(all_0_9_9) = 0 % 21.71/5.82 | (29) empty(all_0_9_9) = all_0_8_8 % 21.71/5.82 | (30) ! [v0] : ! [v1] : (v1 = 0 | ~ (ordinal(v0) = v1) | ? [v2] : (( ~ (v2 = 0) & epsilon_transitive(v0) = v2) | ( ~ (v2 = 0) & epsilon_connected(v0) = v2))) % 21.71/5.82 | (31) ? [v0] : ? [v1] : transitive(v0) = v1 % 21.71/5.82 | (32) ~ (all_0_8_8 = 0) % 21.71/5.82 | (33) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (ordinal(v2) = v1) | ~ (ordinal(v2) = v0)) % 21.71/5.82 | (34) ! [v0] : ! [v1] : ! [v2] : ( ~ (ordered_pair(v0, v1) = v2) | ? [v3] : ? [v4] : (singleton(v0) = v4 & unordered_pair(v3, v4) = v2 & unordered_pair(v0, v1) = v3)) % 21.71/5.82 | (35) epsilon_transitive(all_0_1_1) = 0 % 21.71/5.82 | (36) epsilon_connected(all_0_1_1) = 0 % 21.71/5.82 | (37) ! [v0] : ! [v1] : ! [v2] : ( ~ (ordered_pair(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & empty(v2) = v3)) % 21.71/5.83 | (38) relation(all_0_3_3) = 0 % 21.71/5.83 | (39) ! [v0] : ( ~ (epsilon_connected(v0) = 0) | ? [v1] : ((v1 = 0 & ordinal(v0) = 0) | ( ~ (v1 = 0) & epsilon_transitive(v0) = v1))) % 21.71/5.83 | (40) ! [v0] : ( ~ (epsilon_transitive(v0) = 0) | ? [v1] : ((v1 = 0 & ordinal(v0) = 0) | ( ~ (v1 = 0) & epsilon_connected(v0) = v1))) % 21.71/5.83 | (41) empty(all_0_6_6) = all_0_5_5 % 21.71/5.83 | (42) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = v2 & relation_dom(v0) = v3 & relation_field(v0) = v2 & set_union2(v3, v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2))) % 21.71/5.83 | (43) ? [v0] : ? [v1] : relation_field(v0) = v1 % 21.71/5.83 | (44) function(all_0_10_10) = 0 % 21.71/5.83 | (45) ! [v0] : ! [v1] : ( ~ (transitive(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v2 = 0) & relation(v0) = v2) | (( ~ (v1 = 0) | (v3 = 0 & relation_field(v0) = v2 & is_transitive_in(v0, v2) = 0)) & (v1 = 0 | ( ~ (v3 = 0) & relation_field(v0) = v2 & is_transitive_in(v0, v2) = v3))))) % 21.71/5.83 | (46) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v0, v1) = v2) | ? [v3] : ((v3 = 0 & empty(v0) = 0) | ( ~ (v3 = 0) & empty(v2) = v3))) % 21.71/5.83 | (47) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (ordered_pair(v3, v2) = v1) | ~ (ordered_pair(v3, v2) = v0)) % 21.71/5.83 | (48) relation(all_0_10_10) = 0 % 21.71/5.83 | (49) ? [v0] : ? [v1] : epsilon_transitive(v0) = v1 % 21.71/5.83 | (50) epsilon_transitive(all_0_4_4) = 0 % 21.71/5.83 | (51) ! [v0] : ( ~ (empty(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & v1 = 0 & one_to_one(v0) = 0 & relation(v0) = 0 & function(v0) = 0) | ( ~ (v1 = 0) & relation(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) % 21.71/5.83 | (52) ! [v0] : ! [v1] : ! [v2] : ( ~ (empty(v2) = 0) | ~ (in(v0, v1) = 0) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v2) = v3 & element(v1, v3) = v4)) % 21.71/5.83 | (53) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (inclusion_relation(v0) = v2) | ~ (relation_field(v1) = v0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ((v6 = 0 & v5 = 0 & in(v4, v0) = 0 & in(v3, v0) = 0 & ((v9 = 0 & subset(v3, v4) = 0) | (v8 = 0 & ordered_pair(v3, v4) = v7 & in(v7, v1) = 0)) & (( ~ (v9 = 0) & subset(v3, v4) = v9) | ( ~ (v8 = 0) & ordered_pair(v3, v4) = v7 & in(v7, v1) = v8))) | ( ~ (v3 = 0) & relation(v1) = v3))) % 21.71/5.83 | (54) ? [v0] : ? [v1] : relation_rng(v0) = v1 % 21.71/5.83 | (55) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (epsilon_transitive(v2) = v1) | ~ (epsilon_transitive(v2) = v0)) % 21.71/5.83 | (56) ! [v0] : ! [v1] : (v1 = v0 | ~ (set_union2(v0, empty_set) = v1)) % 21.71/5.83 | (57) ordinal(all_0_9_9) = 0 % 21.71/5.83 | (58) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_rng(v2) = v1) | ~ (relation_rng(v2) = v0)) % 21.71/5.83 | (59) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) % 21.71/5.83 | (60) ? [v0] : ? [v1] : empty(v0) = v1 % 21.71/5.83 | (61) ? [v0] : ? [v1] : ? [v2] : element(v1, v0) = v2 % 21.71/5.83 | (62) relation(empty_set) = 0 % 21.71/5.83 | (63) relation_empty_yielding(all_0_10_10) = 0 % 21.71/5.83 | (64) ! [v0] : ! [v1] : ! [v2] : ( ~ (subset(v1, v2) = 0) | ~ (subset(v0, v1) = 0) | subset(v0, v2) = 0) % 21.71/5.83 | (65) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : (relation_dom(v0) = v2 & relation_rng(v0) = v3 & relation_field(v0) = v1 & set_union2(v2, v3) = v1)) % 21.71/5.83 | (66) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v1, v0) = v2) | ? [v3] : ((v3 = 0 & empty(v0) = 0) | ( ~ (v3 = 0) & empty(v2) = v3))) % 21.71/5.83 | (67) one_to_one(all_0_7_7) = 0 % 21.71/5.83 | (68) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation(v2) = v1) | ~ (relation(v2) = v0)) % 21.71/5.83 | (69) ! [v0] : ! [v1] : ( ~ (epsilon_transitive(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & v1 = 0 & ordinal(v0) = 0 & epsilon_connected(v0) = 0) | ( ~ (v2 = 0) & empty(v0) = v2))) % 21.71/5.83 | (70) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v1) = v3 & element(v0, v3) = v4)) % 21.71/5.83 | (71) ! [v0] : (v0 = empty_set | ~ (empty(v0) = 0)) % 21.71/5.83 | (72) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (epsilon_connected(v2) = v1) | ~ (epsilon_connected(v2) = v0)) % 21.71/5.83 | (73) function(empty_set) = 0 % 21.71/5.83 | (74) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (ordered_pair(v3, v4) = v6) | ~ (ordered_pair(v2, v3) = v5) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v6, v0) = 0) | ~ (in(v5, v0) = 0) | ? [v7] : ? [v8] : ((v8 = 0 & ordered_pair(v2, v4) = v7 & in(v7, v0) = 0) | ( ~ (v7 = 0) & in(v4, v1) = v7) | ( ~ (v7 = 0) & in(v3, v1) = v7) | ( ~ (v7 = 0) & in(v2, v1) = v7))) % 21.71/5.84 | (75) ? [v0] : ? [v1] : ? [v2] : ordered_pair(v1, v0) = v2 % 21.71/5.84 | (76) ! [v0] : ! [v1] : ( ~ (relation_field(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = v1 & relation_dom(v0) = v2 & relation_rng(v0) = v3 & set_union2(v2, v3) = v1) | ( ~ (v2 = 0) & relation(v0) = v2))) % 21.71/5.84 | (77) ! [v0] : ! [v1] : ( ~ (element(v0, v1) = 0) | ? [v2] : ((v2 = 0 & empty(v1) = 0) | (v2 = 0 & in(v0, v1) = 0))) % 21.71/5.84 | (78) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) % 21.71/5.84 | (79) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) % 21.71/5.84 | (80) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & empty(v2) = v4)) % 21.71/5.84 | (81) ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | unordered_pair(v1, v0) = v2) % 21.71/5.84 | (82) ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v1, v0) = v2) | unordered_pair(v0, v1) = v2) % 21.71/5.84 | (83) ! [v0] : ! [v1] : ( ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & v1 = 0 & relation(v0) = 0 & function(v0) = 0) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2) | ( ~ (v2 = 0) & empty(v0) = v2))) % 21.71/5.84 | (84) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (inclusion_relation(v2) = v1) | ~ (inclusion_relation(v2) = v0)) % 21.71/5.84 | (85) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (inclusion_relation(v0) = v1) | ~ (subset(v3, v4) = v5) | ~ (relation_field(v1) = v2) | ? [v6] : ? [v7] : (( ~ (v6 = 0) & relation(v1) = v6) | ( ~ (v6 = 0) & in(v4, v0) = v6) | ( ~ (v6 = 0) & in(v3, v0) = v6) | (( ~ (v5 = 0) | (v7 = 0 & ordered_pair(v3, v4) = v6 & in(v6, v1) = 0)) & (v5 = 0 | ( ~ (v7 = 0) & ordered_pair(v3, v4) = v6 & in(v6, v1) = v7))))) % 21.71/5.84 | (86) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (element(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & in(v0, v1) = v3)) % 21.71/5.84 | (87) ? [v0] : ? [v1] : ? [v2] : unordered_pair(v1, v0) = v2 % 21.71/5.84 | (88) ! [v0] : ! [v1] : ( ~ (subset(v0, v1) = 0) | ? [v2] : (powerset(v1) = v2 & element(v0, v2) = 0)) % 21.71/5.84 | (89) ordinal(empty_set) = 0 % 21.71/5.84 | (90) ? [v0] : ? [v1] : element(v1, v0) = 0 % 21.71/5.84 | (91) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_field(v2) = v1) | ~ (relation_field(v2) = v0)) % 21.71/5.84 | (92) ? [v0] : ? [v1] : ? [v2] : set_union2(v1, v0) = v2 % 21.71/5.84 | (93) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & one_to_one(v0) = 0 & relation(v0) = 0) | ( ~ (v1 = 0) & relation(v0) = v1) | ( ~ (v1 = 0) & empty(v0) = v1))) % 21.71/5.84 | (94) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) % 21.71/5.84 | (95) epsilon_transitive(all_0_9_9) = 0 % 21.71/5.84 | (96) ~ (all_0_11_11 = 0) % 21.71/5.84 | (97) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v1, v0) = v2)) % 21.71/5.84 | (98) ! [v0] : ( ~ (empty(v0) = 0) | function(v0) = 0) % 21.71/5.84 | (99) ! [v0] : ! [v1] : ( ~ (ordinal(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & v1 = 0 & epsilon_transitive(v0) = 0 & epsilon_connected(v0) = 0) | ( ~ (v2 = 0) & empty(v0) = v2))) % 21.71/5.84 | (100) ? [v0] : ? [v1] : function(v0) = v1 % 21.71/5.84 | (101) ! [v0] : ! [v1] : ( ~ (relation_field(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v2 = 0) & relation(v0) = v2) | (((v3 = 0 & is_transitive_in(v0, v1) = 0) | ( ~ (v2 = 0) & transitive(v0) = v2)) & ((v2 = 0 & transitive(v0) = 0) | ( ~ (v3 = 0) & is_transitive_in(v0, v1) = v3))))) % 21.71/5.84 | (102) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_dom(v2) = v1) | ~ (relation_dom(v2) = v0)) % 21.71/5.84 | (103) ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) % 21.71/5.84 | (104) ! [v0] : ! [v1] : ( ~ (epsilon_transitive(v0) = v1) | ? [v2] : ((v2 = 0 & v1 = 0 & epsilon_connected(v0) = 0) | ( ~ (v2 = 0) & ordinal(v0) = v2))) % 21.71/5.84 | (105) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (ordered_pair(v3, v4) = v5) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v5, v0) = 0) | ~ (in(v2, v1) = 0) | ? [v6] : ? [v7] : ((v7 = 0 & ordered_pair(v2, v4) = v6 & in(v6, v0) = 0) | ( ~ (v7 = 0) & ordered_pair(v2, v3) = v6 & in(v6, v0) = v7) | ( ~ (v6 = 0) & in(v4, v1) = v6) | ( ~ (v6 = 0) & in(v3, v1) = v6))) % 21.71/5.85 | (106) ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ (inclusion_relation(v0) = v1) | ~ (relation_field(v1) = v2) | ? [v3] : ( ~ (v3 = 0) & relation(v1) = v3)) % 21.71/5.85 | (107) ! [v0] : ! [v1] : ( ~ (inclusion_relation(v0) = v1) | relation(v1) = 0) % 21.71/5.85 | (108) ? [v0] : ? [v1] : ordinal(v0) = v1 % 21.71/5.85 | (109) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (unordered_pair(v3, v2) = v1) | ~ (unordered_pair(v3, v2) = v0)) % 21.71/5.85 | (110) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & one_to_one(v0) = 0 & function(v0) = 0) | ( ~ (v1 = 0) & function(v0) = v1) | ( ~ (v1 = 0) & empty(v0) = v1))) % 21.71/5.85 | (111) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_empty_yielding(v2) = v1) | ~ (relation_empty_yielding(v2) = v0)) % 21.71/5.85 | (112) ! [v0] : ! [v1] : ! [v2] : ( ~ (unordered_pair(v0, v1) = v2) | ? [v3] : ? [v4] : (singleton(v0) = v4 & ordered_pair(v0, v1) = v3 & unordered_pair(v2, v4) = v3)) % 21.71/5.85 | (113) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (is_transitive_in(v0, v1) = v2) | ~ (relation(v0) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v9 = 0) & ordered_pair(v4, v5) = v7 & ordered_pair(v3, v5) = v8 & ordered_pair(v3, v4) = v6 & in(v8, v0) = v9 & in(v7, v0) = 0 & in(v6, v0) = 0 & in(v5, v1) = 0 & in(v4, v1) = 0 & in(v3, v1) = 0)) % 21.71/5.85 | (114) function(all_0_7_7) = 0 % 21.71/5.85 | (115) ~ (all_0_5_5 = 0) % 21.71/5.85 | (116) function(all_0_0_0) = 0 % 21.71/5.85 | (117) transitive(all_0_12_12) = all_0_11_11 % 21.71/5.85 | (118) relation(all_0_0_0) = 0 % 21.71/5.85 | (119) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : (((v3 = 0 & relation_field(v0) = v2 & is_transitive_in(v0, v2) = 0) | ( ~ (v1 = 0) & transitive(v0) = v1)) & ((v1 = 0 & transitive(v0) = 0) | ( ~ (v3 = 0) & relation_field(v0) = v2 & is_transitive_in(v0, v2) = v3)))) % 21.71/5.85 | (120) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v4, v1) = 0) | ~ (in(v3, v1) = 0) | ~ (in(v2, v1) = 0) | ? [v5] : ? [v6] : ((v6 = 0 & ordered_pair(v2, v4) = v5 & in(v5, v0) = 0) | ( ~ (v6 = 0) & ordered_pair(v3, v4) = v5 & in(v5, v0) = v6) | ( ~ (v6 = 0) & ordered_pair(v2, v3) = v5 & in(v5, v0) = v6))) % 21.71/5.85 | (121) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (set_union2(v3, v2) = v1) | ~ (set_union2(v3, v2) = v0)) % 21.71/5.85 | (122) ? [v0] : ? [v1] : epsilon_connected(v0) = v1 % 21.71/5.85 | (123) one_to_one(all_0_4_4) = 0 % 21.71/5.85 | (124) empty(all_0_2_2) = 0 % 21.71/5.85 | (125) empty(all_0_3_3) = 0 % 21.71/5.85 | (126) ! [v0] : ! [v1] : ( ~ (epsilon_connected(v0) = v1) | ? [v2] : ((v2 = 0 & v1 = 0 & epsilon_transitive(v0) = 0) | ( ~ (v2 = 0) & ordinal(v0) = v2))) % 21.71/5.85 | (127) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | element(v0, v1) = 0) % 21.71/5.85 | (128) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (is_transitive_in(v3, v2) = v1) | ~ (is_transitive_in(v3, v2) = v0)) % 21.71/5.85 | (129) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (powerset(v1) = v2) | ~ (element(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subset(v0, v1) = v4)) % 21.71/5.85 | (130) ? [v0] : ? [v1] : inclusion_relation(v0) = v1 % 21.71/5.85 | (131) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (inclusion_relation(v0) = v1) | ~ (ordered_pair(v3, v4) = v5) | ~ (relation_field(v1) = v2) | ? [v6] : ? [v7] : (( ~ (v6 = 0) & relation(v1) = v6) | ( ~ (v6 = 0) & in(v4, v0) = v6) | ( ~ (v6 = 0) & in(v3, v0) = v6) | (((v7 = 0 & subset(v3, v4) = 0) | ( ~ (v6 = 0) & in(v5, v1) = v6)) & ((v6 = 0 & in(v5, v1) = 0) | ( ~ (v7 = 0) & subset(v3, v4) = v7))))) % 21.71/5.85 | (132) ! [v0] : ! [v1] : (v1 = v0 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) % 21.71/5.85 | (133) ? [v0] : ? [v1] : ? [v2] : is_transitive_in(v1, v0) = v2 % 21.71/5.85 | (134) ordinal(all_0_4_4) = 0 % 21.71/5.85 | (135) ! [v0] : ! [v1] : ! [v2] : ( ~ (inclusion_relation(v0) = v2) | ~ (relation(v1) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : (( ~ (v2 = v1) | (v3 = v0 & relation_field(v1) = v0 & ! [v11] : ! [v12] : ! [v13] : ( ~ (subset(v11, v12) = v13) | ? [v14] : ? [v15] : (( ~ (v14 = 0) & in(v12, v0) = v14) | ( ~ (v14 = 0) & in(v11, v0) = v14) | (( ~ (v13 = 0) | (v15 = 0 & ordered_pair(v11, v12) = v14 & in(v14, v1) = 0)) & (v13 = 0 | ( ~ (v15 = 0) & ordered_pair(v11, v12) = v14 & in(v14, v1) = v15))))) & ! [v11] : ! [v12] : ! [v13] : ( ~ (ordered_pair(v11, v12) = v13) | ? [v14] : ? [v15] : (( ~ (v14 = 0) & in(v12, v0) = v14) | ( ~ (v14 = 0) & in(v11, v0) = v14) | (((v15 = 0 & subset(v11, v12) = 0) | ( ~ (v14 = 0) & in(v13, v1) = v14)) & ((v14 = 0 & in(v13, v1) = 0) | ( ~ (v15 = 0) & subset(v11, v12) = v15))))))) & (v2 = v1 | (v7 = 0 & v6 = 0 & in(v5, v0) = 0 & in(v4, v0) = 0 & ((v10 = 0 & subset(v4, v5) = 0) | (v9 = 0 & ordered_pair(v4, v5) = v8 & in(v8, v1) = 0)) & (( ~ (v10 = 0) & subset(v4, v5) = v10) | ( ~ (v9 = 0) & ordered_pair(v4, v5) = v8 & in(v8, v1) = v9))) | ( ~ (v3 = v0) & relation_field(v1) = v3)))) % 21.71/5.85 | (136) ! [v0] : ! [v1] : (v1 = v0 | ~ (set_union2(v0, v0) = v1)) % 21.71/5.85 | (137) ? [v0] : ? [v1] : one_to_one(v0) = v1 % 21.71/5.85 | (138) ! [v0] : ! [v1] : ( ~ (in(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v0, v1) = v2)) % 21.71/5.85 | (139) ? [v0] : ? [v1] : singleton(v0) = v1 % 21.71/5.85 | (140) one_to_one(empty_set) = 0 % 21.71/5.85 | (141) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (element(v0, v2) = v3) | ~ (in(v0, v1) = 0) | ? [v4] : ? [v5] : ( ~ (v5 = 0) & powerset(v2) = v4 & element(v1, v4) = v5)) % 21.71/5.85 | (142) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v0, v1) = v2) | set_union2(v1, v0) = v2) % 21.71/5.86 | (143) ! [v0] : ! [v1] : ! [v2] : ( ~ (set_union2(v1, v0) = v2) | set_union2(v0, v1) = v2) % 21.71/5.86 | (144) relation_empty_yielding(empty_set) = 0 % 21.71/5.86 | (145) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | element(v0, v2) = 0) % 21.71/5.86 | (146) epsilon_transitive(empty_set) = 0 % 21.71/5.86 | (147) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (function(v2) = v1) | ~ (function(v2) = v0)) % 21.71/5.86 | (148) epsilon_connected(empty_set) = 0 % 21.71/5.86 | (149) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (subset(v0, v2) = v3) | ~ (subset(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & subset(v1, v2) = v4)) % 21.71/5.86 | (150) epsilon_connected(all_0_4_4) = 0 % 21.71/5.86 | (151) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (ordered_pair(v3, v4) = v5) | ~ (ordered_pair(v2, v4) = v6) | ~ (is_transitive_in(v0, v1) = 0) | ~ (relation(v0) = 0) | ~ (in(v6, v0) = v7) | ~ (in(v5, v0) = 0) | ? [v8] : ? [v9] : (( ~ (v9 = 0) & ordered_pair(v2, v3) = v8 & in(v8, v0) = v9) | ( ~ (v8 = 0) & in(v4, v1) = v8) | ( ~ (v8 = 0) & in(v3, v1) = v8) | ( ~ (v8 = 0) & in(v2, v1) = v8))) % 21.71/5.86 | (152) ? [v0] : ? [v1] : relation_empty_yielding(v0) = v1 % 21.71/5.86 | (153) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (transitive(v2) = v1) | ~ (transitive(v2) = v0)) % 21.71/5.86 | (154) function(all_0_3_3) = 0 % 21.71/5.86 | (155) ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ (element(v0, v2) = 0) | subset(v0, v1) = 0) % 21.71/5.86 | (156) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (element(v0, v2) = v4) | ? [v5] : ( ~ (v5 = 0) & in(v0, v1) = v5)) % 21.71/5.86 | % 21.71/5.86 | Instantiating formula (107) with all_0_12_12, all_0_13_13 and discharging atoms inclusion_relation(all_0_13_13) = all_0_12_12, yields: % 21.71/5.86 | (157) relation(all_0_12_12) = 0 % 21.71/5.86 | % 21.71/5.86 | Instantiating formula (45) with all_0_11_11, all_0_12_12 and discharging atoms transitive(all_0_12_12) = all_0_11_11, yields: % 21.71/5.86 | (158) ? [v0] : ? [v1] : (( ~ (v0 = 0) & relation(all_0_12_12) = v0) | (( ~ (all_0_11_11 = 0) | (v1 = 0 & relation_field(all_0_12_12) = v0 & is_transitive_in(all_0_12_12, v0) = 0)) & (all_0_11_11 = 0 | ( ~ (v1 = 0) & relation_field(all_0_12_12) = v0 & is_transitive_in(all_0_12_12, v0) = v1)))) % 21.71/5.86 | % 21.71/5.86 | Instantiating (158) with all_73_0_101, all_73_1_102 yields: % 21.71/5.86 | (159) ( ~ (all_73_1_102 = 0) & relation(all_0_12_12) = all_73_1_102) | (( ~ (all_0_11_11 = 0) | (all_73_0_101 = 0 & relation_field(all_0_12_12) = all_73_1_102 & is_transitive_in(all_0_12_12, all_73_1_102) = 0)) & (all_0_11_11 = 0 | ( ~ (all_73_0_101 = 0) & relation_field(all_0_12_12) = all_73_1_102 & is_transitive_in(all_0_12_12, all_73_1_102) = all_73_0_101))) % 21.71/5.86 | % 21.71/5.86 +-Applying beta-rule and splitting (159), into two cases. % 21.71/5.86 |-Branch one: % 21.71/5.86 | (160) ~ (all_73_1_102 = 0) & relation(all_0_12_12) = all_73_1_102 % 21.71/5.86 | % 21.71/5.86 | Applying alpha-rule on (160) yields: % 21.71/5.86 | (161) ~ (all_73_1_102 = 0) % 21.71/5.86 | (162) relation(all_0_12_12) = all_73_1_102 % 21.71/5.86 | % 21.71/5.86 | Instantiating formula (68) with all_0_12_12, 0, all_73_1_102 and discharging atoms relation(all_0_12_12) = all_73_1_102, relation(all_0_12_12) = 0, yields: % 21.71/5.86 | (163) all_73_1_102 = 0 % 21.71/5.86 | % 21.71/5.86 | Equations (163) can reduce 161 to: % 21.71/5.86 | (164) $false % 21.71/5.86 | % 21.71/5.86 |-The branch is then unsatisfiable % 21.71/5.86 |-Branch two: % 21.71/5.86 | (165) ( ~ (all_0_11_11 = 0) | (all_73_0_101 = 0 & relation_field(all_0_12_12) = all_73_1_102 & is_transitive_in(all_0_12_12, all_73_1_102) = 0)) & (all_0_11_11 = 0 | ( ~ (all_73_0_101 = 0) & relation_field(all_0_12_12) = all_73_1_102 & is_transitive_in(all_0_12_12, all_73_1_102) = all_73_0_101)) % 21.71/5.86 | % 21.71/5.86 | Applying alpha-rule on (165) yields: % 21.71/5.86 | (166) ~ (all_0_11_11 = 0) | (all_73_0_101 = 0 & relation_field(all_0_12_12) = all_73_1_102 & is_transitive_in(all_0_12_12, all_73_1_102) = 0) % 21.71/5.86 | (167) all_0_11_11 = 0 | ( ~ (all_73_0_101 = 0) & relation_field(all_0_12_12) = all_73_1_102 & is_transitive_in(all_0_12_12, all_73_1_102) = all_73_0_101) % 21.71/5.86 | % 21.71/5.86 +-Applying beta-rule and splitting (167), into two cases. % 21.71/5.86 |-Branch one: % 21.71/5.86 | (168) all_0_11_11 = 0 % 21.71/5.86 | % 21.71/5.86 | Equations (168) can reduce 96 to: % 21.71/5.86 | (164) $false % 21.71/5.86 | % 21.71/5.86 |-The branch is then unsatisfiable % 21.71/5.86 |-Branch two: % 21.71/5.86 | (96) ~ (all_0_11_11 = 0) % 21.71/5.86 | (171) ~ (all_73_0_101 = 0) & relation_field(all_0_12_12) = all_73_1_102 & is_transitive_in(all_0_12_12, all_73_1_102) = all_73_0_101 % 21.71/5.86 | % 21.71/5.86 | Applying alpha-rule on (171) yields: % 21.71/5.86 | (172) ~ (all_73_0_101 = 0) % 21.71/5.86 | (173) relation_field(all_0_12_12) = all_73_1_102 % 21.71/5.86 | (174) is_transitive_in(all_0_12_12, all_73_1_102) = all_73_0_101 % 21.71/5.86 | % 21.71/5.86 | Instantiating formula (106) with all_73_1_102, all_0_12_12, all_0_13_13 and discharging atoms inclusion_relation(all_0_13_13) = all_0_12_12, relation_field(all_0_12_12) = all_73_1_102, yields: % 21.71/5.86 | (175) all_73_1_102 = all_0_13_13 | ? [v0] : ( ~ (v0 = 0) & relation(all_0_12_12) = v0) % 21.71/5.86 | % 21.71/5.86 | Instantiating formula (113) with all_73_0_101, all_73_1_102, all_0_12_12 and discharging atoms is_transitive_in(all_0_12_12, all_73_1_102) = all_73_0_101, relation(all_0_12_12) = 0, yields: % 21.71/5.86 | (176) all_73_0_101 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = 0) & ordered_pair(v1, v2) = v4 & ordered_pair(v0, v2) = v5 & ordered_pair(v0, v1) = v3 & in(v5, all_0_12_12) = v6 & in(v4, all_0_12_12) = 0 & in(v3, all_0_12_12) = 0 & in(v2, all_73_1_102) = 0 & in(v1, all_73_1_102) = 0 & in(v0, all_73_1_102) = 0) % 21.71/5.86 | % 21.71/5.86 | Instantiating formula (135) with all_0_12_12, all_0_12_12, all_0_13_13 and discharging atoms inclusion_relation(all_0_13_13) = all_0_12_12, relation(all_0_12_12) = 0, yields: % 21.71/5.86 | (177) relation_field(all_0_12_12) = all_0_13_13 & ! [v0] : ! [v1] : ! [v2] : ( ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : (( ~ (v3 = 0) & in(v1, all_0_13_13) = v3) | ( ~ (v3 = 0) & in(v0, all_0_13_13) = v3) | (( ~ (v2 = 0) | (v4 = 0 & ordered_pair(v0, v1) = v3 & in(v3, all_0_12_12) = 0)) & (v2 = 0 | ( ~ (v4 = 0) & ordered_pair(v0, v1) = v3 & in(v3, all_0_12_12) = v4))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (ordered_pair(v0, v1) = v2) | ? [v3] : ? [v4] : (( ~ (v3 = 0) & in(v1, all_0_13_13) = v3) | ( ~ (v3 = 0) & in(v0, all_0_13_13) = v3) | (((v4 = 0 & subset(v0, v1) = 0) | ( ~ (v3 = 0) & in(v2, all_0_12_12) = v3)) & ((v3 = 0 & in(v2, all_0_12_12) = 0) | ( ~ (v4 = 0) & subset(v0, v1) = v4))))) % 21.71/5.87 | % 21.71/5.87 | Applying alpha-rule on (177) yields: % 21.71/5.87 | (178) relation_field(all_0_12_12) = all_0_13_13 % 21.71/5.87 | (179) ! [v0] : ! [v1] : ! [v2] : ( ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : (( ~ (v3 = 0) & in(v1, all_0_13_13) = v3) | ( ~ (v3 = 0) & in(v0, all_0_13_13) = v3) | (( ~ (v2 = 0) | (v4 = 0 & ordered_pair(v0, v1) = v3 & in(v3, all_0_12_12) = 0)) & (v2 = 0 | ( ~ (v4 = 0) & ordered_pair(v0, v1) = v3 & in(v3, all_0_12_12) = v4))))) % 21.71/5.87 | (180) ! [v0] : ! [v1] : ! [v2] : ( ~ (ordered_pair(v0, v1) = v2) | ? [v3] : ? [v4] : (( ~ (v3 = 0) & in(v1, all_0_13_13) = v3) | ( ~ (v3 = 0) & in(v0, all_0_13_13) = v3) | (((v4 = 0 & subset(v0, v1) = 0) | ( ~ (v3 = 0) & in(v2, all_0_12_12) = v3)) & ((v3 = 0 & in(v2, all_0_12_12) = 0) | ( ~ (v4 = 0) & subset(v0, v1) = v4))))) % 21.71/5.87 | % 21.71/5.87 | Instantiating formula (65) with all_0_12_12 and discharging atoms relation(all_0_12_12) = 0, yields: % 21.71/5.87 | (181) ? [v0] : ? [v1] : ? [v2] : (relation_dom(all_0_12_12) = v1 & relation_rng(all_0_12_12) = v2 & relation_field(all_0_12_12) = v0 & set_union2(v1, v2) = v0) % 21.71/5.87 | % 21.71/5.87 | Instantiating (181) with all_108_0_158, all_108_1_159, all_108_2_160 yields: % 21.71/5.87 | (182) relation_dom(all_0_12_12) = all_108_1_159 & relation_rng(all_0_12_12) = all_108_0_158 & relation_field(all_0_12_12) = all_108_2_160 & set_union2(all_108_1_159, all_108_0_158) = all_108_2_160 % 21.71/5.87 | % 21.71/5.87 | Applying alpha-rule on (182) yields: % 21.71/5.87 | (183) relation_dom(all_0_12_12) = all_108_1_159 % 21.71/5.87 | (184) relation_rng(all_0_12_12) = all_108_0_158 % 21.71/5.87 | (185) relation_field(all_0_12_12) = all_108_2_160 % 21.71/5.87 | (186) set_union2(all_108_1_159, all_108_0_158) = all_108_2_160 % 21.71/5.87 | % 21.71/5.87 +-Applying beta-rule and splitting (175), into two cases. % 21.71/5.87 |-Branch one: % 21.71/5.87 | (187) all_73_1_102 = all_0_13_13 % 21.71/5.87 | % 21.71/5.87 | From (187) and (173) follows: % 21.71/5.87 | (178) relation_field(all_0_12_12) = all_0_13_13 % 21.71/5.87 | % 21.71/5.87 +-Applying beta-rule and splitting (176), into two cases. % 21.71/5.87 |-Branch one: % 21.71/5.87 | (189) all_73_0_101 = 0 % 21.71/5.87 | % 21.71/5.87 | Equations (189) can reduce 172 to: % 21.71/5.87 | (164) $false % 21.71/5.87 | % 21.71/5.87 |-The branch is then unsatisfiable % 21.71/5.87 |-Branch two: % 21.71/5.87 | (172) ~ (all_73_0_101 = 0) % 21.71/5.87 | (192) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = 0) & ordered_pair(v1, v2) = v4 & ordered_pair(v0, v2) = v5 & ordered_pair(v0, v1) = v3 & in(v5, all_0_12_12) = v6 & in(v4, all_0_12_12) = 0 & in(v3, all_0_12_12) = 0 & in(v2, all_73_1_102) = 0 & in(v1, all_73_1_102) = 0 & in(v0, all_73_1_102) = 0) % 21.71/5.87 | % 21.71/5.87 | Instantiating (192) with all_126_0_176, all_126_1_177, all_126_2_178, all_126_3_179, all_126_4_180, all_126_5_181, all_126_6_182 yields: % 21.71/5.87 | (193) ~ (all_126_0_176 = 0) & ordered_pair(all_126_5_181, all_126_4_180) = all_126_2_178 & ordered_pair(all_126_6_182, all_126_4_180) = all_126_1_177 & ordered_pair(all_126_6_182, all_126_5_181) = all_126_3_179 & in(all_126_1_177, all_0_12_12) = all_126_0_176 & in(all_126_2_178, all_0_12_12) = 0 & in(all_126_3_179, all_0_12_12) = 0 & in(all_126_4_180, all_73_1_102) = 0 & in(all_126_5_181, all_73_1_102) = 0 & in(all_126_6_182, all_73_1_102) = 0 % 21.71/5.87 | % 21.71/5.87 | Applying alpha-rule on (193) yields: % 21.71/5.87 | (194) in(all_126_1_177, all_0_12_12) = all_126_0_176 % 21.71/5.87 | (195) in(all_126_3_179, all_0_12_12) = 0 % 21.71/5.87 | (196) ordered_pair(all_126_6_182, all_126_4_180) = all_126_1_177 % 21.71/5.87 | (197) in(all_126_2_178, all_0_12_12) = 0 % 21.71/5.87 | (198) in(all_126_6_182, all_73_1_102) = 0 % 21.71/5.87 | (199) in(all_126_4_180, all_73_1_102) = 0 % 21.71/5.87 | (200) ~ (all_126_0_176 = 0) % 21.71/5.87 | (201) ordered_pair(all_126_5_181, all_126_4_180) = all_126_2_178 % 21.71/5.87 | (202) in(all_126_5_181, all_73_1_102) = 0 % 21.71/5.87 | (203) ordered_pair(all_126_6_182, all_126_5_181) = all_126_3_179 % 21.71/5.87 | % 21.71/5.87 | From (187) and (199) follows: % 21.71/5.87 | (204) in(all_126_4_180, all_0_13_13) = 0 % 21.71/5.87 | % 21.71/5.87 | From (187) and (202) follows: % 21.71/5.87 | (205) in(all_126_5_181, all_0_13_13) = 0 % 21.71/5.87 | % 21.71/5.87 | From (187) and (198) follows: % 21.71/5.87 | (206) in(all_126_6_182, all_0_13_13) = 0 % 21.71/5.87 | % 21.71/5.87 | Instantiating formula (91) with all_0_12_12, all_0_13_13, all_108_2_160 and discharging atoms relation_field(all_0_12_12) = all_108_2_160, relation_field(all_0_12_12) = all_0_13_13, yields: % 21.71/5.87 | (207) all_108_2_160 = all_0_13_13 % 21.71/5.87 | % 21.71/5.87 | From (207) and (185) follows: % 21.71/5.87 | (178) relation_field(all_0_12_12) = all_0_13_13 % 21.71/5.87 | % 21.71/5.87 | Instantiating formula (180) with all_126_2_178, all_126_4_180, all_126_5_181 and discharging atoms ordered_pair(all_126_5_181, all_126_4_180) = all_126_2_178, yields: % 21.71/5.87 | (209) ? [v0] : ? [v1] : (( ~ (v0 = 0) & in(all_126_4_180, all_0_13_13) = v0) | ( ~ (v0 = 0) & in(all_126_5_181, all_0_13_13) = v0) | (((v1 = 0 & subset(all_126_5_181, all_126_4_180) = 0) | ( ~ (v0 = 0) & in(all_126_2_178, all_0_12_12) = v0)) & ((v0 = 0 & in(all_126_2_178, all_0_12_12) = 0) | ( ~ (v1 = 0) & subset(all_126_5_181, all_126_4_180) = v1)))) % 21.71/5.87 | % 21.71/5.87 | Instantiating formula (180) with all_126_1_177, all_126_4_180, all_126_6_182 and discharging atoms ordered_pair(all_126_6_182, all_126_4_180) = all_126_1_177, yields: % 21.71/5.87 | (210) ? [v0] : ? [v1] : (( ~ (v0 = 0) & in(all_126_4_180, all_0_13_13) = v0) | ( ~ (v0 = 0) & in(all_126_6_182, all_0_13_13) = v0) | (((v1 = 0 & subset(all_126_6_182, all_126_4_180) = 0) | ( ~ (v0 = 0) & in(all_126_1_177, all_0_12_12) = v0)) & ((v0 = 0 & in(all_126_1_177, all_0_12_12) = 0) | ( ~ (v1 = 0) & subset(all_126_6_182, all_126_4_180) = v1)))) % 21.71/5.87 | % 21.71/5.87 | Instantiating formula (180) with all_126_3_179, all_126_5_181, all_126_6_182 and discharging atoms ordered_pair(all_126_6_182, all_126_5_181) = all_126_3_179, yields: % 21.71/5.87 | (211) ? [v0] : ? [v1] : (( ~ (v0 = 0) & in(all_126_5_181, all_0_13_13) = v0) | ( ~ (v0 = 0) & in(all_126_6_182, all_0_13_13) = v0) | (((v1 = 0 & subset(all_126_6_182, all_126_5_181) = 0) | ( ~ (v0 = 0) & in(all_126_3_179, all_0_12_12) = v0)) & ((v0 = 0 & in(all_126_3_179, all_0_12_12) = 0) | ( ~ (v1 = 0) & subset(all_126_6_182, all_126_5_181) = v1)))) % 21.71/5.87 | % 21.71/5.87 | Instantiating formula (131) with all_126_2_178, all_126_4_180, all_126_5_181, all_0_13_13, all_0_12_12, all_0_13_13 and discharging atoms inclusion_relation(all_0_13_13) = all_0_12_12, ordered_pair(all_126_5_181, all_126_4_180) = all_126_2_178, relation_field(all_0_12_12) = all_0_13_13, yields: % 21.71/5.87 | (212) ? [v0] : ? [v1] : (( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & in(all_126_4_180, all_0_13_13) = v0) | ( ~ (v0 = 0) & in(all_126_5_181, all_0_13_13) = v0) | (((v1 = 0 & subset(all_126_5_181, all_126_4_180) = 0) | ( ~ (v0 = 0) & in(all_126_2_178, all_0_12_12) = v0)) & ((v0 = 0 & in(all_126_2_178, all_0_12_12) = 0) | ( ~ (v1 = 0) & subset(all_126_5_181, all_126_4_180) = v1)))) % 21.71/5.87 | % 21.71/5.87 | Instantiating formula (131) with all_126_1_177, all_126_4_180, all_126_6_182, all_0_13_13, all_0_12_12, all_0_13_13 and discharging atoms inclusion_relation(all_0_13_13) = all_0_12_12, ordered_pair(all_126_6_182, all_126_4_180) = all_126_1_177, relation_field(all_0_12_12) = all_0_13_13, yields: % 21.71/5.87 | (213) ? [v0] : ? [v1] : (( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & in(all_126_4_180, all_0_13_13) = v0) | ( ~ (v0 = 0) & in(all_126_6_182, all_0_13_13) = v0) | (((v1 = 0 & subset(all_126_6_182, all_126_4_180) = 0) | ( ~ (v0 = 0) & in(all_126_1_177, all_0_12_12) = v0)) & ((v0 = 0 & in(all_126_1_177, all_0_12_12) = 0) | ( ~ (v1 = 0) & subset(all_126_6_182, all_126_4_180) = v1)))) % 21.71/5.87 | % 21.71/5.87 | Instantiating formula (131) with all_126_3_179, all_126_5_181, all_126_6_182, all_0_13_13, all_0_12_12, all_0_13_13 and discharging atoms inclusion_relation(all_0_13_13) = all_0_12_12, ordered_pair(all_126_6_182, all_126_5_181) = all_126_3_179, relation_field(all_0_12_12) = all_0_13_13, yields: % 21.71/5.87 | (214) ? [v0] : ? [v1] : (( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & in(all_126_5_181, all_0_13_13) = v0) | ( ~ (v0 = 0) & in(all_126_6_182, all_0_13_13) = v0) | (((v1 = 0 & subset(all_126_6_182, all_126_5_181) = 0) | ( ~ (v0 = 0) & in(all_126_3_179, all_0_12_12) = v0)) & ((v0 = 0 & in(all_126_3_179, all_0_12_12) = 0) | ( ~ (v1 = 0) & subset(all_126_6_182, all_126_5_181) = v1)))) % 21.71/5.87 | % 21.71/5.87 | Instantiating formula (15) with all_126_0_176, all_0_12_12, all_126_1_177 and discharging atoms in(all_126_1_177, all_0_12_12) = all_126_0_176, yields: % 21.71/5.87 | (215) all_126_0_176 = 0 | ? [v0] : ((v0 = 0 & empty(all_0_12_12) = 0) | ( ~ (v0 = 0) & element(all_126_1_177, all_0_12_12) = v0)) % 21.71/5.87 | % 21.71/5.87 | Instantiating (214) with all_159_0_195, all_159_1_196 yields: % 21.71/5.87 | (216) ( ~ (all_159_1_196 = 0) & relation(all_0_12_12) = all_159_1_196) | ( ~ (all_159_1_196 = 0) & in(all_126_5_181, all_0_13_13) = all_159_1_196) | ( ~ (all_159_1_196 = 0) & in(all_126_6_182, all_0_13_13) = all_159_1_196) | (((all_159_0_195 = 0 & subset(all_126_6_182, all_126_5_181) = 0) | ( ~ (all_159_1_196 = 0) & in(all_126_3_179, all_0_12_12) = all_159_1_196)) & ((all_159_1_196 = 0 & in(all_126_3_179, all_0_12_12) = 0) | ( ~ (all_159_0_195 = 0) & subset(all_126_6_182, all_126_5_181) = all_159_0_195))) % 21.71/5.87 | % 21.71/5.87 | Instantiating (213) with all_160_0_197, all_160_1_198 yields: % 21.71/5.87 | (217) ( ~ (all_160_1_198 = 0) & relation(all_0_12_12) = all_160_1_198) | ( ~ (all_160_1_198 = 0) & in(all_126_4_180, all_0_13_13) = all_160_1_198) | ( ~ (all_160_1_198 = 0) & in(all_126_6_182, all_0_13_13) = all_160_1_198) | (((all_160_0_197 = 0 & subset(all_126_6_182, all_126_4_180) = 0) | ( ~ (all_160_1_198 = 0) & in(all_126_1_177, all_0_12_12) = all_160_1_198)) & ((all_160_1_198 = 0 & in(all_126_1_177, all_0_12_12) = 0) | ( ~ (all_160_0_197 = 0) & subset(all_126_6_182, all_126_4_180) = all_160_0_197))) % 21.71/5.87 | % 21.71/5.87 | Instantiating (212) with all_163_0_200, all_163_1_201 yields: % 21.71/5.87 | (218) ( ~ (all_163_1_201 = 0) & relation(all_0_12_12) = all_163_1_201) | ( ~ (all_163_1_201 = 0) & in(all_126_4_180, all_0_13_13) = all_163_1_201) | ( ~ (all_163_1_201 = 0) & in(all_126_5_181, all_0_13_13) = all_163_1_201) | (((all_163_0_200 = 0 & subset(all_126_5_181, all_126_4_180) = 0) | ( ~ (all_163_1_201 = 0) & in(all_126_2_178, all_0_12_12) = all_163_1_201)) & ((all_163_1_201 = 0 & in(all_126_2_178, all_0_12_12) = 0) | ( ~ (all_163_0_200 = 0) & subset(all_126_5_181, all_126_4_180) = all_163_0_200))) % 21.71/5.88 | % 21.71/5.88 | Instantiating (211) with all_171_0_207, all_171_1_208 yields: % 21.71/5.88 | (219) ( ~ (all_171_1_208 = 0) & in(all_126_5_181, all_0_13_13) = all_171_1_208) | ( ~ (all_171_1_208 = 0) & in(all_126_6_182, all_0_13_13) = all_171_1_208) | (((all_171_0_207 = 0 & subset(all_126_6_182, all_126_5_181) = 0) | ( ~ (all_171_1_208 = 0) & in(all_126_3_179, all_0_12_12) = all_171_1_208)) & ((all_171_1_208 = 0 & in(all_126_3_179, all_0_12_12) = 0) | ( ~ (all_171_0_207 = 0) & subset(all_126_6_182, all_126_5_181) = all_171_0_207))) % 21.71/5.88 | % 21.71/5.88 | Instantiating (210) with all_178_0_214, all_178_1_215 yields: % 21.71/5.88 | (220) ( ~ (all_178_1_215 = 0) & in(all_126_4_180, all_0_13_13) = all_178_1_215) | ( ~ (all_178_1_215 = 0) & in(all_126_6_182, all_0_13_13) = all_178_1_215) | (((all_178_0_214 = 0 & subset(all_126_6_182, all_126_4_180) = 0) | ( ~ (all_178_1_215 = 0) & in(all_126_1_177, all_0_12_12) = all_178_1_215)) & ((all_178_1_215 = 0 & in(all_126_1_177, all_0_12_12) = 0) | ( ~ (all_178_0_214 = 0) & subset(all_126_6_182, all_126_4_180) = all_178_0_214))) % 22.19/5.88 | % 22.19/5.88 | Instantiating (209) with all_183_0_220, all_183_1_221 yields: % 22.19/5.88 | (221) ( ~ (all_183_1_221 = 0) & in(all_126_4_180, all_0_13_13) = all_183_1_221) | ( ~ (all_183_1_221 = 0) & in(all_126_5_181, all_0_13_13) = all_183_1_221) | (((all_183_0_220 = 0 & subset(all_126_5_181, all_126_4_180) = 0) | ( ~ (all_183_1_221 = 0) & in(all_126_2_178, all_0_12_12) = all_183_1_221)) & ((all_183_1_221 = 0 & in(all_126_2_178, all_0_12_12) = 0) | ( ~ (all_183_0_220 = 0) & subset(all_126_5_181, all_126_4_180) = all_183_0_220))) % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (219), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.88 | (222) ( ~ (all_171_1_208 = 0) & in(all_126_5_181, all_0_13_13) = all_171_1_208) | ( ~ (all_171_1_208 = 0) & in(all_126_6_182, all_0_13_13) = all_171_1_208) % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (222), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.88 | (223) ~ (all_171_1_208 = 0) & in(all_126_5_181, all_0_13_13) = all_171_1_208 % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (223) yields: % 22.19/5.88 | (224) ~ (all_171_1_208 = 0) % 22.19/5.88 | (225) in(all_126_5_181, all_0_13_13) = all_171_1_208 % 22.19/5.88 | % 22.19/5.88 | Instantiating formula (27) with all_126_5_181, all_0_13_13, all_171_1_208, 0 and discharging atoms in(all_126_5_181, all_0_13_13) = all_171_1_208, in(all_126_5_181, all_0_13_13) = 0, yields: % 22.19/5.88 | (226) all_171_1_208 = 0 % 22.19/5.88 | % 22.19/5.88 | Equations (226) can reduce 224 to: % 22.19/5.88 | (164) $false % 22.19/5.88 | % 22.19/5.88 |-The branch is then unsatisfiable % 22.19/5.88 |-Branch two: % 22.19/5.88 | (228) ~ (all_171_1_208 = 0) & in(all_126_6_182, all_0_13_13) = all_171_1_208 % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (228) yields: % 22.19/5.88 | (224) ~ (all_171_1_208 = 0) % 22.19/5.88 | (230) in(all_126_6_182, all_0_13_13) = all_171_1_208 % 22.19/5.88 | % 22.19/5.88 | Instantiating formula (27) with all_126_6_182, all_0_13_13, all_171_1_208, 0 and discharging atoms in(all_126_6_182, all_0_13_13) = all_171_1_208, in(all_126_6_182, all_0_13_13) = 0, yields: % 22.19/5.88 | (226) all_171_1_208 = 0 % 22.19/5.88 | % 22.19/5.88 | Equations (226) can reduce 224 to: % 22.19/5.88 | (164) $false % 22.19/5.88 | % 22.19/5.88 |-The branch is then unsatisfiable % 22.19/5.88 |-Branch two: % 22.19/5.88 | (233) ((all_171_0_207 = 0 & subset(all_126_6_182, all_126_5_181) = 0) | ( ~ (all_171_1_208 = 0) & in(all_126_3_179, all_0_12_12) = all_171_1_208)) & ((all_171_1_208 = 0 & in(all_126_3_179, all_0_12_12) = 0) | ( ~ (all_171_0_207 = 0) & subset(all_126_6_182, all_126_5_181) = all_171_0_207)) % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (233) yields: % 22.19/5.88 | (234) (all_171_0_207 = 0 & subset(all_126_6_182, all_126_5_181) = 0) | ( ~ (all_171_1_208 = 0) & in(all_126_3_179, all_0_12_12) = all_171_1_208) % 22.19/5.88 | (235) (all_171_1_208 = 0 & in(all_126_3_179, all_0_12_12) = 0) | ( ~ (all_171_0_207 = 0) & subset(all_126_6_182, all_126_5_181) = all_171_0_207) % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (221), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.88 | (236) ( ~ (all_183_1_221 = 0) & in(all_126_4_180, all_0_13_13) = all_183_1_221) | ( ~ (all_183_1_221 = 0) & in(all_126_5_181, all_0_13_13) = all_183_1_221) % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (236), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.88 | (237) ~ (all_183_1_221 = 0) & in(all_126_4_180, all_0_13_13) = all_183_1_221 % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (237) yields: % 22.19/5.88 | (238) ~ (all_183_1_221 = 0) % 22.19/5.88 | (239) in(all_126_4_180, all_0_13_13) = all_183_1_221 % 22.19/5.88 | % 22.19/5.88 | Instantiating formula (27) with all_126_4_180, all_0_13_13, all_183_1_221, 0 and discharging atoms in(all_126_4_180, all_0_13_13) = all_183_1_221, in(all_126_4_180, all_0_13_13) = 0, yields: % 22.19/5.88 | (240) all_183_1_221 = 0 % 22.19/5.88 | % 22.19/5.88 | Equations (240) can reduce 238 to: % 22.19/5.88 | (164) $false % 22.19/5.88 | % 22.19/5.88 |-The branch is then unsatisfiable % 22.19/5.88 |-Branch two: % 22.19/5.88 | (242) ~ (all_183_1_221 = 0) & in(all_126_5_181, all_0_13_13) = all_183_1_221 % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (242) yields: % 22.19/5.88 | (238) ~ (all_183_1_221 = 0) % 22.19/5.88 | (244) in(all_126_5_181, all_0_13_13) = all_183_1_221 % 22.19/5.88 | % 22.19/5.88 | Instantiating formula (27) with all_126_5_181, all_0_13_13, all_183_1_221, 0 and discharging atoms in(all_126_5_181, all_0_13_13) = all_183_1_221, in(all_126_5_181, all_0_13_13) = 0, yields: % 22.19/5.88 | (240) all_183_1_221 = 0 % 22.19/5.88 | % 22.19/5.88 | Equations (240) can reduce 238 to: % 22.19/5.88 | (164) $false % 22.19/5.88 | % 22.19/5.88 |-The branch is then unsatisfiable % 22.19/5.88 |-Branch two: % 22.19/5.88 | (247) ((all_183_0_220 = 0 & subset(all_126_5_181, all_126_4_180) = 0) | ( ~ (all_183_1_221 = 0) & in(all_126_2_178, all_0_12_12) = all_183_1_221)) & ((all_183_1_221 = 0 & in(all_126_2_178, all_0_12_12) = 0) | ( ~ (all_183_0_220 = 0) & subset(all_126_5_181, all_126_4_180) = all_183_0_220)) % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (247) yields: % 22.19/5.88 | (248) (all_183_0_220 = 0 & subset(all_126_5_181, all_126_4_180) = 0) | ( ~ (all_183_1_221 = 0) & in(all_126_2_178, all_0_12_12) = all_183_1_221) % 22.19/5.88 | (249) (all_183_1_221 = 0 & in(all_126_2_178, all_0_12_12) = 0) | ( ~ (all_183_0_220 = 0) & subset(all_126_5_181, all_126_4_180) = all_183_0_220) % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (220), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.88 | (250) ( ~ (all_178_1_215 = 0) & in(all_126_4_180, all_0_13_13) = all_178_1_215) | ( ~ (all_178_1_215 = 0) & in(all_126_6_182, all_0_13_13) = all_178_1_215) % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (250), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.88 | (251) ~ (all_178_1_215 = 0) & in(all_126_4_180, all_0_13_13) = all_178_1_215 % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (251) yields: % 22.19/5.88 | (252) ~ (all_178_1_215 = 0) % 22.19/5.88 | (253) in(all_126_4_180, all_0_13_13) = all_178_1_215 % 22.19/5.88 | % 22.19/5.88 | Instantiating formula (27) with all_126_4_180, all_0_13_13, all_178_1_215, 0 and discharging atoms in(all_126_4_180, all_0_13_13) = all_178_1_215, in(all_126_4_180, all_0_13_13) = 0, yields: % 22.19/5.88 | (254) all_178_1_215 = 0 % 22.19/5.88 | % 22.19/5.88 | Equations (254) can reduce 252 to: % 22.19/5.88 | (164) $false % 22.19/5.88 | % 22.19/5.88 |-The branch is then unsatisfiable % 22.19/5.88 |-Branch two: % 22.19/5.88 | (256) ~ (all_178_1_215 = 0) & in(all_126_6_182, all_0_13_13) = all_178_1_215 % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (256) yields: % 22.19/5.88 | (252) ~ (all_178_1_215 = 0) % 22.19/5.88 | (258) in(all_126_6_182, all_0_13_13) = all_178_1_215 % 22.19/5.88 | % 22.19/5.88 | Instantiating formula (27) with all_126_6_182, all_0_13_13, all_178_1_215, 0 and discharging atoms in(all_126_6_182, all_0_13_13) = all_178_1_215, in(all_126_6_182, all_0_13_13) = 0, yields: % 22.19/5.88 | (254) all_178_1_215 = 0 % 22.19/5.88 | % 22.19/5.88 | Equations (254) can reduce 252 to: % 22.19/5.88 | (164) $false % 22.19/5.88 | % 22.19/5.88 |-The branch is then unsatisfiable % 22.19/5.88 |-Branch two: % 22.19/5.88 | (261) ((all_178_0_214 = 0 & subset(all_126_6_182, all_126_4_180) = 0) | ( ~ (all_178_1_215 = 0) & in(all_126_1_177, all_0_12_12) = all_178_1_215)) & ((all_178_1_215 = 0 & in(all_126_1_177, all_0_12_12) = 0) | ( ~ (all_178_0_214 = 0) & subset(all_126_6_182, all_126_4_180) = all_178_0_214)) % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (261) yields: % 22.19/5.88 | (262) (all_178_0_214 = 0 & subset(all_126_6_182, all_126_4_180) = 0) | ( ~ (all_178_1_215 = 0) & in(all_126_1_177, all_0_12_12) = all_178_1_215) % 22.19/5.88 | (263) (all_178_1_215 = 0 & in(all_126_1_177, all_0_12_12) = 0) | ( ~ (all_178_0_214 = 0) & subset(all_126_6_182, all_126_4_180) = all_178_0_214) % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (263), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.88 | (264) all_178_1_215 = 0 & in(all_126_1_177, all_0_12_12) = 0 % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (264) yields: % 22.19/5.88 | (254) all_178_1_215 = 0 % 22.19/5.88 | (266) in(all_126_1_177, all_0_12_12) = 0 % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (215), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.88 | (267) all_126_0_176 = 0 % 22.19/5.88 | % 22.19/5.88 | Equations (267) can reduce 200 to: % 22.19/5.88 | (164) $false % 22.19/5.88 | % 22.19/5.88 |-The branch is then unsatisfiable % 22.19/5.88 |-Branch two: % 22.19/5.88 | (200) ~ (all_126_0_176 = 0) % 22.19/5.88 | (270) ? [v0] : ((v0 = 0 & empty(all_0_12_12) = 0) | ( ~ (v0 = 0) & element(all_126_1_177, all_0_12_12) = v0)) % 22.19/5.88 | % 22.19/5.88 | Instantiating formula (27) with all_126_1_177, all_0_12_12, 0, all_126_0_176 and discharging atoms in(all_126_1_177, all_0_12_12) = all_126_0_176, in(all_126_1_177, all_0_12_12) = 0, yields: % 22.19/5.88 | (267) all_126_0_176 = 0 % 22.19/5.88 | % 22.19/5.88 | Equations (267) can reduce 200 to: % 22.19/5.88 | (164) $false % 22.19/5.88 | % 22.19/5.88 |-The branch is then unsatisfiable % 22.19/5.88 |-Branch two: % 22.19/5.88 | (273) ~ (all_178_0_214 = 0) & subset(all_126_6_182, all_126_4_180) = all_178_0_214 % 22.19/5.88 | % 22.19/5.88 | Applying alpha-rule on (273) yields: % 22.19/5.88 | (274) ~ (all_178_0_214 = 0) % 22.19/5.88 | (275) subset(all_126_6_182, all_126_4_180) = all_178_0_214 % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (217), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.88 | (276) ( ~ (all_160_1_198 = 0) & relation(all_0_12_12) = all_160_1_198) | ( ~ (all_160_1_198 = 0) & in(all_126_4_180, all_0_13_13) = all_160_1_198) | ( ~ (all_160_1_198 = 0) & in(all_126_6_182, all_0_13_13) = all_160_1_198) % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (276), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.88 | (277) ( ~ (all_160_1_198 = 0) & relation(all_0_12_12) = all_160_1_198) | ( ~ (all_160_1_198 = 0) & in(all_126_4_180, all_0_13_13) = all_160_1_198) % 22.19/5.88 | % 22.19/5.88 +-Applying beta-rule and splitting (277), into two cases. % 22.19/5.88 |-Branch one: % 22.19/5.89 | (278) ~ (all_160_1_198 = 0) & relation(all_0_12_12) = all_160_1_198 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (278) yields: % 22.19/5.89 | (279) ~ (all_160_1_198 = 0) % 22.19/5.89 | (280) relation(all_0_12_12) = all_160_1_198 % 22.19/5.89 | % 22.19/5.89 | Instantiating formula (68) with all_0_12_12, all_160_1_198, 0 and discharging atoms relation(all_0_12_12) = all_160_1_198, relation(all_0_12_12) = 0, yields: % 22.19/5.89 | (281) all_160_1_198 = 0 % 22.19/5.89 | % 22.19/5.89 | Equations (281) can reduce 279 to: % 22.19/5.89 | (164) $false % 22.19/5.89 | % 22.19/5.89 |-The branch is then unsatisfiable % 22.19/5.89 |-Branch two: % 22.19/5.89 | (283) ~ (all_160_1_198 = 0) & in(all_126_4_180, all_0_13_13) = all_160_1_198 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (283) yields: % 22.19/5.89 | (279) ~ (all_160_1_198 = 0) % 22.19/5.89 | (285) in(all_126_4_180, all_0_13_13) = all_160_1_198 % 22.19/5.89 | % 22.19/5.89 | Instantiating formula (27) with all_126_4_180, all_0_13_13, all_160_1_198, 0 and discharging atoms in(all_126_4_180, all_0_13_13) = all_160_1_198, in(all_126_4_180, all_0_13_13) = 0, yields: % 22.19/5.89 | (281) all_160_1_198 = 0 % 22.19/5.89 | % 22.19/5.89 | Equations (281) can reduce 279 to: % 22.19/5.89 | (164) $false % 22.19/5.89 | % 22.19/5.89 |-The branch is then unsatisfiable % 22.19/5.89 |-Branch two: % 22.19/5.89 | (288) ~ (all_160_1_198 = 0) & in(all_126_6_182, all_0_13_13) = all_160_1_198 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (288) yields: % 22.19/5.89 | (279) ~ (all_160_1_198 = 0) % 22.19/5.89 | (290) in(all_126_6_182, all_0_13_13) = all_160_1_198 % 22.19/5.89 | % 22.19/5.89 | Instantiating formula (27) with all_126_6_182, all_0_13_13, all_160_1_198, 0 and discharging atoms in(all_126_6_182, all_0_13_13) = all_160_1_198, in(all_126_6_182, all_0_13_13) = 0, yields: % 22.19/5.89 | (281) all_160_1_198 = 0 % 22.19/5.89 | % 22.19/5.89 | Equations (281) can reduce 279 to: % 22.19/5.89 | (164) $false % 22.19/5.89 | % 22.19/5.89 |-The branch is then unsatisfiable % 22.19/5.89 |-Branch two: % 22.19/5.89 | (293) ((all_160_0_197 = 0 & subset(all_126_6_182, all_126_4_180) = 0) | ( ~ (all_160_1_198 = 0) & in(all_126_1_177, all_0_12_12) = all_160_1_198)) & ((all_160_1_198 = 0 & in(all_126_1_177, all_0_12_12) = 0) | ( ~ (all_160_0_197 = 0) & subset(all_126_6_182, all_126_4_180) = all_160_0_197)) % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (293) yields: % 22.19/5.89 | (294) (all_160_0_197 = 0 & subset(all_126_6_182, all_126_4_180) = 0) | ( ~ (all_160_1_198 = 0) & in(all_126_1_177, all_0_12_12) = all_160_1_198) % 22.19/5.89 | (295) (all_160_1_198 = 0 & in(all_126_1_177, all_0_12_12) = 0) | ( ~ (all_160_0_197 = 0) & subset(all_126_6_182, all_126_4_180) = all_160_0_197) % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (215), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (267) all_126_0_176 = 0 % 22.19/5.89 | % 22.19/5.89 | Equations (267) can reduce 200 to: % 22.19/5.89 | (164) $false % 22.19/5.89 | % 22.19/5.89 |-The branch is then unsatisfiable % 22.19/5.89 |-Branch two: % 22.19/5.89 | (200) ~ (all_126_0_176 = 0) % 22.19/5.89 | (270) ? [v0] : ((v0 = 0 & empty(all_0_12_12) = 0) | ( ~ (v0 = 0) & element(all_126_1_177, all_0_12_12) = v0)) % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (295), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (300) all_160_1_198 = 0 & in(all_126_1_177, all_0_12_12) = 0 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (300) yields: % 22.19/5.89 | (281) all_160_1_198 = 0 % 22.19/5.89 | (266) in(all_126_1_177, all_0_12_12) = 0 % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (262), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (303) all_178_0_214 = 0 & subset(all_126_6_182, all_126_4_180) = 0 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (303) yields: % 22.19/5.89 | (304) all_178_0_214 = 0 % 22.19/5.89 | (305) subset(all_126_6_182, all_126_4_180) = 0 % 22.19/5.89 | % 22.19/5.89 | Equations (304) can reduce 274 to: % 22.19/5.89 | (164) $false % 22.19/5.89 | % 22.19/5.89 |-The branch is then unsatisfiable % 22.19/5.89 |-Branch two: % 22.19/5.89 | (307) ~ (all_178_1_215 = 0) & in(all_126_1_177, all_0_12_12) = all_178_1_215 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (307) yields: % 22.19/5.89 | (252) ~ (all_178_1_215 = 0) % 22.19/5.89 | (309) in(all_126_1_177, all_0_12_12) = all_178_1_215 % 22.19/5.89 | % 22.19/5.89 | Instantiating formula (27) with all_126_1_177, all_0_12_12, all_178_1_215, all_126_0_176 and discharging atoms in(all_126_1_177, all_0_12_12) = all_178_1_215, in(all_126_1_177, all_0_12_12) = all_126_0_176, yields: % 22.19/5.89 | (310) all_178_1_215 = all_126_0_176 % 22.19/5.89 | % 22.19/5.89 | Instantiating formula (27) with all_126_1_177, all_0_12_12, 0, all_178_1_215 and discharging atoms in(all_126_1_177, all_0_12_12) = all_178_1_215, in(all_126_1_177, all_0_12_12) = 0, yields: % 22.19/5.89 | (254) all_178_1_215 = 0 % 22.19/5.89 | % 22.19/5.89 | Combining equations (310,254) yields a new equation: % 22.19/5.89 | (312) all_126_0_176 = 0 % 22.19/5.89 | % 22.19/5.89 | Simplifying 312 yields: % 22.19/5.89 | (267) all_126_0_176 = 0 % 22.19/5.89 | % 22.19/5.89 | Equations (267) can reduce 200 to: % 22.19/5.89 | (164) $false % 22.19/5.89 | % 22.19/5.89 |-The branch is then unsatisfiable % 22.19/5.89 |-Branch two: % 22.19/5.89 | (315) ~ (all_160_0_197 = 0) & subset(all_126_6_182, all_126_4_180) = all_160_0_197 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (315) yields: % 22.19/5.89 | (316) ~ (all_160_0_197 = 0) % 22.19/5.89 | (317) subset(all_126_6_182, all_126_4_180) = all_160_0_197 % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (248), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (318) all_183_0_220 = 0 & subset(all_126_5_181, all_126_4_180) = 0 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (318) yields: % 22.19/5.89 | (319) all_183_0_220 = 0 % 22.19/5.89 | (320) subset(all_126_5_181, all_126_4_180) = 0 % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (249), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (321) all_183_1_221 = 0 & in(all_126_2_178, all_0_12_12) = 0 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (321) yields: % 22.19/5.89 | (240) all_183_1_221 = 0 % 22.19/5.89 | (197) in(all_126_2_178, all_0_12_12) = 0 % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (216), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (324) ( ~ (all_159_1_196 = 0) & relation(all_0_12_12) = all_159_1_196) | ( ~ (all_159_1_196 = 0) & in(all_126_5_181, all_0_13_13) = all_159_1_196) | ( ~ (all_159_1_196 = 0) & in(all_126_6_182, all_0_13_13) = all_159_1_196) % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (324), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (325) ( ~ (all_159_1_196 = 0) & relation(all_0_12_12) = all_159_1_196) | ( ~ (all_159_1_196 = 0) & in(all_126_5_181, all_0_13_13) = all_159_1_196) % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (325), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (326) ~ (all_159_1_196 = 0) & relation(all_0_12_12) = all_159_1_196 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (326) yields: % 22.19/5.89 | (327) ~ (all_159_1_196 = 0) % 22.19/5.89 | (328) relation(all_0_12_12) = all_159_1_196 % 22.19/5.89 | % 22.19/5.89 | Instantiating formula (68) with all_0_12_12, all_159_1_196, 0 and discharging atoms relation(all_0_12_12) = all_159_1_196, relation(all_0_12_12) = 0, yields: % 22.19/5.89 | (329) all_159_1_196 = 0 % 22.19/5.89 | % 22.19/5.89 | Equations (329) can reduce 327 to: % 22.19/5.89 | (164) $false % 22.19/5.89 | % 22.19/5.89 |-The branch is then unsatisfiable % 22.19/5.89 |-Branch two: % 22.19/5.89 | (331) ~ (all_159_1_196 = 0) & in(all_126_5_181, all_0_13_13) = all_159_1_196 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (331) yields: % 22.19/5.89 | (327) ~ (all_159_1_196 = 0) % 22.19/5.89 | (333) in(all_126_5_181, all_0_13_13) = all_159_1_196 % 22.19/5.89 | % 22.19/5.89 | Instantiating formula (27) with all_126_5_181, all_0_13_13, all_159_1_196, 0 and discharging atoms in(all_126_5_181, all_0_13_13) = all_159_1_196, in(all_126_5_181, all_0_13_13) = 0, yields: % 22.19/5.89 | (329) all_159_1_196 = 0 % 22.19/5.89 | % 22.19/5.89 | Equations (329) can reduce 327 to: % 22.19/5.89 | (164) $false % 22.19/5.89 | % 22.19/5.89 |-The branch is then unsatisfiable % 22.19/5.89 |-Branch two: % 22.19/5.89 | (336) ~ (all_159_1_196 = 0) & in(all_126_6_182, all_0_13_13) = all_159_1_196 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (336) yields: % 22.19/5.89 | (327) ~ (all_159_1_196 = 0) % 22.19/5.89 | (338) in(all_126_6_182, all_0_13_13) = all_159_1_196 % 22.19/5.89 | % 22.19/5.89 | Instantiating formula (27) with all_126_6_182, all_0_13_13, all_159_1_196, 0 and discharging atoms in(all_126_6_182, all_0_13_13) = all_159_1_196, in(all_126_6_182, all_0_13_13) = 0, yields: % 22.19/5.89 | (329) all_159_1_196 = 0 % 22.19/5.89 | % 22.19/5.89 | Equations (329) can reduce 327 to: % 22.19/5.89 | (164) $false % 22.19/5.89 | % 22.19/5.89 |-The branch is then unsatisfiable % 22.19/5.89 |-Branch two: % 22.19/5.89 | (341) ((all_159_0_195 = 0 & subset(all_126_6_182, all_126_5_181) = 0) | ( ~ (all_159_1_196 = 0) & in(all_126_3_179, all_0_12_12) = all_159_1_196)) & ((all_159_1_196 = 0 & in(all_126_3_179, all_0_12_12) = 0) | ( ~ (all_159_0_195 = 0) & subset(all_126_6_182, all_126_5_181) = all_159_0_195)) % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (341) yields: % 22.19/5.89 | (342) (all_159_0_195 = 0 & subset(all_126_6_182, all_126_5_181) = 0) | ( ~ (all_159_1_196 = 0) & in(all_126_3_179, all_0_12_12) = all_159_1_196) % 22.19/5.89 | (343) (all_159_1_196 = 0 & in(all_126_3_179, all_0_12_12) = 0) | ( ~ (all_159_0_195 = 0) & subset(all_126_6_182, all_126_5_181) = all_159_0_195) % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (342), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (344) all_159_0_195 = 0 & subset(all_126_6_182, all_126_5_181) = 0 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (344) yields: % 22.19/5.89 | (345) all_159_0_195 = 0 % 22.19/5.89 | (346) subset(all_126_6_182, all_126_5_181) = 0 % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (343), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (347) all_159_1_196 = 0 & in(all_126_3_179, all_0_12_12) = 0 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (347) yields: % 22.19/5.89 | (329) all_159_1_196 = 0 % 22.19/5.89 | (195) in(all_126_3_179, all_0_12_12) = 0 % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (218), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (350) ( ~ (all_163_1_201 = 0) & relation(all_0_12_12) = all_163_1_201) | ( ~ (all_163_1_201 = 0) & in(all_126_4_180, all_0_13_13) = all_163_1_201) | ( ~ (all_163_1_201 = 0) & in(all_126_5_181, all_0_13_13) = all_163_1_201) % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (350), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (351) ( ~ (all_163_1_201 = 0) & relation(all_0_12_12) = all_163_1_201) | ( ~ (all_163_1_201 = 0) & in(all_126_4_180, all_0_13_13) = all_163_1_201) % 22.19/5.89 | % 22.19/5.89 +-Applying beta-rule and splitting (351), into two cases. % 22.19/5.89 |-Branch one: % 22.19/5.89 | (352) ~ (all_163_1_201 = 0) & relation(all_0_12_12) = all_163_1_201 % 22.19/5.89 | % 22.19/5.89 | Applying alpha-rule on (352) yields: % 22.19/5.89 | (353) ~ (all_163_1_201 = 0) % 22.19/5.89 | (354) relation(all_0_12_12) = all_163_1_201 % 22.19/5.90 | % 22.19/5.90 | Instantiating formula (68) with all_0_12_12, all_163_1_201, 0 and discharging atoms relation(all_0_12_12) = all_163_1_201, relation(all_0_12_12) = 0, yields: % 22.19/5.90 | (355) all_163_1_201 = 0 % 22.19/5.90 | % 22.19/5.90 | Equations (355) can reduce 353 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (357) ~ (all_163_1_201 = 0) & in(all_126_4_180, all_0_13_13) = all_163_1_201 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (357) yields: % 22.19/5.90 | (353) ~ (all_163_1_201 = 0) % 22.19/5.90 | (359) in(all_126_4_180, all_0_13_13) = all_163_1_201 % 22.19/5.90 | % 22.19/5.90 | Instantiating formula (27) with all_126_4_180, all_0_13_13, all_163_1_201, 0 and discharging atoms in(all_126_4_180, all_0_13_13) = all_163_1_201, in(all_126_4_180, all_0_13_13) = 0, yields: % 22.19/5.90 | (355) all_163_1_201 = 0 % 22.19/5.90 | % 22.19/5.90 | Equations (355) can reduce 353 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (362) ~ (all_163_1_201 = 0) & in(all_126_5_181, all_0_13_13) = all_163_1_201 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (362) yields: % 22.19/5.90 | (353) ~ (all_163_1_201 = 0) % 22.19/5.90 | (364) in(all_126_5_181, all_0_13_13) = all_163_1_201 % 22.19/5.90 | % 22.19/5.90 | Instantiating formula (27) with all_126_5_181, all_0_13_13, all_163_1_201, 0 and discharging atoms in(all_126_5_181, all_0_13_13) = all_163_1_201, in(all_126_5_181, all_0_13_13) = 0, yields: % 22.19/5.90 | (355) all_163_1_201 = 0 % 22.19/5.90 | % 22.19/5.90 | Equations (355) can reduce 353 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (367) ((all_163_0_200 = 0 & subset(all_126_5_181, all_126_4_180) = 0) | ( ~ (all_163_1_201 = 0) & in(all_126_2_178, all_0_12_12) = all_163_1_201)) & ((all_163_1_201 = 0 & in(all_126_2_178, all_0_12_12) = 0) | ( ~ (all_163_0_200 = 0) & subset(all_126_5_181, all_126_4_180) = all_163_0_200)) % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (367) yields: % 22.19/5.90 | (368) (all_163_0_200 = 0 & subset(all_126_5_181, all_126_4_180) = 0) | ( ~ (all_163_1_201 = 0) & in(all_126_2_178, all_0_12_12) = all_163_1_201) % 22.19/5.90 | (369) (all_163_1_201 = 0 & in(all_126_2_178, all_0_12_12) = 0) | ( ~ (all_163_0_200 = 0) & subset(all_126_5_181, all_126_4_180) = all_163_0_200) % 22.19/5.90 | % 22.19/5.90 +-Applying beta-rule and splitting (235), into two cases. % 22.19/5.90 |-Branch one: % 22.19/5.90 | (370) all_171_1_208 = 0 & in(all_126_3_179, all_0_12_12) = 0 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (370) yields: % 22.19/5.90 | (226) all_171_1_208 = 0 % 22.19/5.90 | (195) in(all_126_3_179, all_0_12_12) = 0 % 22.19/5.90 | % 22.19/5.90 +-Applying beta-rule and splitting (369), into two cases. % 22.19/5.90 |-Branch one: % 22.19/5.90 | (373) all_163_1_201 = 0 & in(all_126_2_178, all_0_12_12) = 0 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (373) yields: % 22.19/5.90 | (355) all_163_1_201 = 0 % 22.19/5.90 | (197) in(all_126_2_178, all_0_12_12) = 0 % 22.19/5.90 | % 22.19/5.90 +-Applying beta-rule and splitting (234), into two cases. % 22.19/5.90 |-Branch one: % 22.19/5.90 | (376) all_171_0_207 = 0 & subset(all_126_6_182, all_126_5_181) = 0 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (376) yields: % 22.19/5.90 | (377) all_171_0_207 = 0 % 22.19/5.90 | (346) subset(all_126_6_182, all_126_5_181) = 0 % 22.19/5.90 | % 22.19/5.90 +-Applying beta-rule and splitting (368), into two cases. % 22.19/5.90 |-Branch one: % 22.19/5.90 | (379) all_163_0_200 = 0 & subset(all_126_5_181, all_126_4_180) = 0 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (379) yields: % 22.19/5.90 | (380) all_163_0_200 = 0 % 22.19/5.90 | (320) subset(all_126_5_181, all_126_4_180) = 0 % 22.19/5.90 | % 22.19/5.90 | Instantiating formula (79) with all_126_6_182, all_126_4_180, all_160_0_197, all_178_0_214 and discharging atoms subset(all_126_6_182, all_126_4_180) = all_178_0_214, subset(all_126_6_182, all_126_4_180) = all_160_0_197, yields: % 22.19/5.90 | (382) all_178_0_214 = all_160_0_197 % 22.19/5.90 | % 22.19/5.90 | Equations (382) can reduce 274 to: % 22.19/5.90 | (316) ~ (all_160_0_197 = 0) % 22.19/5.90 | % 22.19/5.90 | From (382) and (275) follows: % 22.19/5.90 | (317) subset(all_126_6_182, all_126_4_180) = all_160_0_197 % 22.19/5.90 | % 22.19/5.90 | Instantiating formula (26) with all_160_0_197, all_126_4_180, all_126_5_181, all_126_6_182 and discharging atoms subset(all_126_5_181, all_126_4_180) = 0, subset(all_126_6_182, all_126_4_180) = all_160_0_197, yields: % 22.19/5.90 | (385) all_160_0_197 = 0 | ? [v0] : ( ~ (v0 = 0) & subset(all_126_6_182, all_126_5_181) = v0) % 22.19/5.90 | % 22.19/5.90 | Instantiating formula (70) with all_160_0_197, all_126_4_180, all_126_6_182 and discharging atoms subset(all_126_6_182, all_126_4_180) = all_160_0_197, yields: % 22.19/5.90 | (386) all_160_0_197 = 0 | ? [v0] : ? [v1] : ( ~ (v1 = 0) & powerset(all_126_4_180) = v0 & element(all_126_6_182, v0) = v1) % 22.19/5.90 | % 22.19/5.90 | Instantiating formula (64) with all_126_4_180, all_126_5_181, all_126_6_182 and discharging atoms subset(all_126_5_181, all_126_4_180) = 0, subset(all_126_6_182, all_126_5_181) = 0, yields: % 22.19/5.90 | (305) subset(all_126_6_182, all_126_4_180) = 0 % 22.19/5.90 | % 22.19/5.90 | Instantiating formula (149) with all_160_0_197, all_126_4_180, all_126_5_181, all_126_6_182 and discharging atoms subset(all_126_6_182, all_126_4_180) = all_160_0_197, subset(all_126_6_182, all_126_5_181) = 0, yields: % 22.19/5.90 | (388) all_160_0_197 = 0 | ? [v0] : ( ~ (v0 = 0) & subset(all_126_5_181, all_126_4_180) = v0) % 22.19/5.90 | % 22.19/5.90 +-Applying beta-rule and splitting (386), into two cases. % 22.19/5.90 |-Branch one: % 22.19/5.90 | (389) all_160_0_197 = 0 % 22.19/5.90 | % 22.19/5.90 | Equations (389) can reduce 316 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (316) ~ (all_160_0_197 = 0) % 22.19/5.90 | (392) ? [v0] : ? [v1] : ( ~ (v1 = 0) & powerset(all_126_4_180) = v0 & element(all_126_6_182, v0) = v1) % 22.19/5.90 | % 22.19/5.90 +-Applying beta-rule and splitting (388), into two cases. % 22.19/5.90 |-Branch one: % 22.19/5.90 | (389) all_160_0_197 = 0 % 22.19/5.90 | % 22.19/5.90 | Equations (389) can reduce 316 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (316) ~ (all_160_0_197 = 0) % 22.19/5.90 | (396) ? [v0] : ( ~ (v0 = 0) & subset(all_126_5_181, all_126_4_180) = v0) % 22.19/5.90 | % 22.19/5.90 +-Applying beta-rule and splitting (385), into two cases. % 22.19/5.90 |-Branch one: % 22.19/5.90 | (389) all_160_0_197 = 0 % 22.19/5.90 | % 22.19/5.90 | Equations (389) can reduce 316 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (316) ~ (all_160_0_197 = 0) % 22.19/5.90 | (400) ? [v0] : ( ~ (v0 = 0) & subset(all_126_6_182, all_126_5_181) = v0) % 22.19/5.90 | % 22.19/5.90 | Instantiating formula (79) with all_126_6_182, all_126_4_180, 0, all_160_0_197 and discharging atoms subset(all_126_6_182, all_126_4_180) = all_160_0_197, subset(all_126_6_182, all_126_4_180) = 0, yields: % 22.19/5.90 | (389) all_160_0_197 = 0 % 22.19/5.90 | % 22.19/5.90 | Equations (389) can reduce 316 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (403) ~ (all_163_1_201 = 0) & in(all_126_2_178, all_0_12_12) = all_163_1_201 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (403) yields: % 22.19/5.90 | (353) ~ (all_163_1_201 = 0) % 22.19/5.90 | (405) in(all_126_2_178, all_0_12_12) = all_163_1_201 % 22.19/5.90 | % 22.19/5.90 | Equations (355) can reduce 353 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (407) ~ (all_171_1_208 = 0) & in(all_126_3_179, all_0_12_12) = all_171_1_208 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (407) yields: % 22.19/5.90 | (224) ~ (all_171_1_208 = 0) % 22.19/5.90 | (409) in(all_126_3_179, all_0_12_12) = all_171_1_208 % 22.19/5.90 | % 22.19/5.90 | Equations (226) can reduce 224 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (411) ~ (all_163_0_200 = 0) & subset(all_126_5_181, all_126_4_180) = all_163_0_200 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (411) yields: % 22.19/5.90 | (412) ~ (all_163_0_200 = 0) % 22.19/5.90 | (413) subset(all_126_5_181, all_126_4_180) = all_163_0_200 % 22.19/5.90 | % 22.19/5.90 +-Applying beta-rule and splitting (368), into two cases. % 22.19/5.90 |-Branch one: % 22.19/5.90 | (379) all_163_0_200 = 0 & subset(all_126_5_181, all_126_4_180) = 0 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (379) yields: % 22.19/5.90 | (380) all_163_0_200 = 0 % 22.19/5.90 | (320) subset(all_126_5_181, all_126_4_180) = 0 % 22.19/5.90 | % 22.19/5.90 | Equations (380) can reduce 412 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (403) ~ (all_163_1_201 = 0) & in(all_126_2_178, all_0_12_12) = all_163_1_201 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (403) yields: % 22.19/5.90 | (353) ~ (all_163_1_201 = 0) % 22.19/5.90 | (405) in(all_126_2_178, all_0_12_12) = all_163_1_201 % 22.19/5.90 | % 22.19/5.90 | Instantiating formula (27) with all_126_2_178, all_0_12_12, all_163_1_201, 0 and discharging atoms in(all_126_2_178, all_0_12_12) = all_163_1_201, in(all_126_2_178, all_0_12_12) = 0, yields: % 22.19/5.90 | (355) all_163_1_201 = 0 % 22.19/5.90 | % 22.19/5.90 | Equations (355) can reduce 353 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (423) ~ (all_171_0_207 = 0) & subset(all_126_6_182, all_126_5_181) = all_171_0_207 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (423) yields: % 22.19/5.90 | (424) ~ (all_171_0_207 = 0) % 22.19/5.90 | (425) subset(all_126_6_182, all_126_5_181) = all_171_0_207 % 22.19/5.90 | % 22.19/5.90 +-Applying beta-rule and splitting (234), into two cases. % 22.19/5.90 |-Branch one: % 22.19/5.90 | (376) all_171_0_207 = 0 & subset(all_126_6_182, all_126_5_181) = 0 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (376) yields: % 22.19/5.90 | (377) all_171_0_207 = 0 % 22.19/5.90 | (346) subset(all_126_6_182, all_126_5_181) = 0 % 22.19/5.90 | % 22.19/5.90 | Equations (377) can reduce 424 to: % 22.19/5.90 | (164) $false % 22.19/5.90 | % 22.19/5.90 |-The branch is then unsatisfiable % 22.19/5.90 |-Branch two: % 22.19/5.90 | (407) ~ (all_171_1_208 = 0) & in(all_126_3_179, all_0_12_12) = all_171_1_208 % 22.19/5.90 | % 22.19/5.90 | Applying alpha-rule on (407) yields: % 22.19/5.90 | (224) ~ (all_171_1_208 = 0) % 22.19/5.90 | (409) in(all_126_3_179, all_0_12_12) = all_171_1_208 % 22.19/5.91 | % 22.19/5.91 | Instantiating formula (27) with all_126_3_179, all_0_12_12, all_171_1_208, 0 and discharging atoms in(all_126_3_179, all_0_12_12) = all_171_1_208, in(all_126_3_179, all_0_12_12) = 0, yields: % 22.19/5.91 | (226) all_171_1_208 = 0 % 22.19/5.91 | % 22.19/5.91 | Equations (226) can reduce 224 to: % 22.19/5.91 | (164) $false % 22.19/5.91 | % 22.19/5.91 |-The branch is then unsatisfiable % 22.19/5.91 |-Branch two: % 22.19/5.91 | (435) ~ (all_159_0_195 = 0) & subset(all_126_6_182, all_126_5_181) = all_159_0_195 % 22.19/5.91 | % 22.19/5.91 | Applying alpha-rule on (435) yields: % 22.19/5.91 | (436) ~ (all_159_0_195 = 0) % 22.19/5.91 | (437) subset(all_126_6_182, all_126_5_181) = all_159_0_195 % 22.19/5.91 | % 22.19/5.91 | Equations (345) can reduce 436 to: % 22.19/5.91 | (164) $false % 22.19/5.91 | % 22.19/5.91 |-The branch is then unsatisfiable % 22.19/5.91 |-Branch two: % 22.19/5.91 | (439) ~ (all_159_1_196 = 0) & in(all_126_3_179, all_0_12_12) = all_159_1_196 % 22.19/5.91 | % 22.19/5.91 | Applying alpha-rule on (439) yields: % 22.19/5.91 | (327) ~ (all_159_1_196 = 0) % 22.19/5.91 | (441) in(all_126_3_179, all_0_12_12) = all_159_1_196 % 22.19/5.91 | % 22.19/5.91 +-Applying beta-rule and splitting (234), into two cases. % 22.19/5.91 |-Branch one: % 22.19/5.91 | (376) all_171_0_207 = 0 & subset(all_126_6_182, all_126_5_181) = 0 % 22.19/5.91 | % 22.19/5.91 | Applying alpha-rule on (376) yields: % 22.19/5.91 | (377) all_171_0_207 = 0 % 22.19/5.91 | (346) subset(all_126_6_182, all_126_5_181) = 0 % 22.19/5.91 | % 22.19/5.91 +-Applying beta-rule and splitting (235), into two cases. % 22.19/5.91 |-Branch one: % 22.19/5.91 | (370) all_171_1_208 = 0 & in(all_126_3_179, all_0_12_12) = 0 % 22.19/5.91 | % 22.19/5.91 | Applying alpha-rule on (370) yields: % 22.19/5.91 | (226) all_171_1_208 = 0 % 22.19/5.91 | (195) in(all_126_3_179, all_0_12_12) = 0 % 22.19/5.91 | % 22.19/5.91 | Instantiating formula (27) with all_126_3_179, all_0_12_12, all_159_1_196, 0 and discharging atoms in(all_126_3_179, all_0_12_12) = all_159_1_196, in(all_126_3_179, all_0_12_12) = 0, yields: % 22.19/5.91 | (329) all_159_1_196 = 0 % 22.19/5.91 | % 22.19/5.91 | Equations (329) can reduce 327 to: % 22.19/5.91 | (164) $false % 22.19/5.91 | % 22.19/5.91 |-The branch is then unsatisfiable % 22.19/5.91 |-Branch two: % 22.19/5.91 | (423) ~ (all_171_0_207 = 0) & subset(all_126_6_182, all_126_5_181) = all_171_0_207 % 22.19/5.91 | % 22.19/5.91 | Applying alpha-rule on (423) yields: % 22.19/5.91 | (424) ~ (all_171_0_207 = 0) % 22.19/5.91 | (425) subset(all_126_6_182, all_126_5_181) = all_171_0_207 % 22.19/5.91 | % 22.19/5.91 | Equations (377) can reduce 424 to: % 22.19/5.91 | (164) $false % 22.19/5.91 | % 22.19/5.91 |-The branch is then unsatisfiable % 22.19/5.91 |-Branch two: % 22.19/5.91 | (407) ~ (all_171_1_208 = 0) & in(all_126_3_179, all_0_12_12) = all_171_1_208 % 22.19/5.91 | % 22.19/5.91 | Applying alpha-rule on (407) yields: % 22.19/5.91 | (224) ~ (all_171_1_208 = 0) % 22.19/5.91 | (409) in(all_126_3_179, all_0_12_12) = all_171_1_208 % 22.19/5.91 | % 22.19/5.91 | Instantiating formula (27) with all_126_3_179, all_0_12_12, all_171_1_208, 0 and discharging atoms in(all_126_3_179, all_0_12_12) = all_171_1_208, in(all_126_3_179, all_0_12_12) = 0, yields: % 22.19/5.91 | (226) all_171_1_208 = 0 % 22.19/5.91 | % 22.19/5.91 | Instantiating formula (27) with all_126_3_179, all_0_12_12, all_159_1_196, all_171_1_208 and discharging atoms in(all_126_3_179, all_0_12_12) = all_171_1_208, in(all_126_3_179, all_0_12_12) = all_159_1_196, yields: % 22.19/5.91 | (458) all_171_1_208 = all_159_1_196 % 22.19/5.91 | % 22.19/5.91 | Combining equations (458,226) yields a new equation: % 22.19/5.91 | (459) all_159_1_196 = 0 % 22.19/5.91 | % 22.19/5.91 | Simplifying 459 yields: % 22.19/5.91 | (329) all_159_1_196 = 0 % 22.19/5.91 | % 22.19/5.91 | Equations (329) can reduce 327 to: % 22.19/5.91 | (164) $false % 22.19/5.91 | % 22.19/5.91 |-The branch is then unsatisfiable % 22.19/5.91 |-Branch two: % 22.19/5.91 | (462) ~ (all_183_0_220 = 0) & subset(all_126_5_181, all_126_4_180) = all_183_0_220 % 22.19/5.91 | % 22.19/5.91 | Applying alpha-rule on (462) yields: % 22.19/5.91 | (463) ~ (all_183_0_220 = 0) % 22.19/5.91 | (464) subset(all_126_5_181, all_126_4_180) = all_183_0_220 % 22.19/5.91 | % 22.19/5.91 | Equations (319) can reduce 463 to: % 22.19/5.91 | (164) $false % 22.19/5.91 | % 22.19/5.91 |-The branch is then unsatisfiable % 22.19/5.91 |-Branch two: % 22.19/5.91 | (466) ~ (all_183_1_221 = 0) & in(all_126_2_178, all_0_12_12) = all_183_1_221 % 22.19/5.91 | % 22.19/5.91 | Applying alpha-rule on (466) yields: % 22.19/5.91 | (238) ~ (all_183_1_221 = 0) % 22.19/5.91 | (468) in(all_126_2_178, all_0_12_12) = all_183_1_221 % 22.19/5.91 | % 22.19/5.91 +-Applying beta-rule and splitting (218), into two cases. % 22.19/5.91 |-Branch one: % 22.19/5.91 | (350) ( ~ (all_163_1_201 = 0) & relation(all_0_12_12) = all_163_1_201) | ( ~ (all_163_1_201 = 0) & in(all_126_4_180, all_0_13_13) = all_163_1_201) | ( ~ (all_163_1_201 = 0) & in(all_126_5_181, all_0_13_13) = all_163_1_201) % 22.19/5.91 | % 22.19/5.91 +-Applying beta-rule and splitting (350), into two cases. % 22.19/5.91 |-Branch one: % 22.19/5.91 | (351) ( ~ (all_163_1_201 = 0) & relation(all_0_12_12) = all_163_1_201) | ( ~ (all_163_1_201 = 0) & in(all_126_4_180, all_0_13_13) = all_163_1_201) % 22.19/5.91 | % 22.19/5.91 +-Applying beta-rule and splitting (351), into two cases. % 22.19/5.91 |-Branch one: % 22.19/5.91 | (352) ~ (all_163_1_201 = 0) & relation(all_0_12_12) = all_163_1_201 % 22.19/5.91 | % 22.19/5.91 | Applying alpha-rule on (352) yields: % 22.19/5.91 | (353) ~ (all_163_1_201 = 0) % 22.19/5.91 | (354) relation(all_0_12_12) = all_163_1_201 % 22.34/5.91 | % 22.34/5.91 | Instantiating formula (68) with all_0_12_12, all_163_1_201, 0 and discharging atoms relation(all_0_12_12) = all_163_1_201, relation(all_0_12_12) = 0, yields: % 22.34/5.91 | (355) all_163_1_201 = 0 % 22.34/5.91 | % 22.34/5.91 | Equations (355) can reduce 353 to: % 22.34/5.91 | (164) $false % 22.34/5.91 | % 22.34/5.91 |-The branch is then unsatisfiable % 22.34/5.91 |-Branch two: % 22.34/5.91 | (357) ~ (all_163_1_201 = 0) & in(all_126_4_180, all_0_13_13) = all_163_1_201 % 22.34/5.91 | % 22.34/5.91 | Applying alpha-rule on (357) yields: % 22.34/5.91 | (353) ~ (all_163_1_201 = 0) % 22.34/5.91 | (359) in(all_126_4_180, all_0_13_13) = all_163_1_201 % 22.34/5.91 | % 22.34/5.91 | Instantiating formula (27) with all_126_4_180, all_0_13_13, all_163_1_201, 0 and discharging atoms in(all_126_4_180, all_0_13_13) = all_163_1_201, in(all_126_4_180, all_0_13_13) = 0, yields: % 22.34/5.91 | (355) all_163_1_201 = 0 % 22.34/5.91 | % 22.34/5.91 | Equations (355) can reduce 353 to: % 22.34/5.91 | (164) $false % 22.34/5.91 | % 22.34/5.91 |-The branch is then unsatisfiable % 22.34/5.91 |-Branch two: % 22.34/5.91 | (362) ~ (all_163_1_201 = 0) & in(all_126_5_181, all_0_13_13) = all_163_1_201 % 22.34/5.91 | % 22.34/5.91 | Applying alpha-rule on (362) yields: % 22.34/5.91 | (353) ~ (all_163_1_201 = 0) % 22.34/5.91 | (364) in(all_126_5_181, all_0_13_13) = all_163_1_201 % 22.34/5.91 | % 22.34/5.91 | Instantiating formula (27) with all_126_5_181, all_0_13_13, all_163_1_201, 0 and discharging atoms in(all_126_5_181, all_0_13_13) = all_163_1_201, in(all_126_5_181, all_0_13_13) = 0, yields: % 22.34/5.91 | (355) all_163_1_201 = 0 % 22.34/5.91 | % 22.34/5.91 | Equations (355) can reduce 353 to: % 22.34/5.91 | (164) $false % 22.34/5.91 | % 22.34/5.91 |-The branch is then unsatisfiable % 22.34/5.91 |-Branch two: % 22.34/5.91 | (367) ((all_163_0_200 = 0 & subset(all_126_5_181, all_126_4_180) = 0) | ( ~ (all_163_1_201 = 0) & in(all_126_2_178, all_0_12_12) = all_163_1_201)) & ((all_163_1_201 = 0 & in(all_126_2_178, all_0_12_12) = 0) | ( ~ (all_163_0_200 = 0) & subset(all_126_5_181, all_126_4_180) = all_163_0_200)) % 22.34/5.91 | % 22.34/5.91 | Applying alpha-rule on (367) yields: % 22.34/5.91 | (368) (all_163_0_200 = 0 & subset(all_126_5_181, all_126_4_180) = 0) | ( ~ (all_163_1_201 = 0) & in(all_126_2_178, all_0_12_12) = all_163_1_201) % 22.34/5.91 | (369) (all_163_1_201 = 0 & in(all_126_2_178, all_0_12_12) = 0) | ( ~ (all_163_0_200 = 0) & subset(all_126_5_181, all_126_4_180) = all_163_0_200) % 22.34/5.91 | % 22.34/5.91 +-Applying beta-rule and splitting (368), into two cases. % 22.34/5.91 |-Branch one: % 22.34/5.91 | (379) all_163_0_200 = 0 & subset(all_126_5_181, all_126_4_180) = 0 % 22.34/5.91 | % 22.34/5.91 | Applying alpha-rule on (379) yields: % 22.34/5.91 | (380) all_163_0_200 = 0 % 22.34/5.91 | (320) subset(all_126_5_181, all_126_4_180) = 0 % 22.34/5.91 | % 22.34/5.91 +-Applying beta-rule and splitting (369), into two cases. % 22.34/5.91 |-Branch one: % 22.34/5.91 | (373) all_163_1_201 = 0 & in(all_126_2_178, all_0_12_12) = 0 % 22.34/5.91 | % 22.34/5.91 | Applying alpha-rule on (373) yields: % 22.34/5.91 | (355) all_163_1_201 = 0 % 22.34/5.91 | (197) in(all_126_2_178, all_0_12_12) = 0 % 22.34/5.91 | % 22.34/5.91 | Instantiating formula (27) with all_126_2_178, all_0_12_12, all_183_1_221, 0 and discharging atoms in(all_126_2_178, all_0_12_12) = all_183_1_221, in(all_126_2_178, all_0_12_12) = 0, yields: % 22.34/5.91 | (240) all_183_1_221 = 0 % 22.34/5.91 | % 22.34/5.91 | Equations (240) can reduce 238 to: % 22.34/5.91 | (164) $false % 22.34/5.91 | % 22.34/5.91 |-The branch is then unsatisfiable % 22.34/5.91 |-Branch two: % 22.34/5.91 | (411) ~ (all_163_0_200 = 0) & subset(all_126_5_181, all_126_4_180) = all_163_0_200 % 22.34/5.91 | % 22.34/5.91 | Applying alpha-rule on (411) yields: % 22.34/5.91 | (412) ~ (all_163_0_200 = 0) % 22.34/5.91 | (413) subset(all_126_5_181, all_126_4_180) = all_163_0_200 % 22.34/5.91 | % 22.34/5.91 | Equations (380) can reduce 412 to: % 22.34/5.91 | (164) $false % 22.34/5.91 | % 22.34/5.91 |-The branch is then unsatisfiable % 22.34/5.91 |-Branch two: % 22.34/5.91 | (403) ~ (all_163_1_201 = 0) & in(all_126_2_178, all_0_12_12) = all_163_1_201 % 22.34/5.91 | % 22.34/5.91 | Applying alpha-rule on (403) yields: % 22.34/5.91 | (353) ~ (all_163_1_201 = 0) % 22.34/5.91 | (405) in(all_126_2_178, all_0_12_12) = all_163_1_201 % 22.34/5.91 | % 22.34/5.91 | Instantiating formula (27) with all_126_2_178, all_0_12_12, all_183_1_221, 0 and discharging atoms in(all_126_2_178, all_0_12_12) = all_183_1_221, in(all_126_2_178, all_0_12_12) = 0, yields: % 22.34/5.91 | (240) all_183_1_221 = 0 % 22.34/5.91 | % 22.34/5.91 | Instantiating formula (27) with all_126_2_178, all_0_12_12, all_163_1_201, all_183_1_221 and discharging atoms in(all_126_2_178, all_0_12_12) = all_183_1_221, in(all_126_2_178, all_0_12_12) = all_163_1_201, yields: % 22.34/5.91 | (505) all_183_1_221 = all_163_1_201 % 22.34/5.91 | % 22.34/5.91 | Combining equations (240,505) yields a new equation: % 22.34/5.91 | (355) all_163_1_201 = 0 % 22.34/5.91 | % 22.34/5.91 | Equations (355) can reduce 353 to: % 22.34/5.91 | (164) $false % 22.34/5.91 | % 22.34/5.91 |-The branch is then unsatisfiable % 22.34/5.92 |-Branch two: % 22.34/5.92 | (508) ~ (all_73_1_102 = all_0_13_13) % 22.34/5.92 | (509) ? [v0] : ( ~ (v0 = 0) & relation(all_0_12_12) = v0) % 22.34/5.92 | % 22.34/5.92 | Instantiating formula (91) with all_0_12_12, all_108_2_160, all_73_1_102 and discharging atoms relation_field(all_0_12_12) = all_108_2_160, relation_field(all_0_12_12) = all_73_1_102, yields: % 22.34/5.92 | (510) all_108_2_160 = all_73_1_102 % 22.34/5.92 | % 22.34/5.92 | Instantiating formula (91) with all_0_12_12, all_0_13_13, all_108_2_160 and discharging atoms relation_field(all_0_12_12) = all_108_2_160, relation_field(all_0_12_12) = all_0_13_13, yields: % 22.34/5.92 | (207) all_108_2_160 = all_0_13_13 % 22.34/5.92 | % 22.34/5.92 | Combining equations (207,510) yields a new equation: % 22.34/5.92 | (187) all_73_1_102 = all_0_13_13 % 22.34/5.92 | % 22.34/5.92 | Equations (187) can reduce 508 to: % 22.34/5.92 | (164) $false % 22.34/5.92 | % 22.34/5.92 |-The branch is then unsatisfiable % 22.34/5.92 % SZS output end Proof for theBenchmark % 22.34/5.92 % 22.34/5.92 5327ms %------------------------------------------------------------------------------