%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ALG210+2 : TPTP v8.1.2. Released v3.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n019.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 : Wed Aug 30 16:39:56 EDT 2023 % Result : Theorem 8.77s 1.96s % Output : Proof 18.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ALG210+2 : TPTP v8.1.2. Released v3.1.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n019.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Mon Aug 28 05:09:43 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.56 ________ _____ % 0.20/0.56 ___ __ \_________(_)________________________________ % 0.20/0.56 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.56 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.56 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.56 % 0.20/0.56 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.56 (2023-06-19) % 0.20/0.56 % 0.20/0.56 (c) Philipp Rümmer, 2009-2023 % 0.20/0.56 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.56 Amanda Stjerna. % 0.20/0.56 Free software under BSD-3-Clause. % 0.20/0.56 % 0.20/0.56 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.56 % 0.20/0.56 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.57 Running up to 7 provers in parallel. % 0.20/0.59 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.59 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.59 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.59 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.59 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.59 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.59 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 1.96/0.96 Prover 4: Preprocessing ... % 1.96/0.96 Prover 1: Preprocessing ... % 1.96/1.00 Prover 3: Preprocessing ... % 1.96/1.00 Prover 5: Preprocessing ... % 1.96/1.00 Prover 6: Preprocessing ... % 1.96/1.00 Prover 0: Preprocessing ... % 1.96/1.00 Prover 2: Preprocessing ... % 3.13/1.15 Prover 5: Proving ... % 3.13/1.16 Prover 1: Constructing countermodel ... % 3.13/1.16 Prover 3: Constructing countermodel ... % 3.13/1.16 Prover 6: Constructing countermodel ... % 3.13/1.17 Prover 4: Constructing countermodel ... % 3.13/1.17 Prover 0: Proving ... % 3.30/1.19 Prover 2: Proving ... % 8.77/1.95 Prover 3: proved (1370ms) % 8.77/1.96 % 8.77/1.96 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.77/1.96 % 8.77/1.96 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 8.77/1.96 Prover 6: stopped % 8.77/1.97 Prover 5: stopped % 8.77/1.97 Prover 0: stopped % 8.77/1.99 Prover 2: stopped % 8.77/2.00 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 8.77/2.00 Prover 7: Preprocessing ... % 8.77/2.00 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 8.77/2.00 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 8.77/2.00 Prover 8: Preprocessing ... % 8.77/2.00 Prover 10: Preprocessing ... % 8.77/2.00 Prover 11: Preprocessing ... % 8.77/2.01 Prover 7: Constructing countermodel ... % 8.77/2.01 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 8.77/2.01 Prover 10: Constructing countermodel ... % 8.77/2.01 Prover 8: Warning: ignoring some quantifiers % 8.77/2.02 Prover 8: Constructing countermodel ... % 8.77/2.02 Prover 13: Preprocessing ... % 8.77/2.02 Prover 10: gave up % 8.77/2.03 Prover 11: Constructing countermodel ... % 8.77/2.04 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 8.77/2.04 Prover 16: Preprocessing ... % 8.77/2.06 Prover 7: gave up % 8.77/2.07 Prover 13: Warning: ignoring some quantifiers % 8.77/2.07 Prover 13: Constructing countermodel ... % 8.77/2.07 Prover 16: Warning: ignoring some quantifiers % 8.77/2.07 Prover 16: Constructing countermodel ... % 8.77/2.08 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 8.77/2.09 Prover 13: gave up % 8.77/2.09 Prover 16: gave up % 8.77/2.10 Prover 19: Preprocessing ... % 8.77/2.15 Prover 19: Warning: ignoring some quantifiers % 8.77/2.15 Prover 19: Constructing countermodel ... % 17.27/3.15 Prover 1: Found proof (size 433) % 17.27/3.15 Prover 1: proved (2566ms) % 17.86/3.15 Prover 8: stopped % 17.86/3.15 Prover 19: stopped % 17.86/3.15 Prover 11: stopped % 17.86/3.15 Prover 4: stopped % 17.86/3.15 % 17.86/3.15 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.86/3.15 % 18.54/3.33 % SZS output start Proof for theBenchmark % 18.54/3.33 Assumptions after simplification: % 18.54/3.33 --------------------------------- % 18.54/3.33 % 18.54/3.33 (axiom_1) % 18.54/3.36 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 18.54/3.36 (times(v3, v2) = v4) | ~ (times(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 18.54/3.36 $i(v0) | ? [v5: $i] : (times(v2, v0) = v5 & times(v1, v5) = v4 & $i(v5) & % 18.54/3.36 $i(v4))) % 18.54/3.36 % 18.54/3.36 (axiom_2) % 18.54/3.36 ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (element(v0) = v1) | ~ $i(v0) | ? % 18.54/3.36 [v2: $i] : (times(v0, v0) = v2 & $i(v2) & ~ (times(v0, v2) = v0))) & ! % 18.54/3.36 [v0: $i] : ( ~ (element(v0) = 0) | ~ $i(v0) | ? [v1: $i] : (times(v0, v1) = % 18.54/3.36 v0 & times(v0, v0) = v1 & $i(v1))) % 18.54/3.36 % 18.54/3.36 (conjecture_1) % 18.54/3.36 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ( ~ (v3 = 0) & % 18.54/3.36 element(v2) = v3 & element(v1) = 0 & element(v0) = 0 & times(v0, v1) = v2 & % 18.54/3.36 $i(v2) & $i(v1) & $i(v0)) % 18.54/3.36 % 18.54/3.36 (function-axioms) % 18.54/3.36 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 18.54/3.36 (times(v3, v2) = v1) | ~ (times(v3, v2) = v0)) & ! [v0: MultipleValueBool] % 18.54/3.36 : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (element(v2) = v1) % 18.54/3.36 | ~ (element(v2) = v0)) % 18.54/3.36 % 18.54/3.36 Those formulas are unsatisfiable: % 18.54/3.36 --------------------------------- % 18.54/3.36 % 18.54/3.36 Begin of proof % 18.54/3.36 | % 18.54/3.36 | ALPHA: (axiom_2) implies: % 18.54/3.37 | (1) ! [v0: $i] : ( ~ (element(v0) = 0) | ~ $i(v0) | ? [v1: $i] : % 18.54/3.37 | (times(v0, v1) = v0 & times(v0, v0) = v1 & $i(v1))) % 18.54/3.37 | (2) ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (element(v0) = v1) | ~ % 18.54/3.37 | $i(v0) | ? [v2: $i] : (times(v0, v0) = v2 & $i(v2) & ~ (times(v0, % 18.54/3.37 | v2) = v0))) % 18.54/3.37 | % 18.54/3.37 | ALPHA: (function-axioms) implies: % 18.54/3.37 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 18.54/3.37 | (times(v3, v2) = v1) | ~ (times(v3, v2) = v0)) % 18.54/3.37 | % 18.54/3.37 | DELTA: instantiating (conjecture_1) with fresh symbols all_5_0, all_5_1, % 18.54/3.37 | all_5_2, all_5_3 gives: % 18.54/3.37 | (4) ~ (all_5_0 = 0) & element(all_5_1) = all_5_0 & element(all_5_2) = 0 & % 18.54/3.37 | element(all_5_3) = 0 & times(all_5_3, all_5_2) = all_5_1 & $i(all_5_1) % 18.75/3.37 | & $i(all_5_2) & $i(all_5_3) % 18.75/3.37 | % 18.75/3.37 | ALPHA: (4) implies: % 18.75/3.37 | (5) ~ (all_5_0 = 0) % 18.75/3.37 | (6) $i(all_5_3) % 18.75/3.37 | (7) $i(all_5_2) % 18.75/3.37 | (8) $i(all_5_1) % 18.75/3.37 | (9) times(all_5_3, all_5_2) = all_5_1 % 18.75/3.37 | (10) element(all_5_3) = 0 % 18.75/3.37 | (11) element(all_5_2) = 0 % 18.75/3.37 | (12) element(all_5_1) = all_5_0 % 18.75/3.37 | % 18.75/3.38 | GROUND_INST: instantiating (1) with all_5_3, simplifying with (6), (10) gives: % 18.75/3.38 | (13) ? [v0: $i] : (times(all_5_3, v0) = all_5_3 & times(all_5_3, all_5_3) % 18.75/3.38 | = v0 & $i(v0)) % 18.75/3.38 | % 18.75/3.38 | GROUND_INST: instantiating (1) with all_5_2, simplifying with (7), (11) gives: % 18.75/3.38 | (14) ? [v0: $i] : (times(all_5_2, v0) = all_5_2 & times(all_5_2, all_5_2) % 18.75/3.38 | = v0 & $i(v0)) % 18.75/3.38 | % 18.75/3.38 | GROUND_INST: instantiating (2) with all_5_1, all_5_0, simplifying with (8), % 18.75/3.38 | (12) gives: % 18.75/3.38 | (15) all_5_0 = 0 | ? [v0: $i] : (times(all_5_1, all_5_1) = v0 & $i(v0) & % 18.75/3.38 | ~ (times(all_5_1, v0) = all_5_1)) % 18.75/3.38 | % 18.75/3.38 | DELTA: instantiating (14) with fresh symbol all_12_0 gives: % 18.75/3.38 | (16) times(all_5_2, all_12_0) = all_5_2 & times(all_5_2, all_5_2) = % 18.75/3.38 | all_12_0 & $i(all_12_0) % 18.75/3.38 | % 18.75/3.38 | ALPHA: (16) implies: % 18.75/3.38 | (17) $i(all_12_0) % 18.75/3.38 | (18) times(all_5_2, all_5_2) = all_12_0 % 18.75/3.38 | (19) times(all_5_2, all_12_0) = all_5_2 % 18.75/3.38 | % 18.75/3.38 | DELTA: instantiating (13) with fresh symbol all_14_0 gives: % 18.75/3.38 | (20) times(all_5_3, all_14_0) = all_5_3 & times(all_5_3, all_5_3) = % 18.75/3.38 | all_14_0 & $i(all_14_0) % 18.75/3.38 | % 18.75/3.38 | ALPHA: (20) implies: % 18.75/3.38 | (21) $i(all_14_0) % 18.75/3.38 | (22) times(all_5_3, all_5_3) = all_14_0 % 18.75/3.38 | (23) times(all_5_3, all_14_0) = all_5_3 % 18.75/3.38 | % 18.75/3.38 | BETA: splitting (15) gives: % 18.75/3.38 | % 18.75/3.38 | Case 1: % 18.75/3.38 | | % 18.75/3.38 | | (24) all_5_0 = 0 % 18.75/3.38 | | % 18.75/3.38 | | REDUCE: (5), (24) imply: % 18.75/3.38 | | (25) $false % 18.75/3.38 | | % 18.75/3.38 | | CLOSE: (25) is inconsistent. % 18.75/3.38 | | % 18.75/3.38 | Case 2: % 18.75/3.38 | | % 18.75/3.38 | | (26) ? [v0: $i] : (times(all_5_1, all_5_1) = v0 & $i(v0) & ~ % 18.75/3.38 | | (times(all_5_1, v0) = all_5_1)) % 18.75/3.39 | | % 18.75/3.39 | | DELTA: instantiating (26) with fresh symbol all_20_0 gives: % 18.75/3.39 | | (27) times(all_5_1, all_5_1) = all_20_0 & $i(all_20_0) & ~ % 18.75/3.39 | | (times(all_5_1, all_20_0) = all_5_1) % 18.75/3.39 | | % 18.75/3.39 | | ALPHA: (27) implies: % 18.75/3.39 | | (28) ~ (times(all_5_1, all_20_0) = all_5_1) % 18.75/3.39 | | (29) times(all_5_1, all_5_1) = all_20_0 % 18.75/3.39 | | % 18.75/3.39 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_14_0, all_5_2, % 18.75/3.39 | | all_5_3, all_5_1, simplifying with (6), (7), (9), (21), (23) % 18.75/3.39 | | gives: % 18.75/3.39 | | (30) ? [v0: $i] : (times(all_14_0, v0) = all_5_1 & times(all_5_2, % 18.75/3.39 | | all_5_3) = v0 & $i(v0) & $i(all_5_1)) % 18.75/3.39 | | % 18.75/3.39 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_14_0, all_14_0, % 18.75/3.39 | | all_5_3, all_5_3, simplifying with (6), (21), (23) gives: % 18.75/3.39 | | (31) ? [v0: $i] : (times(all_14_0, v0) = all_5_3 & times(all_14_0, % 18.75/3.39 | | all_5_3) = v0 & $i(v0)) % 18.75/3.39 | | % 18.75/3.39 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_14_0, all_5_3, % 18.75/3.39 | | all_5_3, all_14_0, simplifying with (6), (21), (22), (23) % 18.75/3.39 | | gives: % 18.75/3.39 | | (32) ? [v0: $i] : (times(all_14_0, v0) = all_14_0 & times(all_5_3, % 18.75/3.39 | | all_5_3) = v0 & $i(v0)) % 18.75/3.39 | | % 18.75/3.39 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_12_0, all_12_0, % 18.75/3.39 | | all_5_2, all_5_2, simplifying with (7), (17), (19) gives: % 18.75/3.39 | | (33) ? [v0: $i] : (times(all_12_0, v0) = all_5_2 & times(all_12_0, % 18.75/3.39 | | all_5_2) = v0 & $i(v0)) % 18.75/3.39 | | % 18.75/3.39 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_12_0, all_5_2, % 18.75/3.39 | | all_5_2, all_12_0, simplifying with (7), (17), (18), (19) % 18.75/3.39 | | gives: % 18.75/3.39 | | (34) ? [v0: $i] : (times(all_12_0, v0) = all_12_0 & times(all_5_2, % 18.75/3.39 | | all_5_2) = v0 & $i(v0)) % 18.75/3.39 | | % 18.75/3.40 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_5_2, all_5_1, % 18.75/3.40 | | all_5_1, all_20_0, simplifying with (6), (7), (8), (9), (29) % 18.75/3.40 | | gives: % 18.75/3.40 | | (35) ? [v0: $i] : (times(all_5_1, all_5_3) = v0 & times(all_5_2, v0) = % 18.75/3.40 | | all_20_0 & $i(v0) & $i(all_20_0)) % 18.75/3.40 | | % 18.75/3.40 | | DELTA: instantiating (34) with fresh symbol all_27_0 gives: % 18.75/3.40 | | (36) times(all_12_0, all_27_0) = all_12_0 & times(all_5_2, all_5_2) = % 18.75/3.40 | | all_27_0 & $i(all_27_0) % 18.75/3.40 | | % 18.75/3.40 | | ALPHA: (36) implies: % 18.75/3.40 | | (37) $i(all_27_0) % 18.75/3.40 | | (38) times(all_5_2, all_5_2) = all_27_0 % 18.75/3.40 | | (39) times(all_12_0, all_27_0) = all_12_0 % 18.75/3.40 | | % 18.75/3.40 | | DELTA: instantiating (33) with fresh symbol all_29_0 gives: % 18.75/3.40 | | (40) times(all_12_0, all_29_0) = all_5_2 & times(all_12_0, all_5_2) = % 18.75/3.40 | | all_29_0 & $i(all_29_0) % 18.75/3.40 | | % 18.75/3.40 | | ALPHA: (40) implies: % 18.75/3.40 | | (41) $i(all_29_0) % 18.75/3.40 | | (42) times(all_12_0, all_5_2) = all_29_0 % 18.75/3.40 | | (43) times(all_12_0, all_29_0) = all_5_2 % 18.75/3.40 | | % 18.75/3.40 | | DELTA: instantiating (31) with fresh symbol all_31_0 gives: % 18.75/3.40 | | (44) times(all_14_0, all_31_0) = all_5_3 & times(all_14_0, all_5_3) = % 18.75/3.40 | | all_31_0 & $i(all_31_0) % 18.75/3.40 | | % 18.75/3.40 | | ALPHA: (44) implies: % 18.75/3.40 | | (45) $i(all_31_0) % 18.75/3.40 | | (46) times(all_14_0, all_5_3) = all_31_0 % 18.75/3.40 | | (47) times(all_14_0, all_31_0) = all_5_3 % 18.75/3.40 | | % 18.75/3.40 | | DELTA: instantiating (32) with fresh symbol all_33_0 gives: % 18.75/3.40 | | (48) times(all_14_0, all_33_0) = all_14_0 & times(all_5_3, all_5_3) = % 18.75/3.40 | | all_33_0 & $i(all_33_0) % 18.75/3.40 | | % 18.75/3.40 | | ALPHA: (48) implies: % 18.75/3.40 | | (49) $i(all_33_0) % 18.75/3.40 | | (50) times(all_5_3, all_5_3) = all_33_0 % 18.75/3.40 | | (51) times(all_14_0, all_33_0) = all_14_0 % 18.75/3.40 | | % 18.75/3.40 | | DELTA: instantiating (35) with fresh symbol all_35_0 gives: % 18.75/3.40 | | (52) times(all_5_1, all_5_3) = all_35_0 & times(all_5_2, all_35_0) = % 18.75/3.40 | | all_20_0 & $i(all_35_0) & $i(all_20_0) % 18.75/3.40 | | % 18.75/3.40 | | ALPHA: (52) implies: % 18.75/3.40 | | (53) $i(all_35_0) % 18.75/3.40 | | (54) times(all_5_2, all_35_0) = all_20_0 % 18.75/3.40 | | (55) times(all_5_1, all_5_3) = all_35_0 % 18.75/3.40 | | % 18.75/3.40 | | DELTA: instantiating (30) with fresh symbol all_37_0 gives: % 18.75/3.40 | | (56) times(all_14_0, all_37_0) = all_5_1 & times(all_5_2, all_5_3) = % 18.75/3.40 | | all_37_0 & $i(all_37_0) & $i(all_5_1) % 18.75/3.40 | | % 18.75/3.40 | | ALPHA: (56) implies: % 18.75/3.40 | | (57) $i(all_37_0) % 18.75/3.40 | | (58) times(all_5_2, all_5_3) = all_37_0 % 18.75/3.40 | | (59) times(all_14_0, all_37_0) = all_5_1 % 18.75/3.40 | | % 18.75/3.40 | | GROUND_INST: instantiating (3) with all_14_0, all_33_0, all_5_3, all_5_3, % 18.75/3.40 | | simplifying with (22), (50) gives: % 18.75/3.40 | | (60) all_33_0 = all_14_0 % 18.75/3.40 | | % 18.75/3.40 | | GROUND_INST: instantiating (3) with all_12_0, all_27_0, all_5_2, all_5_2, % 18.75/3.40 | | simplifying with (18), (38) gives: % 18.75/3.40 | | (61) all_27_0 = all_12_0 % 18.75/3.40 | | % 18.75/3.40 | | REDUCE: (51), (60) imply: % 18.75/3.40 | | (62) times(all_14_0, all_14_0) = all_14_0 % 18.75/3.40 | | % 18.75/3.41 | | REDUCE: (39), (61) imply: % 18.75/3.41 | | (63) times(all_12_0, all_12_0) = all_12_0 % 18.75/3.41 | | % 18.75/3.41 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_12_0, all_5_3, % 18.75/3.41 | | all_5_2, all_37_0, simplifying with (6), (7), (17), (19), (58) % 18.75/3.41 | | gives: % 18.75/3.41 | | (64) ? [v0: $i] : (times(all_12_0, v0) = all_37_0 & times(all_5_3, % 18.75/3.41 | | all_5_2) = v0 & $i(v0) & $i(all_37_0)) % 18.75/3.41 | | % 18.75/3.41 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_12_0, all_35_0, % 18.75/3.41 | | all_5_2, all_20_0, simplifying with (7), (17), (19), (53), (54) % 18.75/3.41 | | gives: % 18.75/3.41 | | (65) ? [v0: $i] : (times(all_35_0, all_5_2) = v0 & times(all_12_0, v0) = % 18.75/3.41 | | all_20_0 & $i(v0) & $i(all_20_0)) % 18.75/3.41 | | % 18.75/3.41 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_5_2, all_5_3, % 18.75/3.41 | | all_5_1, all_35_0, simplifying with (6), (7), (9), (55) gives: % 18.75/3.41 | | (66) ? [v0: $i] : (times(all_5_2, v0) = all_35_0 & times(all_5_3, % 18.75/3.41 | | all_5_3) = v0 & $i(v0) & $i(all_35_0)) % 18.75/3.41 | | % 18.75/3.41 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_5_2, all_5_2, % 18.75/3.41 | | all_12_0, all_29_0, simplifying with (7), (18), (42) gives: % 18.75/3.41 | | (67) ? [v0: $i] : (times(all_5_2, v0) = all_29_0 & times(all_5_2, % 18.75/3.41 | | all_5_2) = v0 & $i(v0) & $i(all_29_0)) % 18.75/3.41 | | % 18.75/3.41 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_5_2, all_12_0, % 18.75/3.41 | | all_12_0, all_12_0, simplifying with (7), (17), (18), (63) % 18.75/3.41 | | gives: % 18.75/3.41 | | (68) ? [v0: $i] : (times(all_12_0, all_5_2) = v0 & times(all_5_2, v0) = % 18.75/3.41 | | all_12_0 & $i(v0)) % 18.75/3.41 | | % 18.75/3.41 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_5_2, all_29_0, % 18.75/3.41 | | all_12_0, all_5_2, simplifying with (7), (18), (41), (43) % 18.75/3.41 | | gives: % 18.75/3.41 | | (69) ? [v0: $i] : (times(all_29_0, all_5_2) = v0 & times(all_5_2, v0) = % 18.75/3.41 | | all_5_2 & $i(v0)) % 18.75/3.41 | | % 18.75/3.41 | | GROUND_INST: instantiating (axiom_1) with all_12_0, all_29_0, all_5_2, % 18.75/3.41 | | all_5_2, all_12_0, simplifying with (7), (17), (18), (41), (43) % 18.75/3.41 | | gives: % 18.75/3.41 | | (70) ? [v0: $i] : (times(all_29_0, v0) = all_12_0 & times(all_5_2, % 18.75/3.41 | | all_12_0) = v0 & $i(v0)) % 18.75/3.41 | | % 18.75/3.41 | | GROUND_INST: instantiating (axiom_1) with all_12_0, all_29_0, all_35_0, % 18.75/3.41 | | all_5_2, all_20_0, simplifying with (17), (41), (43), (53), % 18.75/3.41 | | (54) gives: % 18.75/3.41 | | (71) ? [v0: $i] : (times(all_35_0, all_12_0) = v0 & times(all_29_0, v0) % 18.75/3.41 | | = all_20_0 & $i(v0) & $i(all_20_0)) % 18.75/3.41 | | % 18.75/3.42 | | GROUND_INST: instantiating (axiom_1) with all_12_0, all_29_0, all_5_3, % 18.75/3.42 | | all_5_2, all_37_0, simplifying with (6), (17), (41), (43), (58) % 18.75/3.42 | | gives: % 18.75/3.42 | | (72) ? [v0: $i] : (times(all_29_0, v0) = all_37_0 & times(all_5_3, % 18.75/3.42 | | all_12_0) = v0 & $i(v0) & $i(all_37_0)) % 18.75/3.42 | | % 18.75/3.42 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_5_3, all_5_3, % 18.75/3.42 | | all_14_0, all_31_0, simplifying with (6), (22), (46) gives: % 18.75/3.42 | | (73) ? [v0: $i] : (times(all_5_3, v0) = all_31_0 & times(all_5_3, % 18.75/3.42 | | all_5_3) = v0 & $i(v0) & $i(all_31_0)) % 18.75/3.42 | | % 18.75/3.42 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_5_3, all_14_0, % 18.75/3.42 | | all_14_0, all_14_0, simplifying with (6), (21), (22), (62) % 18.75/3.42 | | gives: % 18.75/3.42 | | (74) ? [v0: $i] : (times(all_14_0, all_5_3) = v0 & times(all_5_3, v0) = % 18.75/3.42 | | all_14_0 & $i(v0)) % 18.75/3.42 | | % 18.75/3.42 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_31_0, all_14_0, % 18.75/3.42 | | all_5_3, all_5_3, simplifying with (21), (23), (45), (47) % 18.75/3.42 | | gives: % 18.75/3.42 | | (75) ? [v0: $i] : (times(all_31_0, v0) = all_5_3 & times(all_14_0, % 18.75/3.42 | | all_14_0) = v0 & $i(v0) & $i(all_5_3)) % 18.75/3.42 | | % 18.75/3.42 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_31_0, all_5_2, % 18.75/3.42 | | all_5_3, all_5_1, simplifying with (7), (9), (21), (45), (47) % 18.75/3.42 | | gives: % 18.75/3.42 | | (76) ? [v0: $i] : (times(all_31_0, v0) = all_5_1 & times(all_5_2, % 18.75/3.42 | | all_14_0) = v0 & $i(v0) & $i(all_5_1)) % 18.75/3.42 | | % 18.75/3.42 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_5_3, all_31_0, % 18.75/3.42 | | all_14_0, all_5_3, simplifying with (6), (22), (45), (47) % 18.75/3.42 | | gives: % 18.75/3.42 | | (77) ? [v0: $i] : (times(all_31_0, all_5_3) = v0 & times(all_5_3, v0) = % 18.75/3.42 | | all_5_3 & $i(v0)) % 18.75/3.42 | | % 18.75/3.42 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_31_0, all_5_3, % 18.75/3.42 | | all_5_3, all_14_0, simplifying with (6), (21), (22), (45), (47) % 18.75/3.42 | | gives: % 18.75/3.42 | | (78) ? [v0: $i] : (times(all_31_0, v0) = all_14_0 & times(all_5_3, % 18.75/3.42 | | all_14_0) = v0 & $i(v0)) % 18.75/3.42 | | % 18.75/3.42 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_37_0, all_5_1, % 18.75/3.42 | | all_5_1, all_20_0, simplifying with (8), (21), (29), (57), (59) % 18.75/3.42 | | gives: % 18.75/3.42 | | (79) ? [v0: $i] : (times(all_37_0, v0) = all_20_0 & times(all_5_1, % 18.75/3.42 | | all_14_0) = v0 & $i(v0) & $i(all_20_0)) % 18.75/3.42 | | % 18.75/3.43 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_5_3, all_37_0, % 18.75/3.43 | | all_14_0, all_5_1, simplifying with (6), (22), (57), (59) % 18.75/3.43 | | gives: % 18.75/3.43 | | (80) ? [v0: $i] : (times(all_37_0, all_5_3) = v0 & times(all_5_3, v0) = % 18.75/3.43 | | all_5_1 & $i(v0) & $i(all_5_1)) % 18.75/3.43 | | % 18.75/3.43 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_14_0, all_37_0, % 18.75/3.43 | | all_14_0, all_5_1, simplifying with (21), (57), (59), (62) % 18.75/3.43 | | gives: % 18.75/3.43 | | (81) ? [v0: $i] : (times(all_37_0, all_14_0) = v0 & times(all_14_0, v0) % 18.75/3.43 | | = all_5_1 & $i(v0) & $i(all_5_1)) % 18.75/3.43 | | % 18.75/3.43 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_37_0, all_5_3, % 18.75/3.43 | | all_5_1, all_35_0, simplifying with (6), (21), (55), (57), (59) % 18.75/3.43 | | gives: % 18.75/3.43 | | (82) ? [v0: $i] : (times(all_37_0, v0) = all_35_0 & times(all_5_3, % 18.75/3.43 | | all_14_0) = v0 & $i(v0) & $i(all_35_0)) % 18.75/3.43 | | % 18.75/3.43 | | DELTA: instantiating (78) with fresh symbol all_48_0 gives: % 18.75/3.43 | | (83) times(all_31_0, all_48_0) = all_14_0 & times(all_5_3, all_14_0) = % 18.75/3.43 | | all_48_0 & $i(all_48_0) % 18.75/3.43 | | % 18.75/3.43 | | ALPHA: (83) implies: % 18.75/3.43 | | (84) times(all_5_3, all_14_0) = all_48_0 % 18.75/3.43 | | (85) times(all_31_0, all_48_0) = all_14_0 % 18.75/3.43 | | % 18.75/3.43 | | DELTA: instantiating (77) with fresh symbol all_50_0 gives: % 18.75/3.43 | | (86) times(all_31_0, all_5_3) = all_50_0 & times(all_5_3, all_50_0) = % 18.75/3.43 | | all_5_3 & $i(all_50_0) % 18.75/3.43 | | % 18.75/3.43 | | ALPHA: (86) implies: % 18.75/3.43 | | (87) $i(all_50_0) % 18.75/3.43 | | (88) times(all_31_0, all_5_3) = all_50_0 % 18.75/3.43 | | % 18.75/3.43 | | DELTA: instantiating (74) with fresh symbol all_52_0 gives: % 18.75/3.43 | | (89) times(all_14_0, all_5_3) = all_52_0 & times(all_5_3, all_52_0) = % 18.75/3.43 | | all_14_0 & $i(all_52_0) % 18.75/3.43 | | % 18.75/3.43 | | ALPHA: (89) implies: % 18.75/3.43 | | (90) $i(all_52_0) % 18.75/3.43 | | (91) times(all_5_3, all_52_0) = all_14_0 % 18.75/3.43 | | (92) times(all_14_0, all_5_3) = all_52_0 % 18.75/3.43 | | % 18.75/3.43 | | DELTA: instantiating (70) with fresh symbol all_54_0 gives: % 18.75/3.43 | | (93) times(all_29_0, all_54_0) = all_12_0 & times(all_5_2, all_12_0) = % 18.75/3.43 | | all_54_0 & $i(all_54_0) % 18.75/3.43 | | % 18.75/3.43 | | ALPHA: (93) implies: % 18.75/3.43 | | (94) times(all_5_2, all_12_0) = all_54_0 % 18.75/3.43 | | (95) times(all_29_0, all_54_0) = all_12_0 % 18.75/3.43 | | % 18.75/3.43 | | DELTA: instantiating (68) with fresh symbol all_56_0 gives: % 18.75/3.43 | | (96) times(all_12_0, all_5_2) = all_56_0 & times(all_5_2, all_56_0) = % 18.75/3.43 | | all_12_0 & $i(all_56_0) % 18.75/3.43 | | % 18.75/3.43 | | ALPHA: (96) implies: % 18.75/3.43 | | (97) $i(all_56_0) % 18.75/3.43 | | (98) times(all_5_2, all_56_0) = all_12_0 % 18.75/3.43 | | (99) times(all_12_0, all_5_2) = all_56_0 % 18.75/3.43 | | % 18.75/3.43 | | DELTA: instantiating (69) with fresh symbol all_58_0 gives: % 18.75/3.43 | | (100) times(all_29_0, all_5_2) = all_58_0 & times(all_5_2, all_58_0) = % 18.75/3.43 | | all_5_2 & $i(all_58_0) % 18.75/3.43 | | % 18.75/3.43 | | ALPHA: (100) implies: % 18.75/3.43 | | (101) $i(all_58_0) % 18.75/3.43 | | (102) times(all_29_0, all_5_2) = all_58_0 % 18.75/3.43 | | % 18.75/3.43 | | DELTA: instantiating (67) with fresh symbol all_60_0 gives: % 18.75/3.43 | | (103) times(all_5_2, all_60_0) = all_29_0 & times(all_5_2, all_5_2) = % 18.75/3.43 | | all_60_0 & $i(all_60_0) & $i(all_29_0) % 18.75/3.43 | | % 18.75/3.43 | | ALPHA: (103) implies: % 18.75/3.43 | | (104) times(all_5_2, all_5_2) = all_60_0 % 18.75/3.44 | | (105) times(all_5_2, all_60_0) = all_29_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (66) with fresh symbol all_62_0 gives: % 18.75/3.44 | | (106) times(all_5_2, all_62_0) = all_35_0 & times(all_5_3, all_5_3) = % 18.75/3.44 | | all_62_0 & $i(all_62_0) & $i(all_35_0) % 18.75/3.44 | | % 18.75/3.44 | | ALPHA: (106) implies: % 18.75/3.44 | | (107) times(all_5_3, all_5_3) = all_62_0 % 18.75/3.44 | | (108) times(all_5_2, all_62_0) = all_35_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (65) with fresh symbol all_64_0 gives: % 18.75/3.44 | | (109) times(all_35_0, all_5_2) = all_64_0 & times(all_12_0, all_64_0) = % 18.75/3.44 | | all_20_0 & $i(all_64_0) & $i(all_20_0) % 18.75/3.44 | | % 18.75/3.44 | | ALPHA: (109) implies: % 18.75/3.44 | | (110) $i(all_64_0) % 18.75/3.44 | | (111) times(all_12_0, all_64_0) = all_20_0 % 18.75/3.44 | | (112) times(all_35_0, all_5_2) = all_64_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (80) with fresh symbol all_68_0 gives: % 18.75/3.44 | | (113) times(all_37_0, all_5_3) = all_68_0 & times(all_5_3, all_68_0) = % 18.75/3.44 | | all_5_1 & $i(all_68_0) & $i(all_5_1) % 18.75/3.44 | | % 18.75/3.44 | | ALPHA: (113) implies: % 18.75/3.44 | | (114) $i(all_68_0) % 18.75/3.44 | | (115) times(all_5_3, all_68_0) = all_5_1 % 18.75/3.44 | | (116) times(all_37_0, all_5_3) = all_68_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (79) with fresh symbol all_70_0 gives: % 18.75/3.44 | | (117) times(all_37_0, all_70_0) = all_20_0 & times(all_5_1, all_14_0) = % 18.75/3.44 | | all_70_0 & $i(all_70_0) & $i(all_20_0) % 18.75/3.44 | | % 18.75/3.44 | | ALPHA: (117) implies: % 18.75/3.44 | | (118) $i(all_70_0) % 18.75/3.44 | | (119) times(all_5_1, all_14_0) = all_70_0 % 18.75/3.44 | | (120) times(all_37_0, all_70_0) = all_20_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (76) with fresh symbol all_72_0 gives: % 18.75/3.44 | | (121) times(all_31_0, all_72_0) = all_5_1 & times(all_5_2, all_14_0) = % 18.75/3.44 | | all_72_0 & $i(all_72_0) & $i(all_5_1) % 18.75/3.44 | | % 18.75/3.44 | | ALPHA: (121) implies: % 18.75/3.44 | | (122) times(all_5_2, all_14_0) = all_72_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (73) with fresh symbol all_74_0 gives: % 18.75/3.44 | | (123) times(all_5_3, all_74_0) = all_31_0 & times(all_5_3, all_5_3) = % 18.75/3.44 | | all_74_0 & $i(all_74_0) & $i(all_31_0) % 18.75/3.44 | | % 18.75/3.44 | | ALPHA: (123) implies: % 18.75/3.44 | | (124) times(all_5_3, all_5_3) = all_74_0 % 18.75/3.44 | | (125) times(all_5_3, all_74_0) = all_31_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (71) with fresh symbol all_76_0 gives: % 18.75/3.44 | | (126) times(all_35_0, all_12_0) = all_76_0 & times(all_29_0, all_76_0) = % 18.75/3.44 | | all_20_0 & $i(all_76_0) & $i(all_20_0) % 18.75/3.44 | | % 18.75/3.44 | | ALPHA: (126) implies: % 18.75/3.44 | | (127) $i(all_76_0) % 18.75/3.44 | | (128) times(all_29_0, all_76_0) = all_20_0 % 18.75/3.44 | | (129) times(all_35_0, all_12_0) = all_76_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (75) with fresh symbol all_78_0 gives: % 18.75/3.44 | | (130) times(all_31_0, all_78_0) = all_5_3 & times(all_14_0, all_14_0) = % 18.75/3.44 | | all_78_0 & $i(all_78_0) & $i(all_5_3) % 18.75/3.44 | | % 18.75/3.44 | | ALPHA: (130) implies: % 18.75/3.44 | | (131) times(all_14_0, all_14_0) = all_78_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (72) with fresh symbol all_82_0 gives: % 18.75/3.44 | | (132) times(all_29_0, all_82_0) = all_37_0 & times(all_5_3, all_12_0) = % 18.75/3.44 | | all_82_0 & $i(all_82_0) & $i(all_37_0) % 18.75/3.44 | | % 18.75/3.44 | | ALPHA: (132) implies: % 18.75/3.44 | | (133) $i(all_82_0) % 18.75/3.44 | | (134) times(all_5_3, all_12_0) = all_82_0 % 18.75/3.44 | | (135) times(all_29_0, all_82_0) = all_37_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (82) with fresh symbol all_84_0 gives: % 18.75/3.44 | | (136) times(all_37_0, all_84_0) = all_35_0 & times(all_5_3, all_14_0) = % 18.75/3.44 | | all_84_0 & $i(all_84_0) & $i(all_35_0) % 18.75/3.44 | | % 18.75/3.44 | | ALPHA: (136) implies: % 18.75/3.44 | | (137) times(all_5_3, all_14_0) = all_84_0 % 18.75/3.44 | | (138) times(all_37_0, all_84_0) = all_35_0 % 18.75/3.44 | | % 18.75/3.44 | | DELTA: instantiating (81) with fresh symbol all_86_0 gives: % 18.75/3.45 | | (139) times(all_37_0, all_14_0) = all_86_0 & times(all_14_0, all_86_0) = % 18.75/3.45 | | all_5_1 & $i(all_86_0) & $i(all_5_1) % 18.75/3.45 | | % 18.75/3.45 | | ALPHA: (139) implies: % 18.75/3.45 | | (140) $i(all_86_0) % 18.75/3.45 | | (141) times(all_14_0, all_86_0) = all_5_1 % 18.75/3.45 | | (142) times(all_37_0, all_14_0) = all_86_0 % 18.75/3.45 | | % 18.75/3.45 | | DELTA: instantiating (64) with fresh symbol all_90_0 gives: % 18.75/3.45 | | (143) times(all_12_0, all_90_0) = all_37_0 & times(all_5_3, all_5_2) = % 18.75/3.45 | | all_90_0 & $i(all_90_0) & $i(all_37_0) % 18.75/3.45 | | % 18.75/3.45 | | ALPHA: (143) implies: % 18.75/3.45 | | (144) $i(all_90_0) % 18.75/3.45 | | (145) times(all_5_3, all_5_2) = all_90_0 % 18.75/3.45 | | (146) times(all_12_0, all_90_0) = all_37_0 % 18.75/3.45 | | % 18.75/3.45 | | GROUND_INST: instantiating (3) with all_14_0, all_74_0, all_5_3, all_5_3, % 18.75/3.45 | | simplifying with (22), (124) gives: % 18.75/3.45 | | (147) all_74_0 = all_14_0 % 18.75/3.45 | | % 18.75/3.45 | | GROUND_INST: instantiating (3) with all_62_0, all_74_0, all_5_3, all_5_3, % 18.75/3.45 | | simplifying with (107), (124) gives: % 18.75/3.45 | | (148) all_74_0 = all_62_0 % 18.75/3.45 | | % 18.75/3.45 | | GROUND_INST: instantiating (3) with all_5_1, all_90_0, all_5_2, all_5_3, % 18.75/3.45 | | simplifying with (9), (145) gives: % 18.75/3.45 | | (149) all_90_0 = all_5_1 % 18.75/3.45 | | % 18.75/3.45 | | GROUND_INST: instantiating (3) with all_5_3, all_84_0, all_14_0, all_5_3, % 18.75/3.45 | | simplifying with (23), (137) gives: % 18.75/3.45 | | (150) all_84_0 = all_5_3 % 18.75/3.45 | | % 18.75/3.45 | | GROUND_INST: instantiating (3) with all_48_0, all_84_0, all_14_0, all_5_3, % 18.75/3.45 | | simplifying with (84), (137) gives: % 18.75/3.45 | | (151) all_84_0 = all_48_0 % 18.75/3.45 | | % 18.75/3.45 | | GROUND_INST: instantiating (3) with all_12_0, all_60_0, all_5_2, all_5_2, % 18.75/3.45 | | simplifying with (18), (104) gives: % 18.75/3.45 | | (152) all_60_0 = all_12_0 % 18.75/3.45 | | % 18.75/3.45 | | GROUND_INST: instantiating (3) with all_5_2, all_54_0, all_12_0, all_5_2, % 18.75/3.45 | | simplifying with (19), (94) gives: % 18.75/3.45 | | (153) all_54_0 = all_5_2 % 18.75/3.45 | | % 18.75/3.45 | | GROUND_INST: instantiating (3) with all_29_0, all_56_0, all_5_2, all_12_0, % 18.75/3.45 | | simplifying with (42), (99) gives: % 18.75/3.45 | | (154) all_56_0 = all_29_0 % 18.75/3.45 | | % 18.75/3.45 | | GROUND_INST: instantiating (3) with all_31_0, all_52_0, all_5_3, all_14_0, % 18.75/3.45 | | simplifying with (46), (92) gives: % 18.75/3.45 | | (155) all_52_0 = all_31_0 % 18.75/3.45 | | % 18.75/3.45 | | GROUND_INST: instantiating (3) with all_14_0, all_78_0, all_14_0, all_14_0, % 18.75/3.45 | | simplifying with (62), (131) gives: % 18.75/3.45 | | (156) all_78_0 = all_14_0 % 18.75/3.45 | | % 18.75/3.45 | | COMBINE_EQS: (150), (151) imply: % 18.75/3.45 | | (157) all_48_0 = all_5_3 % 18.75/3.45 | | % 18.75/3.45 | | COMBINE_EQS: (147), (148) imply: % 18.75/3.45 | | (158) all_62_0 = all_14_0 % 18.75/3.45 | | % 18.75/3.45 | | REDUCE: (138), (150) imply: % 18.75/3.45 | | (159) times(all_37_0, all_5_3) = all_35_0 % 18.75/3.45 | | % 18.75/3.45 | | REDUCE: (85), (157) imply: % 18.75/3.45 | | (160) times(all_31_0, all_5_3) = all_14_0 % 18.75/3.45 | | % 18.75/3.45 | | REDUCE: (95), (153) imply: % 18.75/3.45 | | (161) times(all_29_0, all_5_2) = all_12_0 % 18.75/3.45 | | % 18.75/3.45 | | REDUCE: (146), (149) imply: % 18.75/3.45 | | (162) times(all_12_0, all_5_1) = all_37_0 % 18.75/3.45 | | % 18.75/3.45 | | REDUCE: (108), (158) imply: % 18.75/3.45 | | (163) times(all_5_2, all_14_0) = all_35_0 % 18.75/3.45 | | % 18.75/3.45 | | REDUCE: (105), (152) imply: % 18.75/3.45 | | (164) times(all_5_2, all_12_0) = all_29_0 % 18.75/3.45 | | % 18.75/3.45 | | REDUCE: (98), (154) imply: % 18.75/3.45 | | (165) times(all_5_2, all_29_0) = all_12_0 % 18.75/3.45 | | % 18.75/3.46 | | REDUCE: (125), (147) imply: % 18.75/3.46 | | (166) times(all_5_3, all_14_0) = all_31_0 % 18.75/3.46 | | % 18.75/3.46 | | REDUCE: (91), (155) imply: % 18.75/3.46 | | (167) times(all_5_3, all_31_0) = all_14_0 % 18.75/3.46 | | % 18.75/3.46 | | GROUND_INST: instantiating (3) with all_5_3, all_31_0, all_14_0, all_5_3, % 18.75/3.46 | | simplifying with (23), (166) gives: % 18.75/3.46 | | (168) all_31_0 = all_5_3 % 18.75/3.46 | | % 18.75/3.46 | | GROUND_INST: instantiating (3) with all_5_2, all_29_0, all_12_0, all_5_2, % 18.75/3.46 | | simplifying with (19), (164) gives: % 18.75/3.46 | | (169) all_29_0 = all_5_2 % 18.75/3.46 | | % 18.75/3.46 | | GROUND_INST: instantiating (3) with all_72_0, all_35_0, all_14_0, all_5_2, % 18.75/3.46 | | simplifying with (122), (163) gives: % 18.75/3.46 | | (170) all_72_0 = all_35_0 % 18.75/3.46 | | % 18.75/3.46 | | GROUND_INST: instantiating (3) with all_58_0, all_12_0, all_5_2, all_29_0, % 18.75/3.46 | | simplifying with (102), (161) gives: % 18.75/3.46 | | (171) all_58_0 = all_12_0 % 18.75/3.46 | | % 18.75/3.46 | | GROUND_INST: instantiating (3) with all_50_0, all_14_0, all_5_3, all_31_0, % 18.75/3.46 | | simplifying with (88), (160) gives: % 18.75/3.46 | | (172) all_50_0 = all_14_0 % 18.75/3.46 | | % 18.75/3.46 | | GROUND_INST: instantiating (3) with all_68_0, all_35_0, all_5_3, all_37_0, % 18.75/3.46 | | simplifying with (116), (159) gives: % 18.75/3.46 | | (173) all_68_0 = all_35_0 % 18.75/3.46 | | % 18.75/3.46 | | REDUCE: (135), (169) imply: % 18.75/3.46 | | (174) times(all_5_2, all_82_0) = all_37_0 % 18.75/3.46 | | % 18.75/3.46 | | REDUCE: (128), (169) imply: % 18.75/3.46 | | (175) times(all_5_2, all_76_0) = all_20_0 % 18.75/3.46 | | % 18.75/3.46 | | REDUCE: (46), (168) imply: % 18.75/3.46 | | (176) times(all_14_0, all_5_3) = all_5_3 % 18.75/3.46 | | % 18.75/3.46 | | REDUCE: (42), (169) imply: % 18.75/3.46 | | (177) times(all_12_0, all_5_2) = all_5_2 % 18.75/3.46 | | % 18.75/3.46 | | REDUCE: (115), (173) imply: % 18.75/3.46 | | (178) times(all_5_3, all_35_0) = all_5_1 % 18.75/3.46 | | % 18.75/3.46 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_35_0, all_5_1, % 18.75/3.46 | | all_5_1, all_20_0, simplifying with (6), (8), (29), (53), (178) % 18.75/3.46 | | gives: % 18.75/3.46 | | (179) ? [v0: $i] : (times(all_35_0, v0) = all_20_0 & times(all_5_1, % 18.75/3.46 | | all_5_3) = v0 & $i(v0) & $i(all_20_0)) % 18.75/3.46 | | % 18.75/3.46 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_35_0, all_5_3, % 18.75/3.46 | | all_5_1, all_35_0, simplifying with (6), (53), (55), (178) % 18.75/3.46 | | gives: % 18.75/3.46 | | (180) ? [v0: $i] : (times(all_35_0, v0) = all_35_0 & times(all_5_3, % 18.75/3.46 | | all_5_3) = v0 & $i(v0)) % 18.75/3.46 | | % 18.75/3.46 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_12_0, all_14_0, % 18.75/3.46 | | all_5_2, all_35_0, simplifying with (7), (17), (19), (21), % 18.75/3.46 | | (163) gives: % 18.75/3.46 | | (181) ? [v0: $i] : (times(all_14_0, all_5_2) = v0 & times(all_12_0, v0) % 18.75/3.46 | | = all_35_0 & $i(v0) & $i(all_35_0)) % 18.75/3.46 | | % 18.75/3.46 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_12_0, all_76_0, % 18.75/3.46 | | all_5_2, all_20_0, simplifying with (7), (17), (19), (127), % 18.75/3.46 | | (175) gives: % 18.75/3.47 | | (182) ? [v0: $i] : (times(all_76_0, all_5_2) = v0 & times(all_12_0, v0) % 18.75/3.47 | | = all_20_0 & $i(v0) & $i(all_20_0)) % 18.75/3.47 | | % 18.75/3.47 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_12_0, all_82_0, % 18.75/3.47 | | all_5_2, all_37_0, simplifying with (7), (17), (19), (133), % 18.75/3.47 | | (174) gives: % 18.75/3.47 | | (183) ? [v0: $i] : (times(all_82_0, all_5_2) = v0 & times(all_12_0, v0) % 18.75/3.47 | | = all_37_0 & $i(v0) & $i(all_37_0)) % 18.75/3.47 | | % 18.75/3.47 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_37_0, all_14_0, % 18.75/3.47 | | all_5_1, all_70_0, simplifying with (21), (57), (59), (119) % 18.75/3.47 | | gives: % 18.75/3.47 | | (184) ? [v0: $i] : (times(all_37_0, v0) = all_70_0 & times(all_14_0, % 18.75/3.47 | | all_14_0) = v0 & $i(v0) & $i(all_70_0)) % 18.75/3.47 | | % 18.75/3.47 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_5_2, all_14_0, % 18.75/3.47 | | all_5_1, all_70_0, simplifying with (6), (7), (9), (21), (119) % 18.75/3.47 | | gives: % 18.75/3.47 | | (185) ? [v0: $i] : (times(all_14_0, all_5_3) = v0 & times(all_5_2, v0) = % 18.75/3.47 | | all_70_0 & $i(v0) & $i(all_70_0)) % 18.75/3.47 | | % 18.75/3.47 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_35_0, all_14_0, % 18.75/3.47 | | all_5_1, all_70_0, simplifying with (6), (21), (53), (119), % 18.75/3.47 | | (178) gives: % 18.75/3.47 | | (186) ? [v0: $i] : (times(all_35_0, v0) = all_70_0 & times(all_14_0, % 18.75/3.47 | | all_5_3) = v0 & $i(v0) & $i(all_70_0)) % 18.75/3.47 | | % 18.75/3.47 | | GROUND_INST: instantiating (axiom_1) with all_12_0, all_5_2, all_14_0, % 18.75/3.47 | | all_5_2, all_35_0, simplifying with (7), (17), (21), (163), % 18.75/3.47 | | (177) gives: % 18.75/3.47 | | (187) ? [v0: $i] : (times(all_14_0, all_12_0) = v0 & times(all_5_2, v0) % 18.75/3.47 | | = all_35_0 & $i(v0) & $i(all_35_0)) % 18.75/3.47 | | % 18.75/3.47 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_5_2, all_5_1, % 18.75/3.47 | | all_12_0, all_37_0, simplifying with (7), (8), (18), (162) % 18.75/3.47 | | gives: % 18.75/3.47 | | (188) ? [v0: $i] : (times(all_5_1, all_5_2) = v0 & times(all_5_2, v0) = % 18.75/3.47 | | all_37_0 & $i(v0) & $i(all_37_0)) % 18.75/3.47 | | % 18.75/3.47 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_5_2, all_64_0, % 18.75/3.47 | | all_12_0, all_20_0, simplifying with (7), (18), (110), (111) % 18.75/3.47 | | gives: % 18.75/3.47 | | (189) ? [v0: $i] : (times(all_64_0, all_5_2) = v0 & times(all_5_2, v0) = % 18.75/3.47 | | all_20_0 & $i(v0) & $i(all_20_0)) % 18.75/3.47 | | % 18.75/3.47 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_5_3, all_35_0, % 18.75/3.47 | | all_5_3, all_5_1, simplifying with (6), (21), (53), (176), % 18.75/3.47 | | (178) gives: % 18.75/3.48 | | (190) ? [v0: $i] : (times(all_35_0, all_14_0) = v0 & times(all_5_3, v0) % 18.75/3.48 | | = all_5_1 & $i(v0) & $i(all_5_1)) % 18.75/3.48 | | % 18.75/3.48 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_5_3, all_12_0, % 18.75/3.48 | | all_5_3, all_82_0, simplifying with (6), (17), (21), (134), % 18.75/3.48 | | (176) gives: % 18.75/3.48 | | (191) ? [v0: $i] : (times(all_12_0, all_14_0) = v0 & times(all_5_3, v0) % 18.75/3.48 | | = all_82_0 & $i(v0) & $i(all_82_0)) % 18.75/3.48 | | % 18.75/3.48 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_86_0, all_5_1, % 18.75/3.48 | | all_5_1, all_20_0, simplifying with (8), (21), (29), (140), % 18.75/3.48 | | (141) gives: % 18.75/3.48 | | (192) ? [v0: $i] : (times(all_86_0, v0) = all_20_0 & times(all_5_1, % 18.75/3.48 | | all_14_0) = v0 & $i(v0) & $i(all_20_0)) % 18.75/3.48 | | % 18.75/3.48 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_86_0, all_5_3, % 18.75/3.48 | | all_5_1, all_35_0, simplifying with (6), (21), (55), (140), % 18.75/3.48 | | (141) gives: % 18.75/3.48 | | (193) ? [v0: $i] : (times(all_86_0, v0) = all_35_0 & times(all_5_3, % 18.75/3.48 | | all_14_0) = v0 & $i(v0) & $i(all_35_0)) % 18.75/3.48 | | % 18.75/3.48 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_5_3, all_86_0, % 18.75/3.48 | | all_14_0, all_5_1, simplifying with (6), (22), (140), (141) % 18.75/3.48 | | gives: % 18.75/3.48 | | (194) ? [v0: $i] : (times(all_86_0, all_5_3) = v0 & times(all_5_3, v0) = % 18.75/3.48 | | all_5_1 & $i(v0) & $i(all_5_1)) % 18.75/3.48 | | % 18.75/3.48 | | GROUND_INST: instantiating (axiom_1) with all_14_0, all_86_0, all_14_0, % 18.75/3.48 | | all_5_1, all_70_0, simplifying with (21), (119), (140), (141) % 18.75/3.48 | | gives: % 18.75/3.48 | | (195) ? [v0: $i] : (times(all_86_0, v0) = all_70_0 & times(all_14_0, % 18.75/3.48 | | all_14_0) = v0 & $i(v0) & $i(all_70_0)) % 18.75/3.48 | | % 18.75/3.48 | | GROUND_INST: instantiating (axiom_1) with all_5_1, all_5_3, all_5_2, % 18.75/3.48 | | all_35_0, all_64_0, simplifying with (6), (7), (8), (55), (112) % 18.75/3.48 | | gives: % 18.75/3.48 | | (196) ? [v0: $i] : (times(all_5_2, all_5_1) = v0 & times(all_5_3, v0) = % 18.75/3.48 | | all_64_0 & $i(v0) & $i(all_64_0)) % 18.75/3.48 | | % 18.75/3.48 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_14_0, all_5_2, % 18.75/3.48 | | all_35_0, all_64_0, simplifying with (7), (21), (112), (163) % 18.75/3.48 | | gives: % 18.75/3.48 | | (197) ? [v0: $i] : (times(all_14_0, v0) = all_64_0 & times(all_5_2, % 18.75/3.48 | | all_5_2) = v0 & $i(v0) & $i(all_64_0)) % 18.75/3.48 | | % 18.75/3.48 | | GROUND_INST: instantiating (axiom_1) with all_5_1, all_5_3, all_12_0, % 18.75/3.48 | | all_35_0, all_76_0, simplifying with (6), (8), (17), (55), % 18.75/3.48 | | (129) gives: % 18.75/3.48 | | (198) ? [v0: $i] : (times(all_12_0, all_5_1) = v0 & times(all_5_3, v0) = % 18.75/3.48 | | all_76_0 & $i(v0) & $i(all_76_0)) % 18.75/3.48 | | % 18.75/3.48 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_14_0, all_12_0, % 18.75/3.48 | | all_35_0, all_76_0, simplifying with (7), (17), (21), (129), % 18.75/3.48 | | (163) gives: % 18.75/3.48 | | (199) ? [v0: $i] : (times(all_14_0, v0) = all_76_0 & times(all_12_0, % 18.75/3.48 | | all_5_2) = v0 & $i(v0) & $i(all_76_0)) % 18.75/3.48 | | % 18.75/3.48 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_5_3, all_5_3, % 18.75/3.48 | | all_37_0, all_35_0, simplifying with (6), (7), (58), (159) % 18.75/3.48 | | gives: % 18.75/3.48 | | (200) ? [v0: $i] : (times(all_5_3, v0) = all_35_0 & times(all_5_3, % 18.75/3.48 | | all_5_2) = v0 & $i(v0) & $i(all_35_0)) % 18.75/3.48 | | % 18.75/3.49 | | GROUND_INST: instantiating (axiom_1) with all_37_0, all_5_3, all_12_0, % 18.75/3.49 | | all_35_0, all_76_0, simplifying with (6), (17), (57), (129), % 18.75/3.49 | | (159) gives: % 18.75/3.49 | | (201) ? [v0: $i] : (times(all_12_0, all_37_0) = v0 & times(all_5_3, v0) % 18.75/3.49 | | = all_76_0 & $i(v0) & $i(all_76_0)) % 18.75/3.49 | | % 18.75/3.49 | | GROUND_INST: instantiating (axiom_1) with all_37_0, all_5_3, all_5_2, % 18.75/3.49 | | all_35_0, all_64_0, simplifying with (6), (7), (57), (112), % 18.75/3.49 | | (159) gives: % 18.75/3.49 | | (202) ? [v0: $i] : (times(all_5_2, all_37_0) = v0 & times(all_5_3, v0) = % 18.75/3.49 | | all_64_0 & $i(v0) & $i(all_64_0)) % 18.75/3.49 | | % 18.75/3.49 | | GROUND_INST: instantiating (axiom_1) with all_12_0, all_5_1, all_5_3, % 18.75/3.49 | | all_37_0, all_35_0, simplifying with (6), (8), (17), (159), % 18.75/3.49 | | (162) gives: % 18.75/3.49 | | (203) ? [v0: $i] : (times(all_5_1, v0) = all_35_0 & times(all_5_3, % 18.75/3.49 | | all_12_0) = v0 & $i(v0) & $i(all_35_0)) % 18.75/3.49 | | % 18.75/3.49 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_82_0, all_5_3, % 18.75/3.49 | | all_37_0, all_35_0, simplifying with (6), (7), (133), (159), % 18.75/3.49 | | (174) gives: % 18.75/3.49 | | (204) ? [v0: $i] : (times(all_82_0, v0) = all_35_0 & times(all_5_3, % 18.75/3.49 | | all_5_2) = v0 & $i(v0) & $i(all_35_0)) % 18.75/3.49 | | % 18.75/3.49 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_5_3, all_14_0, % 18.75/3.49 | | all_37_0, all_86_0, simplifying with (6), (7), (21), (58), % 18.75/3.49 | | (142) gives: % 18.75/3.49 | | (205) ? [v0: $i] : (times(all_14_0, all_5_2) = v0 & times(all_5_3, v0) = % 18.75/3.49 | | all_86_0 & $i(v0) & $i(all_86_0)) % 18.75/3.49 | | % 18.75/3.49 | | GROUND_INST: instantiating (axiom_1) with all_12_0, all_5_1, all_14_0, % 18.75/3.49 | | all_37_0, all_86_0, simplifying with (8), (17), (21), (142), % 18.75/3.49 | | (162) gives: % 18.75/3.49 | | (206) ? [v0: $i] : (times(all_14_0, all_12_0) = v0 & times(all_5_1, v0) % 18.75/3.49 | | = all_86_0 & $i(v0) & $i(all_86_0)) % 18.75/3.49 | | % 18.75/3.49 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_82_0, all_14_0, % 18.75/3.49 | | all_37_0, all_86_0, simplifying with (7), (21), (133), (142), % 18.75/3.49 | | (174) gives: % 18.75/3.49 | | (207) ? [v0: $i] : (times(all_82_0, v0) = all_86_0 & times(all_14_0, % 18.75/3.49 | | all_5_2) = v0 & $i(v0) & $i(all_86_0)) % 18.75/3.49 | | % 18.75/3.49 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_5_3, all_70_0, % 18.75/3.49 | | all_37_0, all_20_0, simplifying with (6), (7), (58), (118), % 18.75/3.49 | | (120) gives: % 18.75/3.49 | | (208) ? [v0: $i] : (times(all_70_0, all_5_2) = v0 & times(all_5_3, v0) = % 18.75/3.49 | | all_20_0 & $i(v0) & $i(all_20_0)) % 18.75/3.49 | | % 18.75/3.49 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_82_0, all_70_0, % 18.75/3.49 | | all_37_0, all_20_0, simplifying with (7), (118), (120), (133), % 18.75/3.49 | | (174) gives: % 18.75/3.49 | | (209) ? [v0: $i] : (times(all_82_0, v0) = all_20_0 & times(all_70_0, % 18.75/3.49 | | all_5_2) = v0 & $i(v0) & $i(all_20_0)) % 18.75/3.49 | | % 18.75/3.49 | | DELTA: instantiating (180) with fresh symbol all_105_0 gives: % 18.75/3.49 | | (210) times(all_35_0, all_105_0) = all_35_0 & times(all_5_3, all_5_3) = % 18.75/3.49 | | all_105_0 & $i(all_105_0) % 18.75/3.49 | | % 18.75/3.49 | | ALPHA: (210) implies: % 18.75/3.49 | | (211) $i(all_105_0) % 18.75/3.49 | | (212) times(all_5_3, all_5_3) = all_105_0 % 18.75/3.49 | | (213) times(all_35_0, all_105_0) = all_35_0 % 18.75/3.49 | | % 18.75/3.49 | | DELTA: instantiating (209) with fresh symbol all_107_0 gives: % 18.75/3.49 | | (214) times(all_82_0, all_107_0) = all_20_0 & times(all_70_0, all_5_2) = % 18.75/3.49 | | all_107_0 & $i(all_107_0) & $i(all_20_0) % 18.75/3.49 | | % 18.75/3.49 | | ALPHA: (214) implies: % 18.75/3.49 | | (215) times(all_70_0, all_5_2) = all_107_0 % 18.75/3.49 | | % 18.75/3.49 | | DELTA: instantiating (208) with fresh symbol all_111_0 gives: % 18.75/3.49 | | (216) times(all_70_0, all_5_2) = all_111_0 & times(all_5_3, all_111_0) = % 18.75/3.49 | | all_20_0 & $i(all_111_0) & $i(all_20_0) % 18.75/3.49 | | % 18.75/3.49 | | ALPHA: (216) implies: % 18.75/3.49 | | (217) times(all_70_0, all_5_2) = all_111_0 % 18.75/3.49 | | % 18.75/3.49 | | DELTA: instantiating (179) with fresh symbol all_117_0 gives: % 18.75/3.50 | | (218) times(all_35_0, all_117_0) = all_20_0 & times(all_5_1, all_5_3) = % 18.75/3.50 | | all_117_0 & $i(all_117_0) & $i(all_20_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (218) implies: % 18.75/3.50 | | (219) times(all_5_1, all_5_3) = all_117_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (188) with fresh symbol all_119_0 gives: % 18.75/3.50 | | (220) times(all_5_1, all_5_2) = all_119_0 & times(all_5_2, all_119_0) = % 18.75/3.50 | | all_37_0 & $i(all_119_0) & $i(all_37_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (220) implies: % 18.75/3.50 | | (221) times(all_5_1, all_5_2) = all_119_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (187) with fresh symbol all_123_0 gives: % 18.75/3.50 | | (222) times(all_14_0, all_12_0) = all_123_0 & times(all_5_2, all_123_0) = % 18.75/3.50 | | all_35_0 & $i(all_123_0) & $i(all_35_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (222) implies: % 18.75/3.50 | | (223) times(all_14_0, all_12_0) = all_123_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (207) with fresh symbol all_125_0 gives: % 18.75/3.50 | | (224) times(all_82_0, all_125_0) = all_86_0 & times(all_14_0, all_5_2) = % 18.75/3.50 | | all_125_0 & $i(all_125_0) & $i(all_86_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (224) implies: % 18.75/3.50 | | (225) times(all_14_0, all_5_2) = all_125_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (206) with fresh symbol all_127_0 gives: % 18.75/3.50 | | (226) times(all_14_0, all_12_0) = all_127_0 & times(all_5_1, all_127_0) = % 18.75/3.50 | | all_86_0 & $i(all_127_0) & $i(all_86_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (226) implies: % 18.75/3.50 | | (227) $i(all_127_0) % 18.75/3.50 | | (228) times(all_5_1, all_127_0) = all_86_0 % 18.75/3.50 | | (229) times(all_14_0, all_12_0) = all_127_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (203) with fresh symbol all_129_0 gives: % 18.75/3.50 | | (230) times(all_5_1, all_129_0) = all_35_0 & times(all_5_3, all_12_0) = % 18.75/3.50 | | all_129_0 & $i(all_129_0) & $i(all_35_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (230) implies: % 18.75/3.50 | | (231) $i(all_129_0) % 18.75/3.50 | | (232) times(all_5_3, all_12_0) = all_129_0 % 18.75/3.50 | | (233) times(all_5_1, all_129_0) = all_35_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (202) with fresh symbol all_131_0 gives: % 18.75/3.50 | | (234) times(all_5_2, all_37_0) = all_131_0 & times(all_5_3, all_131_0) = % 18.75/3.50 | | all_64_0 & $i(all_131_0) & $i(all_64_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (234) implies: % 18.75/3.50 | | (235) $i(all_131_0) % 18.75/3.50 | | (236) times(all_5_3, all_131_0) = all_64_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (199) with fresh symbol all_133_0 gives: % 18.75/3.50 | | (237) times(all_14_0, all_133_0) = all_76_0 & times(all_12_0, all_5_2) = % 18.75/3.50 | | all_133_0 & $i(all_133_0) & $i(all_76_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (237) implies: % 18.75/3.50 | | (238) $i(all_133_0) % 18.75/3.50 | | (239) times(all_12_0, all_5_2) = all_133_0 % 18.75/3.50 | | (240) times(all_14_0, all_133_0) = all_76_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (197) with fresh symbol all_135_0 gives: % 18.75/3.50 | | (241) times(all_14_0, all_135_0) = all_64_0 & times(all_5_2, all_5_2) = % 18.75/3.50 | | all_135_0 & $i(all_135_0) & $i(all_64_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (241) implies: % 18.75/3.50 | | (242) $i(all_135_0) % 18.75/3.50 | | (243) times(all_5_2, all_5_2) = all_135_0 % 18.75/3.50 | | (244) times(all_14_0, all_135_0) = all_64_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (184) with fresh symbol all_137_0 gives: % 18.75/3.50 | | (245) times(all_37_0, all_137_0) = all_70_0 & times(all_14_0, all_14_0) = % 18.75/3.50 | | all_137_0 & $i(all_137_0) & $i(all_70_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (245) implies: % 18.75/3.50 | | (246) times(all_14_0, all_14_0) = all_137_0 % 18.75/3.50 | | (247) times(all_37_0, all_137_0) = all_70_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (182) with fresh symbol all_139_0 gives: % 18.75/3.50 | | (248) times(all_76_0, all_5_2) = all_139_0 & times(all_12_0, all_139_0) = % 18.75/3.50 | | all_20_0 & $i(all_139_0) & $i(all_20_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (248) implies: % 18.75/3.50 | | (249) times(all_76_0, all_5_2) = all_139_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (181) with fresh symbol all_141_0 gives: % 18.75/3.50 | | (250) times(all_14_0, all_5_2) = all_141_0 & times(all_12_0, all_141_0) = % 18.75/3.50 | | all_35_0 & $i(all_141_0) & $i(all_35_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (250) implies: % 18.75/3.50 | | (251) $i(all_141_0) % 18.75/3.50 | | (252) times(all_12_0, all_141_0) = all_35_0 % 18.75/3.50 | | (253) times(all_14_0, all_5_2) = all_141_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (196) with fresh symbol all_143_0 gives: % 18.75/3.50 | | (254) times(all_5_2, all_5_1) = all_143_0 & times(all_5_3, all_143_0) = % 18.75/3.50 | | all_64_0 & $i(all_143_0) & $i(all_64_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (254) implies: % 18.75/3.50 | | (255) $i(all_143_0) % 18.75/3.50 | | (256) times(all_5_3, all_143_0) = all_64_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (183) with fresh symbol all_145_0 gives: % 18.75/3.50 | | (257) times(all_82_0, all_5_2) = all_145_0 & times(all_12_0, all_145_0) = % 18.75/3.50 | | all_37_0 & $i(all_145_0) & $i(all_37_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (257) implies: % 18.75/3.50 | | (258) times(all_82_0, all_5_2) = all_145_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (198) with fresh symbol all_147_0 gives: % 18.75/3.50 | | (259) times(all_12_0, all_5_1) = all_147_0 & times(all_5_3, all_147_0) = % 18.75/3.50 | | all_76_0 & $i(all_147_0) & $i(all_76_0) % 18.75/3.50 | | % 18.75/3.50 | | ALPHA: (259) implies: % 18.75/3.50 | | (260) times(all_5_3, all_147_0) = all_76_0 % 18.75/3.50 | | (261) times(all_12_0, all_5_1) = all_147_0 % 18.75/3.50 | | % 18.75/3.50 | | DELTA: instantiating (201) with fresh symbol all_149_0 gives: % 18.75/3.50 | | (262) times(all_12_0, all_37_0) = all_149_0 & times(all_5_3, all_149_0) = % 18.75/3.51 | | all_76_0 & $i(all_149_0) & $i(all_76_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (262) implies: % 18.75/3.51 | | (263) $i(all_149_0) % 18.75/3.51 | | (264) times(all_5_3, all_149_0) = all_76_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (200) with fresh symbol all_151_0 gives: % 18.75/3.51 | | (265) times(all_5_3, all_151_0) = all_35_0 & times(all_5_3, all_5_2) = % 18.75/3.51 | | all_151_0 & $i(all_151_0) & $i(all_35_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (265) implies: % 18.75/3.51 | | (266) $i(all_151_0) % 18.75/3.51 | | (267) times(all_5_3, all_5_2) = all_151_0 % 18.75/3.51 | | (268) times(all_5_3, all_151_0) = all_35_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (186) with fresh symbol all_155_0 gives: % 18.75/3.51 | | (269) times(all_35_0, all_155_0) = all_70_0 & times(all_14_0, all_5_3) = % 18.75/3.51 | | all_155_0 & $i(all_155_0) & $i(all_70_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (269) implies: % 18.75/3.51 | | (270) $i(all_155_0) % 18.75/3.51 | | (271) times(all_14_0, all_5_3) = all_155_0 % 18.75/3.51 | | (272) times(all_35_0, all_155_0) = all_70_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (185) with fresh symbol all_157_0 gives: % 18.75/3.51 | | (273) times(all_14_0, all_5_3) = all_157_0 & times(all_5_2, all_157_0) = % 18.75/3.51 | | all_70_0 & $i(all_157_0) & $i(all_70_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (273) implies: % 18.75/3.51 | | (274) times(all_5_2, all_157_0) = all_70_0 % 18.75/3.51 | | (275) times(all_14_0, all_5_3) = all_157_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (195) with fresh symbol all_161_0 gives: % 18.75/3.51 | | (276) times(all_86_0, all_161_0) = all_70_0 & times(all_14_0, all_14_0) = % 18.75/3.51 | | all_161_0 & $i(all_161_0) & $i(all_70_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (276) implies: % 18.75/3.51 | | (277) times(all_14_0, all_14_0) = all_161_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (193) with fresh symbol all_163_0 gives: % 18.75/3.51 | | (278) times(all_86_0, all_163_0) = all_35_0 & times(all_5_3, all_14_0) = % 18.75/3.51 | | all_163_0 & $i(all_163_0) & $i(all_35_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (278) implies: % 18.75/3.51 | | (279) times(all_5_3, all_14_0) = all_163_0 % 18.75/3.51 | | (280) times(all_86_0, all_163_0) = all_35_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (192) with fresh symbol all_165_0 gives: % 18.75/3.51 | | (281) times(all_86_0, all_165_0) = all_20_0 & times(all_5_1, all_14_0) = % 18.75/3.51 | | all_165_0 & $i(all_165_0) & $i(all_20_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (281) implies: % 18.75/3.51 | | (282) $i(all_165_0) % 18.75/3.51 | | (283) times(all_5_1, all_14_0) = all_165_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (205) with fresh symbol all_169_0 gives: % 18.75/3.51 | | (284) times(all_14_0, all_5_2) = all_169_0 & times(all_5_3, all_169_0) = % 18.75/3.51 | | all_86_0 & $i(all_169_0) & $i(all_86_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (284) implies: % 18.75/3.51 | | (285) times(all_5_3, all_169_0) = all_86_0 % 18.75/3.51 | | (286) times(all_14_0, all_5_2) = all_169_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (204) with fresh symbol all_171_0 gives: % 18.75/3.51 | | (287) times(all_82_0, all_171_0) = all_35_0 & times(all_5_3, all_5_2) = % 18.75/3.51 | | all_171_0 & $i(all_171_0) & $i(all_35_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (287) implies: % 18.75/3.51 | | (288) times(all_5_3, all_5_2) = all_171_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (194) with fresh symbol all_173_0 gives: % 18.75/3.51 | | (289) times(all_86_0, all_5_3) = all_173_0 & times(all_5_3, all_173_0) = % 18.75/3.51 | | all_5_1 & $i(all_173_0) & $i(all_5_1) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (289) implies: % 18.75/3.51 | | (290) $i(all_173_0) % 18.75/3.51 | | (291) times(all_5_3, all_173_0) = all_5_1 % 18.75/3.51 | | (292) times(all_86_0, all_5_3) = all_173_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (191) with fresh symbol all_177_0 gives: % 18.75/3.51 | | (293) times(all_12_0, all_14_0) = all_177_0 & times(all_5_3, all_177_0) = % 18.75/3.51 | | all_82_0 & $i(all_177_0) & $i(all_82_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (293) implies: % 18.75/3.51 | | (294) $i(all_177_0) % 18.75/3.51 | | (295) times(all_5_3, all_177_0) = all_82_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (190) with fresh symbol all_179_0 gives: % 18.75/3.51 | | (296) times(all_35_0, all_14_0) = all_179_0 & times(all_5_3, all_179_0) = % 18.75/3.51 | | all_5_1 & $i(all_179_0) & $i(all_5_1) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (296) implies: % 18.75/3.51 | | (297) times(all_35_0, all_14_0) = all_179_0 % 18.75/3.51 | | % 18.75/3.51 | | DELTA: instantiating (189) with fresh symbol all_181_0 gives: % 18.75/3.51 | | (298) times(all_64_0, all_5_2) = all_181_0 & times(all_5_2, all_181_0) = % 18.75/3.51 | | all_20_0 & $i(all_181_0) & $i(all_20_0) % 18.75/3.51 | | % 18.75/3.51 | | ALPHA: (298) implies: % 18.75/3.51 | | (299) times(all_64_0, all_5_2) = all_181_0 % 18.75/3.51 | | % 18.75/3.51 | | GROUND_INST: instantiating (3) with all_14_0, all_105_0, all_5_3, all_5_3, % 18.75/3.51 | | simplifying with (22), (212) gives: % 18.75/3.51 | | (300) all_105_0 = all_14_0 % 18.75/3.51 | | % 18.75/3.51 | | GROUND_INST: instantiating (3) with all_5_1, all_171_0, all_5_2, all_5_3, % 18.75/3.51 | | simplifying with (9), (288) gives: % 18.75/3.51 | | (301) all_171_0 = all_5_1 % 18.75/3.51 | | % 18.75/3.51 | | GROUND_INST: instantiating (3) with all_151_0, all_171_0, all_5_2, all_5_3, % 18.75/3.51 | | simplifying with (267), (288) gives: % 18.75/3.51 | | (302) all_171_0 = all_151_0 % 18.75/3.51 | | % 18.75/3.51 | | GROUND_INST: instantiating (3) with all_82_0, all_129_0, all_12_0, all_5_3, % 18.75/3.51 | | simplifying with (134), (232) gives: % 18.75/3.51 | | (303) all_129_0 = all_82_0 % 18.75/3.51 | | % 18.75/3.51 | | GROUND_INST: instantiating (3) with all_5_3, all_163_0, all_14_0, all_5_3, % 18.75/3.51 | | simplifying with (23), (279) gives: % 18.75/3.51 | | (304) all_163_0 = all_5_3 % 18.75/3.51 | | % 18.75/3.51 | | GROUND_INST: instantiating (3) with all_12_0, all_135_0, all_5_2, all_5_2, % 18.75/3.51 | | simplifying with (18), (243) gives: % 18.75/3.51 | | (305) all_135_0 = all_12_0 % 18.75/3.51 | | % 18.75/3.51 | | GROUND_INST: instantiating (3) with all_35_0, all_117_0, all_5_3, all_5_1, % 18.75/3.51 | | simplifying with (55), (219) gives: % 18.75/3.51 | | (306) all_117_0 = all_35_0 % 18.75/3.51 | | % 18.75/3.51 | | GROUND_INST: instantiating (3) with all_70_0, all_165_0, all_14_0, all_5_1, % 18.75/3.51 | | simplifying with (119), (283) gives: % 18.75/3.51 | | (307) all_165_0 = all_70_0 % 18.75/3.51 | | % 18.75/3.51 | | GROUND_INST: instantiating (3) with all_5_2, all_133_0, all_5_2, all_12_0, % 18.75/3.51 | | simplifying with (177), (239) gives: % 18.75/3.52 | | (308) all_133_0 = all_5_2 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_37_0, all_147_0, all_5_1, all_12_0, % 18.75/3.52 | | simplifying with (162), (261) gives: % 18.75/3.52 | | (309) all_147_0 = all_37_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_5_3, all_157_0, all_5_3, all_14_0, % 18.75/3.52 | | simplifying with (176), (275) gives: % 18.75/3.52 | | (310) all_157_0 = all_5_3 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_155_0, all_157_0, all_5_3, all_14_0, % 18.75/3.52 | | simplifying with (271), (275) gives: % 18.75/3.52 | | (311) all_157_0 = all_155_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_141_0, all_169_0, all_5_2, all_14_0, % 18.75/3.52 | | simplifying with (253), (286) gives: % 18.75/3.52 | | (312) all_169_0 = all_141_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_125_0, all_169_0, all_5_2, all_14_0, % 18.75/3.52 | | simplifying with (225), (286) gives: % 18.75/3.52 | | (313) all_169_0 = all_125_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_123_0, all_127_0, all_12_0, % 18.75/3.52 | | all_14_0, simplifying with (223), (229) gives: % 18.75/3.52 | | (314) all_127_0 = all_123_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_14_0, all_161_0, all_14_0, all_14_0, % 18.75/3.52 | | simplifying with (62), (277) gives: % 18.75/3.52 | | (315) all_161_0 = all_14_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_137_0, all_161_0, all_14_0, % 18.75/3.52 | | all_14_0, simplifying with (246), (277) gives: % 18.75/3.52 | | (316) all_161_0 = all_137_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_107_0, all_111_0, all_5_2, all_70_0, % 18.75/3.52 | | simplifying with (215), (217) gives: % 18.75/3.52 | | (317) all_111_0 = all_107_0 % 18.75/3.52 | | % 18.75/3.52 | | COMBINE_EQS: (301), (302) imply: % 18.75/3.52 | | (318) all_151_0 = all_5_1 % 18.75/3.52 | | % 18.75/3.52 | | COMBINE_EQS: (312), (313) imply: % 18.75/3.52 | | (319) all_141_0 = all_125_0 % 18.75/3.52 | | % 18.75/3.52 | | SIMP: (319) implies: % 18.75/3.52 | | (320) all_141_0 = all_125_0 % 18.75/3.52 | | % 18.75/3.52 | | COMBINE_EQS: (315), (316) imply: % 18.75/3.52 | | (321) all_137_0 = all_14_0 % 18.75/3.52 | | % 18.75/3.52 | | SIMP: (321) implies: % 18.75/3.52 | | (322) all_137_0 = all_14_0 % 18.75/3.52 | | % 18.75/3.52 | | COMBINE_EQS: (310), (311) imply: % 18.75/3.52 | | (323) all_155_0 = all_5_3 % 18.75/3.52 | | % 18.75/3.52 | | SIMP: (323) implies: % 18.75/3.52 | | (324) all_155_0 = all_5_3 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (280), (304) imply: % 18.75/3.52 | | (325) times(all_86_0, all_5_3) = all_35_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (247), (322) imply: % 18.75/3.52 | | (326) times(all_37_0, all_14_0) = all_70_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (272), (324) imply: % 18.75/3.52 | | (327) times(all_35_0, all_5_3) = all_70_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (213), (300) imply: % 18.75/3.52 | | (328) times(all_35_0, all_14_0) = all_35_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (244), (305) imply: % 18.75/3.52 | | (329) times(all_14_0, all_12_0) = all_64_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (240), (308) imply: % 18.75/3.52 | | (330) times(all_14_0, all_5_2) = all_76_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (252), (320) imply: % 18.75/3.52 | | (331) times(all_12_0, all_125_0) = all_35_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (233), (303) imply: % 18.75/3.52 | | (332) times(all_5_1, all_82_0) = all_35_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (228), (314) imply: % 18.75/3.52 | | (333) times(all_5_1, all_123_0) = all_86_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (274), (310) imply: % 18.75/3.52 | | (334) times(all_5_2, all_5_3) = all_70_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (285), (313) imply: % 18.75/3.52 | | (335) times(all_5_3, all_125_0) = all_86_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (268), (318) imply: % 18.75/3.52 | | (336) times(all_5_3, all_5_1) = all_35_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (260), (309) imply: % 18.75/3.52 | | (337) times(all_5_3, all_37_0) = all_76_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (251), (320) imply: % 18.75/3.52 | | (338) $i(all_125_0) % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (227), (314) imply: % 18.75/3.52 | | (339) $i(all_123_0) % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_37_0, all_70_0, all_5_3, all_5_2, % 18.75/3.52 | | simplifying with (58), (334) gives: % 18.75/3.52 | | (340) all_70_0 = all_37_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_125_0, all_76_0, all_5_2, all_14_0, % 18.75/3.52 | | simplifying with (225), (330) gives: % 18.75/3.52 | | (341) all_125_0 = all_76_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_123_0, all_64_0, all_12_0, all_14_0, % 18.75/3.52 | | simplifying with (223), (329) gives: % 18.75/3.52 | | (342) all_123_0 = all_64_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_179_0, all_35_0, all_14_0, all_35_0, % 18.75/3.52 | | simplifying with (297), (328) gives: % 18.75/3.52 | | (343) all_179_0 = all_35_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_86_0, all_70_0, all_14_0, all_37_0, % 18.75/3.52 | | simplifying with (142), (326) gives: % 18.75/3.52 | | (344) all_86_0 = all_70_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (3) with all_173_0, all_35_0, all_5_3, all_86_0, % 18.75/3.52 | | simplifying with (292), (325) gives: % 18.75/3.52 | | (345) all_173_0 = all_35_0 % 18.75/3.52 | | % 18.75/3.52 | | COMBINE_EQS: (340), (344) imply: % 18.75/3.52 | | (346) all_86_0 = all_37_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (215), (340) imply: % 18.75/3.52 | | (347) times(all_37_0, all_5_2) = all_107_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (120), (340) imply: % 18.75/3.52 | | (348) times(all_37_0, all_37_0) = all_20_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (326), (340) imply: % 18.75/3.52 | | (349) times(all_37_0, all_14_0) = all_37_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (327), (340) imply: % 18.75/3.52 | | (350) times(all_35_0, all_5_3) = all_37_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (331), (341) imply: % 18.75/3.52 | | (351) times(all_12_0, all_76_0) = all_35_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (333), (342), (346) imply: % 18.75/3.52 | | (352) times(all_5_1, all_64_0) = all_37_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (119), (340) imply: % 18.75/3.52 | | (353) times(all_5_1, all_14_0) = all_37_0 % 18.75/3.52 | | % 18.75/3.52 | | REDUCE: (335), (341), (346) imply: % 18.75/3.52 | | (354) times(all_5_3, all_76_0) = all_37_0 % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_5_1, all_5_2, % 18.75/3.52 | | all_35_0, all_64_0, simplifying with (6), (7), (8), (112), % 18.75/3.52 | | (336) gives: % 18.75/3.52 | | (355) ? [v0: $i] : (times(all_5_1, v0) = all_64_0 & times(all_5_2, % 18.75/3.52 | | all_5_3) = v0 & $i(v0) & $i(all_64_0)) % 18.75/3.52 | | % 18.75/3.52 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_35_0, all_5_2, % 18.75/3.52 | | all_5_1, all_119_0, simplifying with (6), (7), (53), (178), % 18.75/3.52 | | (221) gives: % 18.75/3.53 | | (356) ? [v0: $i] : (times(all_35_0, v0) = all_119_0 & times(all_5_2, % 18.75/3.53 | | all_5_3) = v0 & $i(v0) & $i(all_119_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_5_2, all_5_2, % 18.75/3.53 | | all_5_1, all_119_0, simplifying with (6), (7), (9), (221) % 18.75/3.53 | | gives: % 18.75/3.53 | | (357) ? [v0: $i] : (times(all_5_2, v0) = all_119_0 & times(all_5_2, % 18.75/3.53 | | all_5_3) = v0 & $i(v0) & $i(all_119_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_1, all_14_0, all_5_3, % 18.75/3.53 | | all_37_0, all_35_0, simplifying with (6), (8), (21), (159), % 18.75/3.53 | | (353) gives: % 18.75/3.53 | | (358) ? [v0: $i] : (times(all_14_0, v0) = all_35_0 & times(all_5_3, % 18.75/3.53 | | all_5_1) = v0 & $i(v0) & $i(all_35_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_1, all_64_0, all_5_3, % 18.75/3.53 | | all_37_0, all_35_0, simplifying with (6), (8), (110), (159), % 18.75/3.53 | | (352) gives: % 18.75/3.53 | | (359) ? [v0: $i] : (times(all_64_0, v0) = all_35_0 & times(all_5_3, % 18.75/3.53 | | all_5_1) = v0 & $i(v0) & $i(all_35_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_12_0, all_76_0, all_5_2, % 18.75/3.53 | | all_35_0, all_64_0, simplifying with (7), (17), (112), (127), % 18.75/3.53 | | (351) gives: % 18.75/3.53 | | (360) ? [v0: $i] : (times(all_76_0, v0) = all_64_0 & times(all_5_2, % 18.75/3.53 | | all_12_0) = v0 & $i(v0) & $i(all_64_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_2, all_5_2, all_76_0, % 18.75/3.53 | | all_12_0, all_35_0, simplifying with (7), (18), (127), (351) % 18.75/3.53 | | gives: % 18.75/3.53 | | (361) ? [v0: $i] : (times(all_76_0, all_5_2) = v0 & times(all_5_2, v0) = % 18.75/3.53 | | all_35_0 & $i(v0) & $i(all_35_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_1, all_5_3, all_5_3, % 18.75/3.53 | | all_35_0, all_37_0, simplifying with (6), (8), (55), (350) % 18.75/3.53 | | gives: % 18.75/3.53 | | (362) ? [v0: $i] : (times(all_5_3, v0) = all_37_0 & times(all_5_3, % 18.75/3.53 | | all_5_1) = v0 & $i(v0) & $i(all_37_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_1, all_82_0, all_5_3, % 18.75/3.53 | | all_35_0, all_37_0, simplifying with (6), (8), (133), (332), % 18.75/3.53 | | (350) gives: % 18.75/3.53 | | (363) ? [v0: $i] : (times(all_82_0, v0) = all_37_0 & times(all_5_3, % 18.75/3.53 | | all_5_1) = v0 & $i(v0) & $i(all_37_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_35_0, all_14_0, all_5_3, % 18.75/3.53 | | all_35_0, all_37_0, simplifying with (6), (21), (53), (328), % 18.75/3.53 | | (350) gives: % 18.75/3.53 | | (364) ? [v0: $i] : (times(all_14_0, v0) = all_37_0 & times(all_5_3, % 18.75/3.53 | | all_35_0) = v0 & $i(v0) & $i(all_37_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_76_0, all_5_2, % 18.75/3.53 | | all_37_0, all_107_0, simplifying with (6), (7), (127), (347), % 18.75/3.53 | | (354) gives: % 18.75/3.53 | | (365) ? [v0: $i] : (times(all_76_0, v0) = all_107_0 & times(all_5_2, % 18.75/3.53 | | all_5_3) = v0 & $i(v0) & $i(all_107_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_37_0, all_14_0, all_37_0, % 18.75/3.53 | | all_37_0, all_20_0, simplifying with (21), (57), (348), (349) % 18.75/3.53 | | gives: % 18.75/3.53 | | (366) ? [v0: $i] : (times(all_37_0, all_37_0) = v0 & times(all_14_0, v0) % 18.75/3.53 | | = all_20_0 & $i(v0) & $i(all_20_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_143_0, all_5_2, % 18.75/3.53 | | all_64_0, all_181_0, simplifying with (6), (7), (255), (256), % 18.75/3.53 | | (299) gives: % 18.75/3.53 | | (367) ? [v0: $i] : (times(all_143_0, v0) = all_181_0 & times(all_5_2, % 18.75/3.53 | | all_5_3) = v0 & $i(v0) & $i(all_181_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_131_0, all_5_2, % 18.75/3.53 | | all_64_0, all_181_0, simplifying with (6), (7), (235), (236), % 18.75/3.53 | | (299) gives: % 18.75/3.53 | | (368) ? [v0: $i] : (times(all_131_0, v0) = all_181_0 & times(all_5_2, % 18.75/3.53 | | all_5_3) = v0 & $i(v0) & $i(all_181_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_149_0, all_5_2, % 18.75/3.53 | | all_76_0, all_139_0, simplifying with (6), (7), (249), (263), % 18.75/3.53 | | (264) gives: % 18.75/3.53 | | (369) ? [v0: $i] : (times(all_149_0, v0) = all_139_0 & times(all_5_2, % 18.75/3.53 | | all_5_3) = v0 & $i(v0) & $i(all_139_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_37_0, all_5_2, % 18.75/3.53 | | all_76_0, all_139_0, simplifying with (6), (7), (57), (249), % 18.75/3.53 | | (337) gives: % 18.75/3.53 | | (370) ? [v0: $i] : (times(all_37_0, v0) = all_139_0 & times(all_5_2, % 18.75/3.53 | | all_5_3) = v0 & $i(v0) & $i(all_139_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_12_0, all_5_2, % 18.75/3.53 | | all_82_0, all_145_0, simplifying with (6), (7), (17), (134), % 18.75/3.53 | | (258) gives: % 18.75/3.53 | | (371) ? [v0: $i] : (times(all_12_0, v0) = all_145_0 & times(all_5_2, % 18.75/3.53 | | all_5_3) = v0 & $i(v0) & $i(all_145_0)) % 18.75/3.53 | | % 18.75/3.53 | | GROUND_INST: instantiating (axiom_1) with all_5_3, all_177_0, all_5_2, % 18.75/3.53 | | all_82_0, all_145_0, simplifying with (6), (7), (258), (294), % 18.75/3.53 | | (295) gives: % 18.75/3.53 | | (372) ? [v0: $i] : (times(all_177_0, v0) = all_145_0 & times(all_5_2, % 18.75/3.53 | | all_5_3) = v0 & $i(v0) & $i(all_145_0)) % 18.75/3.53 | | % 18.75/3.53 | | DELTA: instantiating (370) with fresh symbol all_216_0 gives: % 18.75/3.53 | | (373) times(all_37_0, all_216_0) = all_139_0 & times(all_5_2, all_5_3) = % 18.75/3.53 | | all_216_0 & $i(all_216_0) & $i(all_139_0) % 18.75/3.53 | | % 18.75/3.53 | | ALPHA: (373) implies: % 18.75/3.53 | | (374) times(all_5_2, all_5_3) = all_216_0 % 18.75/3.53 | | (375) times(all_37_0, all_216_0) = all_139_0 % 18.75/3.53 | | % 18.75/3.53 | | DELTA: instantiating (367) with fresh symbol all_234_0 gives: % 18.75/3.53 | | (376) times(all_143_0, all_234_0) = all_181_0 & times(all_5_2, all_5_3) = % 18.75/3.53 | | all_234_0 & $i(all_234_0) & $i(all_181_0) % 18.75/3.53 | | % 18.75/3.53 | | ALPHA: (376) implies: % 18.75/3.53 | | (377) times(all_5_2, all_5_3) = all_234_0 % 18.75/3.53 | | % 18.75/3.53 | | DELTA: instantiating (356) with fresh symbol all_292_0 gives: % 18.75/3.54 | | (378) times(all_35_0, all_292_0) = all_119_0 & times(all_5_2, all_5_3) = % 18.75/3.54 | | all_292_0 & $i(all_292_0) & $i(all_119_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (378) implies: % 18.75/3.54 | | (379) times(all_5_2, all_5_3) = all_292_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (357) with fresh symbol all_298_0 gives: % 18.75/3.54 | | (380) times(all_5_2, all_298_0) = all_119_0 & times(all_5_2, all_5_3) = % 18.75/3.54 | | all_298_0 & $i(all_298_0) & $i(all_119_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (380) implies: % 18.75/3.54 | | (381) times(all_5_2, all_5_3) = all_298_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (368) with fresh symbol all_320_0 gives: % 18.75/3.54 | | (382) times(all_131_0, all_320_0) = all_181_0 & times(all_5_2, all_5_3) = % 18.75/3.54 | | all_320_0 & $i(all_320_0) & $i(all_181_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (382) implies: % 18.75/3.54 | | (383) times(all_5_2, all_5_3) = all_320_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (369) with fresh symbol all_348_0 gives: % 18.75/3.54 | | (384) times(all_149_0, all_348_0) = all_139_0 & times(all_5_2, all_5_3) = % 18.75/3.54 | | all_348_0 & $i(all_348_0) & $i(all_139_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (384) implies: % 18.75/3.54 | | (385) times(all_5_2, all_5_3) = all_348_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (372) with fresh symbol all_356_0 gives: % 18.75/3.54 | | (386) times(all_177_0, all_356_0) = all_145_0 & times(all_5_2, all_5_3) = % 18.75/3.54 | | all_356_0 & $i(all_356_0) & $i(all_145_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (386) implies: % 18.75/3.54 | | (387) times(all_5_2, all_5_3) = all_356_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (371) with fresh symbol all_358_0 gives: % 18.75/3.54 | | (388) times(all_12_0, all_358_0) = all_145_0 & times(all_5_2, all_5_3) = % 18.75/3.54 | | all_358_0 & $i(all_358_0) & $i(all_145_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (388) implies: % 18.75/3.54 | | (389) times(all_5_2, all_5_3) = all_358_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (360) with fresh symbol all_404_0 gives: % 18.75/3.54 | | (390) times(all_76_0, all_404_0) = all_64_0 & times(all_5_2, all_12_0) = % 18.75/3.54 | | all_404_0 & $i(all_404_0) & $i(all_64_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (390) implies: % 18.75/3.54 | | (391) times(all_5_2, all_12_0) = all_404_0 % 18.75/3.54 | | (392) times(all_76_0, all_404_0) = all_64_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (364) with fresh symbol all_412_0 gives: % 18.75/3.54 | | (393) times(all_14_0, all_412_0) = all_37_0 & times(all_5_3, all_35_0) = % 18.75/3.54 | | all_412_0 & $i(all_412_0) & $i(all_37_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (393) implies: % 18.75/3.54 | | (394) times(all_5_3, all_35_0) = all_412_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (365) with fresh symbol all_428_0 gives: % 18.75/3.54 | | (395) times(all_76_0, all_428_0) = all_107_0 & times(all_5_2, all_5_3) = % 18.75/3.54 | | all_428_0 & $i(all_428_0) & $i(all_107_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (395) implies: % 18.75/3.54 | | (396) times(all_5_2, all_5_3) = all_428_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (363) with fresh symbol all_432_0 gives: % 18.75/3.54 | | (397) times(all_82_0, all_432_0) = all_37_0 & times(all_5_3, all_5_1) = % 18.75/3.54 | | all_432_0 & $i(all_432_0) & $i(all_37_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (397) implies: % 18.75/3.54 | | (398) times(all_5_3, all_5_1) = all_432_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (359) with fresh symbol all_464_0 gives: % 18.75/3.54 | | (399) times(all_64_0, all_464_0) = all_35_0 & times(all_5_3, all_5_1) = % 18.75/3.54 | | all_464_0 & $i(all_464_0) & $i(all_35_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (399) implies: % 18.75/3.54 | | (400) times(all_5_3, all_5_1) = all_464_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (362) with fresh symbol all_468_0 gives: % 18.75/3.54 | | (401) times(all_5_3, all_468_0) = all_37_0 & times(all_5_3, all_5_1) = % 18.75/3.54 | | all_468_0 & $i(all_468_0) & $i(all_37_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (401) implies: % 18.75/3.54 | | (402) times(all_5_3, all_5_1) = all_468_0 % 18.75/3.54 | | (403) times(all_5_3, all_468_0) = all_37_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (358) with fresh symbol all_472_0 gives: % 18.75/3.54 | | (404) times(all_14_0, all_472_0) = all_35_0 & times(all_5_3, all_5_1) = % 18.75/3.54 | | all_472_0 & $i(all_472_0) & $i(all_35_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (404) implies: % 18.75/3.54 | | (405) times(all_5_3, all_5_1) = all_472_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (366) with fresh symbol all_478_0 gives: % 18.75/3.54 | | (406) times(all_37_0, all_37_0) = all_478_0 & times(all_14_0, all_478_0) % 18.75/3.54 | | = all_20_0 & $i(all_478_0) & $i(all_20_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (406) implies: % 18.75/3.54 | | (407) times(all_37_0, all_37_0) = all_478_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (355) with fresh symbol all_488_0 gives: % 18.75/3.54 | | (408) times(all_5_1, all_488_0) = all_64_0 & times(all_5_2, all_5_3) = % 18.75/3.54 | | all_488_0 & $i(all_488_0) & $i(all_64_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (408) implies: % 18.75/3.54 | | (409) times(all_5_2, all_5_3) = all_488_0 % 18.75/3.54 | | % 18.75/3.54 | | DELTA: instantiating (361) with fresh symbol all_566_0 gives: % 18.75/3.54 | | (410) times(all_76_0, all_5_2) = all_566_0 & times(all_5_2, all_566_0) = % 18.75/3.54 | | all_35_0 & $i(all_566_0) & $i(all_35_0) % 18.75/3.54 | | % 18.75/3.54 | | ALPHA: (410) implies: % 18.75/3.54 | | (411) times(all_76_0, all_5_2) = all_566_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_35_0, all_468_0, all_5_1, all_5_3, % 18.75/3.54 | | simplifying with (336), (402) gives: % 18.75/3.54 | | (412) all_468_0 = all_35_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_432_0, all_468_0, all_5_1, all_5_3, % 18.75/3.54 | | simplifying with (398), (402) gives: % 18.75/3.54 | | (413) all_468_0 = all_432_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_468_0, all_472_0, all_5_1, all_5_3, % 18.75/3.54 | | simplifying with (402), (405) gives: % 18.75/3.54 | | (414) all_472_0 = all_468_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_464_0, all_472_0, all_5_1, all_5_3, % 18.75/3.54 | | simplifying with (400), (405) gives: % 18.75/3.54 | | (415) all_472_0 = all_464_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_5_1, all_412_0, all_35_0, all_5_3, % 18.75/3.54 | | simplifying with (178), (394) gives: % 18.75/3.54 | | (416) all_412_0 = all_5_1 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_37_0, all_292_0, all_5_3, all_5_2, % 18.75/3.54 | | simplifying with (58), (379) gives: % 18.75/3.54 | | (417) all_292_0 = all_37_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_292_0, all_298_0, all_5_3, all_5_2, % 18.75/3.54 | | simplifying with (379), (381) gives: % 18.75/3.54 | | (418) all_298_0 = all_292_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_292_0, all_320_0, all_5_3, all_5_2, % 18.75/3.54 | | simplifying with (379), (383) gives: % 18.75/3.54 | | (419) all_320_0 = all_292_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_298_0, all_348_0, all_5_3, all_5_2, % 18.75/3.54 | | simplifying with (381), (385) gives: % 18.75/3.54 | | (420) all_348_0 = all_298_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_216_0, all_348_0, all_5_3, all_5_2, % 18.75/3.54 | | simplifying with (374), (385) gives: % 18.75/3.54 | | (421) all_348_0 = all_216_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_320_0, all_356_0, all_5_3, all_5_2, % 18.75/3.54 | | simplifying with (383), (387) gives: % 18.75/3.54 | | (422) all_356_0 = all_320_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_356_0, all_358_0, all_5_3, all_5_2, % 18.75/3.54 | | simplifying with (387), (389) gives: % 18.75/3.54 | | (423) all_358_0 = all_356_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_358_0, all_428_0, all_5_3, all_5_2, % 18.75/3.54 | | simplifying with (389), (396) gives: % 18.75/3.54 | | (424) all_428_0 = all_358_0 % 18.75/3.54 | | % 18.75/3.54 | | GROUND_INST: instantiating (3) with all_428_0, all_488_0, all_5_3, all_5_2, % 18.75/3.54 | | simplifying with (396), (409) gives: % 18.75/3.54 | | (425) all_488_0 = all_428_0 % 18.75/3.54 | | % 18.75/3.55 | | GROUND_INST: instantiating (3) with all_234_0, all_488_0, all_5_3, all_5_2, % 18.75/3.55 | | simplifying with (377), (409) gives: % 18.75/3.55 | | (426) all_488_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | GROUND_INST: instantiating (3) with all_5_2, all_404_0, all_12_0, all_5_2, % 18.75/3.55 | | simplifying with (19), (391) gives: % 18.75/3.55 | | (427) all_404_0 = all_5_2 % 18.75/3.55 | | % 18.75/3.55 | | GROUND_INST: instantiating (3) with all_20_0, all_478_0, all_37_0, all_37_0, % 18.75/3.55 | | simplifying with (348), (407) gives: % 18.75/3.55 | | (428) all_478_0 = all_20_0 % 18.75/3.55 | | % 18.75/3.55 | | GROUND_INST: instantiating (3) with all_139_0, all_566_0, all_5_2, all_76_0, % 18.75/3.55 | | simplifying with (249), (411) gives: % 18.75/3.55 | | (429) all_566_0 = all_139_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (425), (426) imply: % 18.75/3.55 | | (430) all_428_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | SIMP: (430) implies: % 18.75/3.55 | | (431) all_428_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (414), (415) imply: % 18.75/3.55 | | (432) all_468_0 = all_464_0 % 18.75/3.55 | | % 18.75/3.55 | | SIMP: (432) implies: % 18.75/3.55 | | (433) all_468_0 = all_464_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (412), (433) imply: % 18.75/3.55 | | (434) all_464_0 = all_35_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (413), (433) imply: % 18.75/3.55 | | (435) all_464_0 = all_432_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (434), (435) imply: % 18.75/3.55 | | (436) all_432_0 = all_35_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (424), (431) imply: % 18.75/3.55 | | (437) all_358_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | SIMP: (437) implies: % 18.75/3.55 | | (438) all_358_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (423), (438) imply: % 18.75/3.55 | | (439) all_356_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | SIMP: (439) implies: % 18.75/3.55 | | (440) all_356_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (422), (440) imply: % 18.75/3.55 | | (441) all_320_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | SIMP: (441) implies: % 18.75/3.55 | | (442) all_320_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (420), (421) imply: % 18.75/3.55 | | (443) all_298_0 = all_216_0 % 18.75/3.55 | | % 18.75/3.55 | | SIMP: (443) implies: % 18.75/3.55 | | (444) all_298_0 = all_216_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (419), (442) imply: % 18.75/3.55 | | (445) all_292_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | SIMP: (445) implies: % 18.75/3.55 | | (446) all_292_0 = all_234_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (418), (444) imply: % 18.75/3.55 | | (447) all_292_0 = all_216_0 % 18.75/3.55 | | % 18.75/3.55 | | SIMP: (447) implies: % 18.75/3.55 | | (448) all_292_0 = all_216_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (417), (446) imply: % 18.75/3.55 | | (449) all_234_0 = all_37_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (446), (448) imply: % 18.75/3.55 | | (450) all_234_0 = all_216_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (449), (450) imply: % 18.75/3.55 | | (451) all_216_0 = all_37_0 % 18.75/3.55 | | % 18.75/3.55 | | REDUCE: (392), (427) imply: % 18.75/3.55 | | (452) times(all_76_0, all_5_2) = all_64_0 % 18.75/3.55 | | % 18.75/3.55 | | REDUCE: (375), (451) imply: % 18.75/3.55 | | (453) times(all_37_0, all_37_0) = all_139_0 % 18.75/3.55 | | % 18.75/3.55 | | REDUCE: (403), (412) imply: % 18.75/3.55 | | (454) times(all_5_3, all_35_0) = all_37_0 % 18.75/3.55 | | % 18.75/3.55 | | GROUND_INST: instantiating (3) with all_5_1, all_37_0, all_35_0, all_5_3, % 18.75/3.55 | | simplifying with (178), (454) gives: % 18.75/3.55 | | (455) all_37_0 = all_5_1 % 18.75/3.55 | | % 18.75/3.55 | | GROUND_INST: instantiating (3) with all_20_0, all_139_0, all_37_0, all_37_0, % 18.75/3.55 | | simplifying with (348), (453) gives: % 18.75/3.55 | | (456) all_139_0 = all_20_0 % 18.75/3.55 | | % 18.75/3.55 | | GROUND_INST: instantiating (3) with all_139_0, all_64_0, all_5_2, all_76_0, % 18.75/3.55 | | simplifying with (249), (452) gives: % 18.75/3.55 | | (457) all_139_0 = all_64_0 % 18.75/3.55 | | % 18.75/3.55 | | COMBINE_EQS: (456), (457) imply: % 18.75/3.55 | | (458) all_64_0 = all_20_0 % 18.75/3.55 | | % 18.75/3.55 | | REDUCE: (352), (455), (458) imply: % 18.75/3.55 | | (459) times(all_5_1, all_20_0) = all_5_1 % 18.75/3.55 | | % 18.75/3.55 | | PRED_UNIFY: (28), (459) imply: % 18.75/3.55 | | (460) $false % 18.75/3.55 | | % 18.75/3.55 | | CLOSE: (460) is inconsistent. % 18.75/3.55 | | % 18.75/3.55 | End of split % 18.75/3.55 | % 18.75/3.56 End of proof % 18.75/3.56 % SZS output end Proof for theBenchmark % 18.75/3.56 % 18.75/3.56 2995ms %------------------------------------------------------------------------------