%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM427+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n021.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:09 EDT 2022
% Result : Theorem 71.73s 72.20s
% Output : Refutation 71.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM427+1 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n021.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Wed Jul 6 13:24:18 EDT 2022
% 0.12/0.33 % CPUTime :
% 9.34/9.78 *** allocated 10000 integers for termspace/termends
% 9.34/9.78 *** allocated 10000 integers for clauses
% 9.34/9.78 *** allocated 10000 integers for justifications
% 9.34/9.78 Bliksem 1.12
% 9.34/9.78
% 9.34/9.78
% 9.34/9.78 Automatic Strategy Selection
% 9.34/9.78
% 9.34/9.78
% 9.34/9.78 Clauses:
% 9.34/9.78
% 9.34/9.78 { && }.
% 9.34/9.78 { aInteger0( sz00 ) }.
% 9.34/9.78 { aInteger0( sz10 ) }.
% 9.34/9.78 { ! aInteger0( X ), aInteger0( smndt0( X ) ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), aInteger0( sdtpldt0( X, Y ) ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), aInteger0( sdtasdt0( X, Y ) ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), sdtpldt0( X,
% 9.34/9.78 sdtpldt0( Y, Z ) ) = sdtpldt0( sdtpldt0( X, Y ), Z ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }
% 9.34/9.78 .
% 9.34/9.78 { ! aInteger0( X ), sdtpldt0( X, sz00 ) = X }.
% 9.34/9.78 { ! aInteger0( X ), X = sdtpldt0( sz00, X ) }.
% 9.34/9.78 { ! aInteger0( X ), sdtpldt0( X, smndt0( X ) ) = sz00 }.
% 9.34/9.78 { ! aInteger0( X ), sz00 = sdtpldt0( smndt0( X ), X ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), sdtasdt0( X,
% 9.34/9.78 sdtasdt0( Y, Z ) ) = sdtasdt0( sdtasdt0( X, Y ), Z ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }
% 9.34/9.78 .
% 9.34/9.78 { ! aInteger0( X ), sdtasdt0( X, sz10 ) = X }.
% 9.34/9.78 { ! aInteger0( X ), X = sdtasdt0( sz10, X ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), sdtasdt0( X,
% 9.34/9.78 sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), sdtasdt0( sdtpldt0
% 9.34/9.78 ( X, Y ), Z ) = sdtpldt0( sdtasdt0( X, Z ), sdtasdt0( Y, Z ) ) }.
% 9.34/9.78 { ! aInteger0( X ), sdtasdt0( X, sz00 ) = sz00 }.
% 9.34/9.78 { ! aInteger0( X ), sz00 = sdtasdt0( sz00, X ) }.
% 9.34/9.78 { ! aInteger0( X ), sdtasdt0( smndt0( sz10 ), X ) = smndt0( X ) }.
% 9.34/9.78 { ! aInteger0( X ), smndt0( X ) = sdtasdt0( X, smndt0( sz10 ) ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), ! sdtasdt0( X, Y ) = sz00, X = sz00,
% 9.34/9.78 Y = sz00 }.
% 9.34/9.78 { ! aInteger0( X ), ! aDivisorOf0( Y, X ), aInteger0( Y ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aDivisorOf0( Y, X ), alpha1( X, Y ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), ! alpha1( X, Y ), aDivisorOf0( Y, X )
% 9.34/9.78 }.
% 9.34/9.78 { ! alpha1( X, Y ), ! Y = sz00 }.
% 9.34/9.78 { ! alpha1( X, Y ), alpha2( X, Y ) }.
% 9.34/9.78 { Y = sz00, ! alpha2( X, Y ), alpha1( X, Y ) }.
% 9.34/9.78 { ! alpha2( X, Y ), aInteger0( skol1( Z, T ) ) }.
% 9.34/9.78 { ! alpha2( X, Y ), sdtasdt0( Y, skol1( X, Y ) ) = X }.
% 9.34/9.78 { ! aInteger0( Z ), ! sdtasdt0( Y, Z ) = X, alpha2( X, Y ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), Z = sz00, !
% 9.34/9.78 sdteqdtlpzmzozddtrp0( X, Y, Z ), aDivisorOf0( Z, sdtpldt0( X, smndt0( Y )
% 9.34/9.78 ) ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), ! aInteger0( Z ), Z = sz00, !
% 9.34/9.78 aDivisorOf0( Z, sdtpldt0( X, smndt0( Y ) ) ), sdteqdtlpzmzozddtrp0( X, Y
% 9.34/9.78 , Z ) }.
% 9.34/9.78 { ! aInteger0( X ), ! aInteger0( Y ), Y = sz00, sdteqdtlpzmzozddtrp0( X, X
% 9.34/9.78 , Y ) }.
% 9.34/9.78 { aInteger0( xa ) }.
% 9.34/9.78 { aInteger0( xb ) }.
% 9.34/9.78 { aInteger0( xq ) }.
% 9.34/9.78 { ! xq = sz00 }.
% 9.34/9.78 { sdteqdtlpzmzozddtrp0( xa, xb, xq ) }.
% 9.34/9.78 { aInteger0( xn ) }.
% 9.34/9.78 { sdtasdt0( xq, xn ) = sdtpldt0( xa, smndt0( xb ) ) }.
% 9.34/9.78 { sdtasdt0( xq, smndt0( xn ) ) = sdtpldt0( xb, smndt0( xa ) ) }.
% 9.34/9.78 { ! sdteqdtlpzmzozddtrp0( xb, xa, xq ) }.
% 9.34/9.78
% 9.34/9.78 percentage equality = 0.271028, percentage horn = 0.886364
% 9.34/9.78 This is a problem with some equality
% 9.34/9.78
% 9.34/9.78
% 9.34/9.78
% 9.34/9.78 Options Used:
% 9.34/9.78
% 9.34/9.78 useres = 1
% 9.34/9.78 useparamod = 1
% 9.34/9.78 useeqrefl = 1
% 9.34/9.78 useeqfact = 1
% 9.34/9.78 usefactor = 1
% 9.34/9.78 usesimpsplitting = 0
% 9.34/9.78 usesimpdemod = 5
% 9.34/9.78 usesimpres = 3
% 9.34/9.78
% 9.34/9.78 resimpinuse = 1000
% 9.34/9.78 resimpclauses = 20000
% 9.34/9.78 substype = eqrewr
% 9.34/9.78 backwardsubs = 1
% 9.34/9.78 selectoldest = 5
% 9.34/9.78
% 9.34/9.78 litorderings [0] = split
% 9.34/9.78 litorderings [1] = extend the termordering, first sorting on arguments
% 9.34/9.78
% 9.34/9.78 termordering = kbo
% 9.34/9.78
% 9.34/9.78 litapriori = 0
% 9.34/9.78 termapriori = 1
% 9.34/9.78 litaposteriori = 0
% 9.34/9.78 termaposteriori = 0
% 9.34/9.78 demodaposteriori = 0
% 9.34/9.78 ordereqreflfact = 0
% 9.34/9.78
% 9.34/9.78 litselect = negord
% 9.34/9.78
% 9.34/9.78 maxweight = 15
% 9.34/9.78 maxdepth = 30000
% 9.34/9.78 maxlength = 115
% 9.34/9.78 maxnrvars = 195
% 9.34/9.78 excuselevel = 1
% 9.34/9.78 increasemaxweight = 1
% 9.34/9.78
% 9.34/9.78 maxselected = 10000000
% 9.34/9.78 maxnrclauses = 10000000
% 9.34/9.78
% 9.34/9.78 showgenerated = 0
% 9.34/9.78 showkept = 0
% 9.34/9.78 showselected = 0
% 9.34/9.78 showdeleted = 0
% 9.34/9.78 showresimp = 1
% 9.34/9.78 showstatus = 2000
% 9.34/9.78
% 9.34/9.78 prologoutput = 0
% 9.34/9.78 nrgoals = 5000000
% 9.34/9.78 totalproof = 1
% 9.34/9.78
% 9.34/9.78 Symbols occurring in the translation:
% 71.73/72.19
% 71.73/72.19 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 71.73/72.19 . [1, 2] (w:1, o:22, a:1, s:1, b:0),
% 71.73/72.19 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 71.73/72.19 ! [4, 1] (w:0, o:15, a:1, s:1, b:0),
% 71.73/72.19 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 71.73/72.19 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 71.73/72.19 aInteger0 [36, 1] (w:1, o:20, a:1, s:1, b:0),
% 71.73/72.19 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 71.73/72.19 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 71.73/72.19 smndt0 [39, 1] (w:1, o:21, a:1, s:1, b:0),
% 71.73/72.19 sdtpldt0 [41, 2] (w:1, o:46, a:1, s:1, b:0),
% 71.73/72.19 sdtasdt0 [42, 2] (w:1, o:47, a:1, s:1, b:0),
% 71.73/72.19 aDivisorOf0 [44, 2] (w:1, o:48, a:1, s:1, b:0),
% 71.73/72.19 sdteqdtlpzmzozddtrp0 [45, 3] (w:1, o:52, a:1, s:1, b:0),
% 71.73/72.19 xa [46, 0] (w:1, o:11, a:1, s:1, b:0),
% 71.73/72.19 xb [47, 0] (w:1, o:12, a:1, s:1, b:0),
% 71.73/72.19 xq [48, 0] (w:1, o:13, a:1, s:1, b:0),
% 71.73/72.19 xn [49, 0] (w:1, o:14, a:1, s:1, b:0),
% 71.73/72.19 alpha1 [50, 2] (w:1, o:49, a:1, s:1, b:1),
% 71.73/72.19 alpha2 [51, 2] (w:1, o:50, a:1, s:1, b:1),
% 71.73/72.19 skol1 [52, 2] (w:1, o:51, a:1, s:1, b:1).
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Starting Search:
% 71.73/72.19
% 71.73/72.19 *** allocated 15000 integers for clauses
% 71.73/72.19 *** allocated 22500 integers for clauses
% 71.73/72.19 *** allocated 33750 integers for clauses
% 71.73/72.19 *** allocated 50625 integers for clauses
% 71.73/72.19 *** allocated 75937 integers for clauses
% 71.73/72.19 *** allocated 15000 integers for termspace/termends
% 71.73/72.19 *** allocated 113905 integers for clauses
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 22500 integers for termspace/termends
% 71.73/72.19 *** allocated 170857 integers for clauses
% 71.73/72.19 *** allocated 33750 integers for termspace/termends
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 5538
% 71.73/72.19 Kept: 2132
% 71.73/72.19 Inuse: 140
% 71.73/72.19 Deleted: 7
% 71.73/72.19 Deletedinuse: 6
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 50625 integers for termspace/termends
% 71.73/72.19 *** allocated 256285 integers for clauses
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 384427 integers for clauses
% 71.73/72.19 *** allocated 75937 integers for termspace/termends
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 16370
% 71.73/72.19 Kept: 4170
% 71.73/72.19 Inuse: 277
% 71.73/72.19 Deleted: 12
% 71.73/72.19 Deletedinuse: 8
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 113905 integers for termspace/termends
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 27163
% 71.73/72.19 Kept: 6258
% 71.73/72.19 Inuse: 345
% 71.73/72.19 Deleted: 15
% 71.73/72.19 Deletedinuse: 9
% 71.73/72.19
% 71.73/72.19 *** allocated 576640 integers for clauses
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 32729
% 71.73/72.19 Kept: 8327
% 71.73/72.19 Inuse: 383
% 71.73/72.19 Deleted: 17
% 71.73/72.19 Deletedinuse: 9
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 864960 integers for clauses
% 71.73/72.19 *** allocated 170857 integers for termspace/termends
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 37273
% 71.73/72.19 Kept: 10355
% 71.73/72.19 Inuse: 410
% 71.73/72.19 Deleted: 17
% 71.73/72.19 Deletedinuse: 9
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 42769
% 71.73/72.19 Kept: 12519
% 71.73/72.19 Inuse: 458
% 71.73/72.19 Deleted: 17
% 71.73/72.19 Deletedinuse: 9
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 256285 integers for termspace/termends
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 47723
% 71.73/72.19 Kept: 15134
% 71.73/72.19 Inuse: 488
% 71.73/72.19 Deleted: 17
% 71.73/72.19 Deletedinuse: 9
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 1297440 integers for clauses
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 52701
% 71.73/72.19 Kept: 17401
% 71.73/72.19 Inuse: 508
% 71.73/72.19 Deleted: 17
% 71.73/72.19 Deletedinuse: 9
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 58045
% 71.73/72.19 Kept: 20368
% 71.73/72.19 Inuse: 523
% 71.73/72.19 Deleted: 17
% 71.73/72.19 Deletedinuse: 9
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying clauses:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 384427 integers for termspace/termends
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 62261
% 71.73/72.19 Kept: 23165
% 71.73/72.19 Inuse: 533
% 71.73/72.19 Deleted: 559
% 71.73/72.19 Deletedinuse: 11
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 1946160 integers for clauses
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 65856
% 71.73/72.19 Kept: 25353
% 71.73/72.19 Inuse: 548
% 71.73/72.19 Deleted: 559
% 71.73/72.19 Deletedinuse: 11
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 69903
% 71.73/72.19 Kept: 27633
% 71.73/72.19 Inuse: 566
% 71.73/72.19 Deleted: 562
% 71.73/72.19 Deletedinuse: 12
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 74008
% 71.73/72.19 Kept: 29991
% 71.73/72.19 Inuse: 579
% 71.73/72.19 Deleted: 564
% 71.73/72.19 Deletedinuse: 12
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 78700
% 71.73/72.19 Kept: 32123
% 71.73/72.19 Inuse: 604
% 71.73/72.19 Deleted: 564
% 71.73/72.19 Deletedinuse: 12
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 576640 integers for termspace/termends
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 87419
% 71.73/72.19 Kept: 34366
% 71.73/72.19 Inuse: 649
% 71.73/72.19 Deleted: 564
% 71.73/72.19 Deletedinuse: 12
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 2919240 integers for clauses
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 92512
% 71.73/72.19 Kept: 36373
% 71.73/72.19 Inuse: 684
% 71.73/72.19 Deleted: 564
% 71.73/72.19 Deletedinuse: 12
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 96407
% 71.73/72.19 Kept: 38529
% 71.73/72.19 Inuse: 714
% 71.73/72.19 Deleted: 564
% 71.73/72.19 Deletedinuse: 12
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 101633
% 71.73/72.19 Kept: 40555
% 71.73/72.19 Inuse: 731
% 71.73/72.19 Deleted: 564
% 71.73/72.19 Deletedinuse: 12
% 71.73/72.19
% 71.73/72.19 Resimplifying clauses:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 113105
% 71.73/72.19 Kept: 42696
% 71.73/72.19 Inuse: 760
% 71.73/72.19 Deleted: 881
% 71.73/72.19 Deletedinuse: 12
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 121582
% 71.73/72.19 Kept: 44784
% 71.73/72.19 Inuse: 789
% 71.73/72.19 Deleted: 881
% 71.73/72.19 Deletedinuse: 12
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 149688
% 71.73/72.19 Kept: 46880
% 71.73/72.19 Inuse: 938
% 71.73/72.19 Deleted: 897
% 71.73/72.19 Deletedinuse: 12
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 156451
% 71.73/72.19 Kept: 48990
% 71.73/72.19 Inuse: 970
% 71.73/72.19 Deleted: 901
% 71.73/72.19 Deletedinuse: 13
% 71.73/72.19
% 71.73/72.19 *** allocated 864960 integers for termspace/termends
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19
% 71.73/72.19 Intermediate Status:
% 71.73/72.19 Generated: 163024
% 71.73/72.19 Kept: 51082
% 71.73/72.19 Inuse: 997
% 71.73/72.19 Deleted: 904
% 71.73/72.19 Deletedinuse: 13
% 71.73/72.19
% 71.73/72.19 Resimplifying inuse:
% 71.73/72.19 Done
% 71.73/72.19
% 71.73/72.19 *** allocated 4378860 integers for clauses
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Intermediate Status:
% 71.73/72.20 Generated: 185485
% 71.73/72.20 Kept: 53253
% 71.73/72.20 Inuse: 1087
% 71.73/72.20 Deleted: 924
% 71.73/72.20 Deletedinuse: 33
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Intermediate Status:
% 71.73/72.20 Generated: 200466
% 71.73/72.20 Kept: 55273
% 71.73/72.20 Inuse: 1129
% 71.73/72.20 Deleted: 1014
% 71.73/72.20 Deletedinuse: 117
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Intermediate Status:
% 71.73/72.20 Generated: 206983
% 71.73/72.20 Kept: 57283
% 71.73/72.20 Inuse: 1142
% 71.73/72.20 Deleted: 1014
% 71.73/72.20 Deletedinuse: 117
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Intermediate Status:
% 71.73/72.20 Generated: 211156
% 71.73/72.20 Kept: 59575
% 71.73/72.20 Inuse: 1151
% 71.73/72.20 Deleted: 1014
% 71.73/72.20 Deletedinuse: 117
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20 Resimplifying clauses:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Intermediate Status:
% 71.73/72.20 Generated: 225699
% 71.73/72.20 Kept: 61751
% 71.73/72.20 Inuse: 1176
% 71.73/72.20 Deleted: 10871
% 71.73/72.20 Deletedinuse: 117
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Intermediate Status:
% 71.73/72.20 Generated: 230908
% 71.73/72.20 Kept: 64079
% 71.73/72.20 Inuse: 1186
% 71.73/72.20 Deleted: 10871
% 71.73/72.20 Deletedinuse: 117
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Intermediate Status:
% 71.73/72.20 Generated: 235807
% 71.73/72.20 Kept: 66143
% 71.73/72.20 Inuse: 1196
% 71.73/72.20 Deleted: 10871
% 71.73/72.20 Deletedinuse: 117
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20 Resimplifying inuse:
% 71.73/72.20 Done
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Intermediate Status:
% 71.73/72.20 Generated: 242065
% 71.73/72.20 Kept: 68213
% 71.73/72.20 Inuse: 1212
% 71.73/72.20 Deleted: 10871
% 71.73/72.20 Deletedinuse: 117
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Bliksems!, er is een bewijs:
% 71.73/72.20 % SZS status Theorem
% 71.73/72.20 % SZS output start Refutation
% 71.73/72.20
% 71.73/72.20 (1) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz00 ) }.
% 71.73/72.20 (2) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz10 ) }.
% 71.73/72.20 (3) {G0,W5,D3,L2,V1,M2} I { ! aInteger0( X ), aInteger0( smndt0( X ) ) }.
% 71.73/72.20 (5) {G0,W8,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y ), aInteger0(
% 71.73/72.20 sdtasdt0( X, Y ) ) }.
% 71.73/72.20 (7) {G0,W11,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y ), sdtpldt0(
% 71.73/72.20 X, Y ) = sdtpldt0( Y, X ) }.
% 71.73/72.20 (14) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X, sz10 ) ==> X
% 71.73/72.20 }.
% 71.73/72.20 (18) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X, sz00 ) ==> sz00
% 71.73/72.20 }.
% 71.73/72.20 (25) {G0,W10,D2,L4,V2,M4} I { ! aInteger0( X ), ! aInteger0( Y ), ! alpha1
% 71.73/72.20 ( X, Y ), aDivisorOf0( Y, X ) }.
% 71.73/72.20 (27) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), alpha2( X, Y ) }.
% 71.73/72.20 (28) {G0,W9,D2,L3,V2,M3} I { Y = sz00, ! alpha2( X, Y ), alpha1( X, Y ) }.
% 71.73/72.20 (29) {G0,W7,D3,L2,V4,M2} I { ! alpha2( X, Y ), aInteger0( skol1( Z, T ) )
% 71.73/72.20 }.
% 71.73/72.20 (30) {G0,W10,D4,L2,V2,M2} I { ! alpha2( X, Y ), sdtasdt0( Y, skol1( X, Y )
% 71.73/72.20 ) ==> X }.
% 71.73/72.20 (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y, Z ) = X,
% 71.73/72.20 alpha2( X, Y ) }.
% 71.73/72.20 (33) {G0,W19,D4,L6,V3,M6} I { ! aInteger0( X ), ! aInteger0( Y ), !
% 71.73/72.20 aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y ) ) )
% 71.73/72.20 , sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 71.73/72.20 (35) {G0,W2,D2,L1,V0,M1} I { aInteger0( xa ) }.
% 71.73/72.20 (36) {G0,W2,D2,L1,V0,M1} I { aInteger0( xb ) }.
% 71.73/72.20 (37) {G0,W2,D2,L1,V0,M1} I { aInteger0( xq ) }.
% 71.73/72.20 (38) {G0,W3,D2,L1,V0,M1} I { ! xq ==> sz00 }.
% 71.73/72.20 (40) {G0,W2,D2,L1,V0,M1} I { aInteger0( xn ) }.
% 71.73/72.20 (42) {G0,W9,D4,L1,V0,M1} I { sdtasdt0( xq, smndt0( xn ) ) ==> sdtpldt0( xb
% 71.73/72.20 , smndt0( xa ) ) }.
% 71.73/72.20 (43) {G0,W4,D2,L1,V0,M1} I { ! sdteqdtlpzmzozddtrp0( xb, xa, xq ) }.
% 71.73/72.20 (79) {G1,W3,D3,L1,V0,M1} R(3,35) { aInteger0( smndt0( xa ) ) }.
% 71.73/72.20 (82) {G1,W3,D3,L1,V0,M1} R(3,40) { aInteger0( smndt0( xn ) ) }.
% 71.73/72.20 (147) {G1,W6,D3,L2,V1,M2} R(5,37) { ! aInteger0( X ), aInteger0( sdtasdt0(
% 71.73/72.20 xq, X ) ) }.
% 71.73/72.20 (275) {G2,W11,D4,L2,V1,M2} R(7,79) { ! aInteger0( X ), sdtpldt0( smndt0( xa
% 71.73/72.20 ), X ) = sdtpldt0( X, smndt0( xa ) ) }.
% 71.73/72.20 (693) {G1,W5,D3,L1,V0,M1} R(14,37) { sdtasdt0( xq, sz10 ) ==> xq }.
% 71.73/72.20 (915) {G1,W5,D3,L1,V0,M1} R(18,40) { sdtasdt0( xn, sz00 ) ==> sz00 }.
% 71.73/72.20 (1816) {G1,W6,D2,L2,V1,M2} P(28,38);q { ! alpha2( X, xq ), alpha1( X, xq )
% 71.73/72.20 }.
% 71.73/72.20 (2004) {G2,W9,D4,L2,V2,M2} R(31,82) { ! sdtasdt0( X, smndt0( xn ) ) = Y,
% 71.73/72.20 alpha2( Y, X ) }.
% 71.73/72.20 (2021) {G2,W6,D2,L2,V1,M2} P(915,31);r(1) { ! sz00 = X, alpha2( X, xn ) }.
% 71.73/72.20 (2029) {G2,W6,D2,L2,V1,M2} P(693,31);r(2) { ! xq = X, alpha2( X, xq ) }.
% 71.73/72.20 (2069) {G3,W3,D2,L1,V0,M1} Q(2021) { alpha2( sz00, xn ) }.
% 71.73/72.20 (2084) {G3,W6,D4,L1,V1,M1} Q(2004) { alpha2( sdtasdt0( X, smndt0( xn ) ), X
% 71.73/72.20 ) }.
% 71.73/72.20 (2133) {G4,W4,D3,L1,V2,M1} R(2069,29) { aInteger0( skol1( X, Y ) ) }.
% 71.73/72.20 (2254) {G1,W13,D4,L4,V0,M4} R(33,43);r(36) { ! aInteger0( xa ), ! aInteger0
% 71.73/72.20 ( xq ), xq ==> sz00, ! aDivisorOf0( xq, sdtpldt0( xb, smndt0( xa ) ) )
% 71.73/72.20 }.
% 71.73/72.20 (20439) {G2,W6,D4,L1,V0,M1} S(2254);r(35);r(37);r(38) { ! aDivisorOf0( xq,
% 71.73/72.20 sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 (29150) {G5,W5,D2,L2,V1,M2} P(30,147);r(2133) { aInteger0( X ), ! alpha2( X
% 71.73/72.20 , xq ) }.
% 71.73/72.20 (29304) {G6,W5,D2,L2,V1,M2} R(29150,2029) { aInteger0( X ), ! xq = X }.
% 71.73/72.20 (29348) {G6,W5,D2,L2,V1,M2} R(29150,27) { aInteger0( X ), ! alpha1( X, xq )
% 71.73/72.20 }.
% 71.73/72.20 (29458) {G7,W11,D2,L4,V2,M4} R(29304,25) { ! xq = X, ! aInteger0( Y ), !
% 71.73/72.20 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 71.73/72.20 (29481) {G8,W6,D2,L2,V1,M2} Q(29458);r(29348) { ! alpha1( X, xq ),
% 71.73/72.20 aDivisorOf0( xq, X ) }.
% 71.73/72.20 (48234) {G9,W6,D2,L2,V1,M2} R(1816,29481) { ! alpha2( X, xq ), aDivisorOf0
% 71.73/72.20 ( xq, X ) }.
% 71.73/72.20 (52543) {G3,W9,D4,L1,V0,M1} R(275,36) { sdtpldt0( xb, smndt0( xa ) ) ==>
% 71.73/72.20 sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 (52749) {G4,W9,D4,L1,V0,M1} S(42);d(52543) { sdtasdt0( xq, smndt0( xn ) )
% 71.73/72.20 ==> sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 (61141) {G4,W6,D4,L1,V0,M1} S(20439);d(52543) { ! aDivisorOf0( xq, sdtpldt0
% 71.73/72.20 ( smndt0( xa ), xb ) ) }.
% 71.73/72.20 (68373) {G10,W0,D0,L0,V0,M0} R(2084,48234);d(52749);r(61141) { }.
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 % SZS output end Refutation
% 71.73/72.20 found a proof!
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Unprocessed initial clauses:
% 71.73/72.20
% 71.73/72.20 (68375) {G0,W1,D1,L1,V0,M1} { && }.
% 71.73/72.20 (68376) {G0,W2,D2,L1,V0,M1} { aInteger0( sz00 ) }.
% 71.73/72.20 (68377) {G0,W2,D2,L1,V0,M1} { aInteger0( sz10 ) }.
% 71.73/72.20 (68378) {G0,W5,D3,L2,V1,M2} { ! aInteger0( X ), aInteger0( smndt0( X ) )
% 71.73/72.20 }.
% 71.73/72.20 (68379) {G0,W8,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y ),
% 71.73/72.20 aInteger0( sdtpldt0( X, Y ) ) }.
% 71.73/72.20 (68380) {G0,W8,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y ),
% 71.73/72.20 aInteger0( sdtasdt0( X, Y ) ) }.
% 71.73/72.20 (68381) {G0,W17,D4,L4,V3,M4} { ! aInteger0( X ), ! aInteger0( Y ), !
% 71.73/72.20 aInteger0( Z ), sdtpldt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtpldt0( X,
% 71.73/72.20 Y ), Z ) }.
% 71.73/72.20 (68382) {G0,W11,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y ),
% 71.73/72.20 sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 71.73/72.20 (68383) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sdtpldt0( X, sz00 ) = X
% 71.73/72.20 }.
% 71.73/72.20 (68384) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), X = sdtpldt0( sz00, X )
% 71.73/72.20 }.
% 71.73/72.20 (68385) {G0,W8,D4,L2,V1,M2} { ! aInteger0( X ), sdtpldt0( X, smndt0( X ) )
% 71.73/72.20 = sz00 }.
% 71.73/72.20 (68386) {G0,W8,D4,L2,V1,M2} { ! aInteger0( X ), sz00 = sdtpldt0( smndt0( X
% 71.73/72.20 ), X ) }.
% 71.73/72.20 (68387) {G0,W17,D4,L4,V3,M4} { ! aInteger0( X ), ! aInteger0( Y ), !
% 71.73/72.20 aInteger0( Z ), sdtasdt0( X, sdtasdt0( Y, Z ) ) = sdtasdt0( sdtasdt0( X,
% 71.73/72.20 Y ), Z ) }.
% 71.73/72.20 (68388) {G0,W11,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y ),
% 71.73/72.20 sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 71.73/72.20 (68389) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sdtasdt0( X, sz10 ) = X
% 71.73/72.20 }.
% 71.73/72.20 (68390) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), X = sdtasdt0( sz10, X )
% 71.73/72.20 }.
% 71.73/72.20 (68391) {G0,W19,D4,L4,V3,M4} { ! aInteger0( X ), ! aInteger0( Y ), !
% 71.73/72.20 aInteger0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X,
% 71.73/72.20 Y ), sdtasdt0( X, Z ) ) }.
% 71.73/72.20 (68392) {G0,W19,D4,L4,V3,M4} { ! aInteger0( X ), ! aInteger0( Y ), !
% 71.73/72.20 aInteger0( Z ), sdtasdt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( sdtasdt0( X,
% 71.73/72.20 Z ), sdtasdt0( Y, Z ) ) }.
% 71.73/72.20 (68393) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sdtasdt0( X, sz00 ) = sz00
% 71.73/72.20 }.
% 71.73/72.20 (68394) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sz00 = sdtasdt0( sz00, X )
% 71.73/72.20 }.
% 71.73/72.20 (68395) {G0,W9,D4,L2,V1,M2} { ! aInteger0( X ), sdtasdt0( smndt0( sz10 ),
% 71.73/72.20 X ) = smndt0( X ) }.
% 71.73/72.20 (68396) {G0,W9,D4,L2,V1,M2} { ! aInteger0( X ), smndt0( X ) = sdtasdt0( X
% 71.73/72.20 , smndt0( sz10 ) ) }.
% 71.73/72.20 (68397) {G0,W15,D3,L5,V2,M5} { ! aInteger0( X ), ! aInteger0( Y ), !
% 71.73/72.20 sdtasdt0( X, Y ) = sz00, X = sz00, Y = sz00 }.
% 71.73/72.20 (68398) {G0,W7,D2,L3,V2,M3} { ! aInteger0( X ), ! aDivisorOf0( Y, X ),
% 71.73/72.20 aInteger0( Y ) }.
% 71.73/72.20 (68399) {G0,W8,D2,L3,V2,M3} { ! aInteger0( X ), ! aDivisorOf0( Y, X ),
% 71.73/72.20 alpha1( X, Y ) }.
% 71.73/72.20 (68400) {G0,W10,D2,L4,V2,M4} { ! aInteger0( X ), ! aInteger0( Y ), !
% 71.73/72.20 alpha1( X, Y ), aDivisorOf0( Y, X ) }.
% 71.73/72.20 (68401) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), ! Y = sz00 }.
% 71.73/72.20 (68402) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), alpha2( X, Y ) }.
% 71.73/72.20 (68403) {G0,W9,D2,L3,V2,M3} { Y = sz00, ! alpha2( X, Y ), alpha1( X, Y )
% 71.73/72.20 }.
% 71.73/72.20 (68404) {G0,W7,D3,L2,V4,M2} { ! alpha2( X, Y ), aInteger0( skol1( Z, T ) )
% 71.73/72.20 }.
% 71.73/72.20 (68405) {G0,W10,D4,L2,V2,M2} { ! alpha2( X, Y ), sdtasdt0( Y, skol1( X, Y
% 71.73/72.20 ) ) = X }.
% 71.73/72.20 (68406) {G0,W10,D3,L3,V3,M3} { ! aInteger0( Z ), ! sdtasdt0( Y, Z ) = X,
% 71.73/72.20 alpha2( X, Y ) }.
% 71.73/72.20 (68407) {G0,W19,D4,L6,V3,M6} { ! aInteger0( X ), ! aInteger0( Y ), !
% 71.73/72.20 aInteger0( Z ), Z = sz00, ! sdteqdtlpzmzozddtrp0( X, Y, Z ), aDivisorOf0
% 71.73/72.20 ( Z, sdtpldt0( X, smndt0( Y ) ) ) }.
% 71.73/72.20 (68408) {G0,W19,D4,L6,V3,M6} { ! aInteger0( X ), ! aInteger0( Y ), !
% 71.73/72.20 aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y ) ) )
% 71.73/72.20 , sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 71.73/72.20 (68409) {G0,W11,D2,L4,V2,M4} { ! aInteger0( X ), ! aInteger0( Y ), Y =
% 71.73/72.20 sz00, sdteqdtlpzmzozddtrp0( X, X, Y ) }.
% 71.73/72.20 (68410) {G0,W2,D2,L1,V0,M1} { aInteger0( xa ) }.
% 71.73/72.20 (68411) {G0,W2,D2,L1,V0,M1} { aInteger0( xb ) }.
% 71.73/72.20 (68412) {G0,W2,D2,L1,V0,M1} { aInteger0( xq ) }.
% 71.73/72.20 (68413) {G0,W3,D2,L1,V0,M1} { ! xq = sz00 }.
% 71.73/72.20 (68414) {G0,W4,D2,L1,V0,M1} { sdteqdtlpzmzozddtrp0( xa, xb, xq ) }.
% 71.73/72.20 (68415) {G0,W2,D2,L1,V0,M1} { aInteger0( xn ) }.
% 71.73/72.20 (68416) {G0,W8,D4,L1,V0,M1} { sdtasdt0( xq, xn ) = sdtpldt0( xa, smndt0(
% 71.73/72.20 xb ) ) }.
% 71.73/72.20 (68417) {G0,W9,D4,L1,V0,M1} { sdtasdt0( xq, smndt0( xn ) ) = sdtpldt0( xb
% 71.73/72.20 , smndt0( xa ) ) }.
% 71.73/72.20 (68418) {G0,W4,D2,L1,V0,M1} { ! sdteqdtlpzmzozddtrp0( xb, xa, xq ) }.
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Total Proof:
% 71.73/72.20
% 71.73/72.20 subsumption: (1) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz00 ) }.
% 71.73/72.20 parent0: (68376) {G0,W2,D2,L1,V0,M1} { aInteger0( sz00 ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (2) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz10 ) }.
% 71.73/72.20 parent0: (68377) {G0,W2,D2,L1,V0,M1} { aInteger0( sz10 ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (3) {G0,W5,D3,L2,V1,M2} I { ! aInteger0( X ), aInteger0(
% 71.73/72.20 smndt0( X ) ) }.
% 71.73/72.20 parent0: (68378) {G0,W5,D3,L2,V1,M2} { ! aInteger0( X ), aInteger0( smndt0
% 71.73/72.20 ( X ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (5) {G0,W8,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y )
% 71.73/72.20 , aInteger0( sdtasdt0( X, Y ) ) }.
% 71.73/72.20 parent0: (68380) {G0,W8,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y )
% 71.73/72.20 , aInteger0( sdtasdt0( X, Y ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 2 ==> 2
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (7) {G0,W11,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y
% 71.73/72.20 ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 71.73/72.20 parent0: (68382) {G0,W11,D3,L3,V2,M3} { ! aInteger0( X ), ! aInteger0( Y )
% 71.73/72.20 , sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 2 ==> 2
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (14) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X,
% 71.73/72.20 sz10 ) ==> X }.
% 71.73/72.20 parent0: (68389) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sdtasdt0( X, sz10
% 71.73/72.20 ) = X }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (18) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X,
% 71.73/72.20 sz00 ) ==> sz00 }.
% 71.73/72.20 parent0: (68393) {G0,W7,D3,L2,V1,M2} { ! aInteger0( X ), sdtasdt0( X, sz00
% 71.73/72.20 ) = sz00 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (25) {G0,W10,D2,L4,V2,M4} I { ! aInteger0( X ), ! aInteger0( Y
% 71.73/72.20 ), ! alpha1( X, Y ), aDivisorOf0( Y, X ) }.
% 71.73/72.20 parent0: (68400) {G0,W10,D2,L4,V2,M4} { ! aInteger0( X ), ! aInteger0( Y )
% 71.73/72.20 , ! alpha1( X, Y ), aDivisorOf0( Y, X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 2 ==> 2
% 71.73/72.20 3 ==> 3
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (27) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), alpha2( X, Y )
% 71.73/72.20 }.
% 71.73/72.20 parent0: (68402) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), alpha2( X, Y )
% 71.73/72.20 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (28) {G0,W9,D2,L3,V2,M3} I { Y = sz00, ! alpha2( X, Y ),
% 71.73/72.20 alpha1( X, Y ) }.
% 71.73/72.20 parent0: (68403) {G0,W9,D2,L3,V2,M3} { Y = sz00, ! alpha2( X, Y ), alpha1
% 71.73/72.20 ( X, Y ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 2 ==> 2
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (29) {G0,W7,D3,L2,V4,M2} I { ! alpha2( X, Y ), aInteger0(
% 71.73/72.20 skol1( Z, T ) ) }.
% 71.73/72.20 parent0: (68404) {G0,W7,D3,L2,V4,M2} { ! alpha2( X, Y ), aInteger0( skol1
% 71.73/72.20 ( Z, T ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 Z := Z
% 71.73/72.20 T := T
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (30) {G0,W10,D4,L2,V2,M2} I { ! alpha2( X, Y ), sdtasdt0( Y,
% 71.73/72.20 skol1( X, Y ) ) ==> X }.
% 71.73/72.20 parent0: (68405) {G0,W10,D4,L2,V2,M2} { ! alpha2( X, Y ), sdtasdt0( Y,
% 71.73/72.20 skol1( X, Y ) ) = X }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y
% 71.73/72.20 , Z ) = X, alpha2( X, Y ) }.
% 71.73/72.20 parent0: (68406) {G0,W10,D3,L3,V3,M3} { ! aInteger0( Z ), ! sdtasdt0( Y, Z
% 71.73/72.20 ) = X, alpha2( X, Y ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 Z := Z
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 2 ==> 2
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (33) {G0,W19,D4,L6,V3,M6} I { ! aInteger0( X ), ! aInteger0( Y
% 71.73/72.20 ), ! aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y
% 71.73/72.20 ) ) ), sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 71.73/72.20 parent0: (68408) {G0,W19,D4,L6,V3,M6} { ! aInteger0( X ), ! aInteger0( Y )
% 71.73/72.20 , ! aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y )
% 71.73/72.20 ) ), sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 Z := Z
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 2 ==> 2
% 71.73/72.20 3 ==> 3
% 71.73/72.20 4 ==> 4
% 71.73/72.20 5 ==> 5
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (35) {G0,W2,D2,L1,V0,M1} I { aInteger0( xa ) }.
% 71.73/72.20 parent0: (68410) {G0,W2,D2,L1,V0,M1} { aInteger0( xa ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (36) {G0,W2,D2,L1,V0,M1} I { aInteger0( xb ) }.
% 71.73/72.20 parent0: (68411) {G0,W2,D2,L1,V0,M1} { aInteger0( xb ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (37) {G0,W2,D2,L1,V0,M1} I { aInteger0( xq ) }.
% 71.73/72.20 parent0: (68412) {G0,W2,D2,L1,V0,M1} { aInteger0( xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (38) {G0,W3,D2,L1,V0,M1} I { ! xq ==> sz00 }.
% 71.73/72.20 parent0: (68413) {G0,W3,D2,L1,V0,M1} { ! xq = sz00 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (40) {G0,W2,D2,L1,V0,M1} I { aInteger0( xn ) }.
% 71.73/72.20 parent0: (68415) {G0,W2,D2,L1,V0,M1} { aInteger0( xn ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (42) {G0,W9,D4,L1,V0,M1} I { sdtasdt0( xq, smndt0( xn ) ) ==>
% 71.73/72.20 sdtpldt0( xb, smndt0( xa ) ) }.
% 71.73/72.20 parent0: (68417) {G0,W9,D4,L1,V0,M1} { sdtasdt0( xq, smndt0( xn ) ) =
% 71.73/72.20 sdtpldt0( xb, smndt0( xa ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (43) {G0,W4,D2,L1,V0,M1} I { ! sdteqdtlpzmzozddtrp0( xb, xa,
% 71.73/72.20 xq ) }.
% 71.73/72.20 parent0: (68418) {G0,W4,D2,L1,V0,M1} { ! sdteqdtlpzmzozddtrp0( xb, xa, xq
% 71.73/72.20 ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69676) {G1,W3,D3,L1,V0,M1} { aInteger0( smndt0( xa ) ) }.
% 71.73/72.20 parent0[0]: (3) {G0,W5,D3,L2,V1,M2} I { ! aInteger0( X ), aInteger0( smndt0
% 71.73/72.20 ( X ) ) }.
% 71.73/72.20 parent1[0]: (35) {G0,W2,D2,L1,V0,M1} I { aInteger0( xa ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := xa
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (79) {G1,W3,D3,L1,V0,M1} R(3,35) { aInteger0( smndt0( xa ) )
% 71.73/72.20 }.
% 71.73/72.20 parent0: (69676) {G1,W3,D3,L1,V0,M1} { aInteger0( smndt0( xa ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69677) {G1,W3,D3,L1,V0,M1} { aInteger0( smndt0( xn ) ) }.
% 71.73/72.20 parent0[0]: (3) {G0,W5,D3,L2,V1,M2} I { ! aInteger0( X ), aInteger0( smndt0
% 71.73/72.20 ( X ) ) }.
% 71.73/72.20 parent1[0]: (40) {G0,W2,D2,L1,V0,M1} I { aInteger0( xn ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := xn
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (82) {G1,W3,D3,L1,V0,M1} R(3,40) { aInteger0( smndt0( xn ) )
% 71.73/72.20 }.
% 71.73/72.20 parent0: (69677) {G1,W3,D3,L1,V0,M1} { aInteger0( smndt0( xn ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69678) {G1,W6,D3,L2,V1,M2} { ! aInteger0( X ), aInteger0(
% 71.73/72.20 sdtasdt0( xq, X ) ) }.
% 71.73/72.20 parent0[0]: (5) {G0,W8,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y )
% 71.73/72.20 , aInteger0( sdtasdt0( X, Y ) ) }.
% 71.73/72.20 parent1[0]: (37) {G0,W2,D2,L1,V0,M1} I { aInteger0( xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := xq
% 71.73/72.20 Y := X
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (147) {G1,W6,D3,L2,V1,M2} R(5,37) { ! aInteger0( X ),
% 71.73/72.20 aInteger0( sdtasdt0( xq, X ) ) }.
% 71.73/72.20 parent0: (69678) {G1,W6,D3,L2,V1,M2} { ! aInteger0( X ), aInteger0(
% 71.73/72.20 sdtasdt0( xq, X ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69680) {G1,W11,D4,L2,V1,M2} { ! aInteger0( X ), sdtpldt0(
% 71.73/72.20 smndt0( xa ), X ) = sdtpldt0( X, smndt0( xa ) ) }.
% 71.73/72.20 parent0[0]: (7) {G0,W11,D3,L3,V2,M3} I { ! aInteger0( X ), ! aInteger0( Y )
% 71.73/72.20 , sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 71.73/72.20 parent1[0]: (79) {G1,W3,D3,L1,V0,M1} R(3,35) { aInteger0( smndt0( xa ) )
% 71.73/72.20 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := smndt0( xa )
% 71.73/72.20 Y := X
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (275) {G2,W11,D4,L2,V1,M2} R(7,79) { ! aInteger0( X ),
% 71.73/72.20 sdtpldt0( smndt0( xa ), X ) = sdtpldt0( X, smndt0( xa ) ) }.
% 71.73/72.20 parent0: (69680) {G1,W11,D4,L2,V1,M2} { ! aInteger0( X ), sdtpldt0( smndt0
% 71.73/72.20 ( xa ), X ) = sdtpldt0( X, smndt0( xa ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69682) {G0,W7,D3,L2,V1,M2} { X ==> sdtasdt0( X, sz10 ), !
% 71.73/72.20 aInteger0( X ) }.
% 71.73/72.20 parent0[1]: (14) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X,
% 71.73/72.20 sz10 ) ==> X }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69683) {G1,W5,D3,L1,V0,M1} { xq ==> sdtasdt0( xq, sz10 ) }.
% 71.73/72.20 parent0[1]: (69682) {G0,W7,D3,L2,V1,M2} { X ==> sdtasdt0( X, sz10 ), !
% 71.73/72.20 aInteger0( X ) }.
% 71.73/72.20 parent1[0]: (37) {G0,W2,D2,L1,V0,M1} I { aInteger0( xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := xq
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69684) {G1,W5,D3,L1,V0,M1} { sdtasdt0( xq, sz10 ) ==> xq }.
% 71.73/72.20 parent0[0]: (69683) {G1,W5,D3,L1,V0,M1} { xq ==> sdtasdt0( xq, sz10 ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (693) {G1,W5,D3,L1,V0,M1} R(14,37) { sdtasdt0( xq, sz10 ) ==>
% 71.73/72.20 xq }.
% 71.73/72.20 parent0: (69684) {G1,W5,D3,L1,V0,M1} { sdtasdt0( xq, sz10 ) ==> xq }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69685) {G0,W7,D3,L2,V1,M2} { sz00 ==> sdtasdt0( X, sz00 ), !
% 71.73/72.20 aInteger0( X ) }.
% 71.73/72.20 parent0[1]: (18) {G0,W7,D3,L2,V1,M2} I { ! aInteger0( X ), sdtasdt0( X,
% 71.73/72.20 sz00 ) ==> sz00 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69686) {G1,W5,D3,L1,V0,M1} { sz00 ==> sdtasdt0( xn, sz00 )
% 71.73/72.20 }.
% 71.73/72.20 parent0[1]: (69685) {G0,W7,D3,L2,V1,M2} { sz00 ==> sdtasdt0( X, sz00 ), !
% 71.73/72.20 aInteger0( X ) }.
% 71.73/72.20 parent1[0]: (40) {G0,W2,D2,L1,V0,M1} I { aInteger0( xn ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := xn
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69687) {G1,W5,D3,L1,V0,M1} { sdtasdt0( xn, sz00 ) ==> sz00 }.
% 71.73/72.20 parent0[0]: (69686) {G1,W5,D3,L1,V0,M1} { sz00 ==> sdtasdt0( xn, sz00 )
% 71.73/72.20 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (915) {G1,W5,D3,L1,V0,M1} R(18,40) { sdtasdt0( xn, sz00 ) ==>
% 71.73/72.20 sz00 }.
% 71.73/72.20 parent0: (69687) {G1,W5,D3,L1,V0,M1} { sdtasdt0( xn, sz00 ) ==> sz00 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69689) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> xq }.
% 71.73/72.20 parent0[0]: (38) {G0,W3,D2,L1,V0,M1} I { ! xq ==> sz00 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 paramod: (69693) {G1,W9,D2,L3,V1,M3} { ! sz00 ==> sz00, ! alpha2( X, xq )
% 71.73/72.20 , alpha1( X, xq ) }.
% 71.73/72.20 parent0[0]: (28) {G0,W9,D2,L3,V2,M3} I { Y = sz00, ! alpha2( X, Y ), alpha1
% 71.73/72.20 ( X, Y ) }.
% 71.73/72.20 parent1[0; 3]: (69689) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> xq }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := xq
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqrefl: (69725) {G0,W6,D2,L2,V1,M2} { ! alpha2( X, xq ), alpha1( X, xq )
% 71.73/72.20 }.
% 71.73/72.20 parent0[0]: (69693) {G1,W9,D2,L3,V1,M3} { ! sz00 ==> sz00, ! alpha2( X, xq
% 71.73/72.20 ), alpha1( X, xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (1816) {G1,W6,D2,L2,V1,M2} P(28,38);q { ! alpha2( X, xq ),
% 71.73/72.20 alpha1( X, xq ) }.
% 71.73/72.20 parent0: (69725) {G0,W6,D2,L2,V1,M2} { ! alpha2( X, xq ), alpha1( X, xq )
% 71.73/72.20 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69726) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), ! aInteger0
% 71.73/72.20 ( Y ), alpha2( Z, X ) }.
% 71.73/72.20 parent0[1]: (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y,
% 71.73/72.20 Z ) = X, alpha2( X, Y ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := Z
% 71.73/72.20 Y := X
% 71.73/72.20 Z := Y
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69727) {G1,W9,D4,L2,V2,M2} { ! X = sdtasdt0( Y, smndt0( xn )
% 71.73/72.20 ), alpha2( X, Y ) }.
% 71.73/72.20 parent0[1]: (69726) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 71.73/72.20 aInteger0( Y ), alpha2( Z, X ) }.
% 71.73/72.20 parent1[0]: (82) {G1,W3,D3,L1,V0,M1} R(3,40) { aInteger0( smndt0( xn ) )
% 71.73/72.20 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := Y
% 71.73/72.20 Y := smndt0( xn )
% 71.73/72.20 Z := X
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69728) {G1,W9,D4,L2,V2,M2} { ! sdtasdt0( Y, smndt0( xn ) ) = X,
% 71.73/72.20 alpha2( X, Y ) }.
% 71.73/72.20 parent0[0]: (69727) {G1,W9,D4,L2,V2,M2} { ! X = sdtasdt0( Y, smndt0( xn )
% 71.73/72.20 ), alpha2( X, Y ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (2004) {G2,W9,D4,L2,V2,M2} R(31,82) { ! sdtasdt0( X, smndt0(
% 71.73/72.20 xn ) ) = Y, alpha2( Y, X ) }.
% 71.73/72.20 parent0: (69728) {G1,W9,D4,L2,V2,M2} { ! sdtasdt0( Y, smndt0( xn ) ) = X,
% 71.73/72.20 alpha2( X, Y ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := Y
% 71.73/72.20 Y := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69730) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), ! aInteger0
% 71.73/72.20 ( Y ), alpha2( Z, X ) }.
% 71.73/72.20 parent0[1]: (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y,
% 71.73/72.20 Z ) = X, alpha2( X, Y ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := Z
% 71.73/72.20 Y := X
% 71.73/72.20 Z := Y
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 paramod: (69731) {G1,W8,D2,L3,V1,M3} { ! X = sz00, ! aInteger0( sz00 ),
% 71.73/72.20 alpha2( X, xn ) }.
% 71.73/72.20 parent0[0]: (915) {G1,W5,D3,L1,V0,M1} R(18,40) { sdtasdt0( xn, sz00 ) ==>
% 71.73/72.20 sz00 }.
% 71.73/72.20 parent1[0; 3]: (69730) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 71.73/72.20 aInteger0( Y ), alpha2( Z, X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := xn
% 71.73/72.20 Y := sz00
% 71.73/72.20 Z := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69732) {G1,W6,D2,L2,V1,M2} { ! X = sz00, alpha2( X, xn ) }.
% 71.73/72.20 parent0[1]: (69731) {G1,W8,D2,L3,V1,M3} { ! X = sz00, ! aInteger0( sz00 )
% 71.73/72.20 , alpha2( X, xn ) }.
% 71.73/72.20 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz00 ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69733) {G1,W6,D2,L2,V1,M2} { ! sz00 = X, alpha2( X, xn ) }.
% 71.73/72.20 parent0[0]: (69732) {G1,W6,D2,L2,V1,M2} { ! X = sz00, alpha2( X, xn ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (2021) {G2,W6,D2,L2,V1,M2} P(915,31);r(1) { ! sz00 = X, alpha2
% 71.73/72.20 ( X, xn ) }.
% 71.73/72.20 parent0: (69733) {G1,W6,D2,L2,V1,M2} { ! sz00 = X, alpha2( X, xn ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69735) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), ! aInteger0
% 71.73/72.20 ( Y ), alpha2( Z, X ) }.
% 71.73/72.20 parent0[1]: (31) {G0,W10,D3,L3,V3,M3} I { ! aInteger0( Z ), ! sdtasdt0( Y,
% 71.73/72.20 Z ) = X, alpha2( X, Y ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := Z
% 71.73/72.20 Y := X
% 71.73/72.20 Z := Y
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 paramod: (69736) {G1,W8,D2,L3,V1,M3} { ! X = xq, ! aInteger0( sz10 ),
% 71.73/72.20 alpha2( X, xq ) }.
% 71.73/72.20 parent0[0]: (693) {G1,W5,D3,L1,V0,M1} R(14,37) { sdtasdt0( xq, sz10 ) ==>
% 71.73/72.20 xq }.
% 71.73/72.20 parent1[0; 3]: (69735) {G0,W10,D3,L3,V3,M3} { ! Z = sdtasdt0( X, Y ), !
% 71.73/72.20 aInteger0( Y ), alpha2( Z, X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := xq
% 71.73/72.20 Y := sz10
% 71.73/72.20 Z := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69737) {G1,W6,D2,L2,V1,M2} { ! X = xq, alpha2( X, xq ) }.
% 71.73/72.20 parent0[1]: (69736) {G1,W8,D2,L3,V1,M3} { ! X = xq, ! aInteger0( sz10 ),
% 71.73/72.20 alpha2( X, xq ) }.
% 71.73/72.20 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aInteger0( sz10 ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69738) {G1,W6,D2,L2,V1,M2} { ! xq = X, alpha2( X, xq ) }.
% 71.73/72.20 parent0[0]: (69737) {G1,W6,D2,L2,V1,M2} { ! X = xq, alpha2( X, xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (2029) {G2,W6,D2,L2,V1,M2} P(693,31);r(2) { ! xq = X, alpha2(
% 71.73/72.20 X, xq ) }.
% 71.73/72.20 parent0: (69738) {G1,W6,D2,L2,V1,M2} { ! xq = X, alpha2( X, xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69739) {G2,W6,D2,L2,V1,M2} { ! X = sz00, alpha2( X, xn ) }.
% 71.73/72.20 parent0[0]: (2021) {G2,W6,D2,L2,V1,M2} P(915,31);r(1) { ! sz00 = X, alpha2
% 71.73/72.20 ( X, xn ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqrefl: (69740) {G0,W3,D2,L1,V0,M1} { alpha2( sz00, xn ) }.
% 71.73/72.20 parent0[0]: (69739) {G2,W6,D2,L2,V1,M2} { ! X = sz00, alpha2( X, xn ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := sz00
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (2069) {G3,W3,D2,L1,V0,M1} Q(2021) { alpha2( sz00, xn ) }.
% 71.73/72.20 parent0: (69740) {G0,W3,D2,L1,V0,M1} { alpha2( sz00, xn ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69741) {G2,W9,D4,L2,V2,M2} { ! Y = sdtasdt0( X, smndt0( xn ) ),
% 71.73/72.20 alpha2( Y, X ) }.
% 71.73/72.20 parent0[0]: (2004) {G2,W9,D4,L2,V2,M2} R(31,82) { ! sdtasdt0( X, smndt0( xn
% 71.73/72.20 ) ) = Y, alpha2( Y, X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqrefl: (69742) {G0,W6,D4,L1,V1,M1} { alpha2( sdtasdt0( X, smndt0( xn ) )
% 71.73/72.20 , X ) }.
% 71.73/72.20 parent0[0]: (69741) {G2,W9,D4,L2,V2,M2} { ! Y = sdtasdt0( X, smndt0( xn )
% 71.73/72.20 ), alpha2( Y, X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := sdtasdt0( X, smndt0( xn ) )
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (2084) {G3,W6,D4,L1,V1,M1} Q(2004) { alpha2( sdtasdt0( X,
% 71.73/72.20 smndt0( xn ) ), X ) }.
% 71.73/72.20 parent0: (69742) {G0,W6,D4,L1,V1,M1} { alpha2( sdtasdt0( X, smndt0( xn ) )
% 71.73/72.20 , X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69743) {G1,W4,D3,L1,V2,M1} { aInteger0( skol1( X, Y ) ) }.
% 71.73/72.20 parent0[0]: (29) {G0,W7,D3,L2,V4,M2} I { ! alpha2( X, Y ), aInteger0( skol1
% 71.73/72.20 ( Z, T ) ) }.
% 71.73/72.20 parent1[0]: (2069) {G3,W3,D2,L1,V0,M1} Q(2021) { alpha2( sz00, xn ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := sz00
% 71.73/72.20 Y := xn
% 71.73/72.20 Z := X
% 71.73/72.20 T := Y
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (2133) {G4,W4,D3,L1,V2,M1} R(2069,29) { aInteger0( skol1( X, Y
% 71.73/72.20 ) ) }.
% 71.73/72.20 parent0: (69743) {G1,W4,D3,L1,V2,M1} { aInteger0( skol1( X, Y ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69744) {G0,W19,D4,L6,V3,M6} { sz00 = X, ! aInteger0( Y ), !
% 71.73/72.20 aInteger0( Z ), ! aInteger0( X ), ! aDivisorOf0( X, sdtpldt0( Y, smndt0(
% 71.73/72.20 Z ) ) ), sdteqdtlpzmzozddtrp0( Y, Z, X ) }.
% 71.73/72.20 parent0[3]: (33) {G0,W19,D4,L6,V3,M6} I { ! aInteger0( X ), ! aInteger0( Y
% 71.73/72.20 ), ! aInteger0( Z ), Z = sz00, ! aDivisorOf0( Z, sdtpldt0( X, smndt0( Y
% 71.73/72.20 ) ) ), sdteqdtlpzmzozddtrp0( X, Y, Z ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := Y
% 71.73/72.20 Y := Z
% 71.73/72.20 Z := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69745) {G1,W15,D4,L5,V0,M5} { sz00 = xq, ! aInteger0( xb ), !
% 71.73/72.20 aInteger0( xa ), ! aInteger0( xq ), ! aDivisorOf0( xq, sdtpldt0( xb,
% 71.73/72.20 smndt0( xa ) ) ) }.
% 71.73/72.20 parent0[0]: (43) {G0,W4,D2,L1,V0,M1} I { ! sdteqdtlpzmzozddtrp0( xb, xa, xq
% 71.73/72.20 ) }.
% 71.73/72.20 parent1[5]: (69744) {G0,W19,D4,L6,V3,M6} { sz00 = X, ! aInteger0( Y ), !
% 71.73/72.20 aInteger0( Z ), ! aInteger0( X ), ! aDivisorOf0( X, sdtpldt0( Y, smndt0(
% 71.73/72.20 Z ) ) ), sdteqdtlpzmzozddtrp0( Y, Z, X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := xq
% 71.73/72.20 Y := xb
% 71.73/72.20 Z := xa
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69746) {G1,W13,D4,L4,V0,M4} { sz00 = xq, ! aInteger0( xa ), !
% 71.73/72.20 aInteger0( xq ), ! aDivisorOf0( xq, sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 parent0[1]: (69745) {G1,W15,D4,L5,V0,M5} { sz00 = xq, ! aInteger0( xb ), !
% 71.73/72.20 aInteger0( xa ), ! aInteger0( xq ), ! aDivisorOf0( xq, sdtpldt0( xb,
% 71.73/72.20 smndt0( xa ) ) ) }.
% 71.73/72.20 parent1[0]: (36) {G0,W2,D2,L1,V0,M1} I { aInteger0( xb ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69747) {G1,W13,D4,L4,V0,M4} { xq = sz00, ! aInteger0( xa ), !
% 71.73/72.20 aInteger0( xq ), ! aDivisorOf0( xq, sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 parent0[0]: (69746) {G1,W13,D4,L4,V0,M4} { sz00 = xq, ! aInteger0( xa ), !
% 71.73/72.20 aInteger0( xq ), ! aDivisorOf0( xq, sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (2254) {G1,W13,D4,L4,V0,M4} R(33,43);r(36) { ! aInteger0( xa )
% 71.73/72.20 , ! aInteger0( xq ), xq ==> sz00, ! aDivisorOf0( xq, sdtpldt0( xb, smndt0
% 71.73/72.20 ( xa ) ) ) }.
% 71.73/72.20 parent0: (69747) {G1,W13,D4,L4,V0,M4} { xq = sz00, ! aInteger0( xa ), !
% 71.73/72.20 aInteger0( xq ), ! aDivisorOf0( xq, sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 2
% 71.73/72.20 1 ==> 0
% 71.73/72.20 2 ==> 1
% 71.73/72.20 3 ==> 3
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69750) {G1,W11,D4,L3,V0,M3} { ! aInteger0( xq ), xq ==> sz00
% 71.73/72.20 , ! aDivisorOf0( xq, sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 parent0[0]: (2254) {G1,W13,D4,L4,V0,M4} R(33,43);r(36) { ! aInteger0( xa )
% 71.73/72.20 , ! aInteger0( xq ), xq ==> sz00, ! aDivisorOf0( xq, sdtpldt0( xb, smndt0
% 71.73/72.20 ( xa ) ) ) }.
% 71.73/72.20 parent1[0]: (35) {G0,W2,D2,L1,V0,M1} I { aInteger0( xa ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69751) {G1,W9,D4,L2,V0,M2} { xq ==> sz00, ! aDivisorOf0( xq,
% 71.73/72.20 sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 parent0[0]: (69750) {G1,W11,D4,L3,V0,M3} { ! aInteger0( xq ), xq ==> sz00
% 71.73/72.20 , ! aDivisorOf0( xq, sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 parent1[0]: (37) {G0,W2,D2,L1,V0,M1} I { aInteger0( xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69752) {G1,W6,D4,L1,V0,M1} { ! aDivisorOf0( xq, sdtpldt0( xb
% 71.73/72.20 , smndt0( xa ) ) ) }.
% 71.73/72.20 parent0[0]: (38) {G0,W3,D2,L1,V0,M1} I { ! xq ==> sz00 }.
% 71.73/72.20 parent1[0]: (69751) {G1,W9,D4,L2,V0,M2} { xq ==> sz00, ! aDivisorOf0( xq,
% 71.73/72.20 sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (20439) {G2,W6,D4,L1,V0,M1} S(2254);r(35);r(37);r(38) { !
% 71.73/72.20 aDivisorOf0( xq, sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 parent0: (69752) {G1,W6,D4,L1,V0,M1} { ! aDivisorOf0( xq, sdtpldt0( xb,
% 71.73/72.20 smndt0( xa ) ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 paramod: (69754) {G1,W9,D3,L3,V1,M3} { aInteger0( X ), ! alpha2( X, xq ),
% 71.73/72.20 ! aInteger0( skol1( X, xq ) ) }.
% 71.73/72.20 parent0[1]: (30) {G0,W10,D4,L2,V2,M2} I { ! alpha2( X, Y ), sdtasdt0( Y,
% 71.73/72.20 skol1( X, Y ) ) ==> X }.
% 71.73/72.20 parent1[1; 1]: (147) {G1,W6,D3,L2,V1,M2} R(5,37) { ! aInteger0( X ),
% 71.73/72.20 aInteger0( sdtasdt0( xq, X ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := xq
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := skol1( X, xq )
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69755) {G2,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha2( X, xq
% 71.73/72.20 ) }.
% 71.73/72.20 parent0[2]: (69754) {G1,W9,D3,L3,V1,M3} { aInteger0( X ), ! alpha2( X, xq
% 71.73/72.20 ), ! aInteger0( skol1( X, xq ) ) }.
% 71.73/72.20 parent1[0]: (2133) {G4,W4,D3,L1,V2,M1} R(2069,29) { aInteger0( skol1( X, Y
% 71.73/72.20 ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := X
% 71.73/72.20 Y := xq
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (29150) {G5,W5,D2,L2,V1,M2} P(30,147);r(2133) { aInteger0( X )
% 71.73/72.20 , ! alpha2( X, xq ) }.
% 71.73/72.20 parent0: (69755) {G2,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha2( X, xq )
% 71.73/72.20 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69756) {G2,W6,D2,L2,V1,M2} { ! X = xq, alpha2( X, xq ) }.
% 71.73/72.20 parent0[0]: (2029) {G2,W6,D2,L2,V1,M2} P(693,31);r(2) { ! xq = X, alpha2( X
% 71.73/72.20 , xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69757) {G3,W5,D2,L2,V1,M2} { aInteger0( X ), ! X = xq }.
% 71.73/72.20 parent0[1]: (29150) {G5,W5,D2,L2,V1,M2} P(30,147);r(2133) { aInteger0( X )
% 71.73/72.20 , ! alpha2( X, xq ) }.
% 71.73/72.20 parent1[1]: (69756) {G2,W6,D2,L2,V1,M2} { ! X = xq, alpha2( X, xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69758) {G3,W5,D2,L2,V1,M2} { ! xq = X, aInteger0( X ) }.
% 71.73/72.20 parent0[1]: (69757) {G3,W5,D2,L2,V1,M2} { aInteger0( X ), ! X = xq }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (29304) {G6,W5,D2,L2,V1,M2} R(29150,2029) { aInteger0( X ), !
% 71.73/72.20 xq = X }.
% 71.73/72.20 parent0: (69758) {G3,W5,D2,L2,V1,M2} { ! xq = X, aInteger0( X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 1
% 71.73/72.20 1 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69759) {G1,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha1( X, xq
% 71.73/72.20 ) }.
% 71.73/72.20 parent0[1]: (29150) {G5,W5,D2,L2,V1,M2} P(30,147);r(2133) { aInteger0( X )
% 71.73/72.20 , ! alpha2( X, xq ) }.
% 71.73/72.20 parent1[1]: (27) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), alpha2( X, Y )
% 71.73/72.20 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := X
% 71.73/72.20 Y := xq
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (29348) {G6,W5,D2,L2,V1,M2} R(29150,27) { aInteger0( X ), !
% 71.73/72.20 alpha1( X, xq ) }.
% 71.73/72.20 parent0: (69759) {G1,W5,D2,L2,V1,M2} { aInteger0( X ), ! alpha1( X, xq )
% 71.73/72.20 }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69760) {G6,W5,D2,L2,V1,M2} { ! X = xq, aInteger0( X ) }.
% 71.73/72.20 parent0[1]: (29304) {G6,W5,D2,L2,V1,M2} R(29150,2029) { aInteger0( X ), !
% 71.73/72.20 xq = X }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69762) {G1,W11,D2,L4,V2,M4} { ! aInteger0( X ), ! alpha1( X,
% 71.73/72.20 Y ), aDivisorOf0( Y, X ), ! Y = xq }.
% 71.73/72.20 parent0[1]: (25) {G0,W10,D2,L4,V2,M4} I { ! aInteger0( X ), ! aInteger0( Y
% 71.73/72.20 ), ! alpha1( X, Y ), aDivisorOf0( Y, X ) }.
% 71.73/72.20 parent1[1]: (69760) {G6,W5,D2,L2,V1,M2} { ! X = xq, aInteger0( X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := Y
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69763) {G1,W11,D2,L4,V2,M4} { ! xq = X, ! aInteger0( Y ), !
% 71.73/72.20 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 71.73/72.20 parent0[3]: (69762) {G1,W11,D2,L4,V2,M4} { ! aInteger0( X ), ! alpha1( X,
% 71.73/72.20 Y ), aDivisorOf0( Y, X ), ! Y = xq }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := Y
% 71.73/72.20 Y := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (29458) {G7,W11,D2,L4,V2,M4} R(29304,25) { ! xq = X, !
% 71.73/72.20 aInteger0( Y ), ! alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 71.73/72.20 parent0: (69763) {G1,W11,D2,L4,V2,M4} { ! xq = X, ! aInteger0( Y ), !
% 71.73/72.20 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 2 ==> 2
% 71.73/72.20 3 ==> 3
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69765) {G7,W11,D2,L4,V2,M4} { ! X = xq, ! aInteger0( Y ), !
% 71.73/72.20 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 71.73/72.20 parent0[0]: (29458) {G7,W11,D2,L4,V2,M4} R(29304,25) { ! xq = X, !
% 71.73/72.20 aInteger0( Y ), ! alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 Y := Y
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqrefl: (69766) {G0,W8,D2,L3,V1,M3} { ! aInteger0( X ), ! alpha1( X, xq )
% 71.73/72.20 , aDivisorOf0( xq, X ) }.
% 71.73/72.20 parent0[0]: (69765) {G7,W11,D2,L4,V2,M4} { ! X = xq, ! aInteger0( Y ), !
% 71.73/72.20 alpha1( Y, X ), aDivisorOf0( X, Y ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := xq
% 71.73/72.20 Y := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69767) {G1,W9,D2,L3,V1,M3} { ! alpha1( X, xq ), aDivisorOf0(
% 71.73/72.20 xq, X ), ! alpha1( X, xq ) }.
% 71.73/72.20 parent0[0]: (69766) {G0,W8,D2,L3,V1,M3} { ! aInteger0( X ), ! alpha1( X,
% 71.73/72.20 xq ), aDivisorOf0( xq, X ) }.
% 71.73/72.20 parent1[0]: (29348) {G6,W5,D2,L2,V1,M2} R(29150,27) { aInteger0( X ), !
% 71.73/72.20 alpha1( X, xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 factor: (69768) {G1,W6,D2,L2,V1,M2} { ! alpha1( X, xq ), aDivisorOf0( xq,
% 71.73/72.20 X ) }.
% 71.73/72.20 parent0[0, 2]: (69767) {G1,W9,D2,L3,V1,M3} { ! alpha1( X, xq ),
% 71.73/72.20 aDivisorOf0( xq, X ), ! alpha1( X, xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (29481) {G8,W6,D2,L2,V1,M2} Q(29458);r(29348) { ! alpha1( X,
% 71.73/72.20 xq ), aDivisorOf0( xq, X ) }.
% 71.73/72.20 parent0: (69768) {G1,W6,D2,L2,V1,M2} { ! alpha1( X, xq ), aDivisorOf0( xq
% 71.73/72.20 , X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 1 ==> 1
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69769) {G2,W6,D2,L2,V1,M2} { aDivisorOf0( xq, X ), ! alpha2(
% 71.73/72.20 X, xq ) }.
% 71.73/72.20 parent0[0]: (29481) {G8,W6,D2,L2,V1,M2} Q(29458);r(29348) { ! alpha1( X, xq
% 71.73/72.20 ), aDivisorOf0( xq, X ) }.
% 71.73/72.20 parent1[1]: (1816) {G1,W6,D2,L2,V1,M2} P(28,38);q { ! alpha2( X, xq ),
% 71.73/72.20 alpha1( X, xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (48234) {G9,W6,D2,L2,V1,M2} R(1816,29481) { ! alpha2( X, xq )
% 71.73/72.20 , aDivisorOf0( xq, X ) }.
% 71.73/72.20 parent0: (69769) {G2,W6,D2,L2,V1,M2} { aDivisorOf0( xq, X ), ! alpha2( X,
% 71.73/72.20 xq ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 1
% 71.73/72.20 1 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 eqswap: (69770) {G2,W11,D4,L2,V1,M2} { sdtpldt0( X, smndt0( xa ) ) =
% 71.73/72.20 sdtpldt0( smndt0( xa ), X ), ! aInteger0( X ) }.
% 71.73/72.20 parent0[1]: (275) {G2,W11,D4,L2,V1,M2} R(7,79) { ! aInteger0( X ), sdtpldt0
% 71.73/72.20 ( smndt0( xa ), X ) = sdtpldt0( X, smndt0( xa ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := X
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69771) {G1,W9,D4,L1,V0,M1} { sdtpldt0( xb, smndt0( xa ) ) =
% 71.73/72.20 sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 parent0[1]: (69770) {G2,W11,D4,L2,V1,M2} { sdtpldt0( X, smndt0( xa ) ) =
% 71.73/72.20 sdtpldt0( smndt0( xa ), X ), ! aInteger0( X ) }.
% 71.73/72.20 parent1[0]: (36) {G0,W2,D2,L1,V0,M1} I { aInteger0( xb ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := xb
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (52543) {G3,W9,D4,L1,V0,M1} R(275,36) { sdtpldt0( xb, smndt0(
% 71.73/72.20 xa ) ) ==> sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 parent0: (69771) {G1,W9,D4,L1,V0,M1} { sdtpldt0( xb, smndt0( xa ) ) =
% 71.73/72.20 sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 paramod: (69775) {G1,W9,D4,L1,V0,M1} { sdtasdt0( xq, smndt0( xn ) ) ==>
% 71.73/72.20 sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 parent0[0]: (52543) {G3,W9,D4,L1,V0,M1} R(275,36) { sdtpldt0( xb, smndt0(
% 71.73/72.20 xa ) ) ==> sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 parent1[0; 5]: (42) {G0,W9,D4,L1,V0,M1} I { sdtasdt0( xq, smndt0( xn ) )
% 71.73/72.20 ==> sdtpldt0( xb, smndt0( xa ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (52749) {G4,W9,D4,L1,V0,M1} S(42);d(52543) { sdtasdt0( xq,
% 71.73/72.20 smndt0( xn ) ) ==> sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 parent0: (69775) {G1,W9,D4,L1,V0,M1} { sdtasdt0( xq, smndt0( xn ) ) ==>
% 71.73/72.20 sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 paramod: (69778) {G3,W6,D4,L1,V0,M1} { ! aDivisorOf0( xq, sdtpldt0( smndt0
% 71.73/72.20 ( xa ), xb ) ) }.
% 71.73/72.20 parent0[0]: (52543) {G3,W9,D4,L1,V0,M1} R(275,36) { sdtpldt0( xb, smndt0(
% 71.73/72.20 xa ) ) ==> sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 parent1[0; 3]: (20439) {G2,W6,D4,L1,V0,M1} S(2254);r(35);r(37);r(38) { !
% 71.73/72.20 aDivisorOf0( xq, sdtpldt0( xb, smndt0( xa ) ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (61141) {G4,W6,D4,L1,V0,M1} S(20439);d(52543) { ! aDivisorOf0
% 71.73/72.20 ( xq, sdtpldt0( smndt0( xa ), xb ) ) }.
% 71.73/72.20 parent0: (69778) {G3,W6,D4,L1,V0,M1} { ! aDivisorOf0( xq, sdtpldt0( smndt0
% 71.73/72.20 ( xa ), xb ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 0 ==> 0
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69780) {G4,W6,D4,L1,V0,M1} { aDivisorOf0( xq, sdtasdt0( xq,
% 71.73/72.20 smndt0( xn ) ) ) }.
% 71.73/72.20 parent0[0]: (48234) {G9,W6,D2,L2,V1,M2} R(1816,29481) { ! alpha2( X, xq ),
% 71.73/72.20 aDivisorOf0( xq, X ) }.
% 71.73/72.20 parent1[0]: (2084) {G3,W6,D4,L1,V1,M1} Q(2004) { alpha2( sdtasdt0( X,
% 71.73/72.20 smndt0( xn ) ), X ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 X := sdtasdt0( xq, smndt0( xn ) )
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 X := xq
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 paramod: (69781) {G5,W6,D4,L1,V0,M1} { aDivisorOf0( xq, sdtpldt0( smndt0(
% 71.73/72.20 xa ), xb ) ) }.
% 71.73/72.20 parent0[0]: (52749) {G4,W9,D4,L1,V0,M1} S(42);d(52543) { sdtasdt0( xq,
% 71.73/72.20 smndt0( xn ) ) ==> sdtpldt0( smndt0( xa ), xb ) }.
% 71.73/72.20 parent1[0; 2]: (69780) {G4,W6,D4,L1,V0,M1} { aDivisorOf0( xq, sdtasdt0( xq
% 71.73/72.20 , smndt0( xn ) ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 resolution: (69782) {G5,W0,D0,L0,V0,M0} { }.
% 71.73/72.20 parent0[0]: (61141) {G4,W6,D4,L1,V0,M1} S(20439);d(52543) { ! aDivisorOf0(
% 71.73/72.20 xq, sdtpldt0( smndt0( xa ), xb ) ) }.
% 71.73/72.20 parent1[0]: (69781) {G5,W6,D4,L1,V0,M1} { aDivisorOf0( xq, sdtpldt0(
% 71.73/72.20 smndt0( xa ), xb ) ) }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 substitution1:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 subsumption: (68373) {G10,W0,D0,L0,V0,M0} R(2084,48234);d(52749);r(61141)
% 71.73/72.20 { }.
% 71.73/72.20 parent0: (69782) {G5,W0,D0,L0,V0,M0} { }.
% 71.73/72.20 substitution0:
% 71.73/72.20 end
% 71.73/72.20 permutation0:
% 71.73/72.20 end
% 71.73/72.20
% 71.73/72.20 Proof check complete!
% 71.73/72.20
% 71.73/72.20 Memory use:
% 71.73/72.20
% 71.73/72.20 space for terms: 814620
% 71.73/72.20 space for clauses: 3748788
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 clauses generated: 242589
% 71.73/72.20 clauses kept: 68374
% 71.73/72.20 clauses selected: 1215
% 71.73/72.20 clauses deleted: 10871
% 71.73/72.20 clauses inuse deleted: 117
% 71.73/72.20
% 71.73/72.20 subsentry: 1011860
% 71.73/72.20 literals s-matched: 362507
% 71.73/72.20 literals matched: 341498
% 71.73/72.20 full subsumption: 141745
% 71.73/72.20
% 71.73/72.20 checksum: -1181474632
% 71.73/72.20
% 71.73/72.20
% 71.73/72.20 Bliksem ended
%------------------------------------------------------------------------------