Some explanations

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

General information on the benchmark

Nameweb/uclid_pb_benchmarks/normalized-ooo.tag14.ucl.opb
MD5SUMe4be8a88d340bbbbfb27e034f74a6524
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 65
Number of bits of the biggest number in a constraint 7
Biggest sum of numbers in a constraint 254
Number of bits of the biggest sum of numbers8
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark148.053
Number of variables40605
Total number of constraints118930
Number of constraints which are clauses117190
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1740
Minimum length of a constraint1
Maximum length of a constraint13

Trace number 2456

Launcher Data

LAUNCH ON wulflinc29 THE 2005-09-18 19:56:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3850 boxname=wulflinc29 idbench=334 idsolver=4 numberseed=0
MD5SUM SOLVER: 21c3ffd7205c96d5f0784fd273b92938  /oldhome/oroussel/solvers/PBS4
MD5SUM BENCH:  e4be8a88d340bbbbfb27e034f74a6524  /oldhome/oroussel/tmp/wulflinc29/normalized-ooo.tag14.ucl.opb
REAL COMMAND:  PBS4 /oldhome/oroussel/tmp/wulflinc29/normalized-ooo.tag14.ucl.opb
IDLAUNCH: 3850
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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	: 3
cpu MHz		: 451.020
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:        907196 kB
Buffers:         33568 kB
Cached:          64104 kB
SwapCached:        792 kB
Active:          32724 kB
Inactive:        67684 kB
HighTotal:      131008 kB
HighFree:        65800 kB
LowTotal:       903652 kB
LowFree:        841396 kB
SwapTotal:     2097892 kB
SwapFree:      2096664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            21372 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:00:20 (client local time) WITH STATUS 20 IN 229.438 SECONDS
stats: 3850 7 229.438 20

Solver Data

c PBS v4 by Bashar Al-Rawi & Fadi Aloul
c Solving /oldhome/oroussel/tmp/wulflinc29/normalized-ooo.tag14.ucl.opb ......
s UNSATISFIABLE
c Done, CPU Time=224.083

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 18 0 0 0 0 0 0 0 22 0 1 0 1843934176 978944 2 4294967295 134512640 135450776 3221224576 3221224576 134512960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24531/statm): 239 2 232 232 0 7 0
[pid=24531] vsize: 956
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-ooo.tag14.ucl.opb
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-ooo.tag14.ucl.opb

[startup+10.0027 s]
Raw data (loadavg): 0.89 0.97 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 5578 0 0 0 969 19 0 0 25 0 1 0 1843934176 21721088 4562 4294967295 134512640 135450776 3221224576 3221223296 134539285 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 5303 4562 232 232 0 5071 0
[pid=24531] vsize: 21212
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 21212

[startup+20.0035 s]
Raw data (loadavg): 0.90 0.97 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 6412 0 0 0 1958 25 0 0 25 0 1 0 1843934176 25526272 5363 4294967295 134512640 135450776 3221224576 3221223376 134547495 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 6232 5363 232 232 0 6000 0
[pid=24531] vsize: 24928
Current children cumulated CPU time (s) 19.83
Current children cumulated vsize (Kb) 24928

[startup+30.0042 s]
Raw data (loadavg): 0.92 0.97 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 7034 0 0 0 2941 32 0 0 25 0 1 0 1843934176 28803072 5985 4294967295 134512640 135450776 3221224576 3221222912 134533833 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 7032 5985 232 232 0 6800 0
[pid=24531] vsize: 28128
Current children cumulated CPU time (s) 29.73
Current children cumulated vsize (Kb) 28128

[startup+40.004 s]
Raw data (loadavg): 0.93 0.97 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 7582 0 0 0 3924 38 0 0 25 0 1 0 1843934176 31965184 6533 4294967295 134512640 135450776 3221224576 3221223424 134540058 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 7804 6533 232 232 0 7572 0
[pid=24531] vsize: 31216
Current children cumulated CPU time (s) 39.62
Current children cumulated vsize (Kb) 31216

[startup+50.0048 s]
Raw data (loadavg): 0.94 0.97 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 7816 0 0 0 4909 42 0 0 25 0 1 0 1843934176 32911360 6767 4294967295 134512640 135450776 3221224576 3221222912 134533833 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24531/statm): 8035 6767 232 232 0 7803 0
[pid=24531] vsize: 32140
Current children cumulated CPU time (s) 49.51
Current children cumulated vsize (Kb) 32140

[startup+60.0046 s]
Raw data (loadavg): 0.95 0.97 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 7929 0 0 0 5889 49 0 0 25 0 1 0 1843934176 37376000 6880 4294967295 134512640 135450776 3221224576 3221222912 134533864 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24531/statm): 9125 6880 232 232 0 8893 0
[pid=24531] vsize: 36500
Current children cumulated CPU time (s) 59.38
Current children cumulated vsize (Kb) 36500

[startup+70.0054 s]
Raw data (loadavg): 0.96 0.97 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8081 0 0 0 6874 54 0 0 25 0 1 0 1843934176 38051840 7032 4294967295 134512640 135450776 3221224576 3221223296 134539307 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9290 7032 232 232 0 9058 0
[pid=24531] vsize: 37160
Current children cumulated CPU time (s) 69.28
Current children cumulated vsize (Kb) 37160

[startup+80.0061 s]
Raw data (loadavg): 0.96 0.97 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8190 0 0 0 7861 58 0 0 25 0 1 0 1843934176 38322176 7141 4294967295 134512640 135450776 3221224576 3221223296 134539323 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9356 7141 232 232 0 9124 0
[pid=24531] vsize: 37424
Current children cumulated CPU time (s) 79.19
Current children cumulated vsize (Kb) 37424

[startup+90.0059 s]
Raw data (loadavg): 0.97 0.97 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8295 0 0 0 8845 65 0 0 25 0 1 0 1843934176 38592512 7246 4294967295 134512640 135450776 3221224576 3221223424 134540101 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9422 7246 232 232 0 9190 0
[pid=24531] vsize: 37688
Current children cumulated CPU time (s) 89.1
Current children cumulated vsize (Kb) 37688

[startup+100.007 s]
Raw data (loadavg): 0.97 0.97 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8403 0 0 0 9835 68 0 0 25 0 1 0 1843934176 38727680 7354 4294967295 134512640 135450776 3221224576 3221223296 134539321 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9455 7354 232 232 0 9223 0
[pid=24531] vsize: 37820
Current children cumulated CPU time (s) 99.03
Current children cumulated vsize (Kb) 37820

[startup+110.007 s]
Raw data (loadavg): 1.05 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8544 0 0 0 10819 73 0 0 25 0 1 0 1843934176 38862848 7415 4294967295 134512640 135450776 3221224576 3221223296 134539413 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9488 7415 232 232 0 9256 0
[pid=24531] vsize: 37952
Current children cumulated CPU time (s) 108.92
Current children cumulated vsize (Kb) 37952

[startup+120.008 s]
Raw data (loadavg): 1.04 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8789 0 0 0 11808 78 0 0 25 0 1 0 1843934176 39534592 7547 4294967295 134512640 135450776 3221224576 3221223296 134539465 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9652 7547 232 232 0 9420 0
[pid=24531] vsize: 38608
Current children cumulated CPU time (s) 118.86
Current children cumulated vsize (Kb) 38608

[startup+130.008 s]
Raw data (loadavg): 1.04 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8793 0 0 0 12790 84 0 0 25 0 1 0 1843934176 39534592 7551 4294967295 134512640 135450776 3221224576 3221223296 134539536 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9652 7551 232 232 0 9420 0
[pid=24531] vsize: 38608
Current children cumulated CPU time (s) 128.74
Current children cumulated vsize (Kb) 38608

[startup+140.008 s]
Raw data (loadavg): 1.03 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9059 0 0 0 13777 90 0 0 25 0 1 0 1843934176 39800832 7657 4294967295 134512640 135450776 3221224576 3221223296 134539591 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9717 7657 232 232 0 9485 0
[pid=24531] vsize: 38868
Current children cumulated CPU time (s) 138.67
Current children cumulated vsize (Kb) 38868

[startup+150.009 s]
Raw data (loadavg): 1.03 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9325 0 0 0 14765 95 0 0 25 0 1 0 1843934176 39800832 7923 4294967295 134512640 135450776 3221224576 3221223296 134539323 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9717 7923 232 232 0 9485 0
[pid=24531] vsize: 38868
Current children cumulated CPU time (s) 148.6
Current children cumulated vsize (Kb) 38868

[startup+160.008 s]
Raw data (loadavg): 1.02 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9533 0 0 0 15758 98 0 0 25 0 1 0 1843934176 39800832 8051 4294967295 134512640 135450776 3221224576 3221223296 134539307 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9717 8051 232 232 0 9485 0
[pid=24531] vsize: 38868
Current children cumulated CPU time (s) 158.56
Current children cumulated vsize (Kb) 38868

[startup+170.008 s]
Raw data (loadavg): 1.02 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9622 0 0 0 16740 103 0 0 25 0 1 0 1843934176 39800832 8140 4294967295 134512640 135450776 3221224576 3221223296 134539418 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9717 8140 232 232 0 9485 0
[pid=24531] vsize: 38868
Current children cumulated CPU time (s) 168.43
Current children cumulated vsize (Kb) 38868

[startup+180.009 s]
Raw data (loadavg): 1.01 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9714 0 0 0 17721 110 0 0 25 0 1 0 1843934176 39800832 8152 4294967295 134512640 135450776 3221224576 3221223296 134539392 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9717 8152 232 232 0 9485 0
[pid=24531] vsize: 38868
Current children cumulated CPU time (s) 178.31
Current children cumulated vsize (Kb) 38868

[startup+190.009 s]
Raw data (loadavg): 1.01 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9801 0 0 0 18712 114 0 0 25 0 1 0 1843934176 39800832 8159 4294967295 134512640 135450776 3221224576 3221223296 134539413 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 9717 8159 232 232 0 9485 0
[pid=24531] vsize: 38868
Current children cumulated CPU time (s) 188.26
Current children cumulated vsize (Kb) 38868

[startup+200.01 s]
Raw data (loadavg): 1.01 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9886 0 0 0 19695 119 0 0 25 0 1 0 1843934176 39800832 8164 4294967295 134512640 135450776 3221224576 3221223296 134539323 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24531/statm): 9717 8164 232 232 0 9485 0
[pid=24531] vsize: 38868
Current children cumulated CPU time (s) 198.14
Current children cumulated vsize (Kb) 38868

[startup+210.01 s]
Raw data (loadavg): 1.01 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 10772 0 0 0 20685 124 0 0 25 0 1 0 1843934176 42946560 8201 4294967295 134512640 135450776 3221224576 3221223296 134539536 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24531/statm): 10485 8201 232 232 0 10253 0
[pid=24531] vsize: 41940
Current children cumulated CPU time (s) 208.09
Current children cumulated vsize (Kb) 41940

[startup+220.01 s]
Raw data (loadavg): 1.01 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 11051 0 0 0 21675 129 0 0 25 0 1 0 1843934176 42946560 8480 4294967295 134512640 135450776 3221224576 3221223280 134536415 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24531/statm): 10485 8480 232 232 0 10253 0
[pid=24531] vsize: 41940
Current children cumulated CPU time (s) 218.04
Current children cumulated vsize (Kb) 41940

[startup+230.011 s]
Raw data (loadavg): 1.00 0.99 0.99 2/56 24531
Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 11310 0 0 0 22668 132 0 0 25 0 1 0 1843934176 51601408 8739 4294967295 134512640 135450776 3221224576 3221223296 134539307 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24531/statm): 12598 8739 232 232 0 12366 0
[pid=24531] vsize: 50392
Current children cumulated CPU time (s) 228
Current children cumulated vsize (Kb) 50392
One traced child (pid=24531) exited with status: 20
All traced children have exited ! Game is over.

Child status: 20
Real time (s): 231.456
CPU time (s): 229.438
CPU user time (s): 228.096
CPU system time (s): 1.3418
CPU usage (%): 99.1283
Max. virtual memory (cumulated for all children) (Kb): 50392

Verifier Data

ERROR: no interpretation found !