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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl15_20_pb.cnf.cr.opb
MD5SUMce39bf71367df072c91f9b7587480c93
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(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 21
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.017996
Number of variables600
Total number of constraints70
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint20

Trace number 4576 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-13 19:22:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3390 boxname=wulflinc23 idbench=6 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ce39bf71367df072c91f9b7587480c93  /oldhome/oroussel/tmp/wulflinc23/normalized-chnl15_20_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-chnl15_20_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc23/normalized-chnl15_20_pb.cnf.cr.opb
IDLAUNCH: 3390
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        913104 kB
Buffers:         33784 kB
Cached:          45380 kB
SwapCached:        192 kB
Active:          43680 kB
Inactive:        38556 kB
HighTotal:      131008 kB
HighFree:        81676 kB
LowTotal:       903652 kB
LowFree:        831428 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            33692 kB
Committed_AS:    63468 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:42:55 (client local time) WITH STATUS 0 IN 1200.08 SECONDS
stats: 3390 7 1200.08 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 70 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................
c ---[  29]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  28]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  27]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  26]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  25]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  24]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  23]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  22]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  21]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  20]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  19]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  18]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  17]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  16]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  15]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  14]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  13]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  12]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  11]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  10]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   9]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   8]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   7]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   6]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   5]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   4]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   3]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   2]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   1]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   0]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6460    23370 |    2153       0        0     nan |  0.000 % |
c |       100 |    6435    23285 |    2368      93      501     5.4 | 10.517 % |
c |       250 |    6395    23141 |    2605     234     1025     4.4 | 10.805 % |
c |       476 |    6149    22304 |    2865     421     1973     4.7 | 13.046 % |
c |       814 |    5583    20368 |    3152     654     3953     6.0 | 18.161 % |
c |      1320 |    4456    16559 |    3467     939     7083     7.5 | 29.253 % |
c |      2079 |    4214    15735 |    3814    1634    82525    50.5 | 31.667 % |
c |      3219 |    4182    15627 |    4195    2762   232182    84.1 | 32.012 % |
c |      4927 |    4166    15575 |    4615    4466   467586   104.7 | 32.184 % |
c |      7492 |    4166    15575 |    5076    4334   536529   123.8 | 32.184 % |
c |     11336 |    4166    15575 |    5584    5241   652459   124.5 | 32.184 % |
c |     17105 |    4166    15575 |    6142    4609   501828   108.9 | 32.184 % |
c |     25754 |    4150    15523 |    6757    6283   718842   114.4 | 32.356 % |
c |     38730 |    4150    15523 |    7432    4036   512856   127.1 | 32.356 % |
c |     58192 |    4150    15523 |    8176    7006   970819   138.6 | 32.356 % |
c |     87385 |    4150    15523 |    8993    4730   605726   128.1 | 32.356 % |
c |    131178 |    4136    15473 |    9892    9197  1181682   128.5 | 32.471 % |
c |    196862 |    4120    15421 |   10882   10655  1458034   136.8 | 32.644 % |
c |    295391 |    4120    15421 |   11970    9743  1155373   118.6 | 32.644 % |
c |    443182 |    4120    15421 |   13167   10288  1197211   116.4 | 32.644 % |
c |    664866 |    4120    15421 |   14484    8190  1005935   122.8 | 32.644 % |
c |    997391 |    4088    15317 |   15932   11936  1353426   113.4 | 32.989 % |
#### 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.00 0.00 0.04 2/54 4543
Raw data (stat): 4543 (runsolver) R 4542 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478437552 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+10.0001 s]
Raw data (loadavg): 0.15 0.03 0.05 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 1319 0 1 0 983 3 0 0 25 0 1 0 478437552 7012352 1298 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1712 1298 603 41 0 1671 0
vsize: 6848
[startup+20.0004 s]
Raw data (loadavg): 0.28 0.06 0.06 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 1509 0 1 0 1982 4 0 0 25 0 1 0 478437552 7688192 1488 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1877 1488 603 41 0 1836 0
vsize: 7508
[startup+30.0002 s]
Raw data (loadavg): 0.39 0.09 0.07 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 1695 0 1 0 2982 5 0 0 25 0 1 0 478437552 8495104 1674 4294967295 134512640 134672761 3221224544 3221223712 134560900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2074 1674 603 41 0 2033 0
vsize: 8296
[startup+40.0009 s]
Raw data (loadavg): 0.49 0.12 0.08 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 1825 0 1 0 3982 5 0 0 25 0 1 0 478437552 9048064 1804 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2209 1804 603 41 0 2168 0
vsize: 8836
[startup+50.0012 s]
Raw data (loadavg): 0.56 0.15 0.09 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 1992 0 1 0 4981 6 0 0 25 0 1 0 478437552 9768960 1971 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2385 1971 603 41 0 2344 0
vsize: 9540
[startup+60.0014 s]
Raw data (loadavg): 0.63 0.18 0.10 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2028 0 1 0 5981 6 0 0 25 0 1 0 478437552 9904128 2007 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2418 2007 603 41 0 2377 0
vsize: 9672
[startup+70.0018 s]
Raw data (loadavg): 0.69 0.21 0.11 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2176 0 1 0 6981 6 0 0 25 0 1 0 478437552 10579968 2155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2583 2155 603 41 0 2542 0
vsize: 10332
[startup+80.0021 s]
Raw data (loadavg): 0.73 0.23 0.12 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2193 0 1 0 7981 6 0 0 25 0 1 0 478437552 10579968 2172 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2583 2172 603 41 0 2542 0
vsize: 10332
[startup+90.0031 s]
Raw data (loadavg): 0.77 0.26 0.13 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2193 0 1 0 8981 6 0 0 25 0 1 0 478437552 10579968 2172 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2583 2172 603 41 0 2542 0
vsize: 10332
[startup+100.003 s]
Raw data (loadavg): 0.81 0.28 0.14 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2219 0 1 0 9980 6 0 0 25 0 1 0 478437552 10743808 2198 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2623 2198 603 41 0 2582 0
vsize: 10492
[startup+110.003 s]
Raw data (loadavg): 0.84 0.30 0.14 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2339 0 1 0 10980 7 0 0 25 0 1 0 478437552 11280384 2318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2754 2318 603 41 0 2713 0
vsize: 11016
[startup+120.004 s]
Raw data (loadavg): 0.86 0.33 0.15 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2339 0 1 0 11980 7 0 0 25 0 1 0 478437552 11280384 2318 4294967295 134512640 134672761 3221224544 3221223648 134559805 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2754 2318 603 41 0 2713 0
vsize: 11016
[startup+130.004 s]
Raw data (loadavg): 0.88 0.35 0.16 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2340 0 1 0 12980 7 0 0 25 0 1 0 478437552 11280384 2319 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2754 2319 603 41 0 2713 0
vsize: 11016
[startup+140.004 s]
Raw data (loadavg): 0.90 0.37 0.17 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2353 0 1 0 13981 7 0 0 25 0 1 0 478437552 11280384 2332 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2754 2332 603 41 0 2713 0
vsize: 11016
[startup+150.005 s]
Raw data (loadavg): 0.92 0.39 0.18 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2355 0 1 0 14981 7 0 0 25 0 1 0 478437552 11280384 2334 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2754 2334 603 41 0 2713 0
vsize: 11016
[startup+160.004 s]
Raw data (loadavg): 0.93 0.41 0.19 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2504 0 1 0 15981 7 0 0 25 0 1 0 478437552 11968512 2483 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2922 2483 603 41 0 2881 0
vsize: 11688
[startup+170.005 s]
Raw data (loadavg): 0.94 0.43 0.20 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2561 0 1 0 16981 7 0 0 25 0 1 0 478437552 12238848 2540 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2988 2540 603 41 0 2947 0
vsize: 11952
[startup+180.005 s]
Raw data (loadavg): 0.95 0.45 0.20 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2601 0 1 0 17981 7 0 0 25 0 1 0 478437552 12374016 2580 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3021 2580 603 41 0 2980 0
vsize: 12084
[startup+190.006 s]
Raw data (loadavg): 0.95 0.46 0.21 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2611 0 1 0 18981 7 0 0 25 0 1 0 478437552 12374016 2590 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3021 2590 603 41 0 2980 0
vsize: 12084
[startup+200.006 s]
Raw data (loadavg): 0.96 0.48 0.22 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2665 0 1 0 19981 7 0 0 25 0 1 0 478437552 12644352 2644 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3087 2644 603 41 0 3046 0
vsize: 12348
[startup+210.006 s]
Raw data (loadavg): 0.97 0.50 0.23 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2703 0 1 0 20981 7 0 0 25 0 1 0 478437552 12779520 2682 4294967295 134512640 134672761 3221224544 3221223640 134555595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3120 2682 603 41 0 3079 0
vsize: 12480
[startup+220.006 s]
Raw data (loadavg): 0.97 0.51 0.24 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2710 0 1 0 21982 7 0 0 25 0 1 0 478437552 12779520 2689 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3120 2689 603 41 0 3079 0
vsize: 12480
[startup+230.006 s]
Raw data (loadavg): 0.98 0.53 0.24 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2723 0 1 0 22982 7 0 0 25 0 1 0 478437552 12914688 2702 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3153 2702 603 41 0 3112 0
vsize: 12612
[startup+240.007 s]
Raw data (loadavg): 0.98 0.54 0.25 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2829 0 1 0 23982 8 0 0 25 0 1 0 478437552 13320192 2808 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2808 603 41 0 3211 0
vsize: 13008
[startup+250.007 s]
Raw data (loadavg): 0.98 0.56 0.26 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2918 0 1 0 24981 8 0 0 25 0 1 0 478437552 13725696 2897 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3351 2897 603 41 0 3310 0
vsize: 13404
[startup+260.008 s]
Raw data (loadavg): 0.98 0.57 0.27 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2989 0 1 0 25981 9 0 0 25 0 1 0 478437552 13996032 2968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3417 2968 603 41 0 3376 0
vsize: 13668
[startup+270.007 s]
Raw data (loadavg): 0.99 0.59 0.27 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 2995 0 1 0 26981 9 0 0 25 0 1 0 478437552 14135296 2974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3451 2974 603 41 0 3410 0
vsize: 13804
[startup+280.007 s]
Raw data (loadavg): 0.99 0.60 0.28 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3028 0 1 0 27981 9 0 0 25 0 1 0 478437552 14299136 3007 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3491 3007 603 41 0 3450 0
vsize: 13964
[startup+290.007 s]
Raw data (loadavg): 0.99 0.61 0.29 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3028 0 1 0 28982 9 0 0 25 0 1 0 478437552 14299136 3007 4294967295 134512640 134672761 3221224544 3221223800 134562593 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3491 3007 603 41 0 3450 0
vsize: 13964
[startup+300.007 s]
Raw data (loadavg): 0.99 0.62 0.29 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3028 0 1 0 29982 9 0 0 25 0 1 0 478437552 14299136 3007 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3491 3007 603 41 0 3450 0
vsize: 13964
[startup+310.007 s]
Raw data (loadavg): 0.99 0.64 0.30 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3042 0 1 0 30982 9 0 0 25 0 1 0 478437552 14299136 3021 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3491 3021 603 41 0 3450 0
vsize: 13964
[startup+320.007 s]
Raw data (loadavg): 0.99 0.65 0.31 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3042 0 1 0 31982 9 0 0 25 0 1 0 478437552 14299136 3021 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3491 3021 603 41 0 3450 0
vsize: 13964
[startup+330.007 s]
Raw data (loadavg): 0.99 0.66 0.32 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3044 0 1 0 32982 9 0 0 25 0 1 0 478437552 14299136 3023 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3491 3023 603 41 0 3450 0
vsize: 13964
[startup+340.008 s]
Raw data (loadavg): 0.99 0.67 0.32 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3044 0 1 0 33982 9 0 0 25 0 1 0 478437552 14299136 3023 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3491 3023 603 41 0 3450 0
vsize: 13964
[startup+350.007 s]
Raw data (loadavg): 0.99 0.68 0.33 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3044 0 1 0 34982 9 0 0 25 0 1 0 478437552 14299136 3023 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3491 3023 603 41 0 3450 0
vsize: 13964
[startup+360.007 s]
Raw data (loadavg): 0.99 0.69 0.34 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3044 0 1 0 35982 9 0 0 25 0 1 0 478437552 14299136 3023 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3491 3023 603 41 0 3450 0
vsize: 13964
[startup+370.008 s]
Raw data (loadavg): 0.99 0.70 0.34 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3068 0 1 0 36982 10 0 0 25 0 1 0 478437552 14434304 3047 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3524 3047 603 41 0 3483 0
vsize: 14096
[startup+380.008 s]
Raw data (loadavg): 0.99 0.71 0.35 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3138 0 1 0 37982 10 0 0 25 0 1 0 478437552 14704640 3117 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3590 3117 603 41 0 3549 0
vsize: 14360
[startup+390.009 s]
Raw data (loadavg): 0.99 0.72 0.36 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3190 0 1 0 38982 10 0 0 25 0 1 0 478437552 14974976 3169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3169 603 41 0 3615 0
vsize: 14624
[startup+400.009 s]
Raw data (loadavg): 0.99 0.73 0.36 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3198 0 1 0 39982 10 0 0 25 0 1 0 478437552 14974976 3177 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3177 603 41 0 3615 0
vsize: 14624
[startup+410.008 s]
Raw data (loadavg): 0.99 0.74 0.37 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3198 0 1 0 40982 10 0 0 25 0 1 0 478437552 14974976 3177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3177 603 41 0 3615 0
vsize: 14624
[startup+420.008 s]
Raw data (loadavg): 0.99 0.74 0.38 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3204 0 1 0 41983 10 0 0 25 0 1 0 478437552 14974976 3183 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3183 603 41 0 3615 0
vsize: 14624
[startup+430.009 s]
Raw data (loadavg): 0.99 0.75 0.38 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3205 0 1 0 42983 10 0 0 25 0 1 0 478437552 14974976 3184 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3184 603 41 0 3615 0
vsize: 14624
[startup+440.009 s]
Raw data (loadavg): 0.99 0.76 0.39 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3207 0 1 0 43983 10 0 0 25 0 1 0 478437552 14974976 3186 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3186 603 41 0 3615 0
vsize: 14624
[startup+450.009 s]
Raw data (loadavg): 0.99 0.77 0.39 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3208 0 1 0 44983 10 0 0 25 0 1 0 478437552 14974976 3187 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3187 603 41 0 3615 0
vsize: 14624
[startup+460.008 s]
Raw data (loadavg): 0.99 0.77 0.40 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3220 0 1 0 45983 10 0 0 25 0 1 0 478437552 14974976 3199 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3199 603 41 0 3615 0
vsize: 14624
[startup+470.009 s]
Raw data (loadavg): 0.99 0.78 0.40 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3220 0 1 0 46983 10 0 0 25 0 1 0 478437552 14974976 3199 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3199 603 41 0 3615 0
vsize: 14624
[startup+480.009 s]
Raw data (loadavg): 0.99 0.79 0.41 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3221 0 1 0 47984 10 0 0 25 0 1 0 478437552 14974976 3200 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3200 603 41 0 3615 0
vsize: 14624
[startup+490.01 s]
Raw data (loadavg): 0.99 0.79 0.42 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3221 0 1 0 48984 10 0 0 25 0 1 0 478437552 14974976 3200 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3200 603 41 0 3615 0
vsize: 14624
[startup+500.01 s]
Raw data (loadavg): 0.99 0.80 0.42 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3222 0 1 0 49984 10 0 0 25 0 1 0 478437552 14974976 3201 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3201 603 41 0 3615 0
vsize: 14624
[startup+510.009 s]
Raw data (loadavg): 0.99 0.81 0.43 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3222 0 1 0 50984 10 0 0 25 0 1 0 478437552 14974976 3201 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3201 603 41 0 3615 0
vsize: 14624
[startup+520.009 s]
Raw data (loadavg): 0.99 0.81 0.43 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3228 0 1 0 51984 10 0 0 25 0 1 0 478437552 15138816 3207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3696 3207 603 41 0 3655 0
vsize: 14784
[startup+530.01 s]
Raw data (loadavg): 0.99 0.82 0.44 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3234 0 1 0 52985 10 0 0 25 0 1 0 478437552 15138816 3213 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3696 3213 603 41 0 3655 0
vsize: 14784
[startup+540.01 s]
Raw data (loadavg): 0.99 0.82 0.45 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3383 0 1 0 53984 11 0 0 25 0 1 0 478437552 15679488 3362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3828 3362 603 41 0 3787 0
vsize: 15312
[startup+550.01 s]
Raw data (loadavg): 0.99 0.83 0.45 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3383 0 1 0 54984 11 0 0 25 0 1 0 478437552 15679488 3362 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3828 3362 603 41 0 3787 0
vsize: 15312
[startup+560.011 s]
Raw data (loadavg): 0.99 0.83 0.46 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3431 0 1 0 55984 11 0 0 25 0 1 0 478437552 15966208 3410 4294967295 134512640 134672761 3221224544 3221223760 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3898 3410 603 41 0 3857 0
vsize: 15592
[startup+570.011 s]
Raw data (loadavg): 0.99 0.84 0.46 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3445 0 1 0 56984 11 0 0 25 0 1 0 478437552 15966208 3424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3898 3424 603 41 0 3857 0
vsize: 15592
[startup+580.011 s]
Raw data (loadavg): 0.99 0.84 0.47 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3447 0 1 0 57985 11 0 0 25 0 1 0 478437552 15966208 3426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3898 3426 603 41 0 3857 0
vsize: 15592
[startup+590.011 s]
Raw data (loadavg): 0.99 0.85 0.47 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3453 0 1 0 58985 11 0 0 25 0 1 0 478437552 16113664 3432 4294967295 134512640 134672761 3221224544 3221223728 134558839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3432 603 41 0 3893 0
vsize: 15736
[startup+600.011 s]
Raw data (loadavg): 0.99 0.85 0.48 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3480 0 1 0 59985 11 0 0 25 0 1 0 478437552 16113664 3459 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3459 603 41 0 3893 0
vsize: 15736
[startup+610.011 s]
Raw data (loadavg): 0.99 0.86 0.48 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3482 0 1 0 60985 11 0 0 25 0 1 0 478437552 16113664 3461 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3461 603 41 0 3893 0
vsize: 15736
[startup+620.012 s]
Raw data (loadavg): 0.99 0.86 0.49 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3482 0 1 0 61985 11 0 0 25 0 1 0 478437552 16113664 3461 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3461 603 41 0 3893 0
vsize: 15736
[startup+630.012 s]
Raw data (loadavg): 0.99 0.86 0.49 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3482 0 1 0 62986 11 0 0 25 0 1 0 478437552 16113664 3461 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3461 603 41 0 3893 0
vsize: 15736
[startup+640.012 s]
Raw data (loadavg): 0.99 0.87 0.50 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3482 0 1 0 63986 11 0 0 25 0 1 0 478437552 16113664 3461 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3461 603 41 0 3893 0
vsize: 15736
[startup+650.011 s]
Raw data (loadavg): 0.99 0.87 0.50 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3484 0 1 0 64986 11 0 0 25 0 1 0 478437552 16113664 3463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3463 603 41 0 3893 0
vsize: 15736
[startup+660.011 s]
Raw data (loadavg): 0.99 0.88 0.51 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3485 0 1 0 65986 11 0 0 25 0 1 0 478437552 16113664 3464 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3464 603 41 0 3893 0
vsize: 15736
[startup+670.012 s]
Raw data (loadavg): 0.99 0.88 0.51 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3490 0 1 0 66986 11 0 0 25 0 1 0 478437552 16113664 3469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3469 603 41 0 3893 0
vsize: 15736
[startup+680.012 s]
Raw data (loadavg): 0.99 0.88 0.52 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3490 0 1 0 67986 11 0 0 25 0 1 0 478437552 16113664 3469 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3934 3469 603 41 0 3893 0
vsize: 15736
[startup+690.012 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3566 0 1 0 68987 11 0 0 25 0 1 0 478437552 16551936 3545 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4041 3545 603 41 0 4000 0
vsize: 16164
[startup+700.013 s]
Raw data (loadavg): 0.99 0.89 0.53 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3573 0 1 0 69987 11 0 0 25 0 1 0 478437552 16551936 3552 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4041 3552 603 41 0 4000 0
vsize: 16164
[startup+710.012 s]
Raw data (loadavg): 0.99 0.89 0.53 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3580 0 1 0 70987 11 0 0 25 0 1 0 478437552 16551936 3559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4041 3559 603 41 0 4000 0
vsize: 16164
[startup+720.013 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3587 0 1 0 71987 11 0 0 25 0 1 0 478437552 16551936 3566 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4041 3566 603 41 0 4000 0
vsize: 16164
[startup+730.013 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3590 0 1 0 72987 11 0 0 25 0 1 0 478437552 16551936 3569 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4041 3569 603 41 0 4000 0
vsize: 16164
[startup+740.012 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3596 0 1 0 73987 11 0 0 25 0 1 0 478437552 16699392 3575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4077 3575 603 41 0 4036 0
vsize: 16308
[startup+750.013 s]
Raw data (loadavg): 0.99 0.90 0.55 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3652 0 1 0 74987 11 0 0 25 0 1 0 478437552 16834560 3631 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4110 3631 603 41 0 4069 0
vsize: 16440
[startup+760.013 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3687 0 1 0 75987 11 0 0 25 0 1 0 478437552 17104896 3666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4176 3666 603 41 0 4135 0
vsize: 16704
[startup+770.013 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3709 0 1 0 76988 11 0 0 25 0 1 0 478437552 17104896 3688 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4176 3688 603 41 0 4135 0
vsize: 16704
[startup+780.013 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3722 0 1 0 77988 11 0 0 25 0 1 0 478437552 17297408 3701 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3701 603 41 0 4182 0
vsize: 16892
[startup+790.013 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3724 0 1 0 78988 11 0 0 25 0 1 0 478437552 17297408 3703 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4223 3703 603 41 0 4182 0
vsize: 16892
[startup+800.013 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3897 0 1 0 79986 13 0 0 25 0 1 0 478437552 17989632 3876 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4392 3876 603 41 0 4351 0
vsize: 17568
[startup+810.012 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3913 0 1 0 80985 13 0 0 25 0 1 0 478437552 17989632 3892 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4392 3892 603 41 0 4351 0
vsize: 17568
[startup+820.012 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3913 0 1 0 81986 13 0 0 25 0 1 0 478437552 17989632 3892 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4392 3892 603 41 0 4351 0
vsize: 17568
[startup+830.013 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3927 0 1 0 82986 13 0 0 25 0 1 0 478437552 18124800 3906 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3906 603 41 0 4384 0
vsize: 17700
[startup+840.012 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3936 0 1 0 83986 13 0 0 25 0 1 0 478437552 18124800 3915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3915 603 41 0 4384 0
vsize: 17700
[startup+850.013 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3943 0 1 0 84986 13 0 0 25 0 1 0 478437552 18124800 3922 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3922 603 41 0 4384 0
vsize: 17700
[startup+860.012 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3944 0 1 0 85986 13 0 0 25 0 1 0 478437552 18124800 3923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3923 603 41 0 4384 0
vsize: 17700
[startup+870.012 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3945 0 1 0 86986 13 0 0 25 0 1 0 478437552 18124800 3924 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4425 3924 603 41 0 4384 0
vsize: 17700
[startup+880.012 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3956 0 1 0 87987 13 0 0 25 0 1 0 478437552 18309120 3935 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3935 603 41 0 4429 0
vsize: 17880
[startup+890.012 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3956 0 1 0 88987 13 0 0 25 0 1 0 478437552 18309120 3935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3935 603 41 0 4429 0
vsize: 17880
[startup+900.012 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3956 0 1 0 89987 13 0 0 25 0 1 0 478437552 18309120 3935 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3935 603 41 0 4429 0
vsize: 17880
[startup+910.012 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3956 0 1 0 90987 13 0 0 25 0 1 0 478437552 18309120 3935 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3935 603 41 0 4429 0
vsize: 17880
[startup+920.013 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3956 0 1 0 91987 13 0 0 25 0 1 0 478437552 18309120 3935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3935 603 41 0 4429 0
vsize: 17880
[startup+930.012 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3956 0 1 0 92987 13 0 0 25 0 1 0 478437552 18309120 3935 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3935 603 41 0 4429 0
vsize: 17880
[startup+940.012 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3957 0 1 0 93988 13 0 0 25 0 1 0 478437552 18309120 3936 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3936 603 41 0 4429 0
vsize: 17880
[startup+950.011 s]
Raw data (loadavg): 0.99 0.94 0.63 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3957 0 1 0 94988 13 0 0 25 0 1 0 478437552 18309120 3936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3936 603 41 0 4429 0
vsize: 17880
[startup+960.011 s]
Raw data (loadavg): 0.99 0.94 0.63 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3959 0 1 0 95988 13 0 0 25 0 1 0 478437552 18309120 3938 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3938 603 41 0 4429 0
vsize: 17880
[startup+970.012 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3959 0 1 0 96988 13 0 0 25 0 1 0 478437552 18309120 3938 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3938 603 41 0 4429 0
vsize: 17880
[startup+980.012 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3968 0 1 0 97988 13 0 0 25 0 1 0 478437552 18309120 3947 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3947 603 41 0 4429 0
vsize: 17880
[startup+990.012 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3968 0 1 0 98988 13 0 0 25 0 1 0 478437552 18309120 3947 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3947 603 41 0 4429 0
vsize: 17880
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3969 0 1 0 99989 13 0 0 25 0 1 0 478437552 18309120 3948 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3948 603 41 0 4429 0
vsize: 17880
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3969 0 1 0 100989 13 0 0 25 0 1 0 478437552 18309120 3948 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3948 603 41 0 4429 0
vsize: 17880
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3969 0 1 0 101989 13 0 0 25 0 1 0 478437552 18309120 3948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3948 603 41 0 4429 0
vsize: 17880
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3969 0 1 0 102989 13 0 0 25 0 1 0 478437552 18309120 3948 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3948 603 41 0 4429 0
vsize: 17880
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3969 0 1 0 103989 13 0 0 25 0 1 0 478437552 18309120 3948 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3948 603 41 0 4429 0
vsize: 17880
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3969 0 1 0 104990 13 0 0 25 0 1 0 478437552 18309120 3948 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3948 603 41 0 4429 0
vsize: 17880
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3979 0 1 0 105990 13 0 0 25 0 1 0 478437552 18309120 3958 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3958 603 41 0 4429 0
vsize: 17880
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3979 0 1 0 106990 13 0 0 25 0 1 0 478437552 18309120 3958 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3958 603 41 0 4429 0
vsize: 17880
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3980 0 1 0 107990 13 0 0 25 0 1 0 478437552 18309120 3959 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 3959 603 41 0 4429 0
vsize: 17880
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3990 0 1 0 108991 13 0 0 25 0 1 0 478437552 18505728 3969 4294967295 134512640 134672761 3221224544 3221223648 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4518 3969 603 41 0 4477 0
vsize: 18072
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3990 0 1 0 109991 13 0 0 25 0 1 0 478437552 18505728 3969 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4518 3969 603 41 0 4477 0
vsize: 18072
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 3991 0 1 0 110991 13 0 0 25 0 1 0 478437552 18505728 3970 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4518 3970 603 41 0 4477 0
vsize: 18072
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4001 0 1 0 111991 13 0 0 25 0 1 0 478437552 18505728 3980 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4518 3980 603 41 0 4477 0
vsize: 18072
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4001 0 1 0 112991 13 0 0 25 0 1 0 478437552 18505728 3980 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4518 3980 603 41 0 4477 0
vsize: 18072
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4010 0 1 0 113991 13 0 0 25 0 1 0 478437552 18505728 3989 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4518 3989 603 41 0 4477 0
vsize: 18072
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4010 0 1 0 114992 13 0 0 25 0 1 0 478437552 18505728 3989 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4518 3989 603 41 0 4477 0
vsize: 18072
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4011 0 1 0 115992 13 0 0 25 0 1 0 478437552 18505728 3990 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4518 3990 603 41 0 4477 0
vsize: 18072
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4023 0 1 0 116992 13 0 0 25 0 1 0 478437552 18640896 4002 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4551 4002 603 41 0 4510 0
vsize: 18204
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4073 0 1 0 117992 14 0 0 25 0 1 0 478437552 18776064 4052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4584 4052 603 41 0 4543 0
vsize: 18336
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4073 0 1 0 118992 14 0 0 25 0 1 0 478437552 18776064 4052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4584 4052 603 41 0 4543 0
vsize: 18336
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 4543
Raw data (stat): 4543 (minisat+) R 4542 3260 3259 0 -1 0 4211 0 1 0 119992 14 0 0 25 0 1 0 478437552 19460096 4190 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4751 4190 603 41 0 4710 0
vsize: 19004
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.70 1/54 4543
Raw data (stat): 4543 (minisat+) Z 4542 3260 3259 0 -1 12 4213 0 1 0 119992 15 0 0 25 0 1 0 478437552 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.03
CPU time (s): 1200.08
CPU user time (s): 1199.92
CPU system time (s): 0.153976
CPU usage (%): 100.004
Max. virtual memory (Kb): 19004
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####