%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : COM017+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n008.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:08 EDT 2022
% Result : Theorem 14.51s 14.86s
% Output : Refutation 14.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : COM017+1 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.13 % Command : bliksem %s
% 0.14/0.34 % Computer : n008.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % DateTime : Thu Jun 16 18:12:37 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.74/1.08 *** allocated 10000 integers for termspace/termends
% 0.74/1.08 *** allocated 10000 integers for clauses
% 0.74/1.08 *** allocated 10000 integers for justifications
% 0.74/1.08 Bliksem 1.12
% 0.74/1.08
% 0.74/1.08
% 0.74/1.08 Automatic Strategy Selection
% 0.74/1.08
% 0.74/1.08
% 0.74/1.08 Clauses:
% 0.74/1.08
% 0.74/1.08 { && }.
% 0.74/1.08 { && }.
% 0.74/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ),
% 0.74/1.08 aElement0( Z ) }.
% 0.74/1.08 { && }.
% 0.74/1.08 { && }.
% 0.74/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.74/1.08 sdtmndtplgtdt0( X, Y, Z ), aReductOfIn0( Z, X, Y ), alpha1( X, Y, Z ) }.
% 0.74/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.74/1.08 aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z ) }.
% 0.74/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha1( X
% 0.74/1.08 , Y, Z ), sdtmndtplgtdt0( X, Y, Z ) }.
% 0.74/1.08 { ! alpha1( X, Y, Z ), aElement0( skol1( T, U, W ) ) }.
% 0.74/1.08 { ! alpha1( X, Y, Z ), alpha6( X, Y, Z, skol1( X, Y, Z ) ) }.
% 0.74/1.08 { ! aElement0( T ), ! alpha6( X, Y, Z, T ), alpha1( X, Y, Z ) }.
% 0.74/1.08 { ! alpha6( X, Y, Z, T ), aReductOfIn0( T, X, Y ) }.
% 0.74/1.08 { ! alpha6( X, Y, Z, T ), sdtmndtplgtdt0( T, Y, Z ) }.
% 0.74/1.08 { ! aReductOfIn0( T, X, Y ), ! sdtmndtplgtdt0( T, Y, Z ), alpha6( X, Y, Z,
% 0.74/1.08 T ) }.
% 0.74/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0
% 0.74/1.08 ( T ), ! sdtmndtplgtdt0( X, Y, Z ), ! sdtmndtplgtdt0( Z, Y, T ),
% 0.74/1.08 sdtmndtplgtdt0( X, Y, T ) }.
% 0.74/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.74/1.08 sdtmndtasgtdt0( X, Y, Z ), X = Z, sdtmndtplgtdt0( X, Y, Z ) }.
% 0.74/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z,
% 0.74/1.08 sdtmndtasgtdt0( X, Y, Z ) }.
% 0.74/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.74/1.08 sdtmndtplgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z ) }.
% 0.74/1.08 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0
% 0.74/1.08 ( T ), ! sdtmndtasgtdt0( X, Y, Z ), ! sdtmndtasgtdt0( Z, Y, T ),
% 0.74/1.08 sdtmndtasgtdt0( X, Y, T ) }.
% 0.74/1.08 { ! aRewritingSystem0( X ), ! isConfluent0( X ), ! alpha2( X, Y, Z ),
% 0.74/1.08 alpha7( X, Y, Z ) }.
% 0.74/1.08 { ! aRewritingSystem0( X ), alpha2( X, skol2( X ), skol12( X ) ),
% 0.74/1.08 isConfluent0( X ) }.
% 0.74/1.08 { ! aRewritingSystem0( X ), ! alpha7( X, skol2( X ), skol12( X ) ),
% 0.74/1.08 isConfluent0( X ) }.
% 0.74/1.08 { ! alpha7( X, Y, Z ), aElement0( skol3( T, U, W ) ) }.
% 0.74/1.08 { ! alpha7( X, Y, Z ), alpha12( X, Y, Z, skol3( X, Y, Z ) ) }.
% 0.74/1.08 { ! aElement0( T ), ! alpha12( X, Y, Z, T ), alpha7( X, Y, Z ) }.
% 0.74/1.08 { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Y, X, T ) }.
% 0.74/1.08 { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Z, X, T ) }.
% 0.74/1.08 { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0( Z, X, T ), alpha12( X, Y,
% 0.74/1.08 Z, T ) }.
% 0.74/1.08 { ! alpha2( X, Y, Z ), aElement0( skol4( T, U, W ) ) }.
% 0.74/1.08 { ! alpha2( X, Y, Z ), alpha8( X, Y, Z, skol4( X, Y, Z ) ) }.
% 0.74/1.08 { ! aElement0( T ), ! alpha8( X, Y, Z, T ), alpha2( X, Y, Z ) }.
% 0.74/1.08 { ! alpha8( X, Y, Z, T ), aElement0( Y ) }.
% 0.74/1.08 { ! alpha8( X, Y, Z, T ), alpha13( X, Y, Z, T ) }.
% 0.74/1.08 { ! aElement0( Y ), ! alpha13( X, Y, Z, T ), alpha8( X, Y, Z, T ) }.
% 0.74/1.08 { ! alpha13( X, Y, Z, T ), aElement0( Z ) }.
% 0.74/1.08 { ! alpha13( X, Y, Z, T ), alpha16( X, Y, Z, T ) }.
% 0.74/1.08 { ! aElement0( Z ), ! alpha16( X, Y, Z, T ), alpha13( X, Y, Z, T ) }.
% 0.74/1.08 { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T, X, Y ) }.
% 0.74/1.08 { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T, X, Z ) }.
% 0.74/1.08 { ! sdtmndtasgtdt0( T, X, Y ), ! sdtmndtasgtdt0( T, X, Z ), alpha16( X, Y,
% 0.74/1.08 Z, T ) }.
% 0.74/1.08 { ! aRewritingSystem0( X ), ! isLocallyConfluent0( X ), ! alpha3( X, Y, Z )
% 0.74/1.08 , alpha9( X, Y, Z ) }.
% 0.74/1.08 { ! aRewritingSystem0( X ), alpha3( X, skol5( X ), skol13( X ) ),
% 0.74/1.08 isLocallyConfluent0( X ) }.
% 0.74/1.08 { ! aRewritingSystem0( X ), ! alpha9( X, skol5( X ), skol13( X ) ),
% 0.74/1.08 isLocallyConfluent0( X ) }.
% 0.74/1.08 { ! alpha9( X, Y, Z ), aElement0( skol6( T, U, W ) ) }.
% 0.74/1.08 { ! alpha9( X, Y, Z ), alpha14( X, Y, Z, skol6( X, Y, Z ) ) }.
% 0.74/1.08 { ! aElement0( T ), ! alpha14( X, Y, Z, T ), alpha9( X, Y, Z ) }.
% 0.74/1.08 { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Y, X, T ) }.
% 0.74/1.08 { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Z, X, T ) }.
% 0.74/1.08 { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0( Z, X, T ), alpha14( X, Y,
% 0.74/1.08 Z, T ) }.
% 0.74/1.08 { ! alpha3( X, Y, Z ), aElement0( skol7( T, U, W ) ) }.
% 0.74/1.08 { ! alpha3( X, Y, Z ), alpha10( X, Y, Z, skol7( X, Y, Z ) ) }.
% 0.74/1.08 { ! aElement0( T ), ! alpha10( X, Y, Z, T ), alpha3( X, Y, Z ) }.
% 0.74/1.08 { ! alpha10( X, Y, Z, T ), aElement0( Y ) }.
% 0.74/1.08 { ! alpha10( X, Y, Z, T ), alpha15( X, Y, Z, T ) }.
% 2.29/2.70 { ! aElement0( Y ), ! alpha15( X, Y, Z, T ), alpha10( X, Y, Z, T ) }.
% 2.29/2.70 { ! alpha15( X, Y, Z, T ), aElement0( Z ) }.
% 2.29/2.70 { ! alpha15( X, Y, Z, T ), alpha17( X, Y, Z, T ) }.
% 2.29/2.70 { ! aElement0( Z ), ! alpha17( X, Y, Z, T ), alpha15( X, Y, Z, T ) }.
% 2.29/2.70 { ! alpha17( X, Y, Z, T ), aReductOfIn0( Y, T, X ) }.
% 2.29/2.70 { ! alpha17( X, Y, Z, T ), aReductOfIn0( Z, T, X ) }.
% 2.29/2.70 { ! aReductOfIn0( Y, T, X ), ! aReductOfIn0( Z, T, X ), alpha17( X, Y, Z, T
% 2.29/2.70 ) }.
% 2.29/2.70 { ! aRewritingSystem0( X ), ! isTerminating0( X ), ! alpha4( Y, Z ),
% 2.29/2.70 alpha11( X, Y, Z ) }.
% 2.29/2.70 { ! aRewritingSystem0( X ), alpha4( skol8( X ), skol14( X ) ),
% 2.29/2.70 isTerminating0( X ) }.
% 2.29/2.70 { ! aRewritingSystem0( X ), ! alpha11( X, skol8( X ), skol14( X ) ),
% 2.29/2.70 isTerminating0( X ) }.
% 2.29/2.70 { ! alpha11( X, Y, Z ), ! sdtmndtplgtdt0( Y, X, Z ), iLess0( Z, Y ) }.
% 2.29/2.70 { sdtmndtplgtdt0( Y, X, Z ), alpha11( X, Y, Z ) }.
% 2.29/2.70 { ! iLess0( Z, Y ), alpha11( X, Y, Z ) }.
% 2.29/2.70 { ! alpha4( X, Y ), aElement0( X ) }.
% 2.29/2.70 { ! alpha4( X, Y ), aElement0( Y ) }.
% 2.29/2.70 { ! aElement0( X ), ! aElement0( Y ), alpha4( X, Y ) }.
% 2.29/2.70 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y )
% 2.29/2.70 , aElement0( Z ) }.
% 2.29/2.70 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y )
% 2.29/2.70 , alpha5( X, Y, Z ) }.
% 2.29/2.70 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha5( X
% 2.29/2.70 , Y, Z ), aNormalFormOfIn0( Z, X, Y ) }.
% 2.29/2.70 { ! alpha5( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z ) }.
% 2.29/2.70 { ! alpha5( X, Y, Z ), ! aReductOfIn0( T, Z, Y ) }.
% 2.29/2.70 { ! sdtmndtasgtdt0( X, Y, Z ), aReductOfIn0( skol9( Y, Z ), Z, Y ), alpha5
% 2.29/2.70 ( X, Y, Z ) }.
% 2.29/2.70 { ! aRewritingSystem0( X ), ! isTerminating0( X ), ! aElement0( Y ),
% 2.29/2.70 aNormalFormOfIn0( skol10( X, Y ), Y, X ) }.
% 2.29/2.70 { aRewritingSystem0( xR ) }.
% 2.29/2.70 { isLocallyConfluent0( xR ) }.
% 2.29/2.70 { isTerminating0( xR ) }.
% 2.29/2.70 { aElement0( xa ) }.
% 2.29/2.70 { aElement0( xb ) }.
% 2.29/2.70 { aElement0( xc ) }.
% 2.29/2.70 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( X
% 2.29/2.70 , xR, Y ), ! sdtmndtasgtdt0( X, xR, Z ), ! iLess0( X, xa ), aElement0(
% 2.29/2.70 skol11( T, U ) ) }.
% 2.29/2.70 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( X
% 2.29/2.70 , xR, Y ), ! sdtmndtasgtdt0( X, xR, Z ), ! iLess0( X, xa ),
% 2.29/2.70 sdtmndtasgtdt0( Z, xR, skol11( T, Z ) ) }.
% 2.29/2.70 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), ! sdtmndtasgtdt0( X
% 2.29/2.70 , xR, Y ), ! sdtmndtasgtdt0( X, xR, Z ), ! iLess0( X, xa ),
% 2.29/2.70 sdtmndtasgtdt0( Y, xR, skol11( Y, Z ) ) }.
% 2.29/2.70 { sdtmndtplgtdt0( xa, xR, xb ) }.
% 2.29/2.70 { sdtmndtplgtdt0( xa, xR, xc ) }.
% 2.29/2.70 { aElement0( xu ) }.
% 2.29/2.70 { aReductOfIn0( xu, xa, xR ) }.
% 2.29/2.70 { sdtmndtasgtdt0( xu, xR, xb ) }.
% 2.29/2.70 { aElement0( xv ) }.
% 2.29/2.70 { aReductOfIn0( xv, xa, xR ) }.
% 2.29/2.70 { sdtmndtasgtdt0( xv, xR, xc ) }.
% 2.29/2.70 { ! aElement0( X ), ! sdtmndtasgtdt0( xu, xR, X ), ! sdtmndtasgtdt0( xv, xR
% 2.29/2.70 , X ) }.
% 2.29/2.70
% 2.29/2.70 percentage equality = 0.007843, percentage horn = 0.923913
% 2.29/2.70 This is a problem with some equality
% 2.29/2.70
% 2.29/2.70
% 2.29/2.70
% 2.29/2.70 Options Used:
% 2.29/2.70
% 2.29/2.70 useres = 1
% 2.29/2.70 useparamod = 1
% 2.29/2.70 useeqrefl = 1
% 2.29/2.70 useeqfact = 1
% 2.29/2.70 usefactor = 1
% 2.29/2.70 usesimpsplitting = 0
% 2.29/2.70 usesimpdemod = 5
% 2.29/2.70 usesimpres = 3
% 2.29/2.70
% 2.29/2.70 resimpinuse = 1000
% 2.29/2.70 resimpclauses = 20000
% 2.29/2.70 substype = eqrewr
% 2.29/2.70 backwardsubs = 1
% 2.29/2.70 selectoldest = 5
% 2.29/2.70
% 2.29/2.70 litorderings [0] = split
% 2.29/2.70 litorderings [1] = extend the termordering, first sorting on arguments
% 2.29/2.70
% 2.29/2.70 termordering = kbo
% 2.29/2.70
% 2.29/2.70 litapriori = 0
% 2.29/2.70 termapriori = 1
% 2.29/2.70 litaposteriori = 0
% 2.29/2.70 termaposteriori = 0
% 2.29/2.70 demodaposteriori = 0
% 2.29/2.70 ordereqreflfact = 0
% 2.29/2.70
% 2.29/2.70 litselect = negord
% 2.29/2.70
% 2.29/2.70 maxweight = 15
% 2.29/2.70 maxdepth = 30000
% 2.29/2.70 maxlength = 115
% 2.29/2.70 maxnrvars = 195
% 2.29/2.70 excuselevel = 1
% 2.29/2.70 increasemaxweight = 1
% 2.29/2.70
% 2.29/2.70 maxselected = 10000000
% 2.29/2.70 maxnrclauses = 10000000
% 2.29/2.70
% 2.29/2.70 showgenerated = 0
% 2.29/2.70 showkept = 0
% 2.29/2.70 showselected = 0
% 2.29/2.70 showdeleted = 0
% 2.29/2.70 showresimp = 1
% 2.29/2.70 showstatus = 2000
% 2.29/2.70
% 2.29/2.70 prologoutput = 0
% 2.29/2.70 nrgoals = 5000000
% 2.29/2.70 totalproof = 1
% 2.29/2.70
% 2.29/2.70 Symbols occurring in the translation:
% 2.29/2.70
% 2.29/2.70 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.29/2.70 . [1, 2] (w:1, o:33, a:1, s:1, b:0),
% 2.29/2.70 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 2.29/2.70 ! [4, 1] (w:0, o:17, a:1, s:1, b:0),
% 2.29/2.70 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.29/2.70 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.29/2.70 aElement0 [36, 1] (w:1, o:22, a:1, s:1, b:0),
% 14.51/14.86 aRewritingSystem0 [37, 1] (w:1, o:23, a:1, s:1, b:0),
% 14.51/14.86 aReductOfIn0 [40, 3] (w:1, o:62, a:1, s:1, b:0),
% 14.51/14.86 iLess0 [41, 2] (w:1, o:57, a:1, s:1, b:0),
% 14.51/14.86 sdtmndtplgtdt0 [42, 3] (w:1, o:63, a:1, s:1, b:0),
% 14.51/14.86 sdtmndtasgtdt0 [44, 3] (w:1, o:64, a:1, s:1, b:0),
% 14.51/14.86 isConfluent0 [45, 1] (w:1, o:24, a:1, s:1, b:0),
% 14.51/14.86 isLocallyConfluent0 [47, 1] (w:1, o:25, a:1, s:1, b:0),
% 14.51/14.86 isTerminating0 [48, 1] (w:1, o:26, a:1, s:1, b:0),
% 14.51/14.86 aNormalFormOfIn0 [49, 3] (w:1, o:65, a:1, s:1, b:0),
% 14.51/14.86 xR [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 14.51/14.86 xa [51, 0] (w:1, o:12, a:1, s:1, b:0),
% 14.51/14.86 xb [52, 0] (w:1, o:13, a:1, s:1, b:0),
% 14.51/14.86 xc [53, 0] (w:1, o:14, a:1, s:1, b:0),
% 14.51/14.86 xu [54, 0] (w:1, o:15, a:1, s:1, b:0),
% 14.51/14.86 xv [55, 0] (w:1, o:16, a:1, s:1, b:0),
% 14.51/14.86 alpha1 [56, 3] (w:1, o:66, a:1, s:1, b:1),
% 14.51/14.86 alpha2 [57, 3] (w:1, o:68, a:1, s:1, b:1),
% 14.51/14.86 alpha3 [58, 3] (w:1, o:69, a:1, s:1, b:1),
% 14.51/14.86 alpha4 [59, 2] (w:1, o:58, a:1, s:1, b:1),
% 14.51/14.86 alpha5 [60, 3] (w:1, o:70, a:1, s:1, b:1),
% 14.51/14.86 alpha6 [61, 4] (w:1, o:78, a:1, s:1, b:1),
% 14.51/14.86 alpha7 [62, 3] (w:1, o:71, a:1, s:1, b:1),
% 14.51/14.86 alpha8 [63, 4] (w:1, o:79, a:1, s:1, b:1),
% 14.51/14.86 alpha9 [64, 3] (w:1, o:72, a:1, s:1, b:1),
% 14.51/14.86 alpha10 [65, 4] (w:1, o:80, a:1, s:1, b:1),
% 14.51/14.86 alpha11 [66, 3] (w:1, o:67, a:1, s:1, b:1),
% 14.51/14.86 alpha12 [67, 4] (w:1, o:81, a:1, s:1, b:1),
% 14.51/14.86 alpha13 [68, 4] (w:1, o:82, a:1, s:1, b:1),
% 14.51/14.86 alpha14 [69, 4] (w:1, o:83, a:1, s:1, b:1),
% 14.51/14.86 alpha15 [70, 4] (w:1, o:84, a:1, s:1, b:1),
% 14.51/14.86 alpha16 [71, 4] (w:1, o:85, a:1, s:1, b:1),
% 14.51/14.86 alpha17 [72, 4] (w:1, o:86, a:1, s:1, b:1),
% 14.51/14.86 skol1 [73, 3] (w:1, o:73, a:1, s:1, b:1),
% 14.51/14.86 skol2 [74, 1] (w:1, o:30, a:1, s:1, b:1),
% 14.51/14.86 skol3 [75, 3] (w:1, o:74, a:1, s:1, b:1),
% 14.51/14.86 skol4 [76, 3] (w:1, o:75, a:1, s:1, b:1),
% 14.51/14.86 skol5 [77, 1] (w:1, o:31, a:1, s:1, b:1),
% 14.51/14.86 skol6 [78, 3] (w:1, o:76, a:1, s:1, b:1),
% 14.51/14.86 skol7 [79, 3] (w:1, o:77, a:1, s:1, b:1),
% 14.51/14.86 skol8 [80, 1] (w:1, o:32, a:1, s:1, b:1),
% 14.51/14.86 skol9 [81, 2] (w:1, o:59, a:1, s:1, b:1),
% 14.51/14.86 skol10 [82, 2] (w:1, o:60, a:1, s:1, b:1),
% 14.51/14.86 skol11 [83, 2] (w:1, o:61, a:1, s:1, b:1),
% 14.51/14.86 skol12 [84, 1] (w:1, o:27, a:1, s:1, b:1),
% 14.51/14.86 skol13 [85, 1] (w:1, o:28, a:1, s:1, b:1),
% 14.51/14.86 skol14 [86, 1] (w:1, o:29, a:1, s:1, b:1).
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Starting Search:
% 14.51/14.86
% 14.51/14.86 *** allocated 15000 integers for clauses
% 14.51/14.86 *** allocated 22500 integers for clauses
% 14.51/14.86 *** allocated 15000 integers for termspace/termends
% 14.51/14.86 *** allocated 33750 integers for clauses
% 14.51/14.86 *** allocated 50625 integers for clauses
% 14.51/14.86 *** allocated 22500 integers for termspace/termends
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 75937 integers for clauses
% 14.51/14.86 *** allocated 33750 integers for termspace/termends
% 14.51/14.86 *** allocated 113905 integers for clauses
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 7742
% 14.51/14.86 Kept: 2014
% 14.51/14.86 Inuse: 300
% 14.51/14.86 Deleted: 2
% 14.51/14.86 Deletedinuse: 1
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 50625 integers for termspace/termends
% 14.51/14.86 *** allocated 170857 integers for clauses
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 75937 integers for termspace/termends
% 14.51/14.86 *** allocated 256285 integers for clauses
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 15555
% 14.51/14.86 Kept: 4026
% 14.51/14.86 Inuse: 558
% 14.51/14.86 Deleted: 36
% 14.51/14.86 Deletedinuse: 6
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 113905 integers for termspace/termends
% 14.51/14.86 *** allocated 384427 integers for clauses
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 33652
% 14.51/14.86 Kept: 6037
% 14.51/14.86 Inuse: 715
% 14.51/14.86 Deleted: 53
% 14.51/14.86 Deletedinuse: 14
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 170857 integers for termspace/termends
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 53884
% 14.51/14.86 Kept: 8038
% 14.51/14.86 Inuse: 1036
% 14.51/14.86 Deleted: 74
% 14.51/14.86 Deletedinuse: 15
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 576640 integers for clauses
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 105375
% 14.51/14.86 Kept: 10039
% 14.51/14.86 Inuse: 1406
% 14.51/14.86 Deleted: 81
% 14.51/14.86 Deletedinuse: 16
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 256285 integers for termspace/termends
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 224283
% 14.51/14.86 Kept: 12040
% 14.51/14.86 Inuse: 1765
% 14.51/14.86 Deleted: 135
% 14.51/14.86 Deletedinuse: 21
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 267239
% 14.51/14.86 Kept: 14078
% 14.51/14.86 Inuse: 1928
% 14.51/14.86 Deleted: 139
% 14.51/14.86 Deletedinuse: 21
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 864960 integers for clauses
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 290288
% 14.51/14.86 Kept: 16174
% 14.51/14.86 Inuse: 2003
% 14.51/14.86 Deleted: 145
% 14.51/14.86 Deletedinuse: 21
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 384427 integers for termspace/termends
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 317979
% 14.51/14.86 Kept: 18217
% 14.51/14.86 Inuse: 2151
% 14.51/14.86 Deleted: 162
% 14.51/14.86 Deletedinuse: 27
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying clauses:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 398994
% 14.51/14.86 Kept: 20857
% 14.51/14.86 Inuse: 2412
% 14.51/14.86 Deleted: 5537
% 14.51/14.86 Deletedinuse: 96
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 1297440 integers for clauses
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 450372
% 14.51/14.86 Kept: 22872
% 14.51/14.86 Inuse: 2696
% 14.51/14.86 Deleted: 5857
% 14.51/14.86 Deletedinuse: 405
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 472892
% 14.51/14.86 Kept: 24879
% 14.51/14.86 Inuse: 2833
% 14.51/14.86 Deleted: 5883
% 14.51/14.86 Deletedinuse: 413
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 576640 integers for termspace/termends
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 516679
% 14.51/14.86 Kept: 26908
% 14.51/14.86 Inuse: 3012
% 14.51/14.86 Deleted: 5979
% 14.51/14.86 Deletedinuse: 421
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 529161
% 14.51/14.86 Kept: 28942
% 14.51/14.86 Inuse: 3064
% 14.51/14.86 Deleted: 5979
% 14.51/14.86 Deletedinuse: 421
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 565609
% 14.51/14.86 Kept: 30951
% 14.51/14.86 Inuse: 3254
% 14.51/14.86 Deleted: 6025
% 14.51/14.86 Deletedinuse: 421
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 1946160 integers for clauses
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 607364
% 14.51/14.86 Kept: 33044
% 14.51/14.86 Inuse: 3400
% 14.51/14.86 Deleted: 6089
% 14.51/14.86 Deletedinuse: 424
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 628202
% 14.51/14.86 Kept: 35089
% 14.51/14.86 Inuse: 3454
% 14.51/14.86 Deleted: 6125
% 14.51/14.86 Deletedinuse: 439
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 655272
% 14.51/14.86 Kept: 37095
% 14.51/14.86 Inuse: 3592
% 14.51/14.86 Deleted: 6181
% 14.51/14.86 Deletedinuse: 443
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 701413
% 14.51/14.86 Kept: 39098
% 14.51/14.86 Inuse: 3938
% 14.51/14.86 Deleted: 6214
% 14.51/14.86 Deletedinuse: 443
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 864960 integers for termspace/termends
% 14.51/14.86 Resimplifying clauses:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 734678
% 14.51/14.86 Kept: 42152
% 14.51/14.86 Inuse: 4074
% 14.51/14.86 Deleted: 10946
% 14.51/14.86 Deletedinuse: 443
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 760483
% 14.51/14.86 Kept: 44185
% 14.51/14.86 Inuse: 4174
% 14.51/14.86 Deleted: 10946
% 14.51/14.86 Deletedinuse: 443
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 792251
% 14.51/14.86 Kept: 46198
% 14.51/14.86 Inuse: 4294
% 14.51/14.86 Deleted: 10970
% 14.51/14.86 Deletedinuse: 443
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 *** allocated 2919240 integers for clauses
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 842394
% 14.51/14.86 Kept: 48273
% 14.51/14.86 Inuse: 4430
% 14.51/14.86 Deleted: 10970
% 14.51/14.86 Deletedinuse: 443
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 870001
% 14.51/14.86 Kept: 50294
% 14.51/14.86 Inuse: 4760
% 14.51/14.86 Deleted: 10970
% 14.51/14.86 Deletedinuse: 443
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 896569
% 14.51/14.86 Kept: 52298
% 14.51/14.86 Inuse: 4992
% 14.51/14.86 Deleted: 10970
% 14.51/14.86 Deletedinuse: 443
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Intermediate Status:
% 14.51/14.86 Generated: 917397
% 14.51/14.86 Kept: 54331
% 14.51/14.86 Inuse: 5145
% 14.51/14.86 Deleted: 10970
% 14.51/14.86 Deletedinuse: 443
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86 Resimplifying inuse:
% 14.51/14.86 Done
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Bliksems!, er is een bewijs:
% 14.51/14.86 % SZS status Theorem
% 14.51/14.86 % SZS output start Refutation
% 14.51/14.86
% 14.51/14.86 (13) {G0,W13,D2,L5,V3,M5} I { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 14.51/14.86 aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y, Z ) }.
% 14.51/14.86 (37) {G0,W12,D2,L4,V3,M4} I { ! aRewritingSystem0( X ), !
% 14.51/14.86 isLocallyConfluent0( X ), ! alpha3( X, Y, Z ), alpha9( X, Y, Z ) }.
% 14.51/14.86 (40) {G0,W9,D3,L2,V6,M2} I { ! alpha9( X, Y, Z ), aElement0( skol6( T, U, W
% 14.51/14.86 ) ) }.
% 14.51/14.86 (41) {G0,W12,D3,L2,V3,M2} I { ! alpha9( X, Y, Z ), alpha14( X, Y, Z, skol6
% 14.51/14.86 ( X, Y, Z ) ) }.
% 14.51/14.86 (42) {G0,W11,D2,L3,V4,M3} I { ! aElement0( T ), ! alpha14( X, Y, Z, T ),
% 14.51/14.86 alpha9( X, Y, Z ) }.
% 14.51/14.86 (43) {G0,W9,D2,L2,V4,M2} I { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Y, X
% 14.51/14.86 , T ) }.
% 14.51/14.86 (44) {G0,W9,D2,L2,V4,M2} I { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Z, X
% 14.51/14.86 , T ) }.
% 14.51/14.86 (45) {G0,W13,D2,L3,V4,M3} I { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0
% 14.51/14.86 ( Z, X, T ), alpha14( X, Y, Z, T ) }.
% 14.51/14.86 (48) {G0,W11,D2,L3,V4,M3} I { ! aElement0( T ), ! alpha10( X, Y, Z, T ),
% 14.51/14.86 alpha3( X, Y, Z ) }.
% 14.51/14.86 (51) {G0,W12,D2,L3,V4,M3} I { ! aElement0( Y ), ! alpha15( X, Y, Z, T ),
% 14.51/14.86 alpha10( X, Y, Z, T ) }.
% 14.51/14.86 (54) {G0,W12,D2,L3,V4,M3} I { ! aElement0( Z ), ! alpha17( X, Y, Z, T ),
% 14.51/14.86 alpha15( X, Y, Z, T ) }.
% 14.51/14.86 (57) {G0,W13,D2,L3,V4,M3} I { ! aReductOfIn0( Y, T, X ), ! aReductOfIn0( Z
% 14.51/14.86 , T, X ), alpha17( X, Y, Z, T ) }.
% 14.51/14.86 (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 14.51/14.86 (75) {G0,W2,D2,L1,V0,M1} I { isLocallyConfluent0( xR ) }.
% 14.51/14.86 (77) {G0,W2,D2,L1,V0,M1} I { aElement0( xa ) }.
% 14.51/14.86 (85) {G0,W2,D2,L1,V0,M1} I { aElement0( xu ) }.
% 14.51/14.86 (86) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xu, xa, xR ) }.
% 14.51/14.86 (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 14.51/14.86 (89) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xv, xa, xR ) }.
% 14.51/14.86 (91) {G0,W10,D2,L3,V1,M3} I { ! aElement0( X ), ! sdtmndtasgtdt0( xu, xR, X
% 14.51/14.86 ), ! sdtmndtasgtdt0( xv, xR, X ) }.
% 14.51/14.86 (99) {G1,W9,D2,L2,V3,M2} F(45) { ! sdtmndtasgtdt0( X, Y, Z ), alpha14( Y, X
% 14.51/14.86 , X, Z ) }.
% 14.51/14.86 (498) {G1,W11,D2,L4,V2,M4} R(13,74) { ! aElement0( X ), ! aElement0( Y ), !
% 14.51/14.86 X = Y, sdtmndtasgtdt0( X, xR, Y ) }.
% 14.51/14.86 (516) {G2,W6,D2,L2,V1,M2} F(498);q { ! aElement0( X ), sdtmndtasgtdt0( X,
% 14.51/14.86 xR, X ) }.
% 14.51/14.86 (688) {G3,W4,D2,L1,V0,M1} R(516,88) { sdtmndtasgtdt0( xv, xR, xv ) }.
% 14.51/14.86 (1045) {G1,W8,D2,L2,V2,M2} R(37,74);r(75) { ! alpha3( xR, X, Y ), alpha9(
% 14.51/14.86 xR, X, Y ) }.
% 14.51/14.86 (1159) {G1,W11,D3,L2,V3,M2} R(43,41) { sdtmndtasgtdt0( X, Y, skol6( Y, X, Z
% 14.51/14.86 ) ), ! alpha9( Y, X, Z ) }.
% 14.51/14.86 (1167) {G1,W11,D3,L2,V3,M2} R(44,41) { sdtmndtasgtdt0( X, Y, skol6( Y, Z, X
% 14.51/14.86 ) ), ! alpha9( Y, Z, X ) }.
% 14.51/14.86 (1316) {G1,W9,D2,L2,V3,M2} R(48,77) { ! alpha10( X, Y, Z, xa ), alpha3( X,
% 14.51/14.86 Y, Z ) }.
% 14.51/14.86 (1405) {G1,W10,D2,L2,V3,M2} R(51,88) { ! alpha15( X, xv, Y, Z ), alpha10( X
% 14.51/14.86 , xv, Y, Z ) }.
% 14.51/14.86 (1441) {G1,W10,D2,L2,V3,M2} R(54,85) { ! alpha17( X, Y, xu, Z ), alpha15( X
% 14.51/14.86 , Y, xu, Z ) }.
% 14.51/14.86 (1485) {G1,W9,D2,L2,V1,M2} R(57,86) { ! aReductOfIn0( X, xa, xR ), alpha17
% 14.51/14.86 ( xR, X, xu, xa ) }.
% 14.51/14.86 (2733) {G4,W5,D2,L1,V0,M1} R(99,688) { alpha14( xR, xv, xv, xv ) }.
% 14.51/14.86 (2796) {G5,W4,D2,L1,V0,M1} R(2733,42);r(88) { alpha9( xR, xv, xv ) }.
% 14.51/14.86 (2798) {G6,W5,D3,L1,V3,M1} R(2796,40) { aElement0( skol6( X, Y, Z ) ) }.
% 14.51/14.86 (55718) {G2,W5,D2,L1,V0,M1} R(1485,89) { alpha17( xR, xv, xu, xa ) }.
% 14.51/14.86 (55719) {G3,W5,D2,L1,V0,M1} R(55718,1441) { alpha15( xR, xv, xu, xa ) }.
% 14.51/14.86 (55721) {G4,W5,D2,L1,V0,M1} R(55719,1405) { alpha10( xR, xv, xu, xa ) }.
% 14.51/14.86 (55726) {G5,W4,D2,L1,V0,M1} R(55721,1316) { alpha3( xR, xv, xu ) }.
% 14.51/14.86 (55735) {G6,W4,D2,L1,V0,M1} R(55726,1045) { alpha9( xR, xv, xu ) }.
% 14.51/14.86 (55749) {G7,W7,D3,L1,V0,M1} R(55735,1167) { sdtmndtasgtdt0( xu, xR, skol6(
% 14.51/14.86 xR, xv, xu ) ) }.
% 14.51/14.86 (55750) {G7,W7,D3,L1,V0,M1} R(55735,1159) { sdtmndtasgtdt0( xv, xR, skol6(
% 14.51/14.86 xR, xv, xu ) ) }.
% 14.51/14.86 (55836) {G8,W7,D3,L1,V0,M1} R(55749,91);r(2798) { ! sdtmndtasgtdt0( xv, xR
% 14.51/14.86 , skol6( xR, xv, xu ) ) }.
% 14.51/14.86 (55860) {G9,W0,D0,L0,V0,M0} S(55836);r(55750) { }.
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 % SZS output end Refutation
% 14.51/14.86 found a proof!
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Unprocessed initial clauses:
% 14.51/14.86
% 14.51/14.86 (55862) {G0,W1,D1,L1,V0,M1} { && }.
% 14.51/14.86 (55863) {G0,W1,D1,L1,V0,M1} { && }.
% 14.51/14.86 (55864) {G0,W10,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aReductOfIn0( Z, X, Y ), aElement0( Z ) }.
% 14.51/14.86 (55865) {G0,W1,D1,L1,V0,M1} { && }.
% 14.51/14.86 (55866) {G0,W1,D1,L1,V0,M1} { && }.
% 14.51/14.86 (55867) {G0,W18,D2,L6,V3,M6} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ), aReductOfIn0( Z, X, Y )
% 14.51/14.86 , alpha1( X, Y, Z ) }.
% 14.51/14.86 (55868) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aElement0( Z ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z )
% 14.51/14.86 }.
% 14.51/14.86 (55869) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aElement0( Z ), ! alpha1( X, Y, Z ), sdtmndtplgtdt0( X, Y, Z ) }.
% 14.51/14.86 (55870) {G0,W9,D3,L2,V6,M2} { ! alpha1( X, Y, Z ), aElement0( skol1( T, U
% 14.51/14.86 , W ) ) }.
% 14.51/14.86 (55871) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), alpha6( X, Y, Z, skol1
% 14.51/14.86 ( X, Y, Z ) ) }.
% 14.51/14.86 (55872) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha6( X, Y, Z, T ),
% 14.51/14.86 alpha1( X, Y, Z ) }.
% 14.51/14.86 (55873) {G0,W9,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), aReductOfIn0( T, X,
% 14.51/14.86 Y ) }.
% 14.51/14.86 (55874) {G0,W9,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), sdtmndtplgtdt0( T, Y
% 14.51/14.86 , Z ) }.
% 14.51/14.86 (55875) {G0,W13,D2,L3,V4,M3} { ! aReductOfIn0( T, X, Y ), ! sdtmndtplgtdt0
% 14.51/14.86 ( T, Y, Z ), alpha6( X, Y, Z, T ) }.
% 14.51/14.86 (55876) {G0,W20,D2,L7,V4,M7} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aElement0( Z ), ! aElement0( T ), ! sdtmndtplgtdt0( X, Y, Z ), !
% 14.51/14.86 sdtmndtplgtdt0( Z, Y, T ), sdtmndtplgtdt0( X, Y, T ) }.
% 14.51/14.86 (55877) {G0,W17,D2,L6,V3,M6} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aElement0( Z ), ! sdtmndtasgtdt0( X, Y, Z ), X = Z, sdtmndtplgtdt0( X
% 14.51/14.86 , Y, Z ) }.
% 14.51/14.86 (55878) {G0,W13,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y, Z ) }.
% 14.51/14.86 (55879) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z
% 14.51/14.86 ) }.
% 14.51/14.86 (55880) {G0,W20,D2,L7,V4,M7} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aElement0( Z ), ! aElement0( T ), ! sdtmndtasgtdt0( X, Y, Z ), !
% 14.51/14.86 sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X, Y, T ) }.
% 14.51/14.86 (55881) {G0,W12,D2,L4,V3,M4} { ! aRewritingSystem0( X ), ! isConfluent0( X
% 14.51/14.86 ), ! alpha2( X, Y, Z ), alpha7( X, Y, Z ) }.
% 14.51/14.86 (55882) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha2( X, skol2
% 14.51/14.86 ( X ), skol12( X ) ), isConfluent0( X ) }.
% 14.51/14.86 (55883) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha7( X,
% 14.51/14.86 skol2( X ), skol12( X ) ), isConfluent0( X ) }.
% 14.51/14.86 (55884) {G0,W9,D3,L2,V6,M2} { ! alpha7( X, Y, Z ), aElement0( skol3( T, U
% 14.51/14.86 , W ) ) }.
% 14.51/14.86 (55885) {G0,W12,D3,L2,V3,M2} { ! alpha7( X, Y, Z ), alpha12( X, Y, Z,
% 14.51/14.86 skol3( X, Y, Z ) ) }.
% 14.51/14.86 (55886) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha12( X, Y, Z, T ),
% 14.51/14.86 alpha7( X, Y, Z ) }.
% 14.51/14.86 (55887) {G0,W9,D2,L2,V4,M2} { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Y,
% 14.51/14.86 X, T ) }.
% 14.51/14.86 (55888) {G0,W9,D2,L2,V4,M2} { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Z,
% 14.51/14.86 X, T ) }.
% 14.51/14.86 (55889) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( Y, X, T ), !
% 14.51/14.86 sdtmndtasgtdt0( Z, X, T ), alpha12( X, Y, Z, T ) }.
% 14.51/14.86 (55890) {G0,W9,D3,L2,V6,M2} { ! alpha2( X, Y, Z ), aElement0( skol4( T, U
% 14.51/14.86 , W ) ) }.
% 14.51/14.86 (55891) {G0,W12,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), alpha8( X, Y, Z, skol4
% 14.51/14.86 ( X, Y, Z ) ) }.
% 14.51/14.86 (55892) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha8( X, Y, Z, T ),
% 14.51/14.86 alpha2( X, Y, Z ) }.
% 14.51/14.86 (55893) {G0,W7,D2,L2,V4,M2} { ! alpha8( X, Y, Z, T ), aElement0( Y ) }.
% 14.51/14.86 (55894) {G0,W10,D2,L2,V4,M2} { ! alpha8( X, Y, Z, T ), alpha13( X, Y, Z, T
% 14.51/14.86 ) }.
% 14.51/14.86 (55895) {G0,W12,D2,L3,V4,M3} { ! aElement0( Y ), ! alpha13( X, Y, Z, T ),
% 14.51/14.86 alpha8( X, Y, Z, T ) }.
% 14.51/14.86 (55896) {G0,W7,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), aElement0( Z ) }.
% 14.51/14.86 (55897) {G0,W10,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), alpha16( X, Y, Z,
% 14.51/14.86 T ) }.
% 14.51/14.86 (55898) {G0,W12,D2,L3,V4,M3} { ! aElement0( Z ), ! alpha16( X, Y, Z, T ),
% 14.51/14.86 alpha13( X, Y, Z, T ) }.
% 14.51/14.86 (55899) {G0,W9,D2,L2,V4,M2} { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T,
% 14.51/14.86 X, Y ) }.
% 14.51/14.86 (55900) {G0,W9,D2,L2,V4,M2} { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T,
% 14.51/14.86 X, Z ) }.
% 14.51/14.86 (55901) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( T, X, Y ), !
% 14.51/14.86 sdtmndtasgtdt0( T, X, Z ), alpha16( X, Y, Z, T ) }.
% 14.51/14.86 (55902) {G0,W12,D2,L4,V3,M4} { ! aRewritingSystem0( X ), !
% 14.51/14.86 isLocallyConfluent0( X ), ! alpha3( X, Y, Z ), alpha9( X, Y, Z ) }.
% 14.51/14.86 (55903) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha3( X, skol5
% 14.51/14.86 ( X ), skol13( X ) ), isLocallyConfluent0( X ) }.
% 14.51/14.86 (55904) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha9( X,
% 14.51/14.86 skol5( X ), skol13( X ) ), isLocallyConfluent0( X ) }.
% 14.51/14.86 (55905) {G0,W9,D3,L2,V6,M2} { ! alpha9( X, Y, Z ), aElement0( skol6( T, U
% 14.51/14.86 , W ) ) }.
% 14.51/14.86 (55906) {G0,W12,D3,L2,V3,M2} { ! alpha9( X, Y, Z ), alpha14( X, Y, Z,
% 14.51/14.86 skol6( X, Y, Z ) ) }.
% 14.51/14.86 (55907) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha14( X, Y, Z, T ),
% 14.51/14.86 alpha9( X, Y, Z ) }.
% 14.51/14.86 (55908) {G0,W9,D2,L2,V4,M2} { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Y,
% 14.51/14.86 X, T ) }.
% 14.51/14.86 (55909) {G0,W9,D2,L2,V4,M2} { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Z,
% 14.51/14.86 X, T ) }.
% 14.51/14.86 (55910) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( Y, X, T ), !
% 14.51/14.86 sdtmndtasgtdt0( Z, X, T ), alpha14( X, Y, Z, T ) }.
% 14.51/14.86 (55911) {G0,W9,D3,L2,V6,M2} { ! alpha3( X, Y, Z ), aElement0( skol7( T, U
% 14.51/14.86 , W ) ) }.
% 14.51/14.86 (55912) {G0,W12,D3,L2,V3,M2} { ! alpha3( X, Y, Z ), alpha10( X, Y, Z,
% 14.51/14.86 skol7( X, Y, Z ) ) }.
% 14.51/14.86 (55913) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha10( X, Y, Z, T ),
% 14.51/14.86 alpha3( X, Y, Z ) }.
% 14.51/14.86 (55914) {G0,W7,D2,L2,V4,M2} { ! alpha10( X, Y, Z, T ), aElement0( Y ) }.
% 14.51/14.86 (55915) {G0,W10,D2,L2,V4,M2} { ! alpha10( X, Y, Z, T ), alpha15( X, Y, Z,
% 14.51/14.86 T ) }.
% 14.51/14.86 (55916) {G0,W12,D2,L3,V4,M3} { ! aElement0( Y ), ! alpha15( X, Y, Z, T ),
% 14.51/14.86 alpha10( X, Y, Z, T ) }.
% 14.51/14.86 (55917) {G0,W7,D2,L2,V4,M2} { ! alpha15( X, Y, Z, T ), aElement0( Z ) }.
% 14.51/14.86 (55918) {G0,W10,D2,L2,V4,M2} { ! alpha15( X, Y, Z, T ), alpha17( X, Y, Z,
% 14.51/14.86 T ) }.
% 14.51/14.86 (55919) {G0,W12,D2,L3,V4,M3} { ! aElement0( Z ), ! alpha17( X, Y, Z, T ),
% 14.51/14.86 alpha15( X, Y, Z, T ) }.
% 14.51/14.86 (55920) {G0,W9,D2,L2,V4,M2} { ! alpha17( X, Y, Z, T ), aReductOfIn0( Y, T
% 14.51/14.86 , X ) }.
% 14.51/14.86 (55921) {G0,W9,D2,L2,V4,M2} { ! alpha17( X, Y, Z, T ), aReductOfIn0( Z, T
% 14.51/14.86 , X ) }.
% 14.51/14.86 (55922) {G0,W13,D2,L3,V4,M3} { ! aReductOfIn0( Y, T, X ), ! aReductOfIn0(
% 14.51/14.86 Z, T, X ), alpha17( X, Y, Z, T ) }.
% 14.51/14.86 (55923) {G0,W11,D2,L4,V3,M4} { ! aRewritingSystem0( X ), ! isTerminating0
% 14.51/14.86 ( X ), ! alpha4( Y, Z ), alpha11( X, Y, Z ) }.
% 14.51/14.86 (55924) {G0,W9,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha4( skol8( X )
% 14.51/14.86 , skol14( X ) ), isTerminating0( X ) }.
% 14.51/14.86 (55925) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha11( X,
% 14.51/14.86 skol8( X ), skol14( X ) ), isTerminating0( X ) }.
% 14.51/14.86 (55926) {G0,W11,D2,L3,V3,M3} { ! alpha11( X, Y, Z ), ! sdtmndtplgtdt0( Y,
% 14.51/14.86 X, Z ), iLess0( Z, Y ) }.
% 14.51/14.86 (55927) {G0,W8,D2,L2,V3,M2} { sdtmndtplgtdt0( Y, X, Z ), alpha11( X, Y, Z
% 14.51/14.86 ) }.
% 14.51/14.86 (55928) {G0,W7,D2,L2,V3,M2} { ! iLess0( Z, Y ), alpha11( X, Y, Z ) }.
% 14.51/14.86 (55929) {G0,W5,D2,L2,V2,M2} { ! alpha4( X, Y ), aElement0( X ) }.
% 14.51/14.86 (55930) {G0,W5,D2,L2,V2,M2} { ! alpha4( X, Y ), aElement0( Y ) }.
% 14.51/14.86 (55931) {G0,W7,D2,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y ), alpha4(
% 14.51/14.86 X, Y ) }.
% 14.51/14.86 (55932) {G0,W10,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aNormalFormOfIn0( Z, X, Y ), aElement0( Z ) }.
% 14.51/14.86 (55933) {G0,W12,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aNormalFormOfIn0( Z, X, Y ), alpha5( X, Y, Z ) }.
% 14.51/14.86 (55934) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y )
% 14.51/14.86 , ! aElement0( Z ), ! alpha5( X, Y, Z ), aNormalFormOfIn0( Z, X, Y ) }.
% 14.51/14.86 (55935) {G0,W8,D2,L2,V3,M2} { ! alpha5( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z
% 14.51/14.86 ) }.
% 14.51/14.86 (55936) {G0,W8,D2,L2,V4,M2} { ! alpha5( X, Y, Z ), ! aReductOfIn0( T, Z, Y
% 14.51/14.86 ) }.
% 14.51/14.86 (55937) {G0,W14,D3,L3,V3,M3} { ! sdtmndtasgtdt0( X, Y, Z ), aReductOfIn0(
% 14.51/14.86 skol9( Y, Z ), Z, Y ), alpha5( X, Y, Z ) }.
% 14.51/14.86 (55938) {G0,W12,D3,L4,V2,M4} { ! aRewritingSystem0( X ), ! isTerminating0
% 14.51/14.86 ( X ), ! aElement0( Y ), aNormalFormOfIn0( skol10( X, Y ), Y, X ) }.
% 14.51/14.86 (55939) {G0,W2,D2,L1,V0,M1} { aRewritingSystem0( xR ) }.
% 14.51/14.86 (55940) {G0,W2,D2,L1,V0,M1} { isLocallyConfluent0( xR ) }.
% 14.51/14.86 (55941) {G0,W2,D2,L1,V0,M1} { isTerminating0( xR ) }.
% 14.51/14.86 (55942) {G0,W2,D2,L1,V0,M1} { aElement0( xa ) }.
% 14.51/14.86 (55943) {G0,W2,D2,L1,V0,M1} { aElement0( xb ) }.
% 14.51/14.86 (55944) {G0,W2,D2,L1,V0,M1} { aElement0( xc ) }.
% 14.51/14.86 (55945) {G0,W21,D3,L7,V5,M7} { ! aElement0( X ), ! aElement0( Y ), !
% 14.51/14.86 aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, Z
% 14.51/14.86 ), ! iLess0( X, xa ), aElement0( skol11( T, U ) ) }.
% 14.51/14.86 (55946) {G0,W23,D3,L7,V4,M7} { ! aElement0( X ), ! aElement0( Y ), !
% 14.51/14.86 aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, Z
% 14.51/14.86 ), ! iLess0( X, xa ), sdtmndtasgtdt0( Z, xR, skol11( T, Z ) ) }.
% 14.51/14.86 (55947) {G0,W23,D3,L7,V3,M7} { ! aElement0( X ), ! aElement0( Y ), !
% 14.51/14.86 aElement0( Z ), ! sdtmndtasgtdt0( X, xR, Y ), ! sdtmndtasgtdt0( X, xR, Z
% 14.51/14.86 ), ! iLess0( X, xa ), sdtmndtasgtdt0( Y, xR, skol11( Y, Z ) ) }.
% 14.51/14.86 (55948) {G0,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xb ) }.
% 14.51/14.86 (55949) {G0,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xc ) }.
% 14.51/14.86 (55950) {G0,W2,D2,L1,V0,M1} { aElement0( xu ) }.
% 14.51/14.86 (55951) {G0,W4,D2,L1,V0,M1} { aReductOfIn0( xu, xa, xR ) }.
% 14.51/14.86 (55952) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, xb ) }.
% 14.51/14.86 (55953) {G0,W2,D2,L1,V0,M1} { aElement0( xv ) }.
% 14.51/14.86 (55954) {G0,W4,D2,L1,V0,M1} { aReductOfIn0( xv, xa, xR ) }.
% 14.51/14.86 (55955) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, xc ) }.
% 14.51/14.86 (55956) {G0,W10,D2,L3,V1,M3} { ! aElement0( X ), ! sdtmndtasgtdt0( xu, xR
% 14.51/14.86 , X ), ! sdtmndtasgtdt0( xv, xR, X ) }.
% 14.51/14.86
% 14.51/14.86
% 14.51/14.86 Total Proof:
% 14.51/14.86
% 14.51/14.86 subsumption: (13) {G0,W13,D2,L5,V3,M5} I { ! aElement0( X ), !
% 14.51/14.86 aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y,
% 14.51/14.86 Z ) }.
% 14.51/14.86 parent0: (55878) {G0,W13,D2,L5,V3,M5} { ! aElement0( X ), !
% 14.51/14.86 aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y,
% 14.51/14.86 Z ) }.
% 14.51/14.86 substitution0:
% 14.51/14.86 X := X
% 14.51/14.86 Y := Y
% 14.51/14.86 Z := Z
% 14.51/14.86 end
% 14.51/14.86 permutation0:
% 14.51/14.86 0 ==> 0
% 14.51/14.86 1 ==> 1
% 14.51/14.86 2 ==> 2
% 14.51/14.86 3 ==> 3
% 14.51/14.86 4 ==> 4
% 14.51/14.86 end
% 14.51/14.86
% 14.51/14.86 subsumption: (37) {G0,W12,D2,L4,V3,M4} I { ! aRewritingSystem0( X ), !
% 14.51/14.86 isLocallyConfluent0( X ), ! alpha3( X, Y, Z ), alpha9( X, Y, Z ) }.
% 14.51/14.86 parent0: (55902) {G0,W12,D2,L4,V3,M4} { ! aRewritingSystem0( X ), !
% 14.51/14.86 isLocallyConfluent0( X ), ! alpha3( X, Y, Z ), alpha9( X, Y, Z ) }.
% 14.51/14.86 substitution0:
% 14.51/14.86 X := X
% 14.51/14.86 Y := Y
% 14.51/14.86 Z := Z
% 14.51/14.86 end
% 14.51/14.86 permutation0:
% 14.51/14.86 0 ==> 0
% 14.51/14.86 1 ==> 1
% 14.51/14.86 2 ==> 2
% 14.51/14.86 3 ==> 3
% 14.51/14.86 end
% 14.51/14.86
% 14.51/14.86 subsumption: (40) {G0,W9,D3,L2,V6,M2} I { ! alpha9( X, Y, Z ), aElement0(
% 14.51/14.86 skol6( T, U, W ) ) }.
% 14.51/14.86 parent0: (55905) {G0,W9,D3,L2,V6,M2} { ! alpha9( X, Y, Z ), aElement0(
% 14.51/14.86 skol6( T, U, W ) ) }.
% 14.51/14.86 substitution0:
% 14.51/14.86 X := X
% 14.51/14.86 Y := Y
% 14.51/14.86 Z := Z
% 14.51/14.86 T := T
% 14.51/14.86 U := U
% 14.51/14.86 W := W
% 14.51/14.86 end
% 14.51/14.86 permutation0:
% 14.51/14.86 0 ==> 0
% 14.51/14.86 1 ==> 1
% 14.51/14.86 end
% 14.51/14.86
% 14.51/14.86 subsumption: (41) {G0,W12,D3,L2,V3,M2} I { ! alpha9( X, Y, Z ), alpha14( X
% 14.51/14.86 , Y, Z, skol6( X, Y, Z ) ) }.
% 14.51/14.86 parent0: (55906) {G0,W12,D3,L2,V3,M2} { ! alpha9( X, Y, Z ), alpha14( X, Y
% 14.51/14.86 , Z, skol6( X, Y, Z ) ) }.
% 14.51/14.86 substitution0:
% 14.51/14.86 X := X
% 14.51/14.86 Y := Y
% 14.51/14.86 Z := Z
% 14.51/14.86 end
% 14.51/14.86 permutation0:
% 14.51/14.86 0 ==> 0
% 14.51/14.86 1 ==> 1
% 14.51/14.86 end
% 14.51/14.86
% 14.51/14.86 subsumption: (42) {G0,W11,D2,L3,V4,M3} I { ! aElement0( T ), ! alpha14( X,
% 14.51/14.86 Y, Z, T ), alpha9( X, Y, Z ) }.
% 14.51/14.86 parent0: (55907) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha14( X, Y
% 14.51/14.86 , Z, T ), alpha9( X, Y, Z ) }.
% 14.51/14.86 substitution0:
% 14.51/14.86 X := X
% 14.51/14.86 Y := Y
% 14.51/14.86 Z := Z
% 14.51/14.86 T := T
% 14.51/14.86 end
% 14.51/14.86 permutation0:
% 14.51/14.86 0 ==> 0
% 14.51/14.86 1 ==> 1
% 14.51/14.86 2 ==> 2
% 14.51/14.86 end
% 14.51/14.86
% 14.51/14.86 subsumption: (43) {G0,W9,D2,L2,V4,M2} I { ! alpha14( X, Y, Z, T ),
% 14.51/14.86 sdtmndtasgtdt0( Y, X, T ) }.
% 14.51/14.86 parent0: (55908) {G0,W9,D2,L2,V4,M2} { ! alpha14( X, Y, Z, T ),
% 14.51/14.86 sdtmndtasgtdt0( Y, X, T ) }.
% 14.51/14.86 substitution0:
% 14.51/14.86 X := X
% 14.51/14.86 Y := Y
% 14.51/14.86 Z := Z
% 14.51/14.86 T := T
% 14.51/14.86 end
% 14.51/14.86 permutation0:
% 14.51/14.86 0 ==> 0
% 14.51/14.86 1 ==> 1
% 14.51/14.86 end
% 14.51/14.86
% 14.51/14.86 subsumption: (44) {G0,W9,D2,L2,V4,M2} I { ! alpha14( X, Y, Z, T ),
% 14.51/14.86 sdtmndtasgtdt0( Z, X, T ) }.
% 14.51/14.86 parent0: (55909) {G0,W9,D2,L2,V4,M2} { ! alpha14( X, Y, Z, T ),
% 14.51/14.86 sdtmndtasgtdt0( Z, X, T ) }.
% 14.51/14.86 substitution0:
% 14.51/14.86 X := X
% 14.51/14.86 Y := Y
% 14.51/14.86 Z := Z
% 14.51/14.86 T := T
% 14.51/14.86 end
% 14.51/14.86 permutation0:
% 14.51/14.86 0 ==> 0
% 14.51/14.86 1 ==> 1
% 14.51/14.86 end
% 14.51/14.86
% 14.51/14.86 subsumption: (45) {G0,W13,D2,L3,V4,M3} I { ! sdtmndtasgtdt0( Y, X, T ), !
% 14.51/14.86 sdtmndtasgtdt0( Z, X, T ), alpha14( X, Y, Z, T ) }.
% 14.51/14.86 parent0: (55910) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( Y, X, T ), !
% 14.51/14.86 sdtmndtasgtdt0( Z, X, T ), alpha14( X, Y, Z, T ) }.
% 14.51/14.86 substitution0:
% 14.51/14.86 X := X
% 14.51/14.86 Y := Y
% 14.51/14.86 Z := Z
% 14.51/14.86 T := T
% 14.51/14.86 end
% 14.51/14.86 permutation0:
% 14.51/14.86 0 ==> 0
% 14.51/14.86 1 ==> 1
% 14.51/14.86 2 ==> 2
% 14.51/14.86 end
% 14.51/14.86
% 14.51/14.86 subsumption: (48) {G0,W11,D2,L3,V4,M3} I { ! aElement0( T ), ! alpha10( X,
% 14.51/14.86 Y, Z, T ), alpha3( X, Y, Z ) }.
% 14.51/14.86 parent0: (55913) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha10( X, Y
% 14.51/14.86 , Z, T ), alpha3( X, Y, Z ) }.
% 14.51/14.86 substitution0:
% 14.51/14.86 X := X
% 14.51/14.86 Y := Y
% 14.51/14.86 Z := Z
% 14.51/14.86 T := T
% 14.51/14.86 end
% 14.51/14.86 permutation0:
% 14.51/14.86 0 ==> 0
% 14.51/14.86 1 ==> 1
% 14.51/14.86 2 ==> 2
% 14.51/14.86 end
% 14.51/14.87
% 14.51/14.87 subsumption: (51) {G0,W12,D2,L3,V4,M3} I { ! aElement0( Y ), ! alpha15( X,
% 14.51/14.87 Y, Z, T ), alpha10( X, Y, Z, T ) }.
% 14.51/14.87 parent0: (55916) {G0,W12,D2,L3,V4,M3} { ! aElement0( Y ), ! alpha15( X, Y
% 14.51/14.87 , Z, T ), alpha10( X, Y, Z, T ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 T := T
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 2 ==> 2
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (54) {G0,W12,D2,L3,V4,M3} I { ! aElement0( Z ), ! alpha17( X,
% 14.51/14.87 Y, Z, T ), alpha15( X, Y, Z, T ) }.
% 14.51/14.87 parent0: (55919) {G0,W12,D2,L3,V4,M3} { ! aElement0( Z ), ! alpha17( X, Y
% 14.51/14.87 , Z, T ), alpha15( X, Y, Z, T ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 T := T
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 2 ==> 2
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (57) {G0,W13,D2,L3,V4,M3} I { ! aReductOfIn0( Y, T, X ), !
% 14.51/14.87 aReductOfIn0( Z, T, X ), alpha17( X, Y, Z, T ) }.
% 14.51/14.87 parent0: (55922) {G0,W13,D2,L3,V4,M3} { ! aReductOfIn0( Y, T, X ), !
% 14.51/14.87 aReductOfIn0( Z, T, X ), alpha17( X, Y, Z, T ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 T := T
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 2 ==> 2
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 14.51/14.87 parent0: (55939) {G0,W2,D2,L1,V0,M1} { aRewritingSystem0( xR ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (75) {G0,W2,D2,L1,V0,M1} I { isLocallyConfluent0( xR ) }.
% 14.51/14.87 parent0: (55940) {G0,W2,D2,L1,V0,M1} { isLocallyConfluent0( xR ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (77) {G0,W2,D2,L1,V0,M1} I { aElement0( xa ) }.
% 14.51/14.87 parent0: (55942) {G0,W2,D2,L1,V0,M1} { aElement0( xa ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (85) {G0,W2,D2,L1,V0,M1} I { aElement0( xu ) }.
% 14.51/14.87 parent0: (55950) {G0,W2,D2,L1,V0,M1} { aElement0( xu ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (86) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xu, xa, xR ) }.
% 14.51/14.87 parent0: (55951) {G0,W4,D2,L1,V0,M1} { aReductOfIn0( xu, xa, xR ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 14.51/14.87 parent0: (55953) {G0,W2,D2,L1,V0,M1} { aElement0( xv ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (89) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xv, xa, xR ) }.
% 14.51/14.87 parent0: (55954) {G0,W4,D2,L1,V0,M1} { aReductOfIn0( xv, xa, xR ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (91) {G0,W10,D2,L3,V1,M3} I { ! aElement0( X ), !
% 14.51/14.87 sdtmndtasgtdt0( xu, xR, X ), ! sdtmndtasgtdt0( xv, xR, X ) }.
% 14.51/14.87 parent0: (55956) {G0,W10,D2,L3,V1,M3} { ! aElement0( X ), ! sdtmndtasgtdt0
% 14.51/14.87 ( xu, xR, X ), ! sdtmndtasgtdt0( xv, xR, X ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 2 ==> 2
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 factor: (56521) {G0,W9,D2,L2,V3,M2} { ! sdtmndtasgtdt0( X, Y, Z ), alpha14
% 14.51/14.87 ( Y, X, X, Z ) }.
% 14.51/14.87 parent0[0, 1]: (45) {G0,W13,D2,L3,V4,M3} I { ! sdtmndtasgtdt0( Y, X, T ), !
% 14.51/14.87 sdtmndtasgtdt0( Z, X, T ), alpha14( X, Y, Z, T ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := Y
% 14.51/14.87 Y := X
% 14.51/14.87 Z := X
% 14.51/14.87 T := Z
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (99) {G1,W9,D2,L2,V3,M2} F(45) { ! sdtmndtasgtdt0( X, Y, Z ),
% 14.51/14.87 alpha14( Y, X, X, Z ) }.
% 14.51/14.87 parent0: (56521) {G0,W9,D2,L2,V3,M2} { ! sdtmndtasgtdt0( X, Y, Z ),
% 14.51/14.87 alpha14( Y, X, X, Z ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 eqswap: (56522) {G0,W13,D2,L5,V3,M5} { ! Y = X, ! aElement0( X ), !
% 14.51/14.87 aRewritingSystem0( Z ), ! aElement0( Y ), sdtmndtasgtdt0( X, Z, Y ) }.
% 14.51/14.87 parent0[3]: (13) {G0,W13,D2,L5,V3,M5} I { ! aElement0( X ), !
% 14.51/14.87 aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y,
% 14.51/14.87 Z ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Z
% 14.51/14.87 Z := Y
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56523) {G1,W11,D2,L4,V2,M4} { ! X = Y, ! aElement0( Y ), !
% 14.51/14.87 aElement0( X ), sdtmndtasgtdt0( Y, xR, X ) }.
% 14.51/14.87 parent0[2]: (56522) {G0,W13,D2,L5,V3,M5} { ! Y = X, ! aElement0( X ), !
% 14.51/14.87 aRewritingSystem0( Z ), ! aElement0( Y ), sdtmndtasgtdt0( X, Z, Y ) }.
% 14.51/14.87 parent1[0]: (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := Y
% 14.51/14.87 Y := X
% 14.51/14.87 Z := xR
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 eqswap: (56524) {G1,W11,D2,L4,V2,M4} { ! Y = X, ! aElement0( Y ), !
% 14.51/14.87 aElement0( X ), sdtmndtasgtdt0( Y, xR, X ) }.
% 14.51/14.87 parent0[0]: (56523) {G1,W11,D2,L4,V2,M4} { ! X = Y, ! aElement0( Y ), !
% 14.51/14.87 aElement0( X ), sdtmndtasgtdt0( Y, xR, X ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (498) {G1,W11,D2,L4,V2,M4} R(13,74) { ! aElement0( X ), !
% 14.51/14.87 aElement0( Y ), ! X = Y, sdtmndtasgtdt0( X, xR, Y ) }.
% 14.51/14.87 parent0: (56524) {G1,W11,D2,L4,V2,M4} { ! Y = X, ! aElement0( Y ), !
% 14.51/14.87 aElement0( X ), sdtmndtasgtdt0( Y, xR, X ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := Y
% 14.51/14.87 Y := X
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 2
% 14.51/14.87 1 ==> 0
% 14.51/14.87 2 ==> 1
% 14.51/14.87 3 ==> 3
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 eqswap: (56526) {G1,W11,D2,L4,V2,M4} { ! Y = X, ! aElement0( X ), !
% 14.51/14.87 aElement0( Y ), sdtmndtasgtdt0( X, xR, Y ) }.
% 14.51/14.87 parent0[2]: (498) {G1,W11,D2,L4,V2,M4} R(13,74) { ! aElement0( X ), !
% 14.51/14.87 aElement0( Y ), ! X = Y, sdtmndtasgtdt0( X, xR, Y ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 factor: (56527) {G1,W9,D2,L3,V1,M3} { ! X = X, ! aElement0( X ),
% 14.51/14.87 sdtmndtasgtdt0( X, xR, X ) }.
% 14.51/14.87 parent0[1, 2]: (56526) {G1,W11,D2,L4,V2,M4} { ! Y = X, ! aElement0( X ), !
% 14.51/14.87 aElement0( Y ), sdtmndtasgtdt0( X, xR, Y ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := X
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 eqrefl: (56528) {G0,W6,D2,L2,V1,M2} { ! aElement0( X ), sdtmndtasgtdt0( X
% 14.51/14.87 , xR, X ) }.
% 14.51/14.87 parent0[0]: (56527) {G1,W9,D2,L3,V1,M3} { ! X = X, ! aElement0( X ),
% 14.51/14.87 sdtmndtasgtdt0( X, xR, X ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (516) {G2,W6,D2,L2,V1,M2} F(498);q { ! aElement0( X ),
% 14.51/14.87 sdtmndtasgtdt0( X, xR, X ) }.
% 14.51/14.87 parent0: (56528) {G0,W6,D2,L2,V1,M2} { ! aElement0( X ), sdtmndtasgtdt0( X
% 14.51/14.87 , xR, X ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56529) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, xv ) }.
% 14.51/14.87 parent0[0]: (516) {G2,W6,D2,L2,V1,M2} F(498);q { ! aElement0( X ),
% 14.51/14.87 sdtmndtasgtdt0( X, xR, X ) }.
% 14.51/14.87 parent1[0]: (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xv
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (688) {G3,W4,D2,L1,V0,M1} R(516,88) { sdtmndtasgtdt0( xv, xR,
% 14.51/14.87 xv ) }.
% 14.51/14.87 parent0: (56529) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, xv ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56530) {G1,W10,D2,L3,V2,M3} { ! isLocallyConfluent0( xR ), !
% 14.51/14.87 alpha3( xR, X, Y ), alpha9( xR, X, Y ) }.
% 14.51/14.87 parent0[0]: (37) {G0,W12,D2,L4,V3,M4} I { ! aRewritingSystem0( X ), !
% 14.51/14.87 isLocallyConfluent0( X ), ! alpha3( X, Y, Z ), alpha9( X, Y, Z ) }.
% 14.51/14.87 parent1[0]: (74) {G0,W2,D2,L1,V0,M1} I { aRewritingSystem0( xR ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xR
% 14.51/14.87 Y := X
% 14.51/14.87 Z := Y
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56531) {G1,W8,D2,L2,V2,M2} { ! alpha3( xR, X, Y ), alpha9( xR
% 14.51/14.87 , X, Y ) }.
% 14.51/14.87 parent0[0]: (56530) {G1,W10,D2,L3,V2,M3} { ! isLocallyConfluent0( xR ), !
% 14.51/14.87 alpha3( xR, X, Y ), alpha9( xR, X, Y ) }.
% 14.51/14.87 parent1[0]: (75) {G0,W2,D2,L1,V0,M1} I { isLocallyConfluent0( xR ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (1045) {G1,W8,D2,L2,V2,M2} R(37,74);r(75) { ! alpha3( xR, X, Y
% 14.51/14.87 ), alpha9( xR, X, Y ) }.
% 14.51/14.87 parent0: (56531) {G1,W8,D2,L2,V2,M2} { ! alpha3( xR, X, Y ), alpha9( xR, X
% 14.51/14.87 , Y ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56532) {G1,W11,D3,L2,V3,M2} { sdtmndtasgtdt0( Y, X, skol6( X
% 14.51/14.87 , Y, Z ) ), ! alpha9( X, Y, Z ) }.
% 14.51/14.87 parent0[0]: (43) {G0,W9,D2,L2,V4,M2} I { ! alpha14( X, Y, Z, T ),
% 14.51/14.87 sdtmndtasgtdt0( Y, X, T ) }.
% 14.51/14.87 parent1[1]: (41) {G0,W12,D3,L2,V3,M2} I { ! alpha9( X, Y, Z ), alpha14( X,
% 14.51/14.87 Y, Z, skol6( X, Y, Z ) ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 T := skol6( X, Y, Z )
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (1159) {G1,W11,D3,L2,V3,M2} R(43,41) { sdtmndtasgtdt0( X, Y,
% 14.51/14.87 skol6( Y, X, Z ) ), ! alpha9( Y, X, Z ) }.
% 14.51/14.87 parent0: (56532) {G1,W11,D3,L2,V3,M2} { sdtmndtasgtdt0( Y, X, skol6( X, Y
% 14.51/14.87 , Z ) ), ! alpha9( X, Y, Z ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := Y
% 14.51/14.87 Y := X
% 14.51/14.87 Z := Z
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56533) {G1,W11,D3,L2,V3,M2} { sdtmndtasgtdt0( Z, X, skol6( X
% 14.51/14.87 , Y, Z ) ), ! alpha9( X, Y, Z ) }.
% 14.51/14.87 parent0[0]: (44) {G0,W9,D2,L2,V4,M2} I { ! alpha14( X, Y, Z, T ),
% 14.51/14.87 sdtmndtasgtdt0( Z, X, T ) }.
% 14.51/14.87 parent1[1]: (41) {G0,W12,D3,L2,V3,M2} I { ! alpha9( X, Y, Z ), alpha14( X,
% 14.51/14.87 Y, Z, skol6( X, Y, Z ) ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 T := skol6( X, Y, Z )
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (1167) {G1,W11,D3,L2,V3,M2} R(44,41) { sdtmndtasgtdt0( X, Y,
% 14.51/14.87 skol6( Y, Z, X ) ), ! alpha9( Y, Z, X ) }.
% 14.51/14.87 parent0: (56533) {G1,W11,D3,L2,V3,M2} { sdtmndtasgtdt0( Z, X, skol6( X, Y
% 14.51/14.87 , Z ) ), ! alpha9( X, Y, Z ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := Y
% 14.51/14.87 Y := Z
% 14.51/14.87 Z := X
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56534) {G1,W9,D2,L2,V3,M2} { ! alpha10( X, Y, Z, xa ), alpha3
% 14.51/14.87 ( X, Y, Z ) }.
% 14.51/14.87 parent0[0]: (48) {G0,W11,D2,L3,V4,M3} I { ! aElement0( T ), ! alpha10( X, Y
% 14.51/14.87 , Z, T ), alpha3( X, Y, Z ) }.
% 14.51/14.87 parent1[0]: (77) {G0,W2,D2,L1,V0,M1} I { aElement0( xa ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 T := xa
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (1316) {G1,W9,D2,L2,V3,M2} R(48,77) { ! alpha10( X, Y, Z, xa )
% 14.51/14.87 , alpha3( X, Y, Z ) }.
% 14.51/14.87 parent0: (56534) {G1,W9,D2,L2,V3,M2} { ! alpha10( X, Y, Z, xa ), alpha3( X
% 14.51/14.87 , Y, Z ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56535) {G1,W10,D2,L2,V3,M2} { ! alpha15( X, xv, Y, Z ),
% 14.51/14.87 alpha10( X, xv, Y, Z ) }.
% 14.51/14.87 parent0[0]: (51) {G0,W12,D2,L3,V4,M3} I { ! aElement0( Y ), ! alpha15( X, Y
% 14.51/14.87 , Z, T ), alpha10( X, Y, Z, T ) }.
% 14.51/14.87 parent1[0]: (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := xv
% 14.51/14.87 Z := Y
% 14.51/14.87 T := Z
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (1405) {G1,W10,D2,L2,V3,M2} R(51,88) { ! alpha15( X, xv, Y, Z
% 14.51/14.87 ), alpha10( X, xv, Y, Z ) }.
% 14.51/14.87 parent0: (56535) {G1,W10,D2,L2,V3,M2} { ! alpha15( X, xv, Y, Z ), alpha10
% 14.51/14.87 ( X, xv, Y, Z ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56536) {G1,W10,D2,L2,V3,M2} { ! alpha17( X, Y, xu, Z ),
% 14.51/14.87 alpha15( X, Y, xu, Z ) }.
% 14.51/14.87 parent0[0]: (54) {G0,W12,D2,L3,V4,M3} I { ! aElement0( Z ), ! alpha17( X, Y
% 14.51/14.87 , Z, T ), alpha15( X, Y, Z, T ) }.
% 14.51/14.87 parent1[0]: (85) {G0,W2,D2,L1,V0,M1} I { aElement0( xu ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := xu
% 14.51/14.87 T := Z
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (1441) {G1,W10,D2,L2,V3,M2} R(54,85) { ! alpha17( X, Y, xu, Z
% 14.51/14.87 ), alpha15( X, Y, xu, Z ) }.
% 14.51/14.87 parent0: (56536) {G1,W10,D2,L2,V3,M2} { ! alpha17( X, Y, xu, Z ), alpha15
% 14.51/14.87 ( X, Y, xu, Z ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56538) {G1,W9,D2,L2,V1,M2} { ! aReductOfIn0( X, xa, xR ),
% 14.51/14.87 alpha17( xR, X, xu, xa ) }.
% 14.51/14.87 parent0[1]: (57) {G0,W13,D2,L3,V4,M3} I { ! aReductOfIn0( Y, T, X ), !
% 14.51/14.87 aReductOfIn0( Z, T, X ), alpha17( X, Y, Z, T ) }.
% 14.51/14.87 parent1[0]: (86) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xu, xa, xR ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xR
% 14.51/14.87 Y := X
% 14.51/14.87 Z := xu
% 14.51/14.87 T := xa
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (1485) {G1,W9,D2,L2,V1,M2} R(57,86) { ! aReductOfIn0( X, xa,
% 14.51/14.87 xR ), alpha17( xR, X, xu, xa ) }.
% 14.51/14.87 parent0: (56538) {G1,W9,D2,L2,V1,M2} { ! aReductOfIn0( X, xa, xR ),
% 14.51/14.87 alpha17( xR, X, xu, xa ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 1 ==> 1
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56539) {G2,W5,D2,L1,V0,M1} { alpha14( xR, xv, xv, xv ) }.
% 14.51/14.87 parent0[0]: (99) {G1,W9,D2,L2,V3,M2} F(45) { ! sdtmndtasgtdt0( X, Y, Z ),
% 14.51/14.87 alpha14( Y, X, X, Z ) }.
% 14.51/14.87 parent1[0]: (688) {G3,W4,D2,L1,V0,M1} R(516,88) { sdtmndtasgtdt0( xv, xR,
% 14.51/14.87 xv ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xv
% 14.51/14.87 Y := xR
% 14.51/14.87 Z := xv
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (2733) {G4,W5,D2,L1,V0,M1} R(99,688) { alpha14( xR, xv, xv, xv
% 14.51/14.87 ) }.
% 14.51/14.87 parent0: (56539) {G2,W5,D2,L1,V0,M1} { alpha14( xR, xv, xv, xv ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56540) {G1,W6,D2,L2,V0,M2} { ! aElement0( xv ), alpha9( xR,
% 14.51/14.87 xv, xv ) }.
% 14.51/14.87 parent0[1]: (42) {G0,W11,D2,L3,V4,M3} I { ! aElement0( T ), ! alpha14( X, Y
% 14.51/14.87 , Z, T ), alpha9( X, Y, Z ) }.
% 14.51/14.87 parent1[0]: (2733) {G4,W5,D2,L1,V0,M1} R(99,688) { alpha14( xR, xv, xv, xv
% 14.51/14.87 ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xR
% 14.51/14.87 Y := xv
% 14.51/14.87 Z := xv
% 14.51/14.87 T := xv
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56541) {G1,W4,D2,L1,V0,M1} { alpha9( xR, xv, xv ) }.
% 14.51/14.87 parent0[0]: (56540) {G1,W6,D2,L2,V0,M2} { ! aElement0( xv ), alpha9( xR,
% 14.51/14.87 xv, xv ) }.
% 14.51/14.87 parent1[0]: (88) {G0,W2,D2,L1,V0,M1} I { aElement0( xv ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (2796) {G5,W4,D2,L1,V0,M1} R(2733,42);r(88) { alpha9( xR, xv,
% 14.51/14.87 xv ) }.
% 14.51/14.87 parent0: (56541) {G1,W4,D2,L1,V0,M1} { alpha9( xR, xv, xv ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56542) {G1,W5,D3,L1,V3,M1} { aElement0( skol6( X, Y, Z ) )
% 14.51/14.87 }.
% 14.51/14.87 parent0[0]: (40) {G0,W9,D3,L2,V6,M2} I { ! alpha9( X, Y, Z ), aElement0(
% 14.51/14.87 skol6( T, U, W ) ) }.
% 14.51/14.87 parent1[0]: (2796) {G5,W4,D2,L1,V0,M1} R(2733,42);r(88) { alpha9( xR, xv,
% 14.51/14.87 xv ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xR
% 14.51/14.87 Y := xv
% 14.51/14.87 Z := xv
% 14.51/14.87 T := X
% 14.51/14.87 U := Y
% 14.51/14.87 W := Z
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (2798) {G6,W5,D3,L1,V3,M1} R(2796,40) { aElement0( skol6( X, Y
% 14.51/14.87 , Z ) ) }.
% 14.51/14.87 parent0: (56542) {G1,W5,D3,L1,V3,M1} { aElement0( skol6( X, Y, Z ) ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := X
% 14.51/14.87 Y := Y
% 14.51/14.87 Z := Z
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56543) {G1,W5,D2,L1,V0,M1} { alpha17( xR, xv, xu, xa ) }.
% 14.51/14.87 parent0[0]: (1485) {G1,W9,D2,L2,V1,M2} R(57,86) { ! aReductOfIn0( X, xa, xR
% 14.51/14.87 ), alpha17( xR, X, xu, xa ) }.
% 14.51/14.87 parent1[0]: (89) {G0,W4,D2,L1,V0,M1} I { aReductOfIn0( xv, xa, xR ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xv
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (55718) {G2,W5,D2,L1,V0,M1} R(1485,89) { alpha17( xR, xv, xu,
% 14.51/14.87 xa ) }.
% 14.51/14.87 parent0: (56543) {G1,W5,D2,L1,V0,M1} { alpha17( xR, xv, xu, xa ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56544) {G2,W5,D2,L1,V0,M1} { alpha15( xR, xv, xu, xa ) }.
% 14.51/14.87 parent0[0]: (1441) {G1,W10,D2,L2,V3,M2} R(54,85) { ! alpha17( X, Y, xu, Z )
% 14.51/14.87 , alpha15( X, Y, xu, Z ) }.
% 14.51/14.87 parent1[0]: (55718) {G2,W5,D2,L1,V0,M1} R(1485,89) { alpha17( xR, xv, xu,
% 14.51/14.87 xa ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xR
% 14.51/14.87 Y := xv
% 14.51/14.87 Z := xa
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (55719) {G3,W5,D2,L1,V0,M1} R(55718,1441) { alpha15( xR, xv,
% 14.51/14.87 xu, xa ) }.
% 14.51/14.87 parent0: (56544) {G2,W5,D2,L1,V0,M1} { alpha15( xR, xv, xu, xa ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56545) {G2,W5,D2,L1,V0,M1} { alpha10( xR, xv, xu, xa ) }.
% 14.51/14.87 parent0[0]: (1405) {G1,W10,D2,L2,V3,M2} R(51,88) { ! alpha15( X, xv, Y, Z )
% 14.51/14.87 , alpha10( X, xv, Y, Z ) }.
% 14.51/14.87 parent1[0]: (55719) {G3,W5,D2,L1,V0,M1} R(55718,1441) { alpha15( xR, xv, xu
% 14.51/14.87 , xa ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xR
% 14.51/14.87 Y := xu
% 14.51/14.87 Z := xa
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (55721) {G4,W5,D2,L1,V0,M1} R(55719,1405) { alpha10( xR, xv,
% 14.51/14.87 xu, xa ) }.
% 14.51/14.87 parent0: (56545) {G2,W5,D2,L1,V0,M1} { alpha10( xR, xv, xu, xa ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56546) {G2,W4,D2,L1,V0,M1} { alpha3( xR, xv, xu ) }.
% 14.51/14.87 parent0[0]: (1316) {G1,W9,D2,L2,V3,M2} R(48,77) { ! alpha10( X, Y, Z, xa )
% 14.51/14.87 , alpha3( X, Y, Z ) }.
% 14.51/14.87 parent1[0]: (55721) {G4,W5,D2,L1,V0,M1} R(55719,1405) { alpha10( xR, xv, xu
% 14.51/14.87 , xa ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xR
% 14.51/14.87 Y := xv
% 14.51/14.87 Z := xu
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (55726) {G5,W4,D2,L1,V0,M1} R(55721,1316) { alpha3( xR, xv, xu
% 14.51/14.87 ) }.
% 14.51/14.87 parent0: (56546) {G2,W4,D2,L1,V0,M1} { alpha3( xR, xv, xu ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56547) {G2,W4,D2,L1,V0,M1} { alpha9( xR, xv, xu ) }.
% 14.51/14.87 parent0[0]: (1045) {G1,W8,D2,L2,V2,M2} R(37,74);r(75) { ! alpha3( xR, X, Y
% 14.51/14.87 ), alpha9( xR, X, Y ) }.
% 14.51/14.87 parent1[0]: (55726) {G5,W4,D2,L1,V0,M1} R(55721,1316) { alpha3( xR, xv, xu
% 14.51/14.87 ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xv
% 14.51/14.87 Y := xu
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (55735) {G6,W4,D2,L1,V0,M1} R(55726,1045) { alpha9( xR, xv, xu
% 14.51/14.87 ) }.
% 14.51/14.87 parent0: (56547) {G2,W4,D2,L1,V0,M1} { alpha9( xR, xv, xu ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56548) {G2,W7,D3,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, skol6(
% 14.51/14.87 xR, xv, xu ) ) }.
% 14.51/14.87 parent0[1]: (1167) {G1,W11,D3,L2,V3,M2} R(44,41) { sdtmndtasgtdt0( X, Y,
% 14.51/14.87 skol6( Y, Z, X ) ), ! alpha9( Y, Z, X ) }.
% 14.51/14.87 parent1[0]: (55735) {G6,W4,D2,L1,V0,M1} R(55726,1045) { alpha9( xR, xv, xu
% 14.51/14.87 ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xu
% 14.51/14.87 Y := xR
% 14.51/14.87 Z := xv
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (55749) {G7,W7,D3,L1,V0,M1} R(55735,1167) { sdtmndtasgtdt0( xu
% 14.51/14.87 , xR, skol6( xR, xv, xu ) ) }.
% 14.51/14.87 parent0: (56548) {G2,W7,D3,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, skol6( xR,
% 14.51/14.87 xv, xu ) ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56549) {G2,W7,D3,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, skol6(
% 14.51/14.87 xR, xv, xu ) ) }.
% 14.51/14.87 parent0[1]: (1159) {G1,W11,D3,L2,V3,M2} R(43,41) { sdtmndtasgtdt0( X, Y,
% 14.51/14.87 skol6( Y, X, Z ) ), ! alpha9( Y, X, Z ) }.
% 14.51/14.87 parent1[0]: (55735) {G6,W4,D2,L1,V0,M1} R(55726,1045) { alpha9( xR, xv, xu
% 14.51/14.87 ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := xv
% 14.51/14.87 Y := xR
% 14.51/14.87 Z := xu
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (55750) {G7,W7,D3,L1,V0,M1} R(55735,1159) { sdtmndtasgtdt0( xv
% 14.51/14.87 , xR, skol6( xR, xv, xu ) ) }.
% 14.51/14.87 parent0: (56549) {G2,W7,D3,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, skol6( xR,
% 14.51/14.87 xv, xu ) ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56550) {G1,W12,D3,L2,V0,M2} { ! aElement0( skol6( xR, xv, xu
% 14.51/14.87 ) ), ! sdtmndtasgtdt0( xv, xR, skol6( xR, xv, xu ) ) }.
% 14.51/14.87 parent0[1]: (91) {G0,W10,D2,L3,V1,M3} I { ! aElement0( X ), !
% 14.51/14.87 sdtmndtasgtdt0( xu, xR, X ), ! sdtmndtasgtdt0( xv, xR, X ) }.
% 14.51/14.87 parent1[0]: (55749) {G7,W7,D3,L1,V0,M1} R(55735,1167) { sdtmndtasgtdt0( xu
% 14.51/14.87 , xR, skol6( xR, xv, xu ) ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 X := skol6( xR, xv, xu )
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56551) {G2,W7,D3,L1,V0,M1} { ! sdtmndtasgtdt0( xv, xR, skol6
% 14.51/14.87 ( xR, xv, xu ) ) }.
% 14.51/14.87 parent0[0]: (56550) {G1,W12,D3,L2,V0,M2} { ! aElement0( skol6( xR, xv, xu
% 14.51/14.87 ) ), ! sdtmndtasgtdt0( xv, xR, skol6( xR, xv, xu ) ) }.
% 14.51/14.87 parent1[0]: (2798) {G6,W5,D3,L1,V3,M1} R(2796,40) { aElement0( skol6( X, Y
% 14.51/14.87 , Z ) ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 X := xR
% 14.51/14.87 Y := xv
% 14.51/14.87 Z := xu
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (55836) {G8,W7,D3,L1,V0,M1} R(55749,91);r(2798) { !
% 14.51/14.87 sdtmndtasgtdt0( xv, xR, skol6( xR, xv, xu ) ) }.
% 14.51/14.87 parent0: (56551) {G2,W7,D3,L1,V0,M1} { ! sdtmndtasgtdt0( xv, xR, skol6( xR
% 14.51/14.87 , xv, xu ) ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 0 ==> 0
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 resolution: (56552) {G8,W0,D0,L0,V0,M0} { }.
% 14.51/14.87 parent0[0]: (55836) {G8,W7,D3,L1,V0,M1} R(55749,91);r(2798) { !
% 14.51/14.87 sdtmndtasgtdt0( xv, xR, skol6( xR, xv, xu ) ) }.
% 14.51/14.87 parent1[0]: (55750) {G7,W7,D3,L1,V0,M1} R(55735,1159) { sdtmndtasgtdt0( xv
% 14.51/14.87 , xR, skol6( xR, xv, xu ) ) }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 substitution1:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 subsumption: (55860) {G9,W0,D0,L0,V0,M0} S(55836);r(55750) { }.
% 14.51/14.87 parent0: (56552) {G8,W0,D0,L0,V0,M0} { }.
% 14.51/14.87 substitution0:
% 14.51/14.87 end
% 14.51/14.87 permutation0:
% 14.51/14.87 end
% 14.51/14.87
% 14.51/14.87 Proof check complete!
% 14.51/14.87
% 14.51/14.87 Memory use:
% 14.51/14.87
% 14.51/14.87 space for terms: 785842
% 14.51/14.87 space for clauses: 2320876
% 14.51/14.87
% 14.51/14.87
% 14.51/14.87 clauses generated: 939590
% 14.51/14.87 clauses kept: 55861
% 14.51/14.87 clauses selected: 5292
% 14.51/14.87 clauses deleted: 10974
% 14.51/14.87 clauses inuse deleted: 443
% 14.51/14.87
% 14.51/14.87 subsentry: 1189609
% 14.51/14.87 literals s-matched: 846012
% 14.51/14.87 literals matched: 607915
% 14.51/14.87 full subsumption: 55338
% 14.51/14.87
% 14.51/14.87 checksum: 665563885
% 14.51/14.87
% 14.51/14.87
% 14.51/14.87 Bliksem ended
%------------------------------------------------------------------------------