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/een/normalized-nw04.opb
MD5SUM	c4c13764e2ea959929790d6ef6d0273c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
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	87482
Biggest coefficient in the objective function	5220
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	120189580
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	42031
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	120189580
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	18.0483
Number of variables	87482
Total number of constraints	72
Number of constraints which are clauses	36
Number of constraints which are cardinality constraints (but not clauses)	36
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	599
Maximum length of a constraint	42032
Trace number 7050

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-14 21:06:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5093 boxname=wulflinc27 idbench=392 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c4c13764e2ea959929790d6ef6d0273c  /oldhome/oroussel/tmp/wulflinc27/normalized-nw04.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc27/normalized-nw04.opb /oldhome/oroussel/tmp/wulflinc27/normalized-nw04.opb
IDLAUNCH: 5093
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        792464 kB
Buffers:         35680 kB
Cached:         168628 kB
SwapCached:       3160 kB
Active:         102656 kB
Inactive:       107572 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        792212 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            26316 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:26:33 (client local time) WITH STATUS 0 IN 1200.45 SECONDS
stats: 5093 7 1200.45 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 72 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ====================================
c   -- Clauses(.)/Splits(s): (none)
c ---[  70]---> Adder-cost: 1186   maxlim: 597   bits: 10/10
c ---[  68]---> Adder-cost: 200   maxlim: 597   bits: 10/10
c ---[  66]---> Adder-cost: 2388   maxlim: 1198   bits: 11/11
c ---[  64]---> Adder-cost: 9504   maxlim: 4756   bits: 13/13
c ---[  62]---> Adder-cost: 9988   maxlim: 5385   bits: 13/13
c ---[  60]---> Adder-cost: 9860   maxlim: 5446   bits: 13/13
c ---[  58]---> Adder-cost: 13298   maxlim: 6793   bits: 13/13
c ---[  56]---> Adder-cost: 13044   maxlim: 6968   bits: 13/13
c ---[  54]---> Adder-cost: 14006   maxlim: 7009   bits: 13/13
c ---[  52]---> Adder-cost: 16560   maxlim: 8425   bits: 14/14
c ---[  50]---> Adder-cost: 16936   maxlim: 8740   bits: 14/14
c ---[  48]---> Adder-cost: 18380   maxlim: 9842   bits: 14/14
c ---[  46]---> Adder-cost: 20892   maxlim: 11082   bits: 14/14
c ---[  44]---> Adder-cost: 21020   maxlim: 11282   bits: 14/14
c ---[  42]---> Adder-cost: 21350   maxlim: 11303   bits: 14/14
c ---[  40]---> Adder-cost: 21046   maxlim: 11395   bits: 14/14
c ---[  38]---> Adder-cost: 21750   maxlim: 11516   bits: 14/14
c ---[  36]---> Adder-cost: 18642   maxlim: 11899   bits: 14/14
c ---[  34]---> Adder-cost: 27430   maxlim: 16016   bits: 14/14
c ---[  32]---> Adder-cost: 26458   maxlim: 16389   bits: 15/15
c ---[  30]---> Adder-cost: 26712   maxlim: 17424   bits: 15/15
c ---[  28]---> Adder-cost: 27698   maxlim: 18484   bits: 15/15
c ---[  26]---> Adder-cost: 35438   maxlim: 21705   bits: 15/15
c ---[  24]---> Adder-cost: 39952   maxlim: 25219   bits: 15/15
c ---[  22]---> Adder-cost: 41450   maxlim: 26304   bits: 15/15
c ---[  20]---> Adder-cost: 41272   maxlim: 26866   bits: 15/15
c ---[  18]---> Adder-cost: 41376   maxlim: 27138   bits: 15/15
c ---[  16]---> Adder-cost: 42948   maxlim: 28017   bits: 15/15
c ---[  14]---> Adder-cost: 37688   maxlim: 28365   bits: 15/15
c ---[  12]---> Adder-cost: 45880   maxlim: 29223   bits: 15/15
c ---[  10]---> Adder-cost: 64458   maxlim: 35471   bits: 16/16
c ---[   8]---> Adder-cost: 50662   maxlim: 35553   bits: 16/16
c ---[   6]---> Adder-cost: 63386   maxlim: 35596   bits: 16/16
c ---[   4]---> Adder-cost: 60590   maxlim: 35617   bits: 16/16
c ---[   2]---> Adder-cost: 50528   maxlim: 36944   bits: 16/16
c ---[   0]---> Adder-cost: 52578   maxlim: 42030   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 7182627 25652125 | 2394209       0        0     nan |  0.000 % |
c |       100 | 7182610 25652066 | 2633629      97      298     3.1 |  0.039 % |
c |       250 | 7180880 25645873 | 2896992      22       65     3.0 |  0.065 % |
c |       475 | 7179674 25641561 | 3186692      76      230     3.0 |  0.083 % |
c |       812 | 7177579 25634182 | 3505361     110      344     3.1 |  0.114 % |
c |      1318 | 7174447 25623030 | 3855897     184      562     3.1 |  0.161 % |
#### 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.77 0.93 0.87 2/54 29058
Raw data (stat): 29058 (runsolver) R 29057 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487699388 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.80 0.93 0.87 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 36822 0 0 0 907 91 0 0 25 0 1 0 487699388 64593920 14470 4294967295 134512640 134672761 3221224576 3221223036 134542792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15770 14470 603 41 0 15729 0
vsize: 63080
[startup+20.0024 s]
Raw data (loadavg): 0.83 0.93 0.87 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 80204 0 0 0 1809 189 0 0 25 0 1 0 487699388 249430016 57852 4294967295 134512640 134672761 3221224576 3221218016 134526793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60896 57853 603 41 0 60855 0
vsize: 243584
[startup+30.0023 s]
Raw data (loadavg): 0.86 0.93 0.87 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 122865 0 0 0 2709 289 0 0 25 0 1 0 487699388 438530048 100513 4294967295 134512640 134672761 3221224576 3221218752 134526651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107063 100514 603 41 0 107022 0
vsize: 428252
[startup+40.0031 s]
Raw data (loadavg): 0.88 0.93 0.87 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 3666 333 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223792 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+50.0042 s]
Raw data (loadavg): 0.90 0.93 0.87 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 4665 334 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+60.0047 s]
Raw data (loadavg): 0.91 0.94 0.87 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 5665 334 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223792 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+70.0046 s]
Raw data (loadavg): 0.93 0.94 0.87 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 6665 334 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+80.0044 s]
Raw data (loadavg): 0.94 0.94 0.88 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 7665 335 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+90.0052 s]
Raw data (loadavg): 0.95 0.94 0.88 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 8665 335 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+100.005 s]
Raw data (loadavg): 0.95 0.94 0.88 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 9664 336 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556664 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+110.006 s]
Raw data (loadavg): 0.96 0.94 0.88 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 10664 336 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+120.007 s]
Raw data (loadavg): 0.97 0.95 0.88 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 11664 336 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+130.006 s]
Raw data (loadavg): 0.97 0.95 0.88 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 12664 337 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.88 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 13664 337 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223792 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.88 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 14664 337 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+160.009 s]
Raw data (loadavg): 0.98 0.95 0.88 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 15664 337 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+170.009 s]
Raw data (loadavg): 0.98 0.95 0.88 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 16664 337 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+180.01 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 17664 338 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+190.01 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 18664 338 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+200.01 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 19664 338 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+210.011 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 20663 339 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+220.012 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 21663 339 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223768 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+230.012 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 22663 339 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+240.013 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 23663 339 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+250.013 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 24663 340 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+260.014 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 25663 340 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+270.014 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 26663 340 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+280.014 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 27663 340 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+290.015 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 28663 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+300.014 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 29663 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+310.015 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 30664 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+320.016 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 31664 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 32664 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 33664 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 34664 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 35665 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 36665 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 37665 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 38665 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 39665 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 40666 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 41666 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 42666 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223792 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 43666 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 44666 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 45667 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223768 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 46667 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 47667 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139761 0 0 0 48667 341 0 0 25 0 1 0 487699388 554643456 117377 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135411 117377 603 41 0 135370 0
vsize: 541644
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139764 0 0 0 49667 341 0 0 25 0 1 0 487699388 554790912 117380 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117380 603 41 0 135406 0
vsize: 541788
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139764 0 0 0 50667 341 0 0 25 0 1 0 487699388 554790912 117380 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117380 603 41 0 135406 0
vsize: 541788
[startup+520.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139764 0 0 0 51668 341 0 0 25 0 1 0 487699388 554790912 117380 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117380 603 41 0 135406 0
vsize: 541788
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139764 0 0 0 52668 341 0 0 25 0 1 0 487699388 554790912 117380 4294967295 134512640 134672761 3221224576 3221223792 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117380 603 41 0 135406 0
vsize: 541788
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139764 0 0 0 53668 341 0 0 25 0 1 0 487699388 554790912 117380 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117380 603 41 0 135406 0
vsize: 541788
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139764 0 0 0 54668 341 0 0 25 0 1 0 487699388 554790912 117380 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117380 603 41 0 135406 0
vsize: 541788
[startup+560.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139765 0 0 0 55669 341 0 0 25 0 1 0 487699388 554790912 117381 4294967295 134512640 134672761 3221224576 3221223748 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117381 603 41 0 135406 0
vsize: 541788
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139776 0 0 0 56669 341 0 0 25 0 1 0 487699388 554790912 117392 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117392 603 41 0 135406 0
vsize: 541788
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139776 0 0 0 57669 341 0 0 25 0 1 0 487699388 554790912 117392 4294967295 134512640 134672761 3221224576 3221223748 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117392 603 41 0 135406 0
vsize: 541788
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139789 0 0 0 58669 341 0 0 25 0 1 0 487699388 554790912 117405 4294967295 134512640 134672761 3221224576 3221223748 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117405 603 41 0 135406 0
vsize: 541788
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139797 0 0 0 59669 341 0 0 25 0 1 0 487699388 554790912 117413 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135447 117413 603 41 0 135406 0
vsize: 541788
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139797 0 0 0 60669 341 0 0 25 0 1 0 487699388 554790912 117413 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135447 117413 603 41 0 135406 0
vsize: 541788
[startup+620.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139800 0 0 0 61669 341 0 0 25 0 1 0 487699388 554926080 117416 4294967295 134512640 134672761 3221224576 3221223772 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135480 117416 603 41 0 135439 0
vsize: 541920
[startup+630.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139805 0 0 0 62669 341 0 0 25 0 1 0 487699388 554926080 117421 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135480 117421 603 41 0 135439 0
vsize: 541920
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139806 0 0 0 63669 341 0 0 25 0 1 0 487699388 554926080 117422 4294967295 134512640 134672761 3221224576 3221223760 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135480 117422 603 41 0 135439 0
vsize: 541920
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139811 0 0 0 64669 341 0 0 25 0 1 0 487699388 554926080 117427 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135480 117427 603 41 0 135439 0
vsize: 541920
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139820 0 0 0 65670 341 0 0 25 0 1 0 487699388 554926080 117436 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135480 117436 603 41 0 135439 0
vsize: 541920
[startup+670.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139820 0 0 0 66670 341 0 0 25 0 1 0 487699388 554926080 117436 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135480 117436 603 41 0 135439 0
vsize: 541920
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139820 0 0 0 67670 341 0 0 25 0 1 0 487699388 554926080 117436 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135480 117436 603 41 0 135439 0
vsize: 541920
[startup+690.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139820 0 0 0 68670 341 0 0 25 0 1 0 487699388 554926080 117436 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135480 117436 603 41 0 135439 0
vsize: 541920
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139829 0 0 0 69670 341 0 0 25 0 1 0 487699388 555061248 117445 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135513 117445 603 41 0 135472 0
vsize: 542052
[startup+710.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139836 0 0 0 70670 341 0 0 25 0 1 0 487699388 555061248 117452 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135513 117452 603 41 0 135472 0
vsize: 542052
[startup+720.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139836 0 0 0 71671 341 0 0 25 0 1 0 487699388 555061248 117452 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135513 117452 603 41 0 135472 0
vsize: 542052
[startup+730.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139836 0 0 0 72671 341 0 0 25 0 1 0 487699388 555061248 117452 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135513 117452 603 41 0 135472 0
vsize: 542052
[startup+740.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139871 0 0 0 73671 341 0 0 25 0 1 0 487699388 555196416 117487 4294967295 134512640 134672761 3221224576 3221223748 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117487 603 41 0 135505 0
vsize: 542184
[startup+750.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139871 0 0 0 74671 341 0 0 25 0 1 0 487699388 555196416 117487 4294967295 134512640 134672761 3221224576 3221223792 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117487 603 41 0 135505 0
vsize: 542184
[startup+760.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139871 0 0 0 75671 341 0 0 25 0 1 0 487699388 555196416 117487 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117487 603 41 0 135505 0
vsize: 542184
[startup+770.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139872 0 0 0 76672 341 0 0 25 0 1 0 487699388 555196416 117488 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117488 603 41 0 135505 0
vsize: 542184
[startup+780.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139873 0 0 0 77672 341 0 0 25 0 1 0 487699388 555196416 117489 4294967295 134512640 134672761 3221224576 3221223792 134561950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117489 603 41 0 135505 0
vsize: 542184
[startup+790.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139873 0 0 0 78672 341 0 0 25 0 1 0 487699388 555196416 117489 4294967295 134512640 134672761 3221224576 3221223748 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117489 603 41 0 135505 0
vsize: 542184
[startup+800.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139873 0 0 0 79672 341 0 0 25 0 1 0 487699388 555196416 117489 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117489 603 41 0 135505 0
vsize: 542184
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139873 0 0 0 80672 341 0 0 25 0 1 0 487699388 555196416 117489 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117489 603 41 0 135505 0
vsize: 542184
[startup+820.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139875 0 0 0 81672 341 0 0 25 0 1 0 487699388 555196416 117491 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117491 603 41 0 135505 0
vsize: 542184
[startup+830.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139875 0 0 0 82673 341 0 0 25 0 1 0 487699388 555196416 117491 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117491 603 41 0 135505 0
vsize: 542184
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139875 0 0 0 83673 341 0 0 25 0 1 0 487699388 555196416 117491 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117491 603 41 0 135505 0
vsize: 542184
[startup+850.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139889 0 0 0 84673 341 0 0 25 0 1 0 487699388 555196416 117505 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117505 603 41 0 135505 0
vsize: 542184
[startup+860.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139889 0 0 0 85673 341 0 0 25 0 1 0 487699388 555196416 117505 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117505 603 41 0 135505 0
vsize: 542184
[startup+870.034 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139889 0 0 0 86673 341 0 0 25 0 1 0 487699388 555196416 117505 4294967295 134512640 134672761 3221224576 3221223776 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117505 603 41 0 135505 0
vsize: 542184
[startup+880.033 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139889 0 0 0 87673 341 0 0 25 0 1 0 487699388 555196416 117505 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117505 603 41 0 135505 0
vsize: 542184
[startup+890.034 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139891 0 0 0 88674 341 0 0 25 0 1 0 487699388 555196416 117507 4294967295 134512640 134672761 3221224576 3221223792 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117507 603 41 0 135505 0
vsize: 542184
[startup+900.035 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139895 0 0 0 89674 341 0 0 25 0 1 0 487699388 555196416 117511 4294967295 134512640 134672761 3221224576 3221223792 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117511 603 41 0 135505 0
vsize: 542184
[startup+910.035 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139895 0 0 0 90674 341 0 0 25 0 1 0 487699388 555196416 117511 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117511 603 41 0 135505 0
vsize: 542184
[startup+920.035 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139895 0 0 0 91674 341 0 0 25 0 1 0 487699388 555196416 117511 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135546 117511 603 41 0 135505 0
vsize: 542184
[startup+930.034 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139897 0 0 0 92674 341 0 0 25 0 1 0 487699388 555331584 117513 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135579 117513 603 41 0 135538 0
vsize: 542316
[startup+940.035 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139898 0 0 0 93675 341 0 0 25 0 1 0 487699388 555331584 117514 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135579 117514 603 41 0 135538 0
vsize: 542316
[startup+950.035 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139901 0 0 0 94675 341 0 0 25 0 1 0 487699388 555331584 117517 4294967295 134512640 134672761 3221224576 3221223792 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135579 117517 603 41 0 135538 0
vsize: 542316
[startup+960.035 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139924 0 0 0 95675 341 0 0 25 0 1 0 487699388 555331584 117540 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135579 117540 603 41 0 135538 0
vsize: 542316
[startup+970.036 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 139924 0 0 0 96675 341 0 0 25 0 1 0 487699388 555331584 117540 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135579 117540 603 41 0 135538 0
vsize: 542316
[startup+980.036 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140083 0 0 0 97675 342 0 0 25 0 1 0 487699388 556040192 117699 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135752 117699 603 41 0 135711 0
vsize: 543008
[startup+990.036 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140091 0 0 0 98675 342 0 0 25 0 1 0 487699388 556040192 117707 4294967295 134512640 134672761 3221224576 3221223748 134556658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135752 117707 603 41 0 135711 0
vsize: 543008
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140108 0 0 0 99675 342 0 0 25 0 1 0 487699388 556175360 117724 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135785 117724 603 41 0 135744 0
vsize: 543140
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140134 0 0 0 100675 342 0 0 25 0 1 0 487699388 556310528 117750 4294967295 134512640 134672761 3221224576 3221223748 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135818 117750 603 41 0 135777 0
vsize: 543272
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140143 0 0 0 101675 342 0 0 25 0 1 0 487699388 556310528 117759 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135818 117759 603 41 0 135777 0
vsize: 543272
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140160 0 0 0 102675 342 0 0 25 0 1 0 487699388 556310528 117776 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135818 117776 603 41 0 135777 0
vsize: 543272
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140210 0 0 0 103675 342 0 0 25 0 1 0 487699388 556580864 117826 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135884 117826 603 41 0 135843 0
vsize: 543536
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140230 0 0 0 104675 342 0 0 25 0 1 0 487699388 556580864 117846 4294967295 134512640 134672761 3221224576 3221223760 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135884 117846 603 41 0 135843 0
vsize: 543536
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140230 0 0 0 105676 342 0 0 25 0 1 0 487699388 556580864 117846 4294967295 134512640 134672761 3221224576 3221223792 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135884 117846 603 41 0 135843 0
vsize: 543536
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140266 0 0 0 106676 342 0 0 25 0 1 0 487699388 556851200 117882 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135950 117882 603 41 0 135909 0
vsize: 543800
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140266 0 0 0 107676 342 0 0 25 0 1 0 487699388 556851200 117882 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135950 117882 603 41 0 135909 0
vsize: 543800
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140266 0 0 0 108676 342 0 0 25 0 1 0 487699388 556851200 117882 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135950 117882 603 41 0 135909 0
vsize: 543800
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140285 0 0 0 109677 342 0 0 25 0 1 0 487699388 556851200 117901 4294967295 134512640 134672761 3221224576 3221223764 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135950 117901 603 41 0 135909 0
vsize: 543800
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140285 0 0 0 110677 342 0 0 25 0 1 0 487699388 556851200 117901 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135950 117901 603 41 0 135909 0
vsize: 543800
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140285 0 0 0 111677 342 0 0 25 0 1 0 487699388 556851200 117901 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135950 117901 603 41 0 135909 0
vsize: 543800
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140318 0 0 0 112677 342 0 0 25 0 1 0 487699388 556986368 117934 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135983 117934 603 41 0 135942 0
vsize: 543932
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140352 0 0 0 113677 342 0 0 25 0 1 0 487699388 557121536 117968 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136016 117968 603 41 0 135975 0
vsize: 544064
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140407 0 0 0 114677 342 0 0 25 0 1 0 487699388 557391872 118023 4294967295 134512640 134672761 3221224576 3221223792 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136082 118023 603 41 0 136041 0
vsize: 544328
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140407 0 0 0 115677 342 0 0 25 0 1 0 487699388 557391872 118023 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136082 118023 603 41 0 136041 0
vsize: 544328
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140408 0 0 0 116678 342 0 0 25 0 1 0 487699388 557391872 118024 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136082 118024 603 41 0 136041 0
vsize: 544328
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140408 0 0 0 117678 342 0 0 25 0 1 0 487699388 557391872 118024 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136082 118024 603 41 0 136041 0
vsize: 544328
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140408 0 0 0 118678 342 0 0 25 0 1 0 487699388 557391872 118024 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136082 118024 603 41 0 136041 0
vsize: 544328
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29058
Raw data (stat): 29058 (minisat+) R 29057 18865 18864 0 -1 0 140431 0 0 0 119678 343 0 0 25 0 1 0 487699388 557527040 118047 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136115 118047 603 41 0 136074 0
vsize: 544460
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.28 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 29058
Raw data (stat): 29058 (minisat+) Z 29057 18865 18864 0 -1 12 140433 0 0 0 119678 366 0 0 25 0 1 0 487699388 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.28
CPU time (s): 1200.45
CPU user time (s): 1196.79
CPU system time (s): 3.66344
CPU usage (%): 100.014
Max. virtual memory (Kb): 544460
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####