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-fpga40_40_sat_pb.cnf.cr.opb
MD5SUM	f9a3a990ebca4aa5457d0675d3f1fe27
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	41
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.9477
Number of variables	2400
Total number of constraints	1720
Number of constraints which are clauses	1640
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	20
Maximum length of a constraint	40
Trace number 5402

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-13 23:41:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3814 boxname=wulflinc18 idbench=54 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f9a3a990ebca4aa5457d0675d3f1fe27  /oldhome/oroussel/tmp/wulflinc18/normalized-fpga40_40_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc18/normalized-fpga40_40_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc18/normalized-fpga40_40_sat_pb.cnf.cr.opb
IDLAUNCH: 3814
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        887228 kB
Buffers:         34300 kB
Cached:          77172 kB
SwapCached:        320 kB
Active:          54616 kB
Inactive:        60076 kB
HighTotal:      131008 kB
HighFree:        49812 kB
LowTotal:       903652 kB
LowFree:        837416 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27180 kB
Committed_AS:    63668 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:01:41 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 3814 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1720 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  79]---> BDD-cost:   77
c ---[  78]---> BDD-cost:   77
c ---[  77]---> BDD-cost:   77
c ---[  76]---> BDD-cost:   77
c ---[  75]---> BDD-cost:   77
c ---[  74]---> BDD-cost:   77
c ---[  73]---> BDD-cost:   77
c ---[  72]---> BDD-cost:   77
c ---[  71]---> BDD-cost:   77
c ---[  70]---> BDD-cost:   77
c ---[  69]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  67]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  65]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  63]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   77
c ---[  61]---> BDD-cost:   77
c ---[  60]---> BDD-cost:   77
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   37
c ---[  38]---> BDD-cost:   37
c ---[  37]---> BDD-cost:   37
c ---[  36]---> BDD-cost:   37
c ---[  35]---> BDD-cost:   37
c ---[  34]---> BDD-cost:   37
c ---[  33]---> BDD-cost:   37
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   37
c ---[  30]---> BDD-cost:   37
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c#### 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/55 24968
Raw data (stat): 24968 (runsolver) R 24967 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479983870 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/55 24968
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 3644 0 0 0 987 10 0 0 25 0 1 0 479983870 16330752 3579 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3987 3579 603 41 0 3946 0
vsize: 15948
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.94 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 5606 0 0 0 1984 14 0 0 25 0 1 0 479983870 24399872 5541 4294967295 134512640 134672761 3221224528 3221223340 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5957 5541 603 41 0 5916 0
vsize: 23828
[startup+30.0014 s]
Raw data (loadavg): 0.90 0.94 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 6629 0 0 0 2981 17 0 0 25 0 1 0 479983870 28585984 6563 4294967295 134512640 134672761 3221224528 3221223568 134614212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6979 6563 603 41 0 6938 0
vsize: 27916
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.94 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 6629 0 0 0 3981 17 0 0 25 0 1 0 479983870 28585984 6563 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6979 6563 603 41 0 6938 0
vsize: 27916
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 6759 0 0 0 4981 17 0 0 25 0 1 0 479983870 29114368 6693 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7108 6693 603 41 0 7067 0
vsize: 28432
[startup+60.0021 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 7739 0 0 0 5979 20 0 0 25 0 1 0 479983870 33071104 7673 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8074 7673 603 41 0 8033 0
vsize: 32296
[startup+70.0031 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 7980 0 0 0 6979 20 0 0 25 0 1 0 479983870 34099200 7914 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8325 7914 603 41 0 8284 0
vsize: 33300
[startup+80.0037 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 7980 0 0 0 7979 20 0 0 25 0 1 0 479983870 34099200 7914 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8325 7914 603 41 0 8284 0
vsize: 33300
[startup+90.0039 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 8090 0 0 0 8979 20 0 0 25 0 1 0 479983870 34643968 8024 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8458 8024 603 41 0 8417 0
vsize: 33832
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 8607 0 0 0 9977 22 0 0 25 0 1 0 479983870 36691968 8541 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8958 8541 603 41 0 8917 0
vsize: 35832
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 9083 0 0 0 10976 24 0 0 25 0 1 0 479983870 38723584 9017 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9454 9017 603 41 0 9413 0
vsize: 37816
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 9146 0 0 0 11976 24 0 0 25 0 1 0 479983870 38977536 9080 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9516 9080 603 41 0 9475 0
vsize: 38064
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 9146 0 0 0 12976 24 0 0 25 0 1 0 479983870 38977536 9080 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9516 9080 603 41 0 9475 0
vsize: 38064
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 9867 0 0 0 13974 26 0 0 25 0 1 0 479983870 41922560 9800 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10235 9800 603 41 0 10194 0
vsize: 40940
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 9867 0 0 0 14974 26 0 0 25 0 1 0 479983870 41922560 9800 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10235 9800 603 41 0 10194 0
vsize: 40940
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 9867 0 0 0 15974 26 0 0 25 0 1 0 479983870 41922560 9800 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10235 9800 603 41 0 10194 0
vsize: 40940
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 3/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 9867 0 0 0 16974 26 0 0 25 0 1 0 479983870 41922560 9800 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10235 9800 603 41 0 10194 0
vsize: 40940
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 9867 0 0 0 17974 26 0 0 25 0 1 0 479983870 41922560 9800 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10235 9800 603 41 0 10194 0
vsize: 40940
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 10440 0 0 0 18974 27 0 0 25 0 1 0 479983870 44331008 10373 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10823 10373 603 41 0 10782 0
vsize: 43292
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 11060 0 0 0 19972 29 0 0 25 0 1 0 479983870 46841856 10993 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11436 10993 603 41 0 11395 0
vsize: 45744
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 11215 0 0 0 20972 30 0 0 25 0 1 0 479983870 47464448 11148 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11588 11148 603 41 0 11547 0
vsize: 46352
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 11215 0 0 0 21972 30 0 0 25 0 1 0 479983870 47464448 11148 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11588 11148 603 41 0 11547 0
vsize: 46352
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 11829 0 0 0 22970 31 0 0 25 0 1 0 479983870 49967104 11762 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12199 11762 603 41 0 12158 0
vsize: 48796
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12966 0 0 0 23968 34 0 0 25 0 1 0 479983870 54759424 12899 4294967295 134512640 134672761 3221224528 3221223584 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13369 12899 603 41 0 13328 0
vsize: 53476
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12968 0 0 0 24968 34 0 0 25 0 1 0 479983870 54628352 12900 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13337 12900 603 41 0 13296 0
vsize: 53348
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12968 0 0 0 25968 34 0 0 25 0 1 0 479983870 54628352 12900 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13337 12900 603 41 0 13296 0
vsize: 53348
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 26968 34 0 0 25 0 1 0 479983870 54628352 12901 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13337 12901 603 41 0 13296 0
vsize: 53348
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 27968 34 0 0 25 0 1 0 479983870 54628352 12901 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13337 12901 603 41 0 13296 0
vsize: 53348
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 28968 34 0 0 25 0 1 0 479983870 54628352 12901 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13337 12901 603 41 0 13296 0
vsize: 53348
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 29968 34 0 0 25 0 1 0 479983870 54628352 12901 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13337 12901 603 41 0 13296 0
vsize: 53348
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24970
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 30969 34 0 0 25 0 1 0 479983870 54628352 12901 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13337 12901 603 41 0 13296 0
vsize: 53348
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 31969 34 0 0 25 0 1 0 479983870 54628352 12901 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13337 12901 603 41 0 13296 0
vsize: 53348
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 32969 34 0 0 25 0 1 0 479983870 54624256 12900 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13336 12900 603 41 0 13295 0
vsize: 53344
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 33969 34 0 0 25 0 1 0 479983870 54624256 12900 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13336 12900 603 41 0 13295 0
vsize: 53344
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 34969 34 0 0 25 0 1 0 479983870 54624256 12900 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13336 12900 603 41 0 13295 0
vsize: 53344
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 35969 34 0 0 25 0 1 0 479983870 54624256 12900 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13336 12900 603 41 0 13295 0
vsize: 53344
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12969 0 0 0 36969 34 0 0 25 0 1 0 479983870 54624256 12900 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13336 12900 603 41 0 13295 0
vsize: 53344
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 12970 0 0 0 37970 34 0 0 25 0 1 0 479983870 54624256 12901 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13336 12901 603 41 0 13295 0
vsize: 53344
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13458 0 0 0 38969 35 0 0 25 0 1 0 479983870 56606720 13389 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13389 603 41 0 13779 0
vsize: 55280
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13458 0 0 0 39969 35 0 0 25 0 1 0 479983870 56606720 13389 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13389 603 41 0 13779 0
vsize: 55280
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13458 0 0 0 40969 35 0 0 25 0 1 0 479983870 56606720 13389 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13389 603 41 0 13779 0
vsize: 55280
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13458 0 0 0 41969 35 0 0 25 0 1 0 479983870 56606720 13389 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13389 603 41 0 13779 0
vsize: 55280
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13458 0 0 0 42970 35 0 0 25 0 1 0 479983870 56606720 13389 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13389 603 41 0 13779 0
vsize: 55280
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13458 0 0 0 43970 35 0 0 25 0 1 0 479983870 56606720 13389 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13389 603 41 0 13779 0
vsize: 55280
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13458 0 0 0 44970 35 0 0 25 0 1 0 479983870 56606720 13389 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13389 603 41 0 13779 0
vsize: 55280
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13458 0 0 0 45970 35 0 0 25 0 1 0 479983870 56606720 13389 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13389 603 41 0 13779 0
vsize: 55280
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13458 0 0 0 46970 35 0 0 25 0 1 0 479983870 56606720 13389 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13389 603 41 0 13779 0
vsize: 55280
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13458 0 0 0 47971 35 0 0 25 0 1 0 479983870 56606720 13389 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13389 603 41 0 13779 0
vsize: 55280
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13702 0 0 0 48970 36 0 0 25 0 1 0 479983870 57683968 13633 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14083 13633 603 41 0 14042 0
vsize: 56332
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 49970 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 50970 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 51970 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 52970 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 53970 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 54971 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 55971 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 56971 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 57971 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 58971 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13981 0 0 0 59971 36 0 0 25 0 1 0 479983870 58777600 13911 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13911 603 41 0 14309 0
vsize: 57400
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24972
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13982 0 0 0 60972 36 0 0 25 0 1 0 479983870 58777600 13912 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13912 603 41 0 14309 0
vsize: 57400
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13982 0 0 0 61972 36 0 0 25 0 1 0 479983870 58777600 13912 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13912 603 41 0 14309 0
vsize: 57400
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 13982 0 0 0 62972 36 0 0 25 0 1 0 479983870 58777600 13912 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14350 13912 603 41 0 14309 0
vsize: 57400
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14208 0 0 0 63972 37 0 0 25 0 1 0 479983870 59703296 14138 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14576 14138 603 41 0 14535 0
vsize: 58304
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14484 0 0 0 64971 38 0 0 25 0 1 0 479983870 60956672 14414 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14882 14414 603 41 0 14841 0
vsize: 59528
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14802 0 0 0 65971 38 0 0 25 0 1 0 479983870 62193664 14732 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15184 14732 603 41 0 15143 0
vsize: 60736
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14945 0 0 0 66970 39 0 0 25 0 1 0 479983870 62754816 14874 4294967295 134512640 134672761 3221224528 3221223568 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15321 14874 603 41 0 15280 0
vsize: 61284
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14945 0 0 0 67971 39 0 0 25 0 1 0 479983870 62754816 14874 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15321 14874 603 41 0 15280 0
vsize: 61284
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14945 0 0 0 68971 39 0 0 25 0 1 0 479983870 62754816 14874 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15321 14874 603 41 0 15280 0
vsize: 61284
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14945 0 0 0 69971 39 0 0 25 0 1 0 479983870 62754816 14874 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15321 14874 603 41 0 15280 0
vsize: 61284
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14945 0 0 0 70971 39 0 0 25 0 1 0 479983870 62754816 14874 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15321 14874 603 41 0 15280 0
vsize: 61284
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14947 0 0 0 71971 39 0 0 25 0 1 0 479983870 62754816 14876 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15321 14876 603 41 0 15280 0
vsize: 61284
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14966 0 0 0 72971 39 0 0 25 0 1 0 479983870 62951424 14895 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15369 14895 603 41 0 15328 0
vsize: 61476
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14993 0 0 0 73971 39 0 0 25 0 1 0 479983870 63016960 14921 4294967295 134512640 134672761 3221224528 3221223568 134613748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14921 603 41 0 15344 0
vsize: 61540
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14993 0 0 0 74972 39 0 0 25 0 1 0 479983870 63016960 14921 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14921 603 41 0 15344 0
vsize: 61540
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14993 0 0 0 75972 39 0 0 25 0 1 0 479983870 63016960 14921 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14921 603 41 0 15344 0
vsize: 61540
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14993 0 0 0 76972 39 0 0 25 0 1 0 479983870 63016960 14921 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14921 603 41 0 15344 0
vsize: 61540
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 77972 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 78972 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 79972 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 80973 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 81973 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 82973 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 83973 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223568 134603506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 84973 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 85974 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 86974 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 87974 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 88974 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 89974 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24974
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 90974 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 91975 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 92975 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 93975 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 94975 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 95975 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 96975 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+980.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 97976 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 98976 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 99976 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 100976 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 101976 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 102977 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223568 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 103977 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 5/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 104977 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 105977 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 106978 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 107978 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 108978 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24976
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 109978 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1110.03 s]
Raw data (loadavg): 1.07 0.99 0.91 3/58 25020
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 110978 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223624 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1120.03 s]
Raw data (loadavg): 1.14 1.00 0.92 2/55 25029
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 111979 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1130.03 s]
Raw data (loadavg): 1.11 1.00 0.92 2/55 25029
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 112979 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1140.03 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 25029
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 113979 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1150.03 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 25029
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 114979 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1160.03 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 25029
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 115979 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1170.03 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 25029
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 116980 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1180.03 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 25031
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14994 0 0 0 117980 39 0 0 25 0 1 0 479983870 63016960 14922 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14922 603 41 0 15344 0
vsize: 61540
[startup+1190.03 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 25031
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14997 0 0 0 118980 39 0 0 25 0 1 0 479983870 63016960 14925 4294967295 134512640 134672761 3221224528 3221223584 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14925 603 41 0 15344 0
vsize: 61540
[startup+1200.04 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 25031
Raw data (stat): 24968 (minisat+) R 24967 20024 20023 0 -1 0 14997 0 0 0 119980 39 0 0 25 0 1 0 479983870 63016960 14925 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15385 14925 603 41 0 15344 0
vsize: 61540
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.03 1.00 0.92 1/55 25031
Raw data (stat): 24968 (minisat+) Z 24967 20024 20023 0 -1 12 14997 0 0 0 119980 42 0 0 25 0 1 0 479983870 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.07
CPU time (s): 1200.23
CPU user time (s): 1199.81
CPU system time (s): 0.421935
CPU usage (%): 100.014
Max. virtual memory (Kb): 61540
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####