%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : PUZ036-1.005 : TPTP v8.1.0. Released v2.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 17:58:17 EDT 2022
% Result : Unsatisfiable 17.29s 17.69s
% Output : Refutation 17.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PUZ036-1.005 : TPTP v8.1.0. Released v2.0.0.
% 0.07/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n021.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 : Sat May 28 21:21:57 EDT 2022
% 0.13/0.34 % CPUTime :
% 17.29/17.69 *** allocated 10000 integers for termspace/termends
% 17.29/17.69 *** allocated 10000 integers for clauses
% 17.29/17.69 *** allocated 10000 integers for justifications
% 17.29/17.69 Bliksem 1.12
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Automatic Strategy Selection
% 17.29/17.69
% 17.29/17.69 Clauses:
% 17.29/17.69 [
% 17.29/17.69 [ ~( state( 'p_1', 'p_2', 'p_3', 'p_4', 'p_5', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20' ) ) ],
% 17.29/17.69 [ state( 'p_5', 'p_4', 'p_3', 'p_2', 'p_1', 'p_6', 'p_7', 'p_8', 'p_9',
% 17.29/17.69 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17', 'p_18',
% 17.29/17.69 'p_19', 'p_20' ) ],
% 17.29/17.69 [ ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8, V9,
% 17.29/17.69 V10, V11, V12, V13 ) ), state( Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6
% 17.29/17.69 , V7, V8, V9, V10, V11, V12, V13, X ) ],
% 17.29/17.69 [ ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8, V9,
% 17.29/17.69 V10, V11, V12, V13 ) ), state( V13, X, Y, Z, T, U, W, V0, V1, V2, V3, V4
% 17.29/17.69 , V5, V6, V7, V8, V9, V10, V11, V12 ) ],
% 17.29/17.69 [ ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8, V9,
% 17.29/17.69 V10, V11, V12, V13 ) ), state( T, Z, Y, X, U, W, V0, V1, V2, V3, V4, V5,
% 17.29/17.69 V6, V7, V8, V9, V10, V11, V12, V13 ) ]
% 17.29/17.69 ] .
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 percentage equality = 0.000000, percentage horn = 1.000000
% 17.29/17.69 This is a near-Horn, non-equality problem
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Options Used:
% 17.29/17.69
% 17.29/17.69 useres = 1
% 17.29/17.69 useparamod = 0
% 17.29/17.69 useeqrefl = 0
% 17.29/17.69 useeqfact = 0
% 17.29/17.69 usefactor = 1
% 17.29/17.69 usesimpsplitting = 0
% 17.29/17.69 usesimpdemod = 0
% 17.29/17.69 usesimpres = 4
% 17.29/17.69
% 17.29/17.69 resimpinuse = 1000
% 17.29/17.69 resimpclauses = 20000
% 17.29/17.69 substype = standard
% 17.29/17.69 backwardsubs = 1
% 17.29/17.69 selectoldest = 5
% 17.29/17.69
% 17.29/17.69 litorderings [0] = split
% 17.29/17.69 litorderings [1] = liftord
% 17.29/17.69
% 17.29/17.69 termordering = none
% 17.29/17.69
% 17.29/17.69 litapriori = 1
% 17.29/17.69 termapriori = 0
% 17.29/17.69 litaposteriori = 0
% 17.29/17.69 termaposteriori = 0
% 17.29/17.69 demodaposteriori = 0
% 17.29/17.69 ordereqreflfact = 0
% 17.29/17.69
% 17.29/17.69 litselect = negative
% 17.29/17.69
% 17.29/17.69 maxweight = 30000
% 17.29/17.69 maxdepth = 30000
% 17.29/17.69 maxlength = 115
% 17.29/17.69 maxnrvars = 195
% 17.29/17.69 excuselevel = 0
% 17.29/17.69 increasemaxweight = 0
% 17.29/17.69
% 17.29/17.69 maxselected = 10000000
% 17.29/17.69 maxnrclauses = 10000000
% 17.29/17.69
% 17.29/17.69 showgenerated = 0
% 17.29/17.69 showkept = 0
% 17.29/17.69 showselected = 0
% 17.29/17.69 showdeleted = 0
% 17.29/17.69 showresimp = 1
% 17.29/17.69 showstatus = 2000
% 17.29/17.69
% 17.29/17.69 prologoutput = 1
% 17.29/17.69 nrgoals = 5000000
% 17.29/17.69 totalproof = 1
% 17.29/17.69
% 17.29/17.69 Symbols occurring in the translation:
% 17.29/17.69
% 17.29/17.69 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 17.29/17.69 . [1, 2] (w:1, o:54, a:1, s:1, b:0),
% 17.29/17.69 ! [4, 1] (w:1, o:49, a:1, s:1, b:0),
% 17.29/17.69 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 17.29/17.69 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 17.29/17.69 'p_1' [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 17.29/17.69 'p_2' [40, 0] (w:1, o:20, a:1, s:1, b:0),
% 17.29/17.69 'p_3' [41, 0] (w:1, o:22, a:1, s:1, b:0),
% 17.29/17.69 'p_4' [42, 0] (w:1, o:23, a:1, s:1, b:0),
% 17.29/17.69 'p_5' [43, 0] (w:1, o:24, a:1, s:1, b:0),
% 17.29/17.69 'p_6' [44, 0] (w:1, o:25, a:1, s:1, b:0),
% 17.29/17.69 'p_7' [45, 0] (w:1, o:26, a:1, s:1, b:0),
% 17.29/17.69 'p_8' [46, 0] (w:1, o:27, a:1, s:1, b:0),
% 17.29/17.69 'p_9' [47, 0] (w:1, o:28, a:1, s:1, b:0),
% 17.29/17.69 'p_10' [48, 0] (w:1, o:10, a:1, s:1, b:0),
% 17.29/17.69 'p_11' [49, 0] (w:1, o:11, a:1, s:1, b:0),
% 17.29/17.69 'p_12' [50, 0] (w:1, o:12, a:1, s:1, b:0),
% 17.29/17.69 'p_13' [51, 0] (w:1, o:13, a:1, s:1, b:0),
% 17.29/17.69 'p_14' [52, 0] (w:1, o:14, a:1, s:1, b:0),
% 17.29/17.69 'p_15' [53, 0] (w:1, o:15, a:1, s:1, b:0),
% 17.29/17.69 'p_16' [54, 0] (w:1, o:16, a:1, s:1, b:0),
% 17.29/17.69 'p_17' [55, 0] (w:1, o:17, a:1, s:1, b:0),
% 17.29/17.69 'p_18' [56, 0] (w:1, o:18, a:1, s:1, b:0),
% 17.29/17.69 'p_19' [57, 0] (w:1, o:19, a:1, s:1, b:0),
% 17.29/17.69 'p_20' [58, 0] (w:1, o:21, a:1, s:1, b:0),
% 17.29/17.69 state [59, 20] (w:1, o:79, a:1, s:1, b:0).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Starting Search:
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 3017
% 17.29/17.69 Kept: 2000
% 17.29/17.69 Inuse: 1008
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 6053
% 17.29/17.69 Kept: 4000
% 17.29/17.69 Inuse: 2020
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 9107
% 17.29/17.69 Kept: 6000
% 17.29/17.69 Inuse: 3038
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 12164
% 17.29/17.69 Kept: 8000
% 17.29/17.69 Inuse: 4057
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 15203
% 17.29/17.69 Kept: 10001
% 17.29/17.69 Inuse: 5070
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 18242
% 17.29/17.69 Kept: 12002
% 17.29/17.69 Inuse: 6083
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 21275
% 17.29/17.69 Kept: 14002
% 17.29/17.69 Inuse: 7094
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 24311
% 17.29/17.69 Kept: 16002
% 17.29/17.69 Inuse: 8106
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 27356
% 17.29/17.69 Kept: 18003
% 17.29/17.69 Inuse: 9121
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying clauses:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 30401
% 17.29/17.69 Kept: 20004
% 17.29/17.69 Inuse: 10136
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 33443
% 17.29/17.69 Kept: 22004
% 17.29/17.69 Inuse: 11150
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 36479
% 17.29/17.69 Kept: 24005
% 17.29/17.69 Inuse: 12162
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 39521
% 17.29/17.69 Kept: 26005
% 17.29/17.69 Inuse: 13176
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 42566
% 17.29/17.69 Kept: 28005
% 17.29/17.69 Inuse: 14191
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 45659
% 17.29/17.69 Kept: 30005
% 17.29/17.69 Inuse: 15222
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 48707
% 17.29/17.69 Kept: 32006
% 17.29/17.69 Inuse: 16238
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 51743
% 17.29/17.69 Kept: 34006
% 17.29/17.69 Inuse: 17250
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 54776
% 17.29/17.69 Kept: 36007
% 17.29/17.69 Inuse: 18261
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 57809
% 17.29/17.69 Kept: 38008
% 17.29/17.69 Inuse: 19272
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying clauses:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 60872
% 17.29/17.69 Kept: 40009
% 17.29/17.69 Inuse: 20293
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 63989
% 17.29/17.69 Kept: 42009
% 17.29/17.69 Inuse: 21332
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 67040
% 17.29/17.69 Kept: 44010
% 17.29/17.69 Inuse: 22349
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 70082
% 17.29/17.69 Kept: 46011
% 17.29/17.69 Inuse: 23363
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 73127
% 17.29/17.69 Kept: 48011
% 17.29/17.69 Inuse: 24378
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 76181
% 17.29/17.69 Kept: 50011
% 17.29/17.69 Inuse: 25396
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 79235
% 17.29/17.69 Kept: 52012
% 17.29/17.69 Inuse: 26414
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Intermediate Status:
% 17.29/17.69 Generated: 82325
% 17.29/17.69 Kept: 54012
% 17.29/17.69 Inuse: 27444
% 17.29/17.69 Deleted: 0
% 17.29/17.69 Deletedinuse: 0
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69 Resimplifying inuse:
% 17.29/17.69 Done
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 Bliksems!, er is een bewijs:
% 17.29/17.69 % SZS status Unsatisfiable
% 17.29/17.69 % SZS output start Refutation
% 17.29/17.69
% 17.29/17.69 clause( 0, [ ~( state( 'p_1', 'p_2', 'p_3', 'p_4', 'p_5', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 1, [ state( 'p_5', 'p_4', 'p_3', 'p_2', 'p_1', 'p_6', 'p_7', 'p_8'
% 17.29/17.69 , 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 2, [ state( Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8, V9,
% 17.29/17.69 V10, V11, V12, V13, X ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4,
% 17.29/17.69 V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 3, [ state( V13, X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7,
% 17.29/17.69 V8, V9, V10, V11, V12 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4,
% 17.29/17.69 V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 4, [ state( T, Z, Y, X, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8,
% 17.29/17.69 V9, V10, V11, V12, V13 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4
% 17.29/17.69 , V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 5, [ state( 'p_2', 'p_3', 'p_4', 'p_5', 'p_1', 'p_6', 'p_7', 'p_8'
% 17.29/17.69 , 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 8, [ state( 'p_3', 'p_4', 'p_5', 'p_1', 'p_6', 'p_7', 'p_8', 'p_9'
% 17.29/17.69 , 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17', 'p_18'
% 17.29/17.69 , 'p_19', 'p_20', 'p_2' ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 11, [ state( 'p_1', 'p_5', 'p_4', 'p_3', 'p_6', 'p_7', 'p_8', 'p_9'
% 17.29/17.69 , 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17', 'p_18'
% 17.29/17.69 , 'p_19', 'p_20', 'p_2' ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 49, [ state( 'p_2', 'p_1', 'p_5', 'p_4', 'p_3', 'p_6', 'p_7', 'p_8'
% 17.29/17.69 , 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 276, [ state( 'p_4', 'p_5', 'p_1', 'p_2', 'p_3', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 1618, [ state( 'p_5', 'p_1', 'p_2', 'p_3', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_4' ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 1621, [ state( 'p_3', 'p_2', 'p_1', 'p_5', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_4' ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 9538, [ state( 'p_4', 'p_3', 'p_2', 'p_1', 'p_5', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 .
% 17.29/17.69 clause( 55788, [] )
% 17.29/17.69 .
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 % SZS output end Refutation
% 17.29/17.69 found a proof!
% 17.29/17.69
% 17.29/17.69 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 17.29/17.69
% 17.29/17.69 initialclauses(
% 17.29/17.69 [ clause( 55790, [ ~( state( 'p_1', 'p_2', 'p_3', 'p_4', 'p_5', 'p_6',
% 17.29/17.69 'p_7', 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15',
% 17.29/17.69 'p_16', 'p_17', 'p_18', 'p_19', 'p_20' ) ) ] )
% 17.29/17.69 , clause( 55791, [ state( 'p_5', 'p_4', 'p_3', 'p_2', 'p_1', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 55792, [ ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6,
% 17.29/17.69 V7, V8, V9, V10, V11, V12, V13 ) ), state( Y, Z, T, U, W, V0, V1, V2, V3
% 17.29/17.69 , V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, X ) ] )
% 17.29/17.69 , clause( 55793, [ ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6,
% 17.29/17.69 V7, V8, V9, V10, V11, V12, V13 ) ), state( V13, X, Y, Z, T, U, W, V0, V1
% 17.29/17.69 , V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12 ) ] )
% 17.29/17.69 , clause( 55794, [ ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6,
% 17.29/17.69 V7, V8, V9, V10, V11, V12, V13 ) ), state( T, Z, Y, X, U, W, V0, V1, V2,
% 17.29/17.69 V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ] )
% 17.29/17.69 ] ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 0, [ ~( state( 'p_1', 'p_2', 'p_3', 'p_4', 'p_5', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ) ] )
% 17.29/17.69 , clause( 55790, [ ~( state( 'p_1', 'p_2', 'p_3', 'p_4', 'p_5', 'p_6',
% 17.29/17.69 'p_7', 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15',
% 17.29/17.69 'p_16', 'p_17', 'p_18', 'p_19', 'p_20' ) ) ] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 1, [ state( 'p_5', 'p_4', 'p_3', 'p_2', 'p_1', 'p_6', 'p_7', 'p_8'
% 17.29/17.69 , 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 55791, [ state( 'p_5', 'p_4', 'p_3', 'p_2', 'p_1', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 2, [ state( Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8, V9,
% 17.29/17.69 V10, V11, V12, V13, X ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4,
% 17.29/17.69 V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , clause( 55792, [ ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6,
% 17.29/17.69 V7, V8, V9, V10, V11, V12, V13 ) ), state( Y, Z, T, U, W, V0, V1, V2, V3
% 17.29/17.69 , V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, X ) ] )
% 17.29/17.69 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 17.29/17.69 , U ), :=( W, W ), :=( V0, V0 ), :=( V1, V1 ), :=( V2, V2 ), :=( V3, V3 )
% 17.29/17.69 , :=( V4, V4 ), :=( V5, V5 ), :=( V6, V6 ), :=( V7, V7 ), :=( V8, V8 ),
% 17.29/17.69 :=( V9, V9 ), :=( V10, V10 ), :=( V11, V11 ), :=( V12, V12 ), :=( V13,
% 17.29/17.69 V13 )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 3, [ state( V13, X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7,
% 17.29/17.69 V8, V9, V10, V11, V12 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4,
% 17.29/17.69 V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , clause( 55793, [ ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6,
% 17.29/17.69 V7, V8, V9, V10, V11, V12, V13 ) ), state( V13, X, Y, Z, T, U, W, V0, V1
% 17.29/17.69 , V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12 ) ] )
% 17.29/17.69 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 17.29/17.69 , U ), :=( W, W ), :=( V0, V0 ), :=( V1, V1 ), :=( V2, V2 ), :=( V3, V3 )
% 17.29/17.69 , :=( V4, V4 ), :=( V5, V5 ), :=( V6, V6 ), :=( V7, V7 ), :=( V8, V8 ),
% 17.29/17.69 :=( V9, V9 ), :=( V10, V10 ), :=( V11, V11 ), :=( V12, V12 ), :=( V13,
% 17.29/17.69 V13 )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 4, [ state( T, Z, Y, X, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8,
% 17.29/17.69 V9, V10, V11, V12, V13 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4
% 17.29/17.69 , V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , clause( 55794, [ ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6,
% 17.29/17.69 V7, V8, V9, V10, V11, V12, V13 ) ), state( T, Z, Y, X, U, W, V0, V1, V2,
% 17.29/17.69 V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ] )
% 17.29/17.69 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 17.29/17.69 , U ), :=( W, W ), :=( V0, V0 ), :=( V1, V1 ), :=( V2, V2 ), :=( V3, V3 )
% 17.29/17.69 , :=( V4, V4 ), :=( V5, V5 ), :=( V6, V6 ), :=( V7, V7 ), :=( V8, V8 ),
% 17.29/17.69 :=( V9, V9 ), :=( V10, V10 ), :=( V11, V11 ), :=( V12, V12 ), :=( V13,
% 17.29/17.69 V13 )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 resolution(
% 17.29/17.69 clause( 55795, [ state( 'p_2', 'p_3', 'p_4', 'p_5', 'p_1', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 4, [ state( T, Z, Y, X, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8
% 17.29/17.69 , V9, V10, V11, V12, V13 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3,
% 17.29/17.69 V4, V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , 1, clause( 1, [ state( 'p_5', 'p_4', 'p_3', 'p_2', 'p_1', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , 0, substitution( 0, [ :=( X, 'p_5' ), :=( Y, 'p_4' ), :=( Z, 'p_3' ),
% 17.29/17.69 :=( T, 'p_2' ), :=( U, 'p_1' ), :=( W, 'p_6' ), :=( V0, 'p_7' ), :=( V1,
% 17.29/17.69 'p_8' ), :=( V2, 'p_9' ), :=( V3, 'p_10' ), :=( V4, 'p_11' ), :=( V5,
% 17.29/17.69 'p_12' ), :=( V6, 'p_13' ), :=( V7, 'p_14' ), :=( V8, 'p_15' ), :=( V9,
% 17.29/17.69 'p_16' ), :=( V10, 'p_17' ), :=( V11, 'p_18' ), :=( V12, 'p_19' ), :=(
% 17.29/17.69 V13, 'p_20' )] ), substitution( 1, [] )).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 5, [ state( 'p_2', 'p_3', 'p_4', 'p_5', 'p_1', 'p_6', 'p_7', 'p_8'
% 17.29/17.69 , 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 55795, [ state( 'p_2', 'p_3', 'p_4', 'p_5', 'p_1', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 resolution(
% 17.29/17.69 clause( 55796, [ state( 'p_3', 'p_4', 'p_5', 'p_1', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_2' ) ] )
% 17.29/17.69 , clause( 2, [ state( Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8, V9
% 17.29/17.69 , V10, V11, V12, V13, X ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4
% 17.29/17.69 , V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , 1, clause( 5, [ state( 'p_2', 'p_3', 'p_4', 'p_5', 'p_1', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , 0, substitution( 0, [ :=( X, 'p_2' ), :=( Y, 'p_3' ), :=( Z, 'p_4' ),
% 17.29/17.69 :=( T, 'p_5' ), :=( U, 'p_1' ), :=( W, 'p_6' ), :=( V0, 'p_7' ), :=( V1,
% 17.29/17.69 'p_8' ), :=( V2, 'p_9' ), :=( V3, 'p_10' ), :=( V4, 'p_11' ), :=( V5,
% 17.29/17.69 'p_12' ), :=( V6, 'p_13' ), :=( V7, 'p_14' ), :=( V8, 'p_15' ), :=( V9,
% 17.29/17.69 'p_16' ), :=( V10, 'p_17' ), :=( V11, 'p_18' ), :=( V12, 'p_19' ), :=(
% 17.29/17.69 V13, 'p_20' )] ), substitution( 1, [] )).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 8, [ state( 'p_3', 'p_4', 'p_5', 'p_1', 'p_6', 'p_7', 'p_8', 'p_9'
% 17.29/17.69 , 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17', 'p_18'
% 17.29/17.69 , 'p_19', 'p_20', 'p_2' ) ] )
% 17.29/17.69 , clause( 55796, [ state( 'p_3', 'p_4', 'p_5', 'p_1', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_2' ) ] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 resolution(
% 17.29/17.69 clause( 55797, [ state( 'p_1', 'p_5', 'p_4', 'p_3', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_2' ) ] )
% 17.29/17.69 , clause( 4, [ state( T, Z, Y, X, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8
% 17.29/17.69 , V9, V10, V11, V12, V13 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3,
% 17.29/17.69 V4, V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , 1, clause( 8, [ state( 'p_3', 'p_4', 'p_5', 'p_1', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_2' ) ] )
% 17.29/17.69 , 0, substitution( 0, [ :=( X, 'p_3' ), :=( Y, 'p_4' ), :=( Z, 'p_5' ),
% 17.29/17.69 :=( T, 'p_1' ), :=( U, 'p_6' ), :=( W, 'p_7' ), :=( V0, 'p_8' ), :=( V1,
% 17.29/17.69 'p_9' ), :=( V2, 'p_10' ), :=( V3, 'p_11' ), :=( V4, 'p_12' ), :=( V5,
% 17.29/17.69 'p_13' ), :=( V6, 'p_14' ), :=( V7, 'p_15' ), :=( V8, 'p_16' ), :=( V9,
% 17.29/17.69 'p_17' ), :=( V10, 'p_18' ), :=( V11, 'p_19' ), :=( V12, 'p_20' ), :=(
% 17.29/17.69 V13, 'p_2' )] ), substitution( 1, [] )).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 11, [ state( 'p_1', 'p_5', 'p_4', 'p_3', 'p_6', 'p_7', 'p_8', 'p_9'
% 17.29/17.69 , 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17', 'p_18'
% 17.29/17.69 , 'p_19', 'p_20', 'p_2' ) ] )
% 17.29/17.69 , clause( 55797, [ state( 'p_1', 'p_5', 'p_4', 'p_3', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_2' ) ] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 resolution(
% 17.29/17.69 clause( 55798, [ state( 'p_2', 'p_1', 'p_5', 'p_4', 'p_3', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 3, [ state( V13, X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7
% 17.29/17.69 , V8, V9, V10, V11, V12 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4
% 17.29/17.69 , V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , 1, clause( 11, [ state( 'p_1', 'p_5', 'p_4', 'p_3', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_2' ) ] )
% 17.29/17.69 , 0, substitution( 0, [ :=( X, 'p_1' ), :=( Y, 'p_5' ), :=( Z, 'p_4' ),
% 17.29/17.69 :=( T, 'p_3' ), :=( U, 'p_6' ), :=( W, 'p_7' ), :=( V0, 'p_8' ), :=( V1,
% 17.29/17.69 'p_9' ), :=( V2, 'p_10' ), :=( V3, 'p_11' ), :=( V4, 'p_12' ), :=( V5,
% 17.29/17.69 'p_13' ), :=( V6, 'p_14' ), :=( V7, 'p_15' ), :=( V8, 'p_16' ), :=( V9,
% 17.29/17.69 'p_17' ), :=( V10, 'p_18' ), :=( V11, 'p_19' ), :=( V12, 'p_20' ), :=(
% 17.29/17.69 V13, 'p_2' )] ), substitution( 1, [] )).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 49, [ state( 'p_2', 'p_1', 'p_5', 'p_4', 'p_3', 'p_6', 'p_7', 'p_8'
% 17.29/17.69 , 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 55798, [ state( 'p_2', 'p_1', 'p_5', 'p_4', 'p_3', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 resolution(
% 17.29/17.69 clause( 55799, [ state( 'p_4', 'p_5', 'p_1', 'p_2', 'p_3', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 4, [ state( T, Z, Y, X, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8
% 17.29/17.69 , V9, V10, V11, V12, V13 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3,
% 17.29/17.69 V4, V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , 1, clause( 49, [ state( 'p_2', 'p_1', 'p_5', 'p_4', 'p_3', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , 0, substitution( 0, [ :=( X, 'p_2' ), :=( Y, 'p_1' ), :=( Z, 'p_5' ),
% 17.29/17.69 :=( T, 'p_4' ), :=( U, 'p_3' ), :=( W, 'p_6' ), :=( V0, 'p_7' ), :=( V1,
% 17.29/17.69 'p_8' ), :=( V2, 'p_9' ), :=( V3, 'p_10' ), :=( V4, 'p_11' ), :=( V5,
% 17.29/17.69 'p_12' ), :=( V6, 'p_13' ), :=( V7, 'p_14' ), :=( V8, 'p_15' ), :=( V9,
% 17.29/17.69 'p_16' ), :=( V10, 'p_17' ), :=( V11, 'p_18' ), :=( V12, 'p_19' ), :=(
% 17.29/17.69 V13, 'p_20' )] ), substitution( 1, [] )).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 276, [ state( 'p_4', 'p_5', 'p_1', 'p_2', 'p_3', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 55799, [ state( 'p_4', 'p_5', 'p_1', 'p_2', 'p_3', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 resolution(
% 17.29/17.69 clause( 55800, [ state( 'p_5', 'p_1', 'p_2', 'p_3', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_4' ) ] )
% 17.29/17.69 , clause( 2, [ state( Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8, V9
% 17.29/17.69 , V10, V11, V12, V13, X ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4
% 17.29/17.69 , V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , 1, clause( 276, [ state( 'p_4', 'p_5', 'p_1', 'p_2', 'p_3', 'p_6', 'p_7'
% 17.29/17.69 , 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , 0, substitution( 0, [ :=( X, 'p_4' ), :=( Y, 'p_5' ), :=( Z, 'p_1' ),
% 17.29/17.69 :=( T, 'p_2' ), :=( U, 'p_3' ), :=( W, 'p_6' ), :=( V0, 'p_7' ), :=( V1,
% 17.29/17.69 'p_8' ), :=( V2, 'p_9' ), :=( V3, 'p_10' ), :=( V4, 'p_11' ), :=( V5,
% 17.29/17.69 'p_12' ), :=( V6, 'p_13' ), :=( V7, 'p_14' ), :=( V8, 'p_15' ), :=( V9,
% 17.29/17.69 'p_16' ), :=( V10, 'p_17' ), :=( V11, 'p_18' ), :=( V12, 'p_19' ), :=(
% 17.29/17.69 V13, 'p_20' )] ), substitution( 1, [] )).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 1618, [ state( 'p_5', 'p_1', 'p_2', 'p_3', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_4' ) ] )
% 17.29/17.69 , clause( 55800, [ state( 'p_5', 'p_1', 'p_2', 'p_3', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_4' ) ] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 resolution(
% 17.29/17.69 clause( 55801, [ state( 'p_3', 'p_2', 'p_1', 'p_5', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_4' ) ] )
% 17.29/17.69 , clause( 4, [ state( T, Z, Y, X, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8
% 17.29/17.69 , V9, V10, V11, V12, V13 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3,
% 17.29/17.69 V4, V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , 1, clause( 1618, [ state( 'p_5', 'p_1', 'p_2', 'p_3', 'p_6', 'p_7', 'p_8'
% 17.29/17.69 , 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_4' ) ] )
% 17.29/17.69 , 0, substitution( 0, [ :=( X, 'p_5' ), :=( Y, 'p_1' ), :=( Z, 'p_2' ),
% 17.29/17.69 :=( T, 'p_3' ), :=( U, 'p_6' ), :=( W, 'p_7' ), :=( V0, 'p_8' ), :=( V1,
% 17.29/17.69 'p_9' ), :=( V2, 'p_10' ), :=( V3, 'p_11' ), :=( V4, 'p_12' ), :=( V5,
% 17.29/17.69 'p_13' ), :=( V6, 'p_14' ), :=( V7, 'p_15' ), :=( V8, 'p_16' ), :=( V9,
% 17.29/17.69 'p_17' ), :=( V10, 'p_18' ), :=( V11, 'p_19' ), :=( V12, 'p_20' ), :=(
% 17.29/17.69 V13, 'p_4' )] ), substitution( 1, [] )).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 1621, [ state( 'p_3', 'p_2', 'p_1', 'p_5', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_4' ) ] )
% 17.29/17.69 , clause( 55801, [ state( 'p_3', 'p_2', 'p_1', 'p_5', 'p_6', 'p_7', 'p_8',
% 17.29/17.69 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_4' ) ] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 resolution(
% 17.29/17.69 clause( 55802, [ state( 'p_4', 'p_3', 'p_2', 'p_1', 'p_5', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 3, [ state( V13, X, Y, Z, T, U, W, V0, V1, V2, V3, V4, V5, V6, V7
% 17.29/17.69 , V8, V9, V10, V11, V12 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3, V4
% 17.29/17.69 , V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , 1, clause( 1621, [ state( 'p_3', 'p_2', 'p_1', 'p_5', 'p_6', 'p_7', 'p_8'
% 17.29/17.69 , 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16', 'p_17',
% 17.29/17.69 'p_18', 'p_19', 'p_20', 'p_4' ) ] )
% 17.29/17.69 , 0, substitution( 0, [ :=( X, 'p_3' ), :=( Y, 'p_2' ), :=( Z, 'p_1' ),
% 17.29/17.69 :=( T, 'p_5' ), :=( U, 'p_6' ), :=( W, 'p_7' ), :=( V0, 'p_8' ), :=( V1,
% 17.29/17.69 'p_9' ), :=( V2, 'p_10' ), :=( V3, 'p_11' ), :=( V4, 'p_12' ), :=( V5,
% 17.29/17.69 'p_13' ), :=( V6, 'p_14' ), :=( V7, 'p_15' ), :=( V8, 'p_16' ), :=( V9,
% 17.29/17.69 'p_17' ), :=( V10, 'p_18' ), :=( V11, 'p_19' ), :=( V12, 'p_20' ), :=(
% 17.29/17.69 V13, 'p_4' )] ), substitution( 1, [] )).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 9538, [ state( 'p_4', 'p_3', 'p_2', 'p_1', 'p_5', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 55802, [ state( 'p_4', 'p_3', 'p_2', 'p_1', 'p_5', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 resolution(
% 17.29/17.69 clause( 55803, [ state( 'p_1', 'p_2', 'p_3', 'p_4', 'p_5', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , clause( 4, [ state( T, Z, Y, X, U, W, V0, V1, V2, V3, V4, V5, V6, V7, V8
% 17.29/17.69 , V9, V10, V11, V12, V13 ), ~( state( X, Y, Z, T, U, W, V0, V1, V2, V3,
% 17.29/17.69 V4, V5, V6, V7, V8, V9, V10, V11, V12, V13 ) ) ] )
% 17.29/17.69 , 1, clause( 9538, [ state( 'p_4', 'p_3', 'p_2', 'p_1', 'p_5', 'p_6', 'p_7'
% 17.29/17.69 , 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , 0, substitution( 0, [ :=( X, 'p_4' ), :=( Y, 'p_3' ), :=( Z, 'p_2' ),
% 17.29/17.69 :=( T, 'p_1' ), :=( U, 'p_5' ), :=( W, 'p_6' ), :=( V0, 'p_7' ), :=( V1,
% 17.29/17.69 'p_8' ), :=( V2, 'p_9' ), :=( V3, 'p_10' ), :=( V4, 'p_11' ), :=( V5,
% 17.29/17.69 'p_12' ), :=( V6, 'p_13' ), :=( V7, 'p_14' ), :=( V8, 'p_15' ), :=( V9,
% 17.29/17.69 'p_16' ), :=( V10, 'p_17' ), :=( V11, 'p_18' ), :=( V12, 'p_19' ), :=(
% 17.29/17.69 V13, 'p_20' )] ), substitution( 1, [] )).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 resolution(
% 17.29/17.69 clause( 55804, [] )
% 17.29/17.69 , clause( 0, [ ~( state( 'p_1', 'p_2', 'p_3', 'p_4', 'p_5', 'p_6', 'p_7',
% 17.29/17.69 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15', 'p_16',
% 17.29/17.69 'p_17', 'p_18', 'p_19', 'p_20' ) ) ] )
% 17.29/17.69 , 0, clause( 55803, [ state( 'p_1', 'p_2', 'p_3', 'p_4', 'p_5', 'p_6',
% 17.29/17.69 'p_7', 'p_8', 'p_9', 'p_10', 'p_11', 'p_12', 'p_13', 'p_14', 'p_15',
% 17.29/17.69 'p_16', 'p_17', 'p_18', 'p_19', 'p_20' ) ] )
% 17.29/17.69 , 0, substitution( 0, [] ), substitution( 1, [] )).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 subsumption(
% 17.29/17.69 clause( 55788, [] )
% 17.29/17.69 , clause( 55804, [] )
% 17.29/17.69 , substitution( 0, [] ), permutation( 0, [] ) ).
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 end.
% 17.29/17.69
% 17.29/17.69 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 17.29/17.69
% 17.29/17.69 Memory use:
% 17.29/17.69
% 17.29/17.69 space for terms: 1171992
% 17.29/17.69 space for clauses: 6088212
% 17.29/17.69
% 17.29/17.69
% 17.29/17.69 clauses generated: 85031
% 17.29/17.69 clauses kept: 55789
% 17.29/17.69 clauses selected: 28346
% 17.29/17.69 clauses deleted: 0
% 17.29/17.69 clauses inuse deleted: 0
% 17.29/17.69
% 17.29/17.69 subsentry: 29581
% 17.29/17.69 literals s-matched: 29581
% 17.29/17.69 literals matched: 29581
% 17.29/17.69 full subsumption: 0
% 17.29/17.69
% 17.29/17.69 checksum: 330934691
% 17.29/17.70
% 17.29/17.70
% 17.29/17.70 Bliksem ended
%------------------------------------------------------------------------------