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 4744 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-13 20:09:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=68 boxname=wulflinc15 idbench=8 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  112c693a7a90a8dc93ad23dc136d9b75  /oldhome/oroussel/tmp/wulflinc15/normalized-chnl20_21_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc15/normalized-chnl20_21_pb.cnf.cr.opb
IDLAUNCH: 68
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        927680 kB
Buffers:         34436 kB
Cached:          51276 kB
SwapCached:       2144 kB
Active:          56248 kB
Inactive:        34472 kB
HighTotal:      131008 kB
HighFree:        75796 kB
LowTotal:       903652 kB
LowFree:        851884 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10664 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:29:40 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 68 7 1200.17 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.95 0.98 0.89 2/54 31601
Raw data (stat): 31601 (runsolver) R 31600 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420494931 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0002 s]
Raw data (loadavg): 0.95 0.98 0.89 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 1205 0 0 0 995 2 0 0 25 0 1 0 420494931 6488064 1183 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1584 1183 603 41 0 1543 0
vsize: 6336
[startup+20.0007 s]
Raw data (loadavg): 0.96 0.98 0.89 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 1504 0 0 0 1993 4 0 0 25 0 1 0 420494931 7704576 1482 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1881 1482 603 41 0 1840 0
vsize: 7524
[startup+30.0016 s]
Raw data (loadavg): 0.97 0.98 0.90 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 1544 0 0 0 2993 4 0 0 25 0 1 0 420494931 7987200 1522 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1950 1522 603 41 0 1909 0
vsize: 7800
[startup+40.0017 s]
Raw data (loadavg): 0.97 0.98 0.90 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 1861 0 0 0 3992 5 0 0 25 0 1 0 420494931 9203712 1839 4294967295 134512640 134672761 3221224624 3221223792 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2247 1839 603 41 0 2206 0
vsize: 8988
[startup+50.0011 s]
Raw data (loadavg): 0.97 0.98 0.90 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 1957 0 0 0 4992 5 0 0 25 0 1 0 420494931 9609216 1935 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2346 1935 603 41 0 2305 0
vsize: 9384
[startup+60.001 s]
Raw data (loadavg): 0.98 0.98 0.90 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2085 0 0 0 5992 5 0 0 25 0 1 0 420494931 10145792 2063 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2477 2063 603 41 0 2436 0
vsize: 9908
[startup+70.0014 s]
Raw data (loadavg): 0.98 0.98 0.90 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2122 0 0 0 6992 5 0 0 25 0 1 0 420494931 10280960 2100 4294967295 134512640 134672761 3221224624 3221223792 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.0016 s]
Raw data (loadavg): 0.98 0.98 0.90 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2488 0 0 0 7991 6 0 0 25 0 1 0 420494931 11898880 2466 4294967295 134512640 134672761 3221224624 3221223620 1075351210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2905 2466 603 41 0 2864 0
vsize: 11620
[startup+90.0014 s]
Raw data (loadavg): 0.99 0.98 0.90 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2488 0 0 0 8991 6 0 0 25 0 1 0 420494931 11894784 2466 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2904 2466 603 41 0 2863 0
vsize: 11616
[startup+100.002 s]
Raw data (loadavg): 0.99 0.98 0.90 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2488 0 0 0 9991 6 0 0 25 0 1 0 420494931 11894784 2466 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2904 2466 603 41 0 2863 0
vsize: 11616
[startup+110.002 s]
Raw data (loadavg): 0.99 0.98 0.90 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2488 0 0 0 10991 6 0 0 25 0 1 0 420494931 11894784 2466 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2904 2466 603 41 0 2863 0
vsize: 11616
[startup+120.002 s]
Raw data (loadavg): 0.99 0.98 0.90 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2489 0 0 0 11991 6 0 0 25 0 1 0 420494931 11894784 2467 4294967295 134512640 134672761 3221224624 3221223760 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2904 2467 603 41 0 2863 0
vsize: 11616
[startup+130.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2692 0 0 0 12991 7 0 0 25 0 1 0 420494931 12705792 2670 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3102 2670 603 41 0 3061 0
vsize: 12408
[startup+140.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2731 0 0 0 13991 7 0 0 25 0 1 0 420494931 12836864 2709 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2709 603 41 0 3093 0
vsize: 12536
[startup+150.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2731 0 0 0 14992 7 0 0 25 0 1 0 420494931 12836864 2709 4294967295 134512640 134672761 3221224624 3221223808 134559553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2709 603 41 0 3093 0
vsize: 12536
[startup+160.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2732 0 0 0 15992 7 0 0 25 0 1 0 420494931 12836864 2710 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2710 603 41 0 3093 0
vsize: 12536
[startup+170.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2733 0 0 0 16992 7 0 0 25 0 1 0 420494931 12836864 2711 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2711 603 41 0 3093 0
vsize: 12536
[startup+180.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2733 0 0 0 17992 7 0 0 25 0 1 0 420494931 12836864 2711 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2711 603 41 0 3093 0
vsize: 12536
[startup+190.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2764 0 0 0 18992 7 0 0 25 0 1 0 420494931 12972032 2742 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+200 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2764 0 0 0 19992 7 0 0 25 0 1 0 420494931 12972032 2742 4294967295 134512640 134672761 3221224624 3221223808 134558768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+210 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2764 0 0 0 20992 7 0 0 25 0 1 0 420494931 12972032 2742 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+220 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2764 0 0 0 21992 7 0 0 25 0 1 0 420494931 12972032 2742 4294967295 134512640 134672761 3221224624 3221223728 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+230.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2764 0 0 0 22993 7 0 0 25 0 1 0 420494931 12972032 2742 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3167 2742 603 41 0 3126 0
vsize: 12668
[startup+240.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2791 0 0 0 23993 7 0 0 25 0 1 0 420494931 13107200 2769 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3200 2769 603 41 0 3159 0
vsize: 12800
[startup+250.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2863 0 0 0 24993 7 0 0 25 0 1 0 420494931 13373440 2841 4294967295 134512640 134672761 3221224624 3221223808 134559618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3265 2841 603 41 0 3224 0
vsize: 13060
[startup+260.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2961 0 0 0 25993 7 0 0 25 0 1 0 420494931 13774848 2939 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2939 603 41 0 3322 0
vsize: 13452
[startup+270.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2961 0 0 0 26993 7 0 0 25 0 1 0 420494931 13774848 2939 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2939 603 41 0 3322 0
vsize: 13452
[startup+280.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 2961 0 0 0 27993 7 0 0 25 0 1 0 420494931 13774848 2939 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2939 603 41 0 3322 0
vsize: 13452
[startup+290.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3058 0 0 0 28993 7 0 0 25 0 1 0 420494931 14176256 3036 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 3036 603 41 0 3420 0
vsize: 13844
[startup+300.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3058 0 0 0 29994 7 0 0 25 0 1 0 420494931 14176256 3036 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 3036 603 41 0 3420 0
vsize: 13844
[startup+310.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3185 0 0 0 30993 7 0 0 25 0 1 0 420494931 14716928 3163 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3593 3163 603 41 0 3552 0
vsize: 14372
[startup+320.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3185 0 0 0 31994 7 0 0 25 0 1 0 420494931 14716928 3163 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3593 3163 603 41 0 3552 0
vsize: 14372
[startup+330.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3228 0 0 0 32994 7 0 0 25 0 1 0 420494931 14848000 3206 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3625 3206 603 41 0 3584 0
vsize: 14500
[startup+340.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3537 0 0 0 33993 8 0 0 25 0 1 0 420494931 16191488 3515 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3953 3515 603 41 0 3912 0
vsize: 15812
[startup+350.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3554 0 0 0 34993 8 0 0 25 0 1 0 420494931 16191488 3532 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3953 3532 603 41 0 3912 0
vsize: 15812
[startup+360.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3602 0 0 0 35993 8 0 0 25 0 1 0 420494931 16461824 3580 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4019 3580 603 41 0 3978 0
vsize: 16076
[startup+370.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3602 0 0 0 36993 8 0 0 25 0 1 0 420494931 16461824 3580 4294967295 134512640 134672761 3221224624 3221223792 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4019 3580 603 41 0 3978 0
vsize: 16076
[startup+380.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3602 0 0 0 37994 8 0 0 25 0 1 0 420494931 16457728 3580 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4018 3580 603 41 0 3977 0
vsize: 16072
[startup+390.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3602 0 0 0 38994 8 0 0 25 0 1 0 420494931 16457728 3580 4294967295 134512640 134672761 3221224624 3221223792 134561005 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.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3603 0 0 0 39994 8 0 0 25 0 1 0 420494931 16453632 3581 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3581 603 41 0 3976 0
vsize: 16068
[startup+410.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3603 0 0 0 40994 8 0 0 25 0 1 0 420494931 16453632 3581 4294967295 134512640 134672761 3221224624 3221223728 134560235 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.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3603 0 0 0 41994 8 0 0 25 0 1 0 420494931 16453632 3581 4294967295 134512640 134672761 3221224624 3221223792 134560898 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3603 0 0 0 42995 8 0 0 25 0 1 0 420494931 16453632 3581 4294967295 134512640 134672761 3221224624 3221223728 134560229 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3603 0 0 0 43995 8 0 0 25 0 1 0 420494931 16453632 3581 4294967295 134512640 134672761 3221224624 3221223728 134559887 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3603 0 0 0 44995 8 0 0 25 0 1 0 420494931 16453632 3581 4294967295 134512640 134672761 3221224624 3221223792 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3603 0 0 0 45995 8 0 0 25 0 1 0 420494931 16453632 3581 4294967295 134512640 134672761 3221224624 3221223792 134560980 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3603 0 0 0 46995 8 0 0 25 0 1 0 420494931 16453632 3581 4294967295 134512640 134672761 3221224624 3221223792 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+480.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3604 0 0 0 47996 8 0 0 25 0 1 0 420494931 16453632 3582 4294967295 134512640 134672761 3221224624 3221223728 134560364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3582 603 41 0 3976 0
vsize: 16068
[startup+490.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3606 0 0 0 48996 8 0 0 25 0 1 0 420494931 16453632 3584 4294967295 134512640 134672761 3221224624 3221223728 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4017 3584 603 41 0 3976 0
vsize: 16068
[startup+500.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3606 0 0 0 49995 8 0 0 25 0 1 0 420494931 16453632 3584 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4017 3584 603 41 0 3976 0
vsize: 16068
[startup+510.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3629 0 0 0 50995 9 0 0 25 0 1 0 420494931 16617472 3607 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4057 3607 603 41 0 4016 0
vsize: 16228
[startup+520.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3629 0 0 0 51995 9 0 0 25 0 1 0 420494931 16617472 3607 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3652 0 0 0 52995 9 0 0 25 0 1 0 420494931 16617472 3630 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4057 3630 603 41 0 4016 0
vsize: 16228
[startup+540.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3696 0 0 0 53995 9 0 0 25 0 1 0 420494931 16916480 3674 4294967295 134512640 134672761 3221224624 3221223808 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3674 603 41 0 4089 0
vsize: 16520
[startup+550.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3720 0 0 0 54995 9 0 0 25 0 1 0 420494931 17080320 3698 4294967295 134512640 134672761 3221224624 3221223728 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3698 603 41 0 4129 0
vsize: 16680
[startup+560.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3732 0 0 0 55995 9 0 0 25 0 1 0 420494931 17080320 3710 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3710 603 41 0 4129 0
vsize: 16680
[startup+570.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3732 0 0 0 56996 9 0 0 25 0 1 0 420494931 17080320 3710 4294967295 134512640 134672761 3221224624 3221223792 134561188 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.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3741 0 0 0 57996 9 0 0 25 0 1 0 420494931 17080320 3719 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3719 603 41 0 4129 0
vsize: 16680
[startup+590.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3749 0 0 0 58996 9 0 0 25 0 1 0 420494931 17080320 3727 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3727 603 41 0 4129 0
vsize: 16680
[startup+600.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3755 0 0 0 59996 9 0 0 25 0 1 0 420494931 17244160 3733 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4210 3733 603 41 0 4169 0
vsize: 16840
[startup+610.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 3909 0 0 0 60996 9 0 0 25 0 1 0 420494931 17780736 3887 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4341 3887 603 41 0 4300 0
vsize: 17364
[startup+620.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4198 0 0 0 61995 10 0 0 25 0 1 0 420494931 18980864 4176 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4176 603 41 0 4593 0
vsize: 18536
[startup+630.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4198 0 0 0 62996 10 0 0 25 0 1 0 420494931 18980864 4176 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4176 603 41 0 4593 0
vsize: 18536
[startup+640.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4198 0 0 0 63996 10 0 0 25 0 1 0 420494931 18980864 4176 4294967295 134512640 134672761 3221224624 3221223792 134560980 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.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4198 0 0 0 64996 10 0 0 25 0 1 0 420494931 18980864 4176 4294967295 134512640 134672761 3221224624 3221223792 134560895 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.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4198 0 0 0 65996 10 0 0 25 0 1 0 420494931 18980864 4176 4294967295 134512640 134672761 3221224624 3221223792 134561205 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4213 0 0 0 66996 10 0 0 25 0 1 0 420494931 19116032 4191 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4667 4191 603 41 0 4626 0
vsize: 18668
[startup+680.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4218 0 0 0 67996 10 0 0 25 0 1 0 420494931 19116032 4196 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4667 4196 603 41 0 4626 0
vsize: 18668
[startup+690.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4239 0 0 0 68996 10 0 0 25 0 1 0 420494931 19263488 4217 4294967295 134512640 134672761 3221224624 3221223792 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+700.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4245 0 0 0 69996 10 0 0 25 0 1 0 420494931 19263488 4223 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4703 4223 603 41 0 4662 0
vsize: 18812
[startup+710.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4245 0 0 0 70997 10 0 0 25 0 1 0 420494931 19263488 4223 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4703 4223 603 41 0 4662 0
vsize: 18812
[startup+720.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4268 0 0 0 71997 10 0 0 25 0 1 0 420494931 19398656 4246 4294967295 134512640 134672761 3221224624 3221223808 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4736 4246 603 41 0 4695 0
vsize: 18944
[startup+730.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4268 0 0 0 72997 10 0 0 25 0 1 0 420494931 19394560 4246 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4735 4246 603 41 0 4694 0
vsize: 18940
[startup+740.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4278 0 0 0 73997 10 0 0 25 0 1 0 420494931 19386368 4256 4294967295 134512640 134672761 3221224624 3221223792 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4733 4256 603 41 0 4692 0
vsize: 18932
[startup+750.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4278 0 0 0 74997 10 0 0 25 0 1 0 420494931 19386368 4256 4294967295 134512640 134672761 3221224624 3221223792 134560830 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.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4278 0 0 0 75998 10 0 0 25 0 1 0 420494931 19386368 4256 4294967295 134512640 134672761 3221224624 3221223772 134559754 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4292 0 0 0 76998 10 0 0 25 0 1 0 420494931 19386368 4270 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4733 4270 603 41 0 4692 0
vsize: 18932
[startup+780.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4292 0 0 0 77998 10 0 0 25 0 1 0 420494931 19386368 4270 4294967295 134512640 134672761 3221224624 3221223760 134560661 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4292 0 0 0 78998 10 0 0 25 0 1 0 420494931 19386368 4270 4294967295 134512640 134672761 3221224624 3221223808 134559354 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.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4316 0 0 0 79997 11 0 0 25 0 1 0 420494931 19521536 4294 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4766 4294 603 41 0 4725 0
vsize: 19064
[startup+810.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4357 0 0 0 80997 11 0 0 25 0 1 0 420494931 19812352 4335 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4837 4335 603 41 0 4796 0
vsize: 19348
[startup+820.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4364 0 0 0 81997 11 0 0 25 0 1 0 420494931 19812352 4342 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4837 4342 603 41 0 4796 0
vsize: 19348
[startup+830.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4378 0 0 0 82997 11 0 0 25 0 1 0 420494931 19812352 4356 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4837 4356 603 41 0 4796 0
vsize: 19348
[startup+840.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4388 0 0 0 83997 11 0 0 25 0 1 0 420494931 19959808 4366 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4873 4366 603 41 0 4832 0
vsize: 19492
[startup+850.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4405 0 0 0 84997 11 0 0 25 0 1 0 420494931 19959808 4383 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4873 4383 603 41 0 4832 0
vsize: 19492
[startup+860.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4820 0 0 0 85997 12 0 0 25 0 1 0 420494931 21721088 4798 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5303 4798 603 41 0 5262 0
vsize: 21212
[startup+870.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4820 0 0 0 86997 12 0 0 25 0 1 0 420494931 21721088 4798 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5303 4798 603 41 0 5262 0
vsize: 21212
[startup+880.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4892 0 0 0 87997 12 0 0 25 0 1 0 420494931 21991424 4870 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5369 4870 603 41 0 5328 0
vsize: 21476
[startup+890.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4892 0 0 0 88997 12 0 0 25 0 1 0 420494931 21991424 4870 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5369 4870 603 41 0 5328 0
vsize: 21476
[startup+900.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4893 0 0 0 89997 12 0 0 25 0 1 0 420494931 21991424 4871 4294967295 134512640 134672761 3221224624 3221223792 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+910.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4893 0 0 0 90997 12 0 0 25 0 1 0 420494931 21991424 4871 4294967295 134512640 134672761 3221224624 3221223792 134561005 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.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4893 0 0 0 91998 12 0 0 25 0 1 0 420494931 21991424 4871 4294967295 134512640 134672761 3221224624 3221223792 134561269 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 4947 0 0 0 92998 12 0 0 25 0 1 0 420494931 22261760 4925 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5435 4925 603 41 0 5394 0
vsize: 21740
[startup+940.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5014 0 0 0 93998 12 0 0 25 0 1 0 420494931 22532096 4992 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5501 4992 603 41 0 5460 0
vsize: 22004
[startup+950.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5089 0 0 0 94998 12 0 0 25 0 1 0 420494931 22814720 5067 4294967295 134512640 134672761 3221224624 3221223792 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+960.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5089 0 0 0 95998 12 0 0 25 0 1 0 420494931 22814720 5067 4294967295 134512640 134672761 3221224624 3221223792 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+970.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5089 0 0 0 96998 12 0 0 25 0 1 0 420494931 22814720 5067 4294967295 134512640 134672761 3221224624 3221223792 134561014 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.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5089 0 0 0 97999 12 0 0 25 0 1 0 420494931 22814720 5067 4294967295 134512640 134672761 3221224624 3221223792 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+990.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5089 0 0 0 98999 12 0 0 25 0 1 0 420494931 22814720 5067 4294967295 134512640 134672761 3221224624 3221223792 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5089 0 0 0 99999 12 0 0 25 0 1 0 420494931 22814720 5067 4294967295 134512640 134672761 3221224624 3221223792 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+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5089 0 0 0 100999 12 0 0 25 0 1 0 420494931 22814720 5067 4294967295 134512640 134672761 3221224624 3221223792 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5091 0 0 0 101999 12 0 0 25 0 1 0 420494931 22814720 5069 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5069 603 41 0 5529 0
vsize: 22280
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5091 0 0 0 102999 12 0 0 25 0 1 0 420494931 22814720 5069 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5069 603 41 0 5529 0
vsize: 22280
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5091 0 0 0 104000 12 0 0 25 0 1 0 420494931 22814720 5069 4294967295 134512640 134672761 3221224624 3221223792 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+1050.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5091 0 0 0 105000 12 0 0 25 0 1 0 420494931 22814720 5069 4294967295 134512640 134672761 3221224624 3221223808 134559550 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5091 0 0 0 106000 12 0 0 25 0 1 0 420494931 22814720 5069 4294967295 134512640 134672761 3221224624 3221223728 134560048 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5092 0 0 0 107000 12 0 0 25 0 1 0 420494931 22814720 5070 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5070 603 41 0 5529 0
vsize: 22280
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5092 0 0 0 108000 12 0 0 25 0 1 0 420494931 22814720 5070 4294967295 134512640 134672761 3221224624 3221223728 134560070 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5093 0 0 0 109001 12 0 0 25 0 1 0 420494931 22814720 5071 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5071 603 41 0 5529 0
vsize: 22280
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5094 0 0 0 110001 12 0 0 25 0 1 0 420494931 22814720 5072 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5072 603 41 0 5529 0
vsize: 22280
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5094 0 0 0 111001 12 0 0 25 0 1 0 420494931 22814720 5072 4294967295 134512640 134672761 3221224624 3221223792 134561001 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5094 0 0 0 112001 12 0 0 25 0 1 0 420494931 22814720 5072 4294967295 134512640 134672761 3221224624 3221223792 134561001 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5094 0 0 0 113001 12 0 0 25 0 1 0 420494931 22814720 5072 4294967295 134512640 134672761 3221224624 3221223792 134560980 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5094 0 0 0 114001 12 0 0 25 0 1 0 420494931 22814720 5072 4294967295 134512640 134672761 3221224624 3221223760 134565056 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5094 0 0 0 115002 12 0 0 25 0 1 0 420494931 22814720 5072 4294967295 134512640 134672761 3221224624 3221223792 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+1160.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5094 0 0 0 116002 12 0 0 25 0 1 0 420494931 22814720 5072 4294967295 134512640 134672761 3221224624 3221223728 134560218 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5094 0 0 0 117002 12 0 0 25 0 1 0 420494931 22814720 5072 4294967295 134512640 134672761 3221224624 3221223808 134558754 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5365 0 0 0 118001 13 0 0 25 0 1 0 420494931 24027136 5343 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5866 5343 603 41 0 5825 0
vsize: 23464
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5431 0 0 0 119001 13 0 0 25 0 1 0 420494931 24293376 5409 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5931 5409 603 41 0 5890 0
vsize: 23724
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 31601
Raw data (stat): 31601 (minisat+) R 31600 29151 29150 0 -1 0 5497 0 0 0 120001 13 0 0 25 0 1 0 420494931 24563712 5475 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5997 5475 603 41 0 5956 0
vsize: 23988
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 31601
Raw data (stat): 31601 (minisat+) Z 31600 29151 29150 0 -1 12 5499 0 0 0 120001 14 0 0 25 0 1 0 420494931 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.17
CPU user time (s): 1200.02
CPU system time (s): 0.148977
CPU usage (%): 100.012
Max. virtual memory (Kb): 23988
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####