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/manquinho/synthesis-ptl-cmos-circuits/normalized-mux.opb
MD5SUM	fa7153262db792d01bec14f5a651af5b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	872
Optimality of the best value was proved	NO
Number of terms in the objective function	232
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	9597
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	9597
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.332949
Number of variables	232
Total number of constraints	527
Number of constraints which are clauses	527
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	27
Trace number 5210

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        909880 kB
Buffers:         34116 kB
Cached:          70856 kB
SwapCached:        564 kB
Active:          51056 kB
Inactive:        57308 kB
HighTotal:      131008 kB
HighFree:        56280 kB
LowTotal:       903652 kB
LowFree:        853600 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10780 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:51:50 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 3638 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 527 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     527     2331 |     175       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1330[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1160   maxlim: 8267   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8555    31002 |    2851       0        0     nan |  0.000 % |
c |       100 |    8539    30950 |    3136      98      346     3.5 |  0.934 % |
c |       252 |    8539    30950 |    3449     250     1158     4.6 |  0.933 % |
c |       477 |    8539    30950 |    3794     475     2561     5.4 |  0.933 % |
c |       814 |    8539    30950 |    4174     812     5406     6.7 |  0.933 % |
c |      1320 |    8539    30950 |    4591    1318    12348     9.4 |  0.933 % |
c |      2079 |    8539    30950 |    5050    2077    38213    18.4 |  0.933 % |
c |      3219 |    8539    30950 |    5555    3217    87428    27.2 |  0.933 % |
c |      4930 |    8501    30844 |    6111    4923   145420    29.5 |  1.077 % |
c |      7492 |    8501    30844 |    6722    4248   224412    52.8 |  1.077 % |
c |     11339 |    8501    30844 |    7394    4537   239991    52.9 |  1.077 % |
c |     17105 |    8501    30844 |    8134    6464   326331    50.5 |  1.077 % |
c |     25755 |    8501    30844 |    8947    6637   399620    60.2 |  1.077 % |
c |     38730 |    8501    30844 |    9842    5801   475685    82.0 |  1.077 % |
c |     58192 |    8501    30844 |   10826    9906   693997    70.1 |  1.077 % |
c |     87384 |    8501    30844 |   11909   11379   960106    84.4 |  1.077 % |
c |    131174 |    8501    30844 |   13100   11884  1083748    91.2 |  1.077 % |
c |    196858 |    8501    30844 |   14410   10153   738369    72.7 |  1.077 % |
c |    295385 |    8501    30844 |   15851   12788  1092240    85.4 |  1.077 % |
c |    443175 |    8501    30844 |   17436   14776  1099768    74.4 |  1.077 % |
c |    664858 |    8501    30844 |   19180   14441  1170497    81.1 |  1.077 % |
c |    997384 |    8501    30844 |   21098   14478  1173786    81.1 |  1.077 % |
#### 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/54 962
Raw data (stat): 962 (runsolver) R 961 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421351073 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 1096 0 0 0 996 2 0 0 25 0 1 0 421351073 6127616 1074 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1496 1074 603 41 0 1455 0
vsize: 5984
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 1274 0 0 0 1995 3 0 0 25 0 1 0 421351073 6795264 1252 4294967295 134512640 134672761 3221224576 3221223760 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1659 1252 603 41 0 1618 0
vsize: 6636
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 1558 0 0 0 2994 4 0 0 25 0 1 0 421351073 8007680 1536 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1955 1536 603 41 0 1914 0
vsize: 7820
[startup+40.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 1561 0 0 0 3994 4 0 0 25 0 1 0 421351073 8007680 1539 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1955 1539 603 41 0 1914 0
vsize: 7820
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 1565 0 0 0 4994 4 0 0 25 0 1 0 421351073 8007680 1543 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1955 1543 603 41 0 1914 0
vsize: 7820
[startup+60.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 1803 0 0 0 5994 5 0 0 25 0 1 0 421351073 8945664 1781 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2184 1781 603 41 0 2143 0
vsize: 8736
[startup+70.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 1937 0 0 0 6993 5 0 0 25 0 1 0 421351073 9478144 1915 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2314 1915 603 41 0 2273 0
vsize: 9256
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 1983 0 0 0 7992 6 0 0 25 0 1 0 421351073 9744384 1961 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2379 1961 603 41 0 2338 0
vsize: 9516
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2080 0 0 0 8991 7 0 0 25 0 1 0 421351073 10162176 2058 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2481 2058 603 41 0 2440 0
vsize: 9924
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2169 0 0 0 9991 7 0 0 25 0 1 0 421351073 10432512 2147 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2547 2147 603 41 0 2506 0
vsize: 10188
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2170 0 0 0 10991 7 0 0 25 0 1 0 421351073 10432512 2148 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2547 2148 603 41 0 2506 0
vsize: 10188
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2170 0 0 0 11992 7 0 0 25 0 1 0 421351073 10432512 2148 4294967295 134512640 134672761 3221224576 3221223760 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2547 2148 603 41 0 2506 0
vsize: 10188
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2331 0 0 0 12992 7 0 0 25 0 1 0 421351073 11120640 2309 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2715 2309 603 41 0 2674 0
vsize: 10860
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2343 0 0 0 13992 7 0 0 25 0 1 0 421351073 11255808 2321 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2748 2321 603 41 0 2707 0
vsize: 10992
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2347 0 0 0 14992 7 0 0 25 0 1 0 421351073 11255808 2325 4294967295 134512640 134672761 3221224576 3221223760 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2748 2325 603 41 0 2707 0
vsize: 10992
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2417 0 0 0 15992 7 0 0 25 0 1 0 421351073 11546624 2395 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2819 2395 603 41 0 2778 0
vsize: 11276
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2418 0 0 0 16992 7 0 0 25 0 1 0 421351073 11546624 2396 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2819 2396 603 41 0 2778 0
vsize: 11276
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2419 0 0 0 17991 7 0 0 25 0 1 0 421351073 11546624 2397 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2819 2397 603 41 0 2778 0
vsize: 11276
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2463 0 0 0 18991 7 0 0 25 0 1 0 421351073 11677696 2441 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2851 2441 603 41 0 2810 0
vsize: 11404
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2481 0 0 0 19991 7 0 0 25 0 1 0 421351073 11812864 2459 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2884 2459 603 41 0 2843 0
vsize: 11536
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2481 0 0 0 20991 7 0 0 25 0 1 0 421351073 11812864 2459 4294967295 134512640 134672761 3221224576 3221223744 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2884 2459 603 41 0 2843 0
vsize: 11536
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2489 0 0 0 21991 7 0 0 25 0 1 0 421351073 11812864 2467 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2884 2467 603 41 0 2843 0
vsize: 11536
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2495 0 0 0 22991 7 0 0 25 0 1 0 421351073 11812864 2473 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2884 2473 603 41 0 2843 0
vsize: 11536
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2627 0 0 0 23991 8 0 0 25 0 1 0 421351073 12353536 2605 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3016 2605 603 41 0 2975 0
vsize: 12064
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2691 0 0 0 24991 8 0 0 25 0 1 0 421351073 12619776 2669 4294967295 134512640 134672761 3221224576 3221223744 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3081 2669 603 41 0 3040 0
vsize: 12324
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2714 0 0 0 25992 8 0 0 25 0 1 0 421351073 12754944 2692 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3114 2692 603 41 0 3073 0
vsize: 12456
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2722 0 0 0 26992 8 0 0 25 0 1 0 421351073 12754944 2700 4294967295 134512640 134672761 3221224576 3221223712 134565039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3114 2700 603 41 0 3073 0
vsize: 12456
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2722 0 0 0 27991 8 0 0 25 0 1 0 421351073 12754944 2700 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3114 2700 603 41 0 3073 0
vsize: 12456
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2727 0 0 0 28992 8 0 0 25 0 1 0 421351073 12906496 2705 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3151 2705 603 41 0 3110 0
vsize: 12604
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2727 0 0 0 29993 8 0 0 25 0 1 0 421351073 12906496 2705 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3151 2705 603 41 0 3110 0
vsize: 12604
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2741 0 0 0 30993 8 0 0 25 0 1 0 421351073 12906496 2719 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3151 2719 603 41 0 3110 0
vsize: 12604
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2755 0 0 0 31993 8 0 0 25 0 1 0 421351073 12906496 2733 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3151 2733 603 41 0 3110 0
vsize: 12604
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2759 0 0 0 32993 8 0 0 25 0 1 0 421351073 13053952 2737 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3187 2737 603 41 0 3146 0
vsize: 12748
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2779 0 0 0 33993 8 0 0 25 0 1 0 421351073 13053952 2757 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3187 2757 603 41 0 3146 0
vsize: 12748
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2792 0 0 0 34993 8 0 0 25 0 1 0 421351073 13201408 2770 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3223 2770 603 41 0 3182 0
vsize: 12892
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2797 0 0 0 35994 8 0 0 25 0 1 0 421351073 13201408 2775 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3223 2775 603 41 0 3182 0
vsize: 12892
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2803 0 0 0 36994 8 0 0 25 0 1 0 421351073 13201408 2781 4294967295 134512640 134672761 3221224576 3221223760 134559188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3223 2781 603 41 0 3182 0
vsize: 12892
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2803 0 0 0 37994 8 0 0 25 0 1 0 421351073 13201408 2781 4294967295 134512640 134672761 3221224576 3221223712 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3223 2781 603 41 0 3182 0
vsize: 12892
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2850 0 0 0 38994 8 0 0 25 0 1 0 421351073 13471744 2828 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3289 2828 603 41 0 3248 0
vsize: 13156
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2881 0 0 0 39994 8 0 0 25 0 1 0 421351073 13664256 2859 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3336 2859 603 41 0 3295 0
vsize: 13344
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2881 0 0 0 40994 8 0 0 25 0 1 0 421351073 13664256 2859 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3336 2859 603 41 0 3295 0
vsize: 13344
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2881 0 0 0 41995 8 0 0 25 0 1 0 421351073 13664256 2859 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3336 2859 603 41 0 3295 0
vsize: 13344
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 2921 0 0 0 42994 9 0 0 25 0 1 0 421351073 13795328 2899 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3368 2899 603 41 0 3327 0
vsize: 13472
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3088 0 0 0 43994 9 0 0 25 0 1 0 421351073 14471168 3066 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3533 3066 603 41 0 3492 0
vsize: 14132
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3244 0 0 0 44994 9 0 0 25 0 1 0 421351073 15142912 3222 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3697 3222 603 41 0 3656 0
vsize: 14788
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3264 0 0 0 45994 9 0 0 25 0 1 0 421351073 15142912 3242 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3697 3242 603 41 0 3656 0
vsize: 14788
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3265 0 0 0 46994 9 0 0 25 0 1 0 421351073 15142912 3243 4294967295 134512640 134672761 3221224576 3221223648 134553557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3697 3243 603 41 0 3656 0
vsize: 14788
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3265 0 0 0 47994 9 0 0 25 0 1 0 421351073 15142912 3243 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3697 3243 603 41 0 3656 0
vsize: 14788
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3265 0 0 0 48995 9 0 0 25 0 1 0 421351073 15142912 3243 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3697 3243 603 41 0 3656 0
vsize: 14788
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3265 0 0 0 49995 9 0 0 25 0 1 0 421351073 15142912 3243 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3697 3243 603 41 0 3656 0
vsize: 14788
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3271 0 0 0 50995 9 0 0 25 0 1 0 421351073 15142912 3249 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3697 3249 603 41 0 3656 0
vsize: 14788
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3277 0 0 0 51995 9 0 0 25 0 1 0 421351073 15298560 3255 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3735 3255 603 41 0 3694 0
vsize: 14940
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3283 0 0 0 52995 9 0 0 25 0 1 0 421351073 15298560 3261 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3735 3261 603 41 0 3694 0
vsize: 14940
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3283 0 0 0 53995 9 0 0 25 0 1 0 421351073 15298560 3261 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3735 3261 603 41 0 3694 0
vsize: 14940
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3283 0 0 0 54996 9 0 0 25 0 1 0 421351073 15298560 3261 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3735 3261 603 41 0 3694 0
vsize: 14940
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3283 0 0 0 55996 9 0 0 25 0 1 0 421351073 15298560 3261 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3735 3261 603 41 0 3694 0
vsize: 14940
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3283 0 0 0 56996 9 0 0 25 0 1 0 421351073 15298560 3261 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3735 3261 603 41 0 3694 0
vsize: 14940
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3305 0 0 0 57996 9 0 0 25 0 1 0 421351073 15298560 3283 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3735 3283 603 41 0 3694 0
vsize: 14940
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3338 0 0 0 58996 10 0 0 25 0 1 0 421351073 15433728 3316 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3768 3316 603 41 0 3727 0
vsize: 15072
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3340 0 0 0 59996 10 0 0 25 0 1 0 421351073 15577088 3318 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3803 3318 603 41 0 3762 0
vsize: 15212
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3345 0 0 0 60997 10 0 0 25 0 1 0 421351073 15577088 3323 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3803 3323 603 41 0 3762 0
vsize: 15212
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3345 0 0 0 61997 10 0 0 25 0 1 0 421351073 15577088 3323 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3803 3323 603 41 0 3762 0
vsize: 15212
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3350 0 0 0 62997 10 0 0 25 0 1 0 421351073 15577088 3328 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3803 3328 603 41 0 3762 0
vsize: 15212
[startup+640.023 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3355 0 0 0 63997 10 0 0 25 0 1 0 421351073 15577088 3333 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3803 3333 603 41 0 3762 0
vsize: 15212
[startup+650.023 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3355 0 0 0 64997 10 0 0 25 0 1 0 421351073 15577088 3333 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3803 3333 603 41 0 3762 0
vsize: 15212
[startup+660.023 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3398 0 0 0 65997 10 0 0 25 0 1 0 421351073 15847424 3376 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3376 603 41 0 3828 0
vsize: 15476
[startup+670.024 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3398 0 0 0 66998 10 0 0 25 0 1 0 421351073 15847424 3376 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3376 603 41 0 3828 0
vsize: 15476
[startup+680.024 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3398 0 0 0 67998 10 0 0 25 0 1 0 421351073 15847424 3376 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3376 603 41 0 3828 0
vsize: 15476
[startup+690.025 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3400 0 0 0 68997 10 0 0 25 0 1 0 421351073 15847424 3378 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3378 603 41 0 3828 0
vsize: 15476
[startup+700.025 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3400 0 0 0 69997 10 0 0 25 0 1 0 421351073 15847424 3378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3378 603 41 0 3828 0
vsize: 15476
[startup+710.025 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3634 0 0 0 70997 11 0 0 25 0 1 0 421351073 16785408 3612 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3612 603 41 0 4057 0
vsize: 16392
[startup+720.025 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3703 0 0 0 71997 11 0 0 25 0 1 0 421351073 17051648 3681 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4163 3681 603 41 0 4122 0
vsize: 16652
[startup+730.024 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3738 0 0 0 72997 11 0 0 25 0 1 0 421351073 17186816 3716 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4196 3716 603 41 0 4155 0
vsize: 16784
[startup+740.026 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3745 0 0 0 73997 11 0 0 25 0 1 0 421351073 17186816 3723 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4196 3723 603 41 0 4155 0
vsize: 16784
[startup+750.025 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3745 0 0 0 74997 11 0 0 25 0 1 0 421351073 17186816 3723 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4196 3723 603 41 0 4155 0
vsize: 16784
[startup+760.026 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3750 0 0 0 75997 11 0 0 25 0 1 0 421351073 17186816 3728 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4196 3728 603 41 0 4155 0
vsize: 16784
[startup+770.026 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3760 0 0 0 76997 11 0 0 25 0 1 0 421351073 17338368 3738 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4233 3738 603 41 0 4192 0
vsize: 16932
[startup+780.026 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3761 0 0 0 77998 11 0 0 25 0 1 0 421351073 17338368 3739 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4233 3739 603 41 0 4192 0
vsize: 16932
[startup+790.026 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3761 0 0 0 78998 11 0 0 25 0 1 0 421351073 17338368 3739 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4233 3739 603 41 0 4192 0
vsize: 16932
[startup+800.026 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3761 0 0 0 79998 11 0 0 25 0 1 0 421351073 17338368 3739 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4233 3739 603 41 0 4192 0
vsize: 16932
[startup+810.027 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3761 0 0 0 80998 11 0 0 25 0 1 0 421351073 17338368 3739 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4233 3739 603 41 0 4192 0
vsize: 16932
[startup+820.027 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3811 0 0 0 81998 11 0 0 25 0 1 0 421351073 17473536 3789 4294967295 134512640 134672761 3221224576 3221223760 134559351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4266 3789 603 41 0 4225 0
vsize: 17064
[startup+830.027 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3825 0 0 0 82998 11 0 0 25 0 1 0 421351073 17620992 3803 4294967295 134512640 134672761 3221224576 3221222896 134565757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4302 3803 603 41 0 4261 0
vsize: 17208
[startup+840.027 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3825 0 0 0 83999 11 0 0 25 0 1 0 421351073 17620992 3803 4294967295 134512640 134672761 3221224576 3221223680 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4302 3803 603 41 0 4261 0
vsize: 17208
[startup+850.028 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3909 0 0 0 84999 11 0 0 25 0 1 0 421351073 17891328 3887 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4368 3887 603 41 0 4327 0
vsize: 17472
[startup+860.028 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3970 0 0 0 85999 12 0 0 25 0 1 0 421351073 18178048 3948 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3948 603 41 0 4397 0
vsize: 17752
[startup+870.028 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3970 0 0 0 86999 12 0 0 25 0 1 0 421351073 18178048 3948 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3948 603 41 0 4397 0
vsize: 17752
[startup+880.027 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3970 0 0 0 87999 12 0 0 25 0 1 0 421351073 18178048 3948 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3948 603 41 0 4397 0
vsize: 17752
[startup+890.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3970 0 0 0 88999 12 0 0 25 0 1 0 421351073 18178048 3948 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3948 603 41 0 4397 0
vsize: 17752
[startup+900.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3970 0 0 0 89999 12 0 0 25 0 1 0 421351073 18178048 3948 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3948 603 41 0 4397 0
vsize: 17752
[startup+910.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3970 0 0 0 90999 12 0 0 25 0 1 0 421351073 18178048 3948 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3948 603 41 0 4397 0
vsize: 17752
[startup+920.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3970 0 0 0 92000 12 0 0 25 0 1 0 421351073 18178048 3948 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3948 603 41 0 4397 0
vsize: 17752
[startup+930.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3970 0 0 0 93000 12 0 0 25 0 1 0 421351073 18178048 3948 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3948 603 41 0 4397 0
vsize: 17752
[startup+940.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3970 0 0 0 94000 12 0 0 25 0 1 0 421351073 18178048 3948 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3948 603 41 0 4397 0
vsize: 17752
[startup+950.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3970 0 0 0 95000 12 0 0 25 0 1 0 421351073 18178048 3948 4294967295 134512640 134672761 3221224576 3221223760 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3948 603 41 0 4397 0
vsize: 17752
[startup+960.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 3971 0 0 0 96001 12 0 0 25 0 1 0 421351073 18178048 3949 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3949 603 41 0 4397 0
vsize: 17752
[startup+970.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4016 0 0 0 97001 12 0 0 25 0 1 0 421351073 18313216 3994 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4471 3994 603 41 0 4430 0
vsize: 17884
[startup+980.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4016 0 0 0 98001 12 0 0 25 0 1 0 421351073 18313216 3994 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4471 3994 603 41 0 4430 0
vsize: 17884
[startup+990.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4054 0 0 0 99001 12 0 0 25 0 1 0 421351073 18448384 4032 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4504 4032 603 41 0 4463 0
vsize: 18016
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4054 0 0 0 100001 12 0 0 25 0 1 0 421351073 18448384 4032 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4504 4032 603 41 0 4463 0
vsize: 18016
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4058 0 0 0 101001 12 0 0 25 0 1 0 421351073 18604032 4036 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4542 4036 603 41 0 4501 0
vsize: 18168
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4068 0 0 0 102002 12 0 0 25 0 1 0 421351073 18604032 4046 4294967295 134512640 134672761 3221224576 3221223760 134559625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4542 4046 603 41 0 4501 0
vsize: 18168
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4109 0 0 0 103002 12 0 0 25 0 1 0 421351073 18735104 4087 4294967295 134512640 134672761 3221224576 3221223776 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4574 4087 603 41 0 4533 0
vsize: 18296
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4128 0 0 0 104002 12 0 0 25 0 1 0 421351073 18878464 4106 4294967295 134512640 134672761 3221224576 3221223744 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4609 4106 603 41 0 4568 0
vsize: 18436
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4128 0 0 0 105002 12 0 0 25 0 1 0 421351073 18878464 4106 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4609 4106 603 41 0 4568 0
vsize: 18436
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4128 0 0 0 106002 12 0 0 25 0 1 0 421351073 18878464 4106 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4609 4106 603 41 0 4568 0
vsize: 18436
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4139 0 0 0 107002 12 0 0 25 0 1 0 421351073 19042304 4117 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4117 603 41 0 4608 0
vsize: 18596
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4139 0 0 0 108002 12 0 0 25 0 1 0 421351073 19042304 4117 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4117 603 41 0 4608 0
vsize: 18596
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4139 0 0 0 109003 12 0 0 25 0 1 0 421351073 19042304 4117 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4117 603 41 0 4608 0
vsize: 18596
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4139 0 0 0 110003 12 0 0 25 0 1 0 421351073 19042304 4117 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4117 603 41 0 4608 0
vsize: 18596
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4139 0 0 0 111003 12 0 0 25 0 1 0 421351073 19042304 4117 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4117 603 41 0 4608 0
vsize: 18596
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4139 0 0 0 112003 12 0 0 25 0 1 0 421351073 19042304 4117 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4117 603 41 0 4608 0
vsize: 18596
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4139 0 0 0 113003 12 0 0 25 0 1 0 421351073 19042304 4117 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4117 603 41 0 4608 0
vsize: 18596
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4139 0 0 0 114003 12 0 0 25 0 1 0 421351073 19042304 4117 4294967295 134512640 134672761 3221224576 3221223744 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4117 603 41 0 4608 0
vsize: 18596
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4141 0 0 0 115003 12 0 0 25 0 1 0 421351073 19042304 4119 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4119 603 41 0 4608 0
vsize: 18596
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4141 0 0 0 116003 12 0 0 25 0 1 0 421351073 19042304 4119 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4119 603 41 0 4608 0
vsize: 18596
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4142 0 0 0 117004 13 0 0 25 0 1 0 421351073 19042304 4120 4294967295 134512640 134672761 3221224576 3221223760 134559367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4120 603 41 0 4608 0
vsize: 18596
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4147 0 0 0 118004 13 0 0 25 0 1 0 421351073 19042304 4125 4294967295 134512640 134672761 3221224576 3221223680 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 4125 603 41 0 4608 0
vsize: 18596
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4179 0 0 0 119004 13 0 0 25 0 1 0 421351073 19197952 4157 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4687 4157 603 41 0 4646 0
vsize: 18748
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 962
Raw data (stat): 962 (minisat+) R 961 30854 30853 0 -1 0 4226 0 0 0 120004 13 0 0 25 0 1 0 421351073 19361792 4204 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4727 4204 603 41 0 4686 0
vsize: 18908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 962
Raw data (stat): 962 (minisat+) Z 961 30854 30853 0 -1 12 4229 0 0 0 120004 14 0 0 25 0 1 0 421351073 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.19
CPU user time (s): 1200.04
CPU system time (s): 0.143978
CPU usage (%): 100.012
Max. virtual memory (Kb): 18908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####