%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : CSR021+1 : TPTP v8.1.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n023.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 02:00:53 EDT 2022
% Result : Theorem 0.76s 1.28s
% Output : Refutation 0.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : CSR021+1 : TPTP v8.1.0. Bugfixed v3.1.0.
% 0.06/0.13 % Command : bliksem %s
% 0.14/0.33 % Computer : n023.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.34 % DateTime : Fri Jun 10 10:45:07 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.71/1.12 *** allocated 10000 integers for termspace/termends
% 0.71/1.12 *** allocated 10000 integers for clauses
% 0.71/1.12 *** allocated 10000 integers for justifications
% 0.71/1.12 Bliksem 1.12
% 0.71/1.12
% 0.71/1.12
% 0.71/1.12 Automatic Strategy Selection
% 0.71/1.12
% 0.71/1.12
% 0.71/1.12 Clauses:
% 0.71/1.12
% 0.71/1.12 { ! stoppedIn( X, Y, Z ), happens( skol1( X, Y, Z ), skol7( X, Y, Z ) ) }.
% 0.71/1.12 { ! stoppedIn( X, Y, Z ), alpha6( X, Y, Z, skol1( X, Y, Z ), skol7( X, Y, Z
% 0.71/1.12 ) ) }.
% 0.71/1.12 { ! happens( T, U ), ! alpha6( X, Y, Z, T, U ), stoppedIn( X, Y, Z ) }.
% 0.71/1.12 { ! alpha6( X, Y, Z, T, U ), less( X, U ) }.
% 0.71/1.12 { ! alpha6( X, Y, Z, T, U ), alpha1( Y, Z, T, U ) }.
% 0.71/1.12 { ! less( X, U ), ! alpha1( Y, Z, T, U ), alpha6( X, Y, Z, T, U ) }.
% 0.71/1.12 { ! alpha1( X, Y, Z, T ), less( T, Y ) }.
% 0.71/1.12 { ! alpha1( X, Y, Z, T ), terminates( Z, X, T ) }.
% 0.71/1.12 { ! less( T, Y ), ! terminates( Z, X, T ), alpha1( X, Y, Z, T ) }.
% 0.71/1.12 { ! startedIn( X, Z, Y ), happens( skol2( X, Y, Z ), skol8( X, Y, Z ) ) }.
% 0.71/1.12 { ! startedIn( X, Z, Y ), alpha7( X, Y, Z, skol2( X, Y, Z ), skol8( X, Y, Z
% 0.71/1.12 ) ) }.
% 0.71/1.12 { ! happens( T, U ), ! alpha7( X, Y, Z, T, U ), startedIn( X, Z, Y ) }.
% 0.71/1.12 { ! alpha7( X, Y, Z, T, U ), less( X, U ) }.
% 0.71/1.12 { ! alpha7( X, Y, Z, T, U ), alpha2( Y, Z, T, U ) }.
% 0.71/1.12 { ! less( X, U ), ! alpha2( Y, Z, T, U ), alpha7( X, Y, Z, T, U ) }.
% 0.71/1.12 { ! alpha2( X, Y, Z, T ), less( T, X ) }.
% 0.71/1.12 { ! alpha2( X, Y, Z, T ), initiates( Z, Y, T ) }.
% 0.71/1.12 { ! less( T, X ), ! initiates( Z, Y, T ), alpha2( X, Y, Z, T ) }.
% 0.71/1.12 { ! happens( T, X ), ! initiates( T, U, X ), ! less( n0, Z ), ! trajectory
% 0.71/1.12 ( U, X, Y, Z ), stoppedIn( X, U, plus( X, Z ) ), holdsAt( Y, plus( X, Z )
% 0.71/1.12 ) }.
% 0.71/1.12 { ! happens( T, X ), ! terminates( T, U, X ), ! less( n0, Y ), !
% 0.71/1.12 antitrajectory( U, X, Z, Y ), startedIn( X, U, plus( X, Y ) ), holdsAt( Z
% 0.71/1.12 , plus( X, Y ) ) }.
% 0.71/1.12 { ! holdsAt( X, Y ), releasedAt( X, plus( Y, n1 ) ), happens( skol3( Z, Y )
% 0.71/1.12 , Y ), holdsAt( X, plus( Y, n1 ) ) }.
% 0.71/1.12 { ! holdsAt( X, Y ), releasedAt( X, plus( Y, n1 ) ), terminates( skol3( X,
% 0.71/1.12 Y ), X, Y ), holdsAt( X, plus( Y, n1 ) ) }.
% 0.71/1.12 { holdsAt( X, Y ), releasedAt( X, plus( Y, n1 ) ), happens( skol4( Z, Y ),
% 0.71/1.12 Y ), ! holdsAt( X, plus( Y, n1 ) ) }.
% 0.71/1.12 { holdsAt( X, Y ), releasedAt( X, plus( Y, n1 ) ), initiates( skol4( X, Y )
% 0.71/1.12 , X, Y ), ! holdsAt( X, plus( Y, n1 ) ) }.
% 0.71/1.12 { ! releasedAt( X, Y ), happens( skol5( Z, Y ), Y ), releasedAt( X, plus( Y
% 0.71/1.12 , n1 ) ) }.
% 0.71/1.12 { ! releasedAt( X, Y ), initiates( skol5( X, Y ), X, Y ), terminates( skol5
% 0.71/1.12 ( X, Y ), X, Y ), releasedAt( X, plus( Y, n1 ) ) }.
% 0.71/1.12 { releasedAt( X, Y ), happens( skol6( Z, Y ), Y ), ! releasedAt( X, plus( Y
% 0.71/1.12 , n1 ) ) }.
% 0.71/1.12 { releasedAt( X, Y ), releases( skol6( X, Y ), X, Y ), ! releasedAt( X,
% 0.71/1.12 plus( Y, n1 ) ) }.
% 0.71/1.12 { ! happens( Z, X ), ! initiates( Z, Y, X ), holdsAt( Y, plus( X, n1 ) ) }
% 0.71/1.12 .
% 0.71/1.12 { ! happens( Z, X ), ! terminates( Z, Y, X ), ! holdsAt( Y, plus( X, n1 ) )
% 0.71/1.12 }.
% 0.71/1.12 { ! happens( Z, X ), ! releases( Z, Y, X ), releasedAt( Y, plus( X, n1 ) )
% 0.71/1.12 }.
% 0.71/1.12 { ! happens( Z, X ), ! initiates( Z, Y, X ), ! releasedAt( Y, plus( X, n1 )
% 0.71/1.12 ) }.
% 0.71/1.12 { ! happens( Z, X ), ! terminates( Z, Y, X ), ! releasedAt( Y, plus( X, n1
% 0.71/1.12 ) ) }.
% 0.71/1.12 { ! initiates( X, Y, Z ), alpha14( X, Y, Z ), alpha17( X, Y, Z ) }.
% 0.71/1.12 { ! alpha14( X, Y, Z ), initiates( X, Y, Z ) }.
% 0.71/1.12 { ! alpha17( X, Y, Z ), initiates( X, Y, Z ) }.
% 0.71/1.12 { ! alpha17( X, Y, Z ), alpha20( X, Y, Z ), alpha23( X, Y, Z ) }.
% 0.71/1.12 { ! alpha20( X, Y, Z ), alpha17( X, Y, Z ) }.
% 0.71/1.12 { ! alpha23( X, Y, Z ), alpha17( X, Y, Z ) }.
% 0.71/1.12 { ! alpha23( X, Y, Z ), X = pull }.
% 0.71/1.12 { ! alpha23( X, Y, Z ), alpha11( Y, Z ) }.
% 0.71/1.12 { ! X = pull, ! alpha11( Y, Z ), alpha23( X, Y, Z ) }.
% 0.71/1.12 { ! alpha20( X, Y, Z ), X = pull }.
% 0.71/1.12 { ! alpha20( X, Y, Z ), alpha8( Y, Z ) }.
% 0.71/1.12 { ! X = pull, ! alpha8( Y, Z ), alpha20( X, Y, Z ) }.
% 0.71/1.12 { ! alpha14( X, Y, Z ), X = push }.
% 0.71/1.12 { ! alpha14( X, Y, Z ), alpha3( Y, Z ) }.
% 0.71/1.12 { ! X = push, ! alpha3( Y, Z ), alpha14( X, Y, Z ) }.
% 0.71/1.12 { ! alpha11( X, Y ), X = spinning }.
% 0.71/1.12 { ! alpha11( X, Y ), happens( push, Y ) }.
% 0.71/1.12 { ! X = spinning, ! happens( push, Y ), alpha11( X, Y ) }.
% 0.71/1.12 { ! alpha8( X, Y ), X = backwards }.
% 0.71/1.12 { ! alpha8( X, Y ), ! happens( push, Y ) }.
% 0.71/1.12 { ! X = backwards, happens( push, Y ), alpha8( X, Y ) }.
% 0.71/1.12 { ! alpha3( X, Y ), X = forwards }.
% 0.71/1.12 { ! alpha3( X, Y ), ! happens( pull, Y ) }.
% 0.71/1.12 { ! X = forwards, happens( pull, Y ), alpha3( X, Y ) }.
% 0.71/1.12 { ! terminates( X, Y, Z ), alpha24( X, Y, Z ), alpha25( X, Y, Z ) }.
% 0.71/1.12 { ! alpha24( X, Y, Z ), terminates( X, Y, Z ) }.
% 0.71/1.12 { ! alpha25( X, Y, Z ), terminates( X, Y, Z ) }.
% 0.71/1.12 { ! alpha25( X, Y, Z ), alpha26( X, Y, Z ), alpha27( X, Y, Z ) }.
% 0.71/1.12 { ! alpha26( X, Y, Z ), alpha25( X, Y, Z ) }.
% 0.71/1.12 { ! alpha27( X, Y, Z ), alpha25( X, Y, Z ) }.
% 0.71/1.12 { ! alpha27( X, Y, Z ), alpha28( X, Y, Z ), alpha29( X, Y, Z ) }.
% 0.71/1.12 { ! alpha28( X, Y, Z ), alpha27( X, Y, Z ) }.
% 0.71/1.12 { ! alpha29( X, Y, Z ), alpha27( X, Y, Z ) }.
% 0.71/1.12 { ! alpha29( X, Y, Z ), alpha30( X, Y, Z ), alpha31( X, Y, Z ) }.
% 0.71/1.12 { ! alpha30( X, Y, Z ), alpha29( X, Y, Z ) }.
% 0.71/1.12 { ! alpha31( X, Y, Z ), alpha29( X, Y, Z ) }.
% 0.71/1.12 { ! alpha31( X, Y, Z ), alpha32( X, Y, Z ), alpha33( X, Y, Z ) }.
% 0.71/1.12 { ! alpha32( X, Y, Z ), alpha31( X, Y, Z ) }.
% 0.71/1.12 { ! alpha33( X, Y, Z ), alpha31( X, Y, Z ) }.
% 0.71/1.12 { ! alpha33( X, Y, Z ), X = pull }.
% 0.71/1.12 { ! alpha33( X, Y, Z ), alpha21( Y, Z ) }.
% 0.71/1.12 { ! X = pull, ! alpha21( Y, Z ), alpha33( X, Y, Z ) }.
% 0.71/1.12 { ! alpha32( X, Y, Z ), X = push }.
% 0.71/1.12 { ! alpha32( X, Y, Z ), alpha18( Y, Z ) }.
% 0.71/1.12 { ! X = push, ! alpha18( Y, Z ), alpha32( X, Y, Z ) }.
% 0.71/1.12 { ! alpha30( X, Y, Z ), X = pull }.
% 0.71/1.12 { ! alpha30( X, Y, Z ), alpha15( Y, Z ) }.
% 0.71/1.12 { ! X = pull, ! alpha15( Y, Z ), alpha30( X, Y, Z ) }.
% 0.71/1.12 { ! alpha28( X, Y, Z ), X = pull }.
% 0.71/1.12 { ! alpha28( X, Y, Z ), alpha12( Y, Z ) }.
% 0.71/1.12 { ! X = pull, ! alpha12( Y, Z ), alpha28( X, Y, Z ) }.
% 0.71/1.12 { ! alpha26( X, Y, Z ), X = pull }.
% 0.71/1.12 { ! alpha26( X, Y, Z ), alpha9( Y, Z ) }.
% 0.71/1.12 { ! X = pull, ! alpha9( Y, Z ), alpha26( X, Y, Z ) }.
% 0.71/1.12 { ! alpha24( X, Y, Z ), X = push }.
% 0.71/1.12 { ! alpha24( X, Y, Z ), alpha4( Y, Z ) }.
% 0.71/1.12 { ! X = push, ! alpha4( Y, Z ), alpha24( X, Y, Z ) }.
% 0.71/1.12 { ! alpha21( X, Y ), X = spinning }.
% 0.71/1.12 { ! alpha21( X, Y ), ! happens( push, Y ) }.
% 0.71/1.12 { ! X = spinning, happens( push, Y ), alpha21( X, Y ) }.
% 0.71/1.12 { ! alpha18( X, Y ), X = spinning }.
% 0.71/1.12 { ! alpha18( X, Y ), ! happens( pull, Y ) }.
% 0.71/1.12 { ! X = spinning, happens( pull, Y ), alpha18( X, Y ) }.
% 0.71/1.12 { ! alpha15( X, Y ), X = backwards }.
% 0.71/1.12 { ! alpha15( X, Y ), happens( push, Y ) }.
% 0.71/1.12 { ! X = backwards, ! happens( push, Y ), alpha15( X, Y ) }.
% 0.71/1.12 { ! alpha12( X, Y ), X = forwards }.
% 0.71/1.12 { ! alpha12( X, Y ), happens( push, Y ) }.
% 0.71/1.12 { ! X = forwards, ! happens( push, Y ), alpha12( X, Y ) }.
% 0.71/1.12 { ! alpha9( X, Y ), X = forwards }.
% 0.71/1.12 { ! alpha9( X, Y ), ! happens( push, Y ) }.
% 0.71/1.12 { ! X = forwards, happens( push, Y ), alpha9( X, Y ) }.
% 0.71/1.12 { ! alpha4( X, Y ), X = backwards }.
% 0.71/1.12 { ! alpha4( X, Y ), ! happens( pull, Y ) }.
% 0.71/1.12 { ! X = backwards, happens( pull, Y ), alpha4( X, Y ) }.
% 0.71/1.12 { ! releases( X, Y, Z ) }.
% 0.71/1.12 { ! happens( X, Y ), alpha5( X, Y ), alpha10( X, Y ) }.
% 0.71/1.12 { ! alpha5( X, Y ), happens( X, Y ) }.
% 0.71/1.12 { ! alpha10( X, Y ), happens( X, Y ) }.
% 0.71/1.12 { ! alpha10( X, Y ), alpha13( X, Y ), alpha16( X, Y ) }.
% 0.71/1.12 { ! alpha13( X, Y ), alpha10( X, Y ) }.
% 0.71/1.12 { ! alpha16( X, Y ), alpha10( X, Y ) }.
% 0.71/1.12 { ! alpha16( X, Y ), alpha19( X, Y ), alpha22( X, Y ) }.
% 0.71/1.12 { ! alpha19( X, Y ), alpha16( X, Y ) }.
% 0.71/1.12 { ! alpha22( X, Y ), alpha16( X, Y ) }.
% 0.71/1.12 { ! alpha22( X, Y ), X = push }.
% 0.71/1.12 { ! alpha22( X, Y ), Y = n2 }.
% 0.71/1.12 { ! X = push, ! Y = n2, alpha22( X, Y ) }.
% 0.71/1.12 { ! alpha19( X, Y ), X = pull }.
% 0.71/1.12 { ! alpha19( X, Y ), Y = n2 }.
% 0.71/1.12 { ! X = pull, ! Y = n2, alpha19( X, Y ) }.
% 0.71/1.12 { ! alpha13( X, Y ), X = pull }.
% 0.71/1.12 { ! alpha13( X, Y ), Y = n1 }.
% 0.71/1.12 { ! X = pull, ! Y = n1, alpha13( X, Y ) }.
% 0.71/1.12 { ! alpha5( X, Y ), X = push }.
% 0.71/1.12 { ! alpha5( X, Y ), Y = n0 }.
% 0.71/1.12 { ! X = push, ! Y = n0, alpha5( X, Y ) }.
% 0.71/1.12 { ! push = pull }.
% 0.71/1.12 { ! forwards = backwards }.
% 0.71/1.12 { ! forwards = spinning }.
% 0.71/1.12 { ! spinning = backwards }.
% 0.71/1.12 { plus( n0, n0 ) = n0 }.
% 0.71/1.12 { plus( n0, n1 ) = n1 }.
% 0.71/1.12 { plus( n0, n2 ) = n2 }.
% 0.71/1.12 { plus( n0, n3 ) = n3 }.
% 0.71/1.12 { plus( n1, n1 ) = n2 }.
% 0.71/1.12 { plus( n1, n2 ) = n3 }.
% 0.71/1.12 { plus( n1, n3 ) = n4 }.
% 0.71/1.12 { plus( n2, n2 ) = n4 }.
% 0.71/1.12 { plus( n2, n3 ) = n5 }.
% 0.71/1.12 { plus( n3, n3 ) = n6 }.
% 0.71/1.12 { plus( X, Y ) = plus( Y, X ) }.
% 0.71/1.12 { ! less_or_equal( X, Y ), less( X, Y ), X = Y }.
% 0.71/1.12 { ! less( X, Y ), less_or_equal( X, Y ) }.
% 0.71/1.12 { ! X = Y, less_or_equal( X, Y ) }.
% 0.71/1.12 { ! less( X, n0 ) }.
% 0.71/1.12 { ! less( X, n1 ), less_or_equal( X, n0 ) }.
% 0.71/1.12 { ! less_or_equal( X, n0 ), less( X, n1 ) }.
% 0.71/1.12 { ! less( X, n2 ), less_or_equal( X, n1 ) }.
% 0.71/1.12 { ! less_or_equal( X, n1 ), less( X, n2 ) }.
% 0.71/1.12 { ! less( X, n3 ), less_or_equal( X, n2 ) }.
% 0.71/1.12 { ! less_or_equal( X, n2 ), less( X, n3 ) }.
% 0.71/1.12 { ! less( X, n4 ), less_or_equal( X, n3 ) }.
% 0.76/1.28 { ! less_or_equal( X, n3 ), less( X, n4 ) }.
% 0.76/1.28 { ! less( X, n5 ), less_or_equal( X, n4 ) }.
% 0.76/1.28 { ! less_or_equal( X, n4 ), less( X, n5 ) }.
% 0.76/1.28 { ! less( X, n6 ), less_or_equal( X, n5 ) }.
% 0.76/1.28 { ! less_or_equal( X, n5 ), less( X, n6 ) }.
% 0.76/1.28 { ! less( X, n7 ), less_or_equal( X, n6 ) }.
% 0.76/1.28 { ! less_or_equal( X, n6 ), less( X, n7 ) }.
% 0.76/1.28 { ! less( X, n8 ), less_or_equal( X, n7 ) }.
% 0.76/1.28 { ! less_or_equal( X, n7 ), less( X, n8 ) }.
% 0.76/1.28 { ! less( X, n9 ), less_or_equal( X, n8 ) }.
% 0.76/1.28 { ! less_or_equal( X, n8 ), less( X, n9 ) }.
% 0.76/1.28 { ! less( X, Y ), ! less( Y, X ) }.
% 0.76/1.28 { ! less( X, Y ), ! Y = X }.
% 0.76/1.28 { less( Y, X ), Y = X, less( X, Y ) }.
% 0.76/1.28 { ! holdsAt( forwards, n0 ) }.
% 0.76/1.28 { ! holdsAt( backwards, n0 ) }.
% 0.76/1.28 { ! holdsAt( spinning, n0 ) }.
% 0.76/1.28 { ! releasedAt( X, Y ) }.
% 0.76/1.28 { holdsAt( backwards, n3 ) }.
% 0.76/1.28
% 0.76/1.28 percentage equality = 0.180203, percentage horn = 0.840000
% 0.76/1.28 This is a problem with some equality
% 0.76/1.28
% 0.76/1.28
% 0.76/1.28
% 0.76/1.28 Options Used:
% 0.76/1.28
% 0.76/1.28 useres = 1
% 0.76/1.28 useparamod = 1
% 0.76/1.28 useeqrefl = 1
% 0.76/1.28 useeqfact = 1
% 0.76/1.28 usefactor = 1
% 0.76/1.28 usesimpsplitting = 0
% 0.76/1.28 usesimpdemod = 5
% 0.76/1.28 usesimpres = 3
% 0.76/1.28
% 0.76/1.28 resimpinuse = 1000
% 0.76/1.28 resimpclauses = 20000
% 0.76/1.28 substype = eqrewr
% 0.76/1.28 backwardsubs = 1
% 0.76/1.28 selectoldest = 5
% 0.76/1.28
% 0.76/1.28 litorderings [0] = split
% 0.76/1.28 litorderings [1] = extend the termordering, first sorting on arguments
% 0.76/1.28
% 0.76/1.28 termordering = kbo
% 0.76/1.28
% 0.76/1.28 litapriori = 0
% 0.76/1.28 termapriori = 1
% 0.76/1.28 litaposteriori = 0
% 0.76/1.28 termaposteriori = 0
% 0.76/1.28 demodaposteriori = 0
% 0.76/1.28 ordereqreflfact = 0
% 0.76/1.28
% 0.76/1.28 litselect = negord
% 0.76/1.28
% 0.76/1.28 maxweight = 15
% 0.76/1.28 maxdepth = 30000
% 0.76/1.28 maxlength = 115
% 0.76/1.28 maxnrvars = 195
% 0.76/1.28 excuselevel = 1
% 0.76/1.28 increasemaxweight = 1
% 0.76/1.28
% 0.76/1.28 maxselected = 10000000
% 0.76/1.28 maxnrclauses = 10000000
% 0.76/1.28
% 0.76/1.28 showgenerated = 0
% 0.76/1.28 showkept = 0
% 0.76/1.28 showselected = 0
% 0.76/1.28 showdeleted = 0
% 0.76/1.28 showresimp = 1
% 0.76/1.28 showstatus = 2000
% 0.76/1.28
% 0.76/1.28 prologoutput = 0
% 0.76/1.28 nrgoals = 5000000
% 0.76/1.28 totalproof = 1
% 0.76/1.28
% 0.76/1.28 Symbols occurring in the translation:
% 0.76/1.28
% 0.76/1.28 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.76/1.28 . [1, 2] (w:1, o:36, a:1, s:1, b:0),
% 0.76/1.28 ! [4, 1] (w:0, o:31, a:1, s:1, b:0),
% 0.76/1.28 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.76/1.28 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.76/1.28 stoppedIn [38, 3] (w:1, o:86, a:1, s:1, b:0),
% 0.76/1.28 happens [41, 2] (w:1, o:60, a:1, s:1, b:0),
% 0.76/1.28 less [42, 2] (w:1, o:61, a:1, s:1, b:0),
% 0.76/1.28 terminates [43, 3] (w:1, o:92, a:1, s:1, b:0),
% 0.76/1.28 startedIn [44, 3] (w:1, o:87, a:1, s:1, b:0),
% 0.76/1.28 initiates [45, 3] (w:1, o:93, a:1, s:1, b:0),
% 0.76/1.28 n0 [48, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.76/1.28 trajectory [49, 4] (w:1, o:108, a:1, s:1, b:0),
% 0.76/1.28 plus [50, 2] (w:1, o:62, a:1, s:1, b:0),
% 0.76/1.28 holdsAt [51, 2] (w:1, o:63, a:1, s:1, b:0),
% 0.76/1.28 antitrajectory [53, 4] (w:1, o:109, a:1, s:1, b:0),
% 0.76/1.28 n1 [54, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.76/1.28 releasedAt [55, 2] (w:1, o:64, a:1, s:1, b:0),
% 0.76/1.28 releases [56, 3] (w:1, o:85, a:1, s:1, b:0),
% 0.76/1.28 push [57, 0] (w:1, o:16, a:1, s:1, b:0),
% 0.76/1.28 forwards [58, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.76/1.28 pull [59, 0] (w:1, o:18, a:1, s:1, b:0),
% 0.76/1.28 backwards [60, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.76/1.28 spinning [61, 0] (w:1, o:20, a:1, s:1, b:0),
% 0.76/1.28 n2 [62, 0] (w:1, o:21, a:1, s:1, b:0),
% 0.76/1.28 n3 [63, 0] (w:1, o:22, a:1, s:1, b:0),
% 0.76/1.28 n4 [64, 0] (w:1, o:23, a:1, s:1, b:0),
% 0.76/1.28 n5 [65, 0] (w:1, o:24, a:1, s:1, b:0),
% 0.76/1.28 n6 [66, 0] (w:1, o:25, a:1, s:1, b:0),
% 0.76/1.28 less_or_equal [69, 2] (w:1, o:65, a:1, s:1, b:0),
% 0.76/1.28 n7 [70, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.76/1.28 n8 [71, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.76/1.28 n9 [72, 0] (w:1, o:30, a:1, s:1, b:0),
% 0.76/1.28 alpha1 [73, 4] (w:1, o:110, a:1, s:1, b:1),
% 0.76/1.28 alpha2 [74, 4] (w:1, o:111, a:1, s:1, b:1),
% 0.76/1.28 alpha3 [75, 2] (w:1, o:68, a:1, s:1, b:1),
% 0.76/1.28 alpha4 [76, 2] (w:1, o:69, a:1, s:1, b:1),
% 0.76/1.28 alpha5 [77, 2] (w:1, o:70, a:1, s:1, b:1),
% 0.76/1.28 alpha6 [78, 5] (w:1, o:112, a:1, s:1, b:1),
% 0.76/1.28 alpha7 [79, 5] (w:1, o:113, a:1, s:1, b:1),
% 0.76/1.28 alpha8 [80, 2] (w:1, o:71, a:1, s:1, b:1),
% 0.76/1.28 alpha9 [81, 2] (w:1, o:72, a:1, s:1, b:1),
% 0.76/1.28 alpha10 [82, 2] (w:1, o:73, a:1, s:1, b:1),
% 0.76/1.28 alpha11 [83, 2] (w:1, o:74, a:1, s:1, b:1),
% 0.76/1.28 alpha12 [84, 2] (w:1, o:75, a:1, s:1, b:1),
% 0.76/1.28 alpha13 [85, 2] (w:1, o:76, a:1, s:1, b:1),
% 0.76/1.28 alpha14 [86, 3] (w:1, o:94, a:1, s:1, b:1),
% 0.76/1.28 alpha15 [87, 2] (w:1, o:77, a:1, s:1, b:1),
% 0.76/1.28 alpha16 [88, 2] (w:1, o:78, a:1, s:1, b:1),
% 0.76/1.28 alpha17 [89, 3] (w:1, o:95, a:1, s:1, b:1),
% 0.76/1.28 alpha18 [90, 2] (w:1, o:79, a:1, s:1, b:1),
% 0.76/1.28 alpha19 [91, 2] (w:1, o:80, a:1, s:1, b:1),
% 0.76/1.28 alpha20 [92, 3] (w:1, o:96, a:1, s:1, b:1),
% 0.76/1.28 alpha21 [93, 2] (w:1, o:66, a:1, s:1, b:1),
% 0.76/1.28 alpha22 [94, 2] (w:1, o:67, a:1, s:1, b:1),
% 0.76/1.28 alpha23 [95, 3] (w:1, o:97, a:1, s:1, b:1),
% 0.76/1.28 alpha24 [96, 3] (w:1, o:98, a:1, s:1, b:1),
% 0.76/1.28 alpha25 [97, 3] (w:1, o:99, a:1, s:1, b:1),
% 0.76/1.28 alpha26 [98, 3] (w:1, o:100, a:1, s:1, b:1),
% 0.76/1.28 alpha27 [99, 3] (w:1, o:101, a:1, s:1, b:1),
% 0.76/1.28 alpha28 [100, 3] (w:1, o:102, a:1, s:1, b:1),
% 0.76/1.28 alpha29 [101, 3] (w:1, o:103, a:1, s:1, b:1),
% 0.76/1.28 alpha30 [102, 3] (w:1, o:104, a:1, s:1, b:1),
% 0.76/1.28 alpha31 [103, 3] (w:1, o:105, a:1, s:1, b:1),
% 0.76/1.28 alpha32 [104, 3] (w:1, o:106, a:1, s:1, b:1),
% 0.76/1.28 alpha33 [105, 3] (w:1, o:107, a:1, s:1, b:1),
% 0.76/1.28 skol1 [106, 3] (w:1, o:88, a:1, s:1, b:1),
% 0.76/1.28 skol2 [107, 3] (w:1, o:89, a:1, s:1, b:1),
% 0.76/1.28 skol3 [108, 2] (w:1, o:81, a:1, s:1, b:1),
% 0.76/1.28 skol4 [109, 2] (w:1, o:82, a:1, s:1, b:1),
% 0.76/1.28 skol5 [110, 2] (w:1, o:83, a:1, s:1, b:1),
% 0.76/1.28 skol6 [111, 2] (w:1, o:84, a:1, s:1, b:1),
% 0.76/1.28 skol7 [112, 3] (w:1, o:90, a:1, s:1, b:1),
% 0.76/1.28 skol8 [113, 3] (w:1, o:91, a:1, s:1, b:1).
% 0.76/1.28
% 0.76/1.28
% 0.76/1.28 Starting Search:
% 0.76/1.28
% 0.76/1.28 *** allocated 15000 integers for clauses
% 0.76/1.28 *** allocated 22500 integers for clauses
% 0.76/1.28 *** allocated 33750 integers for clauses
% 0.76/1.28 *** allocated 15000 integers for termspace/termends
% 0.76/1.28 *** allocated 50625 integers for clauses
% 0.76/1.28 Resimplifying inuse:
% 0.76/1.28 Done
% 0.76/1.28
% 0.76/1.28 *** allocated 22500 integers for termspace/termends
% 0.76/1.28 *** allocated 75937 integers for clauses
% 0.76/1.28 *** allocated 33750 integers for termspace/termends
% 0.76/1.28 *** allocated 113905 integers for clauses
% 0.76/1.28
% 0.76/1.28 Intermediate Status:
% 0.76/1.28 Generated: 2962
% 0.76/1.28 Kept: 2049
% 0.76/1.28 Inuse: 210
% 0.76/1.28 Deleted: 23
% 0.76/1.28 Deletedinuse: 0
% 0.76/1.28
% 0.76/1.28 Resimplifying inuse:
% 0.76/1.28 Done
% 0.76/1.28
% 0.76/1.28 *** allocated 50625 integers for termspace/termends
% 0.76/1.28 *** allocated 170857 integers for clauses
% 0.76/1.28 Resimplifying inuse:
% 0.76/1.28 Done
% 0.76/1.28
% 0.76/1.28
% 0.76/1.28 Intermediate Status:
% 0.76/1.28 Generated: 5894
% 0.76/1.28 Kept: 4081
% 0.76/1.28 Inuse: 362
% 0.76/1.28 Deleted: 34
% 0.76/1.28 Deletedinuse: 0
% 0.76/1.28
% 0.76/1.28 Resimplifying inuse:
% 0.76/1.28 Done
% 0.76/1.28
% 0.76/1.28 *** allocated 75937 integers for termspace/termends
% 0.76/1.28 *** allocated 256285 integers for clauses
% 0.76/1.28 Resimplifying inuse:
% 0.76/1.28 Done
% 0.76/1.28
% 0.76/1.28
% 0.76/1.28 Intermediate Status:
% 0.76/1.28 Generated: 8665
% 0.76/1.28 Kept: 6122
% 0.76/1.28 Inuse: 437
% 0.76/1.28 Deleted: 34
% 0.76/1.28 Deletedinuse: 0
% 0.76/1.28
% 0.76/1.28 Resimplifying inuse:
% 0.76/1.28 Done
% 0.76/1.28
% 0.76/1.28 *** allocated 113905 integers for termspace/termends
% 0.76/1.28 *** allocated 384427 integers for clauses
% 0.76/1.28 Resimplifying inuse:
% 0.76/1.28 Done
% 0.76/1.28
% 0.76/1.28
% 0.76/1.28 Intermediate Status:
% 0.76/1.28 Generated: 11751
% 0.76/1.28 Kept: 8206
% 0.76/1.28 Inuse: 497
% 0.76/1.28 Deleted: 34
% 0.76/1.28 Deletedinuse: 0
% 0.76/1.28
% 0.76/1.28 Resimplifying inuse:
% 0.76/1.28 Done
% 0.76/1.28
% 0.76/1.28
% 0.76/1.28 Bliksems!, er is een bewijs:
% 0.76/1.28 % SZS status Theorem
% 0.76/1.28 % SZS output start Refutation
% 0.76/1.28
% 0.76/1.28 (29) {G0,W12,D3,L3,V3,M3} I { ! happens( Z, X ), ! terminates( Z, Y, X ), !
% 0.76/1.28 holdsAt( Y, plus( X, n1 ) ) }.
% 0.76/1.28 (59) {G0,W8,D2,L2,V3,M2} I { ! alpha25( X, Y, Z ), terminates( X, Y, Z )
% 0.76/1.28 }.
% 0.76/1.28 (62) {G0,W8,D2,L2,V3,M2} I { ! alpha27( X, Y, Z ), alpha25( X, Y, Z ) }.
% 0.76/1.28 (65) {G0,W8,D2,L2,V3,M2} I { ! alpha29( X, Y, Z ), alpha27( X, Y, Z ) }.
% 0.76/1.28 (67) {G0,W8,D2,L2,V3,M2} I { ! alpha30( X, Y, Z ), alpha29( X, Y, Z ) }.
% 0.76/1.28 (80) {G0,W10,D2,L3,V3,M3} I { ! X = pull, ! alpha15( Y, Z ), alpha30( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 (98) {G0,W9,D2,L3,V2,M3} I { ! X = backwards, ! happens( push, Y ), alpha15
% 0.76/1.28 ( X, Y ) }.
% 0.76/1.28 (111) {G0,W6,D2,L2,V2,M2} I { ! alpha10( X, Y ), happens( X, Y ) }.
% 0.76/1.28 (114) {G0,W6,D2,L2,V2,M2} I { ! alpha16( X, Y ), alpha10( X, Y ) }.
% 0.76/1.28 (116) {G0,W6,D2,L2,V2,M2} I { ! alpha19( X, Y ), alpha16( X, Y ) }.
% 0.76/1.28 (117) {G0,W6,D2,L2,V2,M2} I { ! alpha22( X, Y ), alpha16( X, Y ) }.
% 0.76/1.28 (120) {G0,W9,D2,L3,V2,M3} I { ! X = push, ! Y = n2, alpha22( X, Y ) }.
% 0.76/1.28 (123) {G0,W9,D2,L3,V2,M3} I { ! X = pull, ! Y = n2, alpha19( X, Y ) }.
% 0.76/1.28 (139) {G0,W5,D3,L1,V0,M1} I { plus( n1, n2 ) ==> n3 }.
% 0.76/1.28 (144) {G0,W7,D3,L1,V2,M1} I { plus( X, Y ) = plus( Y, X ) }.
% 0.76/1.28 (174) {G0,W3,D2,L1,V0,M1} I { holdsAt( backwards, n3 ) }.
% 0.76/1.28 (194) {G1,W6,D2,L2,V1,M2} Q(120) { ! X = push, alpha22( X, n2 ) }.
% 0.76/1.28 (195) {G2,W3,D2,L1,V0,M1} Q(194) { alpha22( push, n2 ) }.
% 0.76/1.28 (197) {G1,W6,D2,L2,V1,M2} Q(123) { ! X = pull, alpha19( X, n2 ) }.
% 0.76/1.28 (198) {G2,W3,D2,L1,V0,M1} Q(197) { alpha19( pull, n2 ) }.
% 0.76/1.28 (991) {G3,W3,D2,L1,V0,M1} R(117,195) { alpha16( push, n2 ) }.
% 0.76/1.28 (992) {G3,W3,D2,L1,V0,M1} R(116,198) { alpha16( pull, n2 ) }.
% 0.76/1.28 (993) {G4,W3,D2,L1,V0,M1} R(114,992) { alpha10( pull, n2 ) }.
% 0.76/1.28 (995) {G4,W3,D2,L1,V0,M1} R(114,991) { alpha10( push, n2 ) }.
% 0.76/1.28 (1002) {G5,W3,D2,L1,V0,M1} R(111,995) { happens( push, n2 ) }.
% 0.76/1.28 (1003) {G5,W3,D2,L1,V0,M1} R(111,993) { happens( pull, n2 ) }.
% 0.76/1.28 (6301) {G6,W6,D2,L2,V1,M2} R(98,1002) { ! X = backwards, alpha15( X, n2 )
% 0.76/1.28 }.
% 0.76/1.28 (6377) {G7,W3,D2,L1,V0,M1} Q(6301) { alpha15( backwards, n2 ) }.
% 0.76/1.28 (6398) {G8,W7,D2,L2,V1,M2} R(6377,80) { ! X = pull, alpha30( X, backwards,
% 0.76/1.28 n2 ) }.
% 0.76/1.28 (6399) {G9,W4,D2,L1,V0,M1} Q(6398) { alpha30( pull, backwards, n2 ) }.
% 0.76/1.28 (6400) {G10,W4,D2,L1,V0,M1} R(6399,67) { alpha29( pull, backwards, n2 ) }.
% 0.76/1.28 (6401) {G11,W4,D2,L1,V0,M1} R(6400,65) { alpha27( pull, backwards, n2 ) }.
% 0.76/1.28 (6891) {G12,W4,D2,L1,V0,M1} R(6401,62) { alpha25( pull, backwards, n2 ) }.
% 0.76/1.28 (6892) {G13,W4,D2,L1,V0,M1} R(6891,59) { terminates( pull, backwards, n2 )
% 0.76/1.28 }.
% 0.76/1.28 (6956) {G14,W5,D3,L1,V0,M1} R(6892,29);r(1003) { ! holdsAt( backwards, plus
% 0.76/1.28 ( n2, n1 ) ) }.
% 0.76/1.28 (8627) {G15,W0,D0,L0,V0,M0} P(144,6956);d(139);r(174) { }.
% 0.76/1.28
% 0.76/1.28
% 0.76/1.28 % SZS output end Refutation
% 0.76/1.28 found a proof!
% 0.76/1.28
% 0.76/1.28
% 0.76/1.28 Unprocessed initial clauses:
% 0.76/1.28
% 0.76/1.28 (8629) {G0,W13,D3,L2,V3,M2} { ! stoppedIn( X, Y, Z ), happens( skol1( X, Y
% 0.76/1.28 , Z ), skol7( X, Y, Z ) ) }.
% 0.76/1.28 (8630) {G0,W16,D3,L2,V3,M2} { ! stoppedIn( X, Y, Z ), alpha6( X, Y, Z,
% 0.76/1.28 skol1( X, Y, Z ), skol7( X, Y, Z ) ) }.
% 0.76/1.28 (8631) {G0,W13,D2,L3,V5,M3} { ! happens( T, U ), ! alpha6( X, Y, Z, T, U )
% 0.76/1.28 , stoppedIn( X, Y, Z ) }.
% 0.76/1.28 (8632) {G0,W9,D2,L2,V5,M2} { ! alpha6( X, Y, Z, T, U ), less( X, U ) }.
% 0.76/1.28 (8633) {G0,W11,D2,L2,V5,M2} { ! alpha6( X, Y, Z, T, U ), alpha1( Y, Z, T,
% 0.76/1.28 U ) }.
% 0.76/1.28 (8634) {G0,W14,D2,L3,V5,M3} { ! less( X, U ), ! alpha1( Y, Z, T, U ),
% 0.76/1.28 alpha6( X, Y, Z, T, U ) }.
% 0.76/1.28 (8635) {G0,W8,D2,L2,V4,M2} { ! alpha1( X, Y, Z, T ), less( T, Y ) }.
% 0.76/1.28 (8636) {G0,W9,D2,L2,V4,M2} { ! alpha1( X, Y, Z, T ), terminates( Z, X, T )
% 0.76/1.28 }.
% 0.76/1.28 (8637) {G0,W12,D2,L3,V4,M3} { ! less( T, Y ), ! terminates( Z, X, T ),
% 0.76/1.28 alpha1( X, Y, Z, T ) }.
% 0.76/1.28 (8638) {G0,W13,D3,L2,V3,M2} { ! startedIn( X, Z, Y ), happens( skol2( X, Y
% 0.76/1.28 , Z ), skol8( X, Y, Z ) ) }.
% 0.76/1.28 (8639) {G0,W16,D3,L2,V3,M2} { ! startedIn( X, Z, Y ), alpha7( X, Y, Z,
% 0.76/1.28 skol2( X, Y, Z ), skol8( X, Y, Z ) ) }.
% 0.76/1.28 (8640) {G0,W13,D2,L3,V5,M3} { ! happens( T, U ), ! alpha7( X, Y, Z, T, U )
% 0.76/1.28 , startedIn( X, Z, Y ) }.
% 0.76/1.28 (8641) {G0,W9,D2,L2,V5,M2} { ! alpha7( X, Y, Z, T, U ), less( X, U ) }.
% 0.76/1.28 (8642) {G0,W11,D2,L2,V5,M2} { ! alpha7( X, Y, Z, T, U ), alpha2( Y, Z, T,
% 0.76/1.28 U ) }.
% 0.76/1.28 (8643) {G0,W14,D2,L3,V5,M3} { ! less( X, U ), ! alpha2( Y, Z, T, U ),
% 0.76/1.28 alpha7( X, Y, Z, T, U ) }.
% 0.76/1.28 (8644) {G0,W8,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), less( T, X ) }.
% 0.76/1.28 (8645) {G0,W9,D2,L2,V4,M2} { ! alpha2( X, Y, Z, T ), initiates( Z, Y, T )
% 0.76/1.28 }.
% 0.76/1.28 (8646) {G0,W12,D2,L3,V4,M3} { ! less( T, X ), ! initiates( Z, Y, T ),
% 0.76/1.28 alpha2( X, Y, Z, T ) }.
% 0.76/1.28 (8647) {G0,W26,D3,L6,V5,M6} { ! happens( T, X ), ! initiates( T, U, X ), !
% 0.76/1.28 less( n0, Z ), ! trajectory( U, X, Y, Z ), stoppedIn( X, U, plus( X, Z )
% 0.76/1.28 ), holdsAt( Y, plus( X, Z ) ) }.
% 0.76/1.28 (8648) {G0,W26,D3,L6,V5,M6} { ! happens( T, X ), ! terminates( T, U, X ),
% 0.76/1.28 ! less( n0, Y ), ! antitrajectory( U, X, Z, Y ), startedIn( X, U, plus( X
% 0.76/1.28 , Y ) ), holdsAt( Z, plus( X, Y ) ) }.
% 0.76/1.28 (8649) {G0,W18,D3,L4,V3,M4} { ! holdsAt( X, Y ), releasedAt( X, plus( Y,
% 0.76/1.28 n1 ) ), happens( skol3( Z, Y ), Y ), holdsAt( X, plus( Y, n1 ) ) }.
% 0.76/1.28 (8650) {G0,W19,D3,L4,V2,M4} { ! holdsAt( X, Y ), releasedAt( X, plus( Y,
% 0.76/1.28 n1 ) ), terminates( skol3( X, Y ), X, Y ), holdsAt( X, plus( Y, n1 ) )
% 0.76/1.28 }.
% 0.76/1.28 (8651) {G0,W18,D3,L4,V3,M4} { holdsAt( X, Y ), releasedAt( X, plus( Y, n1
% 0.76/1.28 ) ), happens( skol4( Z, Y ), Y ), ! holdsAt( X, plus( Y, n1 ) ) }.
% 0.76/1.28 (8652) {G0,W19,D3,L4,V2,M4} { holdsAt( X, Y ), releasedAt( X, plus( Y, n1
% 0.76/1.28 ) ), initiates( skol4( X, Y ), X, Y ), ! holdsAt( X, plus( Y, n1 ) ) }.
% 0.76/1.28 (8653) {G0,W13,D3,L3,V3,M3} { ! releasedAt( X, Y ), happens( skol5( Z, Y )
% 0.76/1.28 , Y ), releasedAt( X, plus( Y, n1 ) ) }.
% 0.76/1.28 (8654) {G0,W20,D3,L4,V2,M4} { ! releasedAt( X, Y ), initiates( skol5( X, Y
% 0.76/1.28 ), X, Y ), terminates( skol5( X, Y ), X, Y ), releasedAt( X, plus( Y, n1
% 0.76/1.28 ) ) }.
% 0.76/1.28 (8655) {G0,W13,D3,L3,V3,M3} { releasedAt( X, Y ), happens( skol6( Z, Y ),
% 0.76/1.28 Y ), ! releasedAt( X, plus( Y, n1 ) ) }.
% 0.76/1.28 (8656) {G0,W14,D3,L3,V2,M3} { releasedAt( X, Y ), releases( skol6( X, Y )
% 0.76/1.28 , X, Y ), ! releasedAt( X, plus( Y, n1 ) ) }.
% 0.76/1.28 (8657) {G0,W12,D3,L3,V3,M3} { ! happens( Z, X ), ! initiates( Z, Y, X ),
% 0.76/1.28 holdsAt( Y, plus( X, n1 ) ) }.
% 0.76/1.28 (8658) {G0,W12,D3,L3,V3,M3} { ! happens( Z, X ), ! terminates( Z, Y, X ),
% 0.76/1.28 ! holdsAt( Y, plus( X, n1 ) ) }.
% 0.76/1.28 (8659) {G0,W12,D3,L3,V3,M3} { ! happens( Z, X ), ! releases( Z, Y, X ),
% 0.76/1.28 releasedAt( Y, plus( X, n1 ) ) }.
% 0.76/1.28 (8660) {G0,W12,D3,L3,V3,M3} { ! happens( Z, X ), ! initiates( Z, Y, X ), !
% 0.76/1.28 releasedAt( Y, plus( X, n1 ) ) }.
% 0.76/1.28 (8661) {G0,W12,D3,L3,V3,M3} { ! happens( Z, X ), ! terminates( Z, Y, X ),
% 0.76/1.28 ! releasedAt( Y, plus( X, n1 ) ) }.
% 0.76/1.28 (8662) {G0,W12,D2,L3,V3,M3} { ! initiates( X, Y, Z ), alpha14( X, Y, Z ),
% 0.76/1.28 alpha17( X, Y, Z ) }.
% 0.76/1.28 (8663) {G0,W8,D2,L2,V3,M2} { ! alpha14( X, Y, Z ), initiates( X, Y, Z )
% 0.76/1.28 }.
% 0.76/1.28 (8664) {G0,W8,D2,L2,V3,M2} { ! alpha17( X, Y, Z ), initiates( X, Y, Z )
% 0.76/1.28 }.
% 0.76/1.28 (8665) {G0,W12,D2,L3,V3,M3} { ! alpha17( X, Y, Z ), alpha20( X, Y, Z ),
% 0.76/1.28 alpha23( X, Y, Z ) }.
% 0.76/1.28 (8666) {G0,W8,D2,L2,V3,M2} { ! alpha20( X, Y, Z ), alpha17( X, Y, Z ) }.
% 0.76/1.28 (8667) {G0,W8,D2,L2,V3,M2} { ! alpha23( X, Y, Z ), alpha17( X, Y, Z ) }.
% 0.76/1.28 (8668) {G0,W7,D2,L2,V3,M2} { ! alpha23( X, Y, Z ), X = pull }.
% 0.76/1.28 (8669) {G0,W7,D2,L2,V3,M2} { ! alpha23( X, Y, Z ), alpha11( Y, Z ) }.
% 0.76/1.28 (8670) {G0,W10,D2,L3,V3,M3} { ! X = pull, ! alpha11( Y, Z ), alpha23( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 (8671) {G0,W7,D2,L2,V3,M2} { ! alpha20( X, Y, Z ), X = pull }.
% 0.76/1.28 (8672) {G0,W7,D2,L2,V3,M2} { ! alpha20( X, Y, Z ), alpha8( Y, Z ) }.
% 0.76/1.28 (8673) {G0,W10,D2,L3,V3,M3} { ! X = pull, ! alpha8( Y, Z ), alpha20( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 (8674) {G0,W7,D2,L2,V3,M2} { ! alpha14( X, Y, Z ), X = push }.
% 0.76/1.28 (8675) {G0,W7,D2,L2,V3,M2} { ! alpha14( X, Y, Z ), alpha3( Y, Z ) }.
% 0.76/1.28 (8676) {G0,W10,D2,L3,V3,M3} { ! X = push, ! alpha3( Y, Z ), alpha14( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 (8677) {G0,W6,D2,L2,V2,M2} { ! alpha11( X, Y ), X = spinning }.
% 0.76/1.28 (8678) {G0,W6,D2,L2,V2,M2} { ! alpha11( X, Y ), happens( push, Y ) }.
% 0.76/1.28 (8679) {G0,W9,D2,L3,V2,M3} { ! X = spinning, ! happens( push, Y ), alpha11
% 0.76/1.28 ( X, Y ) }.
% 0.76/1.28 (8680) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), X = backwards }.
% 0.76/1.28 (8681) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), ! happens( push, Y ) }.
% 0.76/1.28 (8682) {G0,W9,D2,L3,V2,M3} { ! X = backwards, happens( push, Y ), alpha8(
% 0.76/1.28 X, Y ) }.
% 0.76/1.28 (8683) {G0,W6,D2,L2,V2,M2} { ! alpha3( X, Y ), X = forwards }.
% 0.76/1.28 (8684) {G0,W6,D2,L2,V2,M2} { ! alpha3( X, Y ), ! happens( pull, Y ) }.
% 0.76/1.28 (8685) {G0,W9,D2,L3,V2,M3} { ! X = forwards, happens( pull, Y ), alpha3( X
% 0.76/1.28 , Y ) }.
% 0.76/1.28 (8686) {G0,W12,D2,L3,V3,M3} { ! terminates( X, Y, Z ), alpha24( X, Y, Z )
% 0.76/1.28 , alpha25( X, Y, Z ) }.
% 0.76/1.28 (8687) {G0,W8,D2,L2,V3,M2} { ! alpha24( X, Y, Z ), terminates( X, Y, Z )
% 0.76/1.28 }.
% 0.76/1.28 (8688) {G0,W8,D2,L2,V3,M2} { ! alpha25( X, Y, Z ), terminates( X, Y, Z )
% 0.76/1.28 }.
% 0.76/1.28 (8689) {G0,W12,D2,L3,V3,M3} { ! alpha25( X, Y, Z ), alpha26( X, Y, Z ),
% 0.76/1.28 alpha27( X, Y, Z ) }.
% 0.76/1.28 (8690) {G0,W8,D2,L2,V3,M2} { ! alpha26( X, Y, Z ), alpha25( X, Y, Z ) }.
% 0.76/1.28 (8691) {G0,W8,D2,L2,V3,M2} { ! alpha27( X, Y, Z ), alpha25( X, Y, Z ) }.
% 0.76/1.28 (8692) {G0,W12,D2,L3,V3,M3} { ! alpha27( X, Y, Z ), alpha28( X, Y, Z ),
% 0.76/1.28 alpha29( X, Y, Z ) }.
% 0.76/1.28 (8693) {G0,W8,D2,L2,V3,M2} { ! alpha28( X, Y, Z ), alpha27( X, Y, Z ) }.
% 0.76/1.28 (8694) {G0,W8,D2,L2,V3,M2} { ! alpha29( X, Y, Z ), alpha27( X, Y, Z ) }.
% 0.76/1.28 (8695) {G0,W12,D2,L3,V3,M3} { ! alpha29( X, Y, Z ), alpha30( X, Y, Z ),
% 0.76/1.28 alpha31( X, Y, Z ) }.
% 0.76/1.28 (8696) {G0,W8,D2,L2,V3,M2} { ! alpha30( X, Y, Z ), alpha29( X, Y, Z ) }.
% 0.76/1.28 (8697) {G0,W8,D2,L2,V3,M2} { ! alpha31( X, Y, Z ), alpha29( X, Y, Z ) }.
% 0.76/1.28 (8698) {G0,W12,D2,L3,V3,M3} { ! alpha31( X, Y, Z ), alpha32( X, Y, Z ),
% 0.76/1.28 alpha33( X, Y, Z ) }.
% 0.76/1.28 (8699) {G0,W8,D2,L2,V3,M2} { ! alpha32( X, Y, Z ), alpha31( X, Y, Z ) }.
% 0.76/1.28 (8700) {G0,W8,D2,L2,V3,M2} { ! alpha33( X, Y, Z ), alpha31( X, Y, Z ) }.
% 0.76/1.28 (8701) {G0,W7,D2,L2,V3,M2} { ! alpha33( X, Y, Z ), X = pull }.
% 0.76/1.28 (8702) {G0,W7,D2,L2,V3,M2} { ! alpha33( X, Y, Z ), alpha21( Y, Z ) }.
% 0.76/1.28 (8703) {G0,W10,D2,L3,V3,M3} { ! X = pull, ! alpha21( Y, Z ), alpha33( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 (8704) {G0,W7,D2,L2,V3,M2} { ! alpha32( X, Y, Z ), X = push }.
% 0.76/1.28 (8705) {G0,W7,D2,L2,V3,M2} { ! alpha32( X, Y, Z ), alpha18( Y, Z ) }.
% 0.76/1.28 (8706) {G0,W10,D2,L3,V3,M3} { ! X = push, ! alpha18( Y, Z ), alpha32( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 (8707) {G0,W7,D2,L2,V3,M2} { ! alpha30( X, Y, Z ), X = pull }.
% 0.76/1.28 (8708) {G0,W7,D2,L2,V3,M2} { ! alpha30( X, Y, Z ), alpha15( Y, Z ) }.
% 0.76/1.28 (8709) {G0,W10,D2,L3,V3,M3} { ! X = pull, ! alpha15( Y, Z ), alpha30( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 (8710) {G0,W7,D2,L2,V3,M2} { ! alpha28( X, Y, Z ), X = pull }.
% 0.76/1.28 (8711) {G0,W7,D2,L2,V3,M2} { ! alpha28( X, Y, Z ), alpha12( Y, Z ) }.
% 0.76/1.28 (8712) {G0,W10,D2,L3,V3,M3} { ! X = pull, ! alpha12( Y, Z ), alpha28( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 (8713) {G0,W7,D2,L2,V3,M2} { ! alpha26( X, Y, Z ), X = pull }.
% 0.76/1.28 (8714) {G0,W7,D2,L2,V3,M2} { ! alpha26( X, Y, Z ), alpha9( Y, Z ) }.
% 0.76/1.28 (8715) {G0,W10,D2,L3,V3,M3} { ! X = pull, ! alpha9( Y, Z ), alpha26( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 (8716) {G0,W7,D2,L2,V3,M2} { ! alpha24( X, Y, Z ), X = push }.
% 0.76/1.28 (8717) {G0,W7,D2,L2,V3,M2} { ! alpha24( X, Y, Z ), alpha4( Y, Z ) }.
% 0.76/1.28 (8718) {G0,W10,D2,L3,V3,M3} { ! X = push, ! alpha4( Y, Z ), alpha24( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 (8719) {G0,W6,D2,L2,V2,M2} { ! alpha21( X, Y ), X = spinning }.
% 0.76/1.28 (8720) {G0,W6,D2,L2,V2,M2} { ! alpha21( X, Y ), ! happens( push, Y ) }.
% 0.76/1.28 (8721) {G0,W9,D2,L3,V2,M3} { ! X = spinning, happens( push, Y ), alpha21(
% 0.76/1.28 X, Y ) }.
% 0.76/1.28 (8722) {G0,W6,D2,L2,V2,M2} { ! alpha18( X, Y ), X = spinning }.
% 0.76/1.28 (8723) {G0,W6,D2,L2,V2,M2} { ! alpha18( X, Y ), ! happens( pull, Y ) }.
% 0.76/1.28 (8724) {G0,W9,D2,L3,V2,M3} { ! X = spinning, happens( pull, Y ), alpha18(
% 0.76/1.28 X, Y ) }.
% 0.76/1.28 (8725) {G0,W6,D2,L2,V2,M2} { ! alpha15( X, Y ), X = backwards }.
% 0.76/1.28 (8726) {G0,W6,D2,L2,V2,M2} { ! alpha15( X, Y ), happens( push, Y ) }.
% 0.76/1.28 (8727) {G0,W9,D2,L3,V2,M3} { ! X = backwards, ! happens( push, Y ),
% 0.76/1.28 alpha15( X, Y ) }.
% 0.76/1.28 (8728) {G0,W6,D2,L2,V2,M2} { ! alpha12( X, Y ), X = forwards }.
% 0.76/1.28 (8729) {G0,W6,D2,L2,V2,M2} { ! alpha12( X, Y ), happens( push, Y ) }.
% 0.76/1.28 (8730) {G0,W9,D2,L3,V2,M3} { ! X = forwards, ! happens( push, Y ), alpha12
% 0.76/1.28 ( X, Y ) }.
% 0.76/1.28 (8731) {G0,W6,D2,L2,V2,M2} { ! alpha9( X, Y ), X = forwards }.
% 0.76/1.28 (8732) {G0,W6,D2,L2,V2,M2} { ! alpha9( X, Y ), ! happens( push, Y ) }.
% 0.76/1.28 (8733) {G0,W9,D2,L3,V2,M3} { ! X = forwards, happens( push, Y ), alpha9( X
% 0.76/1.28 , Y ) }.
% 0.76/1.28 (8734) {G0,W6,D2,L2,V2,M2} { ! alpha4( X, Y ), X = backwards }.
% 0.76/1.28 (8735) {G0,W6,D2,L2,V2,M2} { ! alpha4( X, Y ), ! happens( pull, Y ) }.
% 0.76/1.28 (8736) {G0,W9,D2,L3,V2,M3} { ! X = backwards, happens( pull, Y ), alpha4(
% 0.76/1.28 X, Y ) }.
% 0.76/1.28 (8737) {G0,W4,D2,L1,V3,M1} { ! releases( X, Y, Z ) }.
% 0.76/1.28 (8738) {G0,W9,D2,L3,V2,M3} { ! happens( X, Y ), alpha5( X, Y ), alpha10( X
% 0.76/1.28 , Y ) }.
% 0.76/1.28 (8739) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), happens( X, Y ) }.
% 0.76/1.28 (8740) {G0,W6,D2,L2,V2,M2} { ! alpha10( X, Y ), happens( X, Y ) }.
% 0.76/1.28 (8741) {G0,W9,D2,L3,V2,M3} { ! alpha10( X, Y ), alpha13( X, Y ), alpha16(
% 0.76/1.28 X, Y ) }.
% 0.76/1.28 (8742) {G0,W6,D2,L2,V2,M2} { ! alpha13( X, Y ), alpha10( X, Y ) }.
% 0.76/1.28 (8743) {G0,W6,D2,L2,V2,M2} { ! alpha16( X, Y ), alpha10( X, Y ) }.
% 0.76/1.28 (8744) {G0,W9,D2,L3,V2,M3} { ! alpha16( X, Y ), alpha19( X, Y ), alpha22(
% 0.76/1.28 X, Y ) }.
% 0.76/1.28 (8745) {G0,W6,D2,L2,V2,M2} { ! alpha19( X, Y ), alpha16( X, Y ) }.
% 0.76/1.28 (8746) {G0,W6,D2,L2,V2,M2} { ! alpha22( X, Y ), alpha16( X, Y ) }.
% 0.76/1.28 (8747) {G0,W6,D2,L2,V2,M2} { ! alpha22( X, Y ), X = push }.
% 0.76/1.28 (8748) {G0,W6,D2,L2,V2,M2} { ! alpha22( X, Y ), Y = n2 }.
% 0.76/1.28 (8749) {G0,W9,D2,L3,V2,M3} { ! X = push, ! Y = n2, alpha22( X, Y ) }.
% 0.76/1.28 (8750) {G0,W6,D2,L2,V2,M2} { ! alpha19( X, Y ), X = pull }.
% 0.76/1.28 (8751) {G0,W6,D2,L2,V2,M2} { ! alpha19( X, Y ), Y = n2 }.
% 0.76/1.28 (8752) {G0,W9,D2,L3,V2,M3} { ! X = pull, ! Y = n2, alpha19( X, Y ) }.
% 0.76/1.28 (8753) {G0,W6,D2,L2,V2,M2} { ! alpha13( X, Y ), X = pull }.
% 0.76/1.28 (8754) {G0,W6,D2,L2,V2,M2} { ! alpha13( X, Y ), Y = n1 }.
% 0.76/1.28 (8755) {G0,W9,D2,L3,V2,M3} { ! X = pull, ! Y = n1, alpha13( X, Y ) }.
% 0.76/1.28 (8756) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), X = push }.
% 0.76/1.28 (8757) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), Y = n0 }.
% 0.76/1.28 (8758) {G0,W9,D2,L3,V2,M3} { ! X = push, ! Y = n0, alpha5( X, Y ) }.
% 0.76/1.28 (8759) {G0,W3,D2,L1,V0,M1} { ! push = pull }.
% 0.76/1.28 (8760) {G0,W3,D2,L1,V0,M1} { ! forwards = backwards }.
% 0.76/1.28 (8761) {G0,W3,D2,L1,V0,M1} { ! forwards = spinning }.
% 0.76/1.28 (8762) {G0,W3,D2,L1,V0,M1} { ! spinning = backwards }.
% 0.76/1.28 (8763) {G0,W5,D3,L1,V0,M1} { plus( n0, n0 ) = n0 }.
% 0.76/1.28 (8764) {G0,W5,D3,L1,V0,M1} { plus( n0, n1 ) = n1 }.
% 0.76/1.28 (8765) {G0,W5,D3,L1,V0,M1} { plus( n0, n2 ) = n2 }.
% 0.76/1.28 (8766) {G0,W5,D3,L1,V0,M1} { plus( n0, n3 ) = n3 }.
% 0.76/1.28 (8767) {G0,W5,D3,L1,V0,M1} { plus( n1, n1 ) = n2 }.
% 0.76/1.28 (8768) {G0,W5,D3,L1,V0,M1} { plus( n1, n2 ) = n3 }.
% 0.76/1.28 (8769) {G0,W5,D3,L1,V0,M1} { plus( n1, n3 ) = n4 }.
% 0.76/1.28 (8770) {G0,W5,D3,L1,V0,M1} { plus( n2, n2 ) = n4 }.
% 0.76/1.28 (8771) {G0,W5,D3,L1,V0,M1} { plus( n2, n3 ) = n5 }.
% 0.76/1.28 (8772) {G0,W5,D3,L1,V0,M1} { plus( n3, n3 ) = n6 }.
% 0.76/1.28 (8773) {G0,W7,D3,L1,V2,M1} { plus( X, Y ) = plus( Y, X ) }.
% 0.76/1.28 (8774) {G0,W9,D2,L3,V2,M3} { ! less_or_equal( X, Y ), less( X, Y ), X = Y
% 0.76/1.28 }.
% 0.76/1.28 (8775) {G0,W6,D2,L2,V2,M2} { ! less( X, Y ), less_or_equal( X, Y ) }.
% 0.76/1.28 (8776) {G0,W6,D2,L2,V2,M2} { ! X = Y, less_or_equal( X, Y ) }.
% 0.76/1.28 (8777) {G0,W3,D2,L1,V1,M1} { ! less( X, n0 ) }.
% 0.76/1.28 (8778) {G0,W6,D2,L2,V1,M2} { ! less( X, n1 ), less_or_equal( X, n0 ) }.
% 0.76/1.28 (8779) {G0,W6,D2,L2,V1,M2} { ! less_or_equal( X, n0 ), less( X, n1 ) }.
% 0.76/1.28 (8780) {G0,W6,D2,L2,V1,M2} { ! less( X, n2 ), less_or_equal( X, n1 ) }.
% 0.76/1.28 (8781) {G0,W6,D2,L2,V1,M2} { ! less_or_equal( X, n1 ), less( X, n2 ) }.
% 0.76/1.28 (8782) {G0,W6,D2,L2,V1,M2} { ! less( X, n3 ), less_or_equal( X, n2 ) }.
% 0.76/1.28 (8783) {G0,W6,D2,L2,V1,M2} { ! less_or_equal( X, n2 ), less( X, n3 ) }.
% 0.76/1.28 (8784) {G0,W6,D2,L2,V1,M2} { ! less( X, n4 ), less_or_equal( X, n3 ) }.
% 0.76/1.28 (8785) {G0,W6,D2,L2,V1,M2} { ! less_or_equal( X, n3 ), less( X, n4 ) }.
% 0.76/1.28 (8786) {G0,W6,D2,L2,V1,M2} { ! less( X, n5 ), less_or_equal( X, n4 ) }.
% 0.76/1.28 (8787) {G0,W6,D2,L2,V1,M2} { ! less_or_equal( X, n4 ), less( X, n5 ) }.
% 0.76/1.28 (8788) {G0,W6,D2,L2,V1,M2} { ! less( X, n6 ), less_or_equal( X, n5 ) }.
% 0.76/1.28 (8789) {G0,W6,D2,L2,V1,M2} { ! less_or_equal( X, n5 ), less( X, n6 ) }.
% 0.76/1.28 (8790) {G0,W6,D2,L2,V1,M2} { ! less( X, n7 ), less_or_equal( X, n6 ) }.
% 0.76/1.28 (8791) {G0,W6,D2,L2,V1,M2} { ! less_or_equal( X, n6 ), less( X, n7 ) }.
% 0.76/1.28 (8792) {G0,W6,D2,L2,V1,M2} { ! less( X, n8 ), less_or_equal( X, n7 ) }.
% 0.76/1.28 (8793) {G0,W6,D2,L2,V1,M2} { ! less_or_equal( X, n7 ), less( X, n8 ) }.
% 0.76/1.28 (8794) {G0,W6,D2,L2,V1,M2} { ! less( X, n9 ), less_or_equal( X, n8 ) }.
% 0.76/1.28 (8795) {G0,W6,D2,L2,V1,M2} { ! less_or_equal( X, n8 ), less( X, n9 ) }.
% 0.76/1.28 (8796) {G0,W6,D2,L2,V2,M2} { ! less( X, Y ), ! less( Y, X ) }.
% 0.76/1.28 (8797) {G0,W6,D2,L2,V2,M2} { ! less( X, Y ), ! Y = X }.
% 0.76/1.28 (8798) {G0,W9,D2,L3,V2,M3} { less( Y, X ), Y = X, less( X, Y ) }.
% 0.76/1.28 (8799) {G0,W3,D2,L1,V0,M1} { ! holdsAt( forwards, n0 ) }.
% 0.76/1.28 (8800) {G0,W3,D2,L1,V0,M1} { ! holdsAt( backwards, n0 ) }.
% 0.76/1.28 (8801) {G0,W3,D2,L1,V0,M1} { ! holdsAt( spinning, n0 ) }.
% 0.76/1.28 (8802) {G0,W3,D2,L1,V2,M1} { ! releasedAt( X, Y ) }.
% 0.76/1.28 (8803) {G0,W3,D2,L1,V0,M1} { holdsAt( backwards, n3 ) }.
% 0.76/1.28
% 0.76/1.28
% 0.76/1.28 Total Proof:
% 0.76/1.28
% 0.76/1.28 subsumption: (29) {G0,W12,D3,L3,V3,M3} I { ! happens( Z, X ), ! terminates
% 0.76/1.28 ( Z, Y, X ), ! holdsAt( Y, plus( X, n1 ) ) }.
% 0.76/1.28 parent0: (8658) {G0,W12,D3,L3,V3,M3} { ! happens( Z, X ), ! terminates( Z
% 0.76/1.28 , Y, X ), ! holdsAt( Y, plus( X, n1 ) ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 Z := Z
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 2 ==> 2
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (59) {G0,W8,D2,L2,V3,M2} I { ! alpha25( X, Y, Z ), terminates
% 0.76/1.28 ( X, Y, Z ) }.
% 0.76/1.28 parent0: (8688) {G0,W8,D2,L2,V3,M2} { ! alpha25( X, Y, Z ), terminates( X
% 0.76/1.28 , Y, Z ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 Z := Z
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (62) {G0,W8,D2,L2,V3,M2} I { ! alpha27( X, Y, Z ), alpha25( X
% 0.76/1.28 , Y, Z ) }.
% 0.76/1.28 parent0: (8691) {G0,W8,D2,L2,V3,M2} { ! alpha27( X, Y, Z ), alpha25( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 Z := Z
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (65) {G0,W8,D2,L2,V3,M2} I { ! alpha29( X, Y, Z ), alpha27( X
% 0.76/1.28 , Y, Z ) }.
% 0.76/1.28 parent0: (8694) {G0,W8,D2,L2,V3,M2} { ! alpha29( X, Y, Z ), alpha27( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 Z := Z
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (67) {G0,W8,D2,L2,V3,M2} I { ! alpha30( X, Y, Z ), alpha29( X
% 0.76/1.28 , Y, Z ) }.
% 0.76/1.28 parent0: (8696) {G0,W8,D2,L2,V3,M2} { ! alpha30( X, Y, Z ), alpha29( X, Y
% 0.76/1.28 , Z ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 Z := Z
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (80) {G0,W10,D2,L3,V3,M3} I { ! X = pull, ! alpha15( Y, Z ),
% 0.76/1.28 alpha30( X, Y, Z ) }.
% 0.76/1.28 parent0: (8709) {G0,W10,D2,L3,V3,M3} { ! X = pull, ! alpha15( Y, Z ),
% 0.76/1.28 alpha30( X, Y, Z ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 Z := Z
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 2 ==> 2
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (98) {G0,W9,D2,L3,V2,M3} I { ! X = backwards, ! happens( push
% 0.76/1.28 , Y ), alpha15( X, Y ) }.
% 0.76/1.28 parent0: (8727) {G0,W9,D2,L3,V2,M3} { ! X = backwards, ! happens( push, Y
% 0.76/1.28 ), alpha15( X, Y ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 2 ==> 2
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (111) {G0,W6,D2,L2,V2,M2} I { ! alpha10( X, Y ), happens( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 parent0: (8740) {G0,W6,D2,L2,V2,M2} { ! alpha10( X, Y ), happens( X, Y )
% 0.76/1.28 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (114) {G0,W6,D2,L2,V2,M2} I { ! alpha16( X, Y ), alpha10( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 parent0: (8743) {G0,W6,D2,L2,V2,M2} { ! alpha16( X, Y ), alpha10( X, Y )
% 0.76/1.28 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (116) {G0,W6,D2,L2,V2,M2} I { ! alpha19( X, Y ), alpha16( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 parent0: (8745) {G0,W6,D2,L2,V2,M2} { ! alpha19( X, Y ), alpha16( X, Y )
% 0.76/1.28 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (117) {G0,W6,D2,L2,V2,M2} I { ! alpha22( X, Y ), alpha16( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 parent0: (8746) {G0,W6,D2,L2,V2,M2} { ! alpha22( X, Y ), alpha16( X, Y )
% 0.76/1.28 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (120) {G0,W9,D2,L3,V2,M3} I { ! X = push, ! Y = n2, alpha22( X
% 0.76/1.28 , Y ) }.
% 0.76/1.28 parent0: (8749) {G0,W9,D2,L3,V2,M3} { ! X = push, ! Y = n2, alpha22( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 2 ==> 2
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (123) {G0,W9,D2,L3,V2,M3} I { ! X = pull, ! Y = n2, alpha19( X
% 0.76/1.28 , Y ) }.
% 0.76/1.28 parent0: (8752) {G0,W9,D2,L3,V2,M3} { ! X = pull, ! Y = n2, alpha19( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 2 ==> 2
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (139) {G0,W5,D3,L1,V0,M1} I { plus( n1, n2 ) ==> n3 }.
% 0.76/1.28 parent0: (8768) {G0,W5,D3,L1,V0,M1} { plus( n1, n2 ) = n3 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (144) {G0,W7,D3,L1,V2,M1} I { plus( X, Y ) = plus( Y, X ) }.
% 0.76/1.28 parent0: (8773) {G0,W7,D3,L1,V2,M1} { plus( X, Y ) = plus( Y, X ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (174) {G0,W3,D2,L1,V0,M1} I { holdsAt( backwards, n3 ) }.
% 0.76/1.28 parent0: (8803) {G0,W3,D2,L1,V0,M1} { holdsAt( backwards, n3 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9372) {G0,W9,D2,L3,V2,M3} { ! push = X, ! Y = n2, alpha22( X, Y )
% 0.76/1.28 }.
% 0.76/1.28 parent0[0]: (120) {G0,W9,D2,L3,V2,M3} I { ! X = push, ! Y = n2, alpha22( X
% 0.76/1.28 , Y ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqrefl: (9376) {G0,W6,D2,L2,V1,M2} { ! push = X, alpha22( X, n2 ) }.
% 0.76/1.28 parent0[1]: (9372) {G0,W9,D2,L3,V2,M3} { ! push = X, ! Y = n2, alpha22( X
% 0.76/1.28 , Y ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := n2
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9377) {G0,W6,D2,L2,V1,M2} { ! X = push, alpha22( X, n2 ) }.
% 0.76/1.28 parent0[0]: (9376) {G0,W6,D2,L2,V1,M2} { ! push = X, alpha22( X, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (194) {G1,W6,D2,L2,V1,M2} Q(120) { ! X = push, alpha22( X, n2
% 0.76/1.28 ) }.
% 0.76/1.28 parent0: (9377) {G0,W6,D2,L2,V1,M2} { ! X = push, alpha22( X, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9379) {G1,W6,D2,L2,V1,M2} { ! push = X, alpha22( X, n2 ) }.
% 0.76/1.28 parent0[0]: (194) {G1,W6,D2,L2,V1,M2} Q(120) { ! X = push, alpha22( X, n2 )
% 0.76/1.28 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqrefl: (9380) {G0,W3,D2,L1,V0,M1} { alpha22( push, n2 ) }.
% 0.76/1.28 parent0[0]: (9379) {G1,W6,D2,L2,V1,M2} { ! push = X, alpha22( X, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := push
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (195) {G2,W3,D2,L1,V0,M1} Q(194) { alpha22( push, n2 ) }.
% 0.76/1.28 parent0: (9380) {G0,W3,D2,L1,V0,M1} { alpha22( push, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9381) {G0,W9,D2,L3,V2,M3} { ! pull = X, ! Y = n2, alpha19( X, Y )
% 0.76/1.28 }.
% 0.76/1.28 parent0[0]: (123) {G0,W9,D2,L3,V2,M3} I { ! X = pull, ! Y = n2, alpha19( X
% 0.76/1.28 , Y ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqrefl: (9385) {G0,W6,D2,L2,V1,M2} { ! pull = X, alpha19( X, n2 ) }.
% 0.76/1.28 parent0[1]: (9381) {G0,W9,D2,L3,V2,M3} { ! pull = X, ! Y = n2, alpha19( X
% 0.76/1.28 , Y ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := n2
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9386) {G0,W6,D2,L2,V1,M2} { ! X = pull, alpha19( X, n2 ) }.
% 0.76/1.28 parent0[0]: (9385) {G0,W6,D2,L2,V1,M2} { ! pull = X, alpha19( X, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (197) {G1,W6,D2,L2,V1,M2} Q(123) { ! X = pull, alpha19( X, n2
% 0.76/1.28 ) }.
% 0.76/1.28 parent0: (9386) {G0,W6,D2,L2,V1,M2} { ! X = pull, alpha19( X, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9388) {G1,W6,D2,L2,V1,M2} { ! pull = X, alpha19( X, n2 ) }.
% 0.76/1.28 parent0[0]: (197) {G1,W6,D2,L2,V1,M2} Q(123) { ! X = pull, alpha19( X, n2 )
% 0.76/1.28 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqrefl: (9389) {G0,W3,D2,L1,V0,M1} { alpha19( pull, n2 ) }.
% 0.76/1.28 parent0[0]: (9388) {G1,W6,D2,L2,V1,M2} { ! pull = X, alpha19( X, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := pull
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (198) {G2,W3,D2,L1,V0,M1} Q(197) { alpha19( pull, n2 ) }.
% 0.76/1.28 parent0: (9389) {G0,W3,D2,L1,V0,M1} { alpha19( pull, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 resolution: (9390) {G1,W3,D2,L1,V0,M1} { alpha16( push, n2 ) }.
% 0.76/1.28 parent0[0]: (117) {G0,W6,D2,L2,V2,M2} I { ! alpha22( X, Y ), alpha16( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 parent1[0]: (195) {G2,W3,D2,L1,V0,M1} Q(194) { alpha22( push, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := push
% 0.76/1.28 Y := n2
% 0.76/1.28 end
% 0.76/1.28 substitution1:
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (991) {G3,W3,D2,L1,V0,M1} R(117,195) { alpha16( push, n2 ) }.
% 0.76/1.28 parent0: (9390) {G1,W3,D2,L1,V0,M1} { alpha16( push, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 resolution: (9391) {G1,W3,D2,L1,V0,M1} { alpha16( pull, n2 ) }.
% 0.76/1.28 parent0[0]: (116) {G0,W6,D2,L2,V2,M2} I { ! alpha19( X, Y ), alpha16( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 parent1[0]: (198) {G2,W3,D2,L1,V0,M1} Q(197) { alpha19( pull, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := pull
% 0.76/1.28 Y := n2
% 0.76/1.28 end
% 0.76/1.28 substitution1:
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (992) {G3,W3,D2,L1,V0,M1} R(116,198) { alpha16( pull, n2 ) }.
% 0.76/1.28 parent0: (9391) {G1,W3,D2,L1,V0,M1} { alpha16( pull, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 resolution: (9392) {G1,W3,D2,L1,V0,M1} { alpha10( pull, n2 ) }.
% 0.76/1.28 parent0[0]: (114) {G0,W6,D2,L2,V2,M2} I { ! alpha16( X, Y ), alpha10( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 parent1[0]: (992) {G3,W3,D2,L1,V0,M1} R(116,198) { alpha16( pull, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := pull
% 0.76/1.28 Y := n2
% 0.76/1.28 end
% 0.76/1.28 substitution1:
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (993) {G4,W3,D2,L1,V0,M1} R(114,992) { alpha10( pull, n2 ) }.
% 0.76/1.28 parent0: (9392) {G1,W3,D2,L1,V0,M1} { alpha10( pull, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 resolution: (9393) {G1,W3,D2,L1,V0,M1} { alpha10( push, n2 ) }.
% 0.76/1.28 parent0[0]: (114) {G0,W6,D2,L2,V2,M2} I { ! alpha16( X, Y ), alpha10( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 parent1[0]: (991) {G3,W3,D2,L1,V0,M1} R(117,195) { alpha16( push, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := push
% 0.76/1.28 Y := n2
% 0.76/1.28 end
% 0.76/1.28 substitution1:
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (995) {G4,W3,D2,L1,V0,M1} R(114,991) { alpha10( push, n2 ) }.
% 0.76/1.28 parent0: (9393) {G1,W3,D2,L1,V0,M1} { alpha10( push, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 resolution: (9394) {G1,W3,D2,L1,V0,M1} { happens( push, n2 ) }.
% 0.76/1.28 parent0[0]: (111) {G0,W6,D2,L2,V2,M2} I { ! alpha10( X, Y ), happens( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 parent1[0]: (995) {G4,W3,D2,L1,V0,M1} R(114,991) { alpha10( push, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := push
% 0.76/1.28 Y := n2
% 0.76/1.28 end
% 0.76/1.28 substitution1:
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (1002) {G5,W3,D2,L1,V0,M1} R(111,995) { happens( push, n2 )
% 0.76/1.28 }.
% 0.76/1.28 parent0: (9394) {G1,W3,D2,L1,V0,M1} { happens( push, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 resolution: (9395) {G1,W3,D2,L1,V0,M1} { happens( pull, n2 ) }.
% 0.76/1.28 parent0[0]: (111) {G0,W6,D2,L2,V2,M2} I { ! alpha10( X, Y ), happens( X, Y
% 0.76/1.28 ) }.
% 0.76/1.28 parent1[0]: (993) {G4,W3,D2,L1,V0,M1} R(114,992) { alpha10( pull, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := pull
% 0.76/1.28 Y := n2
% 0.76/1.28 end
% 0.76/1.28 substitution1:
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (1003) {G5,W3,D2,L1,V0,M1} R(111,993) { happens( pull, n2 )
% 0.76/1.28 }.
% 0.76/1.28 parent0: (9395) {G1,W3,D2,L1,V0,M1} { happens( pull, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9396) {G0,W9,D2,L3,V2,M3} { ! backwards = X, ! happens( push, Y )
% 0.76/1.28 , alpha15( X, Y ) }.
% 0.76/1.28 parent0[0]: (98) {G0,W9,D2,L3,V2,M3} I { ! X = backwards, ! happens( push,
% 0.76/1.28 Y ), alpha15( X, Y ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 resolution: (9397) {G1,W6,D2,L2,V1,M2} { ! backwards = X, alpha15( X, n2 )
% 0.76/1.28 }.
% 0.76/1.28 parent0[1]: (9396) {G0,W9,D2,L3,V2,M3} { ! backwards = X, ! happens( push
% 0.76/1.28 , Y ), alpha15( X, Y ) }.
% 0.76/1.28 parent1[0]: (1002) {G5,W3,D2,L1,V0,M1} R(111,995) { happens( push, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := n2
% 0.76/1.28 end
% 0.76/1.28 substitution1:
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9398) {G1,W6,D2,L2,V1,M2} { ! X = backwards, alpha15( X, n2 ) }.
% 0.76/1.28 parent0[0]: (9397) {G1,W6,D2,L2,V1,M2} { ! backwards = X, alpha15( X, n2 )
% 0.76/1.28 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (6301) {G6,W6,D2,L2,V1,M2} R(98,1002) { ! X = backwards,
% 0.76/1.28 alpha15( X, n2 ) }.
% 0.76/1.28 parent0: (9398) {G1,W6,D2,L2,V1,M2} { ! X = backwards, alpha15( X, n2 )
% 0.76/1.28 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9399) {G6,W6,D2,L2,V1,M2} { ! backwards = X, alpha15( X, n2 ) }.
% 0.76/1.28 parent0[0]: (6301) {G6,W6,D2,L2,V1,M2} R(98,1002) { ! X = backwards,
% 0.76/1.28 alpha15( X, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqrefl: (9400) {G0,W3,D2,L1,V0,M1} { alpha15( backwards, n2 ) }.
% 0.76/1.28 parent0[0]: (9399) {G6,W6,D2,L2,V1,M2} { ! backwards = X, alpha15( X, n2 )
% 0.76/1.28 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := backwards
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (6377) {G7,W3,D2,L1,V0,M1} Q(6301) { alpha15( backwards, n2 )
% 0.76/1.28 }.
% 0.76/1.28 parent0: (9400) {G0,W3,D2,L1,V0,M1} { alpha15( backwards, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9401) {G0,W10,D2,L3,V3,M3} { ! pull = X, ! alpha15( Y, Z ),
% 0.76/1.28 alpha30( X, Y, Z ) }.
% 0.76/1.28 parent0[0]: (80) {G0,W10,D2,L3,V3,M3} I { ! X = pull, ! alpha15( Y, Z ),
% 0.76/1.28 alpha30( X, Y, Z ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := Y
% 0.76/1.28 Z := Z
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 resolution: (9402) {G1,W7,D2,L2,V1,M2} { ! pull = X, alpha30( X, backwards
% 0.76/1.28 , n2 ) }.
% 0.76/1.28 parent0[1]: (9401) {G0,W10,D2,L3,V3,M3} { ! pull = X, ! alpha15( Y, Z ),
% 0.76/1.28 alpha30( X, Y, Z ) }.
% 0.76/1.28 parent1[0]: (6377) {G7,W3,D2,L1,V0,M1} Q(6301) { alpha15( backwards, n2 )
% 0.76/1.28 }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 Y := backwards
% 0.76/1.28 Z := n2
% 0.76/1.28 end
% 0.76/1.28 substitution1:
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9403) {G1,W7,D2,L2,V1,M2} { ! X = pull, alpha30( X, backwards, n2
% 0.76/1.28 ) }.
% 0.76/1.28 parent0[0]: (9402) {G1,W7,D2,L2,V1,M2} { ! pull = X, alpha30( X, backwards
% 0.76/1.28 , n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (6398) {G8,W7,D2,L2,V1,M2} R(6377,80) { ! X = pull, alpha30( X
% 0.76/1.28 , backwards, n2 ) }.
% 0.76/1.28 parent0: (9403) {G1,W7,D2,L2,V1,M2} { ! X = pull, alpha30( X, backwards,
% 0.76/1.28 n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 1 ==> 1
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqswap: (9404) {G8,W7,D2,L2,V1,M2} { ! pull = X, alpha30( X, backwards, n2
% 0.76/1.28 ) }.
% 0.76/1.28 parent0[0]: (6398) {G8,W7,D2,L2,V1,M2} R(6377,80) { ! X = pull, alpha30( X
% 0.76/1.28 , backwards, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := X
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 eqrefl: (9405) {G0,W4,D2,L1,V0,M1} { alpha30( pull, backwards, n2 ) }.
% 0.76/1.28 parent0[0]: (9404) {G8,W7,D2,L2,V1,M2} { ! pull = X, alpha30( X, backwards
% 0.76/1.28 , n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := pull
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (6399) {G9,W4,D2,L1,V0,M1} Q(6398) { alpha30( pull, backwards
% 0.76/1.28 , n2 ) }.
% 0.76/1.28 parent0: (9405) {G0,W4,D2,L1,V0,M1} { alpha30( pull, backwards, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 end
% 0.76/1.28 permutation0:
% 0.76/1.28 0 ==> 0
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 resolution: (9406) {G1,W4,D2,L1,V0,M1} { alpha29( pull, backwards, n2 )
% 0.76/1.28 }.
% 0.76/1.28 parent0[0]: (67) {G0,W8,D2,L2,V3,M2} I { ! alpha30( X, Y, Z ), alpha29( X,
% 0.76/1.28 Y, Z ) }.
% 0.76/1.28 parent1[0]: (6399) {G9,W4,D2,L1,V0,M1} Q(6398) { alpha30( pull, backwards,
% 0.76/1.28 n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.28 X := pull
% 0.76/1.28 Y := backwards
% 0.76/1.28 Z := n2
% 0.76/1.28 end
% 0.76/1.28 substitution1:
% 0.76/1.28 end
% 0.76/1.28
% 0.76/1.28 subsumption: (6400) {G10,W4,D2,L1,V0,M1} R(6399,67) { alpha29( pull,
% 0.76/1.28 backwards, n2 ) }.
% 0.76/1.28 parent0: (9406) {G1,W4,D2,L1,V0,M1} { alpha29( pull, backwards, n2 ) }.
% 0.76/1.28 substitution0:
% 0.76/1.29 end
% 0.76/1.29 permutation0:
% 0.76/1.29 0 ==> 0
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 resolution: (9407) {G1,W4,D2,L1,V0,M1} { alpha27( pull, backwards, n2 )
% 0.76/1.29 }.
% 0.76/1.29 parent0[0]: (65) {G0,W8,D2,L2,V3,M2} I { ! alpha29( X, Y, Z ), alpha27( X,
% 0.76/1.29 Y, Z ) }.
% 0.76/1.29 parent1[0]: (6400) {G10,W4,D2,L1,V0,M1} R(6399,67) { alpha29( pull,
% 0.76/1.29 backwards, n2 ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 X := pull
% 0.76/1.29 Y := backwards
% 0.76/1.29 Z := n2
% 0.76/1.29 end
% 0.76/1.29 substitution1:
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 subsumption: (6401) {G11,W4,D2,L1,V0,M1} R(6400,65) { alpha27( pull,
% 0.76/1.29 backwards, n2 ) }.
% 0.76/1.29 parent0: (9407) {G1,W4,D2,L1,V0,M1} { alpha27( pull, backwards, n2 ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 end
% 0.76/1.29 permutation0:
% 0.76/1.29 0 ==> 0
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 resolution: (9408) {G1,W4,D2,L1,V0,M1} { alpha25( pull, backwards, n2 )
% 0.76/1.29 }.
% 0.76/1.29 parent0[0]: (62) {G0,W8,D2,L2,V3,M2} I { ! alpha27( X, Y, Z ), alpha25( X,
% 0.76/1.29 Y, Z ) }.
% 0.76/1.29 parent1[0]: (6401) {G11,W4,D2,L1,V0,M1} R(6400,65) { alpha27( pull,
% 0.76/1.29 backwards, n2 ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 X := pull
% 0.76/1.29 Y := backwards
% 0.76/1.29 Z := n2
% 0.76/1.29 end
% 0.76/1.29 substitution1:
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 subsumption: (6891) {G12,W4,D2,L1,V0,M1} R(6401,62) { alpha25( pull,
% 0.76/1.29 backwards, n2 ) }.
% 0.76/1.29 parent0: (9408) {G1,W4,D2,L1,V0,M1} { alpha25( pull, backwards, n2 ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 end
% 0.76/1.29 permutation0:
% 0.76/1.29 0 ==> 0
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 resolution: (9409) {G1,W4,D2,L1,V0,M1} { terminates( pull, backwards, n2 )
% 0.76/1.29 }.
% 0.76/1.29 parent0[0]: (59) {G0,W8,D2,L2,V3,M2} I { ! alpha25( X, Y, Z ), terminates(
% 0.76/1.29 X, Y, Z ) }.
% 0.76/1.29 parent1[0]: (6891) {G12,W4,D2,L1,V0,M1} R(6401,62) { alpha25( pull,
% 0.76/1.29 backwards, n2 ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 X := pull
% 0.76/1.29 Y := backwards
% 0.76/1.29 Z := n2
% 0.76/1.29 end
% 0.76/1.29 substitution1:
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 subsumption: (6892) {G13,W4,D2,L1,V0,M1} R(6891,59) { terminates( pull,
% 0.76/1.29 backwards, n2 ) }.
% 0.76/1.29 parent0: (9409) {G1,W4,D2,L1,V0,M1} { terminates( pull, backwards, n2 )
% 0.76/1.29 }.
% 0.76/1.29 substitution0:
% 0.76/1.29 end
% 0.76/1.29 permutation0:
% 0.76/1.29 0 ==> 0
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 resolution: (9410) {G1,W8,D3,L2,V0,M2} { ! happens( pull, n2 ), ! holdsAt
% 0.76/1.29 ( backwards, plus( n2, n1 ) ) }.
% 0.76/1.29 parent0[1]: (29) {G0,W12,D3,L3,V3,M3} I { ! happens( Z, X ), ! terminates(
% 0.76/1.29 Z, Y, X ), ! holdsAt( Y, plus( X, n1 ) ) }.
% 0.76/1.29 parent1[0]: (6892) {G13,W4,D2,L1,V0,M1} R(6891,59) { terminates( pull,
% 0.76/1.29 backwards, n2 ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 X := n2
% 0.76/1.29 Y := backwards
% 0.76/1.29 Z := pull
% 0.76/1.29 end
% 0.76/1.29 substitution1:
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 resolution: (9411) {G2,W5,D3,L1,V0,M1} { ! holdsAt( backwards, plus( n2,
% 0.76/1.29 n1 ) ) }.
% 0.76/1.29 parent0[0]: (9410) {G1,W8,D3,L2,V0,M2} { ! happens( pull, n2 ), ! holdsAt
% 0.76/1.29 ( backwards, plus( n2, n1 ) ) }.
% 0.76/1.29 parent1[0]: (1003) {G5,W3,D2,L1,V0,M1} R(111,993) { happens( pull, n2 ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 end
% 0.76/1.29 substitution1:
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 subsumption: (6956) {G14,W5,D3,L1,V0,M1} R(6892,29);r(1003) { ! holdsAt(
% 0.76/1.29 backwards, plus( n2, n1 ) ) }.
% 0.76/1.29 parent0: (9411) {G2,W5,D3,L1,V0,M1} { ! holdsAt( backwards, plus( n2, n1 )
% 0.76/1.29 ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 end
% 0.76/1.29 permutation0:
% 0.76/1.29 0 ==> 0
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 paramod: (9413) {G1,W5,D3,L1,V0,M1} { ! holdsAt( backwards, plus( n1, n2 )
% 0.76/1.29 ) }.
% 0.76/1.29 parent0[0]: (144) {G0,W7,D3,L1,V2,M1} I { plus( X, Y ) = plus( Y, X ) }.
% 0.76/1.29 parent1[0; 3]: (6956) {G14,W5,D3,L1,V0,M1} R(6892,29);r(1003) { ! holdsAt(
% 0.76/1.29 backwards, plus( n2, n1 ) ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 X := n2
% 0.76/1.29 Y := n1
% 0.76/1.29 end
% 0.76/1.29 substitution1:
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 paramod: (9415) {G1,W3,D2,L1,V0,M1} { ! holdsAt( backwards, n3 ) }.
% 0.76/1.29 parent0[0]: (139) {G0,W5,D3,L1,V0,M1} I { plus( n1, n2 ) ==> n3 }.
% 0.76/1.29 parent1[0; 3]: (9413) {G1,W5,D3,L1,V0,M1} { ! holdsAt( backwards, plus( n1
% 0.76/1.29 , n2 ) ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 end
% 0.76/1.29 substitution1:
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 resolution: (9416) {G1,W0,D0,L0,V0,M0} { }.
% 0.76/1.29 parent0[0]: (9415) {G1,W3,D2,L1,V0,M1} { ! holdsAt( backwards, n3 ) }.
% 0.76/1.29 parent1[0]: (174) {G0,W3,D2,L1,V0,M1} I { holdsAt( backwards, n3 ) }.
% 0.76/1.29 substitution0:
% 0.76/1.29 end
% 0.76/1.29 substitution1:
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 subsumption: (8627) {G15,W0,D0,L0,V0,M0} P(144,6956);d(139);r(174) { }.
% 0.76/1.29 parent0: (9416) {G1,W0,D0,L0,V0,M0} { }.
% 0.76/1.29 substitution0:
% 0.76/1.29 end
% 0.76/1.29 permutation0:
% 0.76/1.29 end
% 0.76/1.29
% 0.76/1.29 Proof check complete!
% 0.76/1.29
% 0.76/1.29 Memory use:
% 0.76/1.29
% 0.76/1.29 space for terms: 101509
% 0.76/1.29 space for clauses: 313258
% 0.76/1.29
% 0.76/1.29
% 0.76/1.29 clauses generated: 12327
% 0.76/1.29 clauses kept: 8628
% 0.76/1.29 clauses selected: 507
% 0.76/1.29 clauses deleted: 34
% 0.76/1.29 clauses inuse deleted: 0
% 0.76/1.29
% 0.76/1.29 subsentry: 22017
% 0.76/1.29 literals s-matched: 16566
% 0.76/1.29 literals matched: 16502
% 0.76/1.29 full subsumption: 1889
% 0.76/1.29
% 0.76/1.29 checksum: -33631220
% 0.76/1.29
% 0.76/1.29
% 0.76/1.29 Bliksem ended
%------------------------------------------------------------------------------