%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : COM020+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n026.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:10 EDT 2022
% Result : Theorem 97.17s 97.54s
% Output : Refutation 97.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : COM020+1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : bliksem %s
% 0.12/0.34 % Computer : n026.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % DateTime : Thu Jun 16 20:01:23 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.70/1.10 *** allocated 10000 integers for termspace/termends
% 0.70/1.10 *** allocated 10000 integers for clauses
% 0.70/1.10 *** allocated 10000 integers for justifications
% 0.70/1.10 Bliksem 1.12
% 0.70/1.10
% 0.70/1.10
% 0.70/1.10 Automatic Strategy Selection
% 0.70/1.10
% 0.70/1.10
% 0.70/1.10 Clauses:
% 0.70/1.10
% 0.70/1.10 { && }.
% 0.70/1.10 { && }.
% 0.70/1.10 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ),
% 0.70/1.10 aElement0( Z ) }.
% 0.70/1.10 { && }.
% 0.70/1.10 { && }.
% 0.70/1.10 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.70/1.10 sdtmndtplgtdt0( X, Y, Z ), aReductOfIn0( Z, X, Y ), alpha1( X, Y, Z ) }.
% 0.70/1.10 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.70/1.10 aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z ) }.
% 0.70/1.10 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha1( X
% 0.70/1.10 , Y, Z ), sdtmndtplgtdt0( X, Y, Z ) }.
% 0.70/1.10 { ! alpha1( X, Y, Z ), aElement0( skol1( T, U, W ) ) }.
% 0.70/1.10 { ! alpha1( X, Y, Z ), alpha6( X, Y, Z, skol1( X, Y, Z ) ) }.
% 0.70/1.10 { ! aElement0( T ), ! alpha6( X, Y, Z, T ), alpha1( X, Y, Z ) }.
% 0.70/1.10 { ! alpha6( X, Y, Z, T ), aReductOfIn0( T, X, Y ) }.
% 0.70/1.10 { ! alpha6( X, Y, Z, T ), sdtmndtplgtdt0( T, Y, Z ) }.
% 0.70/1.10 { ! aReductOfIn0( T, X, Y ), ! sdtmndtplgtdt0( T, Y, Z ), alpha6( X, Y, Z,
% 0.70/1.10 T ) }.
% 0.70/1.10 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0
% 0.70/1.10 ( T ), ! sdtmndtplgtdt0( X, Y, Z ), ! sdtmndtplgtdt0( Z, Y, T ),
% 0.70/1.10 sdtmndtplgtdt0( X, Y, T ) }.
% 0.70/1.10 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.70/1.10 sdtmndtasgtdt0( X, Y, Z ), X = Z, sdtmndtplgtdt0( X, Y, Z ) }.
% 0.70/1.10 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z,
% 0.70/1.10 sdtmndtasgtdt0( X, Y, Z ) }.
% 0.70/1.10 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.70/1.10 sdtmndtplgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z ) }.
% 0.70/1.10 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0
% 0.70/1.10 ( T ), ! sdtmndtasgtdt0( X, Y, Z ), ! sdtmndtasgtdt0( Z, Y, T ),
% 0.70/1.10 sdtmndtasgtdt0( X, Y, T ) }.
% 0.70/1.10 { ! aRewritingSystem0( X ), ! isConfluent0( X ), ! alpha2( X, Y, Z ),
% 0.70/1.10 alpha7( X, Y, Z ) }.
% 0.70/1.10 { ! aRewritingSystem0( X ), alpha2( X, skol2( X ), skol12( X ) ),
% 0.70/1.10 isConfluent0( X ) }.
% 0.70/1.10 { ! aRewritingSystem0( X ), ! alpha7( X, skol2( X ), skol12( X ) ),
% 0.70/1.10 isConfluent0( X ) }.
% 0.70/1.10 { ! alpha7( X, Y, Z ), aElement0( skol3( T, U, W ) ) }.
% 0.70/1.10 { ! alpha7( X, Y, Z ), alpha12( X, Y, Z, skol3( X, Y, Z ) ) }.
% 0.70/1.10 { ! aElement0( T ), ! alpha12( X, Y, Z, T ), alpha7( X, Y, Z ) }.
% 0.70/1.10 { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Y, X, T ) }.
% 0.70/1.10 { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Z, X, T ) }.
% 0.70/1.10 { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0( Z, X, T ), alpha12( X, Y,
% 0.70/1.10 Z, T ) }.
% 0.70/1.10 { ! alpha2( X, Y, Z ), aElement0( skol4( T, U, W ) ) }.
% 0.70/1.10 { ! alpha2( X, Y, Z ), alpha8( X, Y, Z, skol4( X, Y, Z ) ) }.
% 0.70/1.10 { ! aElement0( T ), ! alpha8( X, Y, Z, T ), alpha2( X, Y, Z ) }.
% 0.70/1.10 { ! alpha8( X, Y, Z, T ), aElement0( Y ) }.
% 0.70/1.10 { ! alpha8( X, Y, Z, T ), alpha13( X, Y, Z, T ) }.
% 0.70/1.10 { ! aElement0( Y ), ! alpha13( X, Y, Z, T ), alpha8( X, Y, Z, T ) }.
% 0.70/1.10 { ! alpha13( X, Y, Z, T ), aElement0( Z ) }.
% 0.70/1.10 { ! alpha13( X, Y, Z, T ), alpha16( X, Y, Z, T ) }.
% 0.70/1.10 { ! aElement0( Z ), ! alpha16( X, Y, Z, T ), alpha13( X, Y, Z, T ) }.
% 0.70/1.10 { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T, X, Y ) }.
% 0.70/1.10 { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T, X, Z ) }.
% 0.70/1.10 { ! sdtmndtasgtdt0( T, X, Y ), ! sdtmndtasgtdt0( T, X, Z ), alpha16( X, Y,
% 0.70/1.10 Z, T ) }.
% 0.70/1.10 { ! aRewritingSystem0( X ), ! isLocallyConfluent0( X ), ! alpha3( X, Y, Z )
% 0.70/1.10 , alpha9( X, Y, Z ) }.
% 0.70/1.10 { ! aRewritingSystem0( X ), alpha3( X, skol5( X ), skol13( X ) ),
% 0.70/1.10 isLocallyConfluent0( X ) }.
% 0.70/1.10 { ! aRewritingSystem0( X ), ! alpha9( X, skol5( X ), skol13( X ) ),
% 0.70/1.10 isLocallyConfluent0( X ) }.
% 0.70/1.10 { ! alpha9( X, Y, Z ), aElement0( skol6( T, U, W ) ) }.
% 0.70/1.10 { ! alpha9( X, Y, Z ), alpha14( X, Y, Z, skol6( X, Y, Z ) ) }.
% 0.70/1.10 { ! aElement0( T ), ! alpha14( X, Y, Z, T ), alpha9( X, Y, Z ) }.
% 0.70/1.10 { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Y, X, T ) }.
% 0.70/1.10 { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Z, X, T ) }.
% 0.70/1.10 { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0( Z, X, T ), alpha14( X, Y,
% 0.70/1.10 Z, T ) }.
% 0.70/1.10 { ! alpha3( X, Y, Z ), aElement0( skol7( T, U, W ) ) }.
% 0.70/1.10 { ! alpha3( X, Y, Z ), alpha10( X, Y, Z, skol7( X, Y, Z ) ) }.
% 0.70/1.10 { ! aElement0( T ), ! alpha10( X, Y, Z, T ), alpha3( X, Y, Z ) }.
% 0.70/1.10 { ! alpha10( X, Y, Z, T ), aElement0( Y ) }.
% 0.70/1.10 { ! alpha10( X, Y, Z, T ), alpha15( X, Y, Z, T ) }.
% 0.73/1.58 { ! aElement0( Y ), ! alpha15( X, Y, Z, T ), alpha10( X, Y, Z, T ) }.
% 0.73/1.58 { ! alpha15( X, Y, Z, T ), aElement0( Z ) }.
% 0.73/1.58 { ! alpha15( X, Y, Z, T ), alpha17( X, Y, Z, T ) }.
% 0.73/1.58 { ! aElement0( Z ), ! alpha17( X, Y, Z, T ), alpha15( X, Y, Z, T ) }.
% 0.73/1.58 { ! alpha17( X, Y, Z, T ), aReductOfIn0( Y, T, X ) }.
% 0.73/1.58 { ! alpha17( X, Y, Z, T ), aReductOfIn0( Z, T, X ) }.
% 0.73/1.58 { ! aReductOfIn0( Y, T, X ), ! aReductOfIn0( Z, T, X ), alpha17( X, Y, Z, T
% 0.73/1.58 ) }.
% 0.73/1.58 { ! aRewritingSystem0( X ), ! isTerminating0( X ), ! alpha4( Y, Z ),
% 0.73/1.58 alpha11( X, Y, Z ) }.
% 0.73/1.58 { ! aRewritingSystem0( X ), alpha4( skol8( X ), skol14( X ) ),
% 0.73/1.58 isTerminating0( X ) }.
% 0.73/1.58 { ! aRewritingSystem0( X ), ! alpha11( X, skol8( X ), skol14( X ) ),
% 0.73/1.58 isTerminating0( X ) }.
% 0.73/1.58 { ! alpha11( X, Y, Z ), ! sdtmndtplgtdt0( Y, X, Z ), iLess0( Z, Y ) }.
% 0.73/1.58 { sdtmndtplgtdt0( Y, X, Z ), alpha11( X, Y, Z ) }.
% 0.73/1.58 { ! iLess0( Z, Y ), alpha11( X, Y, Z ) }.
% 0.73/1.58 { ! alpha4( X, Y ), aElement0( X ) }.
% 0.73/1.58 { ! alpha4( X, Y ), aElement0( Y ) }.
% 0.73/1.58 { ! aElement0( X ), ! aElement0( Y ), alpha4( X, Y ) }.
% 0.73/1.58 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y )
% 0.73/1.58 , aElement0( Z ) }.
% 0.73/1.58 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y )
% 0.73/1.58 , alpha5( X, Y, Z ) }.
% 0.73/1.58 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha5( X
% 0.73/1.58 , Y, Z ), aNormalFormOfIn0( Z, X, Y ) }.
% 0.73/1.58 { ! alpha5( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z ) }.
% 0.73/1.58 { ! alpha5( X, Y, Z ), ! aReductOfIn0( T, Z, Y ) }.
% 0.73/1.58 { ! sdtmndtasgtdt0( X, Y, Z ), aReductOfIn0( skol9( Y, Z ), Z, Y ), alpha5
% 0.73/1.58 ( X, Y, Z ) }.
% 0.73/1.58 { ! aRewritingSystem0( X ), ! isTerminating0( X ), ! aElement0( Y ),
% 0.73/1.58 aNormalFormOfIn0( skol10( X, Y ), Y, X ) }.
% 0.73/1.58 { aRewritingSystem0( xR ) }.
% 0.73/1.58 { isLocallyConfluent0( xR ) }.
% 0.73/1.58 { isTerminating0( xR ) }.
% 0.73/1.58 { aElement0( xa ) }.
% 0.73/1.58 { aElement0( xb ) }.
% 0.73/1.58 { aElement0( xc ) }.
% 0.73/1.58 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( X
% 0.73/1.58 , xR, Y ), ! sdtmndtasgtdt0( X, xR, Z ), ! iLess0( X, xa ), aElement0(
% 0.73/1.58 skol11( T, U ) ) }.
% 0.73/1.58 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( X
% 0.73/1.58 , xR, Y ), ! sdtmndtasgtdt0( X, xR, Z ), ! iLess0( X, xa ),
% 0.73/1.58 sdtmndtasgtdt0( Z, xR, skol11( T, Z ) ) }.
% 0.73/1.58 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( X
% 0.73/1.58 , xR, Y ), ! sdtmndtasgtdt0( X, xR, Z ), ! iLess0( X, xa ),
% 0.73/1.58 sdtmndtasgtdt0( Y, xR, skol11( Y, Z ) ) }.
% 0.73/1.58 { sdtmndtplgtdt0( xa, xR, xb ) }.
% 0.73/1.58 { sdtmndtplgtdt0( xa, xR, xc ) }.
% 0.73/1.58 { aElement0( xu ) }.
% 0.73/1.58 { aReductOfIn0( xu, xa, xR ) }.
% 0.73/1.58 { sdtmndtasgtdt0( xu, xR, xb ) }.
% 0.73/1.58 { aElement0( xv ) }.
% 0.73/1.58 { aReductOfIn0( xv, xa, xR ) }.
% 0.73/1.58 { sdtmndtasgtdt0( xv, xR, xc ) }.
% 0.73/1.58 { aElement0( xw ) }.
% 0.73/1.58 { sdtmndtasgtdt0( xu, xR, xw ) }.
% 0.73/1.58 { sdtmndtasgtdt0( xv, xR, xw ) }.
% 0.73/1.58 { aNormalFormOfIn0( xd, xw, xR ) }.
% 0.73/1.58 { ! aElement0( X ), ! sdtmndtasgtdt0( xb, xR, X ), ! sdtmndtasgtdt0( xd, xR
% 0.73/1.58 , X ) }.
% 0.73/1.58
% 0.73/1.58 percentage equality = 0.007722, percentage horn = 0.927083
% 0.73/1.58 This is a problem with some equality
% 0.73/1.58
% 0.73/1.58
% 0.73/1.58
% 0.73/1.58 Options Used:
% 0.73/1.58
% 0.73/1.58 useres = 1
% 0.73/1.58 useparamod = 1
% 0.73/1.58 useeqrefl = 1
% 0.73/1.58 useeqfact = 1
% 0.73/1.58 usefactor = 1
% 0.73/1.58 usesimpsplitting = 0
% 0.73/1.58 usesimpdemod = 5
% 0.73/1.58 usesimpres = 3
% 0.73/1.58
% 0.73/1.58 resimpinuse = 1000
% 0.73/1.58 resimpclauses = 20000
% 0.73/1.58 substype = eqrewr
% 0.73/1.58 backwardsubs = 1
% 0.73/1.58 selectoldest = 5
% 0.73/1.58
% 0.73/1.58 litorderings [0] = split
% 0.73/1.58 litorderings [1] = extend the termordering, first sorting on arguments
% 0.73/1.58
% 0.73/1.58 termordering = kbo
% 0.73/1.58
% 0.73/1.58 litapriori = 0
% 0.73/1.58 termapriori = 1
% 0.73/1.58 litaposteriori = 0
% 0.73/1.58 termaposteriori = 0
% 0.73/1.58 demodaposteriori = 0
% 0.73/1.58 ordereqreflfact = 0
% 0.73/1.58
% 0.73/1.58 litselect = negord
% 0.73/1.58
% 0.73/1.58 maxweight = 15
% 0.73/1.58 maxdepth = 30000
% 0.73/1.58 maxlength = 115
% 0.73/1.58 maxnrvars = 195
% 0.73/1.58 excuselevel = 1
% 0.73/1.58 increasemaxweight = 1
% 0.73/1.58
% 0.73/1.58 maxselected = 10000000
% 0.73/1.58 maxnrclauses = 10000000
% 0.73/1.58
% 0.73/1.58 showgenerated = 0
% 0.73/1.58 showkept = 0
% 0.73/1.58 showselected = 0
% 0.73/1.58 showdeleted = 0
% 0.73/1.58 showresimp = 1
% 0.73/1.58 showstatus = 2000
% 0.73/1.58
% 0.73/1.58 prologoutput = 0
% 0.73/1.58 nrgoals = 5000000
% 0.73/1.58 totalproof = 1
% 0.73/1.58
% 0.73/1.58 Symbols occurring in the translation:
% 0.73/1.58
% 0.73/1.58 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.73/1.58 . [1, 2] (w:1, o:35, a:1, s:1, b:0),
% 0.73/1.58 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 0.73/1.58 ! [4, 1] (w:0, o:19, a:1, s:1, b:0),
% 17.43/17.82 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 17.43/17.82 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 17.43/17.82 aElement0 [36, 1] (w:1, o:24, a:1, s:1, b:0),
% 17.43/17.82 aRewritingSystem0 [37, 1] (w:1, o:25, a:1, s:1, b:0),
% 17.43/17.82 aReductOfIn0 [40, 3] (w:1, o:64, a:1, s:1, b:0),
% 17.43/17.82 iLess0 [41, 2] (w:1, o:59, a:1, s:1, b:0),
% 17.43/17.82 sdtmndtplgtdt0 [42, 3] (w:1, o:65, a:1, s:1, b:0),
% 17.43/17.82 sdtmndtasgtdt0 [44, 3] (w:1, o:66, a:1, s:1, b:0),
% 17.43/17.82 isConfluent0 [45, 1] (w:1, o:26, a:1, s:1, b:0),
% 17.43/17.82 isLocallyConfluent0 [47, 1] (w:1, o:27, a:1, s:1, b:0),
% 17.43/17.82 isTerminating0 [48, 1] (w:1, o:28, a:1, s:1, b:0),
% 17.43/17.82 aNormalFormOfIn0 [49, 3] (w:1, o:67, a:1, s:1, b:0),
% 17.43/17.82 xR [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 17.43/17.82 xa [51, 0] (w:1, o:12, a:1, s:1, b:0),
% 17.43/17.82 xb [52, 0] (w:1, o:13, a:1, s:1, b:0),
% 17.43/17.82 xc [53, 0] (w:1, o:14, a:1, s:1, b:0),
% 17.43/17.82 xu [54, 0] (w:1, o:15, a:1, s:1, b:0),
% 17.43/17.82 xv [55, 0] (w:1, o:16, a:1, s:1, b:0),
% 17.43/17.82 xw [56, 0] (w:1, o:17, a:1, s:1, b:0),
% 17.43/17.82 xd [57, 0] (w:1, o:18, a:1, s:1, b:0),
% 17.43/17.82 alpha1 [58, 3] (w:1, o:68, a:1, s:1, b:1),
% 17.43/17.82 alpha2 [59, 3] (w:1, o:70, a:1, s:1, b:1),
% 17.43/17.82 alpha3 [60, 3] (w:1, o:71, a:1, s:1, b:1),
% 17.43/17.82 alpha4 [61, 2] (w:1, o:60, a:1, s:1, b:1),
% 17.43/17.82 alpha5 [62, 3] (w:1, o:72, a:1, s:1, b:1),
% 17.43/17.82 alpha6 [63, 4] (w:1, o:80, a:1, s:1, b:1),
% 17.43/17.82 alpha7 [64, 3] (w:1, o:73, a:1, s:1, b:1),
% 17.43/17.82 alpha8 [65, 4] (w:1, o:81, a:1, s:1, b:1),
% 17.43/17.82 alpha9 [66, 3] (w:1, o:74, a:1, s:1, b:1),
% 17.43/17.82 alpha10 [67, 4] (w:1, o:82, a:1, s:1, b:1),
% 17.43/17.82 alpha11 [68, 3] (w:1, o:69, a:1, s:1, b:1),
% 17.43/17.82 alpha12 [69, 4] (w:1, o:83, a:1, s:1, b:1),
% 17.43/17.82 alpha13 [70, 4] (w:1, o:84, a:1, s:1, b:1),
% 17.43/17.82 alpha14 [71, 4] (w:1, o:85, a:1, s:1, b:1),
% 17.43/17.82 alpha15 [72, 4] (w:1, o:86, a:1, s:1, b:1),
% 17.43/17.82 alpha16 [73, 4] (w:1, o:87, a:1, s:1, b:1),
% 17.43/17.82 alpha17 [74, 4] (w:1, o:88, a:1, s:1, b:1),
% 17.43/17.82 skol1 [75, 3] (w:1, o:75, a:1, s:1, b:1),
% 17.43/17.82 skol2 [76, 1] (w:1, o:32, a:1, s:1, b:1),
% 17.43/17.82 skol3 [77, 3] (w:1, o:76, a:1, s:1, b:1),
% 17.43/17.82 skol4 [78, 3] (w:1, o:77, a:1, s:1, b:1),
% 17.43/17.82 skol5 [79, 1] (w:1, o:33, a:1, s:1, b:1),
% 17.43/17.82 skol6 [80, 3] (w:1, o:78, a:1, s:1, b:1),
% 17.43/17.82 skol7 [81, 3] (w:1, o:79, a:1, s:1, b:1),
% 17.43/17.82 skol8 [82, 1] (w:1, o:34, a:1, s:1, b:1),
% 17.43/17.82 skol9 [83, 2] (w:1, o:61, a:1, s:1, b:1),
% 17.43/17.82 skol10 [84, 2] (w:1, o:62, a:1, s:1, b:1),
% 17.43/17.82 skol11 [85, 2] (w:1, o:63, a:1, s:1, b:1),
% 17.43/17.82 skol12 [86, 1] (w:1, o:29, a:1, s:1, b:1),
% 17.43/17.82 skol13 [87, 1] (w:1, o:30, a:1, s:1, b:1),
% 17.43/17.82 skol14 [88, 1] (w:1, o:31, a:1, s:1, b:1).
% 17.43/17.82
% 17.43/17.82
% 17.43/17.82 Starting Search:
% 17.43/17.82
% 17.43/17.82 *** allocated 15000 integers for clauses
% 17.43/17.82 *** allocated 22500 integers for clauses
% 17.43/17.82 *** allocated 15000 integers for termspace/termends
% 17.43/17.82 *** allocated 33750 integers for clauses
% 17.43/17.82 *** allocated 50625 integers for clauses
% 17.43/17.82 *** allocated 22500 integers for termspace/termends
% 17.43/17.82 Resimplifying inuse:
% 17.43/17.82 Done
% 17.43/17.82
% 17.43/17.82 *** allocated 75937 integers for clauses
% 17.43/17.82 *** allocated 33750 integers for termspace/termends
% 17.43/17.82 *** allocated 113905 integers for clauses
% 17.43/17.82
% 17.43/17.82 Intermediate Status:
% 17.43/17.82 Generated: 8157
% 17.43/17.82 Kept: 2002
% 17.43/17.82 Inuse: 276
% 17.43/17.82 Deleted: 1
% 17.43/17.82 Deletedinuse: 1
% 17.43/17.82
% 17.43/17.82 Resimplifying inuse:
% 17.43/17.82 Done
% 17.43/17.82
% 17.43/17.82 *** allocated 50625 integers for termspace/termends
% 17.43/17.82 *** allocated 170857 integers for clauses
% 17.43/17.82 Resimplifying inuse:
% 17.43/17.82 Done
% 17.43/17.82
% 17.43/17.82 *** allocated 75937 integers for termspace/termends
% 17.43/17.82 *** allocated 256285 integers for clauses
% 17.43/17.82
% 17.43/17.82 Intermediate Status:
% 17.43/17.82 Generated: 15191
% 17.43/17.82 Kept: 4020
% 17.43/17.82 Inuse: 526
% 17.43/17.82 Deleted: 18
% 17.43/17.82 Deletedinuse: 5
% 17.43/17.82
% 17.43/17.82 Resimplifying inuse:
% 17.43/17.82 Done
% 17.43/17.82
% 17.43/17.82 Resimplifying inuse:
% 17.43/17.82 Done
% 17.43/17.82
% 17.43/17.82 *** allocated 113905 integers for termspace/termends
% 17.43/17.82 *** allocated 384427 integers for clauses
% 17.43/17.82
% 17.43/17.82 Intermediate Status:
% 17.43/17.82 Generated: 23886
% 17.43/17.82 Kept: 6036
% 17.43/17.82 Inuse: 694
% 17.43/17.82 Deleted: 57
% 17.43/17.82 Deletedinuse: 16
% 17.43/17.82
% 17.43/17.82 Resimplifying inuse:
% 17.43/17.82 Done
% 17.43/17.82
% 17.43/17.82 Resimplifying inuse:
% 17.43/17.82 Done
% 17.43/17.82
% 17.43/17.82
% 17.43/17.82 Intermediate Status:
% 17.43/17.82 Generated: 55390
% 17.43/17.82 Kept: 8036
% 17.43/17.82 Inuse: 938
% 17.43/17.82 Deleted: 80
% 17.43/17.82 Deletedinuse: 16
% 17.43/17.82
% 17.43/17.82 Resimplifying inuse:
% 17.43/17.82 Done
% 17.43/17.82
% 17.43/17.82 *** allocated 170857 integers for termspace/termends
% 17.43/17.82 *** allocated 576640 integers for clauses
% 17.43/17.82 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79
% 42.41/42.79 Intermediate Status:
% 42.41/42.79 Generated: 64559
% 42.41/42.79 Kept: 10052
% 42.41/42.79 Inuse: 1088
% 42.41/42.79 Deleted: 92
% 42.41/42.79 Deletedinuse: 16
% 42.41/42.79
% 42.41/42.79 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79
% 42.41/42.79 Intermediate Status:
% 42.41/42.79 Generated: 123948
% 42.41/42.79 Kept: 12052
% 42.41/42.79 Inuse: 1510
% 42.41/42.79 Deleted: 103
% 42.41/42.79 Deletedinuse: 19
% 42.41/42.79
% 42.41/42.79 *** allocated 256285 integers for termspace/termends
% 42.41/42.79 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79
% 42.41/42.79 Intermediate Status:
% 42.41/42.79 Generated: 257591
% 42.41/42.79 Kept: 14058
% 42.41/42.79 Inuse: 1932
% 42.41/42.79 Deleted: 114
% 42.41/42.79 Deletedinuse: 24
% 42.41/42.79
% 42.41/42.79 *** allocated 864960 integers for clauses
% 42.41/42.79 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79
% 42.41/42.79 Intermediate Status:
% 42.41/42.79 Generated: 301126
% 42.41/42.79 Kept: 16081
% 42.41/42.79 Inuse: 2107
% 42.41/42.79 Deleted: 120
% 42.41/42.79 Deletedinuse: 24
% 42.41/42.79
% 42.41/42.79 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79 *** allocated 384427 integers for termspace/termends
% 42.41/42.79
% 42.41/42.79 Intermediate Status:
% 42.41/42.79 Generated: 334146
% 42.41/42.79 Kept: 18098
% 42.41/42.79 Inuse: 2249
% 42.41/42.79 Deleted: 146
% 42.41/42.79 Deletedinuse: 24
% 42.41/42.79
% 42.41/42.79 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79 Resimplifying inuse:
% 42.41/42.79 Done
% 42.41/42.79
% 42.41/42.79 Resimplifying clauses:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 393644
% 42.41/42.80 Kept: 21336
% 42.41/42.80 Inuse: 2452
% 42.41/42.80 Deleted: 4749
% 42.41/42.80 Deletedinuse: 37
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 *** allocated 1297440 integers for clauses
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 441922
% 42.41/42.80 Kept: 23343
% 42.41/42.80 Inuse: 2670
% 42.41/42.80 Deleted: 4877
% 42.41/42.80 Deletedinuse: 127
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 491235
% 42.41/42.80 Kept: 25363
% 42.41/42.80 Inuse: 2791
% 42.41/42.80 Deleted: 4934
% 42.41/42.80 Deletedinuse: 156
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 *** allocated 576640 integers for termspace/termends
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 538161
% 42.41/42.80 Kept: 27365
% 42.41/42.80 Inuse: 2991
% 42.41/42.80 Deleted: 4947
% 42.41/42.80 Deletedinuse: 156
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 576492
% 42.41/42.80 Kept: 29398
% 42.41/42.80 Inuse: 3174
% 42.41/42.80 Deleted: 4959
% 42.41/42.80 Deletedinuse: 156
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 620519
% 42.41/42.80 Kept: 31412
% 42.41/42.80 Inuse: 3411
% 42.41/42.80 Deleted: 4959
% 42.41/42.80 Deletedinuse: 156
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 *** allocated 1946160 integers for clauses
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 678127
% 42.41/42.80 Kept: 33419
% 42.41/42.80 Inuse: 3653
% 42.41/42.80 Deleted: 4967
% 42.41/42.80 Deletedinuse: 156
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 705727
% 42.41/42.80 Kept: 35428
% 42.41/42.80 Inuse: 3757
% 42.41/42.80 Deleted: 5008
% 42.41/42.80 Deletedinuse: 194
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 727900
% 42.41/42.80 Kept: 37463
% 42.41/42.80 Inuse: 3884
% 42.41/42.80 Deleted: 5039
% 42.41/42.80 Deletedinuse: 194
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 757453
% 42.41/42.80 Kept: 39516
% 42.41/42.80 Inuse: 3983
% 42.41/42.80 Deleted: 5077
% 42.41/42.80 Deletedinuse: 194
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 *** allocated 864960 integers for termspace/termends
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying clauses:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 822775
% 42.41/42.80 Kept: 43854
% 42.41/42.80 Inuse: 4188
% 42.41/42.80 Deleted: 11497
% 42.41/42.80 Deletedinuse: 214
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 844843
% 42.41/42.80 Kept: 45868
% 42.41/42.80 Inuse: 4361
% 42.41/42.80 Deleted: 11649
% 42.41/42.80 Deletedinuse: 350
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 870353
% 42.41/42.80 Kept: 47916
% 42.41/42.80 Inuse: 4449
% 42.41/42.80 Deleted: 11678
% 42.41/42.80 Deletedinuse: 376
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 *** allocated 2919240 integers for clauses
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 914219
% 42.41/42.80 Kept: 49932
% 42.41/42.80 Inuse: 4523
% 42.41/42.80 Deleted: 11724
% 42.41/42.80 Deletedinuse: 376
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 938949
% 42.41/42.80 Kept: 51975
% 42.41/42.80 Inuse: 4612
% 42.41/42.80 Deleted: 11737
% 42.41/42.80 Deletedinuse: 376
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80
% 42.41/42.80 Intermediate Status:
% 42.41/42.80 Generated: 959183
% 42.41/42.80 Kept: 53976
% 42.41/42.80 Inuse: 4667
% 42.41/42.80 Deleted: 11741
% 42.41/42.80 Deletedinuse: 378
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 42.41/42.80
% 42.41/42.80 Resimplifying inuse:
% 42.41/42.80 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 983817
% 97.17/97.54 Kept: 55998
% 97.17/97.54 Inuse: 4770
% 97.17/97.54 Deleted: 11774
% 97.17/97.54 Deletedinuse: 388
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1027591
% 97.17/97.54 Kept: 58041
% 97.17/97.54 Inuse: 4852
% 97.17/97.54 Deleted: 11774
% 97.17/97.54 Deletedinuse: 388
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1052948
% 97.17/97.54 Kept: 60054
% 97.17/97.54 Inuse: 4920
% 97.17/97.54 Deleted: 11775
% 97.17/97.54 Deletedinuse: 388
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 *** allocated 1297440 integers for termspace/termends
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1087084
% 97.17/97.54 Kept: 62071
% 97.17/97.54 Inuse: 5075
% 97.17/97.54 Deleted: 11812
% 97.17/97.54 Deletedinuse: 388
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying clauses:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1096710
% 97.17/97.54 Kept: 65233
% 97.17/97.54 Inuse: 5097
% 97.17/97.54 Deleted: 18716
% 97.17/97.54 Deletedinuse: 392
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1128604
% 97.17/97.54 Kept: 67248
% 97.17/97.54 Inuse: 5215
% 97.17/97.54 Deleted: 18766
% 97.17/97.54 Deletedinuse: 438
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1166185
% 97.17/97.54 Kept: 69261
% 97.17/97.54 Inuse: 5296
% 97.17/97.54 Deleted: 18776
% 97.17/97.54 Deletedinuse: 444
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1222516
% 97.17/97.54 Kept: 71298
% 97.17/97.54 Inuse: 5533
% 97.17/97.54 Deleted: 18782
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 *** allocated 4378860 integers for clauses
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1277295
% 97.17/97.54 Kept: 73316
% 97.17/97.54 Inuse: 5755
% 97.17/97.54 Deleted: 18785
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1308312
% 97.17/97.54 Kept: 75324
% 97.17/97.54 Inuse: 5948
% 97.17/97.54 Deleted: 18787
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1324192
% 97.17/97.54 Kept: 77417
% 97.17/97.54 Inuse: 6010
% 97.17/97.54 Deleted: 18787
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1344239
% 97.17/97.54 Kept: 79436
% 97.17/97.54 Inuse: 6079
% 97.17/97.54 Deleted: 18787
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1349889
% 97.17/97.54 Kept: 81617
% 97.17/97.54 Inuse: 6091
% 97.17/97.54 Deleted: 18787
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1361332
% 97.17/97.54 Kept: 83657
% 97.17/97.54 Inuse: 6129
% 97.17/97.54 Deleted: 18787
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying clauses:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1378901
% 97.17/97.54 Kept: 85779
% 97.17/97.54 Inuse: 6189
% 97.17/97.54 Deleted: 25546
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1437155
% 97.17/97.54 Kept: 87780
% 97.17/97.54 Inuse: 6368
% 97.17/97.54 Deleted: 25546
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1463836
% 97.17/97.54 Kept: 89811
% 97.17/97.54 Inuse: 6519
% 97.17/97.54 Deleted: 25546
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1476579
% 97.17/97.54 Kept: 91892
% 97.17/97.54 Inuse: 6589
% 97.17/97.54 Deleted: 25546
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 *** allocated 1946160 integers for termspace/termends
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1481842
% 97.17/97.54 Kept: 93904
% 97.17/97.54 Inuse: 6600
% 97.17/97.54 Deleted: 25546
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1498883
% 97.17/97.54 Kept: 95904
% 97.17/97.54 Inuse: 6668
% 97.17/97.54 Deleted: 25546
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1513248
% 97.17/97.54 Kept: 98062
% 97.17/97.54 Inuse: 6728
% 97.17/97.54 Deleted: 25546
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1523202
% 97.17/97.54 Kept: 100124
% 97.17/97.54 Inuse: 6773
% 97.17/97.54 Deleted: 25546
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1551404
% 97.17/97.54 Kept: 102140
% 97.17/97.54 Inuse: 6803
% 97.17/97.54 Deleted: 25546
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1592801
% 97.17/97.54 Kept: 104153
% 97.17/97.54 Inuse: 6933
% 97.17/97.54 Deleted: 25546
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying clauses:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1623703
% 97.17/97.54 Kept: 106954
% 97.17/97.54 Inuse: 7023
% 97.17/97.54 Deleted: 28300
% 97.17/97.54 Deletedinuse: 449
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1703773
% 97.17/97.54 Kept: 109007
% 97.17/97.54 Inuse: 7132
% 97.17/97.54 Deleted: 28320
% 97.17/97.54 Deletedinuse: 469
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1733594
% 97.17/97.54 Kept: 111166
% 97.17/97.54 Inuse: 7184
% 97.17/97.54 Deleted: 28320
% 97.17/97.54 Deletedinuse: 469
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1765280
% 97.17/97.54 Kept: 113227
% 97.17/97.54 Inuse: 7238
% 97.17/97.54 Deleted: 28320
% 97.17/97.54 Deletedinuse: 469
% 97.17/97.54
% 97.17/97.54 *** allocated 6568290 integers for clauses
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1814808
% 97.17/97.54 Kept: 115293
% 97.17/97.54 Inuse: 7368
% 97.17/97.54 Deleted: 28320
% 97.17/97.54 Deletedinuse: 469
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1852057
% 97.17/97.54 Kept: 117293
% 97.17/97.54 Inuse: 7469
% 97.17/97.54 Deleted: 28324
% 97.17/97.54 Deletedinuse: 473
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1902535
% 97.17/97.54 Kept: 119297
% 97.17/97.54 Inuse: 7587
% 97.17/97.54 Deleted: 28324
% 97.17/97.54 Deletedinuse: 473
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1918789
% 97.17/97.54 Kept: 121373
% 97.17/97.54 Inuse: 7633
% 97.17/97.54 Deleted: 28324
% 97.17/97.54 Deletedinuse: 473
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1965138
% 97.17/97.54 Kept: 123383
% 97.17/97.54 Inuse: 7692
% 97.17/97.54 Deleted: 28334
% 97.17/97.54 Deletedinuse: 480
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 1983667
% 97.17/97.54 Kept: 125395
% 97.17/97.54 Inuse: 7725
% 97.17/97.54 Deleted: 28334
% 97.17/97.54 Deletedinuse: 480
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying clauses:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 2010989
% 97.17/97.54 Kept: 128084
% 97.17/97.54 Inuse: 7790
% 97.17/97.54 Deleted: 33019
% 97.17/97.54 Deletedinuse: 480
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 2044930
% 97.17/97.54 Kept: 130102
% 97.17/97.54 Inuse: 7866
% 97.17/97.54 Deleted: 33022
% 97.17/97.54 Deletedinuse: 483
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 2063899
% 97.17/97.54 Kept: 132151
% 97.17/97.54 Inuse: 7924
% 97.17/97.54 Deleted: 33022
% 97.17/97.54 Deletedinuse: 483
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 2109967
% 97.17/97.54 Kept: 134174
% 97.17/97.54 Inuse: 8047
% 97.17/97.54 Deleted: 33022
% 97.17/97.54 Deletedinuse: 483
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 *** allocated 2919240 integers for termspace/termends
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 2134816
% 97.17/97.54 Kept: 136324
% 97.17/97.54 Inuse: 8123
% 97.17/97.54 Deleted: 33022
% 97.17/97.54 Deletedinuse: 483
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 2153746
% 97.17/97.54 Kept: 140036
% 97.17/97.54 Inuse: 8132
% 97.17/97.54 Deleted: 33022
% 97.17/97.54 Deletedinuse: 483
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 2235447
% 97.17/97.54 Kept: 142038
% 97.17/97.54 Inuse: 8296
% 97.17/97.54 Deleted: 33098
% 97.17/97.54 Deletedinuse: 535
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 2295760
% 97.17/97.54 Kept: 144119
% 97.17/97.54 Inuse: 8389
% 97.17/97.54 Deleted: 33101
% 97.17/97.54 Deletedinuse: 535
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Intermediate Status:
% 97.17/97.54 Generated: 2329135
% 97.17/97.54 Kept: 146180
% 97.17/97.54 Inuse: 8437
% 97.17/97.54 Deleted: 33101
% 97.17/97.54 Deletedinuse: 535
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying inuse:
% 97.17/97.54 Done
% 97.17/97.54
% 97.17/97.54 Resimplifying clauses:
% 97.17/97.54
% 97.17/97.54 Bliksems!, er is een bewijs:
% 97.17/97.54 % SZS status Theorem
% 97.17/97.54 % SZS output start Refutation
% 97.17/97.54
% 97.17/97.54 (3) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 97.17/97.54 aElement0( Z ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z ) }.
% 97.17/97.54 (13) {G0,W13,D2,L5,V3,M5} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 97.17/97.54 aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y, Z ) }.
% 97.17/97.54 (15) {G0,W20,D2,L7,V4,M7} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 97.17/97.54 aElement0( Z ), ! aElement0( T ), ! sdtmndtasgtdt0( X, Y, Z ), !
% 97.17/97.54 sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X, Y, T ) }.
% 97.17/97.54 (58) {G0,W11,D2,L4,V3,M4} I { ! aRewritingSystem0( X ), ! isTerminating0( X
% 97.17/97.54 ), ! alpha4( Y, Z ), alpha11( X, Y, Z ) }.
% 97.17/97.54 (61) {G0,W11,D2,L3,V3,M3} I { ! alpha11( X, Y, Z ), ! sdtmndtplgtdt0( Y, X
% 97.17/97.54 , Z ), iLess0( Z, Y ) }.
% 97.17/97.54 (66) {G0,W7,D2,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y ), alpha4( X
% 97.17/97.54 , Y ) }.
% 97.17/97.54 (67) {G0,W10,D2,L4,V3,M4} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 97.17/97.54 aNormalFormOfIn0( Z, X, Y ), aElement0( Z ) }.
% 97.17/97.54 (68) {G0,W12,D2,L4,V3,M4} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 97.17/97.54 aNormalFormOfIn0( Z, X, Y ), alpha5( X, Y, Z ) }.
% 97.17/97.54 (70) {G0,W8,D2,L2,V3,M2} I { ! alpha5( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z )
% 97.17/97.54 }.
% 97.17/97.54 (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 97.17/97.54 (76) {G0,W2,D2,L1,V0,M1} I { isTerminating0( xR ) }.
% 97.17/97.54 (77) {G0,W2,D2,L1,V0,M1} I { aElement0( xa ) }.
% 97.17/97.54 (78) {G0,W2,D2,L1,V0,M1} I { aElement0( xb ) }.
% 97.17/97.54 (80) {G0,W21,D3,L7,V5,M7} I { ! aElement0( X ), ! aElement0( Y ), !
% 97.17/97.54 aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, Z
% 97.17/97.54 ), ! iLess0( X, xa ), aElement0( skol11( T, U ) ) }.
% 97.17/97.54 (81) {G0,W23,D3,L7,V4,M7} I { ! aElement0( X ), ! aElement0( Y ), !
% 97.17/97.54 aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, Z
% 97.17/97.54 ), ! iLess0( X, xa ), sdtmndtasgtdt0( Z, xR, skol11( T, Z ) ) }.
% 97.17/97.54 (82) {G0,W23,D3,L7,V3,M7} I { ! aElement0( X ), ! aElement0( Y ), !
% 97.17/97.54 aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, Z
% 97.17/97.54 ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, Z ) ) }.
% 97.17/97.54 (83) {G0,W4,D2,L1,V0,M1} I { sdtmndtplgtdt0( xa, xR, xb ) }.
% 97.17/97.54 (85) {G0,W2,D2,L1,V0,M1} I { aElement0( xu ) }.
% 97.17/97.54 (86) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xu, xa, xR ) }.
% 97.17/97.54 (87) {G0,W4,D2,L1,V0,M1} I { sdtmndtasgtdt0( xu, xR, xb ) }.
% 97.17/97.54 (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 97.17/97.54 (89) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xv, xa, xR ) }.
% 97.17/97.54 (91) {G0,W2,D2,L1,V0,M1} I { aElement0( xw ) }.
% 97.17/97.54 (92) {G0,W4,D2,L1,V0,M1} I { sdtmndtasgtdt0( xu, xR, xw ) }.
% 97.17/97.54 (94) {G0,W4,D2,L1,V0,M1} I { aNormalFormOfIn0( xd, xw, xR ) }.
% 97.17/97.54 (95) {G0,W10,D2,L3,V1,M3} I { ! aElement0( X ), ! sdtmndtasgtdt0( xb, xR, X
% 97.17/97.54 ), ! sdtmndtasgtdt0( xd, xR, X ) }.
% 97.17/97.54 (108) {G1,W15,D3,L5,V4,M5} F(80);f { ! aElement0( X ), ! aElement0( Y ), !
% 97.17/97.54 sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ), aElement0( skol11( Z, T )
% 97.17/97.54 ) }.
% 97.17/97.54 (111) {G1,W17,D3,L5,V3,M5} F(81);f { ! aElement0( X ), ! aElement0( Y ), !
% 97.17/97.54 sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y, xR,
% 97.17/97.54 skol11( Z, Y ) ) }.
% 97.17/97.54 (140) {G1,W12,D2,L4,V2,M4} R(3,74) { ! aElement0( X ), ! aElement0( Y ), !
% 97.17/97.54 aReductOfIn0( Y, X, xR ), sdtmndtplgtdt0( X, xR, Y ) }.
% 97.17/97.54 (272) {G1,W5,D2,L2,V1,M2} R(66,77) { ! aElement0( X ), alpha4( xa, X ) }.
% 97.17/97.54 (295) {G2,W3,D2,L1,V0,M1} R(272,78) { alpha4( xa, xb ) }.
% 97.17/97.54 (298) {G2,W3,D2,L1,V0,M1} R(272,85) { alpha4( xa, xu ) }.
% 97.17/97.54 (299) {G2,W3,D2,L1,V0,M1} R(272,88) { alpha4( xa, xv ) }.
% 97.17/97.54 (510) {G1,W11,D2,L4,V2,M4} R(13,74) { ! aElement0( X ), ! aElement0( Y ), !
% 97.17/97.54 X = Y, sdtmndtasgtdt0( X, xR, Y ) }.
% 97.17/97.54 (531) {G2,W6,D2,L2,V1,M2} F(510);q { ! aElement0( X ), sdtmndtasgtdt0( X,
% 97.17/97.54 xR, X ) }.
% 97.17/97.54 (638) {G1,W18,D2,L6,V3,M6} R(15,85) { ! aRewritingSystem0( X ), ! aElement0
% 97.17/97.54 ( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( xu, X, Y ), ! sdtmndtasgtdt0(
% 97.17/97.54 Y, X, Z ), sdtmndtasgtdt0( xu, X, Z ) }.
% 97.17/97.54 (853) {G3,W4,D2,L1,V0,M1} R(531,78) { sdtmndtasgtdt0( xb, xR, xb ) }.
% 97.17/97.54 (857) {G3,W4,D2,L1,V0,M1} R(531,88) { sdtmndtasgtdt0( xv, xR, xv ) }.
% 97.17/97.54 (1804) {G1,W7,D2,L2,V2,M2} R(58,74);r(76) { ! alpha4( X, Y ), alpha11( xR,
% 97.17/97.54 X, Y ) }.
% 97.17/97.54 (1954) {G3,W4,D2,L1,V0,M1} R(1804,299) { alpha11( xR, xa, xv ) }.
% 97.17/97.54 (1955) {G3,W4,D2,L1,V0,M1} R(1804,298) { alpha11( xR, xa, xu ) }.
% 97.17/97.54 (1957) {G3,W4,D2,L1,V0,M1} R(1804,295) { alpha11( xR, xa, xb ) }.
% 97.17/97.54 (2021) {G4,W3,D2,L1,V0,M1} R(61,83);r(1957) { iLess0( xb, xa ) }.
% 97.17/97.54 (2108) {G1,W4,D2,L2,V0,M2} R(67,94);r(91) { ! aRewritingSystem0( xR ),
% 97.17/97.54 aElement0( xd ) }.
% 97.17/97.54 (2153) {G1,W6,D2,L2,V0,M2} R(68,94);r(91) { ! aRewritingSystem0( xR ),
% 97.17/97.54 alpha5( xw, xR, xd ) }.
% 97.17/97.54 (2273) {G2,W2,D2,L1,V0,M1} S(2108);r(74) { aElement0( xd ) }.
% 97.17/97.54 (2465) {G1,W21,D3,L6,V2,M6} R(82,78) { ! aElement0( X ), ! aElement0( Y ),
% 97.17/97.54 ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, xb ), ! iLess0( X
% 97.17/97.54 , xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, xb ) ) }.
% 97.17/97.54 (2812) {G4,W7,D3,L2,V2,M2} R(108,857);f;r(88) { ! iLess0( xv, xa ),
% 97.17/97.54 aElement0( skol11( X, Y ) ) }.
% 97.17/97.54 (2842) {G4,W9,D3,L2,V1,M2} R(111,853);f;r(78) { ! iLess0( xb, xa ),
% 97.17/97.54 sdtmndtasgtdt0( xb, xR, skol11( X, xb ) ) }.
% 97.17/97.54 (4306) {G2,W4,D2,L1,V0,M1} S(2153);r(74) { alpha5( xw, xR, xd ) }.
% 97.17/97.54 (4308) {G3,W4,D2,L1,V0,M1} R(4306,70) { sdtmndtasgtdt0( xw, xR, xd ) }.
% 97.17/97.54 (4355) {G2,W6,D2,L2,V0,M2} R(140,86);r(77) { ! aElement0( xu ),
% 97.17/97.54 sdtmndtplgtdt0( xa, xR, xu ) }.
% 97.17/97.54 (4356) {G2,W6,D2,L2,V0,M2} R(140,89);r(77) { ! aElement0( xv ),
% 97.17/97.54 sdtmndtplgtdt0( xa, xR, xv ) }.
% 97.17/97.54 (4474) {G3,W4,D2,L1,V0,M1} S(4355);r(85) { sdtmndtplgtdt0( xa, xR, xu ) }.
% 97.17/97.54 (4477) {G4,W3,D2,L1,V0,M1} R(4474,61);r(1955) { iLess0( xu, xa ) }.
% 97.17/97.54 (4489) {G3,W4,D2,L1,V0,M1} S(4356);r(88) { sdtmndtplgtdt0( xa, xR, xv ) }.
% 97.17/97.54 (4492) {G4,W3,D2,L1,V0,M1} R(4489,61);r(1954) { iLess0( xv, xa ) }.
% 97.17/97.54 (9960) {G5,W4,D3,L1,V2,M1} S(2812);r(4492) { aElement0( skol11( X, Y ) )
% 97.17/97.54 }.
% 97.17/97.54 (21312) {G5,W6,D3,L1,V1,M1} S(2842);r(2021) { sdtmndtasgtdt0( xb, xR,
% 97.17/97.54 skol11( X, xb ) ) }.
% 97.17/97.54 (21784) {G4,W12,D2,L4,V0,M4} R(638,4308);r(74) { ! aElement0( xw ), !
% 97.17/97.54 aElement0( xd ), ! sdtmndtasgtdt0( xu, xR, xw ), sdtmndtasgtdt0( xu, xR,
% 97.17/97.54 xd ) }.
% 97.17/97.54 (23029) {G6,W6,D3,L1,V1,M1} R(21312,95);r(9960) { ! sdtmndtasgtdt0( xd, xR
% 97.17/97.54 , skol11( X, xb ) ) }.
% 97.17/97.54 (43720) {G5,W4,D2,L1,V0,M1} S(21784);r(91);r(2273);r(92) { sdtmndtasgtdt0(
% 97.17/97.54 xu, xR, xd ) }.
% 97.17/97.54 (147823) {G6,W15,D3,L4,V0,M4} R(2465,43720);r(85) { ! aElement0( xd ), !
% 97.17/97.54 sdtmndtasgtdt0( xu, xR, xb ), ! iLess0( xu, xa ), sdtmndtasgtdt0( xd, xR
% 97.17/97.54 , skol11( xd, xb ) ) }.
% 97.17/97.54 (148150) {G7,W0,D0,L0,V0,M0} S(147823);r(2273);r(87);r(4477);r(23029) {
% 97.17/97.54 }.
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 % SZS output end Refutation
% 97.17/97.54 found a proof!
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Unprocessed initial clauses:
% 97.17/97.54
% 97.17/97.54 (148152) {G0,W1,D1,L1,V0,M1} { && }.
% 97.17/97.54 (148153) {G0,W1,D1,L1,V0,M1} { && }.
% 97.17/97.54 (148154) {G0,W10,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aReductOfIn0( Z, X, Y ), aElement0( Z ) }.
% 97.17/97.54 (148155) {G0,W1,D1,L1,V0,M1} { && }.
% 97.17/97.54 (148156) {G0,W1,D1,L1,V0,M1} { && }.
% 97.17/97.54 (148157) {G0,W18,D2,L6,V3,M6} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ), aReductOfIn0( Z, X, Y )
% 97.17/97.54 , alpha1( X, Y, Z ) }.
% 97.17/97.54 (148158) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aElement0( Z ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z )
% 97.17/97.54 }.
% 97.17/97.54 (148159) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aElement0( Z ), ! alpha1( X, Y, Z ), sdtmndtplgtdt0( X, Y, Z ) }.
% 97.17/97.54 (148160) {G0,W9,D3,L2,V6,M2} { ! alpha1( X, Y, Z ), aElement0( skol1( T, U
% 97.17/97.54 , W ) ) }.
% 97.17/97.54 (148161) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), alpha6( X, Y, Z,
% 97.17/97.54 skol1( X, Y, Z ) ) }.
% 97.17/97.54 (148162) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha6( X, Y, Z, T ),
% 97.17/97.54 alpha1( X, Y, Z ) }.
% 97.17/97.54 (148163) {G0,W9,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), aReductOfIn0( T, X
% 97.17/97.54 , Y ) }.
% 97.17/97.54 (148164) {G0,W9,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), sdtmndtplgtdt0( T,
% 97.17/97.54 Y, Z ) }.
% 97.17/97.54 (148165) {G0,W13,D2,L3,V4,M3} { ! aReductOfIn0( T, X, Y ), !
% 97.17/97.54 sdtmndtplgtdt0( T, Y, Z ), alpha6( X, Y, Z, T ) }.
% 97.17/97.54 (148166) {G0,W20,D2,L7,V4,M7} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aElement0( Z ), ! aElement0( T ), ! sdtmndtplgtdt0( X, Y, Z ), !
% 97.17/97.54 sdtmndtplgtdt0( Z, Y, T ), sdtmndtplgtdt0( X, Y, T ) }.
% 97.17/97.54 (148167) {G0,W17,D2,L6,V3,M6} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aElement0( Z ), ! sdtmndtasgtdt0( X, Y, Z ), X = Z, sdtmndtplgtdt0( X
% 97.17/97.54 , Y, Z ) }.
% 97.17/97.54 (148168) {G0,W13,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y, Z ) }.
% 97.17/97.54 (148169) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z
% 97.17/97.54 ) }.
% 97.17/97.54 (148170) {G0,W20,D2,L7,V4,M7} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aElement0( Z ), ! aElement0( T ), ! sdtmndtasgtdt0( X, Y, Z ), !
% 97.17/97.54 sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X, Y, T ) }.
% 97.17/97.54 (148171) {G0,W12,D2,L4,V3,M4} { ! aRewritingSystem0( X ), ! isConfluent0(
% 97.17/97.54 X ), ! alpha2( X, Y, Z ), alpha7( X, Y, Z ) }.
% 97.17/97.54 (148172) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha2( X, skol2
% 97.17/97.54 ( X ), skol12( X ) ), isConfluent0( X ) }.
% 97.17/97.54 (148173) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha7( X,
% 97.17/97.54 skol2( X ), skol12( X ) ), isConfluent0( X ) }.
% 97.17/97.54 (148174) {G0,W9,D3,L2,V6,M2} { ! alpha7( X, Y, Z ), aElement0( skol3( T, U
% 97.17/97.54 , W ) ) }.
% 97.17/97.54 (148175) {G0,W12,D3,L2,V3,M2} { ! alpha7( X, Y, Z ), alpha12( X, Y, Z,
% 97.17/97.54 skol3( X, Y, Z ) ) }.
% 97.17/97.54 (148176) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha12( X, Y, Z, T )
% 97.17/97.54 , alpha7( X, Y, Z ) }.
% 97.17/97.54 (148177) {G0,W9,D2,L2,V4,M2} { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Y
% 97.17/97.54 , X, T ) }.
% 97.17/97.54 (148178) {G0,W9,D2,L2,V4,M2} { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Z
% 97.17/97.54 , X, T ) }.
% 97.17/97.54 (148179) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( Y, X, T ), !
% 97.17/97.54 sdtmndtasgtdt0( Z, X, T ), alpha12( X, Y, Z, T ) }.
% 97.17/97.54 (148180) {G0,W9,D3,L2,V6,M2} { ! alpha2( X, Y, Z ), aElement0( skol4( T, U
% 97.17/97.54 , W ) ) }.
% 97.17/97.54 (148181) {G0,W12,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), alpha8( X, Y, Z,
% 97.17/97.54 skol4( X, Y, Z ) ) }.
% 97.17/97.54 (148182) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha8( X, Y, Z, T ),
% 97.17/97.54 alpha2( X, Y, Z ) }.
% 97.17/97.54 (148183) {G0,W7,D2,L2,V4,M2} { ! alpha8( X, Y, Z, T ), aElement0( Y ) }.
% 97.17/97.54 (148184) {G0,W10,D2,L2,V4,M2} { ! alpha8( X, Y, Z, T ), alpha13( X, Y, Z,
% 97.17/97.54 T ) }.
% 97.17/97.54 (148185) {G0,W12,D2,L3,V4,M3} { ! aElement0( Y ), ! alpha13( X, Y, Z, T )
% 97.17/97.54 , alpha8( X, Y, Z, T ) }.
% 97.17/97.54 (148186) {G0,W7,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), aElement0( Z ) }.
% 97.17/97.54 (148187) {G0,W10,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), alpha16( X, Y, Z
% 97.17/97.54 , T ) }.
% 97.17/97.54 (148188) {G0,W12,D2,L3,V4,M3} { ! aElement0( Z ), ! alpha16( X, Y, Z, T )
% 97.17/97.54 , alpha13( X, Y, Z, T ) }.
% 97.17/97.54 (148189) {G0,W9,D2,L2,V4,M2} { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T
% 97.17/97.54 , X, Y ) }.
% 97.17/97.54 (148190) {G0,W9,D2,L2,V4,M2} { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T
% 97.17/97.54 , X, Z ) }.
% 97.17/97.54 (148191) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( T, X, Y ), !
% 97.17/97.54 sdtmndtasgtdt0( T, X, Z ), alpha16( X, Y, Z, T ) }.
% 97.17/97.54 (148192) {G0,W12,D2,L4,V3,M4} { ! aRewritingSystem0( X ), !
% 97.17/97.54 isLocallyConfluent0( X ), ! alpha3( X, Y, Z ), alpha9( X, Y, Z ) }.
% 97.17/97.54 (148193) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha3( X, skol5
% 97.17/97.54 ( X ), skol13( X ) ), isLocallyConfluent0( X ) }.
% 97.17/97.54 (148194) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha9( X,
% 97.17/97.54 skol5( X ), skol13( X ) ), isLocallyConfluent0( X ) }.
% 97.17/97.54 (148195) {G0,W9,D3,L2,V6,M2} { ! alpha9( X, Y, Z ), aElement0( skol6( T, U
% 97.17/97.54 , W ) ) }.
% 97.17/97.54 (148196) {G0,W12,D3,L2,V3,M2} { ! alpha9( X, Y, Z ), alpha14( X, Y, Z,
% 97.17/97.54 skol6( X, Y, Z ) ) }.
% 97.17/97.54 (148197) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha14( X, Y, Z, T )
% 97.17/97.54 , alpha9( X, Y, Z ) }.
% 97.17/97.54 (148198) {G0,W9,D2,L2,V4,M2} { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Y
% 97.17/97.54 , X, T ) }.
% 97.17/97.54 (148199) {G0,W9,D2,L2,V4,M2} { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Z
% 97.17/97.54 , X, T ) }.
% 97.17/97.54 (148200) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( Y, X, T ), !
% 97.17/97.54 sdtmndtasgtdt0( Z, X, T ), alpha14( X, Y, Z, T ) }.
% 97.17/97.54 (148201) {G0,W9,D3,L2,V6,M2} { ! alpha3( X, Y, Z ), aElement0( skol7( T, U
% 97.17/97.54 , W ) ) }.
% 97.17/97.54 (148202) {G0,W12,D3,L2,V3,M2} { ! alpha3( X, Y, Z ), alpha10( X, Y, Z,
% 97.17/97.54 skol7( X, Y, Z ) ) }.
% 97.17/97.54 (148203) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha10( X, Y, Z, T )
% 97.17/97.54 , alpha3( X, Y, Z ) }.
% 97.17/97.54 (148204) {G0,W7,D2,L2,V4,M2} { ! alpha10( X, Y, Z, T ), aElement0( Y ) }.
% 97.17/97.54 (148205) {G0,W10,D2,L2,V4,M2} { ! alpha10( X, Y, Z, T ), alpha15( X, Y, Z
% 97.17/97.54 , T ) }.
% 97.17/97.54 (148206) {G0,W12,D2,L3,V4,M3} { ! aElement0( Y ), ! alpha15( X, Y, Z, T )
% 97.17/97.54 , alpha10( X, Y, Z, T ) }.
% 97.17/97.54 (148207) {G0,W7,D2,L2,V4,M2} { ! alpha15( X, Y, Z, T ), aElement0( Z ) }.
% 97.17/97.54 (148208) {G0,W10,D2,L2,V4,M2} { ! alpha15( X, Y, Z, T ), alpha17( X, Y, Z
% 97.17/97.54 , T ) }.
% 97.17/97.54 (148209) {G0,W12,D2,L3,V4,M3} { ! aElement0( Z ), ! alpha17( X, Y, Z, T )
% 97.17/97.54 , alpha15( X, Y, Z, T ) }.
% 97.17/97.54 (148210) {G0,W9,D2,L2,V4,M2} { ! alpha17( X, Y, Z, T ), aReductOfIn0( Y, T
% 97.17/97.54 , X ) }.
% 97.17/97.54 (148211) {G0,W9,D2,L2,V4,M2} { ! alpha17( X, Y, Z, T ), aReductOfIn0( Z, T
% 97.17/97.54 , X ) }.
% 97.17/97.54 (148212) {G0,W13,D2,L3,V4,M3} { ! aReductOfIn0( Y, T, X ), ! aReductOfIn0
% 97.17/97.54 ( Z, T, X ), alpha17( X, Y, Z, T ) }.
% 97.17/97.54 (148213) {G0,W11,D2,L4,V3,M4} { ! aRewritingSystem0( X ), ! isTerminating0
% 97.17/97.54 ( X ), ! alpha4( Y, Z ), alpha11( X, Y, Z ) }.
% 97.17/97.54 (148214) {G0,W9,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha4( skol8( X
% 97.17/97.54 ), skol14( X ) ), isTerminating0( X ) }.
% 97.17/97.54 (148215) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha11( X,
% 97.17/97.54 skol8( X ), skol14( X ) ), isTerminating0( X ) }.
% 97.17/97.54 (148216) {G0,W11,D2,L3,V3,M3} { ! alpha11( X, Y, Z ), ! sdtmndtplgtdt0( Y
% 97.17/97.54 , X, Z ), iLess0( Z, Y ) }.
% 97.17/97.54 (148217) {G0,W8,D2,L2,V3,M2} { sdtmndtplgtdt0( Y, X, Z ), alpha11( X, Y, Z
% 97.17/97.54 ) }.
% 97.17/97.54 (148218) {G0,W7,D2,L2,V3,M2} { ! iLess0( Z, Y ), alpha11( X, Y, Z ) }.
% 97.17/97.54 (148219) {G0,W5,D2,L2,V2,M2} { ! alpha4( X, Y ), aElement0( X ) }.
% 97.17/97.54 (148220) {G0,W5,D2,L2,V2,M2} { ! alpha4( X, Y ), aElement0( Y ) }.
% 97.17/97.54 (148221) {G0,W7,D2,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y ), alpha4
% 97.17/97.54 ( X, Y ) }.
% 97.17/97.54 (148222) {G0,W10,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aNormalFormOfIn0( Z, X, Y ), aElement0( Z ) }.
% 97.17/97.54 (148223) {G0,W12,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aNormalFormOfIn0( Z, X, Y ), alpha5( X, Y, Z ) }.
% 97.17/97.54 (148224) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 97.17/97.54 , ! aElement0( Z ), ! alpha5( X, Y, Z ), aNormalFormOfIn0( Z, X, Y ) }.
% 97.17/97.54 (148225) {G0,W8,D2,L2,V3,M2} { ! alpha5( X, Y, Z ), sdtmndtasgtdt0( X, Y,
% 97.17/97.54 Z ) }.
% 97.17/97.54 (148226) {G0,W8,D2,L2,V4,M2} { ! alpha5( X, Y, Z ), ! aReductOfIn0( T, Z,
% 97.17/97.54 Y ) }.
% 97.17/97.54 (148227) {G0,W14,D3,L3,V3,M3} { ! sdtmndtasgtdt0( X, Y, Z ), aReductOfIn0
% 97.17/97.54 ( skol9( Y, Z ), Z, Y ), alpha5( X, Y, Z ) }.
% 97.17/97.54 (148228) {G0,W12,D3,L4,V2,M4} { ! aRewritingSystem0( X ), ! isTerminating0
% 97.17/97.54 ( X ), ! aElement0( Y ), aNormalFormOfIn0( skol10( X, Y ), Y, X ) }.
% 97.17/97.54 (148229) {G0,W2,D2,L1,V0,M1} { aRewritingSystem0( xR ) }.
% 97.17/97.54 (148230) {G0,W2,D2,L1,V0,M1} { isLocallyConfluent0( xR ) }.
% 97.17/97.54 (148231) {G0,W2,D2,L1,V0,M1} { isTerminating0( xR ) }.
% 97.17/97.54 (148232) {G0,W2,D2,L1,V0,M1} { aElement0( xa ) }.
% 97.17/97.54 (148233) {G0,W2,D2,L1,V0,M1} { aElement0( xb ) }.
% 97.17/97.54 (148234) {G0,W2,D2,L1,V0,M1} { aElement0( xc ) }.
% 97.17/97.54 (148235) {G0,W21,D3,L7,V5,M7} { ! aElement0( X ), ! aElement0( Y ), !
% 97.17/97.54 aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, Z
% 97.17/97.54 ), ! iLess0( X, xa ), aElement0( skol11( T, U ) ) }.
% 97.17/97.54 (148236) {G0,W23,D3,L7,V4,M7} { ! aElement0( X ), ! aElement0( Y ), !
% 97.17/97.54 aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, Z
% 97.17/97.54 ), ! iLess0( X, xa ), sdtmndtasgtdt0( Z, xR, skol11( T, Z ) ) }.
% 97.17/97.54 (148237) {G0,W23,D3,L7,V3,M7} { ! aElement0( X ), ! aElement0( Y ), !
% 97.17/97.54 aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, Z
% 97.17/97.54 ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, Z ) ) }.
% 97.17/97.54 (148238) {G0,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xb ) }.
% 97.17/97.54 (148239) {G0,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xc ) }.
% 97.17/97.54 (148240) {G0,W2,D2,L1,V0,M1} { aElement0( xu ) }.
% 97.17/97.54 (148241) {G0,W4,D2,L1,V0,M1} { aReductOfIn0( xu, xa, xR ) }.
% 97.17/97.54 (148242) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, xb ) }.
% 97.17/97.54 (148243) {G0,W2,D2,L1,V0,M1} { aElement0( xv ) }.
% 97.17/97.54 (148244) {G0,W4,D2,L1,V0,M1} { aReductOfIn0( xv, xa, xR ) }.
% 97.17/97.54 (148245) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, xc ) }.
% 97.17/97.54 (148246) {G0,W2,D2,L1,V0,M1} { aElement0( xw ) }.
% 97.17/97.54 (148247) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, xw ) }.
% 97.17/97.54 (148248) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, xw ) }.
% 97.17/97.54 (148249) {G0,W4,D2,L1,V0,M1} { aNormalFormOfIn0( xd, xw, xR ) }.
% 97.17/97.54 (148250) {G0,W10,D2,L3,V1,M3} { ! aElement0( X ), ! sdtmndtasgtdt0( xb, xR
% 97.17/97.54 , X ), ! sdtmndtasgtdt0( xd, xR, X ) }.
% 97.17/97.54
% 97.17/97.54
% 97.17/97.54 Total Proof:
% 97.17/97.54
% 97.17/97.54 subsumption: (3) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aReductOfIn0( Z, X, Y ),
% 97.17/97.54 sdtmndtplgtdt0( X, Y, Z ) }.
% 97.17/97.54 parent0: (148158) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aReductOfIn0( Z, X, Y ),
% 97.17/97.54 sdtmndtplgtdt0( X, Y, Z ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 4 ==> 4
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (13) {G0,W13,D2,L5,V3,M5} I { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y,
% 97.17/97.54 Z ) }.
% 97.17/97.54 parent0: (148168) {G0,W13,D2,L5,V3,M5} { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y,
% 97.17/97.54 Z ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 4 ==> 4
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (15) {G0,W20,D2,L7,V4,M7} I { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 97.17/97.54 sdtmndtasgtdt0( X, Y, Z ), ! sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X
% 97.17/97.54 , Y, T ) }.
% 97.17/97.54 parent0: (148170) {G0,W20,D2,L7,V4,M7} { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 97.17/97.54 sdtmndtasgtdt0( X, Y, Z ), ! sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X
% 97.17/97.54 , Y, T ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 T := T
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 4 ==> 4
% 97.17/97.54 5 ==> 5
% 97.17/97.54 6 ==> 6
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (58) {G0,W11,D2,L4,V3,M4} I { ! aRewritingSystem0( X ), !
% 97.17/97.54 isTerminating0( X ), ! alpha4( Y, Z ), alpha11( X, Y, Z ) }.
% 97.17/97.54 parent0: (148213) {G0,W11,D2,L4,V3,M4} { ! aRewritingSystem0( X ), !
% 97.17/97.54 isTerminating0( X ), ! alpha4( Y, Z ), alpha11( X, Y, Z ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (61) {G0,W11,D2,L3,V3,M3} I { ! alpha11( X, Y, Z ), !
% 97.17/97.54 sdtmndtplgtdt0( Y, X, Z ), iLess0( Z, Y ) }.
% 97.17/97.54 parent0: (148216) {G0,W11,D2,L3,V3,M3} { ! alpha11( X, Y, Z ), !
% 97.17/97.54 sdtmndtplgtdt0( Y, X, Z ), iLess0( Z, Y ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (66) {G0,W7,D2,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), alpha4( X, Y ) }.
% 97.17/97.54 parent0: (148221) {G0,W7,D2,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y )
% 97.17/97.54 , alpha4( X, Y ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (67) {G0,W10,D2,L4,V3,M4} I { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y ), aElement0( Z ) }.
% 97.17/97.54 parent0: (148222) {G0,W10,D2,L4,V3,M4} { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y ), aElement0( Z ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (68) {G0,W12,D2,L4,V3,M4} I { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y ), alpha5( X, Y, Z )
% 97.17/97.54 }.
% 97.17/97.54 parent0: (148223) {G0,W12,D2,L4,V3,M4} { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y ), alpha5( X, Y, Z )
% 97.17/97.54 }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (70) {G0,W8,D2,L2,V3,M2} I { ! alpha5( X, Y, Z ),
% 97.17/97.54 sdtmndtasgtdt0( X, Y, Z ) }.
% 97.17/97.54 parent0: (148225) {G0,W8,D2,L2,V3,M2} { ! alpha5( X, Y, Z ),
% 97.17/97.54 sdtmndtasgtdt0( X, Y, Z ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 97.17/97.54 parent0: (148229) {G0,W2,D2,L1,V0,M1} { aRewritingSystem0( xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (76) {G0,W2,D2,L1,V0,M1} I { isTerminating0( xR ) }.
% 97.17/97.54 parent0: (148231) {G0,W2,D2,L1,V0,M1} { isTerminating0( xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (77) {G0,W2,D2,L1,V0,M1} I { aElement0( xa ) }.
% 97.17/97.54 parent0: (148232) {G0,W2,D2,L1,V0,M1} { aElement0( xa ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( xb ) }.
% 97.17/97.54 parent0: (148233) {G0,W2,D2,L1,V0,M1} { aElement0( xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (80) {G0,W21,D3,L7,V5,M7} I { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X,
% 97.17/97.54 xR, Z ), ! iLess0( X, xa ), aElement0( skol11( T, U ) ) }.
% 97.17/97.54 parent0: (148235) {G0,W21,D3,L7,V5,M7} { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X,
% 97.17/97.54 xR, Z ), ! iLess0( X, xa ), aElement0( skol11( T, U ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Y
% 97.17/97.54 T := T
% 97.17/97.54 U := U
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 1
% 97.17/97.54 3 ==> 3
% 97.17/97.54 4 ==> 3
% 97.17/97.54 5 ==> 5
% 97.17/97.54 6 ==> 6
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (81) {G0,W23,D3,L7,V4,M7} I { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X,
% 97.17/97.54 xR, Z ), ! iLess0( X, xa ), sdtmndtasgtdt0( Z, xR, skol11( T, Z ) ) }.
% 97.17/97.54 parent0: (148236) {G0,W23,D3,L7,V4,M7} { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X,
% 97.17/97.54 xR, Z ), ! iLess0( X, xa ), sdtmndtasgtdt0( Z, xR, skol11( T, Z ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 T := T
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 4 ==> 4
% 97.17/97.54 5 ==> 5
% 97.17/97.54 6 ==> 6
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (82) {G0,W23,D3,L7,V3,M7} I { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X,
% 97.17/97.54 xR, Z ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, Z ) ) }.
% 97.17/97.54 parent0: (148237) {G0,W23,D3,L7,V3,M7} { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X,
% 97.17/97.54 xR, Z ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, Z ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 4 ==> 4
% 97.17/97.54 5 ==> 5
% 97.17/97.54 6 ==> 6
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (83) {G0,W4,D2,L1,V0,M1} I { sdtmndtplgtdt0( xa, xR, xb ) }.
% 97.17/97.54 parent0: (148238) {G0,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (85) {G0,W2,D2,L1,V0,M1} I { aElement0( xu ) }.
% 97.17/97.54 parent0: (148240) {G0,W2,D2,L1,V0,M1} { aElement0( xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (86) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xu, xa, xR ) }.
% 97.17/97.54 parent0: (148241) {G0,W4,D2,L1,V0,M1} { aReductOfIn0( xu, xa, xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (87) {G0,W4,D2,L1,V0,M1} I { sdtmndtasgtdt0( xu, xR, xb ) }.
% 97.17/97.54 parent0: (148242) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 97.17/97.54 parent0: (148243) {G0,W2,D2,L1,V0,M1} { aElement0( xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (89) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xv, xa, xR ) }.
% 97.17/97.54 parent0: (148244) {G0,W4,D2,L1,V0,M1} { aReductOfIn0( xv, xa, xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (91) {G0,W2,D2,L1,V0,M1} I { aElement0( xw ) }.
% 97.17/97.54 parent0: (148246) {G0,W2,D2,L1,V0,M1} { aElement0( xw ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (92) {G0,W4,D2,L1,V0,M1} I { sdtmndtasgtdt0( xu, xR, xw ) }.
% 97.17/97.54 parent0: (148247) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, xw ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (94) {G0,W4,D2,L1,V0,M1} I { aNormalFormOfIn0( xd, xw, xR )
% 97.17/97.54 }.
% 97.17/97.54 parent0: (148249) {G0,W4,D2,L1,V0,M1} { aNormalFormOfIn0( xd, xw, xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (95) {G0,W10,D2,L3,V1,M3} I { ! aElement0( X ), !
% 97.17/97.54 sdtmndtasgtdt0( xb, xR, X ), ! sdtmndtasgtdt0( xd, xR, X ) }.
% 97.17/97.54 parent0: (148250) {G0,W10,D2,L3,V1,M3} { ! aElement0( X ), !
% 97.17/97.54 sdtmndtasgtdt0( xb, xR, X ), ! sdtmndtasgtdt0( xd, xR, X ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 factor: (149106) {G0,W17,D3,L6,V4,M6} { ! aElement0( X ), ! aElement0( Y )
% 97.17/97.54 , ! aElement0( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ),
% 97.17/97.54 aElement0( skol11( Z, T ) ) }.
% 97.17/97.54 parent0[3, 4]: (80) {G0,W21,D3,L7,V5,M7} I { ! aElement0( X ), ! aElement0
% 97.17/97.54 ( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0(
% 97.17/97.54 X, xR, Z ), ! iLess0( X, xa ), aElement0( skol11( T, U ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Y
% 97.17/97.54 T := Z
% 97.17/97.54 U := T
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 factor: (149108) {G0,W15,D3,L5,V4,M5} { ! aElement0( X ), ! aElement0( Y )
% 97.17/97.54 , ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ), aElement0( skol11( Z,
% 97.17/97.54 T ) ) }.
% 97.17/97.54 parent0[1, 2]: (149106) {G0,W17,D3,L6,V4,M6} { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! aElement0( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0
% 97.17/97.54 ( X, xa ), aElement0( skol11( Z, T ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 T := T
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (108) {G1,W15,D3,L5,V4,M5} F(80);f { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ),
% 97.17/97.54 aElement0( skol11( Z, T ) ) }.
% 97.17/97.54 parent0: (149108) {G0,W15,D3,L5,V4,M5} { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ), aElement0( skol11( Z
% 97.17/97.54 , T ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 T := T
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 4 ==> 4
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 factor: (149112) {G0,W19,D3,L6,V3,M6} { ! aElement0( X ), ! aElement0( Y )
% 97.17/97.54 , ! aElement0( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ),
% 97.17/97.54 sdtmndtasgtdt0( Y, xR, skol11( Z, Y ) ) }.
% 97.17/97.54 parent0[3, 4]: (81) {G0,W23,D3,L7,V4,M7} I { ! aElement0( X ), ! aElement0
% 97.17/97.54 ( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0(
% 97.17/97.54 X, xR, Z ), ! iLess0( X, xa ), sdtmndtasgtdt0( Z, xR, skol11( T, Z ) )
% 97.17/97.54 }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Y
% 97.17/97.54 T := Z
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 factor: (149114) {G0,W17,D3,L5,V3,M5} { ! aElement0( X ), ! aElement0( Y )
% 97.17/97.54 , ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y, xR
% 97.17/97.54 , skol11( Z, Y ) ) }.
% 97.17/97.54 parent0[1, 2]: (149112) {G0,W19,D3,L6,V3,M6} { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! aElement0( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0
% 97.17/97.54 ( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Z, Y ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (111) {G1,W17,D3,L5,V3,M5} F(81);f { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ),
% 97.17/97.54 sdtmndtasgtdt0( Y, xR, skol11( Z, Y ) ) }.
% 97.17/97.54 parent0: (149114) {G0,W17,D3,L5,V3,M5} { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y,
% 97.17/97.54 xR, skol11( Z, Y ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 4 ==> 4
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149116) {G1,W12,D2,L4,V2,M4} { ! aElement0( X ), ! aElement0
% 97.17/97.54 ( Y ), ! aReductOfIn0( Y, X, xR ), sdtmndtplgtdt0( X, xR, Y ) }.
% 97.17/97.54 parent0[1]: (3) {G0,W14,D2,L5,V3,M5} I { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aReductOfIn0( Z, X, Y ),
% 97.17/97.54 sdtmndtplgtdt0( X, Y, Z ) }.
% 97.17/97.54 parent1[0]: (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := xR
% 97.17/97.54 Z := Y
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (140) {G1,W12,D2,L4,V2,M4} R(3,74) { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! aReductOfIn0( Y, X, xR ), sdtmndtplgtdt0( X, xR, Y )
% 97.17/97.54 }.
% 97.17/97.54 parent0: (149116) {G1,W12,D2,L4,V2,M4} { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! aReductOfIn0( Y, X, xR ), sdtmndtplgtdt0( X, xR, Y ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149118) {G1,W5,D2,L2,V1,M2} { ! aElement0( X ), alpha4( xa, X
% 97.17/97.54 ) }.
% 97.17/97.54 parent0[0]: (66) {G0,W7,D2,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 97.17/97.54 , alpha4( X, Y ) }.
% 97.17/97.54 parent1[0]: (77) {G0,W2,D2,L1,V0,M1} I { aElement0( xa ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xa
% 97.17/97.54 Y := X
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (272) {G1,W5,D2,L2,V1,M2} R(66,77) { ! aElement0( X ), alpha4
% 97.17/97.54 ( xa, X ) }.
% 97.17/97.54 parent0: (149118) {G1,W5,D2,L2,V1,M2} { ! aElement0( X ), alpha4( xa, X )
% 97.17/97.54 }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149120) {G1,W3,D2,L1,V0,M1} { alpha4( xa, xb ) }.
% 97.17/97.54 parent0[0]: (272) {G1,W5,D2,L2,V1,M2} R(66,77) { ! aElement0( X ), alpha4(
% 97.17/97.54 xa, X ) }.
% 97.17/97.54 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xb
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (295) {G2,W3,D2,L1,V0,M1} R(272,78) { alpha4( xa, xb ) }.
% 97.17/97.54 parent0: (149120) {G1,W3,D2,L1,V0,M1} { alpha4( xa, xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149121) {G1,W3,D2,L1,V0,M1} { alpha4( xa, xu ) }.
% 97.17/97.54 parent0[0]: (272) {G1,W5,D2,L2,V1,M2} R(66,77) { ! aElement0( X ), alpha4(
% 97.17/97.54 xa, X ) }.
% 97.17/97.54 parent1[0]: (85) {G0,W2,D2,L1,V0,M1} I { aElement0( xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xu
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (298) {G2,W3,D2,L1,V0,M1} R(272,85) { alpha4( xa, xu ) }.
% 97.17/97.54 parent0: (149121) {G1,W3,D2,L1,V0,M1} { alpha4( xa, xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149122) {G1,W3,D2,L1,V0,M1} { alpha4( xa, xv ) }.
% 97.17/97.54 parent0[0]: (272) {G1,W5,D2,L2,V1,M2} R(66,77) { ! aElement0( X ), alpha4(
% 97.17/97.54 xa, X ) }.
% 97.17/97.54 parent1[0]: (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xv
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (299) {G2,W3,D2,L1,V0,M1} R(272,88) { alpha4( xa, xv ) }.
% 97.17/97.54 parent0: (149122) {G1,W3,D2,L1,V0,M1} { alpha4( xa, xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 eqswap: (149123) {G0,W13,D2,L5,V3,M5} { ! Y = X, ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Z ), ! aElement0( Y ), sdtmndtasgtdt0( X, Z, Y ) }.
% 97.17/97.54 parent0[3]: (13) {G0,W13,D2,L5,V3,M5} I { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y,
% 97.17/97.54 Z ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Z
% 97.17/97.54 Z := Y
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149124) {G1,W11,D2,L4,V2,M4} { ! X = Y, ! aElement0( Y ), !
% 97.17/97.54 aElement0( X ), sdtmndtasgtdt0( Y, xR, X ) }.
% 97.17/97.54 parent0[2]: (149123) {G0,W13,D2,L5,V3,M5} { ! Y = X, ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Z ), ! aElement0( Y ), sdtmndtasgtdt0( X, Z, Y ) }.
% 97.17/97.54 parent1[0]: (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := Y
% 97.17/97.54 Y := X
% 97.17/97.54 Z := xR
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 eqswap: (149125) {G1,W11,D2,L4,V2,M4} { ! Y = X, ! aElement0( Y ), !
% 97.17/97.54 aElement0( X ), sdtmndtasgtdt0( Y, xR, X ) }.
% 97.17/97.54 parent0[0]: (149124) {G1,W11,D2,L4,V2,M4} { ! X = Y, ! aElement0( Y ), !
% 97.17/97.54 aElement0( X ), sdtmndtasgtdt0( Y, xR, X ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (510) {G1,W11,D2,L4,V2,M4} R(13,74) { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! X = Y, sdtmndtasgtdt0( X, xR, Y ) }.
% 97.17/97.54 parent0: (149125) {G1,W11,D2,L4,V2,M4} { ! Y = X, ! aElement0( Y ), !
% 97.17/97.54 aElement0( X ), sdtmndtasgtdt0( Y, xR, X ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := Y
% 97.17/97.54 Y := X
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 2
% 97.17/97.54 1 ==> 0
% 97.17/97.54 2 ==> 1
% 97.17/97.54 3 ==> 3
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 eqswap: (149127) {G1,W11,D2,L4,V2,M4} { ! Y = X, ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), sdtmndtasgtdt0( X, xR, Y ) }.
% 97.17/97.54 parent0[2]: (510) {G1,W11,D2,L4,V2,M4} R(13,74) { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! X = Y, sdtmndtasgtdt0( X, xR, Y ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 factor: (149128) {G1,W9,D2,L3,V1,M3} { ! X = X, ! aElement0( X ),
% 97.17/97.54 sdtmndtasgtdt0( X, xR, X ) }.
% 97.17/97.54 parent0[1, 2]: (149127) {G1,W11,D2,L4,V2,M4} { ! Y = X, ! aElement0( X ),
% 97.17/97.54 ! aElement0( Y ), sdtmndtasgtdt0( X, xR, Y ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := X
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 eqrefl: (149129) {G0,W6,D2,L2,V1,M2} { ! aElement0( X ), sdtmndtasgtdt0( X
% 97.17/97.54 , xR, X ) }.
% 97.17/97.54 parent0[0]: (149128) {G1,W9,D2,L3,V1,M3} { ! X = X, ! aElement0( X ),
% 97.17/97.54 sdtmndtasgtdt0( X, xR, X ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (531) {G2,W6,D2,L2,V1,M2} F(510);q { ! aElement0( X ),
% 97.17/97.54 sdtmndtasgtdt0( X, xR, X ) }.
% 97.17/97.54 parent0: (149129) {G0,W6,D2,L2,V1,M2} { ! aElement0( X ), sdtmndtasgtdt0(
% 97.17/97.54 X, xR, X ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149130) {G1,W18,D2,L6,V3,M6} { ! aRewritingSystem0( X ), !
% 97.17/97.54 aElement0( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( xu, X, Y ), !
% 97.17/97.54 sdtmndtasgtdt0( Y, X, Z ), sdtmndtasgtdt0( xu, X, Z ) }.
% 97.17/97.54 parent0[0]: (15) {G0,W20,D2,L7,V4,M7} I { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0( T ), !
% 97.17/97.54 sdtmndtasgtdt0( X, Y, Z ), ! sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X
% 97.17/97.54 , Y, T ) }.
% 97.17/97.54 parent1[0]: (85) {G0,W2,D2,L1,V0,M1} I { aElement0( xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xu
% 97.17/97.54 Y := X
% 97.17/97.54 Z := Y
% 97.17/97.54 T := Z
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (638) {G1,W18,D2,L6,V3,M6} R(15,85) { ! aRewritingSystem0( X )
% 97.17/97.54 , ! aElement0( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( xu, X, Y ), !
% 97.17/97.54 sdtmndtasgtdt0( Y, X, Z ), sdtmndtasgtdt0( xu, X, Z ) }.
% 97.17/97.54 parent0: (149130) {G1,W18,D2,L6,V3,M6} { ! aRewritingSystem0( X ), !
% 97.17/97.54 aElement0( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( xu, X, Y ), !
% 97.17/97.54 sdtmndtasgtdt0( Y, X, Z ), sdtmndtasgtdt0( xu, X, Z ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := Z
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 4 ==> 4
% 97.17/97.54 5 ==> 5
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149138) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xb, xR, xb )
% 97.17/97.54 }.
% 97.17/97.54 parent0[0]: (531) {G2,W6,D2,L2,V1,M2} F(510);q { ! aElement0( X ),
% 97.17/97.54 sdtmndtasgtdt0( X, xR, X ) }.
% 97.17/97.54 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xb
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (853) {G3,W4,D2,L1,V0,M1} R(531,78) { sdtmndtasgtdt0( xb, xR,
% 97.17/97.54 xb ) }.
% 97.17/97.54 parent0: (149138) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xb, xR, xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149139) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, xv )
% 97.17/97.54 }.
% 97.17/97.54 parent0[0]: (531) {G2,W6,D2,L2,V1,M2} F(510);q { ! aElement0( X ),
% 97.17/97.54 sdtmndtasgtdt0( X, xR, X ) }.
% 97.17/97.54 parent1[0]: (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xv
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (857) {G3,W4,D2,L1,V0,M1} R(531,88) { sdtmndtasgtdt0( xv, xR,
% 97.17/97.54 xv ) }.
% 97.17/97.54 parent0: (149139) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149140) {G1,W9,D2,L3,V2,M3} { ! isTerminating0( xR ), !
% 97.17/97.54 alpha4( X, Y ), alpha11( xR, X, Y ) }.
% 97.17/97.54 parent0[0]: (58) {G0,W11,D2,L4,V3,M4} I { ! aRewritingSystem0( X ), !
% 97.17/97.54 isTerminating0( X ), ! alpha4( Y, Z ), alpha11( X, Y, Z ) }.
% 97.17/97.54 parent1[0]: (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xR
% 97.17/97.54 Y := X
% 97.17/97.54 Z := Y
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149141) {G1,W7,D2,L2,V2,M2} { ! alpha4( X, Y ), alpha11( xR,
% 97.17/97.54 X, Y ) }.
% 97.17/97.54 parent0[0]: (149140) {G1,W9,D2,L3,V2,M3} { ! isTerminating0( xR ), !
% 97.17/97.54 alpha4( X, Y ), alpha11( xR, X, Y ) }.
% 97.17/97.54 parent1[0]: (76) {G0,W2,D2,L1,V0,M1} I { isTerminating0( xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (1804) {G1,W7,D2,L2,V2,M2} R(58,74);r(76) { ! alpha4( X, Y ),
% 97.17/97.54 alpha11( xR, X, Y ) }.
% 97.17/97.54 parent0: (149141) {G1,W7,D2,L2,V2,M2} { ! alpha4( X, Y ), alpha11( xR, X,
% 97.17/97.54 Y ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149142) {G2,W4,D2,L1,V0,M1} { alpha11( xR, xa, xv ) }.
% 97.17/97.54 parent0[0]: (1804) {G1,W7,D2,L2,V2,M2} R(58,74);r(76) { ! alpha4( X, Y ),
% 97.17/97.54 alpha11( xR, X, Y ) }.
% 97.17/97.54 parent1[0]: (299) {G2,W3,D2,L1,V0,M1} R(272,88) { alpha4( xa, xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xa
% 97.17/97.54 Y := xv
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (1954) {G3,W4,D2,L1,V0,M1} R(1804,299) { alpha11( xR, xa, xv )
% 97.17/97.54 }.
% 97.17/97.54 parent0: (149142) {G2,W4,D2,L1,V0,M1} { alpha11( xR, xa, xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149143) {G2,W4,D2,L1,V0,M1} { alpha11( xR, xa, xu ) }.
% 97.17/97.54 parent0[0]: (1804) {G1,W7,D2,L2,V2,M2} R(58,74);r(76) { ! alpha4( X, Y ),
% 97.17/97.54 alpha11( xR, X, Y ) }.
% 97.17/97.54 parent1[0]: (298) {G2,W3,D2,L1,V0,M1} R(272,85) { alpha4( xa, xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xa
% 97.17/97.54 Y := xu
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (1955) {G3,W4,D2,L1,V0,M1} R(1804,298) { alpha11( xR, xa, xu )
% 97.17/97.54 }.
% 97.17/97.54 parent0: (149143) {G2,W4,D2,L1,V0,M1} { alpha11( xR, xa, xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149144) {G2,W4,D2,L1,V0,M1} { alpha11( xR, xa, xb ) }.
% 97.17/97.54 parent0[0]: (1804) {G1,W7,D2,L2,V2,M2} R(58,74);r(76) { ! alpha4( X, Y ),
% 97.17/97.54 alpha11( xR, X, Y ) }.
% 97.17/97.54 parent1[0]: (295) {G2,W3,D2,L1,V0,M1} R(272,78) { alpha4( xa, xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xa
% 97.17/97.54 Y := xb
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (1957) {G3,W4,D2,L1,V0,M1} R(1804,295) { alpha11( xR, xa, xb )
% 97.17/97.54 }.
% 97.17/97.54 parent0: (149144) {G2,W4,D2,L1,V0,M1} { alpha11( xR, xa, xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149145) {G1,W7,D2,L2,V0,M2} { ! alpha11( xR, xa, xb ), iLess0
% 97.17/97.54 ( xb, xa ) }.
% 97.17/97.54 parent0[1]: (61) {G0,W11,D2,L3,V3,M3} I { ! alpha11( X, Y, Z ), !
% 97.17/97.54 sdtmndtplgtdt0( Y, X, Z ), iLess0( Z, Y ) }.
% 97.17/97.54 parent1[0]: (83) {G0,W4,D2,L1,V0,M1} I { sdtmndtplgtdt0( xa, xR, xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xR
% 97.17/97.54 Y := xa
% 97.17/97.54 Z := xb
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149146) {G2,W3,D2,L1,V0,M1} { iLess0( xb, xa ) }.
% 97.17/97.54 parent0[0]: (149145) {G1,W7,D2,L2,V0,M2} { ! alpha11( xR, xa, xb ), iLess0
% 97.17/97.54 ( xb, xa ) }.
% 97.17/97.54 parent1[0]: (1957) {G3,W4,D2,L1,V0,M1} R(1804,295) { alpha11( xR, xa, xb )
% 97.17/97.54 }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (2021) {G4,W3,D2,L1,V0,M1} R(61,83);r(1957) { iLess0( xb, xa )
% 97.17/97.54 }.
% 97.17/97.54 parent0: (149146) {G2,W3,D2,L1,V0,M1} { iLess0( xb, xa ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149147) {G1,W6,D2,L3,V0,M3} { ! aElement0( xw ), !
% 97.17/97.54 aRewritingSystem0( xR ), aElement0( xd ) }.
% 97.17/97.54 parent0[2]: (67) {G0,W10,D2,L4,V3,M4} I { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y ), aElement0( Z ) }.
% 97.17/97.54 parent1[0]: (94) {G0,W4,D2,L1,V0,M1} I { aNormalFormOfIn0( xd, xw, xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xw
% 97.17/97.54 Y := xR
% 97.17/97.54 Z := xd
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149148) {G1,W4,D2,L2,V0,M2} { ! aRewritingSystem0( xR ),
% 97.17/97.54 aElement0( xd ) }.
% 97.17/97.54 parent0[0]: (149147) {G1,W6,D2,L3,V0,M3} { ! aElement0( xw ), !
% 97.17/97.54 aRewritingSystem0( xR ), aElement0( xd ) }.
% 97.17/97.54 parent1[0]: (91) {G0,W2,D2,L1,V0,M1} I { aElement0( xw ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (2108) {G1,W4,D2,L2,V0,M2} R(67,94);r(91) { !
% 97.17/97.54 aRewritingSystem0( xR ), aElement0( xd ) }.
% 97.17/97.54 parent0: (149148) {G1,W4,D2,L2,V0,M2} { ! aRewritingSystem0( xR ),
% 97.17/97.54 aElement0( xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149149) {G1,W8,D2,L3,V0,M3} { ! aElement0( xw ), !
% 97.17/97.54 aRewritingSystem0( xR ), alpha5( xw, xR, xd ) }.
% 97.17/97.54 parent0[2]: (68) {G0,W12,D2,L4,V3,M4} I { ! aElement0( X ), !
% 97.17/97.54 aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y ), alpha5( X, Y, Z )
% 97.17/97.54 }.
% 97.17/97.54 parent1[0]: (94) {G0,W4,D2,L1,V0,M1} I { aNormalFormOfIn0( xd, xw, xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xw
% 97.17/97.54 Y := xR
% 97.17/97.54 Z := xd
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149150) {G1,W6,D2,L2,V0,M2} { ! aRewritingSystem0( xR ),
% 97.17/97.54 alpha5( xw, xR, xd ) }.
% 97.17/97.54 parent0[0]: (149149) {G1,W8,D2,L3,V0,M3} { ! aElement0( xw ), !
% 97.17/97.54 aRewritingSystem0( xR ), alpha5( xw, xR, xd ) }.
% 97.17/97.54 parent1[0]: (91) {G0,W2,D2,L1,V0,M1} I { aElement0( xw ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (2153) {G1,W6,D2,L2,V0,M2} R(68,94);r(91) { !
% 97.17/97.54 aRewritingSystem0( xR ), alpha5( xw, xR, xd ) }.
% 97.17/97.54 parent0: (149150) {G1,W6,D2,L2,V0,M2} { ! aRewritingSystem0( xR ), alpha5
% 97.17/97.54 ( xw, xR, xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149151) {G1,W2,D2,L1,V0,M1} { aElement0( xd ) }.
% 97.17/97.54 parent0[0]: (2108) {G1,W4,D2,L2,V0,M2} R(67,94);r(91) { ! aRewritingSystem0
% 97.17/97.54 ( xR ), aElement0( xd ) }.
% 97.17/97.54 parent1[0]: (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (2273) {G2,W2,D2,L1,V0,M1} S(2108);r(74) { aElement0( xd ) }.
% 97.17/97.54 parent0: (149151) {G1,W2,D2,L1,V0,M1} { aElement0( xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149154) {G1,W21,D3,L6,V2,M6} { ! aElement0( X ), ! aElement0
% 97.17/97.54 ( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, xb ), !
% 97.17/97.54 iLess0( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, xb ) ) }.
% 97.17/97.54 parent0[2]: (82) {G0,W23,D3,L7,V3,M7} I { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X,
% 97.17/97.54 xR, Z ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, Z ) ) }.
% 97.17/97.54 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 Z := xb
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (2465) {G1,W21,D3,L6,V2,M6} R(82,78) { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, xb
% 97.17/97.54 ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, xb ) ) }.
% 97.17/97.54 parent0: (149154) {G1,W21,D3,L6,V2,M6} { ! aElement0( X ), ! aElement0( Y
% 97.17/97.54 ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, xb ), ! iLess0
% 97.17/97.54 ( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, xb ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 4 ==> 4
% 97.17/97.54 5 ==> 5
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149161) {G2,W11,D3,L4,V2,M4} { ! aElement0( xv ), ! aElement0
% 97.17/97.54 ( xv ), ! iLess0( xv, xa ), aElement0( skol11( X, Y ) ) }.
% 97.17/97.54 parent0[2]: (108) {G1,W15,D3,L5,V4,M5} F(80);f { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ),
% 97.17/97.54 aElement0( skol11( Z, T ) ) }.
% 97.17/97.54 parent1[0]: (857) {G3,W4,D2,L1,V0,M1} R(531,88) { sdtmndtasgtdt0( xv, xR,
% 97.17/97.54 xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xv
% 97.17/97.54 Y := xv
% 97.17/97.54 Z := X
% 97.17/97.54 T := Y
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 factor: (149162) {G2,W9,D3,L3,V2,M3} { ! aElement0( xv ), ! iLess0( xv, xa
% 97.17/97.54 ), aElement0( skol11( X, Y ) ) }.
% 97.17/97.54 parent0[0, 1]: (149161) {G2,W11,D3,L4,V2,M4} { ! aElement0( xv ), !
% 97.17/97.54 aElement0( xv ), ! iLess0( xv, xa ), aElement0( skol11( X, Y ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149164) {G1,W7,D3,L2,V2,M2} { ! iLess0( xv, xa ), aElement0(
% 97.17/97.54 skol11( X, Y ) ) }.
% 97.17/97.54 parent0[0]: (149162) {G2,W9,D3,L3,V2,M3} { ! aElement0( xv ), ! iLess0( xv
% 97.17/97.54 , xa ), aElement0( skol11( X, Y ) ) }.
% 97.17/97.54 parent1[0]: (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (2812) {G4,W7,D3,L2,V2,M2} R(108,857);f;r(88) { ! iLess0( xv,
% 97.17/97.54 xa ), aElement0( skol11( X, Y ) ) }.
% 97.17/97.54 parent0: (149164) {G1,W7,D3,L2,V2,M2} { ! iLess0( xv, xa ), aElement0(
% 97.17/97.54 skol11( X, Y ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149165) {G2,W13,D3,L4,V1,M4} { ! aElement0( xb ), ! aElement0
% 97.17/97.54 ( xb ), ! iLess0( xb, xa ), sdtmndtasgtdt0( xb, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent0[2]: (111) {G1,W17,D3,L5,V3,M5} F(81);f { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! iLess0( X, xa ),
% 97.17/97.54 sdtmndtasgtdt0( Y, xR, skol11( Z, Y ) ) }.
% 97.17/97.54 parent1[0]: (853) {G3,W4,D2,L1,V0,M1} R(531,78) { sdtmndtasgtdt0( xb, xR,
% 97.17/97.54 xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xb
% 97.17/97.54 Y := xb
% 97.17/97.54 Z := X
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 factor: (149166) {G2,W11,D3,L3,V1,M3} { ! aElement0( xb ), ! iLess0( xb,
% 97.17/97.54 xa ), sdtmndtasgtdt0( xb, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent0[0, 1]: (149165) {G2,W13,D3,L4,V1,M4} { ! aElement0( xb ), !
% 97.17/97.54 aElement0( xb ), ! iLess0( xb, xa ), sdtmndtasgtdt0( xb, xR, skol11( X,
% 97.17/97.54 xb ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149168) {G1,W9,D3,L2,V1,M2} { ! iLess0( xb, xa ),
% 97.17/97.54 sdtmndtasgtdt0( xb, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent0[0]: (149166) {G2,W11,D3,L3,V1,M3} { ! aElement0( xb ), ! iLess0(
% 97.17/97.54 xb, xa ), sdtmndtasgtdt0( xb, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { aElement0( xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (2842) {G4,W9,D3,L2,V1,M2} R(111,853);f;r(78) { ! iLess0( xb,
% 97.17/97.54 xa ), sdtmndtasgtdt0( xb, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent0: (149168) {G1,W9,D3,L2,V1,M2} { ! iLess0( xb, xa ), sdtmndtasgtdt0
% 97.17/97.54 ( xb, xR, skol11( X, xb ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149169) {G1,W4,D2,L1,V0,M1} { alpha5( xw, xR, xd ) }.
% 97.17/97.54 parent0[0]: (2153) {G1,W6,D2,L2,V0,M2} R(68,94);r(91) { ! aRewritingSystem0
% 97.17/97.54 ( xR ), alpha5( xw, xR, xd ) }.
% 97.17/97.54 parent1[0]: (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (4306) {G2,W4,D2,L1,V0,M1} S(2153);r(74) { alpha5( xw, xR, xd
% 97.17/97.54 ) }.
% 97.17/97.54 parent0: (149169) {G1,W4,D2,L1,V0,M1} { alpha5( xw, xR, xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149170) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xw, xR, xd )
% 97.17/97.54 }.
% 97.17/97.54 parent0[0]: (70) {G0,W8,D2,L2,V3,M2} I { ! alpha5( X, Y, Z ),
% 97.17/97.54 sdtmndtasgtdt0( X, Y, Z ) }.
% 97.17/97.54 parent1[0]: (4306) {G2,W4,D2,L1,V0,M1} S(2153);r(74) { alpha5( xw, xR, xd )
% 97.17/97.54 }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xw
% 97.17/97.54 Y := xR
% 97.17/97.54 Z := xd
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (4308) {G3,W4,D2,L1,V0,M1} R(4306,70) { sdtmndtasgtdt0( xw, xR
% 97.17/97.54 , xd ) }.
% 97.17/97.54 parent0: (149170) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xw, xR, xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149171) {G1,W8,D2,L3,V0,M3} { ! aElement0( xa ), ! aElement0
% 97.17/97.54 ( xu ), sdtmndtplgtdt0( xa, xR, xu ) }.
% 97.17/97.54 parent0[2]: (140) {G1,W12,D2,L4,V2,M4} R(3,74) { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! aReductOfIn0( Y, X, xR ), sdtmndtplgtdt0( X, xR, Y )
% 97.17/97.54 }.
% 97.17/97.54 parent1[0]: (86) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xu, xa, xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xa
% 97.17/97.54 Y := xu
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149172) {G1,W6,D2,L2,V0,M2} { ! aElement0( xu ),
% 97.17/97.54 sdtmndtplgtdt0( xa, xR, xu ) }.
% 97.17/97.54 parent0[0]: (149171) {G1,W8,D2,L3,V0,M3} { ! aElement0( xa ), ! aElement0
% 97.17/97.54 ( xu ), sdtmndtplgtdt0( xa, xR, xu ) }.
% 97.17/97.54 parent1[0]: (77) {G0,W2,D2,L1,V0,M1} I { aElement0( xa ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (4355) {G2,W6,D2,L2,V0,M2} R(140,86);r(77) { ! aElement0( xu )
% 97.17/97.54 , sdtmndtplgtdt0( xa, xR, xu ) }.
% 97.17/97.54 parent0: (149172) {G1,W6,D2,L2,V0,M2} { ! aElement0( xu ), sdtmndtplgtdt0
% 97.17/97.54 ( xa, xR, xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149173) {G1,W8,D2,L3,V0,M3} { ! aElement0( xa ), ! aElement0
% 97.17/97.54 ( xv ), sdtmndtplgtdt0( xa, xR, xv ) }.
% 97.17/97.54 parent0[2]: (140) {G1,W12,D2,L4,V2,M4} R(3,74) { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! aReductOfIn0( Y, X, xR ), sdtmndtplgtdt0( X, xR, Y )
% 97.17/97.54 }.
% 97.17/97.54 parent1[0]: (89) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xv, xa, xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xa
% 97.17/97.54 Y := xv
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149174) {G1,W6,D2,L2,V0,M2} { ! aElement0( xv ),
% 97.17/97.54 sdtmndtplgtdt0( xa, xR, xv ) }.
% 97.17/97.54 parent0[0]: (149173) {G1,W8,D2,L3,V0,M3} { ! aElement0( xa ), ! aElement0
% 97.17/97.54 ( xv ), sdtmndtplgtdt0( xa, xR, xv ) }.
% 97.17/97.54 parent1[0]: (77) {G0,W2,D2,L1,V0,M1} I { aElement0( xa ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (4356) {G2,W6,D2,L2,V0,M2} R(140,89);r(77) { ! aElement0( xv )
% 97.17/97.54 , sdtmndtplgtdt0( xa, xR, xv ) }.
% 97.17/97.54 parent0: (149174) {G1,W6,D2,L2,V0,M2} { ! aElement0( xv ), sdtmndtplgtdt0
% 97.17/97.54 ( xa, xR, xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149175) {G1,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xu )
% 97.17/97.54 }.
% 97.17/97.54 parent0[0]: (4355) {G2,W6,D2,L2,V0,M2} R(140,86);r(77) { ! aElement0( xu )
% 97.17/97.54 , sdtmndtplgtdt0( xa, xR, xu ) }.
% 97.17/97.54 parent1[0]: (85) {G0,W2,D2,L1,V0,M1} I { aElement0( xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (4474) {G3,W4,D2,L1,V0,M1} S(4355);r(85) { sdtmndtplgtdt0( xa
% 97.17/97.54 , xR, xu ) }.
% 97.17/97.54 parent0: (149175) {G1,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149176) {G1,W7,D2,L2,V0,M2} { ! alpha11( xR, xa, xu ), iLess0
% 97.17/97.54 ( xu, xa ) }.
% 97.17/97.54 parent0[1]: (61) {G0,W11,D2,L3,V3,M3} I { ! alpha11( X, Y, Z ), !
% 97.17/97.54 sdtmndtplgtdt0( Y, X, Z ), iLess0( Z, Y ) }.
% 97.17/97.54 parent1[0]: (4474) {G3,W4,D2,L1,V0,M1} S(4355);r(85) { sdtmndtplgtdt0( xa,
% 97.17/97.54 xR, xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xR
% 97.17/97.54 Y := xa
% 97.17/97.54 Z := xu
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149177) {G2,W3,D2,L1,V0,M1} { iLess0( xu, xa ) }.
% 97.17/97.54 parent0[0]: (149176) {G1,W7,D2,L2,V0,M2} { ! alpha11( xR, xa, xu ), iLess0
% 97.17/97.54 ( xu, xa ) }.
% 97.17/97.54 parent1[0]: (1955) {G3,W4,D2,L1,V0,M1} R(1804,298) { alpha11( xR, xa, xu )
% 97.17/97.54 }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (4477) {G4,W3,D2,L1,V0,M1} R(4474,61);r(1955) { iLess0( xu, xa
% 97.17/97.54 ) }.
% 97.17/97.54 parent0: (149177) {G2,W3,D2,L1,V0,M1} { iLess0( xu, xa ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149178) {G1,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xv )
% 97.17/97.54 }.
% 97.17/97.54 parent0[0]: (4356) {G2,W6,D2,L2,V0,M2} R(140,89);r(77) { ! aElement0( xv )
% 97.17/97.54 , sdtmndtplgtdt0( xa, xR, xv ) }.
% 97.17/97.54 parent1[0]: (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (4489) {G3,W4,D2,L1,V0,M1} S(4356);r(88) { sdtmndtplgtdt0( xa
% 97.17/97.54 , xR, xv ) }.
% 97.17/97.54 parent0: (149178) {G1,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149179) {G1,W7,D2,L2,V0,M2} { ! alpha11( xR, xa, xv ), iLess0
% 97.17/97.54 ( xv, xa ) }.
% 97.17/97.54 parent0[1]: (61) {G0,W11,D2,L3,V3,M3} I { ! alpha11( X, Y, Z ), !
% 97.17/97.54 sdtmndtplgtdt0( Y, X, Z ), iLess0( Z, Y ) }.
% 97.17/97.54 parent1[0]: (4489) {G3,W4,D2,L1,V0,M1} S(4356);r(88) { sdtmndtplgtdt0( xa,
% 97.17/97.54 xR, xv ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xR
% 97.17/97.54 Y := xa
% 97.17/97.54 Z := xv
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149180) {G2,W3,D2,L1,V0,M1} { iLess0( xv, xa ) }.
% 97.17/97.54 parent0[0]: (149179) {G1,W7,D2,L2,V0,M2} { ! alpha11( xR, xa, xv ), iLess0
% 97.17/97.54 ( xv, xa ) }.
% 97.17/97.54 parent1[0]: (1954) {G3,W4,D2,L1,V0,M1} R(1804,299) { alpha11( xR, xa, xv )
% 97.17/97.54 }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (4492) {G4,W3,D2,L1,V0,M1} R(4489,61);r(1954) { iLess0( xv, xa
% 97.17/97.54 ) }.
% 97.17/97.54 parent0: (149180) {G2,W3,D2,L1,V0,M1} { iLess0( xv, xa ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149181) {G5,W4,D3,L1,V2,M1} { aElement0( skol11( X, Y ) ) }.
% 97.17/97.54 parent0[0]: (2812) {G4,W7,D3,L2,V2,M2} R(108,857);f;r(88) { ! iLess0( xv,
% 97.17/97.54 xa ), aElement0( skol11( X, Y ) ) }.
% 97.17/97.54 parent1[0]: (4492) {G4,W3,D2,L1,V0,M1} R(4489,61);r(1954) { iLess0( xv, xa
% 97.17/97.54 ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (9960) {G5,W4,D3,L1,V2,M1} S(2812);r(4492) { aElement0( skol11
% 97.17/97.54 ( X, Y ) ) }.
% 97.17/97.54 parent0: (149181) {G5,W4,D3,L1,V2,M1} { aElement0( skol11( X, Y ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 Y := Y
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149182) {G5,W6,D3,L1,V1,M1} { sdtmndtasgtdt0( xb, xR, skol11
% 97.17/97.54 ( X, xb ) ) }.
% 97.17/97.54 parent0[0]: (2842) {G4,W9,D3,L2,V1,M2} R(111,853);f;r(78) { ! iLess0( xb,
% 97.17/97.54 xa ), sdtmndtasgtdt0( xb, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent1[0]: (2021) {G4,W3,D2,L1,V0,M1} R(61,83);r(1957) { iLess0( xb, xa )
% 97.17/97.54 }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (21312) {G5,W6,D3,L1,V1,M1} S(2842);r(2021) { sdtmndtasgtdt0(
% 97.17/97.54 xb, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent0: (149182) {G5,W6,D3,L1,V1,M1} { sdtmndtasgtdt0( xb, xR, skol11( X
% 97.17/97.54 , xb ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149183) {G2,W14,D2,L5,V0,M5} { ! aRewritingSystem0( xR ), !
% 97.17/97.54 aElement0( xw ), ! aElement0( xd ), ! sdtmndtasgtdt0( xu, xR, xw ),
% 97.17/97.54 sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 parent0[4]: (638) {G1,W18,D2,L6,V3,M6} R(15,85) { ! aRewritingSystem0( X )
% 97.17/97.54 , ! aElement0( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( xu, X, Y ), !
% 97.17/97.54 sdtmndtasgtdt0( Y, X, Z ), sdtmndtasgtdt0( xu, X, Z ) }.
% 97.17/97.54 parent1[0]: (4308) {G3,W4,D2,L1,V0,M1} R(4306,70) { sdtmndtasgtdt0( xw, xR
% 97.17/97.54 , xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xR
% 97.17/97.54 Y := xw
% 97.17/97.54 Z := xd
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149184) {G1,W12,D2,L4,V0,M4} { ! aElement0( xw ), ! aElement0
% 97.17/97.54 ( xd ), ! sdtmndtasgtdt0( xu, xR, xw ), sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 parent0[0]: (149183) {G2,W14,D2,L5,V0,M5} { ! aRewritingSystem0( xR ), !
% 97.17/97.54 aElement0( xw ), ! aElement0( xd ), ! sdtmndtasgtdt0( xu, xR, xw ),
% 97.17/97.54 sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 parent1[0]: (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (21784) {G4,W12,D2,L4,V0,M4} R(638,4308);r(74) { ! aElement0(
% 97.17/97.54 xw ), ! aElement0( xd ), ! sdtmndtasgtdt0( xu, xR, xw ), sdtmndtasgtdt0(
% 97.17/97.54 xu, xR, xd ) }.
% 97.17/97.54 parent0: (149184) {G1,W12,D2,L4,V0,M4} { ! aElement0( xw ), ! aElement0(
% 97.17/97.54 xd ), ! sdtmndtasgtdt0( xu, xR, xw ), sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149185) {G1,W10,D3,L2,V1,M2} { ! aElement0( skol11( X, xb ) )
% 97.17/97.54 , ! sdtmndtasgtdt0( xd, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent0[1]: (95) {G0,W10,D2,L3,V1,M3} I { ! aElement0( X ), !
% 97.17/97.54 sdtmndtasgtdt0( xb, xR, X ), ! sdtmndtasgtdt0( xd, xR, X ) }.
% 97.17/97.54 parent1[0]: (21312) {G5,W6,D3,L1,V1,M1} S(2842);r(2021) { sdtmndtasgtdt0(
% 97.17/97.54 xb, xR, skol11( X, xb ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := skol11( X, xb )
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149186) {G2,W6,D3,L1,V1,M1} { ! sdtmndtasgtdt0( xd, xR,
% 97.17/97.54 skol11( X, xb ) ) }.
% 97.17/97.54 parent0[0]: (149185) {G1,W10,D3,L2,V1,M2} { ! aElement0( skol11( X, xb ) )
% 97.17/97.54 , ! sdtmndtasgtdt0( xd, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent1[0]: (9960) {G5,W4,D3,L1,V2,M1} S(2812);r(4492) { aElement0( skol11
% 97.17/97.54 ( X, Y ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 X := X
% 97.17/97.54 Y := xb
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (23029) {G6,W6,D3,L1,V1,M1} R(21312,95);r(9960) { !
% 97.17/97.54 sdtmndtasgtdt0( xd, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent0: (149186) {G2,W6,D3,L1,V1,M1} { ! sdtmndtasgtdt0( xd, xR, skol11(
% 97.17/97.54 X, xb ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := X
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149187) {G1,W10,D2,L3,V0,M3} { ! aElement0( xd ), !
% 97.17/97.54 sdtmndtasgtdt0( xu, xR, xw ), sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 parent0[0]: (21784) {G4,W12,D2,L4,V0,M4} R(638,4308);r(74) { ! aElement0(
% 97.17/97.54 xw ), ! aElement0( xd ), ! sdtmndtasgtdt0( xu, xR, xw ), sdtmndtasgtdt0(
% 97.17/97.54 xu, xR, xd ) }.
% 97.17/97.54 parent1[0]: (91) {G0,W2,D2,L1,V0,M1} I { aElement0( xw ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149188) {G2,W8,D2,L2,V0,M2} { ! sdtmndtasgtdt0( xu, xR, xw )
% 97.17/97.54 , sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 parent0[0]: (149187) {G1,W10,D2,L3,V0,M3} { ! aElement0( xd ), !
% 97.17/97.54 sdtmndtasgtdt0( xu, xR, xw ), sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 parent1[0]: (2273) {G2,W2,D2,L1,V0,M1} S(2108);r(74) { aElement0( xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149189) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, xd )
% 97.17/97.54 }.
% 97.17/97.54 parent0[0]: (149188) {G2,W8,D2,L2,V0,M2} { ! sdtmndtasgtdt0( xu, xR, xw )
% 97.17/97.54 , sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 parent1[0]: (92) {G0,W4,D2,L1,V0,M1} I { sdtmndtasgtdt0( xu, xR, xw ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (43720) {G5,W4,D2,L1,V0,M1} S(21784);r(91);r(2273);r(92) {
% 97.17/97.54 sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 parent0: (149189) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149190) {G2,W17,D3,L5,V0,M5} { ! aElement0( xu ), ! aElement0
% 97.17/97.54 ( xd ), ! sdtmndtasgtdt0( xu, xR, xb ), ! iLess0( xu, xa ),
% 97.17/97.54 sdtmndtasgtdt0( xd, xR, skol11( xd, xb ) ) }.
% 97.17/97.54 parent0[2]: (2465) {G1,W21,D3,L6,V2,M6} R(82,78) { ! aElement0( X ), !
% 97.17/97.54 aElement0( Y ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, xb
% 97.17/97.54 ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, xb ) ) }.
% 97.17/97.54 parent1[0]: (43720) {G5,W4,D2,L1,V0,M1} S(21784);r(91);r(2273);r(92) {
% 97.17/97.54 sdtmndtasgtdt0( xu, xR, xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xu
% 97.17/97.54 Y := xd
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149191) {G1,W15,D3,L4,V0,M4} { ! aElement0( xd ), !
% 97.17/97.54 sdtmndtasgtdt0( xu, xR, xb ), ! iLess0( xu, xa ), sdtmndtasgtdt0( xd, xR
% 97.17/97.54 , skol11( xd, xb ) ) }.
% 97.17/97.54 parent0[0]: (149190) {G2,W17,D3,L5,V0,M5} { ! aElement0( xu ), ! aElement0
% 97.17/97.54 ( xd ), ! sdtmndtasgtdt0( xu, xR, xb ), ! iLess0( xu, xa ),
% 97.17/97.54 sdtmndtasgtdt0( xd, xR, skol11( xd, xb ) ) }.
% 97.17/97.54 parent1[0]: (85) {G0,W2,D2,L1,V0,M1} I { aElement0( xu ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (147823) {G6,W15,D3,L4,V0,M4} R(2465,43720);r(85) { !
% 97.17/97.54 aElement0( xd ), ! sdtmndtasgtdt0( xu, xR, xb ), ! iLess0( xu, xa ),
% 97.17/97.54 sdtmndtasgtdt0( xd, xR, skol11( xd, xb ) ) }.
% 97.17/97.54 parent0: (149191) {G1,W15,D3,L4,V0,M4} { ! aElement0( xd ), !
% 97.17/97.54 sdtmndtasgtdt0( xu, xR, xb ), ! iLess0( xu, xa ), sdtmndtasgtdt0( xd, xR
% 97.17/97.54 , skol11( xd, xb ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 0 ==> 0
% 97.17/97.54 1 ==> 1
% 97.17/97.54 2 ==> 2
% 97.17/97.54 3 ==> 3
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149192) {G3,W13,D3,L3,V0,M3} { ! sdtmndtasgtdt0( xu, xR, xb )
% 97.17/97.54 , ! iLess0( xu, xa ), sdtmndtasgtdt0( xd, xR, skol11( xd, xb ) ) }.
% 97.17/97.54 parent0[0]: (147823) {G6,W15,D3,L4,V0,M4} R(2465,43720);r(85) { ! aElement0
% 97.17/97.54 ( xd ), ! sdtmndtasgtdt0( xu, xR, xb ), ! iLess0( xu, xa ),
% 97.17/97.54 sdtmndtasgtdt0( xd, xR, skol11( xd, xb ) ) }.
% 97.17/97.54 parent1[0]: (2273) {G2,W2,D2,L1,V0,M1} S(2108);r(74) { aElement0( xd ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149193) {G1,W9,D3,L2,V0,M2} { ! iLess0( xu, xa ),
% 97.17/97.54 sdtmndtasgtdt0( xd, xR, skol11( xd, xb ) ) }.
% 97.17/97.54 parent0[0]: (149192) {G3,W13,D3,L3,V0,M3} { ! sdtmndtasgtdt0( xu, xR, xb )
% 97.17/97.54 , ! iLess0( xu, xa ), sdtmndtasgtdt0( xd, xR, skol11( xd, xb ) ) }.
% 97.17/97.54 parent1[0]: (87) {G0,W4,D2,L1,V0,M1} I { sdtmndtasgtdt0( xu, xR, xb ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149194) {G2,W6,D3,L1,V0,M1} { sdtmndtasgtdt0( xd, xR, skol11
% 97.17/97.54 ( xd, xb ) ) }.
% 97.17/97.54 parent0[0]: (149193) {G1,W9,D3,L2,V0,M2} { ! iLess0( xu, xa ),
% 97.17/97.54 sdtmndtasgtdt0( xd, xR, skol11( xd, xb ) ) }.
% 97.17/97.54 parent1[0]: (4477) {G4,W3,D2,L1,V0,M1} R(4474,61);r(1955) { iLess0( xu, xa
% 97.17/97.54 ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 resolution: (149195) {G3,W0,D0,L0,V0,M0} { }.
% 97.17/97.54 parent0[0]: (23029) {G6,W6,D3,L1,V1,M1} R(21312,95);r(9960) { !
% 97.17/97.54 sdtmndtasgtdt0( xd, xR, skol11( X, xb ) ) }.
% 97.17/97.54 parent1[0]: (149194) {G2,W6,D3,L1,V0,M1} { sdtmndtasgtdt0( xd, xR, skol11
% 97.17/97.54 ( xd, xb ) ) }.
% 97.17/97.54 substitution0:
% 97.17/97.54 X := xd
% 97.17/97.54 end
% 97.17/97.54 substitution1:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 subsumption: (148150) {G7,W0,D0,L0,V0,M0} S(147823);r(2273);r(87);r(4477);r
% 97.17/97.54 (23029) { }.
% 97.17/97.54 parent0: (149195) {G3,W0,D0,L0,V0,M0} { }.
% 97.17/97.54 substitution0:
% 97.17/97.54 end
% 97.17/97.54 permutation0:
% 97.17/97.54 end
% 97.17/97.54
% 97.17/97.54 Proof check complete!
% 97.17/97.54
% 97.17/97.54 Memory use:
% 97.17/97.54
% 97.17/97.55 space for terms: 2099686
% 97.17/97.55 space for clauses: 5839365
% 97.17/97.55
% 97.17/97.55
% 97.17/97.55 clauses generated: 2434683
% 97.17/97.55 clauses kept: 148151
% 97.17/97.55 clauses selected: 8562
% 97.17/97.55 clauses deleted: 33260
% 97.17/97.55 clauses inuse deleted: 535
% 97.17/97.55
% 97.17/97.55 subsentry: 4090057
% 97.17/97.55 literals s-matched: 2751419
% 97.17/97.55 literals matched: 1933776
% 97.17/97.55 full subsumption: 170252
% 97.17/97.55
% 97.17/97.55 checksum: 819910164
% 97.17/97.55
% 97.17/97.55
% 97.17/97.55 Bliksem ended
%------------------------------------------------------------------------------