[Toss-devel-svn] SF.net SVN: toss:[1567] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1567] trunk/Toss
|
From: <luk...@us...> - 2011-09-14 01:01:00
|
Revision: 1567
http://toss.svn.sourceforge.net/toss/?rev=1567&view=rev
Author: lukaszkaiser
Date: 2011-09-14 01:00:51 +0000 (Wed, 14 Sep 2011)
Log Message:
-----------
Moving translate examples testing to OUnit, correcting parsing, adding timeouts and new examples.
Modified Paths:
--------------
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/GGP/GDL.ml
trunk/Toss/GGP/GDL.mli
trunk/Toss/GGP/GDLParser.mly
trunk/Toss/GGP/KIFLexer.mll
trunk/Toss/GGP/Makefile
trunk/Toss/GGP/TranslateGame.ml
trunk/Toss/GGP/TranslateGame.mli
trunk/Toss/GGP/TranslateGameTest.ml
Added Paths:
-----------
trunk/Toss/GGP/examples/ad_game_2x2.gdl
trunk/Toss/GGP/examples/aipsrovers01.gdl
trunk/Toss/GGP/examples/asteroids.gdl
trunk/Toss/GGP/examples/asteroidsparallel.gdl
trunk/Toss/GGP/examples/asteroidsserial.gdl
Removed Paths:
-------------
trunk/Toss/GGP/examples/3qbf-5cnf-20var-40cl.1.qdimacs.SAT.gdl
trunk/Toss/GGP/examples/3qbf-5cnf-20var-40cl.1.qdimacs.viz.SAT.gdl
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/Formula/Aux.ml 2011-09-14 01:00:51 UTC (rev 1567)
@@ -691,6 +691,11 @@
with End_of_file -> ());
Buffer.contents buf
+let list_dir dirname =
+ let files, dir_handle = (ref [], Unix.opendir dirname) in
+ let rec add () = files := (Unix.readdir dir_handle) :: !files; add () in
+ try add () with End_of_file -> Unix.closedir dir_handle; !files
+
let is_space c =
c = '\n' || c = '\r' || c = ' ' || c = '\t'
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/Formula/Aux.mli 2011-09-14 01:00:51 UTC (rev 1567)
@@ -332,6 +332,9 @@
(** Input a file to a string. *)
val input_file : in_channel -> string
+(** List the contents of a directory *)
+val list_dir : string -> string list
+
(** Extracting the [Content-length] field and input the content of
an HTTP message. Return the pair: header first, content next. *)
val input_http_message : in_channel -> string * string * (string * string) list
Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/GGP/GDL.ml 2011-09-14 01:00:51 UTC (rev 1567)
@@ -12,6 +12,13 @@
let debug_level = ref 0
let playout_fixpoint = ref true
+(** Timeout functions *)
+let timeout = ref (fun () -> false)
+let set_timeout f = timeout := f
+let check_timeout ?(print=true) msg =
+ if print && !debug_level > 1 then print_endline ("TimeoutCheck: " ^ msg);
+ if !timeout () then (timeout := (fun () -> false); raise (Aux.Timeout msg))
+
type term =
| Const of string
| Var of string
@@ -675,6 +682,7 @@
cls
let rec run_clauses a p sc fc sb =
+ check_timeout ~print:false "GDL: run_clauses";
match a with
| Distinct ts ->
(try
@@ -828,6 +836,7 @@
| Disj disj as l ->
List.fold_left (+) 0 (List.map (fst -| branching_f) disj), l
| _ -> assert false in
+ check_timeout ~print:false "GDL: optimize_goal";
let posi = List.map branching_f posi in
let posi = List.sort (fun (i,_) (j,_) -> i-j) posi in
ground @ unif @ List.map snd posi @ nega
@@ -1160,6 +1169,7 @@
let playout_satur ~aggregate players horizon rules =
(* separate and precompute the static part *)
let rec separate static_rels state_rels =
+ check_timeout "GDL: playout_satur: separate";
let static, more_state =
List.partition (fun rel ->
List.for_all (fun ((rule,_), body, neg_body) ->
@@ -1183,6 +1193,7 @@
(* head, body, [] *)
| rule -> rule) dynamic_rules in
let rec loop actions_accu state_accu step state =
+ check_timeout ("GDL: playout_satur: loop step " ^ (string_of_int step));
(* {{{ log entry *)
if !debug_level > 0 then (
Printf.printf "playout: step %d...\n%!" step
@@ -1327,6 +1338,7 @@
Printf.printf "playout_prolog: step %d...\n%!" step
);
(* }}} *)
+ check_timeout ("GDL: playout_prolog: step " ^ (string_of_int step));
(let try actions, next =
ply_prolog ~aggregate players state program in
(* {{{ log entry *)
Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/GGP/GDL.mli 2011-09-14 01:00:51 UTC (rev 1567)
@@ -3,6 +3,7 @@
val debug_level : int ref
val playout_fixpoint : bool ref
+val set_timeout : (unit -> bool) -> unit
(** {3 Datalog programs: Type definitions and saturation.} *)
Modified: trunk/Toss/GGP/GDLParser.mly
===================================================================
--- trunk/Toss/GGP/GDLParser.mly 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/GGP/GDLParser.mly 2011-09-14 01:00:51 UTC (rev 1567)
@@ -9,9 +9,8 @@
%token <string> SEQVAR
%token OPEN CLOSE COMMA QUOTE BACKQUOTE DBLQUOTE SHARP DOT
%token NOT_EQ NOT AND OR IMPL REVIMPL EQUIV LISTOF SETOF QUOTE_KWD
-%token IF COND THE SETOFALL KAPPA LAMBDA RULE_RIGHT RULE_LEFT CONSIS
-%token DEFOBJECT DEFUNCTION DEFRELATION ASSIGN ASSIGN_IMPLIES ASSIGN_AND
-%token FORALL EXISTS EOF
+%token IF COND SETOFALL KAPPA LAMBDA RULE_RIGHT RULE_LEFT CONSIS
+%token DEFOBJECT DEFUNCTION DEFRELATION ASSIGN ASSIGN_IMPLIES ASSIGN_AND EOF
%start parse_game_description parse_request parse_term parse_literal_list
Modified: trunk/Toss/GGP/KIFLexer.mll
===================================================================
--- trunk/Toss/GGP/KIFLexer.mll 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/GGP/KIFLexer.mll 2011-09-14 01:00:51 UTC (rev 1567)
@@ -36,8 +36,6 @@
| ASSIGN
| ASSIGN_IMPLIES
| ASSIGN_AND
- | FORALL
- | EXISTS
| EOF
let reset_as_file lexbuf s =
@@ -123,8 +121,6 @@
| "IF" { IF }
| "cond" { COND }
| "COND" { COND }
- | "the" { THE }
- | "THE" { THE }
| "setofall" { SETOFALL }
| "SETOFALL" { SETOFALL }
| "kappa" { KAPPA }
@@ -144,10 +140,6 @@
| ":=" { ASSIGN }
| ":=>" { ASSIGN_IMPLIES }
| ":&" { ASSIGN_AND }
- | "forall" { FORALL }
- | "FORALL" { FORALL }
- | "exists" { EXISTS }
- | "EXISTS" { EXISTS }
| ['!' '$' '%' '&' '*' '+' '-' '/' '0'-'9' ':' '<' '>'
'A'-'Z' '[' ']' '^' '_' 'a'-'z' '{' '|' '}' '~'] as s
{WORD (Char.escaped s)}
Modified: trunk/Toss/GGP/Makefile
===================================================================
--- trunk/Toss/GGP/Makefile 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/GGP/Makefile 2011-09-14 01:00:51 UTC (rev 1567)
@@ -42,7 +42,9 @@
@-ulimit -t $(TESTTIME); ../TranslateGameTest.native -v -f $< > /dev/null
@echo ''
-translate_all: $(addsuffix .translate, $(GDL_GAMES))
+translate_all:
+ make -C .. GGP/TranslateGameTest.native
+ ../TranslateGameTest.native -t examples/ -s $(TESTTIME)
.PHONY: clean
Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/GGP/TranslateGame.ml 2011-09-14 01:00:51 UTC (rev 1567)
@@ -35,6 +35,14 @@
let debug_level = ref 0
let generate_test_case = ref None
+(** Timeout functions *)
+let timeout = ref (fun () -> false)
+let set_timeout f = (timeout := f; GDL.set_timeout f)
+let check_timeout ?(print=true) msg =
+ if print && !debug_level > 1 then print_endline ("TimeoutCheck: " ^ msg);
+ if !timeout () then (timeout := (fun () -> false); raise (Aux.Timeout msg))
+
+
(** Refine fluent paths to always point to some leaf, keeping the same
coverage of leafs on all ground state terms. *)
let refine_leaf_f_paths = ref false
@@ -242,6 +250,7 @@
Aux.sorted_merge (Aux.unique_sorted st) acc) []
(terminal_state::agg_states) in
let init_state = List.hd agg_states in
+ check_timeout "TranslateGame: create_init_struc: init_state";
let arities =
("EQ_", 2)::
Aux.unique_sorted
@@ -575,6 +584,7 @@
| Pos (Does (dp, d)) when dp = p -> Some d
| _ -> None) body in
let sb = unify_all sb djs in
+ check_timeout ~print:false "TranslateGame: move_tuples: does_facts: sb";
let d =
match djs with
| [] ->
@@ -583,9 +593,9 @@
| d::_ -> subst sb d in
sb, d::dis
) players ([], []) in
+ check_timeout "TranslateGame: move_tuples: start";
let next_cls =
- if mode = `Environment
- then
+ if mode = `Environment then
Aux.map_some (fun (_,_,body as cl) ->
if List.exists
(function Pos (Does _) | Neg (Does _) -> true | _ -> false) body
@@ -598,6 +608,7 @@
subst_fnextcl sb cl, ds) next_cls in
(* selecting $\ol{\calC},\ol{\calN}$ clauses with
$\sigma_{\ol{\calC},\ol{\calN}}$ applied *)
+ check_timeout "TranslateGame: move_tuples: next_cls";
let tup_unifies ts1 ts2 =
try ignore (unify [] ts1 ts2); true
with Not_found -> false in
@@ -625,6 +636,7 @@
| _, [] -> assert false in
let cl_tups =
coverage (next_clauses, [[], cs, []]) in
+ check_timeout "TranslateGame: move_tuples: cl_tups";
let maximality cl_tup =
List.fold_left (fun (sb, tup_ds, n_cls as cl_tup) (n_cl, ds) ->
if List.mem n_cl n_cls then cl_tup
@@ -658,6 +670,7 @@
let add_erasure_clauses f_paths (legal_tup, next_cls) =
let fixed_vars = terms_vars (Aux.array_map_of_list fst legal_tup) in
+ check_timeout "TranslateGame: add_erasure_clauses: start";
(* {{{ log entry *)
if !debug_level > 2 then (
Printf.printf "add_erasure_clauses: fixed_vars=%s\n%!"
@@ -692,6 +705,7 @@
| (s, body)::more_cls, [] ->
coverage (more_cls, [[], s, [body]]) in
let frames = coverage (frame_cls, []) in
+ check_timeout "TranslateGame: add_erasure_clauses: basic frames";
let maximality frame =
List.fold_left (fun (sb, s_acc, bodies as frame) (s, body) ->
if List.mem body bodies then frame
@@ -712,7 +726,8 @@
List.filter
(function Pos (True t) when t=s -> false | _ -> true) body in
List.map (fun (s, bodies) ->
- s, List.map (filter_out s) bodies) frames in
+ s, List.map (filter_out s) bodies) frames in
+ check_timeout "TranslateGame: add_erasure_clauses: frames filtered";
(* {{{ log entry *)
if !debug_level > 2 then (
Printf.printf "add_erasure_clauses: frames --\n%!";
@@ -1119,6 +1134,7 @@
num_not_noops = 1
|| (num_not_noops = 0 && not !noops_not_moves))
legal_tuples in
+ check_timeout "TranslateGame: turnbased_rule_cases: legal tuples";
(* {{{ log entry *)
if !debug_level > 2 then (
Printf.printf "turnbased_rule_cases: legal_tuples --\n%!";
@@ -1131,6 +1147,7 @@
let move_tups =
process_rule_cands
used_vars f_paths next_cls `General players legal_tuples in
+ check_timeout "TranslateGame: turnbased_rule_cases: processed rule cands";
let rules = Aux.concat_map
(add_legal_cond counters num_functors static_rels
testground program playout_states) move_tups in
@@ -1154,6 +1171,7 @@
used_vars f_paths next_cls `Concurrent [player] legal_tuples in
player, move_tups
) players legal_by_player in
+ check_timeout "TranslateGame: concurrent_rule_cases";
let player_rules = List.map
(fun (player, move_tups) ->
player, Aux.concat_map
@@ -2019,15 +2037,21 @@
| _ -> None
) clauses in
let players = Array.of_list players in
+ check_timeout "TranslateGame: players";
let program = preprocess_program clauses in
+ check_timeout "TranslateGame: preprocessed clauses";
let init_state = List.map (fun (_,args) -> args.(0))
(run_prolog_atom ("init", [|Var "x"|]) program) in
+ check_timeout "TranslateGame: init_state";
let testground =
replace_rel_in_program "true" (state_cls init_state) program in
+ check_timeout "TranslateGame: testground";
let program = optimize_program ~testground program in
+ check_timeout "TranslateGame: optimized program";
let playout_states = generate_playout_states program players in
(* We also detect and remove the goal clauses that use counters to
determine values, not to expand their goal value variables later. *)
+ check_timeout "TranslateGame: generated playout";
let counter_inits, counter_cls, goal_cls_w_counters,
num_functions, clauses = detect_counters clauses in
(* {{{ log entry *)
@@ -2047,6 +2071,7 @@
let clauses = ground_goal_values ground_state_terms clauses in
(* Now, we can add back the separated clauses. *)
let clauses = counter_cls @ goal_cls_w_counters @ clauses in
+ check_timeout "TranslateGame: basic clauses";
let ground_at paths = List.map
(fun p ->
p, Aux.unique_sorted
@@ -2060,6 +2085,7 @@
else body in
let clauses =
GDL.ground_vars_at_paths prepare_lits ground_at_f_paths clauses in
+ check_timeout "TranslateGame: clauses";
let defined_rels = Aux.list_diff defined_rels
["goal"; "legal"; "next"] in
let defined_rels, clauses = elim_ground_args defined_rels clauses in
@@ -2069,6 +2095,7 @@
| ("next",[|s_C|]),body_C -> Some (s_C, false, body_C)
| _ -> None)
clauses in
+ check_timeout "TranslateGame: defined rels";
(* For determining turn-based we can use the original program, but
for filtering the rule candidates we need the transformed
clauses. We restore the frame clauses. *)
@@ -2090,12 +2117,14 @@
replace_rel_in_program "true" (state_cls init_state) program in
let static_rels, nonstatic_rels =
static_rels (defs_of_rules (Aux.concat_map rules_of_clause clauses)) in
+ check_timeout "TranslateGame: static rels";
let counters = List.map fst counter_inits
and num_functors = List.map fst num_functions in
let rule_cands, is_concurrent =
create_rule_cands counters num_functors static_rels turn_data
used_vars f_paths
testground program playout_states next_cls clauses in
+ check_timeout "TranslateGame: first rule cands";
(* optimize candidates for fast pruning *)
let rule_cands =
let process cands = List.map
Modified: trunk/Toss/GGP/TranslateGame.mli
===================================================================
--- trunk/Toss/GGP/TranslateGame.mli 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/GGP/TranslateGame.mli 2011-09-14 01:00:51 UTC (rev 1567)
@@ -1,6 +1,7 @@
(** Local level of logging. *)
val debug_level : int ref
val generate_test_case : string option ref
+val set_timeout : (unit -> bool) -> unit
(** two heuristics for selecting defined relations: select relations
with arity smaller than three; or, select relations that have ground
Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/GGP/TranslateGameTest.ml 2011-09-14 01:00:51 UTC (rev 1567)
@@ -362,6 +362,34 @@
(* failwith "generated"; *)
()
+let translate_file fname =
+ try
+ let descr = load_rules fname in
+ let gdl_data, result =
+ TranslateGame.translate_game ~playing_as:(GDL.Const "") descr in
+ (true, Arena.state_str result)
+ with
+ | Aux.Timeout msg -> (false, "Timeout: " ^ msg)
+ | _ -> (false, "Failed")
+
+let translate_dir_tests dirname timeout =
+ let is_gdl fn = (String.length fn > 4) &&
+ String.sub fn ((String.length fn) - 4) 4 = ".gdl" in
+ let files = List.sort compare (List.filter is_gdl (Aux.list_dir dirname)) in
+ let mk_tst fname =
+ (fname ^ " (" ^ (string_of_int timeout) ^ "s)") >::
+ (fun () ->
+ let start = Unix.gettimeofday () in
+ TranslateGame.set_timeout
+ (fun () -> Unix.gettimeofday() -. start > float (timeout));
+ let res, msg = translate_file (dirname ^ fname) in
+ let t = Unix.gettimeofday() -. start in
+ let final = if res then Printf.sprintf "Suceeded (%f sec.)\n%!" t else
+ Printf.sprintf "%s (%f sec)\n%!" msg t in
+ assert_bool final res
+ ) in
+ ("TranslateGame " ^ dirname) >::: (List.map mk_tst files)
+
let exec () =
Aux.run_test_if_target "TranslateGameTest"
("TranslateGame" >::: [tests; bigtests])
@@ -369,17 +397,20 @@
let main () =
Aux.set_optimized_gc ();
- let (file) = (ref "") in
+ let (file, testdir, timeout) = (ref "", ref "", ref 45) in
let opts = [
("-v", Arg.Unit (fun () -> set_debug_level 1), "be verbose");
("-d", Arg.Int (fun i -> set_debug_level i), "set debug level");
("-f", Arg.String (fun s -> file := s), "process file");
+ ("-t", Arg.String (fun s -> testdir:= s), "run all tests from a directory");
+ ("-s", Arg.Int (fun i -> timeout := i), "set timeout for tests (seconds)");
] in
Arg.parse opts (fun _ -> ()) "Try -help for help or one of the following.";
- if !file = "" then exec () else
- let descr = load_rules !file in
- let gdl_data, result =
- TranslateGame.translate_game ~playing_as:(GDL.Const "") descr in
- print_endline (Arena.state_str result)
+ if !file <> "" then
+ print_endline (snd (translate_file !file))
+ else if !testdir <> "" then
+ Aux.run_test_if_target "TranslateGameTest"
+ (translate_dir_tests !testdir !timeout)
+ else exec ()
let _ = Aux.run_if_target "TranslateGameTest" main
Deleted: trunk/Toss/GGP/examples/3qbf-5cnf-20var-40cl.1.qdimacs.SAT.gdl
===================================================================
--- trunk/Toss/GGP/examples/3qbf-5cnf-20var-40cl.1.qdimacs.SAT.gdl 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/GGP/examples/3qbf-5cnf-20var-40cl.1.qdimacs.SAT.gdl 2011-09-14 01:00:51 UTC (rev 1567)
@@ -1,578 +0,0 @@
-(contains 1 (not 1))
-(contains 1 52)
-(contains 1 16)
-(contains 1 4)
-(contains 1 (not 27))
-(contains 2 (not 27))
-(contains 2 (not 51))
-(contains 2 19)
-(contains 2 1)
-(contains 2 30)
-(contains 3 35)
-(contains 3 52)
-(contains 3 (not 41))
-(contains 3 (not 18))
-(contains 3 (not 59))
-(contains 4 24)
-(contains 4 30)
-(contains 4 20)
-(contains 4 (not 7))
-(contains 4 (not 23))
-(contains 5 (not 34))
-(contains 5 (not 4))
-(contains 5 13)
-(contains 5 (not 49))
-(contains 5 (not 17))
-(contains 6 51)
-(contains 6 (not 37))
-(contains 6 1)
-(contains 6 5)
-(contains 6 (not 29))
-(contains 7 (not 2))
-(contains 7 (not 7))
-(contains 7 (not 53))
-(contains 7 (not 12))
-(contains 7 (not 35))
-(contains 8 (not 39))
-(contains 8 (not 44))
-(contains 8 28)
-(contains 8 (not 2))
-(contains 8 51)
-(contains 9 (not 21))
-(contains 9 (not 11))
-(contains 9 8)
-(contains 9 (not 20))
-(contains 9 2)
-(contains 10 (not 37))
-(contains 10 (not 21))
-(contains 10 58)
-(contains 10 (not 59))
-(contains 10 7)
-(contains 11 33)
-(contains 11 59)
-(contains 11 (not 41))
-(contains 11 52)
-(contains 11 21)
-(contains 12 43)
-(contains 12 35)
-(contains 12 (not 7))
-(contains 12 33)
-(contains 12 50)
-(contains 13 29)
-(contains 13 45)
-(contains 13 (not 14))
-(contains 13 25)
-(contains 13 24)
-(contains 14 (not 21))
-(contains 14 54)
-(contains 14 49)
-(contains 14 2)
-(contains 14 42)
-(contains 15 (not 25))
-(contains 15 7)
-(contains 15 (not 43))
-(contains 15 (not 39))
-(contains 15 59)
-(contains 16 32)
-(contains 16 (not 30))
-(contains 16 14)
-(contains 16 17)
-(contains 16 51)
-(contains 17 (not 9))
-(contains 17 44)
-(contains 17 (not 3))
-(contains 17 4)
-(contains 17 (not 54))
-(contains 18 (not 46))
-(contains 18 48)
-(contains 18 55)
-(contains 18 (not 6))
-(contains 18 59)
-(contains 19 51)
-(contains 19 (not 12))
-(contains 19 1)
-(contains 19 52)
-(contains 19 58)
-(contains 20 (not 8))
-(contains 20 47)
-(contains 20 19)
-(contains 20 (not 42))
-(contains 20 (not 12))
-(contains 21 (not 39))
-(contains 21 11)
-(contains 21 1)
-(contains 21 (not 41))
-(contains 21 (not 31))
-(contains 22 (not 26))
-(contains 22 34)
-(contains 22 9)
-(contains 22 (not 35))
-(contains 22 41)
-(contains 23 54)
-(contains 23 26)
-(contains 23 (not 47))
-(contains 23 31)
-(contains 23 (not 36))
-(contains 24 (not 15))
-(contains 24 (not 60))
-(contains 24 (not 13))
-(contains 24 6)
-(contains 24 47)
-(contains 25 (not 21))
-(contains 25 (not 10))
-(contains 25 26)
-(contains 25 33)
-(contains 25 15)
-(contains 26 (not 20))
-(contains 26 11)
-(contains 26 49)
-(contains 26 12)
-(contains 26 (not 41))
-(contains 27 (not 3))
-(contains 27 53)
-(contains 27 15)
-(contains 27 (not 23))
-(contains 27 58)
-(contains 28 (not 3))
-(contains 28 (not 48))
-(contains 28 (not 21))
-(contains 28 59)
-(contains 28 46)
-(contains 29 28)
-(contains 29 25)
-(contains 29 (not 10))
-(contains 29 18)
-(contains 29 4)
-(contains 30 (not 55))
-(contains 30 7)
-(contains 30 (not 44))
-(contains 30 22)
-(contains 30 (not 32))
-(contains 31 (not 12))
-(contains 31 (not 35))
-(contains 31 (not 48))
-(contains 31 (not 14))
-(contains 31 (not 39))
-(contains 32 13)
-(contains 32 (not 45))
-(contains 32 49)
-(contains 32 (not 35))
-(contains 32 60)
-(contains 33 (not 60))
-(contains 33 27)
-(contains 33 (not 19))
-(contains 33 (not 25))
-(contains 33 29)
-(contains 34 (not 12))
-(contains 34 43)
-(contains 34 3)
-(contains 34 (not 5))
-(contains 34 30)
-(contains 35 (not 9))
-(contains 35 50)
-(contains 35 (not 19))
-(contains 35 (not 59))
-(contains 35 (not 2))
-(contains 36 (not 20))
-(contains 36 14)
-(contains 36 (not 58))
-(contains 36 (not 12))
-(contains 36 (not 34))
-(contains 37 22)
-(contains 37 (not 16))
-(contains 37 (not 4))
-(contains 37 (not 14))
-(contains 37 52)
-(contains 38 (not 45))
-(contains 38 (not 13))
-(contains 38 47)
-(contains 38 (not 12))
-(contains 38 15)
-(contains 39 (not 50))
-(contains 39 60)
-(contains 39 9)
-(contains 39 (not 4))
-(contains 39 18)
-(contains 40 (not 10))
-(contains 40 (not 54))
-(contains 40 (not 15))
-(contains 40 47)
-(contains 40 (not 22))
-(prop_var 1)
-(prop_var 2)
-(prop_var 3)
-(prop_var 4)
-(prop_var 5)
-(prop_var 6)
-(prop_var 7)
-(prop_var 8)
-(prop_var 9)
-(prop_var 10)
-(prop_var 11)
-(prop_var 12)
-(prop_var 13)
-(prop_var 14)
-(prop_var 15)
-(prop_var 16)
-(prop_var 17)
-(prop_var 18)
-(prop_var 19)
-(prop_var 20)
-(prop_var 21)
-(prop_var 22)
-(prop_var 23)
-(prop_var 24)
-(prop_var 25)
-(prop_var 26)
-(prop_var 27)
-(prop_var 28)
-(prop_var 29)
-(prop_var 30)
-(prop_var 31)
-(prop_var 32)
-(prop_var 33)
-(prop_var 34)
-(prop_var 35)
-(prop_var 36)
-(prop_var 37)
-(prop_var 38)
-(prop_var 39)
-(prop_var 40)
-(prop_var 41)
-(prop_var 42)
-(prop_var 43)
-(prop_var 44)
-(prop_var 45)
-(prop_var 46)
-(prop_var 47)
-(prop_var 48)
-(prop_var 49)
-(prop_var 50)
-(prop_var 51)
-(prop_var 52)
-(prop_var 53)
-(prop_var 54)
-(prop_var 55)
-(prop_var 56)
-(prop_var 57)
-(prop_var 58)
-(prop_var 59)
-(prop_var 60)
-(clause 1)
-(clause 2)
-(clause 3)
-(clause 4)
-(clause 5)
-(clause 6)
-(clause 7)
-(clause 8)
-(clause 9)
-(clause 10)
-(clause 11)
-(clause 12)
-(clause 13)
-(clause 14)
-(clause 15)
-(clause 16)
-(clause 17)
-(clause 18)
-(clause 19)
-(clause 20)
-(clause 21)
-(clause 22)
-(clause 23)
-(clause 24)
-(clause 25)
-(clause 26)
-(clause 27)
-(clause 28)
-(clause 29)
-(clause 30)
-(clause 31)
-(clause 32)
-(clause 33)
-(clause 34)
-(clause 35)
-(clause 36)
-(clause 37)
-(clause 38)
-(clause 39)
-(clause 40)
-(role exists)
-(role forall)
-(truth_value t)
-(truth_value f)
-(init (control exists 1))
-(<= (legal ?v5689 (assign ?v5699 ?v5700)) (true (control ?v5689 ?v5699)) (role ?v5689) (prop_var ?v5699) (truth_value ?v5700))
-(<= (legal exists noop) (true (control forall ?v5735)) (prop_var ?v5735))
-(<= (legal forall noop) (true (control exists ?v5735)) (prop_var ?v5735))
-(<= (next (sat ?v5759)) (true (sat ?v5759)) (clause ?v5759))
-(<= (next (control exists 2)) (true (control exists 1)))
-(<= (next (control exists 3)) (true (control exists 2)))
-(<= (next (control exists 4)) (true (control exists 3)))
-(<= (next (control exists 5)) (true (control exists 4)))
-(<= (next (control exists 6)) (true (control exists 5)))
-(<= (next (control exists 7)) (true (control exists 6)))
-(<= (next (control exists 8)) (true (control exists 7)))
-(<= (next (control exists 9)) (true (control exists 8)))
-(<= (next (control exists 10)) (true (control exists 9)))
-(<= (next (control exists 11)) (true (control exists 10)))
-(<= (next (control exists 12)) (true (control exists 11)))
-(<= (next (control exists 13)) (true (control exists 12)))
-(<= (next (control exists 14)) (true (control exists 13)))
-(<= (next (control exists 15)) (true (control exists 14)))
-(<= (next (control exists 16)) (true (control exists 15)))
-(<= (next (control exists 17)) (true (control exists 16)))
-(<= (next (control exists 18)) (true (control exists 17)))
-(<= (next (control exists 19)) (true (control exists 18)))
-(<= (next (control exists 20)) (true (control exists 19)))
-(<= (next (control forall 21)) (true (control exists 20)))
-(<= (next (control forall 22)) (true (control forall 21)))
-(<= (next (control forall 23)) (true (control forall 22)))
-(<= (next (control forall 24)) (true (control forall 23)))
-(<= (next (control forall 25)) (true (control forall 24)))
-(<= (next (control forall 26)) (true (control forall 25)))
-(<= (next (control forall 27)) (true (control forall 26)))
-(<= (next (control forall 28)) (true (control forall 27)))
-(<= (next (control forall 29)) (true (control forall 28)))
-(<= (next (control forall 30)) (true (control forall 29)))
-(<= (next (control forall 31)) (true (control forall 30)))
-(<= (next (control forall 32)) (true (control forall 31)))
-(<= (next (control forall 33)) (true (control forall 32)))
-(<= (next (control forall 34)) (true (control forall 33)))
-(<= (next (control forall 35)) (true (control forall 34)))
-(<= (next (control forall 36)) (true (control forall 35)))
-(<= (next (control forall 37)) (true (control forall 36)))
-(<= (next (control forall 38)) (true (control forall 37)))
-(<= (next (control forall 39)) (true (control forall 38)))
-(<= (next (control forall 40)) (true (control forall 39)))
-(<= (next (control exists 41)) (true (control forall 40)))
-(<= (next (control exists 42)) (true (control exists 41)))
-(<= (next (control exists 43)) (true (control exists 42)))
-(<= (next (control exists 44)) (true (control exists 43)))
-(<= (next (control exists 45)) (true (control exists 44)))
-(<= (next (control exists 46)) (true (control exists 45)))
-(<= (next (control exists 47)) (true (control exists 46)))
-(<= (next (control exists 48)) (true (control exists 47)))
-(<= (next (control exists 49)) (true (control exists 48)))
-(<= (next (control exists 50)) (true (control exists 49)))
-(<= (next (control exists 51)) (true (control exists 50)))
-(<= (next (control exists 52)) (true (control exists 51)))
-(<= (next (control exists 53)) (true (control exists 52)))
-(<= (next (control exists 54)) (true (control exists 53)))
-(<= (next (control exists 55)) (true (control exists 54)))
-(<= (next (control exists 56)) (true (control exists 55)))
-(<= (next (control exists 57)) (true (control exists 56)))
-(<= (next (control exists 58)) (true (control exists 57)))
-(<= (next (control exists 59)) (true (control exists 58)))
-(<= (next (control exists 60)) (true (control exists 59)))
-(<= (next (control the end)) (true (control exists 60)))
-(<= (next (sat 1)) (does ?v9608 (assign 1 f)) (role ?v9608))
-(<= (next (sat 1)) (does ?v9629 (assign 52 t)) (role ?v9629))
-(<= (next (sat 1)) (does ?v9650 (assign 16 t)) (role ?v9650))
-(<= (next (sat 1)) (does ?v9671 (assign 4 t)) (role ?v9671))
-(<= (next (sat 1)) (does ?v9692 (assign 27 f)) (role ?v9692))
-(<= (next (sat 2)) (does ?v9715 (assign 27 f)) (role ?v9715))
-(<= (next (sat 2)) (does ?v9736 (assign 51 f)) (role ?v9736))
-(<= (next (sat 2)) (does ?v9757 (assign 19 t)) (role ?v9757))
-(<= (next (sat 2)) (does ?v9778 (assign 1 t)) (role ?v9778))
-(<= (next (sat 2)) (does ?v9799 (assign 30 t)) (role ?v9799))
-(<= (next (sat 3)) (does ?v9822 (assign 35 t)) (role ?v9822))
-(<= (next (sat 3)) (does ?v9843 (assign 52 t)) (role ?v9843))
-(<= (next (sat 3)) (does ?v9864 (assign 41 f)) (role ?v9864))
-(<= (next (sat 3)) (does ?v9885 (assign 18 f)) (role ?v9885))
-(<= (next (sat 3)) (does ?v9906 (assign 59 f)) (role ?v9906))
-(<= (next (sat 4)) (does ?v9929 (assign 24 t)) (role ?v9929))
-(<= (next (sat 4)) (does ?v9950 (assign 30 t)) (role ?v9950))
-(<= (next (sat 4)) (does ?v9971 (assign 20 t)) (role ?v9971))
-(<= (next (sat 4)) (does ?v9992 (assign 7 f)) (role ?v9992))
-(<= (next (sat 4)) (does ?v10013 (assign 23 f)) (role ?v10013))
-(<= (next (sat 5)) (does ?v10036 (assign 34 f)) (role ?v10036))
-(<= (next (sat 5)) (does ?v10057 (assign 4 f)) (role ?v10057))
-(<= (next (sat 5)) (does ?v10078 (assign 13 t)) (role ?v10078))
-(<= (next (sat 5)) (does ?v10099 (assign 49 f)) (role ?v10099))
-(<= (next (sat 5)) (does ?v10120 (assign 17 f)) (role ?v10120))
-(<= (next (sat 6)) (does ?v10143 (assign 51 t)) (role ?v10143))
-(<= (next (sat 6)) (does ?v10164 (assign 37 f)) (role ?v10164))
-(<= (next (sat 6)) (does ?v10185 (assign 1 t)) (role ?v10185))
-(<= (next (sat 6)) (does ?v10206 (assign 5 t)) (role ?v10206))
-(<= (next (sat 6)) (does ?v10227 (assign 29 f)) (role ?v10227))
-(<= (next (sat 7)) (does ?v10250 (assign 2 f)) (role ?v10250))
-(<= (next (sat 7)) (does ?v10271 (assign 7 f)) (role ?v10271))
-(<= (next (sat 7)) (does ?v10292 (assign 53 f)) (role ?v10292))
-(<= (next (sat 7)) (does ?v10313 (assign 12 f)) (role ?v10313))
-(<= (next (sat 7)) (does ?v10334 (assign 35 f)) (role ?v10334))
-(<= (next (sat 8)) (does ?v10357 (assign 39 f)) (role ?v10357))
-(<= (next (sat 8)) (does ?v10378 (assign 44 f)) (role ?v10378))
-(<= (next (sat 8)) (does ?v10399 (assign 28 t)) (role ?v10399))
-(<= (next (sat 8)) (does ?v10420 (assign 2 f)) (role ?v10420))
-(<= (next (sat 8)) (does ?v10441 (assign 51 t)) (role ?v10441))
-(<= (next (sat 9)) (does ?v10464 (assign 21 f)) (role ?v10464))
-(<= (next (sat 9)) (does ?v10485 (assign 11 f)) (role ?v10485))
-(<= (next (sat 9)) (does ?v10506 (assign 8 t)) (role ?v10506))
-(<= (next (sat 9)) (does ?v10527 (assign 20 f)) (role ?v10527))
-(<= (next (sat 9)) (does ?v10548 (assign 2 t)) (role ?v10548))
-(<= (next (sat 10)) (does ?v10571 (assign 37 f)) (role ?v10571))
-(<= (next (sat 10)) (does ?v10592 (assign 21 f)) (role ?v10592))
-(<= (next (sat 10)) (does ?v10613 (assign 58 t)) (role ?v10613))
-(<= (next (sat 10)) (does ?v10634 (assign 59 f)) (role ?v10634))
-(<= (next (sat 10)) (does ?v10655 (assign 7 t)) (role ?v10655))
-(<= (next (sat 11)) (does ?v10678 (assign 33 t)) (role ?v10678))
-(<= (next (sat 11)) (does ?v10699 (assign 59 t)) (role ?v10699))
-(<= (next (sat 11)) (does ?v10720 (assign 41 f)) (role ?v10720))
-(<= (next (sat 11)) (does ?v10741 (assign 52 t)) (role ?v10741))
-(<= (next (sat 11)) (does ?v10762 (assign 21 t)) (role ?v10762))
-(<= (next (sat 12)) (does ?v10785 (assign 43 t)) (role ?v10785))
-(<= (next (sat 12)) (does ?v10806 (assign 35 t)) (role ?v10806))
-(<= (next (sat 12)) (does ?v10827 (assign 7 f)) (role ?v10827))
-(<= (next (sat 12)) (does ?v10848 (assign 33 t)) (role ?v10848))
-(<= (next (sat 12)) (does ?v10869 (assign 50 t)) (role ?v10869))
-(<= (next (sat 13)) (does ?v10892 (assign 29 t)) (role ?v10892))
-(<= (next (sat 13)) (does ?v10913 (assign 45 t)) (role ?v10913))
-(<= (next (sat 13)) (does ?v10934 (assign 14 f)) (role ?v10934))
-(<= (next (sat 13)) (does ?v10955 (assign 25 t)) (role ?v10955))
-(<= (next (sat 13)) (does ?v10976 (assign 24 t)) (role ?v10976))
-(<= (next (sat 14)) (does ?v10999 (assign 21 f)) (role ?v10999))
-(<= (next (sat 14)) (does ?v11020 (assign 54 t)) (role ?v11020))
-(<= (next (sat 14)) (does ?v11041 (assign 49 t)) (role ?v11041))
-(<= (next (sat 14)) (does ?v11062 (assign 2 t)) (role ?v11062))
-(<= (next (sat 14)) (does ?v11083 (assign 42 t)) (role ?v11083))
-(<= (next (sat 15)) (does ?v11106 (assign 25 f)) (role ?v11106))
-(<= (next (sat 15)) (does ?v11127 (assign 7 t)) (role ?v11127))
-(<= (next (sat 15)) (does ?v11148 (assign 43 f)) (role ?v11148))
-(<= (next (sat 15)) (does ?v11169 (assign 39 f)) (role ?v11169))
-(<= (next (sat 15)) (does ?v11190 (assign 59 t)) (role ?v11190))
-(<= (next (sat 16)) (does ?v11213 (assign 32 t)) (role ?v11213))
-(<= (next (sat 16)) (does ?v11234 (assign 30 f)) (role ?v11234))
-(<= (next (sat 16)) (does ?v11255 (assign 14 t)) (role ?v11255))
-(<= (next (sat 16)) (does ?v11276 (assign 17 t)) (role ?v11276))
-(<= (next (sat 16)) (does ?v11297 (assign 51 t)) (role ?v11297))
-(<= (next (sat 17)) (does ?v11320 (assign 9 f)) (role ?v11320))
-(<= (next (sat 17)) (does ?v11341 (assign 44 t)) (role ?v11341))
-(<= (next (sat 17)) (does ?v11362 (assign 3 f)) (role ?v11362))
-(<= (next (sat 17)) (does ?v11383 (assign 4 t)) (role ?v11383))
-(<= (next (sat 17)) (does ?v11404 (assign 54 f)) (role ?v11404))
-(<= (next (sat 18)) (does ?v11427 (assign 46 f)) (role ?v11427))
-(<= (next (sat 18)) (does ?v11448 (assign 48 t)) (role ?v11448))
-(<= (next (sat 18)) (does ?v11469 (assign 55 t)) (role ?v11469))
-(<= (next (sat 18)) (does ?v11490 (assign 6 f)) (role ?v11490))
-(<= (next (sat 18)) (does ?v11511 (assign 59 t)) (role ?v11511))
-(<= (next (sat 19)) (does ?v11534 (assign 51 t)) (role ?v11534))
-(<= (next (sat 19)) (does ?v11555 (assign 12 f)) (role ?v11555))
-(<= (next (sat 19)) (does ?v11576 (assign 1 t)) (role ?v11576))
-(<= (next (sat 19)) (does ?v11597 (assign 52 t)) (role ?v11597))
-(<= (next (sat 19)) (does ?v11618 (assign 58 t)) (role ?v11618))
-(<= (next (sat 20)) (does ?v11641 (assign 8 f)) (role ?v11641))
-(<= (next (sat 20)) (does ?v11662 (assign 47 t)) (role ?v11662))
-(<= (next (sat 20)) (does ?v11683 (assign 19 t)) (role ?v11683))
-(<= (next (sat 20)) (does ?v11704 (assign 42 f)) (role ?v11704))
-(<= (next (sat 20)) (does ?v11725 (assign 12 f)) (role ?v11725))
-(<= (next (sat 21)) (does ?v11748 (assign 39 f)) (role ?v11748))
-(<= (next (sat 21)) (does ?v11769 (assign 11 t)) (role ?v11769))
-(<= (next (sat 21)) (does ?v11790 (assign 1 t)) (role ?v11790))
-(<= (next (sat 21)) (does ?v11811 (assign 41 f)) (role ?v11811))
-(<= (next (sat 21)) (does ?v11832 (assign 31 f)) (role ?v11832))
-(<= (next (sat 22)) (does ?v11855 (assign 26 f)) (role ?v11855))
-(<= (next (sat 22)) (does ?v11876 (assign 34 t)) (role ?v11876))
-(<= (next (sat 22)) (does ?v11897 (assign 9 t)) (role ?v11897))
-(<= (next (sat 22)) (does ?v11918 (assign 35 f)) (role ?v11918))
-(<= (next (sat 22)) (does ?v11939 (assign 41 t)) (role ?v11939))
-(<= (next (sat 23)) (does ?v11962 (assign 54 t)) (role ?v11962))
-(<= (next (sat 23)) (does ?v11983 (assign 26 t)) (role ?v11983))
-(<= (next (sat 23)) (does ?v12004 (assign 47 f)) (role ?v12004))
-(<= (next (sat 23)) (does ?v12025 (assign 31 t)) (role ?v12025))
-(<= (next (sat 23)) (does ?v12046 (assign 36 f)) (role ?v12046))
-(<= (next (sat 24)) (does ?v12069 (assign 15 f)) (role ?v12069))
-(<= (next (sat 24)) (does ?v12090 (assign 60 f)) (role ?v12090))
-(<= (next (sat 24)) (does ?v12111 (assign 13 f)) (role ?v12111))
-(<= (next (sat 24)) (does ?v12132 (assign 6 t)) (role ?v12132))
-(<= (next (sat 24)) (does ?v12153 (assign 47 t)) (role ?v12153))
-(<= (next (sat 25)) (does ?v12176 (assign 21 f)) (role ?v12176))
-(<= (next (sat 25)) (does ?v12197 (assign 10 f)) (role ?v12197))
-(<= (next (sat 25)) (does ?v12218 (assign 26 t)) (role ?v12218))
-(<= (next (sat 25)) (does ?v12239 (assign 33 t)) (role ?v12239))
-(<= (next (sat 25)) (does ?v12260 (assign 15 t)) (role ?v12260))
-(<= (next (sat 26)) (does ?v12283 (assign 20 f)) (role ?v12283))
-(<= (next (sat 26)) (does ?v12304 (assign 11 t)) (role ?v12304))
-(<= (next (sat 26)) (does ?v12325 (assign 49 t)) (role ?v12325))
-(<= (next (sat 26)) (does ?v12346 (assign 12 t)) (role ?v12346))
-(<= (next (sat 26)) (does ?v12367 (assign 41 f)) (role ?v12367))
-(<= (next (sat 27)) (does ?v12390 (assign 3 f)) (role ?v12390))
-(<= (next (sat 27)) (does ?v12411 (assign 53 t)) (role ?v12411))
-(<= (next (sat 27)) (does ?v12432 (assign 15 t)) (role ?v12432))
-(<= (next (sat 27)) (does ?v12453 (assign 23 f)) (role ?v12453))
-(<= (next (sat 27)) (does ?v12474 (assign 58 t)) (role ?v12474))
-(<= (next (sat 28)) (does ?v12497 (assign 3 f)) (role ?v12497))
-(<= (next (sat 28)) (does ?v12518 (assign 48 f)) (role ?v12518))
-(<= (next (sat 28)) (does ?v12539 (assign 21 f)) (role ?v12539))
-(<= (next (sat 28)) (does ?v12560 (assign 59 t)) (role ?v12560))
-(<= (next (sat 28)) (does ?v12581 (assign 46 t)) (role ?v12581))
-(<= (next (sat 29)) (does ?v12604 (assign 28 t)) (role ?v12604))
-(<= (next (sat 29)) (does ?v12625 (assign 25 t)) (role ?v12625))
-(<= (next (sat 29)) (does ?v12646 (assign 10 f)) (role ?v12646))
-(<= (next (sat 29)) (does ?v12667 (assign 18 t)) (role ?v12667))
-(<= (next (sat 29)) (does ?v12688 (assign 4 t)) (role ?v12688))
-(<= (next (sat 30)) (does ?v12711 (assign 55 f)) (role ?v12711))
-(<= (next (sat 30)) (does ?v12732 (assign 7 t)) (role ?v12732))
-(<= (next (sat 30)) (does ?v12753 (assign 44 f)) (role ?v12753))
-(<= (next (sat 30)) (does ?v12774 (assign 22 t)) (role ?v12774))
-(<= (next (sat 30)) (does ?v12795 (assign 32 f)) (role ?v12795))
-(<= (next (sat 31)) (does ?v12818 (assign 12 f)) (role ?v12818))
-(<= (next (sat 31)) (does ?v12839 (assign 35 f)) (role ?v12839))
-(<= (next (sat 31)) (does ?v12860 (assign 48 f)) (role ?v12860))
-(<= (next (sat 31)) (does ?v12881 (assign 14 f)) (role ?v12881))
-(<= (next (sat 31)) (does ?v12902 (assign 39 f)) (role ?v12902))
-(<= (next (sat 32)) (does ?v12925 (assign 13 t)) (role ?v12925))
-(<= (next (sat 32)) (does ?v12946 (assign 45 f)) (role ?v12946))
-(<= (next (sat 32)) (does ?v12967 (assign 49 t)) (role ?v12967))
-(<= (next (sat 32)) (does ?v12988 (assign 35 f)) (role ?v12988))
-(<= (next (sat 32)) (does ?v13009 (assign 60 t)) (role ?v13009))
-(<= (next (sat 33)) (does ?v13032 (assign 60 f)) (role ?v13032))
-(<= (next (sat 33)) (does ?v13053 (assign 27 t)) (role ?v13053))
-(<= (next (sat 33)) (does ?v13074 (assign 19 f)) (role ?v13074))
-(<= (next (sat 33)) (does ?v13095 (assign 25 f)) (role ?v13095))
-(<= (next (sat 33)) (does ?v13116 (assign 29 t)) (role ?v13116))
-(<= (next (sat 34)) (does ?v13139 (assign 12 f)) (role ?v13139))
-(<= (next (sat 34)) (does ?v13160 (assign 43 t)) (role ?v13160))
-(<= (next (sat 34)) (does ?v13181 (assign 3 t)) (role ?v13181))
-(<= (next (sat 34)) (does ?v13202 (assign 5 f)) (role ?v13202))
-(<= (next (sat 34)) (does ?v13223 (assign 30 t)) (role ?v13223))
-(<= (next (sat 35)) (does ?v13246 (assign 9 f)) (role ?v13246))
-(<= (next (sat 35)) (does ?v13267 (assign 50 t)) (role ?v13267))
-(<= (next (sat 35)) (does ?v13288 (assign 19 f)) (role ?v13288))
-(<= (next (sat 35)) (does ?v13309 (assign 59 f)) (role ?v13309))
-(<= (next (sat 35)) (does ?v13330 (assign 2 f)) (role ?v13330))
-(<= (next (sat 36)) (does ?v13353 (assign 20 f)) (role ?v13353))
-(<= (next (sat 36)) (does ?v13374 (assign 14 t)) (role ?v13374))
-(<= (next (sat 36)) (does ?v13395 (assign 58 f)) (role ?v13395))
-(<= (next (sat 36)) (does ?v13416 (assign 12 f)) (role ?v13416))
-(<= (next (sat 36)) (does ?v13437 (assign 34 f)) (role ?v13437))
-(<= (next (sat 37)) (does ?v13460 (assign 22 t)) (role ?v13460))
-(<= (next (sat 37)) (does ?v13481 (assign 16 f)) (role ?v13481))
-(<= (next (sat 37)) (does ?v13502 (assign 4 f)) (role ?v13502))
-(<= (next (sat 37)) (does ?v13523 (assign 14 f)) (role ?v13523))
-(<= (next (sat 37)) (does ?v13544 (assign 52 t)) (role ?v13544))
-(<= (next (sat 38)) (does ?v13567 (assign 45 f)) (role ?v13567))
-(<= (next (sat 38)) (does ?v13588 (assign 13 f)) (role ?v13588))
-(<= (next (sat 38)) (does ?v13609 (assign 47 t)) (role ?v13609))
-(<= (next (sat 38)) (does ?v13630 (assign 12 f)) (role ?v13630))
-(<= (next (sat 38)) (does ?v13651 (assign 15 t)) (role ?v13651))
-(<= (next (sat 39)) (does ?v13674 (assign 50 f)) (role ?v13674))
-(<= (next (sat 39)) (does ?v13695 (assign 60 t)) (role ?v13695))
-(<= (next (sat 39)) (does ?v13716 (assign 9 t)) (role ?v13716))
-(<= (next (sat 39)) (does ?v13737 (assign 4 f)) (role ?v13737))
-(<= (next (sat 39)) (does ?v13758 (assign 18 t)) (role ?v13758))
-(<= (next (sat 40)) (does ?v13781 (assign 10 f)) (role ?v13781))
-(<= (next (sat 40)) (does ?v13802 (assign 54 f)) (role ?v13802))
-(<= (next (sat 40)) (does ?v13823 (assign 15 f)) (role ?v13823))
-(<= (next (sat 40)) (does ?v13844 (assign 47 t)) (role ?v13844))
-(<= (next (sat 40)) (does ?v13865 (assign 22 f)) (role ?v13865))
-(<= all_sat (true (sat 1)) (true (sat 2)) (true (sat 3)) (true (sat 4)) (true (sat 5)) (true (sat 6)) (true (sat 7)) (true (sat 8)) (true (sat 9)) (true (sat 10)) (true (sat 11)) (true (sat 12)) (true (sat 13)) (true (sat 14)) (true (sat 15)) (true (sat 16)) (true (sat 17)) (true (sat 18)) (true (sat 19)) (true (sat 20)) (true (sat 21)) (true (sat 22)) (true (sat 23)) (true (sat 24)) (true (sat 25)) (true (sat 26)) (true (sat 27)) (true (sat 28)) (true (sat 29)) (true (sat 30)) (true (sat 31)) (true (sat 32)) (true (sat 33)) (true (sat 34)) (true (sat 35)) (true (sat 36)) (true (sat 37)) (true (sat 38)) (true (sat 39)) (true (sat 40)))
-(<= terminal all_sat)
-(<= terminal (true (control the end)))
-(<= (goal exists 100) all_sat)
-(<= (goal exists 0) (not all_sat))
-(<= (goal forall 100) (not all_sat))
-(<= (goal forall 0) all_sat)
-
-
Deleted: trunk/Toss/GGP/examples/3qbf-5cnf-20var-40cl.1.qdimacs.viz.SAT.gdl
===================================================================
--- trunk/Toss/GGP/examples/3qbf-5cnf-20var-40cl.1.qdimacs.viz.SAT.gdl 2011-09-13 17:47:33 UTC (rev 1566)
+++ trunk/Toss/GGP/examples/3qbf-5cnf-20var-40cl.1.qdimacs.viz.SAT.gdl 2011-09-14 01:00:51 UTC (rev 1567)
@@ -1,578 +0,0 @@
-(contains 1 (not 1))
-(contains 1 52)
-(contains 1 16)
-(contains 1 4)
-(contains 1 (not 27))
-(contains 2 (not 27))
-(contains 2 (not 51))
-(contains 2 19)
-(contains 2 1)
-(contains 2 30)
-(contains 3 35)
-(contains 3 52)
-(contains 3 (not 41))
-(contains 3 (not 18))
-(contains 3 (not 59))
-(contains 4 24)
-(contains 4 30)
-(contains 4 20)
-(contains 4 (not 7))
-(contains 4 (not 23))
-(contains 5 (not 34))
-(contains 5 (not 4))
-(contains 5 13)
-(contains 5 (not 49))
-(contains 5 (not 17))
-(contains 6 51)
-(contains 6 (not 37))
-(contains 6 1)
-(contains 6 5)
-(contains 6 (not 29))
-(contains 7 (not 2))
-(contains 7 (not 7))
-(contains 7 (not 53))
-(contains 7 (not 12))
-(contains 7 (not 35))
-(contains 8 (not 39))
-(contains 8 (not 44))
-(contains 8 28)
-(contains 8 (not 2))
-(contains 8 51)
-(contains 9 (not 21))
-(contains 9 (not 11))
-(contains 9 8)
-(contains 9 (not 20))
-(contains 9 2)
-(contains 10 (not 37))
-(contains 10 (not 21))
-(contains 10 58)
-(contains 10 (not 59))
-(contains 10 7)
-(contains 11 33)
-(contains 11 59)
-(contains 11 (not 41))
-(contains 11 52)
-(contains 11 21)
-(contains 12 43)
-(contains 12 35)
-(contains 12 (not 7))
-(contains 12 33)
-(contains 12 50)
-(contains 13 29)
-(contains 13 45)
-(contains 13 (not 14))
-(contains 13 25)
-(contains 13 24)
-(contains 14 (not 21))
-(contains 14 54)
-(contains 14 49)
-(contains 14 2)
-(contains 14 42)
-(contains 15 (not 25))
-(contains 15 7)
-(contains 15 (not 43))
-(contains 15 (not 39))
-(contains 15 59)
-(contains 16 32)
-(contains 16 (not 30))
-(contains 16 14)
-(contains 16 17)
-(contains 16 51)
-(contains 17 (not 9))
-(contains 17 44)
-(contains 17 (not 3))
-(contains 17 4)
-(contains 17 (not 54))
-(contains 18 (not 46))
-(contains 18 48)
-(contains 18 55)
-(contains 18 (not 6))
-(contains 18 59)
-(contains 19 51)
-(contains 19 (not 12))
-(contains 19 1)
-(contains 19 52)
-(contains 19 58)
-(contains 20 (not 8))
-(contains 20 47)
-(contains 20 19)
-(contains 20 (not 42))
-(contains 20 (not 12))
-(contains 21 (not 39))
-(contains 21 11)
-(contains 21 1)
-(contains 21 (not 41))
-(contains 21 (not 31))
-(contains 22 (not 26))
-(contains 22 34)
-(contains 22 9)
-(contains 22 (not 35))
-(contains 22 41)
-(contains 23 54)
-(contains 23 26)
-(contains 23 (not 47))
-(contains 23 31)
-(contains 23 (not 36))
-(contains 24 (not 15))
-(contains 24 (not 60))
-(contains 24 (not 13))
-(contains 24 6)
-(contains 24 47)
-(contains 25 (not 21))
-(contains 25 (not 10))
-(contains 25 26)
-(contains 25 33)
-(contains 25 15)
-(contains 26 (not 20))
-(contains 26 11)
-(contains 26 49)
-(contains 26 12)
-(contains 26 (not 41))
-(contains 27 (not 3))
-(contains 27 53)
-(contains 27 15)
-(contains 27 (not 23))
-(contains 27 58)
-(contains 28 (not 3))
-(contains 28 (not 48))
-(contains 28 (not 21))
-(contains 28 59)
-(contains 28 46)
-(contains 29 28)
-(contains 29 25)
-(contains 29 (not 10))
-(contains 29 18)
-(contains 29 4)
-(contains 30 (not 55))
-(contains 30 7)
-(contains 30 (not 44))
-(contains 30 22)
-(contains 30 (not 32))
-(contains 31 (not 12))
-(contains 31 (not 35))
-(contains 31 (not 48))
-(contains 31 (not 14))
-(contains 31 (not 39))
-(contains 32 13)
-(contains 32 (not 45))
-(contains 32 49)
-(contains 32 (not 35))
-(contains 32 60)
-(contains 33 (not 60))
-(contains 33 27)
-(contains 33 (not 19))
-(contains 33 (not 25))
-(contains 33 29)
-(contains 34 (not 12))
-(contains 34 43)
-(contains 34 3)
-(contains 34 (not 5))
-(contains 34 30)
-(contains 35 (not 9))
-(contains 35 50)
-(contains 35 (not 19))
-(contains 35 (not 59))
-(contains 35 (not 2))
-(contains 36 (not 20))
-(contains 36 14)
-(contains 36 (not 58))
-(contains 36 (not 12))
-(contains 36 (not 34))
-(contains 37 22)
-(contains 37 (not 16))
-(contains 37 (not 4))
-(contains 37 (not 14))
-(contains 37 52)
-(contains 38 (not 45))
-(contains 38 (not 13))
-(contains 38 47)
-(contains 38 (not 12))
-(contains 38 15)
-(contains 39 (not 50))
-(contains 39 60)
-(contains 39 9)
-(contains 39 (not 4))
-(contains 39 18)
-(contains 40 (not 10))
-(contains 40 (not 54))
-(contains 40 (not 15))
-(contains 40 47)
-(contains 40 (not 22))
-(prop_var 1)
-(prop_var 2)
-(prop_var 3)
-(prop_var 4)
-(prop_var 5)
-(prop_var 6)
-(prop_var 7)
-(prop_var 8)
-(prop_var 9)
-(prop_var 10)
-(prop_var 11)
-(prop_var 12)
-(prop_var 13)
-(prop_var 14)
-(prop_var 15)
-(prop_var 16)
-(prop_var 17)
-(prop_var 18)
-(prop_var 19)
-(prop_var 20)
-(prop_var 21)
-(prop_var 22)
-(prop_var 23)
-(prop_var 24)
-(prop_var 25)
-(prop_var 26)
-(prop_var 27)
-(prop_var 28)
-(prop_var 29)
-(prop_var 30)
-(prop_var 31)
-(prop_var 32)
-(prop_var 33)
-(prop_var 34)
-(prop_var 35)
-(prop_var 36)
-(prop_var 37)
-(prop_var 38)
-(prop_var 39)
-(prop_var 40)
-(prop_var 41)
-(prop_var 42)
-(prop_var 43)
-(prop_var 44)
-(prop_var 45)
-(prop_var 46)
-(prop_var 47)
-(prop_var 48)
-(prop_var 49)
-(prop_var 50)
-(prop_var 51)
-(prop_var 52)
-(prop_var 53)
-(prop_var 54)
-(prop_var 55)
-(prop_var 56)
-(prop_var 57)
-(prop_var 58)
-(prop_var 59)
-(prop_var 60)
-(clause 1)
-(clause 2)
-(clause 3)
-(clause 4)
-(clause 5)
-(clause 6)
-(clause 7)
-(clause 8)
-(clause 9)
-(clause 10)
-(clause 11)
-(clause 12)
-(clause 13)
-(clause 14)
-(clause 15)
-(clause 16)
-(clause 17)
-(clause 18)
-(clause 19)
-(clause 20)
-(clause 21)
-(clause 22)
-(clause 23)
-(clause 24)
-(clause 25)
-(clause 26)
-(clause 27)
-(clause 28)
-(clause 29)
-(clause 30)
-(clause 31)
-(clause 32)
-(clause 33)
-(clause 34)
-(clause 35)
-(clause 36)
-(clause 37)
-(clause 38)
-(clause 39)
-(clause 40)
-(role exists)
-(role forall)
-(truth_value t)
-(truth_value f)
-(init (control exists 1))
-(<= (legal ?v5689 (assign ?v5699 ?v5700)) (true (control ?v5689 ?v5699)) (role ?v5689) (prop_var ?v5699) (truth_value ?v5700))
-(<= (legal exists noop) (true (control forall ?v5735)) (prop_var ?v5735))
-(<= (legal forall noop) (true (control exists ?v5735)) (prop_var ?v5735))
-(<= (next (sat ?v5759)) (true (sat ?v5759)) (clause ?v5759))
-(<= (next (control exists 2)) (true (control exists 1)))
-(<= (next (control exists 3)) (true (control exists 2)))
-(<= (next (control exists 4)) (true (control exists 3)))
-(<= (next (control exists 5)) (true (control exists 4)))
-(<= (next (control exists 6)) (true (control exists 5)))
-(<= (next (control exists 7)) (true (control exists 6)))
-(<= (next (control exists 8)) (true (control exists 7)))
-(<= (next (control exists 9)) (true (control exists 8)))
-(<= (next (control exists 10)) (true (control exists 9)))
-(<= (next (control exists 11)) (true (control exists 10)))
-(<= (next (control exists 12)) (true (control exists 11)))
-(<= (next (control exists 13)) (true (control exists 12)))
-(<= (next (control exists 14)) (true (control exists 13)))
-(<= (next (control exists 15)) (true (control exists 14)))
-(<= (next (control exists 16)) (true (control exists 15)))
-(<= (next (control exists 17)) (true (control exists 16)))
-(<= (next (control exists 18)) (true (control exists 17)))
-(<= (next (control exists 19)) (true (control exists 18)))
-(<= (next (control exists 20)) (true (control exists 19)))
-(<= (next (control forall 21)) (true (control exists 20)))
-(<= (next (control forall 22)) (true (control forall 21)))
-(<= (next (control forall 23)) (true (control forall 22)))
-(<= (next (control forall 24)) (true (control forall 23)))
-(<= (next (control forall 25)) (true (control forall 24)))
-(<= (next (control forall 26)) (true (control forall 25)))
-(<= (next (control forall 27)) (true (control forall 26)))
-(<= (next (control forall 28)) (true (control forall 27)))
-(<= (next (control forall 29)) (true (control forall 28)))
-(<= (next (control forall 30)) (true (control forall 29)))
-(<= (next (control forall 31)) (true (control forall 30)))
-(<= (next (control forall 32)) (true (control forall 31)))
-(<= (next (control forall 33)) (true (control forall 32)))
-(<= (next (control forall 34)) (true (control forall 33)))
-(<= (next (control forall 35)) (true (control forall 34)))
-(<= (next (control forall 36)) (true (control forall 35)))
-(<= (next (control forall 37)) (true (control forall 36)))
-(<= (next (control forall 38)) (true (control forall 37)))
-(<= (next (control forall 39)) (true (control forall 38)))
-(<= (next (control forall 40)) (true (control forall 39)))
-(<= (next (control exists 41)) (true (control forall 40)))
-(<= (next (control exists 42)) (true (control exists 41)))
-(<= (next (control exists 43)) (true (control exists 42)))
-(<= (next (control exists 44)) (true (control exists 43)))
-(<= (next (control exists 45)) (true (control exists 44)))
-(<= (next (control exists 46)) (true (control exists 45)))
-(<= (next (control exists 47)) (true (control exists 46)))
-(<= (next (control exists 48)) (true (control exists 47)))
-(<= (next (control exists 49)) (true (control exists 48)))
-(<= (next (control exists 50)) (true (control exists 49)))
-(<= (next (control exists 51)) (true (control exists 50)))
-(<= (next (control exists 52)) (true (control exists 51)))
-(<= (next (control exists 53)) (true (control exists 52)))
-(<= (next (control exists 54)) (true (control exists 53)))
-(<= (next (control exists 55)) (true (control exists 54)))
-(<= (next (control exists 56)) (true (control exists 55)))
-(<= (next (control exists 57)) (true (control exists 56)))
-(<= (next (control exists 58)) (true (control exists 57)))
-(<= (next (control exists 59)) (true (control exists 58)))
-(<= (next (control exists 60)) (true (control exists 59)))
-(<= (next (control the end)) (true (control exists 60)))
-(<= (next (sat 1)) (does ?v9608 (assign 1 f)) (role ?v9608))
-(<= (next (sat 1)) (does ?v9629 (assign 52 t)) (role ?v9629))
-(<= (next (sat 1)) (does ?v9650 (assign 16 t)) (role ?v9650))
-(<= (next (sat 1)) (does ?v9671 (assign 4 t)) (role ?v9671))
-(<= (next (sat 1)) (does ?v9692 (assign 27 f)) (role ?v9692))
-(<= (next (sat 2)) (does ?v9715 (assign 27 f)) (role ?v9715))
-(<= (next (sat 2)) (does ?v9736 (assign 51 f)) (role ?v9736))
-(<= (next (sat 2)) (does ?v9757 (assign 19 t)) (role ?v9757))
-(<= (next (sat 2)) (does ?v9778 (assign 1 t)) (role ?v9778))
-(<= (next (sat 2)) (does ?v9799 (assign 30 t)) (role ?v9799))
-(<= (next (sat 3)) (does ?v9822 (assign 35 t)) (role ?v9822))
-(<= (next (sat 3)) (does ?v9843 (assign 52 t)) (role ?v9843))
-(<= (next (sat 3)) (does ?v9864 (assign 41 f)) (role ?v9864))
-(<= (next (sat 3)) (does ?v9885 (assign 18 f)) (role ?v9885))
-(<= (next (sat 3)) (does ?v9906 (assign 59 f)) (role ?v9906))
-(<= (next (sat 4)) (does ?v9929 (assign 24 t)) (role ?v9929))
-(<= (next (sat 4)) (does ?v9950 (assign 30 t)) (role ?v9950))
-(<= (next (sat 4)) (does ?v9971 (assign 20 t)) (role ?v9971))
-(<= (next (sat 4)) (does ?v9992 (assign 7 f)) (role ?v9992))
-(<= (next (sat 4)) (does ?v10013 (assign 23 f)) (role ?v10013))
-(<= (next (sat 5)) (does ?v10036 (assign 34 f)) (role ?v10036))
-(<= (next (sat 5)) (does ?v10057 (assign 4 f)) (role ?v10057))
-(<= (next (sat 5)) (does ?v10078 (assign 13 t)) (role ?v10078))
-(<= (next (sat 5)) (does ?v10099 (assign 49 f)) (role ?v10099))
-(<= (next (sat 5)) (does ?v10120 (assign 17 f)) (role ?v10120))
-(<= (next (sat 6)) (does ?v10143 (assign 51 t)) (role ?v10143))
-(<= (next (sat 6)) (does ?v10164 (assign 37 f)) (role ?v10164))
-(<= (next (sat 6)) (does ?v10185 (assign 1 t)) (role ?v10185))
-(<= (next (sat 6)) (does ?v10206 (assign 5 t)) (role ?v10206))
-(<= (next (sat 6)) (does ?v10227 (assign 29 f)) (role ?v10227))
-(<= (next (sat 7)) (does ?v10250 (assign 2 f)) (role ?v10250))
-(<= (next (sat 7)) (does ?v10271 (assign 7 f)) (role ?v10271))
-(<= (next (sat 7)) (does ?v10292 (assign 53 f)) (role ?v10292))
-(<= (next (sat 7)) (does ?v10313 (assign 12 f)) (role ?v10313))
-(<= (next (sat 7)) (does ?v10334 (assign 35 f)) (role ?v10334))
-(<= (next (sat 8)) (does ?v10357 (assign 39 f)) (role ?v10357))
-(<= (next (sat 8)) (does ?v10378 (assign 44 f)) (role ?v10378))
-(<= (next (sat 8)) (does ?v10399 (assign 28 t)) (role ?v10399))
-(<= (next (sat 8)) (does ?v10420 (assign 2 f)) (role ?v10420))
-(<= (next (sat 8)) (does ?v10441 (assign 51 t)) (role ?v10441))
-(<= (next (sat 9)) (does ?v10464 (assign 21 f)) (role ?v10464))
-(<= (next (sat 9)) (does ?v10485 (assign 11 f)) (role ?v10485))
-(<= (next (sat 9)) (does ?v10506 (assign 8 t)) (role ?v10506))
-(<= (next (sat 9)) (does ?v10527 (assign 20 f)) (role ?v10527))
-(<= (next (sat 9)) (does ?v10548 (assign 2 t)) (role ?v10548))
-(<= (next (sat 10)) (does ?v10571 (assign 37 f)) (role ?v10571))
-(<= (next (sat 10)) (does ?v10592 (assign 21 f)) (role ?v10592))
-(<= (next (sat 10)) (does ?v10613 (assign 58 t)) (role ?v10613))
-(<= (next (sat 10)) (does ?v10634 (assign 59 f)) (role ?v10634))
-(<= (next (sat 10)) (does ?v10655 (assign 7 t)) (role ?v10655))
-(<= (next (sat 11)) (does ?v10678 (assign 33 t)) (role ?v10678))
-(<= (next (sat 11)) (does ?v10699 (assign 59 t)) (role ?v10699))
-(<= (next (sat 11)) (does ?v10720 (assign 41 f)) (role ?v10720))
-(<= (next (sat 11)) (does ?v10741 (assign 52 t)) (role ?v10741))
-(<= (next (sat 11)) (does ?v10762 (assign 21 t)) (role ?v10762))
-(<= (next (sat 12)) (does ?v10785 (assign 43 t)) (role ?v10785))
-(<= (next (sat 12)) (does ?v10806 (assign 35 t)) (role ?v10806))
-(<= (next (sat 12)) (does ?v10827 (assign 7 f)) (role ?v10827))
-(<= (next (sat 12)) (does ?v10848 (assign 33 t)) (role ?v10848))
-(<= (next (sat 12)) (does ?v10869 (assign 50 t)) (role ?v10869))
-(<= (next (sat 13)) (does ?v10892 (assign 29 t)) (role ?v10892))
-(<= (next (sat 13)) (does ?v10913 (assign 45 t)) (role ?v10913))
-(<= (next (sat 13)) (does ?v10934 (assign 14 f)) (role ?v10934))
-(<= (next (sat 13)) (does ?v10955 (assign 25 t)) (role ?v10955))
-(<= (next (sat 13)) (does ?v10976 (assign 24 t)) (role ?v10976))
-(<= (next (sat 14)) (does ?v10999 (assign 21 f)) (role ?v10999))
-(<= (next (sat 14)) (does ?v11020 (assign 54 t)) (role ?v11020))
-(<= (next (sat 14)) (does ?v11041 (assign 49 t)) (role ?v11041))
-(<= (next (sat 14)) (does ?v11062 (assign 2 t)) (role ?v11062))
-(<= (next (sat 14)) (does ?v11083 (assign 42 t)) (role ?v11083))
-(<= (next (sat 15)) (does ?v11106 (assign 25 f)) (role ?v11106))
-(<= (next (sat 15)) (does ?v11127 (assign 7 t)) (role ?v11127))
-(<= (next (sat 15)) (does ?v11148 (assign 43 f)) (role ?v11148))
-(<= (next (sat 15)) (does ?v11169 (assign 39 f)) (role ?v11169))
-(<= (next (sat 15)) (does ?v11190 (assign 59 t)) (role ?v11190))
-(<= (next (sat 16)) (does ?v11213 (assign 32 t)) (role ?v11213))
-(<= (next (sat 16)) (does ?v11234 (assign 30 f)) (role ?v11234))
-(<= (next (sat 16)) (does ?v11255 (assign 14 t)) (role ?v11255))
-(<= (next (sat 16)) (does ?v11276 (assign 17 t)) (role ?v11276))
-(<= (next (sat 16)) (does ?v11297 (assign 51 t)) (role ?v11297))
-(<= (next (sat 17)) (does ?v11320 (assign 9 f)) (role ?v11320))
-(<= (next (sat 17)) (does ?v11341 (assign 44 t)) (role ?v11341))
-(<= (next (sat 17)) (does ?v11362 (assign 3 f)) (role ?v11362))
-(<= (next (sat 17)) (does ?v11383 (assign 4 t)) (role ?v11383))
-(<= (next (sat 17)) (does ?v11404 (assign 54 f)) (role ?v11404))
-(<= (next (sat 18)) (does ?v11427 (assign 46 f)) (role ?v11427))
-(<= (next (sat 18)) (does ?v11448 (assign 48 t)) (role ?v11448))
-(<= (next (sat 18)) (does ?v11469 (assign 55 t)) (role ?v11469))
-(<= (next (sat 18)) (does ?v11490 (assign 6 f)) (role ?v11490))
-(<= (next (sat 18)) (does ?v11511 (assign 59 t)) (role ?v11511))
-(<= (next (sat 19)) (does ?v11534 (assign 51 t)) (role ?v11534))
-(<= (next (sat 19)) (does ?v11555 (assign 12 f)) (role ?v11555))
-(<= (next (sat 19)) (does ?v11576 (assign 1 t)) (role ?v11576))
-(<= (next (sat 19)) (does ?v11597 (assign 52 t)) (role ?v11597))
-(<= (next (sat 19)) (does ?v11618 (assign 58 t)) (role ?v11618))
-(<= (next (sat 20)) (does ?v11641 (assign 8 f)) (role ?v11641))
-(<= (next (sat 20)) (does ?v11662 (assign 47 t)) (role ?v11662))
-(<= (next (sat 20)) (does ?v11683 (assign 19 t)) (role ?v11683))
-(<= (next (sat 20)) (does ?v11704 (assign 42 f)) (role ?v11704))
-(<= (next (sat 20)) (does ?v11725 (assign 12 f)) (role ?v11725))
-(<= (next (sat 21)) (does ?v11748 (assign 39 f)) (role ?v11748))
-(<= (next (sat 21)) (does ?v11769 (assign 11 t)) (role ?v11769))
-(<= (next (sat 21)) (does ?v11790 (assign 1 t)) (role ?v11790))
-(<= (next (sat 21)) (does ?v11811 (assign 41 f)) (role ?v11811))
-(<= (next (sat 21)) (does ?v11832 (assign 31 f)) (role ?v11832))
-(<= (next (sat 22)) (does ?v11855 (assign 26 f)) (role ?v11855))
-(<= (next (sat 22)) (does ?v11876 (assign 34 t)) (role ?v11876))
-(<= (next (sat 22)) (does ?v11897 (assign 9 t)) (role ?v11897))
-(<= (next (sat 22)) (does ?v11918 (assign 35 f)) (role ?v11918))
-(<= (next (sat 22)) (does ?v11939 (assign 41 t)) (role ?v11939))
-(<= (next (sat 23)) (does ?v11962 (assign 54 t)) (role ?v11962))
-(<= (next (sat 23)) (does ?v11983 (assign 26 t)) (role ?v11983))
-(<= (next (sat 23)) (does ?v12004 (assign 47 f)) (role ?v12004))
-(<= (next (sat 23)) (does ?v12025 (assign 31 t)) (role ?v12025))
-(<= (next (sat 23)) (does ?v12046 (assign 36 f)) (role ?v12046))
-(<= (next (sat 24)) (does ?v12069 (assign 15 f)) (role ?v12069))
-(<= (next (sat 24)) (does ?v12090 (assign 60 f)) (role ?v12090))
-(<= (next (sat 24)) (does ?v12111 (assign 13 f)) (role ?v12111))
-(<= (next (sat 24)) (does ?v12132 (assign 6 t)) (role ?v12132))
-(<= (next (sat 24)) (does ?v12153 (assign 47 t)) (role ?v12153))
-(<= (next (sat 25)) (does ?v12176 (assign 21 f)) (role ?v12176))
-(<= (next (sat 25)) (does ?v12197 (assign 10 f)) (role ?v12197))
-(<= (next (sat 25)) (does ?v12218 (assign 26 t)) (role ?v12218))
-(<= (next (sat 25)) (does ?v12239 (assign 33 t)) (role ?v12239))
-(<= (next (sat 25)) (does ?v12260 (assign 15 t)) (role ?v12260))
-(<= (next (sat 26)) (does ?v12283 (assign 20 f)) (role ?v12283))
-(<= (next (sat 26)) (does ?v12304 (assign 11 t)) (role ?v12304))
-(<= (next (sat 26)) (does ?v12325 (assign 49 t)) (role ?v12325))
-(<= (next (sat 26)) (does ?v12346 (assign 12 t)) (role ?v12346))
-(<= (next (sat 26)) (does ?v12367 (assign 41 f)) (role ?v12367))
-(<= (next (sat 27)) (does ?v12390 (assign 3 f)) (role ?v12390))
-(<= (next (sat 27)) (does ?v12411 (assign 53 t)) (role ?v12411))
-(<= (next (sat 27)) (does ?v12432 (assign 15 t)) (role ?v12432))
-(<= (next (sat 27)) (does ?v12453 (assign 23 f)) (role ?v12453))
-(<= (next (sat 27)) (does ?v12474 (assign 58 t)) (role ?v12474))
-(<= (next (sat 28)) (does ?v12497 (assign 3 f)) (role ?v12497))
-(<= (next (sat 28)) (does ?v12518 (assign 48 f)) (role ?v12518))
-(<= (next (sat 28)) (does ?v12539 (assign 21 f)) (role ?v12539))
-(<= (next (sat 28)) (does ?v12560 (assign 59 t)) (role ?v12560))
-(<= (next (sat 28)) (does ?v12581 (assign 46 t)) (role ?v12581))
-(<= (next (sat 29)) (does ?v12604 (assign 28 t)) (role ?v12604))
-(<= (next (sat 29)) (does ?v12625 (assign 25 t)) (role ?v12625))
-(<= (next (sat 29)) (does ?v12646 (assign 10 f)) (role ?v12646))
-(<= (next (sat 29)) (does ?v12667 (assign 18 t...
[truncated message content] |
