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-chnl15_25_pb.cnf.cr.opb
MD5SUM808390b13d2d87ec4e78f628ed3af9ba
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 26
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.021995
Number of variables750
Total number of constraints80
Number of constraints which are clauses50
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint25

Trace number 4743 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-13 20:09:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=59 boxname=wulflinc12 idbench=7 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  808390b13d2d87ec4e78f628ed3af9ba  /oldhome/oroussel/tmp/wulflinc12/normalized-chnl15_25_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc12/normalized-chnl15_25_pb.cnf.cr.opb
IDLAUNCH: 59
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        921684 kB
Buffers:         34612 kB
Cached:          59280 kB
SwapCached:         16 kB
Active:          58400 kB
Inactive:        38300 kB
HighTotal:      131008 kB
HighFree:        67900 kB
LowTotal:       903652 kB
LowFree:        853784 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10696 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:38 (client local time) WITH STATUS 0 IN 1210 SECONDS
stats: 59 7 1210 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  29]---> BDD-cost:   47
c ---[  28]---> BDD-cost:   47
c ---[  27]---> BDD-cost:   47
c ---[  26]---> BDD-cost:   47
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:   47
c ---[  23]---> BDD-cost:   47
c ---[  22]---> BDD-cost:   47
c ---[  21]---> BDD-cost:   47
c ---[  20]---> BDD-cost:   47
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:   47
c ---[  17]---> BDD-cost:   47
c ---[  16]---> BDD-cost:   47
c ---[  15]---> BDD-cost:   47
c ---[  14]---> BDD-cost:   47
c ---[  13]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   47
c ---[  11]---> BDD-cost:   47
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   7]---> BDD-cost:   47
c ---[   6]---> BDD-cost:   47
c ---[   5]---> BDD-cost:   47
c ---[   4]---> BDD-cost:   47
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:   47
c ---[   1]---> BDD-cost:   47
c ---[   0]---> BDD-cost:   47
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3530     9810 |    1176       0        0     nan |  0.000 % |
c |       103 |    3530     9810 |    1293     103     5007    48.6 |  1.389 % |
c |       253 |    3530     9810 |    1422     253    13026    51.5 |  1.389 % |
c |       478 |    3530     9810 |    1565     478    27883    58.3 |  1.390 % |
c |       818 |    3530     9810 |    1721     818    54244    66.3 |  1.389 % |
c |      1324 |    3530     9810 |    1893    1324    89008    67.2 |  1.389 % |
c |      2084 |    3530     9810 |    2083    2084   154915    74.3 |  1.389 % |
c |      3224 |    3530     9810 |    2291    1835   146216    79.7 |  1.389 % |
c |      4932 |    3530     9810 |    2520    2209   220568    99.8 |  1.389 % |
c |      7494 |    3530     9810 |    2772    1902   214616   112.8 |  1.389 % |
c |     11338 |    3530     9810 |    3050    2643   352193   133.3 |  1.389 % |
c |     17107 |    3530     9810 |    3355    3014   336789   111.7 |  1.389 % |
c |     25756 |    3530     9810 |    3690    2249   281918   125.4 |  1.389 % |
c |     38731 |    3530     9810 |    4059    2796   359962   128.7 |  1.389 % |
c |     58192 |    3530     9810 |    4465    2453   289039   117.8 |  1.389 % |
c |     87386 |    3530     9810 |    4912    2518   277999   110.4 |  1.389 % |
c |    131177 |    3530     9810 |    5403    3570   478640   134.1 |  1.389 % |
c |    196861 |    3530     9810 |    5944    4748   630300   132.8 |  1.389 % |
c |    295392 |    3530     9810 |    6538    4647   519495   111.8 |  1.389 % |
c |    443181 |    3530     9810 |    7192    6344   768707   121.2 |  1.389 % |
c |    664866 |    3530     9810 |    7911    7564   930517   123.0 |  1.389 % |
c |    997394 |    3530     9810 |    8702    5038   677958   134.6 |  1.389 % |
#### 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.93 0.98 0.89 2/54 27746
Raw data (stat): 27746 (runsolver) R 27745 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420493661 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.0001 s]
Raw data (loadavg): 0.94 0.98 0.89 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1059 0 0 0 995 3 0 0 25 0 1 0 420493661 5955584 1037 4294967295 134512640 134672761 3221224624 3221223728 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1454 1037 603 41 0 1413 0
vsize: 5816
[startup+20.0005 s]
Raw data (loadavg): 0.95 0.98 0.89 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1203 0 0 0 1994 4 0 0 25 0 1 0 420493661 6483968 1181 4294967295 134512640 134672761 3221224624 3221223728 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1583 1181 603 41 0 1542 0
vsize: 6332
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.98 0.89 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1349 0 0 0 2994 4 0 0 25 0 1 0 420493661 7159808 1327 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1748 1327 603 41 0 1707 0
vsize: 6992
[startup+40.0026 s]
Raw data (loadavg): 0.96 0.98 0.89 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1370 0 0 0 3993 4 0 0 25 0 1 0 420493661 7159808 1348 4294967295 134512640 134672761 3221224624 3221223748 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1748 1348 603 41 0 1707 0
vsize: 6992
[startup+50.003 s]
Raw data (loadavg): 0.97 0.98 0.89 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1419 0 0 0 4993 5 0 0 25 0 1 0 420493661 7430144 1397 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1814 1397 603 41 0 1773 0
vsize: 7256
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.98 0.89 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1453 0 0 0 5993 5 0 0 25 0 1 0 420493661 7565312 1431 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1847 1431 603 41 0 1806 0
vsize: 7388
[startup+70.0041 s]
Raw data (loadavg): 0.97 0.98 0.90 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1556 0 0 0 6992 5 0 0 25 0 1 0 420493661 7970816 1534 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1946 1534 603 41 0 1905 0
vsize: 7784
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.98 0.90 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1636 0 0 0 7992 6 0 0 25 0 1 0 420493661 8376320 1614 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2045 1614 603 41 0 2004 0
vsize: 8180
[startup+90.0057 s]
Raw data (loadavg): 0.98 0.98 0.90 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1667 0 0 0 8991 6 0 0 25 0 1 0 420493661 8523776 1645 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2081 1645 603 41 0 2040 0
vsize: 8324
[startup+100.007 s]
Raw data (loadavg): 0.98 0.98 0.90 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1677 0 0 0 9991 6 0 0 25 0 1 0 420493661 8523776 1655 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2081 1655 603 41 0 2040 0
vsize: 8324
[startup+110.007 s]
Raw data (loadavg): 0.99 0.98 0.90 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1756 0 0 0 10990 7 0 0 25 0 1 0 420493661 8794112 1734 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1734 603 41 0 2106 0
vsize: 8588
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.90 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1759 0 0 0 11990 7 0 0 25 0 1 0 420493661 8794112 1737 4294967295 134512640 134672761 3221224624 3221223808 134558853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1737 603 41 0 2106 0
vsize: 8588
[startup+130.009 s]
Raw data (loadavg): 0.99 0.98 0.90 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1762 0 0 0 12989 8 0 0 25 0 1 0 420493661 8933376 1740 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2181 1740 603 41 0 2140 0
vsize: 8724
[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.90 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1783 0 0 0 13989 8 0 0 25 0 1 0 420493661 8933376 1761 4294967295 134512640 134672761 3221224624 3221223808 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2181 1761 603 41 0 2140 0
vsize: 8724
[startup+150.011 s]
Raw data (loadavg): 0.99 0.98 0.90 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1890 0 0 0 14988 9 0 0 25 0 1 0 420493661 9482240 1868 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2315 1868 603 41 0 2274 0
vsize: 9260
[startup+160.011 s]
Raw data (loadavg): 0.99 0.98 0.90 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 1941 0 0 0 15988 9 0 0 25 0 1 0 420493661 9617408 1919 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2348 1919 603 41 0 2307 0
vsize: 9392
[startup+170.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2029 0 0 0 16987 10 0 0 25 0 1 0 420493661 10022912 2007 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2447 2007 603 41 0 2406 0
vsize: 9788
[startup+180.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2030 0 0 0 17987 10 0 0 25 0 1 0 420493661 10010624 2008 4294967295 134512640 134672761 3221224624 3221223624 1075349698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2444 2008 603 41 0 2403 0
vsize: 9776
[startup+190.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2031 0 0 0 18986 10 0 0 25 0 1 0 420493661 10010624 2009 4294967295 134512640 134672761 3221224624 3221223728 134554668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2444 2009 603 41 0 2403 0
vsize: 9776
[startup+200.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2031 0 0 0 19986 11 0 0 25 0 1 0 420493661 10010624 2009 4294967295 134512640 134672761 3221224624 3221223792 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2444 2009 603 41 0 2403 0
vsize: 9776
[startup+210.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2046 0 0 0 20986 11 0 0 25 0 1 0 420493661 10010624 2024 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2444 2024 603 41 0 2403 0
vsize: 9776
[startup+220.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2100 0 0 0 21986 11 0 0 25 0 1 0 420493661 10285056 2078 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2511 2078 603 41 0 2470 0
vsize: 10044
[startup+230.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2125 0 0 0 22985 11 0 0 25 0 1 0 420493661 10420224 2103 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2544 2103 603 41 0 2503 0
vsize: 10176
[startup+240.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2125 0 0 0 23985 12 0 0 25 0 1 0 420493661 10420224 2103 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2544 2103 603 41 0 2503 0
vsize: 10176
[startup+250.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2209 0 0 0 24984 12 0 0 25 0 1 0 420493661 10698752 2187 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2187 603 41 0 2571 0
vsize: 10448
[startup+260.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2250 0 0 0 25984 13 0 0 25 0 1 0 420493661 10833920 2228 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2228 603 41 0 2604 0
vsize: 10580
[startup+270.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2251 0 0 0 26983 13 0 0 25 0 1 0 420493661 10833920 2229 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2229 603 41 0 2604 0
vsize: 10580
[startup+280.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2286 0 0 0 27983 14 0 0 25 0 1 0 420493661 11104256 2264 4294967295 134512640 134672761 3221224624 3221223728 134555200 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2711 2264 603 41 0 2670 0
vsize: 10844
[startup+290.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2299 0 0 0 28983 14 0 0 25 0 1 0 420493661 11104256 2277 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2711 2277 603 41 0 2670 0
vsize: 10844
[startup+300.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2319 0 0 0 29982 14 0 0 25 0 1 0 420493661 11239424 2297 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2297 603 41 0 2703 0
vsize: 10976
[startup+310.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2323 0 0 0 30982 14 0 0 25 0 1 0 420493661 11239424 2301 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2301 603 41 0 2703 0
vsize: 10976
[startup+320.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2329 0 0 0 31981 15 0 0 25 0 1 0 420493661 11239424 2307 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2307 603 41 0 2703 0
vsize: 10976
[startup+330.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2343 0 0 0 32981 15 0 0 25 0 1 0 420493661 11382784 2321 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2779 2321 603 41 0 2738 0
vsize: 11116
[startup+340.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2391 0 0 0 33981 15 0 0 25 0 1 0 420493661 11517952 2369 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2812 2369 603 41 0 2771 0
vsize: 11248
[startup+350.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2401 0 0 0 34981 15 0 0 25 0 1 0 420493661 11517952 2379 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2812 2379 603 41 0 2771 0
vsize: 11248
[startup+360.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2420 0 0 0 35981 15 0 0 25 0 1 0 420493661 11673600 2398 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2850 2398 603 41 0 2809 0
vsize: 11400
[startup+370.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2433 0 0 0 36980 16 0 0 25 0 1 0 420493661 11673600 2411 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2850 2411 603 41 0 2809 0
vsize: 11400
[startup+380.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2456 0 0 0 37980 16 0 0 25 0 1 0 420493661 11808768 2434 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2883 2434 603 41 0 2842 0
vsize: 11532
[startup+390.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2477 0 0 0 38980 16 0 0 25 0 1 0 420493661 11964416 2455 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2921 2455 603 41 0 2880 0
vsize: 11684
[startup+400.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2547 0 0 0 39980 16 0 0 25 0 1 0 420493661 12234752 2525 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2987 2525 603 41 0 2946 0
vsize: 11948
[startup+410.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2704 0 0 0 40979 17 0 0 25 0 1 0 420493661 12910592 2682 4294967295 134512640 134672761 3221224624 3221223728 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3152 2682 603 41 0 3111 0
vsize: 12608
[startup+420.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2727 0 0 0 41979 17 0 0 25 0 1 0 420493661 13045760 2705 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3185 2705 603 41 0 3144 0
vsize: 12740
[startup+430.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2743 0 0 0 42978 17 0 0 25 0 1 0 420493661 13045760 2721 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3185 2721 603 41 0 3144 0
vsize: 12740
[startup+440.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2748 0 0 0 43978 18 0 0 25 0 1 0 420493661 13189120 2726 4294967295 134512640 134672761 3221224624 3221223728 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3220 2726 603 41 0 3179 0
vsize: 12880
[startup+450.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2754 0 0 0 44977 18 0 0 25 0 1 0 420493661 13189120 2732 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3220 2732 603 41 0 3179 0
vsize: 12880
[startup+460.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2774 0 0 0 45977 19 0 0 25 0 1 0 420493661 13189120 2752 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3220 2752 603 41 0 3179 0
vsize: 12880
[startup+470.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2786 0 0 0 46976 19 0 0 25 0 1 0 420493661 13352960 2764 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3260 2764 603 41 0 3219 0
vsize: 13040
[startup+480.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2797 0 0 0 47976 19 0 0 25 0 1 0 420493661 13352960 2775 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3260 2775 603 41 0 3219 0
vsize: 13040
[startup+490.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2851 0 0 0 48975 20 0 0 25 0 1 0 420493661 13623296 2829 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2829 603 41 0 3285 0
vsize: 13304
[startup+500.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2851 0 0 0 49975 20 0 0 25 0 1 0 420493661 13623296 2829 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2829 603 41 0 3285 0
vsize: 13304
[startup+510.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2853 0 0 0 50975 20 0 0 25 0 1 0 420493661 13623296 2831 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2831 603 41 0 3285 0
vsize: 13304
[startup+520.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2859 0 0 0 51974 21 0 0 25 0 1 0 420493661 13623296 2837 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2837 603 41 0 3285 0
vsize: 13304
[startup+530.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2859 0 0 0 52974 21 0 0 25 0 1 0 420493661 13623296 2837 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2837 603 41 0 3285 0
vsize: 13304
[startup+540.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2859 0 0 0 53974 21 0 0 25 0 1 0 420493661 13623296 2837 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2837 603 41 0 3285 0
vsize: 13304
[startup+550.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2865 0 0 0 54974 21 0 0 25 0 1 0 420493661 13623296 2843 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2843 603 41 0 3285 0
vsize: 13304
[startup+560.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2870 0 0 0 55973 22 0 0 25 0 1 0 420493661 13770752 2848 4294967295 134512640 134672761 3221224624 3221223808 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2848 603 41 0 3321 0
vsize: 13448
[startup+570.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2870 0 0 0 56973 22 0 0 25 0 1 0 420493661 13770752 2848 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2848 603 41 0 3321 0
vsize: 13448
[startup+580.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2875 0 0 0 57973 22 0 0 25 0 1 0 420493661 13770752 2853 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2853 603 41 0 3321 0
vsize: 13448
[startup+590.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2879 0 0 0 58972 23 0 0 25 0 1 0 420493661 13770752 2857 4294967295 134512640 134672761 3221224624 3221223720 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2857 603 41 0 3321 0
vsize: 13448
[startup+600.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2881 0 0 0 59972 23 0 0 25 0 1 0 420493661 13770752 2859 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2859 603 41 0 3321 0
vsize: 13448
[startup+610.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2881 0 0 0 60972 23 0 0 25 0 1 0 420493661 13770752 2859 4294967295 134512640 134672761 3221224624 3221223728 134555225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2859 603 41 0 3321 0
vsize: 13448
[startup+620.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2890 0 0 0 61971 23 0 0 25 0 1 0 420493661 13905920 2868 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2868 603 41 0 3354 0
vsize: 13580
[startup+630.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 2973 0 0 0 62971 24 0 0 25 0 1 0 420493661 14176256 2951 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3461 2951 603 41 0 3420 0
vsize: 13844
[startup+640.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3096 0 0 0 63970 25 0 0 25 0 1 0 420493661 14716928 3074 4294967295 134512640 134672761 3221224624 3221223808 134558978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3593 3074 603 41 0 3552 0
vsize: 14372
[startup+650.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3135 0 0 0 64969 25 0 0 25 0 1 0 420493661 14864384 3113 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3629 3113 603 41 0 3588 0
vsize: 14516
[startup+660.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3147 0 0 0 65969 25 0 0 25 0 1 0 420493661 15028224 3125 4294967295 134512640 134672761 3221224624 3221223808 134559179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3125 603 41 0 3628 0
vsize: 14676
[startup+670.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3147 0 0 0 66969 25 0 0 25 0 1 0 420493661 15028224 3125 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3125 603 41 0 3628 0
vsize: 14676
[startup+680.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3149 0 0 0 67969 26 0 0 25 0 1 0 420493661 15028224 3127 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3127 603 41 0 3628 0
vsize: 14676
[startup+690.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3162 0 0 0 68969 26 0 0 25 0 1 0 420493661 15028224 3140 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3140 603 41 0 3628 0
vsize: 14676
[startup+700.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3178 0 0 0 69968 26 0 0 25 0 1 0 420493661 15028224 3156 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3156 603 41 0 3628 0
vsize: 14676
[startup+710.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3188 0 0 0 70968 27 0 0 25 0 1 0 420493661 15183872 3166 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3707 3166 603 41 0 3666 0
vsize: 14828
[startup+720.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3207 0 0 0 71967 27 0 0 25 0 1 0 420493661 15183872 3185 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3707 3185 603 41 0 3666 0
vsize: 14828
[startup+730.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3237 0 0 0 72967 28 0 0 25 0 1 0 420493661 15319040 3215 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3215 603 41 0 3699 0
vsize: 14960
[startup+740.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3237 0 0 0 73966 28 0 0 25 0 1 0 420493661 15319040 3215 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3215 603 41 0 3699 0
vsize: 14960
[startup+750.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3252 0 0 0 74966 28 0 0 25 0 1 0 420493661 15462400 3230 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3775 3230 603 41 0 3734 0
vsize: 15100
[startup+760.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3258 0 0 0 75966 29 0 0 25 0 1 0 420493661 15462400 3236 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3775 3236 603 41 0 3734 0
vsize: 15100
[startup+770.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3265 0 0 0 76965 29 0 0 25 0 1 0 420493661 15462400 3243 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3775 3243 603 41 0 3734 0
vsize: 15100
[startup+780.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3272 0 0 0 77965 29 0 0 25 0 1 0 420493661 15626240 3250 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3815 3250 603 41 0 3774 0
vsize: 15260
[startup+790.053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3293 0 0 0 78965 29 0 0 25 0 1 0 420493661 15626240 3271 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3815 3271 603 41 0 3774 0
vsize: 15260
[startup+800.053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3305 0 0 0 79964 30 0 0 25 0 1 0 420493661 15790080 3283 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3283 603 41 0 3814 0
vsize: 15420
[startup+810.054 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3307 0 0 0 80964 30 0 0 25 0 1 0 420493661 15790080 3285 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3285 603 41 0 3814 0
vsize: 15420
[startup+820.055 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3335 0 0 0 81964 30 0 0 25 0 1 0 420493661 15953920 3313 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3895 3313 603 41 0 3854 0
vsize: 15580
[startup+830.055 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3340 0 0 0 82964 30 0 0 25 0 1 0 420493661 15953920 3318 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3895 3318 603 41 0 3854 0
vsize: 15580
[startup+840.056 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3345 0 0 0 83963 30 0 0 25 0 1 0 420493661 15953920 3323 4294967295 134512640 134672761 3221224624 3221223808 134559383 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3895 3323 603 41 0 3854 0
vsize: 15580
[startup+850.057 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3415 0 0 0 84962 31 0 0 25 0 1 0 420493661 16232448 3393 4294967295 134512640 134672761 3221224624 3221223728 134560269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3963 3393 603 41 0 3922 0
vsize: 15852
[startup+860.057 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3417 0 0 0 85963 31 0 0 25 0 1 0 420493661 16232448 3395 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3963 3395 603 41 0 3922 0
vsize: 15852
[startup+870.058 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3418 0 0 0 86963 31 0 0 25 0 1 0 420493661 16232448 3396 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3963 3396 603 41 0 3922 0
vsize: 15852
[startup+880.058 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3418 0 0 0 87963 31 0 0 25 0 1 0 420493661 16232448 3396 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3963 3396 603 41 0 3922 0
vsize: 15852
[startup+890.059 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3424 0 0 0 88963 31 0 0 25 0 1 0 420493661 16384000 3402 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3402 603 41 0 3959 0
vsize: 16000
[startup+900.059 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3426 0 0 0 89963 31 0 0 25 0 1 0 420493661 16384000 3404 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3404 603 41 0 3959 0
vsize: 16000
[startup+910.059 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3427 0 0 0 90963 31 0 0 25 0 1 0 420493661 16384000 3405 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3405 603 41 0 3959 0
vsize: 16000
[startup+920.059 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3427 0 0 0 91964 31 0 0 25 0 1 0 420493661 16384000 3405 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3405 603 41 0 3959 0
vsize: 16000
[startup+930.059 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3427 0 0 0 92964 31 0 0 25 0 1 0 420493661 16384000 3405 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3405 603 41 0 3959 0
vsize: 16000
[startup+940.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3427 0 0 0 93964 31 0 0 25 0 1 0 420493661 16384000 3405 4294967295 134512640 134672761 3221224624 3221223788 134559748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3405 603 41 0 3959 0
vsize: 16000
[startup+950.061 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3427 0 0 0 94964 31 0 0 25 0 1 0 420493661 16384000 3405 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3405 603 41 0 3959 0
vsize: 16000
[startup+960.061 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3427 0 0 0 95965 31 0 0 25 0 1 0 420493661 16384000 3405 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3405 603 41 0 3959 0
vsize: 16000
[startup+970.062 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3427 0 0 0 96965 31 0 0 25 0 1 0 420493661 16384000 3405 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3405 603 41 0 3959 0
vsize: 16000
[startup+980.062 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3429 0 0 0 97965 31 0 0 25 0 1 0 420493661 16384000 3407 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3407 603 41 0 3959 0
vsize: 16000
[startup+990.064 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3429 0 0 0 98965 31 0 0 25 0 1 0 420493661 16384000 3407 4294967295 134512640 134672761 3221224624 3221223728 134560335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3407 603 41 0 3959 0
vsize: 16000
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3429 0 0 0 99966 31 0 0 25 0 1 0 420493661 16384000 3407 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3407 603 41 0 3959 0
vsize: 16000
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3446 0 0 0 100964 32 0 0 25 0 1 0 420493661 16384000 3424 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3424 603 41 0 3959 0
vsize: 16000
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3503 0 0 0 101963 32 0 0 25 0 1 0 420493661 16654336 3481 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4066 3481 603 41 0 4025 0
vsize: 16264
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3517 0 0 0 102962 33 0 0 25 0 1 0 420493661 16793600 3495 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4100 3495 603 41 0 4059 0
vsize: 16400
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3523 0 0 0 103962 33 0 0 25 0 1 0 420493661 16793600 3501 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4100 3501 603 41 0 4059 0
vsize: 16400
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3523 0 0 0 104962 33 0 0 25 0 1 0 420493661 16793600 3501 4294967295 134512640 134672761 3221224624 3221223792 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4100 3501 603 41 0 4059 0
vsize: 16400
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3523 0 0 0 105962 33 0 0 25 0 1 0 420493661 16793600 3501 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4100 3501 603 41 0 4059 0
vsize: 16400
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3523 0 0 0 106962 33 0 0 25 0 1 0 420493661 16793600 3501 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4100 3501 603 41 0 4059 0
vsize: 16400
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3534 0 0 0 107962 33 0 0 25 0 1 0 420493661 16793600 3512 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4100 3512 603 41 0 4059 0
vsize: 16400
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3570 0 0 0 108963 33 0 0 25 0 1 0 420493661 16928768 3548 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4133 3548 603 41 0 4092 0
vsize: 16532
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3604 0 0 0 109963 33 0 0 25 0 1 0 420493661 17063936 3582 4294967295 134512640 134672761 3221224624 3221223728 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4166 3582 603 41 0 4125 0
vsize: 16664
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3604 0 0 0 110963 33 0 0 25 0 1 0 420493661 17063936 3582 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4166 3582 603 41 0 4125 0
vsize: 16664
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3604 0 0 0 111963 33 0 0 25 0 1 0 420493661 17063936 3582 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4166 3582 603 41 0 4125 0
vsize: 16664
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3604 0 0 0 112964 33 0 0 25 0 1 0 420493661 17063936 3582 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4166 3582 603 41 0 4125 0
vsize: 16664
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3604 0 0 0 113964 33 0 0 25 0 1 0 420493661 17063936 3582 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4166 3582 603 41 0 4125 0
vsize: 16664
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3663 0 0 0 114963 33 0 0 25 0 1 0 420493661 17334272 3641 4294967295 134512640 134672761 3221224624 3221223808 134559625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4232 3641 603 41 0 4191 0
vsize: 16928
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3674 0 0 0 115964 33 0 0 25 0 1 0 420493661 17489920 3652 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3652 603 41 0 4229 0
vsize: 17080
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3676 0 0 0 116964 33 0 0 25 0 1 0 420493661 17489920 3654 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3654 603 41 0 4229 0
vsize: 17080
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3686 0 0 0 117964 33 0 0 25 0 1 0 420493661 17489920 3664 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3664 603 41 0 4229 0
vsize: 17080
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3705 0 0 0 118964 33 0 0 25 0 1 0 420493661 17625088 3683 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4303 3683 603 41 0 4262 0
vsize: 17212
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3710 0 0 0 119964 33 0 0 25 0 1 0 420493661 17625088 3688 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4303 3688 603 41 0 4262 0
vsize: 17212
[startup+1210.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 27746
Raw data (stat): 27746 (minisat+) R 27745 25285 25284 0 -1 0 3710 0 0 0 120965 33 0 0 25 0 1 0 420493661 17625088 3688 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4303 3688 603 41 0 4262 0
vsize: 17212
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.08 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 27746
Raw data (stat): 27746 (minisat+) Z 27745 25285 25284 0 -1 12 3712 0 0 0 120965 34 0 0 25 0 1 0 420493661 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): 1210.08
CPU time (s): 1210
CPU user time (s): 1209.65
CPU system time (s): 0.346947
CPU usage (%): 99.9931
Max. virtual memory (Kb): 17212
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####