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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl20_21_pb.cnf.cr.opb
MD5SUM112c693a7a90a8dc93ad23dc136d9b75
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(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 22
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.026995
Number of variables840
Total number of constraints82
Number of constraints which are clauses42
Number of constraints which are cardinality constraints (but not clauses)40
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint21

Trace number 5706 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-14 01:31:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4144 boxname=wulflinc23 idbench=8 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  112c693a7a90a8dc93ad23dc136d9b75  /oldhome/oroussel/tmp/wulflinc23/normalized-chnl20_21_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-chnl20_21_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc23/normalized-chnl20_21_pb.cnf.cr.opb
IDLAUNCH: 4144
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        893932 kB
Buffers:         34848 kB
Cached:          62948 kB
SwapCached:        192 kB
Active:          52852 kB
Inactive:        47984 kB
HighTotal:      131008 kB
HighFree:        64288 kB
LowTotal:       903652 kB
LowFree:        829644 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34344 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:51:06 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 4144 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 82 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................
c ---[  39]---> BDD-cost:   39
c ---[  38]---> BDD-cost:   39
c ---[  37]---> BDD-cost:   39
c ---[  36]---> BDD-cost:   39
c ---[  35]---> BDD-cost:   39
c ---[  34]---> BDD-cost:   39
c ---[  33]---> BDD-cost:   39
c ---[  32]---> BDD-cost:   39
c ---[  31]---> BDD-cost:   39
c ---[  30]---> BDD-cost:   39
c ---[  29]---> BDD-cost:   39
c ---[  28]---> BDD-cost:   39
c ---[  27]---> BDD-cost:   39
c ---[  26]---> BDD-cost:   39
c ---[  25]---> BDD-cost:   39
c ---[  24]---> BDD-cost:   39
c ---[  23]---> BDD-cost:   39
c ---[  22]---> BDD-cost:   39
c ---[  21]---> BDD-cost:   39
c ---[  20]---> BDD-cost:   39
c ---[  19]---> BDD-cost:   39
c ---[  18]---> BDD-cost:   39
c ---[  17]---> BDD-cost:   39
c ---[  16]---> BDD-cost:   39
c ---[  15]---> BDD-cost:   39
c ---[  14]---> BDD-cost:   39
c ---[  13]---> BDD-cost:   39
c ---[  12]---> BDD-cost:   39
c ---[  11]---> BDD-cost:   39
c ---[  10]---> BDD-cost:   39
c ---[   9]---> BDD-cost:   39
c ---[   8]---> BDD-cost:   39
c ---[   7]---> BDD-cost:   39
c ---[   6]---> BDD-cost:   39
c ---[   5]---> BDD-cost:   39
c ---[   4]---> BDD-cost:   39
c ---[   3]---> BDD-cost:   39
c ---[   2]---> BDD-cost:   39
c ---[   1]---> BDD-cost:   39
c ---[   0]---> BDD-cost:   39
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3882    10840 |    1294       0        0     nan |  0.000 % |
c |       105 |    3882    10840 |    1423     105     7385    70.3 |  1.667 % |
c |       255 |    3882    10840 |    1565     255    18850    73.9 |  1.667 % |
c |       481 |    3882    10840 |    1722     481    40545    84.3 |  1.667 % |
c |       818 |    3882    10840 |    1894     818    71265    87.1 |  1.667 % |
c |      1330 |    3882    10840 |    2083    1330   131039    98.5 |  1.667 % |
c |      2092 |    3882    10840 |    2292    2092   211172   100.9 |  1.667 % |
c |      3231 |    3882    10840 |    2521    1659   186225   112.3 |  1.667 % |
c |      4942 |    3882    10840 |    2773    3370   365003   108.3 |  1.667 % |
c |      7507 |    3882    10840 |    3051    2457   314757   128.1 |  1.667 % |
c |     11351 |    3882    10840 |    3356    2383   263788   110.7 |  1.667 % |
c |     17118 |    3882    10840 |    3691    3938   513865   130.5 |  1.667 % |
c |     25770 |    3882    10840 |    4061    3926   537570   136.9 |  1.667 % |
c |     38745 |    3882    10840 |    4467    4621   522096   113.0 |  1.667 % |
c |     58208 |    3882    10840 |    4913    3339   584284   175.0 |  1.667 % |
c |     87400 |    3882    10840 |    5405    5035   947887   188.3 |  1.667 % |
c |    131189 |    3882    10840 |    5945    3280   620922   189.3 |  1.667 % |
c |    196874 |    3882    10840 |    6540    5430   876118   161.3 |  1.667 % |
c |    295400 |    3882    10840 |    7194    4105   759531   185.0 |  1.667 % |
c |    443191 |    3882    10840 |    7913    8832  1414915   160.2 |  1.667 % |
c |    664876 |    3882    10840 |    8705    6366  1068393   167.8 |  1.667 % |
#### 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.92 0.97 0.91 2/54 7233
Raw data (stat): 7233 (runsolver) R 7232 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480646930 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+9.99982 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 1205 0 0 0 995 3 0 0 25 0 1 0 480646930 6488064 1183 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1584 1183 603 41 0 1543 0
vsize: 6336
[startup+20.0001 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 1504 0 0 0 1993 5 0 0 25 0 1 0 480646930 7704576 1482 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1881 1482 603 41 0 1840 0
vsize: 7524
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 1540 0 0 0 2993 5 0 0 25 0 1 0 480646930 7852032 1518 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1917 1518 603 41 0 1876 0
vsize: 7668
[startup+40.0018 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 1861 0 0 0 3992 6 0 0 25 0 1 0 480646930 9203712 1839 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2247 1839 603 41 0 2206 0
vsize: 8988
[startup+50.002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 1948 0 0 0 4991 7 0 0 25 0 1 0 480646930 9609216 1926 4294967295 134512640 134672761 3221224528 3221223712 134558771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2346 1926 603 41 0 2305 0
vsize: 9384
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2085 0 0 0 5990 8 0 0 25 0 1 0 480646930 10145792 2063 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2477 2063 603 41 0 2436 0
vsize: 9908
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2122 0 0 0 6990 8 0 0 25 0 1 0 480646930 10280960 2100 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2510 2100 603 41 0 2469 0
vsize: 10040
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2376 0 0 0 7989 9 0 0 25 0 1 0 480646930 11358208 2354 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2773 2354 603 41 0 2732 0
vsize: 11092
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2488 0 0 0 8989 10 0 0 25 0 1 0 480646930 11894784 2466 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2904 2466 603 41 0 2863 0
vsize: 11616
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2488 0 0 0 9989 10 0 0 25 0 1 0 480646930 11894784 2466 4294967295 134512640 134672761 3221224528 3221223664 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2904 2466 603 41 0 2863 0
vsize: 11616
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2488 0 0 0 10988 11 0 0 25 0 1 0 480646930 11894784 2466 4294967295 134512640 134672761 3221224528 3221223632 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2904 2466 603 41 0 2863 0
vsize: 11616
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2489 0 0 0 11988 11 0 0 25 0 1 0 480646930 11894784 2467 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2904 2467 603 41 0 2863 0
vsize: 11616
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2655 0 0 0 12988 11 0 0 25 0 1 0 480646930 12570624 2633 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3069 2633 603 41 0 3028 0
vsize: 12276
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2731 0 0 0 13988 11 0 0 25 0 1 0 480646930 12836864 2709 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3134 2709 603 41 0 3093 0
vsize: 12536
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2731 0 0 0 14988 12 0 0 25 0 1 0 480646930 12836864 2709 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3134 2709 603 41 0 3093 0
vsize: 12536
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2732 0 0 0 15988 12 0 0 25 0 1 0 480646930 12836864 2710 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3134 2710 603 41 0 3093 0
vsize: 12536
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2733 0 0 0 16988 12 0 0 25 0 1 0 480646930 12836864 2711 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3134 2711 603 41 0 3093 0
vsize: 12536
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2733 0 0 0 17987 13 0 0 25 0 1 0 480646930 12836864 2711 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3134 2711 603 41 0 3093 0
vsize: 12536
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2764 0 0 0 18987 13 0 0 25 0 1 0 480646930 12972032 2742 4294967295 134512640 134672761 3221224528 3221223712 134559397 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2764 0 0 0 19987 13 0 0 25 0 1 0 480646930 12972032 2742 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2764 0 0 0 20986 14 0 0 25 0 1 0 480646930 12972032 2742 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2764 0 0 0 21986 14 0 0 25 0 1 0 480646930 12972032 2742 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2764 0 0 0 22986 14 0 0 25 0 1 0 480646930 12972032 2742 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2764 0 0 0 23986 15 0 0 25 0 1 0 480646930 12972032 2742 4294967295 134512640 134672761 3221224528 3221223632 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2791 0 0 0 24986 15 0 0 25 0 1 0 480646930 13107200 2769 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3200 2769 603 41 0 3159 0
vsize: 12800
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2921 0 0 0 25984 16 0 0 25 0 1 0 480646930 13639680 2899 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3330 2899 603 41 0 3289 0
vsize: 13320
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2961 0 0 0 26984 17 0 0 25 0 1 0 480646930 13774848 2939 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3363 2939 603 41 0 3322 0
vsize: 13452
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 2961 0 0 0 27984 17 0 0 25 0 1 0 480646930 13774848 2939 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3363 2939 603 41 0 3322 0
vsize: 13452
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3047 0 0 0 28983 18 0 0 25 0 1 0 480646930 14176256 3025 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3461 3025 603 41 0 3420 0
vsize: 13844
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3058 0 0 0 29983 18 0 0 25 0 1 0 480646930 14176256 3036 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3461 3036 603 41 0 3420 0
vsize: 13844
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3182 0 0 0 30983 19 0 0 25 0 1 0 480646930 14716928 3160 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3593 3160 603 41 0 3552 0
vsize: 14372
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3185 0 0 0 31983 19 0 0 25 0 1 0 480646930 14716928 3163 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3593 3163 603 41 0 3552 0
vsize: 14372
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3185 0 0 0 32982 19 0 0 25 0 1 0 480646930 14716928 3163 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3593 3163 603 41 0 3552 0
vsize: 14372
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3383 0 0 0 33982 19 0 0 25 0 1 0 480646930 15515648 3361 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3788 3361 603 41 0 3747 0
vsize: 15152
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3537 0 0 0 34982 20 0 0 25 0 1 0 480646930 16191488 3515 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3953 3515 603 41 0 3912 0
vsize: 15812
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3554 0 0 0 35982 20 0 0 25 0 1 0 480646930 16191488 3532 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3953 3532 603 41 0 3912 0
vsize: 15812
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3602 0 0 0 36981 21 0 0 25 0 1 0 480646930 16461824 3580 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4019 3580 603 41 0 3978 0
vsize: 16076
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3602 0 0 0 37981 21 0 0 25 0 1 0 480646930 16461824 3580 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4019 3580 603 41 0 3978 0
vsize: 16076
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3602 0 0 0 38981 21 0 0 25 0 1 0 480646930 16457728 3580 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4018 3580 603 41 0 3977 0
vsize: 16072
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3602 0 0 0 39981 21 0 0 25 0 1 0 480646930 16457728 3580 4294967295 134512640 134672761 3221224528 3221223712 134559618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4018 3580 603 41 0 3977 0
vsize: 16072
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3603 0 0 0 40982 21 0 0 25 0 1 0 480646930 16453632 3581 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3581 603 41 0 3976 0
vsize: 16068
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3603 0 0 0 41982 21 0 0 25 0 1 0 480646930 16453632 3581 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3581 603 41 0 3976 0
vsize: 16068
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3603 0 0 0 42982 21 0 0 25 0 1 0 480646930 16453632 3581 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3581 603 41 0 3976 0
vsize: 16068
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3603 0 0 0 43982 21 0 0 25 0 1 0 480646930 16453632 3581 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3581 603 41 0 3976 0
vsize: 16068
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3603 0 0 0 44982 21 0 0 25 0 1 0 480646930 16453632 3581 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3581 603 41 0 3976 0
vsize: 16068
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3603 0 0 0 45982 21 0 0 25 0 1 0 480646930 16453632 3581 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3581 603 41 0 3976 0
vsize: 16068
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3603 0 0 0 46983 21 0 0 25 0 1 0 480646930 16453632 3581 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3581 603 41 0 3976 0
vsize: 16068
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3603 0 0 0 47983 21 0 0 25 0 1 0 480646930 16453632 3581 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3581 603 41 0 3976 0
vsize: 16068
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3604 0 0 0 48983 21 0 0 25 0 1 0 480646930 16453632 3582 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3582 603 41 0 3976 0
vsize: 16068
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3606 0 0 0 49983 21 0 0 25 0 1 0 480646930 16453632 3584 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3584 603 41 0 3976 0
vsize: 16068
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3606 0 0 0 50983 21 0 0 25 0 1 0 480646930 16453632 3584 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3584 603 41 0 3976 0
vsize: 16068
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3629 0 0 0 51983 21 0 0 25 0 1 0 480646930 16617472 3607 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4057 3607 603 41 0 4016 0
vsize: 16228
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3629 0 0 0 52983 21 0 0 25 0 1 0 480646930 16617472 3607 4294967295 134512640 134672761 3221224528 3221223632 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4057 3607 603 41 0 4016 0
vsize: 16228
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3646 0 0 0 53983 21 0 0 25 0 1 0 480646930 16617472 3624 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4057 3624 603 41 0 4016 0
vsize: 16228
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3696 0 0 0 54983 22 0 0 25 0 1 0 480646930 16916480 3674 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3674 603 41 0 4089 0
vsize: 16520
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3720 0 0 0 55984 22 0 0 25 0 1 0 480646930 17080320 3698 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3698 603 41 0 4129 0
vsize: 16680
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3732 0 0 0 56984 22 0 0 25 0 1 0 480646930 17080320 3710 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3710 603 41 0 4129 0
vsize: 16680
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3732 0 0 0 57984 22 0 0 25 0 1 0 480646930 17080320 3710 4294967295 134512640 134672761 3221224528 3221223712 134558859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3710 603 41 0 4129 0
vsize: 16680
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3741 0 0 0 58984 22 0 0 25 0 1 0 480646930 17080320 3719 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3719 603 41 0 4129 0
vsize: 16680
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3748 0 0 0 59984 22 0 0 25 0 1 0 480646930 17080320 3726 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3726 603 41 0 4129 0
vsize: 16680
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3755 0 0 0 60984 22 0 0 25 0 1 0 480646930 17244160 3733 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4210 3733 603 41 0 4169 0
vsize: 16840
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 3909 0 0 0 61984 22 0 0 25 0 1 0 480646930 17780736 3887 4294967295 134512640 134672761 3221224528 3221223712 134559607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4341 3887 603 41 0 4300 0
vsize: 17364
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4150 0 0 0 62984 22 0 0 25 0 1 0 480646930 18849792 4128 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4602 4128 603 41 0 4561 0
vsize: 18408
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4198 0 0 0 63984 22 0 0 25 0 1 0 480646930 18980864 4176 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4176 603 41 0 4593 0
vsize: 18536
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4198 0 0 0 64984 22 0 0 25 0 1 0 480646930 18980864 4176 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4176 603 41 0 4593 0
vsize: 18536
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4198 0 0 0 65985 22 0 0 25 0 1 0 480646930 18980864 4176 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4176 603 41 0 4593 0
vsize: 18536
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4198 0 0 0 66985 22 0 0 25 0 1 0 480646930 18980864 4176 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4176 603 41 0 4593 0
vsize: 18536
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4213 0 0 0 67985 23 0 0 25 0 1 0 480646930 19116032 4191 4294967295 134512640 134672761 3221224528 3221223712 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4667 4191 603 41 0 4626 0
vsize: 18668
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4218 0 0 0 68985 23 0 0 25 0 1 0 480646930 19116032 4196 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4667 4196 603 41 0 4626 0
vsize: 18668
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4239 0 0 0 69985 23 0 0 25 0 1 0 480646930 19263488 4217 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4703 4217 603 41 0 4662 0
vsize: 18812
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4239 0 0 0 70985 23 0 0 25 0 1 0 480646930 19263488 4217 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4703 4217 603 41 0 4662 0
vsize: 18812
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4245 0 0 0 71985 23 0 0 25 0 1 0 480646930 19263488 4223 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4703 4223 603 41 0 4662 0
vsize: 18812
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4245 0 0 0 72986 23 0 0 25 0 1 0 480646930 19263488 4223 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4703 4223 603 41 0 4662 0
vsize: 18812
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4268 0 0 0 73986 23 0 0 25 0 1 0 480646930 19394560 4246 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4735 4246 603 41 0 4694 0
vsize: 18940
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4278 0 0 0 74986 23 0 0 25 0 1 0 480646930 19386368 4256 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4733 4256 603 41 0 4692 0
vsize: 18932
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4278 0 0 0 75986 23 0 0 25 0 1 0 480646930 19386368 4256 4294967295 134512640 134672761 3221224528 3221223696 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4733 4256 603 41 0 4692 0
vsize: 18932
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4278 0 0 0 76986 23 0 0 25 0 1 0 480646930 19386368 4256 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4733 4256 603 41 0 4692 0
vsize: 18932
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4292 0 0 0 77987 23 0 0 25 0 1 0 480646930 19386368 4270 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4733 4270 603 41 0 4692 0
vsize: 18932
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4292 0 0 0 78987 23 0 0 25 0 1 0 480646930 19386368 4270 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4733 4270 603 41 0 4692 0
vsize: 18932
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4292 0 0 0 79987 23 0 0 25 0 1 0 480646930 19386368 4270 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4733 4270 603 41 0 4692 0
vsize: 18932
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4316 0 0 0 80987 23 0 0 25 0 1 0 480646930 19521536 4294 4294967295 134512640 134672761 3221224528 3221223696 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4766 4294 603 41 0 4725 0
vsize: 19064
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4350 0 0 0 81987 23 0 0 25 0 1 0 480646930 19664896 4328 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4801 4328 603 41 0 4760 0
vsize: 19204
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4364 0 0 0 82987 23 0 0 25 0 1 0 480646930 19812352 4342 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4837 4342 603 41 0 4796 0
vsize: 19348
[startup+840.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4378 0 0 0 83987 23 0 0 25 0 1 0 480646930 19812352 4356 4294967295 134512640 134672761 3221224528 3221223632 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4837 4356 603 41 0 4796 0
vsize: 19348
[startup+850.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4388 0 0 0 84988 23 0 0 25 0 1 0 480646930 19959808 4366 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4873 4366 603 41 0 4832 0
vsize: 19492
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4400 0 0 0 85988 23 0 0 25 0 1 0 480646930 19959808 4378 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4873 4378 603 41 0 4832 0
vsize: 19492
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4654 0 0 0 86987 24 0 0 25 0 1 0 480646930 21045248 4632 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5138 4632 603 41 0 5097 0
vsize: 20552
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4820 0 0 0 87987 24 0 0 25 0 1 0 480646930 21721088 4798 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5303 4798 603 41 0 5262 0
vsize: 21212
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4840 0 0 0 88987 24 0 0 25 0 1 0 480646930 21856256 4818 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5336 4818 603 41 0 5295 0
vsize: 21344
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4892 0 0 0 89987 24 0 0 25 0 1 0 480646930 21991424 4870 4294967295 134512640 134672761 3221224528 3221223632 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5369 4870 603 41 0 5328 0
vsize: 21476
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4893 0 0 0 90987 24 0 0 25 0 1 0 480646930 21991424 4871 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5369 4871 603 41 0 5328 0
vsize: 21476
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4893 0 0 0 91987 24 0 0 25 0 1 0 480646930 21991424 4871 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5369 4871 603 41 0 5328 0
vsize: 21476
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4893 0 0 0 92987 24 0 0 25 0 1 0 480646930 21991424 4871 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5369 4871 603 41 0 5328 0
vsize: 21476
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 4947 0 0 0 93988 24 0 0 25 0 1 0 480646930 22261760 4925 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5435 4925 603 41 0 5394 0
vsize: 21740
[startup+950.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5014 0 0 0 94988 25 0 0 25 0 1 0 480646930 22532096 4992 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5501 4992 603 41 0 5460 0
vsize: 22004
[startup+960.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5056 0 0 0 95988 25 0 0 25 0 1 0 480646930 22667264 5034 4294967295 134512640 134672761 3221224528 3221223632 134559787 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5534 5034 603 41 0 5493 0
vsize: 22136
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5089 0 0 0 96987 25 0 0 25 0 1 0 480646930 22814720 5067 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5067 603 41 0 5529 0
vsize: 22280
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5089 0 0 0 97988 25 0 0 25 0 1 0 480646930 22814720 5067 4294967295 134512640 134672761 3221224528 3221223632 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5067 603 41 0 5529 0
vsize: 22280
[startup+990.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5089 0 0 0 98988 25 0 0 25 0 1 0 480646930 22814720 5067 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5067 603 41 0 5529 0
vsize: 22280
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5089 0 0 0 99988 25 0 0 25 0 1 0 480646930 22814720 5067 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5067 603 41 0 5529 0
vsize: 22280
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5089 0 0 0 100988 25 0 0 25 0 1 0 480646930 22814720 5067 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5067 603 41 0 5529 0
vsize: 22280
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5089 0 0 0 101988 25 0 0 25 0 1 0 480646930 22814720 5067 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5067 603 41 0 5529 0
vsize: 22280
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5089 0 0 0 102988 25 0 0 25 0 1 0 480646930 22814720 5067 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5067 603 41 0 5529 0
vsize: 22280
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5091 0 0 0 103989 25 0 0 25 0 1 0 480646930 22814720 5069 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5069 603 41 0 5529 0
vsize: 22280
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5091 0 0 0 104989 25 0 0 25 0 1 0 480646930 22814720 5069 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5069 603 41 0 5529 0
vsize: 22280
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5091 0 0 0 105989 25 0 0 25 0 1 0 480646930 22814720 5069 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5069 603 41 0 5529 0
vsize: 22280
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5091 0 0 0 106989 25 0 0 25 0 1 0 480646930 22814720 5069 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5069 603 41 0 5529 0
vsize: 22280
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5092 0 0 0 107989 25 0 0 25 0 1 0 480646930 22814720 5070 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5070 603 41 0 5529 0
vsize: 22280
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5092 0 0 0 108990 25 0 0 25 0 1 0 480646930 22814720 5070 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5070 603 41 0 5529 0
vsize: 22280
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5092 0 0 0 109990 25 0 0 25 0 1 0 480646930 22814720 5070 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5070 603 41 0 5529 0
vsize: 22280
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5094 0 0 0 110990 25 0 0 25 0 1 0 480646930 22814720 5072 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5072 603 41 0 5529 0
vsize: 22280
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5094 0 0 0 111990 25 0 0 25 0 1 0 480646930 22814720 5072 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5072 603 41 0 5529 0
vsize: 22280
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5094 0 0 0 112991 25 0 0 25 0 1 0 480646930 22814720 5072 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5072 603 41 0 5529 0
vsize: 22280
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5094 0 0 0 113991 25 0 0 25 0 1 0 480646930 22814720 5072 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5072 603 41 0 5529 0
vsize: 22280
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5094 0 0 0 114991 25 0 0 25 0 1 0 480646930 22814720 5072 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5072 603 41 0 5529 0
vsize: 22280
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5094 0 0 0 115991 25 0 0 25 0 1 0 480646930 22814720 5072 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5072 603 41 0 5529 0
vsize: 22280
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5094 0 0 0 116991 25 0 0 25 0 1 0 480646930 22814720 5072 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5072 603 41 0 5529 0
vsize: 22280
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5094 0 0 0 117991 25 0 0 25 0 1 0 480646930 22814720 5072 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5072 603 41 0 5529 0
vsize: 22280
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5094 0 0 0 118992 25 0 0 25 0 1 0 480646930 22814720 5072 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5072 603 41 0 5529 0
vsize: 22280
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7233
Raw data (stat): 7233 (minisat+) R 7232 3260 3259 0 -1 0 5365 0 0 0 119990 27 0 0 25 0 1 0 480646930 24027136 5343 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5866 5343 603 41 0 5825 0
vsize: 23464
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 7233
Raw data (stat): 7233 (minisat+) Z 7232 3260 3259 0 -1 12 5367 0 0 0 119990 28 0 0 25 0 1 0 480646930 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.03
CPU time (s): 1200.19
CPU user time (s): 1199.91
CPU system time (s): 0.284956
CPU usage (%): 100.013
Max. virtual memory (Kb): 23464
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####