%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM436+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n020.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 : Mon Jul 18 06:22:15 EDT 2022
% Result : Theorem 277.15s 277.60s
% Output : Refutation 277.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NUM436+1 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Wed Jul 6 01:44:14 EDT 2022
% 0.13/0.34 % CPUTime :
% 6.67/7.05 *** allocated 10000 integers for termspace/termends
% 6.67/7.05 *** allocated 10000 integers for clauses
% 6.67/7.05 *** allocated 10000 integers for justifications
% 6.67/7.05 Bliksem 1.12
% 6.67/7.05
% 6.67/7.05
% 6.67/7.05 Automatic Strategy Selection
% 6.67/7.05
% 6.67/7.05
% 6.67/7.05 Clauses:
% 6.67/7.05
% 6.67/7.05 { && }.
% 6.67/7.05 { aInteger0( sz00 ) }.
% 6.67/7.05 { aInteger0( sz10 ) }.
% 6.67/7.05 { ! aInteger0( X ), aInteger0( smndt0( X ) ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), aInteger0( sdtpldt0( X, Y ) ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), aInteger0( sdtasdt0( X, Y ) ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), sdtpldt0( X,
% 6.67/7.05 sdtpldt0( Y, Z ) ) = sdtpldt0( sdtpldt0( X, Y ), Z ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }
% 6.67/7.05 .
% 6.67/7.05 { ! aInteger0( X ), sdtpldt0( X, sz00 ) = X }.
% 6.67/7.05 { ! aInteger0( X ), X = sdtpldt0( sz00, X ) }.
% 6.67/7.05 { ! aInteger0( X ), sdtpldt0( X, smndt0( X ) ) = sz00 }.
% 6.67/7.05 { ! aInteger0( X ), sz00 = sdtpldt0( smndt0( X ), X ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), sdtasdt0( X,
% 6.67/7.05 sdtasdt0( Y, Z ) ) = sdtasdt0( sdtasdt0( X, Y ), Z ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }
% 6.67/7.05 .
% 6.67/7.05 { ! aInteger0( X ), sdtasdt0( X, sz10 ) = X }.
% 6.67/7.05 { ! aInteger0( X ), X = sdtasdt0( sz10, X ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), sdtasdt0( X,
% 6.67/7.05 sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), sdtasdt0( sdtpldt0
% 6.67/7.05 ( X, Y ), Z ) = sdtpldt0( sdtasdt0( X, Z ), sdtasdt0( Y, Z ) ) }.
% 6.67/7.05 { ! aInteger0( X ), sdtasdt0( X, sz00 ) = sz00 }.
% 6.67/7.05 { ! aInteger0( X ), sz00 = sdtasdt0( sz00, X ) }.
% 6.67/7.05 { ! aInteger0( X ), sdtasdt0( smndt0( sz10 ), X ) = smndt0( X ) }.
% 6.67/7.05 { ! aInteger0( X ), smndt0( X ) = sdtasdt0( X, smndt0( sz10 ) ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), ! sdtasdt0( X, Y ) = sz00, X = sz00,
% 6.67/7.05 Y = sz00 }.
% 6.67/7.05 { ! aInteger0( X ), ! aDivisorOf0( Y, X ), aInteger0( Y ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aDivisorOf0( Y, X ), alpha1( X, Y ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), ! alpha1( X, Y ), aDivisorOf0( Y, X )
% 6.67/7.05 }.
% 6.67/7.05 { ! alpha1( X, Y ), ! Y = sz00 }.
% 6.67/7.05 { ! alpha1( X, Y ), alpha2( X, Y ) }.
% 6.67/7.05 { Y = sz00, ! alpha2( X, Y ), alpha1( X, Y ) }.
% 6.67/7.05 { ! alpha2( X, Y ), aInteger0( skol1( Z, T ) ) }.
% 6.67/7.05 { ! alpha2( X, Y ), sdtasdt0( Y, skol1( X, Y ) ) = X }.
% 6.67/7.05 { ! aInteger0( Z ), ! sdtasdt0( Y, Z ) = X, alpha2( X, Y ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), Z = sz00, !
% 6.67/7.05 sdteqdtlpzmzozddtrp0( X, Y, Z ), aDivisorOf0( Z, sdtpldt0( X, smndt0( Y )
% 6.67/7.05 ) ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), Z = sz00, !
% 6.67/7.05 aDivisorOf0( Z, sdtpldt0( X, smndt0( Y ) ) ), sdteqdtlpzmzozddtrp0( X, Y
% 6.67/7.05 , Z ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), Y = sz00, sdteqdtlpzmzozddtrp0( X, X
% 6.67/7.05 , Y ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), Z = sz00, !
% 6.67/7.05 sdteqdtlpzmzozddtrp0( X, Y, Z ), sdteqdtlpzmzozddtrp0( Y, X, Z ) }.
% 6.67/7.05 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), Z = sz00, !
% 6.67/7.05 aInteger0( T ), ! sdteqdtlpzmzozddtrp0( X, Y, Z ), ! sdteqdtlpzmzozddtrp0
% 6.67/7.05 ( Y, T, Z ), sdteqdtlpzmzozddtrp0( X, T, Z ) }.
% 6.67/7.05 { aInteger0( xa ) }.
% 6.67/7.05 { aInteger0( xb ) }.
% 6.67/7.05 { aInteger0( xp ) }.
% 6.67/7.05 { ! xp = sz00 }.
% 6.67/7.05 { aInteger0( xq ) }.
% 6.67/7.05 { ! xq = sz00 }.
% 6.67/7.05 { sdteqdtlpzmzozddtrp0( xa, xb, sdtasdt0( xp, xq ) ) }.
% 6.67/7.05 { aInteger0( xm ) }.
% 6.67/7.05 { sdtasdt0( sdtasdt0( xp, xq ), xm ) = sdtpldt0( xa, smndt0( xb ) ) }.
% 6.67/7.05 { sdtasdt0( xp, sdtasdt0( xq, xm ) ) = sdtpldt0( xa, smndt0( xb ) ) }.
% 6.67/7.05 { sdtpldt0( xa, smndt0( xb ) ) = sdtasdt0( xq, sdtasdt0( xp, xm ) ) }.
% 6.67/7.05 { ! sdteqdtlpzmzozddtrp0( xa, xb, xp ), ! sdteqdtlpzmzozddtrp0( xa, xb, xq
% 6.67/7.05 ) }.
% 6.67/7.05
% 6.67/7.05 percentage equality = 0.264000, percentage horn = 0.857143
% 6.67/7.05 This is a problem with some equality
% 6.67/7.05
% 6.67/7.05
% 6.67/7.05
% 6.67/7.05 Options Used:
% 6.67/7.05
% 6.67/7.05 useres = 1
% 6.67/7.05 useparamod = 1
% 6.67/7.05 useeqrefl = 1
% 6.67/7.05 useeqfact = 1
% 6.67/7.05 usefactor = 1
% 6.67/7.05 usesimpsplitting = 0
% 6.67/7.05 usesimpdemod = 5
% 6.67/7.05 usesimpres = 3
% 6.67/7.05
% 6.67/7.05 resimpinuse = 1000
% 6.67/7.05 resimpclauses = 20000
% 6.67/7.05 substype = eqrewr
% 6.67/7.05 backwardsubs = 1
% 6.67/7.05 selectoldest = 5
% 6.67/7.05
% 6.67/7.05 litorderings [0] = split
% 6.67/7.05 litorderings [1] = extend the termordering, first sorting on arguments
% 6.67/7.05
% 6.67/7.05 termordering = kbo
% 6.67/7.05
% 6.67/7.05 litapriori = 0
% 6.67/7.05 termapriori = 1
% 6.67/7.05 litaposteriori = 0
% 6.67/7.05 termaposteriori = 0
% 76.74/77.13 demodaposteriori = 0
% 76.74/77.13 ordereqreflfact = 0
% 76.74/77.13
% 76.74/77.13 litselect = negord
% 76.74/77.13
% 76.74/77.13 maxweight = 15
% 76.74/77.13 maxdepth = 30000
% 76.74/77.13 maxlength = 115
% 76.74/77.13 maxnrvars = 195
% 76.74/77.13 excuselevel = 1
% 76.74/77.13 increasemaxweight = 1
% 76.74/77.13
% 76.74/77.13 maxselected = 10000000
% 76.74/77.13 maxnrclauses = 10000000
% 76.74/77.13
% 76.74/77.13 showgenerated = 0
% 76.74/77.13 showkept = 0
% 76.74/77.13 showselected = 0
% 76.74/77.13 showdeleted = 0
% 76.74/77.13 showresimp = 1
% 76.74/77.13 showstatus = 2000
% 76.74/77.13
% 76.74/77.13 prologoutput = 0
% 76.74/77.13 nrgoals = 5000000
% 76.74/77.13 totalproof = 1
% 76.74/77.13
% 76.74/77.13 Symbols occurring in the translation:
% 76.74/77.13
% 76.74/77.13 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 76.74/77.13 . [1, 2] (w:1, o:24, a:1, s:1, b:0),
% 76.74/77.13 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 76.74/77.13 ! [4, 1] (w:0, o:17, a:1, s:1, b:0),
% 76.74/77.13 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 76.74/77.13 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 76.74/77.13 aInteger0 [36, 1] (w:1, o:22, a:1, s:1, b:0),
% 76.74/77.13 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 76.74/77.13 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 76.74/77.13 smndt0 [39, 1] (w:1, o:23, a:1, s:1, b:0),
% 76.74/77.13 sdtpldt0 [41, 2] (w:1, o:48, a:1, s:1, b:0),
% 76.74/77.13 sdtasdt0 [42, 2] (w:1, o:49, a:1, s:1, b:0),
% 76.74/77.13 aDivisorOf0 [44, 2] (w:1, o:50, a:1, s:1, b:0),
% 76.74/77.13 sdteqdtlpzmzozddtrp0 [45, 3] (w:1, o:54, a:1, s:1, b:0),
% 76.74/77.13 xa [47, 0] (w:1, o:12, a:1, s:1, b:0),
% 76.74/77.13 xb [48, 0] (w:1, o:13, a:1, s:1, b:0),
% 76.74/77.13 xp [49, 0] (w:1, o:14, a:1, s:1, b:0),
% 76.74/77.13 xq [50, 0] (w:1, o:15, a:1, s:1, b:0),
% 76.74/77.13 xm [51, 0] (w:1, o:16, a:1, s:1, b:0),
% 76.74/77.13 alpha1 [52, 2] (w:1, o:51, a:1, s:1, b:1),
% 76.74/77.13 alpha2 [53, 2] (w:1, o:52, a:1, s:1, b:1),
% 76.74/77.13 skol1 [54, 2] (w:1, o:53, a:1, s:1, b:1).
% 76.74/77.13
% 76.74/77.13
% 76.74/77.13 Starting Search:
% 76.74/77.13
% 76.74/77.13 *** allocated 15000 integers for clauses
% 76.74/77.13 *** allocated 22500 integers for clauses
% 76.74/77.13 *** allocated 33750 integers for clauses
% 76.74/77.13 *** allocated 50625 integers for clauses
% 76.74/77.13 *** allocated 75937 integers for clauses
% 76.74/77.13 *** allocated 15000 integers for termspace/termends
% 76.74/77.13 *** allocated 113905 integers for clauses
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 *** allocated 22500 integers for termspace/termends
% 76.74/77.13 *** allocated 170857 integers for clauses
% 76.74/77.13 *** allocated 33750 integers for termspace/termends
% 76.74/77.13
% 76.74/77.13 Intermediate Status:
% 76.74/77.13 Generated: 5322
% 76.74/77.13 Kept: 2002
% 76.74/77.13 Inuse: 140
% 76.74/77.13 Deleted: 7
% 76.74/77.13 Deletedinuse: 5
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 *** allocated 50625 integers for termspace/termends
% 76.74/77.13 *** allocated 256285 integers for clauses
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 *** allocated 75937 integers for termspace/termends
% 76.74/77.13 *** allocated 384427 integers for clauses
% 76.74/77.13
% 76.74/77.13 Intermediate Status:
% 76.74/77.13 Generated: 16658
% 76.74/77.13 Kept: 4047
% 76.74/77.13 Inuse: 276
% 76.74/77.13 Deleted: 11
% 76.74/77.13 Deletedinuse: 6
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 *** allocated 113905 integers for termspace/termends
% 76.74/77.13
% 76.74/77.13 Intermediate Status:
% 76.74/77.13 Generated: 36115
% 76.74/77.13 Kept: 6076
% 76.74/77.13 Inuse: 383
% 76.74/77.13 Deleted: 17
% 76.74/77.13 Deletedinuse: 7
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 *** allocated 576640 integers for clauses
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13
% 76.74/77.13 Intermediate Status:
% 76.74/77.13 Generated: 42915
% 76.74/77.13 Kept: 8078
% 76.74/77.13 Inuse: 415
% 76.74/77.13 Deleted: 17
% 76.74/77.13 Deletedinuse: 7
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 *** allocated 170857 integers for termspace/termends
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 *** allocated 864960 integers for clauses
% 76.74/77.13
% 76.74/77.13 Intermediate Status:
% 76.74/77.13 Generated: 48676
% 76.74/77.13 Kept: 10125
% 76.74/77.13 Inuse: 440
% 76.74/77.13 Deleted: 17
% 76.74/77.13 Deletedinuse: 7
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13
% 76.74/77.13 Intermediate Status:
% 76.74/77.13 Generated: 53815
% 76.74/77.13 Kept: 12256
% 76.74/77.13 Inuse: 471
% 76.74/77.13 Deleted: 17
% 76.74/77.13 Deletedinuse: 7
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13
% 76.74/77.13 Intermediate Status:
% 76.74/77.13 Generated: 60162
% 76.74/77.13 Kept: 14413
% 76.74/77.13 Inuse: 521
% 76.74/77.13 Deleted: 17
% 76.74/77.13 Deletedinuse: 7
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 *** allocated 256285 integers for termspace/termends
% 76.74/77.13 *** allocated 1297440 integers for clauses
% 76.74/77.13
% 76.74/77.13 Intermediate Status:
% 76.74/77.13 Generated: 63884
% 76.74/77.13 Kept: 16446
% 76.74/77.13 Inuse: 541
% 76.74/77.13 Deleted: 17
% 76.74/77.13 Deletedinuse: 7
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13
% 76.74/77.13 Intermediate Status:
% 76.74/77.13 Generated: 68597
% 76.74/77.13 Kept: 18470
% 76.74/77.13 Inuse: 572
% 76.74/77.13 Deleted: 17
% 76.74/77.13 Deletedinuse: 7
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 Resimplifying inuse:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13 Resimplifying clauses:
% 76.74/77.13 Done
% 76.74/77.13
% 76.74/77.13
% 76.74/77.13 Intermediate Status:
% 76.74/77.13 Generated: 74820
% 205.67/206.05 Kept: 21620
% 205.67/206.05 Inuse: 586
% 205.67/206.05 Deleted: 619
% 205.67/206.05 Deletedinuse: 7
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 *** allocated 384427 integers for termspace/termends
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 *** allocated 1946160 integers for clauses
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 79125
% 205.67/206.05 Kept: 24459
% 205.67/206.05 Inuse: 596
% 205.67/206.05 Deleted: 619
% 205.67/206.05 Deletedinuse: 7
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 82629
% 205.67/206.05 Kept: 26529
% 205.67/206.05 Inuse: 611
% 205.67/206.05 Deleted: 619
% 205.67/206.05 Deletedinuse: 7
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 86635
% 205.67/206.05 Kept: 28637
% 205.67/206.05 Inuse: 626
% 205.67/206.05 Deleted: 620
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 90878
% 205.67/206.05 Kept: 30762
% 205.67/206.05 Inuse: 639
% 205.67/206.05 Deleted: 620
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 95185
% 205.67/206.05 Kept: 33061
% 205.67/206.05 Inuse: 651
% 205.67/206.05 Deleted: 620
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 *** allocated 576640 integers for termspace/termends
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 100003
% 205.67/206.05 Kept: 35196
% 205.67/206.05 Inuse: 671
% 205.67/206.05 Deleted: 620
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 *** allocated 2919240 integers for clauses
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 109110
% 205.67/206.05 Kept: 37436
% 205.67/206.05 Inuse: 706
% 205.67/206.05 Deleted: 625
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 118050
% 205.67/206.05 Kept: 39709
% 205.67/206.05 Inuse: 746
% 205.67/206.05 Deleted: 625
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying clauses:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 122958
% 205.67/206.05 Kept: 41879
% 205.67/206.05 Inuse: 776
% 205.67/206.05 Deleted: 840
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 127517
% 205.67/206.05 Kept: 44092
% 205.67/206.05 Inuse: 806
% 205.67/206.05 Deleted: 840
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 149197
% 205.67/206.05 Kept: 46247
% 205.67/206.05 Inuse: 909
% 205.67/206.05 Deleted: 840
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 157775
% 205.67/206.05 Kept: 48273
% 205.67/206.05 Inuse: 932
% 205.67/206.05 Deleted: 840
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 *** allocated 864960 integers for termspace/termends
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 165444
% 205.67/206.05 Kept: 50407
% 205.67/206.05 Inuse: 948
% 205.67/206.05 Deleted: 840
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 172226
% 205.67/206.05 Kept: 52421
% 205.67/206.05 Inuse: 963
% 205.67/206.05 Deleted: 840
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 *** allocated 4378860 integers for clauses
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 178768
% 205.67/206.05 Kept: 54433
% 205.67/206.05 Inuse: 978
% 205.67/206.05 Deleted: 840
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 185386
% 205.67/206.05 Kept: 56434
% 205.67/206.05 Inuse: 993
% 205.67/206.05 Deleted: 840
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 192505
% 205.67/206.05 Kept: 58590
% 205.67/206.05 Inuse: 1009
% 205.67/206.05 Deleted: 840
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying clauses:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 199843
% 205.67/206.05 Kept: 60995
% 205.67/206.05 Inuse: 1023
% 205.67/206.05 Deleted: 1737
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 207486
% 205.67/206.05 Kept: 63024
% 205.67/206.05 Inuse: 1041
% 205.67/206.05 Deleted: 1737
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 214818
% 205.67/206.05 Kept: 65200
% 205.67/206.05 Inuse: 1056
% 205.67/206.05 Deleted: 1737
% 205.67/206.05 Deletedinuse: 8
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 223857
% 205.67/206.05 Kept: 67634
% 205.67/206.05 Inuse: 1091
% 205.67/206.05 Deleted: 1738
% 205.67/206.05 Deletedinuse: 9
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05 Resimplifying inuse:
% 205.67/206.05 Done
% 205.67/206.05
% 205.67/206.05
% 205.67/206.05 Intermediate Status:
% 205.67/206.05 Generated: 229402
% 205.67/206.05 Kept: 70070
% 205.67/206.05 Inuse: 1116
% 277.15/277.60 Deleted: 1738
% 277.15/277.60 Deletedinuse: 9
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 239661
% 277.15/277.60 Kept: 72133
% 277.15/277.60 Inuse: 1161
% 277.15/277.60 Deleted: 1738
% 277.15/277.60 Deletedinuse: 9
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 252958
% 277.15/277.60 Kept: 74207
% 277.15/277.60 Inuse: 1211
% 277.15/277.60 Deleted: 1766
% 277.15/277.60 Deletedinuse: 37
% 277.15/277.60
% 277.15/277.60 *** allocated 1297440 integers for termspace/termends
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 264033
% 277.15/277.60 Kept: 76361
% 277.15/277.60 Inuse: 1243
% 277.15/277.60 Deleted: 1876
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 *** allocated 6568290 integers for clauses
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 282153
% 277.15/277.60 Kept: 78545
% 277.15/277.60 Inuse: 1287
% 277.15/277.60 Deleted: 1900
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 289931
% 277.15/277.60 Kept: 80666
% 277.15/277.60 Inuse: 1322
% 277.15/277.60 Deleted: 1900
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying clauses:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 310030
% 277.15/277.60 Kept: 82840
% 277.15/277.60 Inuse: 1342
% 277.15/277.60 Deleted: 16685
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 319776
% 277.15/277.60 Kept: 85129
% 277.15/277.60 Inuse: 1408
% 277.15/277.60 Deleted: 16685
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 346153
% 277.15/277.60 Kept: 87133
% 277.15/277.60 Inuse: 1568
% 277.15/277.60 Deleted: 16688
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 393870
% 277.15/277.60 Kept: 89472
% 277.15/277.60 Inuse: 1839
% 277.15/277.60 Deleted: 16688
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 405838
% 277.15/277.60 Kept: 91499
% 277.15/277.60 Inuse: 1889
% 277.15/277.60 Deleted: 16688
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 412460
% 277.15/277.60 Kept: 93712
% 277.15/277.60 Inuse: 1913
% 277.15/277.60 Deleted: 16688
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 423088
% 277.15/277.60 Kept: 95719
% 277.15/277.60 Inuse: 1925
% 277.15/277.60 Deleted: 16688
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 432201
% 277.15/277.60 Kept: 97849
% 277.15/277.60 Inuse: 1936
% 277.15/277.60 Deleted: 16688
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 437814
% 277.15/277.60 Kept: 100110
% 277.15/277.60 Inuse: 1945
% 277.15/277.60 Deleted: 16688
% 277.15/277.60 Deletedinuse: 147
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying clauses:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 466830
% 277.15/277.60 Kept: 103401
% 277.15/277.60 Inuse: 1971
% 277.15/277.60 Deleted: 37141
% 277.15/277.60 Deletedinuse: 149
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 483451
% 277.15/277.60 Kept: 105615
% 277.15/277.60 Inuse: 2038
% 277.15/277.60 Deleted: 37316
% 277.15/277.60 Deletedinuse: 324
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 502683
% 277.15/277.60 Kept: 107719
% 277.15/277.60 Inuse: 2129
% 277.15/277.60 Deleted: 37317
% 277.15/277.60 Deletedinuse: 325
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 511673
% 277.15/277.60 Kept: 110314
% 277.15/277.60 Inuse: 2154
% 277.15/277.60 Deleted: 37317
% 277.15/277.60 Deletedinuse: 325
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 *** allocated 1946160 integers for termspace/termends
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 518711
% 277.15/277.60 Kept: 112458
% 277.15/277.60 Inuse: 2174
% 277.15/277.60 Deleted: 37317
% 277.15/277.60 Deletedinuse: 325
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 536418
% 277.15/277.60 Kept: 114464
% 277.15/277.60 Inuse: 2236
% 277.15/277.60 Deleted: 37401
% 277.15/277.60 Deletedinuse: 406
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 560410
% 277.15/277.60 Kept: 116699
% 277.15/277.60 Inuse: 2313
% 277.15/277.60 Deleted: 37555
% 277.15/277.60 Deletedinuse: 547
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 *** allocated 9852435 integers for clauses
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 567475
% 277.15/277.60 Kept: 118911
% 277.15/277.60 Inuse: 2331
% 277.15/277.60 Deleted: 37564
% 277.15/277.60 Deletedinuse: 547
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 573756
% 277.15/277.60 Kept: 121015
% 277.15/277.60 Inuse: 2342
% 277.15/277.60 Deleted: 37572
% 277.15/277.60 Deletedinuse: 547
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 589134
% 277.15/277.60 Kept: 123015
% 277.15/277.60 Inuse: 2499
% 277.15/277.60 Deleted: 37613
% 277.15/277.60 Deletedinuse: 547
% 277.15/277.60
% 277.15/277.60 Resimplifying clauses:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 615613
% 277.15/277.60 Kept: 126972
% 277.15/277.60 Inuse: 2558
% 277.15/277.60 Deleted: 57795
% 277.15/277.60 Deletedinuse: 547
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 654089
% 277.15/277.60 Kept: 129131
% 277.15/277.60 Inuse: 2703
% 277.15/277.60 Deleted: 57796
% 277.15/277.60 Deletedinuse: 548
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 704934
% 277.15/277.60 Kept: 131161
% 277.15/277.60 Inuse: 2876
% 277.15/277.60 Deleted: 57796
% 277.15/277.60 Deletedinuse: 548
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 719305
% 277.15/277.60 Kept: 133269
% 277.15/277.60 Inuse: 2899
% 277.15/277.60 Deleted: 57800
% 277.15/277.60 Deletedinuse: 548
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 734126
% 277.15/277.60 Kept: 135353
% 277.15/277.60 Inuse: 2950
% 277.15/277.60 Deleted: 57800
% 277.15/277.60 Deletedinuse: 548
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 744043
% 277.15/277.60 Kept: 137354
% 277.15/277.60 Inuse: 2964
% 277.15/277.60 Deleted: 57800
% 277.15/277.60 Deletedinuse: 548
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 754121
% 277.15/277.60 Kept: 139432
% 277.15/277.60 Inuse: 2978
% 277.15/277.60 Deleted: 57803
% 277.15/277.60 Deletedinuse: 548
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 765309
% 277.15/277.60 Kept: 141513
% 277.15/277.60 Inuse: 2994
% 277.15/277.60 Deleted: 57803
% 277.15/277.60 Deletedinuse: 548
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 775277
% 277.15/277.60 Kept: 143568
% 277.15/277.60 Inuse: 3008
% 277.15/277.60 Deleted: 57803
% 277.15/277.60 Deletedinuse: 548
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60
% 277.15/277.60 Intermediate Status:
% 277.15/277.60 Generated: 786148
% 277.15/277.60 Kept: 145594
% 277.15/277.60 Inuse: 3024
% 277.15/277.60 Deleted: 57803
% 277.15/277.60 Deletedinuse: 548
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying inuse:
% 277.15/277.60 Done
% 277.15/277.60
% 277.15/277.60 Resimplifying clauses:
% 277.15/277.60
% 277.15/277.60 Bliksems!, er is een bewijs:
% 277.15/277.60 % SZS status Theorem
% 277.15/277.60 % SZS output start Refutation
% 277.15/277.60
% 277.15/277.60 (1) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz00 ) }.
% 277.15/277.60 (2) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz10 ) }.
% 277.15/277.60 (3) {G0,W5,D3,L2,V1,M2} I { ! aInteger0( X ), aInteger0( smndt0( X ) ) }.
% 277.15/277.60 (5) {G0,W8,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y ), aInteger0(
% 277.15/277.60 sdtasdt0( X, Y ) ) }.
% 277.15/277.60 (7) {G0,W11,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y ), sdtpldt0(
% 277.15/277.60 X, Y ) = sdtpldt0( Y, X ) }.
% 277.15/277.60 (14) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X, sz10 ) ==> X
% 277.15/277.60 }.
% 277.15/277.60 (18) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X, sz00 ) ==> sz00
% 277.15/277.60 }.
% 277.15/277.60 (25) {G0,W10,D2,L4,V2,M4} I { ! aInteger0( X ), ! aInteger0( Y ), ! alpha1
% 277.15/277.60 ( X, Y ), aDivisorOf0( Y, X ) }.
% 277.15/277.60 (27) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), alpha2( X, Y ) }.
% 277.15/277.60 (28) {G0,W9,D2,L3,V2,M3} I { Y = sz00, ! alpha2( X, Y ), alpha1( X, Y ) }.
% 277.15/277.60 (29) {G0,W7,D3,L2,V4,M2} I { ! alpha2( X, Y ), aInteger0( skol1( Z, T ) )
% 277.15/277.60 }.
% 277.15/277.60 (30) {G0,W10,D4,L2,V2,M2} I { ! alpha2( X, Y ), sdtasdt0( Y, skol1( X, Y )
% 277.15/277.60 ) ==> X }.
% 277.15/277.60 (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y, Z ) = X,
% 277.15/277.60 alpha2( X, Y ) }.
% 277.15/277.60 (33) {G0,W19,D4,L6,V3,M6} I { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.60 aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y ) ) )
% 277.15/277.60 , sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 277.15/277.60 (37) {G0,W2,D2,L1,V0,M1} I { aInteger0( xa ) }.
% 277.15/277.60 (38) {G0,W2,D2,L1,V0,M1} I { aInteger0( xb ) }.
% 277.15/277.60 (39) {G0,W2,D2,L1,V0,M1} I { aInteger0( xp ) }.
% 277.15/277.60 (40) {G0,W3,D2,L1,V0,M1} I { ! xp ==> sz00 }.
% 277.15/277.60 (41) {G0,W2,D2,L1,V0,M1} I { aInteger0( xq ) }.
% 277.15/277.60 (42) {G0,W3,D2,L1,V0,M1} I { ! xq ==> sz00 }.
% 277.15/277.60 (44) {G0,W2,D2,L1,V0,M1} I { aInteger0( xm ) }.
% 277.15/277.60 (46) {G0,W10,D4,L1,V0,M1} I { sdtasdt0( xp, sdtasdt0( xq, xm ) ) ==>
% 277.15/277.60 sdtpldt0( xa, smndt0( xb ) ) }.
% 277.15/277.60 (47) {G0,W10,D4,L1,V0,M1} I { sdtasdt0( xq, sdtasdt0( xp, xm ) ) ==>
% 277.15/277.60 sdtpldt0( xa, smndt0( xb ) ) }.
% 277.15/277.60 (48) {G0,W8,D2,L2,V0,M2} I { ! sdteqdtlpzmzozddtrp0( xa, xb, xp ), !
% 277.15/277.60 sdteqdtlpzmzozddtrp0( xa, xb, xq ) }.
% 277.15/277.61 (90) {G1,W3,D3,L1,V0,M1} R(3,38) { aInteger0( smndt0( xb ) ) }.
% 277.15/277.61 (160) {G1,W6,D3,L2,V1,M2} R(5,39) { ! aInteger0( X ), aInteger0( sdtasdt0(
% 277.15/277.61 xp, X ) ) }.
% 277.15/277.61 (162) {G1,W6,D3,L2,V1,M2} R(5,41) { ! aInteger0( X ), aInteger0( sdtasdt0(
% 277.15/277.61 xq, X ) ) }.
% 277.15/277.61 (294) {G2,W11,D4,L2,V1,M2} R(7,90) { ! aInteger0( X ), sdtpldt0( smndt0( xb
% 277.15/277.61 ), X ) = sdtpldt0( X, smndt0( xb ) ) }.
% 277.15/277.61 (682) {G1,W5,D3,L1,V0,M1} R(14,39) { sdtasdt0( xp, sz10 ) ==> xp }.
% 277.15/277.61 (683) {G1,W5,D3,L1,V0,M1} R(14,41) { sdtasdt0( xq, sz10 ) ==> xq }.
% 277.15/277.61 (901) {G1,W5,D3,L1,V0,M1} R(18,44) { sdtasdt0( xm, sz00 ) ==> sz00 }.
% 277.15/277.61 (1661) {G1,W6,D2,L2,V1,M2} P(28,40);q { ! alpha2( X, xp ), alpha1( X, xp )
% 277.15/277.61 }.
% 277.15/277.61 (1662) {G1,W6,D2,L2,V1,M2} P(28,42);q { ! alpha2( X, xq ), alpha1( X, xq )
% 277.15/277.61 }.
% 277.15/277.61 (1886) {G2,W6,D2,L2,V1,M2} P(901,31);r(1) { ! sz00 = X, alpha2( X, xm ) }.
% 277.15/277.61 (1895) {G2,W6,D2,L2,V1,M2} P(683,31);r(2) { ! xq = X, alpha2( X, xq ) }.
% 277.15/277.61 (1896) {G2,W6,D2,L2,V1,M2} P(682,31);r(2) { ! xp = X, alpha2( X, xp ) }.
% 277.15/277.61 (1940) {G3,W3,D2,L1,V0,M1} Q(1886) { alpha2( sz00, xm ) }.
% 277.15/277.61 (2000) {G4,W4,D3,L1,V2,M1} R(1940,29) { aInteger0( skol1( X, Y ) ) }.
% 277.15/277.61 (2797) {G1,W13,D4,L3,V1,M3} P(46,31) { ! aInteger0( sdtasdt0( xq, xm ) ), !
% 277.15/277.61 sdtpldt0( xa, smndt0( xb ) ) = X, alpha2( X, xp ) }.
% 277.15/277.61 (2808) {G2,W10,D4,L2,V0,M2} Q(2797) { ! aInteger0( sdtasdt0( xq, xm ) ),
% 277.15/277.61 alpha2( sdtpldt0( xa, smndt0( xb ) ), xp ) }.
% 277.15/277.61 (2817) {G1,W13,D4,L3,V1,M3} P(47,31) { ! aInteger0( sdtasdt0( xp, xm ) ), !
% 277.15/277.61 sdtpldt0( xa, smndt0( xb ) ) = X, alpha2( X, xq ) }.
% 277.15/277.61 (2827) {G2,W10,D4,L2,V0,M2} Q(2817) { ! aInteger0( sdtasdt0( xp, xm ) ),
% 277.15/277.61 alpha2( sdtpldt0( xa, smndt0( xb ) ), xq ) }.
% 277.15/277.61 (2886) {G1,W17,D4,L5,V0,M5} R(48,33);r(37) { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.15/277.61 , xp ), ! aInteger0( xb ), ! aInteger0( xq ), xq ==> sz00, ! aDivisorOf0
% 277.15/277.61 ( xq, sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.15/277.61 (20068) {G2,W10,D4,L2,V0,M2} S(2886);r(38);r(41);r(42) { !
% 277.15/277.61 sdteqdtlpzmzozddtrp0( xa, xb, xp ), ! aDivisorOf0( xq, sdtpldt0( xa,
% 277.15/277.61 smndt0( xb ) ) ) }.
% 277.15/277.61 (30287) {G2,W4,D3,L1,V0,M1} R(160,44) { aInteger0( sdtasdt0( xp, xm ) ) }.
% 277.15/277.61 (30288) {G5,W5,D2,L2,V1,M2} P(30,160);r(2000) { aInteger0( X ), ! alpha2( X
% 277.15/277.61 , xp ) }.
% 277.15/277.61 (30700) {G6,W5,D2,L2,V1,M2} R(30288,1896) { aInteger0( X ), ! xp = X }.
% 277.15/277.61 (30736) {G6,W5,D2,L2,V1,M2} R(30288,27) { aInteger0( X ), ! alpha1( X, xp )
% 277.15/277.61 }.
% 277.15/277.61 (30853) {G7,W11,D2,L4,V2,M4} R(30700,25) { ! xp = X, ! aInteger0( Y ), !
% 277.15/277.61 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.15/277.61 (30875) {G8,W6,D2,L2,V1,M2} Q(30853);r(30736) { ! alpha1( X, xp ),
% 277.15/277.61 aDivisorOf0( xp, X ) }.
% 277.15/277.61 (32071) {G2,W4,D3,L1,V0,M1} R(162,44) { aInteger0( sdtasdt0( xq, xm ) ) }.
% 277.15/277.61 (32072) {G5,W5,D2,L2,V1,M2} P(30,162);r(2000) { aInteger0( X ), ! alpha2( X
% 277.15/277.61 , xq ) }.
% 277.15/277.61 (32360) {G6,W5,D2,L2,V1,M2} R(32072,1895) { aInteger0( X ), ! xq = X }.
% 277.15/277.61 (32396) {G6,W5,D2,L2,V1,M2} R(32072,27) { aInteger0( X ), ! alpha1( X, xq )
% 277.15/277.61 }.
% 277.15/277.61 (32515) {G7,W11,D2,L4,V2,M4} R(32360,25) { ! xq = X, ! aInteger0( Y ), !
% 277.15/277.61 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.15/277.61 (32537) {G8,W6,D2,L2,V1,M2} Q(32515);r(32396) { ! alpha1( X, xq ),
% 277.15/277.61 aDivisorOf0( xq, X ) }.
% 277.15/277.61 (40431) {G3,W6,D4,L1,V0,M1} S(2827);r(30287) { alpha2( sdtpldt0( xa, smndt0
% 277.15/277.61 ( xb ) ), xq ) }.
% 277.15/277.61 (40433) {G3,W6,D4,L1,V0,M1} S(2808);r(32071) { alpha2( sdtpldt0( xa, smndt0
% 277.15/277.61 ( xb ) ), xp ) }.
% 277.15/277.61 (73587) {G3,W9,D4,L1,V0,M1} R(294,37) { sdtpldt0( xa, smndt0( xb ) ) ==>
% 277.15/277.61 sdtpldt0( smndt0( xb ), xa ) }.
% 277.15/277.61 (78712) {G9,W6,D2,L2,V1,M2} R(1661,30875) { ! alpha2( X, xp ), aDivisorOf0
% 277.15/277.61 ( xp, X ) }.
% 277.15/277.61 (79620) {G9,W6,D2,L2,V1,M2} R(1662,32537) { ! alpha2( X, xq ), aDivisorOf0
% 277.15/277.61 ( xq, X ) }.
% 277.15/277.61 (81893) {G4,W6,D4,L1,V0,M1} S(40431);d(73587) { alpha2( sdtpldt0( smndt0(
% 277.15/277.61 xb ), xa ), xq ) }.
% 277.15/277.61 (81895) {G4,W6,D4,L1,V0,M1} S(40433);d(73587) { alpha2( sdtpldt0( smndt0(
% 277.15/277.61 xb ), xa ), xp ) }.
% 277.15/277.61 (81901) {G4,W10,D4,L2,V0,M2} S(20068);d(73587) { ! sdteqdtlpzmzozddtrp0( xa
% 277.15/277.61 , xb, xp ), ! aDivisorOf0( xq, sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.15/277.61 (122652) {G10,W6,D4,L1,V0,M1} R(81893,79620) { aDivisorOf0( xq, sdtpldt0(
% 277.15/277.61 smndt0( xb ), xa ) ) }.
% 277.15/277.61 (122787) {G10,W6,D4,L1,V0,M1} R(81895,78712) { aDivisorOf0( xp, sdtpldt0(
% 277.15/277.61 smndt0( xb ), xa ) ) }.
% 277.15/277.61 (126029) {G11,W4,D2,L1,V0,M1} S(81901);r(122652) { ! sdteqdtlpzmzozddtrp0(
% 277.15/277.61 xa, xb, xp ) }.
% 277.15/277.61 (127009) {G12,W13,D4,L4,V0,M4} R(126029,33);d(73587);r(37) { ! aInteger0(
% 277.15/277.61 xb ), ! aInteger0( xp ), xp ==> sz00, ! aDivisorOf0( xp, sdtpldt0( smndt0
% 277.15/277.61 ( xb ), xa ) ) }.
% 277.15/277.61 (147236) {G13,W0,D0,L0,V0,M0} S(127009);r(38);r(39);r(40);r(122787) { }.
% 277.15/277.61
% 277.15/277.61
% 277.15/277.61 % SZS output end Refutation
% 277.15/277.61 found a proof!
% 277.15/277.61
% 277.15/277.61
% 277.15/277.61 Unprocessed initial clauses:
% 277.15/277.61
% 277.15/277.61 (147238) {G0,W1,D1,L1,V0,M1} { && }.
% 277.15/277.61 (147239) {G0,W2,D2,L1,V0,M1} { aInteger0( sz00 ) }.
% 277.15/277.61 (147240) {G0,W2,D2,L1,V0,M1} { aInteger0( sz10 ) }.
% 277.15/277.61 (147241) {G0,W5,D3,L2,V1,M2} { ! aInteger0( X ), aInteger0( smndt0( X ) )
% 277.15/277.61 }.
% 277.15/277.61 (147242) {G0,W8,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y ),
% 277.15/277.61 aInteger0( sdtpldt0( X, Y ) ) }.
% 277.15/277.61 (147243) {G0,W8,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y ),
% 277.15/277.61 aInteger0( sdtasdt0( X, Y ) ) }.
% 277.15/277.61 (147244) {G0,W17,D4,L4,V3,M4} { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.61 aInteger0( Z ), sdtpldt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtpldt0( X,
% 277.15/277.61 Y ), Z ) }.
% 277.15/277.61 (147245) {G0,W11,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y ),
% 277.15/277.61 sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 277.15/277.61 (147246) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sdtpldt0( X, sz00 ) = X
% 277.15/277.61 }.
% 277.15/277.61 (147247) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), X = sdtpldt0( sz00, X )
% 277.15/277.61 }.
% 277.15/277.61 (147248) {G0,W8,D4,L2,V1,M2} { ! aInteger0( X ), sdtpldt0( X, smndt0( X )
% 277.15/277.61 ) = sz00 }.
% 277.15/277.61 (147249) {G0,W8,D4,L2,V1,M2} { ! aInteger0( X ), sz00 = sdtpldt0( smndt0(
% 277.15/277.61 X ), X ) }.
% 277.15/277.61 (147250) {G0,W17,D4,L4,V3,M4} { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.61 aInteger0( Z ), sdtasdt0( X, sdtasdt0( Y, Z ) ) = sdtasdt0( sdtasdt0( X,
% 277.15/277.61 Y ), Z ) }.
% 277.15/277.61 (147251) {G0,W11,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y ),
% 277.15/277.61 sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 277.15/277.61 (147252) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sdtasdt0( X, sz10 ) = X
% 277.15/277.61 }.
% 277.15/277.61 (147253) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), X = sdtasdt0( sz10, X )
% 277.15/277.61 }.
% 277.15/277.61 (147254) {G0,W19,D4,L4,V3,M4} { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.61 aInteger0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X,
% 277.15/277.61 Y ), sdtasdt0( X, Z ) ) }.
% 277.15/277.61 (147255) {G0,W19,D4,L4,V3,M4} { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.61 aInteger0( Z ), sdtasdt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( sdtasdt0( X,
% 277.15/277.61 Z ), sdtasdt0( Y, Z ) ) }.
% 277.15/277.61 (147256) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sdtasdt0( X, sz00 ) =
% 277.15/277.61 sz00 }.
% 277.15/277.61 (147257) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sz00 = sdtasdt0( sz00, X
% 277.15/277.61 ) }.
% 277.15/277.61 (147258) {G0,W9,D4,L2,V1,M2} { ! aInteger0( X ), sdtasdt0( smndt0( sz10 )
% 277.15/277.61 , X ) = smndt0( X ) }.
% 277.15/277.61 (147259) {G0,W9,D4,L2,V1,M2} { ! aInteger0( X ), smndt0( X ) = sdtasdt0( X
% 277.15/277.61 , smndt0( sz10 ) ) }.
% 277.15/277.61 (147260) {G0,W15,D3,L5,V2,M5} { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.61 sdtasdt0( X, Y ) = sz00, X = sz00, Y = sz00 }.
% 277.15/277.61 (147261) {G0,W7,D2,L3,V2,M3} { ! aInteger0( X ), ! aDivisorOf0( Y, X ),
% 277.15/277.61 aInteger0( Y ) }.
% 277.15/277.61 (147262) {G0,W8,D2,L3,V2,M3} { ! aInteger0( X ), ! aDivisorOf0( Y, X ),
% 277.15/277.61 alpha1( X, Y ) }.
% 277.15/277.61 (147263) {G0,W10,D2,L4,V2,M4} { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.61 alpha1( X, Y ), aDivisorOf0( Y, X ) }.
% 277.15/277.61 (147264) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), ! Y = sz00 }.
% 277.15/277.61 (147265) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), alpha2( X, Y ) }.
% 277.15/277.61 (147266) {G0,W9,D2,L3,V2,M3} { Y = sz00, ! alpha2( X, Y ), alpha1( X, Y )
% 277.15/277.61 }.
% 277.15/277.61 (147267) {G0,W7,D3,L2,V4,M2} { ! alpha2( X, Y ), aInteger0( skol1( Z, T )
% 277.15/277.61 ) }.
% 277.15/277.61 (147268) {G0,W10,D4,L2,V2,M2} { ! alpha2( X, Y ), sdtasdt0( Y, skol1( X, Y
% 277.15/277.61 ) ) = X }.
% 277.15/277.61 (147269) {G0,W10,D3,L3,V3,M3} { ! aInteger0( Z ), ! sdtasdt0( Y, Z ) = X,
% 277.15/277.61 alpha2( X, Y ) }.
% 277.15/277.61 (147270) {G0,W19,D4,L6,V3,M6} { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.61 aInteger0( Z ), Z = sz00, ! sdteqdtlpzmzozddtrp0( X, Y, Z ), aDivisorOf0
% 277.15/277.61 ( Z, sdtpldt0( X, smndt0( Y ) ) ) }.
% 277.15/277.61 (147271) {G0,W19,D4,L6,V3,M6} { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.61 aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y ) ) )
% 277.15/277.61 , sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 277.15/277.61 (147272) {G0,W11,D2,L4,V2,M4} { ! aInteger0( X ), ! aInteger0( Y ), Y =
% 277.15/277.61 sz00, sdteqdtlpzmzozddtrp0( X, X, Y ) }.
% 277.15/277.61 (147273) {G0,W17,D2,L6,V3,M6} { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.61 aInteger0( Z ), Z = sz00, ! sdteqdtlpzmzozddtrp0( X, Y, Z ),
% 277.15/277.61 sdteqdtlpzmzozddtrp0( Y, X, Z ) }.
% 277.15/277.61 (147274) {G0,W23,D2,L8,V4,M8} { ! aInteger0( X ), ! aInteger0( Y ), !
% 277.15/277.61 aInteger0( Z ), Z = sz00, ! aInteger0( T ), ! sdteqdtlpzmzozddtrp0( X, Y
% 277.15/277.61 , Z ), ! sdteqdtlpzmzozddtrp0( Y, T, Z ), sdteqdtlpzmzozddtrp0( X, T, Z )
% 277.15/277.61 }.
% 277.15/277.61 (147275) {G0,W2,D2,L1,V0,M1} { aInteger0( xa ) }.
% 277.15/277.61 (147276) {G0,W2,D2,L1,V0,M1} { aInteger0( xb ) }.
% 277.15/277.61 (147277) {G0,W2,D2,L1,V0,M1} { aInteger0( xp ) }.
% 277.15/277.61 (147278) {G0,W3,D2,L1,V0,M1} { ! xp = sz00 }.
% 277.15/277.61 (147279) {G0,W2,D2,L1,V0,M1} { aInteger0( xq ) }.
% 277.15/277.61 (147280) {G0,W3,D2,L1,V0,M1} { ! xq = sz00 }.
% 277.15/277.61 (147281) {G0,W6,D3,L1,V0,M1} { sdteqdtlpzmzozddtrp0( xa, xb, sdtasdt0( xp
% 277.15/277.61 , xq ) ) }.
% 277.15/277.61 (147282) {G0,W2,D2,L1,V0,M1} { aInteger0( xm ) }.
% 277.15/277.61 (147283) {G0,W10,D4,L1,V0,M1} { sdtasdt0( sdtasdt0( xp, xq ), xm ) =
% 277.15/277.61 sdtpldt0( xa, smndt0( xb ) ) }.
% 277.15/277.61 (147284) {G0,W10,D4,L1,V0,M1} { sdtasdt0( xp, sdtasdt0( xq, xm ) ) =
% 277.15/277.61 sdtpldt0( xa, smndt0( xb ) ) }.
% 277.15/277.61 (147285) {G0,W10,D4,L1,V0,M1} { sdtpldt0( xa, smndt0( xb ) ) = sdtasdt0(
% 277.15/277.61 xq, sdtasdt0( xp, xm ) ) }.
% 277.15/277.61 (147286) {G0,W8,D2,L2,V0,M2} { ! sdteqdtlpzmzozddtrp0( xa, xb, xp ), !
% 277.15/277.61 sdteqdtlpzmzozddtrp0( xa, xb, xq ) }.
% 277.15/277.61
% 277.15/277.61
% 277.15/277.61 Total Proof:
% 277.15/277.61
% 277.15/277.61 subsumption: (1) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz00 ) }.
% 277.15/277.61 parent0: (147239) {G0,W2,D2,L1,V0,M1} { aInteger0( sz00 ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (2) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz10 ) }.
% 277.15/277.61 parent0: (147240) {G0,W2,D2,L1,V0,M1} { aInteger0( sz10 ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (3) {G0,W5,D3,L2,V1,M2} I { ! aInteger0( X ), aInteger0(
% 277.15/277.61 smndt0( X ) ) }.
% 277.15/277.61 parent0: (147241) {G0,W5,D3,L2,V1,M2} { ! aInteger0( X ), aInteger0(
% 277.15/277.61 smndt0( X ) ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (5) {G0,W8,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y )
% 277.15/277.61 , aInteger0( sdtasdt0( X, Y ) ) }.
% 277.15/277.61 parent0: (147243) {G0,W8,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y )
% 277.15/277.61 , aInteger0( sdtasdt0( X, Y ) ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 Y := Y
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 2 ==> 2
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (7) {G0,W11,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y
% 277.15/277.61 ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 277.15/277.61 parent0: (147245) {G0,W11,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y
% 277.15/277.61 ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 Y := Y
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 2 ==> 2
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (14) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X,
% 277.15/277.61 sz10 ) ==> X }.
% 277.15/277.61 parent0: (147252) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sdtasdt0( X,
% 277.15/277.61 sz10 ) = X }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (18) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X,
% 277.15/277.61 sz00 ) ==> sz00 }.
% 277.15/277.61 parent0: (147256) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sdtasdt0( X,
% 277.15/277.61 sz00 ) = sz00 }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (25) {G0,W10,D2,L4,V2,M4} I { ! aInteger0( X ), ! aInteger0( Y
% 277.15/277.61 ), ! alpha1( X, Y ), aDivisorOf0( Y, X ) }.
% 277.15/277.61 parent0: (147263) {G0,W10,D2,L4,V2,M4} { ! aInteger0( X ), ! aInteger0( Y
% 277.15/277.61 ), ! alpha1( X, Y ), aDivisorOf0( Y, X ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 Y := Y
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 2 ==> 2
% 277.15/277.61 3 ==> 3
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (27) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), alpha2( X, Y )
% 277.15/277.61 }.
% 277.15/277.61 parent0: (147265) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), alpha2( X, Y )
% 277.15/277.61 }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 Y := Y
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (28) {G0,W9,D2,L3,V2,M3} I { Y = sz00, ! alpha2( X, Y ),
% 277.15/277.61 alpha1( X, Y ) }.
% 277.15/277.61 parent0: (147266) {G0,W9,D2,L3,V2,M3} { Y = sz00, ! alpha2( X, Y ), alpha1
% 277.15/277.61 ( X, Y ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 Y := Y
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 2 ==> 2
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (29) {G0,W7,D3,L2,V4,M2} I { ! alpha2( X, Y ), aInteger0(
% 277.15/277.61 skol1( Z, T ) ) }.
% 277.15/277.61 parent0: (147267) {G0,W7,D3,L2,V4,M2} { ! alpha2( X, Y ), aInteger0( skol1
% 277.15/277.61 ( Z, T ) ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 Y := Y
% 277.15/277.61 Z := Z
% 277.15/277.61 T := T
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (30) {G0,W10,D4,L2,V2,M2} I { ! alpha2( X, Y ), sdtasdt0( Y,
% 277.15/277.61 skol1( X, Y ) ) ==> X }.
% 277.15/277.61 parent0: (147268) {G0,W10,D4,L2,V2,M2} { ! alpha2( X, Y ), sdtasdt0( Y,
% 277.15/277.61 skol1( X, Y ) ) = X }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 Y := Y
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y
% 277.15/277.61 , Z ) = X, alpha2( X, Y ) }.
% 277.15/277.61 parent0: (147269) {G0,W10,D3,L3,V3,M3} { ! aInteger0( Z ), ! sdtasdt0( Y,
% 277.15/277.61 Z ) = X, alpha2( X, Y ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 Y := Y
% 277.15/277.61 Z := Z
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 2 ==> 2
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (33) {G0,W19,D4,L6,V3,M6} I { ! aInteger0( X ), ! aInteger0( Y
% 277.15/277.61 ), ! aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y
% 277.15/277.61 ) ) ), sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 277.15/277.61 parent0: (147271) {G0,W19,D4,L6,V3,M6} { ! aInteger0( X ), ! aInteger0( Y
% 277.15/277.61 ), ! aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y
% 277.15/277.61 ) ) ), sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 Y := Y
% 277.15/277.61 Z := Z
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 2 ==> 2
% 277.15/277.61 3 ==> 3
% 277.15/277.61 4 ==> 4
% 277.15/277.61 5 ==> 5
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (37) {G0,W2,D2,L1,V0,M1} I { aInteger0( xa ) }.
% 277.15/277.61 parent0: (147275) {G0,W2,D2,L1,V0,M1} { aInteger0( xa ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (38) {G0,W2,D2,L1,V0,M1} I { aInteger0( xb ) }.
% 277.15/277.61 parent0: (147276) {G0,W2,D2,L1,V0,M1} { aInteger0( xb ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (39) {G0,W2,D2,L1,V0,M1} I { aInteger0( xp ) }.
% 277.15/277.61 parent0: (147277) {G0,W2,D2,L1,V0,M1} { aInteger0( xp ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (40) {G0,W3,D2,L1,V0,M1} I { ! xp ==> sz00 }.
% 277.15/277.61 parent0: (147278) {G0,W3,D2,L1,V0,M1} { ! xp = sz00 }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (41) {G0,W2,D2,L1,V0,M1} I { aInteger0( xq ) }.
% 277.15/277.61 parent0: (147279) {G0,W2,D2,L1,V0,M1} { aInteger0( xq ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (42) {G0,W3,D2,L1,V0,M1} I { ! xq ==> sz00 }.
% 277.15/277.61 parent0: (147280) {G0,W3,D2,L1,V0,M1} { ! xq = sz00 }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (44) {G0,W2,D2,L1,V0,M1} I { aInteger0( xm ) }.
% 277.15/277.61 parent0: (147282) {G0,W2,D2,L1,V0,M1} { aInteger0( xm ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (46) {G0,W10,D4,L1,V0,M1} I { sdtasdt0( xp, sdtasdt0( xq, xm )
% 277.15/277.61 ) ==> sdtpldt0( xa, smndt0( xb ) ) }.
% 277.15/277.61 parent0: (147284) {G0,W10,D4,L1,V0,M1} { sdtasdt0( xp, sdtasdt0( xq, xm )
% 277.15/277.61 ) = sdtpldt0( xa, smndt0( xb ) ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 eqswap: (149132) {G0,W10,D4,L1,V0,M1} { sdtasdt0( xq, sdtasdt0( xp, xm ) )
% 277.15/277.61 = sdtpldt0( xa, smndt0( xb ) ) }.
% 277.15/277.61 parent0[0]: (147285) {G0,W10,D4,L1,V0,M1} { sdtpldt0( xa, smndt0( xb ) ) =
% 277.15/277.61 sdtasdt0( xq, sdtasdt0( xp, xm ) ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (47) {G0,W10,D4,L1,V0,M1} I { sdtasdt0( xq, sdtasdt0( xp, xm )
% 277.15/277.61 ) ==> sdtpldt0( xa, smndt0( xb ) ) }.
% 277.15/277.61 parent0: (149132) {G0,W10,D4,L1,V0,M1} { sdtasdt0( xq, sdtasdt0( xp, xm )
% 277.15/277.61 ) = sdtpldt0( xa, smndt0( xb ) ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (48) {G0,W8,D2,L2,V0,M2} I { ! sdteqdtlpzmzozddtrp0( xa, xb,
% 277.15/277.61 xp ), ! sdteqdtlpzmzozddtrp0( xa, xb, xq ) }.
% 277.15/277.61 parent0: (147286) {G0,W8,D2,L2,V0,M2} { ! sdteqdtlpzmzozddtrp0( xa, xb, xp
% 277.15/277.61 ), ! sdteqdtlpzmzozddtrp0( xa, xb, xq ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 resolution: (149275) {G1,W3,D3,L1,V0,M1} { aInteger0( smndt0( xb ) ) }.
% 277.15/277.61 parent0[0]: (3) {G0,W5,D3,L2,V1,M2} I { ! aInteger0( X ), aInteger0( smndt0
% 277.15/277.61 ( X ) ) }.
% 277.15/277.61 parent1[0]: (38) {G0,W2,D2,L1,V0,M1} I { aInteger0( xb ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := xb
% 277.15/277.61 end
% 277.15/277.61 substitution1:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (90) {G1,W3,D3,L1,V0,M1} R(3,38) { aInteger0( smndt0( xb ) )
% 277.15/277.61 }.
% 277.15/277.61 parent0: (149275) {G1,W3,D3,L1,V0,M1} { aInteger0( smndt0( xb ) ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 resolution: (149276) {G1,W6,D3,L2,V1,M2} { ! aInteger0( X ), aInteger0(
% 277.15/277.61 sdtasdt0( xp, X ) ) }.
% 277.15/277.61 parent0[0]: (5) {G0,W8,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y )
% 277.15/277.61 , aInteger0( sdtasdt0( X, Y ) ) }.
% 277.15/277.61 parent1[0]: (39) {G0,W2,D2,L1,V0,M1} I { aInteger0( xp ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := xp
% 277.15/277.61 Y := X
% 277.15/277.61 end
% 277.15/277.61 substitution1:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (160) {G1,W6,D3,L2,V1,M2} R(5,39) { ! aInteger0( X ),
% 277.15/277.61 aInteger0( sdtasdt0( xp, X ) ) }.
% 277.15/277.61 parent0: (149276) {G1,W6,D3,L2,V1,M2} { ! aInteger0( X ), aInteger0(
% 277.15/277.61 sdtasdt0( xp, X ) ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 resolution: (149278) {G1,W6,D3,L2,V1,M2} { ! aInteger0( X ), aInteger0(
% 277.15/277.61 sdtasdt0( xq, X ) ) }.
% 277.15/277.61 parent0[0]: (5) {G0,W8,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y )
% 277.15/277.61 , aInteger0( sdtasdt0( X, Y ) ) }.
% 277.15/277.61 parent1[0]: (41) {G0,W2,D2,L1,V0,M1} I { aInteger0( xq ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := xq
% 277.15/277.61 Y := X
% 277.15/277.61 end
% 277.15/277.61 substitution1:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (162) {G1,W6,D3,L2,V1,M2} R(5,41) { ! aInteger0( X ),
% 277.15/277.61 aInteger0( sdtasdt0( xq, X ) ) }.
% 277.15/277.61 parent0: (149278) {G1,W6,D3,L2,V1,M2} { ! aInteger0( X ), aInteger0(
% 277.15/277.61 sdtasdt0( xq, X ) ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 resolution: (149280) {G1,W11,D4,L2,V1,M2} { ! aInteger0( X ), sdtpldt0(
% 277.15/277.61 smndt0( xb ), X ) = sdtpldt0( X, smndt0( xb ) ) }.
% 277.15/277.61 parent0[0]: (7) {G0,W11,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y )
% 277.15/277.61 , sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 277.15/277.61 parent1[0]: (90) {G1,W3,D3,L1,V0,M1} R(3,38) { aInteger0( smndt0( xb ) )
% 277.15/277.61 }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := smndt0( xb )
% 277.15/277.61 Y := X
% 277.15/277.61 end
% 277.15/277.61 substitution1:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (294) {G2,W11,D4,L2,V1,M2} R(7,90) { ! aInteger0( X ),
% 277.15/277.61 sdtpldt0( smndt0( xb ), X ) = sdtpldt0( X, smndt0( xb ) ) }.
% 277.15/277.61 parent0: (149280) {G1,W11,D4,L2,V1,M2} { ! aInteger0( X ), sdtpldt0(
% 277.15/277.61 smndt0( xb ), X ) = sdtpldt0( X, smndt0( xb ) ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 1 ==> 1
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 eqswap: (149282) {G0,W7,D3,L2,V1,M2} { X ==> sdtasdt0( X, sz10 ), !
% 277.15/277.61 aInteger0( X ) }.
% 277.15/277.61 parent0[1]: (14) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X,
% 277.15/277.61 sz10 ) ==> X }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 resolution: (149283) {G1,W5,D3,L1,V0,M1} { xp ==> sdtasdt0( xp, sz10 ) }.
% 277.15/277.61 parent0[1]: (149282) {G0,W7,D3,L2,V1,M2} { X ==> sdtasdt0( X, sz10 ), !
% 277.15/277.61 aInteger0( X ) }.
% 277.15/277.61 parent1[0]: (39) {G0,W2,D2,L1,V0,M1} I { aInteger0( xp ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := xp
% 277.15/277.61 end
% 277.15/277.61 substitution1:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 eqswap: (149284) {G1,W5,D3,L1,V0,M1} { sdtasdt0( xp, sz10 ) ==> xp }.
% 277.15/277.61 parent0[0]: (149283) {G1,W5,D3,L1,V0,M1} { xp ==> sdtasdt0( xp, sz10 ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (682) {G1,W5,D3,L1,V0,M1} R(14,39) { sdtasdt0( xp, sz10 ) ==>
% 277.15/277.61 xp }.
% 277.15/277.61 parent0: (149284) {G1,W5,D3,L1,V0,M1} { sdtasdt0( xp, sz10 ) ==> xp }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 eqswap: (149285) {G0,W7,D3,L2,V1,M2} { X ==> sdtasdt0( X, sz10 ), !
% 277.15/277.61 aInteger0( X ) }.
% 277.15/277.61 parent0[1]: (14) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X,
% 277.15/277.61 sz10 ) ==> X }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 resolution: (149286) {G1,W5,D3,L1,V0,M1} { xq ==> sdtasdt0( xq, sz10 ) }.
% 277.15/277.61 parent0[1]: (149285) {G0,W7,D3,L2,V1,M2} { X ==> sdtasdt0( X, sz10 ), !
% 277.15/277.61 aInteger0( X ) }.
% 277.15/277.61 parent1[0]: (41) {G0,W2,D2,L1,V0,M1} I { aInteger0( xq ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := xq
% 277.15/277.61 end
% 277.15/277.61 substitution1:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 eqswap: (149287) {G1,W5,D3,L1,V0,M1} { sdtasdt0( xq, sz10 ) ==> xq }.
% 277.15/277.61 parent0[0]: (149286) {G1,W5,D3,L1,V0,M1} { xq ==> sdtasdt0( xq, sz10 ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (683) {G1,W5,D3,L1,V0,M1} R(14,41) { sdtasdt0( xq, sz10 ) ==>
% 277.15/277.61 xq }.
% 277.15/277.61 parent0: (149287) {G1,W5,D3,L1,V0,M1} { sdtasdt0( xq, sz10 ) ==> xq }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61 permutation0:
% 277.15/277.61 0 ==> 0
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 eqswap: (149288) {G0,W7,D3,L2,V1,M2} { sz00 ==> sdtasdt0( X, sz00 ), !
% 277.15/277.61 aInteger0( X ) }.
% 277.15/277.61 parent0[1]: (18) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X,
% 277.15/277.61 sz00 ) ==> sz00 }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := X
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 resolution: (149289) {G1,W5,D3,L1,V0,M1} { sz00 ==> sdtasdt0( xm, sz00 )
% 277.15/277.61 }.
% 277.15/277.61 parent0[1]: (149288) {G0,W7,D3,L2,V1,M2} { sz00 ==> sdtasdt0( X, sz00 ), !
% 277.15/277.61 aInteger0( X ) }.
% 277.15/277.61 parent1[0]: (44) {G0,W2,D2,L1,V0,M1} I { aInteger0( xm ) }.
% 277.15/277.61 substitution0:
% 277.15/277.61 X := xm
% 277.15/277.61 end
% 277.15/277.61 substitution1:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 eqswap: (149290) {G1,W5,D3,L1,V0,M1} { sdtasdt0( xm, sz00 ) ==> sz00 }.
% 277.15/277.61 parent0[0]: (149289) {G1,W5,D3,L1,V0,M1} { sz00 ==> sdtasdt0( xm, sz00 )
% 277.15/277.61 }.
% 277.15/277.61 substitution0:
% 277.15/277.61 end
% 277.15/277.61
% 277.15/277.61 subsumption: (901) {G1,W5,D3,L1,V0,M1} R(18,44) { sdtasdt0( xm, sz00 ) ==>
% 277.23/277.62 sz00 }.
% 277.23/277.62 parent0: (149290) {G1,W5,D3,L1,V0,M1} { sdtasdt0( xm, sz00 ) ==> sz00 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149292) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> xp }.
% 277.23/277.62 parent0[0]: (40) {G0,W3,D2,L1,V0,M1} I { ! xp ==> sz00 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149296) {G1,W9,D2,L3,V1,M3} { ! sz00 ==> sz00, ! alpha2( X, xp )
% 277.23/277.62 , alpha1( X, xp ) }.
% 277.23/277.62 parent0[0]: (28) {G0,W9,D2,L3,V2,M3} I { Y = sz00, ! alpha2( X, Y ), alpha1
% 277.23/277.62 ( X, Y ) }.
% 277.23/277.62 parent1[0; 3]: (149292) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> xp }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := xp
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqrefl: (149328) {G0,W6,D2,L2,V1,M2} { ! alpha2( X, xp ), alpha1( X, xp )
% 277.23/277.62 }.
% 277.23/277.62 parent0[0]: (149296) {G1,W9,D2,L3,V1,M3} { ! sz00 ==> sz00, ! alpha2( X,
% 277.23/277.62 xp ), alpha1( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (1661) {G1,W6,D2,L2,V1,M2} P(28,40);q { ! alpha2( X, xp ),
% 277.23/277.62 alpha1( X, xp ) }.
% 277.23/277.62 parent0: (149328) {G0,W6,D2,L2,V1,M2} { ! alpha2( X, xp ), alpha1( X, xp )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149330) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> xq }.
% 277.23/277.62 parent0[0]: (42) {G0,W3,D2,L1,V0,M1} I { ! xq ==> sz00 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149334) {G1,W9,D2,L3,V1,M3} { ! sz00 ==> sz00, ! alpha2( X, xq )
% 277.23/277.62 , alpha1( X, xq ) }.
% 277.23/277.62 parent0[0]: (28) {G0,W9,D2,L3,V2,M3} I { Y = sz00, ! alpha2( X, Y ), alpha1
% 277.23/277.62 ( X, Y ) }.
% 277.23/277.62 parent1[0; 3]: (149330) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> xq }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := xq
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqrefl: (149366) {G0,W6,D2,L2,V1,M2} { ! alpha2( X, xq ), alpha1( X, xq )
% 277.23/277.62 }.
% 277.23/277.62 parent0[0]: (149334) {G1,W9,D2,L3,V1,M3} { ! sz00 ==> sz00, ! alpha2( X,
% 277.23/277.62 xq ), alpha1( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (1662) {G1,W6,D2,L2,V1,M2} P(28,42);q { ! alpha2( X, xq ),
% 277.23/277.62 alpha1( X, xq ) }.
% 277.23/277.62 parent0: (149366) {G0,W6,D2,L2,V1,M2} { ! alpha2( X, xq ), alpha1( X, xq )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149368) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 277.23/277.62 aInteger0( Y ), alpha2( Z, X ) }.
% 277.23/277.62 parent0[1]: (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y,
% 277.23/277.62 Z ) = X, alpha2( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := Z
% 277.23/277.62 Y := X
% 277.23/277.62 Z := Y
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149369) {G1,W8,D2,L3,V1,M3} { ! X = sz00, ! aInteger0( sz00 ),
% 277.23/277.62 alpha2( X, xm ) }.
% 277.23/277.62 parent0[0]: (901) {G1,W5,D3,L1,V0,M1} R(18,44) { sdtasdt0( xm, sz00 ) ==>
% 277.23/277.62 sz00 }.
% 277.23/277.62 parent1[0; 3]: (149368) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 277.23/277.62 aInteger0( Y ), alpha2( Z, X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := xm
% 277.23/277.62 Y := sz00
% 277.23/277.62 Z := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149370) {G1,W6,D2,L2,V1,M2} { ! X = sz00, alpha2( X, xm ) }.
% 277.23/277.62 parent0[1]: (149369) {G1,W8,D2,L3,V1,M3} { ! X = sz00, ! aInteger0( sz00 )
% 277.23/277.62 , alpha2( X, xm ) }.
% 277.23/277.62 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz00 ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149371) {G1,W6,D2,L2,V1,M2} { ! sz00 = X, alpha2( X, xm ) }.
% 277.23/277.62 parent0[0]: (149370) {G1,W6,D2,L2,V1,M2} { ! X = sz00, alpha2( X, xm ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (1886) {G2,W6,D2,L2,V1,M2} P(901,31);r(1) { ! sz00 = X, alpha2
% 277.23/277.62 ( X, xm ) }.
% 277.23/277.62 parent0: (149371) {G1,W6,D2,L2,V1,M2} { ! sz00 = X, alpha2( X, xm ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149373) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 277.23/277.62 aInteger0( Y ), alpha2( Z, X ) }.
% 277.23/277.62 parent0[1]: (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y,
% 277.23/277.62 Z ) = X, alpha2( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := Z
% 277.23/277.62 Y := X
% 277.23/277.62 Z := Y
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149374) {G1,W8,D2,L3,V1,M3} { ! X = xq, ! aInteger0( sz10 ),
% 277.23/277.62 alpha2( X, xq ) }.
% 277.23/277.62 parent0[0]: (683) {G1,W5,D3,L1,V0,M1} R(14,41) { sdtasdt0( xq, sz10 ) ==>
% 277.23/277.62 xq }.
% 277.23/277.62 parent1[0; 3]: (149373) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 277.23/277.62 aInteger0( Y ), alpha2( Z, X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := xq
% 277.23/277.62 Y := sz10
% 277.23/277.62 Z := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149375) {G1,W6,D2,L2,V1,M2} { ! X = xq, alpha2( X, xq ) }.
% 277.23/277.62 parent0[1]: (149374) {G1,W8,D2,L3,V1,M3} { ! X = xq, ! aInteger0( sz10 ),
% 277.23/277.62 alpha2( X, xq ) }.
% 277.23/277.62 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz10 ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149376) {G1,W6,D2,L2,V1,M2} { ! xq = X, alpha2( X, xq ) }.
% 277.23/277.62 parent0[0]: (149375) {G1,W6,D2,L2,V1,M2} { ! X = xq, alpha2( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (1895) {G2,W6,D2,L2,V1,M2} P(683,31);r(2) { ! xq = X, alpha2(
% 277.23/277.62 X, xq ) }.
% 277.23/277.62 parent0: (149376) {G1,W6,D2,L2,V1,M2} { ! xq = X, alpha2( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149378) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 277.23/277.62 aInteger0( Y ), alpha2( Z, X ) }.
% 277.23/277.62 parent0[1]: (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y,
% 277.23/277.62 Z ) = X, alpha2( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := Z
% 277.23/277.62 Y := X
% 277.23/277.62 Z := Y
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149379) {G1,W8,D2,L3,V1,M3} { ! X = xp, ! aInteger0( sz10 ),
% 277.23/277.62 alpha2( X, xp ) }.
% 277.23/277.62 parent0[0]: (682) {G1,W5,D3,L1,V0,M1} R(14,39) { sdtasdt0( xp, sz10 ) ==>
% 277.23/277.62 xp }.
% 277.23/277.62 parent1[0; 3]: (149378) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 277.23/277.62 aInteger0( Y ), alpha2( Z, X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := xp
% 277.23/277.62 Y := sz10
% 277.23/277.62 Z := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149380) {G1,W6,D2,L2,V1,M2} { ! X = xp, alpha2( X, xp ) }.
% 277.23/277.62 parent0[1]: (149379) {G1,W8,D2,L3,V1,M3} { ! X = xp, ! aInteger0( sz10 ),
% 277.23/277.62 alpha2( X, xp ) }.
% 277.23/277.62 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz10 ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149381) {G1,W6,D2,L2,V1,M2} { ! xp = X, alpha2( X, xp ) }.
% 277.23/277.62 parent0[0]: (149380) {G1,W6,D2,L2,V1,M2} { ! X = xp, alpha2( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (1896) {G2,W6,D2,L2,V1,M2} P(682,31);r(2) { ! xp = X, alpha2(
% 277.23/277.62 X, xp ) }.
% 277.23/277.62 parent0: (149381) {G1,W6,D2,L2,V1,M2} { ! xp = X, alpha2( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149382) {G2,W6,D2,L2,V1,M2} { ! X = sz00, alpha2( X, xm ) }.
% 277.23/277.62 parent0[0]: (1886) {G2,W6,D2,L2,V1,M2} P(901,31);r(1) { ! sz00 = X, alpha2
% 277.23/277.62 ( X, xm ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqrefl: (149383) {G0,W3,D2,L1,V0,M1} { alpha2( sz00, xm ) }.
% 277.23/277.62 parent0[0]: (149382) {G2,W6,D2,L2,V1,M2} { ! X = sz00, alpha2( X, xm ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := sz00
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (1940) {G3,W3,D2,L1,V0,M1} Q(1886) { alpha2( sz00, xm ) }.
% 277.23/277.62 parent0: (149383) {G0,W3,D2,L1,V0,M1} { alpha2( sz00, xm ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149384) {G1,W4,D3,L1,V2,M1} { aInteger0( skol1( X, Y ) ) }.
% 277.23/277.62 parent0[0]: (29) {G0,W7,D3,L2,V4,M2} I { ! alpha2( X, Y ), aInteger0( skol1
% 277.23/277.62 ( Z, T ) ) }.
% 277.23/277.62 parent1[0]: (1940) {G3,W3,D2,L1,V0,M1} Q(1886) { alpha2( sz00, xm ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := sz00
% 277.23/277.62 Y := xm
% 277.23/277.62 Z := X
% 277.23/277.62 T := Y
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (2000) {G4,W4,D3,L1,V2,M1} R(1940,29) { aInteger0( skol1( X, Y
% 277.23/277.62 ) ) }.
% 277.23/277.62 parent0: (149384) {G1,W4,D3,L1,V2,M1} { aInteger0( skol1( X, Y ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := Y
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149386) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 277.23/277.62 aInteger0( Y ), alpha2( Z, X ) }.
% 277.23/277.62 parent0[1]: (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y,
% 277.23/277.62 Z ) = X, alpha2( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := Z
% 277.23/277.62 Y := X
% 277.23/277.62 Z := Y
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149387) {G1,W13,D4,L3,V1,M3} { ! X = sdtpldt0( xa, smndt0( xb )
% 277.23/277.62 ), ! aInteger0( sdtasdt0( xq, xm ) ), alpha2( X, xp ) }.
% 277.23/277.62 parent0[0]: (46) {G0,W10,D4,L1,V0,M1} I { sdtasdt0( xp, sdtasdt0( xq, xm )
% 277.23/277.62 ) ==> sdtpldt0( xa, smndt0( xb ) ) }.
% 277.23/277.62 parent1[0; 3]: (149386) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 277.23/277.62 aInteger0( Y ), alpha2( Z, X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := xp
% 277.23/277.62 Y := sdtasdt0( xq, xm )
% 277.23/277.62 Z := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149388) {G1,W13,D4,L3,V1,M3} { ! sdtpldt0( xa, smndt0( xb ) ) = X
% 277.23/277.62 , ! aInteger0( sdtasdt0( xq, xm ) ), alpha2( X, xp ) }.
% 277.23/277.62 parent0[0]: (149387) {G1,W13,D4,L3,V1,M3} { ! X = sdtpldt0( xa, smndt0( xb
% 277.23/277.62 ) ), ! aInteger0( sdtasdt0( xq, xm ) ), alpha2( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (2797) {G1,W13,D4,L3,V1,M3} P(46,31) { ! aInteger0( sdtasdt0(
% 277.23/277.62 xq, xm ) ), ! sdtpldt0( xa, smndt0( xb ) ) = X, alpha2( X, xp ) }.
% 277.23/277.62 parent0: (149388) {G1,W13,D4,L3,V1,M3} { ! sdtpldt0( xa, smndt0( xb ) ) =
% 277.23/277.62 X, ! aInteger0( sdtasdt0( xq, xm ) ), alpha2( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 1
% 277.23/277.62 1 ==> 0
% 277.23/277.62 2 ==> 2
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149389) {G1,W13,D4,L3,V1,M3} { ! X = sdtpldt0( xa, smndt0( xb ) )
% 277.23/277.62 , ! aInteger0( sdtasdt0( xq, xm ) ), alpha2( X, xp ) }.
% 277.23/277.62 parent0[1]: (2797) {G1,W13,D4,L3,V1,M3} P(46,31) { ! aInteger0( sdtasdt0(
% 277.23/277.62 xq, xm ) ), ! sdtpldt0( xa, smndt0( xb ) ) = X, alpha2( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqrefl: (149390) {G0,W10,D4,L2,V0,M2} { ! aInteger0( sdtasdt0( xq, xm ) )
% 277.23/277.62 , alpha2( sdtpldt0( xa, smndt0( xb ) ), xp ) }.
% 277.23/277.62 parent0[0]: (149389) {G1,W13,D4,L3,V1,M3} { ! X = sdtpldt0( xa, smndt0( xb
% 277.23/277.62 ) ), ! aInteger0( sdtasdt0( xq, xm ) ), alpha2( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := sdtpldt0( xa, smndt0( xb ) )
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (2808) {G2,W10,D4,L2,V0,M2} Q(2797) { ! aInteger0( sdtasdt0(
% 277.23/277.62 xq, xm ) ), alpha2( sdtpldt0( xa, smndt0( xb ) ), xp ) }.
% 277.23/277.62 parent0: (149390) {G0,W10,D4,L2,V0,M2} { ! aInteger0( sdtasdt0( xq, xm ) )
% 277.23/277.62 , alpha2( sdtpldt0( xa, smndt0( xb ) ), xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149392) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 277.23/277.62 aInteger0( Y ), alpha2( Z, X ) }.
% 277.23/277.62 parent0[1]: (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y,
% 277.23/277.62 Z ) = X, alpha2( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := Z
% 277.23/277.62 Y := X
% 277.23/277.62 Z := Y
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149393) {G1,W13,D4,L3,V1,M3} { ! X = sdtpldt0( xa, smndt0( xb )
% 277.23/277.62 ), ! aInteger0( sdtasdt0( xp, xm ) ), alpha2( X, xq ) }.
% 277.23/277.62 parent0[0]: (47) {G0,W10,D4,L1,V0,M1} I { sdtasdt0( xq, sdtasdt0( xp, xm )
% 277.23/277.62 ) ==> sdtpldt0( xa, smndt0( xb ) ) }.
% 277.23/277.62 parent1[0; 3]: (149392) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 277.23/277.62 aInteger0( Y ), alpha2( Z, X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := xq
% 277.23/277.62 Y := sdtasdt0( xp, xm )
% 277.23/277.62 Z := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149394) {G1,W13,D4,L3,V1,M3} { ! sdtpldt0( xa, smndt0( xb ) ) = X
% 277.23/277.62 , ! aInteger0( sdtasdt0( xp, xm ) ), alpha2( X, xq ) }.
% 277.23/277.62 parent0[0]: (149393) {G1,W13,D4,L3,V1,M3} { ! X = sdtpldt0( xa, smndt0( xb
% 277.23/277.62 ) ), ! aInteger0( sdtasdt0( xp, xm ) ), alpha2( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (2817) {G1,W13,D4,L3,V1,M3} P(47,31) { ! aInteger0( sdtasdt0(
% 277.23/277.62 xp, xm ) ), ! sdtpldt0( xa, smndt0( xb ) ) = X, alpha2( X, xq ) }.
% 277.23/277.62 parent0: (149394) {G1,W13,D4,L3,V1,M3} { ! sdtpldt0( xa, smndt0( xb ) ) =
% 277.23/277.62 X, ! aInteger0( sdtasdt0( xp, xm ) ), alpha2( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 1
% 277.23/277.62 1 ==> 0
% 277.23/277.62 2 ==> 2
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149395) {G1,W13,D4,L3,V1,M3} { ! X = sdtpldt0( xa, smndt0( xb ) )
% 277.23/277.62 , ! aInteger0( sdtasdt0( xp, xm ) ), alpha2( X, xq ) }.
% 277.23/277.62 parent0[1]: (2817) {G1,W13,D4,L3,V1,M3} P(47,31) { ! aInteger0( sdtasdt0(
% 277.23/277.62 xp, xm ) ), ! sdtpldt0( xa, smndt0( xb ) ) = X, alpha2( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqrefl: (149396) {G0,W10,D4,L2,V0,M2} { ! aInteger0( sdtasdt0( xp, xm ) )
% 277.23/277.62 , alpha2( sdtpldt0( xa, smndt0( xb ) ), xq ) }.
% 277.23/277.62 parent0[0]: (149395) {G1,W13,D4,L3,V1,M3} { ! X = sdtpldt0( xa, smndt0( xb
% 277.23/277.62 ) ), ! aInteger0( sdtasdt0( xp, xm ) ), alpha2( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := sdtpldt0( xa, smndt0( xb ) )
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (2827) {G2,W10,D4,L2,V0,M2} Q(2817) { ! aInteger0( sdtasdt0(
% 277.23/277.62 xp, xm ) ), alpha2( sdtpldt0( xa, smndt0( xb ) ), xq ) }.
% 277.23/277.62 parent0: (149396) {G0,W10,D4,L2,V0,M2} { ! aInteger0( sdtasdt0( xp, xm ) )
% 277.23/277.62 , alpha2( sdtpldt0( xa, smndt0( xb ) ), xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149397) {G0,W19,D4,L6,V3,M6} { sz00 = X, ! aInteger0( Y ), !
% 277.23/277.62 aInteger0( Z ), ! aInteger0( X ), ! aDivisorOf0( X, sdtpldt0( Y, smndt0(
% 277.23/277.62 Z ) ) ), sdteqdtlpzmzozddtrp0( Y, Z, X ) }.
% 277.23/277.62 parent0[3]: (33) {G0,W19,D4,L6,V3,M6} I { ! aInteger0( X ), ! aInteger0( Y
% 277.23/277.62 ), ! aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y
% 277.23/277.62 ) ) ), sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := Y
% 277.23/277.62 Y := Z
% 277.23/277.62 Z := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149399) {G1,W19,D4,L6,V0,M6} { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.23/277.62 , xp ), sz00 = xq, ! aInteger0( xa ), ! aInteger0( xb ), ! aInteger0( xq
% 277.23/277.62 ), ! aDivisorOf0( xq, sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.23/277.62 parent0[1]: (48) {G0,W8,D2,L2,V0,M2} I { ! sdteqdtlpzmzozddtrp0( xa, xb, xp
% 277.23/277.62 ), ! sdteqdtlpzmzozddtrp0( xa, xb, xq ) }.
% 277.23/277.62 parent1[5]: (149397) {G0,W19,D4,L6,V3,M6} { sz00 = X, ! aInteger0( Y ), !
% 277.23/277.62 aInteger0( Z ), ! aInteger0( X ), ! aDivisorOf0( X, sdtpldt0( Y, smndt0(
% 277.23/277.62 Z ) ) ), sdteqdtlpzmzozddtrp0( Y, Z, X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := xq
% 277.23/277.62 Y := xa
% 277.23/277.62 Z := xb
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149402) {G1,W17,D4,L5,V0,M5} { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.23/277.62 , xp ), sz00 = xq, ! aInteger0( xb ), ! aInteger0( xq ), ! aDivisorOf0(
% 277.23/277.62 xq, sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.23/277.62 parent0[2]: (149399) {G1,W19,D4,L6,V0,M6} { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.23/277.62 , xp ), sz00 = xq, ! aInteger0( xa ), ! aInteger0( xb ), ! aInteger0( xq
% 277.23/277.62 ), ! aDivisorOf0( xq, sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.23/277.62 parent1[0]: (37) {G0,W2,D2,L1,V0,M1} I { aInteger0( xa ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149403) {G1,W17,D4,L5,V0,M5} { xq = sz00, ! sdteqdtlpzmzozddtrp0
% 277.23/277.62 ( xa, xb, xp ), ! aInteger0( xb ), ! aInteger0( xq ), ! aDivisorOf0( xq,
% 277.23/277.62 sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.23/277.62 parent0[1]: (149402) {G1,W17,D4,L5,V0,M5} { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.23/277.62 , xp ), sz00 = xq, ! aInteger0( xb ), ! aInteger0( xq ), ! aDivisorOf0(
% 277.23/277.62 xq, sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (2886) {G1,W17,D4,L5,V0,M5} R(48,33);r(37) { !
% 277.23/277.62 sdteqdtlpzmzozddtrp0( xa, xb, xp ), ! aInteger0( xb ), ! aInteger0( xq )
% 277.23/277.62 , xq ==> sz00, ! aDivisorOf0( xq, sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.23/277.62 parent0: (149403) {G1,W17,D4,L5,V0,M5} { xq = sz00, ! sdteqdtlpzmzozddtrp0
% 277.23/277.62 ( xa, xb, xp ), ! aInteger0( xb ), ! aInteger0( xq ), ! aDivisorOf0( xq,
% 277.23/277.62 sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 3
% 277.23/277.62 1 ==> 0
% 277.23/277.62 2 ==> 1
% 277.23/277.62 3 ==> 2
% 277.23/277.62 4 ==> 4
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149406) {G1,W15,D4,L4,V0,M4} { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.23/277.62 , xp ), ! aInteger0( xq ), xq ==> sz00, ! aDivisorOf0( xq, sdtpldt0( xa,
% 277.23/277.62 smndt0( xb ) ) ) }.
% 277.23/277.62 parent0[1]: (2886) {G1,W17,D4,L5,V0,M5} R(48,33);r(37) { !
% 277.23/277.62 sdteqdtlpzmzozddtrp0( xa, xb, xp ), ! aInteger0( xb ), ! aInteger0( xq )
% 277.23/277.62 , xq ==> sz00, ! aDivisorOf0( xq, sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.23/277.62 parent1[0]: (38) {G0,W2,D2,L1,V0,M1} I { aInteger0( xb ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149407) {G1,W13,D4,L3,V0,M3} { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.23/277.62 , xp ), xq ==> sz00, ! aDivisorOf0( xq, sdtpldt0( xa, smndt0( xb ) ) )
% 277.23/277.62 }.
% 277.23/277.62 parent0[1]: (149406) {G1,W15,D4,L4,V0,M4} { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.23/277.62 , xp ), ! aInteger0( xq ), xq ==> sz00, ! aDivisorOf0( xq, sdtpldt0( xa,
% 277.23/277.62 smndt0( xb ) ) ) }.
% 277.23/277.62 parent1[0]: (41) {G0,W2,D2,L1,V0,M1} I { aInteger0( xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149408) {G1,W10,D4,L2,V0,M2} { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.23/277.62 , xp ), ! aDivisorOf0( xq, sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.23/277.62 parent0[0]: (42) {G0,W3,D2,L1,V0,M1} I { ! xq ==> sz00 }.
% 277.23/277.62 parent1[1]: (149407) {G1,W13,D4,L3,V0,M3} { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.23/277.62 , xp ), xq ==> sz00, ! aDivisorOf0( xq, sdtpldt0( xa, smndt0( xb ) ) )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (20068) {G2,W10,D4,L2,V0,M2} S(2886);r(38);r(41);r(42) { !
% 277.23/277.62 sdteqdtlpzmzozddtrp0( xa, xb, xp ), ! aDivisorOf0( xq, sdtpldt0( xa,
% 277.23/277.62 smndt0( xb ) ) ) }.
% 277.23/277.62 parent0: (149408) {G1,W10,D4,L2,V0,M2} { ! sdteqdtlpzmzozddtrp0( xa, xb,
% 277.23/277.62 xp ), ! aDivisorOf0( xq, sdtpldt0( xa, smndt0( xb ) ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149409) {G1,W4,D3,L1,V0,M1} { aInteger0( sdtasdt0( xp, xm ) )
% 277.23/277.62 }.
% 277.23/277.62 parent0[0]: (160) {G1,W6,D3,L2,V1,M2} R(5,39) { ! aInteger0( X ), aInteger0
% 277.23/277.62 ( sdtasdt0( xp, X ) ) }.
% 277.23/277.62 parent1[0]: (44) {G0,W2,D2,L1,V0,M1} I { aInteger0( xm ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := xm
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (30287) {G2,W4,D3,L1,V0,M1} R(160,44) { aInteger0( sdtasdt0(
% 277.23/277.62 xp, xm ) ) }.
% 277.23/277.62 parent0: (149409) {G1,W4,D3,L1,V0,M1} { aInteger0( sdtasdt0( xp, xm ) )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149411) {G1,W9,D3,L3,V1,M3} { aInteger0( X ), ! alpha2( X, xp )
% 277.23/277.62 , ! aInteger0( skol1( X, xp ) ) }.
% 277.23/277.62 parent0[1]: (30) {G0,W10,D4,L2,V2,M2} I { ! alpha2( X, Y ), sdtasdt0( Y,
% 277.23/277.62 skol1( X, Y ) ) ==> X }.
% 277.23/277.62 parent1[1; 1]: (160) {G1,W6,D3,L2,V1,M2} R(5,39) { ! aInteger0( X ),
% 277.23/277.62 aInteger0( sdtasdt0( xp, X ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := xp
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := skol1( X, xp )
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149412) {G2,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha2( X, xp
% 277.23/277.62 ) }.
% 277.23/277.62 parent0[2]: (149411) {G1,W9,D3,L3,V1,M3} { aInteger0( X ), ! alpha2( X, xp
% 277.23/277.62 ), ! aInteger0( skol1( X, xp ) ) }.
% 277.23/277.62 parent1[0]: (2000) {G4,W4,D3,L1,V2,M1} R(1940,29) { aInteger0( skol1( X, Y
% 277.23/277.62 ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := X
% 277.23/277.62 Y := xp
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (30288) {G5,W5,D2,L2,V1,M2} P(30,160);r(2000) { aInteger0( X )
% 277.23/277.62 , ! alpha2( X, xp ) }.
% 277.23/277.62 parent0: (149412) {G2,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha2( X, xp )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149413) {G2,W6,D2,L2,V1,M2} { ! X = xp, alpha2( X, xp ) }.
% 277.23/277.62 parent0[0]: (1896) {G2,W6,D2,L2,V1,M2} P(682,31);r(2) { ! xp = X, alpha2( X
% 277.23/277.62 , xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149414) {G3,W5,D2,L2,V1,M2} { aInteger0( X ), ! X = xp }.
% 277.23/277.62 parent0[1]: (30288) {G5,W5,D2,L2,V1,M2} P(30,160);r(2000) { aInteger0( X )
% 277.23/277.62 , ! alpha2( X, xp ) }.
% 277.23/277.62 parent1[1]: (149413) {G2,W6,D2,L2,V1,M2} { ! X = xp, alpha2( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149415) {G3,W5,D2,L2,V1,M2} { ! xp = X, aInteger0( X ) }.
% 277.23/277.62 parent0[1]: (149414) {G3,W5,D2,L2,V1,M2} { aInteger0( X ), ! X = xp }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (30700) {G6,W5,D2,L2,V1,M2} R(30288,1896) { aInteger0( X ), !
% 277.23/277.62 xp = X }.
% 277.23/277.62 parent0: (149415) {G3,W5,D2,L2,V1,M2} { ! xp = X, aInteger0( X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 1
% 277.23/277.62 1 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149416) {G1,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha1( X, xp
% 277.23/277.62 ) }.
% 277.23/277.62 parent0[1]: (30288) {G5,W5,D2,L2,V1,M2} P(30,160);r(2000) { aInteger0( X )
% 277.23/277.62 , ! alpha2( X, xp ) }.
% 277.23/277.62 parent1[1]: (27) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), alpha2( X, Y )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := X
% 277.23/277.62 Y := xp
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (30736) {G6,W5,D2,L2,V1,M2} R(30288,27) { aInteger0( X ), !
% 277.23/277.62 alpha1( X, xp ) }.
% 277.23/277.62 parent0: (149416) {G1,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha1( X, xp )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149417) {G6,W5,D2,L2,V1,M2} { ! X = xp, aInteger0( X ) }.
% 277.23/277.62 parent0[1]: (30700) {G6,W5,D2,L2,V1,M2} R(30288,1896) { aInteger0( X ), !
% 277.23/277.62 xp = X }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149419) {G1,W11,D2,L4,V2,M4} { ! aInteger0( X ), ! alpha1( X
% 277.23/277.62 , Y ), aDivisorOf0( Y, X ), ! Y = xp }.
% 277.23/277.62 parent0[1]: (25) {G0,W10,D2,L4,V2,M4} I { ! aInteger0( X ), ! aInteger0( Y
% 277.23/277.62 ), ! alpha1( X, Y ), aDivisorOf0( Y, X ) }.
% 277.23/277.62 parent1[1]: (149417) {G6,W5,D2,L2,V1,M2} { ! X = xp, aInteger0( X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := Y
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := Y
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149420) {G1,W11,D2,L4,V2,M4} { ! xp = X, ! aInteger0( Y ), !
% 277.23/277.62 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 parent0[3]: (149419) {G1,W11,D2,L4,V2,M4} { ! aInteger0( X ), ! alpha1( X
% 277.23/277.62 , Y ), aDivisorOf0( Y, X ), ! Y = xp }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := Y
% 277.23/277.62 Y := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (30853) {G7,W11,D2,L4,V2,M4} R(30700,25) { ! xp = X, !
% 277.23/277.62 aInteger0( Y ), ! alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 parent0: (149420) {G1,W11,D2,L4,V2,M4} { ! xp = X, ! aInteger0( Y ), !
% 277.23/277.62 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := Y
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 2 ==> 2
% 277.23/277.62 3 ==> 3
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149422) {G7,W11,D2,L4,V2,M4} { ! X = xp, ! aInteger0( Y ), !
% 277.23/277.62 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 parent0[0]: (30853) {G7,W11,D2,L4,V2,M4} R(30700,25) { ! xp = X, !
% 277.23/277.62 aInteger0( Y ), ! alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := Y
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqrefl: (149423) {G0,W8,D2,L3,V1,M3} { ! aInteger0( X ), ! alpha1( X, xp )
% 277.23/277.62 , aDivisorOf0( xp, X ) }.
% 277.23/277.62 parent0[0]: (149422) {G7,W11,D2,L4,V2,M4} { ! X = xp, ! aInteger0( Y ), !
% 277.23/277.62 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := xp
% 277.23/277.62 Y := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149424) {G1,W9,D2,L3,V1,M3} { ! alpha1( X, xp ), aDivisorOf0
% 277.23/277.62 ( xp, X ), ! alpha1( X, xp ) }.
% 277.23/277.62 parent0[0]: (149423) {G0,W8,D2,L3,V1,M3} { ! aInteger0( X ), ! alpha1( X,
% 277.23/277.62 xp ), aDivisorOf0( xp, X ) }.
% 277.23/277.62 parent1[0]: (30736) {G6,W5,D2,L2,V1,M2} R(30288,27) { aInteger0( X ), !
% 277.23/277.62 alpha1( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 factor: (149425) {G1,W6,D2,L2,V1,M2} { ! alpha1( X, xp ), aDivisorOf0( xp
% 277.23/277.62 , X ) }.
% 277.23/277.62 parent0[0, 2]: (149424) {G1,W9,D2,L3,V1,M3} { ! alpha1( X, xp ),
% 277.23/277.62 aDivisorOf0( xp, X ), ! alpha1( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (30875) {G8,W6,D2,L2,V1,M2} Q(30853);r(30736) { ! alpha1( X,
% 277.23/277.62 xp ), aDivisorOf0( xp, X ) }.
% 277.23/277.62 parent0: (149425) {G1,W6,D2,L2,V1,M2} { ! alpha1( X, xp ), aDivisorOf0( xp
% 277.23/277.62 , X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149426) {G1,W4,D3,L1,V0,M1} { aInteger0( sdtasdt0( xq, xm ) )
% 277.23/277.62 }.
% 277.23/277.62 parent0[0]: (162) {G1,W6,D3,L2,V1,M2} R(5,41) { ! aInteger0( X ), aInteger0
% 277.23/277.62 ( sdtasdt0( xq, X ) ) }.
% 277.23/277.62 parent1[0]: (44) {G0,W2,D2,L1,V0,M1} I { aInteger0( xm ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := xm
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (32071) {G2,W4,D3,L1,V0,M1} R(162,44) { aInteger0( sdtasdt0(
% 277.23/277.62 xq, xm ) ) }.
% 277.23/277.62 parent0: (149426) {G1,W4,D3,L1,V0,M1} { aInteger0( sdtasdt0( xq, xm ) )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149428) {G1,W9,D3,L3,V1,M3} { aInteger0( X ), ! alpha2( X, xq )
% 277.23/277.62 , ! aInteger0( skol1( X, xq ) ) }.
% 277.23/277.62 parent0[1]: (30) {G0,W10,D4,L2,V2,M2} I { ! alpha2( X, Y ), sdtasdt0( Y,
% 277.23/277.62 skol1( X, Y ) ) ==> X }.
% 277.23/277.62 parent1[1; 1]: (162) {G1,W6,D3,L2,V1,M2} R(5,41) { ! aInteger0( X ),
% 277.23/277.62 aInteger0( sdtasdt0( xq, X ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := xq
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := skol1( X, xq )
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149429) {G2,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha2( X, xq
% 277.23/277.62 ) }.
% 277.23/277.62 parent0[2]: (149428) {G1,W9,D3,L3,V1,M3} { aInteger0( X ), ! alpha2( X, xq
% 277.23/277.62 ), ! aInteger0( skol1( X, xq ) ) }.
% 277.23/277.62 parent1[0]: (2000) {G4,W4,D3,L1,V2,M1} R(1940,29) { aInteger0( skol1( X, Y
% 277.23/277.62 ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := X
% 277.23/277.62 Y := xq
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (32072) {G5,W5,D2,L2,V1,M2} P(30,162);r(2000) { aInteger0( X )
% 277.23/277.62 , ! alpha2( X, xq ) }.
% 277.23/277.62 parent0: (149429) {G2,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha2( X, xq )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149430) {G2,W6,D2,L2,V1,M2} { ! X = xq, alpha2( X, xq ) }.
% 277.23/277.62 parent0[0]: (1895) {G2,W6,D2,L2,V1,M2} P(683,31);r(2) { ! xq = X, alpha2( X
% 277.23/277.62 , xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149431) {G3,W5,D2,L2,V1,M2} { aInteger0( X ), ! X = xq }.
% 277.23/277.62 parent0[1]: (32072) {G5,W5,D2,L2,V1,M2} P(30,162);r(2000) { aInteger0( X )
% 277.23/277.62 , ! alpha2( X, xq ) }.
% 277.23/277.62 parent1[1]: (149430) {G2,W6,D2,L2,V1,M2} { ! X = xq, alpha2( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149432) {G3,W5,D2,L2,V1,M2} { ! xq = X, aInteger0( X ) }.
% 277.23/277.62 parent0[1]: (149431) {G3,W5,D2,L2,V1,M2} { aInteger0( X ), ! X = xq }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (32360) {G6,W5,D2,L2,V1,M2} R(32072,1895) { aInteger0( X ), !
% 277.23/277.62 xq = X }.
% 277.23/277.62 parent0: (149432) {G3,W5,D2,L2,V1,M2} { ! xq = X, aInteger0( X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 1
% 277.23/277.62 1 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149433) {G1,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha1( X, xq
% 277.23/277.62 ) }.
% 277.23/277.62 parent0[1]: (32072) {G5,W5,D2,L2,V1,M2} P(30,162);r(2000) { aInteger0( X )
% 277.23/277.62 , ! alpha2( X, xq ) }.
% 277.23/277.62 parent1[1]: (27) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), alpha2( X, Y )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := X
% 277.23/277.62 Y := xq
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (32396) {G6,W5,D2,L2,V1,M2} R(32072,27) { aInteger0( X ), !
% 277.23/277.62 alpha1( X, xq ) }.
% 277.23/277.62 parent0: (149433) {G1,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha1( X, xq )
% 277.23/277.62 }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149434) {G6,W5,D2,L2,V1,M2} { ! X = xq, aInteger0( X ) }.
% 277.23/277.62 parent0[1]: (32360) {G6,W5,D2,L2,V1,M2} R(32072,1895) { aInteger0( X ), !
% 277.23/277.62 xq = X }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149436) {G1,W11,D2,L4,V2,M4} { ! aInteger0( X ), ! alpha1( X
% 277.23/277.62 , Y ), aDivisorOf0( Y, X ), ! Y = xq }.
% 277.23/277.62 parent0[1]: (25) {G0,W10,D2,L4,V2,M4} I { ! aInteger0( X ), ! aInteger0( Y
% 277.23/277.62 ), ! alpha1( X, Y ), aDivisorOf0( Y, X ) }.
% 277.23/277.62 parent1[1]: (149434) {G6,W5,D2,L2,V1,M2} { ! X = xq, aInteger0( X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := Y
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := Y
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149437) {G1,W11,D2,L4,V2,M4} { ! xq = X, ! aInteger0( Y ), !
% 277.23/277.62 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 parent0[3]: (149436) {G1,W11,D2,L4,V2,M4} { ! aInteger0( X ), ! alpha1( X
% 277.23/277.62 , Y ), aDivisorOf0( Y, X ), ! Y = xq }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := Y
% 277.23/277.62 Y := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (32515) {G7,W11,D2,L4,V2,M4} R(32360,25) { ! xq = X, !
% 277.23/277.62 aInteger0( Y ), ! alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 parent0: (149437) {G1,W11,D2,L4,V2,M4} { ! xq = X, ! aInteger0( Y ), !
% 277.23/277.62 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := Y
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 2 ==> 2
% 277.23/277.62 3 ==> 3
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149439) {G7,W11,D2,L4,V2,M4} { ! X = xq, ! aInteger0( Y ), !
% 277.23/277.62 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 parent0[0]: (32515) {G7,W11,D2,L4,V2,M4} R(32360,25) { ! xq = X, !
% 277.23/277.62 aInteger0( Y ), ! alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 Y := Y
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqrefl: (149440) {G0,W8,D2,L3,V1,M3} { ! aInteger0( X ), ! alpha1( X, xq )
% 277.23/277.62 , aDivisorOf0( xq, X ) }.
% 277.23/277.62 parent0[0]: (149439) {G7,W11,D2,L4,V2,M4} { ! X = xq, ! aInteger0( Y ), !
% 277.23/277.62 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := xq
% 277.23/277.62 Y := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149441) {G1,W9,D2,L3,V1,M3} { ! alpha1( X, xq ), aDivisorOf0
% 277.23/277.62 ( xq, X ), ! alpha1( X, xq ) }.
% 277.23/277.62 parent0[0]: (149440) {G0,W8,D2,L3,V1,M3} { ! aInteger0( X ), ! alpha1( X,
% 277.23/277.62 xq ), aDivisorOf0( xq, X ) }.
% 277.23/277.62 parent1[0]: (32396) {G6,W5,D2,L2,V1,M2} R(32072,27) { aInteger0( X ), !
% 277.23/277.62 alpha1( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 factor: (149442) {G1,W6,D2,L2,V1,M2} { ! alpha1( X, xq ), aDivisorOf0( xq
% 277.23/277.62 , X ) }.
% 277.23/277.62 parent0[0, 2]: (149441) {G1,W9,D2,L3,V1,M3} { ! alpha1( X, xq ),
% 277.23/277.62 aDivisorOf0( xq, X ), ! alpha1( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (32537) {G8,W6,D2,L2,V1,M2} Q(32515);r(32396) { ! alpha1( X,
% 277.23/277.62 xq ), aDivisorOf0( xq, X ) }.
% 277.23/277.62 parent0: (149442) {G1,W6,D2,L2,V1,M2} { ! alpha1( X, xq ), aDivisorOf0( xq
% 277.23/277.62 , X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 1 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149443) {G3,W6,D4,L1,V0,M1} { alpha2( sdtpldt0( xa, smndt0(
% 277.23/277.62 xb ) ), xq ) }.
% 277.23/277.62 parent0[0]: (2827) {G2,W10,D4,L2,V0,M2} Q(2817) { ! aInteger0( sdtasdt0( xp
% 277.23/277.62 , xm ) ), alpha2( sdtpldt0( xa, smndt0( xb ) ), xq ) }.
% 277.23/277.62 parent1[0]: (30287) {G2,W4,D3,L1,V0,M1} R(160,44) { aInteger0( sdtasdt0( xp
% 277.23/277.62 , xm ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (40431) {G3,W6,D4,L1,V0,M1} S(2827);r(30287) { alpha2(
% 277.23/277.62 sdtpldt0( xa, smndt0( xb ) ), xq ) }.
% 277.23/277.62 parent0: (149443) {G3,W6,D4,L1,V0,M1} { alpha2( sdtpldt0( xa, smndt0( xb )
% 277.23/277.62 ), xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149444) {G3,W6,D4,L1,V0,M1} { alpha2( sdtpldt0( xa, smndt0(
% 277.23/277.62 xb ) ), xp ) }.
% 277.23/277.62 parent0[0]: (2808) {G2,W10,D4,L2,V0,M2} Q(2797) { ! aInteger0( sdtasdt0( xq
% 277.23/277.62 , xm ) ), alpha2( sdtpldt0( xa, smndt0( xb ) ), xp ) }.
% 277.23/277.62 parent1[0]: (32071) {G2,W4,D3,L1,V0,M1} R(162,44) { aInteger0( sdtasdt0( xq
% 277.23/277.62 , xm ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (40433) {G3,W6,D4,L1,V0,M1} S(2808);r(32071) { alpha2(
% 277.23/277.62 sdtpldt0( xa, smndt0( xb ) ), xp ) }.
% 277.23/277.62 parent0: (149444) {G3,W6,D4,L1,V0,M1} { alpha2( sdtpldt0( xa, smndt0( xb )
% 277.23/277.62 ), xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149445) {G2,W11,D4,L2,V1,M2} { sdtpldt0( X, smndt0( xb ) ) =
% 277.23/277.62 sdtpldt0( smndt0( xb ), X ), ! aInteger0( X ) }.
% 277.23/277.62 parent0[1]: (294) {G2,W11,D4,L2,V1,M2} R(7,90) { ! aInteger0( X ), sdtpldt0
% 277.23/277.62 ( smndt0( xb ), X ) = sdtpldt0( X, smndt0( xb ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149446) {G1,W9,D4,L1,V0,M1} { sdtpldt0( xa, smndt0( xb ) ) =
% 277.23/277.62 sdtpldt0( smndt0( xb ), xa ) }.
% 277.23/277.62 parent0[1]: (149445) {G2,W11,D4,L2,V1,M2} { sdtpldt0( X, smndt0( xb ) ) =
% 277.23/277.62 sdtpldt0( smndt0( xb ), X ), ! aInteger0( X ) }.
% 277.23/277.62 parent1[0]: (37) {G0,W2,D2,L1,V0,M1} I { aInteger0( xa ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := xa
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (73587) {G3,W9,D4,L1,V0,M1} R(294,37) { sdtpldt0( xa, smndt0(
% 277.23/277.62 xb ) ) ==> sdtpldt0( smndt0( xb ), xa ) }.
% 277.23/277.62 parent0: (149446) {G1,W9,D4,L1,V0,M1} { sdtpldt0( xa, smndt0( xb ) ) =
% 277.23/277.62 sdtpldt0( smndt0( xb ), xa ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149448) {G2,W6,D2,L2,V1,M2} { aDivisorOf0( xp, X ), ! alpha2
% 277.23/277.62 ( X, xp ) }.
% 277.23/277.62 parent0[0]: (30875) {G8,W6,D2,L2,V1,M2} Q(30853);r(30736) { ! alpha1( X, xp
% 277.23/277.62 ), aDivisorOf0( xp, X ) }.
% 277.23/277.62 parent1[1]: (1661) {G1,W6,D2,L2,V1,M2} P(28,40);q { ! alpha2( X, xp ),
% 277.23/277.62 alpha1( X, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (78712) {G9,W6,D2,L2,V1,M2} R(1661,30875) { ! alpha2( X, xp )
% 277.23/277.62 , aDivisorOf0( xp, X ) }.
% 277.23/277.62 parent0: (149448) {G2,W6,D2,L2,V1,M2} { aDivisorOf0( xp, X ), ! alpha2( X
% 277.23/277.62 , xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 1
% 277.23/277.62 1 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149449) {G2,W6,D2,L2,V1,M2} { aDivisorOf0( xq, X ), ! alpha2
% 277.23/277.62 ( X, xq ) }.
% 277.23/277.62 parent0[0]: (32537) {G8,W6,D2,L2,V1,M2} Q(32515);r(32396) { ! alpha1( X, xq
% 277.23/277.62 ), aDivisorOf0( xq, X ) }.
% 277.23/277.62 parent1[1]: (1662) {G1,W6,D2,L2,V1,M2} P(28,42);q { ! alpha2( X, xq ),
% 277.23/277.62 alpha1( X, xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (79620) {G9,W6,D2,L2,V1,M2} R(1662,32537) { ! alpha2( X, xq )
% 277.23/277.62 , aDivisorOf0( xq, X ) }.
% 277.23/277.62 parent0: (149449) {G2,W6,D2,L2,V1,M2} { aDivisorOf0( xq, X ), ! alpha2( X
% 277.23/277.62 , xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := X
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 1
% 277.23/277.62 1 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149451) {G4,W6,D4,L1,V0,M1} { alpha2( sdtpldt0( smndt0( xb ), xa
% 277.23/277.62 ), xq ) }.
% 277.23/277.62 parent0[0]: (73587) {G3,W9,D4,L1,V0,M1} R(294,37) { sdtpldt0( xa, smndt0(
% 277.23/277.62 xb ) ) ==> sdtpldt0( smndt0( xb ), xa ) }.
% 277.23/277.62 parent1[0; 1]: (40431) {G3,W6,D4,L1,V0,M1} S(2827);r(30287) { alpha2(
% 277.23/277.62 sdtpldt0( xa, smndt0( xb ) ), xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (81893) {G4,W6,D4,L1,V0,M1} S(40431);d(73587) { alpha2(
% 277.23/277.62 sdtpldt0( smndt0( xb ), xa ), xq ) }.
% 277.23/277.62 parent0: (149451) {G4,W6,D4,L1,V0,M1} { alpha2( sdtpldt0( smndt0( xb ), xa
% 277.23/277.62 ), xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149453) {G4,W6,D4,L1,V0,M1} { alpha2( sdtpldt0( smndt0( xb ), xa
% 277.23/277.62 ), xp ) }.
% 277.23/277.62 parent0[0]: (73587) {G3,W9,D4,L1,V0,M1} R(294,37) { sdtpldt0( xa, smndt0(
% 277.23/277.62 xb ) ) ==> sdtpldt0( smndt0( xb ), xa ) }.
% 277.23/277.62 parent1[0; 1]: (40433) {G3,W6,D4,L1,V0,M1} S(2808);r(32071) { alpha2(
% 277.23/277.62 sdtpldt0( xa, smndt0( xb ) ), xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (81895) {G4,W6,D4,L1,V0,M1} S(40433);d(73587) { alpha2(
% 277.23/277.62 sdtpldt0( smndt0( xb ), xa ), xp ) }.
% 277.23/277.62 parent0: (149453) {G4,W6,D4,L1,V0,M1} { alpha2( sdtpldt0( smndt0( xb ), xa
% 277.23/277.62 ), xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149455) {G3,W10,D4,L2,V0,M2} { ! aDivisorOf0( xq, sdtpldt0(
% 277.23/277.62 smndt0( xb ), xa ) ), ! sdteqdtlpzmzozddtrp0( xa, xb, xp ) }.
% 277.23/277.62 parent0[0]: (73587) {G3,W9,D4,L1,V0,M1} R(294,37) { sdtpldt0( xa, smndt0(
% 277.23/277.62 xb ) ) ==> sdtpldt0( smndt0( xb ), xa ) }.
% 277.23/277.62 parent1[1; 3]: (20068) {G2,W10,D4,L2,V0,M2} S(2886);r(38);r(41);r(42) { !
% 277.23/277.62 sdteqdtlpzmzozddtrp0( xa, xb, xp ), ! aDivisorOf0( xq, sdtpldt0( xa,
% 277.23/277.62 smndt0( xb ) ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (81901) {G4,W10,D4,L2,V0,M2} S(20068);d(73587) { !
% 277.23/277.62 sdteqdtlpzmzozddtrp0( xa, xb, xp ), ! aDivisorOf0( xq, sdtpldt0( smndt0(
% 277.23/277.62 xb ), xa ) ) }.
% 277.23/277.62 parent0: (149455) {G3,W10,D4,L2,V0,M2} { ! aDivisorOf0( xq, sdtpldt0(
% 277.23/277.62 smndt0( xb ), xa ) ), ! sdteqdtlpzmzozddtrp0( xa, xb, xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 1
% 277.23/277.62 1 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149456) {G5,W6,D4,L1,V0,M1} { aDivisorOf0( xq, sdtpldt0(
% 277.23/277.62 smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent0[0]: (79620) {G9,W6,D2,L2,V1,M2} R(1662,32537) { ! alpha2( X, xq ),
% 277.23/277.62 aDivisorOf0( xq, X ) }.
% 277.23/277.62 parent1[0]: (81893) {G4,W6,D4,L1,V0,M1} S(40431);d(73587) { alpha2(
% 277.23/277.62 sdtpldt0( smndt0( xb ), xa ), xq ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := sdtpldt0( smndt0( xb ), xa )
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (122652) {G10,W6,D4,L1,V0,M1} R(81893,79620) { aDivisorOf0( xq
% 277.23/277.62 , sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent0: (149456) {G5,W6,D4,L1,V0,M1} { aDivisorOf0( xq, sdtpldt0( smndt0
% 277.23/277.62 ( xb ), xa ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149457) {G5,W6,D4,L1,V0,M1} { aDivisorOf0( xp, sdtpldt0(
% 277.23/277.62 smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent0[0]: (78712) {G9,W6,D2,L2,V1,M2} R(1661,30875) { ! alpha2( X, xp ),
% 277.23/277.62 aDivisorOf0( xp, X ) }.
% 277.23/277.62 parent1[0]: (81895) {G4,W6,D4,L1,V0,M1} S(40433);d(73587) { alpha2(
% 277.23/277.62 sdtpldt0( smndt0( xb ), xa ), xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := sdtpldt0( smndt0( xb ), xa )
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (122787) {G10,W6,D4,L1,V0,M1} R(81895,78712) { aDivisorOf0( xp
% 277.23/277.62 , sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent0: (149457) {G5,W6,D4,L1,V0,M1} { aDivisorOf0( xp, sdtpldt0( smndt0
% 277.23/277.62 ( xb ), xa ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149458) {G5,W4,D2,L1,V0,M1} { ! sdteqdtlpzmzozddtrp0( xa, xb
% 277.23/277.62 , xp ) }.
% 277.23/277.62 parent0[1]: (81901) {G4,W10,D4,L2,V0,M2} S(20068);d(73587) { !
% 277.23/277.62 sdteqdtlpzmzozddtrp0( xa, xb, xp ), ! aDivisorOf0( xq, sdtpldt0( smndt0(
% 277.23/277.62 xb ), xa ) ) }.
% 277.23/277.62 parent1[0]: (122652) {G10,W6,D4,L1,V0,M1} R(81893,79620) { aDivisorOf0( xq
% 277.23/277.62 , sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (126029) {G11,W4,D2,L1,V0,M1} S(81901);r(122652) { !
% 277.23/277.62 sdteqdtlpzmzozddtrp0( xa, xb, xp ) }.
% 277.23/277.62 parent0: (149458) {G5,W4,D2,L1,V0,M1} { ! sdteqdtlpzmzozddtrp0( xa, xb, xp
% 277.23/277.62 ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 0
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149459) {G0,W19,D4,L6,V3,M6} { sz00 = X, ! aInteger0( Y ), !
% 277.23/277.62 aInteger0( Z ), ! aInteger0( X ), ! aDivisorOf0( X, sdtpldt0( Y, smndt0(
% 277.23/277.62 Z ) ) ), sdteqdtlpzmzozddtrp0( Y, Z, X ) }.
% 277.23/277.62 parent0[3]: (33) {G0,W19,D4,L6,V3,M6} I { ! aInteger0( X ), ! aInteger0( Y
% 277.23/277.62 ), ! aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y
% 277.23/277.62 ) ) ), sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 X := Y
% 277.23/277.62 Y := Z
% 277.23/277.62 Z := X
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149461) {G1,W15,D4,L5,V0,M5} { sz00 = xp, ! aInteger0( xa ),
% 277.23/277.62 ! aInteger0( xb ), ! aInteger0( xp ), ! aDivisorOf0( xp, sdtpldt0( xa,
% 277.23/277.62 smndt0( xb ) ) ) }.
% 277.23/277.62 parent0[0]: (126029) {G11,W4,D2,L1,V0,M1} S(81901);r(122652) { !
% 277.23/277.62 sdteqdtlpzmzozddtrp0( xa, xb, xp ) }.
% 277.23/277.62 parent1[5]: (149459) {G0,W19,D4,L6,V3,M6} { sz00 = X, ! aInteger0( Y ), !
% 277.23/277.62 aInteger0( Z ), ! aInteger0( X ), ! aDivisorOf0( X, sdtpldt0( Y, smndt0(
% 277.23/277.62 Z ) ) ), sdteqdtlpzmzozddtrp0( Y, Z, X ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 X := xp
% 277.23/277.62 Y := xa
% 277.23/277.62 Z := xb
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 paramod: (149462) {G2,W15,D4,L5,V0,M5} { ! aDivisorOf0( xp, sdtpldt0(
% 277.23/277.62 smndt0( xb ), xa ) ), sz00 = xp, ! aInteger0( xa ), ! aInteger0( xb ), !
% 277.23/277.62 aInteger0( xp ) }.
% 277.23/277.62 parent0[0]: (73587) {G3,W9,D4,L1,V0,M1} R(294,37) { sdtpldt0( xa, smndt0(
% 277.23/277.62 xb ) ) ==> sdtpldt0( smndt0( xb ), xa ) }.
% 277.23/277.62 parent1[4; 3]: (149461) {G1,W15,D4,L5,V0,M5} { sz00 = xp, ! aInteger0( xa
% 277.23/277.62 ), ! aInteger0( xb ), ! aInteger0( xp ), ! aDivisorOf0( xp, sdtpldt0( xa
% 277.23/277.62 , smndt0( xb ) ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149463) {G1,W13,D4,L4,V0,M4} { ! aDivisorOf0( xp, sdtpldt0(
% 277.23/277.62 smndt0( xb ), xa ) ), sz00 = xp, ! aInteger0( xb ), ! aInteger0( xp ) }.
% 277.23/277.62 parent0[2]: (149462) {G2,W15,D4,L5,V0,M5} { ! aDivisorOf0( xp, sdtpldt0(
% 277.23/277.62 smndt0( xb ), xa ) ), sz00 = xp, ! aInteger0( xa ), ! aInteger0( xb ), !
% 277.23/277.62 aInteger0( xp ) }.
% 277.23/277.62 parent1[0]: (37) {G0,W2,D2,L1,V0,M1} I { aInteger0( xa ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 eqswap: (149464) {G1,W13,D4,L4,V0,M4} { xp = sz00, ! aDivisorOf0( xp,
% 277.23/277.62 sdtpldt0( smndt0( xb ), xa ) ), ! aInteger0( xb ), ! aInteger0( xp ) }.
% 277.23/277.62 parent0[1]: (149463) {G1,W13,D4,L4,V0,M4} { ! aDivisorOf0( xp, sdtpldt0(
% 277.23/277.62 smndt0( xb ), xa ) ), sz00 = xp, ! aInteger0( xb ), ! aInteger0( xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (127009) {G12,W13,D4,L4,V0,M4} R(126029,33);d(73587);r(37) { !
% 277.23/277.62 aInteger0( xb ), ! aInteger0( xp ), xp ==> sz00, ! aDivisorOf0( xp,
% 277.23/277.62 sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent0: (149464) {G1,W13,D4,L4,V0,M4} { xp = sz00, ! aDivisorOf0( xp,
% 277.23/277.62 sdtpldt0( smndt0( xb ), xa ) ), ! aInteger0( xb ), ! aInteger0( xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 0 ==> 2
% 277.23/277.62 1 ==> 3
% 277.23/277.62 2 ==> 0
% 277.23/277.62 3 ==> 1
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149467) {G1,W11,D4,L3,V0,M3} { ! aInteger0( xp ), xp ==> sz00
% 277.23/277.62 , ! aDivisorOf0( xp, sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent0[0]: (127009) {G12,W13,D4,L4,V0,M4} R(126029,33);d(73587);r(37) { !
% 277.23/277.62 aInteger0( xb ), ! aInteger0( xp ), xp ==> sz00, ! aDivisorOf0( xp,
% 277.23/277.62 sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent1[0]: (38) {G0,W2,D2,L1,V0,M1} I { aInteger0( xb ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149468) {G1,W9,D4,L2,V0,M2} { xp ==> sz00, ! aDivisorOf0( xp
% 277.23/277.62 , sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent0[0]: (149467) {G1,W11,D4,L3,V0,M3} { ! aInteger0( xp ), xp ==> sz00
% 277.23/277.62 , ! aDivisorOf0( xp, sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent1[0]: (39) {G0,W2,D2,L1,V0,M1} I { aInteger0( xp ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149469) {G1,W6,D4,L1,V0,M1} { ! aDivisorOf0( xp, sdtpldt0(
% 277.23/277.62 smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent0[0]: (40) {G0,W3,D2,L1,V0,M1} I { ! xp ==> sz00 }.
% 277.23/277.62 parent1[0]: (149468) {G1,W9,D4,L2,V0,M2} { xp ==> sz00, ! aDivisorOf0( xp
% 277.23/277.62 , sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 resolution: (149470) {G2,W0,D0,L0,V0,M0} { }.
% 277.23/277.62 parent0[0]: (149469) {G1,W6,D4,L1,V0,M1} { ! aDivisorOf0( xp, sdtpldt0(
% 277.23/277.62 smndt0( xb ), xa ) ) }.
% 277.23/277.62 parent1[0]: (122787) {G10,W6,D4,L1,V0,M1} R(81895,78712) { aDivisorOf0( xp
% 277.23/277.62 , sdtpldt0( smndt0( xb ), xa ) ) }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 substitution1:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 subsumption: (147236) {G13,W0,D0,L0,V0,M0} S(127009);r(38);r(39);r(40);r(
% 277.23/277.62 122787) { }.
% 277.23/277.62 parent0: (149470) {G2,W0,D0,L0,V0,M0} { }.
% 277.23/277.62 substitution0:
% 277.23/277.62 end
% 277.23/277.62 permutation0:
% 277.23/277.62 end
% 277.23/277.62
% 277.23/277.62 Proof check complete!
% 277.23/277.62
% 277.23/277.62 Memory use:
% 277.23/277.62
% 277.23/277.62 space for terms: 1757155
% 277.23/277.62 space for clauses: 8435090
% 277.23/277.62
% 277.23/277.62
% 277.23/277.62 clauses generated: 795597
% 277.23/277.62 clauses kept: 147237
% 277.23/277.62 clauses selected: 3036
% 277.23/277.62 clauses deleted: 58007
% 277.23/277.62 clauses inuse deleted: 548
% 277.23/277.62
% 277.23/277.62 subsentry: 2889896
% 277.23/277.62 literals s-matched: 1011694
% 277.23/277.62 literals matched: 942149
% 277.23/277.62 full subsumption: 354283
% 277.23/277.62
% 277.23/277.62 checksum: 2000525682
% 277.23/277.62
% 277.23/277.62
% 277.23/277.62 Bliksem ended
%------------------------------------------------------------------------------