Princess---230619.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Princess---230619
% Problem  : SWC009+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm  : none
% Format   : tptp
% Command  : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s

% Computer : n029.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 20:49:09 EDT 2023

% Result   : Theorem 53.25s 7.52s
% Output   : Proof 106.89s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12  % Problem  : SWC009+1 : TPTP v8.1.2. Released v2.4.0.
% 0.10/0.12  % Command  : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s
% 0.12/0.34  % Computer : n029.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Mon Aug 28 16:43:11 EDT 2023
% 0.12/0.34  % CPUTime  : 
% 0.66/0.63  ________       _____
% 0.66/0.63  ___  __ \_________(_)________________________________
% 0.66/0.63  __  /_/ /_  ___/_  /__  __ \  ___/  _ \_  ___/_  ___/
% 0.66/0.63  _  ____/_  /   _  / _  / / / /__ /  __/(__  )_(__  )
% 0.66/0.63  /_/     /_/    /_/  /_/ /_/\___/ \___//____/ /____/
% 0.66/0.63  
% 0.66/0.63  A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic
% 0.66/0.63  (2023-06-19)
% 0.66/0.63  
% 0.66/0.63  (c) Philipp Rümmer, 2009-2023
% 0.66/0.63  Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen,
% 0.66/0.63                Amanda Stjerna.
% 0.66/0.63  Free software under BSD-3-Clause.
% 0.66/0.63  
% 0.66/0.63  For more information, visit http://www.philipp.ruemmer.org/princess.shtml
% 0.66/0.63  
% 0.66/0.63  Loading /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.66/0.64  Running up to 7 provers in parallel.
% 0.66/0.65  Prover 2: Options:  +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994
% 0.66/0.65  Prover 1: Options:  +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423
% 0.66/0.65  Prover 0: Options:  +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893
% 0.66/0.65  Prover 3: Options:  +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996
% 0.66/0.65  Prover 4: Options:  +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696
% 0.66/0.65  Prover 5: Options:  +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288
% 0.66/0.65  Prover 6: Options:  -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365
% 6.43/1.54  Prover 4: Preprocessing ...
% 6.43/1.55  Prover 1: Preprocessing ...
% 6.43/1.58  Prover 2: Preprocessing ...
% 6.43/1.58  Prover 0: Preprocessing ...
% 6.43/1.58  Prover 3: Preprocessing ...
% 6.43/1.58  Prover 5: Preprocessing ...
% 6.43/1.58  Prover 6: Preprocessing ...
% 16.32/2.84  Prover 2: Proving ...
% 16.32/2.90  Prover 1: Constructing countermodel ...
% 17.03/2.91  Prover 5: Constructing countermodel ...
% 17.03/2.93  Prover 6: Proving ...
% 17.03/2.95  Prover 3: Constructing countermodel ...
% 23.99/3.81  Prover 4: Constructing countermodel ...
% 24.58/3.91  Prover 0: Proving ...
% 53.25/7.52  Prover 5: proved (6866ms)
% 53.25/7.52  
% 53.25/7.52  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 53.25/7.52  
% 53.25/7.52  Prover 2: stopped
% 53.25/7.53  Prover 3: stopped
% 53.25/7.53  Prover 6: stopped
% 53.25/7.54  Prover 7: Options:  +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470
% 53.25/7.54  Prover 0: stopped
% 53.25/7.55  Prover 8: Options:  +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089
% 53.25/7.55  Prover 10: Options:  +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125
% 53.25/7.55  Prover 11: Options:  +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984
% 53.25/7.56  Prover 13: Options:  +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443
% 55.07/7.78  Prover 7: Preprocessing ...
% 56.13/7.88  Prover 8: Preprocessing ...
% 56.13/7.89  Prover 10: Preprocessing ...
% 56.13/7.91  Prover 13: Preprocessing ...
% 56.13/7.93  Prover 11: Preprocessing ...
% 56.13/7.93  Prover 7: Constructing countermodel ...
% 57.35/8.06  Prover 10: Constructing countermodel ...
% 58.44/8.20  Prover 13: Constructing countermodel ...
% 58.44/8.24  Prover 8: Warning: ignoring some quantifiers
% 58.44/8.25  Prover 8: Constructing countermodel ...
% 63.41/8.85  Prover 11: Constructing countermodel ...
% 88.83/12.10  Prover 13: stopped
% 88.83/12.11  Prover 16: Options:  +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683
% 90.23/12.24  Prover 16: Preprocessing ...
% 91.21/12.33  Prover 16: Constructing countermodel ...
% 105.87/14.19  Prover 10: Found proof (size 350)
% 105.87/14.19  Prover 10: proved (6647ms)
% 105.87/14.19  Prover 16: stopped
% 105.87/14.19  Prover 7: stopped
% 105.87/14.19  Prover 8: stopped
% 105.87/14.19  Prover 1: stopped
% 105.87/14.19  Prover 11: stopped
% 105.87/14.20  Prover 4: stopped
% 105.87/14.20  
% 105.87/14.20  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 105.87/14.20  
% 106.22/14.28  % SZS output start Proof for theBenchmark
% 106.27/14.28  Assumptions after simplification:
% 106.27/14.28  ---------------------------------
% 106.27/14.28  
% 106.27/14.28    (ax1)
% 106.27/14.29     ! [v0: $i] :  ! [v1: $i] : (v1 = v0 |  ~ $i(v1) |  ~ $i(v0) |  ~ ssItem(v1) |
% 106.27/14.29       ~ ssItem(v0) | neq(v0, v1)) &  ! [v0: $i] : ( ~ $i(v0) |  ~ neq(v0, v0) | 
% 106.27/14.29      ~ ssItem(v0))
% 106.27/14.29  
% 106.27/14.29    (ax15)
% 106.27/14.29     ! [v0: $i] :  ! [v1: $i] : (v1 = v0 |  ~ $i(v1) |  ~ $i(v0) |  ~ ssList(v1) |
% 106.27/14.29       ~ ssList(v0) | neq(v0, v1)) &  ! [v0: $i] : ( ~ $i(v0) |  ~ ssList(v0) |  ~
% 106.27/14.29      neq(v0, v0))
% 106.27/14.29  
% 106.27/14.29    (ax17)
% 106.27/14.29    $i(nil) & ssList(nil)
% 106.27/14.29  
% 106.27/14.29    (ax2)
% 106.27/14.29     ? [v0: $i] :  ? [v1: $i] : ( ~ (v1 = v0) & $i(v1) & $i(v0) & ssItem(v1) &
% 106.27/14.29      ssItem(v0))
% 106.27/14.29  
% 106.27/14.29    (ax26)
% 106.27/14.31     ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] : ( ~ (app(v0, v1) = v2) |  ~ $i(v1) |
% 106.27/14.31       ~ $i(v0) |  ~ ssList(v1) |  ~ ssList(v0) | ssList(v2))
% 106.27/14.31  
% 106.27/14.31    (ax28)
% 106.27/14.31    $i(nil) &  ! [v0: $i] :  ! [v1: $i] : (v1 = v0 |  ~ (app(nil, v0) = v1) |  ~
% 106.27/14.32      $i(v0) |  ~ ssList(v0))
% 106.27/14.32  
% 106.27/14.32    (ax42)
% 106.27/14.32     ! [v0: $i] : ( ~ $i(v0) |  ~ ssList(v0) | frontsegP(v0, v0))
% 106.27/14.32  
% 106.27/14.32    (ax45)
% 106.27/14.32    $i(nil) &  ! [v0: $i] : ( ~ $i(v0) |  ~ ssList(v0) | frontsegP(v0, nil))
% 106.27/14.32  
% 106.27/14.32    (ax46)
% 106.42/14.32    $i(nil) &  ! [v0: $i] : (v0 = nil |  ~ $i(v0) |  ~ frontsegP(nil, v0) |  ~
% 106.42/14.32      ssList(v0)) & ( ~ ssList(nil) | frontsegP(nil, nil))
% 106.42/14.32  
% 106.42/14.32    (ax49)
% 106.42/14.32     ! [v0: $i] : ( ~ $i(v0) |  ~ ssList(v0) | rearsegP(v0, v0))
% 106.42/14.32  
% 106.42/14.32    (ax5)
% 106.42/14.32     ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] : ( ~ (app(v1, v2) = v0) |  ~ $i(v2) |
% 106.42/14.32       ~ $i(v1) |  ~ $i(v0) |  ~ ssList(v2) |  ~ ssList(v1) |  ~ ssList(v0) |
% 106.42/14.32      frontsegP(v0, v1)) &  ! [v0: $i] :  ! [v1: $i] : ( ~ $i(v1) |  ~ $i(v0) |  ~
% 106.42/14.32      frontsegP(v0, v1) |  ~ ssList(v1) |  ~ ssList(v0) |  ? [v2: $i] : (app(v1,
% 106.42/14.32          v2) = v0 & $i(v2) & ssList(v2)))
% 106.42/14.32  
% 106.42/14.32    (ax51)
% 106.42/14.32    $i(nil) &  ! [v0: $i] : ( ~ $i(v0) |  ~ ssList(v0) | rearsegP(v0, nil))
% 106.42/14.32  
% 106.42/14.32    (ax52)
% 106.42/14.32    $i(nil) &  ! [v0: $i] : (v0 = nil |  ~ $i(v0) |  ~ rearsegP(nil, v0) |  ~
% 106.42/14.32      ssList(v0)) & ( ~ ssList(nil) | rearsegP(nil, nil))
% 106.42/14.32  
% 106.42/14.32    (ax58)
% 106.42/14.32    $i(nil) &  ! [v0: $i] : (v0 = nil |  ~ $i(v0) |  ~ segmentP(nil, v0) |  ~
% 106.42/14.32      ssList(v0)) & ( ~ ssList(nil) | segmentP(nil, nil))
% 106.42/14.32  
% 106.42/14.32    (ax6)
% 106.42/14.32     ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] : ( ~ (app(v2, v1) = v0) |  ~ $i(v2) |
% 106.42/14.32       ~ $i(v1) |  ~ $i(v0) |  ~ ssList(v2) |  ~ ssList(v1) |  ~ ssList(v0) |
% 106.42/14.32      rearsegP(v0, v1)) &  ! [v0: $i] :  ! [v1: $i] : ( ~ $i(v1) |  ~ $i(v0) |  ~
% 106.42/14.32      rearsegP(v0, v1) |  ~ ssList(v1) |  ~ ssList(v0) |  ? [v2: $i] : (app(v2,
% 106.42/14.33          v1) = v0 & $i(v2) & ssList(v2)))
% 106.42/14.33  
% 106.42/14.33    (ax7)
% 106.42/14.33     ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] :  ! [v3: $i] :  ! [v4: $i] : ( ~
% 106.42/14.33      (app(v3, v4) = v0) |  ~ (app(v2, v1) = v3) |  ~ $i(v4) |  ~ $i(v2) |  ~
% 106.42/14.33      $i(v1) |  ~ $i(v0) |  ~ ssList(v4) |  ~ ssList(v2) |  ~ ssList(v1) |  ~
% 106.42/14.33      ssList(v0) | segmentP(v0, v1)) &  ! [v0: $i] :  ! [v1: $i] : ( ~ $i(v1) |  ~
% 106.42/14.33      $i(v0) |  ~ segmentP(v0, v1) |  ~ ssList(v1) |  ~ ssList(v0) |  ? [v2: $i] :
% 106.42/14.33       ? [v3: $i] :  ? [v4: $i] : (app(v3, v4) = v0 & app(v2, v1) = v3 & $i(v4) &
% 106.42/14.33        $i(v3) & $i(v2) & ssList(v4) & ssList(v2)))
% 106.42/14.33  
% 106.42/14.33    (ax79)
% 106.42/14.33     ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] :  ! [v3: $i] : (v3 = v0 |  ~ (app(v3,
% 106.42/14.33          v1) = v2) |  ~ (app(v0, v1) = v2) |  ~ $i(v3) |  ~ $i(v1) |  ~ $i(v0) | 
% 106.42/14.33      ~ ssList(v3) |  ~ ssList(v1) |  ~ ssList(v0))
% 106.42/14.33  
% 106.42/14.33    (ax80)
% 106.42/14.33     ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] :  ! [v3: $i] : (v3 = v0 |  ~ (app(v1,
% 106.42/14.33          v3) = v2) |  ~ (app(v1, v0) = v2) |  ~ $i(v3) |  ~ $i(v1) |  ~ $i(v0) | 
% 106.42/14.33      ~ ssList(v3) |  ~ ssList(v1) |  ~ ssList(v0))
% 106.42/14.33  
% 106.42/14.33    (ax82)
% 106.50/14.33     ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] :  ! [v3: $i] :  ! [v4: $i] : ( ~
% 106.50/14.33      (app(v2, v3) = v4) |  ~ (app(v0, v1) = v2) |  ~ $i(v3) |  ~ $i(v1) |  ~
% 106.50/14.33      $i(v0) |  ~ ssList(v3) |  ~ ssList(v1) |  ~ ssList(v0) |  ? [v5: $i] :
% 106.50/14.33      (app(v1, v3) = v5 & app(v0, v5) = v4 & $i(v5) & $i(v4)))
% 106.50/14.33  
% 106.50/14.33    (ax83)
% 106.50/14.34    $i(nil) &  ! [v0: $i] :  ! [v1: $i] : (v1 = nil |  ~ (app(v0, v1) = nil) |  ~
% 106.50/14.34      $i(v1) |  ~ $i(v0) |  ~ ssList(v1) |  ~ ssList(v0)) &  ! [v0: $i] :  ! [v1:
% 106.50/14.34      $i] : (v0 = nil |  ~ (app(v0, v1) = nil) |  ~ $i(v1) |  ~ $i(v0) |  ~
% 106.50/14.34      ssList(v1) |  ~ ssList(v0)) &  ! [v0: $i] : (v0 = nil |  ~ (app(nil, nil) =
% 106.50/14.34        v0) |  ~ ssList(nil))
% 106.50/14.34  
% 106.50/14.34    (ax84)
% 106.50/14.34    $i(nil) &  ! [v0: $i] :  ! [v1: $i] : (v1 = v0 |  ~ (app(v0, nil) = v1) |  ~
% 106.50/14.34      $i(v0) |  ~ ssList(v0))
% 106.50/14.34  
% 106.50/14.34    (co1)
% 106.50/14.34    $i(nil) &  ? [v0: $i] :  ? [v1: $i] :  ? [v2: $i] : (app(v0, v2) = v1 & $i(v2)
% 106.50/14.34      & $i(v1) & $i(v0) & strictorderedP(v0) & ssList(v2) & ssList(v1) &
% 106.50/14.34      ssList(v0) &  ! [v3: $i] :  ! [v4: $i] :  ! [v5: $i] :  ! [v6: $i] :  ! [v7:
% 106.50/14.34        $i] :  ! [v8: $i] : ( ~ (cons(v6, nil) = v7) |  ~ (cons(v3, nil) = v4) | 
% 106.50/14.34        ~ (app(v8, v7) = v0) |  ~ (app(v4, v5) = v2) |  ~ $i(v8) |  ~ $i(v6) |  ~
% 106.50/14.34        $i(v5) |  ~ $i(v3) |  ~ lt(v6, v3) |  ~ ssList(v8) |  ~ ssList(v5) |  ~
% 106.50/14.34        ssItem(v6) |  ~ ssItem(v3)) &  ! [v3: $i] :  ! [v4: $i] :  ! [v5: $i] :  !
% 106.50/14.34      [v6: $i] : ( ~ (app(v5, v6) = v1) |  ~ (app(v3, v4) = v5) |  ~ $i(v6) |  ~
% 106.50/14.34        $i(v4) |  ~ $i(v3) |  ~ ssList(v6) |  ~ ssList(v4) |  ~ ssList(v3) |  ?
% 106.50/14.34        [v7: $i] : ( ~ (v7 = v0) & app(v3, v6) = v7 & $i(v7))) & ( ~ (v0 = nil) |
% 106.50/14.34        v1 = nil))
% 106.50/14.34  
% 106.50/14.34    (function-axioms)
% 106.50/14.34     ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] :  ! [v3: $i] : (v1 = v0 |  ~
% 106.50/14.34      (cons(v3, v2) = v1) |  ~ (cons(v3, v2) = v0)) &  ! [v0: $i] :  ! [v1: $i] : 
% 106.50/14.34    ! [v2: $i] :  ! [v3: $i] : (v1 = v0 |  ~ (app(v3, v2) = v1) |  ~ (app(v3, v2)
% 106.50/14.34        = v0)) &  ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] : (v1 = v0 |  ~ (tl(v2) =
% 106.50/14.34        v1) |  ~ (tl(v2) = v0)) &  ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] : (v1 =
% 106.50/14.34      v0 |  ~ (hd(v2) = v1) |  ~ (hd(v2) = v0))
% 106.50/14.34  
% 106.50/14.34  Further assumptions not needed in the proof:
% 106.50/14.34  --------------------------------------------
% 106.50/14.34  ax10, ax11, ax12, ax13, ax14, ax16, ax18, ax19, ax20, ax21, ax22, ax23, ax24,
% 106.50/14.34  ax25, ax27, ax29, ax3, ax30, ax31, ax32, ax33, ax34, ax35, ax36, ax37, ax38,
% 106.50/14.34  ax39, ax4, ax40, ax41, ax43, ax44, ax47, ax48, ax50, ax53, ax54, ax55, ax56,
% 106.50/14.34  ax57, ax59, ax60, ax61, ax62, ax63, ax64, ax65, ax66, ax67, ax68, ax69, ax70,
% 106.50/14.34  ax71, ax72, ax73, ax74, ax75, ax76, ax77, ax78, ax8, ax81, ax85, ax86, ax87,
% 106.50/14.34  ax88, ax89, ax9, ax90, ax91, ax92, ax93, ax94, ax95
% 106.50/14.34  
% 106.50/14.34  Those formulas are unsatisfiable:
% 106.50/14.34  ---------------------------------
% 106.50/14.34  
% 106.50/14.34  Begin of proof
% 106.50/14.34  | 
% 106.50/14.34  | ALPHA: (ax1) implies:
% 106.50/14.35  |   (1)   ! [v0: $i] :  ! [v1: $i] : (v1 = v0 |  ~ $i(v1) |  ~ $i(v0) |  ~
% 106.50/14.35  |          ssItem(v1) |  ~ ssItem(v0) | neq(v0, v1))
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax5) implies:
% 106.50/14.35  |   (2)   ! [v0: $i] :  ! [v1: $i] : ( ~ $i(v1) |  ~ $i(v0) |  ~ frontsegP(v0,
% 106.50/14.35  |            v1) |  ~ ssList(v1) |  ~ ssList(v0) |  ? [v2: $i] : (app(v1, v2) =
% 106.50/14.35  |            v0 & $i(v2) & ssList(v2)))
% 106.50/14.35  |   (3)   ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] : ( ~ (app(v1, v2) = v0) |  ~
% 106.50/14.35  |          $i(v2) |  ~ $i(v1) |  ~ $i(v0) |  ~ ssList(v2) |  ~ ssList(v1) |  ~
% 106.50/14.35  |          ssList(v0) | frontsegP(v0, v1))
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax6) implies:
% 106.50/14.35  |   (4)   ! [v0: $i] :  ! [v1: $i] : ( ~ $i(v1) |  ~ $i(v0) |  ~ rearsegP(v0,
% 106.50/14.35  |            v1) |  ~ ssList(v1) |  ~ ssList(v0) |  ? [v2: $i] : (app(v2, v1) =
% 106.50/14.35  |            v0 & $i(v2) & ssList(v2)))
% 106.50/14.35  |   (5)   ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] : ( ~ (app(v2, v1) = v0) |  ~
% 106.50/14.35  |          $i(v2) |  ~ $i(v1) |  ~ $i(v0) |  ~ ssList(v2) |  ~ ssList(v1) |  ~
% 106.50/14.35  |          ssList(v0) | rearsegP(v0, v1))
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax7) implies:
% 106.50/14.35  |   (6)   ! [v0: $i] :  ! [v1: $i] : ( ~ $i(v1) |  ~ $i(v0) |  ~ segmentP(v0,
% 106.50/14.35  |            v1) |  ~ ssList(v1) |  ~ ssList(v0) |  ? [v2: $i] :  ? [v3: $i] : 
% 106.50/14.35  |          ? [v4: $i] : (app(v3, v4) = v0 & app(v2, v1) = v3 & $i(v4) & $i(v3) &
% 106.50/14.35  |            $i(v2) & ssList(v4) & ssList(v2)))
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax15) implies:
% 106.50/14.35  |   (7)   ! [v0: $i] :  ! [v1: $i] : (v1 = v0 |  ~ $i(v1) |  ~ $i(v0) |  ~
% 106.50/14.35  |          ssList(v1) |  ~ ssList(v0) | neq(v0, v1))
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax17) implies:
% 106.50/14.35  |   (8)  ssList(nil)
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax28) implies:
% 106.50/14.35  |   (9)   ! [v0: $i] :  ! [v1: $i] : (v1 = v0 |  ~ (app(nil, v0) = v1) |  ~
% 106.50/14.35  |          $i(v0) |  ~ ssList(v0))
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax45) implies:
% 106.50/14.35  |   (10)   ! [v0: $i] : ( ~ $i(v0) |  ~ ssList(v0) | frontsegP(v0, nil))
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax46) implies:
% 106.50/14.35  |   (11)   ~ ssList(nil) | frontsegP(nil, nil)
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax51) implies:
% 106.50/14.35  |   (12)   ! [v0: $i] : ( ~ $i(v0) |  ~ ssList(v0) | rearsegP(v0, nil))
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax52) implies:
% 106.50/14.35  |   (13)   ~ ssList(nil) | rearsegP(nil, nil)
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax58) implies:
% 106.50/14.35  |   (14)   ~ ssList(nil) | segmentP(nil, nil)
% 106.50/14.35  | 
% 106.50/14.35  | ALPHA: (ax83) implies:
% 106.50/14.35  |   (15)   ! [v0: $i] : (v0 = nil |  ~ (app(nil, nil) = v0) |  ~ ssList(nil))
% 106.50/14.35  |   (16)   ! [v0: $i] :  ! [v1: $i] : (v0 = nil |  ~ (app(v0, v1) = nil) |  ~
% 106.50/14.35  |           $i(v1) |  ~ $i(v0) |  ~ ssList(v1) |  ~ ssList(v0))
% 106.50/14.36  |   (17)   ! [v0: $i] :  ! [v1: $i] : (v1 = nil |  ~ (app(v0, v1) = nil) |  ~
% 106.50/14.36  |           $i(v1) |  ~ $i(v0) |  ~ ssList(v1) |  ~ ssList(v0))
% 106.50/14.36  | 
% 106.50/14.36  | ALPHA: (ax84) implies:
% 106.50/14.36  |   (18)   ! [v0: $i] :  ! [v1: $i] : (v1 = v0 |  ~ (app(v0, nil) = v1) |  ~
% 106.50/14.36  |           $i(v0) |  ~ ssList(v0))
% 106.50/14.36  | 
% 106.50/14.36  | ALPHA: (co1) implies:
% 106.50/14.36  |   (19)  $i(nil)
% 106.50/14.36  |   (20)   ? [v0: $i] :  ? [v1: $i] :  ? [v2: $i] : (app(v0, v2) = v1 & $i(v2) &
% 106.50/14.36  |           $i(v1) & $i(v0) & strictorderedP(v0) & ssList(v2) & ssList(v1) &
% 106.50/14.36  |           ssList(v0) &  ! [v3: $i] :  ! [v4: $i] :  ! [v5: $i] :  ! [v6: $i] :
% 106.50/14.36  |            ! [v7: $i] :  ! [v8: $i] : ( ~ (cons(v6, nil) = v7) |  ~ (cons(v3,
% 106.50/14.36  |                 nil) = v4) |  ~ (app(v8, v7) = v0) |  ~ (app(v4, v5) = v2) | 
% 106.50/14.36  |             ~ $i(v8) |  ~ $i(v6) |  ~ $i(v5) |  ~ $i(v3) |  ~ lt(v6, v3) |  ~
% 106.50/14.36  |             ssList(v8) |  ~ ssList(v5) |  ~ ssItem(v6) |  ~ ssItem(v3)) &  !
% 106.50/14.36  |           [v3: $i] :  ! [v4: $i] :  ! [v5: $i] :  ! [v6: $i] : ( ~ (app(v5,
% 106.50/14.36  |                 v6) = v1) |  ~ (app(v3, v4) = v5) |  ~ $i(v6) |  ~ $i(v4) |  ~
% 106.50/14.36  |             $i(v3) |  ~ ssList(v6) |  ~ ssList(v4) |  ~ ssList(v3) |  ? [v7:
% 106.50/14.36  |               $i] : ( ~ (v7 = v0) & app(v3, v6) = v7 & $i(v7))) & ( ~ (v0 =
% 106.50/14.36  |               nil) | v1 = nil))
% 106.50/14.36  | 
% 106.50/14.36  | ALPHA: (function-axioms) implies:
% 106.50/14.36  |   (21)   ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] :  ! [v3: $i] : (v1 = v0 |  ~
% 106.50/14.36  |           (app(v3, v2) = v1) |  ~ (app(v3, v2) = v0))
% 106.50/14.36  | 
% 106.50/14.36  | DELTA: instantiating (ax2) with fresh symbols all_89_0, all_89_1 gives:
% 106.50/14.36  |   (22)   ~ (all_89_0 = all_89_1) & $i(all_89_0) & $i(all_89_1) &
% 106.50/14.36  |         ssItem(all_89_0) & ssItem(all_89_1)
% 106.50/14.36  | 
% 106.50/14.36  | ALPHA: (22) implies:
% 106.50/14.36  |   (23)   ~ (all_89_0 = all_89_1)
% 106.50/14.36  |   (24)  ssItem(all_89_1)
% 106.50/14.36  |   (25)  ssItem(all_89_0)
% 106.50/14.36  |   (26)  $i(all_89_1)
% 106.50/14.36  |   (27)  $i(all_89_0)
% 106.50/14.36  | 
% 106.50/14.36  | DELTA: instantiating (20) with fresh symbols all_91_0, all_91_1, all_91_2
% 106.50/14.36  |        gives:
% 106.50/14.36  |   (28)  app(all_91_2, all_91_0) = all_91_1 & $i(all_91_0) & $i(all_91_1) &
% 106.50/14.36  |         $i(all_91_2) & strictorderedP(all_91_2) & ssList(all_91_0) &
% 106.50/14.36  |         ssList(all_91_1) & ssList(all_91_2) &  ! [v0: $i] :  ! [v1: $i] :  !
% 106.50/14.36  |         [v2: $i] :  ! [v3: $i] :  ! [v4: $i] :  ! [v5: $i] : ( ~ (cons(v3,
% 106.50/14.36  |               nil) = v4) |  ~ (cons(v0, nil) = v1) |  ~ (app(v5, v4) =
% 106.50/14.36  |             all_91_2) |  ~ (app(v1, v2) = all_91_0) |  ~ $i(v5) |  ~ $i(v3) | 
% 106.50/14.36  |           ~ $i(v2) |  ~ $i(v0) |  ~ lt(v3, v0) |  ~ ssList(v5) |  ~ ssList(v2)
% 106.50/14.36  |           |  ~ ssItem(v3) |  ~ ssItem(v0)) &  ! [v0: $i] :  ! [v1: $i] :  !
% 106.50/14.36  |         [v2: $i] :  ! [v3: $i] : ( ~ (app(v2, v3) = all_91_1) |  ~ (app(v0,
% 106.50/14.36  |               v1) = v2) |  ~ $i(v3) |  ~ $i(v1) |  ~ $i(v0) |  ~ ssList(v3) | 
% 106.50/14.36  |           ~ ssList(v1) |  ~ ssList(v0) |  ? [v4: any] : ( ~ (v4 = all_91_2) &
% 106.50/14.36  |             app(v0, v3) = v4 & $i(v4))) & ( ~ (all_91_2 = nil) | all_91_1 =
% 106.50/14.37  |           nil)
% 106.50/14.37  | 
% 106.50/14.37  | ALPHA: (28) implies:
% 106.50/14.37  |   (29)  ssList(all_91_2)
% 106.50/14.37  |   (30)  ssList(all_91_1)
% 106.50/14.37  |   (31)  ssList(all_91_0)
% 106.50/14.37  |   (32)  $i(all_91_2)
% 106.50/14.37  |   (33)  $i(all_91_1)
% 106.50/14.37  |   (34)  $i(all_91_0)
% 106.50/14.37  |   (35)  app(all_91_2, all_91_0) = all_91_1
% 106.50/14.37  |   (36)   ! [v0: $i] :  ! [v1: $i] :  ! [v2: $i] :  ! [v3: $i] : ( ~ (app(v2,
% 106.50/14.37  |               v3) = all_91_1) |  ~ (app(v0, v1) = v2) |  ~ $i(v3) |  ~ $i(v1)
% 106.50/14.37  |           |  ~ $i(v0) |  ~ ssList(v3) |  ~ ssList(v1) |  ~ ssList(v0) |  ?
% 106.50/14.37  |           [v4: any] : ( ~ (v4 = all_91_2) & app(v0, v3) = v4 & $i(v4)))
% 106.50/14.37  | 
% 106.50/14.37  | BETA: splitting (13) gives:
% 106.50/14.37  | 
% 106.50/14.37  | Case 1:
% 106.50/14.37  | | 
% 106.50/14.37  | |   (37)   ~ ssList(nil)
% 106.50/14.37  | | 
% 106.50/14.37  | | PRED_UNIFY: (8), (37) imply:
% 106.50/14.37  | |   (38)  $false
% 106.50/14.37  | | 
% 106.50/14.37  | | CLOSE: (38) is inconsistent.
% 106.50/14.37  | | 
% 106.50/14.37  | Case 2:
% 106.50/14.37  | | 
% 106.50/14.37  | |   (39)  rearsegP(nil, nil)
% 106.50/14.37  | | 
% 106.50/14.37  | | BETA: splitting (11) gives:
% 106.50/14.37  | | 
% 106.50/14.37  | | Case 1:
% 106.50/14.37  | | | 
% 106.50/14.37  | | |   (40)   ~ ssList(nil)
% 106.50/14.37  | | | 
% 106.50/14.37  | | | PRED_UNIFY: (8), (40) imply:
% 106.50/14.37  | | |   (41)  $false
% 106.50/14.37  | | | 
% 106.50/14.37  | | | CLOSE: (41) is inconsistent.
% 106.50/14.37  | | | 
% 106.50/14.37  | | Case 2:
% 106.50/14.37  | | | 
% 106.50/14.37  | | |   (42)  frontsegP(nil, nil)
% 106.50/14.37  | | | 
% 106.50/14.37  | | | BETA: splitting (14) gives:
% 106.50/14.37  | | | 
% 106.50/14.37  | | | Case 1:
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | |   (43)   ~ ssList(nil)
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | PRED_UNIFY: (8), (43) imply:
% 106.50/14.37  | | | |   (44)  $false
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | CLOSE: (44) is inconsistent.
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | Case 2:
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | |   (45)  segmentP(nil, nil)
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | GROUND_INST: instantiating (1) with all_89_0, all_89_1, simplifying with
% 106.50/14.37  | | | |              (24), (25), (26), (27) gives:
% 106.50/14.37  | | | |   (46)  all_89_0 = all_89_1 | neq(all_89_0, all_89_1)
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | GROUND_INST: instantiating (ax49) with all_91_2, simplifying with (29),
% 106.50/14.37  | | | |              (32) gives:
% 106.50/14.37  | | | |   (47)  rearsegP(all_91_2, all_91_2)
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | GROUND_INST: instantiating (12) with all_91_2, simplifying with (29),
% 106.50/14.37  | | | |              (32) gives:
% 106.50/14.37  | | | |   (48)  rearsegP(all_91_2, nil)
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | GROUND_INST: instantiating (ax42) with all_91_2, simplifying with (29),
% 106.50/14.37  | | | |              (32) gives:
% 106.50/14.37  | | | |   (49)  frontsegP(all_91_2, all_91_2)
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | GROUND_INST: instantiating (10) with all_91_2, simplifying with (29),
% 106.50/14.37  | | | |              (32) gives:
% 106.50/14.37  | | | |   (50)  frontsegP(all_91_2, nil)
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | GROUND_INST: instantiating (12) with all_91_1, simplifying with (30),
% 106.50/14.37  | | | |              (33) gives:
% 106.50/14.37  | | | |   (51)  rearsegP(all_91_1, nil)
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | GROUND_INST: instantiating (ax42) with all_91_1, simplifying with (30),
% 106.50/14.37  | | | |              (33) gives:
% 106.50/14.37  | | | |   (52)  frontsegP(all_91_1, all_91_1)
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | GROUND_INST: instantiating (10) with all_91_1, simplifying with (30),
% 106.50/14.37  | | | |              (33) gives:
% 106.50/14.37  | | | |   (53)  frontsegP(all_91_1, nil)
% 106.50/14.37  | | | | 
% 106.50/14.37  | | | | GROUND_INST: instantiating (10) with all_91_0, simplifying with (31),
% 106.50/14.37  | | | |              (34) gives:
% 106.50/14.37  | | | |   (54)  frontsegP(all_91_0, nil)
% 106.50/14.37  | | | | 
% 106.50/14.38  | | | | GROUND_INST: instantiating (2) with nil, nil, simplifying with (8),
% 106.50/14.38  | | | |              (19), (42) gives:
% 106.50/14.38  | | | |   (55)   ? [v0: $i] : (app(nil, v0) = nil & $i(v0) & ssList(v0))
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | GROUND_INST: instantiating (4) with nil, nil, simplifying with (8),
% 106.50/14.38  | | | |              (19), (39) gives:
% 106.50/14.38  | | | |   (56)   ? [v0: $i] : (app(v0, nil) = nil & $i(v0) & ssList(v0))
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | GROUND_INST: instantiating (6) with nil, nil, simplifying with (8),
% 106.50/14.38  | | | |              (19), (45) gives:
% 106.50/14.38  | | | |   (57)   ? [v0: $i] :  ? [v1: $i] :  ? [v2: $i] : (app(v1, v2) = nil &
% 106.50/14.38  | | | |           app(v0, nil) = v1 & $i(v2) & $i(v1) & $i(v0) & ssList(v2) &
% 106.50/14.38  | | | |           ssList(v0))
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | GROUND_INST: instantiating (3) with all_91_1, all_91_2, all_91_0,
% 106.50/14.38  | | | |              simplifying with (29), (30), (31), (32), (33), (34), (35)
% 106.50/14.38  | | | |              gives:
% 106.50/14.38  | | | |   (58)  frontsegP(all_91_1, all_91_2)
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | GROUND_INST: instantiating (5) with all_91_1, all_91_0, all_91_2,
% 106.50/14.38  | | | |              simplifying with (29), (30), (31), (32), (33), (34), (35)
% 106.50/14.38  | | | |              gives:
% 106.50/14.38  | | | |   (59)  rearsegP(all_91_1, all_91_0)
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | DELTA: instantiating (56) with fresh symbol all_112_0 gives:
% 106.50/14.38  | | | |   (60)  app(all_112_0, nil) = nil & $i(all_112_0) & ssList(all_112_0)
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | ALPHA: (60) implies:
% 106.50/14.38  | | | |   (61)  ssList(all_112_0)
% 106.50/14.38  | | | |   (62)  $i(all_112_0)
% 106.50/14.38  | | | |   (63)  app(all_112_0, nil) = nil
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | DELTA: instantiating (55) with fresh symbol all_114_0 gives:
% 106.50/14.38  | | | |   (64)  app(nil, all_114_0) = nil & $i(all_114_0) & ssList(all_114_0)
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | ALPHA: (64) implies:
% 106.50/14.38  | | | |   (65)  ssList(all_114_0)
% 106.50/14.38  | | | |   (66)  $i(all_114_0)
% 106.50/14.38  | | | |   (67)  app(nil, all_114_0) = nil
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | DELTA: instantiating (57) with fresh symbols all_116_0, all_116_1,
% 106.50/14.38  | | | |        all_116_2 gives:
% 106.50/14.38  | | | |   (68)  app(all_116_1, all_116_0) = nil & app(all_116_2, nil) =
% 106.50/14.38  | | | |         all_116_1 & $i(all_116_0) & $i(all_116_1) & $i(all_116_2) &
% 106.50/14.38  | | | |         ssList(all_116_0) & ssList(all_116_2)
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | ALPHA: (68) implies:
% 106.50/14.38  | | | |   (69)  ssList(all_116_2)
% 106.50/14.38  | | | |   (70)  ssList(all_116_0)
% 106.50/14.38  | | | |   (71)  $i(all_116_2)
% 106.50/14.38  | | | |   (72)  $i(all_116_1)
% 106.50/14.38  | | | |   (73)  $i(all_116_0)
% 106.50/14.38  | | | |   (74)  app(all_116_2, nil) = all_116_1
% 106.50/14.38  | | | |   (75)  app(all_116_1, all_116_0) = nil
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | BETA: splitting (46) gives:
% 106.50/14.38  | | | | 
% 106.50/14.38  | | | | Case 1:
% 106.50/14.38  | | | | | 
% 106.50/14.38  | | | | | 
% 106.50/14.38  | | | | | GROUND_INST: instantiating (2) with all_91_2, nil, simplifying with
% 106.50/14.38  | | | | |              (8), (19), (29), (32), (50) gives:
% 106.50/14.38  | | | | |   (76)   ? [v0: $i] : (app(nil, v0) = all_91_2 & $i(v0) & ssList(v0))
% 106.50/14.38  | | | | | 
% 106.50/14.38  | | | | | GROUND_INST: instantiating (2) with all_91_2, all_91_2, simplifying
% 106.50/14.38  | | | | |              with (29), (32), (49) gives:
% 106.50/14.38  | | | | |   (77)   ? [v0: $i] : (app(all_91_2, v0) = all_91_2 & $i(v0) &
% 106.50/14.38  | | | | |           ssList(v0))
% 106.50/14.38  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (2) with all_91_1, nil, simplifying with
% 106.50/14.39  | | | | |              (8), (19), (30), (33), (53) gives:
% 106.50/14.39  | | | | |   (78)   ? [v0: $i] : (app(nil, v0) = all_91_1 & $i(v0) & ssList(v0))
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (2) with all_91_1, all_91_2, simplifying
% 106.50/14.39  | | | | |              with (29), (30), (32), (33), (58) gives:
% 106.50/14.39  | | | | |   (79)   ? [v0: $i] : (app(all_91_2, v0) = all_91_1 & $i(v0) &
% 106.50/14.39  | | | | |           ssList(v0))
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (2) with all_91_1, all_91_1, simplifying
% 106.50/14.39  | | | | |              with (30), (33), (52) gives:
% 106.50/14.39  | | | | |   (80)   ? [v0: $i] : (app(all_91_1, v0) = all_91_1 & $i(v0) &
% 106.50/14.39  | | | | |           ssList(v0))
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (2) with all_91_0, nil, simplifying with
% 106.50/14.39  | | | | |              (8), (19), (31), (34), (54) gives:
% 106.50/14.39  | | | | |   (81)   ? [v0: $i] : (app(nil, v0) = all_91_0 & $i(v0) & ssList(v0))
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (4) with all_91_2, nil, simplifying with
% 106.50/14.39  | | | | |              (8), (19), (29), (32), (48) gives:
% 106.50/14.39  | | | | |   (82)   ? [v0: $i] : (app(v0, nil) = all_91_2 & $i(v0) & ssList(v0))
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (4) with all_91_2, all_91_2, simplifying
% 106.50/14.39  | | | | |              with (29), (32), (47) gives:
% 106.50/14.39  | | | | |   (83)   ? [v0: $i] : (app(v0, all_91_2) = all_91_2 & $i(v0) &
% 106.50/14.39  | | | | |           ssList(v0))
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (4) with all_91_1, nil, simplifying with
% 106.50/14.39  | | | | |              (8), (19), (30), (33), (51) gives:
% 106.50/14.39  | | | | |   (84)   ? [v0: $i] : (app(v0, nil) = all_91_1 & $i(v0) & ssList(v0))
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (4) with all_91_1, all_91_0, simplifying
% 106.50/14.39  | | | | |              with (30), (31), (33), (34), (59) gives:
% 106.50/14.39  | | | | |   (85)   ? [v0: $i] : (app(v0, all_91_0) = all_91_1 & $i(v0) &
% 106.50/14.39  | | | | |           ssList(v0))
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (ax82) with nil, all_114_0, nil, all_114_0,
% 106.50/14.39  | | | | |              nil, simplifying with (8), (19), (65), (66), (67) gives:
% 106.50/14.39  | | | | |   (86)   ? [v0: $i] : (app(all_114_0, all_114_0) = v0 & app(nil, v0) =
% 106.50/14.39  | | | | |           nil & $i(v0))
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (9) with all_114_0, nil, simplifying with
% 106.50/14.39  | | | | |              (65), (66), (67) gives:
% 106.50/14.39  | | | | |   (87)  all_114_0 = nil
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (18) with all_112_0, nil, simplifying with
% 106.50/14.39  | | | | |              (61), (62), (63) gives:
% 106.50/14.39  | | | | |   (88)  all_112_0 = nil
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (ax26) with all_116_2, nil, all_116_1,
% 106.50/14.39  | | | | |              simplifying with (8), (19), (69), (71), (74) gives:
% 106.50/14.39  | | | | |   (89)  ssList(all_116_1)
% 106.50/14.39  | | | | | 
% 106.50/14.39  | | | | | GROUND_INST: instantiating (18) with all_116_2, all_116_1, simplifying
% 106.50/14.39  | | | | |              with (69), (71), (74) gives:
% 106.50/14.39  | | | | |   (90)  all_116_1 = all_116_2
% 106.50/14.39  | | | | | 
% 106.50/14.40  | | | | | GROUND_INST: instantiating (ax82) with all_116_2, nil, all_116_1,
% 106.50/14.40  | | | | |              all_116_0, nil, simplifying with (8), (19), (69), (70),
% 106.50/14.40  | | | | |              (71), (73), (74), (75) gives:
% 106.50/14.40  | | | | |   (91)   ? [v0: $i] : (app(all_116_2, v0) = nil & app(nil, all_116_0)
% 106.50/14.40  | | | | |           = v0 & $i(v0))
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | DELTA: instantiating (86) with fresh symbol all_132_0 gives:
% 106.50/14.40  | | | | |   (92)  app(all_114_0, all_114_0) = all_132_0 & app(nil, all_132_0) =
% 106.50/14.40  | | | | |         nil & $i(all_132_0)
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | ALPHA: (92) implies:
% 106.50/14.40  | | | | |   (93)  $i(all_132_0)
% 106.50/14.40  | | | | |   (94)  app(all_114_0, all_114_0) = all_132_0
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | DELTA: instantiating (79) with fresh symbol all_134_0 gives:
% 106.50/14.40  | | | | |   (95)  app(all_91_2, all_134_0) = all_91_1 & $i(all_134_0) &
% 106.50/14.40  | | | | |         ssList(all_134_0)
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | ALPHA: (95) implies:
% 106.50/14.40  | | | | |   (96)  ssList(all_134_0)
% 106.50/14.40  | | | | |   (97)  $i(all_134_0)
% 106.50/14.40  | | | | |   (98)  app(all_91_2, all_134_0) = all_91_1
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | DELTA: instantiating (78) with fresh symbol all_136_0 gives:
% 106.50/14.40  | | | | |   (99)  app(nil, all_136_0) = all_91_1 & $i(all_136_0) &
% 106.50/14.40  | | | | |         ssList(all_136_0)
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | ALPHA: (99) implies:
% 106.50/14.40  | | | | |   (100)  ssList(all_136_0)
% 106.50/14.40  | | | | |   (101)  $i(all_136_0)
% 106.50/14.40  | | | | |   (102)  app(nil, all_136_0) = all_91_1
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | DELTA: instantiating (77) with fresh symbol all_138_0 gives:
% 106.50/14.40  | | | | |   (103)  app(all_91_2, all_138_0) = all_91_2 & $i(all_138_0) &
% 106.50/14.40  | | | | |          ssList(all_138_0)
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | ALPHA: (103) implies:
% 106.50/14.40  | | | | |   (104)  ssList(all_138_0)
% 106.50/14.40  | | | | |   (105)  $i(all_138_0)
% 106.50/14.40  | | | | |   (106)  app(all_91_2, all_138_0) = all_91_2
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | DELTA: instantiating (76) with fresh symbol all_140_0 gives:
% 106.50/14.40  | | | | |   (107)  app(nil, all_140_0) = all_91_2 & $i(all_140_0) &
% 106.50/14.40  | | | | |          ssList(all_140_0)
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | ALPHA: (107) implies:
% 106.50/14.40  | | | | |   (108)  ssList(all_140_0)
% 106.50/14.40  | | | | |   (109)  $i(all_140_0)
% 106.50/14.40  | | | | |   (110)  app(nil, all_140_0) = all_91_2
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | DELTA: instantiating (85) with fresh symbol all_142_0 gives:
% 106.50/14.40  | | | | |   (111)  app(all_142_0, all_91_0) = all_91_1 & $i(all_142_0) &
% 106.50/14.40  | | | | |          ssList(all_142_0)
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | ALPHA: (111) implies:
% 106.50/14.40  | | | | |   (112)  ssList(all_142_0)
% 106.50/14.40  | | | | |   (113)  $i(all_142_0)
% 106.50/14.40  | | | | |   (114)  app(all_142_0, all_91_0) = all_91_1
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | DELTA: instantiating (84) with fresh symbol all_146_0 gives:
% 106.50/14.40  | | | | |   (115)  app(all_146_0, nil) = all_91_1 & $i(all_146_0) &
% 106.50/14.40  | | | | |          ssList(all_146_0)
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | ALPHA: (115) implies:
% 106.50/14.40  | | | | |   (116)  ssList(all_146_0)
% 106.50/14.40  | | | | |   (117)  $i(all_146_0)
% 106.50/14.40  | | | | |   (118)  app(all_146_0, nil) = all_91_1
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | DELTA: instantiating (83) with fresh symbol all_148_0 gives:
% 106.50/14.40  | | | | |   (119)  app(all_148_0, all_91_2) = all_91_2 & $i(all_148_0) &
% 106.50/14.40  | | | | |          ssList(all_148_0)
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | ALPHA: (119) implies:
% 106.50/14.40  | | | | |   (120)  ssList(all_148_0)
% 106.50/14.40  | | | | |   (121)  $i(all_148_0)
% 106.50/14.40  | | | | |   (122)  app(all_148_0, all_91_2) = all_91_2
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | DELTA: instantiating (82) with fresh symbol all_152_0 gives:
% 106.50/14.40  | | | | |   (123)  app(all_152_0, nil) = all_91_2 & $i(all_152_0) &
% 106.50/14.40  | | | | |          ssList(all_152_0)
% 106.50/14.40  | | | | | 
% 106.50/14.40  | | | | | ALPHA: (123) implies:
% 106.50/14.40  | | | | |   (124)  ssList(all_152_0)
% 106.50/14.40  | | | | |   (125)  $i(all_152_0)
% 106.50/14.41  | | | | |   (126)  app(all_152_0, nil) = all_91_2
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | DELTA: instantiating (91) with fresh symbol all_156_0 gives:
% 106.50/14.41  | | | | |   (127)  app(all_116_2, all_156_0) = nil & app(nil, all_116_0) =
% 106.50/14.41  | | | | |          all_156_0 & $i(all_156_0)
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | ALPHA: (127) implies:
% 106.50/14.41  | | | | |   (128)  app(nil, all_116_0) = all_156_0
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | DELTA: instantiating (81) with fresh symbol all_158_0 gives:
% 106.50/14.41  | | | | |   (129)  app(nil, all_158_0) = all_91_0 & $i(all_158_0) &
% 106.50/14.41  | | | | |          ssList(all_158_0)
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | ALPHA: (129) implies:
% 106.50/14.41  | | | | |   (130)  ssList(all_158_0)
% 106.50/14.41  | | | | |   (131)  $i(all_158_0)
% 106.50/14.41  | | | | |   (132)  app(nil, all_158_0) = all_91_0
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | DELTA: instantiating (80) with fresh symbol all_160_0 gives:
% 106.50/14.41  | | | | |   (133)  app(all_91_1, all_160_0) = all_91_1 & $i(all_160_0) &
% 106.50/14.41  | | | | |          ssList(all_160_0)
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | ALPHA: (133) implies:
% 106.50/14.41  | | | | |   (134)  ssList(all_160_0)
% 106.50/14.41  | | | | |   (135)  $i(all_160_0)
% 106.50/14.41  | | | | |   (136)  app(all_91_1, all_160_0) = all_91_1
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | REDUCE: (75), (90) imply:
% 106.50/14.41  | | | | |   (137)  app(all_116_2, all_116_0) = nil
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | REDUCE: (87), (94) imply:
% 106.50/14.41  | | | | |   (138)  app(nil, nil) = all_132_0
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | GROUND_INST: instantiating (15) with all_132_0, simplifying with (8),
% 106.50/14.41  | | | | |              (138) gives:
% 106.50/14.41  | | | | |   (139)  all_132_0 = nil
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | REDUCE: (138), (139) imply:
% 106.50/14.41  | | | | |   (140)  app(nil, nil) = nil
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | GROUND_INST: instantiating (7) with all_136_0, all_91_2, simplifying
% 106.50/14.41  | | | | |              with (29), (32), (100), (101) gives:
% 106.50/14.41  | | | | |   (141)  all_136_0 = all_91_2 | neq(all_136_0, all_91_2)
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | GROUND_INST: instantiating (ax82) with nil, nil, nil, all_116_0,
% 106.50/14.41  | | | | |              all_156_0, simplifying with (8), (19), (70), (73), (128),
% 106.50/14.41  | | | | |              (140) gives:
% 106.50/14.41  | | | | |   (142)   ? [v0: $i] : (app(nil, v0) = all_156_0 & app(nil, all_116_0)
% 106.50/14.41  | | | | |            = v0 & $i(v0) & $i(all_156_0))
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | GROUND_INST: instantiating (9) with all_116_0, all_156_0, simplifying
% 106.50/14.41  | | | | |              with (70), (73), (128) gives:
% 106.50/14.41  | | | | |   (143)  all_156_0 = all_116_0
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | GROUND_INST: instantiating (ax82) with nil, nil, nil, all_136_0,
% 106.50/14.41  | | | | |              all_91_1, simplifying with (8), (19), (100), (101),
% 106.50/14.41  | | | | |              (102), (140) gives:
% 106.50/14.41  | | | | |   (144)   ? [v0: $i] : (app(nil, v0) = all_91_1 & app(nil, all_136_0)
% 106.50/14.41  | | | | |            = v0 & $i(v0) & $i(all_91_1))
% 106.50/14.41  | | | | | 
% 106.50/14.41  | | | | | GROUND_INST: instantiating (36) with nil, nil, nil, all_136_0,
% 106.50/14.41  | | | | |              simplifying with (8), (19), (100), (101), (102), (140)
% 106.50/14.41  | | | | |              gives:
% 106.89/14.41  | | | | |   (145)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(nil, all_136_0) = v0
% 106.89/14.41  | | | | |            & $i(v0))
% 106.89/14.41  | | | | | 
% 106.89/14.41  | | | | | GROUND_INST: instantiating (9) with all_136_0, all_91_1, simplifying
% 106.89/14.41  | | | | |              with (100), (101), (102) gives:
% 106.89/14.41  | | | | |   (146)  all_136_0 = all_91_1
% 106.89/14.41  | | | | | 
% 106.89/14.41  | | | | | GROUND_INST: instantiating (ax82) with nil, all_140_0, all_91_2,
% 106.89/14.41  | | | | |              all_91_0, all_91_1, simplifying with (8), (19), (31),
% 106.89/14.41  | | | | |              (34), (35), (108), (109), (110) gives:
% 106.89/14.41  | | | | |   (147)   ? [v0: $i] : (app(all_140_0, all_91_0) = v0 & app(nil, v0) =
% 106.89/14.41  | | | | |            all_91_1 & $i(v0) & $i(all_91_1))
% 106.89/14.41  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (36) with nil, all_140_0, all_91_2,
% 106.89/14.42  | | | | |              all_91_0, simplifying with (8), (19), (31), (34), (35),
% 106.89/14.42  | | | | |              (108), (109), (110) gives:
% 106.89/14.42  | | | | |   (148)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(nil, all_91_0) = v0
% 106.89/14.42  | | | | |            & $i(v0))
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (ax82) with nil, nil, nil, all_140_0,
% 106.89/14.42  | | | | |              all_91_2, simplifying with (8), (19), (108), (109),
% 106.89/14.42  | | | | |              (110), (140) gives:
% 106.89/14.42  | | | | |   (149)   ? [v0: $i] : (app(nil, v0) = all_91_2 & app(nil, all_140_0)
% 106.89/14.42  | | | | |            = v0 & $i(v0) & $i(all_91_2))
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (9) with all_140_0, all_91_2, simplifying
% 106.89/14.42  | | | | |              with (108), (109), (110) gives:
% 106.89/14.42  | | | | |   (150)  all_140_0 = all_91_2
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (ax82) with nil, nil, nil, all_158_0,
% 106.89/14.42  | | | | |              all_91_0, simplifying with (8), (19), (130), (131),
% 106.89/14.42  | | | | |              (132), (140) gives:
% 106.89/14.42  | | | | |   (151)   ? [v0: $i] : (app(nil, v0) = all_91_0 & app(nil, all_158_0)
% 106.89/14.42  | | | | |            = v0 & $i(v0) & $i(all_91_0))
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (9) with all_158_0, all_91_0, simplifying
% 106.89/14.42  | | | | |              with (130), (131), (132) gives:
% 106.89/14.42  | | | | |   (152)  all_158_0 = all_91_0
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (ax80) with all_134_0, all_91_2, all_91_1,
% 106.89/14.42  | | | | |              all_91_0, simplifying with (29), (31), (32), (34), (35),
% 106.89/14.42  | | | | |              (96), (97), (98) gives:
% 106.89/14.42  | | | | |   (153)  all_134_0 = all_91_0
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (ax82) with nil, all_140_0, all_91_2,
% 106.89/14.42  | | | | |              all_134_0, all_91_1, simplifying with (8), (19), (96),
% 106.89/14.42  | | | | |              (97), (98), (108), (109), (110) gives:
% 106.89/14.42  | | | | |   (154)   ? [v0: $i] : (app(all_140_0, all_134_0) = v0 & app(nil, v0)
% 106.89/14.42  | | | | |            = all_91_1 & $i(v0) & $i(all_91_1))
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (36) with nil, all_140_0, all_91_2,
% 106.89/14.42  | | | | |              all_134_0, simplifying with (8), (19), (96), (97), (98),
% 106.89/14.42  | | | | |              (108), (109), (110) gives:
% 106.89/14.42  | | | | |   (155)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(nil, all_134_0) = v0
% 106.89/14.42  | | | | |            & $i(v0))
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (36) with all_91_2, all_138_0, all_91_2,
% 106.89/14.42  | | | | |              all_91_0, simplifying with (29), (31), (32), (34), (35),
% 106.89/14.42  | | | | |              (104), (105), (106) gives:
% 106.89/14.42  | | | | |   (156)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(all_91_2, all_91_0)
% 106.89/14.42  | | | | |            = v0 & $i(v0))
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (36) with all_91_2, all_138_0, all_91_2,
% 106.89/14.42  | | | | |              all_134_0, simplifying with (29), (32), (96), (97), (98),
% 106.89/14.42  | | | | |              (104), (105), (106) gives:
% 106.89/14.42  | | | | |   (157)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(all_91_2, all_134_0)
% 106.89/14.42  | | | | |            = v0 & $i(v0))
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (ax82) with nil, all_140_0, all_91_2,
% 106.89/14.42  | | | | |              all_138_0, all_91_2, simplifying with (8), (19), (104),
% 106.89/14.42  | | | | |              (105), (106), (108), (109), (110) gives:
% 106.89/14.42  | | | | |   (158)   ? [v0: $i] : (app(all_140_0, all_138_0) = v0 & app(nil, v0)
% 106.89/14.42  | | | | |            = all_91_2 & $i(v0) & $i(all_91_2))
% 106.89/14.42  | | | | | 
% 106.89/14.42  | | | | | GROUND_INST: instantiating (36) with all_91_1, all_160_0, all_91_1,
% 106.89/14.42  | | | | |              all_160_0, simplifying with (30), (33), (134), (135),
% 106.89/14.42  | | | | |              (136) gives:
% 106.89/14.43  | | | | |   (159)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(all_91_1, all_160_0)
% 106.89/14.43  | | | | |            = v0 & $i(v0))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (ax82) with nil, all_136_0, all_91_1,
% 106.89/14.43  | | | | |              all_160_0, all_91_1, simplifying with (8), (19), (100),
% 106.89/14.43  | | | | |              (101), (102), (134), (135), (136) gives:
% 106.89/14.43  | | | | |   (160)   ? [v0: $i] : (app(all_136_0, all_160_0) = v0 & app(nil, v0)
% 106.89/14.43  | | | | |            = all_91_1 & $i(v0) & $i(all_91_1))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (36) with all_91_2, all_134_0, all_91_1,
% 106.89/14.43  | | | | |              all_160_0, simplifying with (29), (32), (96), (97), (98),
% 106.89/14.43  | | | | |              (134), (135), (136) gives:
% 106.89/14.43  | | | | |   (161)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(all_91_2, all_160_0)
% 106.89/14.43  | | | | |            = v0 & $i(v0))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (ax82) with all_116_2, all_116_0, nil,
% 106.89/14.43  | | | | |              all_158_0, all_91_0, simplifying with (69), (70), (71),
% 106.89/14.43  | | | | |              (73), (130), (131), (132), (137) gives:
% 106.89/14.43  | | | | |   (162)   ? [v0: $i] : (app(all_116_0, all_158_0) = v0 &
% 106.89/14.43  | | | | |            app(all_116_2, v0) = all_91_0 & $i(v0) & $i(all_91_0))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (ax82) with all_116_2, all_116_0, nil,
% 106.89/14.43  | | | | |              all_140_0, all_91_2, simplifying with (69), (70), (71),
% 106.89/14.43  | | | | |              (73), (108), (109), (110), (137) gives:
% 106.89/14.43  | | | | |   (163)   ? [v0: $i] : (app(all_116_0, all_140_0) = v0 &
% 106.89/14.43  | | | | |            app(all_116_2, v0) = all_91_2 & $i(v0) & $i(all_91_2))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (ax82) with all_116_2, all_116_0, nil,
% 106.89/14.43  | | | | |              all_136_0, all_91_1, simplifying with (69), (70), (71),
% 106.89/14.43  | | | | |              (73), (100), (101), (102), (137) gives:
% 106.89/14.43  | | | | |   (164)   ? [v0: $i] : (app(all_116_0, all_136_0) = v0 &
% 106.89/14.43  | | | | |            app(all_116_2, v0) = all_91_1 & $i(v0) & $i(all_91_1))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (36) with all_116_2, all_116_0, nil,
% 106.89/14.43  | | | | |              all_136_0, simplifying with (69), (70), (71), (73),
% 106.89/14.43  | | | | |              (100), (101), (102), (137) gives:
% 106.89/14.43  | | | | |   (165)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(all_116_2,
% 106.89/14.43  | | | | |              all_136_0) = v0 & $i(v0))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (ax82) with all_116_2, all_116_0, nil,
% 106.89/14.43  | | | | |              all_116_0, all_156_0, simplifying with (69), (70), (71),
% 106.89/14.43  | | | | |              (73), (128), (137) gives:
% 106.89/14.43  | | | | |   (166)   ? [v0: $i] : (app(all_116_0, all_116_0) = v0 &
% 106.89/14.43  | | | | |            app(all_116_2, v0) = all_156_0 & $i(v0) & $i(all_156_0))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (ax82) with all_116_2, all_116_0, nil, nil,
% 106.89/14.43  | | | | |              nil, simplifying with (8), (19), (69), (70), (71), (73),
% 106.89/14.43  | | | | |              (137), (140) gives:
% 106.89/14.43  | | | | |   (167)   ? [v0: $i] : (app(all_116_0, nil) = v0 & app(all_116_2, v0)
% 106.89/14.43  | | | | |            = nil & $i(v0))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (17) with all_116_2, all_116_0, simplifying
% 106.89/14.43  | | | | |              with (69), (70), (71), (73), (137) gives:
% 106.89/14.43  | | | | |   (168)  all_116_0 = nil
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (16) with all_116_2, all_116_0, simplifying
% 106.89/14.43  | | | | |              with (69), (70), (71), (73), (137) gives:
% 106.89/14.43  | | | | |   (169)  all_116_2 = nil
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (ax79) with all_142_0, all_91_0, all_91_1,
% 106.89/14.43  | | | | |              all_91_2, simplifying with (29), (31), (32), (34), (35),
% 106.89/14.43  | | | | |              (112), (113), (114) gives:
% 106.89/14.43  | | | | |   (170)  all_142_0 = all_91_2
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (36) with all_142_0, all_91_0, all_91_1,
% 106.89/14.43  | | | | |              all_160_0, simplifying with (31), (34), (112), (113),
% 106.89/14.43  | | | | |              (114), (134), (135), (136) gives:
% 106.89/14.43  | | | | |   (171)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(all_142_0,
% 106.89/14.43  | | | | |              all_160_0) = v0 & $i(v0))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (36) with all_146_0, nil, all_91_1,
% 106.89/14.43  | | | | |              all_160_0, simplifying with (8), (19), (116), (117),
% 106.89/14.43  | | | | |              (118), (134), (135), (136) gives:
% 106.89/14.43  | | | | |   (172)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(all_146_0,
% 106.89/14.43  | | | | |              all_160_0) = v0 & $i(v0))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (18) with all_146_0, all_91_1, simplifying
% 106.89/14.43  | | | | |              with (116), (117), (118) gives:
% 106.89/14.43  | | | | |   (173)  all_146_0 = all_91_1
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (ax82) with all_148_0, all_91_2, all_91_2,
% 106.89/14.43  | | | | |              all_91_0, all_91_1, simplifying with (29), (31), (32),
% 106.89/14.43  | | | | |              (34), (35), (120), (121), (122) gives:
% 106.89/14.43  | | | | |   (174)   ? [v0: $i] : (app(all_148_0, v0) = all_91_1 & app(all_91_2,
% 106.89/14.43  | | | | |              all_91_0) = v0 & $i(v0) & $i(all_91_1))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (ax82) with all_148_0, all_91_2, all_91_2,
% 106.89/14.43  | | | | |              all_134_0, all_91_1, simplifying with (29), (32), (96),
% 106.89/14.43  | | | | |              (97), (98), (120), (121), (122) gives:
% 106.89/14.43  | | | | |   (175)   ? [v0: $i] : (app(all_148_0, v0) = all_91_1 & app(all_91_2,
% 106.89/14.43  | | | | |              all_134_0) = v0 & $i(v0) & $i(all_91_1))
% 106.89/14.43  | | | | | 
% 106.89/14.43  | | | | | GROUND_INST: instantiating (ax82) with all_152_0, nil, all_91_2,
% 106.89/14.43  | | | | |              all_91_0, all_91_1, simplifying with (8), (19), (31),
% 106.89/14.43  | | | | |              (34), (35), (124), (125), (126) gives:
% 106.89/14.44  | | | | |   (176)   ? [v0: $i] : (app(all_152_0, v0) = all_91_1 & app(nil,
% 106.89/14.44  | | | | |              all_91_0) = v0 & $i(v0) & $i(all_91_1))
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | GROUND_INST: instantiating (36) with all_152_0, nil, all_91_2,
% 106.89/14.44  | | | | |              all_91_0, simplifying with (8), (19), (31), (34), (35),
% 106.89/14.44  | | | | |              (124), (125), (126) gives:
% 106.89/14.44  | | | | |   (177)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(all_152_0, all_91_0)
% 106.89/14.44  | | | | |            = v0 & $i(v0))
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | GROUND_INST: instantiating (ax82) with all_152_0, nil, all_91_2,
% 106.89/14.44  | | | | |              all_134_0, all_91_1, simplifying with (8), (19), (96),
% 106.89/14.44  | | | | |              (97), (98), (124), (125), (126) gives:
% 106.89/14.44  | | | | |   (178)   ? [v0: $i] : (app(all_152_0, v0) = all_91_1 & app(nil,
% 106.89/14.44  | | | | |              all_134_0) = v0 & $i(v0) & $i(all_91_1))
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | GROUND_INST: instantiating (36) with all_152_0, nil, all_91_2,
% 106.89/14.44  | | | | |              all_134_0, simplifying with (8), (19), (96), (97), (98),
% 106.89/14.44  | | | | |              (124), (125), (126) gives:
% 106.89/14.44  | | | | |   (179)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(all_152_0,
% 106.89/14.44  | | | | |              all_134_0) = v0 & $i(v0))
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | GROUND_INST: instantiating (18) with all_152_0, all_91_2, simplifying
% 106.89/14.44  | | | | |              with (124), (125), (126) gives:
% 106.89/14.44  | | | | |   (180)  all_152_0 = all_91_2
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | COMBINE_EQS: (143), (168) imply:
% 106.89/14.44  | | | | |   (181)  all_156_0 = nil
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (148) with fresh symbol all_188_0 gives:
% 106.89/14.44  | | | | |   (182)   ~ (all_188_0 = all_91_2) & app(nil, all_91_0) = all_188_0 &
% 106.89/14.44  | | | | |          $i(all_188_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (182) implies:
% 106.89/14.44  | | | | |   (183)  $i(all_188_0)
% 106.89/14.44  | | | | |   (184)  app(nil, all_91_0) = all_188_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (165) with fresh symbol all_190_0 gives:
% 106.89/14.44  | | | | |   (185)   ~ (all_190_0 = all_91_2) & app(all_116_2, all_136_0) =
% 106.89/14.44  | | | | |          all_190_0 & $i(all_190_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (185) implies:
% 106.89/14.44  | | | | |   (186)   ~ (all_190_0 = all_91_2)
% 106.89/14.44  | | | | |   (187)  $i(all_190_0)
% 106.89/14.44  | | | | |   (188)  app(all_116_2, all_136_0) = all_190_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (161) with fresh symbol all_194_0 gives:
% 106.89/14.44  | | | | |   (189)   ~ (all_194_0 = all_91_2) & app(all_91_2, all_160_0) =
% 106.89/14.44  | | | | |          all_194_0 & $i(all_194_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (189) implies:
% 106.89/14.44  | | | | |   (190)  app(all_91_2, all_160_0) = all_194_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (159) with fresh symbol all_198_0 gives:
% 106.89/14.44  | | | | |   (191)   ~ (all_198_0 = all_91_2) & app(all_91_1, all_160_0) =
% 106.89/14.44  | | | | |          all_198_0 & $i(all_198_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (191) implies:
% 106.89/14.44  | | | | |   (192)  app(all_91_1, all_160_0) = all_198_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (157) with fresh symbol all_204_0 gives:
% 106.89/14.44  | | | | |   (193)   ~ (all_204_0 = all_91_2) & app(all_91_2, all_134_0) =
% 106.89/14.44  | | | | |          all_204_0 & $i(all_204_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (193) implies:
% 106.89/14.44  | | | | |   (194)  app(all_91_2, all_134_0) = all_204_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (145) with fresh symbol all_206_0 gives:
% 106.89/14.44  | | | | |   (195)   ~ (all_206_0 = all_91_2) & app(nil, all_136_0) = all_206_0 &
% 106.89/14.44  | | | | |          $i(all_206_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (195) implies:
% 106.89/14.44  | | | | |   (196)  app(nil, all_136_0) = all_206_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (172) with fresh symbol all_208_0 gives:
% 106.89/14.44  | | | | |   (197)   ~ (all_208_0 = all_91_2) & app(all_146_0, all_160_0) =
% 106.89/14.44  | | | | |          all_208_0 & $i(all_208_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (197) implies:
% 106.89/14.44  | | | | |   (198)  app(all_146_0, all_160_0) = all_208_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (177) with fresh symbol all_212_0 gives:
% 106.89/14.44  | | | | |   (199)   ~ (all_212_0 = all_91_2) & app(all_152_0, all_91_0) =
% 106.89/14.44  | | | | |          all_212_0 & $i(all_212_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (199) implies:
% 106.89/14.44  | | | | |   (200)  app(all_152_0, all_91_0) = all_212_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (167) with fresh symbol all_216_0 gives:
% 106.89/14.44  | | | | |   (201)  app(all_116_0, nil) = all_216_0 & app(all_116_2, all_216_0) =
% 106.89/14.44  | | | | |          nil & $i(all_216_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (201) implies:
% 106.89/14.44  | | | | |   (202)  $i(all_216_0)
% 106.89/14.44  | | | | |   (203)  app(all_116_0, nil) = all_216_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (179) with fresh symbol all_222_0 gives:
% 106.89/14.44  | | | | |   (204)   ~ (all_222_0 = all_91_2) & app(all_152_0, all_134_0) =
% 106.89/14.44  | | | | |          all_222_0 & $i(all_222_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (204) implies:
% 106.89/14.44  | | | | |   (205)  app(all_152_0, all_134_0) = all_222_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (156) with fresh symbol all_226_0 gives:
% 106.89/14.44  | | | | |   (206)   ~ (all_226_0 = all_91_2) & app(all_91_2, all_91_0) =
% 106.89/14.44  | | | | |          all_226_0 & $i(all_226_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (206) implies:
% 106.89/14.44  | | | | |   (207)  app(all_91_2, all_91_0) = all_226_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (171) with fresh symbol all_246_0 gives:
% 106.89/14.44  | | | | |   (208)   ~ (all_246_0 = all_91_2) & app(all_142_0, all_160_0) =
% 106.89/14.44  | | | | |          all_246_0 & $i(all_246_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (208) implies:
% 106.89/14.44  | | | | |   (209)   ~ (all_246_0 = all_91_2)
% 106.89/14.44  | | | | |   (210)  app(all_142_0, all_160_0) = all_246_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (155) with fresh symbol all_248_0 gives:
% 106.89/14.44  | | | | |   (211)   ~ (all_248_0 = all_91_2) & app(nil, all_134_0) = all_248_0 &
% 106.89/14.44  | | | | |          $i(all_248_0)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (211) implies:
% 106.89/14.44  | | | | |   (212)  app(nil, all_134_0) = all_248_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (158) with fresh symbol all_252_0 gives:
% 106.89/14.44  | | | | |   (213)  app(all_140_0, all_138_0) = all_252_0 & app(nil, all_252_0) =
% 106.89/14.44  | | | | |          all_91_2 & $i(all_252_0) & $i(all_91_2)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (213) implies:
% 106.89/14.44  | | | | |   (214)  $i(all_252_0)
% 106.89/14.44  | | | | |   (215)  app(all_140_0, all_138_0) = all_252_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (178) with fresh symbol all_254_0 gives:
% 106.89/14.44  | | | | |   (216)  app(all_152_0, all_254_0) = all_91_1 & app(nil, all_134_0) =
% 106.89/14.44  | | | | |          all_254_0 & $i(all_254_0) & $i(all_91_1)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (216) implies:
% 106.89/14.44  | | | | |   (217)  app(nil, all_134_0) = all_254_0
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | DELTA: instantiating (160) with fresh symbol all_258_0 gives:
% 106.89/14.44  | | | | |   (218)  app(all_136_0, all_160_0) = all_258_0 & app(nil, all_258_0) =
% 106.89/14.44  | | | | |          all_91_1 & $i(all_258_0) & $i(all_91_1)
% 106.89/14.44  | | | | | 
% 106.89/14.44  | | | | | ALPHA: (218) implies:
% 106.89/14.45  | | | | |   (219)  app(all_136_0, all_160_0) = all_258_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (144) with fresh symbol all_262_0 gives:
% 106.89/14.45  | | | | |   (220)  app(nil, all_262_0) = all_91_1 & app(nil, all_136_0) =
% 106.89/14.45  | | | | |          all_262_0 & $i(all_262_0) & $i(all_91_1)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (220) implies:
% 106.89/14.45  | | | | |   (221)  app(nil, all_136_0) = all_262_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (163) with fresh symbol all_268_0 gives:
% 106.89/14.45  | | | | |   (222)  app(all_116_0, all_140_0) = all_268_0 & app(all_116_2,
% 106.89/14.45  | | | | |            all_268_0) = all_91_2 & $i(all_268_0) & $i(all_91_2)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (222) implies:
% 106.89/14.45  | | | | |   (223)  app(all_116_0, all_140_0) = all_268_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (162) with fresh symbol all_272_0 gives:
% 106.89/14.45  | | | | |   (224)  app(all_116_0, all_158_0) = all_272_0 & app(all_116_2,
% 106.89/14.45  | | | | |            all_272_0) = all_91_0 & $i(all_272_0) & $i(all_91_0)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (224) implies:
% 106.89/14.45  | | | | |   (225)  app(all_116_0, all_158_0) = all_272_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (174) with fresh symbol all_284_0 gives:
% 106.89/14.45  | | | | |   (226)  app(all_148_0, all_284_0) = all_91_1 & app(all_91_2,
% 106.89/14.45  | | | | |            all_91_0) = all_284_0 & $i(all_284_0) & $i(all_91_1)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (226) implies:
% 106.89/14.45  | | | | |   (227)  app(all_91_2, all_91_0) = all_284_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (149) with fresh symbol all_286_0 gives:
% 106.89/14.45  | | | | |   (228)  app(nil, all_286_0) = all_91_2 & app(nil, all_140_0) =
% 106.89/14.45  | | | | |          all_286_0 & $i(all_286_0) & $i(all_91_2)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (228) implies:
% 106.89/14.45  | | | | |   (229)  app(nil, all_140_0) = all_286_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (142) with fresh symbol all_288_0 gives:
% 106.89/14.45  | | | | |   (230)  app(nil, all_288_0) = all_156_0 & app(nil, all_116_0) =
% 106.89/14.45  | | | | |          all_288_0 & $i(all_288_0) & $i(all_156_0)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (230) implies:
% 106.89/14.45  | | | | |   (231)  app(nil, all_116_0) = all_288_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (176) with fresh symbol all_290_0 gives:
% 106.89/14.45  | | | | |   (232)  app(all_152_0, all_290_0) = all_91_1 & app(nil, all_91_0) =
% 106.89/14.45  | | | | |          all_290_0 & $i(all_290_0) & $i(all_91_1)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (232) implies:
% 106.89/14.45  | | | | |   (233)  app(nil, all_91_0) = all_290_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (175) with fresh symbol all_294_0 gives:
% 106.89/14.45  | | | | |   (234)  app(all_148_0, all_294_0) = all_91_1 & app(all_91_2,
% 106.89/14.45  | | | | |            all_134_0) = all_294_0 & $i(all_294_0) & $i(all_91_1)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (234) implies:
% 106.89/14.45  | | | | |   (235)  app(all_91_2, all_134_0) = all_294_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (147) with fresh symbol all_296_0 gives:
% 106.89/14.45  | | | | |   (236)  app(all_140_0, all_91_0) = all_296_0 & app(nil, all_296_0) =
% 106.89/14.45  | | | | |          all_91_1 & $i(all_296_0) & $i(all_91_1)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (236) implies:
% 106.89/14.45  | | | | |   (237)  app(all_140_0, all_91_0) = all_296_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (154) with fresh symbol all_298_0 gives:
% 106.89/14.45  | | | | |   (238)  app(all_140_0, all_134_0) = all_298_0 & app(nil, all_298_0) =
% 106.89/14.45  | | | | |          all_91_1 & $i(all_298_0) & $i(all_91_1)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (238) implies:
% 106.89/14.45  | | | | |   (239)  app(all_140_0, all_134_0) = all_298_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (164) with fresh symbol all_300_0 gives:
% 106.89/14.45  | | | | |   (240)  app(all_116_0, all_136_0) = all_300_0 & app(all_116_2,
% 106.89/14.45  | | | | |            all_300_0) = all_91_1 & $i(all_300_0) & $i(all_91_1)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (240) implies:
% 106.89/14.45  | | | | |   (241)  app(all_116_0, all_136_0) = all_300_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (151) with fresh symbol all_302_0 gives:
% 106.89/14.45  | | | | |   (242)  app(nil, all_302_0) = all_91_0 & app(nil, all_158_0) =
% 106.89/14.45  | | | | |          all_302_0 & $i(all_302_0) & $i(all_91_0)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (242) implies:
% 106.89/14.45  | | | | |   (243)  app(nil, all_158_0) = all_302_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | DELTA: instantiating (166) with fresh symbol all_304_0 gives:
% 106.89/14.45  | | | | |   (244)  app(all_116_0, all_116_0) = all_304_0 & app(all_116_2,
% 106.89/14.45  | | | | |            all_304_0) = all_156_0 & $i(all_304_0) & $i(all_156_0)
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | ALPHA: (244) implies:
% 106.89/14.45  | | | | |   (245)  app(all_116_0, all_116_0) = all_304_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (153), (180), (205) imply:
% 106.89/14.45  | | | | |   (246)  app(all_91_2, all_91_0) = all_222_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (180), (200) imply:
% 106.89/14.45  | | | | |   (247)  app(all_91_2, all_91_0) = all_212_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (126), (180) imply:
% 106.89/14.45  | | | | |   (248)  app(all_91_2, nil) = all_91_2
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (173), (198) imply:
% 106.89/14.45  | | | | |   (249)  app(all_91_1, all_160_0) = all_208_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (118), (173) imply:
% 106.89/14.45  | | | | |   (250)  app(all_91_1, nil) = all_91_1
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (170), (210) imply:
% 106.89/14.45  | | | | |   (251)  app(all_91_2, all_160_0) = all_246_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (150), (215) imply:
% 106.89/14.45  | | | | |   (252)  app(all_91_2, all_138_0) = all_252_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (150), (153), (239) imply:
% 106.89/14.45  | | | | |   (253)  app(all_91_2, all_91_0) = all_298_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (150), (237) imply:
% 106.89/14.45  | | | | |   (254)  app(all_91_2, all_91_0) = all_296_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (146), (219) imply:
% 106.89/14.45  | | | | |   (255)  app(all_91_1, all_160_0) = all_258_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (152), (168), (225) imply:
% 106.89/14.45  | | | | |   (256)  app(nil, all_91_0) = all_272_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (150), (168), (223) imply:
% 106.89/14.45  | | | | |   (257)  app(nil, all_91_2) = all_268_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (146), (168), (241) imply:
% 106.89/14.45  | | | | |   (258)  app(nil, all_91_1) = all_300_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (168), (245) imply:
% 106.89/14.45  | | | | |   (259)  app(nil, nil) = all_304_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (168), (203) imply:
% 106.89/14.45  | | | | |   (260)  app(nil, nil) = all_216_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (146), (169), (188) imply:
% 106.89/14.45  | | | | |   (261)  app(nil, all_91_1) = all_190_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (153), (235) imply:
% 106.89/14.45  | | | | |   (262)  app(all_91_2, all_91_0) = all_294_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (153), (194) imply:
% 106.89/14.45  | | | | |   (263)  app(all_91_2, all_91_0) = all_204_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (152), (243) imply:
% 106.89/14.45  | | | | |   (264)  app(nil, all_91_0) = all_302_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (132), (152) imply:
% 106.89/14.45  | | | | |   (265)  app(nil, all_91_0) = all_91_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (150), (229) imply:
% 106.89/14.45  | | | | |   (266)  app(nil, all_91_2) = all_286_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (110), (150) imply:
% 106.89/14.45  | | | | |   (267)  app(nil, all_91_2) = all_91_2
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (146), (221) imply:
% 106.89/14.45  | | | | |   (268)  app(nil, all_91_1) = all_262_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (146), (196) imply:
% 106.89/14.45  | | | | |   (269)  app(nil, all_91_1) = all_206_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (102), (146) imply:
% 106.89/14.45  | | | | |   (270)  app(nil, all_91_1) = all_91_1
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (153), (217) imply:
% 106.89/14.45  | | | | |   (271)  app(nil, all_91_0) = all_254_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (153), (212) imply:
% 106.89/14.45  | | | | |   (272)  app(nil, all_91_0) = all_248_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | REDUCE: (168), (231) imply:
% 106.89/14.45  | | | | |   (273)  app(nil, nil) = all_288_0
% 106.89/14.45  | | | | | 
% 106.89/14.45  | | | | | GROUND_INST: instantiating (21) with all_216_0, all_288_0, nil, nil,
% 106.89/14.45  | | | | |              simplifying with (260), (273) gives:
% 106.89/14.45  | | | | |   (274)  all_288_0 = all_216_0
% 106.89/14.45  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with nil, all_304_0, nil, nil,
% 106.89/14.46  | | | | |              simplifying with (140), (259) gives:
% 106.89/14.46  | | | | |   (275)  all_304_0 = nil
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_288_0, all_304_0, nil, nil,
% 106.89/14.46  | | | | |              simplifying with (259), (273) gives:
% 106.89/14.46  | | | | |   (276)  all_304_0 = all_288_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_268_0, all_286_0, all_91_2,
% 106.89/14.46  | | | | |              nil, simplifying with (257), (266) gives:
% 106.89/14.46  | | | | |   (277)  all_286_0 = all_268_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_91_2, all_286_0, all_91_2,
% 106.89/14.46  | | | | |              nil, simplifying with (266), (267) gives:
% 106.89/14.46  | | | | |   (278)  all_286_0 = all_91_2
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_91_1, all_206_0, all_91_1,
% 106.89/14.46  | | | | |              nil, simplifying with (269), (270) gives:
% 106.89/14.46  | | | | |   (279)  all_206_0 = all_91_1
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_262_0, all_300_0, all_91_1,
% 106.89/14.46  | | | | |              nil, simplifying with (258), (268) gives:
% 106.89/14.46  | | | | |   (280)  all_300_0 = all_262_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_206_0, all_300_0, all_91_1,
% 106.89/14.46  | | | | |              nil, simplifying with (258), (269) gives:
% 106.89/14.46  | | | | |   (281)  all_300_0 = all_206_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_190_0, all_300_0, all_91_1,
% 106.89/14.46  | | | | |              nil, simplifying with (258), (261) gives:
% 106.89/14.46  | | | | |   (282)  all_300_0 = all_190_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_254_0, all_272_0, all_91_0,
% 106.89/14.46  | | | | |              nil, simplifying with (256), (271) gives:
% 106.89/14.46  | | | | |   (283)  all_272_0 = all_254_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_188_0, all_272_0, all_91_0,
% 106.89/14.46  | | | | |              nil, simplifying with (184), (256) gives:
% 106.89/14.46  | | | | |   (284)  all_272_0 = all_188_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_254_0, all_290_0, all_91_0,
% 106.89/14.46  | | | | |              nil, simplifying with (233), (271) gives:
% 106.89/14.46  | | | | |   (285)  all_290_0 = all_254_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_248_0, all_290_0, all_91_0,
% 106.89/14.46  | | | | |              nil, simplifying with (233), (272) gives:
% 106.89/14.46  | | | | |   (286)  all_290_0 = all_248_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_290_0, all_302_0, all_91_0,
% 106.89/14.46  | | | | |              nil, simplifying with (233), (264) gives:
% 106.89/14.46  | | | | |   (287)  all_302_0 = all_290_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_91_0, all_302_0, all_91_0,
% 106.89/14.46  | | | | |              nil, simplifying with (264), (265) gives:
% 106.89/14.46  | | | | |   (288)  all_302_0 = all_91_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_226_0, all_284_0, all_91_0,
% 106.89/14.46  | | | | |              all_91_2, simplifying with (207), (227) gives:
% 106.89/14.46  | | | | |   (289)  all_284_0 = all_226_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_91_1, all_296_0, all_91_0,
% 106.89/14.46  | | | | |              all_91_2, simplifying with (35), (254) gives:
% 106.89/14.46  | | | | |   (290)  all_296_0 = all_91_1
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_294_0, all_296_0, all_91_0,
% 106.89/14.46  | | | | |              all_91_2, simplifying with (254), (262) gives:
% 106.89/14.46  | | | | |   (291)  all_296_0 = all_294_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_226_0, all_296_0, all_91_0,
% 106.89/14.46  | | | | |              all_91_2, simplifying with (207), (254) gives:
% 106.89/14.46  | | | | |   (292)  all_296_0 = all_226_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_222_0, all_296_0, all_91_0,
% 106.89/14.46  | | | | |              all_91_2, simplifying with (246), (254) gives:
% 106.89/14.46  | | | | |   (293)  all_296_0 = all_222_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_204_0, all_296_0, all_91_0,
% 106.89/14.46  | | | | |              all_91_2, simplifying with (254), (263) gives:
% 106.89/14.46  | | | | |   (294)  all_296_0 = all_204_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_284_0, all_298_0, all_91_0,
% 106.89/14.46  | | | | |              all_91_2, simplifying with (227), (253) gives:
% 106.89/14.46  | | | | |   (295)  all_298_0 = all_284_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_212_0, all_298_0, all_91_0,
% 106.89/14.46  | | | | |              all_91_2, simplifying with (247), (253) gives:
% 106.89/14.46  | | | | |   (296)  all_298_0 = all_212_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_91_2, all_252_0, all_138_0,
% 106.89/14.46  | | | | |              all_91_2, simplifying with (106), (252) gives:
% 106.89/14.46  | | | | |   (297)  all_252_0 = all_91_2
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_194_0, all_246_0, all_160_0,
% 106.89/14.46  | | | | |              all_91_2, simplifying with (190), (251) gives:
% 106.89/14.46  | | | | |   (298)  all_246_0 = all_194_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_91_1, all_208_0, all_160_0,
% 106.89/14.46  | | | | |              all_91_1, simplifying with (136), (249) gives:
% 106.89/14.46  | | | | |   (299)  all_208_0 = all_91_1
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_208_0, all_258_0, all_160_0,
% 106.89/14.46  | | | | |              all_91_1, simplifying with (249), (255) gives:
% 106.89/14.46  | | | | |   (300)  all_258_0 = all_208_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | GROUND_INST: instantiating (21) with all_198_0, all_258_0, all_160_0,
% 106.89/14.46  | | | | |              all_91_1, simplifying with (192), (255) gives:
% 106.89/14.46  | | | | |   (301)  all_258_0 = all_198_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (275), (276) imply:
% 106.89/14.46  | | | | |   (302)  all_288_0 = nil
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (302) implies:
% 106.89/14.46  | | | | |   (303)  all_288_0 = nil
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (287), (288) imply:
% 106.89/14.46  | | | | |   (304)  all_290_0 = all_91_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (304) implies:
% 106.89/14.46  | | | | |   (305)  all_290_0 = all_91_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (280), (282) imply:
% 106.89/14.46  | | | | |   (306)  all_262_0 = all_190_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (280), (281) imply:
% 106.89/14.46  | | | | |   (307)  all_262_0 = all_206_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (295), (296) imply:
% 106.89/14.46  | | | | |   (308)  all_284_0 = all_212_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (308) implies:
% 106.89/14.46  | | | | |   (309)  all_284_0 = all_212_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (290), (291) imply:
% 106.89/14.46  | | | | |   (310)  all_294_0 = all_91_1
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (291), (293) imply:
% 106.89/14.46  | | | | |   (311)  all_294_0 = all_222_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (291), (292) imply:
% 106.89/14.46  | | | | |   (312)  all_294_0 = all_226_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (291), (294) imply:
% 106.89/14.46  | | | | |   (313)  all_294_0 = all_204_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (310), (311) imply:
% 106.89/14.46  | | | | |   (314)  all_222_0 = all_91_1
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (311), (312) imply:
% 106.89/14.46  | | | | |   (315)  all_226_0 = all_222_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (315) implies:
% 106.89/14.46  | | | | |   (316)  all_226_0 = all_222_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (311), (313) imply:
% 106.89/14.46  | | | | |   (317)  all_222_0 = all_204_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (285), (286) imply:
% 106.89/14.46  | | | | |   (318)  all_254_0 = all_248_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (318) implies:
% 106.89/14.46  | | | | |   (319)  all_254_0 = all_248_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (286), (305) imply:
% 106.89/14.46  | | | | |   (320)  all_248_0 = all_91_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (274), (303) imply:
% 106.89/14.46  | | | | |   (321)  all_216_0 = nil
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (321) implies:
% 106.89/14.46  | | | | |   (322)  all_216_0 = nil
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (277), (278) imply:
% 106.89/14.46  | | | | |   (323)  all_268_0 = all_91_2
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (289), (309) imply:
% 106.89/14.46  | | | | |   (324)  all_226_0 = all_212_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (324) implies:
% 106.89/14.46  | | | | |   (325)  all_226_0 = all_212_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (283), (284) imply:
% 106.89/14.46  | | | | |   (326)  all_254_0 = all_188_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (326) implies:
% 106.89/14.46  | | | | |   (327)  all_254_0 = all_188_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (306), (307) imply:
% 106.89/14.46  | | | | |   (328)  all_206_0 = all_190_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (328) implies:
% 106.89/14.46  | | | | |   (329)  all_206_0 = all_190_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (300), (301) imply:
% 106.89/14.46  | | | | |   (330)  all_208_0 = all_198_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (330) implies:
% 106.89/14.46  | | | | |   (331)  all_208_0 = all_198_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (319), (327) imply:
% 106.89/14.46  | | | | |   (332)  all_248_0 = all_188_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (332) implies:
% 106.89/14.46  | | | | |   (333)  all_248_0 = all_188_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (320), (333) imply:
% 106.89/14.46  | | | | |   (334)  all_188_0 = all_91_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (334) implies:
% 106.89/14.46  | | | | |   (335)  all_188_0 = all_91_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (316), (325) imply:
% 106.89/14.46  | | | | |   (336)  all_222_0 = all_212_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (336) implies:
% 106.89/14.46  | | | | |   (337)  all_222_0 = all_212_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (317), (337) imply:
% 106.89/14.46  | | | | |   (338)  all_212_0 = all_204_0
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (314), (337) imply:
% 106.89/14.46  | | | | |   (339)  all_212_0 = all_91_1
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (338), (339) imply:
% 106.89/14.46  | | | | |   (340)  all_204_0 = all_91_1
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | SIMP: (340) implies:
% 106.89/14.46  | | | | |   (341)  all_204_0 = all_91_1
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (299), (331) imply:
% 106.89/14.46  | | | | |   (342)  all_198_0 = all_91_1
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | COMBINE_EQS: (279), (329) imply:
% 106.89/14.46  | | | | |   (343)  all_190_0 = all_91_1
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | REDUCE: (209), (298) imply:
% 106.89/14.46  | | | | |   (344)   ~ (all_194_0 = all_91_2)
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | REDUCE: (186), (343) imply:
% 106.89/14.46  | | | | |   (345)   ~ (all_91_1 = all_91_2)
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | BETA: splitting (141) gives:
% 106.89/14.46  | | | | | 
% 106.89/14.46  | | | | | Case 1:
% 106.89/14.46  | | | | | | 
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | GROUND_INST: instantiating (ax80) with nil, all_91_2, all_91_2,
% 106.89/14.47  | | | | | |              all_138_0, simplifying with (8), (19), (29), (32),
% 106.89/14.47  | | | | | |              (104), (105), (106), (248) gives:
% 106.89/14.47  | | | | | |   (346)  all_138_0 = nil
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | GROUND_INST: instantiating (ax82) with all_148_0, all_91_2,
% 106.89/14.47  | | | | | |              all_91_2, all_160_0, all_194_0, simplifying with (29),
% 106.89/14.47  | | | | | |              (32), (120), (121), (122), (134), (135), (190) gives:
% 106.89/14.47  | | | | | |   (347)   ? [v0: $i] : (app(all_148_0, v0) = all_194_0 &
% 106.89/14.47  | | | | | |            app(all_91_2, all_160_0) = v0 & $i(v0) & $i(all_194_0))
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | GROUND_INST: instantiating (ax82) with nil, all_91_2, all_91_2,
% 106.89/14.47  | | | | | |              all_160_0, all_194_0, simplifying with (8), (19), (29),
% 106.89/14.47  | | | | | |              (32), (134), (135), (190), (267) gives:
% 106.89/14.47  | | | | | |   (348)   ? [v0: $i] : (app(all_91_2, all_160_0) = v0 & app(nil, v0)
% 106.89/14.47  | | | | | |            = all_194_0 & $i(v0) & $i(all_194_0))
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | GROUND_INST: instantiating (ax80) with nil, all_91_1, all_91_1,
% 106.89/14.47  | | | | | |              all_160_0, simplifying with (8), (19), (30), (33),
% 106.89/14.47  | | | | | |              (134), (135), (136), (250) gives:
% 106.89/14.47  | | | | | |   (349)  all_160_0 = nil
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | GROUND_INST: instantiating (36) with all_91_2, all_91_0, all_91_1,
% 106.89/14.47  | | | | | |              nil, simplifying with (8), (19), (29), (31), (32),
% 106.89/14.47  | | | | | |              (34), (35), (250) gives:
% 106.89/14.47  | | | | | |   (350)   ? [v0: any] : ( ~ (v0 = all_91_2) & app(all_91_2, nil) =
% 106.89/14.47  | | | | | |            v0 & $i(v0))
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | DELTA: instantiating (350) with fresh symbol all_492_0 gives:
% 106.89/14.47  | | | | | |   (351)   ~ (all_492_0 = all_91_2) & app(all_91_2, nil) = all_492_0
% 106.89/14.47  | | | | | |          & $i(all_492_0)
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | ALPHA: (351) implies:
% 106.89/14.47  | | | | | |   (352)  app(all_91_2, nil) = all_492_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | DELTA: instantiating (348) with fresh symbol all_802_0 gives:
% 106.89/14.47  | | | | | |   (353)  app(all_91_2, all_160_0) = all_802_0 & app(nil, all_802_0)
% 106.89/14.47  | | | | | |          = all_194_0 & $i(all_802_0) & $i(all_194_0)
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | ALPHA: (353) implies:
% 106.89/14.47  | | | | | |   (354)  app(all_91_2, all_160_0) = all_802_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | DELTA: instantiating (347) with fresh symbol all_810_0 gives:
% 106.89/14.47  | | | | | |   (355)  app(all_148_0, all_810_0) = all_194_0 & app(all_91_2,
% 106.89/14.47  | | | | | |            all_160_0) = all_810_0 & $i(all_810_0) & $i(all_194_0)
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | ALPHA: (355) implies:
% 106.89/14.47  | | | | | |   (356)  app(all_91_2, all_160_0) = all_810_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | REDUCE: (349), (356) imply:
% 106.89/14.47  | | | | | |   (357)  app(all_91_2, nil) = all_810_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | REDUCE: (349), (354) imply:
% 106.89/14.47  | | | | | |   (358)  app(all_91_2, nil) = all_802_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | REDUCE: (190), (349) imply:
% 106.89/14.47  | | | | | |   (359)  app(all_91_2, nil) = all_194_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | GROUND_INST: instantiating (21) with all_91_2, all_802_0, nil,
% 106.89/14.47  | | | | | |              all_91_2, simplifying with (248), (358) gives:
% 106.89/14.47  | | | | | |   (360)  all_802_0 = all_91_2
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | GROUND_INST: instantiating (21) with all_492_0, all_802_0, nil,
% 106.89/14.47  | | | | | |              all_91_2, simplifying with (352), (358) gives:
% 106.89/14.47  | | | | | |   (361)  all_802_0 = all_492_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | GROUND_INST: instantiating (21) with all_492_0, all_810_0, nil,
% 106.89/14.47  | | | | | |              all_91_2, simplifying with (352), (357) gives:
% 106.89/14.47  | | | | | |   (362)  all_810_0 = all_492_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | GROUND_INST: instantiating (21) with all_194_0, all_810_0, nil,
% 106.89/14.47  | | | | | |              all_91_2, simplifying with (357), (359) gives:
% 106.89/14.47  | | | | | |   (363)  all_810_0 = all_194_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | COMBINE_EQS: (362), (363) imply:
% 106.89/14.47  | | | | | |   (364)  all_492_0 = all_194_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | SIMP: (364) implies:
% 106.89/14.47  | | | | | |   (365)  all_492_0 = all_194_0
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | COMBINE_EQS: (360), (361) imply:
% 106.89/14.47  | | | | | |   (366)  all_492_0 = all_91_2
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | SIMP: (366) implies:
% 106.89/14.47  | | | | | |   (367)  all_492_0 = all_91_2
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | COMBINE_EQS: (365), (367) imply:
% 106.89/14.47  | | | | | |   (368)  all_194_0 = all_91_2
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | SIMP: (368) implies:
% 106.89/14.47  | | | | | |   (369)  all_194_0 = all_91_2
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | REDUCE: (344), (369) imply:
% 106.89/14.47  | | | | | |   (370)  $false
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | CLOSE: (370) is inconsistent.
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | Case 2:
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | |   (371)  all_136_0 = all_91_2
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | COMBINE_EQS: (146), (371) imply:
% 106.89/14.47  | | | | | |   (372)  all_91_1 = all_91_2
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | REDUCE: (345), (372) imply:
% 106.89/14.47  | | | | | |   (373)  $false
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | | CLOSE: (373) is inconsistent.
% 106.89/14.47  | | | | | | 
% 106.89/14.47  | | | | | End of split
% 106.89/14.47  | | | | | 
% 106.89/14.47  | | | | Case 2:
% 106.89/14.47  | | | | | 
% 106.89/14.47  | | | | |   (374)  all_89_0 = all_89_1
% 106.89/14.47  | | | | | 
% 106.89/14.47  | | | | | REDUCE: (23), (374) imply:
% 106.89/14.47  | | | | |   (375)  $false
% 106.89/14.47  | | | | | 
% 106.89/14.47  | | | | | CLOSE: (375) is inconsistent.
% 106.89/14.47  | | | | | 
% 106.89/14.47  | | | | End of split
% 106.89/14.47  | | | | 
% 106.89/14.47  | | | End of split
% 106.89/14.47  | | | 
% 106.89/14.47  | | End of split
% 106.89/14.47  | | 
% 106.89/14.47  | End of split
% 106.89/14.47  | 
% 106.89/14.47  End of proof
% 106.89/14.47  % SZS output end Proof for theBenchmark
% 106.89/14.47  
% 106.89/14.48  13845ms
%------------------------------------------------------------------------------