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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-set1cl.opb
MD5SUM	4468fb60f3f07c6d5f7ce05d137a7203
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3323904
Optimality of the best value was proved	NO
Number of terms in the objective function	4880
Biggest coefficient in the objective function	10485760
Number of bits for the biggest coefficient in the objective function	24
Sum of the numbers in the objective function	1581429279
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	10485760
Number of bits of the biggest number in a constraint	24
Biggest sum of numbers in a constraint	1581429279
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1240.2
Number of variables	9680
Total number of constraints	732
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	240
Number of constraints which are nor clauses,nor cardinality constraints	492
Minimum length of a constraint	1
Maximum length of a constraint	420
Trace number 31120

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-05-25 22:12:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22515 boxname=wulflinc23 idbench=1331 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  4468fb60f3f07c6d5f7ce05d137a7203  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-set1cl.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-set1cl.opb
IDLAUNCH: 22515
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        606616 kB
Buffers:         33508 kB
Cached:         372736 kB
SwapCached:        532 kB
Active:          26676 kB
Inactive:       381972 kB
HighTotal:      131008 kB
HighFree:         2576 kB
LowTotal:       903652 kB
LowFree:        604040 kB
SwapTotal:     2097136 kB
SwapFree:      2096016 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5628 kB
Slab:            13880 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 22:33:02 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 22515 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 732 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 731]---> Adder-cost: 660   maxlim: 1948523   bits: 22/21
c ---[ 730]---> Adder-cost: 660   maxlim: 1882987   bits: 22/21
c ---[ 729]---> Adder-cost: 650   maxlim: 1424235   bits: 22/21
c ---[ 728]---> Adder-cost: 650   maxlim: 1391467   bits: 22/21
c ---[ 727]---> Adder-cost: 644   maxlim: 1293163   bits: 22/21
c ---[ 726]---> Adder-cost: 636   maxlim: 1162091   bits: 22/21
c ---[ 725]---> Adder-cost: 633   maxlim: 916331   bits: 21/20
c ---[ 724]---> Adder-cost: 610   maxlim: 637803   bits: 21/20
c ---[ 723]---> Adder-cost: 608   maxlim: 605035   bits: 21/20
c ---[ 722]---> Adder-cost: 594   maxlim: 383851   bits: 20/19
c ---[ 721]---> Adder-cost: 569   maxlim: 228203   bits: 19/18
c ---[ 720]---> Adder-cost: 524   maxlim: 31595   bits: 16/15
c ---[ 718]---> BDD-cost:   59
c ---[ 716]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 714]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 712]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 710]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 708]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 706]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 704]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 702]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 700]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 698]---> BDD-cost:  125
c ---[ 696]---> BDD-cost:   60
c ---[ 694]---> BDD-cost:   66
c ---[ 692]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 690]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 688]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 686]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 684]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 682]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 680]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 678]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 676]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 674]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 672]---> BDD-cost:   60
c ---[ 670]---> BDD-cost:   54
c ---[ 668]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 666]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 664]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 662]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 660]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 658]---> Sorter-cost:  352     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 656]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 654]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 652]---> BDD-cost:  123
c ---[ 650]---> BDD-cost:  118
c ---[ 648]---> BDD-cost:   55
c ---[ 646]---> BDD-cost:   61
c ---[ 644]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 642]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 640]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 638]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 636]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 634]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 632]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 630]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 628]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> BDD-cost:   60
c ---[ 622]---> BDD-cost:   69
c ---[ 620]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 618]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 616]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 614]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 612]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 610]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 608]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 606]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 604]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 602]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 600]---> BDD-cost:   65
c ---[ 598]---> BDD-cost:   71
c ---[ 596]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 594]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 590]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 588]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 584]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 582]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 580]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 578]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 576]---> BDD-cost:   65
c ---[ 574]---> BDD-cost:   56
c ---[ 572]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 570]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 568]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 566]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 564]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> BDD-cost:  147
c ---[ 560]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 558]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 556]---> BDD-cost:  119
c ---[ 554]---> BDD-cost:  118
c ---[ 552]---> BDD-cost:   55
c ---[ 550]---> BDD-cost:   62
c ---[ 548]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 546]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 544]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 542]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 540]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 538]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 536]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 534]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 532]---> BDD-cost:  132
c ---[ 530]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> BDD-cost:   60
c ---[ 526]---> BDD-cost:   64
c ---[ 524]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 522]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 520]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 514]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 508]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 506]---> BDD-cost:  118
c ---[ 504]---> BDD-cost:   60
c ---[ 502]---> BDD-cost:   66
c ---[ 500]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> BDD-cost:  130
c ---[ 480]---> BDD-cost:   65
c ---[ 478]---> BDD-cost:   61
c ---[ 476]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 470]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 464]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> BDD-cost:  117
c ---[ 456]---> BDD-cost:   55
c ---[ 454]---> BDD-cost:   53
c ---[ 452]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 438]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> BDD-cost:  129
c ---[ 434]---> BDD-cost:  125
c ---[ 432]---> BDD-cost:   55
c ---[ 430]---> BDD-cost:   61
c ---[ 428]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 426]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 420]---> BDD-cost:  158
c ---[ 418]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 416]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 414]---> BDD-cost:  141
c ---[ 412]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 410]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 408]---> BDD-cost:   60
c ---[ 406]---> BDD-cost:   61
c ---[ 404]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 398]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 390]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 388]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> BDD-cost:   60
c ---[ 382]---> BDD-cost:   61
c ---[ 380]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> BDD-cost:  158
c ---[ 370]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> BDD-cost:  115
c ---[ 360]---> BDD-cost:   60
c ---[ 358]---> BDD-cost:   59
c ---[ 356]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 354]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 346]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 344]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 342]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 336]---> BDD-cost:   60
c ---[ 334]---> BDD-cost:   64
c ---[ 332]---> BDD-cost:  158
c ---[ 330]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> BDD-cost:  124
c ---[ 314]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> BDD-cost:   60
c ---[ 310]---> BDD-cost:   59
c ---[ 308]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> BDD-cost:  124
c ---[ 288]---> BDD-cost:   60
c ---[ 286]---> BDD-cost:   66
c ---[ 284]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost:  325     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> BDD-cost:   60
c ---[ 262]---> BDD-cost:   60
c ---[ 260]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 256]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 250]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 248]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 246]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> Sorter-cost:  347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 242]---> BDD-cost:  124
c ---[ 240]---> BDD-cost:   65
c ---[ 239]---> BDD-cost:   24
c ---[ 238]---> BDD-cost:   22
c ---[ 237]---> BDD-cost:   24
c ---[ 236]---> BDD-cost:   25
c ---[ 235]---> BDD-cost:   23
c ---[ 234]---> BDD-cost:   23
c ---[ 233]---> BDD-cost:   23
c ---[ 232]---> BDD-cost:   22
c ---[ 231]---> BDD-cost:   23
c ---[ 230]---> BDD-cost:   21
c ---[ 229]---> BDD-cost:   19
c ---[ 228]---> BDD-cost:   18
c ---[ 227]---> BDD-cost:   27
c ---[ 226]---> BDD-cost:   26
c ---[ 225]---> BDD-cost:   21
c ---[ 224]---> BDD-cost:   24
c ---[ 223]---> BDD-cost:   21
c ---[ 222]---> BDD-cost:   25
c ---[ 221]---> BDD-cost:   21
c ---[ 220]---> BDD-cost:   22
c ---[ 219]---> BDD-cost:   23
c ---[ 218]---> BDD-cost:   18
c ---[ 217]---> BDD-cost:   21
c ---[ 216]---> BDD-cost:   16
c ---[ 215]---> BDD-cost:   22
c ---[ 214]---> BDD-cost:   21
c ---[ 213]---> BDD-cost:   23
c ---[ 212]---> BDD-cost:   21
c ---[ 211]---> BDD-cost:   21
c ---[ 210]---> BDD-cost:   23
c ---[ 209]---> BDD-cost:   19
c ---[ 208]---> BDD-cost:   16
c ---[ 207]---> BDD-cost:   19
c ---[ 206]---> BDD-cost:   19
c ---[ 205]---> BDD-cost:   19
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   25
c ---[ 202]---> BDD-cost:   23
c ---[ 201]---> BDD-cost:   22
c ---[ 200]---> BDD-cost:   25
c ---[ 199]---> BDD-cost:   23
c ---[ 198]---> BDD-cost:   25
c ---[ 197]---> BDD-cost:   25
c ---[ 196]---> BDD-cost:   21
c ---[ 195]---> BDD-cost:   23
c ---[ 194]---> BDD-cost:   20
c ---[ 193]---> BDD-cost:   21
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   28
c ---[ 190]---> BDD-cost:   26
c ---[ 189]---> BDD-cost:   27
c ---[ 188]---> BDD-cost:   27
c ---[ 187]---> BDD-cost:   27
c ---[ 186]---> BDD-cost:   27
c ---[ 185]---> BDD-cost:   27
c ---[ 184]---> BDD-cost:   24
c ---[ 183]---> BDD-cost:   25
c ---[ 182]---> BDD-cost:   24
c ---[ 181]---> BDD-cost:   22
c ---[ 180]---> BDD-cost:   17
c ---[ 179]---> BDD-cost:   29
c ---[ 178]---> BDD-cost:   26
c ---[ 177]---> BDD-cost:   27
c ---[ 176]---> BDD-cost:   23
c ---[ 175]---> BDD-cost:   24
c ---[ 174]---> BDD-cost:   26
c ---[ 173]---> BDD-cost:   24
c ---[ 172]---> BDD-cost:   24
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   25
c ---[ 169]---> BDD-cost:   21
c ---[ 168]---> BDD-cost:   21
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   22
c ---[ 165]---> BDD-cost:   22
c ---[ 164]---> BDD-cost:   23
c ---[ 163]---> BDD-cost:   20
c ---[ 162]---> BDD-cost:   20
c ---[ 161]---> BDD-cost:   16
c ---[ 160]---> BDD-cost:   17
c ---[ 159]---> BDD-cost:   21
c ---[ 158]---> BDD-cost:   20
c ---[ 157]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:   17
c ---[ 155]---> BDD-cost:   27
c ---[ 154]---> BDD-cost:   25
c ---[ 153]---> BDD-cost:   22
c ---[ 152]---> BDD-cost:   24
c ---[ 151]---> BDD-cost:   22
c ---[ 150]---> BDD-cost:   25
c ---[ 149]---> BDD-cost:   24
c ---[ 148]---> BDD-cost:   22
c ---[ 147]---> BDD-cost:   23
c ---[ 146]---> BDD-cost:   21
c ---[ 145]---> BDD-cost:   21
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   27
c ---[ 142]---> BDD-cost:   27
c ---[ 141]---> BDD-cost:   24
c ---[ 140]---> BDD-cost:   25
c ---[ 139]---> BDD-cost:   24
c ---[ 138]---> BDD-cost:   25
c ---[ 137]---> BDD-cost:   25
c ---[ 136]---> BDD-cost:   20
c ---[ 135]---> BDD-cost:   22
c ---[ 134]---> BDD-cost:   22
c ---[ 133]---> BDD-cost:   21
c ---[ 132]---> BDD-cost:   19
c ---[ 131]---> BDD-cost:   26
c ---[ 130]---> BDD-cost:   27
c ---[ 129]---> BDD-cost:   27
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   22
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   25
c ---[ 124]---> BDD-cost:   24
c ---[ 123]---> BDD-cost:   22
c ---[ 122]---> BDD-cost:   23
c ---[ 121]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:   21
c ---[ 119]---> BDD-cost:   22
c ---[ 118]---> BDD-cost:   25
c ---[ 117]---> BDD-cost:   23
c ---[ 116]---> BDD-cost:   23
c ---[ 115]---> BDD-cost:   21
c ---[ 114]---> BDD-cost:   22
c ---[ 113]---> BDD-cost:   23
c ---[ 112]---> BDD-cost:   23
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:   20
c ---[ 109]---> BDD-cost:   19
c ---[ 108]---> BDD-cost:   17
c ---[ 107]---> BDD-cost:   25
c ---[ 106]---> BDD-cost:   25
c ---[ 105]---> BDD-cost:   25
c ---[ 104]---> BDD-cost:   21
c ---[ 103]---> BDD-cost:   23
c ---[ 102]---> BDD-cost:   22
c ---[ 101]---> BDD-cost:   23
c ---[ 100]---> BDD-cost:   22
c ---[  99]---> BDD-cost:   21
c ---[  98]---> BDD-cost:   21
c ---[  97]---> BDD-cost:   21
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   25
c ---[  94]---> BDD-cost:   24
c ---[  93]---> BDD-cost:   23
c ---[  92]---> BDD-cost:   25
c ---[  91]---> BDD-cost:   23
c ---[  90]---> BDD-cost:   21
c ---[  89]---> BDD-cost:   21
c ---[  88]---> BDD-cost:   22
c ---[  87]---> BDD-cost:   23
c ---[  86]---> BDD-cost:   21
c ---[  85]---> BDD-cost:   21
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   25
c ---[  82]---> BDD-cost:   24
c ---[  81]---> BDD-cost:   25
c ---[  80]---> BDD-cost:   25
c ---[  79]---> BDD-cost:   25
c ---[  78]---> BDD-cost:   23
c ---[  77]---> BDD-cost:   21
c ---[  76]---> BDD-cost:   23
c ---[  75]---> BDD-cost:   20
c ---[  74]---> BDD-cost:   20
c ---[  73]---> BDD-cost:   21
c ---[  72]---> BDD-cost:   18
c ---[  71]---> BDD-cost:   22
c ---[  70]---> BDD-cost:   25
c ---[  69]---> BDD-cost:   25
c ---[  68]---> BDD-cost:   19
c ---[  67]---> BDD-cost:   25
c ---[  66]---> BDD-cost:   19
c ---[  65]---> BDD-cost:   19
c ---[  64]---> BDD-cost:   23
c ---[  63]---> BDD-cost:   23
c ---[  62]---> BDD-cost:   21
c ---[  61]---> BDD-cost:   21
c ---[  60]---> BDD-cost:   19
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   24
c ---[  57]---> BDD-cost:   25
c ---[  56]---> BDD-cost:   21
c ---[  55]---> BDD-cost:   20
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   23
c ---[  52]---> BDD-cost:   22
c ---[  51]---> BDD-cost:   23
c ---[  50]---> BDD-cost:   21
c ---[  49]---> BDD-cost:   18
c ---[  48]---> BDD-cost:   19
c ---[  47]---> BDD-cost:   24
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   24
c ---[  44]---> BDD-cost:   25
c ---[  43]---> BDD-cost:   24
c ---[  42]---> BDD-cost:   24
c ---[  41]---> BDD-cost:   23
c ---[  40]---> BDD-cost:   20
c ---[  39]---> BDD-cost:   23
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:   21
c ---[  36]---> BDD-cost:   18
c ---[  35]---> BDD-cost:   25
c ---[  34]---> BDD-cost:   25
c ---[  33]---> BDD-cost:   25
c ---[  32]---> BDD-cost:   25
c ---[  31]---> BDD-cost:   20
c ---[  30]---> BDD-cost:   21
c ---[  29]---> BDD-cost:   22
c ---[  28]---> BDD-cost:   22
c ---[  27]---> BDD-cost:   23
c ---[  26]---> BDD-cost:   20
c ---[  25]---> BDD-cost:   19
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   25
c ---[  22]---> BDD-cost:   27
c ---[  21]---> BDD-cost:   25
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   25
c ---[  16]---> BDD-cost:   25
c ---[  15]---> BDD-cost:   24
c ---[  14]---> BDD-cost:   23
c ---[  13]---> BDD-cost:   23
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   27
c ---[  10]---> BDD-cost:   27
c ---[   9]---> BDD-cost:   26
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   22
c ---[   4]---> BDD-cost:   24
c ---[   3]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   20
c ---[   1]---> BDD-cost:   23
c ---[   0]---> BDD-cost:   21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  225269   599765 |   75089       0        0     nan |  0.000 % |
c |       100 |  225034   599242 |   82597      73      236     3.2 | 13.200 % |
c |       250 |  224543   598144 |   90857     161      495     3.1 | 13.374 % |
c |       475 |  223251   595187 |   99943     275      839     3.1 | 13.864 % |
c |       812 |  222049   592494 |  109937     468     1501     3.2 | 14.284 % |
c |      1318 |  220116   588150 |  120931     743     2410     3.2 | 14.999 % |
c |      2077 |  216593   580137 |  133024    1146     3832     3.3 | 16.308 % |
c |      3216 |  212204   570209 |  146327    1830     6112     3.3 | 17.907 % |
c |      4924 |  206683   557685 |  160959    2943    10024     3.4 | 19.948 % |
c |      7488 |  201113   544910 |  177055    4973    17906     3.6 | 22.060 % |
c |     11332 |  197250   536105 |  194761    8374    32627     3.9 | 23.550 % |
c |     17098 |  195871   532888 |  214237   13980    62180     4.4 | 24.111 % |
c |     25747 |  194806   530370 |  235661   22546   116227     5.2 | 24.544 % |
c ==============================================================================
c [1mFound solution: 74840032[0m
c ---[   0]---> Adder-cost: 14114   maxlim: 255953471   bits: 29/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29932 |  293157   881972 |   97719   26701   149591     5.6 | 24.544 % |
c |     30032 |  293116   881861 |  107490   26794   150079     5.6 | 21.040 % |
c |     30182 |  293099   881823 |  118239   26941   151014     5.6 | 21.046 % |
c |     30407 |  292932   881404 |  130063   27147   152654     5.6 | 21.104 % |
c |     30744 |  292831   881127 |  143070   27481   155090     5.6 | 21.127 % |
c |     31250 |  292806   881067 |  157377   27986   158808     5.7 | 21.135 % |
c |     32009 |  292706   880785 |  173115   28738   165476     5.8 | 21.157 % |
c ==============================================================================
c [1mFound solution: 59063636[0m
c ---[   0]---> Adder-cost: 6078   maxlim: 269567179   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32995 |  335155  1032480 |  111718   29724   174622     5.9 | 21.157 % |
c |     33097 |  335118  1032380 |  122889   29824   175213     5.9 | 19.913 % |
c |     33247 |  335118  1032380 |  135178   29974   176188     5.9 | 19.913 % |
c |     33472 |  335049  1032166 |  148696   30193   177569     5.9 | 19.920 % |
c |     33809 |  335028  1032119 |  163566   30529   179844     5.9 | 19.926 % |
c |     34315 |  334947  1031918 |  179922   31026   182771     5.9 | 19.952 % |
c |     35074 |  334788  1031468 |  197915   31772   188093     5.9 | 19.980 % |
c |     36213 |  334613  1031016 |  217706   32890   195234     5.9 | 20.028 % |
c |     37921 |  334571  1030896 |  239477   34596   207464     6.0 | 20.035 % |
c |     40483 |  334397  1030447 |  263425   37143   228821     6.2 | 20.085 % |
c |     44327 |  334081  1029616 |  289767   40959   252597     6.2 | 20.174 % |
c |     50094 |  334037  1029514 |  318744   46720   294483     6.3 | 20.188 % |
c |     58744 |  333777  1028850 |  350618   55343   369254     6.7 | 20.258 % |
c |     71718 |  333600  1028408 |  385680   68299   506515     7.4 | 20.309 % |
c |     91180 |  333536  1028254 |  424248   87752   784802     8.9 | 20.330 % |
c |    120372 |  333439  1028005 |  466673  116934  1778992    15.2 | 20.357 % |
c |    164161 |  333089  1027088 |  513341  160694  2385606    14.8 | 20.447 % |
c |    229845 |  332922  1026634 |  564675  226365  4199669    18.6 | 20.487 % |
c |    328371 |  332848  1026452 |  621142  324883  7604253    23.4 | 20.510 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 21036 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.99 0.97 0.92 2/54 21032
Raw data (stat): 21032 (runsolver) R 21031 5562 5561 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842387708 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99961 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+19.9999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+29.9999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.73 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 21036
Raw data (stat): 21032 (minisat+_script) S 21031 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387708 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.73
CPU time (s): 1229.89
CPU user time (s): 1228.97
CPU system time (s): 0.91586
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####