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-chnl30_40_pb.cnf.cr.opb
MD5SUM	6a0000bd3257094a387dbf208b4df8cf
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
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	41
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.073987
Number of variables	2400
Total number of constraints	140
Number of constraints which are clauses	80
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	30
Maximum length of a constraint	40
Trace number 5712

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-14 01:38:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4149 boxname=wulflinc25 idbench=13 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6a0000bd3257094a387dbf208b4df8cf  /oldhome/oroussel/tmp/wulflinc25/normalized-chnl30_40_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc25/normalized-chnl30_40_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc25/normalized-chnl30_40_pb.cnf.cr.opb
IDLAUNCH: 4149
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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	: 3
cpu MHz		: 451.220
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:        894152 kB
Buffers:         34512 kB
Cached:          71396 kB
SwapCached:         36 kB
Active:          48800 kB
Inactive:        60024 kB
HighTotal:      131008 kB
HighFree:        55860 kB
LowTotal:       903652 kB
LowFree:        838292 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26028 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:58:09 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 4149 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   77
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:   77
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   5]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   3]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   1]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11540    32220 |    3846       0        0     nan |  0.000 % |
c |       105 |   11540    32220 |    4230     105    11655   111.0 |  0.855 % |
c |       256 |   11540    32220 |    4653     256    29323   114.5 |  0.855 % |
c |       482 |   11540    32220 |    5119     482    59867   124.2 |  0.855 % |
c |       819 |   11540    32220 |    5630     819   119821   146.3 |  0.855 % |
c |      1326 |   11540    32220 |    6194    1326   200884   151.5 |  0.855 % |
c |      2085 |   11540    32220 |    6813    2085   338592   162.4 |  0.855 % |
c |      3224 |   11540    32220 |    7494    3224   573967   178.0 |  0.855 % |
c |      4933 |   11540    32220 |    8244    4933  1020753   206.9 |  0.855 % |
c |      7495 |   11540    32220 |    9068    7495  1644283   219.4 |  0.855 % |
c |     11343 |   11540    32220 |    9975   11343  2620703   231.0 |  0.855 % |
c |     17110 |   11540    32220 |   10973   11439  2978380   260.4 |  0.855 % |
c |     25760 |   11540    32220 |   12070    7811  2675183   342.5 |  0.855 % |
c |     38735 |   11540    32220 |   13277   13643  5459721   400.2 |  0.855 % |
c |     58196 |   11540    32220 |   14605   10980  5555897   506.0 |  0.855 % |
c |     87389 |   11540    32220 |   16065   15223  7944453   521.9 |  0.855 % |
c |    131185 |   11540    32220 |   17672   13326  6647495   498.8 |  0.855 % |
c |    196871 |   11540    32220 |   19439   19364  9746152   503.3 |  0.855 % |
c |    295399 |   11540    32220 |   21383   18529  5847392   315.6 |  0.855 % |
#### 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.91 0.98 0.91 2/54 32629
Raw data (stat): 32629 (runsolver) R 32628 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480700071 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.99951 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 2950 0 0 0 990 8 0 0 25 0 1 0 480700071 13729792 2928 4294967295 134512640 134672761 3221224528 3221223712 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3352 2928 603 41 0 3311 0
vsize: 13408
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 3651 0 0 0 1988 10 0 0 25 0 1 0 480700071 16560128 3629 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4043 3629 603 41 0 4002 0
vsize: 16172
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 4082 0 0 0 2986 11 0 0 25 0 1 0 480700071 18313216 4060 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4471 4060 603 41 0 4430 0
vsize: 17884
[startup+40.0004 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 5145 0 0 0 3983 14 0 0 25 0 1 0 480700071 22753280 5123 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5555 5123 603 41 0 5514 0
vsize: 22220
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 5405 0 0 0 4982 15 0 0 25 0 1 0 480700071 23834624 5383 4294967295 134512640 134672761 3221224528 3221223696 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5819 5383 603 41 0 5778 0
vsize: 23276
[startup+60.0008 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 6167 0 0 0 5981 16 0 0 25 0 1 0 480700071 26943488 6145 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6578 6145 603 41 0 6537 0
vsize: 26312
[startup+70.0011 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 6167 0 0 0 6980 16 0 0 25 0 1 0 480700071 26943488 6145 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6578 6145 603 41 0 6537 0
vsize: 26312
[startup+80.0013 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 6820 0 0 0 7978 18 0 0 25 0 1 0 480700071 29511680 6798 4294967295 134512640 134672761 3221224528 3221223632 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7205 6798 603 41 0 7164 0
vsize: 28820
[startup+90.0008 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 6821 0 0 0 8978 18 0 0 25 0 1 0 480700071 29511680 6799 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7205 6799 603 41 0 7164 0
vsize: 28820
[startup+100.001 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 7789 0 0 0 9974 21 0 0 25 0 1 0 480700071 33579008 7767 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8198 7767 603 41 0 8157 0
vsize: 32792
[startup+110.001 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 8077 0 0 0 10974 22 0 0 25 0 1 0 480700071 34799616 8055 4294967295 134512640 134672761 3221224528 3221223712 134559607 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8496 8055 603 41 0 8455 0
vsize: 33984
[startup+120.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 8077 0 0 0 11974 22 0 0 25 0 1 0 480700071 34799616 8055 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8496 8055 603 41 0 8455 0
vsize: 33984
[startup+130.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 8201 0 0 0 12973 22 0 0 25 0 1 0 480700071 35205120 8179 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8595 8179 603 41 0 8554 0
vsize: 34380
[startup+140.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 8205 0 0 0 13973 23 0 0 25 0 1 0 480700071 35340288 8183 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8628 8183 603 41 0 8587 0
vsize: 34512
[startup+150.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 8205 0 0 0 14974 23 0 0 25 0 1 0 480700071 35340288 8183 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8628 8183 603 41 0 8587 0
vsize: 34512
[startup+160.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 9373 0 0 0 15971 25 0 0 25 0 1 0 480700071 40071168 9351 4294967295 134512640 134672761 3221224528 3221223712 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9351 603 41 0 9742 0
vsize: 39132
[startup+170.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 9933 0 0 0 16970 26 0 0 25 0 1 0 480700071 42385408 9911 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10348 9911 603 41 0 10307 0
vsize: 41392
[startup+180.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 9933 0 0 0 17970 26 0 0 25 0 1 0 480700071 42385408 9911 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10348 9911 603 41 0 10307 0
vsize: 41392
[startup+190.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 9933 0 0 0 18970 26 0 0 25 0 1 0 480700071 42385408 9911 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10348 9911 603 41 0 10307 0
vsize: 41392
[startup+200.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 9933 0 0 0 19971 26 0 0 25 0 1 0 480700071 42385408 9911 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10348 9911 603 41 0 10307 0
vsize: 41392
[startup+210.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 10330 0 0 0 20970 27 0 0 25 0 1 0 480700071 44003328 10308 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10743 10308 603 41 0 10702 0
vsize: 42972
[startup+220.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 10330 0 0 0 21970 27 0 0 25 0 1 0 480700071 44003328 10308 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10743 10308 603 41 0 10702 0
vsize: 42972
[startup+230.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 10330 0 0 0 22970 27 0 0 25 0 1 0 480700071 44003328 10308 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10743 10308 603 41 0 10702 0
vsize: 42972
[startup+240.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 10330 0 0 0 23970 28 0 0 25 0 1 0 480700071 44003328 10308 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10743 10308 603 41 0 10702 0
vsize: 42972
[startup+250.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 10531 0 0 0 24970 28 0 0 25 0 1 0 480700071 44810240 10509 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10940 10509 603 41 0 10899 0
vsize: 43760
[startup+260.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 10615 0 0 0 25970 28 0 0 25 0 1 0 480700071 45211648 10593 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11038 10593 603 41 0 10997 0
vsize: 44152
[startup+270 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 10615 0 0 0 26970 28 0 0 25 0 1 0 480700071 45211648 10593 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11038 10593 603 41 0 10997 0
vsize: 44152
[startup+280.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 10615 0 0 0 27970 28 0 0 25 0 1 0 480700071 45211648 10593 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11038 10593 603 41 0 10997 0
vsize: 44152
[startup+290.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 10615 0 0 0 28971 28 0 0 25 0 1 0 480700071 45211648 10593 4294967295 134512640 134672761 3221224528 3221223664 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11038 10593 603 41 0 10997 0
vsize: 44152
[startup+300.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 10644 0 0 0 29970 28 0 0 25 0 1 0 480700071 45346816 10622 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11071 10622 603 41 0 11030 0
vsize: 44284
[startup+310.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11237 0 0 0 30969 30 0 0 25 0 1 0 480700071 47775744 11215 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11215 603 41 0 11623 0
vsize: 46656
[startup+320.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11237 0 0 0 31969 30 0 0 25 0 1 0 480700071 47775744 11215 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11215 603 41 0 11623 0
vsize: 46656
[startup+330.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11237 0 0 0 32969 30 0 0 25 0 1 0 480700071 47775744 11215 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11215 603 41 0 11623 0
vsize: 46656
[startup+340.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11237 0 0 0 33969 30 0 0 25 0 1 0 480700071 47775744 11215 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11215 603 41 0 11623 0
vsize: 46656
[startup+350.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11237 0 0 0 34969 30 0 0 25 0 1 0 480700071 47775744 11215 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11215 603 41 0 11623 0
vsize: 46656
[startup+360.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11237 0 0 0 35970 30 0 0 25 0 1 0 480700071 47775744 11215 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11215 603 41 0 11623 0
vsize: 46656
[startup+370.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11237 0 0 0 36970 30 0 0 25 0 1 0 480700071 47775744 11215 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11215 603 41 0 11623 0
vsize: 46656
[startup+380.001 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 37970 30 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+390.001 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 38970 30 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223712 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+400.001 s]
Raw data (loadavg): 1.10 1.01 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 39970 30 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+410.001 s]
Raw data (loadavg): 1.09 1.01 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 40970 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+420.002 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 41970 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+430.001 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 42970 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+440 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 43970 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+450 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 44970 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+460.001 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 45970 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+470.002 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 46971 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+480.001 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 47971 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+490.001 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 48971 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+500.001 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 49971 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+510.001 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 50971 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223728 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+520.002 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11238 0 0 0 51971 31 0 0 25 0 1 0 480700071 47775744 11216 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+530.002 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11510 0 0 0 52970 33 0 0 25 0 1 0 480700071 48857088 11488 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11928 11488 603 41 0 11887 0
vsize: 47712
[startup+540.002 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11817 0 0 0 53970 33 0 0 25 0 1 0 480700071 50208768 11795 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11795 603 41 0 12217 0
vsize: 49032
[startup+550.002 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11817 0 0 0 54970 33 0 0 25 0 1 0 480700071 50208768 11795 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11795 603 41 0 12217 0
vsize: 49032
[startup+560.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11817 0 0 0 55970 33 0 0 25 0 1 0 480700071 50208768 11795 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11795 603 41 0 12217 0
vsize: 49032
[startup+570.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 56969 33 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223696 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+580.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 57970 33 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223632 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+590.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 58970 33 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+600.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 59970 33 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+610.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 60970 34 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223632 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+620.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 61970 34 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+630.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 62970 34 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+640.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 63970 34 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+650.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 64971 34 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+660.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 65971 34 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+670.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 66971 34 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+680.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 67971 34 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+690.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 68971 34 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+700.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11819 0 0 0 69971 34 0 0 25 0 1 0 480700071 50208768 11797 4294967295 134512640 134672761 3221224528 3221223632 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11797 603 41 0 12217 0
vsize: 49032
[startup+710.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11933 0 0 0 70971 34 0 0 25 0 1 0 480700071 50614272 11911 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11911 603 41 0 12316 0
vsize: 49428
[startup+720.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11933 0 0 0 71971 34 0 0 25 0 1 0 480700071 50614272 11911 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11911 603 41 0 12316 0
vsize: 49428
[startup+730.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11933 0 0 0 72971 34 0 0 25 0 1 0 480700071 50614272 11911 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11911 603 41 0 12316 0
vsize: 49428
[startup+740.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11933 0 0 0 73971 35 0 0 25 0 1 0 480700071 50614272 11911 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11911 603 41 0 12316 0
vsize: 49428
[startup+750.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 11938 0 0 0 74972 35 0 0 25 0 1 0 480700071 50614272 11916 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11916 603 41 0 12316 0
vsize: 49428
[startup+760.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 12661 0 0 0 75970 36 0 0 25 0 1 0 480700071 53587968 12639 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13083 12639 603 41 0 13042 0
vsize: 52332
[startup+770.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 12661 0 0 0 76970 36 0 0 25 0 1 0 480700071 53587968 12639 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13083 12639 603 41 0 13042 0
vsize: 52332
[startup+780.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 12661 0 0 0 77970 36 0 0 25 0 1 0 480700071 53587968 12639 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13083 12639 603 41 0 13042 0
vsize: 52332
[startup+790.001 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 12661 0 0 0 78970 37 0 0 25 0 1 0 480700071 53587968 12639 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13083 12639 603 41 0 13042 0
vsize: 52332
[startup+800.001 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 12728 0 0 0 79970 37 0 0 25 0 1 0 480700071 53993472 12706 4294967295 134512640 134672761 3221224528 3221223484 1075349707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13182 12706 603 41 0 13141 0
vsize: 52728
[startup+810.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 12728 0 0 0 80970 37 0 0 25 0 1 0 480700071 53993472 12706 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13182 12706 603 41 0 13141 0
vsize: 52728
[startup+820.002 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 12728 0 0 0 81970 37 0 0 25 0 1 0 480700071 53993472 12706 4294967295 134512640 134672761 3221224528 3221223680 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13182 12706 603 41 0 13141 0
vsize: 52728
[startup+830.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 12728 0 0 0 82970 37 0 0 25 0 1 0 480700071 53993472 12706 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13182 12706 603 41 0 13141 0
vsize: 52728
[startup+840.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13178 0 0 0 83969 39 0 0 25 0 1 0 480700071 55746560 13156 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13610 13156 603 41 0 13569 0
vsize: 54440
[startup+850.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13611 0 0 0 84967 40 0 0 25 0 1 0 480700071 57491456 13589 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13589 603 41 0 13995 0
vsize: 56144
[startup+860.003 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13611 0 0 0 85967 40 0 0 25 0 1 0 480700071 57491456 13589 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13589 603 41 0 13995 0
vsize: 56144
[startup+870.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 86968 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+880.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 87968 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+890.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 88968 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+900.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 89968 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+910.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 90968 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+920.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 91968 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+930.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 92969 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+940.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 93969 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+950.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 94969 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+960.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 95969 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+970.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 96969 40 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+980.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 97970 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+990.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 98970 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 99970 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 100970 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223632 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 101970 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 102970 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 103970 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223632 134554912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 104971 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 105971 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 106971 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 107971 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 108971 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 109971 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 110971 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 111971 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 112971 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223632 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 113972 41 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 114972 42 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 115972 42 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 116972 42 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 117972 42 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223728 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 118972 42 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32629
Raw data (stat): 32629 (minisat+) R 32628 28099 28098 0 -1 0 13612 0 0 0 119972 42 0 0 25 0 1 0 480700071 57491456 13590 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 32629
Raw data (stat): 32629 (minisat+) Z 32628 28099 28098 0 -1 12 13614 0 0 0 119972 44 0 0 25 0 1 0 480700071 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.04
CPU time (s): 1200.18
CPU user time (s): 1199.73
CPU system time (s): 0.447931
CPU usage (%): 100.012
Max. virtual memory (Kb): 56144
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####