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