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-chnl30_40_pb.cnf.cr.opb
MD5SUM6a0000bd3257094a387dbf208b4df8cf
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 41
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.073987
Number of variables2400
Total number of constraints140
Number of constraints which are clauses80
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint30
Maximum length of a constraint40

Trace number 4750 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-13 20:11:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=113 boxname=wulflinc1 idbench=13 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6a0000bd3257094a387dbf208b4df8cf  /oldhome/oroussel/tmp/wulflinc1/normalized-chnl30_40_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc1/normalized-chnl30_40_pb.cnf.cr.opb
IDLAUNCH: 113
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        864612 kB
Buffers:         39944 kB
Cached:         106052 kB
SwapCached:          0 kB
Active:         106408 kB
Inactive:        42716 kB
HighTotal:      131008 kB
HighFree:        32200 kB
LowTotal:       903652 kB
LowFree:        832412 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           7196 kB
Slab:            15184 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:31:08 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 113 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   77
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:   77
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   5]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   3]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   1]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11540    32220 |    3846       0        0     nan |  0.000 % |
c |       105 |   11540    32220 |    4230     105    11655   111.0 |  0.855 % |
c |       256 |   11540    32220 |    4653     256    29323   114.5 |  0.855 % |
c |       482 |   11540    32220 |    5119     482    59867   124.2 |  0.855 % |
c |       819 |   11540    32220 |    5630     819   119821   146.3 |  0.855 % |
c |      1326 |   11540    32220 |    6194    1326   200884   151.5 |  0.855 % |
c |      2085 |   11540    32220 |    6813    2085   338592   162.4 |  0.855 % |
c |      3224 |   11540    32220 |    7494    3224   573967   178.0 |  0.855 % |
c |      4933 |   11540    32220 |    8244    4933  1020753   206.9 |  0.855 % |
c |      7495 |   11540    32220 |    9068    7495  1644283   219.4 |  0.855 % |
c |     11343 |   11540    32220 |    9975   11343  2620703   231.0 |  0.855 % |
c |     17110 |   11540    32220 |   10973   11439  2978380   260.4 |  0.855 % |
c |     25760 |   11540    32220 |   12070    7811  2675183   342.5 |  0.855 % |
c |     38735 |   11540    32220 |   13277   13643  5459721   400.2 |  0.855 % |
c |     58196 |   11540    32220 |   14605   10980  5555897   506.0 |  0.855 % |
c |     87389 |   11540    32220 |   16065   15223  7944453   521.9 |  0.855 % |
c |    131185 |   11540    32220 |   17672   13326  6647495   498.8 |  0.855 % |
c |    196871 |   11540    32220 |   19439   19364  9746152   503.3 |  0.855 % |
c |    295399 |   11540    32220 |   21383   18529  5847392   315.6 |  0.855 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/56 14924
Raw data (stat): 14924 (runsolver) R 14923 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 363651960 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99954 s]
Raw data (loadavg): 0.87 0.95 0.90 2/56 14924
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 2933 0 0 0 993 6 0 0 25 0 1 0 363651960 13594624 2911 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3319 2911 603 41 0 3278 0
vsize: 13276
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.96 0.90 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 3652 0 0 0 1991 8 0 0 25 0 1 0 363651960 16560128 3630 4294967295 134512640 134672761 3221224624 3221223728 134555096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4043 3630 603 41 0 4002 0
vsize: 16172
[startup+30.0001 s]
Raw data (loadavg): 0.91 0.96 0.90 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 4083 0 0 0 2989 9 0 0 25 0 1 0 363651960 18313216 4061 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4471 4061 603 41 0 4430 0
vsize: 17884
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.96 0.90 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 5146 0 0 0 3987 12 0 0 25 0 1 0 363651960 22753280 5124 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5555 5124 603 41 0 5514 0
vsize: 22220
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.96 0.90 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 5341 0 0 0 4987 13 0 0 25 0 1 0 363651960 23564288 5319 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5753 5319 603 41 0 5712 0
vsize: 23012
[startup+60.0016 s]
Raw data (loadavg): 0.94 0.96 0.90 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 6168 0 0 0 5985 15 0 0 25 0 1 0 363651960 26931200 6146 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6575 6146 603 41 0 6534 0
vsize: 26300
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.96 0.90 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 6168 0 0 0 6985 15 0 0 25 0 1 0 363651960 26931200 6146 4294967295 134512640 134672761 3221224624 3221223640 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6575 6146 603 41 0 6534 0
vsize: 26300
[startup+80.0018 s]
Raw data (loadavg): 0.96 0.96 0.90 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 6821 0 0 0 7984 16 0 0 25 0 1 0 363651960 29634560 6799 4294967295 134512640 134672761 3221224624 3221223728 134559805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7235 6799 603 41 0 7194 0
vsize: 28940
[startup+90.0016 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 6822 0 0 0 8985 16 0 0 25 0 1 0 363651960 29634560 6800 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7235 6800 603 41 0 7194 0
vsize: 28940
[startup+100.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 7796 0 0 0 9983 18 0 0 25 0 1 0 363651960 33562624 7774 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8194 7774 603 41 0 8153 0
vsize: 32776
[startup+110.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 8078 0 0 0 10982 18 0 0 25 0 1 0 363651960 34775040 8056 4294967295 134512640 134672761 3221224624 3221223728 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8490 8056 603 41 0 8449 0
vsize: 33960
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 8078 0 0 0 11982 18 0 0 25 0 1 0 363651960 34775040 8056 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8490 8056 603 41 0 8449 0
vsize: 33960
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 8206 0 0 0 12982 19 0 0 25 0 1 0 363651960 35315712 8184 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8622 8184 603 41 0 8581 0
vsize: 34488
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 8206 0 0 0 13982 19 0 0 25 0 1 0 363651960 35315712 8184 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8622 8184 603 41 0 8581 0
vsize: 34488
[startup+150.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 8206 0 0 0 14982 19 0 0 25 0 1 0 363651960 35315712 8184 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8622 8184 603 41 0 8581 0
vsize: 34488
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 9470 0 0 0 15979 22 0 0 25 0 1 0 363651960 40448000 9448 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9875 9448 603 41 0 9834 0
vsize: 39500
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 9934 0 0 0 16979 23 0 0 25 0 1 0 363651960 42385408 9912 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9912 603 41 0 10307 0
vsize: 41392
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 9934 0 0 0 17979 23 0 0 25 0 1 0 363651960 42385408 9912 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9912 603 41 0 10307 0
vsize: 41392
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 9934 0 0 0 18979 23 0 0 25 0 1 0 363651960 42385408 9912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9912 603 41 0 10307 0
vsize: 41392
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 9934 0 0 0 19979 23 0 0 25 0 1 0 363651960 42385408 9912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9912 603 41 0 10307 0
vsize: 41392
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 10331 0 0 0 20978 24 0 0 25 0 1 0 363651960 44003328 10309 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10743 10309 603 41 0 10702 0
vsize: 42972
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 10331 0 0 0 21979 24 0 0 25 0 1 0 363651960 44003328 10309 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10743 10309 603 41 0 10702 0
vsize: 42972
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 10331 0 0 0 22979 24 0 0 25 0 1 0 363651960 44003328 10309 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10743 10309 603 41 0 10702 0
vsize: 42972
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 10331 0 0 0 23979 24 0 0 25 0 1 0 363651960 44003328 10309 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10743 10309 603 41 0 10702 0
vsize: 42972
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 10616 0 0 0 24979 24 0 0 25 0 1 0 363651960 45211648 10594 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11038 10594 603 41 0 10997 0
vsize: 44152
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 10616 0 0 0 25979 24 0 0 25 0 1 0 363651960 45211648 10594 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11038 10594 603 41 0 10997 0
vsize: 44152
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 10616 0 0 0 26979 24 0 0 25 0 1 0 363651960 45211648 10594 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11038 10594 603 41 0 10997 0
vsize: 44152
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 10616 0 0 0 27979 24 0 0 25 0 1 0 363651960 45211648 10594 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11038 10594 603 41 0 10997 0
vsize: 44152
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 10616 0 0 0 28979 24 0 0 25 0 1 0 363651960 45211648 10594 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11038 10594 603 41 0 10997 0
vsize: 44152
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 10789 0 0 0 29979 25 0 0 25 0 1 0 363651960 45887488 10767 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11203 10767 603 41 0 11162 0
vsize: 44812
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14926
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11238 0 0 0 30977 27 0 0 25 0 1 0 363651960 47775744 11216 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11238 0 0 0 31976 27 0 0 25 0 1 0 363651960 47775744 11216 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11238 0 0 0 32976 27 0 0 25 0 1 0 363651960 47775744 11216 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11238 0 0 0 33976 28 0 0 25 0 1 0 363651960 47775744 11216 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11238 0 0 0 34976 28 0 0 25 0 1 0 363651960 47775744 11216 4294967295 134512640 134672761 3221224624 3221222496 134565779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11238 0 0 0 35976 28 0 0 25 0 1 0 363651960 47775744 11216 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11238 0 0 0 36976 28 0 0 25 0 1 0 363651960 47775744 11216 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11216 603 41 0 11623 0
vsize: 46656
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 37976 28 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 38976 28 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 39976 28 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 40976 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 41976 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 42976 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 43976 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 44976 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 45976 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 46977 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 47977 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 48977 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 49977 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 50977 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11239 0 0 0 51977 29 0 0 25 0 1 0 363651960 47775744 11217 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11664 11217 603 41 0 11623 0
vsize: 46656
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11717 0 0 0 52976 30 0 0 25 0 1 0 363651960 49803264 11695 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12159 11695 603 41 0 12118 0
vsize: 48636
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11818 0 0 0 53976 31 0 0 25 0 1 0 363651960 50208768 11796 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11796 603 41 0 12217 0
vsize: 49032
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11818 0 0 0 54977 31 0 0 25 0 1 0 363651960 50208768 11796 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11796 603 41 0 12217 0
vsize: 49032
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11818 0 0 0 55976 31 0 0 25 0 1 0 363651960 50208768 11796 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11796 603 41 0 12217 0
vsize: 49032
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 56977 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 57977 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 58977 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 59977 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14928
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 60977 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 61977 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 62977 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 63977 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 64978 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 65978 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 66978 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 67978 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 68978 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11820 0 0 0 69978 31 0 0 25 0 1 0 363651960 50208768 11798 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11798 603 41 0 12217 0
vsize: 49032
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11934 0 0 0 70978 32 0 0 25 0 1 0 363651960 50614272 11912 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12357 11912 603 41 0 12316 0
vsize: 49428
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11934 0 0 0 71979 32 0 0 25 0 1 0 363651960 50614272 11912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12357 11912 603 41 0 12316 0
vsize: 49428
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11934 0 0 0 72979 32 0 0 25 0 1 0 363651960 50614272 11912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12357 11912 603 41 0 12316 0
vsize: 49428
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 11934 0 0 0 73979 32 0 0 25 0 1 0 363651960 50614272 11912 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12357 11912 603 41 0 12316 0
vsize: 49428
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 12326 0 0 0 74978 33 0 0 25 0 1 0 363651960 52236288 12304 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12753 12304 603 41 0 12712 0
vsize: 51012
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 12662 0 0 0 75977 34 0 0 25 0 1 0 363651960 53587968 12640 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13083 12640 603 41 0 13042 0
vsize: 52332
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 12662 0 0 0 76977 34 0 0 25 0 1 0 363651960 53587968 12640 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13083 12640 603 41 0 13042 0
vsize: 52332
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 12662 0 0 0 77978 34 0 0 25 0 1 0 363651960 53587968 12640 4294967295 134512640 134672761 3221224624 3221223728 134555105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13083 12640 603 41 0 13042 0
vsize: 52332
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 12729 0 0 0 78978 34 0 0 25 0 1 0 363651960 53993472 12707 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13182 12707 603 41 0 13141 0
vsize: 52728
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 12729 0 0 0 79978 34 0 0 25 0 1 0 363651960 53993472 12707 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13182 12707 603 41 0 13141 0
vsize: 52728
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 12729 0 0 0 80978 34 0 0 25 0 1 0 363651960 53993472 12707 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13182 12707 603 41 0 13141 0
vsize: 52728
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 12729 0 0 0 81978 34 0 0 25 0 1 0 363651960 53993472 12707 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13182 12707 603 41 0 13141 0
vsize: 52728
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 12759 0 0 0 82978 34 0 0 25 0 1 0 363651960 53993472 12737 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13182 12737 603 41 0 13141 0
vsize: 52728
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13612 0 0 0 83976 36 0 0 25 0 1 0 363651960 57491456 13590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+850.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13612 0 0 0 84976 36 0 0 25 0 1 0 363651960 57491456 13590 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+860.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13612 0 0 0 85976 36 0 0 25 0 1 0 363651960 57491456 13590 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13590 603 41 0 13995 0
vsize: 56144
[startup+870.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 86977 36 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 87977 36 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 88977 37 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 89977 37 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14930
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 90976 37 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 91976 38 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+930.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 92976 38 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 93976 38 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+950.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 94977 38 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 95976 38 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 96976 38 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 97976 38 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+990.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 98976 38 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 99976 39 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 100976 39 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 101976 39 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223776 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 102976 39 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 103976 39 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 104976 39 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 105976 40 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 106976 40 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 107976 40 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223808 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 108976 40 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 109976 40 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 110976 40 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 111976 40 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 112976 40 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 113976 41 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 114977 41 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 115977 41 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 116977 41 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 117977 41 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13613 0 0 0 118977 41 0 0 25 0 1 0 363651960 57491456 13591 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14036 13591 603 41 0 13995 0
vsize: 56144
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 14932
Raw data (stat): 14924 (minisat+) R 14923 12452 12451 0 -1 0 13614 0 0 0 119977 41 0 0 25 0 1 0 363651960 57491456 13592 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 13592 603 41 0 13995 0
vsize: 56144
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 14932
Raw data (stat): 14924 (minisat+) Z 14923 12452 12451 0 -1 12 13616 0 0 0 119977 43 0 0 25 0 1 0 363651960 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.21
CPU user time (s): 1199.78
CPU system time (s): 0.437933
CPU usage (%): 100.014
Max. virtual memory (Kb): 56144
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####