

__def_1 is now fully defined.
__def_2 is now fully defined.
__def_4 is now fully defined.
killed is now fully defined.
__def_6 is now fully defined.

not_richer is now fully defined.
#q3 is now fully defined.
hates is now fully defined.
#q2 is now fully defined.

Auto:
__def_1(agatha).
hates (X1,X2) :- __def_2(X2), __def_1(X1).
__def_2(charles).
hates (X1,X2) :- __def_1(X2), __def_1(X1).
__def_4(butler).
killed (X1,X2) :- __def_1(X2), __def_2(X1).
__def_6(butler).
hates (X1,X2) :- __def_3(X2), __def_4(X1).
hates (X1,X2) :- __def_5(X2), __def_6(X1).
#q2 (X1) :- __def_1(X1).
#q2 (X1) :- __def_2(X1).
__def_5(agatha).
__def_5(charles).
not_richer (X1,X2) :- __def_1(X2), __def_2(X1).
#q3 (X1) :- __def_2(X1).
__def_3(charles).
hates (X1,X2) :- __def_1(X2), __def_2(X1).

selfq:
#false(charles_hates_noone_agatha_hates) :- #q2 (X1), #q1 (X1).
(* #q1 (X1) :- hates (charles,X1). : hates fully defined. *)
(* #q2 (X1) :- hates (agatha,X1). : hates fully defined. *)
(* #q3 (X1) :- not_richer (X1,agatha). : not_richer fully defined. *)
(* __def_5(X1) :- #q2 (X1). : #q2 fully defined. *)
(* __def_3(X1) :- #q3 (X1). : #q3 fully defined. *)

selxq:
__def_5(X1) :- __def_1(X1).
__def_5(X1) :- __def_2(X1).
__def_3(X1) :- __def_2(X1).

(* #q2 (X1) :- __def_1(agatha), __def_1(X1). *)
(* #q2 (X1) :- __def_1(agatha), __def_2(X1). *)
(* not_richer (X1,X2) :- killed (X1,X2). : killed fully defined *)
(* #q3 (X1) :- __def_1(agatha), __def_2(X1). *)
(* hates (X1,X2) :- killed (X1,X2). : killed fully defined *)



#q1 (X1) :- __def_2(charles), __def_1(X1).
















memtime ./h1mc -v3 -exact-sig -type coq nsl7.pl nsl7.p >nsl7.v



subgoal 2 is:
 auto___def_16 X1 -> auto___def_69 X1 -> False
tauto.
Error while reading /local/home/goubault/H1.1/eapaka.v :
File "/local/home/goubault/H1.1/eapaka.v", line 1907, characters 55-60
User error: Tauto failed

rem_60 < Show.
2 subgoals

  X1 : term
  ============================
   (auto___def_16 X1 -> auto___def_69 X1 -> False) ->
   auto_knows_old X1 -> auto___def_16 X1 -> False

subgoal 2 is:
 auto___def_16 X1 -> auto___def_69 X1 -> False

Remark rem_60 : forall X1:term, auto_knows_old X1 -> auto___def_16 X1 -> False. (* Subsumption by simpler clause. *)

MC_SUBSUMED



Ajouter MC_NORMALIZE
 and produce Coq proofs to show equivalence with normalized clause
Enlever MC_SUBSUMED_DONE, ou en temps cas le modifier.
Enlever MC_DONE
Verifier que les modes d'impression -type tree, etc., ont ete modifies.
Virer les epsdone de model.ml; !epsdoner fait ca mieux.
   ... adapter en consequence coqmodel.ml
Verifier toutes les fonctions qui font des cas sur MC_,
	pour voir si elles prevoient tous les cas.
Ne pas oublier de rajouter les epsilon clauses via epssub_add

MC_SUBSUMED (MC_TAUTO ...) -> MC_TAUTO.

Changement en Coq 8:
- pas de 'Require Refine.'
- (X,Y:A) toto devient forall X Y : A, toto
- en principe, au lieu d'ecrire (f x y) on peut \'ecrire f x y.
- apparemment toutes les tactiques s'\'ecrivent maintenant en
  minuscules.  Proof et Defined (et sans doute Qed) restent
  en majuscules.
- les inductifs avec param\`etres prennent des parenth\`eses
  et non des crochets:  'Inductive or_1 [H1:Prop]:Prop :='
  -> 'Inductive or_1 (H1:Prop):Prop :='.

Bugs:
- sometimes, terms disappear from the <clause> sections
  in h1 log files (e.g., we have knows(,) instead of knows(M,K).)
	Heisenbug.
- SortSimplifyBBug raised;
- in h1mc, fix epsilon_m__type_4_pknows_current 1
  where epsilon_m__type_4_pknows_current was already intro'd by intros.
	(Load yhl.)
- InconsistentSig raised, no indication: better send a
  proper error message.
- it is not checked that no two clauses have the same name in h1.

- wait_insert_2 should in general normalize the sets of free
  variables in the body when h is ground.
- remove all 'sub map's, and replace them by controlled
	calls to iter_sub_map (as a first patch).
- -sort-simplify produces [sort-simplify: in the trace;
	but should write which automaton clauses it used;
  Also, change proof extraction code (h1trace, maybe others).
- h1mc -v1 needham_preuve.model.pl needham_preuve.h1.log >a.tree
	says "Warning: clause ... remains unproved" a lot!

memtime h1 -v2 -progress needham_preuve.h1.p
*** Derived: clause338 ***
Exit [0]
24.73 user, 0.08 system, 26.33 elapsed -- Max VSize = 17296KB, Max RSS = 15244KB
gunzip needham_preuve.h1.log.gz
memtime h1logstrip -v2 needham_preuve.h1.log >np.log
memtime h1trace np.log >np.tree

memtime h1mc -v1 needham_preuve.h1.model.pl needham_preuve.h1.log >a.tree
Checking clause __def_3 (X1,X2,X3) :- __def_274 (X1,X5), __def_274 (X4,X5), __def_252 (X2,X3,X4)... OK.

memtime pldet -v1 needham_preuve.h1.model.pl >np.xml
memtime auto2pl -defs np.xml >np.pl
pl2tptp np.pl >np.p
memtime h1 -all -no-trim np.p
memtime h1mc -v1 np.model.pl needham_preuve.h1.log >a.tree

Checking clause __def_19 (X1,X2,X3,X4,X5) :- __def_275 (X2,X1,X3,X6,X4), __def_251 (X1,X5), __def_251 (X1,X6)...
__def_19: 606 clauses.
%[def] __def_275 (X2,X1,X3,X6,X4) :- values (field(field(field(X6,X2),X3),X1),X4).
__def_275: 145 clauses.
%[def] __def_251 (X1,X6) :- values (X6,address(X1)).
__def_251: 78 clauses.
145*78*78 = 882180

Mais pourtant:
grep "__def_19 (X1,X2,X3,X4,X5) :-" needham_preuve.h1.log | grep -v '%' | wc -l
16458

C'est grace au naive static soft typing!
/usr/local/misc/coq-8.0/doc/coq-docs-html/tutorial.html

Linux dell14.lsv.ens-cachan.fr 2.6.8-1.521 #1 Mon Aug 16 09:01:18 EDT 2004 i686 i686 i386 GNU/Linux
processor       : 0
vendor_id       : GenuineIntel
cpu family      : 6
model           : 13
model name      : Intel(R) Pentium(R) M processor 1.80GHz
stepping        : 6
cpu MHz         : 1794.614
cache size      : 64 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 mce cx8 mtrr pge mca cmov pat clflush dts acpi mmx fxsr s
se sse2 ss tm pbe tm2 est
bogomips        : 3555.32
memtime ./h1.opt -gctrace gc.out -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
298.24 user, 0.91 system, 312.35 elapsed -- Max VSize = 363460KB, Max RSS = 361316KB


Linux dell7001.lsv.ens-cachan.fr 2.6.10-1.12_FC2smp #1 SMP Wed Feb 2 01:45:04 EST 2005 i686 i686 i386 GNU/Linux
processor       : 0
vendor_id       : GenuineIntel
cpu family      : 15
model           : 3
model name      : Intel(R) Pentium(R) 4 CPU 3.40GHz
stepping        : 4
cpu MHz         : 3393.417
cache size      : 1024 KB
physical id     : 0
siblings        : 2
fdiv_bug        : no
hlt_bug         : no
f00f_bug        : no
coma_bug        : no
fpu             : yes
fpu_exception   : yes
cpuid level     : 5
wp              : yes
flags           : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat
 pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe pni monitor ds_cpl cid x
tpr
bogomips        : 6717.44
memtime ./h1.opt -gctrace gc.out -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
615.22 user, 1.84 system, 617.41 elapsed -- Max VSize = 334588KB, Max RSS = 332896KB

Linux dell7001.lsv.ens-cachan.fr 2.6.10-1.12_FC2smp #1 SMP Wed Feb 2 01:45:04 EST 2005 i686 i686 i386 GNU/Linux
processor       : 0
vendor_id       : GenuineIntel
cpu family      : 15
model           : 3
model name      : Intel(R) Pentium(R) 4 CPU 3.40GHz
stepping        : 4
cpu MHz         : 3393.417
cache size      : 1024 KB
physical id     : 0
siblings        : 2
fdiv_bug        : no
hlt_bug         : no
f00f_bug        : no
coma_bug        : no
fpu             : yes
fpu_exception   : yes
cpuid level     : 5
wp              : yes
flags           : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat
pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe pni monitor ds_cpl cid xtp
r
bogomips        : 6717.44
memtime ./h1.opt -gctrace gc.out -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
410.18 user, 0.69 system, 423.74 elapsed -- Max VSize = 334592KB, Max RSS = 332892KB


Linux noisette.lsv.ens-cachan.fr 2.6.10-1.9_FC2 #1 Thu Jan 13 17:54:57 EST 2005 i686 i686 i386 GNU/Linux
processor       : 0
vendor_id       : GenuineIntel
cpu family      : 15
model           : 2
model name      : Intel(R) Pentium(R) 4 CPU 2.40GHz
stepping        : 7
cpu MHz         : 2386.948
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 mtrr pge mca cmov pat
pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe cid
bogomips        : 4734.97
memtime ./h1.opt -gctrace gc.out -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
508.67 user, 1.62 system, 517.55 elapsed -- Max VSize = 334592KB, Max RSS = 332892KB

Linux fraise.lsv.ens-cachan.fr 2.6.10-1.9_FC2 #1 Thu Jan 13 17:54:57 EST 2005 i686 athlon i386 GNU/Linux
processor       : 0
vendor_id       : AuthenticAMD
cpu family      : 6
model           : 6
model name      : AMD Athlon(TM) XP 1800+
stepping        : 2
cpu MHz         : 1534.121
cache size      : 256 KB
fdiv_bug        : no
hlt_bug         : no
f00f_bug        : no
coma_bug        : no
fpu             : yes
fpu_exception   : yes
cpuid level     : 1
wp              : yes
flags           : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat
pse36 mmx fxsr sse pni syscall mp mmxext 3dnowext 3dnow
bogomips        : 3039.23
memtime ./h1.opt -gctrace gc.out -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
539.98 user, 1.17 system, 544.16 elapsed -- Max VSize = 334592KB, Max RSS = 332892KB


Avec #define COUNT
dans cons.c:

/* via a.out en -ggdb -pg -O2 */
p nKPairs
462725490
p nNewPairs
 79047000
p nKTuples
 53469531
p nNewTuples
 43553736

p nKPairs
406952580
p nNewPairs
 59565994
p nKTuples
 50826681
p nNewTuples
 41535397

p nKPairs
404053677
p nNewPairs
 61938454
p nKTuples
 49014074
p nNewTuples
 39365884

398061241
 61153911
 47297608
 38087414

/* en utilisant himmlrun: */
nKPairs =	476884810
nNewPairs =	72614003
nKTuples =	84163248
nNewTuples =	75268187

Bizarre, quand on met $P+ dans clause.ml:
memtime ./h1.opt -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
266.35 user, 0.55 system, 283.62 elapsed -- Max VSize = 342252KB, Max RSS = 338384KB
memtime h1 -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
320.31 user, 34.31 system, 2758.77 elapsed -- Max VSize = 327500KB, Max RSS = 316088KB


Mais en $P-:
memtime ./h1.opt -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
547.31 user, 0.92 system, 595.06 elapsed -- Max VSize = 415852KB, Max RSS = 411608KB
memtime h1 -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
347.13 user, 0.58 system, 372.86 elapsed -- Max VSize = 319720KB, Max RSS = 317764KB


In pl2gastex, instruct neato/dot that font size is larger
 than what it thinks.

Maybe set Nadjust=wh for regular nodes instead of just =w.

Determinization:
list_even_union_tree3plus2_d.pl does not mention q;
	-defs produces stupid clauses list_even(X) :- list_even(X).
	Possible solution: instead of printing {P,Q} as __inter_P_Q,
	add all states that are also satisfied at P&Q.
Do not use XML format any longer.
Output deterministic automata in Prolog format.
The former definitions are given by the names of the state
	(more or less).
Output negations as new option in pldet.
In determinize.ml, for each #P (invisible fun)
	do not create a value P, or containing P.
Check arities of predicates at parsing time.
Long node names: write a reference, with the real
	name in some kind of footnote.
	(Then reinstall =w instead of =wh.)

Add plpurge tool to doc.

Options names:
	Also make more uniform -v vs. -v <n>

ulimit -S -v 400000
himml -pair-hash-size 273253 -data-hash-size 218509 -array-hash-size 292069 -gctrace gc.out
memtime ./h1 -gctrace gc.out -p -progress -model Fabrice/alice_full1.p
memtime ./h1 -gctrace gc.out -progress -model +xm -v3 Fabrice/essai11.p
memtime ./h1 -v1 -log -model -progress Fabrice/essai3.p

memtime ./h1 -all -log -progress -model nspriv.p
memtime ./h1mc nspriv.model.pl nspriv.log >nspriv.tree.mc

memtime ./h1 -log -progress -model Fabrice/alice_full1.p

memtime ./h1 -all -p -progress -model -body-chop 1 Fabrice/alice_full1.p
cp Fabrice/alice_full1.model.pl a.pl
memtime ./h1 -p -progress -auto a.pl Fabrice/alice_full1.p

TEST=Fabrice/essai13
TEST=Needham_Schroeder.clauses
memtime ./h1 -v1 -log -model -progress $TEST.p
./h1trace $TEST.log | cpp -C -P -D "values(x,y)=x=y" -D "field(x,y)=x.y" -D "offset(x,y)=x[y]" -D "address(x)=&x" -D "cons(x,y)=x::y" -D "crypt(x,y)={x}_ y" >$TEST.tree


./h1getlog noproof $TEST.log | ./h1mc $TEST.model.pl - >$TEST.mc
./h1getlog noproof $TEST.log | ./h1mc -type coq $TEST.model.pl - >$TEST.v
  (* faster than ./h1mc $TEST.model.pl $TEST.log
	since h1mc will then just not have to parse the proof part. *)

./h1trace -type coq nspriv.log >nspriv.v
./h1mc -type coq nspriv.model.pl nspriv.log >nspriv.model.v
./h1mc nspriv.model.pl nspriv.log >nspriv.mc

./h1mc b.pl a.log

pldet list_even_inter_tree3plus2.model.pl | auto2pl -no-defs - | pl2gastex -v - >a.tex
-----------

Portable dellpe14 (monoproc Pentium M family 6 model 13, 1.80GHz, 64 KB cache)

===

- 07 jan 2005
memtime h1 -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
642.78 user, 0.80 system, 703.82 elapsed -- Max VSize = 280124KB, Max RSS = 276920KB
*** Derived: clause_conj ***
Exit [0]
660.66 user, 0.79 system, 703.57 elapsed -- Max VSize = 279248KB, Max RSS = 277024KB

- 09 jan 2005
memtime h1 -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
754.26 user, 0.50 system, 794.60 elapsed -- Max VSize = 310132KB, Max RSS = 307736KB

- 10 jan 2005
memtime h1 -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
403.27 user, 0.51 system, 425.84 elapsed -- Max VSize = 294888KB, Max RSS = 291644KB

- 27 jan 2005
memtime ./h1.opt -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
256.90 user, 0.65 system, 269.03 elapsed -- Max VSize = 363408KB, Max RSS = 359328KB
# after adding CallCC trampoline generation in himmlx
memtime ./h1.opt -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
270.11 user, 0.64 system, 283.59 elapsed -- Max VSize = 360148KB, Max RSS = 356744KB
# after correcting the #lab bug in HimML
memtime ./h1.opt -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
258.81 user, 0.54 system, 271.24 elapsed -- Max VSize = 328980KB, Max RSS = 324784KB

===

- 07 jan 2005
memtime h1 -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
663.50 user, 0.77 system, 700.71 elapsed -- Max VSize = 276988KB, Max RSS = 274784KB
memtime h1 -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
912.88 user, 0.75 system, 935.62 elapsed -- Max VSize = 276868KB, Max RSS = 274324KB

- 09 jan 2005
memtime h1 -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
753.53 user, 0.36 system, 816.70 elapsed -- Max VSize = 284556KB, Max RSS = 282612KB

- 10 jan 2005
memtime h1 -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
403.35 user, 0.41 system, 432.78 elapsed -- Max VSize = 304820KB, Max RSS = 303116KB
memtime h1 -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
352.30 user, 0.42 system, 358.37 elapsed -- Max VSize = 300032KB, Max RSS = 297828KB
memtime h1 -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
347.84 user, 0.37 system, 353.66 elapsed -- Max VSize = 288780KB, Max RSS = 286976KB
emtime h1 -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
377.44 user, 0.48 system, 384.82 elapsed -- Max VSize = 325064KB, Max RSS = 322500KB

- 27 jan 2005
memtime ./h1.opt -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
290.31 user, 0.57 system, 310.31 elapsed -- Max VSize = 354328KB, Max RSS = 349656KB
# after adding CallCC trampoline generation in himmlx
memtime ./h1.opt -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
301.20 user, 0.55 system, 321.76 elapsed -- Max VSize = 351672KB, Max RSS = 347012KB
# after correcting the #lab bug in HimML
memtime ./h1.opt -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
288.19 user, 0.80 system, 297.07 elapsed -- Max VSize = 379248KB, Max RSS = 374348KB

===

- 07 jan 2005
memtime h1 -all -log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
2167.57 user, 8.85 system, 2505.85 elapsed -- Max VSize = 278016KB, Max RSS = 274760KB
	(complètement anormal: hier j'avais 1320 user...)
memtime h1 -all -log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
1545.07 user, 7.23 system, 1755.39 elapsed -- Max VSize = 259328KB, Max RSS = 256484KB

- 09 jan 2005
memtime h1 -all -log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
1317.41 user, 6.77 system, 1486.83 elapsed -- Max VSize = 315504KB, Max RSS = 312960KB

- 10 jan 2005
memtime h1 -all -log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
1087.31 user, 6.60 system, 1250.53 elapsed -- Max VSize = 311964KB, Max RSS = 309932KB

- 27 jan 2005
memtime ./h1.opt -all -log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
682.01 user, 5.97 system, 845.34 elapsed -- Max VSize = 318764KB, Max RSS = 315368KB
# after adding CallCC trampoline generation in himmlx
memtime ./h1.opt -all -log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
741.86 user, 6.36 system, 881.35 elapsed -- Max VSize = 342944KB, Max RSS = 338268KB
# after correcting the #lab bug in HimML
memtime ./h1.opt -all -log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
708.92 user, 6.14 system, 846.24 elapsed -- Max VSize = 341992KB, Max RSS = 338224KB

-----------

dellpe02 (4-proc Xeon family 15 model 2, 3.0 GHz, 512 KB cache)

===

- 07 jan 2005
1009 : memtime h1 -p +trace +all Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
1488.31 user, 0.84 system, 1490.09 elapsed -- Max VSize = 279796KB, Max RSS = 278452KB
memtime h1 -all -no-log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
3908.45 user, 0.76 system, 3910.51 elapsed -- Max VSize = 257268KB, Max RSS = 255896KB

===

- 07 jan 2005
memtime h1 -p -trace +all Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
1834.43 user, 0.68 system, 1835.46 elapsed -- Max VSize = 271488KB, Max RSS = 270068KB
memtime h1 -all -no-log -no-progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
1752.29 user, 5.60 system, 1760.86 elapsed -- Max VSize = 265324KB, Max RSS = 263952KB

===

- 07 jan 2005
memtime h1 -all -log -progress Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
2604.38 user, 32.86 system, 2641.10 elapsed -- Max VSize = 338444KB, Max RSS = 337116KB
memtime h1 -all -log -progress Fabrice/alice_full1.p
        *** Derived: clause_conj ***
Exit [0]
2582.81 user, 34.49 system, 2621.12 elapsed -- Max VSize = 338444KB, Max RSS = 337116KB

--------------
--------------

himmlx -E h1 >toto.c
gcc -pg -ggdb -O3 toto.c -L/usr/local/lib/himml -lhimml -lm
valgrind --tool=cachegrind a.out -no-log -progress nspriv.p

==16486== Cachegrind, an I1/D1/L2 cache profiler for x86-linux.
==16486== Copyright (C) 2002-2004, and GNU GPL'd, by Nicholas Nethercote et al.
==16486== Using valgrind-2.2.0, a program supervision framework for x86-linux.
==16486== Copyright (C) 2000-2004, and GNU GPL'd, by Julian Seward et al.
--16486-- warning: Unknown Intel cache config value (0xF0), ignoring
--16486-- warning: Unknown Intel cache config value (0x7D), ignoring
--16486-- warning: L2 cache not installed, ignore L2 results.
==16486== For more details, rerun with: -v
==16486==
*** Derived: intruder_knows_session_key_as_seen_by_B ***
==16486==
==16486== I   refs:      147,567,453
==16486== I1  misses:        325,747
==16486== L2i misses:         15,107
==16486== I1  miss rate:        0.22%
==16486== L2i miss rate:         0.1%
==16486==
==16486== D   refs:       85,077,293  (52,915,074 rd + 32,162,219 wr)
==16486== D1  misses:      2,930,268  ( 2,579,142 rd +    351,126 wr)
==16486== L2d misses:        198,890  (     5,321 rd +    193,569 wr)
==16486== D1  miss rate:         3.4% (       4.8%   +        1.0%  )
==16486== L2d miss rate:         0.2% (       0.0%   +        0.6%  )
==16486==
==16486== L2 refs:         3,256,015  ( 2,904,889 rd +    351,126 wr)
==16486== L2 misses:         213,997  (    20,428 rd +    193,569 wr)
==16486== L2 miss rate:          0.0% (       0.0%   +        0.6%  )

cg_annotate --16486 toto.c cons.c gc.c >cg.16486

--------------
==16929== Cachegrind, an I1/D1/L2 cache profiler for x86-linux.
==16929== Copyright (C) 2002-2004, and GNU GPL'd, by Nicholas Nethercote et al.
==16929== Using valgrind-2.2.0, a program supervision framework for x86-linux.
==16929== Copyright (C) 2000-2004, and GNU GPL'd, by Julian Seward et al.
--16929-- warning: Unknown Intel cache config value (0xF0), ignoring
--16929-- warning: Unknown Intel cache config value (0x7D), ignoring
--16929-- warning: L2 cache not installed, ignore L2 results.
==16929== For more details, rerun with: -v
==16929==
*** Derived: intruder_knows_session_key_as_seen_by_B ***
==16929==
==16929== I   refs:      173,453,135
==16929== I1  misses:        296,739
==16929== L2i misses:         14,961
==16929== I1  miss rate:        0.17%
==16929== L2i miss rate:         0.0%
==16929==
==16929== D   refs:       96,810,633  (61,751,190 rd + 35,059,443 wr)
==16929== D1  misses:      2,974,492  ( 2,594,423 rd +    380,069 wr)
==16929== L2d misses:        232,831  (     5,322 rd +    227,509 wr)
==16929== D1  miss rate:         3.0% (       4.2%   +        1.0%  )
==16929== L2d miss rate:         0.2% (       0.0%   +        0.6%  )
==16929==
==16929== L2 refs:         3,271,231  ( 2,891,162 rd +    380,069 wr)
==16929== L2 misses:         247,792  (    20,283 rd +    227,509 wr)
==16929== L2 miss rate:          0.0% (       0.0%   +        0.6%  )

cg_annotate --16929 toto.c cons.c gc.c >cg.16929

--------------

memtime ./h1 -log -progress Fabrice/alice_full1.p
** Derived: clause_conj ***
Exit [0]
1639.85 user, 10.37 system, 1854.45 elapsed -- Max VSize = 283640KB, Max RSS = 282248KB
Derived clauses: 872193 (50951 splitting defs, 672 ne facts)
Dealt with, not subsumed: 267810
Subsumed clauses [forward] : 604371 (of which 573229 automata clauses)
Subsumed clauses [backward]: 11546 (of which 10964 automata clauses)
Frozen clauses: 1458770, awaken: 14504.
Fully defined predicate symbols: 507
  Backward subsumed clauses because of fully defined symbols: 0
  Subsumed parent clauses because of fully defined symbols: 105934
Abbreviations: 1273
Ground facts: 0
Pruned clauses: 0
Automata clauses: 85117


-----------
memtime ./h1 -log -progress -all Fabrice/alice_full1.p
*** Derived: clause_conj ***
Exit [0]
2394.72 user, 4.82 system, 2745.12 elapsed -- Max VSize = 255348KB, Max RSS = 253636KB

Derived clauses: 874432 (51017 splitting defs, 671 ne facts)
Dealt with, not subsumed: 271956
Subsumed clauses [forward] : 602476 (of which 570719 automata clauses)
Subsumed clauses [backward]: 14040 (of which 13420 automata clauses)
Frozen clauses: 1458713, awaken: 16826.
Fully defined predicate symbols: 507
  Backward subsumed clauses because of fully defined symbols: 0
  Subsumed parent clauses because of fully defined symbols: 107009
Abbreviations: 1284
Ground facts: 0
Pruned clauses: 0
Automata clauses: 87455

-----------


memtime ./h1logstrip -v2 Fabrice/alice_full1.log.gz >gag
Scanning ...  done: 9493508 deduction steps, 6595998 clauses.
Marking ...  done: 1722 live clauses.
Outputting ...  done.
Exit [0]
558.04 user, 1.64 system, 603.86 elapsed -- Max VSize = 377908KB, Max RSS = 377004KB

gprof   -l h1logstrip >logstrip.out

------------

valgrind --tool=cachegrind h1 -log -progress nspriv.p
==5183== Cachegrind, an I1/D1/L2 cache profiler for x86-linux.
==5183== Copyright (C) 2002-2004, and GNU GPL'd, by Nicholas Nethercote et al.
==5183== Using valgrind-2.2.0, a program supervision framework for x86-linux.
==5183== Copyright (C) 2000-2004, and GNU GPL'd, by Julian Seward et al.
--5183-- warning: Unknown Intel cache config value (0xF0), ignoring
--5183-- warning: Unknown Intel cache config value (0x7D), ignoring
--5183-- warning: L2 cache not installed, ignore L2 results.
==5183== For more details, rerun with: -v
==5183==
*** Derived: intruder_knows_session_key_as_seen_by_B ***
==5183==
==5183== I   refs:      198,854,174
==5183== I1  misses:         59,385
==5183== L2i misses:          2,756
==5183== I1  miss rate:         0.2%
==5183== L2i miss rate:         0.0%
==5183==
==5183== D   refs:      115,125,422  (78,538,055 rd + 36,587,367 wr)
==5183== D1  misses:      2,834,446  ( 2,558,936 rd +    275,510 wr)
==5183== L2d misses:         88,822  (       543 rd +     88,279 wr)
==5183== D1  miss rate:         2.4% (       3.2%   +        0.7%  )
==5183== L2d miss rate:         0.0% (       0.0%   +        0.2%  )
==5183==
==5183== L2 refs:         2,893,831  ( 2,618,321 rd +    275,510 wr)
==5183== L2 misses:          91,578  (     3,299 rd +     88,279 wr)
==5183== L2 miss rate:          0.0% (       0.0%   +        0.2%  )


cg_annotate --5183 cons.c gc.c >cg.5183

*

valgrind --tool=cachegrind h1 -all -no-log -no-progress Fabrice/alice_full1.p
==5536== Cachegrind, an I1/D1/L2 cache profiler for x86-linux.
==5536== Copyright (C) 2002-2004, and GNU GPL'd, by Nicholas Nethercote et al.
==5536== Using valgrind-2.2.0, a program supervision framework for x86-linux.
==5536== Copyright (C) 2000-2004, and GNU GPL'd, by Julian Seward et al.
--5536-- warning: Unknown Intel cache config value (0xF0), ignoring
--5536-- warning: Unknown Intel cache config value (0x7D), ignoring
--5536-- warning: L2 cache not installed, ignore L2 results.
==5536== For more details, rerun with: -v
==5536==
*** Derived: clause_conj ***
==5536==
==5536== I   refs:      402,128,873,186
==5536== I1  misses:            650,269
==5536== L2i misses:              7,122
==5536== I1  miss rate:             0.0%
==5536== L2i miss rate:             0.0%
==5536==
==5536== D   refs:      257,212,558,192  (186,705,680,587 rd + 70,506,877,605 wr)
==5536== D1  misses:      6,323,953,684  (  5,958,621,698 rd +    365,331,986 wr)
==5536== L2d misses:         26,996,717  (     16,516,344 rd +     10,480,373 wr)
==5536== D1  miss rate:             2.4% (            3.1%   +            0.5%  )
==5536== L2d miss rate:             0.0% (            0.0%   +            0.0%  )
==5536==
==5536== L2 refs:         6,324,603,953  (  5,959,271,967 rd +    365,331,986 wr)
==5536== L2 misses:          27,003,839  (     16,523,466 rd +     10,480,373 wr)
==5536== L2 miss rate:              0.0% (            0.0%   +            0.0%  )



[Warning: the following takes 17h 45 min!]

valgrind --tool=cachegrind h1 -log -progress Fabrice/alice_full1.p
==32571== Cachegrind, an I1/D1/L2 cache profiler for x86-linux.
==32571== Copyright (C) 2002-2004, and GNU GPL'd, by Nicholas Nethercote et al.
==32571== Using valgrind-2.2.0, a program supervision framework for x86-linux.
==32571== Copyright (C) 2000-2004, and GNU GPL'd, by Julian Seward et al.
--32571-- warning: Unknown Intel cache config value (0xF0), ignoring
--32571-- warning: Unknown Intel cache config value (0x7D), ignoring
--32571-- warning: L2 cache not installed, ignore L2 results.
==32571== For more details, rerun with: -v
==32571==
*** Derived: clause_conj ***
==32571==
==32571== I   refs:      1,245,738,001,475
==32571== I1  misses:          872,207,899
==32571== L2i misses:                7,811
==32571== I1  miss rate:               0.7%
==32571== L2i miss rate:               0.0%
==32571==
==32571== D   refs:        785,580,177,150  (546,727,906,670 rd + 238,852,270,480 wr)
==32571== D1  misses:       12,611,438,691  ( 11,520,690,724 rd +   1,090,747,967 wr)
==32571== L2d misses:           13,586,450  (      6,441,008 rd +       7,145,442 wr)
==32571== D1  miss rate:               1.6% (            2.1%   +             0.4%  )
==32571== L2d miss rate:               0.0% (            0.0%   +             0.0%  )
==32571==
==32571== L2 refs:          13,483,646,590  ( 12,392,898,623 rd +   1,090,747,967 wr)
==32571== L2 misses:            13,594,261  (      6,448,819 rd +       7,145,442 wr)
==32571== L2 miss rate:                0.0% (            0.0%   +             0.0%  )

ln -s ~/HimML/Alpha17/cons.c .
ln -s ~/HimML/Alpha17/gc.c .
ln -s ~/HimML/Alpha17/exec.c .
ln -s ~/HimML/Alpha17/map.c .
cg_annotate --32571 cons.c gc.c exec.c map.c >cg.32571

*

determinize.ml ignores predicates in univ!
and auto2pl should also consider them (in particular for negation).

*

A better trick to approximate equality (and in fact not
just equational theories).

First, clauses  t=u <= B  are replaced by X=Y <= B, X=t, Y=u
for two new variables X, Y.

Then, equalities in bodies are just ignored (they are just constraints,
that keep on accumulating).  OK, that means that they are never selected.
And we consider that equalities are less than any other P(t) (not q).

OK, maybe that needs a fresh completeness proof.  The idea is
never to resolve on an equality.  Eventually, we get a bunch of
clauses that contain only equalities, S_=, amongst the saturated
clause set S_*.
	S_* is satisfiable if and only if S_= is.
We then check whether S_= is satisfiable by using a
Paradox-like technique.

*

Equality is typically a STTG thing.

eq (f (X1, ..., Xn), f (Y1, ..., Yn)) :- eq (X1, Y1), ..., eq (Xn, Yn).
noneq (f (X1, ..., Xn), g (Y1, ..., Ym)).
noneq (f (X1, ..., Xn), f (Y1, ..., Ym)) :- noneq (Xi, Yi).
	(for all i=1..n)

Specialize h1 to these two relations?
	Nothing should be selected in either of the clauses above.
	This produces the following refinement in resolution rules:
A :- body, eq (f (t1, ..., tn), f (u1, ..., un))
------------------------------------------
A :- body, eq (t1,u1), ..., eq (tn,un)

A :- body, eq (f (t1, ..., tn), Y)
------------------------------------------------------------------------
A [Y:=f(Y1,...,Yn)] :- body [Y:=f(Y1,...,Yn)], eq(t1,Y1), ..., eq(tn,Yn)
	provided eq (f(t1,...,tn), Y) is selected

We can also erase all clauses with some eq (f (...), g (...)) in
	the body (eq is fully defined).
etc.

Simpler:
limit STTG clauses to be automata-like clauses.
Encode P (f (X1, ..., Xn), g (Y1, ..., Yn)) :- Q1 (X1, Y1), ..., Qn (Xn, Yn)
as n automata clauses:
	Pfg1 (X1, Y1) :- Q1 (X1, Y1)
	...
	Pfgn (Xn, Yn) :- Qn (Xn, Yn)

In non-automata clauses, only allow P in the body.
	Then do as though P was defined by a collection of clauses
	P (f (X1, ..., Xn), g (Y1, ..., Yn)) :- Pfg1 (X1, Y1), ..., Pfgn (Xn, Yn)

Problem: this is undecidable, by reduction from Post's correspondence problem.
Recognize pairs of equal non-empty terms (at P_1):
	P_0 (epsilon, epsilon).
	P_1 (a_j X, a_j Y) :- P_0 (X, Y).
	P_1 (a_j X, a_j Y) :- P_1 (X, Y).

Then destruct terms:
	P (c (X, Y)) :- P_1 (X, Y). // recognize pairs of equal non-empty words.
	P (c (X, Y)) :- P (c (u_i (X), v_i (X))). // destruct one Post pair.
	false :- P (c (epsilon, epsilon)). // until we reach two empty words.

It follows that the theory of homomorphism with H1 is also undecidable
	(e.g., add equations of the form f (c (X,Y)) = c (g (X), h (Y)):
	P_0 (c (epsilon, epsilon)).	[codable in H1]
	P_1 (f_j Z) :- P_0 Z.
	P_1 (f_j Z) :- P_1 Z.	[with equation f_j (c (X, Y)) = c (a_j (X), a_j (Y))]
	+ clauses to destruct terms as above.)

*

encoding AC.  Idea: encode a sum as any binary +-tree with the same
leaves (and the same multiplicity).  Sums in the body are then left
as they are.  For sums in the head, transform
	P (x+y) <- body
into P (plus (plus (x1,y1), plus (x2,y2))) <- body [x:=plus (x1,x2), y:=plus (y1, y2)]
	and variants.
Problem: this is no longer in H1.
In fact, the class is undecidable (Kumar's thesis).
No longer so if x and y occur at most once in body (reduces to STTGs?)

*

encoding AC (again).
Idea: add integer variables (in Z), and simple arithmetic constraints to
clauses (i.e., x<=y+c, or x<=c, or x>=c).  Unification of
an arithmetic variable with a non-arithmetic term f (...) fails.
Unification of arithmetic variables adds a constraint, and projects
to the subspace of remaining free variables.

Problem: we cannot add two variables (x=y+z).
However this is enough to encode GDH.2 (check that Ni occurs once,
then increment the number of occurrences of Nj.
	ie, P([n1, ..., nk]) <- P' ([n'1, ..., n'k]) |
		n1=n'1, ..., ni=n'i=1, ..., nj=n'j+1, ..., nk=n'k.
	where ni is #occurrences of Ni.
including the abelian group law case.

*

constraints:

(A1) C (x,y,...) never holds when x or y or ... is instantiated by f(...)
	where f is a free function symbol; i.e., constraints are applied
	to values outside the range of the free function symbols, e.g.,
	to natural numbers where no f yields back a natural number.

Clauses are head :- body | C(x,y,...)

Resolution is applied as though on head :- body, i.e., constraints are
not resolved upon.

Simple inequality constraints:
	x <= y+3 (edge x --3--> y)

head :- body, Leq (x, s^3 y)

Using (2) we can derive any head :- body, Leq (s^n x, s^{n+3} y)
	(except this is not by ord.res.sel.)

Given head :- body, Leq (x, s^3 y), Leq (y, s^2 z)
we can derive ... :- ..., Leq (x, s^3 y), Leq (s^3 y, s^5 z) using (2)

[?]

... :- ..., Leq (s^n x, s^m x) (n<m)
	-> remove.

(1) Leq (s x, s y) <- Leq (x, y)	[pas H1]
(2) Leq (x, y) <- Leq (s x, s y)	[OK]
(3) Leq (x, y) <- Leq (x, z), Leq (z, y)	[OK]
(4) Leq (x, x)			[pas H1]

*

Constraints:

The idea was to have function symbols with some arguments that
are always variables, constrained by some constraints.  Typically,
these denote integers, subject to some Presburger constraints.
Then we need constraints in automata clauses, but not in epsilon
clauses for example (no function symbol).
	But this is undecidable in most cases.  For example, we
can encode two-register machines this way:
. p -- R1++ --> q:	q(a (M', N')) :- p(a (M, N)) | M'=M+1, N'=N.
. p -- R1-- --> q:	q(a (M', N')) :- p(a (M, N)) | M'=M-1, N'=N.
. p -- R1==0 -> q:	q(a (M, N)) :- p(a (M, N)) | M=0.
	This only uses a (very specific) fragment of even
constraints x<=y+k.
	No wonder this cannot be encoded in H1.

*

Abelian group law.

Make clauses use only free function symbols, or only +, -, and 0.
(Only one group law; others can be handled using parenthesizing
operators, as in Kumar's dmtcs paper.)
Call the latter clauses +-clauses.

Because of inverses, we can always rewrite +-clauses as:
P (sum_{i=1}^n a_i X_i) :- B_1(X_1), ..., B_n(X_n)
	where B_1, ..., B_n are blocks (conjunctions of
predicates); we may also have %ne symbols.
	We take as selection function the usual one,
extended so that:
	- possible %ne symbols are selected, as usual;
	- otherwise, some predicate in the body is selected;
This of course generates possibly infinitely many clauses,
but:
	- we replace this by rewrite rules of the
	form sum_q a_q -> a_P
	where a_q counts the number of terms recognized
	at q in the sum on the left of :-.

	- we approximate this by taking the coefficients a_i
	modulo some fixed integer m (or some more complicated
	structure?)

	- we then compute the transitive closure of these
	rewrite rules together with epsilon-rules.

*

To model multisets of a fixed number k of objects,
use a synchronized representation of k-tuples of natural numbers.
The alphabet is that of k-tuples of symbols in {s, #}.

Note: never any s atop a #.

On 2-tuples:

Tuple (00).
Tuple (s# (00)).
Tuple (#s (00)).
Tuple (ss (00)).
Tuple (## (X)) :- Tuple (X).
Tuple (#s (#s (X)) :- Tuple (#s (X)).
Tuple (#s (ss (X)) :- Tuple (ss (X)).
Tuple (s# (s# (X)) :- Tuple (s# (X)).
Tuple (s# (ss (X)) :- Tuple (ss (X)).
Tuple (ss (ss (X)) :- Tuple (ss (X)).

OK, represent whole relations by the standard synchronization trick:
E.g.,
	(* Succ2 (n1-m1-n2-m2) iff n1=m1 and n2=m2+1. *)

For every a in {#, s}:
Succ2(aas# (0000)).
Succ2(aas# (aass (X))).
Succ2(aa## (X)) :- Succ2 (X).

Pred2(aa#s (0000)).
Pred2(aa#s (ssaa (X))).
Pred2(aa## (X)) :- Pred2 (X).

Projection (e.g, get a relation on n2-m2 from relation on n1-m1-n2-m2):
Proj2 (ab (X), cdab (Y)) :- Proj2 (X, Y)	for every a, b, c, d.
Proj2 (00, 0000).
	-> not in H1.

I now want to encode +-terms as sums of a fixed number of constants
	c1 ... ck.  Let us say k=2
Such sums are encoded as f (g (... (00))), where f, g, ... are taken
among ss, s#, #s, ##.

To encode P (x+c2) :- Q (x)
we write:
Q (00) :- Q (0).
Q (#s (00)) :- Q (c2).
Q (s# (00)) :- Q (c1).  (this assumes every term is either c1 or c2 or 0. *)
Q (## (X)) :- Q (X).

P (bs (00)) :- Q (b# (00)).
P (bs (as (X))) :- Q (b# (as (X))).	(for every a, b)
P (#s (as (X))) :- Q (as (X)).	(useless since Q (as (X)) implies Q (## (as (X)))
				and we apply the previous rule.)
	(no clause to go below ## symbols and leave them in place.)
P (## (X)) :- P (X).

P (0) :- P (00).
P (c1) :- P (s# (00)).
P (c2) :- P (#s (00)).
P (X) :- P (## (X)).

*

Equational theories.  Encode y=f(x) for f equational
as P_f (y,x).

Example: let crypt be some basic encryption primitive,
	crypt_ecb be ECB encryption based on crypt.
	That is, crypt_ecb ([M, N, ...], K) = [crypt (M, K), crypt (N, K), ...]

Then we write:
	P_crypt_ecb (nil, nil).
	P_crypt_ecb (T::Z, X::Y, K) :- P_crypt (T, X, K), P_crypt_ecb (Z, Y, K).
	But this is not in H1.

	And P_crypt (crypt (X, K), X, K).
	Again not in H1.

AC:
	P_+ (T, X, V) :- P_+ (Z, X, Y), P_+ (T, Z, U), P_+ (V, Y, U).
	(* if X+Y=Z, T=Z+U, i.e., T=(X+Y)+U,
	   and if Y+U=V, then T=X+V. *)
	P_+ (Z, Y, X) :- P_+ (Z, X, Y).

Problem: if we just write this, then P_+ is the empty predicate.

*

autodot devrait prendre en entrée un fichier parsé par plauto.

In waitq, add reference to parents; if one of the parents got
	backward subsumed, then ignore clause.
 
In selfq, instead of storing maps from every (al, acc) to clauses,
	(with missing atom P (f $ ...))
	only store the case where acc=nil.
	Use another map from (P, f) to the corresponding
	possible als (with acc=nil).

Ameliorer un peu le splitting: si on doit prouver h :- body, body'
	avec h clos et fv(body) & fv(body'), splitter.

clause5.ml: ce qui fonctionne
  clause6.ml: on remplace les pathset par des ensembles de simple_term,
	mais leur taille est limitee par un pathset global.
  clause7.ml: comme clause5.ml, mais taille des pathsets limitee par
	un pathset global.
  clause8.ml: plein d'experiences en cours avortees, celle des
	simple_skeleta laissee, mais inutile.
  clause9.ml: on ne genere plus les split_def, mais une fois
	l'ensemble courant sature, on rajoute l'une des split_def
	et on boucle.
  clause10.ml: met a part les predicats fully defined; il y a
	probablement un bug, qui empeche de trouver une attaque
	dans Fabrice/needham_preuve.p.
  clause12.ml: supprimé le code en commentaire qui implémentait
	le terminator (qui s'est révélé largement inutile).

Peut-on calculer en plus des pathsets une forme reduite de relation
	de coherence entre chemins?  (entre suites de deux symboles
	typiquement)

L'option -auto ne semble pas fonctionner pour determiniser un
	automate.
	La changer pour guider plutot le processus de resolution.

Peut-on rendre plus efficace la subsomption arriere par une
	clause de la forme __type_values values (X1, X2)?
	(Ce n'est pas une clause univ, mais pas loin.)

Dans les automates produits, supprimer toutes les clauses
	P (f (...)) :- ...
si f est un symbole __aux_*: elles ne servent a priori a rien
pour verifier l'ensemble de clauses de depart?

Des que A (clause unitaire clause) est produite, la resoudre avec
	tout ce qu'il faut dans selfq, selxq, selqq et effacer
	les entrees correspondantes dans ces dernieres.

Utiliser les pathsets pour preinstancier les clauses epsilon?

------------------------------------------
Doc:

It may be that in Coq-checking nspriv.model.v, Coq
complains about:

Warning: translate_auto___false__intruder_knows_session_key_as_seen_by_alice_from___false__intruder_knows_session_key_as_seen_by_alice is non-recursively defined
Warning: translate_auto___false__intruder_knows_session_key_generated_by_server_from___false__intruder_knows_session_key_generated_by_server is non-recursively defined

	This is because these are defined without
recursion.  This is normal.

------------------------------------------

SMASH_TWO_NEG_LIT:
------------------

Fabrice/alice_full1.p:
*** Derived: clause_conj ***
Exit [1]
3.35 user, 0.14 system, 3.73 elapsed -- Max VSize = 40352KB, Max RSS = 39104KB
Derived clauses:  4148 (493 splitting defs,  148 ne facts)
Dealt with:  3075 (0 splitting defs)
Subsumed clauses [forward]:  880
Automata clauses:  1336

en -all:
Exit [0]
571.17 user, 7.84 system, 658.65 elapsed -- Max VSize = 190412KB, Max RSS = 189164KB
Derived clauses:  139597 (93217 splitting defs,  46510 ne facts)
Dealt with:  106976 (0 splitting defs)
Subsumed clauses [forward]:  32621
Automata clauses:  3518

Fabrice/needham_preuve.p:
*** Derived: clause_conj ***
Exit [1]
8.26 user, 0.73 system, 13.09 elapsed -- Max VSize = 48768KB, Max RSS = 47520KB
Derived clauses:  40386 (726 splitting defs,  340 ne facts)
Dealt with:  5316 (0 splitting defs)
Subsumed clauses [forward]:  19307
Automata clauses:  1430

Fabrice/needham_saturation.p:
*** Derived: clause_conj ***
Exit [1]
7.23 user, 0.79 system, 12.27 elapsed -- Max VSize = 48528KB, Max RSS = 47280KB
Derived clauses:  36519 (608 splitting defs,  303 ne facts)
Dealt with:  8691 (0 splitting defs)
Subsumed clauses [forward]:  13273
Automata clauses:  1020

SMASH_NONE:
-----------

Fabrice/needham_preuve.p:
*** Derived: clause_conj ***
Exit [1]
287.97 user, 21.60 system, 567.81 elapsed -- Max VSize = 427704KB, Max RSS = 403436KB
Derived clauses:  371612 (783 splitting defs,  359 ne facts)
Dealt with:  360810 (0 splitting defs)
Subsumed clauses [forward]:  10595
Useless function symbols:  0
Automata clauses:  2133

Fabrice/needham_saturation.p:
*** Derived: clause_conj ***
Exit [1]
293.85 user, 21.14 system, 502.86 elapsed -- Max VSize = 440632KB, Max RSS = 407060KB
Derived clauses:  382969 (795 splitting defs,  373 ne facts)
Dealt with:  369009 (0 splitting defs)
Subsumed clauses [forward]:  13941
Automata clauses:  2146

-------------------------------------------
"alice_gets_server_message_and_forwards_submessage_to_bob"
 knows Msg :- knows crypt(cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(Kab,cons(Msg,nil)))),key(sym,cons(alice,cons(server,nil)))).

"alice_gets_server_message_and_stores_current_session_key"
 alice_key key(Mode,current_session(X,Y,N)) :- knows crypt(cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(Mode,current_session(X,Y,N)),cons(Msg,nil)))),key(sym,cons(alice,cons(server,nil)))). </clause>

approx:
alice_key key(X1,X2) :- __aux_47 X2, __aux_46 X1.

definitions:
__aux_47 current_session(X1,X2,X3) :- __aux_45 (X2,X3,X1,X4,X5).
__aux_46 X1 :- __aux_45 (X2,X3,X4,X5,X1).
__aux_45 (X1,X2,X3,X4,X5) :- knows crypt(cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X5,current_session(X3,X1,X2)),cons(X4,nil)))),key(sym,cons(alice,cons(server,nil)))).

%abbrv-11 (X1,X2,X3,X4,X5) :- knows crypt(cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))),key(sym,cons(alice,cons(server,nil)))). [abbrv-def]

__aux_45 (X1,X2,X3,X4,X5) :- %abbrv-11 (X2,X5,X1,X3,X4). [abbrv-use:
  __aux_45 (X1,X2,X3,X4,X5) :- knows crypt(cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X2,current_session(X5,X1,X3)),cons(X4,nil)))),key(sym,cons(alice,cons(server,nil)))).
  ]

-----

%abbrv-11 (X1,X2,X3,X4,X5) :- __aux_17 key(sym,cons(alice,cons(server,nil))), __aux_16 cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))). [auto-resolve:
  %abbrv-11 (X1,X2,X3,X4,X5) :- knows crypt(cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))),key(sym,cons(alice,cons(server,nil)))).
  knows crypt(X1,X2) :- __aux_17 X2, __aux_16 X1.{X1=cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))),X2=key(sym,cons(alice,cons(server,nil)))}
  ]

-----

%abbrv-11 (X1,X2,X3,X4,X5) :- %abbrv-31 , %abbrv-49 (X1,X2,X3,X4,X5). [abbrv-use:
  %abbrv-11 (X1,X2,X3,X4,X5) :- __aux_17 key(sym,cons(alice,cons(server,nil))), __aux_16 cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))).
  ]

%abbrv-11 (X1,X2,X3,X4,X5) :- knows key(sym,cons(alice,cons(server,nil))), knows cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))). [auto-resolve:
  %abbrv-11 (X1,X2,X3,X4,X5) :- knows crypt(cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))),key(sym,cons(alice,cons(server,nil)))).
  knows crypt(X1,X2) :- knows X2, knows X1.{X1=cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))),X2=key(sym,cons(alice,cons(server,nil)))}
  ]

-----

%abbrv-11 (X1,X2,X3,X4,X5) :- %abbrv-33 , %abbrv-50 (X1,X2,X3,X4,X5). [abbrv-use:
  %abbrv-11 (X1,X2,X3,X4,X5) :- knows key(sym,cons(alice,cons(server,nil))), knows cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))).
  ]

%abbrv-11 (X1,X2,X3,X4,X5) :- __aux_17 key(sym,cons(alice,cons(server,nil))), __aux_36 cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))). [auto-resolve:
  %abbrv-11 (X1,X2,X3,X4,X5) :- knows crypt(cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))),key(sym,cons(alice,cons(server,nil)))).
  knows crypt(X1,X2) :- __aux_17 X2, __aux_36 X1.{X1=cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))),X2=key(sym,cons(alice,cons(server,nil)))}
  ]

-----

%abbrv-11 (X1,X2,X3,X4,X5) :- %abbrv-31 , %abbrv-51 (X1,X2,X3,X4,X5). [abbrv-use:
  %abbrv-11 (X1,X2,X3,X4,X5) :- __aux_17 key(sym,cons(alice,cons(server,nil))), __aux_36 cons(noncea(cons(alice,cons(bob,nil))),cons(bob,cons(key(X1,current_session(X2,X3,X4)),cons(X5,nil)))).
  ]

+++++

%abbrv-31  :- __aux_17 key(sym,cons(alice,cons(server,nil))). [abbrv-def]

%abbrv-31  :- __aux_24 sym, __aux_35 cons(alice,cons(server,nil)). [auto-resolve:
  %abbrv-31  :- __aux_17 key(sym,cons(alice,cons(server,nil))).
  __aux_17 key(X1,X2) :- __aux_35 X2, __aux_24 X1.{X1=sym,X2=cons(alice,cons(server,nil))}
  ]

-----

%abbrv-31  :- __aux_24 sym, %abbrv-36 . [abbrv-use:
  %abbrv-31  :- __aux_24 sym, __aux_35 cons(alice,cons(server,nil)).
  ]
%abbrv-31  :- %abbrv-36 . [auto-resolve:
  %abbrv-31  :- __aux_24 sym, %abbrv-36 .
  __aux_24 sym.
  ]

-----

%abbrv-31 . [auto-resolve:
  %abbrv-31  :- %abbrv-36 .
  %abbrv-36 .
  ]

*** Probleme semble etre que l'on dérive %abbrv-31,
	mais ca n'est jamais résolu avec %abbrv-11 (X1,X2,X3,X4,X5) :- %abbrv-31 , %abbrv-51 (X1,X2,X3,X4,X5).
	Note: le fait %abbrv-31 est produit avant la clause %abbrv-11 (X1,X2,X3,X4,X5) :- %abbrv-31 , %abbrv-51 (X1,X2,X3,X4,X5).
	Note: a ce moment, %abbrv-31 doit etre fully defined?

./h1 -v2 -log-out -progress Fabrice/essai1.p

-------------------------------------------
waitq:
% |- __def_3(X1) :- fun_main(nil), #q2 (X1).
% |- values (X1,X2) :- fun_main(nil), __def_9(X2), __def_8(X1).
% |- __def_6(X1) :- fun_main(nil), #q3 (X1).
% |- values (X1,X2) :- fun_main(nil), __def_2(X2), __def_1(X1).

----------
autoinfoq:
% |- values (X1,X2) :- __def_3(X2), __def_5(X1).
% |- values (X1,X2) :- __def_6(X2), __def_7(X1).
% |- values (X1,X2) :- __def_3(X2), __def_4(X1).

0
add 5/1, 3/2.
b(5/1,
  b(3/2,1,0),
  0)
add 7/1, 6/2.
b(7/1,
  b(6/2,
   b(5/1,
     b(3/2,1,0),
     0),
   0),
  0)

------
selfq:
% |- #false(clause_conj) :- #q1 .

-----
#q2 (X1) :- values (x,X1). [abbrv-def]

Fully defined:
% |- __def_9(0).
% |- __def_5(y).
% |- __def_7(x2).
% |- __def_8(main_return).
% |- __def_4(x1).
% |- fun_main(nil).
% |- __def_1(x).
% |- __def_2(4).


#q1  :- values (y,4). [abbrv-def]
#q3 (X1) :- values (y,X1). [abbrv-def]

nspriv:
=======

%false(clause_conj)  :- values (x,2).

values(X1,X2) :- __aux_1(X1), __aux_2(X2).
__aux_1(x).

values(X1,X2) :- __aux_13(X1), __aux_12(X2).
__aux_13(x).
__aux_12(2).

---------------------------------------------------------

__aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb) :- state_B_4 (P_S,app2(c_shr,c(r_p(P_B),c(r_p(P_S),v__e))),P_Nb,P_N,P_A,P_B,V__XB1,V__XB2,P_Kab). [rename-resolve:
  __aux_138 (X1,X2,X3,X4,X5,X6,X7,X8) :- state_B_4 (X5,app2(c_shr,c(r_p(X1),c(r_p(X5),v__e))),X8,X3,X7,X1,X2,X4,X6). {X1=P_B,X2=V__XB1,X3=P_N,X4=V__XB2,X5=P_S,X6=P_Kab,X7=P_A,X8=P_Nb}
  ]
	%OK

__aux_139 P_S :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [rename-resolve:
  __aux_139 X1 :- __aux_138 (X2,X3,X4,X5,X1,X6,X7,X8). {X2=P_B,X3=V__XB1,X4=P_N,X5=V__XB2,X1=P_S,X6=P_Kab,X7=P_A,X8=P_Nb}
  ]
	%OK
__aux_141 P_Nb :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [rename-resolve:
  __aux_141 X1 :- __aux_138 (X2,X3,X4,X5,X6,X7,X8,X1). {X2=P_B,X3=V__XB1,X4=P_N,X5=V__XB2,X6=P_S,X7=P_Kab,X8=P_A,X1=P_Nb}
  ]
	%OK
__aux_142 P_N :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [rename-resolve:
  __aux_142 X1 :- __aux_138 (X2,X3,X1,X4,X5,X6,X7,X8). {X2=P_B,X3=V__XB1,X1=P_N,X4=V__XB2,X5=P_S,X6=P_Kab,X7=P_A,X8=P_Nb}
  ]
	%OK
__aux_143 P_A :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [rename-resolve:
  __aux_143 X1 :- __aux_138 (X2,X3,X4,X5,X6,X7,X1,X8). {X2=P_B,X3=V__XB1,X4=P_N,X5=V__XB2,X6=P_S,X7=P_Kab,X1=P_A,X8=P_Nb}
  ]
	%OK
__aux_144 P_B :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [rename-resolve:
  __aux_144 X1 :- __aux_138 (X1,X2,X3,X4,X5,X6,X7,X8). {X1=P_B,X2=V__XB1,X3=P_N,X4=V__XB2,X5=P_S,X6=P_Kab,X7=P_A,X8=P_Nb}
  ]
	%OK
__aux_150 r_p(P_B) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [rename-resolve:
  __aux_150 r_p(X1) :- __aux_138 (X1,X2,X3,X4,X5,X6,X7,X8). {X1=P_B,X2=V__XB1,X3=P_N,X4=V__XB2,X5=P_S,X6=P_Kab,X7=P_A,X8=P_Nb}
  ]
	%OK
__aux_145 V__XB1 :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [rename-resolve:
  __aux_145 X1 :- __aux_138 (X2,X1,X3,X4,X5,X6,X7,X8). {X2=P_B,X1=V__XB1,X3=P_N,X4=V__XB2,X5=P_S,X6=P_Kab,X7=P_A,X8=P_Nb}
  ]
	%OK
__aux_146 V__XB2 :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [rename-resolve:
  __aux_146 X1 :- __aux_138 (X2,X3,X4,X1,X5,X6,X7,X8). {X2=P_B,X3=V__XB1,X4=P_N,X1=V__XB2,X5=P_S,X6=P_Kab,X7=P_A,X8=P_Nb}
  ]
	%OK
__aux_147 P_Kab :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [rename-resolve:
  __aux_147 X1 :- __aux_138 (X2,X3,X4,X5,X6,X1,X7,X8). {X2=P_B,X3=V__XB1,X4=P_N,X5=V__XB2,X6=P_S,X1=P_Kab,X7=P_A,X8=P_Nb}
  ]
	%OK
__aux_152 r_p(P_S) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [rename-resolve:
  __aux_152 r_p(X1) :- __aux_138 (X2,X3,X4,X5,X1,X6,X7,X8). {X2=P_B,X3=V__XB1,X4=P_N,X5=V__XB2,X1=P_S,X6=P_Kab,X7=P_A,X8=P_Nb}
  ]
	%OK
__aux_151 c(r_p(P_S),v__e) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [def-resolve-1:
  __aux_151 c(X1,X2) :- __aux_153 X2, __aux_152 X1.{X1=r_p(P_S),X2=v__e}
  __aux_152 r_p(P_S) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_153 v__e.
  ]
	%OK
__aux_149 c(r_p(P_B),c(r_p(P_S),v__e)) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [def-resolve-1:
  __aux_149 c(X1,X2) :- __aux_151 X2, __aux_150 X1.{X1=r_p(P_B),X2=c(r_p(P_S),v__e)}
  __aux_150 r_p(P_B) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_151 c(r_p(P_S),v__e) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  ]
	%OK (with factoring of two identical literals in body)
__aux_140 app2(c_shr,c(r_p(P_B),c(r_p(P_S),v__e))) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [def-resolve-1:
  __aux_140 app2(X1,X2) :- __aux_149 X2, __aux_148 X1.{X1=c_shr,X2=c(r_p(P_B),c(r_p(P_S),v__e))}
  __aux_148 c_shr.
  __aux_149 c(r_p(P_B),c(r_p(P_S),v__e)) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  ]
	%OK
state_B_end (P_S,app2(c_shr,c(r_p(P_B),c(r_p(P_S),v__e))),P_Nb,P_N,P_A,P_B,V__XB1,V__XB2,P_Kab) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb). [def-resolve-1:
  state_B_end (X1,X2,X3,X4,X5,X6,X7,X8,X9) :- __aux_144 X6, __aux_141 X3, __aux_147 X9, __aux_140 X2, __aux_142 X4, __aux_143 X5, __aux_145 X7, __aux_139 X1, __aux_146 X8.{X1=P_S,X2=app2(c_shr,c(r_p(P_B),c(r_p(P_S),v__e))),X3=P_Nb,X4=P_N,X5=P_A,X6=P_B,X7=V__XB1,X8=V__XB2,X9=P_Kab}
  __aux_139 P_S :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_140 app2(c_shr,c(r_p(P_B),c(r_p(P_S),v__e))) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_141 P_Nb :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_142 P_N :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_143 P_A :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_144 P_B :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_145 V__XB1 :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_146 V__XB2 :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_147 P_Kab :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  ]
	%OK (with factoring of nine identical literals in body).
state_B_end (P_S,app2(c_shr,c(r_p(P_B),c(r_p(P_S),v__e))),P_Nb,P_N,P_A,P_B,V__XB1,V__XB2,P_Kab) :- state_B_4 (P_S,app2(c_shr,c(r_p(P_B),c(r_p(P_S),v__e))),P_Nb,P_N,P_A,P_B,V__XB1,V__XB2,P_Kab). [def-resolve-2:
  state_B_end (P_S,app2(c_shr,c(r_p(P_B),c(r_p(P_S),v__e))),P_Nb,P_N,P_A,P_B,V__XB1,V__XB2,P_Kab) :- __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb).
  __aux_138 (P_B,V__XB1,P_N,V__XB2,P_S,P_Kab,P_A,P_Nb) :- state_B_4 (P_S,app2(c_shr,c(r_p(P_B),c(r_p(P_S),v__e))),P_Nb,P_N,P_A,P_B,V__XB1,V__XB2,P_Kab).
  ]

b defineMe
p pat->what.pair.cdr->what.quote.ref->what.pair.car->what.str.text

stackDepth=6 avant le all
wrongp du all: 0x8550f68
neutralp du all: 0x8550f88
outp du compileSweep: 0x8550f98

list = 5
---[6] list

après startSweep():
---[6] list map-data*29
	profondeur 36

enterp du compileSweep: 0x8550ff8
exitp: 0x8551028
startp: 0x8551038 (en backward)
prof. 36.

---[36] Pblkl

...

compileApply1(), en E_PAT_AS,
stackDepth = 110.
---[110] Pblk Qblk

appelle compilePolyFun1().
compilePolyFun1 (f=0x85a7728, env=0x85aaa30, func=0x8581a78, nargs=2,
    compile=0x80d7fe1 <compileTest>, push=0, wrongp=0x854d380,
    arglist=0x8129120) at bc.c:3516
finp = 0x854d780
globerrp = 0x854d790
compilePolyFun0 (f=0x85a7728, env=0x85aaa30, func=0x8581a78, nargs=2,
    compile=0x80d7fe1 <compileTest>, push=0, wrongp=0x854d380,
    globerrp=0x854d790, finp=0x854d780, arglist=0x8129120) at bc.c:3205
compileTest (f=0x85a7728, env=0x85aaa80, test=0x8581a58, wrongp=0x854d380)



après le 4ème pretty:
top = 0x8586110
top-2:
0x8586108:      0x084f72c0      0x080f43d8
0x857b91a	DROP 1		--- Qblkl=0x084f72c0
0x857b91e:      [9       -32]
		FETCH -32	--- Qblkl Pblkl=0x84f7730
		[195     1       8]
		IS_NIL 1, 8	[goto taken]
0x857b936:      [70      -32]
		STARTLISTSWEEP -32	--- Qblkl Pblkl=0x84f7730
		[70      -2]
		STARTLISTSWEEP -2	--- Qblkl Pblkl Qblkl
		[86      0       11]
		GOTO_0 0, 11
0x857b956:      [73      -2]
		GETLISTSWEEP -2		--- Qblkl Pblkl Qblkl Pblk=0x84f76c0
		[73      -2]
		GETLISTSWEEP -2		--- Qblkl Pblkl Qblkl Pblk Qblk=0x84f7250
		[143]
		FETCH_m2
		[143]
		FETCH_m2
		[88]
		FUNCTION	--- Qblkl Pblkl Qblkl Pblk Qblk Pblk Qblk
		[144]
		FETCH_m1	--- Qblkl Pblkl Qblkl Pblk Qblk Pblk Qblk Qblk
0x857b966:      [142]
		FETCH_m3	--- Qblkl Pblkl Qblkl Pblk Qblk Pblk Qblk Qblk Pblk
		[172]
		DIFF		--- Qblkl Pblkl Qblkl Pblk Qblk Pblk Qblk Qblk-Pblk
		[201     0       4]
		IS_EMPTY 0,4	--- Qblkl Pblkl Qblkl Pblk Qblk Pblk Qblk Qblk-Pblk
			(* top = 0x8586128 *)
			(* Qblk-Pblk = Qblk *)
0x857b976:      [71      -1]
		STARTMAPSWEEP -1
		--- Qblkl Pblkl Qblkl Pblk Qblk Pblk Qblk Qblk-Pblk 0x084f7250 29*0
			(* top = 0x85861a0 Qblk=Qblk-Pblk=0x084f7250 *)
		[86      0       8]
		GOTO_0 0, 8
0x857b98c:      [74      -30]
		GETMAPSWEEP -30	--- ... 0x084f7250
		[38]
		CAR	--- ... 0x84f8ef8
			(* 0x84f8ef8 = "__inter_odd_and_zero__mod__3__inter_odd_and_two__mod__3" *)
		[9       -34]
		FETCH -34	--- ... 0x84f8ef8 Pblk
		[201     1       4]
		IS_EMPTY 1, 4
			(* drop 1 ici *)
0x857b9a2:      [71      -34]
		STARTMAPSWEEP -34	--- ... 0x84f8ef8 0x084f76c0 29*0
			(* Pblk=0x084f76c0 *)
		[86      0       8]
		GOTO_0 0, 8
0x857b9b8:      [74      -30]
		GETMAPSWEEP -30		--- ... 0x84f8ef8 0x084f76c0 29*0 0x084f76c0
		[38]
		CAR		--- ... 0x84f8ef8 0x084f76c0 29*0 0x81f5f30
			(* 0x81f5f30 = "__inter_even_and_zero__mod__3" *)
		[23      -175    1]
		VARREF0 -175, 1	--- ... 0x84f8ef8 0x084f76c0 29*0 0x81f5f30 detect
			(* detect = 0x84f7bc0 *)
		[143]
		FETCH_m2	--- ... 0x84f8ef8 0x084f76c0 29*0 0x81f5f30 detect 0x81f5f30
		[9 -34]
		FETCH -34	--- ... 0x84f8ef8 0x084f76c0 29*0 0x81f5f30 detect 0x81f5f30 0x84f8ef8
			(* top = 0x858622c *)
		[55      2]
		N_CALL 2	(* retourne true *)
       62      0       6       87      2
0x857b9d8:      31      31      13      29      1       86      0       -28
0x857b9e8:      87      2       29      30      86      0       5       86



h1mc -v needham_saturation.model.pl a.log
h1mc.opt -v needham_saturation.model.pl a1.log



Checking clause __def_231(pub(X1)) :- __def_229 (X1,X2,X3)... failed.

__def_231(pub(X1)) :- __def_229 (X1,X2,X3).

knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).

__def_231(pub(A)) :- __def_229 (A,B,Na). [rename-resolve:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3). {X1=A,X2=B,X3=Na}
  ]

knows(crypt(cons(Na,cons(nonceb(cons(B,cons(A,nil))),cons(pub(B),nil))),pub(A))) :- __def_229 (A,B,Na). [def-resolve-1:
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).{X1=cons(Na,cons(nonceb(cons(B,cons(A,nil))),cons(pub(B),nil))),X2=pub(A)}
  __def_230(cons(Na,cons(nonceb(cons(B,cons(A,nil))),cons(pub(B),nil)))) :- __def_229 (A,B,Na).
  __def_231(pub(A)) :- __def_229 (A,B,Na).
  ]

#q61 (X1,X2) :- __def_231(pub(X2)), __def_230(X1). [auto-resolve:
  #q61 (X1,X2) :- knows(crypt(X1,pub(X2))).
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).{X2=pub(X2)}
  ]
#ne(knows) :- __def_231(X2), __def_230(X1). [eps-resolve:
  #ne(knows) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(knows) :- __def_231(X2), __def_230(X1). [auto-resolve:
  #ne(knows) :- __def_231(X2), __def_230(X1).
  ]
#ne(__def_231) :- __def_231(X1). [split-def]
#ne(__def_230) :- __def_230(X1). [split-def]
#ne(knows) :- #ne(__def_231), #ne(__def_230). [split-use:
  #ne(knows) :- __def_231(X2), __def_230(X1).
  ]
__type_57(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  __type_57(X1) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__type_57(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [auto-resolve:
  __type_57(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_57) :- __def_231(X2), __def_230(X1). [eps-resolve:
  #ne(__type_57) :- __type_57(X1). {X1=crypt(X1,X2)}
  __type_57(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_57) :- #ne(__def_231), #ne(__def_230). [split-use:
  #ne(__type_57) :- __def_231(X2), __def_230(X1).
  ]
__type_59(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  __type_59(X1) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__type_59(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [auto-resolve:
  __type_59(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_59) :- __def_231(X2), __def_230(X1). [eps-resolve:
  #ne(__type_59) :- __type_59(X1). {X1=crypt(X1,X2)}
  __type_59(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_59) :- #ne(__def_231), #ne(__def_230). [split-use:
  #ne(__type_59) :- __def_231(X2), __def_230(X1).
  ]
__def_231(pub(X1)) :- knows(X3), agent(X2), knows(X1). [auto-resolve:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- knows(X3), agent(X2), knows(X1).
  ]
__def_231(pub(X1)) :- #ne(knows), #ne(agent), knows(X1). [split-use:
  __def_231(pub(X1)) :- knows(X3), agent(X2), knows(X1).
  ]
__def_231(pub(X1)) :- #ne(agent), knows(X1). [q-resolve:
  __def_231(pub(X1)) :- #ne(knows), #ne(agent), knows(X1).
  #ne(knows).
  ]
__def_231(pub(X1)) :- knows(X1). [q-resolve:
  __def_231(pub(X1)) :- #ne(agent), knows(X1).
  #ne(agent).
  ]
__def_231(pub(X1)) :- __def_208(X3), __type_49(X2), __type_48(X1). [auto-re
solve:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_49(X2), __type_48(X1).
  ]
__def_231(pub(X1)) :- #ne(__def_208), #ne(__type_49), __type_48(X1). [split
-use:
  __def_231(pub(X1)) :- __def_208(X3), __type_49(X2), __type_48(X1).
  ]
#q61 (X1,X2) :- knows(X2), __def_230(X1). [auto-resolve:
  #q61 (X1,X2) :- __def_231(pub(X2)), __def_230(X1).
  __def_231(pub(X1)) :- knows(X1).{X1=X2}
  ]
#ne(__def_231) :- knows(X1). [eps-resolve:
  #ne(__def_231) :- __def_231(X1). {X1=pub(X1)}
  __def_231(pub(X1)) :- knows(X1).
  ]
#ne(__def_231) :- agent(X1). [eps-resolve:
  #ne(__def_231) :- knows(X1). {X1=pub(X1)}
  knows(pub(X1)) :- agent(X1).
  ]
#ne(__def_231) :- agent(X1). [auto-resolve:
  #ne(__def_231) :- agent(X1).
  ]
#ne(__def_231). [eps-resolve:
  #ne(__def_231) :- knows(X1). {X1=nil}
  knows(nil).
  ]
#ne(__def_231). [auto-resolve:
  #ne(__def_231).
  ]
#ne(__def_231) :- __type_44(X2), __type_45(X1). [eps-resolve:
  #ne(__def_231) :- knows(X1). {X1=encr(X1,X2)}
  knows(encr(X1,X2)) :- __type_44(X2), __type_45(X1).
  ]
#ne(__def_231) :- __type_44(X2), __type_45(X1). [auto-resolve:
  #ne(__def_231) :- __type_44(X2), __type_45(X1).
  ]
#ne(__def_231) :- #ne(__type_44), #ne(__type_45). [split-use:
  #ne(__def_231) :- __type_44(X2), __type_45(X1).
  ]
#ne(__def_231) :- #ne(__type_45). [q-resolve:
  #ne(__def_231) :- #ne(__type_44), #ne(__type_45).
  #ne(__type_44).
  ]
#ne(__def_231). [q-resolve:
  #ne(__def_231) :- #ne(__type_45).
  #ne(__type_45).
  ]
#ne(__def_231) :- knows(X2), knows(X1). [eps-resolve:
  #ne(__def_231) :- knows(X1). {X1=cons(X1,X2)}
  knows(cons(X1,X2)) :- knows(X2), knows(X1).
  ]
#ne(__def_231) :- knows(X2), knows(X1). [auto-resolve:
  #ne(__def_231) :- knows(X2), knows(X1).
  ]
#ne(__def_231) :- #ne(knows). [split-use:
  #ne(__def_231) :- knows(X2), knows(X1).
  ]
#ne(__def_231). [q-resolve:
  #ne(__def_231) :- #ne(knows).
  #ne(knows).
  ]
#ne(__def_231) :- __def_228(X1). [eps-resolve:
  #ne(__def_231) :- knows(X1). {X1=prv(X1)}
  knows(prv(X1)) :- __def_228(X1).
  ]
#ne(__def_231) :- __def_228(X1). [auto-resolve:
  #ne(__def_231) :- __def_228(X1).
  ]
#ne(__def_231) :- knows(X2), knows(X1). [eps-resolve:
  #ne(__def_231) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- knows(X2), knows(X1).
  ]
#ne(__def_231) :- knows(X2), knows(X1). [auto-resolve:
  #ne(__def_231) :- knows(X2), knows(X1).
  ]
#ne(__def_231) :- #ne(knows). [split-use:
  #ne(__def_231) :- knows(X2), knows(X1).
  ]
#ne(__def_231). [q-resolve:
  #ne(__def_231) :- #ne(knows).
  #ne(knows).
  ]
#ne(__def_231) :- __def_231(X2), __def_230(X1). [eps-resolve:
  #ne(__def_231) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__def_231) :- __def_231(X2), __def_230(X1). [auto-resolve:
  #ne(__def_231) :- __def_231(X2), __def_230(X1).
  ]
#ne(__def_231) :- #ne(__def_231), #ne(__def_230). [split-use:
  #ne(__def_231) :- __def_231(X2), __def_230(X1).
  ]
#ne(__def_231) :- #ne(__def_231). [q-resolve:
  #ne(__def_231) :- #ne(__def_231), #ne(__def_230).
  #ne(__def_230).
#ne(__def_231) :- __def_207(X2), __def_206(X1). [eps-resolve:
  #ne(__def_231) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_207(X2), __def_206(X1).
  ]
#ne(__def_231) :- __def_207(X2), __def_206(X1). [auto-resolve:
  #ne(__def_231) :- __def_207(X2), __def_206(X1).
  ]
#ne(__def_231) :- #ne(__def_206), #ne(__def_207). [split-use:
  #ne(__def_231) :- __def_207(X2), __def_206(X1).
  ]
#ne(__def_231) :- __def_225(X2), __type_56(X1). [eps-resolve:
  #ne(__def_231) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_225(X2), __type_56(X1).
  ]
#ne(__def_231) :- __def_225(X2), __type_56(X1). [auto-resolve:
  #ne(__def_231) :- __def_225(X2), __type_56(X1).
  ]
#ne(__def_231) :- #ne(__type_56), #ne(__def_225). [split-use:
  #ne(__def_231) :- __def_225(X2), __type_56(X1).
  ]
#ne(__def_231). [eps-resolve:
  #ne(__def_231) :- agent(X1). {X1=bob}
  agent(bob).
  ]
#ne(__def_231). [eps-resolve:
  #ne(__def_231) :- agent(X1). {X1=alice}
  agent(alice).
  ]
#ne(__def_231). [eps-resolve:
  #ne(__def_231) :- agent(X1). {X1=intrus}
  agent(intrus).
  ]
#ne(knows) :- #ne(__def_230). [q-resolve:
  #ne(knows) :- #ne(__def_231), #ne(__def_230).
  #ne(__def_231).
  ]
#ne(__type_59) :- #ne(__def_230). [q-resolve:
  #ne(__type_59) :- #ne(__def_231), #ne(__def_230).
  #ne(__def_231).
  ]
#ne(__type_57) :- #ne(__def_230). [q-resolve:
  #ne(__type_57) :- #ne(__def_231), #ne(__def_230).
  #ne(__def_231).
  ]
#ne(__def_231). [q-resolve:
  #ne(__def_231) :- #ne(__def_231).
  #ne(__def_231).
  ]
__def_231(pub(X1)) :- __def_208(X3), agent(X2), __type_48(X1). [auto-resolv
e:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), agent(X2), __type_48(X1).
  ]
__def_231(pub(X1)) :- #ne(__def_208), #ne(agent), __type_48(X1). [split-use
:
  __def_231(pub(X1)) :- __def_208(X3), agent(X2), __type_48(X1).
  ]
__def_231(pub(X1)) :- #ne(__def_208), __type_48(X1). [q-resolve:
  __def_231(pub(X1)) :- #ne(__def_208), #ne(agent), __type_48(X1).
  #ne(agent).
  ]
__def_147(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  __def_147(X1) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__def_147(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [auto-resolve:
  __def_147(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#q85 (X1) :- __def_231(pub(alice)), __def_230(X1). [auto-resolve:
  #q85 (X1) :- __def_147(crypt(X1,pub(alice))).
  __def_147(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).{X2=pub(alice)}
  ]
#q85 (X1) :- knows(alice), __def_230(X1). [auto-resolve:
  #q85 (X1) :- __def_231(pub(alice)), __def_230(X1).
  __def_231(pub(X1)) :- knows(X1).{X1=alice}
  ]
__def_143(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  __def_143(X1) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__def_143(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [auto-resolve:
  __def_143(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__def_143) :- __def_231(X2), __def_230(X1). [eps-resolve:
  #ne(__def_143) :- __def_143(X1). {X1=crypt(X1,X2)}
  __def_143(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__def_143) :- #ne(__def_231), #ne(__def_230). [split-use:
  #ne(__def_143) :- __def_231(X2), __def_230(X1).
  ]
#ne(__def_143) :- #ne(__def_230). [q-resolve:
  #ne(__def_143) :- #ne(__def_231), #ne(__def_230).
  #ne(__def_231).
  ]
__type_52(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  __type_52(X1) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__type_52(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [auto-resolve:
  __type_52(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_52) :- __def_231(X2), __def_230(X1). [eps-resolve:
  #ne(__type_52) :- __type_52(X1). {X1=crypt(X1,X2)}
  __type_52(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_52) :- #ne(__def_231), #ne(__def_230). [split-use:
  #ne(__type_52) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_52) :- #ne(__def_230). [q-resolve:
  #ne(__type_52) :- #ne(__def_231), #ne(__def_230).
  #ne(__def_231).
  ]
__type_51(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  __type_51(X1) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__type_51(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [auto-resolve:
  __type_51(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__type_53(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  __type_53(X1) :- knows(X1). {X1=crypt(X1,X2)}
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__type_53(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [auto-resolve:
  __type_53(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_53) :- __def_231(X2), __def_230(X1). [eps-resolve:
  #ne(__type_53) :- __type_53(X1). {X1=crypt(X1,X2)}
  __type_53(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_53) :- #ne(__def_231), #ne(__def_230). [split-use:
  #ne(__type_53) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_53) :- #ne(__def_230). [q-resolve:
  #ne(__type_53) :- #ne(__def_231), #ne(__def_230).
  #ne(__def_231).
  ]
__type_55(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  __type_55(X1) :- __type_52(X1). {X1=crypt(X1,X2)}
  __type_52(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__type_55(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [auto-resolve:
  __type_55(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__type_56(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  __type_56(X1) :- __type_55(X1). {X1=crypt(X1,X2)}
  __type_55(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_56) :- __def_231(X2), __def_230(X1). [eps-resolve:
  #ne(__type_56) :- __type_56(X1). {X1=crypt(X1,X2)}
  __type_56(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_56) :- #ne(__def_231), #ne(__def_230). [split-use:
  #ne(__type_56) :- __def_231(X2), __def_230(X1).
  ]
#ne(__type_56) :- #ne(__def_230). [q-resolve:
  #ne(__type_56) :- #ne(__def_231), #ne(__def_230).
  #ne(__def_231).
  ]
#ne(__def_231) :- #ne(__def_225). [q-resolve:
  #ne(__def_231) :- #ne(__type_56), #ne(__def_225).
  #ne(__type_56).
  ]
__def_231(pub(X1)) :- __def_208(X3), __type_54(X2), __type_48(X1). [auto-re
solve:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_54(X2), __type_48(X1).
  ]
__def_231(pub(X1)) :- #ne(__def_208), #ne(__type_54), __type_48(X1). [split
-use:
  __def_231(pub(X1)) :- __def_208(X3), __type_54(X2), __type_48(X1).
  ]
__def_231(pub(X1)) :- #ne(__def_208), __type_48(X1). [q-resolve:
  __def_231(pub(X1)) :- #ne(__def_208), #ne(__type_54), __type_48(X1).
  #ne(__type_54).
  ]
__def_231(pub(X1)) :- knows(X3), __type_54(X2), knows(X1). [auto-resolve:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- knows(X3), __type_54(X2), knows(X1).
  ]
__def_231(pub(X1)) :- #ne(knows), #ne(__type_54), knows(X1). [split-use:
  __def_231(pub(X1)) :- knows(X3), __type_54(X2), knows(X1).
  ]
__def_231(pub(X1)) :- #ne(__type_54), knows(X1). [q-resolve:
  __def_231(pub(X1)) :- #ne(knows), #ne(__type_54), knows(X1).
  #ne(knows).
  ]
__def_231(pub(X1)) :- knows(X1). [q-resolve:
  __def_231(pub(X1)) :- #ne(__type_54), knows(X1).
  #ne(__type_54).
  ]
__def_143(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  __def_143(X1) :- __type_56(X1). {X1=crypt(X1,X2)}
  __type_56(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
__def_143(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [auto-resolve:
  __def_143(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [eps-resolve:
  knows(X1) :- __type_56(X1). {X1=crypt(X1,X2)}
  __type_56(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]
knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1). [auto-resolve:
  knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
  ]

---------------

knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
__type_57(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
__type_59(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
__def_231(pub(X1)) :- knows(X1).
__def_143(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
(__def_231(pub(X1)) :- knows(X1).)
(__def_143(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).)
(knows(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).)

__def_231(pub(X1)) :- __def_229 (X1,X2,X3).
#q61 (X1,X2) :- __def_231(pub(X2)), __def_230(X1).
#ne(knows) :- __def_231(X2), __def_230(X1).
#ne(__type_59) :- __def_231(X2), __def_230(X1).
__def_231(pub(X1)) :- __def_208(X3), __type_49(X2), __type_48(X1).
__def_231(pub(X1)) :- #ne(__def_208), #ne(__type_49), __type_48(X1).
#q61 (X1,X2) :- knows(X2), __def_230(X1).
#ne(__def_231).
#ne(knows) :- #ne(__def_230).
#ne(__type_59) :- #ne(__def_230).
#ne(__type_57) :- #ne(__def_230).
__def_231(pub(X1)) :- __def_208(X3), agent(X2), __type_48(X1).
__def_231(pub(X1)) :- #ne(__def_208), __type_48(X1).
__def_147(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
#q85 (X1) :- __def_231(pub(alice)), __def_230(X1).
#q85 (X1) :- knows(alice), __def_230(X1).
#ne(__def_143) :- __def_231(X2), __def_230(X1).
#ne(__def_143) :- #ne(__def_230).
__type_52(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
#ne(__type_52) :- __def_231(X2), __def_230(X1).
#ne(__type_52) :- #ne(__def_230).
__type_51(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
__type_53(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
#ne(__type_53) :- __def_231(X2), __def_230(X1).
#ne(__type_53) :- #ne(__def_230).
__type_55(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
__type_56(crypt(X1,X2)) :- __def_231(X2), __def_230(X1).
#ne(__type_56) :- __def_231(X2), __def_230(X1).
#ne(__type_56) :- #ne(__def_230).
#ne(__def_231) :- #ne(__def_225).
__def_231(pub(X1)) :- __def_208(X3), __type_54(X2), __type_48(X1).
__def_231(pub(X1)) :- #ne(__def_208), __type_48(X1).

-----------------

__def_229 (A,B,Na) :- knows(crypt(cons(Na,cons(A,nil)),pub(B))).

__def_229 (X1,X2,X3) :- knows(X3), agent(X2), knows(X1).
__def_229 (X1,X2,X3) :- __def_208(X3), __type_49(X2), __type_48(X1).
__def_229 (X1,X2,X3) :- __def_208(X3), agent(X2), __type_48(X1).
__def_229 (X1,X2,X3) :- __def_208(X3), __type_54(X2), __type_48(X1).
__def_229 (X1,X2,X3) :- knows(X3), __type_54(X2), knows(X1).

__def_231(pub(X1)) :- __def_208(X3), __type_49(X2), __type_48(X1).

#q18 (X1,X2,X3) :- knows(crypt(cons(X1,cons(X2,nil)),pub(X3))). [abbrv-def]
__def_229 (X1,X2,X3) :- #q18 (X3,X1,X2). [abbrv-use:
  __def_229 (X1,X2,X3) :- knows(crypt(cons(X3,cons(X1,nil)),pub(X2))).
  ]
__def_229 (X1,X2,X3) :- knows(X3), agent(X2), knows(X1). [auto-resolve:
  __def_229 (X1,X2,X3) :- #q18 (X3,X1,X2).
  #q18 (X1,X2,X3) :- agent(X3), knows(X2), knows(X1).{X1=X3,X2=X1,X3=X2}
  ]
__def_229 (X1,X2,X3) :- __def_208(X3), __type_49(X2), __type_48(X1). [auto-
resolve:
  __def_229 (X1,X2,X3) :- #q18 (X3,X1,X2).
  #q18 (X1,X2,X3) :- __type_49(X3), __type_48(X2), __def_208(X1).{X1=X3,X2=
X1,X3=X2}
  ]
__type_57(X1) :- agent(X3), knows(X2), knows(X1). [auto-resolve:
  __type_57(X1) :- __def_229 (X2,X3,X1).
  __def_229 (X1,X2,X3) :- knows(X3), agent(X2), knows(X1).{X1=X2,X2=X3,X3=X
1}
  ]
__type_59(X1) :- knows(X3), agent(X2), knows(X1). [auto-resolve:
  __type_59(X1) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- knows(X3), agent(X2), knows(X1).
  ]
__type_58(X1) :- knows(X3), knows(X2), agent(X1). [auto-resolve:
  __type_58(X1) :- __def_229 (X2,X1,X3).
  __def_229 (X1,X2,X3) :- knows(X3), agent(X2), knows(X1).{X1=X2,X2=X1}
  ]
__type_57(X1) :- __type_49(X3), __type_48(X2), __def_208(X1). [auto-resolve
:
  __type_57(X1) :- __def_229 (X2,X3,X1).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_49(X2), __type_48(X1).{X1=X
2,X2=X3,X3=X1}
  ]
__type_59(X1) :- __def_208(X3), __type_49(X2), __type_48(X1). [auto-resolve
:
  __type_59(X1) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_49(X2), __type_48(X1).
  ]
__type_58(X1) :- __def_208(X3), __type_48(X2), __type_49(X1). [auto-resolve
:
  __type_58(X1) :- __def_229 (X2,X1,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_49(X2), __type_48(X1).{X1=X
2,X2=X1}
  ]
__def_238(pub(X1)) :- knows(X3), knows(X2), agent(X1). [auto-resolve:
  __def_238(pub(X1)) :- __def_229 (X2,X1,X3).
  __def_229 (X1,X2,X3) :- knows(X3), agent(X2), knows(X1).{X1=X2,X2=X1}
  ]
__def_238(pub(X1)) :- __def_208(X3), __type_48(X2), __type_49(X1). [auto-re
solve:
  __def_238(pub(X1)) :- __def_229 (X2,X1,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_49(X2), __type_48(X1).{X1=X
2,X2=X1}
  ]
__def_231(pub(X1)) :- knows(X3), agent(X2), knows(X1). [auto-resolve:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- knows(X3), agent(X2), knows(X1).
  ]
__def_231(pub(X1)) :- __def_208(X3), __type_49(X2), __type_48(X1). [auto-re
solve:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_49(X2), __type_48(X1).
  ]
__def_229 (X1,X2,X3) :- __def_208(X3), agent(X2), __type_48(X1). [auto-reso
lve:
  __def_229 (X1,X2,X3) :- #q18 (X3,X1,X2).
  #q18 (X1,X2,X3) :- agent(X3), __type_48(X2), __def_208(X1).{X1=X3,X2=X1,X
3=X2}
  ]
__type_57(X1) :- agent(X3), __type_48(X2), __def_208(X1). [auto-resolve:
  __type_57(X1) :- __def_229 (X2,X3,X1).
  __def_229 (X1,X2,X3) :- __def_208(X3), agent(X2), __type_48(X1).{X1=X2,X2
=X3,X3=X1}
  ]
__type_59(X1) :- __def_208(X3), agent(X2), __type_48(X1). [auto-resolve:
  __type_59(X1) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), agent(X2), __type_48(X1).
  ]
__def_238(pub(X1)) :- __def_208(X3), __type_48(X2), agent(X1). [auto-resolv
e:
  __def_238(pub(X1)) :- __def_229 (X2,X1,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), agent(X2), __type_48(X1).{X1=X2,X2
=X1}
  ]
__type_58(X1) :- __def_208(X3), __type_48(X2), agent(X1). [auto-resolve:
  __type_58(X1) :- __def_229 (X2,X1,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), agent(X2), __type_48(X1).{X1=X2,X2
=X1}
  ]
__def_231(pub(X1)) :- __def_208(X3), agent(X2), __type_48(X1). [auto-resolv
e:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), agent(X2), __type_48(X1).
  ]
__def_229 (X1,X2,X3) :- __def_208(X3), __type_54(X2), __type_48(X1). [auto-
resolve:
  __def_229 (X1,X2,X3) :- #q18 (X3,X1,X2).
  #q18 (X1,X2,X3) :- __type_54(X3), __type_48(X2), __def_208(X1).{X1=X3,X2=
X1,X3=X2}
  ]
__type_57(X1) :- __type_54(X3), __type_48(X2), __def_208(X1). [auto-resolve
:
  __type_57(X1) :- __def_229 (X2,X3,X1).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_54(X2), __type_48(X1).{X1=X
2,X2=X3,X3=X1}
  ]
__type_59(X1) :- __def_208(X3), __type_54(X2), __type_48(X1). [auto-resolve
:
  __type_59(X1) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_54(X2), __type_48(X1).
  ]
__def_238(pub(X1)) :- __def_208(X3), __type_48(X2), __type_54(X1). [auto-re
solve:
  __def_238(pub(X1)) :- __def_229 (X2,X1,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_54(X2), __type_48(X1).{X1=X
2,X2=X1}
  ]
__type_58(X1) :- __def_208(X3), __type_48(X2), __type_54(X1). [auto-resolve
:
  __type_58(X1) :- __def_229 (X2,X1,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_54(X2), __type_48(X1).{X1=X
2,X2=X1}
  ]
__def_231(pub(X1)) :- __def_208(X3), __type_54(X2), __type_48(X1). [auto-re
solve:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- __def_208(X3), __type_54(X2), __type_48(X1).
  ]
__def_229 (X1,X2,X3) :- knows(X3), __type_54(X2), knows(X1). [auto-resolve:
  __def_229 (X1,X2,X3) :- #q18 (X3,X1,X2).
  #q18 (X1,X2,X3) :- __type_54(X3), knows(X2), knows(X1).{X1=X3,X2=X1,X3=X2
}
  ]
__type_57(X1) :- __type_54(X3), knows(X2), knows(X1). [auto-resolve:
  __type_57(X1) :- __def_229 (X2,X3,X1).
  __def_229 (X1,X2,X3) :- knows(X3), __type_54(X2), knows(X1).{X1=X2,X2=X3,
X3=X1}
  ]
__type_59(X1) :- knows(X3), __type_54(X2), knows(X1). [auto-resolve:
  __type_59(X1) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- knows(X3), __type_54(X2), knows(X1).
  ]
__def_238(pub(X1)) :- knows(X3), knows(X2), __type_54(X1). [auto-resolve:
  __def_238(pub(X1)) :- __def_229 (X2,X1,X3).
  __def_229 (X1,X2,X3) :- knows(X3), __type_54(X2), knows(X1).{X1=X2,X2=X1}
  ]
__type_58(X1) :- knows(X3), knows(X2), __type_54(X1). [auto-resolve:
  __type_58(X1) :- __def_229 (X2,X1,X3).
  __def_229 (X1,X2,X3) :- knows(X3), __type_54(X2), knows(X1).{X1=X2,X2=X1}
  ]
__def_231(pub(X1)) :- knows(X3), __type_54(X2), knows(X1). [auto-resolve:
  __def_231(pub(X1)) :- __def_229 (X1,X2,X3).
  __def_229 (X1,X2,X3) :- knows(X3), __type_54(X2), knows(X1).
  ]


[goubault@dell14 Fabrice]$ memtime ../h1 -v2 -no-sort-simplify -monadic-proxy needham_saturation.p
Error: uncaught exception: CheckPdef |[refcount = 11,shouldbe = 9,predicate = "#q1"]|.
Exit [10]
0.92 user, 0.02 system, 1.35 elapsed -- Max VSize = 14980KB, Max RSS = 12052KB

% |- #q1 (X1,X2) :- values (field(field(field(alice_mess_3,msg),msg3),nonce),cons(X1,cons(pub(X2),nil))).
% |- #q1 (X1,X2) :- __def_73(field(field(field(alice_mess_3,msg),msg3),nonce)), __def_72(cons(X1,cons(pub(X2),nil))).
% |- #q1 (X1,X2) :- __def_56(field(field(field(alice_mess_3,msg),msg3),nonce)), __def_55(cons(X1,cons(pub(X2),nil))).
% |- #q1 (X1,X2) :- __type_25(cons(X1,cons(pub(X2),nil))), __def_8(field(field(field(alice_mess_3,msg),msg3),nonce)).
% |- #q1 (X1,X2) :- knows(cons(X1,cons(pub(X2),nil))), __def_127(field(field(field(alice_mess_3,msg),msg3),nonce)).
% |- #q1 (X1,X2) :- __type_8(cons(X1,cons(pub(X2),nil))), __def_2(field(field(field(alice_mess_3,msg),msg3),nonce)).
% |- #q1 (X1,X2) :- __type_19(cons(X1,cons(pub(X2),nil))), __def_6(field(field(field(alice_mess_3,msg),msg3),nonce)).
% |- #q1 (X1,X2) :- __type_32(cons(X1,cons(pub(X2),nil))), __def_10(field(field(field(alice_mess_3,msg),msg3),nonce)).
% |- #q1 (X1,X2) :- __type_40(cons(X1,cons(pub(X2),nil))), __def_13(field(field(field(alice_mess_3,msg),msg3),nonce)).
% |- #q1 (X1,X2) :- __def_143(cons(X1,cons(pub(X2),nil))), __def_142(field(field(field(alice_mess_3,msg),msg3),nonce)).
% |- #q1 (X1,X2) :- __def_158(field(field(field(alice_mess_3,msg),msg3),nonce)), __def_157(cons(X1,cons(pub(X2),nil))).
% |- #q1 (X1,X2) :- __type_4(cons(X1,cons(pub(X2),nil))), __def_1(field(field(field(alice_mess_3,msg),msg3),nonce)).

Adding __type_5 <= __def_529.
Adding __type_5 <= __def_284.
Adding __type_5 <= __def_305.
Adding __type_5 <= __def_5.
Adding __type_5 <= __def_12.
Adding __type_5 <= __type_14.
Adding __type_5 <= __type_18.

Adding __type_18 <= __type_5.
Adding __type_18 <= __def_305.
Adding __type_18 <= __type_14.
Adding __type_18 <= __def_5.
Adding __type_18 <= __def_12.


Checking clause values (X1,X2) :- __def_167(X2), __def_168(X1)...*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++values (X2,X1)
 ** Testing {[{"__def_102"},{"__def_132"}],
 [{"__def_73"},{"__def_74"}],
 [{"__def_122"},{"__def_123"}],
 [{"__def_47"},{"__def_48"}],
 [{"__def_64"},{"__def_54"}],
 [{"__def_50"},{"__def_49"}],
 [{"__def_77"},{"__def_78"}],
 [{"__type_16"},{"__def_108"}],
 [{"__def_99"},{"__def_98"}],
 [{"__def_205"},{"__def_204"}],
 [{"__def_139"},{"__def_138"}],
 [{"__def_152"},{"__def_153"}],
 [{"__def_26"},{"__def_27"}],
 [{"__def_136"},{"__def_123"}],
 [{"__def_232"},{"__type_19"}],
 [{"__def_90"},{"__def_91"}],
 [{"__def_2"},{"__type_1"}],
 [{"__def_212"},{"__def_128"}],
 [{"__def_183"},{"__def_184"}],
 [{"__def_150"},{"__def_151"}],
 [{"__def_109"},{"__def_110"}],
 [{"__def_200"},{"__def_199"}],
 [{"__def_190"},{"__def_191"}],
 [{"__def_117"},{"__def_116"}],
 [{"__def_35"},{"__def_36"}],
 [{"__def_125"},{"__def_124"}],
 [{"__def_182"},{"__def_153"}],
 [{"__def_82"},{"__type_1"}],
 [{"__def_69"},{"__def_70"}],
 [{"__def_111"},{"__def_54"}],
 [{"__def_60"},{"__def_61"}],
 [{"__def_115"},{"__def_114"}],
 [{"__def_160"},{"__def_159"}],
 [{"__def_10"},{"__type_5"}],
 [{"__def_149"},{"__def_138"}],
 [{"__def_143"},{"knows"}],
 [{"__def_65"},{"__def_66"}],
 [{"__def_80"},{"__def_79"}],
 [{"__def_208"},{"__def_207"}],
 [{"__def_158"},{"__def_157"}],
 [{"__type_3"},{"__def_6"}],
 [{"__def_52"},{"__def_51"}],
 [{"__def_102"},{"__def_103"}],
 [{"__def_201"},{"__def_202"}],
 [{"__def_121"},{"__def_116"}],
 [{"__def_210"},{"__def_209"}],
 [{"__def_83"},{"__def_54"}],
 [{"__def_38"},{"__def_39"}],
 [{"__def_134"},{"__def_105"}],
 [{"__def_211"},{"__def_209"}],
 [{"__def_84"},{"__def_85"}],
 [{"__def_194"},{"__def_48"}],
 [{"__def_106"},{"__def_105"}],
 [{"__def_226"},{"__def_227"}],
 [{"__def_196"},{"__def_195"}],
 [{"__def_131"},{"__def_130"}],
 [{"__def_13"},{"__type_7"}],
 [{"__def_148"},{"__def_147"}],
 [{"__def_23"},{"__def_24"}],
 [{"__def_141"},{"__def_140"}],
 [{"__type_15"},{"__def_42"}],
 [{"__def_175"},{"__def_176"}],
 [{"__def_97"},{"__def_96"}],
 [{"__def_87"},{"__def_88"}],
 [{"__def_129"},{"__def_128"}],
 [{"__def_95"},{"__def_48"}],
 [{"__def_206"},{"__def_170"}],
 [{"__def_135"},{"knows"}],
 [{"__def_186"},{"__def_187"}],
 [{"__def_53"},{"__def_54"}],
 [{"__def_165"},{"__def_166"}],
 [{"__def_119"},{"__def_118"}],
 [{"__def_144"},{"__def_145"}],
 [{"__def_56"},{"__def_57"}],
 [{"__def_29"},{"__def_30"}],
 [{"__def_172"},{"__def_173"}],
 [{"__def_113"},{"__def_112"}],
 [{"__def_4"},{"__type_2"}],
 [{"__def_198"},{"__def_197"}],
 [{"__def_16"},{"__type_9"}],
 [{"__def_169"},{"__def_170"}],
 [{"__def_94"},{"__def_49"}],
 [{"__def_156"},{"__def_155"}],
 [{"__def_162"},{"__def_163"}],
 [{"__def_161"},{"__def_54"}],
 [{"__def_32"},{"__def_33"}],
 [{"__def_213"},{"__def_123"}],
 [{"__def_179"},{"__def_180"}]}
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_132(X1)
*** find_auto_subsumer --__def_168(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_167(mSG3)
*** find_auto_subsumer
*** find_auto_subsumer --__def_167(mSG3), ++__def_132(mSG3)
*** find_auto_subsumer ++__def_132(mSG3)
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_73(X2)
*** find_auto_subsumer --__def_168(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_168(field(X1,X2)), ++__def_73(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_73(field(X1,X2))
*** find_auto_subsumer --__def_167(mSG3)
*** find_auto_subsumer
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_123(X1)
*** find_auto_subsumer --__def_167(mSG3)
*** find_auto_subsumer
*** find_auto_subsumer --__def_167(mSG3), ++__def_123(mSG3)
*** find_auto_subsumer ++__def_123(mSG3)
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_48(X1)
*** find_auto_subsumer --__def_167(mSG3)
*** find_auto_subsumer
*** find_auto_subsumer --__def_167(mSG3), ++__def_48(mSG3)
*** find_auto_subsumer ++__def_48(mSG3)
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_64(X2)
*** find_auto_subsumer --__def_168(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_168(field(X1,X2)), ++__def_64(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_64(field(X1,X2))
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_49(X1)
*** find_auto_subsumer --__def_167(mSG3)
*** find_auto_subsumer
*** find_auto_subsumer --__def_167(mSG3), ++__def_49(mSG3)
*** find_auto_subsumer ++__def_49(mSG3)
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_77(X2)
*** find_auto_subsumer --__def_168(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_168(field(X1,X2)), ++__def_77(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_77(field(X1,X2))
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__type_16(X2)
*** find_auto_subsumer --__def_168(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_168(field(X1,X2)), ++__type_16(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__type_16(field(X1,X2))
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_99(X2)
*** find_auto_subsumer --__def_168(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_168(field(X1,X2)), ++__def_99(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_99(field(X1,X2))
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_205(X2)
*** find_auto_subsumer --__def_168(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_168(field(X1,X2)), ++__def_205(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_205(field(X1,X2))
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_138(X1)
*** find_auto_subsumer --__def_167(mSG3)
*** find_auto_subsumer
*** find_auto_subsumer --__def_167(mSG3), ++__def_138(mSG3)
*** find_auto_subsumer ++__def_138(mSG3)
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_153(X1)
*** find_auto_subsumer --__def_167(mSG3)
*** find_auto_subsumer
*** find_auto_subsumer --__def_167(mSG3), ++__def_153(mSG3)
*** find_auto_subsumer ++__def_153(mSG3)
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_26(X2)
*** find_auto_subsumer --__def_168(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_168(field(X1,X2)), ++__def_26(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_26(field(X1,X2))
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__type_19(X1)
*** find_auto_subsumer --__def_167(mSG3)
*** find_auto_subsumer
*** find_auto_subsumer --__def_167(mSG3), ++__type_19(mSG3)
*** find_auto_subsumer ++__type_19(mSG3)
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_90(X2)
*** find_auto_subsumer --__def_168(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_168(field(X1,X2)), ++__def_90(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_90(field(X1,X2))
*** find_auto_subsumer --__def_167(X1), --__def_168(X2), ++__def_2(X2)
*** find_auto_subsumer --__def_168(field(X1,X2))
*** find_auto_subsumer --__def_161(X1), --__def_59(X2)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_168(field(X1,X2)), ++__def_2(field(X1,X2))
 ** Testing {[{"__def_7"},{"__def_93"}],
 [{"__def_75"},{"__def_193"}],
 [{"__def_7"},{"__def_193"}],
 [{"__def_181"},{"__def_93"}],
 [{"__def_89"},{"__def_193"}],
 [{"__def_171"},{"__def_59"}],
 [{"__def_192"},{"__def_193"}],
 [{"__def_181"},{"__def_76"}],
 [{"__def_192"},{"__def_93"}],
 [{"__def_75"},{"__def_93"}],
 [{"__def_55"},{"__def_59"}],
 [{"__def_181"},{"__def_193"}],
 [{"__def_92"},{"__def_93"}],
 [{"__def_75"},{"__def_76"}],
 [{"__def_188"},{"__def_76"}],
 [{"__def_89"},{"__def_93"}],
 [{"__def_71"},{"__def_76"}],
 [{"__def_92"},{"__def_76"}],
 [{"__def_177"},{"__def_76"}],
 [{"__def_92"},{"__def_193"}],
 [{"__def_7"},{"__def_76"}],
 [{"__def_31"},{"__def_193"}],
 [{"__def_89"},{"__def_76"}],
 [{"__def_177"},{"__def_93"}],
 [{"__def_31"},{"__def_76"}],
 [{"__def_188"},{"__def_193"}],
 [{"__def_31"},{"__def_93"}],
 [{"__def_188"},{"__def_93"}],
 [{"__def_71"},{"__def_193"}],
 [{"__def_192"},{"__def_76"}],
 [{"__def_177"},{"__def_193"}],
 [{"__def_71"},{"__def_93"}]}
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_2(field(X1,X2))
 ** Testing {[{"__def_7"},{"__def_93"}],
 [{"__def_75"},{"__def_193"}],
 [{"__def_7"},{"__def_193"}],
 [{"__def_181"},{"__def_93"}],
 [{"__def_89"},{"__def_193"}],
 [{"__def_171"},{"__def_59"}],
 [{"__def_192"},{"__def_193"}],
 [{"__def_181"},{"__def_76"}],
 [{"__def_192"},{"__def_93"}],
 [{"__def_75"},{"__def_93"}],
 [{"__def_55"},{"__def_59"}],
 [{"__def_181"},{"__def_193"}],
 [{"__def_92"},{"__def_93"}],
 [{"__def_75"},{"__def_76"}],
 [{"__def_188"},{"__def_76"}],
 [{"__def_89"},{"__def_93"}],
 [{"__def_71"},{"__def_76"}],
 [{"__def_92"},{"__def_76"}],
 [{"__def_177"},{"__def_76"}],
 [{"__def_92"},{"__def_193"}],
 [{"__def_7"},{"__def_76"}],
 [{"__def_31"},{"__def_193"}],
 [{"__def_89"},{"__def_76"}],
 [{"__def_177"},{"__def_93"}],
 [{"__def_31"},{"__def_76"}],
 [{"__def_188"},{"__def_193"}],
 [{"__def_31"},{"__def_93"}],
 [{"__def_188"},{"__def_93"}],
 [{"__def_71"},{"__def_193"}],
 [{"__def_192"},{"__def_76"}],
 [{"__def_177"},{"__def_193"}],
 [{"__def_71"},{"__def_93"}]}
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_7(X1)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_161(x235), ++__def_7(x235)
*** find_auto_subsumer ++__def_7(x235)
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_75(X1)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_161(x235), ++__def_75(x235)
*** find_auto_subsumer ++__def_75(x235)
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_193(X2)
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type), ++__def_193(msg_type)
*** find_auto_subsumer ++__def_193(msg_type)
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_93(X2)
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type), ++__def_93(msg_type)
*** find_auto_subsumer ++__def_93(msg_type)
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_171(X1)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_161(x235), ++__def_171(x235)
*** find_auto_subsumer ++__def_171(x235)
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_76(X2)
*** find_auto_subsumer --__def_59(msg_type)
*** find_auto_subsumer
*** find_auto_subsumer --__def_59(msg_type), ++__def_76(msg_type)
*** find_auto_subsumer ++__def_76(msg_type)
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_192(X1)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_161(x235), ++__def_192(x235)
*** find_auto_subsumer ++__def_192(x235)
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_55(X1)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_161(x235), ++__def_55(x235)
*** find_auto_subsumer ++__def_55(x235)
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_92(X1)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_161(x235), ++__def_92(x235)
*** find_auto_subsumer ++__def_92(x235)
*** find_auto_subsumer --__def_161(X1), --__def_59(X2), ++__def_31(X1)
*** find_auto_subsumer --__def_161(x235)
*** find_auto_subsumer
*** find_auto_subsumer --__def_161(x235), ++__def_31(x235)
*** find_auto_subsumer ++__def_31(x235)
