| ?- go. Step1 .... Step2 ........ Step3 ................... Step4 ........................................................... Step5 ................................................................................................................. Step6 ................................................................................................................................................................................................... Step7 ............................................................................................................................................................... Step8 ................................................................................................................................................ Step9 ............................................................................... Step10 ....................................................................................... Step11 .................................................... Step12 ...................................... Step13 ...................... Step14 ............ Step15 .... Step16 .. Step17 -------------------------------------------------------- The fixpoint has been reached! Search for the initial configuration using :-ls. yes | ?- check(K,L). no | ?- ls. f(16, [initM(_),fresh(_),zero(_),init], {}, 999, 994, call_create). f(16, [genB(_,A,_),fresh(B),initM(_),zero(_),init], {A-B>0.0}, 998, 997, bob_generates_a_fresh_name). f(15, [initM(_),fresh(A),zero(_),init,readyB(_,B,_)], {B-A>0.0}, 997, 984, call_create). f(15, [genB(_,A,_),fresh(B),initM(_),zero(_),init,readyB(_,A,C)], {A-C>0.0,A-B>0.0}, 996, 992, bob_generates_a_fresh_name). f(15, [genB(_,A,_),fresh(B),initM(_),zero(_),init,readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 995, 992, bob_generates_a_fresh_name). f(15, [create(_),zero(_),fresh(_),init], {}, 994, 993, create_bob). f(14, [initM(_),fresh(_),zero(_),init,initB(_,_,_)], {}, 993, 960, call_create). f(14, [initM(_),fresh(A),zero(_),init,readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 992, 961, call_create). f(14, [initA(_,_,_),fresh(_),init], {}, 991, 970, alice_generates_a_fresh_name). f(14, [create(_),zero(_),fresh(_),init,create(_)], {}, 990, 971, create_alice). f(14, [initM(_),fresh(_),initA(_,_,_),init], {}, 989, 971, call_create). f(14, [stopB(_,_,_),zero(_),genA(_,_,_),fresh(A),genA(_,B,_)], {B-A>0.0}, 988, 972, bob_restarts). f(14, [genB(_,A,_),fresh(B),create(_),zero(_),init,create(_)], {A-B>0.0}, 987, 975, bob_generates_a_fresh_name). f(14, [genB(_,A,_),fresh(B),initA(_,_,_),init], {A-B>0.0}, 986, 976, bob_generates_a_fresh_name). f(14, [genB(_,A,_),fresh(B),initM(_),zero(_),initB(_,_,_),init], {A-B>0.0}, 985, 979, bob_generates_a_fresh_name). f(14, [create(_),zero(_),fresh(A),init,readyB(_,B,_)], {B-A>0.0}, 984, 979, create_bob). f(14, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),genA(_,_,_)], {A-B>0.0}, 983, 980, bob_generates_a_fresh_name). f(14, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,C,_),genA(_,A,_)], {C-B>0.0}, 982, 981, bob_generates_a_fresh_name). f(13, [stopB(_,_,_),zero(_),genA(_,A,_),fresh(B),genA(_,C,_),readyB(_,C,_)], {B-A<-0.0}, 981, 928, bob_restarts). f(13, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),genA(_,_,_),fresh(B)], {B-A<-0.0}, 980, 930, bob_restarts). f(13, [initM(_),fresh(A),zero(_),initB(_,_,_),init,readyB(_,B,_)], {B-A>0.0}, 979, 932, call_create). f(13, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,C,_),readyB(_,C,_),genA(_,A,_)], {A-B>0.0}, 978, 936, bob_generates_a_fresh_name). f(13, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,C,_),genA(_,C,_)], {C-B>0.0}, 977, 936, bob_generates_a_fresh_name). f(13, [initA(_,_,_),fresh(A),init,readyB(_,B,_)], {B-A>0.0}, 976, 937, alice_generates_a_fresh_name). f(13, [create(_),zero(_),fresh(A),init,create(_),readyB(_,B,_)], {B-A>0.0}, 975, 939, create_alice). f(13, [initM(_),fresh(A),initA(_,_,_),init,readyB(_,B,_)], {B-A>0.0}, 974, 939, call_create). f(13, [initM(_),fresh(A),zero(_),init,create(_),create(_),readyB(_,B,_)], {B-A>0.0}, 973, 941, call_create). f(13, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),genA(_,B,_)], {B-A>0.0}, 972, 946, alice_sends_nonce_Na_to_bob). f(13, [initA(_,_,_),fresh(_),init,create(_)], {}, 971, 950, alice_generates_a_fresh_name). f(13, [init,genA(_,_,_)], {}, 970, 951, initialize_system). f(13, [create(_),zero(_),initA(_,_,_),fresh(_),init], {}, 969, 952, create_bob). f(13, [create(_),zero(_),create(_),fresh(_),init,create(_)], {}, 968, 953, create_bob). f(13, [genB(_,A,_),fresh(B),create(_),zero(_),init,create(_),readyB(_,A,C)], {A-C>0.0,A-B>0.0}, 967, 956, bob_generates_a_fresh_name). f(13, [genB(_,A,_),fresh(B),create(_),zero(_),init,create(_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 966, 956, bob_generates_a_fresh_name). f(13, [genB(_,A,_),fresh(B),initA(_,_,_),init,readyB(_,A,C)], {A-C>0.0,A-B>0.0}, 965, 957, bob_generates_a_fresh_name). f(13, [genB(_,A,_),fresh(B),initA(_,_,_),init,readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 964, 957, bob_generates_a_fresh_name). f(13, [genB(_,A,_),fresh(B),initM(_),zero(_),init,readyB(_,A,C),initB(_,_,_)], {A-C>0.0,A-B>0.0}, 963, 958, bob_generates_a_fresh_name). f(13, [genB(_,A,_),fresh(B),initM(_),zero(_),init,initB(_,_,_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 962, 958, bob_generates_a_fresh_name). f(13, [create(_),zero(_),fresh(A),init,readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 961, 958, create_bob). f(13, [create(_),zero(_),fresh(_),init,initB(_,_,_)], {}, 960, 959, create_bob). f(12, [initM(_),fresh(_),zero(_),init,initB(_,_,_),initB(_,_,_)], {}, 959, 877, call_create). f(12, [initM(_),fresh(A),zero(_),init,readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 958, 882, call_create). f(12, [initA(_,_,_),fresh(A),init,readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 957, 886, alice_generates_a_fresh_name). f(12, [create(_),zero(_),fresh(A),init,create(_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 956, 889, create_alice). f(12, [initM(_),fresh(A),initA(_,_,_),init,readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 955, 889, call_create). f(12, [initM(_),fresh(A),zero(_),create(_),init,create(_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 954, 892, call_create). f(12, [create(_),zero(_),fresh(_),initB(_,_,_),init,create(_)], {}, 953, 895, create_alice). f(12, [initA(_,_,_),fresh(_),init,initB(_,_,_)], {}, 952, 896, alice_generates_a_fresh_name). f(12, [initM(_),fresh(A),zero(_),genA(_,B,_)], {B-A>0.0}, 951, 897, call_create). f(12, [init,create(_),genA(_,_,_)], {}, 950, 897, initialize_system). f(12, [initA(_,_,_),fresh(_),init,create(_),create(_)], {}, 949, 902, alice_generates_a_fresh_name). f(12, [initM(_),fresh(_),init,create(_),genA(_,_,_)], {}, 948, 902, call_create). f(12, [create(_),zero(_),fresh(_),init,create(_),initA(_,_,_)], {}, 947, 904, create_alice). f(12, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),genA(_,C,_)], {C-B>0.0}, 946, 905, bob_generates_a_fresh_name). f(12, [initA(_,_,_),fresh(_),init,initA(_,_,_)], {}, 945, 907, alice_generates_a_fresh_name). f(12, [create(_),zero(_),init,genA(_,_,_)], {}, 944, 907, create_alice). f(12, [genB(_,A,_),fresh(B),initA(_,_,_),init,initA(_,_,_)], {A-B>0.0}, 943, 909, bob_generates_a_fresh_name). f(12, [genB(_,A,_),fresh(B),initA(_,_,_),init,create(_),create(_)], {A-B>0.0}, 942, 911, bob_generates_a_fresh_name). f(12, [create(_),zero(_),fresh(A),init,create(_),create(_),readyB(_,B,_)], {B-A>0.0}, 941, 911, create_alice). f(12, [genB(_,A,_),fresh(_),init,create(_),genA(_,A,_)], {}, 940, 912, bob_generates_a_fresh_name). f(12, [initA(_,_,_),fresh(A),init,create(_),readyB(_,B,_)], {B-A>0.0}, 939, 912, alice_generates_a_fresh_name). f(12, [genB(_,A,_),fresh(B),initM(_),zero(_),genA(_,A,_)], {A-B>0.0}, 938, 913, bob_generates_a_fresh_name). f(12, [init,readyB(_,A,_),genA(_,A,_)], {}, 937, 913, initialize_system). f(12, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),readyB(_,C,_),genA(_,C,_)], {C-B>0.0}, 936, 915, bob_restarts). f(12, [genB(_,A,_),fresh(B),genB(_,C,_),waitA(_,C,_),zero(_),genA(_,A,_)], {A-B>0.0}, 935, 916, bob_generates_a_fresh_name). f(12, [genB(_,A,_),fresh(B),initA(_,_,_),initB(_,_,_),init], {A-B>0.0}, 934, 917, bob_generates_a_fresh_name). f(12, [create(_),zero(_),initA(_,_,_),fresh(A),init,readyB(_,B,_)], {B-A>0.0}, 933, 917, create_bob). f(12, [create(_),zero(_),fresh(A),initB(_,_,_),init,readyB(_,B,_)], {B-A>0.0}, 932, 917, create_alice). f(12, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),genA(_,_,_)], {A-B>0.0}, 931, 918, bob_generates_a_fresh_name). f(12, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),genA(_,_,_),fresh(B)], {B-A<-0.0}, 930, 918, alice_sends_nonce_Na_to_bob). f(12, [genB(_,A,_),fresh(B),genB(_,C,_),waitA(_,C,_),zero(_),genA(_,A,_)], {C-B>0.0}, 929, 919, bob_generates_a_fresh_name). f(12, [genA(_,A,_),initB(_,_,_),fresh(B),zero(_),genA(_,C,_),readyB(_,C,_)], {B-A<-0.0}, 928, 919, alice_sends_nonce_Na_to_bob). f(12, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,B),genA(_,_,_),fresh(C),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 927, 920, bob_restarts). f(12, [genB(_,A,_),fresh(B),genA(_,A,_),initB(_,_,_),readyB(_,A,C),zero(_),genA(_,_,_)], {A-C>0.0,A-B>0.0}, 926, 920, bob_generates_a_fresh_name). f(12, [genB(_,A,_),fresh(B),genA(_,A,_),initB(_,_,_),zero(_),genA(_,_,_),readyB(_,A,C)], {B-C<-0.0,B-A<-0.0}, 925, 920, bob_generates_a_fresh_name). f(12, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,C,_),readyB(_,C,_),readyB(_,A,D),genA(_,A,_)], {A-D>0.0,A-B>0.0}, 924, 921, bob_generates_a_fresh_name). f(12, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,C,_),readyB(_,C,_),genA(_,A,_),readyB(_,A,D)], {B-A<-0.0,B-D<-0.0}, 923, 921, bob_generates_a_fresh_name). f(12, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,C,D),genA(_,C,_),readyB(_,C,E)], {C-B>0.0,E-D>0.0}, 922, 921, bob_generates_a_fresh_name). f(11, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),readyB(_,C,D),genA(_,C,_),readyB(_,C,E)], {C-B>0.0,E-D>0.0}, 921, 799, bob_restarts). f(11, [genA(_,A,_),initB(_,_,_),readyB(_,A,B),zero(_),genA(_,_,_),fresh(C),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 920, 804, alice_sends_nonce_Na_to_bob). f(11, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),genA(_,C,_),readyB(_,C,_)], {A-B>0.0}, 919, 808, bob_generates_a_fresh_name). f(11, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,_,_),fresh(B)], {B-A<-0.0}, 918, 809, rendez_vous_over_Nb_for_alice_and_bob). f(11, [initA(_,_,_),fresh(A),initB(_,_,_),init,readyB(_,B,_)], {B-A>0.0}, 917, 810, alice_generates_a_fresh_name). f(11, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),readyB(_,C,_),genA(_,C,_)], {C-B>0.0}, 916, 813, bob_generates_a_fresh_name). f(11, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,_),genA(_,C,_)], {C-B>0.0}, 915, 813, alice_sends_nonce_Na_to_bob). f(11, [stopA(_,_,_),zero(_),fresh(A),genB(_,B,_),waitA(_,B,_),readyB(_,C,_),genA(_,C,_)], {C-A>0.0}, 914, 814, alice_restarts). f(11, [initM(_),fresh(A),zero(_),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 913, 820, call_create). f(11, [init,create(_),readyB(_,A,_),genA(_,A,_)], {}, 912, 820, initialize_system). f(11, [initA(_,_,_),fresh(A),init,create(_),create(_),readyB(_,B,_)], {B-A>0.0}, 911, 825, alice_generates_a_fresh_name). f(11, [initM(_),fresh(_),init,create(_),readyB(_,A,_),genA(_,A,_)], {}, 910, 825, call_create). f(11, [initA(_,_,_),fresh(A),init,initA(_,_,_),readyB(_,B,_)], {B-A>0.0}, 909, 830, alice_generates_a_fresh_name). f(11, [create(_),zero(_),init,readyB(_,A,_),genA(_,A,_)], {}, 908, 830, create_alice). f(11, [init,initA(_,_,_),genA(_,_,_)], {}, 907, 834, initialize_system). f(11, [initM(_),fresh(A),zero(_),stopA(_,_,_),genA(_,B,_)], {B-A>0.0}, 906, 836, call_create). f(11, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),genA(_,C,_)], {C-B>0.0}, 905, 838, rendez_vous_over_Nb_for_alice_and_bob). f(11, [initA(_,_,_),fresh(_),init,create(_),initA(_,_,_)], {}, 904, 839, alice_generates_a_fresh_name). f(11, [initM(_),fresh(_),init,initA(_,_,_),genA(_,_,_)], {}, 903, 839, call_create). f(11, [init,create(_),create(_),genA(_,_,_)], {}, 902, 840, initialize_system). f(11, [stopA(_,_,_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),genA(_,C,_)], {C-A>0.0}, 901, 841, alice_restarts). f(11, [initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_),zero(_),genA(_,C,_)], {C-A>0.0}, 900, 842, alice_generates_a_fresh_name). f(11, [create(_),zero(_),initA(_,_,_),fresh(_),init,initA(_,_,_)], {}, 899, 845, create_bob). f(11, [stopB(_,_,_),zero(_),genA(_,A,_),initM(_),fresh(B)], {B-A<-0.0}, 898, 847, bob_restarts). f(11, [create(_),zero(_),genA(_,A,_),fresh(B)], {B-A<-0.0}, 897, 847, create_bob). f(11, [init,genA(_,_,_),initB(_,_,_)], {}, 896, 847, initialize_system). f(11, [initA(_,_,_),fresh(_),initB(_,_,_),init,create(_)], {}, 895, 848, alice_generates_a_fresh_name). f(11, [create(_),zero(_),genA(_,_,_),init,create(_)], {}, 894, 848, create_bob). f(11, [initM(_),fresh(_),genA(_,_,_),initB(_,_,_),init], {}, 893, 848, call_create). f(11, [create(_),zero(_),create(_),fresh(A),init,create(_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 892, 852, create_bob). f(11, [genB(_,A,_),fresh(_),init,create(_),genA(_,A,_),readyB(_,A,_)], {}, 891, 855, bob_generates_a_fresh_name). f(11, [genB(_,A,_),fresh(B),init,create(_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 890, 855, bob_generates_a_fresh_name). f(11, [initA(_,_,_),fresh(A),init,create(_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 889, 855, alice_generates_a_fresh_name). f(11, [genB(_,A,_),fresh(B),initM(_),zero(_),genA(_,A,_),readyB(_,A,C)], {A-C>0.0,A-B>0.0}, 888, 856, bob_generates_a_fresh_name). f(11, [genB(_,A,_),fresh(B),initM(_),zero(_),genA(_,A,_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 887, 856, bob_generates_a_fresh_name). f(11, [init,genA(_,A,_),readyB(_,A,B),readyB(_,A,C)], {C-B>0.0}, 886, 856, initialize_system). f(11, [genB(_,A,_),fresh(B),initA(_,_,_),init,readyB(_,A,C),initB(_,_,_)], {A-C>0.0,A-B>0.0}, 885, 857, bob_generates_a_fresh_name). f(11, [genB(_,A,_),fresh(B),initA(_,_,_),init,initB(_,_,_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 884, 857, bob_generates_a_fresh_name). f(11, [create(_),zero(_),initA(_,_,_),fresh(A),init,readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 883, 857, create_bob). f(11, [create(_),zero(_),fresh(A),init,readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 882, 858, create_bob). f(11, [genB(_,A,_),fresh(B),initA(_,_,_),initB(_,_,_),init,create(_)], {A-B>0.0}, 881, 862, bob_generates_a_fresh_name). f(11, [create(_),zero(_),initA(_,_,_),fresh(A),readyB(_,B,_),init,create(_)], {B-A>0.0}, 880, 862, create_bob). f(11, [initM(_),fresh(A),initA(_,_,_),initB(_,_,_),readyB(_,B,_),init], {B-A>0.0}, 879, 862, call_create). f(11, [create(_),zero(_),initA(_,_,_),fresh(_),init,initB(_,_,_)], {}, 878, 863, create_bob). f(11, [create(_),zero(_),fresh(_),init,initB(_,_,_),initB(_,_,_)], {}, 877, 863, create_alice). f(11, [genA(_,A,_),initB(_,_,_),genB(_,B,_),fresh(C),waitA(_,B,_),zero(_)], {C-A<-0.0}, 876, 864, alice_sends_nonce_Na_to_bob). f(11, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),stopB(_,_,_),fresh(C)], {C-B<-0.0}, 875, 865, rendez_vous_over_Nb_for_alice_and_bob). f(11, [genB(_,A,_),fresh(B),create(_),zero(_),init,initB(_,_,_),initB(_,_,_)], {A-B>0.0}, 874, 866, bob_generates_a_fresh_name). f(11, [create(_),zero(_),create(_),fresh(A),init,readyB(_,B,_),initB(_,_,_)], {B-A>0.0}, 873, 866, create_bob). f(11, [initM(_),fresh(A),zero(_),init,initB(_,_,_),readyB(_,B,_),initB(_,_,_)], {B-A>0.0}, 872, 866, call_create). f(11, [stopB(_,_,_),zero(_),genB(_,A,_),fresh(B),waitA(_,A,_),genA(_,C,_),readyB(_,C,_)], {C-B>0.0}, 871, 867, bob_restarts). f(11, [genB(_,A,_),fresh(B),genB(_,C,_),waitA(_,C,_),zero(_),genA(_,A,_),initB(_,_,_)], {A-B>0.0}, 870, 867, bob_generates_a_fresh_name). f(10, [stopB(_,_,_),zero(_),genA(_,_,_),fresh(A),stopB(_,B,_)], {B-A>0.0}, 869, 705, bob_restarts). f(10, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),stopB(_,C,_)], {C-B>0.0}, 868, 707, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),genA(_,C,_),readyB(_,C,_),initB(_,_,_)], {C-B>0.0}, 867, 711, bob_generates_a_fresh_name). f(10, [create(_),zero(_),fresh(A),init,initB(_,_,_),readyB(_,B,_),initB(_,_,_)], {B-A>0.0}, 866, 714, create_alice). f(10, [stopB(_,_,_),zero(_),genA(_,A,_),stopB(_,_,_),fresh(B)], {B-A<-0.0}, 865, 716, bob_restarts). f(10, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),genB(_,C,_),waitA(_,C,_)], {C-B>0.0}, 864, 717, bob_generates_a_fresh_name). f(10, [initA(_,_,_),fresh(_),init,initB(_,_,_),initB(_,_,_)], {}, 863, 718, alice_generates_a_fresh_name). f(10, [initA(_,_,_),fresh(A),initB(_,_,_),readyB(_,B,_),init,create(_)], {B-A>0.0}, 862, 722, alice_generates_a_fresh_name). f(10, [create(_),zero(_),fresh(_),initB(_,_,_),init,initA(_,_,_),initB(_,_,_)], {}, 861, 725, create_alice). f(10, [genB(_,A,_),fresh(B),create(_),zero(_),init,initB(_,_,_),readyB(_,A,C),initB(_,_,_)], {A-C>0.0,A-B>0.0}, 860, 726, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),create(_),zero(_),init,initB(_,_,_),initB(_,_,_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 859, 726, bob_generates_a_fresh_name). f(10, [initM(_),fresh(A),zero(_),init,initB(_,_,_),readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 858, 726, call_create). f(10, [initA(_,_,_),fresh(A),init,readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 857, 728, alice_generates_a_fresh_name). f(10, [initM(_),fresh(A),zero(_),genA(_,B,_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 856, 729, call_create). f(10, [init,create(_),genA(_,A,_),readyB(_,A,B),readyB(_,A,C)], {C-B>0.0}, 855, 729, initialize_system). f(10, [genB(_,A,_),fresh(B),initA(_,_,_),init,create(_),readyB(_,A,C),initB(_,_,_)], {A-C>0.0,A-B>0.0}, 854, 734, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),initA(_,_,_),init,create(_),initB(_,_,_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 853, 734, bob_generates_a_fresh_name). f(10, [create(_),zero(_),fresh(A),init,create(_),readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 852, 734, create_alice). f(10, [initM(_),fresh(A),initA(_,_,_),init,readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 851, 734, call_create). f(10, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,_,_),stopB(_,A,C)], {A-C>0.0,A-B>0.0}, 850, 737, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,_,_),stopB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 849, 745, bob_generates_a_fresh_name). f(10, [genA(_,_,_),initB(_,_,_),init,create(_)], {}, 848, 746, alice_sends_nonce_Na_to_bob). f(10, [genA(_,A,_),initB(_,_,_),initM(_),fresh(B),zero(_)], {B-A<-0.0}, 847, 747, alice_sends_nonce_Na_to_bob). f(10, [init,genB(_,A,_),waitA(_,A,_)], {}, 846, 747, initialize_system). f(10, [initA(_,_,_),fresh(_),initB(_,_,_),init,initA(_,_,_)], {}, 845, 748, alice_generates_a_fresh_name). f(10, [create(_),zero(_),genA(_,_,_),initB(_,_,_),init], {}, 844, 748, create_alice). f(10, [create(_),zero(_),fresh(A),stopB(_,_,_),genA(_,B,_)], {B-A>0.0}, 843, 750, create_alice). f(10, [genB(_,A,_),fresh(_),waitA(_,A,_),zero(_),genA(_,B,_),genA(_,B,_)], {}, 842, 751, bob_generates_a_fresh_name). f(10, [initA(_,_,_),fresh(A),waitA(_,B,_),readyB(_,B,_),zero(_),genA(_,C,_)], {C-A>0.0}, 841, 751, alice_generates_a_fresh_name). f(10, [create(_),zero(_),create(_),fresh(A),genA(_,B,_)], {B-A>0.0}, 840, 752, create_alice). f(10, [init,create(_),initA(_,_,_),genA(_,_,_)], {}, 839, 752, initialize_system). f(10, [stopB(_,_,_),zero(_),stopA(_,_,_),fresh(A),genA(_,B,_)], {B-A>0.0}, 838, 753, bob_restarts). f(10, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),genA(_,C,_)], {C-B>0.0}, 837, 753, rendez_vous_over_Nb_for_alice_and_bob). f(10, [create(_),zero(_),stopA(_,_,_),fresh(A),genA(_,B,_)], {B-A>0.0}, 836, 753, create_bob). f(10, [initA(_,_,_),fresh(A),init,create(_),genA(_,B,_)], {B-A>0.0}, 835, 754, alice_generates_a_fresh_name). f(10, [initA(_,_,_),fresh(A),initM(_),zero(_),genA(_,B,_)], {B-A>0.0}, 834, 755, alice_generates_a_fresh_name). f(10, [init,genA(_,A,_),genA(_,A,_)], {}, 833, 755, initialize_system). f(10, [genB(_,A,_),fresh(_),init,genA(_,A,_),genA(_,A,_)], {}, 832, 756, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),initA(_,_,_),initM(_),zero(_),genA(_,A,_)], {A-B>0.0}, 831, 757, bob_generates_a_fresh_name). f(10, [init,initA(_,_,_),readyB(_,A,_),genA(_,A,_)], {}, 830, 757, initialize_system). f(10, [genB(_,A,_),fresh(_),init,create(_),initA(_,_,_),genA(_,A,_)], {}, 829, 759, bob_generates_a_fresh_name). f(10, [initA(_,_,_),fresh(A),init,create(_),initA(_,_,_),readyB(_,B,_)], {B-A>0.0}, 828, 759, alice_generates_a_fresh_name). f(10, [initM(_),fresh(_),init,initA(_,_,_),readyB(_,A,_),genA(_,A,_)], {}, 827, 759, call_create). f(10, [genB(_,A,_),fresh(B),create(_),zero(_),create(_),genA(_,A,_)], {A-B>0.0}, 826, 760, bob_generates_a_fresh_name). f(10, [init,create(_),create(_),readyB(_,A,_),genA(_,A,_)], {}, 825, 760, initialize_system). f(10, [genB(_,A,_),fresh(B),stopA(_,_,_),zero(_),create(_),genA(_,A,_)], {A-B>0.0}, 824, 761, bob_generates_a_fresh_name). f(10, [initM(_),fresh(A),stopA(_,_,_),zero(_),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 823, 761, call_create). f(10, [stopB(_,_,_),zero(_),initM(_),fresh(A),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 822, 762, bob_restarts). f(10, [genB(_,A,_),fresh(B),initM(_),zero(_),initB(_,_,_),genA(_,A,_)], {A-B>0.0}, 821, 762, bob_generates_a_fresh_name). f(10, [create(_),zero(_),fresh(A),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 820, 762, create_bob). f(10, [genB(_,A,_),fresh(B),initA(_,_,_),init,initA(_,_,_),initB(_,_,_)], {A-B>0.0}, 819, 763, bob_generates_a_fresh_name). f(10, [create(_),zero(_),initA(_,_,_),fresh(A),init,initA(_,_,_),readyB(_,B,_)], {B-A>0.0}, 818, 763, create_bob). f(10, [create(_),zero(_),fresh(A),init,initA(_,_,_),initB(_,_,_),readyB(_,B,_)], {B-A>0.0}, 817, 763, create_alice). f(10, [genB(_,A,_),fresh(B),initA(_,_,_),waitA(_,C,_),readyB(_,C,_),zero(_),genA(_,A,_)], {A-B>0.0}, 816, 764, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(_),genB(_,B,_),waitA(_,B,_),zero(_),genA(_,A,_),genA(_,A,_)], {}, 815, 765, bob_generates_a_fresh_name). f(10, [initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_),zero(_),readyB(_,C,_),genA(_,C,_)], {C-A>0.0}, 814, 765, alice_generates_a_fresh_name). f(10, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,_),genA(_,C,_)], {C-B>0.0}, 813, 766, rendez_vous_over_Nb_for_alice_and_bob). f(10, [genB(_,A,_),fresh(B),stopA(_,_,_),zero(_),stopB(_,_,_),genA(_,A,_)], {A-B>0.0}, 812, 766, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(_),init,waitA(_,A,_)], {}, 811, 768, bob_generates_a_fresh_name). f(10, [genA(_,A,_),initB(_,_,_),init,readyB(_,A,_)], {}, 810, 768, alice_sends_nonce_Na_to_bob). f(10, [stopB(_,_,_),zero(_),genA(_,_,_),fresh(A),stopA(_,B,_)], {B-A>0.0}, 809, 770, bob_restarts). f(10, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),readyB(_,B,_),fresh(C)], {C-A<-0.0}, 808, 771, rendez_vous_over_Nb_for_alice_and_bob). f(10, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),stopA(_,C,_)], {C-B>0.0}, 807, 771, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),genB(_,C,_),waitA(_,C,_),genA(_,A,_),initB(_,_,_),readyB(_,A,D),zero(_)], {A-D>0.0,A-B>0.0}, 806, 772, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),genB(_,C,_),waitA(_,C,_),genA(_,A,_),initB(_,_,_),zero(_),readyB(_,A,D)], {B-A<-0.0,B-D<-0.0}, 805, 772, bob_generates_a_fresh_name). f(10, [waitA(_,A,_),readyB(_,A,B),zero(_),genA(_,_,_),fresh(C),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 804, 774, rendez_vous_over_Nb_for_alice_and_bob). f(10, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,_,_),stopA(_,A,C)], {A-C>0.0,A-B>0.0}, 803, 774, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),waitA(_,C,_),readyB(_,C,_),zero(_),readyB(_,A,D),genA(_,A,_)], {A-D>0.0,A-B>0.0}, 802, 775, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),waitA(_,C,_),readyB(_,C,_),zero(_),genA(_,A,_),readyB(_,A,D)], {B-A<-0.0,B-D<-0.0}, 801, 775, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),readyB(_,C,D),genA(_,C,_),readyB(_,C,E)], {C-B>0.0,E-D>0.0}, 800, 775, bob_generates_a_fresh_name). f(10, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,D),genA(_,C,_),readyB(_,C,E)], {C-B>0.0,E-D>0.0}, 799, 775, alice_sends_nonce_Na_to_bob). f(10, [stopA(_,_,_),zero(_),fresh(A),genB(_,B,_),waitA(_,B,_),readyB(_,C,D),genA(_,C,_),readyB(_,C,E)], {C-A>0.0,E-D>0.0}, 798, 776, alice_restarts). f(10, [genB(_,A,_),fresh(B),initA(_,_,_),genB(_,C,_),waitA(_,C,_),zero(_),readyB(_,A,D),genA(_,A,_)], {A-D>0.0,A-B>0.0}, 797, 776, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),initA(_,_,_),genB(_,C,_),waitA(_,C,_),zero(_),genA(_,A,_),readyB(_,A,D)], {B-A<-0.0,B-D<-0.0}, 796, 776, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),initM(_),stopA(_,_,_),zero(_),readyB(_,A,C),genA(_,A,_)], {A-C>0.0,A-B>0.0}, 795, 778, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),initM(_),stopA(_,_,_),zero(_),genA(_,A,_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 794, 778, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(_),init,create(_),create(_),readyB(_,A,_),genA(_,A,_)], {}, 793, 779, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),init,create(_),create(_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 792, 779, bob_generates_a_fresh_name). f(10, [initA(_,_,_),fresh(A),init,create(_),create(_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 791, 779, alice_generates_a_fresh_name). f(10, [initM(_),fresh(_),init,create(_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 790, 779, call_create). f(10, [genB(_,A,_),fresh(B),initA(_,_,_),init,create(_),initA(_,_,_),readyB(_,A,C)], {A-C>0.0,A-B>0.0}, 789, 781, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),initA(_,_,_),init,create(_),initA(_,_,_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 788, 781, bob_generates_a_fresh_name). f(10, [create(_),zero(_),fresh(A),init,create(_),initA(_,_,_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 787, 781, create_alice). f(10, [genB(_,A,_),fresh(_),init,initA(_,_,_),readyB(_,A,_),genA(_,A,_)], {}, 786, 782, bob_generates_a_fresh_name). f(10, [genB(_,A,_),fresh(B),init,initA(_,_,_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 785, 782, bob_generates_a_fresh_name). f(10, [initA(_,_,_),fresh(A),init,initA(_,_,_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 784, 782, alice_generates_a_fresh_name). f(10, [create(_),zero(_),init,readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 783, 782, create_alice). f(9, [init,initA(_,_,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 782, 561, initialize_system). f(9, [initA(_,_,_),fresh(A),init,create(_),initA(_,_,_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 781, 567, alice_generates_a_fresh_name). f(9, [initM(_),fresh(_),init,initA(_,_,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 780, 567, call_create). f(9, [init,create(_),create(_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 779, 568, initialize_system). f(9, [initM(_),fresh(A),stopA(_,_,_),zero(_),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 778, 571, call_create). f(9, [create(_),zero(_),initA(_,_,_),fresh(A),init,initA(_,_,_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 777, 573, create_bob). f(9, [initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_),zero(_),readyB(_,C,D),genA(_,C,_),readyB(_,C,E)], {C-A>0.0,E-D>0.0}, 776, 577, alice_generates_a_fresh_name). f(9, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,D),genA(_,C,_),readyB(_,C,E)], {C-B>0.0,E-D>0.0}, 775, 583, rendez_vous_over_Nb_for_alice_and_bob). f(9, [stopB(_,_,_),zero(_),genA(_,_,_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 774, 591, bob_restarts). f(9, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-B>0.0}, 773, 595, bob_generates_a_fresh_name). f(9, [genB(_,A,_),fresh(B),waitA(_,A,_),genA(_,C,_),initB(_,_,_),readyB(_,C,D),zero(_),readyB(_,C,E)], {C-B>0.0,E-D>0.0}, 772, 599, bob_generates_a_fresh_name). f(9, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),stopA(_,C,_)], {C-B>0.0}, 771, 610, bob_restarts). f(9, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),stopA(_,B,_)], {B-A>0.0}, 770, 611, alice_sends_nonce_Na_to_bob). f(9, [init,stopA(_,_,_)], {}, 769, 616, initialize_system). f(9, [init,waitA(_,A,_),readyB(_,A,_)], {}, 768, 619, initialize_system). f(9, [init,genB(_,A,_),stopA(_,_,_),waitA(_,A,_)], {}, 767, 625, initialize_system). f(9, [stopA(_,_,_),zero(_),fresh(A),stopB(_,_,_),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 766, 627, alice_restarts). f(9, [genB(_,A,_),fresh(_),waitA(_,A,_),zero(_),genA(_,B,_),readyB(_,B,_),genA(_,B,_)], {}, 765, 629, bob_generates_a_fresh_name). f(9, [initA(_,_,_),fresh(A),waitA(_,B,_),readyB(_,B,_),zero(_),readyB(_,C,_),genA(_,C,_)], {C-A>0.0}, 764, 629, alice_generates_a_fresh_name). f(9, [initA(_,_,_),fresh(A),init,initA(_,_,_),initB(_,_,_),readyB(_,B,_)], {B-A>0.0}, 763, 630, alice_generates_a_fresh_name). f(9, [initM(_),fresh(A),zero(_),initB(_,_,_),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 762, 631, call_create). f(9, [stopA(_,_,_),zero(_),create(_),fresh(A),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 761, 632, alice_restarts). f(9, [create(_),zero(_),create(_),fresh(A),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 760, 632, create_alice). f(9, [init,create(_),initA(_,_,_),readyB(_,A,_),genA(_,A,_)], {}, 759, 632, initialize_system). f(9, [initA(_,_,_),fresh(A),init,create(_),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 758, 634, alice_generates_a_fresh_name). f(9, [initA(_,_,_),fresh(A),initM(_),zero(_),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 757, 635, alice_generates_a_fresh_name). f(9, [init,genA(_,A,_),readyB(_,A,_),genA(_,A,_)], {}, 756, 635, initialize_system). f(9, [initM(_),fresh(_),zero(_),genA(_,A,_),genA(_,A,_)], {}, 755, 639, call_create). f(9, [init,create(_),genA(_,A,_),genA(_,A,_)], {}, 754, 639, initialize_system). f(9, [stopA(_,_,_),zero(_),fresh(A),initB(_,_,_),genA(_,B,_)], {B-A>0.0}, 753, 640, alice_restarts). f(9, [create(_),zero(_),initA(_,_,_),fresh(A),genA(_,B,_)], {B-A>0.0}, 752, 640, create_bob). f(9, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),fresh(_),genA(_,B,_)], {}, 751, 641, rendez_vous_over_Nb_for_alice_and_bob). f(9, [initA(_,_,_),fresh(A),stopB(_,_,_),zero(_),genA(_,B,_)], {B-A>0.0}, 750, 641, alice_generates_a_fresh_name). f(9, [stopA(_,_,_),zero(_),init,genB(_,A,_),waitA(_,A,_)], {}, 749, 642, alice_restarts). f(9, [genA(_,_,_),initB(_,_,_),init,initA(_,_,_)], {}, 748, 642, alice_sends_nonce_Na_to_bob). f(9, [initM(_),fresh(A),zero(_),genB(_,B,_),waitA(_,B,_)], {B-A>0.0}, 747, 643, call_create). f(9, [init,create(_),genB(_,A,_),waitA(_,A,_)], {}, 746, 643, initialize_system). f(9, [stopB(_,_,_),zero(_),genA(_,_,_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 745, 649, bob_restarts). f(9, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,C,D),stopB(_,C,E)], {C-B>0.0,E-D>0.0}, 744, 652, bob_generates_a_fresh_name). f(9, [genB(_,A,_),fresh(B),init,stopA(_,A,C)], {C-B>0.0}, 743, 655, bob_generates_a_fresh_name). f(9, [stopB(_,_,_),zero(_),genA(_,_,_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 742, 656, bob_restarts). f(9, [genB(_,A,_),fresh(B),genA(_,_,_),initB(_,_,_),zero(_),stopA(_,A,C)], {B-A<-0.0,B-C<-0.0}, 741, 656, bob_generates_a_fresh_name). f(9, [waitA(_,A,_),readyB(_,A,B),zero(_),genA(_,C,_),readyB(_,C,_),fresh(D),readyB(_,A,E)], {E-B<-0.0,A-D>0.0}, 740, 657, rendez_vous_over_Nb_for_alice_and_bob). f(9, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,C,_),readyB(_,C,_),stopA(_,A,D)], {B-A<-0.0,B-D<-0.0}, 739, 657, bob_generates_a_fresh_name). f(9, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,C,D),stopA(_,C,E)], {C-B>0.0,E-D>0.0}, 738, 657, bob_generates_a_fresh_name). f(9, [stopB(_,_,_),zero(_),genA(_,_,_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 737, 665, bob_restarts). f(9, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-B>0.0}, 736, 668, bob_generates_a_fresh_name). f(9, [waitA(_,A,_),readyB(_,A,_),zero(_),stopB(_,_,_),genA(_,B,_),readyB(_,B,C),fresh(D),readyB(_,B,E)], {E-C>0.0,B-D>0.0}, 735, 673, rendez_vous_over_Nb_for_alice_and_bob). f(9, [initA(_,_,_),fresh(A),init,create(_),readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 734, 674, alice_generates_a_fresh_name). f(9, [create(_),zero(_),init,create(_),genA(_,A,_),readyB(_,A,B),readyB(_,A,C)], {C-B>0.0}, 733, 674, create_bob). f(9, [stopB(_,_,_),zero(_),initM(_),fresh(A),genA(_,B,_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 732, 675, bob_restarts). f(9, [genB(_,A,_),fresh(B),initM(_),zero(_),genA(_,A,_),readyB(_,A,C),initB(_,_,_)], {A-C>0.0,A-B>0.0}, 731, 675, bob_generates_a_fresh_name). f(9, [genB(_,A,_),fresh(B),initM(_),zero(_),genA(_,A,_),initB(_,_,_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 730, 675, bob_generates_a_fresh_name). f(9, [create(_),zero(_),fresh(A),genA(_,B,_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 729, 675, create_bob). f(9, [init,genA(_,A,_),readyB(_,A,B),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 728, 675, initialize_system). f(9, [create(_),zero(_),initA(_,_,_),fresh(A),init,readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 727, 676, create_bob). f(9, [create(_),zero(_),fresh(A),init,initB(_,_,_),readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 726, 676, create_alice). f(9, [initA(_,_,_),fresh(_),initB(_,_,_),init,initA(_,_,_),initB(_,_,_)], {}, 725, 682, alice_generates_a_fresh_name). f(9, [create(_),zero(_),genA(_,_,_),init,initA(_,_,_),initB(_,_,_)], {}, 724, 682, create_bob). f(9, [genB(_,A,_),fresh(_),waitA(_,A,_),init,create(_)], {}, 723, 686, bob_generates_a_fresh_name). f(9, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),init,create(_)], {}, 722, 686, alice_sends_nonce_Na_to_bob). f(9, [initM(_),fresh(_),waitA(_,A,_),readyB(_,A,_),init], {}, 721, 686, call_create). f(9, [create(_),zero(_),init,genB(_,A,_),waitA(_,A,_)], {}, 720, 687, create_bob). f(9, [create(_),zero(_),genA(_,A,_),fresh(B),initB(_,_,_)], {B-A<-0.0}, 719, 688, create_bob). f(9, [init,genA(_,_,_),initB(_,_,_),initB(_,_,_)], {}, 718, 688, initialize_system). f(9, [waitA(_,A,_),readyB(_,A,_),zero(_),genB(_,B,_),fresh(C),waitA(_,B,_)], {B-C>0.0}, 717, 689, rendez_vous_over_Nb_for_alice_and_bob). f(9, [genA(_,A,_),initB(_,_,_),stopB(_,_,_),zero(_),fresh(B)], {B-A<-0.0}, 716, 689, alice_sends_nonce_Na_to_bob). f(9, [genB(_,A,_),fresh(_),init,genA(_,A,_),initB(_,_,_),initB(_,_,_)], {}, 715, 690, bob_generates_a_fresh_name). f(9, [initA(_,_,_),fresh(A),init,initB(_,_,_),readyB(_,B,_),initB(_,_,_)], {B-A>0.0}, 714, 690, alice_generates_a_fresh_name). f(9, [create(_),zero(_),init,genA(_,A,_),readyB(_,A,_),initB(_,_,_)], {}, 713, 690, create_bob). f(9, [stopB(_,_,_),zero(_),stopB(_,_,_),genA(_,A,_),readyB(_,A,_),fresh(B)], {B-A<-0.0}, 712, 691, bob_restarts). f(9, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),readyB(_,B,_),fresh(C),initB(_,_,_)], {C-B<-0.0}, 711, 691, rendez_vous_over_Nb_for_alice_and_bob). f(9, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),initB(_,_,_)], {A-B>0.0}, 710, 691, bob_generates_a_fresh_name). f(9, [create(_),zero(_),stopB(_,_,_),genA(_,A,_),readyB(_,A,_),fresh(B)], {B-A<-0.0}, 709, 691, create_bob). f(9, [waitA(_,A,_),readyB(_,A,_),init,waitA(_,B,_),readyB(_,B,_)], {}, 708, 696, rendez_vous_over_Nb_for_alice_and_bob). f(9, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),stopB(_,C,_)], {C-B>0.0}, 707, 697, bob_restarts). f(9, [waitA(_,A,_),readyB(_,A,_),genB(_,B,_),fresh(C),waitA(_,B,_),zero(_)], {C-A<-0.0}, 706, 698, rendez_vous_over_Nb_for_alice_and_bob). f(9, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),stopB(_,B,_)], {B-A>0.0}, 705, 698, alice_sends_nonce_Na_to_bob). f(9, [init,stopB(_,_,_)], {}, 704, 701, initialize_system). f(8, [init,stopB(_,_,_),stopB(_,_,_)], {}, 703, 408, initialize_system). f(8, [stopB(_,_,_),zero(_),init,stopB(_,_,_)], {}, 702, 410, bob_restarts). f(8, [initM(_),fresh(A),zero(_),stopB(_,B,_)], {B-A>0.0}, 701, 411, call_create). f(8, [init,create(_),stopB(_,_,_)], {}, 700, 411, initialize_system). f(8, [initM(_),fresh(_),init,create(_),stopB(_,_,_)], {}, 699, 414, call_create). f(8, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),stopB(_,C,_)], {C-B>0.0}, 698, 420, bob_generates_a_fresh_name). f(8, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),stopB(_,C,_)], {C-B>0.0}, 697, 420, alice_sends_nonce_Na_to_bob). f(8, [init,waitA(_,A,_),readyB(_,A,_),stopB(_,_,_)], {}, 696, 421, initialize_system). f(8, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),initB(_,_,_),stopB(_,C,_)], {C-B>0.0}, 695, 422, bob_restarts). f(8, [stopB(_,_,_),zero(_),genB(_,A,_),fresh(B),waitA(_,A,_),stopB(_,C,_)], {C-B>0.0}, 694, 423, bob_restarts). f(8, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),initB(_,_,_),stopB(_,B,_)], {B-A>0.0}, 693, 423, alice_sends_nonce_Na_to_bob). f(8, [stopB(_,_,_),zero(_),init,waitA(_,A,_),readyB(_,A,_)], {}, 692, 424, bob_restarts). f(8, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),initB(_,_,_)], {B-A<-0.0}, 691, 426, bob_restarts). f(8, [init,genA(_,A,_),initB(_,_,_),readyB(_,A,_),initB(_,_,_)], {}, 690, 426, initialize_system). f(8, [stopB(_,_,_),zero(_),genB(_,A,_),fresh(B),waitA(_,A,_)], {A-B>0.0}, 689, 427, bob_restarts). f(8, [genA(_,A,_),initB(_,_,_),fresh(B),zero(_),initB(_,_,_)], {B-A<-0.0}, 688, 427, alice_sends_nonce_Na_to_bob). f(8, [init,genB(_,A,_),waitA(_,A,_),initB(_,_,_)], {}, 687, 427, initialize_system). f(8, [waitA(_,A,_),readyB(_,A,_),init,create(_)], {}, 686, 428, rendez_vous_over_Nb_for_alice_and_bob). f(8, [create(_),zero(_),init,stopB(_,_,_)], {}, 685, 430, create_alice). f(8, [stopA(_,_,_),zero(_),fresh(A),initB(_,_,_),genA(_,B,_),initB(_,_,_)], {B-A>0.0}, 684, 433, alice_restarts). f(8, [create(_),zero(_),fresh(A),initB(_,_,_),genA(_,B,_),initB(_,_,_)], {B-A>0.0}, 683, 433, create_alice). f(8, [genA(_,_,_),initB(_,_,_),init,initA(_,_,_),initB(_,_,_)], {}, 682, 435, alice_sends_nonce_Na_to_bob). f(8, [create(_),zero(_),init,initB(_,_,_),genB(_,A,_),waitA(_,A,_)], {}, 681, 435, create_alice). f(8, [genB(_,A,_),fresh(_),waitA(_,A,_),readyB(_,A,_),init,create(_)], {}, 680, 444, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),waitA(_,A,_),init,create(_),readyB(_,A,C)], {C-B>0.0}, 679, 444, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(_),init,genA(_,A,_),initB(_,_,_),readyB(_,A,_),initB(_,_,_)], {}, 678, 446, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),init,genA(_,A,_),initB(_,_,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 677, 446, bob_generates_a_fresh_name). f(8, [initA(_,_,_),fresh(A),init,initB(_,_,_),readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 676, 446, alice_generates_a_fresh_name). f(8, [initM(_),fresh(A),zero(_),genA(_,B,_),readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 675, 447, call_create). f(8, [init,create(_),genA(_,A,_),readyB(_,A,B),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 674, 447, initialize_system). f(8, [stopB(_,_,_),zero(_),stopB(_,_,_),genA(_,A,_),readyB(_,A,B),fresh(C),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 673, 448, bob_restarts). f(8, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,C),initB(_,_,_)], {A-C>0.0,A-B>0.0}, 672, 448, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),initB(_,_,_),readyB(_,A,C)], {B-C<-0.0,B-A<-0.0}, 671, 448, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),genA(_,_,_),initB(_,_,_),zero(_),initB(_,_,_),stopB(_,A,C)], {A-C>0.0,A-B>0.0}, 670, 449, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(_),init,waitA(_,B,_),readyB(_,B,_),stopB(_,A,_)], {}, 669, 452, bob_generates_a_fresh_name). f(8, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-B>0.0}, 668, 453, bob_restarts). f(8, [genB(_,A,_),fresh(B),genA(_,C,_),initB(_,_,_),readyB(_,C,_),zero(_),stopB(_,A,D)], {A-D>0.0,A-B>0.0}, 667, 453, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),genB(_,C,_),waitA(_,C,_),zero(_),stopB(_,A,D)], {A-D>0.0,A-B>0.0}, 666, 454, bob_generates_a_fresh_name). f(8, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 665, 454, alice_sends_nonce_Na_to_bob). f(8, [genB(_,A,_),fresh(_),waitA(_,A,_),readyB(_,A,_),init,stopB(_,_,_)], {}, 664, 456, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),waitA(_,A,_),init,stopB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 663, 456, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(_),init,create(_),stopB(_,A,_)], {}, 662, 458, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),initM(_),zero(_),stopB(_,A,C)], {A-C>0.0,A-B>0.0}, 661, 459, bob_generates_a_fresh_name). f(8, [init,readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 660, 459, initialize_system). f(8, [genB(_,A,_),fresh(_),init,stopB(_,_,_),stopB(_,A,_)], {}, 659, 461, bob_generates_a_fresh_name). f(8, [create(_),zero(_),fresh(A),init,initA(_,_,_),initB(_,_,_),readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 658, 463, create_alice). f(8, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),readyB(_,C,D),stopA(_,C,E)], {C-B>0.0,E-D>0.0}, 657, 479, bob_restarts). f(8, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 656, 480, alice_sends_nonce_Na_to_bob). f(8, [init,readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 655, 487, initialize_system). f(8, [genB(_,A,_),fresh(B),genA(_,_,_),initB(_,_,_),zero(_),initB(_,_,_),stopB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 654, 498, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),init,waitA(_,C,_),readyB(_,C,_),stopB(_,A,D)], {D-B>0.0}, 653, 501, bob_generates_a_fresh_name). f(8, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),readyB(_,C,D),stopB(_,C,E)], {C-B>0.0,E-D>0.0}, 652, 502, bob_restarts). f(8, [genB(_,A,_),fresh(B),genA(_,C,_),initB(_,_,_),readyB(_,C,_),zero(_),stopB(_,A,D)], {B-A<-0.0,B-D<-0.0}, 651, 502, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),genB(_,C,_),waitA(_,C,_),zero(_),stopB(_,A,D)], {B-A<-0.0,B-D<-0.0}, 650, 503, bob_generates_a_fresh_name). f(8, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 649, 503, alice_sends_nonce_Na_to_bob). f(8, [genB(_,A,_),fresh(B),init,create(_),stopB(_,A,C)], {C-B>0.0}, 648, 505, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),initM(_),zero(_),stopB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 647, 506, bob_generates_a_fresh_name). f(8, [init,readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 646, 506, initialize_system). f(8, [genB(_,A,_),fresh(B),init,stopB(_,_,_),stopB(_,A,C)], {C-B>0.0}, 645, 508, bob_generates_a_fresh_name). f(8, [create(_),zero(_),waitA(_,A,_),readyB(_,A,_),init], {}, 644, 509, create_alice). f(8, [create(_),zero(_),fresh(A),genB(_,B,_),waitA(_,B,_)], {B-A>0.0}, 643, 512, create_alice). f(8, [init,initA(_,_,_),genB(_,A,_),waitA(_,A,_)], {}, 642, 512, initialize_system). f(8, [stopB(_,_,_),zero(_),genA(_,A,_),fresh(_),genA(_,A,_)], {}, 641, 513, bob_restarts). f(8, [initA(_,_,_),fresh(A),initB(_,_,_),zero(_),genA(_,B,_)], {B-A>0.0}, 640, 513, alice_generates_a_fresh_name). f(8, [create(_),zero(_),genA(_,A,_),fresh(_),genA(_,A,_)], {}, 639, 513, create_bob). f(8, [init,genA(_,A,_),initB(_,_,_),genA(_,A,_)], {}, 638, 513, initialize_system). f(8, [genB(_,A,_),fresh(_),init,genA(_,A,_),initB(_,_,_),genA(_,A,_)], {}, 637, 514, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(_),create(_),zero(_),genA(_,A,_),genA(_,A,_)], {}, 636, 515, bob_generates_a_fresh_name). f(8, [initM(_),fresh(_),zero(_),genA(_,A,_),readyB(_,A,_),genA(_,A,_)], {}, 635, 515, call_create). f(8, [init,create(_),genA(_,A,_),readyB(_,A,_),genA(_,A,_)], {}, 634, 515, initialize_system). f(8, [genB(_,A,_),fresh(B),initA(_,_,_),initB(_,_,_),zero(_),genA(_,A,_)], {A-B>0.0}, 633, 516, bob_generates_a_fresh_name). f(8, [create(_),zero(_),initA(_,_,_),fresh(A),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 632, 516, create_bob). f(8, [create(_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 631, 516, create_alice). f(8, [init,initA(_,_,_),initB(_,_,_),readyB(_,A,_),genA(_,A,_)], {}, 630, 516, initialize_system). f(8, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),readyB(_,B,_),genA(_,B,_),fresh(_)], {}, 629, 517, rendez_vous_over_Nb_for_alice_and_bob). f(8, [genB(_,A,_),fresh(_),stopB(_,_,_),zero(_),genA(_,A,_),genA(_,A,_)], {}, 628, 517, bob_generates_a_fresh_name). f(8, [initA(_,_,_),fresh(A),stopB(_,_,_),zero(_),readyB(_,B,_),genA(_,B,_)], {B-A>0.0}, 627, 517, alice_generates_a_fresh_name). f(8, [init,stopB(_,_,_),genA(_,A,_),readyB(_,A,_),genA(_,A,_)], {}, 626, 517, initialize_system). f(8, [genB(_,A,_),fresh(B),stopA(_,_,_),zero(_),waitA(_,A,_)], {A-B>0.0}, 625, 518, bob_generates_a_fresh_name). f(8, [genA(_,A,_),initB(_,_,_),stopA(_,_,_),zero(_),fresh(B),readyB(_,A,_)], {A-B>0.0}, 624, 518, alice_sends_nonce_Na_to_bob). f(8, [genB(_,A,_),fresh(_),init,initA(_,_,_),initB(_,_,_),genA(_,A,_),initB(_,_,_)], {}, 623, 522, bob_generates_a_fresh_name). f(8, [initA(_,_,_),fresh(A),init,initA(_,_,_),initB(_,_,_),readyB(_,B,_),initB(_,_,_)], {B-A>0.0}, 622, 522, alice_generates_a_fresh_name). f(8, [create(_),zero(_),init,initA(_,_,_),readyB(_,A,_),genA(_,A,_),initB(_,_,_)], {}, 621, 522, create_bob). f(8, [create(_),zero(_),init,initB(_,_,_),readyB(_,A,_),genA(_,A,_),initB(_,_,_)], {}, 620, 522, create_alice). f(8, [waitA(_,A,_),readyB(_,A,_),initM(_),fresh(B),zero(_)], {B-A<-0.0}, 619, 523, rendez_vous_over_Nb_for_alice_and_bob). f(8, [init,stopB(_,_,_),stopA(_,_,_)], {}, 618, 523, initialize_system). f(8, [stopB(_,_,_),zero(_),init,stopA(_,_,_)], {}, 617, 524, bob_restarts). f(8, [initM(_),fresh(A),zero(_),stopA(_,B,_)], {B-A>0.0}, 616, 525, call_create). f(8, [init,create(_),stopA(_,_,_)], {}, 615, 525, initialize_system). f(8, [waitA(_,A,_),readyB(_,A,_),init,create(_),create(_)], {}, 614, 527, rendez_vous_over_Nb_for_alice_and_bob). f(8, [initM(_),fresh(_),init,create(_),stopA(_,_,_)], {}, 613, 527, call_create). f(8, [waitA(_,A,_),readyB(_,A,_),waitA(_,B,_),readyB(_,B,_),zero(_),fresh(C)], {C-A<-0.0}, 612, 531, rendez_vous_over_Nb_for_alice_and_bob). f(8, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),stopA(_,C,_)], {C-B>0.0}, 611, 531, bob_generates_a_fresh_name). f(8, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),stopA(_,C,_)], {C-B>0.0}, 610, 531, alice_sends_nonce_Na_to_bob). f(8, [init,waitA(_,A,_),readyB(_,A,_),stopA(_,_,_)], {}, 609, 531, initialize_system). f(8, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),initB(_,_,_),stopA(_,C,_)], {C-B>0.0}, 608, 532, bob_restarts). f(8, [stopB(_,_,_),zero(_),genB(_,A,_),fresh(B),waitA(_,A,_),stopA(_,C,_)], {C-B>0.0}, 607, 533, bob_restarts). f(8, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),initB(_,_,_),stopA(_,B,_)], {B-A>0.0}, 606, 533, alice_sends_nonce_Na_to_bob). f(8, [waitA(_,A,_),readyB(_,A,_),init,create(_),stopA(_,_,_)], {}, 605, 534, rendez_vous_over_Nb_for_alice_and_bob). f(8, [init,stopA(_,_,_),stopA(_,_,_)], {}, 604, 535, initialize_system). f(8, [stopA(_,_,_),zero(_),init,stopA(_,_,_)], {}, 603, 536, alice_restarts). f(8, [create(_),zero(_),init,stopA(_,_,_)], {}, 602, 536, create_alice). f(8, [genB(_,A,_),fresh(_),init,stopA(_,_,_),stopA(_,A,_)], {}, 601, 539, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),genA(_,_,_),initB(_,_,_),zero(_),initB(_,_,_),stopA(_,A,C)], {A-C>0.0,A-B>0.0}, 600, 541, bob_generates_a_fresh_name). f(8, [waitA(_,A,_),readyB(_,A,_),genA(_,B,_),initB(_,_,_),readyB(_,B,C),zero(_),fresh(D),readyB(_,B,E)], {E-C>0.0,B-D>0.0}, 599, 544, rendez_vous_over_Nb_for_alice_and_bob). f(8, [genB(_,A,_),fresh(B),genA(_,A,_),initB(_,_,_),readyB(_,A,C),zero(_),stopA(_,_,_)], {A-C>0.0,A-B>0.0}, 598, 544, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),genA(_,A,_),initB(_,_,_),zero(_),stopA(_,_,_),readyB(_,A,C)], {B-C<-0.0,B-A<-0.0}, 597, 544, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(_),init,waitA(_,B,_),readyB(_,B,_),stopA(_,A,_)], {}, 596, 545, bob_generates_a_fresh_name). f(8, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-B>0.0}, 595, 546, bob_restarts). f(8, [genB(_,A,_),fresh(B),genA(_,C,_),initB(_,_,_),readyB(_,C,_),zero(_),stopA(_,A,D)], {A-D>0.0,A-B>0.0}, 594, 546, bob_generates_a_fresh_name). f(8, [waitA(_,A,_),readyB(_,A,B),genB(_,C,_),fresh(D),waitA(_,C,_),zero(_),readyB(_,A,E)], {E-B>0.0,A-D>0.0}, 593, 547, rendez_vous_over_Nb_for_alice_and_bob). f(8, [genB(_,A,_),fresh(B),genB(_,C,_),waitA(_,C,_),zero(_),stopA(_,A,D)], {A-D>0.0,A-B>0.0}, 592, 547, bob_generates_a_fresh_name). f(8, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 591, 547, alice_sends_nonce_Na_to_bob). f(8, [genB(_,A,_),fresh(_),init,create(_),stopA(_,A,_)], {}, 590, 549, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),initM(_),zero(_),stopA(_,A,C)], {A-C>0.0,A-B>0.0}, 589, 550, bob_generates_a_fresh_name). f(8, [init,readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 588, 550, initialize_system). f(8, [waitA(_,A,_),readyB(_,A,B),init,readyB(_,A,C)], {C-B>0.0}, 587, 552, rendez_vous_over_Nb_for_alice_and_bob). f(8, [genB(_,A,_),fresh(_),init,stopB(_,_,_),stopA(_,A,_)], {}, 586, 552, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(_),init,stopB(_,_,_),genA(_,A,_),readyB(_,A,_),genA(_,A,_)], {}, 585, 553, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),init,stopB(_,_,_),genA(_,A,_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 584, 553, bob_generates_a_fresh_name). f(8, [stopA(_,_,_),zero(_),fresh(A),stopB(_,_,_),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 583, 554, alice_restarts). f(8, [genB(_,A,_),fresh(B),initA(_,_,_),stopB(_,_,_),zero(_),readyB(_,A,C),genA(_,A,_)], {A-C>0.0,A-B>0.0}, 582, 554, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),initA(_,_,_),stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 581, 554, bob_generates_a_fresh_name). f(8, [create(_),zero(_),fresh(A),stopB(_,_,_),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 580, 554, create_alice). f(8, [genB(_,A,_),fresh(_),waitA(_,B,_),readyB(_,B,_),zero(_),genA(_,A,_),readyB(_,A,_),genA(_,A,_)], {}, 579, 555, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),waitA(_,C,_),readyB(_,C,_),zero(_),genA(_,A,_),genA(_,A,_),readyB(_,A,D)], {D-B>0.0}, 578, 555, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(_),waitA(_,A,_),zero(_),genA(_,B,_),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {D-C>0.0}, 577, 555, bob_generates_a_fresh_name). f(8, [initA(_,_,_),fresh(A),waitA(_,B,_),readyB(_,B,_),zero(_),readyB(_,C,D),genA(_,C,_),readyB(_,C,E)], {C-A>0.0,E-D>0.0}, 576, 555, alice_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(_),init,initA(_,_,_),initB(_,_,_),readyB(_,A,_),genA(_,A,_)], {}, 575, 556, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),init,initA(_,_,_),initB(_,_,_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 574, 556, bob_generates_a_fresh_name). f(8, [initA(_,_,_),fresh(A),init,initA(_,_,_),initB(_,_,_),readyB(_,B,C),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 573, 556, alice_generates_a_fresh_name). f(8, [create(_),zero(_),init,initB(_,_,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 572, 556, create_alice). f(8, [stopA(_,_,_),zero(_),create(_),fresh(A),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 571, 557, alice_restarts). f(8, [genB(_,A,_),fresh(B),create(_),zero(_),initA(_,_,_),readyB(_,A,C),genA(_,A,_)], {A-C>0.0,A-B>0.0}, 570, 557, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),create(_),zero(_),initA(_,_,_),genA(_,A,_),readyB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 569, 557, bob_generates_a_fresh_name). f(8, [create(_),zero(_),create(_),fresh(A),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 568, 557, create_alice). f(8, [init,create(_),initA(_,_,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 567, 557, initialize_system). f(8, [genB(_,A,_),fresh(_),init,create(_),genA(_,A,_),readyB(_,A,_),genA(_,A,_)], {}, 566, 558, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),init,create(_),genA(_,A,_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 565, 558, bob_generates_a_fresh_name). f(8, [initA(_,_,_),fresh(A),init,create(_),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 564, 558, alice_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(_),initM(_),zero(_),genA(_,A,_),readyB(_,A,_),genA(_,A,_)], {}, 563, 559, bob_generates_a_fresh_name). f(8, [genB(_,A,_),fresh(B),initM(_),zero(_),genA(_,A,_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 562, 559, bob_generates_a_fresh_name). f(8, [initA(_,_,_),fresh(A),initM(_),zero(_),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 561, 559, alice_generates_a_fresh_name). f(8, [init,genA(_,A,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 560, 559, initialize_system). f(7, [initM(_),fresh(_),zero(_),genA(_,A,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 559, 212, call_create). f(7, [init,create(_),genA(_,A,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 558, 212, initialize_system). f(7, [create(_),zero(_),initA(_,_,_),fresh(A),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 557, 213, create_bob). f(7, [init,initA(_,_,_),initB(_,_,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 556, 213, initialize_system). f(7, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {D-C>0.0}, 555, 216, rendez_vous_over_Nb_for_alice_and_bob). f(7, [initA(_,_,_),fresh(A),stopB(_,_,_),zero(_),readyB(_,B,C),genA(_,B,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 554, 216, alice_generates_a_fresh_name). f(7, [init,stopB(_,_,_),genA(_,A,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 553, 216, initialize_system). f(7, [init,stopB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 552, 223, initialize_system). f(7, [stopB(_,_,_),zero(_),init,readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 551, 226, bob_restarts). f(7, [initM(_),fresh(A),zero(_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 550, 227, call_create). f(7, [init,create(_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 549, 227, initialize_system). f(7, [initM(_),fresh(_),init,create(_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 548, 232, call_create). f(7, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-B>0.0}, 547, 239, bob_generates_a_fresh_name). f(7, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-B>0.0}, 546, 239, alice_sends_nonce_Na_to_bob). f(7, [init,waitA(_,A,_),readyB(_,A,_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0}, 545, 239, initialize_system). f(7, [genA(_,A,_),initB(_,_,_),readyB(_,A,B),zero(_),stopA(_,_,_),fresh(C),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 544, 240, alice_sends_nonce_Na_to_bob). f(7, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),initB(_,_,_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-B>0.0}, 543, 241, bob_restarts). f(7, [stopB(_,_,_),zero(_),genB(_,A,_),fresh(B),waitA(_,A,_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-B>0.0}, 542, 242, bob_restarts). f(7, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),initB(_,_,_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 541, 242, alice_sends_nonce_Na_to_bob). f(7, [waitA(_,A,_),readyB(_,A,_),init,create(_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0}, 540, 244, rendez_vous_over_Nb_for_alice_and_bob). f(7, [init,stopA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 539, 245, initialize_system). f(7, [stopA(_,_,_),zero(_),init,readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 538, 249, alice_restarts). f(7, [create(_),zero(_),init,readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 537, 249, create_alice). f(7, [init,initA(_,_,_),stopA(_,_,_)], {}, 536, 253, initialize_system). f(7, [initM(_),fresh(A),zero(_),stopA(_,_,_),stopA(_,B,_)], {B-A>0.0}, 535, 257, call_create). f(7, [init,create(_),stopA(_,_,_),stopA(_,_,_)], {}, 534, 257, initialize_system). f(7, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),initB(_,_,_),stopA(_,C,_)], {C-B>0.0}, 533, 258, bob_generates_a_fresh_name). f(7, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),stopA(_,C,_)], {C-B>0.0}, 532, 258, alice_sends_nonce_Na_to_bob). f(7, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),stopA(_,C,_)], {C-B>0.0}, 531, 260, rendez_vous_over_Nb_for_alice_and_bob). f(7, [init,stopB(_,_,_),stopA(_,_,_),stopA(_,_,_)], {}, 530, 260, initialize_system). f(7, [stopA(_,_,_),zero(_),init,create(_),stopA(_,_,_)], {}, 529, 261, alice_restarts). f(7, [initM(_),fresh(_),init,initA(_,_,_),stopA(_,_,_)], {}, 528, 261, call_create). f(7, [init,create(_),create(_),stopA(_,_,_)], {}, 527, 262, initialize_system). f(7, [create(_),zero(_),init,create(_),stopA(_,_,_)], {}, 526, 264, create_bob). f(7, [create(_),zero(_),fresh(A),stopA(_,B,_)], {B-A>0.0}, 525, 265, create_bob). f(7, [init,initB(_,_,_),stopA(_,_,_)], {}, 524, 265, initialize_system). f(7, [initM(_),fresh(A),stopB(_,_,_),zero(_),stopA(_,B,_)], {B-A>0.0}, 523, 267, call_create). f(7, [init,initA(_,_,_),initB(_,_,_),readyB(_,A,_),genA(_,A,_),initB(_,_,_)], {}, 522, 272, initialize_system). f(7, [stopA(_,_,_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),stopA(_,C,_)], {C-A>0.0}, 521, 275, alice_restarts). f(7, [create(_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),stopA(_,C,_)], {C-A>0.0}, 520, 275, create_alice). f(7, [initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_),zero(_),stopA(_,C,_)], {C-A>0.0}, 519, 276, alice_generates_a_fresh_name). f(7, [stopA(_,_,_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_)], {B-A>0.0}, 518, 278, alice_restarts). f(7, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),genA(_,A,_),fresh(_)], {}, 517, 279, bob_restarts). f(7, [initA(_,_,_),fresh(A),initB(_,_,_),readyB(_,B,_),zero(_),genA(_,B,_)], {B-A>0.0}, 516, 279, alice_generates_a_fresh_name). f(7, [create(_),zero(_),genA(_,A,_),readyB(_,A,_),genA(_,A,_),fresh(_)], {}, 515, 279, create_bob). f(7, [init,genA(_,A,_),initB(_,_,_),readyB(_,A,_),genA(_,A,_)], {}, 514, 279, initialize_system). f(7, [genA(_,A,_),initB(_,_,_),fresh(_),zero(_),genA(_,A,_)], {}, 513, 280, alice_sends_nonce_Na_to_bob). f(7, [initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_),zero(_)], {B-A>0.0}, 512, 280, alice_generates_a_fresh_name). f(7, [init,genB(_,A,_),waitA(_,A,_),genA(_,A,_)], {}, 511, 280, initialize_system). f(7, [stopA(_,_,_),zero(_),init,stopB(_,_,_),stopA(_,_,_)], {}, 510, 281, alice_restarts). f(7, [waitA(_,A,_),readyB(_,A,_),init,initA(_,_,_)], {}, 509, 281, rendez_vous_over_Nb_for_alice_and_bob). f(7, [init,stopB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 508, 292, initialize_system). f(7, [stopB(_,_,_),zero(_),init,readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 507, 294, bob_restarts). f(7, [initM(_),fresh(A),zero(_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 506, 295, call_create). f(7, [init,create(_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 505, 295, initialize_system). f(7, [initM(_),fresh(_),init,create(_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 504, 299, call_create). f(7, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),readyB(_,C,D),stopB(_,C,E)], {C-B>0.0,E-D>0.0}, 503, 306, bob_generates_a_fresh_name). f(7, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,D),stopB(_,C,E)], {C-B>0.0,E-D>0.0}, 502, 306, alice_sends_nonce_Na_to_bob). f(7, [init,waitA(_,A,_),readyB(_,A,_),readyB(_,B,C),stopB(_,B,D)], {D-C>0.0}, 501, 306, initialize_system). f(7, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),initB(_,_,_),readyB(_,C,D),stopB(_,C,E)], {C-B>0.0,E-D>0.0}, 500, 308, bob_restarts). f(7, [stopB(_,_,_),zero(_),genB(_,A,_),fresh(B),waitA(_,A,_),readyB(_,C,D),stopB(_,C,E)], {C-B>0.0,E-D>0.0}, 499, 309, bob_restarts). f(7, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),initB(_,_,_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 498, 309, alice_sends_nonce_Na_to_bob). f(7, [waitA(_,A,_),readyB(_,A,_),init,create(_),readyB(_,B,C),stopB(_,B,D)], {D-C>0.0}, 497, 311, rendez_vous_over_Nb_for_alice_and_bob). f(7, [init,stopA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 496, 312, initialize_system). f(7, [stopA(_,_,_),zero(_),init,readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 495, 316, alice_restarts). f(7, [create(_),zero(_),init,readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 494, 316, create_alice). f(7, [genB(_,A,_),fresh(B),initA(_,_,_),genB(_,C,_),waitA(_,C,_),zero(_),stopA(_,A,D)], {B-A<-0.0,B-D<-0.0}, 493, 322, bob_generates_a_fresh_name). f(7, [genB(_,A,_),fresh(B),initM(_),stopB(_,_,_),zero(_),stopA(_,A,C)], {B-A<-0.0,B-C<-0.0}, 492, 326, bob_generates_a_fresh_name). f(7, [init,stopB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 491, 326, initialize_system). f(7, [stopB(_,_,_),zero(_),init,readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 490, 327, bob_restarts). f(7, [genB(_,A,_),fresh(B),init,initB(_,_,_),stopA(_,A,C)], {C-B>0.0}, 489, 327, bob_generates_a_fresh_name). f(7, [genB(_,A,_),fresh(B),create(_),zero(_),stopA(_,A,C)], {B-A<-0.0,B-C<-0.0}, 488, 328, bob_generates_a_fresh_name). f(7, [initM(_),fresh(A),zero(_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 487, 328, call_create). f(7, [init,create(_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 486, 328, initialize_system). f(7, [genB(_,A,_),fresh(B),init,create(_),create(_),stopA(_,A,C)], {C-B>0.0}, 485, 330, bob_generates_a_fresh_name). f(7, [initM(_),fresh(_),init,create(_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 484, 330, call_create). f(7, [waitA(_,A,_),readyB(_,A,B),init,stopA(_,_,_),readyB(_,A,C)], {C-B<-0.0}, 483, 333, rendez_vous_over_Nb_for_alice_and_bob). f(7, [genB(_,A,_),fresh(B),init,stopB(_,_,_),stopA(_,_,_),stopA(_,A,C)], {C-B>0.0}, 482, 333, bob_generates_a_fresh_name). f(7, [genB(_,A,_),fresh(B),waitA(_,C,_),readyB(_,C,_),zero(_),stopA(_,A,D)], {B-A<-0.0,B-D<-0.0}, 481, 334, bob_generates_a_fresh_name). f(7, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),readyB(_,C,D),stopA(_,C,E)], {C-B>0.0,E-D>0.0}, 480, 334, bob_generates_a_fresh_name). f(7, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,D),stopA(_,C,E)], {C-B>0.0,E-D>0.0}, 479, 334, alice_sends_nonce_Na_to_bob). f(7, [init,waitA(_,A,_),readyB(_,A,_),readyB(_,B,C),stopA(_,B,D)], {D-C>0.0}, 478, 334, initialize_system). f(7, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),initB(_,_,_),readyB(_,C,D),stopA(_,C,E)], {C-B>0.0,E-D>0.0}, 477, 335, bob_restarts). f(7, [genB(_,A,_),fresh(B),genA(_,C,_),initB(_,_,_),readyB(_,C,_),zero(_),initB(_,_,_),stopA(_,A,D)], {B-A<-0.0,B-D<-0.0}, 476, 335, bob_generates_a_fresh_name). f(7, [stopB(_,_,_),zero(_),genB(_,A,_),fresh(B),waitA(_,A,_),readyB(_,C,D),stopA(_,C,E)], {C-B>0.0,E-D>0.0}, 475, 336, bob_restarts). f(7, [genB(_,A,_),fresh(B),genB(_,C,_),waitA(_,C,_),zero(_),initB(_,_,_),stopA(_,A,D)], {B-A<-0.0,B-D<-0.0}, 474, 336, bob_generates_a_fresh_name). f(7, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),initB(_,_,_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 473, 336, alice_sends_nonce_Na_to_bob). f(7, [waitA(_,A,_),readyB(_,A,_),init,create(_),readyB(_,B,C),stopA(_,B,D)], {D-C>0.0}, 472, 337, rendez_vous_over_Nb_for_alice_and_bob). f(7, [genB(_,A,_),fresh(B),init,create(_),stopA(_,_,_),stopA(_,A,C)], {C-B>0.0}, 471, 337, bob_generates_a_fresh_name). f(7, [genB(_,A,_),fresh(B),initM(_),zero(_),stopA(_,_,_),stopA(_,A,C)], {B-A<-0.0,B-C<-0.0}, 470, 338, bob_generates_a_fresh_name). f(7, [init,stopA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 469, 338, initialize_system). f(7, [stopA(_,_,_),zero(_),init,readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 468, 339, alice_restarts). f(7, [genB(_,A,_),fresh(B),init,initA(_,_,_),stopA(_,A,C)], {C-B>0.0}, 467, 339, bob_generates_a_fresh_name). f(7, [create(_),zero(_),init,readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 466, 339, create_alice). f(7, [genB(_,A,_),fresh(_),init,initA(_,_,_),initB(_,_,_),readyB(_,A,_),genA(_,A,_),initB(_,_,_)], {}, 465, 349, bob_generates_a_fresh_name). f(7, [genB(_,A,_),fresh(B),init,initA(_,_,_),initB(_,_,_),genA(_,A,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 464, 349, bob_generates_a_fresh_name). f(7, [initA(_,_,_),fresh(A),init,initA(_,_,_),initB(_,_,_),readyB(_,B,C),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 463, 349, alice_generates_a_fresh_name). f(7, [create(_),zero(_),init,initA(_,_,_),readyB(_,A,B),genA(_,A,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 462, 349, create_bob). f(7, [init,stopB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 461, 353, initialize_system). f(7, [stopB(_,_,_),zero(_),init,readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 460, 355, bob_restarts). f(7, [initM(_),fresh(A),zero(_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 459, 356, call_create). f(7, [init,create(_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 458, 356, initialize_system). f(7, [initM(_),fresh(_),init,create(_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 457, 360, call_create). f(7, [waitA(_,A,_),readyB(_,A,B),init,stopB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 456, 365, rendez_vous_over_Nb_for_alice_and_bob). f(7, [waitA(_,A,_),readyB(_,A,B),waitA(_,C,_),readyB(_,C,_),zero(_),fresh(D),readyB(_,A,E)], {E-B>0.0,A-D>0.0}, 455, 367, rendez_vous_over_Nb_for_alice_and_bob). f(7, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-B>0.0}, 454, 367, bob_generates_a_fresh_name). f(7, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-B>0.0}, 453, 367, alice_sends_nonce_Na_to_bob). f(7, [init,waitA(_,A,_),readyB(_,A,_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0}, 452, 367, initialize_system). f(7, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),fresh(B),initB(_,_,_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-B>0.0}, 451, 368, bob_restarts). f(7, [stopB(_,_,_),zero(_),genB(_,A,_),fresh(B),waitA(_,A,_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-B>0.0}, 450, 369, bob_restarts). f(7, [genA(_,_,_),initB(_,_,_),fresh(A),zero(_),initB(_,_,_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 449, 369, alice_sends_nonce_Na_to_bob). f(7, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,B),fresh(C),initB(_,_,_),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 448, 371, bob_restarts). f(7, [create(_),zero(_),genA(_,A,_),readyB(_,A,B),fresh(C),initB(_,_,_),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 447, 371, create_bob). f(7, [init,genA(_,A,_),initB(_,_,_),readyB(_,A,B),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 446, 371, initialize_system). f(7, [waitA(_,A,_),readyB(_,A,_),init,create(_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0}, 445, 374, rendez_vous_over_Nb_for_alice_and_bob). f(7, [waitA(_,A,_),readyB(_,A,B),init,create(_),readyB(_,A,C)], {C-B>0.0}, 444, 374, rendez_vous_over_Nb_for_alice_and_bob). f(7, [waitA(_,A,_),readyB(_,A,B),initM(_),fresh(C),zero(_),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 443, 375, rendez_vous_over_Nb_for_alice_and_bob). f(7, [init,stopA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 442, 375, initialize_system). f(7, [stopA(_,_,_),zero(_),init,readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 441, 378, alice_restarts). f(7, [create(_),zero(_),init,readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 440, 378, create_alice). f(7, [stopB(_,_,_),zero(_),init,genA(_,A,_),genB(_,A,_),waitA(_,A,_)], {}, 439, 381, bob_restarts). f(7, [create(_),zero(_),init,genA(_,A,_),genB(_,A,_),waitA(_,A,_)], {}, 438, 381, create_bob). f(7, [stopB(_,_,_),zero(_),initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_)], {B-A>0.0}, 437, 382, bob_restarts). f(7, [create(_),zero(_),initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_)], {B-A>0.0}, 436, 382, create_bob). f(7, [init,initA(_,_,_),initB(_,_,_),genB(_,A,_),waitA(_,A,_)], {}, 435, 382, initialize_system). f(7, [stopB(_,_,_),zero(_),genA(_,A,_),genA(_,A,_),initB(_,_,_),fresh(_)], {}, 434, 383, bob_restarts). f(7, [initA(_,_,_),fresh(A),initB(_,_,_),genA(_,B,_),initB(_,_,_)], {B-A>0.0}, 433, 383, alice_generates_a_fresh_name). f(7, [create(_),zero(_),genA(_,A,_),genA(_,A,_),initB(_,_,_),fresh(_)], {}, 432, 383, create_bob). f(7, [init,genA(_,A,_),initB(_,_,_),genA(_,A,_),initB(_,_,_)], {}, 431, 383, initialize_system). f(7, [init,initA(_,_,_),stopB(_,_,_)], {}, 430, 385, initialize_system). f(7, [initM(_),fresh(A),zero(_),stopA(_,_,_),stopB(_,B,_)], {B-A>0.0}, 429, 388, call_create). f(7, [init,create(_),stopA(_,_,_),stopB(_,_,_)], {}, 428, 388, initialize_system). f(7, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),initB(_,_,_)], {A-B>0.0}, 427, 389, bob_generates_a_fresh_name). f(7, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_)], {B-A<-0.0}, 426, 389, alice_sends_nonce_Na_to_bob). f(7, [create(_),zero(_),waitA(_,A,_),readyB(_,A,_),fresh(B)], {B-A<-0.0}, 425, 389, create_bob). f(7, [init,waitA(_,A,_),readyB(_,A,_),initB(_,_,_)], {}, 424, 389, initialize_system). f(7, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),initB(_,_,_),stopB(_,C,_)], {C-B>0.0}, 423, 390, bob_generates_a_fresh_name). f(7, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),stopB(_,C,_)], {C-B>0.0}, 422, 390, alice_sends_nonce_Na_to_bob). f(7, [waitA(_,A,_),readyB(_,A,_),stopB(_,_,_),zero(_),fresh(B)], {B-A<-0.0}, 421, 391, rendez_vous_over_Nb_for_alice_and_bob). f(7, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),stopB(_,C,_)], {C-B>0.0}, 420, 391, rendez_vous_over_Nb_for_alice_and_bob). f(7, [init,stopB(_,_,_),stopA(_,_,_),stopB(_,_,_)], {}, 419, 391, initialize_system). f(7, [stopA(_,_,_),zero(_),init,create(_),stopB(_,_,_)], {}, 418, 392, alice_restarts). f(7, [waitA(_,A,_),readyB(_,A,_),init,create(_),initA(_,_,_)], {}, 417, 392, rendez_vous_over_Nb_for_alice_and_bob). f(7, [initM(_),fresh(_),init,initA(_,_,_),stopB(_,_,_)], {}, 416, 392, call_create). f(7, [waitA(_,A,_),readyB(_,A,_),create(_),zero(_),create(_),fresh(B)], {B-A<-0.0}, 415, 393, rendez_vous_over_Nb_for_alice_and_bob). f(7, [init,create(_),create(_),stopB(_,_,_)], {}, 414, 393, initialize_system). f(7, [waitA(_,A,_),readyB(_,A,_),init,create(_),initB(_,_,_)], {}, 413, 394, rendez_vous_over_Nb_for_alice_and_bob). f(7, [create(_),zero(_),init,create(_),stopB(_,_,_)], {}, 412, 394, create_bob). f(7, [create(_),zero(_),fresh(A),stopB(_,B,_)], {B-A>0.0}, 411, 395, create_bob). f(7, [init,initB(_,_,_),stopB(_,_,_)], {}, 410, 395, initialize_system). f(7, [waitA(_,A,_),readyB(_,A,_),stopB(_,_,_),zero(_),create(_),fresh(B)], {B-A<-0.0}, 409, 396, rendez_vous_over_Nb_for_alice_and_bob). f(7, [initM(_),fresh(A),stopB(_,_,_),zero(_),stopB(_,B,_)], {B-A>0.0}, 408, 396, call_create). f(7, [init,stopB(_,_,_),create(_),stopB(_,_,_)], {}, 407, 396, initialize_system). f(7, [stopA(_,_,_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),stopB(_,C,_)], {C-A>0.0}, 406, 398, alice_restarts). f(7, [create(_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),stopB(_,C,_)], {C-A>0.0}, 405, 398, create_alice). f(7, [initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_),zero(_),stopB(_,C,_)], {C-A>0.0}, 404, 399, alice_generates_a_fresh_name). f(7, [stopA(_,_,_),zero(_),init,stopB(_,_,_),stopB(_,_,_)], {}, 403, 400, alice_restarts). f(7, [waitA(_,A,_),readyB(_,A,_),init,initA(_,_,_),stopB(_,_,_)], {}, 402, 400, rendez_vous_over_Nb_for_alice_and_bob). f(7, [create(_),zero(_),init,stopB(_,_,_),stopB(_,_,_)], {}, 401, 400, create_alice). f(6, [init,initA(_,_,_),stopB(_,_,_),stopB(_,_,_)], {}, 400, 94, initialize_system). f(6, [genB(_,A,_),fresh(_),waitA(_,A,_),zero(_),genA(_,B,_),stopB(_,B,_)], {}, 399, 95, bob_generates_a_fresh_name). f(6, [initA(_,_,_),fresh(A),waitA(_,B,_),readyB(_,B,_),zero(_),stopB(_,C,_)], {C-A>0.0}, 398, 95, alice_generates_a_fresh_name). f(6, [stopB(_,_,_),zero(_),init,initA(_,_,_),stopB(_,_,_)], {}, 397, 97, bob_restarts). f(6, [stopB(_,_,_),zero(_),create(_),fresh(A),stopB(_,B,_)], {B-A>0.0}, 396, 98, bob_restarts). f(6, [initM(_),fresh(A),zero(_),initB(_,_,_),stopB(_,B,_)], {B-A>0.0}, 395, 98, call_create). f(6, [init,create(_),initB(_,_,_),stopB(_,_,_)], {}, 394, 98, initialize_system). f(6, [create(_),zero(_),create(_),fresh(A),stopB(_,B,_)], {B-A>0.0}, 393, 99, create_alice). f(6, [init,create(_),initA(_,_,_),stopB(_,_,_)], {}, 392, 99, initialize_system). f(6, [stopB(_,_,_),zero(_),stopA(_,_,_),fresh(A),stopB(_,B,_)], {B-A>0.0}, 391, 101, bob_restarts). f(6, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),stopB(_,C,_)], {C-B>0.0}, 390, 101, rendez_vous_over_Nb_for_alice_and_bob). f(6, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_)], {B-A<-0.0}, 389, 101, rendez_vous_over_Nb_for_alice_and_bob). f(6, [create(_),zero(_),stopA(_,_,_),fresh(A),stopB(_,B,_)], {B-A>0.0}, 388, 101, create_bob). f(6, [init,stopA(_,_,_),initB(_,_,_),stopB(_,_,_)], {}, 387, 101, initialize_system). f(6, [initA(_,_,_),fresh(A),init,create(_),stopB(_,B,_)], {B-A>0.0}, 386, 102, alice_generates_a_fresh_name). f(6, [initA(_,_,_),fresh(A),initM(_),zero(_),stopB(_,B,_)], {B-A>0.0}, 385, 103, alice_generates_a_fresh_name). f(6, [init,genA(_,A,_),stopB(_,A,_)], {}, 384, 103, initialize_system). f(6, [genA(_,A,_),initB(_,_,_),genA(_,A,_),initB(_,_,_),fresh(_)], {}, 383, 107, alice_sends_nonce_Na_to_bob). f(6, [initA(_,_,_),fresh(A),initB(_,_,_),genB(_,B,_),waitA(_,B,_)], {B-A>0.0}, 382, 107, alice_generates_a_fresh_name). f(6, [init,genA(_,A,_),initB(_,_,_),genB(_,A,_),waitA(_,A,_)], {}, 381, 107, initialize_system). f(6, [genB(_,A,_),fresh(_),init,genA(_,A,_),stopB(_,A,_)], {}, 380, 108, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),initA(_,_,_),initM(_),zero(_),stopB(_,A,C)], {A-C>0.0,A-B>0.0}, 379, 109, bob_generates_a_fresh_name). f(6, [init,initA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 378, 109, initialize_system). f(6, [genB(_,A,_),fresh(_),init,stopA(_,_,_),initB(_,_,_),stopB(_,A,_)], {}, 377, 112, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),create(_),zero(_),stopA(_,_,_),stopB(_,A,C)], {A-C>0.0,A-B>0.0}, 376, 113, bob_generates_a_fresh_name). f(6, [initM(_),fresh(A),zero(_),stopA(_,_,_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 375, 113, call_create). f(6, [init,create(_),stopA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 374, 113, initialize_system). f(6, [genB(_,A,_),fresh(B),waitA(_,A,_),readyB(_,A,C),zero(_),initB(_,_,_)], {A-C>0.0,A-B>0.0}, 373, 114, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),initB(_,_,_),readyB(_,A,C)], {B-C<-0.0,B-A<-0.0}, 372, 114, bob_generates_a_fresh_name). f(6, [genA(_,A,_),initB(_,_,_),readyB(_,A,B),zero(_),fresh(C),initB(_,_,_),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 371, 114, alice_sends_nonce_Na_to_bob). f(6, [genB(_,A,_),fresh(B),waitA(_,C,_),readyB(_,C,_),zero(_),initB(_,_,_),stopB(_,A,D)], {A-D>0.0,A-B>0.0}, 370, 115, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),initB(_,_,_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-B>0.0}, 369, 115, bob_generates_a_fresh_name). f(6, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-B>0.0}, 368, 115, alice_sends_nonce_Na_to_bob). f(6, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-B>0.0}, 367, 116, rendez_vous_over_Nb_for_alice_and_bob). f(6, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),stopA(_,_,_),stopB(_,A,C)], {A-C>0.0,A-B>0.0}, 366, 116, bob_generates_a_fresh_name). f(6, [init,stopB(_,_,_),stopA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 365, 116, initialize_system). f(6, [stopA(_,_,_),zero(_),init,create(_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 364, 117, alice_restarts). f(6, [genB(_,A,_),fresh(_),init,create(_),initA(_,_,_),stopB(_,A,_)], {}, 363, 117, bob_generates_a_fresh_name). f(6, [initM(_),fresh(_),init,initA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 362, 117, call_create). f(6, [genB(_,A,_),fresh(B),create(_),zero(_),create(_),stopB(_,A,C)], {A-C>0.0,A-B>0.0}, 361, 118, bob_generates_a_fresh_name). f(6, [init,create(_),create(_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 360, 118, initialize_system). f(6, [genB(_,A,_),fresh(_),init,create(_),initB(_,_,_),stopB(_,A,_)], {}, 359, 120, bob_generates_a_fresh_name). f(6, [create(_),zero(_),init,create(_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 358, 120, create_bob). f(6, [genB(_,A,_),fresh(B),initM(_),zero(_),initB(_,_,_),stopB(_,A,C)], {A-C>0.0,A-B>0.0}, 357, 121, bob_generates_a_fresh_name). f(6, [create(_),zero(_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 356, 121, create_bob). f(6, [init,initB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 355, 121, initialize_system). f(6, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),create(_),stopB(_,A,C)], {A-C>0.0,A-B>0.0}, 354, 122, bob_generates_a_fresh_name). f(6, [initM(_),fresh(A),stopB(_,_,_),zero(_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 353, 122, call_create). f(6, [init,stopB(_,_,_),create(_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 352, 122, initialize_system). f(6, [stopA(_,_,_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,C),genA(_,B,_),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 351, 126, alice_restarts). f(6, [create(_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,C),genA(_,B,_),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 350, 126, create_alice). f(6, [init,initA(_,_,_),initB(_,_,_),readyB(_,A,B),genA(_,A,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 349, 126, initialize_system). f(6, [stopA(_,_,_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-A>0.0}, 348, 130, alice_restarts). f(6, [genB(_,A,_),fresh(B),initA(_,_,_),waitA(_,C,_),readyB(_,C,_),zero(_),stopB(_,A,D)], {A-D>0.0,A-B>0.0}, 347, 130, bob_generates_a_fresh_name). f(6, [create(_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-A>0.0}, 346, 130, create_alice). f(6, [genB(_,A,_),fresh(_),genB(_,B,_),waitA(_,B,_),zero(_),genA(_,A,_),stopB(_,A,_)], {}, 345, 131, bob_generates_a_fresh_name). f(6, [initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_),zero(_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-A>0.0}, 344, 131, alice_generates_a_fresh_name). f(6, [stopA(_,_,_),zero(_),init,stopB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 343, 132, alice_restarts). f(6, [waitA(_,A,_),readyB(_,A,_),init,initA(_,_,_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0}, 342, 132, rendez_vous_over_Nb_for_alice_and_bob). f(6, [genB(_,A,_),fresh(_),init,initA(_,_,_),stopB(_,_,_),stopB(_,A,_)], {}, 341, 132, bob_generates_a_fresh_name). f(6, [create(_),zero(_),init,stopB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 340, 132, create_alice). f(6, [init,initA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 339, 136, initialize_system). f(6, [initM(_),fresh(A),zero(_),stopA(_,_,_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 338, 141, call_create). f(6, [init,create(_),stopA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 337, 141, initialize_system). f(6, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),initB(_,_,_),readyB(_,C,D),stopA(_,C,E)], {C-B>0.0,E-D>0.0}, 336, 143, bob_generates_a_fresh_name). f(6, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),readyB(_,C,D),stopA(_,C,E)], {C-B>0.0,E-D>0.0}, 335, 143, alice_sends_nonce_Na_to_bob). f(6, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,D),stopA(_,C,E)], {C-B>0.0,E-D>0.0}, 334, 144, rendez_vous_over_Nb_for_alice_and_bob). f(6, [init,stopB(_,_,_),stopA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 333, 144, initialize_system). f(6, [stopA(_,_,_),zero(_),init,create(_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 332, 145, alice_restarts). f(6, [initM(_),fresh(_),init,initA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 331, 145, call_create). f(6, [init,create(_),create(_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 330, 146, initialize_system). f(6, [create(_),zero(_),init,create(_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 329, 148, create_bob). f(6, [create(_),zero(_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 328, 149, create_bob). f(6, [init,initB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 327, 149, initialize_system). f(6, [initM(_),fresh(A),stopB(_,_,_),zero(_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 326, 151, call_create). f(6, [init,stopB(_,_,_),create(_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 325, 151, initialize_system). f(6, [stopA(_,_,_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),readyB(_,C,D),stopA(_,C,E)], {C-A>0.0,E-D>0.0}, 324, 154, alice_restarts). f(6, [create(_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),readyB(_,C,D),stopA(_,C,E)], {C-A>0.0,E-D>0.0}, 323, 154, create_alice). f(6, [initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_),zero(_),readyB(_,C,D),stopA(_,C,E)], {C-A>0.0,E-D>0.0}, 322, 155, alice_generates_a_fresh_name). f(6, [stopA(_,_,_),zero(_),init,stopB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 321, 157, alice_restarts). f(6, [waitA(_,A,_),readyB(_,A,_),init,initA(_,_,_),readyB(_,B,C),stopA(_,B,D)], {D-C>0.0}, 320, 157, rendez_vous_over_Nb_for_alice_and_bob). f(6, [create(_),zero(_),init,stopB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 319, 157, create_alice). f(6, [genB(_,A,_),fresh(B),init,genA(_,A,_),stopB(_,A,C)], {C-B>0.0}, 318, 162, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),initA(_,_,_),initM(_),zero(_),stopB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 317, 163, bob_generates_a_fresh_name). f(6, [init,initA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 316, 163, initialize_system). f(6, [waitA(_,A,_),readyB(_,A,B),init,initB(_,_,_),readyB(_,A,C)], {C-B<-0.0}, 315, 165, rendez_vous_over_Nb_for_alice_and_bob). f(6, [genB(_,A,_),fresh(B),init,stopA(_,_,_),initB(_,_,_),stopB(_,A,C)], {C-B>0.0}, 314, 165, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),create(_),zero(_),stopA(_,_,_),stopB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 313, 166, bob_generates_a_fresh_name). f(6, [initM(_),fresh(A),zero(_),stopA(_,_,_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 312, 166, call_create). f(6, [init,create(_),stopA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 311, 166, initialize_system). f(6, [genB(_,A,_),fresh(B),waitA(_,C,_),readyB(_,C,_),zero(_),initB(_,_,_),stopB(_,A,D)], {B-A<-0.0,B-D<-0.0}, 310, 167, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),initB(_,_,_),readyB(_,C,D),stopB(_,C,E)], {C-B>0.0,E-D>0.0}, 309, 167, bob_generates_a_fresh_name). f(6, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),readyB(_,C,D),stopB(_,C,E)], {C-B>0.0,E-D>0.0}, 308, 167, alice_sends_nonce_Na_to_bob). f(6, [waitA(_,A,_),readyB(_,A,B),stopB(_,_,_),zero(_),fresh(C),readyB(_,A,D)], {D-B<-0.0,A-C>0.0}, 307, 168, rendez_vous_over_Nb_for_alice_and_bob). f(6, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,D),stopB(_,C,E)], {C-B>0.0,E-D>0.0}, 306, 168, rendez_vous_over_Nb_for_alice_and_bob). f(6, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),stopA(_,_,_),stopB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 305, 168, bob_generates_a_fresh_name). f(6, [init,stopB(_,_,_),stopA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 304, 168, initialize_system). f(6, [stopA(_,_,_),zero(_),init,create(_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 303, 169, alice_restarts). f(6, [genB(_,A,_),fresh(B),init,create(_),initA(_,_,_),stopB(_,A,C)], {C-B>0.0}, 302, 169, bob_generates_a_fresh_name). f(6, [initM(_),fresh(_),init,initA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 301, 169, call_create). f(6, [genB(_,A,_),fresh(B),create(_),zero(_),create(_),stopB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 300, 170, bob_generates_a_fresh_name). f(6, [init,create(_),create(_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 299, 170, initialize_system). f(6, [genB(_,A,_),fresh(B),init,create(_),initB(_,_,_),stopB(_,A,C)], {C-B>0.0}, 298, 171, bob_generates_a_fresh_name). f(6, [create(_),zero(_),init,create(_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 297, 171, create_bob). f(6, [genB(_,A,_),fresh(B),initM(_),zero(_),initB(_,_,_),stopB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 296, 172, bob_generates_a_fresh_name). f(6, [create(_),zero(_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 295, 172, create_bob). f(6, [init,initB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 294, 172, initialize_system). f(6, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),create(_),stopB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 293, 173, bob_generates_a_fresh_name). f(6, [initM(_),fresh(A),stopB(_,_,_),zero(_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 292, 173, call_create). f(6, [init,stopB(_,_,_),create(_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 291, 173, initialize_system). f(6, [stopA(_,_,_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),readyB(_,C,D),stopB(_,C,E)], {C-A>0.0,E-D>0.0}, 290, 175, alice_restarts). f(6, [genB(_,A,_),fresh(B),initA(_,_,_),waitA(_,C,_),readyB(_,C,_),zero(_),stopB(_,A,D)], {B-A<-0.0,B-D<-0.0}, 289, 175, bob_generates_a_fresh_name). f(6, [create(_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),readyB(_,C,D),stopB(_,C,E)], {C-A>0.0,E-D>0.0}, 288, 175, create_alice). f(6, [genB(_,A,_),fresh(B),genB(_,C,_),waitA(_,C,_),zero(_),genA(_,A,_),stopB(_,A,D)], {D-B>0.0}, 287, 176, bob_generates_a_fresh_name). f(6, [initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_),zero(_),readyB(_,C,D),stopB(_,C,E)], {C-A>0.0,E-D>0.0}, 286, 176, alice_generates_a_fresh_name). f(6, [stopA(_,_,_),zero(_),init,stopB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 285, 177, alice_restarts). f(6, [waitA(_,A,_),readyB(_,A,_),init,initA(_,_,_),readyB(_,B,C),stopB(_,B,D)], {D-C>0.0}, 284, 177, rendez_vous_over_Nb_for_alice_and_bob). f(6, [genB(_,A,_),fresh(B),init,initA(_,_,_),stopB(_,_,_),stopB(_,A,C)], {C-B>0.0}, 283, 177, bob_generates_a_fresh_name). f(6, [create(_),zero(_),init,stopB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 282, 177, create_alice). f(6, [init,initA(_,_,_),stopB(_,_,_),stopA(_,_,_)], {}, 281, 179, initialize_system). f(6, [genB(_,A,_),fresh(_),waitA(_,A,_),zero(_),genA(_,A,_)], {}, 280, 180, bob_generates_a_fresh_name). f(6, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),genA(_,A,_),fresh(_)], {}, 279, 180, alice_sends_nonce_Na_to_bob). f(6, [initA(_,_,_),fresh(A),waitA(_,B,_),readyB(_,B,_),zero(_)], {B-A>0.0}, 278, 180, alice_generates_a_fresh_name). f(6, [init,waitA(_,A,_),readyB(_,A,_),genA(_,A,_)], {}, 277, 180, initialize_system). f(6, [genB(_,A,_),fresh(_),waitA(_,A,_),zero(_),genA(_,B,_),stopA(_,B,_)], {}, 276, 181, bob_generates_a_fresh_name). f(6, [initA(_,_,_),fresh(A),waitA(_,B,_),readyB(_,B,_),zero(_),stopA(_,C,_)], {C-A>0.0}, 275, 181, alice_generates_a_fresh_name). f(6, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,_),genA(_,A,_),initB(_,_,_),fresh(_)], {}, 274, 182, bob_restarts). f(6, [genB(_,A,_),fresh(_),genA(_,A,_),initB(_,_,_),genA(_,A,_),initB(_,_,_)], {}, 273, 182, bob_generates_a_fresh_name). f(6, [initA(_,_,_),fresh(A),initB(_,_,_),readyB(_,B,_),genA(_,B,_),initB(_,_,_)], {B-A>0.0}, 272, 182, alice_generates_a_fresh_name). f(6, [create(_),zero(_),genA(_,A,_),readyB(_,A,_),genA(_,A,_),initB(_,_,_),fresh(_)], {}, 271, 182, create_bob). f(6, [init,genA(_,A,_),initB(_,_,_),readyB(_,A,_),genA(_,A,_),initB(_,_,_)], {}, 270, 182, initialize_system). f(6, [stopB(_,_,_),zero(_),init,initA(_,_,_),stopA(_,_,_)], {}, 269, 183, bob_restarts). f(6, [waitA(_,A,_),readyB(_,A,_),init,initA(_,_,_),initB(_,_,_)], {}, 268, 183, rendez_vous_over_Nb_for_alice_and_bob). f(6, [stopB(_,_,_),zero(_),create(_),fresh(A),stopA(_,B,_)], {B-A>0.0}, 267, 184, bob_restarts). f(6, [waitA(_,A,_),readyB(_,A,_),create(_),zero(_),fresh(B),initB(_,_,_)], {B-A<-0.0}, 266, 184, rendez_vous_over_Nb_for_alice_and_bob). f(6, [initM(_),fresh(A),zero(_),initB(_,_,_),stopA(_,B,_)], {B-A>0.0}, 265, 184, call_create). f(6, [init,create(_),initB(_,_,_),stopA(_,_,_)], {}, 264, 184, initialize_system). f(6, [waitA(_,A,_),readyB(_,A,_),create(_),zero(_),initA(_,_,_),fresh(B)], {B-A<-0.0}, 263, 185, rendez_vous_over_Nb_for_alice_and_bob). f(6, [create(_),zero(_),create(_),fresh(A),stopA(_,B,_)], {B-A>0.0}, 262, 185, create_alice). f(6, [init,create(_),initA(_,_,_),stopA(_,_,_)], {}, 261, 185, initialize_system). f(6, [stopB(_,_,_),zero(_),stopA(_,_,_),fresh(A),stopA(_,B,_)], {B-A>0.0}, 260, 186, bob_restarts). f(6, [waitA(_,A,_),readyB(_,A,_),stopA(_,_,_),zero(_),fresh(B),initB(_,_,_)], {B-A<-0.0}, 259, 186, rendez_vous_over_Nb_for_alice_and_bob). f(6, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),stopA(_,C,_)], {C-B>0.0}, 258, 186, rendez_vous_over_Nb_for_alice_and_bob). f(6, [create(_),zero(_),stopA(_,_,_),fresh(A),stopA(_,B,_)], {B-A>0.0}, 257, 186, create_bob). f(6, [init,stopA(_,_,_),initB(_,_,_),stopA(_,_,_)], {}, 256, 186, initialize_system). f(6, [waitA(_,A,_),readyB(_,A,_),init,create(_),genA(_,A,_)], {}, 255, 187, rendez_vous_over_Nb_for_alice_and_bob). f(6, [initA(_,_,_),fresh(A),init,create(_),stopA(_,B,_)], {B-A>0.0}, 254, 187, alice_generates_a_fresh_name). f(6, [initA(_,_,_),fresh(A),initM(_),zero(_),stopA(_,B,_)], {B-A>0.0}, 253, 188, alice_generates_a_fresh_name). f(6, [init,genA(_,A,_),stopA(_,A,_)], {}, 252, 188, initialize_system). f(6, [genB(_,A,_),fresh(_),init,genA(_,A,_),stopA(_,A,_)], {}, 251, 189, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),initA(_,_,_),initM(_),zero(_),stopA(_,A,C)], {A-C>0.0,A-B>0.0}, 250, 190, bob_generates_a_fresh_name). f(6, [init,initA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 249, 190, initialize_system). f(6, [waitA(_,A,_),readyB(_,A,B),init,stopA(_,_,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 248, 192, rendez_vous_over_Nb_for_alice_and_bob). f(6, [genB(_,A,_),fresh(_),init,stopA(_,_,_),initB(_,_,_),stopA(_,A,_)], {}, 247, 192, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),create(_),zero(_),stopA(_,_,_),stopA(_,A,C)], {A-C>0.0,A-B>0.0}, 246, 193, bob_generates_a_fresh_name). f(6, [initM(_),fresh(A),zero(_),stopA(_,_,_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 245, 193, call_create). f(6, [init,create(_),stopA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 244, 193, initialize_system). f(6, [genB(_,A,_),fresh(B),waitA(_,C,_),readyB(_,C,_),zero(_),initB(_,_,_),stopA(_,A,D)], {A-D>0.0,A-B>0.0}, 243, 194, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),waitA(_,A,_),zero(_),initB(_,_,_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-B>0.0}, 242, 194, bob_generates_a_fresh_name). f(6, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-B>0.0}, 241, 194, alice_sends_nonce_Na_to_bob). f(6, [waitA(_,A,_),readyB(_,A,B),zero(_),stopA(_,_,_),fresh(C),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 240, 195, rendez_vous_over_Nb_for_alice_and_bob). f(6, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-B>0.0}, 239, 195, rendez_vous_over_Nb_for_alice_and_bob). f(6, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),stopA(_,_,_),stopA(_,A,C)], {A-C>0.0,A-B>0.0}, 238, 195, bob_generates_a_fresh_name). f(6, [init,stopB(_,_,_),stopA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 237, 195, initialize_system). f(6, [stopA(_,_,_),zero(_),init,create(_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 236, 196, alice_restarts). f(6, [genB(_,A,_),fresh(_),init,create(_),initA(_,_,_),stopA(_,A,_)], {}, 235, 196, bob_generates_a_fresh_name). f(6, [initM(_),fresh(_),init,initA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 234, 196, call_create). f(6, [genB(_,A,_),fresh(B),create(_),zero(_),create(_),stopA(_,A,C)], {A-C>0.0,A-B>0.0}, 233, 197, bob_generates_a_fresh_name). f(6, [init,create(_),create(_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 232, 197, initialize_system). f(6, [waitA(_,A,_),readyB(_,A,B),init,create(_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 231, 198, rendez_vous_over_Nb_for_alice_and_bob). f(6, [genB(_,A,_),fresh(_),init,create(_),initB(_,_,_),stopA(_,A,_)], {}, 230, 198, bob_generates_a_fresh_name). f(6, [create(_),zero(_),init,create(_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 229, 198, create_bob). f(6, [genB(_,A,_),fresh(B),initM(_),zero(_),initB(_,_,_),stopA(_,A,C)], {A-C>0.0,A-B>0.0}, 228, 199, bob_generates_a_fresh_name). f(6, [create(_),zero(_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 227, 199, create_bob). f(6, [init,initB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 226, 199, initialize_system). f(6, [waitA(_,A,_),readyB(_,A,B),zero(_),create(_),fresh(C),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 225, 200, rendez_vous_over_Nb_for_alice_and_bob). f(6, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),create(_),stopA(_,A,C)], {A-C>0.0,A-B>0.0}, 224, 200, bob_generates_a_fresh_name). f(6, [initM(_),fresh(A),stopB(_,_,_),zero(_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 223, 200, call_create). f(6, [init,stopB(_,_,_),create(_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 222, 200, initialize_system). f(6, [stopA(_,_,_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-A>0.0}, 221, 202, alice_restarts). f(6, [genB(_,A,_),fresh(B),initA(_,_,_),waitA(_,C,_),readyB(_,C,_),zero(_),stopA(_,A,D)], {A-D>0.0,A-B>0.0}, 220, 202, bob_generates_a_fresh_name). f(6, [create(_),zero(_),fresh(A),waitA(_,B,_),readyB(_,B,_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-A>0.0}, 219, 202, create_alice). f(6, [genB(_,A,_),fresh(_),genB(_,B,_),waitA(_,B,_),zero(_),genA(_,A,_),stopA(_,A,_)], {}, 218, 203, bob_generates_a_fresh_name). f(6, [initA(_,_,_),fresh(A),genB(_,B,_),waitA(_,B,_),zero(_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-A>0.0}, 217, 203, alice_generates_a_fresh_name). f(6, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 216, 204, bob_restarts). f(6, [genB(_,A,_),fresh(_),genA(_,A,_),initB(_,_,_),readyB(_,A,_),zero(_),genA(_,A,_)], {}, 215, 204, bob_generates_a_fresh_name). f(6, [genB(_,A,_),fresh(B),genA(_,A,_),initB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 214, 204, bob_generates_a_fresh_name). f(6, [initA(_,_,_),fresh(A),initB(_,_,_),readyB(_,B,C),zero(_),genA(_,B,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 213, 204, alice_generates_a_fresh_name). f(6, [create(_),zero(_),genA(_,A,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 212, 204, create_bob). f(6, [init,genA(_,A,_),initB(_,_,_),readyB(_,A,B),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 211, 204, initialize_system). f(6, [stopA(_,_,_),zero(_),init,stopB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 210, 205, alice_restarts). f(6, [waitA(_,A,_),readyB(_,A,_),init,initA(_,_,_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0}, 209, 205, rendez_vous_over_Nb_for_alice_and_bob). f(6, [waitA(_,A,_),readyB(_,A,B),init,initA(_,_,_),readyB(_,A,C)], {C-B>0.0}, 208, 205, rendez_vous_over_Nb_for_alice_and_bob). f(6, [genB(_,A,_),fresh(_),init,initA(_,_,_),stopB(_,_,_),stopA(_,A,_)], {}, 207, 205, bob_generates_a_fresh_name). f(6, [create(_),zero(_),init,stopB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 206, 205, create_alice). f(5, [init,initA(_,_,_),stopB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 205, 35, initialize_system). f(5, [genA(_,A,_),initB(_,_,_),readyB(_,A,B),zero(_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 204, 37, alice_sends_nonce_Na_to_bob). f(5, [genB(_,A,_),fresh(_),waitA(_,A,_),zero(_),genA(_,B,_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0}, 203, 38, bob_generates_a_fresh_name). f(5, [initA(_,_,_),fresh(A),waitA(_,B,_),readyB(_,B,_),zero(_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-A>0.0}, 202, 38, alice_generates_a_fresh_name). f(5, [stopB(_,_,_),zero(_),init,initA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 201, 39, bob_restarts). f(5, [stopB(_,_,_),zero(_),create(_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 200, 40, bob_restarts). f(5, [initM(_),fresh(A),zero(_),initB(_,_,_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 199, 40, call_create). f(5, [init,create(_),initB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 198, 40, initialize_system). f(5, [create(_),zero(_),create(_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 197, 41, create_alice). f(5, [init,create(_),initA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 196, 41, initialize_system). f(5, [stopB(_,_,_),zero(_),stopA(_,_,_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 195, 44, bob_restarts). f(5, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),readyB(_,C,D),stopA(_,C,E)], {E-D<-0.0,C-B>0.0}, 194, 44, rendez_vous_over_Nb_for_alice_and_bob). f(5, [create(_),zero(_),stopA(_,_,_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 193, 44, create_bob). f(5, [init,stopA(_,_,_),initB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 192, 44, initialize_system). f(5, [initA(_,_,_),fresh(A),init,create(_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 191, 45, alice_generates_a_fresh_name). f(5, [initA(_,_,_),fresh(A),initM(_),zero(_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 190, 46, alice_generates_a_fresh_name). f(5, [init,genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 189, 46, initialize_system). f(5, [initM(_),fresh(_),zero(_),genA(_,A,_),stopA(_,A,_)], {}, 188, 49, call_create). f(5, [init,create(_),genA(_,A,_),stopA(_,A,_)], {}, 187, 49, initialize_system). f(5, [stopA(_,_,_),zero(_),fresh(A),initB(_,_,_),stopA(_,B,_)], {B-A>0.0}, 186, 50, alice_restarts). f(5, [create(_),zero(_),initA(_,_,_),fresh(A),stopA(_,B,_)], {B-A>0.0}, 185, 50, create_bob). f(5, [create(_),zero(_),fresh(A),initB(_,_,_),stopA(_,B,_)], {B-A>0.0}, 184, 50, create_alice). f(5, [init,initA(_,_,_),initB(_,_,_),stopA(_,_,_)], {}, 183, 50, initialize_system). f(5, [genA(_,A,_),initB(_,_,_),readyB(_,A,_),genA(_,A,_),initB(_,_,_),fresh(_)], {}, 182, 51, alice_sends_nonce_Na_to_bob). f(5, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),fresh(_),stopA(_,B,_)], {}, 181, 52, rendez_vous_over_Nb_for_alice_and_bob). f(5, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,A,_),fresh(_)], {}, 180, 52, rendez_vous_over_Nb_for_alice_and_bob). f(5, [initA(_,_,_),fresh(A),stopB(_,_,_),zero(_),stopA(_,B,_)], {B-A>0.0}, 179, 52, alice_generates_a_fresh_name). f(5, [init,stopB(_,_,_),genA(_,A,_),stopA(_,A,_)], {}, 178, 52, initialize_system). f(5, [init,initA(_,_,_),stopB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 177, 55, initialize_system). f(5, [genB(_,A,_),fresh(_),waitA(_,A,_),zero(_),genA(_,B,_),readyB(_,B,C),stopB(_,B,D)], {D-C>0.0}, 176, 57, bob_generates_a_fresh_name). f(5, [initA(_,_,_),fresh(A),waitA(_,B,_),readyB(_,B,_),zero(_),readyB(_,C,D),stopB(_,C,E)], {C-A>0.0,E-D>0.0}, 175, 57, alice_generates_a_fresh_name). f(5, [stopB(_,_,_),zero(_),init,initA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 174, 58, bob_restarts). f(5, [stopB(_,_,_),zero(_),create(_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 173, 59, bob_restarts). f(5, [initM(_),fresh(A),zero(_),initB(_,_,_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 172, 59, call_create). f(5, [init,create(_),initB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 171, 59, initialize_system). f(5, [create(_),zero(_),create(_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 170, 60, create_alice). f(5, [init,create(_),initA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 169, 60, initialize_system). f(5, [stopB(_,_,_),zero(_),stopA(_,_,_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 168, 62, bob_restarts). f(5, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),readyB(_,C,D),stopB(_,C,E)], {C-B>0.0,E-D>0.0}, 167, 62, rendez_vous_over_Nb_for_alice_and_bob). f(5, [create(_),zero(_),stopA(_,_,_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 166, 62, create_bob). f(5, [init,stopA(_,_,_),initB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 165, 62, initialize_system). f(5, [initA(_,_,_),fresh(A),init,create(_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 164, 63, alice_generates_a_fresh_name). f(5, [initA(_,_,_),fresh(A),initM(_),zero(_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 163, 64, alice_generates_a_fresh_name). f(5, [init,genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 162, 64, initialize_system). f(5, [waitA(_,A,_),readyB(_,A,B),init,genA(_,A,_),readyB(_,A,C)], {C-B<-0.0}, 161, 66, rendez_vous_over_Nb_for_alice_and_bob). f(5, [genB(_,A,_),fresh(B),init,stopB(_,_,_),genA(_,A,_),stopA(_,A,C)], {C-B>0.0}, 160, 66, bob_generates_a_fresh_name). f(5, [waitA(_,A,_),readyB(_,A,B),initA(_,_,_),fresh(C),zero(_),readyB(_,A,D)], {D-B<-0.0,A-C>0.0}, 159, 67, rendez_vous_over_Nb_for_alice_and_bob). f(5, [genB(_,A,_),fresh(B),initA(_,_,_),stopB(_,_,_),zero(_),stopA(_,A,C)], {B-A<-0.0,B-C<-0.0}, 158, 67, bob_generates_a_fresh_name). f(5, [init,initA(_,_,_),stopB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 157, 67, initialize_system). f(5, [genB(_,A,_),fresh(B),waitA(_,C,_),readyB(_,C,_),zero(_),genA(_,A,_),stopA(_,A,D)], {D-B>0.0}, 156, 68, bob_generates_a_fresh_name). f(5, [genB(_,A,_),fresh(_),waitA(_,A,_),zero(_),genA(_,B,_),readyB(_,B,C),stopA(_,B,D)], {D-C>0.0}, 155, 68, bob_generates_a_fresh_name). f(5, [initA(_,_,_),fresh(A),waitA(_,B,_),readyB(_,B,_),zero(_),readyB(_,C,D),stopA(_,C,E)], {C-A>0.0,E-D>0.0}, 154, 68, alice_generates_a_fresh_name). f(5, [stopB(_,_,_),zero(_),init,initA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 153, 69, bob_restarts). f(5, [genB(_,A,_),fresh(B),init,initA(_,_,_),initB(_,_,_),stopA(_,A,C)], {C-B>0.0}, 152, 69, bob_generates_a_fresh_name). f(5, [stopB(_,_,_),zero(_),create(_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 151, 70, bob_restarts). f(5, [genB(_,A,_),fresh(B),create(_),zero(_),initB(_,_,_),stopA(_,A,C)], {B-A<-0.0,B-C<-0.0}, 150, 70, bob_generates_a_fresh_name). f(5, [initM(_),fresh(A),zero(_),initB(_,_,_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 149, 70, call_create). f(5, [init,create(_),initB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 148, 70, initialize_system). f(5, [genB(_,A,_),fresh(B),create(_),zero(_),initA(_,_,_),stopA(_,A,C)], {B-A<-0.0,B-C<-0.0}, 147, 71, bob_generates_a_fresh_name). f(5, [create(_),zero(_),create(_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 146, 71, create_alice). f(5, [init,create(_),initA(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 145, 71, initialize_system). f(5, [stopB(_,_,_),zero(_),stopA(_,_,_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 144, 72, bob_restarts). f(5, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),readyB(_,C,D),stopA(_,C,E)], {C-B>0.0,E-D>0.0}, 143, 72, rendez_vous_over_Nb_for_alice_and_bob). f(5, [genB(_,A,_),fresh(B),stopA(_,_,_),zero(_),initB(_,_,_),stopA(_,A,C)], {B-A<-0.0,B-C<-0.0}, 142, 72, bob_generates_a_fresh_name). f(5, [create(_),zero(_),stopA(_,_,_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 141, 72, create_bob). f(5, [init,stopA(_,_,_),initB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 140, 72, initialize_system). f(5, [genB(_,A,_),fresh(B),init,create(_),genA(_,A,_),stopA(_,A,C)], {C-B>0.0}, 139, 73, bob_generates_a_fresh_name). f(5, [initA(_,_,_),fresh(A),init,create(_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 138, 73, alice_generates_a_fresh_name). f(5, [genB(_,A,_),fresh(B),initM(_),zero(_),genA(_,A,_),stopA(_,A,C)], {C-B>0.0}, 137, 74, bob_generates_a_fresh_name). f(5, [initA(_,_,_),fresh(A),initM(_),zero(_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 136, 74, alice_generates_a_fresh_name). f(5, [init,genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 135, 74, initialize_system). f(5, [waitA(_,A,_),readyB(_,A,B),init,stopB(_,_,_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 134, 75, rendez_vous_over_Nb_for_alice_and_bob). f(5, [waitA(_,A,_),readyB(_,A,B),initA(_,_,_),fresh(C),stopB(_,_,_),zero(_),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 133, 76, rendez_vous_over_Nb_for_alice_and_bob). f(5, [init,initA(_,_,_),stopB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 132, 76, initialize_system). f(5, [genB(_,A,_),fresh(_),waitA(_,A,_),zero(_),genA(_,B,_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0}, 131, 78, bob_generates_a_fresh_name). f(5, [initA(_,_,_),fresh(A),waitA(_,B,_),readyB(_,B,_),zero(_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-A>0.0}, 130, 78, alice_generates_a_fresh_name). f(5, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,B),genA(_,A,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 129, 79, bob_restarts). f(5, [genB(_,A,_),fresh(_),genA(_,A,_),initB(_,_,_),readyB(_,A,_),genA(_,A,_),initB(_,_,_)], {}, 128, 79, bob_generates_a_fresh_name). f(5, [genB(_,A,_),fresh(B),genA(_,A,_),initB(_,_,_),genA(_,A,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 127, 79, bob_generates_a_fresh_name). f(5, [initA(_,_,_),fresh(A),initB(_,_,_),readyB(_,B,C),genA(_,B,_),initB(_,_,_),readyB(_,B,D)], {B-A>0.0,D-C>0.0}, 126, 79, alice_generates_a_fresh_name). f(5, [create(_),zero(_),genA(_,A,_),readyB(_,A,B),genA(_,A,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 125, 79, create_bob). f(5, [stopB(_,_,_),zero(_),init,initA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 124, 80, bob_restarts). f(5, [waitA(_,A,_),readyB(_,A,B),init,initA(_,_,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 123, 80, rendez_vous_over_Nb_for_alice_and_bob). f(5, [stopB(_,_,_),zero(_),create(_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 122, 81, bob_restarts). f(5, [initM(_),fresh(A),zero(_),initB(_,_,_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 121, 81, call_create). f(5, [init,create(_),initB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 120, 81, initialize_system). f(5, [waitA(_,A,_),readyB(_,A,B),create(_),zero(_),initA(_,_,_),fresh(C),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 119, 82, rendez_vous_over_Nb_for_alice_and_bob). f(5, [create(_),zero(_),create(_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 118, 82, create_alice). f(5, [init,create(_),initA(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 117, 82, initialize_system). f(5, [stopB(_,_,_),zero(_),stopA(_,_,_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 116, 84, bob_restarts). f(5, [waitA(_,A,_),readyB(_,A,_),zero(_),fresh(B),initB(_,_,_),readyB(_,C,D),stopB(_,C,E)], {E-D<-0.0,C-B>0.0}, 115, 84, rendez_vous_over_Nb_for_alice_and_bob). f(5, [waitA(_,A,_),readyB(_,A,B),zero(_),fresh(C),initB(_,_,_),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 114, 84, rendez_vous_over_Nb_for_alice_and_bob). f(5, [create(_),zero(_),stopA(_,_,_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 113, 84, create_bob). f(5, [init,stopA(_,_,_),initB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 112, 84, initialize_system). f(5, [waitA(_,A,_),readyB(_,A,B),init,create(_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 111, 85, rendez_vous_over_Nb_for_alice_and_bob). f(5, [initA(_,_,_),fresh(A),init,create(_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 110, 85, alice_generates_a_fresh_name). f(5, [initA(_,_,_),fresh(A),initM(_),zero(_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 109, 86, alice_generates_a_fresh_name). f(5, [init,genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 108, 86, initialize_system). f(5, [genA(_,A,_),initB(_,_,_),fresh(_),genB(_,A,_),waitA(_,A,_)], {}, 107, 88, alice_sends_nonce_Na_to_bob). f(5, [init,genB(_,A,_),waitA(_,A,_),genB(_,A,_),waitA(_,A,_)], {}, 106, 88, initialize_system). f(5, [waitA(_,A,_),readyB(_,A,_),init,genA(_,A,_),initB(_,_,_)], {}, 105, 89, rendez_vous_over_Nb_for_alice_and_bob). f(5, [waitA(_,A,_),readyB(_,A,_),create(_),zero(_),genA(_,A,_),fresh(_)], {}, 104, 90, rendez_vous_over_Nb_for_alice_and_bob). f(5, [initM(_),fresh(_),zero(_),genA(_,A,_),stopB(_,A,_)], {}, 103, 90, call_create). f(5, [init,create(_),genA(_,A,_),stopB(_,A,_)], {}, 102, 90, initialize_system). f(5, [stopA(_,_,_),zero(_),fresh(A),initB(_,_,_),stopB(_,B,_)], {B-A>0.0}, 101, 91, alice_restarts). f(5, [waitA(_,A,_),readyB(_,A,_),initA(_,_,_),fresh(B),initB(_,_,_)], {B-A<-0.0}, 100, 91, rendez_vous_over_Nb_for_alice_and_bob). f(5, [create(_),zero(_),initA(_,_,_),fresh(A),stopB(_,B,_)], {B-A>0.0}, 99, 91, create_bob). f(5, [create(_),zero(_),fresh(A),initB(_,_,_),stopB(_,B,_)], {B-A>0.0}, 98, 91, create_alice). f(5, [init,initA(_,_,_),initB(_,_,_),stopB(_,_,_)], {}, 97, 91, initialize_system). f(5, [waitA(_,A,_),readyB(_,A,_),stopB(_,_,_),zero(_),genA(_,A,_),fresh(_)], {}, 96, 92, rendez_vous_over_Nb_for_alice_and_bob). f(5, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),fresh(_),stopB(_,B,_)], {}, 95, 92, rendez_vous_over_Nb_for_alice_and_bob). f(5, [initA(_,_,_),fresh(A),stopB(_,_,_),zero(_),stopB(_,B,_)], {B-A>0.0}, 94, 92, alice_generates_a_fresh_name). f(5, [init,stopB(_,_,_),genA(_,A,_),stopB(_,A,_)], {}, 93, 92, initialize_system). f(4, [stopB(_,_,_),zero(_),genA(_,A,_),fresh(_),stopB(_,A,_)], {}, 92, 16, bob_restarts). f(4, [initA(_,_,_),fresh(A),initB(_,_,_),stopB(_,B,_)], {B-A>0.0}, 91, 16, alice_generates_a_fresh_name). f(4, [create(_),zero(_),genA(_,A,_),fresh(_),stopB(_,A,_)], {}, 90, 16, create_bob). f(4, [init,genA(_,A,_),initB(_,_,_),stopB(_,A,_)], {}, 89, 16, initialize_system). f(4, [genB(_,A,_),fresh(_),waitA(_,A,_),genB(_,A,_),waitA(_,A,_)], {}, 88, 17, bob_generates_a_fresh_name). f(4, [genB(_,A,_),fresh(_),create(_),zero(_),genA(_,A,_),stopB(_,A,_)], {}, 87, 18, bob_generates_a_fresh_name). f(4, [initM(_),fresh(_),zero(_),genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 86, 18, call_create). f(4, [init,create(_),genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 85, 18, initialize_system). f(4, [stopA(_,_,_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 84, 19, alice_restarts). f(4, [genB(_,A,_),fresh(B),initA(_,_,_),initB(_,_,_),stopB(_,A,C)], {A-C>0.0,A-B>0.0}, 83, 19, bob_generates_a_fresh_name). f(4, [create(_),zero(_),initA(_,_,_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 82, 19, create_bob). f(4, [create(_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 81, 19, create_alice). f(4, [init,initA(_,_,_),initB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 80, 19, initialize_system). f(4, [genA(_,A,_),initB(_,_,_),readyB(_,A,B),genA(_,A,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 79, 20, alice_sends_nonce_Na_to_bob). f(4, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0}, 78, 21, rendez_vous_over_Nb_for_alice_and_bob). f(4, [genB(_,A,_),fresh(_),stopB(_,_,_),zero(_),genA(_,A,_),stopB(_,A,_)], {}, 77, 21, bob_generates_a_fresh_name). f(4, [initA(_,_,_),fresh(A),stopB(_,_,_),zero(_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 76, 21, alice_generates_a_fresh_name). f(4, [init,stopB(_,_,_),genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 75, 21, initialize_system). f(4, [initM(_),fresh(_),zero(_),genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 74, 22, call_create). f(4, [init,create(_),genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 73, 22, initialize_system). f(4, [stopA(_,_,_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 72, 23, alice_restarts). f(4, [create(_),zero(_),initA(_,_,_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 71, 23, create_bob). f(4, [create(_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 70, 23, create_alice). f(4, [init,initA(_,_,_),initB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 69, 23, initialize_system). f(4, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),readyB(_,B,C),stopA(_,B,D)], {D-C>0.0}, 68, 25, rendez_vous_over_Nb_for_alice_and_bob). f(4, [initA(_,_,_),fresh(A),stopB(_,_,_),zero(_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 67, 25, alice_generates_a_fresh_name). f(4, [init,stopB(_,_,_),genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 66, 25, initialize_system). f(4, [genB(_,A,_),fresh(B),create(_),zero(_),genA(_,A,_),stopB(_,A,C)], {C-B>0.0}, 65, 26, bob_generates_a_fresh_name). f(4, [initM(_),fresh(_),zero(_),genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 64, 26, call_create). f(4, [init,create(_),genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 63, 26, initialize_system). f(4, [stopA(_,_,_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 62, 27, alice_restarts). f(4, [genB(_,A,_),fresh(B),initA(_,_,_),initB(_,_,_),stopB(_,A,C)], {B-A<-0.0,B-C<-0.0}, 61, 27, bob_generates_a_fresh_name). f(4, [create(_),zero(_),initA(_,_,_),fresh(A),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 60, 27, create_bob). f(4, [create(_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 59, 27, create_alice). f(4, [init,initA(_,_,_),initB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 58, 27, initialize_system). f(4, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),readyB(_,B,C),stopB(_,B,D)], {D-C>0.0}, 57, 28, rendez_vous_over_Nb_for_alice_and_bob). f(4, [genB(_,A,_),fresh(B),stopB(_,_,_),zero(_),genA(_,A,_),stopB(_,A,C)], {C-B>0.0}, 56, 28, bob_generates_a_fresh_name). f(4, [initA(_,_,_),fresh(A),stopB(_,_,_),zero(_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 55, 28, alice_generates_a_fresh_name). f(4, [init,stopB(_,_,_),genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 54, 28, initialize_system). f(4, [waitA(_,A,_),readyB(_,A,_),init,genB(_,A,_),waitA(_,A,_)], {}, 53, 29, rendez_vous_over_Nb_for_alice_and_bob). f(4, [stopB(_,_,_),zero(_),genA(_,A,_),fresh(_),stopA(_,A,_)], {}, 52, 30, bob_restarts). f(4, [waitA(_,A,_),readyB(_,A,_),genA(_,A,_),initB(_,_,_),fresh(_)], {}, 51, 30, rendez_vous_over_Nb_for_alice_and_bob). f(4, [initA(_,_,_),fresh(A),initB(_,_,_),stopA(_,B,_)], {B-A>0.0}, 50, 30, alice_generates_a_fresh_name). f(4, [create(_),zero(_),genA(_,A,_),fresh(_),stopA(_,A,_)], {}, 49, 30, create_bob). f(4, [init,genA(_,A,_),initB(_,_,_),stopA(_,A,_)], {}, 48, 30, initialize_system). f(4, [genB(_,A,_),fresh(_),create(_),zero(_),genA(_,A,_),stopA(_,A,_)], {}, 47, 31, bob_generates_a_fresh_name). f(4, [initM(_),fresh(_),zero(_),genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 46, 31, call_create). f(4, [init,create(_),genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 45, 31, initialize_system). f(4, [stopA(_,_,_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 44, 32, alice_restarts). f(4, [waitA(_,A,_),readyB(_,A,B),initA(_,_,_),fresh(C),initB(_,_,_),readyB(_,A,D)], {D-B>0.0,A-C>0.0}, 43, 32, rendez_vous_over_Nb_for_alice_and_bob). f(4, [genB(_,A,_),fresh(B),initA(_,_,_),initB(_,_,_),stopA(_,A,C)], {A-C>0.0,A-B>0.0}, 42, 32, bob_generates_a_fresh_name). f(4, [create(_),zero(_),initA(_,_,_),fresh(A),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 41, 32, create_bob). f(4, [create(_),zero(_),fresh(A),initB(_,_,_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 40, 32, create_alice). f(4, [init,initA(_,_,_),initB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 39, 32, initialize_system). f(4, [waitA(_,A,_),readyB(_,A,_),zero(_),genA(_,B,_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0}, 38, 33, rendez_vous_over_Nb_for_alice_and_bob). f(4, [waitA(_,A,_),readyB(_,A,B),zero(_),genA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 37, 33, rendez_vous_over_Nb_for_alice_and_bob). f(4, [genB(_,A,_),fresh(_),stopB(_,_,_),zero(_),genA(_,A,_),stopA(_,A,_)], {}, 36, 33, bob_generates_a_fresh_name). f(4, [initA(_,_,_),fresh(A),stopB(_,_,_),zero(_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 35, 33, alice_generates_a_fresh_name). f(4, [init,stopB(_,_,_),genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 34, 33, initialize_system). f(3, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 33, 7, bob_restarts). f(3, [initA(_,_,_),fresh(A),initB(_,_,_),readyB(_,B,C),stopA(_,B,D)], {D-C<-0.0,B-A>0.0}, 32, 7, alice_generates_a_fresh_name). f(3, [create(_),zero(_),genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 31, 7, create_bob). f(3, [genA(_,A,_),initB(_,_,_),fresh(_),stopA(_,A,_)], {}, 30, 8, alice_sends_nonce_Na_to_bob). f(3, [init,genB(_,A,_),waitA(_,A,_),stopA(_,A,_)], {}, 29, 8, initialize_system). f(3, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 28, 10, bob_restarts). f(3, [initA(_,_,_),fresh(A),initB(_,_,_),readyB(_,B,C),stopB(_,B,D)], {B-A>0.0,D-C>0.0}, 27, 10, alice_generates_a_fresh_name). f(3, [create(_),zero(_),genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 26, 10, create_bob). f(3, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 25, 12, bob_restarts). f(3, [genB(_,A,_),fresh(B),genA(_,A,_),initB(_,_,_),stopA(_,A,C)], {C-B>0.0}, 24, 12, bob_generates_a_fresh_name). f(3, [initA(_,_,_),fresh(A),initB(_,_,_),readyB(_,B,C),stopA(_,B,D)], {B-A>0.0,D-C>0.0}, 23, 12, alice_generates_a_fresh_name). f(3, [create(_),zero(_),genA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 22, 12, create_bob). f(3, [stopB(_,_,_),zero(_),genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 21, 13, bob_restarts). f(3, [waitA(_,A,_),readyB(_,A,B),genA(_,A,_),initB(_,_,_),readyB(_,A,C)], {C-B>0.0}, 20, 13, rendez_vous_over_Nb_for_alice_and_bob). f(3, [initA(_,_,_),fresh(A),initB(_,_,_),readyB(_,B,C),stopB(_,B,D)], {D-C<-0.0,B-A>0.0}, 19, 13, alice_generates_a_fresh_name). f(3, [create(_),zero(_),genA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 18, 13, create_bob). f(3, [waitA(_,A,_),readyB(_,A,_),genB(_,A,_),fresh(_),waitA(_,A,_)], {}, 17, 14, rendez_vous_over_Nb_for_alice_and_bob). f(3, [genA(_,A,_),initB(_,_,_),fresh(_),stopB(_,A,_)], {}, 16, 14, alice_sends_nonce_Na_to_bob). f(3, [init,genB(_,A,_),waitA(_,A,_),stopB(_,A,_)], {}, 15, 14, initialize_system). f(2, [genB(_,A,_),fresh(_),waitA(_,A,_),stopB(_,A,_)], {}, 14, 3, bob_generates_a_fresh_name). f(2, [genA(_,A,_),initB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 13, 3, alice_sends_nonce_Na_to_bob). f(2, [genA(_,A,_),initB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 12, 4, alice_sends_nonce_Na_to_bob). f(2, [genB(_,A,_),fresh(B),waitA(_,A,_),stopB(_,A,C)], {C-B>0.0}, 11, 5, bob_generates_a_fresh_name). f(2, [genA(_,A,_),initB(_,_,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 10, 5, alice_sends_nonce_Na_to_bob). f(2, [waitA(_,A,_),readyB(_,A,B),waitA(_,A,_),readyB(_,A,C)], {C-B>0.0}, 9, 6, rendez_vous_over_Nb_for_alice_and_bob). f(2, [genB(_,A,_),fresh(_),waitA(_,A,_),stopA(_,A,_)], {}, 8, 6, bob_generates_a_fresh_name). f(2, [genA(_,A,_),initB(_,_,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 7, 6, alice_sends_nonce_Na_to_bob). f(1, [waitA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B<-0.0}, 6, 2, rendez_vous_over_Nb_for_alice_and_bob). f(1, [waitA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B>0.0}, 5, 2, rendez_vous_over_Nb_for_alice_and_bob). f(1, [waitA(_,A,_),readyB(_,A,B),stopA(_,A,C)], {C-B>0.0}, 4, 1, rendez_vous_over_Nb_for_alice_and_bob). f(1, [waitA(_,A,_),readyB(_,A,B),stopB(_,A,C)], {C-B<-0.0}, 3, 1, rendez_vous_over_Nb_for_alice_and_bob). f(0, [stopA(_,A,B),stopB(_,A,C)], {B>C}, 1, 0, 0). f(0, [stopA(_,A,B),stopB(_,A,C)], {B