%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SEU020+1 : TPTP v8.1.2. Released v3.2.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n015.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 : 300s % DateTime : Thu Aug 31 17:42:19 EDT 2023 % Result : Theorem 13.93s 2.62s % Output : Proof 22.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SEU020+1 : TPTP v8.1.2. Released v3.2.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.35 % Computer : n015.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Aug 24 00:45:50 EDT 2023 % 0.13/0.35 % CPUTime : % 0.19/0.63 ________ _____ % 0.19/0.63 ___ __ \_________(_)________________________________ % 0.19/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.63 % 0.19/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.63 (2023-06-19) % 0.19/0.63 % 0.19/0.63 (c) Philipp Rümmer, 2009-2023 % 0.19/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.63 Amanda Stjerna. % 0.19/0.63 Free software under BSD-3-Clause. % 0.19/0.63 % 0.19/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.63 % 0.19/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.64 Running up to 7 provers in parallel. % 0.19/0.66 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.77/1.08 Prover 4: Preprocessing ... % 2.77/1.08 Prover 1: Preprocessing ... % 2.77/1.12 Prover 5: Preprocessing ... % 2.77/1.12 Prover 0: Preprocessing ... % 2.77/1.12 Prover 6: Preprocessing ... % 2.77/1.12 Prover 3: Preprocessing ... % 2.77/1.12 Prover 2: Preprocessing ... % 6.59/1.60 Prover 1: Warning: ignoring some quantifiers % 6.59/1.64 Prover 1: Constructing countermodel ... % 6.59/1.65 Prover 5: Proving ... % 6.59/1.65 Prover 3: Warning: ignoring some quantifiers % 6.59/1.67 Prover 3: Constructing countermodel ... % 6.59/1.67 Prover 6: Proving ... % 6.59/1.68 Prover 2: Proving ... % 7.41/1.79 Prover 4: Warning: ignoring some quantifiers % 8.14/1.82 Prover 4: Constructing countermodel ... % 8.83/1.96 Prover 0: Proving ... % 8.83/1.98 Prover 3: gave up % 8.83/1.98 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 9.55/2.09 Prover 7: Preprocessing ... % 10.53/2.23 Prover 7: Warning: ignoring some quantifiers % 11.26/2.24 Prover 7: Constructing countermodel ... % 11.26/2.26 Prover 1: gave up % 11.26/2.27 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 11.69/2.35 Prover 8: Preprocessing ... % 12.79/2.52 Prover 8: Warning: ignoring some quantifiers % 12.79/2.53 Prover 8: Constructing countermodel ... % 13.93/2.62 Prover 5: proved (1962ms) % 13.93/2.62 % 13.93/2.62 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.93/2.62 % 13.93/2.64 Prover 6: stopped % 13.93/2.65 Prover 2: stopped % 14.34/2.66 Prover 0: stopped % 14.34/2.67 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 14.34/2.67 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 14.34/2.67 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 14.34/2.67 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 14.34/2.68 Prover 10: Preprocessing ... % 14.34/2.71 Prover 11: Preprocessing ... % 14.34/2.73 Prover 13: Preprocessing ... % 14.34/2.74 Prover 16: Preprocessing ... % 15.07/2.80 Prover 16: Warning: ignoring some quantifiers % 15.07/2.80 Prover 16: Constructing countermodel ... % 15.07/2.81 Prover 10: Warning: ignoring some quantifiers % 15.07/2.81 Prover 10: Constructing countermodel ... % 15.83/2.87 Prover 13: Warning: ignoring some quantifiers % 15.83/2.88 Prover 13: Constructing countermodel ... % 15.83/2.88 Prover 10: gave up % 15.83/2.91 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 16.41/2.94 Prover 19: Preprocessing ... % 16.68/3.03 Prover 11: Warning: ignoring some quantifiers % 17.11/3.04 Prover 11: Constructing countermodel ... % 17.30/3.08 Prover 19: Warning: ignoring some quantifiers % 17.30/3.09 Prover 19: Constructing countermodel ... % 17.80/3.16 Prover 8: gave up % 21.26/3.61 Prover 19: gave up % 21.81/3.68 Prover 13: Found proof (size 125) % 21.81/3.68 Prover 13: proved (1024ms) % 21.81/3.68 Prover 11: stopped % 21.81/3.68 Prover 7: stopped % 21.81/3.69 Prover 16: stopped % 21.81/3.69 Prover 4: stopped % 21.81/3.69 % 21.81/3.69 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 21.81/3.69 % 22.02/3.72 % SZS output start Proof for theBenchmark % 22.02/3.73 Assumptions after simplification: % 22.02/3.73 --------------------------------- % 22.02/3.73 % 22.02/3.73 (dt_k5_relat_1) % 22.16/3.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (relation_composition(v0, v1) = % 22.16/3.75 v2) | ~ $i(v1) | ~ $i(v0) | ~ relation(v1) | ~ relation(v0) | % 22.16/3.75 relation(v2)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 22.16/3.75 relation(v1) | ~ relation(v0) | ? [v2: $i] : (relation_composition(v0, v1) % 22.16/3.75 = v2 & $i(v2) & relation(v2))) % 22.16/3.75 % 22.16/3.75 (fc1_funct_1) % 22.16/3.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (relation_composition(v0, v1) = % 22.16/3.76 v2) | ~ $i(v1) | ~ $i(v0) | ~ relation(v1) | ~ relation(v0) | ~ % 22.16/3.76 function(v1) | ~ function(v0) | relation(v2)) & ! [v0: $i] : ! [v1: $i] : % 22.16/3.76 ! [v2: $i] : ( ~ (relation_composition(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) % 22.16/3.76 | ~ relation(v1) | ~ relation(v0) | ~ function(v1) | ~ function(v0) | % 22.16/3.76 function(v2)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 22.16/3.76 relation(v1) | ~ relation(v0) | ~ function(v1) | ~ function(v0) | ? [v2: % 22.16/3.76 $i] : (relation_composition(v0, v1) = v2 & $i(v2) & relation(v2) & % 22.16/3.76 function(v2))) % 22.16/3.76 % 22.16/3.76 (rc1_funct_1) % 22.16/3.76 ? [v0: $i] : ($i(v0) & relation(v0) & function(v0)) % 22.16/3.76 % 22.16/3.76 (t27_funct_1) % 22.16/3.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (relation_rng(v2) % 22.16/3.76 = v3) | ~ (relation_dom(v0) = v1) | ~ $i(v2) | ~ $i(v0) | ~ % 22.16/3.76 relation(v2) | ~ relation(v0) | ~ function(v2) | ~ function(v0) | % 22.16/3.76 subset(v3, v1) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ( ~ (v6 = v5) & % 22.16/3.76 relation_dom(v4) = v5 & relation_dom(v2) = v6 & relation_composition(v2, % 22.16/3.76 v0) = v4 & $i(v6) & $i(v5) & $i(v4))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 22.16/3.76 relation(v0) | ~ function(v0) | ? [v1: $i] : (relation_dom(v0) = v1 & % 22.16/3.76 $i(v1) & ! [v2: $i] : ( ~ $i(v2) | ~ relation(v2) | ~ function(v2) | ? % 22.16/3.76 [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : (relation_rng(v2) = % 22.16/3.76 v6 & relation_dom(v3) = v4 & relation_dom(v2) = v5 & % 22.16/3.76 relation_composition(v2, v0) = v3 & $i(v6) & $i(v5) & $i(v4) & $i(v3) % 22.16/3.76 & ( ~ (v5 = v4) | subset(v6, v1)))))) % 22.16/3.76 % 22.16/3.76 (t47_funct_1) % 22.16/3.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (relation_rng(v2) % 22.16/3.77 = v3) | ~ (relation_dom(v0) = v1) | ~ $i(v2) | ~ $i(v0) | ~ subset(v3, % 22.16/3.77 v1) | ~ relation(v2) | ~ relation(v0) | ~ function(v2) | ~ % 22.16/3.77 function(v0) | one_to_one(v2) | ? [v4: $i] : (relation_composition(v2, v0) % 22.16/3.77 = v4 & $i(v4) & ~ one_to_one(v4))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 22.16/3.77 relation(v0) | ~ function(v0) | ? [v1: $i] : (relation_dom(v0) = v1 & % 22.16/3.77 $i(v1) & ! [v2: $i] : ( ~ $i(v2) | ~ relation(v2) | ~ function(v2) | % 22.16/3.77 one_to_one(v2) | ? [v3: $i] : ? [v4: $i] : (relation_rng(v2) = v4 & % 22.16/3.77 relation_composition(v2, v0) = v3 & $i(v4) & $i(v3) & ( ~ % 22.16/3.77 one_to_one(v3) | ~ subset(v4, v1)))))) % 22.16/3.77 % 22.16/3.77 (t52_funct_1) % 22.16/3.77 ! [v0: $i] : ! [v1: $i] : ( ~ (identity_relation(v0) = v1) | ~ $i(v0) | % 22.16/3.77 one_to_one(v1)) % 22.16/3.77 % 22.16/3.77 (t53_funct_1) % 22.16/3.77 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (relation_dom(v0) = v1 % 22.16/3.77 & identity_relation(v1) = v2 & relation_composition(v0, v3) = v2 & $i(v3) & % 22.16/3.77 $i(v2) & $i(v1) & $i(v0) & relation(v3) & relation(v0) & function(v3) & % 22.16/3.77 function(v0) & ~ one_to_one(v0)) % 22.16/3.77 % 22.16/3.77 (t71_relat_1) % 22.16/3.77 ! [v0: $i] : ! [v1: $i] : ( ~ (identity_relation(v0) = v1) | ~ $i(v0) | % 22.16/3.77 relation_rng(v1) = v0) & ! [v0: $i] : ! [v1: $i] : ( ~ % 22.16/3.77 (identity_relation(v0) = v1) | ~ $i(v0) | relation_dom(v1) = v0) & ? [v0: % 22.16/3.77 $i] : ( ~ $i(v0) | ? [v1: $i] : (relation_rng(v1) = v0 & % 22.16/3.77 identity_relation(v0) = v1 & $i(v1))) & ? [v0: $i] : ( ~ $i(v0) | ? [v1: % 22.16/3.77 $i] : (relation_dom(v1) = v0 & identity_relation(v0) = v1 & $i(v1))) % 22.16/3.77 % 22.16/3.77 (function-axioms) % 22.16/3.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.16/3.77 (relation_composition(v3, v2) = v1) | ~ (relation_composition(v3, v2) = % 22.16/3.77 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 22.16/3.77 (relation_rng(v2) = v1) | ~ (relation_rng(v2) = v0)) & ! [v0: $i] : ! % 22.16/3.77 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (relation_dom(v2) = v1) | ~ % 22.16/3.77 (relation_dom(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 22.16/3.77 v0 | ~ (powerset(v2) = v1) | ~ (powerset(v2) = v0)) & ! [v0: $i] : ! % 22.16/3.77 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (identity_relation(v2) = v1) | ~ % 22.16/3.77 (identity_relation(v2) = v0)) % 22.16/3.77 % 22.16/3.77 Further assumptions not needed in the proof: % 22.16/3.77 -------------------------------------------- % 22.16/3.77 antisymmetry_r2_hidden, cc1_funct_1, cc1_relat_1, dt_k6_relat_1, % 22.16/3.77 existence_m1_subset_1, fc10_relat_1, fc12_relat_1, fc1_subset_1, fc1_xboole_0, % 22.16/3.77 fc2_funct_1, fc4_relat_1, fc5_relat_1, fc6_relat_1, fc7_relat_1, fc8_relat_1, % 22.16/3.77 fc9_relat_1, rc1_relat_1, rc1_subset_1, rc1_xboole_0, rc2_relat_1, rc2_subset_1, % 22.16/3.77 rc2_xboole_0, rc3_relat_1, reflexivity_r1_tarski, t1_subset, t2_subset, % 22.16/3.77 t3_subset, t4_subset, t5_subset, t6_boole, t7_boole, t8_boole % 22.16/3.77 % 22.16/3.77 Those formulas are unsatisfiable: % 22.16/3.77 --------------------------------- % 22.16/3.77 % 22.16/3.77 Begin of proof % 22.16/3.77 | % 22.16/3.77 | ALPHA: (dt_k5_relat_1) implies: % 22.16/3.78 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ relation(v1) | % 22.16/3.78 | ~ relation(v0) | ? [v2: $i] : (relation_composition(v0, v1) = v2 & % 22.16/3.78 | $i(v2) & relation(v2))) % 22.16/3.78 | % 22.16/3.78 | ALPHA: (fc1_funct_1) implies: % 22.16/3.78 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ relation(v1) | % 22.16/3.78 | ~ relation(v0) | ~ function(v1) | ~ function(v0) | ? [v2: $i] : % 22.16/3.78 | (relation_composition(v0, v1) = v2 & $i(v2) & relation(v2) & % 22.16/3.78 | function(v2))) % 22.16/3.78 | % 22.16/3.78 | ALPHA: (t27_funct_1) implies: % 22.16/3.78 | (3) ! [v0: $i] : ( ~ $i(v0) | ~ relation(v0) | ~ function(v0) | ? [v1: % 22.16/3.78 | $i] : (relation_dom(v0) = v1 & $i(v1) & ! [v2: $i] : ( ~ $i(v2) | % 22.16/3.78 | ~ relation(v2) | ~ function(v2) | ? [v3: $i] : ? [v4: $i] : ? % 22.16/3.78 | [v5: $i] : ? [v6: $i] : (relation_rng(v2) = v6 & % 22.16/3.78 | relation_dom(v3) = v4 & relation_dom(v2) = v5 & % 22.16/3.78 | relation_composition(v2, v0) = v3 & $i(v6) & $i(v5) & $i(v4) & % 22.16/3.78 | $i(v3) & ( ~ (v5 = v4) | subset(v6, v1)))))) % 22.16/3.78 | % 22.16/3.78 | ALPHA: (t47_funct_1) implies: % 22.16/3.78 | (4) ! [v0: $i] : ( ~ $i(v0) | ~ relation(v0) | ~ function(v0) | ? [v1: % 22.16/3.78 | $i] : (relation_dom(v0) = v1 & $i(v1) & ! [v2: $i] : ( ~ $i(v2) | % 22.16/3.78 | ~ relation(v2) | ~ function(v2) | one_to_one(v2) | ? [v3: $i] : % 22.16/3.78 | ? [v4: $i] : (relation_rng(v2) = v4 & relation_composition(v2, % 22.16/3.78 | v0) = v3 & $i(v4) & $i(v3) & ( ~ one_to_one(v3) | ~ % 22.16/3.78 | subset(v4, v1)))))) % 22.16/3.78 | % 22.16/3.78 | ALPHA: (t71_relat_1) implies: % 22.16/3.78 | (5) ! [v0: $i] : ! [v1: $i] : ( ~ (identity_relation(v0) = v1) | ~ % 22.16/3.78 | $i(v0) | relation_dom(v1) = v0) % 22.16/3.78 | % 22.16/3.78 | ALPHA: (function-axioms) implies: % 22.16/3.78 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 22.16/3.78 | (relation_dom(v2) = v1) | ~ (relation_dom(v2) = v0)) % 22.16/3.78 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 22.16/3.78 | (relation_rng(v2) = v1) | ~ (relation_rng(v2) = v0)) % 22.16/3.78 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.16/3.78 | (relation_composition(v3, v2) = v1) | ~ (relation_composition(v3, % 22.16/3.78 | v2) = v0)) % 22.16/3.78 | % 22.16/3.78 | DELTA: instantiating (rc1_funct_1) with fresh symbol all_42_0 gives: % 22.16/3.78 | (9) $i(all_42_0) & relation(all_42_0) & function(all_42_0) % 22.16/3.78 | % 22.16/3.78 | ALPHA: (9) implies: % 22.16/3.78 | (10) function(all_42_0) % 22.16/3.78 | (11) relation(all_42_0) % 22.16/3.78 | (12) $i(all_42_0) % 22.16/3.78 | % 22.16/3.78 | DELTA: instantiating (t53_funct_1) with fresh symbols all_49_0, all_49_1, % 22.16/3.78 | all_49_2, all_49_3 gives: % 22.16/3.78 | (13) relation_dom(all_49_3) = all_49_2 & identity_relation(all_49_2) = % 22.16/3.78 | all_49_1 & relation_composition(all_49_3, all_49_0) = all_49_1 & % 22.16/3.78 | $i(all_49_0) & $i(all_49_1) & $i(all_49_2) & $i(all_49_3) & % 22.16/3.78 | relation(all_49_0) & relation(all_49_3) & function(all_49_0) & % 22.16/3.78 | function(all_49_3) & ~ one_to_one(all_49_3) % 22.16/3.78 | % 22.16/3.78 | ALPHA: (13) implies: % 22.16/3.78 | (14) ~ one_to_one(all_49_3) % 22.16/3.78 | (15) function(all_49_3) % 22.16/3.78 | (16) function(all_49_0) % 22.16/3.78 | (17) relation(all_49_3) % 22.16/3.78 | (18) relation(all_49_0) % 22.16/3.78 | (19) $i(all_49_3) % 22.16/3.78 | (20) $i(all_49_2) % 22.16/3.78 | (21) $i(all_49_0) % 22.16/3.78 | (22) relation_composition(all_49_3, all_49_0) = all_49_1 % 22.16/3.78 | (23) identity_relation(all_49_2) = all_49_1 % 22.16/3.78 | (24) relation_dom(all_49_3) = all_49_2 % 22.16/3.78 | % 22.16/3.79 | GROUND_INST: instantiating (4) with all_42_0, simplifying with (10), (11), % 22.16/3.79 | (12) gives: % 22.16/3.79 | (25) ? [v0: $i] : (relation_dom(all_42_0) = v0 & $i(v0) & ! [v1: $i] : ( % 22.16/3.79 | ~ $i(v1) | ~ relation(v1) | ~ function(v1) | one_to_one(v1) | ? % 22.16/3.79 | [v2: $i] : ? [v3: $i] : (relation_rng(v1) = v3 & % 22.16/3.79 | relation_composition(v1, all_42_0) = v2 & $i(v3) & $i(v2) & ( ~ % 22.16/3.79 | one_to_one(v2) | ~ subset(v3, v0))))) % 22.16/3.79 | % 22.16/3.79 | GROUND_INST: instantiating (3) with all_42_0, simplifying with (10), (11), % 22.16/3.79 | (12) gives: % 22.16/3.79 | (26) ? [v0: $i] : (relation_dom(all_42_0) = v0 & $i(v0) & ! [v1: $i] : ( % 22.16/3.79 | ~ $i(v1) | ~ relation(v1) | ~ function(v1) | ? [v2: $i] : ? % 22.16/3.79 | [v3: $i] : ? [v4: $i] : ? [v5: $i] : (relation_rng(v1) = v5 & % 22.16/3.79 | relation_dom(v2) = v3 & relation_dom(v1) = v4 & % 22.16/3.79 | relation_composition(v1, all_42_0) = v2 & $i(v5) & $i(v4) & % 22.16/3.79 | $i(v3) & $i(v2) & ( ~ (v4 = v3) | subset(v5, v0))))) % 22.16/3.79 | % 22.16/3.79 | GROUND_INST: instantiating (4) with all_49_3, simplifying with (15), (17), % 22.16/3.79 | (19) gives: % 22.16/3.79 | (27) ? [v0: $i] : (relation_dom(all_49_3) = v0 & $i(v0) & ! [v1: $i] : ( % 22.16/3.79 | ~ $i(v1) | ~ relation(v1) | ~ function(v1) | one_to_one(v1) | ? % 22.16/3.79 | [v2: $i] : ? [v3: $i] : (relation_rng(v1) = v3 & % 22.16/3.79 | relation_composition(v1, all_49_3) = v2 & $i(v3) & $i(v2) & ( ~ % 22.16/3.79 | one_to_one(v2) | ~ subset(v3, v0))))) % 22.16/3.79 | % 22.16/3.79 | GROUND_INST: instantiating (3) with all_49_3, simplifying with (15), (17), % 22.16/3.79 | (19) gives: % 22.16/3.79 | (28) ? [v0: $i] : (relation_dom(all_49_3) = v0 & $i(v0) & ! [v1: $i] : ( % 22.16/3.79 | ~ $i(v1) | ~ relation(v1) | ~ function(v1) | ? [v2: $i] : ? % 22.16/3.79 | [v3: $i] : ? [v4: $i] : ? [v5: $i] : (relation_rng(v1) = v5 & % 22.16/3.79 | relation_dom(v2) = v3 & relation_dom(v1) = v4 & % 22.16/3.79 | relation_composition(v1, all_49_3) = v2 & $i(v5) & $i(v4) & % 22.16/3.79 | $i(v3) & $i(v2) & ( ~ (v4 = v3) | subset(v5, v0))))) % 22.16/3.79 | % 22.16/3.79 | GROUND_INST: instantiating (2) with all_49_3, all_49_0, simplifying with (15), % 22.16/3.79 | (16), (17), (18), (19), (21) gives: % 22.16/3.79 | (29) ? [v0: $i] : (relation_composition(all_49_3, all_49_0) = v0 & $i(v0) % 22.16/3.79 | & relation(v0) & function(v0)) % 22.16/3.79 | % 22.16/3.79 | GROUND_INST: instantiating (1) with all_49_3, all_49_0, simplifying with (17), % 22.16/3.79 | (18), (19), (21) gives: % 22.16/3.79 | (30) ? [v0: $i] : (relation_composition(all_49_3, all_49_0) = v0 & $i(v0) % 22.16/3.79 | & relation(v0)) % 22.16/3.79 | % 22.16/3.79 | GROUND_INST: instantiating (4) with all_49_0, simplifying with (16), (18), % 22.16/3.79 | (21) gives: % 22.16/3.79 | (31) ? [v0: $i] : (relation_dom(all_49_0) = v0 & $i(v0) & ! [v1: $i] : ( % 22.16/3.79 | ~ $i(v1) | ~ relation(v1) | ~ function(v1) | one_to_one(v1) | ? % 22.16/3.79 | [v2: $i] : ? [v3: $i] : (relation_rng(v1) = v3 & % 22.16/3.79 | relation_composition(v1, all_49_0) = v2 & $i(v3) & $i(v2) & ( ~ % 22.16/3.79 | one_to_one(v2) | ~ subset(v3, v0))))) % 22.16/3.79 | % 22.16/3.79 | GROUND_INST: instantiating (3) with all_49_0, simplifying with (16), (18), % 22.16/3.79 | (21) gives: % 22.16/3.79 | (32) ? [v0: $i] : (relation_dom(all_49_0) = v0 & $i(v0) & ! [v1: $i] : ( % 22.16/3.79 | ~ $i(v1) | ~ relation(v1) | ~ function(v1) | ? [v2: $i] : ? % 22.16/3.79 | [v3: $i] : ? [v4: $i] : ? [v5: $i] : (relation_rng(v1) = v5 & % 22.16/3.79 | relation_dom(v2) = v3 & relation_dom(v1) = v4 & % 22.16/3.79 | relation_composition(v1, all_49_0) = v2 & $i(v5) & $i(v4) & % 22.16/3.79 | $i(v3) & $i(v2) & ( ~ (v4 = v3) | subset(v5, v0))))) % 22.16/3.79 | % 22.16/3.79 | GROUND_INST: instantiating (5) with all_49_2, all_49_1, simplifying with (20), % 22.16/3.79 | (23) gives: % 22.16/3.79 | (33) relation_dom(all_49_1) = all_49_2 % 22.16/3.79 | % 22.16/3.79 | GROUND_INST: instantiating (t52_funct_1) with all_49_2, all_49_1, simplifying % 22.16/3.79 | with (20), (23) gives: % 22.16/3.79 | (34) one_to_one(all_49_1) % 22.16/3.79 | % 22.16/3.79 | DELTA: instantiating (30) with fresh symbol all_63_0 gives: % 22.16/3.80 | (35) relation_composition(all_49_3, all_49_0) = all_63_0 & $i(all_63_0) & % 22.16/3.80 | relation(all_63_0) % 22.16/3.80 | % 22.16/3.80 | ALPHA: (35) implies: % 22.16/3.80 | (36) relation_composition(all_49_3, all_49_0) = all_63_0 % 22.16/3.80 | % 22.16/3.80 | DELTA: instantiating (29) with fresh symbol all_183_0 gives: % 22.16/3.80 | (37) relation_composition(all_49_3, all_49_0) = all_183_0 & $i(all_183_0) & % 22.16/3.80 | relation(all_183_0) & function(all_183_0) % 22.16/3.80 | % 22.16/3.80 | ALPHA: (37) implies: % 22.16/3.80 | (38) relation_composition(all_49_3, all_49_0) = all_183_0 % 22.16/3.80 | % 22.16/3.80 | DELTA: instantiating (25) with fresh symbol all_265_0 gives: % 22.16/3.80 | (39) relation_dom(all_42_0) = all_265_0 & $i(all_265_0) & ! [v0: $i] : ( ~ % 22.16/3.80 | $i(v0) | ~ relation(v0) | ~ function(v0) | one_to_one(v0) | ? % 22.16/3.80 | [v1: $i] : ? [v2: $i] : (relation_rng(v0) = v2 & % 22.16/3.80 | relation_composition(v0, all_42_0) = v1 & $i(v2) & $i(v1) & ( ~ % 22.16/3.80 | one_to_one(v1) | ~ subset(v2, all_265_0)))) % 22.16/3.80 | % 22.16/3.80 | ALPHA: (39) implies: % 22.16/3.80 | (40) ! [v0: $i] : ( ~ $i(v0) | ~ relation(v0) | ~ function(v0) | % 22.16/3.80 | one_to_one(v0) | ? [v1: $i] : ? [v2: $i] : (relation_rng(v0) = v2 % 22.16/3.80 | & relation_composition(v0, all_42_0) = v1 & $i(v2) & $i(v1) & ( ~ % 22.16/3.80 | one_to_one(v1) | ~ subset(v2, all_265_0)))) % 22.16/3.80 | % 22.16/3.80 | GROUND_INST: instantiating (40) with all_49_3, simplifying with (14), (15), % 22.16/3.80 | (17), (19) gives: % 22.16/3.80 | (41) ? [v0: $i] : ? [v1: $i] : (relation_rng(all_49_3) = v1 & % 22.16/3.80 | relation_composition(all_49_3, all_42_0) = v0 & $i(v1) & $i(v0) & ( % 22.16/3.80 | ~ one_to_one(v0) | ~ subset(v1, all_265_0))) % 22.16/3.80 | % 22.16/3.80 | DELTA: instantiating (31) with fresh symbol all_268_0 gives: % 22.16/3.80 | (42) relation_dom(all_49_0) = all_268_0 & $i(all_268_0) & ! [v0: $i] : ( ~ % 22.16/3.80 | $i(v0) | ~ relation(v0) | ~ function(v0) | one_to_one(v0) | ? % 22.16/3.80 | [v1: $i] : ? [v2: $i] : (relation_rng(v0) = v2 & % 22.16/3.80 | relation_composition(v0, all_49_0) = v1 & $i(v2) & $i(v1) & ( ~ % 22.16/3.80 | one_to_one(v1) | ~ subset(v2, all_268_0)))) % 22.16/3.80 | % 22.16/3.80 | ALPHA: (42) implies: % 22.16/3.80 | (43) relation_dom(all_49_0) = all_268_0 % 22.16/3.80 | (44) ! [v0: $i] : ( ~ $i(v0) | ~ relation(v0) | ~ function(v0) | % 22.16/3.80 | one_to_one(v0) | ? [v1: $i] : ? [v2: $i] : (relation_rng(v0) = v2 % 22.16/3.80 | & relation_composition(v0, all_49_0) = v1 & $i(v2) & $i(v1) & ( ~ % 22.16/3.80 | one_to_one(v1) | ~ subset(v2, all_268_0)))) % 22.16/3.80 | % 22.16/3.80 | GROUND_INST: instantiating (44) with all_49_3, simplifying with (14), (15), % 22.16/3.80 | (17), (19) gives: % 22.16/3.80 | (45) ? [v0: $i] : ? [v1: $i] : (relation_rng(all_49_3) = v1 & % 22.16/3.80 | relation_composition(all_49_3, all_49_0) = v0 & $i(v1) & $i(v0) & ( % 22.16/3.80 | ~ one_to_one(v0) | ~ subset(v1, all_268_0))) % 22.16/3.80 | % 22.16/3.80 | DELTA: instantiating (27) with fresh symbol all_271_0 gives: % 22.16/3.80 | (46) relation_dom(all_49_3) = all_271_0 & $i(all_271_0) & ! [v0: $i] : ( ~ % 22.16/3.80 | $i(v0) | ~ relation(v0) | ~ function(v0) | one_to_one(v0) | ? % 22.16/3.80 | [v1: $i] : ? [v2: $i] : (relation_rng(v0) = v2 & % 22.16/3.80 | relation_composition(v0, all_49_3) = v1 & $i(v2) & $i(v1) & ( ~ % 22.16/3.80 | one_to_one(v1) | ~ subset(v2, all_271_0)))) % 22.16/3.80 | % 22.16/3.80 | ALPHA: (46) implies: % 22.16/3.80 | (47) relation_dom(all_49_3) = all_271_0 % 22.16/3.80 | (48) ! [v0: $i] : ( ~ $i(v0) | ~ relation(v0) | ~ function(v0) | % 22.16/3.80 | one_to_one(v0) | ? [v1: $i] : ? [v2: $i] : (relation_rng(v0) = v2 % 22.16/3.80 | & relation_composition(v0, all_49_3) = v1 & $i(v2) & $i(v1) & ( ~ % 22.16/3.80 | one_to_one(v1) | ~ subset(v2, all_271_0)))) % 22.16/3.80 | % 22.16/3.80 | GROUND_INST: instantiating (48) with all_49_3, simplifying with (14), (15), % 22.16/3.80 | (17), (19) gives: % 22.16/3.80 | (49) ? [v0: $i] : ? [v1: $i] : (relation_rng(all_49_3) = v1 & % 22.16/3.80 | relation_composition(all_49_3, all_49_3) = v0 & $i(v1) & $i(v0) & ( % 22.16/3.80 | ~ one_to_one(v0) | ~ subset(v1, all_271_0))) % 22.16/3.80 | % 22.16/3.80 | DELTA: instantiating (32) with fresh symbol all_274_0 gives: % 22.16/3.80 | (50) relation_dom(all_49_0) = all_274_0 & $i(all_274_0) & ! [v0: $i] : ( ~ % 22.16/3.81 | $i(v0) | ~ relation(v0) | ~ function(v0) | ? [v1: $i] : ? [v2: % 22.16/3.81 | $i] : ? [v3: $i] : ? [v4: $i] : (relation_rng(v0) = v4 & % 22.16/3.81 | relation_dom(v1) = v2 & relation_dom(v0) = v3 & % 22.16/3.81 | relation_composition(v0, all_49_0) = v1 & $i(v4) & $i(v3) & $i(v2) % 22.16/3.81 | & $i(v1) & ( ~ (v3 = v2) | subset(v4, all_274_0)))) % 22.16/3.81 | % 22.16/3.81 | ALPHA: (50) implies: % 22.16/3.81 | (51) relation_dom(all_49_0) = all_274_0 % 22.16/3.81 | (52) ! [v0: $i] : ( ~ $i(v0) | ~ relation(v0) | ~ function(v0) | ? [v1: % 22.16/3.81 | $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (relation_rng(v0) % 22.16/3.81 | = v4 & relation_dom(v1) = v2 & relation_dom(v0) = v3 & % 22.16/3.81 | relation_composition(v0, all_49_0) = v1 & $i(v4) & $i(v3) & $i(v2) % 22.16/3.81 | & $i(v1) & ( ~ (v3 = v2) | subset(v4, all_274_0)))) % 22.16/3.81 | % 22.16/3.81 | GROUND_INST: instantiating (52) with all_49_3, simplifying with (15), (17), % 22.16/3.81 | (19) gives: % 22.16/3.81 | (53) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 22.16/3.81 | (relation_rng(all_49_3) = v3 & relation_dom(v0) = v1 & % 22.16/3.81 | relation_dom(all_49_3) = v2 & relation_composition(all_49_3, % 22.16/3.81 | all_49_0) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v1) % 22.16/3.81 | | subset(v3, all_274_0))) % 22.16/3.81 | % 22.16/3.81 | GROUND_INST: instantiating (52) with all_49_0, simplifying with (16), (18), % 22.16/3.81 | (21) gives: % 22.16/3.81 | (54) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 22.16/3.81 | (relation_rng(all_49_0) = v3 & relation_dom(v0) = v1 & % 22.16/3.81 | relation_dom(all_49_0) = v2 & relation_composition(all_49_0, % 22.16/3.81 | all_49_0) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v1) % 22.16/3.81 | | subset(v3, all_274_0))) % 22.16/3.81 | % 22.16/3.81 | DELTA: instantiating (26) with fresh symbol all_277_0 gives: % 22.16/3.81 | (55) relation_dom(all_42_0) = all_277_0 & $i(all_277_0) & ! [v0: $i] : ( ~ % 22.16/3.81 | $i(v0) | ~ relation(v0) | ~ function(v0) | ? [v1: $i] : ? [v2: % 22.16/3.81 | $i] : ? [v3: $i] : ? [v4: $i] : (relation_rng(v0) = v4 & % 22.16/3.81 | relation_dom(v1) = v2 & relation_dom(v0) = v3 & % 22.16/3.81 | relation_composition(v0, all_42_0) = v1 & $i(v4) & $i(v3) & $i(v2) % 22.16/3.81 | & $i(v1) & ( ~ (v3 = v2) | subset(v4, all_277_0)))) % 22.16/3.81 | % 22.16/3.81 | ALPHA: (55) implies: % 22.16/3.81 | (56) ! [v0: $i] : ( ~ $i(v0) | ~ relation(v0) | ~ function(v0) | ? [v1: % 22.16/3.81 | $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (relation_rng(v0) % 22.16/3.81 | = v4 & relation_dom(v1) = v2 & relation_dom(v0) = v3 & % 22.16/3.81 | relation_composition(v0, all_42_0) = v1 & $i(v4) & $i(v3) & $i(v2) % 22.16/3.81 | & $i(v1) & ( ~ (v3 = v2) | subset(v4, all_277_0)))) % 22.16/3.81 | % 22.16/3.81 | GROUND_INST: instantiating (56) with all_49_3, simplifying with (15), (17), % 22.16/3.81 | (19) gives: % 22.16/3.81 | (57) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 22.16/3.81 | (relation_rng(all_49_3) = v3 & relation_dom(v0) = v1 & % 22.16/3.81 | relation_dom(all_49_3) = v2 & relation_composition(all_49_3, % 22.16/3.81 | all_42_0) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v1) % 22.16/3.81 | | subset(v3, all_277_0))) % 22.16/3.81 | % 22.16/3.81 | GROUND_INST: instantiating (56) with all_49_0, simplifying with (16), (18), % 22.16/3.81 | (21) gives: % 22.16/3.81 | (58) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 22.16/3.81 | (relation_rng(all_49_0) = v3 & relation_dom(v0) = v1 & % 22.16/3.81 | relation_dom(all_49_0) = v2 & relation_composition(all_49_0, % 22.16/3.81 | all_42_0) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v1) % 22.16/3.81 | | subset(v3, all_277_0))) % 22.16/3.81 | % 22.16/3.81 | DELTA: instantiating (28) with fresh symbol all_280_0 gives: % 22.16/3.81 | (59) relation_dom(all_49_3) = all_280_0 & $i(all_280_0) & ! [v0: $i] : ( ~ % 22.16/3.81 | $i(v0) | ~ relation(v0) | ~ function(v0) | ? [v1: $i] : ? [v2: % 22.16/3.81 | $i] : ? [v3: $i] : ? [v4: $i] : (relation_rng(v0) = v4 & % 22.16/3.81 | relation_dom(v1) = v2 & relation_dom(v0) = v3 & % 22.16/3.81 | relation_composition(v0, all_49_3) = v1 & $i(v4) & $i(v3) & $i(v2) % 22.16/3.81 | & $i(v1) & ( ~ (v3 = v2) | subset(v4, all_280_0)))) % 22.16/3.81 | % 22.16/3.81 | ALPHA: (59) implies: % 22.16/3.81 | (60) relation_dom(all_49_3) = all_280_0 % 22.16/3.82 | (61) ! [v0: $i] : ( ~ $i(v0) | ~ relation(v0) | ~ function(v0) | ? [v1: % 22.16/3.82 | $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (relation_rng(v0) % 22.16/3.82 | = v4 & relation_dom(v1) = v2 & relation_dom(v0) = v3 & % 22.16/3.82 | relation_composition(v0, all_49_3) = v1 & $i(v4) & $i(v3) & $i(v2) % 22.16/3.82 | & $i(v1) & ( ~ (v3 = v2) | subset(v4, all_280_0)))) % 22.16/3.82 | % 22.16/3.82 | GROUND_INST: instantiating (61) with all_49_3, simplifying with (15), (17), % 22.16/3.82 | (19) gives: % 22.16/3.82 | (62) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 22.16/3.82 | (relation_rng(all_49_3) = v3 & relation_dom(v0) = v1 & % 22.16/3.82 | relation_dom(all_49_3) = v2 & relation_composition(all_49_3, % 22.16/3.82 | all_49_3) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v1) % 22.16/3.82 | | subset(v3, all_280_0))) % 22.16/3.82 | % 22.16/3.82 | GROUND_INST: instantiating (61) with all_49_0, simplifying with (16), (18), % 22.16/3.82 | (21) gives: % 22.16/3.82 | (63) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 22.16/3.82 | (relation_rng(all_49_0) = v3 & relation_dom(v0) = v1 & % 22.16/3.82 | relation_dom(all_49_0) = v2 & relation_composition(all_49_0, % 22.16/3.82 | all_49_3) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v1) % 22.16/3.82 | | subset(v3, all_280_0))) % 22.16/3.82 | % 22.16/3.82 | DELTA: instantiating (41) with fresh symbols all_283_0, all_283_1 gives: % 22.16/3.82 | (64) relation_rng(all_49_3) = all_283_0 & relation_composition(all_49_3, % 22.16/3.82 | all_42_0) = all_283_1 & $i(all_283_0) & $i(all_283_1) & ( ~ % 22.16/3.82 | one_to_one(all_283_1) | ~ subset(all_283_0, all_265_0)) % 22.16/3.82 | % 22.16/3.82 | ALPHA: (64) implies: % 22.16/3.82 | (65) relation_rng(all_49_3) = all_283_0 % 22.16/3.82 | % 22.16/3.82 | DELTA: instantiating (45) with fresh symbols all_285_0, all_285_1 gives: % 22.16/3.82 | (66) relation_rng(all_49_3) = all_285_0 & relation_composition(all_49_3, % 22.16/3.82 | all_49_0) = all_285_1 & $i(all_285_0) & $i(all_285_1) & ( ~ % 22.16/3.82 | one_to_one(all_285_1) | ~ subset(all_285_0, all_268_0)) % 22.16/3.82 | % 22.16/3.82 | ALPHA: (66) implies: % 22.16/3.82 | (67) relation_composition(all_49_3, all_49_0) = all_285_1 % 22.16/3.82 | (68) relation_rng(all_49_3) = all_285_0 % 22.16/3.82 | (69) ~ one_to_one(all_285_1) | ~ subset(all_285_0, all_268_0) % 22.16/3.82 | % 22.16/3.82 | DELTA: instantiating (49) with fresh symbols all_287_0, all_287_1 gives: % 22.16/3.82 | (70) relation_rng(all_49_3) = all_287_0 & relation_composition(all_49_3, % 22.16/3.82 | all_49_3) = all_287_1 & $i(all_287_0) & $i(all_287_1) & ( ~ % 22.16/3.82 | one_to_one(all_287_1) | ~ subset(all_287_0, all_271_0)) % 22.16/3.82 | % 22.16/3.82 | ALPHA: (70) implies: % 22.16/3.82 | (71) relation_rng(all_49_3) = all_287_0 % 22.16/3.82 | % 22.16/3.82 | DELTA: instantiating (54) with fresh symbols all_289_0, all_289_1, all_289_2, % 22.16/3.82 | all_289_3 gives: % 22.16/3.82 | (72) relation_rng(all_49_0) = all_289_0 & relation_dom(all_289_3) = % 22.16/3.82 | all_289_2 & relation_dom(all_49_0) = all_289_1 & % 22.16/3.82 | relation_composition(all_49_0, all_49_0) = all_289_3 & $i(all_289_0) & % 22.16/3.82 | $i(all_289_1) & $i(all_289_2) & $i(all_289_3) & ( ~ (all_289_1 = % 22.16/3.82 | all_289_2) | subset(all_289_0, all_274_0)) % 22.16/3.82 | % 22.16/3.82 | ALPHA: (72) implies: % 22.16/3.82 | (73) relation_dom(all_49_0) = all_289_1 % 22.16/3.82 | % 22.16/3.82 | DELTA: instantiating (53) with fresh symbols all_291_0, all_291_1, all_291_2, % 22.16/3.82 | all_291_3 gives: % 22.16/3.82 | (74) relation_rng(all_49_3) = all_291_0 & relation_dom(all_291_3) = % 22.16/3.82 | all_291_2 & relation_dom(all_49_3) = all_291_1 & % 22.16/3.82 | relation_composition(all_49_3, all_49_0) = all_291_3 & $i(all_291_0) & % 22.16/3.82 | $i(all_291_1) & $i(all_291_2) & $i(all_291_3) & ( ~ (all_291_1 = % 22.16/3.82 | all_291_2) | subset(all_291_0, all_274_0)) % 22.16/3.82 | % 22.16/3.82 | ALPHA: (74) implies: % 22.16/3.82 | (75) relation_composition(all_49_3, all_49_0) = all_291_3 % 22.16/3.82 | (76) relation_dom(all_49_3) = all_291_1 % 22.16/3.82 | (77) relation_dom(all_291_3) = all_291_2 % 22.16/3.82 | (78) relation_rng(all_49_3) = all_291_0 % 22.16/3.82 | (79) ~ (all_291_1 = all_291_2) | subset(all_291_0, all_274_0) % 22.16/3.82 | % 22.16/3.82 | DELTA: instantiating (58) with fresh symbols all_295_0, all_295_1, all_295_2, % 22.16/3.82 | all_295_3 gives: % 22.16/3.82 | (80) relation_rng(all_49_0) = all_295_0 & relation_dom(all_295_3) = % 22.16/3.82 | all_295_2 & relation_dom(all_49_0) = all_295_1 & % 22.16/3.82 | relation_composition(all_49_0, all_42_0) = all_295_3 & $i(all_295_0) & % 22.16/3.82 | $i(all_295_1) & $i(all_295_2) & $i(all_295_3) & ( ~ (all_295_1 = % 22.16/3.82 | all_295_2) | subset(all_295_0, all_277_0)) % 22.16/3.82 | % 22.16/3.82 | ALPHA: (80) implies: % 22.16/3.82 | (81) relation_dom(all_49_0) = all_295_1 % 22.16/3.82 | % 22.16/3.82 | DELTA: instantiating (57) with fresh symbols all_297_0, all_297_1, all_297_2, % 22.16/3.82 | all_297_3 gives: % 22.16/3.82 | (82) relation_rng(all_49_3) = all_297_0 & relation_dom(all_297_3) = % 22.16/3.82 | all_297_2 & relation_dom(all_49_3) = all_297_1 & % 22.16/3.82 | relation_composition(all_49_3, all_42_0) = all_297_3 & $i(all_297_0) & % 22.16/3.82 | $i(all_297_1) & $i(all_297_2) & $i(all_297_3) & ( ~ (all_297_1 = % 22.16/3.82 | all_297_2) | subset(all_297_0, all_277_0)) % 22.16/3.82 | % 22.16/3.82 | ALPHA: (82) implies: % 22.16/3.82 | (83) relation_dom(all_49_3) = all_297_1 % 22.16/3.82 | (84) relation_rng(all_49_3) = all_297_0 % 22.16/3.82 | % 22.16/3.82 | DELTA: instantiating (63) with fresh symbols all_301_0, all_301_1, all_301_2, % 22.16/3.82 | all_301_3 gives: % 22.16/3.82 | (85) relation_rng(all_49_0) = all_301_0 & relation_dom(all_301_3) = % 22.16/3.82 | all_301_2 & relation_dom(all_49_0) = all_301_1 & % 22.16/3.82 | relation_composition(all_49_0, all_49_3) = all_301_3 & $i(all_301_0) & % 22.16/3.82 | $i(all_301_1) & $i(all_301_2) & $i(all_301_3) & ( ~ (all_301_1 = % 22.16/3.82 | all_301_2) | subset(all_301_0, all_280_0)) % 22.16/3.82 | % 22.16/3.82 | ALPHA: (85) implies: % 22.16/3.82 | (86) relation_dom(all_49_0) = all_301_1 % 22.16/3.82 | % 22.16/3.82 | DELTA: instantiating (62) with fresh symbols all_303_0, all_303_1, all_303_2, % 22.16/3.82 | all_303_3 gives: % 22.16/3.83 | (87) relation_rng(all_49_3) = all_303_0 & relation_dom(all_303_3) = % 22.16/3.83 | all_303_2 & relation_dom(all_49_3) = all_303_1 & % 22.16/3.83 | relation_composition(all_49_3, all_49_3) = all_303_3 & $i(all_303_0) & % 22.16/3.83 | $i(all_303_1) & $i(all_303_2) & $i(all_303_3) & ( ~ (all_303_1 = % 22.16/3.83 | all_303_2) | subset(all_303_0, all_280_0)) % 22.16/3.83 | % 22.16/3.83 | ALPHA: (87) implies: % 22.16/3.83 | (88) relation_dom(all_49_3) = all_303_1 % 22.16/3.83 | (89) relation_rng(all_49_3) = all_303_0 % 22.16/3.83 | % 22.16/3.83 | GROUND_INST: instantiating (8) with all_183_0, all_285_1, all_49_0, all_49_3, % 22.16/3.83 | simplifying with (38), (67) gives: % 22.16/3.83 | (90) all_285_1 = all_183_0 % 22.16/3.83 | % 22.16/3.83 | GROUND_INST: instantiating (8) with all_63_0, all_285_1, all_49_0, all_49_3, % 22.16/3.83 | simplifying with (36), (67) gives: % 22.16/3.83 | (91) all_285_1 = all_63_0 % 22.16/3.83 | % 22.16/3.83 | GROUND_INST: instantiating (8) with all_49_1, all_291_3, all_49_0, all_49_3, % 22.16/3.83 | simplifying with (22), (75) gives: % 22.16/3.83 | (92) all_291_3 = all_49_1 % 22.16/3.83 | % 22.16/3.83 | GROUND_INST: instantiating (8) with all_183_0, all_291_3, all_49_0, all_49_3, % 22.16/3.83 | simplifying with (38), (75) gives: % 22.16/3.83 | (93) all_291_3 = all_183_0 % 22.16/3.83 | % 22.16/3.83 | GROUND_INST: instantiating (6) with all_49_2, all_280_0, all_49_3, simplifying % 22.16/3.83 | with (24), (60) gives: % 22.16/3.83 | (94) all_280_0 = all_49_2 % 22.16/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (6) with all_280_0, all_291_1, all_49_3, % 22.63/3.83 | simplifying with (60), (76) gives: % 22.63/3.83 | (95) all_291_1 = all_280_0 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (6) with all_291_1, all_297_1, all_49_3, % 22.63/3.83 | simplifying with (76), (83) gives: % 22.63/3.83 | (96) all_297_1 = all_291_1 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (6) with all_297_1, all_303_1, all_49_3, % 22.63/3.83 | simplifying with (83), (88) gives: % 22.63/3.83 | (97) all_303_1 = all_297_1 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (6) with all_271_0, all_303_1, all_49_3, % 22.63/3.83 | simplifying with (47), (88) gives: % 22.63/3.83 | (98) all_303_1 = all_271_0 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (6) with all_274_0, all_289_1, all_49_0, % 22.63/3.83 | simplifying with (51), (73) gives: % 22.63/3.83 | (99) all_289_1 = all_274_0 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (6) with all_289_1, all_295_1, all_49_0, % 22.63/3.83 | simplifying with (73), (81) gives: % 22.63/3.83 | (100) all_295_1 = all_289_1 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (6) with all_295_1, all_301_1, all_49_0, % 22.63/3.83 | simplifying with (81), (86) gives: % 22.63/3.83 | (101) all_301_1 = all_295_1 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (6) with all_268_0, all_301_1, all_49_0, % 22.63/3.83 | simplifying with (43), (86) gives: % 22.63/3.83 | (102) all_301_1 = all_268_0 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (7) with all_287_0, all_291_0, all_49_3, % 22.63/3.83 | simplifying with (71), (78) gives: % 22.63/3.83 | (103) all_291_0 = all_287_0 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (7) with all_285_0, all_291_0, all_49_3, % 22.63/3.83 | simplifying with (68), (78) gives: % 22.63/3.83 | (104) all_291_0 = all_285_0 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (7) with all_297_0, all_303_0, all_49_3, % 22.63/3.83 | simplifying with (84), (89) gives: % 22.63/3.83 | (105) all_303_0 = all_297_0 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (7) with all_287_0, all_303_0, all_49_3, % 22.63/3.83 | simplifying with (71), (89) gives: % 22.63/3.83 | (106) all_303_0 = all_287_0 % 22.63/3.83 | % 22.63/3.83 | GROUND_INST: instantiating (7) with all_283_0, all_303_0, all_49_3, % 22.63/3.83 | simplifying with (65), (89) gives: % 22.63/3.83 | (107) all_303_0 = all_283_0 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (105), (107) imply: % 22.63/3.83 | (108) all_297_0 = all_283_0 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (105), (106) imply: % 22.63/3.83 | (109) all_297_0 = all_287_0 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (97), (98) imply: % 22.63/3.83 | (110) all_297_1 = all_271_0 % 22.63/3.83 | % 22.63/3.83 | SIMP: (110) implies: % 22.63/3.83 | (111) all_297_1 = all_271_0 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (101), (102) imply: % 22.63/3.83 | (112) all_295_1 = all_268_0 % 22.63/3.83 | % 22.63/3.83 | SIMP: (112) implies: % 22.63/3.83 | (113) all_295_1 = all_268_0 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (108), (109) imply: % 22.63/3.83 | (114) all_287_0 = all_283_0 % 22.63/3.83 | % 22.63/3.83 | SIMP: (114) implies: % 22.63/3.83 | (115) all_287_0 = all_283_0 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (96), (111) imply: % 22.63/3.83 | (116) all_291_1 = all_271_0 % 22.63/3.83 | % 22.63/3.83 | SIMP: (116) implies: % 22.63/3.83 | (117) all_291_1 = all_271_0 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (100), (113) imply: % 22.63/3.83 | (118) all_289_1 = all_268_0 % 22.63/3.83 | % 22.63/3.83 | SIMP: (118) implies: % 22.63/3.83 | (119) all_289_1 = all_268_0 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (103), (104) imply: % 22.63/3.83 | (120) all_287_0 = all_285_0 % 22.63/3.83 | % 22.63/3.83 | SIMP: (120) implies: % 22.63/3.83 | (121) all_287_0 = all_285_0 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (95), (117) imply: % 22.63/3.83 | (122) all_280_0 = all_271_0 % 22.63/3.83 | % 22.63/3.83 | SIMP: (122) implies: % 22.63/3.83 | (123) all_280_0 = all_271_0 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (92), (93) imply: % 22.63/3.83 | (124) all_183_0 = all_49_1 % 22.63/3.83 | % 22.63/3.83 | SIMP: (124) implies: % 22.63/3.83 | (125) all_183_0 = all_49_1 % 22.63/3.83 | % 22.63/3.83 | COMBINE_EQS: (99), (119) imply: % 22.63/3.83 | (126) all_274_0 = all_268_0 % 22.63/3.84 | % 22.63/3.84 | SIMP: (126) implies: % 22.63/3.84 | (127) all_274_0 = all_268_0 % 22.63/3.84 | % 22.63/3.84 | COMBINE_EQS: (115), (121) imply: % 22.63/3.84 | (128) all_285_0 = all_283_0 % 22.63/3.84 | % 22.63/3.84 | SIMP: (128) implies: % 22.63/3.84 | (129) all_285_0 = all_283_0 % 22.63/3.84 | % 22.63/3.84 | COMBINE_EQS: (90), (91) imply: % 22.63/3.84 | (130) all_183_0 = all_63_0 % 22.63/3.84 | % 22.63/3.84 | SIMP: (130) implies: % 22.63/3.84 | (131) all_183_0 = all_63_0 % 22.63/3.84 | % 22.63/3.84 | COMBINE_EQS: (94), (123) imply: % 22.63/3.84 | (132) all_271_0 = all_49_2 % 22.63/3.84 | % 22.63/3.84 | COMBINE_EQS: (125), (131) imply: % 22.63/3.84 | (133) all_63_0 = all_49_1 % 22.63/3.84 | % 22.63/3.84 | COMBINE_EQS: (91), (133) imply: % 22.63/3.84 | (134) all_285_1 = all_49_1 % 22.63/3.84 | % 22.63/3.84 | COMBINE_EQS: (117), (132) imply: % 22.63/3.84 | (135) all_291_1 = all_49_2 % 22.63/3.84 | % 22.63/3.84 | COMBINE_EQS: (104), (129) imply: % 22.63/3.84 | (136) all_291_0 = all_283_0 % 22.63/3.84 | % 22.63/3.84 | REDUCE: (77), (92) imply: % 22.63/3.84 | (137) relation_dom(all_49_1) = all_291_2 % 22.63/3.84 | % 22.63/3.84 | BETA: splitting (69) gives: % 22.63/3.84 | % 22.63/3.84 | Case 1: % 22.63/3.84 | | % 22.63/3.84 | | (138) ~ one_to_one(all_285_1) % 22.63/3.84 | | % 22.63/3.84 | | REDUCE: (134), (138) imply: % 22.63/3.84 | | (139) ~ one_to_one(all_49_1) % 22.63/3.84 | | % 22.63/3.84 | | PRED_UNIFY: (34), (139) imply: % 22.63/3.84 | | (140) $false % 22.63/3.84 | | % 22.63/3.84 | | CLOSE: (140) is inconsistent. % 22.63/3.84 | | % 22.63/3.84 | Case 2: % 22.63/3.84 | | % 22.63/3.84 | | (141) ~ subset(all_285_0, all_268_0) % 22.63/3.84 | | % 22.63/3.84 | | REDUCE: (129), (141) imply: % 22.63/3.84 | | (142) ~ subset(all_283_0, all_268_0) % 22.63/3.84 | | % 22.63/3.84 | | BETA: splitting (79) gives: % 22.63/3.84 | | % 22.63/3.84 | | Case 1: % 22.63/3.84 | | | % 22.63/3.84 | | | (143) subset(all_291_0, all_274_0) % 22.63/3.84 | | | % 22.63/3.84 | | | REDUCE: (127), (136), (143) imply: % 22.63/3.84 | | | (144) subset(all_283_0, all_268_0) % 22.63/3.84 | | | % 22.63/3.84 | | | PRED_UNIFY: (142), (144) imply: % 22.63/3.84 | | | (145) $false % 22.63/3.84 | | | % 22.63/3.84 | | | CLOSE: (145) is inconsistent. % 22.63/3.84 | | | % 22.63/3.84 | | Case 2: % 22.63/3.84 | | | % 22.63/3.84 | | | (146) ~ (all_291_1 = all_291_2) % 22.63/3.84 | | | % 22.63/3.84 | | | REDUCE: (135), (146) imply: % 22.63/3.84 | | | (147) ~ (all_291_2 = all_49_2) % 22.63/3.84 | | | % 22.63/3.84 | | | SIMP: (147) implies: % 22.63/3.84 | | | (148) ~ (all_291_2 = all_49_2) % 22.63/3.84 | | | % 22.63/3.84 | | | GROUND_INST: instantiating (6) with all_49_2, all_291_2, all_49_1, % 22.63/3.84 | | | simplifying with (33), (137) gives: % 22.63/3.84 | | | (149) all_291_2 = all_49_2 % 22.63/3.84 | | | % 22.63/3.84 | | | REDUCE: (148), (149) imply: % 22.63/3.84 | | | (150) $false % 22.63/3.84 | | | % 22.63/3.84 | | | CLOSE: (150) is inconsistent. % 22.63/3.84 | | | % 22.63/3.84 | | End of split % 22.63/3.84 | | % 22.63/3.84 | End of split % 22.63/3.84 | % 22.63/3.84 End of proof % 22.63/3.84 % SZS output end Proof for theBenchmark % 22.63/3.84 % 22.63/3.84 3210ms %------------------------------------------------------------------------------