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-fpga40_39_sat_pb.cnf.cr.opb
MD5SUM	b0b9c98556325dcf5a5811fc2d17a816
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	41
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	4.5833
Number of variables	2340
Total number of constraints	1678
Number of constraints which are clauses	1599
Number of constraints which are cardinality constraints (but not clauses)	79
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	20
Maximum length of a constraint	40
Trace number 5775

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-14 01:44:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4189 boxname=wulflinc11 idbench=53 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b0b9c98556325dcf5a5811fc2d17a816  /oldhome/oroussel/tmp/wulflinc11/normalized-fpga40_39_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc11/normalized-fpga40_39_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc11/normalized-fpga40_39_sat_pb.cnf.cr.opb
IDLAUNCH: 4189
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        909748 kB
Buffers:         35920 kB
Cached:          64412 kB
SwapCached:       4932 kB
Active:          56880 kB
Inactive:        51288 kB
HighTotal:      131008 kB
HighFree:        62748 kB
LowTotal:       903652 kB
LowFree:        847000 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11160 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:02:20 (client local time) WITH STATUS 30 IN 1070.86 SECONDS
stats: 4189 7 1070.86 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1678 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  78]---> BDD-cost:   75
c ---[  77]---> BDD-cost:   75
c ---[  76]---> BDD-cost:   75
c ---[  75]---> BDD-cost:   75
c ---[  74]---> BDD-cost:   75
c ---[  73]---> BDD-cost:   75
c ---[  72]---> BDD-cost:   75
c ---[  71]---> BDD-cost:   75
c ---[  70]---> BDD-cost:   75
c ---[  69]---> BDD-cost:   75
c ---[  68]---> BDD-cost:   75
c ---[  67]---> BDD-cost:   75
c ---[  66]---> BDD-cost:   75
c ---[  65]---> BDD-cost:   75
c ---[  64]---> BDD-cost:   75
c ---[  63]---> BDD-cost:   75
c ---[  62]---> BDD-cost:   75
c ---[  61]---> BDD-cost:   75
c ---[  60]---> BDD-cost:   75
c ---[  59]---> BDD-cost:   75
c ---[  58]---> BDD-cost:   75
c ---[  57]---> BDD-cost:   75
c ---[  56]---> BDD-cost:   75
c ---[  55]---> BDD-cost:   75
c ---[  54]---> BDD-cost:   75
c ---[  53]---> BDD-cost:   75
c ---[  52]---> BDD-cost:   75
c ---[  51]---> BDD-cost:   75
c ---[  50]---> BDD-cost:   75
c ---[  49]---> BDD-cost:   75
c ---[  48]---> BDD-cost:   75
c ---[  47]---> BDD-cost:   75
c ---[  46]---> BDD-cost:   75
c ---[  45]---> BDD-cost:   75
c ---[  44]---> BDD-cost:   75
c ---[  43]---> BDD-cost:   75
c ---[  42]---> BDD-cost:   75
c ---[  41]---> BDD-cost:   75
c ---[  40]---> BDD-cost:   75
c ---[  39]---> BDD-cost:   75
c ---[  38]---> BDD-cost:   37
c ---[  37]---> BDD-cost:   37
c ---[  36]---> BDD-cost:   37
c ---[  35]---> BDD-cost:   37
c ---[  34]---> BDD-cost:   37
c ---[  33]---> BDD-cost:   37
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   37
c ---[  30]---> BDD-cost:   37
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12588    62143 |    4196       0        0     nan |  0.000 % |
c |       111 |   12588    62143 |    4615     111    33739   304.0 |  1.165 % |
c |       263 |   12588    62143 |    5077     263    74695   284.0 |  1.165 % |
c |       488 |   12588    62143 |    5584     488   117851   241.5 |  1.165 % |
c |       825 |   12588    62143 |    6143     825   182982   221.8 |  1.165 % |
c |      1332 |   12588    62143 |    6757    1332   313395   235.3 |  1.165 % |
c |      2093 |   12588    62143 |    7433    2093   552175   263.8 |  1.165 % |
c |      3234 |   12588    62143 |    8176    3234   826036   255.4 |  1.165 % |
c |      4942 |   12588    62143 |    8994    4942  1185368   239.9 |  1.165 % |
c |      7505 |   12588    62143 |    9893    7505  1634136   217.7 |  1.165 % |
c |     11350 |   12588    62143 |   10883   11350  3068153   270.3 |  1.165 % |
c |     17118 |   12588    62143 |   11971   11443  3648096   318.8 |  1.165 % |
c |     25767 |   12588    62143 |   13168   12050  3959642   328.6 |  1.165 % |
c |     38744 |   12588    62143 |   14485   16496  5481733   332.3 |  1.165 % |
c |     58205 |   12588    62143 |   15934   17828  2135865   119.8 |  1.165 % |
c |     87397 |   12588    62143 |   17527   17964  6583862   366.5 |  1.165 % |
c |    131186 |   12588    62143 |   19280   20533  8190543   398.9 |  1.165 % |
c |    196874 |   12588    62143 |   21208   16916  7196074   425.4 |  1.165 % |
c |    295401 |   12588    62143 |   23329   21506  5077493   236.1 |  1.165 % |
c ==============================================================================
c [1mSATISFIABLE: No goal function specified.[0m
s SATISFIABLE
v
c _______________________________________________________________________________
c 
c restarts              : 19
c conflicts             : 314711         (294 /sec)
c decisions             : 438316         (410 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1070.31 s
c _______________________________________________________________________________
#### 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.84 0.94 0.90 2/54 6276
Raw data (stat): 6276 (runsolver) R 6275 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422505086 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 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+10.0002 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 3067 0 0 0 990 7 0 0 25 0 1 0 422505086 14159872 3045 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3457 3045 603 41 0 3416 0
vsize: 13828
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 4164 0 0 0 1987 10 0 0 25 0 1 0 422505086 18604032 4142 4294967295 134512640 134672761 3221224528 3221223632 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4542 4142 603 41 0 4501 0
vsize: 18168
[startup+30.0022 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 5025 0 0 0 2984 13 0 0 25 0 1 0 422505086 22110208 5003 4294967295 134512640 134672761 3221224528 3221223632 134560128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 5003 603 41 0 5357 0
vsize: 21592
[startup+40.0026 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 6255 0 0 0 3979 16 0 0 25 0 1 0 422505086 27238400 6233 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6650 6233 603 41 0 6609 0
vsize: 26600
[startup+50.0038 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 6370 0 0 0 4979 17 0 0 25 0 1 0 422505086 27643904 6348 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6749 6348 603 41 0 6708 0
vsize: 26996
[startup+60.0035 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 6638 0 0 0 5977 18 0 0 25 0 1 0 422505086 28835840 6616 4294967295 134512640 134672761 3221224528 3221223712 134559038 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7040 6616 603 41 0 6999 0
vsize: 28160
[startup+70.0039 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 6863 0 0 0 6976 20 0 0 25 0 1 0 422505086 29782016 6841 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7271 6841 603 41 0 7230 0
vsize: 29084
[startup+80.0054 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 6863 0 0 0 7976 20 0 0 25 0 1 0 422505086 29782016 6841 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7271 6841 603 41 0 7230 0
vsize: 29084
[startup+90.0059 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 6864 0 0 0 8975 20 0 0 25 0 1 0 422505086 29782016 6842 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7271 6842 603 41 0 7230 0
vsize: 29084
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 7010 0 0 0 9975 20 0 0 25 0 1 0 422505086 30322688 6988 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6988 603 41 0 7362 0
vsize: 29612
[startup+110.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 7013 0 0 0 10975 20 0 0 25 0 1 0 422505086 30322688 6991 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6991 603 41 0 7362 0
vsize: 29612
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 7013 0 0 0 11974 21 0 0 25 0 1 0 422505086 30322688 6991 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6991 603 41 0 7362 0
vsize: 29612
[startup+130.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 7013 0 0 0 12974 21 0 0 25 0 1 0 422505086 30322688 6991 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6991 603 41 0 7362 0
vsize: 29612
[startup+140.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 7013 0 0 0 13974 22 0 0 25 0 1 0 422505086 30322688 6991 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6991 603 41 0 7362 0
vsize: 29612
[startup+150.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 7473 0 0 0 14972 23 0 0 25 0 1 0 422505086 32227328 7451 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7868 7451 603 41 0 7827 0
vsize: 31472
[startup+160.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 7959 0 0 0 15970 25 0 0 25 0 1 0 422505086 34242560 7937 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8360 7937 603 41 0 8319 0
vsize: 33440
[startup+170.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 8036 0 0 0 16970 25 0 0 25 0 1 0 422505086 34672640 8014 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8465 8014 603 41 0 8424 0
vsize: 33860
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 8713 0 0 0 17968 27 0 0 25 0 1 0 422505086 37453824 8691 4294967295 134512640 134672761 3221224528 3221223712 134558903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9144 8691 603 41 0 9103 0
vsize: 36576
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10135 0 0 0 18963 31 0 0 25 0 1 0 422505086 43307008 10113 4294967295 134512640 134672761 3221224528 3221223088 134565745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10573 10113 603 41 0 10532 0
vsize: 42292
[startup+200.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10135 0 0 0 19963 31 0 0 25 0 1 0 422505086 43307008 10113 4294967295 134512640 134672761 3221224528 3221223696 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10573 10113 603 41 0 10532 0
vsize: 42292
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10135 0 0 0 20963 32 0 0 25 0 1 0 422505086 43307008 10113 4294967295 134512640 134672761 3221224528 3221223716 1075346949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10573 10113 603 41 0 10532 0
vsize: 42292
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10135 0 0 0 21962 32 0 0 25 0 1 0 422505086 43307008 10113 4294967295 134512640 134672761 3221224528 3221223712 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10573 10113 603 41 0 10532 0
vsize: 42292
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10135 0 0 0 22962 33 0 0 25 0 1 0 422505086 43307008 10113 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10573 10113 603 41 0 10532 0
vsize: 42292
[startup+240.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10135 0 0 0 23962 33 0 0 25 0 1 0 422505086 43307008 10113 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10573 10113 603 41 0 10532 0
vsize: 42292
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10136 0 0 0 24962 33 0 0 25 0 1 0 422505086 43307008 10114 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10573 10114 603 41 0 10532 0
vsize: 42292
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10445 0 0 0 25962 33 0 0 25 0 1 0 422505086 44539904 10423 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10874 10423 603 41 0 10833 0
vsize: 43496
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10445 0 0 0 26961 34 0 0 25 0 1 0 422505086 44539904 10423 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10874 10423 603 41 0 10833 0
vsize: 43496
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10445 0 0 0 27961 34 0 0 25 0 1 0 422505086 44539904 10423 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10874 10423 603 41 0 10833 0
vsize: 43496
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10445 0 0 0 28960 35 0 0 25 0 1 0 422505086 44539904 10423 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10874 10423 603 41 0 10833 0
vsize: 43496
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10445 0 0 0 29960 35 0 0 25 0 1 0 422505086 44539904 10423 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10874 10423 603 41 0 10833 0
vsize: 43496
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10548 0 0 0 30960 35 0 0 25 0 1 0 422505086 45076480 10526 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11005 10526 603 41 0 10964 0
vsize: 44020
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10896 0 0 0 31958 37 0 0 25 0 1 0 422505086 46428160 10874 4294967295 134512640 134672761 3221224528 3221223528 1075349698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10874 603 41 0 11294 0
vsize: 45340
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10896 0 0 0 32958 37 0 0 25 0 1 0 422505086 46428160 10874 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10874 603 41 0 11294 0
vsize: 45340
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10896 0 0 0 33958 37 0 0 25 0 1 0 422505086 46428160 10874 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10874 603 41 0 11294 0
vsize: 45340
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10896 0 0 0 34958 37 0 0 25 0 1 0 422505086 46428160 10874 4294967295 134512640 134672761 3221224528 3221223696 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10874 603 41 0 11294 0
vsize: 45340
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10896 0 0 0 35958 38 0 0 25 0 1 0 422505086 46428160 10874 4294967295 134512640 134672761 3221224528 3221223632 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10874 603 41 0 11294 0
vsize: 45340
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 10896 0 0 0 36957 38 0 0 25 0 1 0 422505086 46428160 10874 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10874 603 41 0 11294 0
vsize: 45340
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 11059 0 0 0 37957 38 0 0 25 0 1 0 422505086 47104000 11037 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11500 11037 603 41 0 11459 0
vsize: 46000
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 11083 0 0 0 38957 39 0 0 25 0 1 0 422505086 47251456 11061 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11536 11061 603 41 0 11495 0
vsize: 46144
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 11095 0 0 0 39957 39 0 0 25 0 1 0 422505086 47251456 11073 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11536 11073 603 41 0 11495 0
vsize: 46144
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 11095 0 0 0 40957 39 0 0 25 0 1 0 422505086 47251456 11073 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11073 603 41 0 11495 0
vsize: 46144
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 11095 0 0 0 41957 39 0 0 25 0 1 0 422505086 47251456 11073 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11073 603 41 0 11495 0
vsize: 46144
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 11095 0 0 0 42957 39 0 0 25 0 1 0 422505086 47251456 11073 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11536 11073 603 41 0 11495 0
vsize: 46144
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 11095 0 0 0 43956 39 0 0 25 0 1 0 422505086 47251456 11073 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11536 11073 603 41 0 11495 0
vsize: 46144
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 11095 0 0 0 44956 40 0 0 25 0 1 0 422505086 47251456 11073 4294967295 134512640 134672761 3221224528 3221223712 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11536 11073 603 41 0 11495 0
vsize: 46144
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 11955 0 0 0 45952 43 0 0 25 0 1 0 422505086 50876416 11933 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12421 11933 603 41 0 12380 0
vsize: 49684
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 12702 0 0 0 46950 46 0 0 25 0 1 0 422505086 53981184 12680 4294967295 134512640 134672761 3221224528 3221223632 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13179 12680 603 41 0 13138 0
vsize: 52716
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 12703 0 0 0 47949 46 0 0 25 0 1 0 422505086 53981184 12681 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13179 12681 603 41 0 13138 0
vsize: 52716
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 12704 0 0 0 48949 47 0 0 25 0 1 0 422505086 53981184 12682 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13179 12682 603 41 0 13138 0
vsize: 52716
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 12704 0 0 0 49949 47 0 0 25 0 1 0 422505086 53981184 12682 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13179 12682 603 41 0 13138 0
vsize: 52716
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 12706 0 0 0 50949 47 0 0 25 0 1 0 422505086 53981184 12684 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13179 12684 603 41 0 13138 0
vsize: 52716
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 12706 0 0 0 51949 47 0 0 25 0 1 0 422505086 53981184 12684 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13179 12684 603 41 0 13138 0
vsize: 52716
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13289 0 0 0 52949 47 0 0 25 0 1 0 422505086 56283136 13267 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13741 13267 603 41 0 13700 0
vsize: 54964
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13613 0 0 0 53948 48 0 0 25 0 1 0 422505086 57626624 13591 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14069 13591 603 41 0 14028 0
vsize: 56276
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13613 0 0 0 54948 48 0 0 25 0 1 0 422505086 57626624 13591 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14069 13591 603 41 0 14028 0
vsize: 56276
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13613 0 0 0 55949 48 0 0 25 0 1 0 422505086 57626624 13591 4294967295 134512640 134672761 3221224528 3221223696 134559126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14069 13591 603 41 0 14028 0
vsize: 56276
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13613 0 0 0 56949 48 0 0 25 0 1 0 422505086 57626624 13591 4294967295 134512640 134672761 3221224528 3221223632 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14069 13591 603 41 0 14028 0
vsize: 56276
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13615 0 0 0 57949 48 0 0 25 0 1 0 422505086 57626624 13593 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14069 13593 603 41 0 14028 0
vsize: 56276
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13617 0 0 0 58949 48 0 0 25 0 1 0 422505086 57626624 13595 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14069 13595 603 41 0 14028 0
vsize: 56276
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13724 0 0 0 59949 49 0 0 25 0 1 0 422505086 58167296 13702 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14201 13702 603 41 0 14160 0
vsize: 56804
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13873 0 0 0 60949 49 0 0 25 0 1 0 422505086 58707968 13851 4294967295 134512640 134672761 3221224528 3221223696 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14333 13851 603 41 0 14292 0
vsize: 57332
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13874 0 0 0 61949 49 0 0 25 0 1 0 422505086 58707968 13852 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14333 13852 603 41 0 14292 0
vsize: 57332
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13874 0 0 0 62949 49 0 0 25 0 1 0 422505086 58707968 13852 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14333 13852 603 41 0 14292 0
vsize: 57332
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13874 0 0 0 63950 49 0 0 25 0 1 0 422505086 58707968 13852 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14333 13852 603 41 0 14292 0
vsize: 57332
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13874 0 0 0 64950 49 0 0 25 0 1 0 422505086 58707968 13852 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14333 13852 603 41 0 14292 0
vsize: 57332
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 13874 0 0 0 65950 49 0 0 25 0 1 0 422505086 58707968 13852 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14333 13852 603 41 0 14292 0
vsize: 57332
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14142 0 0 0 66949 50 0 0 25 0 1 0 422505086 59883520 14120 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14620 14120 603 41 0 14579 0
vsize: 58480
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14142 0 0 0 67950 50 0 0 25 0 1 0 422505086 59883520 14120 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14620 14120 603 41 0 14579 0
vsize: 58480
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14142 0 0 0 68950 50 0 0 25 0 1 0 422505086 59883520 14120 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14620 14120 603 41 0 14579 0
vsize: 58480
[startup+700.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14142 0 0 0 69950 50 0 0 25 0 1 0 422505086 59883520 14120 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14620 14120 603 41 0 14579 0
vsize: 58480
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14142 0 0 0 70950 50 0 0 25 0 1 0 422505086 59883520 14120 4294967295 134512640 134672761 3221224528 3221223632 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14620 14120 603 41 0 14579 0
vsize: 58480
[startup+720.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14142 0 0 0 71950 50 0 0 25 0 1 0 422505086 59883520 14120 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14620 14120 603 41 0 14579 0
vsize: 58480
[startup+730.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14143 0 0 0 72951 50 0 0 25 0 1 0 422505086 59883520 14121 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14620 14121 603 41 0 14579 0
vsize: 58480
[startup+740.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14144 0 0 0 73950 50 0 0 25 0 1 0 422505086 59883520 14122 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14620 14122 603 41 0 14579 0
vsize: 58480
[startup+750.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 74950 50 0 0 25 0 1 0 422505086 59867136 14125 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14616 14125 603 41 0 14575 0
vsize: 58464
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 75950 50 0 0 25 0 1 0 422505086 59867136 14125 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14616 14125 603 41 0 14575 0
vsize: 58464
[startup+770.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 76950 50 0 0 25 0 1 0 422505086 59867136 14125 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14616 14125 603 41 0 14575 0
vsize: 58464
[startup+780.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 77950 50 0 0 25 0 1 0 422505086 59867136 14125 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14616 14125 603 41 0 14575 0
vsize: 58464
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 78951 50 0 0 25 0 1 0 422505086 59858944 14125 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14614 14125 603 41 0 14573 0
vsize: 58456
[startup+800.032 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 79951 50 0 0 25 0 1 0 422505086 59858944 14125 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14614 14125 603 41 0 14573 0
vsize: 58456
[startup+810.031 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 80951 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+820.032 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 81951 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223632 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+830.032 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 82951 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+840.033 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 83952 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+850.034 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 84952 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+860.034 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 85952 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+870.034 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 86952 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+880.034 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 87952 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+890.035 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 88953 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+900.034 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 89953 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+910.034 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14147 0 0 0 90953 50 0 0 25 0 1 0 422505086 59813888 14121 4294967295 134512640 134672761 3221224528 3221223712 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14603 14121 603 41 0 14562 0
vsize: 58412
[startup+920.035 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14223 0 0 0 91953 50 0 0 25 0 1 0 422505086 60219392 14197 4294967295 134512640 134672761 3221224528 3221223728 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 14197 603 41 0 14661 0
vsize: 58808
[startup+930.036 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6276
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14386 0 0 0 92953 50 0 0 25 0 1 0 422505086 60895232 14360 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14360 603 41 0 14826 0
vsize: 59468
[startup+940.114 s]
Raw data (loadavg): 1.09 1.02 0.93 3/58 6319
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14386 0 0 0 93961 50 0 0 25 0 1 0 422505086 60895232 14360 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14360 603 41 0 14826 0
vsize: 59468
[startup+950.114 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 6329
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14386 0 0 0 94960 50 0 0 25 0 1 0 422505086 60895232 14360 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14360 603 41 0 14826 0
vsize: 59468
[startup+960.114 s]
Raw data (loadavg): 1.14 1.03 0.93 2/54 6329
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14386 0 0 0 95960 50 0 0 25 0 1 0 422505086 60895232 14360 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14360 603 41 0 14826 0
vsize: 59468
[startup+970.114 s]
Raw data (loadavg): 1.12 1.03 0.93 2/54 6329
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14386 0 0 0 96961 50 0 0 25 0 1 0 422505086 60895232 14360 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14360 603 41 0 14826 0
vsize: 59468
[startup+980.114 s]
Raw data (loadavg): 1.10 1.03 0.93 2/54 6329
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14386 0 0 0 97961 50 0 0 25 0 1 0 422505086 60895232 14360 4294967295 134512640 134672761 3221224528 3221223712 134558700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14360 603 41 0 14826 0
vsize: 59468
[startup+990.114 s]
Raw data (loadavg): 1.08 1.03 0.93 2/54 6329
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14386 0 0 0 98961 50 0 0 25 0 1 0 422505086 60895232 14360 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14360 603 41 0 14826 0
vsize: 59468
[startup+1000.11 s]
Raw data (loadavg): 1.07 1.03 0.93 2/54 6329
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14386 0 0 0 99961 50 0 0 25 0 1 0 422505086 60895232 14360 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14360 603 41 0 14826 0
vsize: 59468
[startup+1010.11 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 6329
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14386 0 0 0 100961 51 0 0 25 0 1 0 422505086 60895232 14360 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14360 603 41 0 14826 0
vsize: 59468
[startup+1020.11 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 6331
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14386 0 0 0 101961 51 0 0 25 0 1 0 422505086 60895232 14360 4294967295 134512640 134672761 3221224528 3221223632 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14360 603 41 0 14826 0
vsize: 59468
[startup+1030.11 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 6331
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14387 0 0 0 102961 51 0 0 25 0 1 0 422505086 60895232 14361 4294967295 134512640 134672761 3221224528 3221223632 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14361 603 41 0 14826 0
vsize: 59468
[startup+1040.12 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 6331
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14387 0 0 0 103961 51 0 0 25 0 1 0 422505086 60895232 14361 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14361 603 41 0 14826 0
vsize: 59468
[startup+1050.12 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 6331
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14387 0 0 0 104962 51 0 0 25 0 1 0 422505086 60895232 14361 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14361 603 41 0 14826 0
vsize: 59468
[startup+1060.12 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 6331
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14387 0 0 0 105962 51 0 0 25 0 1 0 422505086 60895232 14361 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14361 603 41 0 14826 0
vsize: 59468
[startup+1070.12 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 6331
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14666 0 0 0 106961 51 0 0 25 0 1 0 422505086 61976576 14640 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15131 14640 603 41 0 15090 0
vsize: 60524
[startup+1070.85 s]
Raw data (loadavg): 1.02 1.02 0.93 1/53 6331
Raw data (stat): 6276 (minisat+) R 6275 32461 32460 0 -1 0 14666 0 0 0 106961 51 0 0 25 0 1 0 422505086 61976576 14640 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15131 14640 603 41 0 15090 0
vsize: 0

Child status: 30
Real time (s): 1070.85
CPU time (s): 1070.86
CPU user time (s): 1070.32
CPU system time (s): 0.546916
CPU usage (%): 100.002
Max. virtual memory (Kb): 60524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####