PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cm42a.opb
MD5SUM	62b75258091a8b1382fa8b1c633d9511
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	694
Optimality of the best value was proved	NO
Number of terms in the objective function	99
Biggest coefficient in the objective function	60
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	4087
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	60
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	4087
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.168973
Number of variables	99
Total number of constraints	185
Number of constraints which are clauses	185
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	20
Trace number 5587

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 00:37:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4012 boxname=wulflinc2 idbench=252 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  62b75258091a8b1382fa8b1c633d9511  /oldhome/oroussel/tmp/wulflinc2/normalized-cm42a.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc2/normalized-cm42a.opb /oldhome/oroussel/tmp/wulflinc2/normalized-cm42a.opb
IDLAUNCH: 4012
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        902392 kB
Buffers:         34752 kB
Cached:          76968 kB
SwapCached:          4 kB
Active:          56484 kB
Inactive:        58060 kB
HighTotal:      131008 kB
HighFree:        50260 kB
LowTotal:       903652 kB
LowFree:        852132 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12048 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:57:38 (client local time) WITH STATUS 10 IN 1200.35 SECONDS
stats: 4012 7 1200.35 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 185 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     185      626 |      55       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  85/85          
c |         0 |     185      626 |      74       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.013997 s)
c ==============================================================================
c [1mFound solution: 939[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 8480     Base: 3 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   21020    49263 |    6305       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7707          
c   -- var.elim.:  2000/7707          
c   -- var.elim.:  3000/7707          
c   -- var.elim.:  4000/7707          
c   -- var.elim.:  5000/7707          
c   -- var.elim.:  6000/7707          
c   -- var.elim.:  7000/7707          
c   -- var.elim.:  7707/7707          
c   -- var.elim.:  1000/4213          
c   -- var.elim.:  2000/4213          
c   -- var.elim.:  3000/4213          
c   -- var.elim.:  4000/4213          
c   -- var.elim.:  4213/4213          
c   -- subsuming                       
c   -- var.elim.:  880/880          
c   -- var.elim.:  260/260          
c   -- subsuming                       
c   -- var.elim.:  6/6          
c |         0 |   18633    59861 |      --       0       --      -- |     --   | -2387/10599
c |         0 |   18633    59861 |    7453       0        0     nan |  0.000 % |
c |       101 |   18633    59861 |    8198     101     1565    15.5 |  0.024 % |
c |       252 |   18633    59861 |    9018     252     3697    14.7 |  0.024 % |
c |       477 |   18201    58148 |    9690     470    14358    30.5 |  1.689 % |
c |       814 |   17983    57167 |   10531     728    17384    23.9 |  2.307 % |
c |      1321 |   17983    57167 |   11584    1235    51265    41.5 |  2.307 % |
c |      2080 |   17983    57167 |   12743    1994    61630    30.9 |  2.307 % |
c |      3219 |   17983    57167 |   14017    3133   117087    37.4 |  2.307 % |
c ==============================================================================
c (current CPU-time: 4.5903 s)
c ==============================================================================
c [1mFound solution: 866[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6777     Base: 3 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3408 |   34827    96642 |   10448    3322   129356    38.9 |  2.307 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7350          
c   -- var.elim.:  2000/7350          
c   -- var.elim.:  3000/7350          
c   -- var.elim.:  4000/7350          
c   -- var.elim.:  5000/7350          
c   -- var.elim.:  6000/7350          
c   -- var.elim.:  7000/7350          
c   -- var.elim.:  7350/7350          
c   -- var.elim.:  1000/4089          
c   -- var.elim.:  2000/4089          
c   -- var.elim.:  3000/4089          
c   -- var.elim.:  4000/4089          
c   -- var.elim.:  4089/4089          
c   -- var.elim.:  314/314          
c   -- var.elim.:  274/274          
c   -- subsuming                       
c   -- var.elim.:  956/956          
c   -- var.elim.:  35/35          
c |      3408 |   32588   105396 |      --    3322       --      -- |     --   | -2239/8755
c |      3408 |   32588   105396 |   13035    3147   106030    33.7 |  2.307 % |
c |      3508 |   32588   105396 |   14338    3247   109693    33.8 |  1.334 % |
c |      3659 |   32588   105396 |   15772    3398   120859    35.6 |  1.334 % |
c |      3884 |   32588   105396 |   17349    3623   131110    36.2 |  1.334 % |
c |      4222 |   32588   105396 |   19084    3961   148623    37.5 |  1.334 % |
c |      4728 |   32588   105396 |   20993    4467   167381    37.5 |  1.334 % |
c |      5487 |   32588   105396 |   23092    5226   203929    39.0 |  1.334 % |
c |      6628 |   32588   105396 |   25401    6367   309182    48.6 |  1.334 % |
c ==============================================================================
c (current CPU-time: 14.8707 s)
c ==============================================================================
c [1mFound solution: 865[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7916 |   33186   107060 |    9955    7655   425161    55.5 |  1.334 % |
c   -- subsuming                       
c   -- var.elim.:  963/963          
c   -- var.elim.:  541/541          
c   -- subsuming                       
c   -- var.elim.:  336/336          
c |      7916 |   32788   107150 |      --    7655       --      -- |     --   | -398/91
c |      7916 |   32788   107150 |   13115    7655   425161    55.5 |  1.334 % |
c |      8016 |   32788   107150 |   14426    7755   430451    55.5 |  1.338 % |
c |      8169 |   32788   107150 |   15869    7908   437395    55.3 |  1.338 % |
c |      8394 |   32788   107150 |   17456    8133   446890    54.9 |  1.338 % |
c ==============================================================================
c (current CPU-time: 16.6185 s)
c ==============================================================================
c [1mFound solution: 856[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8432 |   33005   107921 |    9901    8171   449855    55.1 |  1.338 % |
c   -- subsuming                       
c   -- var.elim.:  546/546          
c   -- var.elim.:  350/350          
c |      8432 |   32810   107942 |      --    8171       --      -- |     --   | -195/22
c |      8432 |   32810   107942 |   13124    8171   449855    55.1 |  1.338 % |
c |      8533 |   32810   107942 |   14436    8272   453218    54.8 |  1.351 % |
c |      8684 |   32810   107942 |   15880    8423   465060    55.2 |  1.351 % |
c |      8910 |   32810   107942 |   17468    8649   492841    57.0 |  1.351 % |
c |      9250 |   32810   107942 |   19214    8989   503086    56.0 |  1.351 % |
c |      9759 |   32544   105545 |   20964    9484   547927    57.8 |  1.716 % |
c |     10518 |   32544   105545 |   23061   10243   593641    58.0 |  1.716 % |
c |     11658 |   32544   105545 |   25367   11383   744362    65.4 |  1.716 % |
c |     13366 |   32544   105545 |   27904   13091   958359    73.2 |  1.716 % |
c |     15928 |   32544   105545 |   30694   15653  1046663    66.9 |  1.716 % |
c |     19775 |   32544   105545 |   33764   19500  1536427    78.8 |  1.716 % |
c ==============================================================================
c (current CPU-time: 43.6214 s)
c ==============================================================================
c [1mFound solution: 850[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20542 |   32358   104726 |    9707   19855  1579857    79.6 |  1.716 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1064          
c   -- var.elim.:  1064/1064          
c   -- var.elim.:  860/860          
c   -- var.elim.:  9/9          
c   -- subsuming                       
c   -- var.elim.:  539/539          
c   -- var.elim.:  44/44          
c |     20542 |   32062   105158 |      --   19855       --      -- |     --   | -294/437
c |     20542 |   32062   105158 |   12824   14684   652868    44.5 |  1.716 % |
c |     20644 |   32062   105158 |   14107    7994   324602    40.6 |  2.497 % |
c |     20796 |   32062   105158 |   15518    8146   327699    40.2 |  2.497 % |
c ==============================================================================
c (current CPU-time: 45.0631 s)
c ==============================================================================
c [1mFound solution: 783[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20799 |   32249   105745 |    9674    8149   327724    40.2 |  2.497 % |
c   -- subsuming                       
c   -- var.elim.:  383/383          
c   -- var.elim.:  251/251          
c |     20799 |   32153   105914 |      --    8149       --      -- |     --   | -96/170
c |     20799 |   32153   105914 |   12861    8149   327724    40.2 |  2.497 % |
c ==============================================================================
c (current CPU-time: 45.3631 s)
c ==============================================================================
c [1mFound solution: 741[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20802 |   32210   106194 |    9662    8152   327886    40.2 |  2.497 % |
c   -- subsuming                       
c   -- var.elim.:  220/220          
c   -- var.elim.:  182/182          
c |     20802 |   32180   106479 |      --    8152       --      -- |     --   | -30/286
c |     20802 |   32180   106479 |   12872    8152   327886    40.2 |  2.497 % |
c ==============================================================================
c (current CPU-time: 45.6171 s)
c ==============================================================================
c [1mFound solution: 732[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20810 |   32224   106731 |    9667    8160   328436    40.2 |  2.497 % |
c   -- subsuming                       
c   -- var.elim.:  207/207          
c   -- var.elim.:  176/176          
c |     20810 |   32198   106926 |      --    8160       --      -- |     --   | -26/196
c |     20810 |   32198   106926 |   12879    8160   328436    40.2 |  2.497 % |
c |     20910 |   32198   106926 |   14167    8260   333148    40.3 |  2.527 % |
c |     21063 |   32198   106926 |   15583    8413   345697    41.1 |  2.527 % |
c |     21288 |   32198   106926 |   17142    8638   368787    42.7 |  2.527 % |
c |     21625 |   32198   106926 |   18856    8975   388123    43.2 |  2.527 % |
c |     22132 |   32198   106926 |   20742    9482   431654    45.5 |  2.527 % |
c |     22891 |   32198   106926 |   22816   10241   540663    52.8 |  2.527 % |
c |     24030 |   32198   106926 |   25097   11380   665008    58.4 |  2.526 % |
c ==============================================================================
c (current CPU-time: 57.2153 s)
c ==============================================================================
c [1mFound solution: 712[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 3 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     25126 |   32221   107085 |    9666   12476   853144    68.4 |  2.526 % |
c   -- subsuming                       
c   -- var.elim.:  187/187          
c   -- var.elim.:  119/119          
c |     25126 |   32208   107109 |      --   12476       --      -- |     --   | -13/25
c |     25126 |   32208   107109 |   12883   12476   853144    68.4 |  2.526 % |
c |     25227 |   32208   107109 |   14171   12577   863936    68.7 |  2.539 % |
c |     25378 |   32208   107109 |   15588   12728   880191    69.2 |  2.539 % |
c |     25605 |   32208   107109 |   17147   12955   907576    70.1 |  2.539 % |
c |     25947 |   32208   107109 |   18862   13297   936754    70.4 |  2.539 % |
c |     26453 |   32208   107109 |   20748   13803  1008801    73.1 |  2.539 % |
c |     27212 |   32208   107109 |   22823   14562  1106717    76.0 |  2.539 % |
c |     28354 |   32208   107109 |   25105   15704  1323279    84.3 |  2.539 % |
c |     30062 |   32208   107109 |   27616   17412  1688803    97.0 |  2.539 % |
c |     32624 |   32208   107109 |   30377   19974  2105718   105.4 |  2.539 % |
c |     36469 |   32208   107109 |   33415   23819  2845004   119.4 |  2.539 % |
c ==============================================================================
c (current CPU-time: 112.005 s)
c ==============================================================================
c [1mFound solution: 696[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ================#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.88 0.95 0.90 2/54 24262
Raw data (stat): 24262 (runsolver) R 24261 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422107686 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0003 s]
Raw data (loadavg): 0.90 0.95 0.90 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 2664 0 0 0 988 9 0 0 25 0 1 0 422107686 11689984 2349 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2854 2349 603 41 0 2813 0
vsize: 11416
[startup+20.0006 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 3610 0 0 0 1984 13 0 0 25 0 1 0 422107686 14237696 2963 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3476 2963 603 41 0 3435 0
vsize: 13904
[startup+30.002 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 3914 0 0 0 2983 14 0 0 25 0 1 0 422107686 15421440 3267 4294967295 134512640 134672761 3221224576 3221223760 134615698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3765 3267 603 41 0 3724 0
vsize: 15060
[startup+40.0024 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 4411 0 0 0 3981 16 0 0 25 0 1 0 422107686 17584128 3764 4294967295 134512640 134672761 3221224576 3221223760 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4293 3764 603 41 0 4252 0
vsize: 17172
[startup+50.0025 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 5934 0 0 0 4975 22 0 0 25 0 1 0 422107686 18505728 4026 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4518 4026 603 41 0 4477 0
vsize: 18072
[startup+60.0031 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 6301 0 0 0 5973 24 0 0 25 0 1 0 422107686 19320832 4217 4294967295 134512640 134672761 3221224576 3221223712 134614753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4217 603 41 0 4676 0
vsize: 18868
[startup+70.0035 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 6301 0 0 0 6974 24 0 0 25 0 1 0 422107686 19320832 4217 4294967295 134512640 134672761 3221224576 3221223616 134612927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4217 603 41 0 4676 0
vsize: 18868
[startup+80.0045 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 6565 0 0 0 7973 24 0 0 25 0 1 0 422107686 20381696 4481 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4976 4481 603 41 0 4935 0
vsize: 19904
[startup+90.0052 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 7035 0 0 0 8973 25 0 0 25 0 1 0 422107686 22372352 4951 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5462 4951 603 41 0 5421 0
vsize: 21848
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 7589 0 0 0 9971 27 0 0 25 0 1 0 422107686 24612864 5505 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6009 5505 603 41 0 5968 0
vsize: 24036
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8073 0 0 0 10970 28 0 0 25 0 1 0 422107686 26587136 5989 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6491 5989 603 41 0 6450 0
vsize: 25964
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8697 0 0 0 11967 31 0 0 25 0 1 0 422107686 28393472 6437 4294967295 134512640 134672761 3221224576 3221223776 134610667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6932 6437 603 41 0 6891 0
vsize: 27728
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8697 0 0 0 12967 31 0 0 25 0 1 0 422107686 28393472 6437 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6932 6437 603 41 0 6891 0
vsize: 27728
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8697 0 0 0 13968 31 0 0 25 0 1 0 422107686 28393472 6437 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6932 6437 603 41 0 6891 0
vsize: 27728
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8697 0 0 0 14968 31 0 0 25 0 1 0 422107686 28393472 6437 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6932 6437 603 41 0 6891 0
vsize: 27728
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8697 0 0 0 15968 31 0 0 25 0 1 0 422107686 28393472 6437 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6932 6437 603 41 0 6891 0
vsize: 27728
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8698 0 0 0 16968 31 0 0 25 0 1 0 422107686 28393472 6438 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6932 6438 603 41 0 6891 0
vsize: 27728
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8995 0 0 0 17968 32 0 0 25 0 1 0 422107686 29700096 6735 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7251 6735 603 41 0 7210 0
vsize: 29004
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 9487 0 0 0 18966 33 0 0 25 0 1 0 422107686 31674368 7227 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7733 7227 603 41 0 7692 0
vsize: 30932
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 9897 0 0 0 19966 34 0 0 25 0 1 0 422107686 33513472 7637 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8182 7637 603 41 0 8141 0
vsize: 32728
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 10349 0 0 0 20965 35 0 0 25 0 1 0 422107686 35364864 8089 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8634 8089 603 41 0 8593 0
vsize: 34536
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 10755 0 0 0 21964 36 0 0 25 0 1 0 422107686 36990976 8495 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9031 8495 603 41 0 8990 0
vsize: 36124
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11158 0 0 0 22963 38 0 0 25 0 1 0 422107686 38572032 8898 4294967295 134512640 134672761 3221224576 3221223760 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9417 8898 603 41 0 9376 0
vsize: 37668
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 23963 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8993 603 41 0 9465 0
vsize: 38024
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 24963 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8993 603 41 0 9465 0
vsize: 38024
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 25963 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8993 603 41 0 9465 0
vsize: 38024
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 26963 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8993 603 41 0 9465 0
vsize: 38024
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 27963 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8993 603 41 0 9465 0
vsize: 38024
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 28964 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8993 603 41 0 9465 0
vsize: 38024
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 29964 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8993 603 41 0 9465 0
vsize: 38024
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 30964 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8993 603 41 0 9465 0
vsize: 38024
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 31964 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8993 603 41 0 9465 0
vsize: 38024
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 32964 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8993 603 41 0 9465 0
vsize: 38024
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11640 0 0 0 33964 38 0 0 25 0 1 0 422107686 40390656 9339 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9861 9339 603 41 0 9820 0
vsize: 39444
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 12009 0 0 0 34963 39 0 0 25 0 1 0 422107686 41959424 9708 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10244 9708 603 41 0 10203 0
vsize: 40976
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 12389 0 0 0 35962 41 0 0 25 0 1 0 422107686 43528192 10088 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 10088 603 41 0 10586 0
vsize: 42508
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 12747 0 0 0 36962 42 0 0 25 0 1 0 422107686 44978176 10446 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10981 10446 603 41 0 10940 0
vsize: 43924
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13119 0 0 0 37960 43 0 0 25 0 1 0 422107686 46419968 10818 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11333 10818 603 41 0 11292 0
vsize: 45332
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13399 0 0 0 38960 44 0 0 25 0 1 0 422107686 47484928 11079 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 11079 603 41 0 11552 0
vsize: 46372
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13399 0 0 0 39960 44 0 0 25 0 1 0 422107686 47484928 11079 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 11079 603 41 0 11552 0
vsize: 46372
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13399 0 0 0 40960 44 0 0 25 0 1 0 422107686 47484928 11079 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 11079 603 41 0 11552 0
vsize: 46372
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13399 0 0 0 41961 44 0 0 25 0 1 0 422107686 47484928 11079 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 11079 603 41 0 11552 0
vsize: 46372
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13400 0 0 0 42961 44 0 0 25 0 1 0 422107686 47484928 11080 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 11080 603 41 0 11552 0
vsize: 46372
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13401 0 0 0 43961 44 0 0 25 0 1 0 422107686 47484928 11081 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 11081 603 41 0 11552 0
vsize: 46372
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13403 0 0 0 44961 44 0 0 25 0 1 0 422107686 47484928 11083 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 11083 603 41 0 11552 0
vsize: 46372
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13403 0 0 0 45961 44 0 0 25 0 1 0 422107686 47484928 11083 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 11083 603 41 0 11552 0
vsize: 46372
[startup+470.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13404 0 0 0 46972 44 0 0 25 0 1 0 422107686 47484928 11084 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 11084 603 41 0 11552 0
vsize: 46372
[startup+480.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13404 0 0 0 47972 44 0 0 25 0 1 0 422107686 47484928 11084 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11593 11084 603 41 0 11552 0
vsize: 46372
[startup+490.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13414 0 0 0 48972 44 0 0 25 0 1 0 422107686 47681536 11094 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11641 11094 603 41 0 11600 0
vsize: 46564
[startup+500.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13425 0 0 0 49972 44 0 0 25 0 1 0 422107686 47681536 11105 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11641 11105 603 41 0 11600 0
vsize: 46564
[startup+510.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13435 0 0 0 50973 44 0 0 25 0 1 0 422107686 47681536 11115 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11641 11115 603 41 0 11600 0
vsize: 46564
[startup+520.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13566 0 0 0 51972 44 0 0 25 0 1 0 422107686 48205824 11246 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11769 11246 603 41 0 11728 0
vsize: 47076
[startup+530.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13963 0 0 0 52972 45 0 0 25 0 1 0 422107686 49909760 11643 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12185 11643 603 41 0 12144 0
vsize: 48740
[startup+540.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14301 0 0 0 53971 46 0 0 25 0 1 0 422107686 51220480 11981 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12505 11981 603 41 0 12464 0
vsize: 50020
[startup+550.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14546 0 0 0 54970 47 0 0 25 0 1 0 422107686 52092928 12172 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12172 603 41 0 12677 0
vsize: 50872
[startup+560.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14546 0 0 0 55971 47 0 0 25 0 1 0 422107686 52092928 12172 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12172 603 41 0 12677 0
vsize: 50872
[startup+570.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14546 0 0 0 56971 47 0 0 25 0 1 0 422107686 52092928 12172 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12172 603 41 0 12677 0
vsize: 50872
[startup+580.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14546 0 0 0 57971 47 0 0 25 0 1 0 422107686 52092928 12172 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12172 603 41 0 12677 0
vsize: 50872
[startup+590.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14546 0 0 0 58972 47 0 0 25 0 1 0 422107686 52092928 12172 4294967295 134512640 134672761 3221224576 3221223616 134612838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12172 603 41 0 12677 0
vsize: 50872
[startup+600.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14547 0 0 0 59972 47 0 0 25 0 1 0 422107686 52092928 12173 4294967295 134512640 134672761 3221224576 3221223616 134613771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12173 603 41 0 12677 0
vsize: 50872
[startup+610.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14547 0 0 0 60973 47 0 0 25 0 1 0 422107686 52092928 12173 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12173 603 41 0 12677 0
vsize: 50872
[startup+620.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 61973 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12175 603 41 0 12677 0
vsize: 50872
[startup+630.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 62973 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12175 603 41 0 12677 0
vsize: 50872
[startup+640.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 63973 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12175 603 41 0 12677 0
vsize: 50872
[startup+650.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 64974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12175 603 41 0 12677 0
vsize: 50872
[startup+660.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 65974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12175 603 41 0 12677 0
vsize: 50872
[startup+670.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 66974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12175 603 41 0 12677 0
vsize: 50872
[startup+680.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 67974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12175 603 41 0 12677 0
vsize: 50872
[startup+690.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 68974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12175 603 41 0 12677 0
vsize: 50872
[startup+700.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 69974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12718 12175 603 41 0 12677 0
vsize: 50872
[startup+710.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14841 0 0 0 70973 48 0 0 25 0 1 0 422107686 53420032 12467 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13042 12467 603 41 0 13001 0
vsize: 52168
[startup+720.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15143 0 0 0 71973 49 0 0 25 0 1 0 422107686 54685696 12769 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13351 12769 603 41 0 13310 0
vsize: 53404
[startup+730.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15485 0 0 0 72972 49 0 0 25 0 1 0 422107686 56123392 13111 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13702 13111 603 41 0 13661 0
vsize: 54808
[startup+740.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 73973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+750.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 74973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223616 134613769 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+760.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 75973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+770.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 76973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223568 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+780.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 77973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+790.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 78973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+800.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 79974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+810.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 80974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+820.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 81974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+830.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 82974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+840.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 83974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+850.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 84974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13243 603 41 0 13762 0
vsize: 55212
[startup+860.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15646 0 0 0 85975 50 0 0 25 0 1 0 422107686 56537088 13244 4294967295 134512640 134672761 3221224576 3221223616 134612851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13244 603 41 0 13762 0
vsize: 55212
[startup+870.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15648 0 0 0 86975 50 0 0 25 0 1 0 422107686 56537088 13246 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13246 603 41 0 13762 0
vsize: 55212
[startup+880.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15649 0 0 0 87975 50 0 0 25 0 1 0 422107686 56537088 13247 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13247 603 41 0 13762 0
vsize: 55212
[startup+890.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15649 0 0 0 88975 50 0 0 25 0 1 0 422107686 56537088 13247 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13247 603 41 0 13762 0
vsize: 55212
[startup+900.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15649 0 0 0 89975 50 0 0 25 0 1 0 422107686 56537088 13247 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13247 603 41 0 13762 0
vsize: 55212
[startup+910.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15649 0 0 0 90976 50 0 0 25 0 1 0 422107686 56537088 13247 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13247 603 41 0 13762 0
vsize: 55212
[startup+920.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15649 0 0 0 91976 50 0 0 25 0 1 0 422107686 56537088 13247 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 13247 603 41 0 13762 0
vsize: 55212
[startup+930.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15842 0 0 0 92975 50 0 0 25 0 1 0 422107686 57327616 13440 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13996 13440 603 41 0 13955 0
vsize: 55984
[startup+940.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 93975 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+950.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 94975 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+960.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 95975 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+970.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 96975 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+980.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 97976 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+990.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 98976 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1000.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 99976 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223776 134610642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1010.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 100976 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1020.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 101976 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1030.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 102977 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1040.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 103977 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1050.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 104977 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1060.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 105977 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1070.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 106977 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1080.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 107978 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1090.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 108978 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1100.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 109978 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1110.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 110978 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1120.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 111978 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13729 603 41 0 14243 0
vsize: 57136
[startup+1130.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16192 0 0 0 112978 51 0 0 25 0 1 0 422107686 58507264 13731 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13731 603 41 0 14243 0
vsize: 57136
[startup+1140.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16194 0 0 0 113979 51 0 0 25 0 1 0 422107686 58507264 13733 4294967295 134512640 134672761 3221224576 3221223760 134615951 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14284 13733 603 41 0 14243 0
vsize: 57136
[startup+1150.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16445 0 0 0 114978 51 0 0 25 0 1 0 422107686 59817984 13984 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14604 13984 603 41 0 14563 0
vsize: 58416
[startup+1160.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16668 0 0 0 115978 52 0 0 25 0 1 0 422107686 60276736 14110 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14716 14110 603 41 0 14675 0
vsize: 58864
[startup+1170.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16668 0 0 0 116979 52 0 0 25 0 1 0 422107686 60276736 14110 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14716 14110 603 41 0 14675 0
vsize: 58864
[startup+1180.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16668 0 0 0 117979 52 0 0 25 0 1 0 422107686 60276736 14110 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14716 14110 603 41 0 14675 0
vsize: 58864
[startup+1190.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16668 0 0 0 118979 52 0 0 25 0 1 0 422107686 60276736 14110 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14716 14110 603 41 0 14675 0
vsize: 58864
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24262
Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16668 0 0 0 119979 52 0 0 25 0 1 0 422107686 60276736 14110 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14716 14110 603 41 0 14675 0
vsize: 58864
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 24262
Raw data (stat): 24262 (minisat+) Z 24261 20937 20936 0 -1 12 16669 0 0 0 119979 54 0 0 25 0 1 0 422107686 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: 10
Real time (s): 1200.18
CPU time (s): 1200.35
CPU user time (s): 1199.8
CPU system time (s): 0.549916
CPU usage (%): 100.014
Max. virtual memory (Kb): 58864
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####