%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : NLP102+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jul 27 13:06:48 EDT 2022 % Result : Unknown 4.98s 5.16s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP102+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.12 % Command : otter-tptp-script %s % 0.13/0.33 % Computer : n020.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Wed Jul 27 08:43:38 EDT 2022 % 0.13/0.33 % CPUTime : % 1.99/2.18 ----- Otter 3.3f, August 2004 ----- % 1.99/2.18 The process was started by sandbox on n020.cluster.edu, % 1.99/2.18 Wed Jul 27 08:43:38 2022 % 1.99/2.18 The command was "./otter". The process ID is 22354. % 1.99/2.18 % 1.99/2.18 set(prolog_style_variables). % 1.99/2.18 set(auto). % 1.99/2.18 dependent: set(auto1). % 1.99/2.18 dependent: set(process_input). % 1.99/2.18 dependent: clear(print_kept). % 1.99/2.18 dependent: clear(print_new_demod). % 1.99/2.18 dependent: clear(print_back_demod). % 1.99/2.18 dependent: clear(print_back_sub). % 1.99/2.18 dependent: set(control_memory). % 1.99/2.18 dependent: assign(max_mem, 12000). % 1.99/2.18 dependent: assign(pick_given_ratio, 4). % 1.99/2.18 dependent: assign(stats_level, 1). % 1.99/2.18 dependent: assign(max_seconds, 10800). % 1.99/2.18 clear(print_given). % 1.99/2.18 % 1.99/2.18 formula_list(usable). % 1.99/2.18 -(-(-(((exists U (actual_world(U)& (exists V W X Y (coffee(U,V)&restaurant(U,W)&human_person(U,X)&event(U,Y)&agent(U,Y,X)&patient(U,Y,V)&past(U,Y)&nonreflexive(U,Y)&drink(U,Y)& (all Z (customer(U,Z)&in(U,Z,W)-> (exists X1 (event(U,X1)&agent(U,X1,Z)&patient(U,X1,X)&past(U,X1)&nonreflexive(U,X1)&see(U,X1)))))))))-> (exists X2 (actual_world(X2)& (exists X3 (coffee(X2,X3)& (all X4 X5 (customer(X2,X4)&restaurant(X2,X5)&in(X2,X4,X5)-> (exists X6 X7 X8 (human_person(X2,X6)&event(X2,X7)&agent(X2,X7,X6)&patient(X2,X7,X3)&past(X2,X7)&nonreflexive(X2,X7)&drink(X2,X7)&event(X2,X8)&agent(X2,X8,X4)&patient(X2,X8,X6)&past(X2,X8)&nonreflexive(X2,X8)&see(X2,X8))))))))))& ((exists X2 (actual_world(X2)& (exists X3 (coffee(X2,X3)& (all X4 X5 (customer(X2,X4)&restaurant(X2,X5)&in(X2,X4,X5)-> (exists X6 X7 X8 (human_person(X2,X6)&event(X2,X7)&agent(X2,X7,X6)&patient(X2,X7,X3)&past(X2,X7)&nonreflexive(X2,X7)&drink(X2,X7)&event(X2,X8)&agent(X2,X8,X4)&patient(X2,X8,X6)&past(X2,X8)&nonreflexive(X2,X8)&see(X2,X8)))))))))-> (exists U (actual_world(U)& (exists V W X Y (coffee(U,V)&restaurant(U,W)&human_person(U,X)&event(U,Y)&agent(U,Y,X)&patient(U,Y,V)&past(U,Y)&nonreflexive(U,Y)&drink(U,Y)& (all Z (customer(U,Z)&in(U,Z,W)-> (exists X1 (event(U,X1)&agent(U,X1,Z)&patient(U,X1,X)&past(U,X1)&nonreflexive(U,X1)&see(U,X1))))))))))))). % 1.99/2.19 end_of_list. % 1.99/2.19 % 1.99/2.19 -------> usable clausifies to: % 1.99/2.19 % 1.99/2.19 list(usable). % 1.99/2.19 0 [] actual_world($c5)|actual_world($c7). % 1.99/2.19 0 [] actual_world($c5)|coffee($c7,$c6). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] actual_world($c5)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] actual_world($c5)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] actual_world($c5)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] coffee($c5,$c4)|actual_world($c7). % 1.99/2.19 0 [] coffee($c5,$c4)|coffee($c7,$c6). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] coffee($c5,$c4)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] coffee($c5,$c4)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] coffee($c5,$c4)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] restaurant($c5,$c3)|actual_world($c7). % 1.99/2.19 0 [] restaurant($c5,$c3)|coffee($c7,$c6). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] restaurant($c5,$c3)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] restaurant($c5,$c3)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] human_person($c5,$c2)|actual_world($c7). % 1.99/2.19 0 [] human_person($c5,$c2)|coffee($c7,$c6). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] human_person($c5,$c2)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] human_person($c5,$c2)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] human_person($c5,$c2)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] event($c5,$c1)|actual_world($c7). % 1.99/2.19 0 [] event($c5,$c1)|coffee($c7,$c6). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] event($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] event($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] event($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] agent($c5,$c1,$c2)|actual_world($c7). % 1.99/2.19 0 [] agent($c5,$c1,$c2)|coffee($c7,$c6). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] agent($c5,$c1,$c2)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] patient($c5,$c1,$c4)|actual_world($c7). % 1.99/2.19 0 [] patient($c5,$c1,$c4)|coffee($c7,$c6). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] patient($c5,$c1,$c4)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] past($c5,$c1)|actual_world($c7). % 1.99/2.19 0 [] past($c5,$c1)|coffee($c7,$c6). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] past($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] past($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] past($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] nonreflexive($c5,$c1)|actual_world($c7). % 1.99/2.19 0 [] nonreflexive($c5,$c1)|coffee($c7,$c6). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] nonreflexive($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] drink($c5,$c1)|actual_world($c7). % 1.99/2.19 0 [] drink($c5,$c1)|coffee($c7,$c6). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] drink($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] drink($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] drink($c5,$c1)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))|actual_world($c7). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))|coffee($c7,$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|event($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)|actual_world($c7). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)|coffee($c7,$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|agent($c5,$f1(Z),Z)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)|actual_world($c7). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)|coffee($c7,$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|patient($c5,$f1(Z),$c2)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))|actual_world($c7). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))|coffee($c7,$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|past($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))|actual_world($c7). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))|coffee($c7,$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|nonreflexive($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))|actual_world($c7). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))|coffee($c7,$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] -customer($c5,Z)| -in($c5,Z,$c3)|see($c5,$f1(Z))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))|actual_world($c7). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))|coffee($c7,$c6). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|customer(X2,$f3(X2,X3))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))|actual_world($c7). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))|coffee($c7,$c6). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|restaurant(X2,$f2(X2,X3))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))|actual_world($c7). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))|coffee($c7,$c6). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.19 0 [] -actual_world(X2)| -coffee(X2,X3)|in(X2,$f3(X2,X3),$f2(X2,X3))| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)|actual_world($c7). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)|coffee($c7,$c6). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|human_person($c7,$f6(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f5(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f5(X4,X5),$f6(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f5(X4,X5),$c6). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f5(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f5(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|drink($c7,$f5(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|event($c7,$f4(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|agent($c7,$f4(X4,X5),X4). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|patient($c7,$f4(X4,X5),$f6(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|past($c7,$f4(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|nonreflexive($c7,$f4(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -customer($c7,X4)| -restaurant($c7,X5)| -in($c7,X4,X5)|see($c7,$f4(X4,X5)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|customer(U,$f7(U,V,W,X,Y)). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)|in(U,$f7(U,V,W,X,Y),W). % 1.99/2.20 0 [] -actual_world(X2)| -coffee(X2,X3)| -human_person(X2,X6)| -event(X2,X7)| -agent(X2,X7,X6)| -patient(X2,X7,X3)| -past(X2,X7)| -nonreflexive(X2,X7)| -drink(X2,X7)| -event(X2,X8)| -agent(X2,X8,$f3(X2,X3))| -patient(X2,X8,X6)| -past(X2,X8)| -nonreflexive(X2,X8)| -see(X2,X8)| -actual_world(U)| -coffee(U,V)| -restaurant(U,W)| -human_person(U,X)| -event(U,Y)| -agent(U,Y,X)| -patient(U,Y,V)| -past(U,Y)| -nonreflexive(U,Y)| -drink(U,Y)| -event(U,X1)| -agent(U,X1,$f7(U,V,W,X,Y))| -patient(U,X1,X)| -past(U,X1)| -nonreflexive(U,X1)| -see(U,X1). % 1.99/2.20 end_of_list. % 1.99/2.20 % 1.99/2.20 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=31. % 1.99/2.20 % 1.99/2.20 This is a non-Horn set without equality. The strategy will % 1.99/2.20 be ordered hyper_res, unit deletion, and factoring, with % 1.99/2.20 satellites in sos and with nuclei in usable. % 1.99/2.20 % 1.99/2.20 dependent: set(hyper_res). % 1.99/2.20 dependent: set(factor). % 1.99/2.20 dependent: set(unit_deletion). % 1.99/2.20 % 1.99/2.20 ------------> process usable: % 1.99/2.20 ** KEPT (pick-wt=17): 1 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|human_person($c7,$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=17): 2 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=20): 3 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f5(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 4 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f5(A,B),$c6). % 1.99/2.20 ** KEPT (pick-wt=17): 5 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=17): 6 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=17): 7 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|drink($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=17): 8 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 9 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f4(A,B),A). % 1.99/2.20 ** KEPT (pick-wt=20): 10 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f4(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=17): 11 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=17): 12 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=17): 13 [] actual_world($c5)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|see($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=41): 14 [] actual_world($c5)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|customer(A,$f7(A,B,C,D,E)). % 1.99/2.20 ** KEPT (pick-wt=42): 15 [] actual_world($c5)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|in(A,$f7(A,B,C,D,E),C). % 1.99/2.20 ** KEPT (pick-wt=58): 16 [] actual_world($c5)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)| -event(A,F)| -agent(A,F,$f7(A,B,C,D,E))| -patient(A,F,D)| -past(A,F)| -nonreflexive(A,F)| -see(A,F). % 1.99/2.20 ** KEPT (pick-wt=18): 17 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|human_person($c7,$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 18 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=21): 19 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f5(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 20 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f5(A,B),$c6). % 1.99/2.20 ** KEPT (pick-wt=18): 21 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 22 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 23 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|drink($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 24 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 25 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f4(A,B),A). % 1.99/2.20 ** KEPT (pick-wt=21): 26 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f4(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 27 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 28 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 29 [] coffee($c5,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|see($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=42): 30 [] coffee($c5,$c4)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|customer(A,$f7(A,B,C,D,E)). % 1.99/2.20 ** KEPT (pick-wt=43): 31 [] coffee($c5,$c4)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|in(A,$f7(A,B,C,D,E),C). % 1.99/2.20 ** KEPT (pick-wt=59): 32 [] coffee($c5,$c4)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)| -event(A,F)| -agent(A,F,$f7(A,B,C,D,E))| -patient(A,F,D)| -past(A,F)| -nonreflexive(A,F)| -see(A,F). % 1.99/2.20 ** KEPT (pick-wt=18): 33 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|human_person($c7,$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 34 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=21): 35 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f5(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 36 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f5(A,B),$c6). % 1.99/2.20 ** KEPT (pick-wt=18): 37 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 38 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 39 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|drink($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 40 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 41 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f4(A,B),A). % 1.99/2.20 ** KEPT (pick-wt=21): 42 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f4(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 43 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 44 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 45 [] restaurant($c5,$c3)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|see($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=42): 46 [] restaurant($c5,$c3)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|customer(A,$f7(A,B,C,D,E)). % 1.99/2.20 ** KEPT (pick-wt=43): 47 [] restaurant($c5,$c3)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|in(A,$f7(A,B,C,D,E),C). % 1.99/2.20 ** KEPT (pick-wt=59): 48 [] restaurant($c5,$c3)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)| -event(A,F)| -agent(A,F,$f7(A,B,C,D,E))| -patient(A,F,D)| -past(A,F)| -nonreflexive(A,F)| -see(A,F). % 1.99/2.20 ** KEPT (pick-wt=18): 49 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|human_person($c7,$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 50 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=21): 51 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f5(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 52 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f5(A,B),$c6). % 1.99/2.20 ** KEPT (pick-wt=18): 53 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 54 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 55 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|drink($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 56 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 57 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f4(A,B),A). % 1.99/2.20 ** KEPT (pick-wt=21): 58 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f4(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 59 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 60 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 61 [] human_person($c5,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|see($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=42): 62 [] human_person($c5,$c2)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|customer(A,$f7(A,B,C,D,E)). % 1.99/2.20 ** KEPT (pick-wt=43): 63 [] human_person($c5,$c2)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|in(A,$f7(A,B,C,D,E),C). % 1.99/2.20 ** KEPT (pick-wt=59): 64 [] human_person($c5,$c2)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)| -event(A,F)| -agent(A,F,$f7(A,B,C,D,E))| -patient(A,F,D)| -past(A,F)| -nonreflexive(A,F)| -see(A,F). % 1.99/2.20 ** KEPT (pick-wt=18): 65 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|human_person($c7,$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 66 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=21): 67 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f5(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 68 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f5(A,B),$c6). % 1.99/2.20 ** KEPT (pick-wt=18): 69 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 70 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 71 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|drink($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 72 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 73 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f4(A,B),A). % 1.99/2.20 ** KEPT (pick-wt=21): 74 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f4(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 75 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 76 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=18): 77 [] event($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|see($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=42): 78 [] event($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|customer(A,$f7(A,B,C,D,E)). % 1.99/2.20 ** KEPT (pick-wt=43): 79 [] event($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|in(A,$f7(A,B,C,D,E),C). % 1.99/2.20 ** KEPT (pick-wt=59): 80 [] event($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)| -event(A,F)| -agent(A,F,$f7(A,B,C,D,E))| -patient(A,F,D)| -past(A,F)| -nonreflexive(A,F)| -see(A,F). % 1.99/2.20 ** KEPT (pick-wt=19): 81 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|human_person($c7,$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 82 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=22): 83 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f5(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=20): 84 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f5(A,B),$c6). % 1.99/2.20 ** KEPT (pick-wt=19): 85 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 86 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 87 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|drink($c7,$f5(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 88 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=20): 89 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f4(A,B),A). % 1.99/2.20 ** KEPT (pick-wt=22): 90 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f4(A,B),$f6(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 91 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f4(A,B)). % 1.99/2.20 ** KEPT (pick-wt=19): 92 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 93 [] agent($c5,$c1,$c2)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|see($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=43): 94 [] agent($c5,$c1,$c2)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|customer(A,$f7(A,B,C,D,E)). % 1.99/2.21 ** KEPT (pick-wt=44): 95 [] agent($c5,$c1,$c2)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|in(A,$f7(A,B,C,D,E),C). % 1.99/2.21 ** KEPT (pick-wt=60): 96 [] agent($c5,$c1,$c2)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)| -event(A,F)| -agent(A,F,$f7(A,B,C,D,E))| -patient(A,F,D)| -past(A,F)| -nonreflexive(A,F)| -see(A,F). % 1.99/2.21 ** KEPT (pick-wt=19): 97 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|human_person($c7,$f6(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 98 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=22): 99 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f5(A,B),$f6(A,B)). % 1.99/2.21 ** KEPT (pick-wt=20): 100 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f5(A,B),$c6). % 1.99/2.21 ** KEPT (pick-wt=19): 101 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 102 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 103 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|drink($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 104 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=20): 105 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f4(A,B),A). % 1.99/2.21 ** KEPT (pick-wt=22): 106 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f4(A,B),$f6(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 107 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 108 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 109 [] patient($c5,$c1,$c4)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|see($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=43): 110 [] patient($c5,$c1,$c4)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|customer(A,$f7(A,B,C,D,E)). % 1.99/2.21 ** KEPT (pick-wt=44): 111 [] patient($c5,$c1,$c4)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|in(A,$f7(A,B,C,D,E),C). % 1.99/2.21 ** KEPT (pick-wt=60): 112 [] patient($c5,$c1,$c4)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)| -event(A,F)| -agent(A,F,$f7(A,B,C,D,E))| -patient(A,F,D)| -past(A,F)| -nonreflexive(A,F)| -see(A,F). % 1.99/2.21 ** KEPT (pick-wt=18): 113 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|human_person($c7,$f6(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 114 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=21): 115 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f5(A,B),$f6(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 116 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f5(A,B),$c6). % 1.99/2.21 ** KEPT (pick-wt=18): 117 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 118 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 119 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|drink($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 120 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 121 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f4(A,B),A). % 1.99/2.21 ** KEPT (pick-wt=21): 122 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f4(A,B),$f6(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 123 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 124 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 125 [] past($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|see($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=42): 126 [] past($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|customer(A,$f7(A,B,C,D,E)). % 1.99/2.21 ** KEPT (pick-wt=43): 127 [] past($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|in(A,$f7(A,B,C,D,E),C). % 1.99/2.21 ** KEPT (pick-wt=59): 128 [] past($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)| -event(A,F)| -agent(A,F,$f7(A,B,C,D,E))| -patient(A,F,D)| -past(A,F)| -nonreflexive(A,F)| -see(A,F). % 1.99/2.21 ** KEPT (pick-wt=18): 129 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|human_person($c7,$f6(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 130 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=21): 131 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f5(A,B),$f6(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 132 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f5(A,B),$c6). % 1.99/2.21 ** KEPT (pick-wt=18): 133 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 134 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 135 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|drink($c7,$f5(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 136 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=19): 137 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f4(A,B),A). % 1.99/2.21 ** KEPT (pick-wt=21): 138 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f4(A,B),$f6(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 139 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 140 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=18): 141 [] nonreflexive($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|see($c7,$f4(A,B)). % 1.99/2.21 ** KEPT (pick-wt=42): 142 [] nonreflexive($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|customer(A,$f7(A,B,C,D,E)). % 1.99/2.21 ** KEPT (pick-wt=43): 143 [] nonreflexive($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|in(A,$f7(A,B,C,D,E),C). % 1.99/2.21 ** KEPT (pick-wt=59): 144 [] nonreflexive($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)| -event(A,F)| -agent(A,F,$f7(A,B,C,D,E))| -patient(A,F,D)| -past(A,F)| -nonreflexive(A,F)| -see(A,F). % 1.99/2.21 ** KEPT (pick-wt=18): 145 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|human_person($c7,$f6(A,B)). % 2.07/2.21 ** KEPT (pick-wt=18): 146 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f5(A,B)). % 2.07/2.21 ** KEPT (pick-wt=21): 147 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f5(A,B),$f6(A,B)). % 2.07/2.21 ** KEPT (pick-wt=19): 148 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f5(A,B),$c6). % 2.07/2.21 ** KEPT (pick-wt=18): 149 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f5(A,B)). % 2.07/2.21 ** KEPT (pick-wt=18): 150 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f5(A,B)). % 2.07/2.21 ** KEPT (pick-wt=18): 151 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|drink($c7,$f5(A,B)). % 2.07/2.21 ** KEPT (pick-wt=18): 152 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|event($c7,$f4(A,B)). % 2.07/2.21 ** KEPT (pick-wt=19): 153 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|agent($c7,$f4(A,B),A). % 2.07/2.21 ** KEPT (pick-wt=21): 154 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|patient($c7,$f4(A,B),$f6(A,B)). % 2.07/2.21 ** KEPT (pick-wt=18): 155 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|past($c7,$f4(A,B)). % 2.07/2.21 ** KEPT (pick-wt=18): 156 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|nonreflexive($c7,$f4(A,B)). % 2.07/2.21 ** KEPT (pick-wt=18): 157 [] drink($c5,$c1)| -customer($c7,A)| -restaurant($c7,B)| -in($c7,A,B)|see($c7,$f4(A,B)). % 2.07/2.21 ** KEPT (pick-wt=42): 158 [] drink($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|customer(A,$f7(A,B,C,D,E)). % 2.07/2.21 ** KEPT (pick-wt=43): 159 [] drink($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)|in(A,$f7(A,B,C,D,E),C). % 2.07/2.21 ** KEPT (pick-wt=59): 160 [] drink($c5,$c1)| -actual_world(A)| -coffee(A,B)| -restaurant(A,C)| -human_person(A,D)| -event(A,E)| -agent(A,E,D)| -patient(A,E,B)| -past(A,E)| -nonreflexive(A,E)| -drink(A,E)| -event(A,F)| -agent(A,F,$f7(A,B,C,D,E))| -patient(A,F,D)| -past(A,F)| -nonreflexive(A,F)| -see(A,F). % 2.07/2.21 ** KEPT (pick-wt=13): 161 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))|actual_world($c7). % 2.07/2.21 ** KEPT (pick-wt=14): 162 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))|coffee($c7,$c6). % 2.07/2.21 ** KEPT (pick-wt=26): 163 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|human_person($c7,$f6(B,C)). % 2.07/2.21 ** KEPT (pick-wt=26): 164 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f5(B,C)). % 2.07/2.21 ** KEPT (pick-wt=29): 165 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f5(B,C),$f6(B,C)). % 2.07/2.21 ** KEPT (pick-wt=27): 166 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f5(B,C),$c6). % 2.07/2.21 ** KEPT (pick-wt=26): 167 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f5(B,C)). % 2.07/2.21 ** KEPT (pick-wt=26): 168 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f5(B,C)). % 2.07/2.21 ** KEPT (pick-wt=26): 169 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|drink($c7,$f5(B,C)). % 2.07/2.21 ** KEPT (pick-wt=26): 170 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f4(B,C)). % 2.07/2.21 ** KEPT (pick-wt=27): 171 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f4(B,C),B). % 2.07/2.21 ** KEPT (pick-wt=29): 172 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f4(B,C),$f6(B,C)). % 2.07/2.21 ** KEPT (pick-wt=26): 173 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=26): 174 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=26): 175 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|see($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=50): 176 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|customer(B,$f7(B,C,D,E,F)). % 2.07/2.22 ** KEPT (pick-wt=51): 177 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|in(B,$f7(B,C,D,E,F),D). % 2.07/2.22 ** KEPT (pick-wt=67): 178 [] -customer($c5,A)| -in($c5,A,$c3)|event($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)| -event(B,G)| -agent(B,G,$f7(B,C,D,E,F))| -patient(B,G,E)| -past(B,G)| -nonreflexive(B,G)| -see(B,G). % 2.07/2.22 ** KEPT (pick-wt=14): 179 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)|actual_world($c7). % 2.07/2.22 ** KEPT (pick-wt=15): 180 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)|coffee($c7,$c6). % 2.07/2.22 ** KEPT (pick-wt=27): 181 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|human_person($c7,$f6(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 182 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f5(B,C)). % 2.07/2.22 ** KEPT (pick-wt=30): 183 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f5(B,C),$f6(B,C)). % 2.07/2.22 ** KEPT (pick-wt=28): 184 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f5(B,C),$c6). % 2.07/2.22 ** KEPT (pick-wt=27): 185 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f5(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 186 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f5(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 187 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|drink($c7,$f5(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 188 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=28): 189 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f4(B,C),B). % 2.07/2.22 ** KEPT (pick-wt=30): 190 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f4(B,C),$f6(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 191 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 192 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 193 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|see($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=51): 194 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|customer(B,$f7(B,C,D,E,F)). % 2.07/2.22 ** KEPT (pick-wt=52): 195 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|in(B,$f7(B,C,D,E,F),D). % 2.07/2.22 ** KEPT (pick-wt=68): 196 [] -customer($c5,A)| -in($c5,A,$c3)|agent($c5,$f1(A),A)| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)| -event(B,G)| -agent(B,G,$f7(B,C,D,E,F))| -patient(B,G,E)| -past(B,G)| -nonreflexive(B,G)| -see(B,G). % 2.07/2.22 ** KEPT (pick-wt=14): 197 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)|actual_world($c7). % 2.07/2.22 ** KEPT (pick-wt=15): 198 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)|coffee($c7,$c6). % 2.07/2.22 ** KEPT (pick-wt=27): 199 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|human_person($c7,$f6(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 200 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f5(B,C)). % 2.07/2.22 ** KEPT (pick-wt=30): 201 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f5(B,C),$f6(B,C)). % 2.07/2.22 ** KEPT (pick-wt=28): 202 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f5(B,C),$c6). % 2.07/2.22 ** KEPT (pick-wt=27): 203 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f5(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 204 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f5(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 205 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|drink($c7,$f5(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 206 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=28): 207 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f4(B,C),B). % 2.07/2.22 ** KEPT (pick-wt=30): 208 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f4(B,C),$f6(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 209 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 210 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=27): 211 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|see($c7,$f4(B,C)). % 2.07/2.22 ** KEPT (pick-wt=51): 212 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|customer(B,$f7(B,C,D,E,F)). % 2.07/2.22 ** KEPT (pick-wt=52): 213 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|in(B,$f7(B,C,D,E,F),D). % 2.07/2.22 ** KEPT (pick-wt=68): 214 [] -customer($c5,A)| -in($c5,A,$c3)|patient($c5,$f1(A),$c2)| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)| -event(B,G)| -agent(B,G,$f7(B,C,D,E,F))| -patient(B,G,E)| -past(B,G)| -nonreflexive(B,G)| -see(B,G). % 2.07/2.22 ** KEPT (pick-wt=13): 215 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))|actual_world($c7). % 2.07/2.22 ** KEPT (pick-wt=14): 216 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))|coffee($c7,$c6). % 2.07/2.22 ** KEPT (pick-wt=26): 217 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|human_person($c7,$f6(B,C)). % 2.07/2.22 ** KEPT (pick-wt=26): 218 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f5(B,C)). % 2.07/2.22 ** KEPT (pick-wt=29): 219 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f5(B,C),$f6(B,C)). % 2.07/2.23 ** KEPT (pick-wt=27): 220 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f5(B,C),$c6). % 2.07/2.23 ** KEPT (pick-wt=26): 221 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 222 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 223 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|drink($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 224 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=27): 225 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f4(B,C),B). % 2.07/2.23 ** KEPT (pick-wt=29): 226 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f4(B,C),$f6(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 227 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 228 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 229 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|see($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=50): 230 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|customer(B,$f7(B,C,D,E,F)). % 2.07/2.23 ** KEPT (pick-wt=51): 231 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|in(B,$f7(B,C,D,E,F),D). % 2.07/2.23 ** KEPT (pick-wt=67): 232 [] -customer($c5,A)| -in($c5,A,$c3)|past($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)| -event(B,G)| -agent(B,G,$f7(B,C,D,E,F))| -patient(B,G,E)| -past(B,G)| -nonreflexive(B,G)| -see(B,G). % 2.07/2.23 ** KEPT (pick-wt=13): 233 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))|actual_world($c7). % 2.07/2.23 ** KEPT (pick-wt=14): 234 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))|coffee($c7,$c6). % 2.07/2.23 ** KEPT (pick-wt=26): 235 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|human_person($c7,$f6(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 236 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=29): 237 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f5(B,C),$f6(B,C)). % 2.07/2.23 ** KEPT (pick-wt=27): 238 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f5(B,C),$c6). % 2.07/2.23 ** KEPT (pick-wt=26): 239 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 240 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 241 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|drink($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 242 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=27): 243 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f4(B,C),B). % 2.07/2.23 ** KEPT (pick-wt=29): 244 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f4(B,C),$f6(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 245 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 246 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 247 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|see($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=50): 248 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|customer(B,$f7(B,C,D,E,F)). % 2.07/2.23 ** KEPT (pick-wt=51): 249 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|in(B,$f7(B,C,D,E,F),D). % 2.07/2.23 ** KEPT (pick-wt=67): 250 [] -customer($c5,A)| -in($c5,A,$c3)|nonreflexive($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)| -event(B,G)| -agent(B,G,$f7(B,C,D,E,F))| -patient(B,G,E)| -past(B,G)| -nonreflexive(B,G)| -see(B,G). % 2.07/2.23 ** KEPT (pick-wt=13): 251 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))|actual_world($c7). % 2.07/2.23 ** KEPT (pick-wt=14): 252 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))|coffee($c7,$c6). % 2.07/2.23 ** KEPT (pick-wt=26): 253 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|human_person($c7,$f6(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 254 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=29): 255 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f5(B,C),$f6(B,C)). % 2.07/2.23 ** KEPT (pick-wt=27): 256 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f5(B,C),$c6). % 2.07/2.23 ** KEPT (pick-wt=26): 257 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 258 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 259 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|drink($c7,$f5(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 260 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|event($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=27): 261 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|agent($c7,$f4(B,C),B). % 2.07/2.23 ** KEPT (pick-wt=29): 262 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|patient($c7,$f4(B,C),$f6(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 263 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|past($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 264 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|nonreflexive($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=26): 265 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -customer($c7,B)| -restaurant($c7,C)| -in($c7,B,C)|see($c7,$f4(B,C)). % 2.07/2.23 ** KEPT (pick-wt=50): 266 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|customer(B,$f7(B,C,D,E,F)). % 2.07/2.24 ** KEPT (pick-wt=51): 267 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)|in(B,$f7(B,C,D,E,F),D). % 2.07/2.24 ** KEPT (pick-wt=67): 268 [] -customer($c5,A)| -in($c5,A,$c3)|see($c5,$f1(A))| -actual_world(B)| -coffee(B,C)| -restaurant(B,D)| -human_person(B,E)| -event(B,F)| -agent(B,F,E)| -patient(B,F,C)| -past(B,F)| -nonreflexive(B,F)| -drink(B,F)| -event(B,G)| -agent(B,G,$f7(B,C,D,E,F))| -patient(B,G,E)| -past(B,G)| -nonreflexive(B,G)| -see(B,G). % 2.07/2.24 ** KEPT (pick-wt=12): 269 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))|actual_world($c7). % 2.07/2.24 ** KEPT (pick-wt=13): 270 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))|coffee($c7,$c6). % 2.07/2.24 ** KEPT (pick-wt=25): 271 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|human_person($c7,$f6(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 272 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|event($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=28): 273 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|agent($c7,$f5(C,D),$f6(C,D)). % 2.07/2.24 ** KEPT (pick-wt=26): 274 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|patient($c7,$f5(C,D),$c6). % 2.07/2.24 ** KEPT (pick-wt=25): 275 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|past($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 276 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|nonreflexive($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 277 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|drink($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 278 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|event($c7,$f4(C,D)). % 2.07/2.24 ** KEPT (pick-wt=26): 279 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|agent($c7,$f4(C,D),C). % 2.07/2.24 ** KEPT (pick-wt=28): 280 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|patient($c7,$f4(C,D),$f6(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 281 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|past($c7,$f4(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 282 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|nonreflexive($c7,$f4(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 283 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|see($c7,$f4(C,D)). % 2.07/2.24 ** KEPT (pick-wt=49): 284 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -actual_world(C)| -coffee(C,D)| -restaurant(C,E)| -human_person(C,F)| -event(C,G)| -agent(C,G,F)| -patient(C,G,D)| -past(C,G)| -nonreflexive(C,G)| -drink(C,G)|customer(C,$f7(C,D,E,F,G)). % 2.07/2.24 ** KEPT (pick-wt=50): 285 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -actual_world(C)| -coffee(C,D)| -restaurant(C,E)| -human_person(C,F)| -event(C,G)| -agent(C,G,F)| -patient(C,G,D)| -past(C,G)| -nonreflexive(C,G)| -drink(C,G)|in(C,$f7(C,D,E,F,G),E). % 2.07/2.24 ** KEPT (pick-wt=66): 286 [] -actual_world(A)| -coffee(A,B)|customer(A,$f3(A,B))| -actual_world(C)| -coffee(C,D)| -restaurant(C,E)| -human_person(C,F)| -event(C,G)| -agent(C,G,F)| -patient(C,G,D)| -past(C,G)| -nonreflexive(C,G)| -drink(C,G)| -event(C,H)| -agent(C,H,$f7(C,D,E,F,G))| -patient(C,H,F)| -past(C,H)| -nonreflexive(C,H)| -see(C,H). % 2.07/2.24 ** KEPT (pick-wt=12): 287 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))|actual_world($c7). % 2.07/2.24 ** KEPT (pick-wt=13): 288 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))|coffee($c7,$c6). % 2.07/2.24 ** KEPT (pick-wt=25): 289 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|human_person($c7,$f6(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 290 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|event($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=28): 291 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|agent($c7,$f5(C,D),$f6(C,D)). % 2.07/2.24 ** KEPT (pick-wt=26): 292 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|patient($c7,$f5(C,D),$c6). % 2.07/2.24 ** KEPT (pick-wt=25): 293 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|past($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 294 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|nonreflexive($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 295 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|drink($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 296 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|event($c7,$f4(C,D)). % 2.07/2.24 ** KEPT (pick-wt=26): 297 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|agent($c7,$f4(C,D),C). % 2.07/2.24 ** KEPT (pick-wt=28): 298 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|patient($c7,$f4(C,D),$f6(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 299 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|past($c7,$f4(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 300 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|nonreflexive($c7,$f4(C,D)). % 2.07/2.24 ** KEPT (pick-wt=25): 301 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|see($c7,$f4(C,D)). % 2.07/2.24 ** KEPT (pick-wt=49): 302 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -actual_world(C)| -coffee(C,D)| -restaurant(C,E)| -human_person(C,F)| -event(C,G)| -agent(C,G,F)| -patient(C,G,D)| -past(C,G)| -nonreflexive(C,G)| -drink(C,G)|customer(C,$f7(C,D,E,F,G)). % 2.07/2.24 ** KEPT (pick-wt=50): 303 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -actual_world(C)| -coffee(C,D)| -restaurant(C,E)| -human_person(C,F)| -event(C,G)| -agent(C,G,F)| -patient(C,G,D)| -past(C,G)| -nonreflexive(C,G)| -drink(C,G)|in(C,$f7(C,D,E,F,G),E). % 2.07/2.24 ** KEPT (pick-wt=66): 304 [] -actual_world(A)| -coffee(A,B)|restaurant(A,$f2(A,B))| -actual_world(C)| -coffee(C,D)| -restaurant(C,E)| -human_person(C,F)| -event(C,G)| -agent(C,G,F)| -patient(C,G,D)| -past(C,G)| -nonreflexive(C,G)| -drink(C,G)| -event(C,H)| -agent(C,H,$f7(C,D,E,F,G))| -patient(C,H,F)| -past(C,H)| -nonreflexive(C,H)| -see(C,H). % 2.07/2.24 ** KEPT (pick-wt=15): 305 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))|actual_world($c7). % 2.07/2.24 ** KEPT (pick-wt=16): 306 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))|coffee($c7,$c6). % 2.07/2.24 ** KEPT (pick-wt=28): 307 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|human_person($c7,$f6(C,D)). % 2.07/2.24 ** KEPT (pick-wt=28): 308 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|event($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=31): 309 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|agent($c7,$f5(C,D),$f6(C,D)). % 2.07/2.24 ** KEPT (pick-wt=29): 310 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|patient($c7,$f5(C,D),$c6). % 2.07/2.24 ** KEPT (pick-wt=28): 311 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|past($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=28): 312 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|nonreflexive($c7,$f5(C,D)). % 2.07/2.24 ** KEPT (pick-wt=28): 313 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|drink($c7,$f5(C,D)). % 2.07/2.26 ** KEPT (pick-wt=28): 314 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|event($c7,$f4(C,D)). % 2.07/2.26 ** KEPT (pick-wt=29): 315 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|agent($c7,$f4(C,D),C). % 2.07/2.26 ** KEPT (pick-wt=31): 316 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|patient($c7,$f4(C,D),$f6(C,D)). % 2.07/2.26 ** KEPT (pick-wt=28): 317 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|past($c7,$f4(C,D)). % 2.07/2.26 ** KEPT (pick-wt=28): 318 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|nonreflexive($c7,$f4(C,D)). % 2.07/2.26 ** KEPT (pick-wt=28): 319 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -customer($c7,C)| -restaurant($c7,D)| -in($c7,C,D)|see($c7,$f4(C,D)). % 2.07/2.26 ** KEPT (pick-wt=52): 320 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -actual_world(C)| -coffee(C,D)| -restaurant(C,E)| -human_person(C,F)| -event(C,G)| -agent(C,G,F)| -patient(C,G,D)| -past(C,G)| -nonreflexive(C,G)| -drink(C,G)|customer(C,$f7(C,D,E,F,G)). % 2.07/2.26 ** KEPT (pick-wt=53): 321 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -actual_world(C)| -coffee(C,D)| -restaurant(C,E)| -human_person(C,F)| -event(C,G)| -agent(C,G,F)| -patient(C,G,D)| -past(C,G)| -nonreflexive(C,G)| -drink(C,G)|in(C,$f7(C,D,E,F,G),E). % 2.07/2.26 ** KEPT (pick-wt=69): 322 [] -actual_world(A)| -coffee(A,B)|in(A,$f3(A,B),$f2(A,B))| -actual_world(C)| -coffee(C,D)| -restaurant(C,E)| -human_person(C,F)| -event(C,G)| -agent(C,G,F)| -patient(C,G,D)| -past(C,G)| -nonreflexive(C,G)| -drink(C,G)| -event(C,H)| -agent(C,H,$f7(C,D,E,F,G))| -patient(C,H,F)| -past(C,H)| -nonreflexive(C,H)| -see(C,H). % 2.07/2.26 ** KEPT (pick-wt=52): 323 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)|actual_world($c7). % 2.07/2.26 ** KEPT (pick-wt=53): 324 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)|coffee($c7,$c6). % 2.07/2.26 ** KEPT (pick-wt=65): 325 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|human_person($c7,$f6(F,G)). % 2.07/2.26 ** KEPT (pick-wt=65): 326 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|event($c7,$f5(F,G)). % 2.07/2.26 ** KEPT (pick-wt=68): 327 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|agent($c7,$f5(F,G),$f6(F,G)). % 2.07/2.26 ** KEPT (pick-wt=66): 328 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|patient($c7,$f5(F,G),$c6). % 2.07/2.26 ** KEPT (pick-wt=65): 329 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|past($c7,$f5(F,G)). % 4.77/4.92 ** KEPT (pick-wt=65): 330 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|nonreflexive($c7,$f5(F,G)). % 4.77/4.92 ** KEPT (pick-wt=65): 331 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|drink($c7,$f5(F,G)). % 4.77/4.92 ** KEPT (pick-wt=65): 332 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|event($c7,$f4(F,G)). % 4.77/4.92 ** KEPT (pick-wt=66): 333 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|agent($c7,$f4(F,G),F). % 4.77/4.92 ** KEPT (pick-wt=68): 334 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|patient($c7,$f4(F,G),$f6(F,G)). % 4.77/4.92 ** KEPT (pick-wt=65): 335 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|past($c7,$f4(F,G)). % 4.77/4.92 ** KEPT (pick-wt=65): 336 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|nonreflexive($c7,$f4(F,G)). % 4.77/4.92 ** KEPT (pick-wt=65): 337 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -customer($c7,F)| -restaurant($c7,G)| -in($c7,F,G)|see($c7,$f4(F,G)). % 4.77/4.92 ** KEPT (pick-wt=89): 338 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -actual_world(F)| -coffee(F,G)| -restaurant(F,H)| -human_person(F,I)| -event(F,J)| -agent(F,J,I)| -patient(F,J,G)| -past(F,J)| -nonreflexive(F,J)| -drink(F,J)|customer(F,$f7(F,G,H,I,J)). % 4.77/4.92 ** KEPT (pick-wt=90): 339 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -actual_world(F)| -coffee(F,G)| -restaurant(F,H)| -human_person(F,I)| -event(F,J)| -agent(F,J,I)| -patient(F,J,G)| -past(F,J)| -nonreflexive(F,J)| -drink(F,J)|in(F,$f7(F,G,H,I,J),H). % 4.77/4.92 ** KEPT (pick-wt=106): 340 [] -actual_world(A)| -coffee(A,B)| -human_person(A,C)| -event(A,D)| -agent(A,D,C)| -patient(A,D,B)| -past(A,D)| -nonreflexive(A,D)| -drink(A,D)| -event(A,E)| -agent(A,E,$f3(A,B))| -patient(A,E,C)| -past(A,E)| -nonreflexive(A,E)| -see(A,E)| -actual_world(F)| -coffee(F,G)| -restaurant(F,H)| -human_person(F,I)| -event(F,J)| -agent(F,J,I)| -patient(F,J,G)| -past(F,J)| -nonreflexive(F,J)| -drink(F,J)| -event(F,K)| -agent(F,K,$f7(F,G,H,I,J))| -patient(F,K,I)| -past(F,K)| -nonreflexive(F,K)| -see(F,K). % 4.98/5.16 % 4.98/5.16 ------------> process sos: % 4.98/5.16 ** KEPT (pick-wt=4): 710 [] actual_world($c5)|actual_world($c7). % 4.98/5.16 ** KEPT (pick-wt=5): 711 [] actual_world($c5)|coffee($c7,$c6). % 4.98/5.16 ** KEPT (pick-wt=5): 712 [] coffee($c5,$c4)|actual_world($c7). % 4.98/5.16 ** KEPT (pick-wt=6): 713 [] coffee($c5,$c4)|coffee($c7,$c6). % 4.98/5.16 ** KEPT (pick-wt=5): 714 [] restaurant($c5,$c3)|actual_world($c7). % 4.98/5.16 ** KEPT (pick-wt=6): 715 [] restaurant($c5,$c3)|coffee($c7,$c6). % 4.98/5.16 ** KEPT (pick-wt=5): 716 [] human_person($c5,$c2)|actual_world($c7). % 4.98/5.16 ** KEPT (pick-wt=6): 717 [] human_person($c5,$c2)|coffee($c7,$c6). % 4.98/5.16 ** KEPT (pick-wt=5): 718 [] event($c5,$c1)|actual_world($c7). % 4.98/5.16 ** KEPT (pick-wt=6): 719 [] event($c5,$c1)|coffee($c7,$c6). % 4.98/5.16 ** KEPT (pick-wt=6): 720 [] agent($c5,$c1,$c2)|actual_world($c7). % 4.98/5.16 ** KEPT (pick-wt=7): 721 [] agent($c5,$c1,$c2)|coffee($c7,$c6). % 4.98/5.16 ** KEPT (pick-wt=6): 722 [] patient($c5,$c1,$c4)|actual_world($c7). % 4.98/5.16 ** KEPT (pick-wt=7): 723 [] patient($c5,$c1,$c4)|coffee($c7,$c6). % 4.98/5.16 ** KEPT (pick-wt=5): 724 [] past($c5,$c1)|actual_world($c7). % 4.98/5.16 ** KEPT (pick-wt=6): 725 [] past($c5,$c1)|coffee($c7,$c6). % 4.98/5.16 ** KEPT (pick-wt=5): 726 [] nonreflexive($c5,$c1)|actual_world($c7). % 4.98/5.16 ** KEPT (pick-wt=6): 727 [] nonreflexive($c5,$c1)|coffee($c7,$c6). % 4.98/5.16 ** KEPT (pick-wt=5): 728 [] drink($c5,$c1)|actual_world($c7). % 4.98/5.16 ** KEPT (pick-wt=6): 729 [] drink($c5,$c1)|coffee($c7,$c6). % 4.98/5.16 % 4.98/5.16 ======= end of input processing ======= % 4.98/5.16 % 4.98/5.16 =========== start of search =========== % 4.98/5.16 % 4.98/5.16 Search stopped because sos empty. % 4.98/5.16 % 4.98/5.16 % 4.98/5.16 Search stopped because sos empty. % 4.98/5.16 % 4.98/5.16 ============ end of search ============ % 4.98/5.16 % 4.98/5.16 -------------- statistics ------------- % 4.98/5.16 clauses given 23 % 4.98/5.16 clauses generated 3323 % 4.98/5.16 clauses kept 732 % 4.98/5.16 clauses forward subsumed 2951 % 4.98/5.16 clauses back subsumed 0 % 4.98/5.16 Kbytes malloced 2929 % 4.98/5.16 % 4.98/5.16 ----------- times (seconds) ----------- % 4.98/5.16 user CPU time 3.03 (0 hr, 0 min, 3 sec) % 4.98/5.16 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 4.98/5.16 wall-clock time 5 (0 hr, 0 min, 5 sec) % 4.98/5.16 % 4.98/5.16 Process 22354 finished Wed Jul 27 08:43:43 2022 % 4.98/5.16 Otter interrupted % 4.98/5.16 PROOF NOT FOUND %------------------------------------------------------------------------------