PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-9symml.opb
MD5SUM	48809ba02390b1184dab90aed89aff8e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4517
Optimality of the best value was proved	NO
Number of terms in the objective function	651
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	28138
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	28138
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02684
Number of variables	651
Total number of constraints	1658
Number of constraints which are clauses	1656
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2
Minimum length of a constraint	1
Maximum length of a constraint	42
Trace number 4998

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-13 21:11:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2210 boxname=wulflinc9 idbench=246 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  48809ba02390b1184dab90aed89aff8e  /oldhome/oroussel/tmp/wulflinc9/normalized-9symml.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc9/normalized-9symml.opb
IDLAUNCH: 2210
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        913924 kB
Buffers:         33980 kB
Cached:          67048 kB
SwapCached:        564 kB
Active:          49728 kB
Inactive:        54708 kB
HighTotal:      131008 kB
HighFree:        60060 kB
LowTotal:       903652 kB
LowFree:        853864 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10684 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:31:11 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 2210 7 1200.15 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1579 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1552     6592 |     517       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 6227[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:101537     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  240640   564833 |   80213       0        0     nan |  0.000 % |
c |       100 |  240294   564068 |   88234      97      554     5.7 |  0.124 % |
c |       250 |  239475   562211 |   97057     242     1239     5.1 |  0.372 % |
c |       475 |  239475   562211 |  106763     467     2772     5.9 |  0.372 % |
c |       812 |  239475   562211 |  117439     804     5080     6.3 |  0.372 % |
c |      1318 |  239344   561924 |  129183    1306    10185     7.8 |  0.418 % |
c |      2077 |  239154   561493 |  142102    2061    21860    10.6 |  0.491 % |
c |      3217 |  238924   560969 |  156312    3195    43126    13.5 |  0.574 % |
c |      4925 |  238870   560853 |  171943    4898   147580    30.1 |  0.598 % |
c |      7488 |  238545   560119 |  189138    7447   199936    26.8 |  0.694 % |
c |     11333 |  238182   559291 |  208051   11252   264258    23.5 |  0.811 % |
c |     17099 |  237688   558162 |  228857   16994   352844    20.8 |  0.969 % |
c |     25751 |  237623   558014 |  251742   25643   903840    35.2 |  0.991 % |
c ==============================================================================
c [1mFound solution: 5682[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:81756     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29821 |  435689  1020432 |  145229   29713  1042028    35.1 |  0.991 % |
c |     29922 |  435689  1020432 |  159751   29814  1042915    35.0 |  0.570 % |
c |     30072 |  435689  1020432 |  175727   29964  1043798    34.8 |  0.570 % |
c |     30297 |  435410  1019814 |  193299   30186  1047211    34.7 |  0.617 % |
c |     30635 |  434343  1017394 |  212629   30492  1053024    34.5 |  0.811 % |
c |     31141 |  434343  1017394 |  233892   30998  1066445    34.4 |  0.811 % |
c |     31900 |  434343  1017394 |  257282   31757  1076013    33.9 |  0.811 % |
c |     33039 |  434343  1017394 |  283010   32896  1253111    38.1 |  0.811 % |
c |     34748 |  434343  1017394 |  311311   34605  1301864    37.6 |  0.811 % |
c |     37311 |  434331  1017367 |  342442   37166  1344836    36.2 |  0.813 % |
c |     41155 |  434331  1017367 |  376686   41010  1457843    35.5 |  0.813 % |
c |     46922 |  434331  1017367 |  414355   46777  2162173    46.2 |  0.813 % |
c |     55572 |  434242  1017165 |  455790   55424  3473368    62.7 |  0.830 % |
c |     68546 |  434242  1017165 |  501369   68398  6520599    95.3 |  0.830 % |
c |     88008 |  434235  1017150 |  551506   87857  9667702   110.0 |  0.832 % |
c |    117200 |  433771  1016104 |  606657  117042 19603779   167.5 |  0.911 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/54 543
Raw data (stat): 543 (runsolver) R 542 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420867096 1052672 99 4294967295 134512640 135381576 3221224544 3221219788 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99997 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 8053 0 0 0 978 20 0 0 25 0 1 0 420867096 35864576 7593 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8756 7593 603 41 0 8715 0
vsize: 35024
[startup+20.0007 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 8175 0 0 0 1978 20 0 0 25 0 1 0 420867096 36265984 7715 4294967295 134512640 134672761 3221224640 3221223788 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8854 7715 603 41 0 8813 0
vsize: 35416
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 8273 0 0 0 2977 21 0 0 25 0 1 0 420867096 36691968 7813 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8958 7813 603 41 0 8917 0
vsize: 35832
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 8356 0 0 0 3977 21 0 0 25 0 1 0 420867096 37019648 7896 4294967295 134512640 134672761 3221224640 3221223808 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9038 7896 603 41 0 8997 0
vsize: 36152
[startup+50.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 8488 0 0 0 4976 22 0 0 25 0 1 0 420867096 37560320 8028 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9170 8028 603 41 0 9129 0
vsize: 36680
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 8744 0 0 0 5975 23 0 0 25 0 1 0 420867096 38596608 8284 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9423 8284 603 41 0 9382 0
vsize: 37692
[startup+70.0035 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 8931 0 0 0 6975 24 0 0 25 0 1 0 420867096 39403520 8471 4294967295 134512640 134672761 3221224640 3221223744 134555091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9620 8471 603 41 0 9579 0
vsize: 38480
[startup+80.0043 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 9024 0 0 0 7973 25 0 0 25 0 1 0 420867096 39804928 8564 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9718 8564 603 41 0 9677 0
vsize: 38872
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 9127 0 0 0 8973 26 0 0 25 0 1 0 420867096 40206336 8667 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 8667 603 41 0 9775 0
vsize: 39264
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 9263 0 0 0 9972 26 0 0 25 0 1 0 420867096 40747008 8803 4294967295 134512640 134672761 3221224640 3221223840 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9948 8803 603 41 0 9907 0
vsize: 39792
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 15625 0 0 0 10955 44 0 0 25 0 1 0 420867096 70361088 14710 4294967295 134512640 134672761 3221224640 3221223812 134556606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17178 14710 603 41 0 17137 0
vsize: 68712
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 15696 0 0 0 11954 44 0 0 25 0 1 0 420867096 70496256 14781 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17211 14781 603 41 0 17170 0
vsize: 68844
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 15845 0 0 0 12954 45 0 0 25 0 1 0 420867096 71168000 14930 4294967295 134512640 134672761 3221224640 3221223744 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17375 14930 603 41 0 17334 0
vsize: 69500
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 15936 0 0 0 13953 45 0 0 25 0 1 0 420867096 71704576 15021 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17506 15021 603 41 0 17465 0
vsize: 70024
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 15994 0 0 0 14952 46 0 0 25 0 1 0 420867096 71835648 15079 4294967295 134512640 134672761 3221224640 3221223808 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17538 15079 603 41 0 17497 0
vsize: 70152
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 16065 0 0 0 15952 46 0 0 25 0 1 0 420867096 72097792 15150 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17602 15150 603 41 0 17561 0
vsize: 70408
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 16131 0 0 0 16951 47 0 0 25 0 1 0 420867096 72368128 15216 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17668 15216 603 41 0 17627 0
vsize: 70672
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 16186 0 0 0 17950 48 0 0 25 0 1 0 420867096 72638464 15271 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17734 15271 603 41 0 17693 0
vsize: 70936
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 16263 0 0 0 18950 48 0 0 25 0 1 0 420867096 72900608 15348 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17798 15348 603 41 0 17757 0
vsize: 71192
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 16376 0 0 0 19949 49 0 0 25 0 1 0 420867096 73306112 15461 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17897 15461 603 41 0 17856 0
vsize: 71588
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 16524 0 0 0 20948 50 0 0 25 0 1 0 420867096 73977856 15609 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18061 15609 603 41 0 18020 0
vsize: 72244
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 16646 0 0 0 21947 51 0 0 25 0 1 0 420867096 74518528 15731 4294967295 134512640 134672761 3221224640 3221223804 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18193 15731 603 41 0 18152 0
vsize: 72772
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 16744 0 0 0 22946 51 0 0 25 0 1 0 420867096 74919936 15829 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18291 15829 603 41 0 18250 0
vsize: 73164
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 16907 0 0 0 23946 52 0 0 25 0 1 0 420867096 75579392 15992 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18452 15992 603 41 0 18411 0
vsize: 73808
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 16979 0 0 0 24945 53 0 0 25 0 1 0 420867096 75849728 16064 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18518 16064 603 41 0 18477 0
vsize: 74072
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 17067 0 0 0 25944 54 0 0 25 0 1 0 420867096 76120064 16152 4294967295 134512640 134672761 3221224640 3221223776 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18584 16152 603 41 0 18543 0
vsize: 74336
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 17138 0 0 0 26944 54 0 0 25 0 1 0 420867096 76521472 16223 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18682 16223 603 41 0 18641 0
vsize: 74728
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 17269 0 0 0 27943 54 0 0 25 0 1 0 420867096 77053952 16354 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18812 16354 603 41 0 18771 0
vsize: 75248
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 17372 0 0 0 28942 55 0 0 25 0 1 0 420867096 77451264 16457 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18909 16457 603 41 0 18868 0
vsize: 75636
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 17552 0 0 0 29941 56 0 0 25 0 1 0 420867096 78118912 16637 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19072 16637 603 41 0 19031 0
vsize: 76288
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 17742 0 0 0 30940 57 0 0 25 0 1 0 420867096 78929920 16827 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19270 16827 603 41 0 19229 0
vsize: 77080
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 17886 0 0 0 31939 58 0 0 25 0 1 0 420867096 79466496 16971 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19401 16971 603 41 0 19360 0
vsize: 77604
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18008 0 0 0 32939 58 0 0 25 0 1 0 420867096 79982592 17093 4294967295 134512640 134672761 3221224640 3221223776 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19527 17093 603 41 0 19486 0
vsize: 78108
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18132 0 0 0 33937 60 0 0 25 0 1 0 420867096 80510976 17217 4294967295 134512640 134672761 3221224640 3221223744 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19656 17217 603 41 0 19615 0
vsize: 78624
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18294 0 0 0 34937 60 0 0 25 0 1 0 420867096 81182720 17379 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19820 17379 603 41 0 19779 0
vsize: 79280
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18341 0 0 0 35936 61 0 0 25 0 1 0 420867096 81317888 17426 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19853 17426 603 41 0 19812 0
vsize: 79412
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18388 0 0 0 36936 61 0 0 25 0 1 0 420867096 81584128 17473 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19918 17473 603 41 0 19877 0
vsize: 79672
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18429 0 0 0 37935 62 0 0 25 0 1 0 420867096 81719296 17514 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19951 17514 603 41 0 19910 0
vsize: 79804
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18482 0 0 0 38935 62 0 0 25 0 1 0 420867096 81981440 17567 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20015 17567 603 41 0 19974 0
vsize: 80060
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18528 0 0 0 39934 63 0 0 25 0 1 0 420867096 82116608 17613 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20048 17613 603 41 0 20007 0
vsize: 80192
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18580 0 0 0 40934 63 0 0 25 0 1 0 420867096 82382848 17665 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20113 17665 603 41 0 20072 0
vsize: 80452
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18655 0 0 0 41933 64 0 0 25 0 1 0 420867096 82649088 17740 4294967295 134512640 134672761 3221224640 3221223808 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20178 17740 603 41 0 20137 0
vsize: 80712
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 18774 0 0 0 42932 65 0 0 25 0 1 0 420867096 83054592 17859 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20277 17859 603 41 0 20236 0
vsize: 81108
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 19140 0 0 0 43930 66 0 0 25 0 1 0 420867096 84553728 18225 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20643 18225 603 41 0 20602 0
vsize: 82572
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 19548 0 0 0 44929 67 0 0 25 0 1 0 420867096 86306816 18633 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 18633 603 41 0 21030 0
vsize: 84284
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 19998 0 0 0 45928 69 0 0 25 0 1 0 420867096 88068096 19083 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21501 19083 603 41 0 21460 0
vsize: 86004
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 20509 0 0 0 46926 71 0 0 25 0 1 0 420867096 90234880 19594 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22030 19594 603 41 0 21989 0
vsize: 88120
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 20938 0 0 0 47925 72 0 0 25 0 1 0 420867096 92262400 20023 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22525 20023 603 41 0 22484 0
vsize: 90100
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 21329 0 0 0 48924 73 0 0 25 0 1 0 420867096 93818880 20414 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22905 20414 603 41 0 22864 0
vsize: 91620
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 21399 0 0 0 49923 73 0 0 25 0 1 0 420867096 94085120 20484 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22970 20484 603 41 0 22929 0
vsize: 91880
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 21487 0 0 0 50923 74 0 0 25 0 1 0 420867096 94486528 20572 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23068 20572 603 41 0 23027 0
vsize: 92272
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 21548 0 0 0 51923 74 0 0 25 0 1 0 420867096 94756864 20633 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23134 20633 603 41 0 23093 0
vsize: 92536
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 21711 0 0 0 52922 75 0 0 25 0 1 0 420867096 95285248 20796 4294967295 134512640 134672761 3221224640 3221223776 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23263 20796 603 41 0 23222 0
vsize: 93052
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 21959 0 0 0 53922 75 0 0 25 0 1 0 420867096 96346112 21044 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23522 21044 603 41 0 23481 0
vsize: 94088
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 22207 0 0 0 54922 76 0 0 25 0 1 0 420867096 97419264 21292 4294967295 134512640 134672761 3221224640 3221223744 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23784 21292 603 41 0 23743 0
vsize: 95136
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 22489 0 0 0 55921 76 0 0 25 0 1 0 420867096 98484224 21574 4294967295 134512640 134672761 3221224640 3221223808 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24044 21574 603 41 0 24003 0
vsize: 96176
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 22775 0 0 0 56920 77 0 0 25 0 1 0 420867096 99655680 21860 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24330 21860 603 41 0 24289 0
vsize: 97320
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 23025 0 0 0 57920 78 0 0 25 0 1 0 420867096 100720640 22110 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24590 22110 603 41 0 24549 0
vsize: 98360
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 23311 0 0 0 58919 79 0 0 25 0 1 0 420867096 101916672 22396 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24882 22396 603 41 0 24841 0
vsize: 99528
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 23523 0 0 0 59918 80 0 0 25 0 1 0 420867096 102842368 22608 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25108 22608 603 41 0 25067 0
vsize: 100432
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 23756 0 0 0 60918 80 0 0 25 0 1 0 420867096 103768064 22841 4294967295 134512640 134672761 3221224640 3221223776 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25334 22841 603 41 0 25293 0
vsize: 101336
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 23996 0 0 0 61918 81 0 0 25 0 1 0 420867096 104697856 23081 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25561 23081 603 41 0 25520 0
vsize: 102244
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 24205 0 0 0 62917 82 0 0 25 0 1 0 420867096 105623552 23290 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25787 23290 603 41 0 25746 0
vsize: 103148
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 24431 0 0 0 63917 82 0 0 25 0 1 0 420867096 106545152 23516 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26012 23516 603 41 0 25971 0
vsize: 104048
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 24572 0 0 0 64917 83 0 0 25 0 1 0 420867096 107081728 23657 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26143 23657 603 41 0 26102 0
vsize: 104572
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 24765 0 0 0 65916 83 0 0 25 0 1 0 420867096 107892736 23850 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26341 23850 603 41 0 26300 0
vsize: 105364
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 24802 0 0 0 66916 83 0 0 25 0 1 0 420867096 108027904 23887 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26374 23887 603 41 0 26333 0
vsize: 105496
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 24871 0 0 0 67916 84 0 0 25 0 1 0 420867096 108294144 23956 4294967295 134512640 134672761 3221224640 3221223784 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26439 23956 603 41 0 26398 0
vsize: 105756
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 24949 0 0 0 68916 84 0 0 25 0 1 0 420867096 108552192 24034 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26502 24034 603 41 0 26461 0
vsize: 106008
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 25071 0 0 0 69916 84 0 0 25 0 1 0 420867096 109088768 24156 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26633 24156 603 41 0 26592 0
vsize: 106532
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 25184 0 0 0 70915 85 0 0 25 0 1 0 420867096 109494272 24269 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26732 24269 603 41 0 26691 0
vsize: 106928
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 25284 0 0 0 71915 86 0 0 25 0 1 0 420867096 109895680 24369 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26830 24369 603 41 0 26789 0
vsize: 107320
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 25398 0 0 0 72914 86 0 0 25 0 1 0 420867096 110432256 24483 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26961 24483 603 41 0 26920 0
vsize: 107844
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 25540 0 0 0 73914 86 0 0 25 0 1 0 420867096 110972928 24625 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27093 24625 603 41 0 27052 0
vsize: 108372
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 25703 0 0 0 74914 87 0 0 25 0 1 0 420867096 111644672 24788 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27257 24788 603 41 0 27216 0
vsize: 109028
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 25911 0 0 0 75914 87 0 0 25 0 1 0 420867096 112562176 24996 4294967295 134512640 134672761 3221224640 3221223808 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24996 603 41 0 27440 0
vsize: 109924
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 26128 0 0 0 76913 88 0 0 25 0 1 0 420867096 113360896 25213 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27676 25213 603 41 0 27635 0
vsize: 110704
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 26310 0 0 0 77913 88 0 0 25 0 1 0 420867096 114159616 25395 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27871 25395 603 41 0 27830 0
vsize: 111484
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 26515 0 0 0 78913 89 0 0 25 0 1 0 420867096 114966528 25600 4294967295 134512640 134672761 3221224640 3221223744 134559922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28068 25600 603 41 0 28027 0
vsize: 112272
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 26636 0 0 0 79913 89 0 0 25 0 1 0 420867096 115499008 25721 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28198 25721 603 41 0 28157 0
vsize: 112792
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 26813 0 0 0 80912 90 0 0 25 0 1 0 420867096 116154368 25898 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28358 25898 603 41 0 28317 0
vsize: 113432
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 26962 0 0 0 81913 90 0 0 25 0 1 0 420867096 116813824 26047 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28519 26047 603 41 0 28478 0
vsize: 114076
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 27146 0 0 0 82912 90 0 0 25 0 1 0 420867096 117616640 26231 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28715 26231 603 41 0 28674 0
vsize: 114860
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 27298 0 0 0 83912 91 0 0 25 0 1 0 420867096 118136832 26383 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28842 26383 603 41 0 28801 0
vsize: 115368
[startup+850.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 27435 0 0 0 84912 91 0 0 25 0 1 0 420867096 118792192 26520 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29002 26520 603 41 0 28961 0
vsize: 116008
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 27593 0 0 0 85912 92 0 0 25 0 1 0 420867096 119332864 26678 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29134 26678 603 41 0 29093 0
vsize: 116536
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 27777 0 0 0 86911 92 0 0 25 0 1 0 420867096 120127488 26862 4294967295 134512640 134672761 3221224640 3221223824 134558563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29328 26862 603 41 0 29287 0
vsize: 117312
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 27952 0 0 0 87911 93 0 0 25 0 1 0 420867096 120807424 27037 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29494 27037 603 41 0 29453 0
vsize: 117976
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 28132 0 0 0 88910 93 0 0 25 0 1 0 420867096 121610240 27217 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29690 27217 603 41 0 29649 0
vsize: 118760
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 28276 0 0 0 89910 94 0 0 25 0 1 0 420867096 122134528 27361 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29818 27361 603 41 0 29777 0
vsize: 119272
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 28459 0 0 0 90910 95 0 0 25 0 1 0 420867096 122945536 27544 4294967295 134512640 134672761 3221224640 3221223808 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30016 27544 603 41 0 29975 0
vsize: 120064
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 28616 0 0 0 91910 95 0 0 25 0 1 0 420867096 123625472 27701 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30182 27701 603 41 0 30141 0
vsize: 120728
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 28805 0 0 0 92909 95 0 0 25 0 1 0 420867096 124284928 27890 4294967295 134512640 134672761 3221224640 3221223744 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30343 27890 603 41 0 30302 0
vsize: 121372
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 28975 0 0 0 93909 96 0 0 25 0 1 0 420867096 125087744 28060 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30539 28060 603 41 0 30498 0
vsize: 122156
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 29175 0 0 0 94909 96 0 0 25 0 1 0 420867096 125894656 28260 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30736 28260 603 41 0 30695 0
vsize: 122944
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 29327 0 0 0 95909 96 0 0 25 0 1 0 420867096 126431232 28412 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30867 28412 603 41 0 30826 0
vsize: 123468
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 29454 0 0 0 96909 97 0 0 25 0 1 0 420867096 126971904 28539 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30999 28539 603 41 0 30958 0
vsize: 123996
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 29583 0 0 0 97908 97 0 0 25 0 1 0 420867096 127496192 28668 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31127 28668 603 41 0 31086 0
vsize: 124508
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 29718 0 0 0 98908 98 0 0 25 0 1 0 420867096 128040960 28803 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31260 28803 603 41 0 31219 0
vsize: 125040
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 29877 0 0 0 99907 99 0 0 25 0 1 0 420867096 128716800 28962 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31425 28962 603 41 0 31384 0
vsize: 125700
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 30022 0 0 0 100907 99 0 0 25 0 1 0 420867096 129388544 29107 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31589 29107 603 41 0 31548 0
vsize: 126356
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 30180 0 0 0 101907 100 0 0 25 0 1 0 420867096 129921024 29265 4294967295 134512640 134672761 3221224640 3221223776 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31719 29265 603 41 0 31678 0
vsize: 126876
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 30336 0 0 0 102906 100 0 0 25 0 1 0 420867096 130592768 29421 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31883 29421 603 41 0 31842 0
vsize: 127532
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 30500 0 0 0 103906 101 0 0 25 0 1 0 420867096 131264512 29585 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32047 29585 603 41 0 32006 0
vsize: 128188
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 30699 0 0 0 104905 101 0 0 25 0 1 0 420867096 132063232 29784 4294967295 134512640 134672761 3221224640 3221223744 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32242 29784 603 41 0 32201 0
vsize: 128968
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 30756 0 0 0 105906 101 0 0 25 0 1 0 420867096 132329472 29841 4294967295 134512640 134672761 3221224640 3221223812 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32307 29841 603 41 0 32266 0
vsize: 129228
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 30843 0 0 0 106906 102 0 0 25 0 1 0 420867096 132599808 29928 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32373 29928 603 41 0 32332 0
vsize: 129492
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 31171 0 0 0 107905 102 0 0 25 0 1 0 420867096 133955584 30256 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32704 30256 603 41 0 32663 0
vsize: 130816
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 31528 0 0 0 108904 103 0 0 25 0 1 0 420867096 135458816 30613 4294967295 134512640 134672761 3221224640 3221223808 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33071 30613 603 41 0 33030 0
vsize: 132284
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 31855 0 0 0 109903 104 0 0 25 0 1 0 420867096 136826880 30940 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33405 30940 603 41 0 33364 0
vsize: 133620
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 32212 0 0 0 110902 105 0 0 25 0 1 0 420867096 138313728 31297 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33768 31297 603 41 0 33727 0
vsize: 135072
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 32579 0 0 0 111901 106 0 0 25 0 1 0 420867096 139812864 31664 4294967295 134512640 134672761 3221224640 3221223744 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34134 31664 603 41 0 34093 0
vsize: 136536
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 32994 0 0 0 112901 107 0 0 25 0 1 0 420867096 141447168 32079 4294967295 134512640 134672761 3221224640 3221223744 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34533 32079 603 41 0 34492 0
vsize: 138132
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 33329 0 0 0 113900 107 0 0 25 0 1 0 420867096 142798848 32414 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34863 32414 603 41 0 34822 0
vsize: 139452
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 33710 0 0 0 114900 108 0 0 25 0 1 0 420867096 144396288 32795 4294967295 134512640 134672761 3221224640 3221223808 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35253 32795 603 41 0 35212 0
vsize: 141012
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 34034 0 0 0 115899 109 0 0 25 0 1 0 420867096 145629184 33119 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35554 33119 603 41 0 35513 0
vsize: 142216
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 34388 0 0 0 116899 109 0 0 25 0 1 0 420867096 147128320 33473 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35920 33473 603 41 0 35879 0
vsize: 143680
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 34715 0 0 0 117898 110 0 0 25 0 1 0 420867096 148504576 33800 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36256 33800 603 41 0 36215 0
vsize: 145024
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 34733 0 0 0 118897 111 0 0 25 0 1 0 420867096 148504576 33818 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36256 33818 603 41 0 36215 0
vsize: 145024
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 543
Raw data (stat): 543 (minisat+) R 542 30854 30853 0 -1 0 34757 0 0 0 119897 111 0 0 25 0 1 0 420867096 148635648 33842 4294967295 134512640 134672761 3221224640 3221223812 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36288 33842 603 41 0 36247 0
vsize: 145152
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 543
Raw data (stat): 543 (minisat+) Z 542 30854 30853 0 -1 12 34760 0 0 0 119897 117 0 0 25 0 1 0 420867096 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.15
CPU user time (s): 1198.98
CPU system time (s): 1.17682
CPU usage (%): 100.004
Max. virtual memory (Kb): 145152
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####