PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl40_41_pb.cnf.cr.opb
MD5SUM	3c9e81ddaaf37dd621fe2bc839a3f27f
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	42
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.098984
Number of variables	3280
Total number of constraints	162
Number of constraints which are clauses	82
Number of constraints which are cardinality constraints (but not clauses)	80
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	40
Maximum length of a constraint	41
Trace number 5337

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 23:34:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3777 boxname=wulflinc31 idbench=17 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c9e81ddaaf37dd621fe2bc839a3f27f  /oldhome/oroussel/tmp/wulflinc31/normalized-chnl40_41_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc31/normalized-chnl40_41_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc31/normalized-chnl40_41_pb.cnf.cr.opb
IDLAUNCH: 3777
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        908232 kB
Buffers:         34772 kB
Cached:          53236 kB
SwapCached:        392 kB
Active:          50056 kB
Inactive:        41148 kB
HighTotal:      131008 kB
HighFree:        74004 kB
LowTotal:       903652 kB
LowFree:        834228 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29620 kB
Committed_AS:    63528 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:54:53 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 3777 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 162 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................
c ---[  79]---> BDD-cost:   79
c ---[  78]---> BDD-cost:   79
c ---[  77]---> BDD-cost:   79
c ---[  76]---> BDD-cost:   79
c ---[  75]---> BDD-cost:   79
c ---[  74]---> BDD-cost:   79
c ---[  73]---> BDD-cost:   79
c ---[  72]---> BDD-cost:   79
c ---[  71]---> BDD-cost:   79
c ---[  70]---> BDD-cost:   79
c ---[  69]---> BDD-cost:   79
c ---[  68]---> BDD-cost:   79
c ---[  67]---> BDD-cost:   79
c ---[  66]---> BDD-cost:   79
c ---[  65]---> BDD-cost:   79
c ---[  64]---> BDD-cost:   79
c ---[  63]---> BDD-cost:   79
c ---[  62]---> BDD-cost:   79
c ---[  61]---> BDD-cost:   79
c ---[  60]---> BDD-cost:   79
c ---[  59]---> BDD-cost:   79
c ---[  58]---> BDD-cost:   79
c ---[  57]---> BDD-cost:   79
c ---[  56]---> BDD-cost:   79
c ---[  55]---> BDD-cost:   79
c ---[  54]---> BDD-cost:   79
c ---[  53]---> BDD-cost:   79
c ---[  52]---> BDD-cost:   79
c ---[  51]---> BDD-cost:   79
c ---[  50]---> BDD-cost:   79
c ---[  49]---> BDD-cost:   79
c ---[  48]---> BDD-cost:   79
c ---[  47]---> BDD-cost:   79
c ---[  46]---> BDD-cost:   79
c ---[  45]---> BDD-cost:   79
c ---[  44]---> BDD-cost:   79
c ---[  43]---> BDD-cost:   79
c ---[  42]---> BDD-cost:   79
c ---[  41]---> BDD-cost:   79
c ---[  40]---> BDD-cost:   79
c ---[  39]---> BDD-cost:   79
c ---[  38]---> BDD-cost:   79
c ---[  37]---> BDD-cost:   79
c ---[  36]---> BDD-cost:   79
c ---[  35]---> BDD-cost:   79
c ---[  34]---> BDD-cost:   79
c ---[  33]---> BDD-cost:   79
c ---[  32]---> BDD-cost:   79
c ---[  31]---> BDD-cost:   79
c ---[  30]---> BDD-cost:   79
c ---[  29]---> BDD-cost:   79
c ---[  28]---> BDD-cost:   79
c ---[  27]---> BDD-cost:   79
c ---[  26]---> BDD-cost:   79
c ---[  25]---> BDD-cost:   79
c ---[  24]---> BDD-cost:   79
c ---[  23]---> BDD-cost:   79
c ---[  22]---> BDD-cost:   79
c ---[  21]---> BDD-cost:   79
c ---[  20]---> BDD-cost:   79
c ---[  19]---> BDD-cost:   79
c ---[  18]---> BDD-cost:   79
c ---[  17]---> BDD-cost:   79
c ---[  16]---> BDD-cost:   79
c ---[  15]---> BDD-cost:   79
c ---[  14]---> BDD-cost:   79
c ---[  13]---> BDD-cost:   79
c ---[  12]---> BDD-cost:   79
c ---[  11]---> BDD-cost:   79
c ---[  10]---> BDD-cost:   79
c ---[   9]---> BDD-cost:   79
c ---[   8]---> BDD-cost:   79
c ---[   7]---> BDD-cost:   79
c ---[   6]---> BDD-cost:   79
c ---[   5]---> BDD-cost:   79
c ---[   4]---> BDD-cost:   79
c ---[   3]---> BDD-cost:   79
c ---[   2]---> BDD-cost:   79
c ---[   1]---> BDD-cost:   79
c ---[   0]---> BDD-cost:   79
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   15762    44080 |    4728       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9520          
c   -- var.elim.:  2000/9520          
c   -- var.elim.:  3000/9520          
c   -- var.elim.:  4000/9520          
c   -- var.elim.:  5000/9520          
c   -- var.elim.:  6000/9520          
c   -- var.elim.:  7000/9520          
c   -- var.elim.:  8000/9520          
c   -- var.elim.:  9000/9520          
c   -- var.elim.:  9520/9520          
c   -- var.elim.:  1000/3616          
c   -- var.elim.:  2000/3616          
c   -- var.elim.:  3000/3616          
c   -- var.elim.:  3616/3616          
c   -- var.elim.:  166/166          
c   -- subsuming                       
c   -- var.elim.:  1000/2060          
c   -- var.elim.:  2000/2060          
c   -- var.elim.:  2060/2060          
c   -- var.elim.:  782/782          
c   -- var.elim.:  254/254          
c   -- var.elim.:  252/252          
c   -- var.elim.:  108/108          
c   -- var#### 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.84 0.94 0.90 2/54 26958
Raw data (stat): 26958 (runsolver) R 26957 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479937875 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0006 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 4034 0 0 0 987 11 0 0 25 0 1 0 479937875 18382848 3959 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4488 3959 603 41 0 4447 0
vsize: 17952
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 6097 0 0 0 1983 15 0 0 25 0 1 0 479937875 26742784 6022 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6529 6022 603 41 0 6488 0
vsize: 26116
[startup+30.0019 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 7339 0 0 0 2979 19 0 0 25 0 1 0 479937875 31907840 7264 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7790 7264 603 41 0 7749 0
vsize: 31160
[startup+40.0032 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 7339 0 0 0 3979 19 0 0 25 0 1 0 479937875 31907840 7264 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7790 7264 603 41 0 7749 0
vsize: 31160
[startup+50.0041 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 8292 0 0 0 4977 22 0 0 25 0 1 0 479937875 35848192 8217 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8752 8217 603 41 0 8711 0
vsize: 35008
[startup+60.0037 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 9139 0 0 0 5975 24 0 0 25 0 1 0 479937875 39284736 9064 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9591 9064 603 41 0 9550 0
vsize: 38364
[startup+70.0049 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 9392 0 0 0 6974 25 0 0 25 0 1 0 479937875 40312832 9317 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9842 9317 603 41 0 9801 0
vsize: 39368
[startup+80.0059 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 9392 0 0 0 7974 25 0 0 25 0 1 0 479937875 40312832 9317 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9842 9317 603 41 0 9801 0
vsize: 39368
[startup+90.0055 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 10100 0 0 0 8972 27 0 0 25 0 1 0 479937875 43220992 10025 4294967295 134512640 134672761 3221224544 3221223744 134610667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10552 10025 603 41 0 10511 0
vsize: 42208
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 10850 0 0 0 9971 28 0 0 25 0 1 0 479937875 46276608 10775 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11298 10775 603 41 0 11257 0
vsize: 45192
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 11373 0 0 0 10970 30 0 0 25 0 1 0 479937875 48525312 11298 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11847 11298 603 41 0 11806 0
vsize: 47388
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 11625 0 0 0 11969 31 0 0 25 0 1 0 479937875 49475584 11549 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12079 11549 603 41 0 12038 0
vsize: 48316
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 11625 0 0 0 12970 31 0 0 25 0 1 0 479937875 49475584 11549 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12079 11549 603 41 0 12038 0
vsize: 48316
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 11625 0 0 0 13970 31 0 0 25 0 1 0 479937875 49475584 11549 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12079 11549 603 41 0 12038 0
vsize: 48316
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 11627 0 0 0 14970 31 0 0 25 0 1 0 479937875 49471488 11550 4294967295 134512640 134672761 3221224544 3221223560 134565025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12078 11550 603 41 0 12037 0
vsize: 48312
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 11627 0 0 0 15970 31 0 0 25 0 1 0 479937875 49471488 11550 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12078 11550 603 41 0 12037 0
vsize: 48312
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 11627 0 0 0 16970 31 0 0 25 0 1 0 479937875 49471488 11550 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12078 11550 603 41 0 12037 0
vsize: 48312
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 11627 0 0 0 17971 31 0 0 25 0 1 0 479937875 49471488 11550 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12078 11550 603 41 0 12037 0
vsize: 48312
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 11630 0 0 0 18971 31 0 0 25 0 1 0 479937875 49471488 11553 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12078 11553 603 41 0 12037 0
vsize: 48312
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 12262 0 0 0 19970 32 0 0 25 0 1 0 479937875 52215808 12185 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12748 12185 603 41 0 12707 0
vsize: 50992
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 12262 0 0 0 20970 32 0 0 25 0 1 0 479937875 52215808 12185 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12748 12185 603 41 0 12707 0
vsize: 50992
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 12262 0 0 0 21970 32 0 0 25 0 1 0 479937875 52215808 12185 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12748 12185 603 41 0 12707 0
vsize: 50992
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 12262 0 0 0 22970 32 0 0 25 0 1 0 479937875 52215808 12185 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12748 12185 603 41 0 12707 0
vsize: 50992
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 12262 0 0 0 23970 32 0 0 25 0 1 0 479937875 52215808 12185 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12748 12185 603 41 0 12707 0
vsize: 50992
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 12263 0 0 0 24971 32 0 0 25 0 1 0 479937875 52215808 12186 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12748 12186 603 41 0 12707 0
vsize: 50992
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 12263 0 0 0 25971 32 0 0 25 0 1 0 479937875 52215808 12186 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12748 12186 603 41 0 12707 0
vsize: 50992
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 12263 0 0 0 26971 32 0 0 25 0 1 0 479937875 52215808 12186 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12748 12186 603 41 0 12707 0
vsize: 50992
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 12527 0 0 0 27971 32 0 0 25 0 1 0 479937875 53276672 12450 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13007 12450 603 41 0 12966 0
vsize: 52028
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 12844 0 0 0 28970 33 0 0 25 0 1 0 479937875 54591488 12767 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13328 12767 603 41 0 13287 0
vsize: 53312
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 13322 0 0 0 29969 34 0 0 25 0 1 0 479937875 56459264 13245 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13784 13245 603 41 0 13743 0
vsize: 55136
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 13714 0 0 0 30969 34 0 0 25 0 1 0 479937875 58044416 13637 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14171 13637 603 41 0 14130 0
vsize: 56684
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14114 0 0 0 31969 35 0 0 25 0 1 0 479937875 59789312 14037 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14597 14037 603 41 0 14556 0
vsize: 58388
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14476 0 0 0 32967 37 0 0 25 0 1 0 479937875 61255680 14399 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14955 14399 603 41 0 14914 0
vsize: 59820
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14741 0 0 0 33967 37 0 0 25 0 1 0 479937875 62312448 14664 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14664 603 41 0 15172 0
vsize: 60852
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14854 0 0 0 34967 37 0 0 25 0 1 0 479937875 62746624 14776 4294967295 134512640 134672761 3221224544 3221223728 134616025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15319 14776 603 41 0 15278 0
vsize: 61276
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14854 0 0 0 35967 37 0 0 25 0 1 0 479937875 62746624 14776 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15319 14776 603 41 0 15278 0
vsize: 61276
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14854 0 0 0 36967 37 0 0 25 0 1 0 479937875 62746624 14776 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15319 14776 603 41 0 15278 0
vsize: 61276
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14854 0 0 0 37968 37 0 0 25 0 1 0 479937875 62746624 14776 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15319 14776 603 41 0 15278 0
vsize: 61276
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14854 0 0 0 38968 37 0 0 25 0 1 0 479937875 62746624 14776 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15319 14776 603 41 0 15278 0
vsize: 61276
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14854 0 0 0 39968 37 0 0 25 0 1 0 479937875 62746624 14776 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15319 14776 603 41 0 15278 0
vsize: 61276
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14854 0 0 0 40968 37 0 0 25 0 1 0 479937875 62746624 14776 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15319 14776 603 41 0 15278 0
vsize: 61276
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14854 0 0 0 41968 37 0 0 25 0 1 0 479937875 62746624 14776 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15319 14776 603 41 0 15278 0
vsize: 61276
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 42968 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 43968 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 44969 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 45969 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 46969 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223584 134612851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 47969 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 48969 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 49970 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 50970 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 51970 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 52970 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 53970 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+550.016 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 54970 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+560.017 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 55971 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+570.017 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 56971 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+580.018 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 57971 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+590.017 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 58971 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134616025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+600.018 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 59971 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+610.018 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 14856 0 0 0 60972 37 0 0 25 0 1 0 479937875 62713856 14772 4294967295 134512640 134672761 3221224544 3221223548 134619829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14772 603 41 0 15270 0
vsize: 61244
[startup+620.019 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 15901 0 0 0 61970 40 0 0 25 0 1 0 479937875 67059712 15817 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16372 15817 603 41 0 16331 0
vsize: 65488
[startup+630.02 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 16828 0 0 0 62967 42 0 0 25 0 1 0 479937875 70893568 16744 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17308 16744 603 41 0 17267 0
vsize: 69232
[startup+640.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17542 0 0 0 63965 45 0 0 25 0 1 0 479937875 73969664 17458 4294967295 134512640 134672761 3221224544 3221223600 134644281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18059 17458 603 41 0 18018 0
vsize: 72236
[startup+650.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 64965 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+660.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 65965 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+670.021 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 66965 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+680.021 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 67965 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+690.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 68966 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+700.022 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 69966 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+710.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 70966 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+720.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 71966 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+730.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 72966 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+740.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 73966 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+750.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 74967 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+760.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17546 0 0 0 75967 45 0 0 25 0 1 0 479937875 73838592 17460 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17460 603 41 0 17986 0
vsize: 72108
[startup+770.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17547 0 0 0 76967 45 0 0 25 0 1 0 479937875 73838592 17461 4294967295 134512640 134672761 3221224544 3221223584 134612682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17461 603 41 0 17986 0
vsize: 72108
[startup+780.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17547 0 0 0 77967 45 0 0 25 0 1 0 479937875 73838592 17461 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17461 603 41 0 17986 0
vsize: 72108
[startup+790.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17547 0 0 0 78967 45 0 0 25 0 1 0 479937875 73838592 17461 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18027 17461 603 41 0 17986 0
vsize: 72108
[startup+800.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17582 0 0 0 79967 45 0 0 25 0 1 0 479937875 73822208 17458 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17458 603 41 0 17982 0
vsize: 72092
[startup+810.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17582 0 0 0 80968 45 0 0 25 0 1 0 479937875 73822208 17458 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17458 603 41 0 17982 0
vsize: 72092
[startup+820.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17582 0 0 0 81968 45 0 0 25 0 1 0 479937875 73822208 17458 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17458 603 41 0 17982 0
vsize: 72092
[startup+830.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17582 0 0 0 82968 45 0 0 25 0 1 0 479937875 73822208 17458 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17458 603 41 0 17982 0
vsize: 72092
[startup+840.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17582 0 0 0 83968 45 0 0 25 0 1 0 479937875 73822208 17458 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17458 603 41 0 17982 0
vsize: 72092
[startup+850.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17582 0 0 0 84968 45 0 0 25 0 1 0 479937875 73822208 17458 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17458 603 41 0 17982 0
vsize: 72092
[startup+860.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17582 0 0 0 85968 45 0 0 25 0 1 0 479937875 73822208 17458 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17458 603 41 0 17982 0
vsize: 72092
[startup+870.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17582 0 0 0 86969 45 0 0 25 0 1 0 479937875 73822208 17458 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17458 603 41 0 17982 0
vsize: 72092
[startup+880.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 87969 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+890.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 88969 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+900.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 89969 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+910.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 90969 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+920.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 91970 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+930.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 92970 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+940.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 93970 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+950.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 94970 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+960.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 95970 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+970.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 96971 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+980.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 97971 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+990.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 98971 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17583 0 0 0 99971 45 0 0 25 0 1 0 479937875 73822208 17459 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17459 603 41 0 17982 0
vsize: 72092
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17584 0 0 0 100971 45 0 0 25 0 1 0 479937875 73822208 17460 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 17460 603 41 0 17982 0
vsize: 72092
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17770 0 0 0 101971 45 0 0 25 0 1 0 479937875 74444800 17612 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18175 17612 603 41 0 18134 0
vsize: 72700
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17770 0 0 0 102972 45 0 0 25 0 1 0 479937875 74444800 17612 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18175 17612 603 41 0 18134 0
vsize: 72700
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17770 0 0 0 103972 45 0 0 25 0 1 0 479937875 74444800 17612 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18175 17612 603 41 0 18134 0
vsize: 72700
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17770 0 0 0 104972 45 0 0 25 0 1 0 479937875 74444800 17612 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18175 17612 603 41 0 18134 0
vsize: 72700
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17770 0 0 0 105972 45 0 0 25 0 1 0 479937875 74444800 17612 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18175 17612 603 41 0 18134 0
vsize: 72700
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17770 0 0 0 106972 45 0 0 25 0 1 0 479937875 74444800 17612 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18175 17612 603 41 0 18134 0
vsize: 72700
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17770 0 0 0 107973 45 0 0 25 0 1 0 479937875 74444800 17612 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18175 17612 603 41 0 18134 0
vsize: 72700
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17770 0 0 0 108973 45 0 0 25 0 1 0 479937875 74444800 17612 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18175 17612 603 41 0 18134 0
vsize: 72700
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 17770 0 0 0 109973 45 0 0 25 0 1 0 479937875 74444800 17612 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18175 17612 603 41 0 18134 0
vsize: 72700
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 18030 0 0 0 110973 46 0 0 25 0 1 0 479937875 75632640 17872 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18465 17872 603 41 0 18424 0
vsize: 73860
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 18217 0 0 0 111972 46 0 0 25 0 1 0 479937875 76152832 18025 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 18025 603 41 0 18551 0
vsize: 74368
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 18217 0 0 0 112972 46 0 0 25 0 1 0 479937875 76152832 18025 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 18025 603 41 0 18551 0
vsize: 74368
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 18218 0 0 0 113973 46 0 0 25 0 1 0 479937875 76152832 18026 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 18026 603 41 0 18551 0
vsize: 74368
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 18218 0 0 0 114973 46 0 0 25 0 1 0 479937875 76152832 18026 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 18026 603 41 0 18551 0
vsize: 74368
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 18218 0 0 0 115973 46 0 0 25 0 1 0 479937875 76152832 18026 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 18026 603 41 0 18551 0
vsize: 74368
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 18218 0 0 0 116973 46 0 0 25 0 1 0 479937875 76152832 18026 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 18026 603 41 0 18551 0
vsize: 74368
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 18218 0 0 0 117973 46 0 0 25 0 1 0 479937875 76152832 18026 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 18026 603 41 0 18551 0
vsize: 74368
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 18218 0 0 0 118973 46 0 0 25 0 1 0 479937875 76152832 18026 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 18026 603 41 0 18551 0
vsize: 74368
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26958
Raw data (stat): 26958 (minisat+) R 26957 23176 23175 0 -1 0 18218 0 0 0 119974 46 0 0 25 0 1 0 479937875 76152832 18026 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 18026 603 41 0 18551 0
vsize: 74368
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 26958
Raw data (stat): 26958 (minisat+) Z 26957 23176 23175 0 -1 12 18218 0 0 0 119974 50 0 0 25 0 1 0 479937875 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.08
CPU time (s): 1200.25
CPU user time (s): 1199.74
CPU system time (s): 0.503923
CPU usage (%): 100.014
Max. virtual memory (Kb): 74368
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####