%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : COM013+4 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n005.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 : 0s
% DateTime : Fri Jul 15 00:51:06 EDT 2022
% Result : Theorem 70.15s 70.53s
% Output : Refutation 70.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM013+4 : TPTP v8.1.0. Released v4.0.0.
% 0.00/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n005.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Thu Jun 16 17:05:23 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.41/1.07 *** allocated 10000 integers for termspace/termends
% 0.41/1.07 *** allocated 10000 integers for clauses
% 0.41/1.07 *** allocated 10000 integers for justifications
% 0.41/1.07 Bliksem 1.12
% 0.41/1.07
% 0.41/1.07
% 0.41/1.07 Automatic Strategy Selection
% 0.41/1.07
% 0.41/1.07
% 0.41/1.07 Clauses:
% 0.41/1.07
% 0.41/1.07 { && }.
% 0.41/1.07 { && }.
% 0.41/1.07 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ),
% 0.41/1.07 aElement0( Z ) }.
% 0.41/1.07 { && }.
% 0.41/1.07 { && }.
% 0.41/1.07 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.41/1.07 sdtmndtplgtdt0( X, Y, Z ), aReductOfIn0( Z, X, Y ), alpha1( X, Y, Z ) }.
% 0.41/1.07 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.41/1.07 aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z ) }.
% 0.41/1.07 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha1( X
% 0.41/1.07 , Y, Z ), sdtmndtplgtdt0( X, Y, Z ) }.
% 0.41/1.07 { ! alpha1( X, Y, Z ), aElement0( skol1( T, U, W ) ) }.
% 0.41/1.07 { ! alpha1( X, Y, Z ), alpha6( X, Y, Z, skol1( X, Y, Z ) ) }.
% 0.41/1.07 { ! aElement0( T ), ! alpha6( X, Y, Z, T ), alpha1( X, Y, Z ) }.
% 0.41/1.07 { ! alpha6( X, Y, Z, T ), aReductOfIn0( T, X, Y ) }.
% 0.41/1.07 { ! alpha6( X, Y, Z, T ), sdtmndtplgtdt0( T, Y, Z ) }.
% 0.41/1.07 { ! aReductOfIn0( T, X, Y ), ! sdtmndtplgtdt0( T, Y, Z ), alpha6( X, Y, Z,
% 0.41/1.08 T ) }.
% 0.41/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0
% 0.41/1.08 ( T ), ! sdtmndtplgtdt0( X, Y, Z ), ! sdtmndtplgtdt0( Z, Y, T ),
% 0.41/1.08 sdtmndtplgtdt0( X, Y, T ) }.
% 0.41/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.41/1.08 sdtmndtasgtdt0( X, Y, Z ), X = Z, sdtmndtplgtdt0( X, Y, Z ) }.
% 0.41/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z,
% 0.41/1.08 sdtmndtasgtdt0( X, Y, Z ) }.
% 0.41/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.41/1.08 sdtmndtplgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z ) }.
% 0.41/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0
% 0.41/1.08 ( T ), ! sdtmndtasgtdt0( X, Y, Z ), ! sdtmndtasgtdt0( Z, Y, T ),
% 0.41/1.08 sdtmndtasgtdt0( X, Y, T ) }.
% 0.41/1.08 { ! aRewritingSystem0( X ), ! isConfluent0( X ), ! alpha2( X, Y, Z ),
% 0.41/1.08 alpha7( X, Y, Z ) }.
% 0.41/1.08 { ! aRewritingSystem0( X ), alpha2( X, skol2( X ), skol14( X ) ),
% 0.41/1.08 isConfluent0( X ) }.
% 0.41/1.08 { ! aRewritingSystem0( X ), ! alpha7( X, skol2( X ), skol14( X ) ),
% 0.41/1.08 isConfluent0( X ) }.
% 0.41/1.08 { ! alpha7( X, Y, Z ), aElement0( skol3( T, U, W ) ) }.
% 0.41/1.08 { ! alpha7( X, Y, Z ), alpha12( X, Y, Z, skol3( X, Y, Z ) ) }.
% 0.41/1.08 { ! aElement0( T ), ! alpha12( X, Y, Z, T ), alpha7( X, Y, Z ) }.
% 0.41/1.08 { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Y, X, T ) }.
% 0.41/1.08 { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Z, X, T ) }.
% 0.41/1.08 { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0( Z, X, T ), alpha12( X, Y,
% 0.41/1.08 Z, T ) }.
% 0.41/1.08 { ! alpha2( X, Y, Z ), aElement0( skol4( T, U, W ) ) }.
% 0.41/1.08 { ! alpha2( X, Y, Z ), alpha8( X, Y, Z, skol4( X, Y, Z ) ) }.
% 0.41/1.08 { ! aElement0( T ), ! alpha8( X, Y, Z, T ), alpha2( X, Y, Z ) }.
% 0.41/1.08 { ! alpha8( X, Y, Z, T ), aElement0( Y ) }.
% 0.41/1.08 { ! alpha8( X, Y, Z, T ), alpha13( X, Y, Z, T ) }.
% 0.41/1.08 { ! aElement0( Y ), ! alpha13( X, Y, Z, T ), alpha8( X, Y, Z, T ) }.
% 0.41/1.08 { ! alpha13( X, Y, Z, T ), aElement0( Z ) }.
% 0.41/1.08 { ! alpha13( X, Y, Z, T ), alpha16( X, Y, Z, T ) }.
% 0.41/1.08 { ! aElement0( Z ), ! alpha16( X, Y, Z, T ), alpha13( X, Y, Z, T ) }.
% 0.41/1.08 { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T, X, Y ) }.
% 0.41/1.08 { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T, X, Z ) }.
% 0.41/1.08 { ! sdtmndtasgtdt0( T, X, Y ), ! sdtmndtasgtdt0( T, X, Z ), alpha16( X, Y,
% 0.41/1.08 Z, T ) }.
% 0.41/1.08 { ! aRewritingSystem0( X ), ! isLocallyConfluent0( X ), ! alpha3( X, Y, Z )
% 0.41/1.08 , alpha9( X, Y, Z ) }.
% 0.41/1.08 { ! aRewritingSystem0( X ), alpha3( X, skol5( X ), skol15( X ) ),
% 0.41/1.08 isLocallyConfluent0( X ) }.
% 0.41/1.08 { ! aRewritingSystem0( X ), ! alpha9( X, skol5( X ), skol15( X ) ),
% 0.41/1.08 isLocallyConfluent0( X ) }.
% 0.41/1.08 { ! alpha9( X, Y, Z ), aElement0( skol6( T, U, W ) ) }.
% 0.41/1.08 { ! alpha9( X, Y, Z ), alpha14( X, Y, Z, skol6( X, Y, Z ) ) }.
% 0.41/1.08 { ! aElement0( T ), ! alpha14( X, Y, Z, T ), alpha9( X, Y, Z ) }.
% 0.41/1.08 { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Y, X, T ) }.
% 0.41/1.08 { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Z, X, T ) }.
% 0.41/1.08 { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0( Z, X, T ), alpha14( X, Y,
% 0.41/1.08 Z, T ) }.
% 0.41/1.08 { ! alpha3( X, Y, Z ), aElement0( skol7( T, U, W ) ) }.
% 0.41/1.08 { ! alpha3( X, Y, Z ), alpha10( X, Y, Z, skol7( X, Y, Z ) ) }.
% 0.41/1.08 { ! aElement0( T ), ! alpha10( X, Y, Z, T ), alpha3( X, Y, Z ) }.
% 0.41/1.08 { ! alpha10( X, Y, Z, T ), aElement0( Y ) }.
% 0.41/1.08 { ! alpha10( X, Y, Z, T ), alpha15( X, Y, Z, T ) }.
% 0.41/1.08 { ! aElement0( Y ), ! alpha15( X, Y, Z, T ), alpha10( X, Y, Z, T ) }.
% 0.41/1.08 { ! alpha15( X, Y, Z, T ), aElement0( Z ) }.
% 0.41/1.08 { ! alpha15( X, Y, Z, T ), alpha17( X, Y, Z, T ) }.
% 0.41/1.08 { ! aElement0( Z ), ! alpha17( X, Y, Z, T ), alpha15( X, Y, Z, T ) }.
% 0.41/1.08 { ! alpha17( X, Y, Z, T ), aReductOfIn0( Y, T, X ) }.
% 0.41/1.08 { ! alpha17( X, Y, Z, T ), aReductOfIn0( Z, T, X ) }.
% 0.41/1.08 { ! aReductOfIn0( Y, T, X ), ! aReductOfIn0( Z, T, X ), alpha17( X, Y, Z, T
% 0.41/1.08 ) }.
% 0.41/1.08 { ! aRewritingSystem0( X ), ! isTerminating0( X ), ! alpha4( Y, Z ),
% 0.41/1.08 alpha11( X, Y, Z ) }.
% 0.41/1.08 { ! aRewritingSystem0( X ), alpha4( skol8( X ), skol16( X ) ),
% 0.41/1.08 isTerminating0( X ) }.
% 0.41/1.08 { ! aRewritingSystem0( X ), ! alpha11( X, skol8( X ), skol16( X ) ),
% 0.41/1.08 isTerminating0( X ) }.
% 0.41/1.08 { ! alpha11( X, Y, Z ), ! sdtmndtplgtdt0( Y, X, Z ), iLess0( Z, Y ) }.
% 0.41/1.08 { sdtmndtplgtdt0( Y, X, Z ), alpha11( X, Y, Z ) }.
% 0.41/1.08 { ! iLess0( Z, Y ), alpha11( X, Y, Z ) }.
% 0.41/1.08 { ! alpha4( X, Y ), aElement0( X ) }.
% 0.41/1.08 { ! alpha4( X, Y ), aElement0( Y ) }.
% 0.41/1.08 { ! aElement0( X ), ! aElement0( Y ), alpha4( X, Y ) }.
% 0.41/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y )
% 0.41/1.08 , aElement0( Z ) }.
% 0.41/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y )
% 0.41/1.08 , alpha5( X, Y, Z ) }.
% 0.41/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha5( X
% 0.41/1.08 , Y, Z ), aNormalFormOfIn0( Z, X, Y ) }.
% 0.41/1.08 { ! alpha5( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z ) }.
% 0.41/1.08 { ! alpha5( X, Y, Z ), ! aReductOfIn0( T, Z, Y ) }.
% 0.41/1.08 { ! sdtmndtasgtdt0( X, Y, Z ), aReductOfIn0( skol9( Y, Z ), Z, Y ), alpha5
% 0.41/1.08 ( X, Y, Z ) }.
% 0.41/1.08 { aRewritingSystem0( xR ) }.
% 0.41/1.08 { ! aElement0( X ), ! aElement0( Y ), ! aReductOfIn0( Y, X, xR ), iLess0( Y
% 0.41/1.08 , X ) }.
% 0.41/1.08 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), ! aReductOfIn0( Z,
% 0.41/1.08 X, xR ), ! sdtmndtplgtdt0( Z, xR, Y ), iLess0( Y, X ) }.
% 0.41/1.08 { ! aElement0( X ), ! aElement0( Y ), ! sdtmndtplgtdt0( X, xR, Y ), iLess0
% 0.41/1.08 ( Y, X ) }.
% 0.41/1.08 { isTerminating0( xR ) }.
% 0.41/1.08 { aElement0( skol10 ) }.
% 0.41/1.08 { ! aElement0( X ), ! iLess0( X, skol10 ), alpha18( X ) }.
% 0.41/1.08 { ! aElement0( X ), alpha19( skol10, X ), aReductOfIn0( skol17( X ), X, xR
% 0.41/1.08 ) }.
% 0.41/1.08 { ! aElement0( X ), ! aElement0( Y ), ! aReductOfIn0( Y, skol10, xR ), !
% 0.41/1.08 sdtmndtplgtdt0( Y, xR, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 0.41/1.08 { ! aElement0( X ), ! sdtmndtplgtdt0( skol10, xR, X ), aReductOfIn0( skol17
% 0.41/1.08 ( X ), X, xR ) }.
% 0.41/1.08 { ! aElement0( X ), ! sdtmndtasgtdt0( skol10, xR, X ), aReductOfIn0( skol17
% 0.41/1.08 ( X ), X, xR ) }.
% 0.41/1.08 { ! aNormalFormOfIn0( X, skol10, xR ) }.
% 0.41/1.08 { ! alpha19( X, Y ), ! X = Y }.
% 0.41/1.08 { ! alpha19( X, Y ), ! aReductOfIn0( Y, X, xR ) }.
% 0.41/1.08 { X = Y, aReductOfIn0( Y, X, xR ), alpha19( X, Y ) }.
% 0.41/1.08 { ! alpha18( X ), alpha20( X, skol11( X ) ) }.
% 0.41/1.08 { ! alpha18( X ), aNormalFormOfIn0( skol11( X ), X, xR ) }.
% 0.41/1.08 { ! alpha20( X, Y ), ! aNormalFormOfIn0( Y, X, xR ), alpha18( X ) }.
% 0.41/1.08 { ! alpha20( X, Y ), alpha21( X, Y ) }.
% 0.41/1.08 { ! alpha20( X, Y ), ! aReductOfIn0( Z, Y, xR ) }.
% 0.41/1.08 { ! alpha21( X, Y ), aReductOfIn0( skol12( Y ), Y, xR ), alpha20( X, Y ) }
% 0.41/1.08 .
% 0.41/1.08 { ! alpha21( X, Y ), alpha22( X, Y ) }.
% 0.41/1.08 { ! alpha21( X, Y ), sdtmndtasgtdt0( X, xR, Y ) }.
% 0.41/1.08 { ! alpha22( X, Y ), ! sdtmndtasgtdt0( X, xR, Y ), alpha21( X, Y ) }.
% 0.41/1.08 { ! alpha22( X, Y ), aElement0( Y ) }.
% 0.41/1.08 { ! alpha22( X, Y ), alpha23( X, Y ) }.
% 0.41/1.08 { ! aElement0( Y ), ! alpha23( X, Y ), alpha22( X, Y ) }.
% 0.41/1.08 { ! alpha23( X, Y ), X = Y, alpha24( X, Y ) }.
% 0.41/1.08 { ! X = Y, alpha23( X, Y ) }.
% 0.41/1.08 { ! alpha24( X, Y ), alpha23( X, Y ) }.
% 0.41/1.08 { ! alpha24( X, Y ), alpha25( X, Y ) }.
% 0.41/1.08 { ! alpha24( X, Y ), sdtmndtplgtdt0( X, xR, Y ) }.
% 0.41/1.08 { ! alpha25( X, Y ), ! sdtmndtplgtdt0( X, xR, Y ), alpha24( X, Y ) }.
% 0.41/1.08 { ! alpha25( X, Y ), aReductOfIn0( Y, X, xR ), alpha26( X, Y ) }.
% 0.41/1.08 { ! aReductOfIn0( Y, X, xR ), alpha25( X, Y ) }.
% 0.41/1.08 { ! alpha26( X, Y ), alpha25( X, Y ) }.
% 0.41/1.08 { ! alpha26( X, Y ), aElement0( skol13( Z, T ) ) }.
% 0.41/1.08 { ! alpha26( X, Y ), sdtmndtplgtdt0( skol13( Z, Y ), xR, Y ) }.
% 0.41/1.08 { ! alpha26( X, Y ), aReductOfIn0( skol13( X, Y ), X, xR ) }.
% 0.41/1.08 { ! aElement0( Z ), ! aReductOfIn0( Z, X, xR ), ! sdtmndtplgtdt0( Z, xR, Y
% 0.41/1.08 ), alpha26( X, Y ) }.
% 0.41/1.08
% 0.41/1.08 percentage equality = 0.019108, percentage horn = 0.893805
% 0.41/1.08 This is a problem with some equality
% 0.41/1.08
% 0.41/1.08
% 0.41/1.08
% 0.41/1.08 Options Used:
% 0.41/1.08
% 0.41/1.08 useres = 1
% 0.41/1.08 useparamod = 1
% 9.15/9.52 useeqrefl = 1
% 9.15/9.52 useeqfact = 1
% 9.15/9.52 usefactor = 1
% 9.15/9.52 usesimpsplitting = 0
% 9.15/9.52 usesimpdemod = 5
% 9.15/9.52 usesimpres = 3
% 9.15/9.52
% 9.15/9.52 resimpinuse = 1000
% 9.15/9.52 resimpclauses = 20000
% 9.15/9.52 substype = eqrewr
% 9.15/9.52 backwardsubs = 1
% 9.15/9.52 selectoldest = 5
% 9.15/9.52
% 9.15/9.52 litorderings [0] = split
% 9.15/9.52 litorderings [1] = extend the termordering, first sorting on arguments
% 9.15/9.52
% 9.15/9.52 termordering = kbo
% 9.15/9.52
% 9.15/9.52 litapriori = 0
% 9.15/9.52 termapriori = 1
% 9.15/9.52 litaposteriori = 0
% 9.15/9.52 termaposteriori = 0
% 9.15/9.52 demodaposteriori = 0
% 9.15/9.52 ordereqreflfact = 0
% 9.15/9.52
% 9.15/9.52 litselect = negord
% 9.15/9.52
% 9.15/9.52 maxweight = 15
% 9.15/9.52 maxdepth = 30000
% 9.15/9.52 maxlength = 115
% 9.15/9.52 maxnrvars = 195
% 9.15/9.52 excuselevel = 1
% 9.15/9.52 increasemaxweight = 1
% 9.15/9.52
% 9.15/9.52 maxselected = 10000000
% 9.15/9.52 maxnrclauses = 10000000
% 9.15/9.52
% 9.15/9.52 showgenerated = 0
% 9.15/9.52 showkept = 0
% 9.15/9.52 showselected = 0
% 9.15/9.52 showdeleted = 0
% 9.15/9.52 showresimp = 1
% 9.15/9.52 showstatus = 2000
% 9.15/9.52
% 9.15/9.52 prologoutput = 0
% 9.15/9.52 nrgoals = 5000000
% 9.15/9.52 totalproof = 1
% 9.15/9.52
% 9.15/9.52 Symbols occurring in the translation:
% 9.15/9.52
% 9.15/9.52 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 9.15/9.52 . [1, 2] (w:1, o:33, a:1, s:1, b:0),
% 9.15/9.52 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 9.15/9.52 ! [4, 1] (w:0, o:13, a:1, s:1, b:0),
% 9.15/9.52 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 9.15/9.52 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 9.15/9.52 aElement0 [36, 1] (w:1, o:18, a:1, s:1, b:0),
% 9.15/9.52 aRewritingSystem0 [37, 1] (w:1, o:19, a:1, s:1, b:0),
% 9.15/9.52 aReductOfIn0 [40, 3] (w:1, o:69, a:1, s:1, b:0),
% 9.15/9.52 iLess0 [41, 2] (w:1, o:57, a:1, s:1, b:0),
% 9.15/9.52 sdtmndtplgtdt0 [42, 3] (w:1, o:70, a:1, s:1, b:0),
% 9.15/9.52 sdtmndtasgtdt0 [44, 3] (w:1, o:71, a:1, s:1, b:0),
% 9.15/9.52 isConfluent0 [45, 1] (w:1, o:20, a:1, s:1, b:0),
% 9.15/9.52 isLocallyConfluent0 [47, 1] (w:1, o:21, a:1, s:1, b:0),
% 9.15/9.52 isTerminating0 [48, 1] (w:1, o:22, a:1, s:1, b:0),
% 9.15/9.52 aNormalFormOfIn0 [49, 3] (w:1, o:72, a:1, s:1, b:0),
% 9.15/9.52 xR [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 9.15/9.52 alpha1 [51, 3] (w:1, o:73, a:1, s:1, b:1),
% 9.15/9.52 alpha2 [52, 3] (w:1, o:75, a:1, s:1, b:1),
% 9.15/9.52 alpha3 [53, 3] (w:1, o:76, a:1, s:1, b:1),
% 9.15/9.52 alpha4 [54, 2] (w:1, o:58, a:1, s:1, b:1),
% 9.15/9.52 alpha5 [55, 3] (w:1, o:77, a:1, s:1, b:1),
% 9.15/9.52 alpha6 [56, 4] (w:1, o:85, a:1, s:1, b:1),
% 9.15/9.52 alpha7 [57, 3] (w:1, o:78, a:1, s:1, b:1),
% 9.15/9.52 alpha8 [58, 4] (w:1, o:86, a:1, s:1, b:1),
% 9.15/9.52 alpha9 [59, 3] (w:1, o:79, a:1, s:1, b:1),
% 9.15/9.52 alpha10 [60, 4] (w:1, o:87, a:1, s:1, b:1),
% 9.15/9.52 alpha11 [61, 3] (w:1, o:74, a:1, s:1, b:1),
% 9.15/9.52 alpha12 [62, 4] (w:1, o:88, a:1, s:1, b:1),
% 9.15/9.52 alpha13 [63, 4] (w:1, o:89, a:1, s:1, b:1),
% 9.15/9.52 alpha14 [64, 4] (w:1, o:90, a:1, s:1, b:1),
% 9.15/9.52 alpha15 [65, 4] (w:1, o:91, a:1, s:1, b:1),
% 9.15/9.52 alpha16 [66, 4] (w:1, o:92, a:1, s:1, b:1),
% 9.15/9.52 alpha17 [67, 4] (w:1, o:93, a:1, s:1, b:1),
% 9.15/9.52 alpha18 [68, 1] (w:1, o:23, a:1, s:1, b:1),
% 9.15/9.52 alpha19 [69, 2] (w:1, o:59, a:1, s:1, b:1),
% 9.15/9.52 alpha20 [70, 2] (w:1, o:60, a:1, s:1, b:1),
% 9.15/9.52 alpha21 [71, 2] (w:1, o:61, a:1, s:1, b:1),
% 9.15/9.52 alpha22 [72, 2] (w:1, o:62, a:1, s:1, b:1),
% 9.15/9.52 alpha23 [73, 2] (w:1, o:63, a:1, s:1, b:1),
% 9.15/9.52 alpha24 [74, 2] (w:1, o:64, a:1, s:1, b:1),
% 9.15/9.52 alpha25 [75, 2] (w:1, o:65, a:1, s:1, b:1),
% 9.15/9.52 alpha26 [76, 2] (w:1, o:66, a:1, s:1, b:1),
% 9.15/9.52 skol1 [77, 3] (w:1, o:80, a:1, s:1, b:1),
% 9.15/9.52 skol2 [78, 1] (w:1, o:30, a:1, s:1, b:1),
% 9.15/9.52 skol3 [79, 3] (w:1, o:81, a:1, s:1, b:1),
% 9.15/9.52 skol4 [80, 3] (w:1, o:82, a:1, s:1, b:1),
% 9.15/9.52 skol5 [81, 1] (w:1, o:31, a:1, s:1, b:1),
% 9.15/9.52 skol6 [82, 3] (w:1, o:83, a:1, s:1, b:1),
% 9.15/9.52 skol7 [83, 3] (w:1, o:84, a:1, s:1, b:1),
% 9.15/9.52 skol8 [84, 1] (w:1, o:32, a:1, s:1, b:1),
% 9.15/9.52 skol9 [85, 2] (w:1, o:67, a:1, s:1, b:1),
% 9.15/9.52 skol10 [86, 0] (w:1, o:12, a:1, s:1, b:1),
% 9.15/9.52 skol11 [87, 1] (w:1, o:24, a:1, s:1, b:1),
% 9.15/9.52 skol12 [88, 1] (w:1, o:25, a:1, s:1, b:1),
% 9.15/9.52 skol13 [89, 2] (w:1, o:68, a:1, s:1, b:1),
% 9.15/9.52 skol14 [90, 1] (w:1, o:26, a:1, s:1, b:1),
% 9.15/9.52 skol15 [91, 1] (w:1, o:27, a:1, s:1, b:1),
% 9.15/9.52 skol16 [92, 1] (w:1, o:28, a:1, s:1, b:1),
% 9.15/9.52 skol17 [93, 1] (w:1, o:29, a:1, s:1, b:1).
% 9.15/9.52
% 9.15/9.52
% 9.15/9.52 Starting Search:
% 9.15/9.52
% 9.15/9.52 *** allocated 15000 integers for clauses
% 40.85/41.26 *** allocated 22500 integers for clauses
% 40.85/41.26 *** allocated 15000 integers for termspace/termends
% 40.85/41.26 *** allocated 33750 integers for clauses
% 40.85/41.26 *** allocated 22500 integers for termspace/termends
% 40.85/41.26 *** allocated 50625 integers for clauses
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 75937 integers for clauses
% 40.85/41.26 *** allocated 33750 integers for termspace/termends
% 40.85/41.26 *** allocated 113905 integers for clauses
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 5220
% 40.85/41.26 Kept: 2020
% 40.85/41.26 Inuse: 245
% 40.85/41.26 Deleted: 9
% 40.85/41.26 Deletedinuse: 3
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 50625 integers for termspace/termends
% 40.85/41.26 *** allocated 170857 integers for clauses
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 75937 integers for termspace/termends
% 40.85/41.26 *** allocated 256285 integers for clauses
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 9569
% 40.85/41.26 Kept: 4185
% 40.85/41.26 Inuse: 357
% 40.85/41.26 Deleted: 15
% 40.85/41.26 Deletedinuse: 6
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 113905 integers for termspace/termends
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 384427 integers for clauses
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 17551
% 40.85/41.26 Kept: 6202
% 40.85/41.26 Inuse: 537
% 40.85/41.26 Deleted: 30
% 40.85/41.26 Deletedinuse: 10
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 170857 integers for termspace/termends
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 31916
% 40.85/41.26 Kept: 8204
% 40.85/41.26 Inuse: 746
% 40.85/41.26 Deleted: 47
% 40.85/41.26 Deletedinuse: 16
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 576640 integers for clauses
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 45429
% 40.85/41.26 Kept: 10279
% 40.85/41.26 Inuse: 986
% 40.85/41.26 Deleted: 71
% 40.85/41.26 Deletedinuse: 17
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 74656
% 40.85/41.26 Kept: 12285
% 40.85/41.26 Inuse: 1203
% 40.85/41.26 Deleted: 80
% 40.85/41.26 Deletedinuse: 19
% 40.85/41.26
% 40.85/41.26 *** allocated 256285 integers for termspace/termends
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 864960 integers for clauses
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 87067
% 40.85/41.26 Kept: 14290
% 40.85/41.26 Inuse: 1323
% 40.85/41.26 Deleted: 88
% 40.85/41.26 Deletedinuse: 19
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 100480
% 40.85/41.26 Kept: 16305
% 40.85/41.26 Inuse: 1359
% 40.85/41.26 Deleted: 90
% 40.85/41.26 Deletedinuse: 19
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 123431
% 40.85/41.26 Kept: 18369
% 40.85/41.26 Inuse: 1415
% 40.85/41.26 Deleted: 93
% 40.85/41.26 Deletedinuse: 21
% 40.85/41.26
% 40.85/41.26 *** allocated 384427 integers for termspace/termends
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying clauses:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 1297440 integers for clauses
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 158332
% 40.85/41.26 Kept: 20377
% 40.85/41.26 Inuse: 1525
% 40.85/41.26 Deleted: 1320
% 40.85/41.26 Deletedinuse: 21
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 186773
% 40.85/41.26 Kept: 22397
% 40.85/41.26 Inuse: 1704
% 40.85/41.26 Deleted: 1326
% 40.85/41.26 Deletedinuse: 27
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 207071
% 40.85/41.26 Kept: 24399
% 40.85/41.26 Inuse: 1812
% 40.85/41.26 Deleted: 1336
% 40.85/41.26 Deletedinuse: 29
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 218856
% 40.85/41.26 Kept: 26434
% 40.85/41.26 Inuse: 1860
% 40.85/41.26 Deleted: 1336
% 40.85/41.26 Deletedinuse: 29
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 576640 integers for termspace/termends
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 235504
% 40.85/41.26 Kept: 28466
% 40.85/41.26 Inuse: 1907
% 40.85/41.26 Deleted: 1336
% 40.85/41.26 Deletedinuse: 29
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 277721
% 40.85/41.26 Kept: 30477
% 40.85/41.26 Inuse: 2037
% 40.85/41.26 Deleted: 1338
% 40.85/41.26 Deletedinuse: 29
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 *** allocated 1946160 integers for clauses
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 296637
% 40.85/41.26 Kept: 32526
% 40.85/41.26 Inuse: 2112
% 40.85/41.26 Deleted: 1338
% 40.85/41.26 Deletedinuse: 29
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 312282
% 40.85/41.26 Kept: 34534
% 40.85/41.26 Inuse: 2174
% 40.85/41.26 Deleted: 1338
% 40.85/41.26 Deletedinuse: 29
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26 Resimplifying inuse:
% 40.85/41.26 Done
% 40.85/41.26
% 40.85/41.26
% 40.85/41.26 Intermediate Status:
% 40.85/41.26 Generated: 344113
% 40.85/41.26 Kept: 36599
% 40.85/41.26 Inuse: 2300
% 40.85/41.26 Deleted: 1341
% 40.85/41.26 Deletedinuse: 31
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 381671
% 70.15/70.53 Kept: 38716
% 70.15/70.53 Inuse: 2441
% 70.15/70.53 Deleted: 1360
% 70.15/70.53 Deletedinuse: 48
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying clauses:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 401375
% 70.15/70.53 Kept: 40797
% 70.15/70.53 Inuse: 2525
% 70.15/70.53 Deleted: 3193
% 70.15/70.53 Deletedinuse: 50
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 *** allocated 864960 integers for termspace/termends
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 419906
% 70.15/70.53 Kept: 42805
% 70.15/70.53 Inuse: 2608
% 70.15/70.53 Deleted: 3193
% 70.15/70.53 Deletedinuse: 50
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 438551
% 70.15/70.53 Kept: 44844
% 70.15/70.53 Inuse: 2732
% 70.15/70.53 Deleted: 3196
% 70.15/70.53 Deletedinuse: 53
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 *** allocated 2919240 integers for clauses
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 470350
% 70.15/70.53 Kept: 46902
% 70.15/70.53 Inuse: 2851
% 70.15/70.53 Deleted: 3197
% 70.15/70.53 Deletedinuse: 54
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 491129
% 70.15/70.53 Kept: 48904
% 70.15/70.53 Inuse: 2958
% 70.15/70.53 Deleted: 3199
% 70.15/70.53 Deletedinuse: 54
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 498482
% 70.15/70.53 Kept: 50904
% 70.15/70.53 Inuse: 3014
% 70.15/70.53 Deleted: 3199
% 70.15/70.53 Deletedinuse: 54
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 515633
% 70.15/70.53 Kept: 52992
% 70.15/70.53 Inuse: 3094
% 70.15/70.53 Deleted: 3201
% 70.15/70.53 Deletedinuse: 56
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 526455
% 70.15/70.53 Kept: 55054
% 70.15/70.53 Inuse: 3163
% 70.15/70.53 Deleted: 3202
% 70.15/70.53 Deletedinuse: 57
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 541966
% 70.15/70.53 Kept: 57084
% 70.15/70.53 Inuse: 3260
% 70.15/70.53 Deleted: 3210
% 70.15/70.53 Deletedinuse: 59
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 559541
% 70.15/70.53 Kept: 59119
% 70.15/70.53 Inuse: 3338
% 70.15/70.53 Deleted: 3210
% 70.15/70.53 Deletedinuse: 59
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying clauses:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 572333
% 70.15/70.53 Kept: 61140
% 70.15/70.53 Inuse: 3385
% 70.15/70.53 Deleted: 4347
% 70.15/70.53 Deletedinuse: 61
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 *** allocated 1297440 integers for termspace/termends
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 585353
% 70.15/70.53 Kept: 63273
% 70.15/70.53 Inuse: 3462
% 70.15/70.53 Deleted: 4347
% 70.15/70.53 Deletedinuse: 61
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 595281
% 70.15/70.53 Kept: 65379
% 70.15/70.53 Inuse: 3481
% 70.15/70.53 Deleted: 4347
% 70.15/70.53 Deletedinuse: 61
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 641440
% 70.15/70.53 Kept: 67406
% 70.15/70.53 Inuse: 3745
% 70.15/70.53 Deleted: 4347
% 70.15/70.53 Deletedinuse: 61
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 *** allocated 4378860 integers for clauses
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 698309
% 70.15/70.53 Kept: 69406
% 70.15/70.53 Inuse: 4007
% 70.15/70.53 Deleted: 4347
% 70.15/70.53 Deletedinuse: 61
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 727990
% 70.15/70.53 Kept: 71468
% 70.15/70.53 Inuse: 4048
% 70.15/70.53 Deleted: 4347
% 70.15/70.53 Deletedinuse: 61
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 741707
% 70.15/70.53 Kept: 73480
% 70.15/70.53 Inuse: 4078
% 70.15/70.53 Deleted: 4347
% 70.15/70.53 Deletedinuse: 61
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 767764
% 70.15/70.53 Kept: 75547
% 70.15/70.53 Inuse: 4126
% 70.15/70.53 Deleted: 4549
% 70.15/70.53 Deletedinuse: 261
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 784909
% 70.15/70.53 Kept: 77552
% 70.15/70.53 Inuse: 4156
% 70.15/70.53 Deleted: 4549
% 70.15/70.53 Deletedinuse: 261
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 811302
% 70.15/70.53 Kept: 79649
% 70.15/70.53 Inuse: 4212
% 70.15/70.53 Deleted: 4549
% 70.15/70.53 Deletedinuse: 261
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying clauses:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 848099
% 70.15/70.53 Kept: 81665
% 70.15/70.53 Inuse: 4296
% 70.15/70.53 Deleted: 12276
% 70.15/70.53 Deletedinuse: 261
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 874431
% 70.15/70.53 Kept: 83666
% 70.15/70.53 Inuse: 4407
% 70.15/70.53 Deleted: 12278
% 70.15/70.53 Deletedinuse: 263
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 907395
% 70.15/70.53 Kept: 85673
% 70.15/70.53 Inuse: 4528
% 70.15/70.53 Deleted: 12283
% 70.15/70.53 Deletedinuse: 263
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 939680
% 70.15/70.53 Kept: 87740
% 70.15/70.53 Inuse: 4612
% 70.15/70.53 Deleted: 12283
% 70.15/70.53 Deletedinuse: 263
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 958604
% 70.15/70.53 Kept: 89756
% 70.15/70.53 Inuse: 4664
% 70.15/70.53 Deleted: 12283
% 70.15/70.53 Deletedinuse: 263
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 998102
% 70.15/70.53 Kept: 91767
% 70.15/70.53 Inuse: 4824
% 70.15/70.53 Deleted: 12283
% 70.15/70.53 Deletedinuse: 263
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 1069509
% 70.15/70.53 Kept: 93898
% 70.15/70.53 Inuse: 5033
% 70.15/70.53 Deleted: 12283
% 70.15/70.53 Deletedinuse: 263
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 *** allocated 1946160 integers for termspace/termends
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 1092728
% 70.15/70.53 Kept: 95917
% 70.15/70.53 Inuse: 5108
% 70.15/70.53 Deleted: 12283
% 70.15/70.53 Deletedinuse: 263
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 1105812
% 70.15/70.53 Kept: 97989
% 70.15/70.53 Inuse: 5163
% 70.15/70.53 Deleted: 12283
% 70.15/70.53 Deletedinuse: 263
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 1128590
% 70.15/70.53 Kept: 99999
% 70.15/70.53 Inuse: 5232
% 70.15/70.53 Deleted: 12283
% 70.15/70.53 Deletedinuse: 263
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying clauses:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Intermediate Status:
% 70.15/70.53 Generated: 1163509
% 70.15/70.53 Kept: 102037
% 70.15/70.53 Inuse: 5348
% 70.15/70.53 Deleted: 13246
% 70.15/70.53 Deletedinuse: 263
% 70.15/70.53
% 70.15/70.53 Resimplifying inuse:
% 70.15/70.53 Done
% 70.15/70.53
% 70.15/70.53
% 70.15/70.53 Bliksems!, er is een bewijs:
% 70.15/70.53 % SZS status Theorem
% 70.15/70.53 % SZS output start Refutation
% 70.15/70.53
% 70.15/70.53 (1) {G0,W10,D2,L4,V3,M4} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 70.15/70.53 aReductOfIn0( Z, X, Y ), aElement0( Z ) }.
% 70.15/70.53 (3) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 70.15/70.54 aElement0( Z ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z ) }.
% 70.15/70.54 (4) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 70.15/70.54 aElement0( Z ), ! alpha1( X, Y, Z ), sdtmndtplgtdt0( X, Y, Z ) }.
% 70.15/70.54 (7) {G0,W11,D2,L3,V4,M3} I { ! aElement0( T ), ! alpha6( X, Y, Z, T ),
% 70.15/70.54 alpha1( X, Y, Z ) }.
% 70.15/70.54 (8) {G0,W9,D2,L2,V4,M2} I { ! alpha6( X, Y, Z, T ), aReductOfIn0( T, X, Y )
% 70.15/70.54 }.
% 70.15/70.54 (10) {G0,W13,D2,L3,V4,M3} I { ! aReductOfIn0( T, X, Y ), ! sdtmndtplgtdt0(
% 70.15/70.54 T, Y, Z ), alpha6( X, Y, Z, T ) }.
% 70.15/70.54 (13) {G0,W13,D2,L5,V3,M5} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 70.15/70.54 aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y, Z ) }.
% 70.15/70.54 (14) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 70.15/70.54 aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z )
% 70.15/70.54 }.
% 70.15/70.54 (15) {G0,W20,D2,L7,V4,M7} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 70.15/70.54 aElement0( Z ), ! aElement0( T ), ! sdtmndtasgtdt0( X, Y, Z ), !
% 70.15/70.54 sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X, Y, T ) }.
% 70.15/70.54 (73) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 70.15/70.54 (74) {G0,W11,D2,L4,V2,M4} I { ! aElement0( X ), ! aElement0( Y ), !
% 70.15/70.54 aReductOfIn0( Y, X, xR ), iLess0( Y, X ) }.
% 70.15/70.54 (78) {G0,W2,D2,L1,V0,M1} I { aElement0( skol10 ) }.
% 70.15/70.54 (79) {G0,W7,D2,L3,V1,M3} I { ! aElement0( X ), ! iLess0( X, skol10 ),
% 70.15/70.54 alpha18( X ) }.
% 70.15/70.54 (80) {G0,W10,D3,L3,V1,M3} I { ! aElement0( X ), alpha19( skol10, X ),
% 70.15/70.54 aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 (82) {G0,W11,D3,L3,V1,M3} I { ! aElement0( X ), ! sdtmndtplgtdt0( skol10,
% 70.15/70.54 xR, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 (83) {G0,W11,D3,L3,V1,M3} I { ! aElement0( X ), ! sdtmndtasgtdt0( skol10,
% 70.15/70.54 xR, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 (85) {G0,W6,D2,L2,V2,M2} I { ! alpha19( X, Y ), ! X = Y }.
% 70.15/70.54 (87) {G0,W10,D2,L3,V2,M3} I { X = Y, aReductOfIn0( Y, X, xR ), alpha19( X,
% 70.15/70.54 Y ) }.
% 70.15/70.54 (88) {G0,W6,D3,L2,V1,M2} I { ! alpha18( X ), alpha20( X, skol11( X ) ) }.
% 70.15/70.54 (91) {G0,W6,D2,L2,V2,M2} I { ! alpha20( X, Y ), alpha21( X, Y ) }.
% 70.15/70.54 (92) {G0,W7,D2,L2,V3,M2} I { ! alpha20( X, Y ), ! aReductOfIn0( Z, Y, xR )
% 70.15/70.54 }.
% 70.15/70.54 (94) {G0,W6,D2,L2,V2,M2} I { ! alpha21( X, Y ), alpha22( X, Y ) }.
% 70.15/70.54 (97) {G0,W5,D2,L2,V2,M2} I { ! alpha22( X, Y ), aElement0( Y ) }.
% 70.15/70.54 (98) {G0,W6,D2,L2,V2,M2} I { ! alpha22( X, Y ), alpha23( X, Y ) }.
% 70.15/70.54 (100) {G0,W9,D2,L3,V2,M3} I { ! alpha23( X, Y ), X = Y, alpha24( X, Y ) }.
% 70.15/70.54 (101) {G0,W6,D2,L2,V2,M2} I { ! X = Y, alpha23( X, Y ) }.
% 70.15/70.54 (104) {G0,W7,D2,L2,V2,M2} I { ! alpha24( X, Y ), sdtmndtplgtdt0( X, xR, Y )
% 70.15/70.54 }.
% 70.15/70.54 (128) {G1,W3,D2,L1,V1,M1} Q(85) { ! alpha19( X, X ) }.
% 70.15/70.54 (129) {G1,W3,D2,L1,V1,M1} Q(101) { alpha23( X, X ) }.
% 70.15/70.54 (131) {G1,W8,D2,L3,V2,M3} R(1,73) { ! aElement0( X ), ! aReductOfIn0( Y, X
% 70.15/70.54 , xR ), aElement0( Y ) }.
% 70.15/70.54 (132) {G1,W8,D2,L3,V2,M3} R(1,78) { ! aRewritingSystem0( X ), !
% 70.15/70.54 aReductOfIn0( Y, skol10, X ), aElement0( Y ) }.
% 70.15/70.54 (161) {G1,W20,D2,L7,V5,M7} R(3,1) { ! aElement0( X ), ! aRewritingSystem0(
% 70.15/70.54 Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z ), ! aElement0( T
% 70.15/70.54 ), ! aRewritingSystem0( U ), ! aReductOfIn0( Z, T, U ) }.
% 70.15/70.54 (166) {G2,W12,D2,L4,V3,M4} F(161);f;f { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ) }.
% 70.15/70.54 (176) {G1,W12,D2,L4,V2,M4} R(4,78) { ! aRewritingSystem0( X ), ! aElement0
% 70.15/70.54 ( Y ), ! alpha1( skol10, X, Y ), sdtmndtplgtdt0( skol10, X, Y ) }.
% 70.15/70.54 (179) {G1,W6,D2,L2,V2,M2} R(94,98) { ! alpha21( X, Y ), alpha23( X, Y ) }.
% 70.15/70.54 (181) {G1,W5,D2,L2,V2,M2} R(94,97) { ! alpha21( X, Y ), aElement0( Y ) }.
% 70.15/70.54 (195) {G2,W6,D2,L2,V2,M2} R(91,179) { ! alpha20( X, Y ), alpha23( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 (196) {G2,W5,D2,L2,V2,M2} R(91,181) { ! alpha20( X, Y ), aElement0( Y ) }.
% 70.15/70.54 (217) {G3,W6,D3,L2,V1,M2} R(88,195) { ! alpha18( X ), alpha23( X, skol11( X
% 70.15/70.54 ) ) }.
% 70.15/70.54 (219) {G3,W5,D3,L2,V1,M2} R(88,196) { ! alpha18( X ), aElement0( skol11( X
% 70.15/70.54 ) ) }.
% 70.15/70.54 (262) {G1,W7,D3,L2,V2,M2} R(92,88) { ! aReductOfIn0( X, skol11( Y ), xR ),
% 70.15/70.54 ! alpha18( Y ) }.
% 70.15/70.54 (276) {G1,W12,D2,L3,V3,M3} R(104,10) { ! alpha24( X, Y ), ! aReductOfIn0( X
% 70.15/70.54 , Z, xR ), alpha6( Z, xR, Y, X ) }.
% 70.15/70.54 (504) {G1,W19,D2,L7,V4,M7} R(15,13);f;f;f { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, T ), ! Z = T }.
% 70.15/70.54 (1297) {G2,W6,D2,L2,V1,M2} R(131,78) { ! aReductOfIn0( X, skol10, xR ),
% 70.15/70.54 aElement0( X ) }.
% 70.15/70.54 (1323) {G3,W7,D2,L2,V2,M2} R(1297,8) { aElement0( X ), ! alpha6( skol10, xR
% 70.15/70.54 , Y, X ) }.
% 70.15/70.54 (1349) {G4,W14,D2,L3,V5,M3} R(1323,7) { ! alpha6( skol10, xR, X, Y ), !
% 70.15/70.54 alpha6( Z, T, U, Y ), alpha1( Z, T, U ) }.
% 70.15/70.54 (1352) {G5,W9,D2,L2,V2,M2} F(1349) { ! alpha6( skol10, xR, X, Y ), alpha1(
% 70.15/70.54 skol10, xR, X ) }.
% 70.15/70.54 (2805) {G3,W7,D2,L2,V1,M2} R(74,78);r(1297) { ! aReductOfIn0( X, skol10, xR
% 70.15/70.54 ), iLess0( X, skol10 ) }.
% 70.15/70.54 (3004) {G4,W6,D2,L2,V1,M2} R(2805,79);r(1297) { ! aReductOfIn0( X, skol10,
% 70.15/70.54 xR ), alpha18( X ) }.
% 70.15/70.54 (3023) {G5,W7,D2,L2,V2,M2} R(3004,8) { alpha18( X ), ! alpha6( skol10, xR,
% 70.15/70.54 Y, X ) }.
% 70.15/70.54 (3121) {G2,W5,D3,L1,V0,M1} R(80,128);r(78) { aReductOfIn0( skol17( skol10 )
% 70.15/70.54 , skol10, xR ) }.
% 70.15/70.54 (3125) {G5,W3,D3,L1,V0,M1} R(3121,3004) { alpha18( skol17( skol10 ) ) }.
% 70.15/70.54 (3130) {G3,W3,D3,L1,V0,M1} R(3121,132);r(73) { aElement0( skol17( skol10 )
% 70.15/70.54 ) }.
% 70.15/70.54 (3148) {G6,W6,D4,L1,V1,M1} R(3125,262) { ! aReductOfIn0( X, skol11( skol17
% 70.15/70.54 ( skol10 ) ), xR ) }.
% 70.15/70.54 (3152) {G6,W6,D4,L1,V0,M1} R(3125,217) { alpha23( skol17( skol10 ), skol11
% 70.15/70.54 ( skol17( skol10 ) ) ) }.
% 70.15/70.54 (3154) {G6,W4,D4,L1,V0,M1} R(3125,219) { aElement0( skol11( skol17( skol10
% 70.15/70.54 ) ) ) }.
% 70.15/70.54 (3173) {G4,W7,D3,L2,V1,M2} R(3130,131) { ! aReductOfIn0( X, skol17( skol10
% 70.15/70.54 ), xR ), aElement0( X ) }.
% 70.15/70.54 (3229) {G4,W7,D3,L2,V1,M2} R(82,262);r(219) { ! sdtmndtplgtdt0( skol10, xR
% 70.15/70.54 , skol11( X ) ), ! alpha18( X ) }.
% 70.15/70.54 (3291) {G7,W6,D4,L1,V0,M1} R(83,3154);r(3148) { ! sdtmndtasgtdt0( skol10,
% 70.15/70.54 xR, skol11( skol17( skol10 ) ) ) }.
% 70.15/70.54 (3391) {G5,W6,D3,L2,V1,M2} P(87,3130);r(3173) { aElement0( X ), alpha19(
% 70.15/70.54 skol17( skol10 ), X ) }.
% 70.15/70.54 (5227) {G6,W6,D3,L2,V1,M2} R(3391,85) { aElement0( X ), ! skol17( skol10 )
% 70.15/70.54 = X }.
% 70.15/70.54 (5799) {G7,W12,D4,L2,V0,M2} R(3152,100) { skol11( skol17( skol10 ) ) ==>
% 70.15/70.54 skol17( skol10 ), alpha24( skol17( skol10 ), skol11( skol17( skol10 ) ) )
% 70.15/70.54 }.
% 70.15/70.54 (6859) {G3,W7,D3,L2,V0,M2} R(166,3121);r(78) { ! aRewritingSystem0( xR ),
% 70.15/70.54 sdtmndtplgtdt0( skol10, xR, skol17( skol10 ) ) }.
% 70.15/70.54 (8721) {G5,W10,D3,L3,V1,M3} R(3229,176);r(73) { ! alpha18( X ), ! aElement0
% 70.15/70.54 ( skol11( X ) ), ! alpha1( skol10, xR, skol11( X ) ) }.
% 70.15/70.54 (8979) {G4,W5,D3,L1,V0,M1} S(6859);r(73) { sdtmndtplgtdt0( skol10, xR,
% 70.15/70.54 skol17( skol10 ) ) }.
% 70.15/70.54 (8991) {G5,W10,D3,L3,V0,M3} R(8979,14);r(78) { ! aRewritingSystem0( xR ), !
% 70.15/70.54 aElement0( skol17( skol10 ) ), sdtmndtasgtdt0( skol10, xR, skol17(
% 70.15/70.54 skol10 ) ) }.
% 70.15/70.54 (20159) {G6,W5,D3,L1,V0,M1} S(8991);r(73);r(3130) { sdtmndtasgtdt0( skol10
% 70.15/70.54 , xR, skol17( skol10 ) ) }.
% 70.15/70.54 (20167) {G6,W7,D3,L2,V1,M2} S(8721);r(219) { ! alpha18( X ), ! alpha1(
% 70.15/70.54 skol10, xR, skol11( X ) ) }.
% 70.15/70.54 (28033) {G7,W15,D3,L5,V1,M5} R(504,20159);r(78) { ! aRewritingSystem0( xR )
% 70.15/70.54 , ! aElement0( skol17( skol10 ) ), ! aElement0( X ), sdtmndtasgtdt0(
% 70.15/70.54 skol10, xR, X ), ! skol17( skol10 ) = X }.
% 70.15/70.54 (40414) {G8,W8,D3,L2,V1,M2} S(28033);r(73);r(3130);r(5227) { sdtmndtasgtdt0
% 70.15/70.54 ( skol10, xR, X ), ! skol17( skol10 ) = X }.
% 70.15/70.54 (54437) {G9,W6,D4,L1,V0,M1} R(40414,3291) { ! skol11( skol17( skol10 ) )
% 70.15/70.54 ==> skol17( skol10 ) }.
% 70.15/70.54 (54467) {G10,W14,D4,L3,V1,M3} P(100,54437) { ! X = skol17( skol10 ), !
% 70.15/70.54 alpha23( X, skol11( skol17( skol10 ) ) ), alpha24( X, skol11( skol17(
% 70.15/70.54 skol10 ) ) ) }.
% 70.15/70.54 (54472) {G11,W6,D4,L1,V0,M1} Q(54467);d(5799);r(129) { alpha24( skol17(
% 70.15/70.54 skol10 ), skol11( skol17( skol10 ) ) ) }.
% 70.15/70.54 (102658) {G7,W8,D3,L2,V2,M2} R(1352,20167) { ! alpha6( skol10, xR, skol11(
% 70.15/70.54 X ), Y ), ! alpha18( X ) }.
% 70.15/70.54 (102770) {G8,W11,D3,L2,V3,M2} R(102658,3023) { ! alpha6( skol10, xR, skol11
% 70.15/70.54 ( X ), Y ), ! alpha6( skol10, xR, Z, X ) }.
% 70.15/70.54 (102783) {G9,W6,D3,L1,V1,M1} F(102770) { ! alpha6( skol10, xR, skol11( X )
% 70.15/70.54 , X ) }.
% 70.15/70.54 (102785) {G10,W8,D3,L2,V1,M2} R(102783,276) { ! alpha24( X, skol11( X ) ),
% 70.15/70.54 ! aReductOfIn0( X, skol10, xR ) }.
% 70.15/70.54 (102802) {G12,W0,D0,L0,V0,M0} R(102785,54472);r(3121) { }.
% 70.15/70.54
% 70.15/70.54
% 70.15/70.54 % SZS output end Refutation
% 70.15/70.54 found a proof!
% 70.15/70.54
% 70.15/70.54
% 70.15/70.54 Unprocessed initial clauses:
% 70.15/70.54
% 70.15/70.54 (102804) {G0,W1,D1,L1,V0,M1} { && }.
% 70.15/70.54 (102805) {G0,W1,D1,L1,V0,M1} { && }.
% 70.15/70.54 (102806) {G0,W10,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aReductOfIn0( Z, X, Y ), aElement0( Z ) }.
% 70.15/70.54 (102807) {G0,W1,D1,L1,V0,M1} { && }.
% 70.15/70.54 (102808) {G0,W1,D1,L1,V0,M1} { && }.
% 70.15/70.54 (102809) {G0,W18,D2,L6,V3,M6} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ), aReductOfIn0( Z, X, Y )
% 70.15/70.54 , alpha1( X, Y, Z ) }.
% 70.15/70.54 (102810) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aElement0( Z ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z )
% 70.15/70.54 }.
% 70.15/70.54 (102811) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aElement0( Z ), ! alpha1( X, Y, Z ), sdtmndtplgtdt0( X, Y, Z ) }.
% 70.15/70.54 (102812) {G0,W9,D3,L2,V6,M2} { ! alpha1( X, Y, Z ), aElement0( skol1( T, U
% 70.15/70.54 , W ) ) }.
% 70.15/70.54 (102813) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), alpha6( X, Y, Z,
% 70.15/70.54 skol1( X, Y, Z ) ) }.
% 70.15/70.54 (102814) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha6( X, Y, Z, T ),
% 70.15/70.54 alpha1( X, Y, Z ) }.
% 70.15/70.54 (102815) {G0,W9,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), aReductOfIn0( T, X
% 70.15/70.54 , Y ) }.
% 70.15/70.54 (102816) {G0,W9,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), sdtmndtplgtdt0( T,
% 70.15/70.54 Y, Z ) }.
% 70.15/70.54 (102817) {G0,W13,D2,L3,V4,M3} { ! aReductOfIn0( T, X, Y ), !
% 70.15/70.54 sdtmndtplgtdt0( T, Y, Z ), alpha6( X, Y, Z, T ) }.
% 70.15/70.54 (102818) {G0,W20,D2,L7,V4,M7} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aElement0( Z ), ! aElement0( T ), ! sdtmndtplgtdt0( X, Y, Z ), !
% 70.15/70.54 sdtmndtplgtdt0( Z, Y, T ), sdtmndtplgtdt0( X, Y, T ) }.
% 70.15/70.54 (102819) {G0,W17,D2,L6,V3,M6} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aElement0( Z ), ! sdtmndtasgtdt0( X, Y, Z ), X = Z, sdtmndtplgtdt0( X
% 70.15/70.54 , Y, Z ) }.
% 70.15/70.54 (102820) {G0,W13,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y, Z ) }.
% 70.15/70.54 (102821) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z
% 70.15/70.54 ) }.
% 70.15/70.54 (102822) {G0,W20,D2,L7,V4,M7} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aElement0( Z ), ! aElement0( T ), ! sdtmndtasgtdt0( X, Y, Z ), !
% 70.15/70.54 sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X, Y, T ) }.
% 70.15/70.54 (102823) {G0,W12,D2,L4,V3,M4} { ! aRewritingSystem0( X ), ! isConfluent0(
% 70.15/70.54 X ), ! alpha2( X, Y, Z ), alpha7( X, Y, Z ) }.
% 70.15/70.54 (102824) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha2( X, skol2
% 70.15/70.54 ( X ), skol14( X ) ), isConfluent0( X ) }.
% 70.15/70.54 (102825) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha7( X,
% 70.15/70.54 skol2( X ), skol14( X ) ), isConfluent0( X ) }.
% 70.15/70.54 (102826) {G0,W9,D3,L2,V6,M2} { ! alpha7( X, Y, Z ), aElement0( skol3( T, U
% 70.15/70.54 , W ) ) }.
% 70.15/70.54 (102827) {G0,W12,D3,L2,V3,M2} { ! alpha7( X, Y, Z ), alpha12( X, Y, Z,
% 70.15/70.54 skol3( X, Y, Z ) ) }.
% 70.15/70.54 (102828) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha12( X, Y, Z, T )
% 70.15/70.54 , alpha7( X, Y, Z ) }.
% 70.15/70.54 (102829) {G0,W9,D2,L2,V4,M2} { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Y
% 70.15/70.54 , X, T ) }.
% 70.15/70.54 (102830) {G0,W9,D2,L2,V4,M2} { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Z
% 70.15/70.54 , X, T ) }.
% 70.15/70.54 (102831) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( Y, X, T ), !
% 70.15/70.54 sdtmndtasgtdt0( Z, X, T ), alpha12( X, Y, Z, T ) }.
% 70.15/70.54 (102832) {G0,W9,D3,L2,V6,M2} { ! alpha2( X, Y, Z ), aElement0( skol4( T, U
% 70.15/70.54 , W ) ) }.
% 70.15/70.54 (102833) {G0,W12,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), alpha8( X, Y, Z,
% 70.15/70.54 skol4( X, Y, Z ) ) }.
% 70.15/70.54 (102834) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha8( X, Y, Z, T ),
% 70.15/70.54 alpha2( X, Y, Z ) }.
% 70.15/70.54 (102835) {G0,W7,D2,L2,V4,M2} { ! alpha8( X, Y, Z, T ), aElement0( Y ) }.
% 70.15/70.54 (102836) {G0,W10,D2,L2,V4,M2} { ! alpha8( X, Y, Z, T ), alpha13( X, Y, Z,
% 70.15/70.54 T ) }.
% 70.15/70.54 (102837) {G0,W12,D2,L3,V4,M3} { ! aElement0( Y ), ! alpha13( X, Y, Z, T )
% 70.15/70.54 , alpha8( X, Y, Z, T ) }.
% 70.15/70.54 (102838) {G0,W7,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), aElement0( Z ) }.
% 70.15/70.54 (102839) {G0,W10,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), alpha16( X, Y, Z
% 70.15/70.54 , T ) }.
% 70.15/70.54 (102840) {G0,W12,D2,L3,V4,M3} { ! aElement0( Z ), ! alpha16( X, Y, Z, T )
% 70.15/70.54 , alpha13( X, Y, Z, T ) }.
% 70.15/70.54 (102841) {G0,W9,D2,L2,V4,M2} { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T
% 70.15/70.54 , X, Y ) }.
% 70.15/70.54 (102842) {G0,W9,D2,L2,V4,M2} { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T
% 70.15/70.54 , X, Z ) }.
% 70.15/70.54 (102843) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( T, X, Y ), !
% 70.15/70.54 sdtmndtasgtdt0( T, X, Z ), alpha16( X, Y, Z, T ) }.
% 70.15/70.54 (102844) {G0,W12,D2,L4,V3,M4} { ! aRewritingSystem0( X ), !
% 70.15/70.54 isLocallyConfluent0( X ), ! alpha3( X, Y, Z ), alpha9( X, Y, Z ) }.
% 70.15/70.54 (102845) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha3( X, skol5
% 70.15/70.54 ( X ), skol15( X ) ), isLocallyConfluent0( X ) }.
% 70.15/70.54 (102846) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha9( X,
% 70.15/70.54 skol5( X ), skol15( X ) ), isLocallyConfluent0( X ) }.
% 70.15/70.54 (102847) {G0,W9,D3,L2,V6,M2} { ! alpha9( X, Y, Z ), aElement0( skol6( T, U
% 70.15/70.54 , W ) ) }.
% 70.15/70.54 (102848) {G0,W12,D3,L2,V3,M2} { ! alpha9( X, Y, Z ), alpha14( X, Y, Z,
% 70.15/70.54 skol6( X, Y, Z ) ) }.
% 70.15/70.54 (102849) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha14( X, Y, Z, T )
% 70.15/70.54 , alpha9( X, Y, Z ) }.
% 70.15/70.54 (102850) {G0,W9,D2,L2,V4,M2} { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Y
% 70.15/70.54 , X, T ) }.
% 70.15/70.54 (102851) {G0,W9,D2,L2,V4,M2} { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Z
% 70.15/70.54 , X, T ) }.
% 70.15/70.54 (102852) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( Y, X, T ), !
% 70.15/70.54 sdtmndtasgtdt0( Z, X, T ), alpha14( X, Y, Z, T ) }.
% 70.15/70.54 (102853) {G0,W9,D3,L2,V6,M2} { ! alpha3( X, Y, Z ), aElement0( skol7( T, U
% 70.15/70.54 , W ) ) }.
% 70.15/70.54 (102854) {G0,W12,D3,L2,V3,M2} { ! alpha3( X, Y, Z ), alpha10( X, Y, Z,
% 70.15/70.54 skol7( X, Y, Z ) ) }.
% 70.15/70.54 (102855) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha10( X, Y, Z, T )
% 70.15/70.54 , alpha3( X, Y, Z ) }.
% 70.15/70.54 (102856) {G0,W7,D2,L2,V4,M2} { ! alpha10( X, Y, Z, T ), aElement0( Y ) }.
% 70.15/70.54 (102857) {G0,W10,D2,L2,V4,M2} { ! alpha10( X, Y, Z, T ), alpha15( X, Y, Z
% 70.15/70.54 , T ) }.
% 70.15/70.54 (102858) {G0,W12,D2,L3,V4,M3} { ! aElement0( Y ), ! alpha15( X, Y, Z, T )
% 70.15/70.54 , alpha10( X, Y, Z, T ) }.
% 70.15/70.54 (102859) {G0,W7,D2,L2,V4,M2} { ! alpha15( X, Y, Z, T ), aElement0( Z ) }.
% 70.15/70.54 (102860) {G0,W10,D2,L2,V4,M2} { ! alpha15( X, Y, Z, T ), alpha17( X, Y, Z
% 70.15/70.54 , T ) }.
% 70.15/70.54 (102861) {G0,W12,D2,L3,V4,M3} { ! aElement0( Z ), ! alpha17( X, Y, Z, T )
% 70.15/70.54 , alpha15( X, Y, Z, T ) }.
% 70.15/70.54 (102862) {G0,W9,D2,L2,V4,M2} { ! alpha17( X, Y, Z, T ), aReductOfIn0( Y, T
% 70.15/70.54 , X ) }.
% 70.15/70.54 (102863) {G0,W9,D2,L2,V4,M2} { ! alpha17( X, Y, Z, T ), aReductOfIn0( Z, T
% 70.15/70.54 , X ) }.
% 70.15/70.54 (102864) {G0,W13,D2,L3,V4,M3} { ! aReductOfIn0( Y, T, X ), ! aReductOfIn0
% 70.15/70.54 ( Z, T, X ), alpha17( X, Y, Z, T ) }.
% 70.15/70.54 (102865) {G0,W11,D2,L4,V3,M4} { ! aRewritingSystem0( X ), ! isTerminating0
% 70.15/70.54 ( X ), ! alpha4( Y, Z ), alpha11( X, Y, Z ) }.
% 70.15/70.54 (102866) {G0,W9,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha4( skol8( X
% 70.15/70.54 ), skol16( X ) ), isTerminating0( X ) }.
% 70.15/70.54 (102867) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha11( X,
% 70.15/70.54 skol8( X ), skol16( X ) ), isTerminating0( X ) }.
% 70.15/70.54 (102868) {G0,W11,D2,L3,V3,M3} { ! alpha11( X, Y, Z ), ! sdtmndtplgtdt0( Y
% 70.15/70.54 , X, Z ), iLess0( Z, Y ) }.
% 70.15/70.54 (102869) {G0,W8,D2,L2,V3,M2} { sdtmndtplgtdt0( Y, X, Z ), alpha11( X, Y, Z
% 70.15/70.54 ) }.
% 70.15/70.54 (102870) {G0,W7,D2,L2,V3,M2} { ! iLess0( Z, Y ), alpha11( X, Y, Z ) }.
% 70.15/70.54 (102871) {G0,W5,D2,L2,V2,M2} { ! alpha4( X, Y ), aElement0( X ) }.
% 70.15/70.54 (102872) {G0,W5,D2,L2,V2,M2} { ! alpha4( X, Y ), aElement0( Y ) }.
% 70.15/70.54 (102873) {G0,W7,D2,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y ), alpha4
% 70.15/70.54 ( X, Y ) }.
% 70.15/70.54 (102874) {G0,W10,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aNormalFormOfIn0( Z, X, Y ), aElement0( Z ) }.
% 70.15/70.54 (102875) {G0,W12,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aNormalFormOfIn0( Z, X, Y ), alpha5( X, Y, Z ) }.
% 70.15/70.54 (102876) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 70.15/70.54 , ! aElement0( Z ), ! alpha5( X, Y, Z ), aNormalFormOfIn0( Z, X, Y ) }.
% 70.15/70.54 (102877) {G0,W8,D2,L2,V3,M2} { ! alpha5( X, Y, Z ), sdtmndtasgtdt0( X, Y,
% 70.15/70.54 Z ) }.
% 70.15/70.54 (102878) {G0,W8,D2,L2,V4,M2} { ! alpha5( X, Y, Z ), ! aReductOfIn0( T, Z,
% 70.15/70.54 Y ) }.
% 70.15/70.54 (102879) {G0,W14,D3,L3,V3,M3} { ! sdtmndtasgtdt0( X, Y, Z ), aReductOfIn0
% 70.15/70.54 ( skol9( Y, Z ), Z, Y ), alpha5( X, Y, Z ) }.
% 70.15/70.54 (102880) {G0,W2,D2,L1,V0,M1} { aRewritingSystem0( xR ) }.
% 70.15/70.54 (102881) {G0,W11,D2,L4,V2,M4} { ! aElement0( X ), ! aElement0( Y ), !
% 70.15/70.54 aReductOfIn0( Y, X, xR ), iLess0( Y, X ) }.
% 70.15/70.54 (102882) {G0,W17,D2,L6,V3,M6} { ! aElement0( X ), ! aElement0( Y ), !
% 70.15/70.54 aElement0( Z ), ! aReductOfIn0( Z, X, xR ), ! sdtmndtplgtdt0( Z, xR, Y )
% 70.15/70.54 , iLess0( Y, X ) }.
% 70.15/70.54 (102883) {G0,W11,D2,L4,V2,M4} { ! aElement0( X ), ! aElement0( Y ), !
% 70.15/70.54 sdtmndtplgtdt0( X, xR, Y ), iLess0( Y, X ) }.
% 70.15/70.54 (102884) {G0,W2,D2,L1,V0,M1} { isTerminating0( xR ) }.
% 70.15/70.54 (102885) {G0,W2,D2,L1,V0,M1} { aElement0( skol10 ) }.
% 70.15/70.54 (102886) {G0,W7,D2,L3,V1,M3} { ! aElement0( X ), ! iLess0( X, skol10 ),
% 70.15/70.54 alpha18( X ) }.
% 70.15/70.54 (102887) {G0,W10,D3,L3,V1,M3} { ! aElement0( X ), alpha19( skol10, X ),
% 70.15/70.54 aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 (102888) {G0,W17,D3,L5,V2,M5} { ! aElement0( X ), ! aElement0( Y ), !
% 70.15/70.54 aReductOfIn0( Y, skol10, xR ), ! sdtmndtplgtdt0( Y, xR, X ), aReductOfIn0
% 70.15/70.54 ( skol17( X ), X, xR ) }.
% 70.15/70.54 (102889) {G0,W11,D3,L3,V1,M3} { ! aElement0( X ), ! sdtmndtplgtdt0( skol10
% 70.15/70.54 , xR, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 (102890) {G0,W11,D3,L3,V1,M3} { ! aElement0( X ), ! sdtmndtasgtdt0( skol10
% 70.15/70.54 , xR, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 (102891) {G0,W4,D2,L1,V1,M1} { ! aNormalFormOfIn0( X, skol10, xR ) }.
% 70.15/70.54 (102892) {G0,W6,D2,L2,V2,M2} { ! alpha19( X, Y ), ! X = Y }.
% 70.15/70.54 (102893) {G0,W7,D2,L2,V2,M2} { ! alpha19( X, Y ), ! aReductOfIn0( Y, X, xR
% 70.15/70.54 ) }.
% 70.15/70.54 (102894) {G0,W10,D2,L3,V2,M3} { X = Y, aReductOfIn0( Y, X, xR ), alpha19(
% 70.15/70.54 X, Y ) }.
% 70.15/70.54 (102895) {G0,W6,D3,L2,V1,M2} { ! alpha18( X ), alpha20( X, skol11( X ) )
% 70.15/70.54 }.
% 70.15/70.54 (102896) {G0,W7,D3,L2,V1,M2} { ! alpha18( X ), aNormalFormOfIn0( skol11( X
% 70.15/70.54 ), X, xR ) }.
% 70.15/70.54 (102897) {G0,W9,D2,L3,V2,M3} { ! alpha20( X, Y ), ! aNormalFormOfIn0( Y, X
% 70.15/70.54 , xR ), alpha18( X ) }.
% 70.15/70.54 (102898) {G0,W6,D2,L2,V2,M2} { ! alpha20( X, Y ), alpha21( X, Y ) }.
% 70.15/70.54 (102899) {G0,W7,D2,L2,V3,M2} { ! alpha20( X, Y ), ! aReductOfIn0( Z, Y, xR
% 70.15/70.54 ) }.
% 70.15/70.54 (102900) {G0,W11,D3,L3,V2,M3} { ! alpha21( X, Y ), aReductOfIn0( skol12( Y
% 70.15/70.54 ), Y, xR ), alpha20( X, Y ) }.
% 70.15/70.54 (102901) {G0,W6,D2,L2,V2,M2} { ! alpha21( X, Y ), alpha22( X, Y ) }.
% 70.15/70.54 (102902) {G0,W7,D2,L2,V2,M2} { ! alpha21( X, Y ), sdtmndtasgtdt0( X, xR, Y
% 70.15/70.54 ) }.
% 70.15/70.54 (102903) {G0,W10,D2,L3,V2,M3} { ! alpha22( X, Y ), ! sdtmndtasgtdt0( X, xR
% 70.15/70.54 , Y ), alpha21( X, Y ) }.
% 70.15/70.54 (102904) {G0,W5,D2,L2,V2,M2} { ! alpha22( X, Y ), aElement0( Y ) }.
% 70.15/70.54 (102905) {G0,W6,D2,L2,V2,M2} { ! alpha22( X, Y ), alpha23( X, Y ) }.
% 70.15/70.54 (102906) {G0,W8,D2,L3,V2,M3} { ! aElement0( Y ), ! alpha23( X, Y ),
% 70.15/70.54 alpha22( X, Y ) }.
% 70.15/70.54 (102907) {G0,W9,D2,L3,V2,M3} { ! alpha23( X, Y ), X = Y, alpha24( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 (102908) {G0,W6,D2,L2,V2,M2} { ! X = Y, alpha23( X, Y ) }.
% 70.15/70.54 (102909) {G0,W6,D2,L2,V2,M2} { ! alpha24( X, Y ), alpha23( X, Y ) }.
% 70.15/70.54 (102910) {G0,W6,D2,L2,V2,M2} { ! alpha24( X, Y ), alpha25( X, Y ) }.
% 70.15/70.54 (102911) {G0,W7,D2,L2,V2,M2} { ! alpha24( X, Y ), sdtmndtplgtdt0( X, xR, Y
% 70.15/70.54 ) }.
% 70.15/70.54 (102912) {G0,W10,D2,L3,V2,M3} { ! alpha25( X, Y ), ! sdtmndtplgtdt0( X, xR
% 70.15/70.54 , Y ), alpha24( X, Y ) }.
% 70.15/70.54 (102913) {G0,W10,D2,L3,V2,M3} { ! alpha25( X, Y ), aReductOfIn0( Y, X, xR
% 70.15/70.54 ), alpha26( X, Y ) }.
% 70.15/70.54 (102914) {G0,W7,D2,L2,V2,M2} { ! aReductOfIn0( Y, X, xR ), alpha25( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 (102915) {G0,W6,D2,L2,V2,M2} { ! alpha26( X, Y ), alpha25( X, Y ) }.
% 70.15/70.54 (102916) {G0,W7,D3,L2,V4,M2} { ! alpha26( X, Y ), aElement0( skol13( Z, T
% 70.15/70.54 ) ) }.
% 70.15/70.54 (102917) {G0,W9,D3,L2,V3,M2} { ! alpha26( X, Y ), sdtmndtplgtdt0( skol13(
% 70.15/70.54 Z, Y ), xR, Y ) }.
% 70.15/70.54 (102918) {G0,W9,D3,L2,V2,M2} { ! alpha26( X, Y ), aReductOfIn0( skol13( X
% 70.15/70.54 , Y ), X, xR ) }.
% 70.15/70.54 (102919) {G0,W13,D2,L4,V3,M4} { ! aElement0( Z ), ! aReductOfIn0( Z, X, xR
% 70.15/70.54 ), ! sdtmndtplgtdt0( Z, xR, Y ), alpha26( X, Y ) }.
% 70.15/70.54
% 70.15/70.54
% 70.15/70.54 Total Proof:
% 70.15/70.54
% 70.15/70.54 subsumption: (1) {G0,W10,D2,L4,V3,M4} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), aElement0( Z ) }.
% 70.15/70.54 parent0: (102806) {G0,W10,D2,L4,V3,M4} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), aElement0( Z ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 3 ==> 3
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (3) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aReductOfIn0( Z, X, Y ),
% 70.15/70.54 sdtmndtplgtdt0( X, Y, Z ) }.
% 70.15/70.54 parent0: (102810) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aReductOfIn0( Z, X, Y ),
% 70.15/70.54 sdtmndtplgtdt0( X, Y, Z ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 3 ==> 3
% 70.15/70.54 4 ==> 4
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (4) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha1( X, Y, Z ),
% 70.15/70.54 sdtmndtplgtdt0( X, Y, Z ) }.
% 70.15/70.54 parent0: (102811) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha1( X, Y, Z ),
% 70.15/70.54 sdtmndtplgtdt0( X, Y, Z ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 3 ==> 3
% 70.15/70.54 4 ==> 4
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (7) {G0,W11,D2,L3,V4,M3} I { ! aElement0( T ), ! alpha6( X, Y
% 70.15/70.54 , Z, T ), alpha1( X, Y, Z ) }.
% 70.15/70.54 parent0: (102814) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha6( X, Y
% 70.15/70.54 , Z, T ), alpha1( X, Y, Z ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 T := T
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (8) {G0,W9,D2,L2,V4,M2} I { ! alpha6( X, Y, Z, T ),
% 70.15/70.54 aReductOfIn0( T, X, Y ) }.
% 70.15/70.54 parent0: (102815) {G0,W9,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ),
% 70.15/70.54 aReductOfIn0( T, X, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 T := T
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (10) {G0,W13,D2,L3,V4,M3} I { ! aReductOfIn0( T, X, Y ), !
% 70.15/70.54 sdtmndtplgtdt0( T, Y, Z ), alpha6( X, Y, Z, T ) }.
% 70.15/70.54 parent0: (102817) {G0,W13,D2,L3,V4,M3} { ! aReductOfIn0( T, X, Y ), !
% 70.15/70.54 sdtmndtplgtdt0( T, Y, Z ), alpha6( X, Y, Z, T ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 T := T
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (13) {G0,W13,D2,L5,V3,M5} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y,
% 70.15/70.54 Z ) }.
% 70.15/70.54 parent0: (102820) {G0,W13,D2,L5,V3,M5} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y,
% 70.15/70.54 Z ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 3 ==> 3
% 70.15/70.54 4 ==> 4
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (14) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ),
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ) }.
% 70.15/70.54 parent0: (102821) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ),
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 3 ==> 3
% 70.15/70.54 4 ==> 4
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (15) {G0,W20,D2,L7,V4,M7} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), ! sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X
% 70.15/70.54 , Y, T ) }.
% 70.15/70.54 parent0: (102822) {G0,W20,D2,L7,V4,M7} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), ! sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X
% 70.15/70.54 , Y, T ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 T := T
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 3 ==> 3
% 70.15/70.54 4 ==> 4
% 70.15/70.54 5 ==> 5
% 70.15/70.54 6 ==> 6
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (73) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 70.15/70.54 parent0: (102880) {G0,W2,D2,L1,V0,M1} { aRewritingSystem0( xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (74) {G0,W11,D2,L4,V2,M4} I { ! aElement0( X ), ! aElement0( Y
% 70.15/70.54 ), ! aReductOfIn0( Y, X, xR ), iLess0( Y, X ) }.
% 70.15/70.54 parent0: (102881) {G0,W11,D2,L4,V2,M4} { ! aElement0( X ), ! aElement0( Y
% 70.15/70.54 ), ! aReductOfIn0( Y, X, xR ), iLess0( Y, X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 3 ==> 3
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( skol10 ) }.
% 70.15/70.54 parent0: (102885) {G0,W2,D2,L1,V0,M1} { aElement0( skol10 ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (79) {G0,W7,D2,L3,V1,M3} I { ! aElement0( X ), ! iLess0( X,
% 70.15/70.54 skol10 ), alpha18( X ) }.
% 70.15/70.54 parent0: (102886) {G0,W7,D2,L3,V1,M3} { ! aElement0( X ), ! iLess0( X,
% 70.15/70.54 skol10 ), alpha18( X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (80) {G0,W10,D3,L3,V1,M3} I { ! aElement0( X ), alpha19(
% 70.15/70.54 skol10, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 parent0: (102887) {G0,W10,D3,L3,V1,M3} { ! aElement0( X ), alpha19( skol10
% 70.15/70.54 , X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (82) {G0,W11,D3,L3,V1,M3} I { ! aElement0( X ), !
% 70.15/70.54 sdtmndtplgtdt0( skol10, xR, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 parent0: (102889) {G0,W11,D3,L3,V1,M3} { ! aElement0( X ), !
% 70.15/70.54 sdtmndtplgtdt0( skol10, xR, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (83) {G0,W11,D3,L3,V1,M3} I { ! aElement0( X ), !
% 70.15/70.54 sdtmndtasgtdt0( skol10, xR, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 parent0: (102890) {G0,W11,D3,L3,V1,M3} { ! aElement0( X ), !
% 70.15/70.54 sdtmndtasgtdt0( skol10, xR, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (85) {G0,W6,D2,L2,V2,M2} I { ! alpha19( X, Y ), ! X = Y }.
% 70.15/70.54 parent0: (102892) {G0,W6,D2,L2,V2,M2} { ! alpha19( X, Y ), ! X = Y }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (87) {G0,W10,D2,L3,V2,M3} I { X = Y, aReductOfIn0( Y, X, xR )
% 70.15/70.54 , alpha19( X, Y ) }.
% 70.15/70.54 parent0: (102894) {G0,W10,D2,L3,V2,M3} { X = Y, aReductOfIn0( Y, X, xR ),
% 70.15/70.54 alpha19( X, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (88) {G0,W6,D3,L2,V1,M2} I { ! alpha18( X ), alpha20( X,
% 70.15/70.54 skol11( X ) ) }.
% 70.15/70.54 parent0: (102895) {G0,W6,D3,L2,V1,M2} { ! alpha18( X ), alpha20( X, skol11
% 70.15/70.54 ( X ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (91) {G0,W6,D2,L2,V2,M2} I { ! alpha20( X, Y ), alpha21( X, Y
% 70.15/70.54 ) }.
% 70.15/70.54 parent0: (102898) {G0,W6,D2,L2,V2,M2} { ! alpha20( X, Y ), alpha21( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (92) {G0,W7,D2,L2,V3,M2} I { ! alpha20( X, Y ), ! aReductOfIn0
% 70.15/70.54 ( Z, Y, xR ) }.
% 70.15/70.54 parent0: (102899) {G0,W7,D2,L2,V3,M2} { ! alpha20( X, Y ), ! aReductOfIn0
% 70.15/70.54 ( Z, Y, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (94) {G0,W6,D2,L2,V2,M2} I { ! alpha21( X, Y ), alpha22( X, Y
% 70.15/70.54 ) }.
% 70.15/70.54 parent0: (102901) {G0,W6,D2,L2,V2,M2} { ! alpha21( X, Y ), alpha22( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (97) {G0,W5,D2,L2,V2,M2} I { ! alpha22( X, Y ), aElement0( Y )
% 70.15/70.54 }.
% 70.15/70.54 parent0: (102904) {G0,W5,D2,L2,V2,M2} { ! alpha22( X, Y ), aElement0( Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (98) {G0,W6,D2,L2,V2,M2} I { ! alpha22( X, Y ), alpha23( X, Y
% 70.15/70.54 ) }.
% 70.15/70.54 parent0: (102905) {G0,W6,D2,L2,V2,M2} { ! alpha22( X, Y ), alpha23( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (100) {G0,W9,D2,L3,V2,M3} I { ! alpha23( X, Y ), X = Y,
% 70.15/70.54 alpha24( X, Y ) }.
% 70.15/70.54 parent0: (102907) {G0,W9,D2,L3,V2,M3} { ! alpha23( X, Y ), X = Y, alpha24
% 70.15/70.54 ( X, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (101) {G0,W6,D2,L2,V2,M2} I { ! X = Y, alpha23( X, Y ) }.
% 70.15/70.54 parent0: (102908) {G0,W6,D2,L2,V2,M2} { ! X = Y, alpha23( X, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (104) {G0,W7,D2,L2,V2,M2} I { ! alpha24( X, Y ),
% 70.15/70.54 sdtmndtplgtdt0( X, xR, Y ) }.
% 70.15/70.54 parent0: (102911) {G0,W7,D2,L2,V2,M2} { ! alpha24( X, Y ), sdtmndtplgtdt0
% 70.15/70.54 ( X, xR, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 eqswap: (103585) {G0,W6,D2,L2,V2,M2} { ! Y = X, ! alpha19( X, Y ) }.
% 70.15/70.54 parent0[1]: (85) {G0,W6,D2,L2,V2,M2} I { ! alpha19( X, Y ), ! X = Y }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 eqrefl: (103586) {G0,W3,D2,L1,V1,M1} { ! alpha19( X, X ) }.
% 70.15/70.54 parent0[0]: (103585) {G0,W6,D2,L2,V2,M2} { ! Y = X, ! alpha19( X, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (128) {G1,W3,D2,L1,V1,M1} Q(85) { ! alpha19( X, X ) }.
% 70.15/70.54 parent0: (103586) {G0,W3,D2,L1,V1,M1} { ! alpha19( X, X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 eqswap: (103587) {G0,W6,D2,L2,V2,M2} { ! Y = X, alpha23( X, Y ) }.
% 70.15/70.54 parent0[0]: (101) {G0,W6,D2,L2,V2,M2} I { ! X = Y, alpha23( X, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 eqrefl: (103588) {G0,W3,D2,L1,V1,M1} { alpha23( X, X ) }.
% 70.15/70.54 parent0[0]: (103587) {G0,W6,D2,L2,V2,M2} { ! Y = X, alpha23( X, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (129) {G1,W3,D2,L1,V1,M1} Q(101) { alpha23( X, X ) }.
% 70.15/70.54 parent0: (103588) {G0,W3,D2,L1,V1,M1} { alpha23( X, X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103589) {G1,W8,D2,L3,V2,M3} { ! aElement0( X ), !
% 70.15/70.54 aReductOfIn0( Y, X, xR ), aElement0( Y ) }.
% 70.15/70.54 parent0[1]: (1) {G0,W10,D2,L4,V3,M4} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), aElement0( Z ) }.
% 70.15/70.54 parent1[0]: (73) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := xR
% 70.15/70.54 Z := Y
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (131) {G1,W8,D2,L3,V2,M3} R(1,73) { ! aElement0( X ), !
% 70.15/70.54 aReductOfIn0( Y, X, xR ), aElement0( Y ) }.
% 70.15/70.54 parent0: (103589) {G1,W8,D2,L3,V2,M3} { ! aElement0( X ), ! aReductOfIn0(
% 70.15/70.54 Y, X, xR ), aElement0( Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103590) {G1,W8,D2,L3,V2,M3} { ! aRewritingSystem0( X ), !
% 70.15/70.54 aReductOfIn0( Y, skol10, X ), aElement0( Y ) }.
% 70.15/70.54 parent0[0]: (1) {G0,W10,D2,L4,V3,M4} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), aElement0( Z ) }.
% 70.15/70.54 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( skol10 ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := skol10
% 70.15/70.54 Y := X
% 70.15/70.54 Z := Y
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (132) {G1,W8,D2,L3,V2,M3} R(1,78) { ! aRewritingSystem0( X ),
% 70.15/70.54 ! aReductOfIn0( Y, skol10, X ), aElement0( Y ) }.
% 70.15/70.54 parent0: (103590) {G1,W8,D2,L3,V2,M3} { ! aRewritingSystem0( X ), !
% 70.15/70.54 aReductOfIn0( Y, skol10, X ), aElement0( Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103592) {G1,W20,D2,L7,V5,M7} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ), ! aElement0( T ), ! aRewritingSystem0( U ), ! aReductOfIn0( Z, T, U
% 70.15/70.54 ) }.
% 70.15/70.54 parent0[2]: (3) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aReductOfIn0( Z, X, Y ),
% 70.15/70.54 sdtmndtplgtdt0( X, Y, Z ) }.
% 70.15/70.54 parent1[3]: (1) {G0,W10,D2,L4,V3,M4} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), aElement0( Z ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := T
% 70.15/70.54 Y := U
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (161) {G1,W20,D2,L7,V5,M7} R(3,1) { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ), ! aElement0( T ), ! aRewritingSystem0( U ), ! aReductOfIn0( Z, T, U
% 70.15/70.54 ) }.
% 70.15/70.54 parent0: (103592) {G1,W20,D2,L7,V5,M7} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ), ! aElement0( T ), ! aRewritingSystem0( U ), ! aReductOfIn0( Z, T, U
% 70.15/70.54 ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 T := X
% 70.15/70.54 U := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 3 ==> 3
% 70.15/70.54 4 ==> 0
% 70.15/70.54 5 ==> 1
% 70.15/70.54 6 ==> 2
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 factor: (103604) {G1,W16,D2,L6,V3,M6} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ), ! aElement0( X ), ! aRewritingSystem0( Y ) }.
% 70.15/70.54 parent0[2, 6]: (161) {G1,W20,D2,L7,V5,M7} R(3,1) { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ), ! aElement0( T ), ! aRewritingSystem0( U ), ! aReductOfIn0( Z, T, U
% 70.15/70.54 ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 T := X
% 70.15/70.54 U := Y
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 factor: (103605) {G1,W14,D2,L5,V3,M5} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ), ! aRewritingSystem0( Y ) }.
% 70.15/70.54 parent0[0, 4]: (103604) {G1,W16,D2,L6,V3,M6} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ), ! aElement0( X ), ! aRewritingSystem0( Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 factor: (103606) {G1,W12,D2,L4,V3,M4} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ) }.
% 70.15/70.54 parent0[1, 4]: (103605) {G1,W14,D2,L5,V3,M5} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ), ! aRewritingSystem0( Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (166) {G2,W12,D2,L4,V3,M4} F(161);f;f { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ) }.
% 70.15/70.54 parent0: (103606) {G1,W12,D2,L4,V3,M4} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y,
% 70.15/70.54 Z ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 3 ==> 3
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103607) {G1,W12,D2,L4,V2,M4} { ! aRewritingSystem0( X ), !
% 70.15/70.54 aElement0( Y ), ! alpha1( skol10, X, Y ), sdtmndtplgtdt0( skol10, X, Y )
% 70.15/70.54 }.
% 70.15/70.54 parent0[0]: (4) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha1( X, Y, Z ),
% 70.15/70.54 sdtmndtplgtdt0( X, Y, Z ) }.
% 70.15/70.54 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( skol10 ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := skol10
% 70.15/70.54 Y := X
% 70.15/70.54 Z := Y
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (176) {G1,W12,D2,L4,V2,M4} R(4,78) { ! aRewritingSystem0( X )
% 70.15/70.54 , ! aElement0( Y ), ! alpha1( skol10, X, Y ), sdtmndtplgtdt0( skol10, X,
% 70.15/70.54 Y ) }.
% 70.15/70.54 parent0: (103607) {G1,W12,D2,L4,V2,M4} { ! aRewritingSystem0( X ), !
% 70.15/70.54 aElement0( Y ), ! alpha1( skol10, X, Y ), sdtmndtplgtdt0( skol10, X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 2 ==> 2
% 70.15/70.54 3 ==> 3
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103609) {G1,W6,D2,L2,V2,M2} { alpha23( X, Y ), ! alpha21( X,
% 70.15/70.54 Y ) }.
% 70.15/70.54 parent0[0]: (98) {G0,W6,D2,L2,V2,M2} I { ! alpha22( X, Y ), alpha23( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 parent1[1]: (94) {G0,W6,D2,L2,V2,M2} I { ! alpha21( X, Y ), alpha22( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (179) {G1,W6,D2,L2,V2,M2} R(94,98) { ! alpha21( X, Y ),
% 70.15/70.54 alpha23( X, Y ) }.
% 70.15/70.54 parent0: (103609) {G1,W6,D2,L2,V2,M2} { alpha23( X, Y ), ! alpha21( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 1
% 70.15/70.54 1 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103610) {G1,W5,D2,L2,V2,M2} { aElement0( Y ), ! alpha21( X, Y
% 70.15/70.54 ) }.
% 70.15/70.54 parent0[0]: (97) {G0,W5,D2,L2,V2,M2} I { ! alpha22( X, Y ), aElement0( Y )
% 70.15/70.54 }.
% 70.15/70.54 parent1[1]: (94) {G0,W6,D2,L2,V2,M2} I { ! alpha21( X, Y ), alpha22( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (181) {G1,W5,D2,L2,V2,M2} R(94,97) { ! alpha21( X, Y ),
% 70.15/70.54 aElement0( Y ) }.
% 70.15/70.54 parent0: (103610) {G1,W5,D2,L2,V2,M2} { aElement0( Y ), ! alpha21( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 1
% 70.15/70.54 1 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103611) {G1,W6,D2,L2,V2,M2} { alpha23( X, Y ), ! alpha20( X,
% 70.15/70.54 Y ) }.
% 70.15/70.54 parent0[0]: (179) {G1,W6,D2,L2,V2,M2} R(94,98) { ! alpha21( X, Y ), alpha23
% 70.15/70.54 ( X, Y ) }.
% 70.15/70.54 parent1[1]: (91) {G0,W6,D2,L2,V2,M2} I { ! alpha20( X, Y ), alpha21( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (195) {G2,W6,D2,L2,V2,M2} R(91,179) { ! alpha20( X, Y ),
% 70.15/70.54 alpha23( X, Y ) }.
% 70.15/70.54 parent0: (103611) {G1,W6,D2,L2,V2,M2} { alpha23( X, Y ), ! alpha20( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 1
% 70.15/70.54 1 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103612) {G1,W5,D2,L2,V2,M2} { aElement0( Y ), ! alpha20( X, Y
% 70.15/70.54 ) }.
% 70.15/70.54 parent0[0]: (181) {G1,W5,D2,L2,V2,M2} R(94,97) { ! alpha21( X, Y ),
% 70.15/70.54 aElement0( Y ) }.
% 70.15/70.54 parent1[1]: (91) {G0,W6,D2,L2,V2,M2} I { ! alpha20( X, Y ), alpha21( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (196) {G2,W5,D2,L2,V2,M2} R(91,181) { ! alpha20( X, Y ),
% 70.15/70.54 aElement0( Y ) }.
% 70.15/70.54 parent0: (103612) {G1,W5,D2,L2,V2,M2} { aElement0( Y ), ! alpha20( X, Y )
% 70.15/70.54 }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 1
% 70.15/70.54 1 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103613) {G1,W6,D3,L2,V1,M2} { alpha23( X, skol11( X ) ), !
% 70.15/70.54 alpha18( X ) }.
% 70.15/70.54 parent0[0]: (195) {G2,W6,D2,L2,V2,M2} R(91,179) { ! alpha20( X, Y ),
% 70.15/70.54 alpha23( X, Y ) }.
% 70.15/70.54 parent1[1]: (88) {G0,W6,D3,L2,V1,M2} I { ! alpha18( X ), alpha20( X, skol11
% 70.15/70.54 ( X ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := skol11( X )
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (217) {G3,W6,D3,L2,V1,M2} R(88,195) { ! alpha18( X ), alpha23
% 70.15/70.54 ( X, skol11( X ) ) }.
% 70.15/70.54 parent0: (103613) {G1,W6,D3,L2,V1,M2} { alpha23( X, skol11( X ) ), !
% 70.15/70.54 alpha18( X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 1
% 70.15/70.54 1 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103614) {G1,W5,D3,L2,V1,M2} { aElement0( skol11( X ) ), !
% 70.15/70.54 alpha18( X ) }.
% 70.15/70.54 parent0[0]: (196) {G2,W5,D2,L2,V2,M2} R(91,181) { ! alpha20( X, Y ),
% 70.15/70.54 aElement0( Y ) }.
% 70.15/70.54 parent1[1]: (88) {G0,W6,D3,L2,V1,M2} I { ! alpha18( X ), alpha20( X, skol11
% 70.15/70.54 ( X ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := skol11( X )
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (219) {G3,W5,D3,L2,V1,M2} R(88,196) { ! alpha18( X ),
% 70.15/70.54 aElement0( skol11( X ) ) }.
% 70.15/70.54 parent0: (103614) {G1,W5,D3,L2,V1,M2} { aElement0( skol11( X ) ), !
% 70.15/70.54 alpha18( X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 1
% 70.15/70.54 1 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103615) {G1,W7,D3,L2,V2,M2} { ! aReductOfIn0( Y, skol11( X )
% 70.15/70.54 , xR ), ! alpha18( X ) }.
% 70.15/70.54 parent0[0]: (92) {G0,W7,D2,L2,V3,M2} I { ! alpha20( X, Y ), ! aReductOfIn0
% 70.15/70.54 ( Z, Y, xR ) }.
% 70.15/70.54 parent1[1]: (88) {G0,W6,D3,L2,V1,M2} I { ! alpha18( X ), alpha20( X, skol11
% 70.15/70.54 ( X ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := skol11( X )
% 70.15/70.54 Z := Y
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (262) {G1,W7,D3,L2,V2,M2} R(92,88) { ! aReductOfIn0( X, skol11
% 70.15/70.54 ( Y ), xR ), ! alpha18( Y ) }.
% 70.15/70.54 parent0: (103615) {G1,W7,D3,L2,V2,M2} { ! aReductOfIn0( Y, skol11( X ), xR
% 70.15/70.54 ), ! alpha18( X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := Y
% 70.15/70.54 Y := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103616) {G1,W12,D2,L3,V3,M3} { ! aReductOfIn0( X, Y, xR ),
% 70.15/70.54 alpha6( Y, xR, Z, X ), ! alpha24( X, Z ) }.
% 70.15/70.54 parent0[1]: (10) {G0,W13,D2,L3,V4,M3} I { ! aReductOfIn0( T, X, Y ), !
% 70.15/70.54 sdtmndtplgtdt0( T, Y, Z ), alpha6( X, Y, Z, T ) }.
% 70.15/70.54 parent1[1]: (104) {G0,W7,D2,L2,V2,M2} I { ! alpha24( X, Y ), sdtmndtplgtdt0
% 70.15/70.54 ( X, xR, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := Y
% 70.15/70.54 Y := xR
% 70.15/70.54 Z := Z
% 70.15/70.54 T := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Z
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (276) {G1,W12,D2,L3,V3,M3} R(104,10) { ! alpha24( X, Y ), !
% 70.15/70.54 aReductOfIn0( X, Z, xR ), alpha6( Z, xR, Y, X ) }.
% 70.15/70.54 parent0: (103616) {G1,W12,D2,L3,V3,M3} { ! aReductOfIn0( X, Y, xR ),
% 70.15/70.54 alpha6( Y, xR, Z, X ), ! alpha24( X, Z ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Z
% 70.15/70.54 Z := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 1
% 70.15/70.54 1 ==> 2
% 70.15/70.54 2 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 eqswap: (103617) {G0,W13,D2,L5,V3,M5} { ! Y = X, ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Z ), ! aElement0( Y ), sdtmndtasgtdt0( X, Z, Y ) }.
% 70.15/70.54 parent0[3]: (13) {G0,W13,D2,L5,V3,M5} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y,
% 70.15/70.54 Z ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Z
% 70.15/70.54 Z := Y
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103619) {G1,W25,D2,L10,V4,M10} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, T ), ! T = Z, !
% 70.15/70.54 aElement0( Z ), ! aRewritingSystem0( Y ), ! aElement0( T ) }.
% 70.15/70.54 parent0[5]: (15) {G0,W20,D2,L7,V4,M7} I { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), ! sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X
% 70.15/70.54 , Y, T ) }.
% 70.15/70.54 parent1[4]: (103617) {G0,W13,D2,L5,V3,M5} { ! Y = X, ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Z ), ! aElement0( Y ), sdtmndtasgtdt0( X, Z, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 T := T
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := Z
% 70.15/70.54 Y := T
% 70.15/70.54 Z := Y
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 factor: (103622) {G1,W23,D2,L9,V4,M9} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, T ), ! T = Z, !
% 70.15/70.54 aElement0( Z ), ! aElement0( T ) }.
% 70.15/70.54 parent0[1, 8]: (103619) {G1,W25,D2,L10,V4,M10} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, T ), ! T = Z, !
% 70.15/70.54 aElement0( Z ), ! aRewritingSystem0( Y ), ! aElement0( T ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 T := T
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 factor: (103626) {G1,W21,D2,L8,V4,M8} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, T ), ! T = Z, !
% 70.15/70.54 aElement0( T ) }.
% 70.15/70.54 parent0[2, 7]: (103622) {G1,W23,D2,L9,V4,M9} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, T ), ! T = Z, !
% 70.15/70.54 aElement0( Z ), ! aElement0( T ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 T := T
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 factor: (103630) {G1,W19,D2,L7,V4,M7} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, T ), ! T = Z }.
% 70.15/70.54 parent0[3, 7]: (103626) {G1,W21,D2,L8,V4,M8} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, T ), ! T = Z, !
% 70.15/70.54 aElement0( T ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := Z
% 70.15/70.54 T := T
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 eqswap: (103666) {G1,W19,D2,L7,V4,M7} { ! Y = X, ! aElement0( Z ), !
% 70.15/70.54 aRewritingSystem0( T ), ! aElement0( Y ), ! aElement0( X ), !
% 70.15/70.54 sdtmndtasgtdt0( Z, T, Y ), sdtmndtasgtdt0( Z, T, X ) }.
% 70.15/70.54 parent0[6]: (103630) {G1,W19,D2,L7,V4,M7} { ! aElement0( X ), !
% 70.15/70.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, T ), ! T = Z }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := Z
% 70.15/70.54 Y := T
% 70.15/70.54 Z := Y
% 70.15/70.54 T := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (504) {G1,W19,D2,L7,V4,M7} R(15,13);f;f;f { ! aElement0( X ),
% 70.15/70.54 ! aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 70.15/70.54 sdtmndtasgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, T ), ! Z = T }.
% 70.15/70.54 parent0: (103666) {G1,W19,D2,L7,V4,M7} { ! Y = X, ! aElement0( Z ), !
% 70.15/70.54 aRewritingSystem0( T ), ! aElement0( Y ), ! aElement0( X ), !
% 70.15/70.54 sdtmndtasgtdt0( Z, T, Y ), sdtmndtasgtdt0( Z, T, X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := T
% 70.15/70.54 Y := Z
% 70.15/70.54 Z := X
% 70.15/70.54 T := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 6
% 70.15/70.54 1 ==> 0
% 70.15/70.54 2 ==> 1
% 70.15/70.54 3 ==> 2
% 70.15/70.54 4 ==> 3
% 70.15/70.54 5 ==> 4
% 70.15/70.54 6 ==> 5
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103670) {G1,W6,D2,L2,V1,M2} { ! aReductOfIn0( X, skol10, xR )
% 70.15/70.54 , aElement0( X ) }.
% 70.15/70.54 parent0[0]: (131) {G1,W8,D2,L3,V2,M3} R(1,73) { ! aElement0( X ), !
% 70.15/70.54 aReductOfIn0( Y, X, xR ), aElement0( Y ) }.
% 70.15/70.54 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( skol10 ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := skol10
% 70.15/70.54 Y := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (1297) {G2,W6,D2,L2,V1,M2} R(131,78) { ! aReductOfIn0( X,
% 70.15/70.54 skol10, xR ), aElement0( X ) }.
% 70.15/70.54 parent0: (103670) {G1,W6,D2,L2,V1,M2} { ! aReductOfIn0( X, skol10, xR ),
% 70.15/70.54 aElement0( X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103671) {G1,W7,D2,L2,V2,M2} { aElement0( X ), ! alpha6(
% 70.15/70.54 skol10, xR, Y, X ) }.
% 70.15/70.54 parent0[0]: (1297) {G2,W6,D2,L2,V1,M2} R(131,78) { ! aReductOfIn0( X,
% 70.15/70.54 skol10, xR ), aElement0( X ) }.
% 70.15/70.54 parent1[1]: (8) {G0,W9,D2,L2,V4,M2} I { ! alpha6( X, Y, Z, T ),
% 70.15/70.54 aReductOfIn0( T, X, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := skol10
% 70.15/70.54 Y := xR
% 70.15/70.54 Z := Y
% 70.15/70.54 T := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (1323) {G3,W7,D2,L2,V2,M2} R(1297,8) { aElement0( X ), !
% 70.15/70.54 alpha6( skol10, xR, Y, X ) }.
% 70.15/70.54 parent0: (103671) {G1,W7,D2,L2,V2,M2} { aElement0( X ), ! alpha6( skol10,
% 70.15/70.54 xR, Y, X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103672) {G1,W14,D2,L3,V5,M3} { ! alpha6( Y, Z, T, X ), alpha1
% 70.15/70.54 ( Y, Z, T ), ! alpha6( skol10, xR, U, X ) }.
% 70.15/70.54 parent0[0]: (7) {G0,W11,D2,L3,V4,M3} I { ! aElement0( T ), ! alpha6( X, Y,
% 70.15/70.54 Z, T ), alpha1( X, Y, Z ) }.
% 70.15/70.54 parent1[0]: (1323) {G3,W7,D2,L2,V2,M2} R(1297,8) { aElement0( X ), ! alpha6
% 70.15/70.54 ( skol10, xR, Y, X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := Y
% 70.15/70.54 Y := Z
% 70.15/70.54 Z := T
% 70.15/70.54 T := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 Y := U
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (1349) {G4,W14,D2,L3,V5,M3} R(1323,7) { ! alpha6( skol10, xR,
% 70.15/70.54 X, Y ), ! alpha6( Z, T, U, Y ), alpha1( Z, T, U ) }.
% 70.15/70.54 parent0: (103672) {G1,W14,D2,L3,V5,M3} { ! alpha6( Y, Z, T, X ), alpha1( Y
% 70.15/70.54 , Z, T ), ! alpha6( skol10, xR, U, X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := Y
% 70.15/70.54 Y := Z
% 70.15/70.54 Z := T
% 70.15/70.54 T := U
% 70.15/70.54 U := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 1
% 70.15/70.54 1 ==> 2
% 70.15/70.54 2 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 factor: (103674) {G4,W9,D2,L2,V2,M2} { ! alpha6( skol10, xR, X, Y ),
% 70.15/70.54 alpha1( skol10, xR, X ) }.
% 70.15/70.54 parent0[0, 1]: (1349) {G4,W14,D2,L3,V5,M3} R(1323,7) { ! alpha6( skol10, xR
% 70.15/70.54 , X, Y ), ! alpha6( Z, T, U, Y ), alpha1( Z, T, U ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 Z := skol10
% 70.15/70.54 T := xR
% 70.15/70.54 U := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (1352) {G5,W9,D2,L2,V2,M2} F(1349) { ! alpha6( skol10, xR, X,
% 70.15/70.54 Y ), alpha1( skol10, xR, X ) }.
% 70.15/70.54 parent0: (103674) {G4,W9,D2,L2,V2,M2} { ! alpha6( skol10, xR, X, Y ),
% 70.15/70.54 alpha1( skol10, xR, X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103675) {G1,W9,D2,L3,V1,M3} { ! aElement0( X ), !
% 70.15/70.54 aReductOfIn0( X, skol10, xR ), iLess0( X, skol10 ) }.
% 70.15/70.54 parent0[0]: (74) {G0,W11,D2,L4,V2,M4} I { ! aElement0( X ), ! aElement0( Y
% 70.15/70.54 ), ! aReductOfIn0( Y, X, xR ), iLess0( Y, X ) }.
% 70.15/70.54 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( skol10 ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := skol10
% 70.15/70.54 Y := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103677) {G2,W11,D2,L3,V1,M3} { ! aReductOfIn0( X, skol10, xR
% 70.15/70.54 ), iLess0( X, skol10 ), ! aReductOfIn0( X, skol10, xR ) }.
% 70.15/70.54 parent0[0]: (103675) {G1,W9,D2,L3,V1,M3} { ! aElement0( X ), !
% 70.15/70.54 aReductOfIn0( X, skol10, xR ), iLess0( X, skol10 ) }.
% 70.15/70.54 parent1[1]: (1297) {G2,W6,D2,L2,V1,M2} R(131,78) { ! aReductOfIn0( X,
% 70.15/70.54 skol10, xR ), aElement0( X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 factor: (103678) {G2,W7,D2,L2,V1,M2} { ! aReductOfIn0( X, skol10, xR ),
% 70.15/70.54 iLess0( X, skol10 ) }.
% 70.15/70.54 parent0[0, 2]: (103677) {G2,W11,D2,L3,V1,M3} { ! aReductOfIn0( X, skol10,
% 70.15/70.54 xR ), iLess0( X, skol10 ), ! aReductOfIn0( X, skol10, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (2805) {G3,W7,D2,L2,V1,M2} R(74,78);r(1297) { ! aReductOfIn0(
% 70.15/70.54 X, skol10, xR ), iLess0( X, skol10 ) }.
% 70.15/70.54 parent0: (103678) {G2,W7,D2,L2,V1,M2} { ! aReductOfIn0( X, skol10, xR ),
% 70.15/70.54 iLess0( X, skol10 ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103679) {G1,W8,D2,L3,V1,M3} { ! aElement0( X ), alpha18( X )
% 70.15/70.54 , ! aReductOfIn0( X, skol10, xR ) }.
% 70.15/70.54 parent0[1]: (79) {G0,W7,D2,L3,V1,M3} I { ! aElement0( X ), ! iLess0( X,
% 70.15/70.54 skol10 ), alpha18( X ) }.
% 70.15/70.54 parent1[1]: (2805) {G3,W7,D2,L2,V1,M2} R(74,78);r(1297) { ! aReductOfIn0( X
% 70.15/70.54 , skol10, xR ), iLess0( X, skol10 ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103680) {G2,W10,D2,L3,V1,M3} { alpha18( X ), ! aReductOfIn0(
% 70.15/70.54 X, skol10, xR ), ! aReductOfIn0( X, skol10, xR ) }.
% 70.15/70.54 parent0[0]: (103679) {G1,W8,D2,L3,V1,M3} { ! aElement0( X ), alpha18( X )
% 70.15/70.54 , ! aReductOfIn0( X, skol10, xR ) }.
% 70.15/70.54 parent1[1]: (1297) {G2,W6,D2,L2,V1,M2} R(131,78) { ! aReductOfIn0( X,
% 70.15/70.54 skol10, xR ), aElement0( X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 factor: (103681) {G2,W6,D2,L2,V1,M2} { alpha18( X ), ! aReductOfIn0( X,
% 70.15/70.54 skol10, xR ) }.
% 70.15/70.54 parent0[1, 2]: (103680) {G2,W10,D2,L3,V1,M3} { alpha18( X ), !
% 70.15/70.54 aReductOfIn0( X, skol10, xR ), ! aReductOfIn0( X, skol10, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (3004) {G4,W6,D2,L2,V1,M2} R(2805,79);r(1297) { ! aReductOfIn0
% 70.15/70.54 ( X, skol10, xR ), alpha18( X ) }.
% 70.15/70.54 parent0: (103681) {G2,W6,D2,L2,V1,M2} { alpha18( X ), ! aReductOfIn0( X,
% 70.15/70.54 skol10, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 1
% 70.15/70.54 1 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103682) {G1,W7,D2,L2,V2,M2} { alpha18( X ), ! alpha6( skol10
% 70.15/70.54 , xR, Y, X ) }.
% 70.15/70.54 parent0[0]: (3004) {G4,W6,D2,L2,V1,M2} R(2805,79);r(1297) { ! aReductOfIn0
% 70.15/70.54 ( X, skol10, xR ), alpha18( X ) }.
% 70.15/70.54 parent1[1]: (8) {G0,W9,D2,L2,V4,M2} I { ! alpha6( X, Y, Z, T ),
% 70.15/70.54 aReductOfIn0( T, X, Y ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := skol10
% 70.15/70.54 Y := xR
% 70.15/70.54 Z := Y
% 70.15/70.54 T := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (3023) {G5,W7,D2,L2,V2,M2} R(3004,8) { alpha18( X ), ! alpha6
% 70.15/70.54 ( skol10, xR, Y, X ) }.
% 70.15/70.54 parent0: (103682) {G1,W7,D2,L2,V2,M2} { alpha18( X ), ! alpha6( skol10, xR
% 70.15/70.54 , Y, X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := Y
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103683) {G1,W7,D3,L2,V0,M2} { ! aElement0( skol10 ),
% 70.15/70.54 aReductOfIn0( skol17( skol10 ), skol10, xR ) }.
% 70.15/70.54 parent0[0]: (128) {G1,W3,D2,L1,V1,M1} Q(85) { ! alpha19( X, X ) }.
% 70.15/70.54 parent1[1]: (80) {G0,W10,D3,L3,V1,M3} I { ! aElement0( X ), alpha19( skol10
% 70.15/70.54 , X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := skol10
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := skol10
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103684) {G1,W5,D3,L1,V0,M1} { aReductOfIn0( skol17( skol10 )
% 70.15/70.54 , skol10, xR ) }.
% 70.15/70.54 parent0[0]: (103683) {G1,W7,D3,L2,V0,M2} { ! aElement0( skol10 ),
% 70.15/70.54 aReductOfIn0( skol17( skol10 ), skol10, xR ) }.
% 70.15/70.54 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( skol10 ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (3121) {G2,W5,D3,L1,V0,M1} R(80,128);r(78) { aReductOfIn0(
% 70.15/70.54 skol17( skol10 ), skol10, xR ) }.
% 70.15/70.54 parent0: (103684) {G1,W5,D3,L1,V0,M1} { aReductOfIn0( skol17( skol10 ),
% 70.15/70.54 skol10, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103685) {G3,W3,D3,L1,V0,M1} { alpha18( skol17( skol10 ) ) }.
% 70.15/70.54 parent0[0]: (3004) {G4,W6,D2,L2,V1,M2} R(2805,79);r(1297) { ! aReductOfIn0
% 70.15/70.54 ( X, skol10, xR ), alpha18( X ) }.
% 70.15/70.54 parent1[0]: (3121) {G2,W5,D3,L1,V0,M1} R(80,128);r(78) { aReductOfIn0(
% 70.15/70.54 skol17( skol10 ), skol10, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := skol17( skol10 )
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (3125) {G5,W3,D3,L1,V0,M1} R(3121,3004) { alpha18( skol17(
% 70.15/70.54 skol10 ) ) }.
% 70.15/70.54 parent0: (103685) {G3,W3,D3,L1,V0,M1} { alpha18( skol17( skol10 ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103686) {G2,W5,D3,L2,V0,M2} { ! aRewritingSystem0( xR ),
% 70.15/70.54 aElement0( skol17( skol10 ) ) }.
% 70.15/70.54 parent0[1]: (132) {G1,W8,D2,L3,V2,M3} R(1,78) { ! aRewritingSystem0( X ), !
% 70.15/70.54 aReductOfIn0( Y, skol10, X ), aElement0( Y ) }.
% 70.15/70.54 parent1[0]: (3121) {G2,W5,D3,L1,V0,M1} R(80,128);r(78) { aReductOfIn0(
% 70.15/70.54 skol17( skol10 ), skol10, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := xR
% 70.15/70.54 Y := skol17( skol10 )
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103687) {G1,W3,D3,L1,V0,M1} { aElement0( skol17( skol10 ) )
% 70.15/70.54 }.
% 70.15/70.54 parent0[0]: (103686) {G2,W5,D3,L2,V0,M2} { ! aRewritingSystem0( xR ),
% 70.15/70.54 aElement0( skol17( skol10 ) ) }.
% 70.15/70.54 parent1[0]: (73) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (3130) {G3,W3,D3,L1,V0,M1} R(3121,132);r(73) { aElement0(
% 70.15/70.54 skol17( skol10 ) ) }.
% 70.15/70.54 parent0: (103687) {G1,W3,D3,L1,V0,M1} { aElement0( skol17( skol10 ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103688) {G2,W6,D4,L1,V1,M1} { ! aReductOfIn0( X, skol11(
% 70.15/70.54 skol17( skol10 ) ), xR ) }.
% 70.15/70.54 parent0[1]: (262) {G1,W7,D3,L2,V2,M2} R(92,88) { ! aReductOfIn0( X, skol11
% 70.15/70.54 ( Y ), xR ), ! alpha18( Y ) }.
% 70.15/70.54 parent1[0]: (3125) {G5,W3,D3,L1,V0,M1} R(3121,3004) { alpha18( skol17(
% 70.15/70.54 skol10 ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 Y := skol17( skol10 )
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (3148) {G6,W6,D4,L1,V1,M1} R(3125,262) { ! aReductOfIn0( X,
% 70.15/70.54 skol11( skol17( skol10 ) ), xR ) }.
% 70.15/70.54 parent0: (103688) {G2,W6,D4,L1,V1,M1} { ! aReductOfIn0( X, skol11( skol17
% 70.15/70.54 ( skol10 ) ), xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103689) {G4,W6,D4,L1,V0,M1} { alpha23( skol17( skol10 ),
% 70.15/70.54 skol11( skol17( skol10 ) ) ) }.
% 70.15/70.54 parent0[0]: (217) {G3,W6,D3,L2,V1,M2} R(88,195) { ! alpha18( X ), alpha23(
% 70.15/70.54 X, skol11( X ) ) }.
% 70.15/70.54 parent1[0]: (3125) {G5,W3,D3,L1,V0,M1} R(3121,3004) { alpha18( skol17(
% 70.15/70.54 skol10 ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := skol17( skol10 )
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (3152) {G6,W6,D4,L1,V0,M1} R(3125,217) { alpha23( skol17(
% 70.15/70.54 skol10 ), skol11( skol17( skol10 ) ) ) }.
% 70.15/70.54 parent0: (103689) {G4,W6,D4,L1,V0,M1} { alpha23( skol17( skol10 ), skol11
% 70.15/70.54 ( skol17( skol10 ) ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103690) {G4,W4,D4,L1,V0,M1} { aElement0( skol11( skol17(
% 70.15/70.54 skol10 ) ) ) }.
% 70.15/70.54 parent0[0]: (219) {G3,W5,D3,L2,V1,M2} R(88,196) { ! alpha18( X ), aElement0
% 70.15/70.54 ( skol11( X ) ) }.
% 70.15/70.54 parent1[0]: (3125) {G5,W3,D3,L1,V0,M1} R(3121,3004) { alpha18( skol17(
% 70.15/70.54 skol10 ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := skol17( skol10 )
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (3154) {G6,W4,D4,L1,V0,M1} R(3125,219) { aElement0( skol11(
% 70.15/70.54 skol17( skol10 ) ) ) }.
% 70.15/70.54 parent0: (103690) {G4,W4,D4,L1,V0,M1} { aElement0( skol11( skol17( skol10
% 70.15/70.54 ) ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103691) {G2,W7,D3,L2,V1,M2} { ! aReductOfIn0( X, skol17(
% 70.15/70.54 skol10 ), xR ), aElement0( X ) }.
% 70.15/70.54 parent0[0]: (131) {G1,W8,D2,L3,V2,M3} R(1,73) { ! aElement0( X ), !
% 70.15/70.54 aReductOfIn0( Y, X, xR ), aElement0( Y ) }.
% 70.15/70.54 parent1[0]: (3130) {G3,W3,D3,L1,V0,M1} R(3121,132);r(73) { aElement0(
% 70.15/70.54 skol17( skol10 ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := skol17( skol10 )
% 70.15/70.54 Y := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 subsumption: (3173) {G4,W7,D3,L2,V1,M2} R(3130,131) { ! aReductOfIn0( X,
% 70.15/70.54 skol17( skol10 ), xR ), aElement0( X ) }.
% 70.15/70.54 parent0: (103691) {G2,W7,D3,L2,V1,M2} { ! aReductOfIn0( X, skol17( skol10
% 70.15/70.54 ), xR ), aElement0( X ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 permutation0:
% 70.15/70.54 0 ==> 0
% 70.15/70.54 1 ==> 1
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103692) {G1,W10,D3,L3,V1,M3} { ! alpha18( X ), ! aElement0(
% 70.15/70.54 skol11( X ) ), ! sdtmndtplgtdt0( skol10, xR, skol11( X ) ) }.
% 70.15/70.54 parent0[0]: (262) {G1,W7,D3,L2,V2,M2} R(92,88) { ! aReductOfIn0( X, skol11
% 70.15/70.54 ( Y ), xR ), ! alpha18( Y ) }.
% 70.15/70.54 parent1[2]: (82) {G0,W11,D3,L3,V1,M3} I { ! aElement0( X ), !
% 70.15/70.54 sdtmndtplgtdt0( skol10, xR, X ), aReductOfIn0( skol17( X ), X, xR ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := skol17( skol11( X ) )
% 70.15/70.54 Y := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := skol11( X )
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 resolution: (103693) {G2,W9,D3,L3,V1,M3} { ! alpha18( X ), !
% 70.15/70.54 sdtmndtplgtdt0( skol10, xR, skol11( X ) ), ! alpha18( X ) }.
% 70.15/70.54 parent0[1]: (103692) {G1,W10,D3,L3,V1,M3} { ! alpha18( X ), ! aElement0(
% 70.15/70.54 skol11( X ) ), ! sdtmndtplgtdt0( skol10, xR, skol11( X ) ) }.
% 70.15/70.54 parent1[1]: (219) {G3,W5,D3,L2,V1,M2} R(88,196) { ! alpha18( X ), aElement0
% 70.15/70.54 ( skol11( X ) ) }.
% 70.15/70.54 substitution0:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54 substitution1:
% 70.15/70.54 X := X
% 70.15/70.54 end
% 70.15/70.54
% 70.15/70.54 factor: (103694) {G2,W7,D3,L2,V1,M2} { ! alpha18( X ), ! sdtmndtplgtdt0(
% 70.15/70.54 skol10, xR, skol11( X ) ) }.
% 70.15/70.54 parent0[0, 2]: (103693) {G2,W9,D3,L3,V1,M3} { ! alpha18( X ), !
% 70.15/70.54 sdtmndtplgtdt0( skoCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------