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/aloul/FPGA_SAT05/normalized-fpga45_45_sat_pb.cnf.cr.opb
MD5SUM	da4cd22fd601b0d838453ba86be8f9aa
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	46
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	6.73997
Number of variables	3038
Total number of constraints	2160
Number of constraints which are clauses	2070
Number of constraints which are cardinality constraints (but not clauses)	90
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	22
Maximum length of a constraint	45
Trace number 4652

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-13 19:29:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3441 boxname=wulflinc13 idbench=57 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  da4cd22fd601b0d838453ba86be8f9aa  /oldhome/oroussel/tmp/wulflinc13/normalized-fpga45_45_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc13/normalized-fpga45_45_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc13/normalized-fpga45_45_sat_pb.cnf.cr.opb
IDLAUNCH: 3441
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        924732 kB
Buffers:         33888 kB
Cached:          56364 kB
SwapCached:        392 kB
Active:          48280 kB
Inactive:        45268 kB
HighTotal:      131008 kB
HighFree:        70672 kB
LowTotal:       903652 kB
LowFree:        854060 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10884 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:49:29 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 3441 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2160 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  89]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  88]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  87]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  86]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  85]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  84]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  83]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  82]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  81]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  80]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  79]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  78]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  77]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  76]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  75]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  74]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  73]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  72]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  71]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  70]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  69]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  68]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  67]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  66]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  65]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  64]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  63]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  62]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  61]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  60]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  59]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  58]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  57]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  56]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  55]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  54]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  53]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  52]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  51]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  50]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  49]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  48]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  47]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  46]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  45]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  44]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  43]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  42]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  41]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  40]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  39]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  38]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  37]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  36]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  35]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  34]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  33]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  32]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  31]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  30]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  29]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  28]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  27]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  26]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  25]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  24]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  23]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  22]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  21]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  20]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  19]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  18]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  17]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  16]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  15]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  14]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  13]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  12]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  11]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  10]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   9]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   8]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   7]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   6]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   5]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   4]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   3]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   2]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   1]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   0]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   36135   170842 |   12045       0        0     nan |  0.000 % |
c |       100 |   35826   169823 |   13249      13       44     3.4 |  8.724 % |
c |       250 |   35629   169094 |   14574     133      469     3.5 |  9.018 % |
c |       475 |   35398   168253 |   16031     314     1112     3.5 |  9.394 % |
c |       812 |   35284   167861 |   17635     631     2285     3.6 |  9.594 % |
c |      1318 |   34941   166638 |   19398    1100     4363     4.0 | 10.347 % |
c |      2077 |   33548   161573 |   21338    1705     7892     4.6 | 13.451 % |
c |      3217 |   31652   154873 |   23472    2580    12224     4.7 | 17.366 % |
c |      4925 |   23543   127454 |   25819    2904    19871     6.8 | 34.638 % |
c |      7487 |   21838   121691 |   28401    5178   606082   117.0 | 38.225 % |
c |     11334 |   21781   121506 |   31241    9016  2234201   247.8 | 38.354 % |
c |     17102 |   21667   121136 |   34365   14765  4098852   277.6 | 38.613 % |
c |     25753 |   21490   120537 |   37802   23390  9538602   407.8 | 38.989 % |
c |     38728 |   21467   120462 |   41582   36360 16241729   446.7 | 39.036 % |
c |     58189 |   20840   118273 |   45740   20901  8781836   420.2 | 40.306 % |
c |     87381 |   20782   118069 |   50314   50085 40947678   817.6 | 40.423 % |
#### 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.77 0.31 0.11 2/54 635
Raw data (stat): 635 (runsolver) R 634 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420260396 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99999 s]
Raw data (loadavg): 0.81 0.33 0.12 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 1198 0 0 0 994 3 0 0 25 0 1 0 420260396 6971392 1175 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1702 1175 603 41 0 1661 0
vsize: 6808
[startup+20.001 s]
Raw data (loadavg): 0.83 0.35 0.13 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 1202 0 0 0 1994 4 0 0 25 0 1 0 420260396 6971392 1179 4294967295 134512640 134672761 3221224528 3221223792 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1702 1179 603 41 0 1661 0
vsize: 6808
[startup+30.0016 s]
Raw data (loadavg): 0.86 0.37 0.13 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 1696 0 0 0 2993 5 0 0 25 0 1 0 420260396 8994816 1673 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2196 1673 603 41 0 2155 0
vsize: 8784
[startup+40.0008 s]
Raw data (loadavg): 0.88 0.39 0.14 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 3725 0 0 0 3988 9 0 0 25 0 1 0 420260396 17350656 3702 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4236 3702 603 41 0 4195 0
vsize: 16944
[startup+50.0019 s]
Raw data (loadavg): 0.90 0.41 0.15 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 5361 0 0 0 4984 13 0 0 25 0 1 0 420260396 23973888 5338 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5853 5338 603 41 0 5812 0
vsize: 23412
[startup+60.0016 s]
Raw data (loadavg): 0.91 0.43 0.16 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 6913 0 0 0 5980 18 0 0 25 0 1 0 420260396 30380032 6890 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7417 6890 603 41 0 7376 0
vsize: 29668
[startup+70.0018 s]
Raw data (loadavg): 0.93 0.45 0.17 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 9292 0 0 0 6975 22 0 0 25 0 1 0 420260396 40181760 9269 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9810 9269 603 41 0 9769 0
vsize: 39240
[startup+80.0029 s]
Raw data (loadavg): 0.94 0.47 0.18 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 10766 0 0 0 7973 25 0 0 25 0 1 0 420260396 46235648 10743 4294967295 134512640 134672761 3221224528 3221223704 134559668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11288 10743 603 41 0 11247 0
vsize: 45152
[startup+90.0025 s]
Raw data (loadavg): 0.95 0.48 0.19 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 12460 0 0 0 8969 29 0 0 25 0 1 0 420260396 53125120 12437 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12970 12437 603 41 0 12929 0
vsize: 51880
[startup+100.003 s]
Raw data (loadavg): 0.95 0.50 0.19 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 14299 0 0 0 9965 33 0 0 25 0 1 0 420260396 60674048 14276 4294967295 134512640 134672761 3221224528 3221223632 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14813 14276 603 41 0 14772 0
vsize: 59252
[startup+110.002 s]
Raw data (loadavg): 0.96 0.52 0.20 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 15635 0 0 0 10961 36 0 0 25 0 1 0 420260396 66080768 15612 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16133 15612 603 41 0 16092 0
vsize: 64532
[startup+120.003 s]
Raw data (loadavg): 0.97 0.53 0.21 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 16556 0 0 0 11959 39 0 0 25 0 1 0 420260396 69992448 16533 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17088 16533 603 41 0 17047 0
vsize: 68352
[startup+130.004 s]
Raw data (loadavg): 0.97 0.55 0.22 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 17520 0 0 0 12956 42 0 0 25 0 1 0 420260396 73912320 17497 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18045 17497 603 41 0 18004 0
vsize: 72180
[startup+140.004 s]
Raw data (loadavg): 0.98 0.56 0.23 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 18668 0 0 0 13953 45 0 0 25 0 1 0 420260396 78622720 18645 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19195 18645 603 41 0 19154 0
vsize: 76780
[startup+150.005 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 20146 0 0 0 14951 47 0 0 25 0 1 0 420260396 84697088 20123 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20678 20123 603 41 0 20637 0
vsize: 82712
[startup+160.005 s]
Raw data (loadavg): 0.98 0.59 0.24 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 21153 0 0 0 15948 50 0 0 25 0 1 0 420260396 88875008 21130 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21698 21130 603 41 0 21657 0
vsize: 86792
[startup+170.005 s]
Raw data (loadavg): 0.98 0.60 0.25 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 21937 0 0 0 16946 52 0 0 25 0 1 0 420260396 91975680 21914 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22455 21914 603 41 0 22414 0
vsize: 89820
[startup+180.005 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 22630 0 0 0 17944 54 0 0 25 0 1 0 420260396 94806016 22607 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23146 22607 603 41 0 23105 0
vsize: 92584
[startup+190.006 s]
Raw data (loadavg): 0.99 0.63 0.26 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 23261 0 0 0 18942 56 0 0 25 0 1 0 420260396 97525760 23238 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23810 23238 603 41 0 23769 0
vsize: 95240
[startup+200.006 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 23927 0 0 0 19940 58 0 0 25 0 1 0 420260396 100220928 23904 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24468 23904 603 41 0 24427 0
vsize: 97872
[startup+210.006 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24021 0 0 0 20940 58 0 0 25 0 1 0 420260396 100626432 23998 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24567 23998 603 41 0 24526 0
vsize: 98268
[startup+220.007 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24021 0 0 0 21939 59 0 0 25 0 1 0 420260396 100626432 23998 4294967295 134512640 134672761 3221224528 3221223632 134555093 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24567 23998 603 41 0 24526 0
vsize: 98268
[startup+230.007 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 22939 59 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+240.007 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 23939 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+250.008 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 24938 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+260.008 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 25938 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+270.008 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 26938 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+280.009 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 27938 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+290.008 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 28938 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+300.008 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 29938 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+310.008 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 30939 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+320.008 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 31939 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+330.008 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 32939 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+340.008 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 33939 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+350.008 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 34939 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+360.008 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 35940 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+370.009 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24022 0 0 0 36940 60 0 0 25 0 1 0 420260396 100626432 23999 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24567 23999 603 41 0 24526 0
vsize: 98268
[startup+380.009 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 24420 0 0 0 37939 62 0 0 25 0 1 0 420260396 102264832 24397 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24967 24397 603 41 0 24926 0
vsize: 99868
[startup+390.009 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 25322 0 0 0 38937 63 0 0 25 0 1 0 420260396 105943040 25299 4294967295 134512640 134672761 3221224528 3221223680 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25865 25299 603 41 0 25824 0
vsize: 103460
[startup+400.009 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 26257 0 0 0 39936 65 0 0 25 0 1 0 420260396 109752320 26234 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26795 26234 603 41 0 26754 0
vsize: 107180
[startup+410.009 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 27475 0 0 0 40934 67 0 0 25 0 1 0 420260396 114782208 27452 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28023 27452 603 41 0 27982 0
vsize: 112092
[startup+420.009 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 27959 0 0 0 41933 68 0 0 25 0 1 0 420260396 116682752 27936 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28487 27936 603 41 0 28446 0
vsize: 113948
[startup+430.01 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 28785 0 0 0 42931 70 0 0 25 0 1 0 420260396 120213504 28762 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29349 28762 603 41 0 29308 0
vsize: 117396
[startup+440.009 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 29471 0 0 0 43930 72 0 0 25 0 1 0 420260396 122945536 29448 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30016 29448 603 41 0 29975 0
vsize: 120064
[startup+450.009 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 30478 0 0 0 44928 73 0 0 25 0 1 0 420260396 127025152 30455 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31012 30455 603 41 0 30971 0
vsize: 124048
[startup+460.008 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 31163 0 0 0 45927 75 0 0 25 0 1 0 420260396 129900544 31140 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31714 31140 603 41 0 31673 0
vsize: 126856
[startup+470.009 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 31442 0 0 0 46927 75 0 0 25 0 1 0 420260396 131014656 31419 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31986 31419 603 41 0 31945 0
vsize: 127944
[startup+480.009 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 32059 0 0 0 47925 77 0 0 25 0 1 0 420260396 133586944 32036 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32614 32036 603 41 0 32573 0
vsize: 130456
[startup+490.008 s]
Raw data (loadavg): 0.99 0.85 0.46 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 32405 0 0 0 48925 78 0 0 25 0 1 0 420260396 135077888 32382 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32978 32382 603 41 0 32937 0
vsize: 131912
[startup+500.009 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 32786 0 0 0 49925 78 0 0 25 0 1 0 420260396 136581120 32763 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33345 32763 603 41 0 33304 0
vsize: 133380
[startup+510.009 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 33271 0 0 0 50924 79 0 0 25 0 1 0 420260396 138608640 33248 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33840 33248 603 41 0 33799 0
vsize: 135360
[startup+520.009 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 34159 0 0 0 51922 81 0 0 25 0 1 0 420260396 142270464 34136 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34734 34136 603 41 0 34693 0
vsize: 138936
[startup+530.01 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 35123 0 0 0 52919 84 0 0 25 0 1 0 420260396 146214912 35100 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35697 35100 603 41 0 35656 0
vsize: 142788
[startup+540.01 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 35395 0 0 0 53919 84 0 0 25 0 1 0 420260396 147300352 35372 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35962 35372 603 41 0 35921 0
vsize: 143848
[startup+550.01 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 35670 0 0 0 54919 85 0 0 25 0 1 0 420260396 148385792 35647 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36227 35647 603 41 0 36186 0
vsize: 144908
[startup+560.01 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 36019 0 0 0 55918 85 0 0 25 0 1 0 420260396 149884928 35996 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36593 35996 603 41 0 36552 0
vsize: 146372
[startup+570.011 s]
Raw data (loadavg): 0.99 0.88 0.50 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 36345 0 0 0 56917 87 0 0 25 0 1 0 420260396 151240704 36322 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36924 36322 603 41 0 36883 0
vsize: 147696
[startup+580.01 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 36751 0 0 0 57916 88 0 0 25 0 1 0 420260396 152862720 36728 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37320 36728 603 41 0 37279 0
vsize: 149280
[startup+590.01 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 37225 0 0 0 58916 89 0 0 25 0 1 0 420260396 154779648 37202 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37788 37202 603 41 0 37747 0
vsize: 151152
[startup+600.01 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 37480 0 0 0 59915 89 0 0 25 0 1 0 420260396 155877376 37457 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38056 37457 603 41 0 38015 0
vsize: 152224
[startup+610.01 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 37759 0 0 0 60915 90 0 0 25 0 1 0 420260396 156971008 37736 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38323 37736 603 41 0 38282 0
vsize: 153292
[startup+620.01 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 38135 0 0 0 61914 91 0 0 25 0 1 0 420260396 158474240 38112 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38690 38112 603 41 0 38649 0
vsize: 154760
[startup+630.01 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 38462 0 0 0 62914 91 0 0 25 0 1 0 420260396 159838208 38439 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39023 38439 603 41 0 38982 0
vsize: 156092
[startup+640.01 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 38760 0 0 0 63913 92 0 0 25 0 1 0 420260396 161067008 38737 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39323 38737 603 41 0 39282 0
vsize: 157292
[startup+650.01 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 39001 0 0 0 64914 92 0 0 25 0 1 0 420260396 162025472 38978 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39557 38978 603 41 0 39516 0
vsize: 158228
[startup+660.01 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 39249 0 0 0 65913 93 0 0 25 0 1 0 420260396 163102720 39226 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39820 39226 603 41 0 39779 0
vsize: 159280
[startup+670.011 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 39550 0 0 0 66913 93 0 0 25 0 1 0 420260396 164327424 39527 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40119 39527 603 41 0 40078 0
vsize: 160476
[startup+680.011 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 39889 0 0 0 67913 94 0 0 25 0 1 0 420260396 165683200 39866 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40450 39866 603 41 0 40409 0
vsize: 161800
[startup+690.011 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 40279 0 0 0 68912 95 0 0 25 0 1 0 420260396 167309312 40256 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40847 40256 603 41 0 40806 0
vsize: 163388
[startup+700.012 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 40714 0 0 0 69911 95 0 0 25 0 1 0 420260396 169078784 40691 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41279 40691 603 41 0 41238 0
vsize: 165116
[startup+710.013 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 41286 0 0 0 70910 97 0 0 25 0 1 0 420260396 171520000 41263 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41875 41263 603 41 0 41834 0
vsize: 167500
[startup+720.013 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 41856 0 0 0 71909 98 0 0 25 0 1 0 420260396 173867008 41833 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42448 41833 603 41 0 42407 0
vsize: 169792
[startup+730.013 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 42428 0 0 0 72908 99 0 0 25 0 1 0 420260396 176181248 42405 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43013 42405 603 41 0 42972 0
vsize: 172052
[startup+740.014 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 42999 0 0 0 73907 101 0 0 25 0 1 0 420260396 178503680 42976 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43580 42976 603 41 0 43539 0
vsize: 174320
[startup+750.014 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 43516 0 0 0 74905 102 0 0 25 0 1 0 420260396 180555776 43493 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44081 43493 603 41 0 44040 0
vsize: 176324
[startup+760.014 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 43658 0 0 0 75904 103 0 0 25 0 1 0 420260396 181264384 43635 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44254 43635 603 41 0 44213 0
vsize: 177016
[startup+770.015 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 43688 0 0 0 76904 103 0 0 25 0 1 0 420260396 181399552 43665 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44287 43665 603 41 0 44246 0
vsize: 177148
[startup+780.014 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 43697 0 0 0 77905 103 0 0 25 0 1 0 420260396 181399552 43674 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44287 43674 603 41 0 44246 0
vsize: 177148
[startup+790.014 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 46002 0 0 0 78899 109 0 0 25 0 1 0 420260396 190742528 45979 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46568 45979 603 41 0 46527 0
vsize: 186272
[startup+800.014 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 47771 0 0 0 79896 112 0 0 25 0 1 0 420260396 198062080 47748 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48355 47748 603 41 0 48314 0
vsize: 193420
[startup+810.014 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49082 0 0 0 80893 115 0 0 25 0 1 0 420260396 203362304 49059 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49649 49059 603 41 0 49608 0
vsize: 198596
[startup+820.015 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 81892 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+830.015 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 82892 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+840.015 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 83892 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+850.015 s]
Raw data (loadavg): 0.99 0.95 0.61 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 84892 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+860.015 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 85892 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+870.016 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 86893 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+880.016 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 87893 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+890.015 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 88893 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+900.016 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 89893 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+910.016 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 90893 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223632 134554912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+920.016 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 91894 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223632 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+930.016 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 92894 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+940.016 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 93894 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+950.016 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 94894 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+960.016 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 95894 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+970.016 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 96894 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+980.016 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 97895 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+990.016 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 98895 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 99895 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 100895 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 101895 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 102896 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 103896 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 104896 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 105896 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 106896 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 107897 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223676 134559754 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 108897 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 109897 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 110897 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 111897 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 112898 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.71 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 113898 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.71 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 114898 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.71 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 115898 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.71 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 116899 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.72 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 117899 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.72 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 118899 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.72 2/54 635
Raw data (stat): 635 (minisat+) R 634 30701 30700 0 -1 0 49809 0 0 0 119899 117 0 0 25 0 1 0 420260396 206348288 49786 4294967295 134512640 134672761 3221224528 3221223712 134559566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50378 49786 603 41 0 50337 0
vsize: 201512
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.72 1/54 635
Raw data (stat): 635 (minisat+) Z 634 30701 30700 0 -1 12 49811 0 0 0 119899 126 0 0 25 0 1 0 420260396 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.27
CPU user time (s): 1199
CPU system time (s): 1.26881
CPU usage (%): 100.012
Max. virtual memory (Kb): 201512
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####