%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SEU020+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Jul 19 08:46:14 EDT 2022 % Result : Theorem 21.33s 6.65s % Output : Proof 51.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SEU020+1 : TPTP v8.1.0. Released v3.2.0. % 0.11/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.11/0.33 % Computer : n025.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Mon Jun 20 11:07:29 EDT 2022 % 0.11/0.33 % CPUTime : % 0.18/0.57 ____ _ % 0.18/0.57 ___ / __ \_____(_)___ ________ __________ % 0.18/0.57 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.18/0.57 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.18/0.57 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.18/0.57 % 0.18/0.57 A Theorem Prover for First-Order Logic % 0.18/0.58 (ePrincess v.1.0) % 0.18/0.58 % 0.18/0.58 (c) Philipp Rümmer, 2009-2015 % 0.18/0.58 (c) Peter Backeman, 2014-2015 % 0.18/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.18/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.18/0.58 Bug reports to peter@backeman.se % 0.18/0.58 % 0.18/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.18/0.58 % 0.18/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.72/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.62/0.95 Prover 0: Preprocessing ... % 2.33/1.23 Prover 0: Warning: ignoring some quantifiers % 2.43/1.26 Prover 0: Constructing countermodel ... % 18.01/5.92 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 18.25/5.98 Prover 1: Preprocessing ... % 18.94/6.10 Prover 1: Warning: ignoring some quantifiers % 18.94/6.11 Prover 1: Constructing countermodel ... % 19.63/6.27 Prover 1: gave up % 19.63/6.27 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 19.63/6.30 Prover 2: Preprocessing ... % 20.31/6.43 Prover 2: Warning: ignoring some quantifiers % 20.31/6.44 Prover 2: Constructing countermodel ... % 21.33/6.65 Prover 2: proved (379ms) % 21.33/6.65 Prover 0: stopped % 21.33/6.65 % 21.33/6.65 No countermodel exists, formula is valid % 21.33/6.65 % SZS status Theorem for theBenchmark % 21.33/6.65 % 21.33/6.65 Generating proof ... Warning: ignoring some quantifiers % 49.97/21.17 found it (size 191) % 49.97/21.17 % 49.97/21.17 % SZS output start Proof for theBenchmark % 49.97/21.17 Assumed formulas after preprocessing and simplification: % 49.97/21.17 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ( ~ (v9 = 0) & ~ (v7 = 0) & ~ (v3 = 0) & one_to_one(v0) = v3 & relation_empty_yielding(v5) = 0 & relation_empty_yielding(empty_set) = 0 & relation_dom(v0) = v1 & identity_relation(v1) = v2 & relation_composition(v0, v4) = v2 & relation(v12) = 0 & relation(v11) = 0 & relation(v8) = 0 & relation(v5) = 0 & relation(v4) = 0 & relation(v0) = 0 & relation(empty_set) = 0 & function(v12) = 0 & function(v4) = 0 & function(v0) = 0 & empty(v11) = 0 & empty(v10) = 0 & empty(v8) = v9 & empty(v6) = v7 & empty(empty_set) = 0 & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (powerset(v15) = v16) | ~ (element(v14, v16) = 0) | ~ (element(v13, v15) = v17) | ? [v18] : ( ~ (v18 = 0) & in(v13, v14) = v18)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (one_to_one(v15) = v16) | ~ (relation_dom(v13) = v14) | ? [v17] : ? [v18] : (( ~ (v18 = 0) & one_to_one(v17) = v18 & relation_composition(v15, v13) = v17) | ( ~ (v18 = 0) & subset(v17, v14) = v18 & relation_rng(v15) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & relation(v13) = v17) | ( ~ (v17 = 0) & function(v15) = v17) | ( ~ (v17 = 0) & function(v13) = v17))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (powerset(v14) = v15) | ~ (element(v13, v15) = v16) | ? [v17] : ( ~ (v17 = 0) & subset(v13, v14) = v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (element(v13, v15) = v16) | ~ (in(v13, v14) = 0) | ? [v17] : ? [v18] : ( ~ (v18 = 0) & powerset(v15) = v17 & element(v14, v17) = v18)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v14 = v13 | ~ (subset(v16, v15) = v14) | ~ (subset(v16, v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v14 = v13 | ~ (element(v16, v15) = v14) | ~ (element(v16, v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v14 = v13 | ~ (relation_composition(v16, v15) = v14) | ~ (relation_composition(v16, v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v14 = v13 | ~ (in(v16, v15) = v14) | ~ (in(v16, v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (relation_rng(v15) = v16) | ~ (relation_dom(v13) = v14) | ? [v17] : ? [v18] : ? [v19] : ((v17 = 0 & subset(v16, v14) = 0) | ( ~ (v19 = v18) & relation_dom(v17) = v18 & relation_dom(v15) = v19 & relation_composition(v15, v13) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & relation(v13) = v17) | ( ~ (v17 = 0) & function(v15) = v17) | ( ~ (v17 = 0) & function(v13) = v17))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (relation_rng(v15) = v16) | ~ (relation_dom(v13) = v14) | ? [v17] : ? [v18] : ((v17 = 0 & one_to_one(v15) = 0) | ( ~ (v18 = 0) & one_to_one(v17) = v18 & relation_composition(v15, v13) = v17) | ( ~ (v17 = 0) & subset(v16, v14) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & relation(v13) = v17) | ( ~ (v17 = 0) & function(v15) = v17) | ( ~ (v17 = 0) & function(v13) = v17))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (relation_dom(v15) = v16) | ~ (relation_dom(v13) = v14) | ? [v17] : ? [v18] : ((v18 = 0 & subset(v17, v14) = 0 & relation_rng(v15) = v17) | ( ~ (v18 = v16) & relation_dom(v17) = v18 & relation_composition(v15, v13) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & relation(v13) = v17) | ( ~ (v17 = 0) & function(v15) = v17) | ( ~ (v17 = 0) & function(v13) = v17))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (relation_dom(v13) = v14) | ~ (relation_composition(v15, v13) = v16) | ? [v17] : ? [v18] : ((v18 = 0 & subset(v17, v14) = 0 & relation_rng(v15) = v17) | ( ~ (v18 = v17) & relation_dom(v16) = v17 & relation_dom(v15) = v18) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & relation(v13) = v17) | ( ~ (v17 = 0) & function(v15) = v17) | ( ~ (v17 = 0) & function(v13) = v17))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (relation_dom(v13) = v14) | ~ (relation_composition(v15, v13) = v16) | ? [v17] : ? [v18] : ((v17 = 0 & one_to_one(v15) = 0) | ( ~ (v18 = 0) & subset(v17, v14) = v18 & relation_rng(v15) = v17) | ( ~ (v17 = 0) & one_to_one(v16) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & relation(v13) = v17) | ( ~ (v17 = 0) & function(v15) = v17) | ( ~ (v17 = 0) & function(v13) = v17))) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (powerset(v15) = v16) | ~ (element(v14, v16) = 0) | ~ (in(v13, v14) = 0) | element(v13, v15) = 0) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (powerset(v15) = v16) | ~ (element(v14, v16) = 0) | ~ (in(v13, v14) = 0) | ? [v17] : ( ~ (v17 = 0) & empty(v15) = v17)) & ! [v13] : ! [v14] : ! [v15] : (v15 = 0 | ~ (subset(v13, v14) = v15) | ? [v16] : ? [v17] : ( ~ (v17 = 0) & powerset(v14) = v16 & element(v13, v16) = v17)) & ! [v13] : ! [v14] : ! [v15] : (v15 = 0 | ~ (element(v13, v14) = v15) | ? [v16] : ( ~ (v16 = 0) & in(v13, v14) = v16)) & ! [v13] : ! [v14] : ! [v15] : (v15 = 0 | ~ (in(v13, v14) = v15) | ? [v16] : ((v16 = 0 & empty(v14) = 0) | ( ~ (v16 = 0) & element(v13, v14) = v16))) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (one_to_one(v15) = v14) | ~ (one_to_one(v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (relation_empty_yielding(v15) = v14) | ~ (relation_empty_yielding(v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (relation_rng(v15) = v14) | ~ (relation_rng(v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (relation_dom(v15) = v14) | ~ (relation_dom(v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (powerset(v15) = v14) | ~ (powerset(v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (identity_relation(v15) = v14) | ~ (identity_relation(v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (relation(v15) = v14) | ~ (relation(v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (function(v15) = v14) | ~ (function(v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (empty(v15) = v14) | ~ (empty(v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : ( ~ (relation_dom(v13) = v14) | ~ (relation(v15) = 0) | ? [v16] : ? [v17] : ? [v18] : ((v17 = 0 & subset(v16, v14) = 0 & relation_rng(v15) = v16) | ( ~ (v18 = v17) & relation_dom(v16) = v17 & relation_dom(v15) = v18 & relation_composition(v15, v13) = v16) | ( ~ (v16 = 0) & relation(v13) = v16) | ( ~ (v16 = 0) & function(v15) = v16) | ( ~ (v16 = 0) & function(v13) = v16))) & ! [v13] : ! [v14] : ! [v15] : ( ~ (relation_dom(v13) = v14) | ~ (relation(v15) = 0) | ? [v16] : ? [v17] : ((v16 = 0 & one_to_one(v15) = 0) | ( ~ (v17 = 0) & one_to_one(v16) = v17 & relation_composition(v15, v13) = v16) | ( ~ (v17 = 0) & subset(v16, v14) = v17 & relation_rng(v15) = v16) | ( ~ (v16 = 0) & relation(v13) = v16) | ( ~ (v16 = 0) & function(v15) = v16) | ( ~ (v16 = 0) & function(v13) = v16))) & ! [v13] : ! [v14] : ! [v15] : ( ~ (relation_dom(v13) = v14) | ~ (function(v15) = 0) | ? [v16] : ? [v17] : ? [v18] : ((v17 = 0 & subset(v16, v14) = 0 & relation_rng(v15) = v16) | ( ~ (v18 = v17) & relation_dom(v16) = v17 & relation_dom(v15) = v18 & relation_composition(v15, v13) = v16) | ( ~ (v16 = 0) & relation(v15) = v16) | ( ~ (v16 = 0) & relation(v13) = v16) | ( ~ (v16 = 0) & function(v13) = v16))) & ! [v13] : ! [v14] : ! [v15] : ( ~ (relation_dom(v13) = v14) | ~ (function(v15) = 0) | ? [v16] : ? [v17] : ((v16 = 0 & one_to_one(v15) = 0) | ( ~ (v17 = 0) & one_to_one(v16) = v17 & relation_composition(v15, v13) = v16) | ( ~ (v17 = 0) & subset(v16, v14) = v17 & relation_rng(v15) = v16) | ( ~ (v16 = 0) & relation(v15) = v16) | ( ~ (v16 = 0) & relation(v13) = v16) | ( ~ (v16 = 0) & function(v13) = v16))) & ! [v13] : ! [v14] : ! [v15] : ( ~ (powerset(v14) = v15) | ~ (element(v13, v15) = 0) | subset(v13, v14) = 0) & ! [v13] : ! [v14] : ! [v15] : ( ~ (relation_composition(v14, v13) = v15) | ? [v16] : ? [v17] : ((v17 = 0 & v16 = 0 & relation(v15) = 0 & empty(v15) = 0) | ( ~ (v16 = 0) & relation(v14) = v16) | ( ~ (v16 = 0) & empty(v13) = v16))) & ! [v13] : ! [v14] : ! [v15] : ( ~ (relation_composition(v13, v14) = v15) | ? [v16] : ? [v17] : ((v17 = 0 & v16 = 0 & relation(v15) = 0 & function(v15) = 0) | ( ~ (v16 = 0) & relation(v14) = v16) | ( ~ (v16 = 0) & relation(v13) = v16) | ( ~ (v16 = 0) & function(v14) = v16) | ( ~ (v16 = 0) & function(v13) = v16))) & ! [v13] : ! [v14] : ! [v15] : ( ~ (relation_composition(v13, v14) = v15) | ? [v16] : ? [v17] : ((v17 = 0 & v16 = 0 & relation(v15) = 0 & empty(v15) = 0) | ( ~ (v16 = 0) & relation(v14) = v16) | ( ~ (v16 = 0) & empty(v13) = v16))) & ! [v13] : ! [v14] : ! [v15] : ( ~ (relation_composition(v13, v14) = v15) | ? [v16] : ((v16 = 0 & relation(v15) = 0) | ( ~ (v16 = 0) & relation(v14) = v16) | ( ~ (v16 = 0) & relation(v13) = v16))) & ! [v13] : ! [v14] : ! [v15] : ( ~ (empty(v15) = 0) | ~ (in(v13, v14) = 0) | ? [v16] : ? [v17] : ( ~ (v17 = 0) & powerset(v15) = v16 & element(v14, v16) = v17)) & ! [v13] : ! [v14] : (v14 = v13 | ~ (empty(v14) = 0) | ~ (empty(v13) = 0)) & ! [v13] : ! [v14] : (v14 = 0 | ~ (subset(v13, v13) = v14)) & ! [v13] : ! [v14] : (v14 = 0 | ~ (relation(v13) = v14) | ? [v15] : ( ~ (v15 = 0) & empty(v13) = v15)) & ! [v13] : ! [v14] : (v14 = 0 | ~ (function(v13) = v14) | ? [v15] : ( ~ (v15 = 0) & empty(v13) = v15)) & ! [v13] : ! [v14] : (v14 = 0 | ~ (empty(v13) = v14) | ? [v15] : ? [v16] : ? [v17] : ( ~ (v17 = 0) & powerset(v13) = v15 & element(v16, v15) = 0 & empty(v16) = v17)) & ! [v13] : ! [v14] : (v14 = 0 | ~ (empty(v13) = v14) | ? [v15] : ? [v16] : (( ~ (v16 = 0) & relation_rng(v13) = v15 & empty(v15) = v16) | ( ~ (v15 = 0) & relation(v13) = v15))) & ! [v13] : ! [v14] : (v14 = 0 | ~ (empty(v13) = v14) | ? [v15] : ? [v16] : (( ~ (v16 = 0) & relation_dom(v13) = v15 & empty(v15) = v16) | ( ~ (v15 = 0) & relation(v13) = v15))) & ! [v13] : ! [v14] : ( ~ (subset(v13, v14) = 0) | ? [v15] : (powerset(v14) = v15 & element(v13, v15) = 0)) & ! [v13] : ! [v14] : ( ~ (relation_rng(v13) = v14) | ? [v15] : ? [v16] : ((v16 = 0 & v15 = 0 & relation(v14) = 0 & empty(v14) = 0) | ( ~ (v15 = 0) & empty(v13) = v15))) & ! [v13] : ! [v14] : ( ~ (relation_rng(v13) = v14) | ? [v15] : ((v15 = 0 & empty(v13) = 0) | ( ~ (v15 = 0) & relation(v13) = v15) | ( ~ (v15 = 0) & empty(v14) = v15))) & ! [v13] : ! [v14] : ( ~ (relation_dom(v13) = v14) | ? [v15] : ? [v16] : ((v16 = 0 & v15 = 0 & relation(v14) = 0 & empty(v14) = 0) | ( ~ (v15 = 0) & empty(v13) = v15))) & ! [v13] : ! [v14] : ( ~ (relation_dom(v13) = v14) | ? [v15] : ((v15 = 0 & empty(v13) = 0) | ( ~ (v15 = 0) & relation(v13) = v15) | ( ~ (v15 = 0) & empty(v14) = v15))) & ! [v13] : ! [v14] : ( ~ (powerset(v13) = v14) | ? [v15] : ? [v16] : ? [v17] : ((v16 = 0 & ~ (v17 = 0) & element(v15, v14) = 0 & empty(v15) = v17) | (v15 = 0 & empty(v13) = 0))) & ! [v13] : ! [v14] : ( ~ (powerset(v13) = v14) | ? [v15] : ( ~ (v15 = 0) & empty(v14) = v15)) & ! [v13] : ! [v14] : ( ~ (powerset(v13) = v14) | ? [v15] : (element(v15, v14) = 0 & empty(v15) = 0)) & ! [v13] : ! [v14] : ( ~ (element(v13, v14) = 0) | ? [v15] : ((v15 = 0 & empty(v14) = 0) | (v15 = 0 & in(v13, v14) = 0))) & ! [v13] : ! [v14] : ( ~ (identity_relation(v13) = v14) | one_to_one(v14) = 0) & ! [v13] : ! [v14] : ( ~ (identity_relation(v13) = v14) | relation_rng(v14) = v13) & ! [v13] : ! [v14] : ( ~ (identity_relation(v13) = v14) | relation_dom(v14) = v13) & ! [v13] : ! [v14] : ( ~ (identity_relation(v13) = v14) | relation(v14) = 0) & ! [v13] : ! [v14] : ( ~ (identity_relation(v13) = v14) | function(v14) = 0) & ! [v13] : ! [v14] : ( ~ (in(v14, v13) = 0) | ? [v15] : ( ~ (v15 = 0) & in(v13, v14) = v15)) & ! [v13] : ! [v14] : ( ~ (in(v13, v14) = 0) | element(v13, v14) = 0) & ! [v13] : ! [v14] : ( ~ (in(v13, v14) = 0) | ? [v15] : ( ~ (v15 = 0) & empty(v14) = v15)) & ! [v13] : ! [v14] : ( ~ (in(v13, v14) = 0) | ? [v15] : ( ~ (v15 = 0) & in(v14, v13) = v15)) & ! [v13] : (v13 = empty_set | ~ (empty(v13) = 0)) & ! [v13] : ( ~ (relation(v13) = 0) | ? [v14] : ? [v15] : ((v14 = 0 & empty(v13) = 0) | ( ~ (v15 = 0) & relation_rng(v13) = v14 & empty(v14) = v15))) & ! [v13] : ( ~ (relation(v13) = 0) | ? [v14] : ? [v15] : ((v14 = 0 & empty(v13) = 0) | ( ~ (v15 = 0) & relation_dom(v13) = v14 & empty(v14) = v15))) & ! [v13] : ( ~ (relation(v13) = 0) | ? [v14] : (( ~ (v14 = 0) & function(v13) = v14) | (relation_dom(v13) = v14 & ! [v15] : ! [v16] : (v16 = 0 | ~ (one_to_one(v15) = v16) | ? [v17] : ? [v18] : (( ~ (v18 = 0) & one_to_one(v17) = v18 & relation_composition(v15, v13) = v17) | ( ~ (v18 = 0) & subset(v17, v14) = v18 & relation_rng(v15) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ! [v16] : ( ~ (relation_rng(v15) = v16) | ? [v17] : ? [v18] : ((v17 = 0 & one_to_one(v15) = 0) | ( ~ (v18 = 0) & one_to_one(v17) = v18 & relation_composition(v15, v13) = v17) | ( ~ (v17 = 0) & subset(v16, v14) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ! [v16] : ( ~ (relation_composition(v15, v13) = v16) | ? [v17] : ? [v18] : ((v17 = 0 & one_to_one(v15) = 0) | ( ~ (v18 = 0) & subset(v17, v14) = v18 & relation_rng(v15) = v17) | ( ~ (v17 = 0) & one_to_one(v16) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ( ~ (relation(v15) = 0) | ? [v16] : ? [v17] : ((v16 = 0 & one_to_one(v15) = 0) | ( ~ (v17 = 0) & one_to_one(v16) = v17 & relation_composition(v15, v13) = v16) | ( ~ (v17 = 0) & subset(v16, v14) = v17 & relation_rng(v15) = v16) | ( ~ (v16 = 0) & function(v15) = v16))) & ! [v15] : ( ~ (function(v15) = 0) | ? [v16] : ? [v17] : ((v16 = 0 & one_to_one(v15) = 0) | ( ~ (v17 = 0) & one_to_one(v16) = v17 & relation_composition(v15, v13) = v16) | ( ~ (v17 = 0) & subset(v16, v14) = v17 & relation_rng(v15) = v16) | ( ~ (v16 = 0) & relation(v15) = v16)))))) & ! [v13] : ( ~ (relation(v13) = 0) | ? [v14] : (( ~ (v14 = 0) & function(v13) = v14) | (relation_dom(v13) = v14 & ! [v15] : ! [v16] : ( ~ (relation_rng(v15) = v16) | ? [v17] : ? [v18] : ? [v19] : ((v17 = 0 & subset(v16, v14) = 0) | ( ~ (v19 = v18) & relation_dom(v17) = v18 & relation_dom(v15) = v19 & relation_composition(v15, v13) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ! [v16] : ( ~ (relation_dom(v15) = v16) | ? [v17] : ? [v18] : ((v18 = 0 & subset(v17, v14) = 0 & relation_rng(v15) = v17) | ( ~ (v18 = v16) & relation_dom(v17) = v18 & relation_composition(v15, v13) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ! [v16] : ( ~ (relation_composition(v15, v13) = v16) | ? [v17] : ? [v18] : ((v18 = 0 & subset(v17, v14) = 0 & relation_rng(v15) = v17) | ( ~ (v18 = v17) & relation_dom(v16) = v17 & relation_dom(v15) = v18) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ( ~ (relation(v15) = 0) | ? [v16] : ? [v17] : ? [v18] : ((v17 = 0 & subset(v16, v14) = 0 & relation_rng(v15) = v16) | ( ~ (v18 = v17) & relation_dom(v16) = v17 & relation_dom(v15) = v18 & relation_composition(v15, v13) = v16) | ( ~ (v16 = 0) & function(v15) = v16))) & ! [v15] : ( ~ (function(v15) = 0) | ? [v16] : ? [v17] : ? [v18] : ((v17 = 0 & subset(v16, v14) = 0 & relation_rng(v15) = v16) | ( ~ (v18 = v17) & relation_dom(v16) = v17 & relation_dom(v15) = v18 & relation_composition(v15, v13) = v16) | ( ~ (v16 = 0) & relation(v15) = v16)))))) & ! [v13] : ( ~ (function(v13) = 0) | ? [v14] : (( ~ (v14 = 0) & relation(v13) = v14) | (relation_dom(v13) = v14 & ! [v15] : ! [v16] : (v16 = 0 | ~ (one_to_one(v15) = v16) | ? [v17] : ? [v18] : (( ~ (v18 = 0) & one_to_one(v17) = v18 & relation_composition(v15, v13) = v17) | ( ~ (v18 = 0) & subset(v17, v14) = v18 & relation_rng(v15) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ! [v16] : ( ~ (relation_rng(v15) = v16) | ? [v17] : ? [v18] : ((v17 = 0 & one_to_one(v15) = 0) | ( ~ (v18 = 0) & one_to_one(v17) = v18 & relation_composition(v15, v13) = v17) | ( ~ (v17 = 0) & subset(v16, v14) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ! [v16] : ( ~ (relation_composition(v15, v13) = v16) | ? [v17] : ? [v18] : ((v17 = 0 & one_to_one(v15) = 0) | ( ~ (v18 = 0) & subset(v17, v14) = v18 & relation_rng(v15) = v17) | ( ~ (v17 = 0) & one_to_one(v16) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ( ~ (relation(v15) = 0) | ? [v16] : ? [v17] : ((v16 = 0 & one_to_one(v15) = 0) | ( ~ (v17 = 0) & one_to_one(v16) = v17 & relation_composition(v15, v13) = v16) | ( ~ (v17 = 0) & subset(v16, v14) = v17 & relation_rng(v15) = v16) | ( ~ (v16 = 0) & function(v15) = v16))) & ! [v15] : ( ~ (function(v15) = 0) | ? [v16] : ? [v17] : ((v16 = 0 & one_to_one(v15) = 0) | ( ~ (v17 = 0) & one_to_one(v16) = v17 & relation_composition(v15, v13) = v16) | ( ~ (v17 = 0) & subset(v16, v14) = v17 & relation_rng(v15) = v16) | ( ~ (v16 = 0) & relation(v15) = v16)))))) & ! [v13] : ( ~ (function(v13) = 0) | ? [v14] : (( ~ (v14 = 0) & relation(v13) = v14) | (relation_dom(v13) = v14 & ! [v15] : ! [v16] : ( ~ (relation_rng(v15) = v16) | ? [v17] : ? [v18] : ? [v19] : ((v17 = 0 & subset(v16, v14) = 0) | ( ~ (v19 = v18) & relation_dom(v17) = v18 & relation_dom(v15) = v19 & relation_composition(v15, v13) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ! [v16] : ( ~ (relation_dom(v15) = v16) | ? [v17] : ? [v18] : ((v18 = 0 & subset(v17, v14) = 0 & relation_rng(v15) = v17) | ( ~ (v18 = v16) & relation_dom(v17) = v18 & relation_composition(v15, v13) = v17) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ! [v16] : ( ~ (relation_composition(v15, v13) = v16) | ? [v17] : ? [v18] : ((v18 = 0 & subset(v17, v14) = 0 & relation_rng(v15) = v17) | ( ~ (v18 = v17) & relation_dom(v16) = v17 & relation_dom(v15) = v18) | ( ~ (v17 = 0) & relation(v15) = v17) | ( ~ (v17 = 0) & function(v15) = v17))) & ! [v15] : ( ~ (relation(v15) = 0) | ? [v16] : ? [v17] : ? [v18] : ((v17 = 0 & subset(v16, v14) = 0 & relation_rng(v15) = v16) | ( ~ (v18 = v17) & relation_dom(v16) = v17 & relation_dom(v15) = v18 & relation_composition(v15, v13) = v16) | ( ~ (v16 = 0) & function(v15) = v16))) & ! [v15] : ( ~ (function(v15) = 0) | ? [v16] : ? [v17] : ? [v18] : ((v17 = 0 & subset(v16, v14) = 0 & relation_rng(v15) = v16) | ( ~ (v18 = v17) & relation_dom(v16) = v17 & relation_dom(v15) = v18 & relation_composition(v15, v13) = v16) | ( ~ (v16 = 0) & relation(v15) = v16)))))) & ! [v13] : ( ~ (empty(v13) = 0) | relation(v13) = 0) & ! [v13] : ( ~ (empty(v13) = 0) | function(v13) = 0) & ! [v13] : ( ~ (empty(v13) = 0) | ? [v14] : (relation_rng(v13) = v14 & relation(v14) = 0 & empty(v14) = 0)) & ! [v13] : ( ~ (empty(v13) = 0) | ? [v14] : (relation_dom(v13) = v14 & relation(v14) = 0 & empty(v14) = 0)) & ? [v13] : ? [v14] : ? [v15] : subset(v14, v13) = v15 & ? [v13] : ? [v14] : ? [v15] : element(v14, v13) = v15 & ? [v13] : ? [v14] : ? [v15] : relation_composition(v14, v13) = v15 & ? [v13] : ? [v14] : ? [v15] : in(v14, v13) = v15 & ? [v13] : ? [v14] : one_to_one(v13) = v14 & ? [v13] : ? [v14] : relation_empty_yielding(v13) = v14 & ? [v13] : ? [v14] : relation_rng(v13) = v14 & ? [v13] : ? [v14] : relation_dom(v13) = v14 & ? [v13] : ? [v14] : powerset(v13) = v14 & ? [v13] : ? [v14] : element(v14, v13) = 0 & ? [v13] : ? [v14] : identity_relation(v13) = v14 & ? [v13] : ? [v14] : relation(v13) = v14 & ? [v13] : ? [v14] : function(v13) = v14 & ? [v13] : ? [v14] : empty(v13) = v14) % 50.29/21.25 | 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 yields: % 50.29/21.25 | (1) ~ (all_0_3_3 = 0) & ~ (all_0_5_5 = 0) & ~ (all_0_9_9 = 0) & one_to_one(all_0_12_12) = all_0_9_9 & relation_empty_yielding(all_0_7_7) = 0 & relation_empty_yielding(empty_set) = 0 & relation_dom(all_0_12_12) = all_0_11_11 & identity_relation(all_0_11_11) = all_0_10_10 & relation_composition(all_0_12_12, all_0_8_8) = all_0_10_10 & relation(all_0_0_0) = 0 & relation(all_0_1_1) = 0 & relation(all_0_4_4) = 0 & relation(all_0_7_7) = 0 & relation(all_0_8_8) = 0 & relation(all_0_12_12) = 0 & relation(empty_set) = 0 & function(all_0_0_0) = 0 & function(all_0_8_8) = 0 & function(all_0_12_12) = 0 & empty(all_0_1_1) = 0 & empty(all_0_2_2) = 0 & empty(all_0_4_4) = all_0_3_3 & empty(all_0_6_6) = all_0_5_5 & empty(empty_set) = 0 & ! [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] : (v3 = 0 | ~ (one_to_one(v2) = v3) | ~ (relation_dom(v0) = v1) | ? [v4] : ? [v5] : (( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) & ! [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] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (relation_composition(v3, v2) = v1) | ~ (relation_composition(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ~ (relation_dom(v0) = v1) | ? [v4] : ? [v5] : ? [v6] : ((v4 = 0 & subset(v3, v1) = 0) | ( ~ (v6 = v5) & relation_dom(v4) = v5 & relation_dom(v2) = v6 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ~ (relation_dom(v0) = v1) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & subset(v3, v1) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (relation_dom(v2) = v3) | ~ (relation_dom(v0) = v1) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v3) & relation_dom(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (relation_dom(v0) = v1) | ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (relation_dom(v0) = v1) | ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & one_to_one(v3) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) & ! [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 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v1) = v3 & element(v0, v3) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (element(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & in(v0, v1) = v3)) & ! [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 | ~ (one_to_one(v2) = v1) | ~ (one_to_one(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_empty_yielding(v2) = v1) | ~ (relation_empty_yielding(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_rng(v2) = v1) | ~ (relation_rng(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_dom(v2) = v1) | ~ (relation_dom(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (identity_relation(v2) = v1) | ~ (identity_relation(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation(v2) = v1) | ~ (relation(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] : ( ~ (relation_dom(v0) = v1) | ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v0) = v3) | ( ~ (v3 = 0) & function(v2) = v3) | ( ~ (v3 = 0) & function(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_dom(v0) = v1) | ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & relation(v0) = v3) | ( ~ (v3 = 0) & function(v2) = v3) | ( ~ (v3 = 0) & function(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_dom(v0) = v1) | ~ (function(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v2) = v3) | ( ~ (v3 = 0) & relation(v0) = v3) | ( ~ (v3 = 0) & function(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_dom(v0) = v1) | ~ (function(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & relation(v2) = v3) | ( ~ (v3 = 0) & relation(v0) = v3) | ( ~ (v3 = 0) & function(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ (element(v0, v2) = 0) | subset(v0, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_composition(v1, v0) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & relation(v2) = 0 & empty(v2) = 0) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & empty(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_composition(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & relation(v2) = 0 & function(v2) = 0) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & relation(v0) = v3) | ( ~ (v3 = 0) & function(v1) = v3) | ( ~ (v3 = 0) & function(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_composition(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & relation(v2) = 0 & empty(v2) = 0) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & empty(v0) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_composition(v0, v1) = v2) | ? [v3] : ((v3 = 0 & relation(v2) = 0) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & relation(v0) = 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 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (relation(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v0) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (function(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v0) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v0) = v2 & element(v3, v2) = 0 & empty(v3) = v4)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & relation_rng(v0) = v2 & empty(v2) = v3) | ( ~ (v2 = 0) & relation(v0) = v2))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & relation_dom(v0) = v2 & empty(v2) = v3) | ( ~ (v2 = 0) & relation(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (subset(v0, v1) = 0) | ? [v2] : (powerset(v1) = v2 & element(v0, v2) = 0)) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & relation(v1) = 0 & empty(v1) = 0) | ( ~ (v2 = 0) & empty(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ((v2 = 0 & empty(v0) = 0) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & empty(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & relation(v1) = 0 & empty(v1) = 0) | ( ~ (v2 = 0) & empty(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ((v2 = 0 & empty(v0) = 0) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & empty(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & ~ (v4 = 0) & element(v2, v1) = 0 & empty(v2) = v4) | (v2 = 0 & empty(v0) = 0))) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) & ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : (element(v2, v1) = 0 & empty(v2) = 0)) & ! [v0] : ! [v1] : ( ~ (element(v0, v1) = 0) | ? [v2] : ((v2 = 0 & empty(v1) = 0) | (v2 = 0 & in(v0, v1) = 0))) & ! [v0] : ! [v1] : ( ~ (identity_relation(v0) = v1) | one_to_one(v1) = 0) & ! [v0] : ! [v1] : ( ~ (identity_relation(v0) = v1) | relation_rng(v1) = v0) & ! [v0] : ! [v1] : ( ~ (identity_relation(v0) = v1) | relation_dom(v1) = v0) & ! [v0] : ! [v1] : ( ~ (identity_relation(v0) = v1) | relation(v1) = 0) & ! [v0] : ! [v1] : ( ~ (identity_relation(v0) = v1) | function(v1) = 0) & ! [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] : ((v1 = 0 & empty(v0) = 0) | ( ~ (v2 = 0) & relation_rng(v0) = v1 & empty(v1) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & empty(v0) = 0) | ( ~ (v2 = 0) & relation_dom(v0) = v1 & empty(v1) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & function(v0) = v1) | (relation_dom(v0) = v1 & ! [v2] : ! [v3] : (v3 = 0 | ~ (one_to_one(v2) = v3) | ? [v4] : ? [v5] : (( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & subset(v3, v1) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & one_to_one(v3) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ( ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & function(v2) = v3))) & ! [v2] : ( ~ (function(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & relation(v2) = v3)))))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & function(v0) = v1) | (relation_dom(v0) = v1 & ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ((v4 = 0 & subset(v3, v1) = 0) | ( ~ (v6 = v5) & relation_dom(v4) = v5 & relation_dom(v2) = v6 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_dom(v2) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v3) & relation_dom(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ( ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & function(v2) = v3))) & ! [v2] : ( ~ (function(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v2) = v3)))))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & relation(v0) = v1) | (relation_dom(v0) = v1 & ! [v2] : ! [v3] : (v3 = 0 | ~ (one_to_one(v2) = v3) | ? [v4] : ? [v5] : (( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & subset(v3, v1) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & one_to_one(v3) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ( ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & function(v2) = v3))) & ! [v2] : ( ~ (function(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & relation(v2) = v3)))))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & relation(v0) = v1) | (relation_dom(v0) = v1 & ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ((v4 = 0 & subset(v3, v1) = 0) | ( ~ (v6 = v5) & relation_dom(v4) = v5 & relation_dom(v2) = v6 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_dom(v2) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v3) & relation_dom(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ( ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & function(v2) = v3))) & ! [v2] : ( ~ (function(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v2) = v3)))))) & ! [v0] : ( ~ (empty(v0) = 0) | relation(v0) = 0) & ! [v0] : ( ~ (empty(v0) = 0) | function(v0) = 0) & ! [v0] : ( ~ (empty(v0) = 0) | ? [v1] : (relation_rng(v0) = v1 & relation(v1) = 0 & empty(v1) = 0)) & ! [v0] : ( ~ (empty(v0) = 0) | ? [v1] : (relation_dom(v0) = v1 & relation(v1) = 0 & empty(v1) = 0)) & ? [v0] : ? [v1] : ? [v2] : subset(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : element(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : relation_composition(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : in(v1, v0) = v2 & ? [v0] : ? [v1] : one_to_one(v0) = v1 & ? [v0] : ? [v1] : relation_empty_yielding(v0) = v1 & ? [v0] : ? [v1] : relation_rng(v0) = v1 & ? [v0] : ? [v1] : relation_dom(v0) = v1 & ? [v0] : ? [v1] : powerset(v0) = v1 & ? [v0] : ? [v1] : element(v1, v0) = 0 & ? [v0] : ? [v1] : identity_relation(v0) = v1 & ? [v0] : ? [v1] : relation(v0) = v1 & ? [v0] : ? [v1] : function(v0) = v1 & ? [v0] : ? [v1] : empty(v0) = v1 % 50.29/21.27 | % 50.29/21.27 | Applying alpha-rule on (1) yields: % 50.29/21.27 | (2) ! [v0] : ! [v1] : (v1 = 0 | ~ (relation(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v0) = v2)) % 50.29/21.27 | (3) relation(all_0_4_4) = 0 % 50.29/21.27 | (4) ! [v0] : ! [v1] : ! [v2] : ( ~ (powerset(v1) = v2) | ~ (element(v0, v2) = 0) | subset(v0, v1) = 0) % 50.29/21.28 | (5) ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_composition(v1, v0) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & relation(v2) = 0 & empty(v2) = 0) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & empty(v0) = v3))) % 50.29/21.28 | (6) ! [v0] : ! [v1] : (v1 = 0 | ~ (subset(v0, v0) = v1)) % 50.29/21.28 | (7) relation(all_0_0_0) = 0 % 50.29/21.28 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) % 50.29/21.28 | (9) ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & relation(v1) = 0 & empty(v1) = 0) | ( ~ (v2 = 0) & empty(v0) = v2))) % 50.29/21.28 | (10) ! [v0] : ! [v1] : (v1 = v0 | ~ (empty(v1) = 0) | ~ (empty(v0) = 0)) % 50.29/21.28 | (11) ! [v0] : ! [v1] : ( ~ (element(v0, v1) = 0) | ? [v2] : ((v2 = 0 & empty(v1) = 0) | (v2 = 0 & in(v0, v1) = 0))) % 50.29/21.28 | (12) ? [v0] : ? [v1] : relation_empty_yielding(v0) = v1 % 50.29/21.28 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_rng(v2) = v1) | ~ (relation_rng(v2) = v0)) % 50.29/21.28 | (14) ! [v0] : ! [v1] : (v1 = 0 | ~ (function(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v0) = v2)) % 50.29/21.28 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (relation_composition(v3, v2) = v1) | ~ (relation_composition(v3, v2) = v0)) % 50.29/21.28 | (16) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ((v2 = 0 & empty(v0) = 0) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & empty(v1) = v2))) % 50.29/21.28 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ (empty(v2) = 0) | ~ (in(v0, v1) = 0) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v2) = v3 & element(v1, v3) = v4)) % 50.29/21.28 | (18) ! [v0] : ! [v1] : ( ~ (identity_relation(v0) = v1) | relation(v1) = 0) % 50.29/21.28 | (19) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (one_to_one(v2) = v1) | ~ (one_to_one(v2) = v0)) % 50.29/21.28 | (20) ! [v0] : ! [v1] : ( ~ (identity_relation(v0) = v1) | function(v1) = 0) % 50.29/21.28 | (21) ? [v0] : ? [v1] : relation_dom(v0) = v1 % 50.29/21.28 | (22) ! [v0] : ! [v1] : ( ~ (identity_relation(v0) = v1) | one_to_one(v1) = 0) % 50.29/21.28 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_empty_yielding(v2) = v1) | ~ (relation_empty_yielding(v2) = v0)) % 50.29/21.28 | (24) ! [v0] : ! [v1] : ( ~ (identity_relation(v0) = v1) | relation_rng(v1) = v0) % 50.29/21.28 | (25) ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_dom(v0) = v1) | ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v0) = v3) | ( ~ (v3 = 0) & function(v2) = v3) | ( ~ (v3 = 0) & function(v0) = v3))) % 50.29/21.28 | (26) ! [v0] : ! [v1] : ( ~ (identity_relation(v0) = v1) | relation_dom(v1) = v0) % 50.29/21.28 | (27) relation_empty_yielding(empty_set) = 0 % 50.29/21.28 | (28) ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ((v2 = 0 & empty(v0) = 0) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & empty(v1) = v2))) % 50.29/21.28 | (29) ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_composition(v0, v1) = v2) | ? [v3] : ((v3 = 0 & relation(v2) = 0) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & relation(v0) = v3))) % 50.29/21.28 | (30) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v1, v0) = v2)) % 50.29/21.28 | (31) ! [v0] : ( ~ (empty(v0) = 0) | ? [v1] : (relation_dom(v0) = v1 & relation(v1) = 0 & empty(v1) = 0)) % 50.29/21.28 | (32) empty(all_0_4_4) = all_0_3_3 % 50.29/21.28 | (33) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) % 50.29/21.28 | (34) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & function(v0) = v1) | (relation_dom(v0) = v1 & ! [v2] : ! [v3] : (v3 = 0 | ~ (one_to_one(v2) = v3) | ? [v4] : ? [v5] : (( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & subset(v3, v1) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & one_to_one(v3) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ( ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & function(v2) = v3))) & ! [v2] : ( ~ (function(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & relation(v2) = v3)))))) % 50.29/21.29 | (35) ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_dom(v0) = v1) | ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & relation(v0) = v3) | ( ~ (v3 = 0) & function(v2) = v3) | ( ~ (v3 = 0) & function(v0) = v3))) % 50.29/21.29 | (36) relation(all_0_1_1) = 0 % 50.29/21.29 | (37) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & ~ (v4 = 0) & element(v2, v1) = 0 & empty(v2) = v4) | (v2 = 0 & empty(v0) = 0))) % 50.29/21.29 | (38) relation_composition(all_0_12_12, all_0_8_8) = all_0_10_10 % 50.29/21.29 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (one_to_one(v2) = v3) | ~ (relation_dom(v0) = v1) | ? [v4] : ? [v5] : (( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) % 50.29/21.29 | (40) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v1) = v3 & element(v0, v3) = v4)) % 50.29/21.29 | (41) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & relation(v0) = v1) | (relation_dom(v0) = v1 & ! [v2] : ! [v3] : (v3 = 0 | ~ (one_to_one(v2) = v3) | ? [v4] : ? [v5] : (( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & subset(v3, v1) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & one_to_one(v3) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ( ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & function(v2) = v3))) & ! [v2] : ( ~ (function(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & relation(v2) = v3)))))) % 50.29/21.29 | (42) identity_relation(all_0_11_11) = all_0_10_10 % 50.29/21.29 | (43) ? [v0] : ? [v1] : relation_rng(v0) = v1 % 50.29/21.29 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) % 50.29/21.29 | (45) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & empty(v0) = 0) | ( ~ (v2 = 0) & relation_dom(v0) = v1 & empty(v1) = v2))) % 50.29/21.29 | (46) ? [v0] : ? [v1] : ? [v2] : relation_composition(v1, v0) = v2 % 50.29/21.29 | (47) ! [v0] : ( ~ (empty(v0) = 0) | relation(v0) = 0) % 50.29/21.29 | (48) empty(all_0_6_6) = all_0_5_5 % 50.29/21.29 | (49) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (element(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & in(v0, v1) = v3)) % 50.29/21.29 | (50) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & empty(v1) = v2)) % 50.29/21.29 | (51) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (in(v0, v1) = v2) | ? [v3] : ((v3 = 0 & empty(v1) = 0) | ( ~ (v3 = 0) & element(v0, v1) = v3))) % 50.29/21.29 | (52) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & empty(v2) = v4)) % 50.29/21.29 | (53) relation_dom(all_0_12_12) = all_0_11_11 % 50.29/21.29 | (54) ~ (all_0_3_3 = 0) % 50.29/21.29 | (55) ! [v0] : ! [v1] : ( ~ (in(v0, v1) = 0) | element(v0, v1) = 0) % 50.29/21.29 | (56) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & relation(v0) = v1) | (relation_dom(v0) = v1 & ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ((v4 = 0 & subset(v3, v1) = 0) | ( ~ (v6 = v5) & relation_dom(v4) = v5 & relation_dom(v2) = v6 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_dom(v2) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v3) & relation_dom(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ( ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & function(v2) = v3))) & ! [v2] : ( ~ (function(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v2) = v3)))))) % 50.29/21.30 | (57) ! [v0] : ( ~ (empty(v0) = 0) | ? [v1] : (relation_rng(v0) = v1 & relation(v1) = 0 & empty(v1) = 0)) % 50.29/21.30 | (58) empty(all_0_2_2) = 0 % 50.29/21.30 | (59) ? [v0] : ? [v1] : ? [v2] : element(v1, v0) = v2 % 50.29/21.30 | (60) function(all_0_0_0) = 0 % 50.29/21.30 | (61) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (identity_relation(v2) = v1) | ~ (identity_relation(v2) = v0)) % 50.29/21.30 | (62) ? [v0] : ? [v1] : element(v1, v0) = 0 % 50.29/21.30 | (63) ! [v0] : ! [v1] : ( ~ (powerset(v0) = v1) | ? [v2] : (element(v2, v1) = 0 & empty(v2) = 0)) % 50.29/21.30 | (64) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & empty(v0) = 0) | ( ~ (v2 = 0) & relation_rng(v0) = v1 & empty(v1) = v2))) % 50.29/21.30 | (65) ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & relation_rng(v0) = v2 & empty(v2) = v3) | ( ~ (v2 = 0) & relation(v0) = v2))) % 50.29/21.30 | (66) ! [v0] : ( ~ (empty(v0) = 0) | function(v0) = 0) % 50.29/21.30 | (67) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) % 50.29/21.30 | (68) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation(v2) = v1) | ~ (relation(v2) = v0)) % 50.67/21.30 | (69) function(all_0_12_12) = 0 % 50.67/21.30 | (70) ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_dom(v0) = v1) | ~ (function(v2) = 0) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v2) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v2, v0) = v3) | ( ~ (v4 = 0) & subset(v3, v1) = v4 & relation_rng(v2) = v3) | ( ~ (v3 = 0) & relation(v2) = v3) | ( ~ (v3 = 0) & relation(v0) = v3) | ( ~ (v3 = 0) & function(v0) = v3))) % 50.67/21.30 | (71) ~ (all_0_9_9 = 0) % 50.67/21.30 | (72) ? [v0] : ? [v1] : ? [v2] : subset(v1, v0) = v2 % 50.67/21.30 | (73) ? [v0] : ? [v1] : identity_relation(v0) = v1 % 50.67/21.30 | (74) ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_composition(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & relation(v2) = 0 & empty(v2) = 0) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & empty(v0) = v3))) % 50.67/21.30 | (75) relation(all_0_8_8) = 0 % 50.67/21.30 | (76) ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_dom(v0) = v1) | ~ (function(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v2) = v3) | ( ~ (v3 = 0) & relation(v0) = v3) | ( ~ (v3 = 0) & function(v0) = v3))) % 50.67/21.30 | (77) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & v2 = 0 & relation(v1) = 0 & empty(v1) = 0) | ( ~ (v2 = 0) & empty(v0) = v2))) % 50.67/21.30 | (78) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) % 50.67/21.30 | (79) ? [v0] : ? [v1] : powerset(v0) = v1 % 50.67/21.30 | (80) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) % 50.67/21.30 | (81) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (relation_dom(v2) = v3) | ~ (relation_dom(v0) = v1) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v3) & relation_dom(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) % 50.67/21.30 | (82) one_to_one(all_0_12_12) = all_0_9_9 % 50.67/21.30 | (83) ? [v0] : ? [v1] : relation(v0) = v1 % 50.67/21.31 | (84) relation(all_0_7_7) = 0 % 50.67/21.31 | (85) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (relation_dom(v0) = v1) | ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & subset(v4, v1) = v5 & relation_rng(v2) = v4) | ( ~ (v4 = 0) & one_to_one(v3) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) % 50.67/21.31 | (86) empty(empty_set) = 0 % 50.67/21.31 | (87) ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & relation_dom(v0) = v2 & empty(v2) = v3) | ( ~ (v2 = 0) & relation(v0) = v2))) % 50.67/21.31 | (88) ! [v0] : ! [v1] : ( ~ (in(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & in(v0, v1) = v2)) % 50.67/21.31 | (89) ! [v0] : (v0 = empty_set | ~ (empty(v0) = 0)) % 50.67/21.31 | (90) relation(empty_set) = 0 % 50.67/21.31 | (91) function(all_0_8_8) = 0 % 50.67/21.31 | (92) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ~ (relation_dom(v0) = v1) | ? [v4] : ? [v5] : ((v4 = 0 & one_to_one(v2) = 0) | ( ~ (v5 = 0) & one_to_one(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & subset(v3, v1) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) % 50.67/21.31 | (93) ! [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)) % 50.67/21.31 | (94) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (powerset(v2) = v3) | ~ (element(v1, v3) = 0) | ~ (in(v0, v1) = 0) | element(v0, v2) = 0) % 50.67/21.31 | (95) empty(all_0_1_1) = 0 % 50.67/21.31 | (96) relation_empty_yielding(all_0_7_7) = 0 % 50.67/21.31 | (97) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (function(v2) = v1) | ~ (function(v2) = v0)) % 50.67/21.31 | (98) ! [v0] : ! [v1] : ( ~ (subset(v0, v1) = 0) | ? [v2] : (powerset(v1) = v2 & element(v0, v2) = 0)) % 50.67/21.31 | (99) relation(all_0_12_12) = 0 % 50.67/21.31 | (100) ! [v0] : ! [v1] : (v1 = 0 | ~ (empty(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & powerset(v0) = v2 & element(v3, v2) = 0 & empty(v3) = v4)) % 50.67/21.31 | (101) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (relation_dom(v0) = v1) | ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) % 50.67/21.31 | (102) ~ (all_0_5_5 = 0) % 50.67/21.31 | (103) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : (( ~ (v1 = 0) & function(v0) = v1) | (relation_dom(v0) = v1 & ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ((v4 = 0 & subset(v3, v1) = 0) | ( ~ (v6 = v5) & relation_dom(v4) = v5 & relation_dom(v2) = v6 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_dom(v2) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v3) & relation_dom(v4) = v5 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ! [v3] : ( ~ (relation_composition(v2, v0) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & subset(v4, v1) = 0 & relation_rng(v2) = v4) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & function(v2) = v4))) & ! [v2] : ( ~ (relation(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & function(v2) = v3))) & ! [v2] : ( ~ (function(v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v4 = 0 & subset(v3, v1) = 0 & relation_rng(v2) = v3) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v2) = v5 & relation_composition(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v2) = v3)))))) % 50.67/21.31 | (104) ! [v0] : ! [v1] : ! [v2] : ( ~ (relation_composition(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & relation(v2) = 0 & function(v2) = 0) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & relation(v0) = v3) | ( ~ (v3 = 0) & function(v1) = v3) | ( ~ (v3 = 0) & function(v0) = v3))) % 50.67/21.31 | (105) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (relation_dom(v2) = v1) | ~ (relation_dom(v2) = v0)) % 50.67/21.31 | (106) ? [v0] : ? [v1] : function(v0) = v1 % 50.67/21.32 | (107) ? [v0] : ? [v1] : one_to_one(v0) = v1 % 50.67/21.32 | (108) ! [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)) % 50.67/21.32 | (109) ? [v0] : ? [v1] : empty(v0) = v1 % 50.67/21.32 | (110) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (relation_rng(v2) = v3) | ~ (relation_dom(v0) = v1) | ? [v4] : ? [v5] : ? [v6] : ((v4 = 0 & subset(v3, v1) = 0) | ( ~ (v6 = v5) & relation_dom(v4) = v5 & relation_dom(v2) = v6 & relation_composition(v2, v0) = v4) | ( ~ (v4 = 0) & relation(v2) = v4) | ( ~ (v4 = 0) & relation(v0) = v4) | ( ~ (v4 = 0) & function(v2) = v4) | ( ~ (v4 = 0) & function(v0) = v4))) % 50.67/21.32 | (111) ? [v0] : ? [v1] : ? [v2] : in(v1, v0) = v2 % 50.67/21.32 | (112) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (powerset(v1) = v2) | ~ (element(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & subset(v0, v1) = v4)) % 50.67/21.32 | % 50.67/21.32 | Instantiating formula (39) with all_0_9_9, all_0_12_12, all_0_11_11, all_0_12_12 and discharging atoms one_to_one(all_0_12_12) = all_0_9_9, relation_dom(all_0_12_12) = all_0_11_11, yields: % 50.67/21.32 | (113) all_0_9_9 = 0 | ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_12_12) = v0) | ( ~ (v1 = 0) & subset(v0, all_0_11_11) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 50.67/21.32 | % 50.67/21.32 | Instantiating formula (22) with all_0_10_10, all_0_11_11 and discharging atoms identity_relation(all_0_11_11) = all_0_10_10, yields: % 50.67/21.32 | (114) one_to_one(all_0_10_10) = 0 % 50.67/21.32 | % 50.67/21.32 | Instantiating formula (26) with all_0_10_10, all_0_11_11 and discharging atoms identity_relation(all_0_11_11) = all_0_10_10, yields: % 50.67/21.32 | (115) relation_dom(all_0_10_10) = all_0_11_11 % 50.67/21.32 | % 50.67/21.32 | Instantiating formula (34) with all_0_0_0 and discharging atoms relation(all_0_0_0) = 0, yields: % 50.67/21.32 | (116) ? [v0] : (( ~ (v0 = 0) & function(all_0_0_0) = v0) | (relation_dom(all_0_0_0) = v0 & ! [v1] : ! [v2] : (v2 = 0 | ~ (one_to_one(v1) = v2) | ? [v3] : ? [v4] : (( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_0_0) = v3) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_rng(v1) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_0_0) = v3) | ( ~ (v3 = 0) & subset(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_composition(v1, all_0_0_0) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & one_to_one(v2) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ( ~ (relation(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_0_0) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & function(v1) = v2))) & ! [v1] : ( ~ (function(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_0_0) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & relation(v1) = v2))))) % 50.67/21.32 | % 50.67/21.32 | Instantiating formula (34) with all_0_8_8 and discharging atoms relation(all_0_8_8) = 0, yields: % 50.67/21.32 | (117) ? [v0] : (( ~ (v0 = 0) & function(all_0_8_8) = v0) | (relation_dom(all_0_8_8) = v0 & ! [v1] : ! [v2] : (v2 = 0 | ~ (one_to_one(v1) = v2) | ? [v3] : ? [v4] : (( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_8_8) = v3) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_rng(v1) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_8_8) = v3) | ( ~ (v3 = 0) & subset(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_composition(v1, all_0_8_8) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & one_to_one(v2) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ( ~ (relation(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_8_8) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & function(v1) = v2))) & ! [v1] : ( ~ (function(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_8_8) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & relation(v1) = v2))))) % 50.67/21.33 | % 50.67/21.33 | Instantiating formula (103) with all_0_8_8 and discharging atoms relation(all_0_8_8) = 0, yields: % 50.67/21.33 | (118) ? [v0] : (( ~ (v0 = 0) & function(all_0_8_8) = v0) | (relation_dom(all_0_8_8) = v0 & ! [v1] : ! [v2] : ( ~ (relation_rng(v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ((v3 = 0 & subset(v2, v0) = 0) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v1) = v5 & relation_composition(v1, all_0_8_8) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_dom(v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & subset(v3, v0) = 0 & relation_rng(v1) = v3) | ( ~ (v4 = v2) & relation_dom(v3) = v4 & relation_composition(v1, all_0_8_8) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_composition(v1, all_0_8_8) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & subset(v3, v0) = 0 & relation_rng(v1) = v3) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v1) = v4) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ( ~ (relation(v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & subset(v2, v0) = 0 & relation_rng(v1) = v2) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v1) = v4 & relation_composition(v1, all_0_8_8) = v2) | ( ~ (v2 = 0) & function(v1) = v2))) & ! [v1] : ( ~ (function(v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & subset(v2, v0) = 0 & relation_rng(v1) = v2) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v1) = v4 & relation_composition(v1, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v1) = v2))))) % 50.67/21.33 | % 50.67/21.33 | Instantiating formula (34) with all_0_12_12 and discharging atoms relation(all_0_12_12) = 0, yields: % 50.67/21.33 | (119) ? [v0] : (( ~ (v0 = 0) & function(all_0_12_12) = v0) | (relation_dom(all_0_12_12) = v0 & ! [v1] : ! [v2] : (v2 = 0 | ~ (one_to_one(v1) = v2) | ? [v3] : ? [v4] : (( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_12_12) = v3) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_rng(v1) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_12_12) = v3) | ( ~ (v3 = 0) & subset(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_composition(v1, all_0_12_12) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & one_to_one(v2) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ( ~ (relation(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_12_12) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & function(v1) = v2))) & ! [v1] : ( ~ (function(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_12_12) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & relation(v1) = v2))))) % 50.67/21.33 | % 50.67/21.33 | Instantiating formula (41) with all_0_0_0 and discharging atoms function(all_0_0_0) = 0, yields: % 50.67/21.33 | (120) ? [v0] : (( ~ (v0 = 0) & relation(all_0_0_0) = v0) | (relation_dom(all_0_0_0) = v0 & ! [v1] : ! [v2] : (v2 = 0 | ~ (one_to_one(v1) = v2) | ? [v3] : ? [v4] : (( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_0_0) = v3) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_rng(v1) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_0_0) = v3) | ( ~ (v3 = 0) & subset(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_composition(v1, all_0_0_0) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & one_to_one(v2) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ( ~ (relation(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_0_0) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & function(v1) = v2))) & ! [v1] : ( ~ (function(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_0_0) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & relation(v1) = v2))))) % 50.67/21.34 | % 50.67/21.34 | Instantiating formula (41) with all_0_8_8 and discharging atoms function(all_0_8_8) = 0, yields: % 50.67/21.34 | (121) ? [v0] : (( ~ (v0 = 0) & relation(all_0_8_8) = v0) | (relation_dom(all_0_8_8) = v0 & ! [v1] : ! [v2] : (v2 = 0 | ~ (one_to_one(v1) = v2) | ? [v3] : ? [v4] : (( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_8_8) = v3) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_rng(v1) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_8_8) = v3) | ( ~ (v3 = 0) & subset(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_composition(v1, all_0_8_8) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & one_to_one(v2) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ( ~ (relation(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_8_8) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & function(v1) = v2))) & ! [v1] : ( ~ (function(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_8_8) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & relation(v1) = v2))))) % 50.67/21.34 | % 50.67/21.34 | Instantiating formula (56) with all_0_8_8 and discharging atoms function(all_0_8_8) = 0, yields: % 50.67/21.34 | (122) ? [v0] : (( ~ (v0 = 0) & relation(all_0_8_8) = v0) | (relation_dom(all_0_8_8) = v0 & ! [v1] : ! [v2] : ( ~ (relation_rng(v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ((v3 = 0 & subset(v2, v0) = 0) | ( ~ (v5 = v4) & relation_dom(v3) = v4 & relation_dom(v1) = v5 & relation_composition(v1, all_0_8_8) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_dom(v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & subset(v3, v0) = 0 & relation_rng(v1) = v3) | ( ~ (v4 = v2) & relation_dom(v3) = v4 & relation_composition(v1, all_0_8_8) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_composition(v1, all_0_8_8) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & subset(v3, v0) = 0 & relation_rng(v1) = v3) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v1) = v4) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ( ~ (relation(v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & subset(v2, v0) = 0 & relation_rng(v1) = v2) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v1) = v4 & relation_composition(v1, all_0_8_8) = v2) | ( ~ (v2 = 0) & function(v1) = v2))) & ! [v1] : ( ~ (function(v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v3 = 0 & subset(v2, v0) = 0 & relation_rng(v1) = v2) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v1) = v4 & relation_composition(v1, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v1) = v2))))) % 50.67/21.34 | % 50.67/21.34 | Instantiating formula (41) with all_0_12_12 and discharging atoms function(all_0_12_12) = 0, yields: % 50.67/21.34 | (123) ? [v0] : (( ~ (v0 = 0) & relation(all_0_12_12) = v0) | (relation_dom(all_0_12_12) = v0 & ! [v1] : ! [v2] : (v2 = 0 | ~ (one_to_one(v1) = v2) | ? [v3] : ? [v4] : (( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_12_12) = v3) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_rng(v1) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & one_to_one(v3) = v4 & relation_composition(v1, all_0_12_12) = v3) | ( ~ (v3 = 0) & subset(v2, v0) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (relation_composition(v1, all_0_12_12) = v2) | ? [v3] : ? [v4] : ((v3 = 0 & one_to_one(v1) = 0) | ( ~ (v4 = 0) & subset(v3, v0) = v4 & relation_rng(v1) = v3) | ( ~ (v3 = 0) & one_to_one(v2) = v3) | ( ~ (v3 = 0) & relation(v1) = v3) | ( ~ (v3 = 0) & function(v1) = v3))) & ! [v1] : ( ~ (relation(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_12_12) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & function(v1) = v2))) & ! [v1] : ( ~ (function(v1) = 0) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v1) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v1, all_0_12_12) = v2) | ( ~ (v3 = 0) & subset(v2, v0) = v3 & relation_rng(v1) = v2) | ( ~ (v2 = 0) & relation(v1) = v2))))) % 50.67/21.34 | % 50.67/21.34 | Instantiating (123) with all_46_0_52 yields: % 50.67/21.34 | (124) ( ~ (all_46_0_52 = 0) & relation(all_0_12_12) = all_46_0_52) | (relation_dom(all_0_12_12) = all_46_0_52 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v3 = 0) & subset(v2, all_46_0_52) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v2 = 0) & subset(v1, all_46_0_52) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_12_12) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_46_0_52) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_46_0_52) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_46_0_52) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1)))) % 50.67/21.34 | % 50.67/21.34 | Instantiating (118) with all_54_0_69 yields: % 50.67/21.34 | (125) ( ~ (all_54_0_69 = 0) & function(all_0_8_8) = all_54_0_69) | (relation_dom(all_0_8_8) = all_54_0_69 & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v2 = 0 & subset(v1, all_54_0_69) = 0) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v0) = v4 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_54_0_69) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v1) & relation_dom(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_54_0_69) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_54_0_69) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_54_0_69) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & relation(v0) = v1)))) % 50.67/21.35 | % 50.67/21.35 | Instantiating (117) with all_55_0_70 yields: % 50.67/21.35 | (126) ( ~ (all_55_0_70 = 0) & function(all_0_8_8) = all_55_0_70) | (relation_dom(all_0_8_8) = all_55_0_70 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v3 = 0) & subset(v2, all_55_0_70) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & subset(v1, all_55_0_70) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_55_0_70) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_55_0_70) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_55_0_70) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1)))) % 50.67/21.35 | % 50.67/21.35 | Instantiating (119) with all_62_0_83 yields: % 50.67/21.35 | (127) ( ~ (all_62_0_83 = 0) & function(all_0_12_12) = all_62_0_83) | (relation_dom(all_0_12_12) = all_62_0_83 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v3 = 0) & subset(v2, all_62_0_83) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v2 = 0) & subset(v1, all_62_0_83) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_12_12) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_62_0_83) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_62_0_83) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_62_0_83) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1)))) % 50.67/21.35 | % 50.67/21.35 | Instantiating (122) with all_63_0_84 yields: % 50.67/21.35 | (128) ( ~ (all_63_0_84 = 0) & relation(all_0_8_8) = all_63_0_84) | (relation_dom(all_0_8_8) = all_63_0_84 & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v2 = 0 & subset(v1, all_63_0_84) = 0) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v0) = v4 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_63_0_84) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v1) & relation_dom(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_63_0_84) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_63_0_84) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_63_0_84) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & relation(v0) = v1)))) % 50.67/21.35 | % 50.67/21.35 | Instantiating (121) with all_64_0_85 yields: % 50.67/21.35 | (129) ( ~ (all_64_0_85 = 0) & relation(all_0_8_8) = all_64_0_85) | (relation_dom(all_0_8_8) = all_64_0_85 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v3 = 0) & subset(v2, all_64_0_85) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & subset(v1, all_64_0_85) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_64_0_85) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_64_0_85) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_64_0_85) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1)))) % 50.67/21.35 | % 50.67/21.35 | Instantiating (120) with all_69_0_94 yields: % 50.67/21.35 | (130) ( ~ (all_69_0_94 = 0) & relation(all_0_0_0) = all_69_0_94) | (relation_dom(all_0_0_0) = all_69_0_94 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v3 = 0) & subset(v2, all_69_0_94) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v2 = 0) & subset(v1, all_69_0_94) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_0_0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_69_0_94) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_69_0_94) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_69_0_94) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1)))) % 50.67/21.36 | % 50.67/21.36 | Instantiating (116) with all_87_0_122 yields: % 50.67/21.36 | (131) ( ~ (all_87_0_122 = 0) & function(all_0_0_0) = all_87_0_122) | (relation_dom(all_0_0_0) = all_87_0_122 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v3 = 0) & subset(v2, all_87_0_122) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v2 = 0) & subset(v1, all_87_0_122) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_0_0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_87_0_122) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_87_0_122) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_87_0_122) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1)))) % 50.67/21.36 | % 50.67/21.36 +-Applying beta-rule and splitting (129), into two cases. % 50.67/21.36 |-Branch one: % 50.67/21.36 | (132) ~ (all_64_0_85 = 0) & relation(all_0_8_8) = all_64_0_85 % 50.67/21.36 | % 50.67/21.36 | Applying alpha-rule on (132) yields: % 50.67/21.36 | (133) ~ (all_64_0_85 = 0) % 50.67/21.36 | (134) relation(all_0_8_8) = all_64_0_85 % 50.67/21.36 | % 50.67/21.36 | Instantiating formula (68) with all_0_8_8, all_64_0_85, 0 and discharging atoms relation(all_0_8_8) = all_64_0_85, relation(all_0_8_8) = 0, yields: % 50.67/21.36 | (135) all_64_0_85 = 0 % 50.67/21.36 | % 50.67/21.36 | Equations (135) can reduce 133 to: % 50.67/21.36 | (136) $false % 50.67/21.36 | % 50.67/21.36 |-The branch is then unsatisfiable % 50.67/21.36 |-Branch two: % 50.67/21.36 | (137) relation_dom(all_0_8_8) = all_64_0_85 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v3 = 0) & subset(v2, all_64_0_85) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & subset(v1, all_64_0_85) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_64_0_85) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_64_0_85) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_64_0_85) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 50.67/21.36 | % 50.67/21.36 | Applying alpha-rule on (137) yields: % 50.67/21.36 | (138) ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v3 = 0) & subset(v2, all_64_0_85) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.36 | (139) relation_dom(all_0_8_8) = all_64_0_85 % 50.67/21.36 | (140) ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_64_0_85) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.36 | (141) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_64_0_85) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 50.67/21.36 | (142) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_64_0_85) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) % 50.67/21.36 | (143) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & subset(v1, all_64_0_85) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.36 | % 50.67/21.36 | Instantiating formula (138) with all_0_9_9, all_0_12_12 and discharging atoms one_to_one(all_0_12_12) = all_0_9_9, yields: % 50.67/21.36 | (144) all_0_9_9 = 0 | ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_8_8) = v0) | ( ~ (v1 = 0) & subset(v0, all_64_0_85) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 50.67/21.36 | % 50.67/21.36 | Instantiating formula (140) with all_0_10_10, all_0_12_12 and discharging atoms relation_composition(all_0_12_12, all_0_8_8) = all_0_10_10, yields: % 50.67/21.36 | (145) ? [v0] : ? [v1] : ((v0 = 0 & one_to_one(all_0_12_12) = 0) | ( ~ (v1 = 0) & subset(v0, all_64_0_85) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & one_to_one(all_0_10_10) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 50.67/21.36 | % 50.67/21.36 | Instantiating (145) with all_141_0_478, all_141_1_479 yields: % 50.67/21.36 | (146) (all_141_1_479 = 0 & one_to_one(all_0_12_12) = 0) | ( ~ (all_141_0_478 = 0) & subset(all_141_1_479, all_64_0_85) = all_141_0_478 & relation_rng(all_0_12_12) = all_141_1_479) | ( ~ (all_141_1_479 = 0) & one_to_one(all_0_10_10) = all_141_1_479) | ( ~ (all_141_1_479 = 0) & relation(all_0_12_12) = all_141_1_479) | ( ~ (all_141_1_479 = 0) & function(all_0_12_12) = all_141_1_479) % 50.67/21.36 | % 50.67/21.36 +-Applying beta-rule and splitting (113), into two cases. % 50.67/21.36 |-Branch one: % 50.67/21.36 | (147) all_0_9_9 = 0 % 50.67/21.36 | % 50.67/21.36 | Equations (147) can reduce 71 to: % 50.67/21.36 | (136) $false % 50.67/21.36 | % 50.67/21.36 |-The branch is then unsatisfiable % 50.67/21.36 |-Branch two: % 50.67/21.36 | (71) ~ (all_0_9_9 = 0) % 50.67/21.36 | (150) ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_12_12) = v0) | ( ~ (v1 = 0) & subset(v0, all_0_11_11) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 50.67/21.36 | % 50.67/21.36 +-Applying beta-rule and splitting (128), into two cases. % 50.67/21.36 |-Branch one: % 50.67/21.36 | (151) ~ (all_63_0_84 = 0) & relation(all_0_8_8) = all_63_0_84 % 50.67/21.36 | % 50.67/21.36 | Applying alpha-rule on (151) yields: % 50.67/21.36 | (152) ~ (all_63_0_84 = 0) % 50.67/21.36 | (153) relation(all_0_8_8) = all_63_0_84 % 50.67/21.36 | % 50.67/21.36 | Instantiating formula (68) with all_0_8_8, all_63_0_84, 0 and discharging atoms relation(all_0_8_8) = all_63_0_84, relation(all_0_8_8) = 0, yields: % 50.67/21.36 | (154) all_63_0_84 = 0 % 50.67/21.36 | % 50.67/21.36 | Equations (154) can reduce 152 to: % 50.67/21.36 | (136) $false % 50.67/21.36 | % 50.67/21.36 |-The branch is then unsatisfiable % 50.67/21.36 |-Branch two: % 50.67/21.36 | (156) relation_dom(all_0_8_8) = all_63_0_84 & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v2 = 0 & subset(v1, all_63_0_84) = 0) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v0) = v4 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_63_0_84) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v1) & relation_dom(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_63_0_84) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_63_0_84) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_63_0_84) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 50.67/21.37 | % 50.67/21.37 | Applying alpha-rule on (156) yields: % 50.67/21.37 | (157) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v2 = 0 & subset(v1, all_63_0_84) = 0) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v0) = v4 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.37 | (158) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_63_0_84) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 50.67/21.37 | (159) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_63_0_84) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) % 50.67/21.37 | (160) ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_63_0_84) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v1) & relation_dom(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.37 | (161) ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_63_0_84) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.37 | (162) relation_dom(all_0_8_8) = all_63_0_84 % 50.67/21.37 | % 50.67/21.37 | Instantiating formula (160) with all_0_11_11, all_0_12_12 and discharging atoms relation_dom(all_0_12_12) = all_0_11_11, yields: % 50.67/21.37 | (163) ? [v0] : ? [v1] : ((v1 = 0 & subset(v0, all_63_0_84) = 0 & relation_rng(all_0_12_12) = v0) | ( ~ (v1 = all_0_11_11) & relation_dom(v0) = v1 & relation_composition(all_0_12_12, all_0_8_8) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 50.67/21.37 | % 50.67/21.37 | Instantiating (163) with all_161_0_702, all_161_1_703 yields: % 50.67/21.37 | (164) (all_161_0_702 = 0 & subset(all_161_1_703, all_63_0_84) = 0 & relation_rng(all_0_12_12) = all_161_1_703) | ( ~ (all_161_0_702 = all_0_11_11) & relation_dom(all_161_1_703) = all_161_0_702 & relation_composition(all_0_12_12, all_0_8_8) = all_161_1_703) | ( ~ (all_161_1_703 = 0) & relation(all_0_12_12) = all_161_1_703) | ( ~ (all_161_1_703 = 0) & function(all_0_12_12) = all_161_1_703) % 50.67/21.37 | % 50.67/21.37 +-Applying beta-rule and splitting (164), into two cases. % 50.67/21.37 |-Branch one: % 50.67/21.37 | (165) (all_161_0_702 = 0 & subset(all_161_1_703, all_63_0_84) = 0 & relation_rng(all_0_12_12) = all_161_1_703) | ( ~ (all_161_0_702 = all_0_11_11) & relation_dom(all_161_1_703) = all_161_0_702 & relation_composition(all_0_12_12, all_0_8_8) = all_161_1_703) | ( ~ (all_161_1_703 = 0) & relation(all_0_12_12) = all_161_1_703) % 50.67/21.37 | % 50.67/21.37 +-Applying beta-rule and splitting (165), into two cases. % 50.67/21.37 |-Branch one: % 50.67/21.37 | (166) (all_161_0_702 = 0 & subset(all_161_1_703, all_63_0_84) = 0 & relation_rng(all_0_12_12) = all_161_1_703) | ( ~ (all_161_0_702 = all_0_11_11) & relation_dom(all_161_1_703) = all_161_0_702 & relation_composition(all_0_12_12, all_0_8_8) = all_161_1_703) % 50.67/21.37 | % 50.67/21.37 +-Applying beta-rule and splitting (166), into two cases. % 50.67/21.37 |-Branch one: % 50.67/21.37 | (167) all_161_0_702 = 0 & subset(all_161_1_703, all_63_0_84) = 0 & relation_rng(all_0_12_12) = all_161_1_703 % 50.67/21.37 | % 50.67/21.37 | Applying alpha-rule on (167) yields: % 50.67/21.37 | (168) all_161_0_702 = 0 % 50.67/21.37 | (169) subset(all_161_1_703, all_63_0_84) = 0 % 50.67/21.37 | (170) relation_rng(all_0_12_12) = all_161_1_703 % 50.67/21.37 | % 50.67/21.37 +-Applying beta-rule and splitting (130), into two cases. % 50.67/21.37 |-Branch one: % 50.67/21.37 | (171) ~ (all_69_0_94 = 0) & relation(all_0_0_0) = all_69_0_94 % 50.67/21.37 | % 50.67/21.37 | Applying alpha-rule on (171) yields: % 50.67/21.37 | (172) ~ (all_69_0_94 = 0) % 50.67/21.37 | (173) relation(all_0_0_0) = all_69_0_94 % 50.67/21.37 | % 50.67/21.37 | Instantiating formula (68) with all_0_0_0, all_69_0_94, 0 and discharging atoms relation(all_0_0_0) = all_69_0_94, relation(all_0_0_0) = 0, yields: % 50.67/21.37 | (174) all_69_0_94 = 0 % 50.67/21.37 | % 50.67/21.37 | Equations (174) can reduce 172 to: % 50.67/21.37 | (136) $false % 50.67/21.37 | % 50.67/21.37 |-The branch is then unsatisfiable % 50.67/21.37 |-Branch two: % 50.67/21.37 | (176) relation_dom(all_0_0_0) = all_69_0_94 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v3 = 0) & subset(v2, all_69_0_94) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v2 = 0) & subset(v1, all_69_0_94) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_0_0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_69_0_94) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_69_0_94) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_69_0_94) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 50.67/21.37 | % 50.67/21.37 | Applying alpha-rule on (176) yields: % 50.67/21.37 | (177) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v2 = 0) & subset(v1, all_69_0_94) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.37 | (178) ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v3 = 0) & subset(v2, all_69_0_94) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.37 | (179) relation_dom(all_0_0_0) = all_69_0_94 % 50.67/21.37 | (180) ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_0_0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_69_0_94) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.37 | (181) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_69_0_94) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 50.67/21.37 | (182) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_69_0_94) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) % 50.67/21.37 | % 50.67/21.37 | Instantiating formula (178) with all_0_9_9, all_0_12_12 and discharging atoms one_to_one(all_0_12_12) = all_0_9_9, yields: % 50.67/21.37 | (183) all_0_9_9 = 0 | ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_0_0) = v0) | ( ~ (v1 = 0) & subset(v0, all_69_0_94) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 50.67/21.37 | % 50.67/21.37 +-Applying beta-rule and splitting (131), into two cases. % 50.67/21.37 |-Branch one: % 50.67/21.37 | (184) ~ (all_87_0_122 = 0) & function(all_0_0_0) = all_87_0_122 % 50.67/21.37 | % 50.67/21.37 | Applying alpha-rule on (184) yields: % 50.67/21.37 | (185) ~ (all_87_0_122 = 0) % 50.67/21.37 | (186) function(all_0_0_0) = all_87_0_122 % 50.67/21.37 | % 50.67/21.37 | Instantiating formula (97) with all_0_0_0, all_87_0_122, 0 and discharging atoms function(all_0_0_0) = all_87_0_122, function(all_0_0_0) = 0, yields: % 50.67/21.37 | (187) all_87_0_122 = 0 % 50.67/21.37 | % 50.67/21.37 | Equations (187) can reduce 185 to: % 50.67/21.37 | (136) $false % 50.67/21.37 | % 50.67/21.37 |-The branch is then unsatisfiable % 50.67/21.37 |-Branch two: % 50.67/21.37 | (189) relation_dom(all_0_0_0) = all_87_0_122 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v3 = 0) & subset(v2, all_87_0_122) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v2 = 0) & subset(v1, all_87_0_122) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_0_0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_87_0_122) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_87_0_122) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_87_0_122) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 50.67/21.38 | % 50.67/21.38 | Applying alpha-rule on (189) yields: % 50.67/21.38 | (190) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_87_0_122) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 50.67/21.38 | (191) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_0_0) = v1) | ( ~ (v2 = 0) & subset(v1, all_87_0_122) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) % 50.67/21.38 | (192) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v2 = 0) & subset(v1, all_87_0_122) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.38 | (193) ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_0_0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_87_0_122) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.38 | (194) relation_dom(all_0_0_0) = all_87_0_122 % 50.67/21.38 | (195) ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_0_0) = v2) | ( ~ (v3 = 0) & subset(v2, all_87_0_122) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.38 | % 50.67/21.38 | Instantiating formula (195) with all_0_9_9, all_0_12_12 and discharging atoms one_to_one(all_0_12_12) = all_0_9_9, yields: % 50.67/21.38 | (196) all_0_9_9 = 0 | ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_0_0) = v0) | ( ~ (v1 = 0) & subset(v0, all_87_0_122) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 50.67/21.38 | % 50.67/21.38 +-Applying beta-rule and splitting (183), into two cases. % 50.67/21.38 |-Branch one: % 50.67/21.38 | (147) all_0_9_9 = 0 % 50.67/21.38 | % 50.67/21.38 | Equations (147) can reduce 71 to: % 50.67/21.38 | (136) $false % 50.67/21.38 | % 50.67/21.38 |-The branch is then unsatisfiable % 50.67/21.38 |-Branch two: % 50.67/21.38 | (71) ~ (all_0_9_9 = 0) % 50.67/21.38 | (200) ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_0_0) = v0) | ( ~ (v1 = 0) & subset(v0, all_69_0_94) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 50.67/21.38 | % 50.67/21.38 +-Applying beta-rule and splitting (124), into two cases. % 50.67/21.38 |-Branch one: % 50.67/21.38 | (201) ~ (all_46_0_52 = 0) & relation(all_0_12_12) = all_46_0_52 % 50.67/21.38 | % 50.67/21.38 | Applying alpha-rule on (201) yields: % 50.67/21.38 | (202) ~ (all_46_0_52 = 0) % 50.67/21.38 | (203) relation(all_0_12_12) = all_46_0_52 % 50.67/21.38 | % 50.67/21.38 | Instantiating formula (68) with all_0_12_12, all_46_0_52, 0 and discharging atoms relation(all_0_12_12) = all_46_0_52, relation(all_0_12_12) = 0, yields: % 50.67/21.38 | (204) all_46_0_52 = 0 % 50.67/21.38 | % 50.67/21.38 | Equations (204) can reduce 202 to: % 50.67/21.38 | (136) $false % 50.67/21.38 | % 50.67/21.38 |-The branch is then unsatisfiable % 50.67/21.38 |-Branch two: % 50.67/21.38 | (206) relation_dom(all_0_12_12) = all_46_0_52 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v3 = 0) & subset(v2, all_46_0_52) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v2 = 0) & subset(v1, all_46_0_52) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_12_12) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_46_0_52) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_46_0_52) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_46_0_52) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 50.67/21.38 | % 50.67/21.38 | Applying alpha-rule on (206) yields: % 50.67/21.38 | (207) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v2 = 0) & subset(v1, all_46_0_52) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 50.67/21.38 | (208) ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_12_12) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_46_0_52) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.38 | (209) relation_dom(all_0_12_12) = all_46_0_52 % 51.06/21.38 | (210) ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v3 = 0) & subset(v2, all_46_0_52) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.38 | (211) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_46_0_52) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 51.06/21.38 | (212) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_46_0_52) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) % 51.06/21.38 | % 51.06/21.38 | Instantiating formula (210) with all_0_9_9, all_0_12_12 and discharging atoms one_to_one(all_0_12_12) = all_0_9_9, yields: % 51.06/21.38 | (213) all_0_9_9 = 0 | ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_12_12) = v0) | ( ~ (v1 = 0) & subset(v0, all_46_0_52) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.38 | % 51.06/21.38 +-Applying beta-rule and splitting (196), into two cases. % 51.06/21.38 |-Branch one: % 51.06/21.38 | (147) all_0_9_9 = 0 % 51.06/21.38 | % 51.06/21.38 | Equations (147) can reduce 71 to: % 51.06/21.38 | (136) $false % 51.06/21.38 | % 51.06/21.38 |-The branch is then unsatisfiable % 51.06/21.38 |-Branch two: % 51.06/21.38 | (71) ~ (all_0_9_9 = 0) % 51.06/21.38 | (217) ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_0_0) = v0) | ( ~ (v1 = 0) & subset(v0, all_87_0_122) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.38 | % 51.06/21.38 +-Applying beta-rule and splitting (125), into two cases. % 51.06/21.38 |-Branch one: % 51.06/21.38 | (218) ~ (all_54_0_69 = 0) & function(all_0_8_8) = all_54_0_69 % 51.06/21.38 | % 51.06/21.38 | Applying alpha-rule on (218) yields: % 51.06/21.38 | (219) ~ (all_54_0_69 = 0) % 51.06/21.38 | (220) function(all_0_8_8) = all_54_0_69 % 51.06/21.38 | % 51.06/21.38 | Instantiating formula (97) with all_0_8_8, all_54_0_69, 0 and discharging atoms function(all_0_8_8) = all_54_0_69, function(all_0_8_8) = 0, yields: % 51.06/21.38 | (221) all_54_0_69 = 0 % 51.06/21.38 | % 51.06/21.38 | Equations (221) can reduce 219 to: % 51.06/21.38 | (136) $false % 51.06/21.38 | % 51.06/21.38 |-The branch is then unsatisfiable % 51.06/21.38 |-Branch two: % 51.06/21.38 | (223) relation_dom(all_0_8_8) = all_54_0_69 & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v2 = 0 & subset(v1, all_54_0_69) = 0) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v0) = v4 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_54_0_69) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v1) & relation_dom(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_54_0_69) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_54_0_69) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_54_0_69) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 51.06/21.39 | % 51.06/21.39 | Applying alpha-rule on (223) yields: % 51.06/21.39 | (224) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v2 = 0 & subset(v1, all_54_0_69) = 0) | ( ~ (v4 = v3) & relation_dom(v2) = v3 & relation_dom(v0) = v4 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.39 | (225) ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_54_0_69) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.39 | (226) ! [v0] : ! [v1] : ( ~ (relation_dom(v0) = v1) | ? [v2] : ? [v3] : ((v3 = 0 & subset(v2, all_54_0_69) = 0 & relation_rng(v0) = v2) | ( ~ (v3 = v1) & relation_dom(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.39 | (227) relation_dom(all_0_8_8) = all_54_0_69 % 51.06/21.39 | (228) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_54_0_69) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 51.06/21.39 | (229) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & subset(v1, all_54_0_69) = 0 & relation_rng(v0) = v1) | ( ~ (v3 = v2) & relation_dom(v1) = v2 & relation_dom(v0) = v3 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) % 51.06/21.39 | % 51.06/21.39 +-Applying beta-rule and splitting (126), into two cases. % 51.06/21.39 |-Branch one: % 51.06/21.39 | (230) ~ (all_55_0_70 = 0) & function(all_0_8_8) = all_55_0_70 % 51.06/21.39 | % 51.06/21.39 | Applying alpha-rule on (230) yields: % 51.06/21.39 | (231) ~ (all_55_0_70 = 0) % 51.06/21.39 | (232) function(all_0_8_8) = all_55_0_70 % 51.06/21.39 | % 51.06/21.39 | Instantiating formula (97) with all_0_8_8, all_55_0_70, 0 and discharging atoms function(all_0_8_8) = all_55_0_70, function(all_0_8_8) = 0, yields: % 51.06/21.39 | (233) all_55_0_70 = 0 % 51.06/21.39 | % 51.06/21.39 | Equations (233) can reduce 231 to: % 51.06/21.39 | (136) $false % 51.06/21.39 | % 51.06/21.39 |-The branch is then unsatisfiable % 51.06/21.39 |-Branch two: % 51.06/21.39 | (235) relation_dom(all_0_8_8) = all_55_0_70 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v3 = 0) & subset(v2, all_55_0_70) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & subset(v1, all_55_0_70) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_55_0_70) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_55_0_70) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_55_0_70) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 51.06/21.39 | % 51.06/21.39 | Applying alpha-rule on (235) yields: % 51.06/21.39 | (236) ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v3 = 0) & subset(v2, all_55_0_70) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.39 | (237) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_8_8) = v2) | ( ~ (v2 = 0) & subset(v1, all_55_0_70) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.39 | (238) relation_dom(all_0_8_8) = all_55_0_70 % 51.06/21.39 | (239) ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_8_8) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_55_0_70) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.39 | (240) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_55_0_70) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 51.06/21.39 | (241) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_8_8) = v1) | ( ~ (v2 = 0) & subset(v1, all_55_0_70) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) % 51.06/21.39 | % 51.06/21.39 | Instantiating formula (236) with all_0_9_9, all_0_12_12 and discharging atoms one_to_one(all_0_12_12) = all_0_9_9, yields: % 51.06/21.39 | (242) all_0_9_9 = 0 | ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_8_8) = v0) | ( ~ (v1 = 0) & subset(v0, all_55_0_70) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.39 | % 51.06/21.39 | Instantiating formula (239) with all_0_10_10, all_0_12_12 and discharging atoms relation_composition(all_0_12_12, all_0_8_8) = all_0_10_10, yields: % 51.06/21.39 | (243) ? [v0] : ? [v1] : ((v0 = 0 & one_to_one(all_0_12_12) = 0) | ( ~ (v1 = 0) & subset(v0, all_55_0_70) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & one_to_one(all_0_10_10) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.39 | % 51.06/21.39 | Instantiating (243) with all_301_0_1289, all_301_1_1290 yields: % 51.06/21.39 | (244) (all_301_1_1290 = 0 & one_to_one(all_0_12_12) = 0) | ( ~ (all_301_0_1289 = 0) & subset(all_301_1_1290, all_55_0_70) = all_301_0_1289 & relation_rng(all_0_12_12) = all_301_1_1290) | ( ~ (all_301_1_1290 = 0) & one_to_one(all_0_10_10) = all_301_1_1290) | ( ~ (all_301_1_1290 = 0) & relation(all_0_12_12) = all_301_1_1290) | ( ~ (all_301_1_1290 = 0) & function(all_0_12_12) = all_301_1_1290) % 51.06/21.39 | % 51.06/21.39 +-Applying beta-rule and splitting (244), into two cases. % 51.06/21.39 |-Branch one: % 51.06/21.39 | (245) (all_301_1_1290 = 0 & one_to_one(all_0_12_12) = 0) | ( ~ (all_301_0_1289 = 0) & subset(all_301_1_1290, all_55_0_70) = all_301_0_1289 & relation_rng(all_0_12_12) = all_301_1_1290) | ( ~ (all_301_1_1290 = 0) & one_to_one(all_0_10_10) = all_301_1_1290) | ( ~ (all_301_1_1290 = 0) & relation(all_0_12_12) = all_301_1_1290) % 51.06/21.39 | % 51.06/21.39 +-Applying beta-rule and splitting (245), into two cases. % 51.06/21.39 |-Branch one: % 51.06/21.39 | (246) (all_301_1_1290 = 0 & one_to_one(all_0_12_12) = 0) | ( ~ (all_301_0_1289 = 0) & subset(all_301_1_1290, all_55_0_70) = all_301_0_1289 & relation_rng(all_0_12_12) = all_301_1_1290) | ( ~ (all_301_1_1290 = 0) & one_to_one(all_0_10_10) = all_301_1_1290) % 51.06/21.39 | % 51.06/21.39 +-Applying beta-rule and splitting (246), into two cases. % 51.06/21.39 |-Branch one: % 51.06/21.39 | (247) (all_301_1_1290 = 0 & one_to_one(all_0_12_12) = 0) | ( ~ (all_301_0_1289 = 0) & subset(all_301_1_1290, all_55_0_70) = all_301_0_1289 & relation_rng(all_0_12_12) = all_301_1_1290) % 51.06/21.39 | % 51.06/21.39 +-Applying beta-rule and splitting (247), into two cases. % 51.06/21.39 |-Branch one: % 51.06/21.39 | (248) all_301_1_1290 = 0 & one_to_one(all_0_12_12) = 0 % 51.06/21.39 | % 51.06/21.39 | Applying alpha-rule on (248) yields: % 51.06/21.39 | (249) all_301_1_1290 = 0 % 51.06/21.39 | (250) one_to_one(all_0_12_12) = 0 % 51.06/21.39 | % 51.06/21.39 +-Applying beta-rule and splitting (242), into two cases. % 51.06/21.39 |-Branch one: % 51.06/21.39 | (147) all_0_9_9 = 0 % 51.06/21.39 | % 51.06/21.39 | Equations (147) can reduce 71 to: % 51.06/21.39 | (136) $false % 51.06/21.39 | % 51.06/21.39 |-The branch is then unsatisfiable % 51.06/21.39 |-Branch two: % 51.06/21.39 | (71) ~ (all_0_9_9 = 0) % 51.06/21.39 | (254) ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_8_8) = v0) | ( ~ (v1 = 0) & subset(v0, all_55_0_70) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.39 | % 51.06/21.39 +-Applying beta-rule and splitting (144), into two cases. % 51.06/21.39 |-Branch one: % 51.06/21.39 | (147) all_0_9_9 = 0 % 51.06/21.39 | % 51.06/21.39 | Equations (147) can reduce 71 to: % 51.06/21.39 | (136) $false % 51.06/21.39 | % 51.06/21.39 |-The branch is then unsatisfiable % 51.06/21.39 |-Branch two: % 51.06/21.39 | (71) ~ (all_0_9_9 = 0) % 51.06/21.39 | (258) ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_8_8) = v0) | ( ~ (v1 = 0) & subset(v0, all_64_0_85) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.39 | % 51.06/21.39 +-Applying beta-rule and splitting (213), into two cases. % 51.06/21.39 |-Branch one: % 51.06/21.39 | (147) all_0_9_9 = 0 % 51.06/21.39 | % 51.06/21.39 | Equations (147) can reduce 71 to: % 51.06/21.39 | (136) $false % 51.06/21.39 | % 51.06/21.39 |-The branch is then unsatisfiable % 51.06/21.39 |-Branch two: % 51.06/21.39 | (71) ~ (all_0_9_9 = 0) % 51.06/21.39 | (262) ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_12_12) = v0) | ( ~ (v1 = 0) & subset(v0, all_46_0_52) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.39 | % 51.06/21.39 | Instantiating formula (19) with all_0_12_12, 0, all_0_9_9 and discharging atoms one_to_one(all_0_12_12) = all_0_9_9, one_to_one(all_0_12_12) = 0, yields: % 51.06/21.39 | (147) all_0_9_9 = 0 % 51.06/21.39 | % 51.06/21.39 | Equations (147) can reduce 71 to: % 51.06/21.39 | (136) $false % 51.06/21.39 | % 51.06/21.39 |-The branch is then unsatisfiable % 51.06/21.39 |-Branch two: % 51.06/21.39 | (265) ~ (all_301_0_1289 = 0) & subset(all_301_1_1290, all_55_0_70) = all_301_0_1289 & relation_rng(all_0_12_12) = all_301_1_1290 % 51.06/21.40 | % 51.06/21.40 | Applying alpha-rule on (265) yields: % 51.06/21.40 | (266) ~ (all_301_0_1289 = 0) % 51.06/21.40 | (267) subset(all_301_1_1290, all_55_0_70) = all_301_0_1289 % 51.06/21.40 | (268) relation_rng(all_0_12_12) = all_301_1_1290 % 51.06/21.40 | % 51.06/21.40 +-Applying beta-rule and splitting (242), into two cases. % 51.06/21.40 |-Branch one: % 51.06/21.40 | (147) all_0_9_9 = 0 % 51.06/21.40 | % 51.06/21.40 | Equations (147) can reduce 71 to: % 51.06/21.40 | (136) $false % 51.06/21.40 | % 51.06/21.40 |-The branch is then unsatisfiable % 51.06/21.40 |-Branch two: % 51.06/21.40 | (71) ~ (all_0_9_9 = 0) % 51.06/21.40 | (254) ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_8_8) = v0) | ( ~ (v1 = 0) & subset(v0, all_55_0_70) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.40 | % 51.06/21.40 +-Applying beta-rule and splitting (127), into two cases. % 51.06/21.40 |-Branch one: % 51.06/21.40 | (273) ~ (all_62_0_83 = 0) & function(all_0_12_12) = all_62_0_83 % 51.06/21.40 | % 51.06/21.40 | Applying alpha-rule on (273) yields: % 51.06/21.40 | (274) ~ (all_62_0_83 = 0) % 51.06/21.40 | (275) function(all_0_12_12) = all_62_0_83 % 51.06/21.40 | % 51.06/21.40 | Instantiating formula (97) with all_0_12_12, all_62_0_83, 0 and discharging atoms function(all_0_12_12) = all_62_0_83, function(all_0_12_12) = 0, yields: % 51.06/21.40 | (276) all_62_0_83 = 0 % 51.06/21.40 | % 51.06/21.40 | Equations (276) can reduce 274 to: % 51.06/21.40 | (136) $false % 51.06/21.40 | % 51.06/21.40 |-The branch is then unsatisfiable % 51.06/21.40 |-Branch two: % 51.06/21.40 | (278) relation_dom(all_0_12_12) = all_62_0_83 & ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v3 = 0) & subset(v2, all_62_0_83) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v2 = 0) & subset(v1, all_62_0_83) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_12_12) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_62_0_83) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) & ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_62_0_83) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) & ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_62_0_83) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 51.06/21.40 | % 51.06/21.40 | Applying alpha-rule on (278) yields: % 51.06/21.40 | (279) ! [v0] : ! [v1] : ( ~ (relation_composition(v0, all_0_12_12) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & subset(v2, all_62_0_83) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & one_to_one(v1) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.40 | (280) ! [v0] : ! [v1] : ( ~ (relation_rng(v0) = v1) | ? [v2] : ? [v3] : ((v2 = 0 & one_to_one(v0) = 0) | ( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v2 = 0) & subset(v1, all_62_0_83) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.40 | (281) ! [v0] : ( ~ (function(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_62_0_83) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & relation(v0) = v1))) % 51.06/21.40 | (282) ! [v0] : ( ~ (relation(v0) = 0) | ? [v1] : ? [v2] : ((v1 = 0 & one_to_one(v0) = 0) | ( ~ (v2 = 0) & one_to_one(v1) = v2 & relation_composition(v0, all_0_12_12) = v1) | ( ~ (v2 = 0) & subset(v1, all_62_0_83) = v2 & relation_rng(v0) = v1) | ( ~ (v1 = 0) & function(v0) = v1))) % 51.06/21.40 | (283) ! [v0] : ! [v1] : (v1 = 0 | ~ (one_to_one(v0) = v1) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & one_to_one(v2) = v3 & relation_composition(v0, all_0_12_12) = v2) | ( ~ (v3 = 0) & subset(v2, all_62_0_83) = v3 & relation_rng(v0) = v2) | ( ~ (v2 = 0) & relation(v0) = v2) | ( ~ (v2 = 0) & function(v0) = v2))) % 51.06/21.40 | (284) relation_dom(all_0_12_12) = all_62_0_83 % 51.06/21.40 | % 51.06/21.40 | Instantiating formula (283) with all_0_9_9, all_0_12_12 and discharging atoms one_to_one(all_0_12_12) = all_0_9_9, yields: % 51.06/21.40 | (285) all_0_9_9 = 0 | ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_12_12) = v0) | ( ~ (v1 = 0) & subset(v0, all_62_0_83) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.40 | % 51.06/21.40 +-Applying beta-rule and splitting (213), into two cases. % 51.06/21.40 |-Branch one: % 51.06/21.40 | (147) all_0_9_9 = 0 % 51.06/21.40 | % 51.06/21.40 | Equations (147) can reduce 71 to: % 51.06/21.40 | (136) $false % 51.06/21.40 | % 51.06/21.40 |-The branch is then unsatisfiable % 51.06/21.40 |-Branch two: % 51.06/21.40 | (71) ~ (all_0_9_9 = 0) % 51.06/21.40 | (262) ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_12_12) = v0) | ( ~ (v1 = 0) & subset(v0, all_46_0_52) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.40 | % 51.06/21.40 +-Applying beta-rule and splitting (285), into two cases. % 51.06/21.40 |-Branch one: % 51.06/21.40 | (147) all_0_9_9 = 0 % 51.06/21.40 | % 51.06/21.40 | Equations (147) can reduce 71 to: % 51.06/21.40 | (136) $false % 51.06/21.40 | % 51.06/21.40 |-The branch is then unsatisfiable % 51.06/21.40 |-Branch two: % 51.06/21.40 | (71) ~ (all_0_9_9 = 0) % 51.06/21.40 | (293) ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_12_12) = v0) | ( ~ (v1 = 0) & subset(v0, all_62_0_83) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.40 | % 51.06/21.40 +-Applying beta-rule and splitting (146), into two cases. % 51.06/21.40 |-Branch one: % 51.06/21.40 | (294) (all_141_1_479 = 0 & one_to_one(all_0_12_12) = 0) | ( ~ (all_141_0_478 = 0) & subset(all_141_1_479, all_64_0_85) = all_141_0_478 & relation_rng(all_0_12_12) = all_141_1_479) | ( ~ (all_141_1_479 = 0) & one_to_one(all_0_10_10) = all_141_1_479) | ( ~ (all_141_1_479 = 0) & relation(all_0_12_12) = all_141_1_479) % 51.06/21.40 | % 51.06/21.40 +-Applying beta-rule and splitting (294), into two cases. % 51.06/21.40 |-Branch one: % 51.06/21.40 | (295) (all_141_1_479 = 0 & one_to_one(all_0_12_12) = 0) | ( ~ (all_141_0_478 = 0) & subset(all_141_1_479, all_64_0_85) = all_141_0_478 & relation_rng(all_0_12_12) = all_141_1_479) | ( ~ (all_141_1_479 = 0) & one_to_one(all_0_10_10) = all_141_1_479) % 51.06/21.40 | % 51.06/21.40 +-Applying beta-rule and splitting (295), into two cases. % 51.06/21.40 |-Branch one: % 51.06/21.40 | (296) (all_141_1_479 = 0 & one_to_one(all_0_12_12) = 0) | ( ~ (all_141_0_478 = 0) & subset(all_141_1_479, all_64_0_85) = all_141_0_478 & relation_rng(all_0_12_12) = all_141_1_479) % 51.06/21.40 | % 51.06/21.40 +-Applying beta-rule and splitting (296), into two cases. % 51.06/21.40 |-Branch one: % 51.06/21.40 | (297) all_141_1_479 = 0 & one_to_one(all_0_12_12) = 0 % 51.06/21.40 | % 51.06/21.40 | Applying alpha-rule on (297) yields: % 51.06/21.40 | (298) all_141_1_479 = 0 % 51.06/21.40 | (250) one_to_one(all_0_12_12) = 0 % 51.06/21.40 | % 51.06/21.40 +-Applying beta-rule and splitting (144), into two cases. % 51.06/21.40 |-Branch one: % 51.06/21.40 | (147) all_0_9_9 = 0 % 51.06/21.40 | % 51.06/21.40 | Equations (147) can reduce 71 to: % 51.06/21.40 | (136) $false % 51.06/21.40 | % 51.06/21.40 |-The branch is then unsatisfiable % 51.06/21.40 |-Branch two: % 51.06/21.40 | (71) ~ (all_0_9_9 = 0) % 51.06/21.40 | (258) ? [v0] : ? [v1] : (( ~ (v1 = 0) & one_to_one(v0) = v1 & relation_composition(all_0_12_12, all_0_8_8) = v0) | ( ~ (v1 = 0) & subset(v0, all_64_0_85) = v1 & relation_rng(all_0_12_12) = v0) | ( ~ (v0 = 0) & relation(all_0_12_12) = v0) | ( ~ (v0 = 0) & function(all_0_12_12) = v0)) % 51.06/21.40 | % 51.06/21.40 | Instantiating formula (19) with all_0_12_12, 0, all_0_9_9 and discharging atoms one_to_one(all_0_12_12) = all_0_9_9, one_to_one(all_0_12_12) = 0, yields: % 51.06/21.40 | (147) all_0_9_9 = 0 % 51.06/21.40 | % 51.06/21.40 | Equations (147) can reduce 71 to: % 51.06/21.40 | (136) $false % 51.06/21.40 | % 51.06/21.40 |-The branch is then unsatisfiable % 51.06/21.40 |-Branch two: % 51.06/21.40 | (306) ~ (all_141_0_478 = 0) & subset(all_141_1_479, all_64_0_85) = all_141_0_478 & relation_rng(all_0_12_12) = all_141_1_479 % 51.06/21.40 | % 51.06/21.40 | Applying alpha-rule on (306) yields: % 51.06/21.40 | (307) ~ (all_141_0_478 = 0) % 51.06/21.40 | (308) subset(all_141_1_479, all_64_0_85) = all_141_0_478 % 51.06/21.40 | (309) relation_rng(all_0_12_12) = all_141_1_479 % 51.06/21.40 | % 51.06/21.40 | Instantiating formula (13) with all_0_12_12, all_161_1_703, all_301_1_1290 and discharging atoms relation_rng(all_0_12_12) = all_301_1_1290, relation_rng(all_0_12_12) = all_161_1_703, yields: % 51.06/21.40 | (310) all_301_1_1290 = all_161_1_703 % 51.06/21.40 | % 51.06/21.40 | Instantiating formula (13) with all_0_12_12, all_141_1_479, all_301_1_1290 and discharging atoms relation_rng(all_0_12_12) = all_301_1_1290, relation_rng(all_0_12_12) = all_141_1_479, yields: % 51.06/21.40 | (311) all_301_1_1290 = all_141_1_479 % 51.06/21.40 | % 51.06/21.40 | Instantiating formula (105) with all_0_8_8, all_63_0_84, all_64_0_85 and discharging atoms relation_dom(all_0_8_8) = all_64_0_85, relation_dom(all_0_8_8) = all_63_0_84, yields: % 51.06/21.40 | (312) all_64_0_85 = all_63_0_84 % 51.06/21.40 | % 51.06/21.40 | Instantiating formula (105) with all_0_8_8, all_55_0_70, all_63_0_84 and discharging atoms relation_dom(all_0_8_8) = all_63_0_84, relation_dom(all_0_8_8) = all_55_0_70, yields: % 51.06/21.40 | (313) all_63_0_84 = all_55_0_70 % 51.06/21.40 | % 51.06/21.40 | Instantiating formula (105) with all_0_8_8, all_54_0_69, all_64_0_85 and discharging atoms relation_dom(all_0_8_8) = all_64_0_85, relation_dom(all_0_8_8) = all_54_0_69, yields: % 51.06/21.40 | (314) all_64_0_85 = all_54_0_69 % 51.06/21.40 | % 51.06/21.40 | Combining equations (310,311) yields a new equation: % 51.06/21.40 | (315) all_161_1_703 = all_141_1_479 % 51.06/21.40 | % 51.06/21.40 | Simplifying 315 yields: % 51.06/21.40 | (316) all_161_1_703 = all_141_1_479 % 51.06/21.40 | % 51.06/21.40 | Combining equations (312,314) yields a new equation: % 51.06/21.40 | (317) all_63_0_84 = all_54_0_69 % 51.06/21.40 | % 51.06/21.40 | Simplifying 317 yields: % 51.06/21.40 | (318) all_63_0_84 = all_54_0_69 % 51.06/21.40 | % 51.06/21.40 | Combining equations (313,318) yields a new equation: % 51.06/21.40 | (319) all_55_0_70 = all_54_0_69 % 51.06/21.40 | % 51.06/21.40 | Simplifying 319 yields: % 51.06/21.40 | (320) all_55_0_70 = all_54_0_69 % 51.06/21.40 | % 51.06/21.40 | From (311)(320) and (267) follows: % 51.06/21.41 | (321) subset(all_141_1_479, all_54_0_69) = all_301_0_1289 % 51.06/21.41 | % 51.06/21.41 | From (316)(318) and (169) follows: % 51.06/21.41 | (322) subset(all_141_1_479, all_54_0_69) = 0 % 51.06/21.41 | % 51.06/21.41 | From (314) and (308) follows: % 51.06/21.41 | (323) subset(all_141_1_479, all_54_0_69) = all_141_0_478 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (8) with all_141_1_479, all_54_0_69, all_141_0_478, all_301_0_1289 and discharging atoms subset(all_141_1_479, all_54_0_69) = all_301_0_1289, subset(all_141_1_479, all_54_0_69) = all_141_0_478, yields: % 51.06/21.41 | (324) all_301_0_1289 = all_141_0_478 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (8) with all_141_1_479, all_54_0_69, 0, all_301_0_1289 and discharging atoms subset(all_141_1_479, all_54_0_69) = all_301_0_1289, subset(all_141_1_479, all_54_0_69) = 0, yields: % 51.06/21.41 | (325) all_301_0_1289 = 0 % 51.06/21.41 | % 51.06/21.41 | Combining equations (324,325) yields a new equation: % 51.06/21.41 | (326) all_141_0_478 = 0 % 51.06/21.41 | % 51.06/21.41 | Simplifying 326 yields: % 51.06/21.41 | (327) all_141_0_478 = 0 % 51.06/21.41 | % 51.06/21.41 | Equations (327) can reduce 307 to: % 51.06/21.41 | (136) $false % 51.06/21.41 | % 51.06/21.41 |-The branch is then unsatisfiable % 51.06/21.41 |-Branch two: % 51.06/21.41 | (329) ~ (all_141_1_479 = 0) & one_to_one(all_0_10_10) = all_141_1_479 % 51.06/21.41 | % 51.06/21.41 | Applying alpha-rule on (329) yields: % 51.06/21.41 | (330) ~ (all_141_1_479 = 0) % 51.06/21.41 | (331) one_to_one(all_0_10_10) = all_141_1_479 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (19) with all_0_10_10, 0, all_141_1_479 and discharging atoms one_to_one(all_0_10_10) = all_141_1_479, one_to_one(all_0_10_10) = 0, yields: % 51.06/21.41 | (298) all_141_1_479 = 0 % 51.06/21.41 | % 51.06/21.41 | Equations (298) can reduce 330 to: % 51.06/21.41 | (136) $false % 51.06/21.41 | % 51.06/21.41 |-The branch is then unsatisfiable % 51.06/21.41 |-Branch two: % 51.06/21.41 | (334) ~ (all_141_1_479 = 0) & relation(all_0_12_12) = all_141_1_479 % 51.06/21.41 | % 51.06/21.41 | Applying alpha-rule on (334) yields: % 51.06/21.41 | (330) ~ (all_141_1_479 = 0) % 51.06/21.41 | (336) relation(all_0_12_12) = all_141_1_479 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (68) with all_0_12_12, all_141_1_479, 0 and discharging atoms relation(all_0_12_12) = all_141_1_479, relation(all_0_12_12) = 0, yields: % 51.06/21.41 | (298) all_141_1_479 = 0 % 51.06/21.41 | % 51.06/21.41 | Equations (298) can reduce 330 to: % 51.06/21.41 | (136) $false % 51.06/21.41 | % 51.06/21.41 |-The branch is then unsatisfiable % 51.06/21.41 |-Branch two: % 51.06/21.41 | (339) ~ (all_141_1_479 = 0) & function(all_0_12_12) = all_141_1_479 % 51.06/21.41 | % 51.06/21.41 | Applying alpha-rule on (339) yields: % 51.06/21.41 | (330) ~ (all_141_1_479 = 0) % 51.06/21.41 | (341) function(all_0_12_12) = all_141_1_479 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (97) with all_0_12_12, all_141_1_479, 0 and discharging atoms function(all_0_12_12) = all_141_1_479, function(all_0_12_12) = 0, yields: % 51.06/21.41 | (298) all_141_1_479 = 0 % 51.06/21.41 | % 51.06/21.41 | Equations (298) can reduce 330 to: % 51.06/21.41 | (136) $false % 51.06/21.41 | % 51.06/21.41 |-The branch is then unsatisfiable % 51.06/21.41 |-Branch two: % 51.06/21.41 | (344) ~ (all_301_1_1290 = 0) & one_to_one(all_0_10_10) = all_301_1_1290 % 51.06/21.41 | % 51.06/21.41 | Applying alpha-rule on (344) yields: % 51.06/21.41 | (345) ~ (all_301_1_1290 = 0) % 51.06/21.41 | (346) one_to_one(all_0_10_10) = all_301_1_1290 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (19) with all_0_10_10, 0, all_301_1_1290 and discharging atoms one_to_one(all_0_10_10) = all_301_1_1290, one_to_one(all_0_10_10) = 0, yields: % 51.06/21.41 | (249) all_301_1_1290 = 0 % 51.06/21.41 | % 51.06/21.41 | Equations (249) can reduce 345 to: % 51.06/21.41 | (136) $false % 51.06/21.41 | % 51.06/21.41 |-The branch is then unsatisfiable % 51.06/21.41 |-Branch two: % 51.06/21.41 | (349) ~ (all_301_1_1290 = 0) & relation(all_0_12_12) = all_301_1_1290 % 51.06/21.41 | % 51.06/21.41 | Applying alpha-rule on (349) yields: % 51.06/21.41 | (345) ~ (all_301_1_1290 = 0) % 51.06/21.41 | (351) relation(all_0_12_12) = all_301_1_1290 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (68) with all_0_12_12, all_301_1_1290, 0 and discharging atoms relation(all_0_12_12) = all_301_1_1290, relation(all_0_12_12) = 0, yields: % 51.06/21.41 | (249) all_301_1_1290 = 0 % 51.06/21.41 | % 51.06/21.41 | Equations (249) can reduce 345 to: % 51.06/21.41 | (136) $false % 51.06/21.41 | % 51.06/21.41 |-The branch is then unsatisfiable % 51.06/21.41 |-Branch two: % 51.06/21.41 | (354) ~ (all_301_1_1290 = 0) & function(all_0_12_12) = all_301_1_1290 % 51.06/21.41 | % 51.06/21.41 | Applying alpha-rule on (354) yields: % 51.06/21.41 | (345) ~ (all_301_1_1290 = 0) % 51.06/21.41 | (356) function(all_0_12_12) = all_301_1_1290 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (97) with all_0_12_12, all_301_1_1290, 0 and discharging atoms function(all_0_12_12) = all_301_1_1290, function(all_0_12_12) = 0, yields: % 51.06/21.41 | (249) all_301_1_1290 = 0 % 51.06/21.41 | % 51.06/21.41 | Equations (249) can reduce 345 to: % 51.06/21.41 | (136) $false % 51.06/21.41 | % 51.06/21.41 |-The branch is then unsatisfiable % 51.06/21.41 |-Branch two: % 51.06/21.41 | (359) ~ (all_161_0_702 = all_0_11_11) & relation_dom(all_161_1_703) = all_161_0_702 & relation_composition(all_0_12_12, all_0_8_8) = all_161_1_703 % 51.06/21.41 | % 51.06/21.41 | Applying alpha-rule on (359) yields: % 51.06/21.41 | (360) ~ (all_161_0_702 = all_0_11_11) % 51.06/21.41 | (361) relation_dom(all_161_1_703) = all_161_0_702 % 51.06/21.41 | (362) relation_composition(all_0_12_12, all_0_8_8) = all_161_1_703 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (15) with all_0_12_12, all_0_8_8, all_161_1_703, all_0_10_10 and discharging atoms relation_composition(all_0_12_12, all_0_8_8) = all_161_1_703, relation_composition(all_0_12_12, all_0_8_8) = all_0_10_10, yields: % 51.06/21.41 | (363) all_161_1_703 = all_0_10_10 % 51.06/21.41 | % 51.06/21.41 | From (363) and (361) follows: % 51.06/21.41 | (364) relation_dom(all_0_10_10) = all_161_0_702 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (105) with all_0_10_10, all_161_0_702, all_0_11_11 and discharging atoms relation_dom(all_0_10_10) = all_161_0_702, relation_dom(all_0_10_10) = all_0_11_11, yields: % 51.06/21.41 | (365) all_161_0_702 = all_0_11_11 % 51.06/21.41 | % 51.06/21.41 | Equations (365) can reduce 360 to: % 51.06/21.41 | (136) $false % 51.06/21.41 | % 51.06/21.41 |-The branch is then unsatisfiable % 51.06/21.41 |-Branch two: % 51.06/21.41 | (367) ~ (all_161_1_703 = 0) & relation(all_0_12_12) = all_161_1_703 % 51.06/21.41 | % 51.06/21.41 | Applying alpha-rule on (367) yields: % 51.06/21.41 | (368) ~ (all_161_1_703 = 0) % 51.06/21.41 | (369) relation(all_0_12_12) = all_161_1_703 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (68) with all_0_12_12, all_161_1_703, 0 and discharging atoms relation(all_0_12_12) = all_161_1_703, relation(all_0_12_12) = 0, yields: % 51.06/21.41 | (370) all_161_1_703 = 0 % 51.06/21.41 | % 51.06/21.41 | Equations (370) can reduce 368 to: % 51.06/21.41 | (136) $false % 51.06/21.41 | % 51.06/21.41 |-The branch is then unsatisfiable % 51.06/21.41 |-Branch two: % 51.06/21.41 | (372) ~ (all_161_1_703 = 0) & function(all_0_12_12) = all_161_1_703 % 51.06/21.41 | % 51.06/21.41 | Applying alpha-rule on (372) yields: % 51.06/21.41 | (368) ~ (all_161_1_703 = 0) % 51.06/21.41 | (374) function(all_0_12_12) = all_161_1_703 % 51.06/21.41 | % 51.06/21.41 | Instantiating formula (97) with all_0_12_12, all_161_1_703, 0 and discharging atoms function(all_0_12_12) = all_161_1_703, function(all_0_12_12) = 0, yields: % 51.06/21.41 | (370) all_161_1_703 = 0 % 51.06/21.41 | % 51.06/21.41 | Equations (370) can reduce 368 to: % 51.06/21.41 | (136) $false % 51.06/21.41 | % 51.06/21.41 |-The branch is then unsatisfiable % 51.06/21.41 % SZS output end Proof for theBenchmark % 51.06/21.41 % 51.06/21.41 20827ms %------------------------------------------------------------------------------