PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga45_44_sat_pb.cnf.cr.opb
MD5SUM	c501a04dd091dbe678ec2743021adc30
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	46
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	15.2037
Number of variables	2970
Total number of constraints	2113
Number of constraints which are clauses	2024
Number of constraints which are cardinality constraints (but not clauses)	89
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	22
Maximum length of a constraint	45
Trace number 6158

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 03:35:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4568 boxname=wulflinc17 idbench=56 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c501a04dd091dbe678ec2743021adc30  /oldhome/oroussel/tmp/wulflinc17/normalized-fpga45_44_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc17/normalized-fpga45_44_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc17/normalized-fpga45_44_sat_pb.cnf.cr.opb
IDLAUNCH: 4568
/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:        818968 kB
Buffers:         36012 kB
Cached:         144668 kB
SwapCached:       2376 kB
Active:          59416 kB
Inactive:       126636 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        818716 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23888 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:55:31 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 4568 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2113 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  88]---> BDD-cost:   85
c ---[  87]---> BDD-cost:   85
c ---[  86]---> BDD-cost:   85
c ---[  85]---> BDD-cost:   85
c ---[  84]---> BDD-cost:   85
c ---[  83]---> BDD-cost:   85
c ---[  82]---> BDD-cost:   85
c ---[  81]---> BDD-cost:   85
c ---[  80]---> BDD-cost:   85
c ---[  79]---> BDD-cost:   85
c ---[  78]---> BDD-cost:   85
c ---[  77]---> BDD-cost:   85
c ---[  76]---> BDD-cost:   85
c ---[  75]---> BDD-cost:   85
c ---[  74]---> BDD-cost:   85
c ---[  73]---> BDD-cost:   85
c ---[  72]---> BDD-cost:   85
c ---[  71]---> BDD-cost:   85
c ---[  70]---> BDD-cost:   85
c ---[  69]---> BDD-cost:   85
c ---[  68]---> BDD-cost:   85
c ---[  67]---> BDD-cost:   85
c ---[  66]---> BDD-cost:   85
c ---[  65]---> BDD-cost:   85
c ---[  64]---> BDD-cost:   85
c ---[  63]---> BDD-cost:   85
c ---[  62]---> BDD-cost:   85
c ---[  61]---> BDD-cost:   85
c ---[  60]---> BDD-cost:   85
c ---[  59]---> BDD-cost:   85
c ---[  58]---> BDD-cost:   85
c ---[  57]---> BDD-cost:   85
c ---[  56]---> BDD-cost:   85
c ---[  55]---> BDD-cost:   85
c ---[  54]---> BDD-cost:   85
c ---[  53]---> BDD-cost:   85
c ---[  52]---> BDD-cost:   85
c ---[  51]---> BDD-cost:   85
c ---[  50]---> BDD-cost:   85
c ---[  49]---> BDD-cost:   85
c ---[  48]---> BDD-cost:   85
c ---[  47]---> BDD-cost:   85
c ---[  46]---> BDD-cost:   85
c ---[  45]---> BDD-cost:   85
c ---[  44]---> BDD-cost:   85
c ---[  43]---> BDD-cost:   41
c ---[  42]---> BDD-cost:   41
c ---[  41]---> BDD-cost:   41
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   41
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:   41
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:   41
c ---[  33]---> BDD-cost:   41
c ---[  32]---> BDD-cost:   41
c ---[  31]---> BDD-cost:   41
c ---[  30]---> BDD-cost:   41
c ---[  29]---> BDD-cost:   41
c ---[  28]---> BDD-cost:   41
c ---[  27]---> BDD-cost:   41
c ---[  26]---> BDD-cost:   41
c ---[  25]---> BDD-cost:   41
c ---[  24]---> BDD-cost:   41
c ---[  23]---> BDD-cost:   41
c ---[  22]---> BDD-cost:   41
c ---[  21]---> BDD-cost:   43
c ---[  20]---> BDD-cost:   43
c ---[  19]---> BDD-cost:   43
c ---[  18]---> BDD-cost:   43
c ---[  17]---> BDD-cost:   43
c ---[  16]---> BDD-cost:   43
c ---[  15]---> BDD-cost:   43
c ---[  14]---> BDD-cost:   43
c ---[  13]---> BDD-cost:   43
c ---[  12]---> BDD-cost:   43
c ---[  11]---> BDD-cost:   43
c ---[  10]---> BDD-cost:   43
c ---[   9]---> BDD-cost:   43
c ---[   8]---> BDD-cost:   43
c ---[   7]---> BDD-cost:   43
c ---[   6]---> BDD-cost:   43
c ---[   5]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   43
c ---[   3]---> BDD-cost:   43
c ---[   2]---> BDD-cost:   43
c ---[   1]---> BDD-cost:   43
c ---[   0]---> BDD-cost:   43
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27152   117142 |    9050       0        0     nan |  0.000 % |
c |       102 |   27048   116832 |    9955      54     3075    56.9 |  1.273 % |
c |       253 |   26773   116007 |   10950      53     1128    21.3 |  1.909 % |
c |       478 |   26263   114477 |   12045      71     1254    17.7 |  3.089 % |
c |       815 |   25673   112707 |   13250     172    16677    97.0 |  4.454 % |
c |      1323 |   25423   111957 |   14575     568   123633   217.7 |  5.033 % |
c |      2082 |   25193   111267 |   16032    1233   352448   285.8 |  5.565 % |
c |      3221 |   24468   109092 |   17635    2100   560481   266.9 |  7.243 % |
c |      4929 |   23098   104982 |   19399    3282   881270   268.5 | 10.413 % |
c |      7491 |   21913   101427 |   21339    5388  1568418   291.1 | 13.155 % |
c |     11335 |   20169    96197 |   23473    8607  2534268   294.4 | 17.193 % |
c |     17101 |   19249    93437 |   25820   14032  4396026   313.3 | 19.322 % |
c |     25750 |   18000    89692 |   28402   22242  7137212   320.9 | 22.215 % |
c |     38730 |   17046    86832 |   31243   15204  4652080   306.0 | 24.424 % |
c |     58193 |   16771    86007 |   34367   34586  9838680   284.5 | 25.061 % |
c |     87385 |   15861    83277 |   37804   39190 10464321   267.0 | 27.166 % |
c |    131174 |   15446    82032 |   41584   21451  5442220   253.7 | 28.127 % |
c |    196858 |   14883    80347 |   45742   21332  6447154   302.2 | 29.434 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/55 28341
Raw data (stat): 28341 (runsolver) R 28340 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481402018 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.99928 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 1650 0 0 0 995 3 0 0 25 0 1 0 481402018 8663040 1627 4294967295 134512640 134672761 3221224528 3221223632 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2115 1628 603 41 0 2074 0
vsize: 8460
[startup+19.9999 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 1883 0 0 0 1994 4 0 0 25 0 1 0 481402018 9609216 1860 4294967295 134512640 134672761 3221224528 3221223708 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1860 603 41 0 2305 0
vsize: 9384
[startup+29.9997 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 2568 0 0 0 2992 6 0 0 25 0 1 0 481402018 12439552 2545 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3037 2545 603 41 0 2996 0
vsize: 12148
[startup+40.0001 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 2834 0 0 0 3992 6 0 0 25 0 1 0 481402018 13512704 2811 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3299 2811 603 41 0 3258 0
vsize: 13196
[startup+49.9997 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 3237 0 0 0 4991 8 0 0 25 0 1 0 481402018 15134720 3214 4294967295 134512640 134672761 3221224528 3221223700 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3695 3214 603 41 0 3654 0
vsize: 14780
[startup+59.9996 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 3341 0 0 0 5990 8 0 0 25 0 1 0 481402018 15540224 3318 4294967295 134512640 134672761 3221224528 3221223680 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3794 3318 603 41 0 3753 0
vsize: 15176
[startup+69.9999 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 3628 0 0 0 6990 9 0 0 25 0 1 0 481402018 16756736 3605 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4091 3605 603 41 0 4050 0
vsize: 16364
[startup+79.9995 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 4540 0 0 0 7988 11 0 0 25 0 1 0 481402018 20537344 4517 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5014 4517 603 41 0 4973 0
vsize: 20056
[startup+89.9994 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 4625 0 0 0 8988 11 0 0 25 0 1 0 481402018 20807680 4602 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5080 4602 603 41 0 5039 0
vsize: 20320
[startup+99.9987 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 5719 0 0 0 9985 14 0 0 25 0 1 0 481402018 25255936 5696 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6166 5696 603 41 0 6125 0
vsize: 24664
[startup+109.998 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 5912 0 0 0 10984 15 0 0 25 0 1 0 481402018 26066944 5889 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6364 5889 603 41 0 6323 0
vsize: 25456
[startup+119.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 6757 0 0 0 11982 17 0 0 25 0 1 0 481402018 29577216 6734 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7221 6734 603 41 0 7180 0
vsize: 28884
[startup+129.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 7339 0 0 0 12980 19 0 0 25 0 1 0 481402018 32026624 7316 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7316 603 41 0 7778 0
vsize: 31276
[startup+139.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 7797 0 0 0 13980 20 0 0 25 0 1 0 481402018 33914880 7774 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8280 7774 603 41 0 8239 0
vsize: 33120
[startup+149.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 7979 0 0 0 14979 20 0 0 25 0 1 0 481402018 34590720 7956 4294967295 134512640 134672761 3221224528 3221223632 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8445 7956 603 41 0 8404 0
vsize: 33780
[startup+159.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 8100 0 0 0 15979 21 0 0 25 0 1 0 481402018 35127296 8077 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8576 8077 603 41 0 8535 0
vsize: 34304
[startup+169.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 8737 0 0 0 16978 22 0 0 25 0 1 0 481402018 37695488 8714 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9203 8714 603 41 0 9162 0
vsize: 36812
[startup+179.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 9157 0 0 0 17977 23 0 0 25 0 1 0 481402018 39448576 9134 4294967295 134512640 134672761 3221224528 3221223632 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9631 9134 603 41 0 9590 0
vsize: 38524
[startup+189.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 9896 0 0 0 18975 25 0 0 25 0 1 0 481402018 42418176 9873 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10356 9873 603 41 0 10315 0
vsize: 41424
[startup+199.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 10098 0 0 0 19975 26 0 0 25 0 1 0 481402018 43229184 10075 4294967295 134512640 134672761 3221224528 3221223632 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10554 10075 603 41 0 10513 0
vsize: 42216
[startup+209.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 10476 0 0 0 20974 27 0 0 25 0 1 0 481402018 44847104 10453 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10949 10453 603 41 0 10908 0
vsize: 43796
[startup+219.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 11463 0 0 0 21971 30 0 0 25 0 1 0 481402018 48893952 11440 4294967295 134512640 134672761 3221224528 3221223700 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11937 11440 603 41 0 11896 0
vsize: 47748
[startup+229.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 11798 0 0 0 22971 30 0 0 25 0 1 0 481402018 50245632 11775 4294967295 134512640 134672761 3221224528 3221223700 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12267 11775 603 41 0 12226 0
vsize: 49068
[startup+239.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12056 0 0 0 23970 31 0 0 25 0 1 0 481402018 51322880 12033 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12530 12033 603 41 0 12489 0
vsize: 50120
[startup+249.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 24970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12859 12364 603 41 0 12818 0
vsize: 51436
[startup+259.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 25970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12859 12364 603 41 0 12818 0
vsize: 51436
[startup+269.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 26970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12859 12364 603 41 0 12818 0
vsize: 51436
[startup+279.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 27970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12859 12364 603 41 0 12818 0
vsize: 51436
[startup+289.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 28970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12859 12364 603 41 0 12818 0
vsize: 51436
[startup+299.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28343
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 29970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12859 12364 603 41 0 12818 0
vsize: 51436
[startup+309.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 30970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12859 12364 603 41 0 12818 0
vsize: 51436
[startup+319.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12466 0 0 0 31970 32 0 0 25 0 1 0 481402018 52940800 12443 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12925 12443 603 41 0 12884 0
vsize: 51700
[startup+329.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 32968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13649 13155 603 41 0 13608 0
vsize: 54596
[startup+339.996 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 33968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13649 13155 603 41 0 13608 0
vsize: 54596
[startup+349.996 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 34968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13649 13155 603 41 0 13608 0
vsize: 54596
[startup+359.995 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 35968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13649 13155 603 41 0 13608 0
vsize: 54596
[startup+369.996 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 36968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13649 13155 603 41 0 13608 0
vsize: 54596
[startup+379.995 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 37968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13649 13155 603 41 0 13608 0
vsize: 54596
[startup+389.995 s]
Raw data (loadavg): 1.11 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 38968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13649 13155 603 41 0 13608 0
vsize: 54596
[startup+399.995 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 39968 35 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13649 13155 603 41 0 13608 0
vsize: 54596
[startup+409.995 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13557 0 0 0 40967 36 0 0 25 0 1 0 481402018 57393152 13534 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14012 13534 603 41 0 13971 0
vsize: 56048
[startup+419.995 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 41965 37 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14734 14241 603 41 0 14693 0
vsize: 58936
[startup+429.995 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 42965 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14734 14241 603 41 0 14693 0
vsize: 58936
[startup+439.995 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 43966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223712 134558771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14734 14241 603 41 0 14693 0
vsize: 58936
[startup+449.995 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 44966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14734 14241 603 41 0 14693 0
vsize: 58936
[startup+459.995 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 45966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14734 14241 603 41 0 14693 0
vsize: 58936
[startup+469.995 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 46966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14734 14241 603 41 0 14693 0
vsize: 58936
[startup+479.995 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 47966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14734 14241 603 41 0 14693 0
vsize: 58936
[startup+489.996 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 48966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14734 14241 603 41 0 14693 0
vsize: 58936
[startup+499.996 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 49966 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 14241 603 41 0 14689 0
vsize: 58920
[startup+509.995 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 50966 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 14241 603 41 0 14689 0
vsize: 58920
[startup+519.996 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 51966 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 14241 603 41 0 14689 0
vsize: 58920
[startup+529.996 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 52967 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 14241 603 41 0 14689 0
vsize: 58920
[startup+539.995 s]
Raw data (loadavg): 1.08 1.02 0.93 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 53967 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 14241 603 41 0 14689 0
vsize: 58920
[startup+549.995 s]
Raw data (loadavg): 1.07 1.02 0.93 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 54967 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223712 134558890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 14241 603 41 0 14689 0
vsize: 58920
[startup+559.995 s]
Raw data (loadavg): 1.06 1.01 0.93 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 55967 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 14241 603 41 0 14689 0
vsize: 58920
[startup+569.994 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 56967 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 14241 603 41 0 14689 0
vsize: 58920
[startup+579.994 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 15353 0 0 0 57965 40 0 0 25 0 1 0 481402018 64815104 15330 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15824 15330 603 41 0 15783 0
vsize: 63296
[startup+589.994 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 16405 0 0 0 58963 43 0 0 25 0 1 0 481402018 69136384 16382 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16879 16382 603 41 0 16838 0
vsize: 67516
[startup+599.994 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 28345
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 17193 0 0 0 59961 45 0 0 25 0 1 0 481402018 72413184 17170 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17679 17170 603 41 0 17638 0
vsize: 70716
[startup+609.994 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 17882 0 0 0 60960 47 0 0 25 0 1 0 481402018 75247616 17859 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18371 17859 603 41 0 18330 0
vsize: 73484
[startup+619.994 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 18741 0 0 0 61957 49 0 0 25 0 1 0 481402018 78753792 18718 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19227 18718 603 41 0 19186 0
vsize: 76908
[startup+629.994 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 19513 0 0 0 62956 51 0 0 25 0 1 0 481402018 81928192 19490 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20002 19490 603 41 0 19961 0
vsize: 80008
[startup+639.995 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 20235 0 0 0 63954 52 0 0 25 0 1 0 481402018 84959232 20212 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20742 20212 603 41 0 20701 0
vsize: 82968
[startup+649.994 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 20811 0 0 0 64954 53 0 0 25 0 1 0 481402018 87310336 20788 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21316 20788 603 41 0 21275 0
vsize: 85264
[startup+659.994 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21337 0 0 0 65953 54 0 0 25 0 1 0 481402018 89600000 21314 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21875 21314 603 41 0 21834 0
vsize: 87500
[startup+669.995 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 66953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+679.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 67953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+689.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 68953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+699.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 69953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+709.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 70953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+719.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 71953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+729.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 72954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+739.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 73954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+749.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 74954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+759.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 75954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+769.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 76954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+779.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 77954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21974 21426 603 41 0 21933 0
vsize: 87896
[startup+789.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21930 0 0 0 78953 56 0 0 25 0 1 0 481402018 92028928 21907 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22468 21907 603 41 0 22427 0
vsize: 89872
[startup+799.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 79953 57 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+809.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 80953 57 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+819.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 81953 57 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223712 134559367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+829.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 82953 57 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+839.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 83953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+849.997 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 84953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+859.997 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 85953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+869.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 86953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223712 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+879.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 87953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+889.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 88953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+899.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28347
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 89953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+909.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 90953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+919.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 91954 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223632 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+929.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 92954 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22252 603 41 0 22755 0
vsize: 91184
[startup+939.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22890 0 0 0 93953 60 0 0 25 0 1 0 481402018 95956992 22867 4294967295 134512640 134672761 3221224528 3221223632 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23427 22867 603 41 0 23386 0
vsize: 93708
[startup+949.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 23772 0 0 0 94951 61 0 0 25 0 1 0 481402018 99606528 23749 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24318 23749 603 41 0 24277 0
vsize: 97272
[startup+959.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 24553 0 0 0 95949 64 0 0 25 0 1 0 481402018 102715392 24530 4294967295 134512640 134672761 3221224528 3221223632 134559916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25077 24530 603 41 0 25036 0
vsize: 100308
[startup+969.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 25299 0 0 0 96948 65 0 0 25 0 1 0 481402018 105852928 25276 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25843 25276 603 41 0 25802 0
vsize: 103372
[startup+979.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 25989 0 0 0 97948 65 0 0 25 0 1 0 481402018 108691456 25966 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26536 25966 603 41 0 26495 0
vsize: 106144
[startup+989.996 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 26583 0 0 0 98947 67 0 0 25 0 1 0 481402018 111140864 26560 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27134 26560 603 41 0 27093 0
vsize: 108536
[startup+999.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 27140 0 0 0 99946 68 0 0 25 0 1 0 481402018 113467392 27117 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27702 27117 603 41 0 27661 0
vsize: 110808
[startup+1009.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 27572 0 0 0 100945 69 0 0 25 0 1 0 481402018 115367936 27549 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28166 27549 603 41 0 28125 0
vsize: 112664
[startup+1019.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 28108 0 0 0 101944 70 0 0 25 0 1 0 481402018 117526528 28085 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28693 28085 603 41 0 28652 0
vsize: 114772
[startup+1030 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 28814 0 0 0 102943 71 0 0 25 0 1 0 481402018 120500224 28791 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29419 28791 603 41 0 29378 0
vsize: 117676
[startup+1040 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29453 0 0 0 103941 73 0 0 25 0 1 0 481402018 123068416 29430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30046 29430 603 41 0 30005 0
vsize: 120184
[startup+1050 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29859 0 0 0 104940 74 0 0 25 0 1 0 481402018 124690432 29836 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29836 603 41 0 30401 0
vsize: 121768
[startup+1059.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29859 0 0 0 105940 74 0 0 25 0 1 0 481402018 124690432 29836 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29836 603 41 0 30401 0
vsize: 121768
[startup+1070 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29859 0 0 0 106941 74 0 0 25 0 1 0 481402018 124690432 29836 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29836 603 41 0 30401 0
vsize: 121768
[startup+1080 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29860 0 0 0 107941 74 0 0 25 0 1 0 481402018 124690432 29837 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29837 603 41 0 30401 0
vsize: 121768
[startup+1090 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 108941 74 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29838 603 41 0 30401 0
vsize: 121768
[startup+1100 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 109941 74 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29838 603 41 0 30401 0
vsize: 121768
[startup+1110 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 110941 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29838 603 41 0 30401 0
vsize: 121768
[startup+1120 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 111941 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29838 603 41 0 30401 0
vsize: 121768
[startup+1130 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 112941 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29838 603 41 0 30401 0
vsize: 121768
[startup+1140 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 113941 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29838 603 41 0 30401 0
vsize: 121768
[startup+1150 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 114942 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29838 603 41 0 30401 0
vsize: 121768
[startup+1160 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 115942 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223632 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30442 29838 603 41 0 30401 0
vsize: 121768
[startup+1170 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 116942 75 0 0 25 0 1 0 481402018 124600320 29825 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30420 29825 603 41 0 30379 0
vsize: 121680
[startup+1180 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 117942 75 0 0 25 0 1 0 481402018 124600320 29825 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30420 29825 603 41 0 30379 0
vsize: 121680
[startup+1190 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 118942 75 0 0 25 0 1 0 481402018 124600320 29825 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30420 29825 603 41 0 30379 0
vsize: 121680
[startup+1200 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28349
Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 119942 75 0 0 25 0 1 0 481402018 124600320 29825 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30420 29825 603 41 0 30379 0
vsize: 121680
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 28349
Raw data (stat): 28341 (minisat+) Z 28340 20838 20837 0 -1 12 29863 0 0 0 119943 80 0 0 25 0 1 0 481402018 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.05
CPU time (s): 1200.24
CPU user time (s): 1199.43
CPU system time (s): 0.809876
CPU usage (%): 100.015
Max. virtual memory (Kb): 121768
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####