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-chnl35_40_pb.cnf.cr.opb
MD5SUM85d4e2fa5fd7a61a85d3ecb1e311bddb
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.083986
Number of variables2800
Total number of constraints150
Number of constraints which are clauses80
Number of constraints which are cardinality constraints (but not clauses)70
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint35
Maximum length of a constraint40

Trace number 4585 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-13 19:24:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3399 boxname=wulflinc17 idbench=15 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  85d4e2fa5fd7a61a85d3ecb1e311bddb  /oldhome/oroussel/tmp/wulflinc17/normalized-chnl35_40_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc17/normalized-chnl35_40_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc17/normalized-chnl35_40_pb.cnf.cr.opb
IDLAUNCH: 3399
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        857920 kB
Buffers:         33832 kB
Cached:         108700 kB
SwapCached:       2376 kB
Active:          49832 kB
Inactive:        98056 kB
HighTotal:      131008 kB
HighFree:        18676 kB
LowTotal:       903652 kB
LowFree:        839244 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23248 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:45:00 (client local time) WITH STATUS 0 IN 1200.14 SECONDS
stats: 3399 7 1200.14 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 150 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  69]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  68]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  67]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  66]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  65]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  64]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  63]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  62]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  61]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  60]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  59]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  58]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  57]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  56]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  55]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  54]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  53]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  52]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  51]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  50]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  49]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  48]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  47]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  46]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  45]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  44]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  43]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  42]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  41]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  40]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  39]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  38]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  37]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  36]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  35]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  34]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  33]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  32]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  31]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  30]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  29]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  28]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  27]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  26]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  25]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  24]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  23]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  22]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  21]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  20]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  19]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  18]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  17]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  16]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  15]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  14]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  13]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  12]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  11]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  10]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   9]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   8]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   7]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   6]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   5]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   4]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   3]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   2]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   1]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   0]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   34240   124250 |   11413       0        0     nan |  0.000 % |
c |       100 |   34240   124250 |   12554     100      200     2.0 |  5.882 % |
c |       250 |   33989   123370 |   13809     205      449     2.2 |  6.291 % |
c |       475 |   33478   121605 |   15190     334      765     2.3 |  7.143 % |
c |       812 |   32708   118959 |   16709     527     1337     2.5 |  8.463 % |
c |      1318 |   32131   117008 |   18380     921     3225     3.5 |  9.568 % |
c |      2077 |   31368   114449 |   20218    1568     6011     3.8 | 11.236 % |
c |      3216 |   30006   109800 |   22240    2499    10231     4.1 | 14.106 % |
c |      4924 |   25900    95596 |   24464    3513    17532     5.0 | 22.029 % |
c |      7486 |   18413    70132 |   26911    4809    54256    11.3 | 37.443 % |
c |     11334 |   17815    68092 |   29602    8536  1018190   119.3 | 38.739 % |
c |     17101 |   17760    67905 |   32562   14291  2547315   178.2 | 38.872 % |
c |     25751 |   17737    67826 |   35818   22930  5242162   228.6 | 38.920 % |
c |     38726 |   17737    67826 |   39400   35905 11503461   320.4 | 38.920 % |
c |     58187 |   17698    67697 |   43340   25705 10015223   389.6 | 39.016 % |
c |     87379 |   17678    67629 |   47674   20396 12781627   626.7 | 39.064 % |
c |    131169 |   17618    67423 |   52442   26262 14348251   546.4 | 39.184 % |
#### 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.00 2/55 23070
Raw data (stat): 23070 (runsolver) R 23069 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478458442 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99954 s]
Raw data (loadavg): 0.15 0.03 0.01 2/55 23070
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 1112 0 1 0 985 2 0 0 25 0 1 0 478458442 6463488 1087 4294967295 134512640 134672761 3221224544 3221223712 134564668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1087 603 41 0 1537 0
vsize: 6312
[startup+20.0001 s]
Raw data (loadavg): 0.28 0.06 0.02 2/55 23070
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 1117 0 1 0 1984 3 0 0 25 0 1 0 478458442 6598656 1092 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1611 1092 603 41 0 1570 0
vsize: 6444
[startup+30.0007 s]
Raw data (loadavg): 0.39 0.09 0.03 2/55 23070
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 1146 0 1 0 2984 3 0 0 25 0 1 0 478458442 6733824 1121 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1644 1121 603 41 0 1603 0
vsize: 6576
[startup+40.0003 s]
Raw data (loadavg): 0.57 0.14 0.04 2/55 23070
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 3485 0 1 0 3978 9 0 0 25 0 1 0 478458442 16302080 3460 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3980 3460 603 41 0 3939 0
vsize: 15920
[startup+50.0009 s]
Raw data (loadavg): 0.63 0.17 0.05 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 5332 0 1 0 4973 14 0 0 25 0 1 0 478458442 23805952 5307 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5812 5307 603 41 0 5771 0
vsize: 23248
[startup+60.0005 s]
Raw data (loadavg): 0.69 0.19 0.06 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 6477 0 1 0 5971 17 0 0 25 0 1 0 478458442 28549120 6452 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6970 6452 603 41 0 6929 0
vsize: 27880
[startup+70.0011 s]
Raw data (loadavg): 0.74 0.22 0.07 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 8529 0 1 0 6965 23 0 0 25 0 1 0 478458442 36925440 8504 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9015 8504 603 41 0 8974 0
vsize: 36060
[startup+80.0017 s]
Raw data (loadavg): 0.78 0.25 0.08 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 10458 0 1 0 7960 29 0 0 25 0 1 0 478458442 44875776 10433 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10956 10433 603 41 0 10915 0
vsize: 43824
[startup+90.0013 s]
Raw data (loadavg): 0.81 0.27 0.09 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 11978 0 1 0 8956 33 0 0 25 0 1 0 478458442 51216384 11953 4294967295 134512640 134672761 3221224544 3221223648 134560299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12504 11953 603 41 0 12463 0
vsize: 50016
[startup+100.001 s]
Raw data (loadavg): 0.84 0.29 0.10 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 13154 0 1 0 9952 37 0 0 25 0 1 0 478458442 56086528 13129 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13693 13129 603 41 0 13652 0
vsize: 54772
[startup+110 s]
Raw data (loadavg): 0.86 0.32 0.11 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 14246 0 1 0 10949 39 0 0 25 0 1 0 478458442 60530688 14221 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14778 14221 603 41 0 14737 0
vsize: 59112
[startup+120.001 s]
Raw data (loadavg): 0.88 0.34 0.12 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 15497 0 1 0 11947 42 0 0 25 0 1 0 478458442 65667072 15472 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16032 15472 603 41 0 15991 0
vsize: 64128
[startup+130.001 s]
Raw data (loadavg): 0.90 0.36 0.13 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 16683 0 1 0 12944 45 0 0 25 0 1 0 478458442 70524928 16658 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17218 16658 603 41 0 17177 0
vsize: 68872
[startup+140 s]
Raw data (loadavg): 0.92 0.38 0.14 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 16951 0 1 0 13943 46 0 0 25 0 1 0 478458442 71602176 16926 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17481 16926 603 41 0 17440 0
vsize: 69924
[startup+150.001 s]
Raw data (loadavg): 0.93 0.40 0.15 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 16951 0 1 0 14943 46 0 0 25 0 1 0 478458442 71602176 16926 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17481 16926 603 41 0 17440 0
vsize: 69924
[startup+160 s]
Raw data (loadavg): 0.94 0.42 0.16 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 16951 0 1 0 15943 46 0 0 25 0 1 0 478458442 71602176 16926 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17481 16926 603 41 0 17440 0
vsize: 69924
[startup+170.001 s]
Raw data (loadavg): 0.95 0.44 0.16 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 16951 0 1 0 16943 47 0 0 25 0 1 0 478458442 71602176 16926 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17481 16926 603 41 0 17440 0
vsize: 69924
[startup+180.001 s]
Raw data (loadavg): 0.95 0.46 0.17 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 16951 0 1 0 17943 47 0 0 25 0 1 0 478458442 71602176 16926 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17481 16926 603 41 0 17440 0
vsize: 69924
[startup+190 s]
Raw data (loadavg): 0.96 0.47 0.18 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 16951 0 1 0 18943 47 0 0 25 0 1 0 478458442 71602176 16926 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17481 16926 603 41 0 17440 0
vsize: 69924
[startup+200 s]
Raw data (loadavg): 0.97 0.49 0.19 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 16951 0 1 0 19943 47 0 0 25 0 1 0 478458442 71602176 16926 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17481 16926 603 41 0 17440 0
vsize: 69924
[startup+210 s]
Raw data (loadavg): 0.97 0.51 0.20 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 17251 0 1 0 20942 48 0 0 25 0 1 0 478458442 72818688 17226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17778 17226 603 41 0 17737 0
vsize: 71112
[startup+220 s]
Raw data (loadavg): 0.98 0.52 0.21 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 18769 0 1 0 21939 52 0 0 25 0 1 0 478458442 79036416 18744 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19296 18744 603 41 0 19255 0
vsize: 77184
[startup+230 s]
Raw data (loadavg): 0.98 0.54 0.21 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 19824 0 1 0 22936 54 0 0 25 0 1 0 478458442 83353600 19799 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20350 19799 603 41 0 20309 0
vsize: 81400
[startup+239.999 s]
Raw data (loadavg): 0.98 0.55 0.22 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 21084 0 1 0 23934 57 0 0 25 0 1 0 478458442 88481792 21059 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21602 21059 603 41 0 21561 0
vsize: 86408
[startup+249.999 s]
Raw data (loadavg): 0.98 0.57 0.23 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 22106 0 1 0 24931 59 0 0 25 0 1 0 478458442 92672000 22081 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22625 22081 603 41 0 22584 0
vsize: 90500
[startup+259.998 s]
Raw data (loadavg): 0.99 0.58 0.24 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 23085 0 1 0 25929 62 0 0 25 0 1 0 478458442 96722944 23060 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23614 23060 603 41 0 23573 0
vsize: 94456
[startup+269.999 s]
Raw data (loadavg): 0.99 0.59 0.24 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 24050 0 1 0 26927 64 0 0 25 0 1 0 478458442 100646912 24025 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24572 24025 603 41 0 24531 0
vsize: 98288
[startup+280 s]
Raw data (loadavg): 0.99 0.61 0.25 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 24903 0 1 0 27924 67 0 0 25 0 1 0 478458442 104185856 24878 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25436 24878 603 41 0 25395 0
vsize: 101744
[startup+289.999 s]
Raw data (loadavg): 0.99 0.62 0.26 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 25979 0 1 0 28921 70 0 0 25 0 1 0 478458442 108670976 25954 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26531 25954 603 41 0 26490 0
vsize: 106124
[startup+299.999 s]
Raw data (loadavg): 0.99 0.63 0.27 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26312 0 1 0 29920 71 0 0 25 0 1 0 478458442 110022656 26287 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26287 603 41 0 26820 0
vsize: 107444
[startup+309.998 s]
Raw data (loadavg): 0.99 0.64 0.28 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26312 0 1 0 30920 72 0 0 25 0 1 0 478458442 110022656 26287 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26287 603 41 0 26820 0
vsize: 107444
[startup+319.999 s]
Raw data (loadavg): 0.99 0.65 0.28 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26312 0 1 0 31920 72 0 0 25 0 1 0 478458442 110022656 26287 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26287 603 41 0 26820 0
vsize: 107444
[startup+330 s]
Raw data (loadavg): 0.99 0.67 0.29 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26313 0 1 0 32920 72 0 0 25 0 1 0 478458442 110022656 26288 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26288 603 41 0 26820 0
vsize: 107444
[startup+339.999 s]
Raw data (loadavg): 0.99 0.68 0.30 2/55 23072
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 33919 73 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+349.999 s]
Raw data (loadavg): 0.99 0.69 0.30 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 34919 73 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+359.998 s]
Raw data (loadavg): 0.99 0.70 0.31 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 35919 74 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+369.999 s]
Raw data (loadavg): 0.99 0.71 0.32 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 36919 74 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+379.999 s]
Raw data (loadavg): 0.99 0.71 0.32 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 37919 74 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+389.999 s]
Raw data (loadavg): 0.99 0.72 0.33 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 38919 74 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+399.999 s]
Raw data (loadavg): 0.99 0.73 0.34 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 39918 75 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+409.998 s]
Raw data (loadavg): 0.99 0.74 0.34 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 40918 75 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+419.999 s]
Raw data (loadavg): 0.99 0.75 0.35 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 41918 75 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+430 s]
Raw data (loadavg): 0.99 0.76 0.36 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 42918 75 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+439.999 s]
Raw data (loadavg): 0.99 0.76 0.36 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 43918 75 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+449.999 s]
Raw data (loadavg): 0.99 0.77 0.37 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 44918 76 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+459.999 s]
Raw data (loadavg): 0.99 0.78 0.38 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 45918 76 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+470 s]
Raw data (loadavg): 0.99 0.79 0.38 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 46917 76 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+480 s]
Raw data (loadavg): 0.99 0.79 0.39 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26314 0 1 0 47917 77 0 0 25 0 1 0 478458442 110022656 26289 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 26289 603 41 0 26820 0
vsize: 107444
[startup+489.999 s]
Raw data (loadavg): 0.99 0.80 0.39 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 26533 0 1 0 48916 78 0 0 25 0 1 0 478458442 110829568 26508 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27058 26508 603 41 0 27017 0
vsize: 108232
[startup+500 s]
Raw data (loadavg): 0.99 0.80 0.40 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 27267 0 1 0 49914 80 0 0 25 0 1 0 478458442 113930240 27242 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27815 27242 603 41 0 27774 0
vsize: 111260
[startup+510 s]
Raw data (loadavg): 0.99 0.81 0.41 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 27925 0 1 0 50913 81 0 0 25 0 1 0 478458442 116621312 27900 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28472 27900 603 41 0 28431 0
vsize: 113888
[startup+520 s]
Raw data (loadavg): 0.99 0.82 0.41 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 28488 0 1 0 51911 83 0 0 25 0 1 0 478458442 118910976 28463 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29031 28463 603 41 0 28990 0
vsize: 116124
[startup+530 s]
Raw data (loadavg): 0.99 0.82 0.42 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 28925 0 1 0 52910 85 0 0 25 0 1 0 478458442 120659968 28900 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29458 28900 603 41 0 29417 0
vsize: 117832
[startup+540 s]
Raw data (loadavg): 0.99 0.83 0.42 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 29589 0 1 0 53909 86 0 0 25 0 1 0 478458442 123379712 29564 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30122 29564 603 41 0 30081 0
vsize: 120488
[startup+550 s]
Raw data (loadavg): 0.99 0.83 0.43 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 30402 0 1 0 54906 89 0 0 25 0 1 0 478458442 126734336 30377 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30941 30377 603 41 0 30900 0
vsize: 123764
[startup+559.999 s]
Raw data (loadavg): 0.99 0.84 0.43 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 30815 0 1 0 55904 91 0 0 25 0 1 0 478458442 128483328 30790 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31368 30790 603 41 0 31327 0
vsize: 125472
[startup+570.001 s]
Raw data (loadavg): 0.99 0.84 0.44 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 31394 0 1 0 56903 92 0 0 25 0 1 0 478458442 130908160 31369 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31960 31369 603 41 0 31919 0
vsize: 127840
[startup+580.001 s]
Raw data (loadavg): 0.99 0.85 0.45 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 31568 0 1 0 57903 93 0 0 25 0 1 0 478458442 131608576 31543 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32131 31543 603 41 0 32090 0
vsize: 128524
[startup+590 s]
Raw data (loadavg): 0.99 0.85 0.45 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 31828 0 1 0 58902 94 0 0 25 0 1 0 478458442 132689920 31803 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32395 31803 603 41 0 32354 0
vsize: 129580
[startup+600 s]
Raw data (loadavg): 0.99 0.86 0.46 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 32023 0 1 0 59901 95 0 0 25 0 1 0 478458442 133500928 31998 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32593 31998 603 41 0 32552 0
vsize: 130372
[startup+610 s]
Raw data (loadavg): 0.99 0.86 0.46 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 32252 0 1 0 60901 95 0 0 25 0 1 0 478458442 134447104 32227 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32824 32227 603 41 0 32783 0
vsize: 131296
[startup+620.001 s]
Raw data (loadavg): 0.99 0.86 0.47 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 32611 0 1 0 61900 97 0 0 25 0 1 0 478458442 135798784 32586 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33154 32586 603 41 0 33113 0
vsize: 132616
[startup+630.001 s]
Raw data (loadavg): 0.99 0.87 0.47 2/55 23074
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 33120 0 1 0 62898 98 0 0 25 0 1 0 478458442 137961472 33095 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33682 33095 603 41 0 33641 0
vsize: 134728
[startup+640.002 s]
Raw data (loadavg): 0.99 0.87 0.48 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 33540 0 1 0 63897 100 0 0 25 0 1 0 478458442 139595776 33515 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34081 33515 603 41 0 34040 0
vsize: 136324
[startup+650.002 s]
Raw data (loadavg): 0.99 0.88 0.48 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 33845 0 1 0 64896 101 0 0 25 0 1 0 478458442 140947456 33820 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34411 33820 603 41 0 34370 0
vsize: 137644
[startup+660.002 s]
Raw data (loadavg): 0.99 0.88 0.49 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 34116 0 1 0 65895 102 0 0 25 0 1 0 478458442 142028800 34091 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34675 34091 603 41 0 34634 0
vsize: 138700
[startup+670.002 s]
Raw data (loadavg): 0.99 0.88 0.49 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 34363 0 1 0 66895 102 0 0 25 0 1 0 478458442 142974976 34338 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34906 34338 603 41 0 34865 0
vsize: 139624
[startup+680.003 s]
Raw data (loadavg): 0.99 0.89 0.50 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 34721 0 1 0 67894 103 0 0 25 0 1 0 478458442 144461824 34696 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35269 34696 603 41 0 35228 0
vsize: 141076
[startup+690.003 s]
Raw data (loadavg): 0.99 0.89 0.50 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 34986 0 1 0 68893 104 0 0 25 0 1 0 478458442 145543168 34961 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35533 34961 603 41 0 35492 0
vsize: 142132
[startup+700.003 s]
Raw data (loadavg): 0.99 0.89 0.51 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 35329 0 1 0 69892 105 0 0 25 0 1 0 478458442 147030016 35304 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35896 35304 603 41 0 35855 0
vsize: 143584
[startup+710.002 s]
Raw data (loadavg): 0.99 0.89 0.51 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 35717 0 1 0 70891 106 0 0 25 0 1 0 478458442 148578304 35692 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36274 35692 603 41 0 36233 0
vsize: 145096
[startup+720.003 s]
Raw data (loadavg): 0.99 0.90 0.52 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 36351 0 1 0 71890 108 0 0 25 0 1 0 478458442 151142400 36326 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36900 36326 603 41 0 36859 0
vsize: 147600
[startup+730.004 s]
Raw data (loadavg): 0.99 0.90 0.52 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 36629 0 1 0 72889 109 0 0 25 0 1 0 478458442 152399872 36604 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37207 36604 603 41 0 37166 0
vsize: 148828
[startup+740.003 s]
Raw data (loadavg): 0.99 0.90 0.53 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 36748 0 1 0 73888 110 0 0 25 0 1 0 478458442 152805376 36723 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37306 36723 603 41 0 37265 0
vsize: 149224
[startup+750.005 s]
Raw data (loadavg): 0.99 0.91 0.53 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 36849 0 1 0 74888 110 0 0 25 0 1 0 478458442 153210880 36824 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37405 36824 603 41 0 37364 0
vsize: 149620
[startup+760.004 s]
Raw data (loadavg): 0.99 0.91 0.54 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 36939 0 1 0 75887 111 0 0 25 0 1 0 478458442 153616384 36914 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37504 36914 603 41 0 37463 0
vsize: 150016
[startup+770.005 s]
Raw data (loadavg): 0.99 0.91 0.54 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37037 0 1 0 76887 111 0 0 25 0 1 0 478458442 154021888 37012 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37603 37012 603 41 0 37562 0
vsize: 150412
[startup+780.006 s]
Raw data (loadavg): 0.99 0.91 0.55 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37131 0 1 0 77887 112 0 0 25 0 1 0 478458442 154427392 37106 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37106 603 41 0 37661 0
vsize: 150808
[startup+790.005 s]
Raw data (loadavg): 0.99 0.92 0.55 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37153 0 1 0 78887 112 0 0 25 0 1 0 478458442 154427392 37128 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37128 603 41 0 37661 0
vsize: 150808
[startup+800.005 s]
Raw data (loadavg): 0.99 0.92 0.55 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37153 0 1 0 79886 113 0 0 25 0 1 0 478458442 154427392 37128 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37128 603 41 0 37661 0
vsize: 150808
[startup+810.005 s]
Raw data (loadavg): 0.99 0.92 0.56 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37153 0 1 0 80886 113 0 0 25 0 1 0 478458442 154427392 37128 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37128 603 41 0 37661 0
vsize: 150808
[startup+820.006 s]
Raw data (loadavg): 0.99 0.92 0.56 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37153 0 1 0 81886 114 0 0 25 0 1 0 478458442 154427392 37128 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37128 603 41 0 37661 0
vsize: 150808
[startup+830.006 s]
Raw data (loadavg): 0.99 0.92 0.57 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37154 0 1 0 82886 114 0 0 25 0 1 0 478458442 154427392 37129 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37129 603 41 0 37661 0
vsize: 150808
[startup+840.006 s]
Raw data (loadavg): 0.99 0.93 0.57 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37154 0 1 0 83885 114 0 0 25 0 1 0 478458442 154427392 37129 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37129 603 41 0 37661 0
vsize: 150808
[startup+850.006 s]
Raw data (loadavg): 0.99 0.93 0.57 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37154 0 1 0 84885 114 0 0 25 0 1 0 478458442 154427392 37129 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37129 603 41 0 37661 0
vsize: 150808
[startup+860.005 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37154 0 1 0 85885 114 0 0 25 0 1 0 478458442 154427392 37129 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37129 603 41 0 37661 0
vsize: 150808
[startup+870.007 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37154 0 1 0 86885 115 0 0 25 0 1 0 478458442 154427392 37129 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37129 603 41 0 37661 0
vsize: 150808
[startup+880.007 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 87885 115 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+890.006 s]
Raw data (loadavg): 0.99 0.94 0.59 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 88885 116 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+900.006 s]
Raw data (loadavg): 0.99 0.94 0.59 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 89885 116 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+910.005 s]
Raw data (loadavg): 0.99 0.94 0.60 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 90884 116 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+920.006 s]
Raw data (loadavg): 0.99 0.94 0.60 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 91884 117 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+930.006 s]
Raw data (loadavg): 0.99 0.94 0.60 2/55 23076
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 92884 117 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+940.005 s]
Raw data (loadavg): 0.99 0.94 0.61 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 93884 117 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+950.006 s]
Raw data (loadavg): 0.99 0.94 0.61 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 94884 117 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+960.006 s]
Raw data (loadavg): 0.99 0.95 0.62 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 95885 117 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+970.006 s]
Raw data (loadavg): 0.99 0.95 0.62 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 96885 117 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+980.006 s]
Raw data (loadavg): 0.99 0.95 0.62 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 97885 117 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223728 134558831 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+990.005 s]
Raw data (loadavg): 0.99 0.95 0.63 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 98885 117 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.95 0.63 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37155 0 1 0 99885 117 0 0 25 0 1 0 478458442 154427392 37130 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37702 37130 603 41 0 37661 0
vsize: 150808
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 37258 0 1 0 100885 117 0 0 25 0 1 0 478458442 154955776 37233 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37831 37233 603 41 0 37790 0
vsize: 151324
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 38159 0 1 0 101883 119 0 0 25 0 1 0 478458442 158609408 38134 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38723 38134 603 41 0 38682 0
vsize: 154892
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 38691 0 1 0 102883 120 0 0 25 0 1 0 478458442 160882688 38666 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39278 38666 603 41 0 39237 0
vsize: 157112
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 39098 0 1 0 103882 121 0 0 25 0 1 0 478458442 162484224 39073 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39669 39073 603 41 0 39628 0
vsize: 158676
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.95 0.65 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 39533 0 1 0 104882 121 0 0 25 0 1 0 478458442 164368384 39508 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40129 39508 603 41 0 40088 0
vsize: 160516
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.96 0.65 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 39978 0 1 0 105881 122 0 0 25 0 1 0 478458442 166223872 39953 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40582 39953 603 41 0 40541 0
vsize: 162328
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.96 0.65 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40486 0 1 0 106880 124 0 0 25 0 1 0 478458442 168251392 40461 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41077 40461 603 41 0 41036 0
vsize: 164308
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 107879 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 108879 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 109879 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 110879 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 111879 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 112879 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 113879 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.96 0.68 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 114880 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.68 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 115880 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.68 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 116880 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.69 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 117880 125 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.69 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 118880 126 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.69 2/55 23078
Raw data (stat): 23070 (minisat+) R 23069 20838 20837 0 -1 0 40723 0 1 0 119880 126 0 0 25 0 1 0 478458442 169308160 40698 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41335 40698 603 41 0 41294 0
vsize: 165340
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.69 1/55 23078
Raw data (stat): 23070 (minisat+) Z 23069 20838 20837 0 -1 12 40725 0 1 0 119880 133 0 0 25 0 1 0 478458442 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.08
CPU time (s): 1200.14
CPU user time (s): 1198.81
CPU system time (s): 1.3348
CPU usage (%): 100.005
Max. virtual memory (Kb): 165340
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####