%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : NLP082-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n004.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:43 EDT 2022 % Result : Timeout 299.89s 300.03s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NLP082-1 : TPTP v8.1.0. Released v2.4.0. % 0.10/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n004.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jul 27 08:45:06 EDT 2022 % 0.12/0.33 % CPUTime : % 3.27/3.85 % 3.27/3.85 % 3.27/3.85 WARNING, multiple arity: set/1, set/2. % 3.27/3.85 % 3.27/3.85 ----- Otter 3.3f, August 2004 ----- % 3.27/3.85 The process was started by sandbox2 on n004.cluster.edu, % 3.27/3.85 Wed Jul 27 08:45:06 2022 % 3.27/3.85 The command was "./otter". The process ID is 25235. % 3.27/3.85 % 3.27/3.85 set(prolog_style_variables). % 3.27/3.85 set(auto). % 3.27/3.85 dependent: set(auto1). % 3.27/3.85 dependent: set(process_input). % 3.27/3.85 dependent: clear(print_kept). % 3.27/3.85 dependent: clear(print_new_demod). % 3.27/3.85 dependent: clear(print_back_demod). % 3.27/3.85 dependent: clear(print_back_sub). % 3.27/3.85 dependent: set(control_memory). % 3.27/3.85 dependent: assign(max_mem, 12000). % 3.27/3.85 dependent: assign(pick_given_ratio, 4). % 3.27/3.85 dependent: assign(stats_level, 1). % 3.27/3.85 dependent: assign(max_seconds, 10800). % 3.27/3.85 clear(print_given). % 3.27/3.85 % 3.27/3.85 list(usable). % 3.27/3.85 0 [] A=A. % 3.27/3.85 0 [] -member(U,V,V). % 3.27/3.85 0 [] -scream(U,V)|sound(U,V). % 3.27/3.85 0 [] -sound(U,V)|event(U,V). % 3.27/3.85 0 [] -event(U,V)|eventuality(U,V). % 3.27/3.85 0 [] -eventuality(U,V)|thing(U,V). % 3.27/3.85 0 [] -thing(U,V)|singleton(U,V). % 3.27/3.85 0 [] -eventuality(U,V)|specific(U,V). % 3.27/3.85 0 [] -eventuality(U,V)|nonexistent(U,V). % 3.27/3.85 0 [] -eventuality(U,V)|unisex(U,V). % 3.27/3.85 0 [] -scream(U,V)|event(U,V). % 3.27/3.85 0 [] -cry(U,V)|event(U,V). % 3.27/3.85 0 [] -revenge(U,V)|action(U,V). % 3.27/3.85 0 [] -action(U,V)|act(U,V). % 3.27/3.85 0 [] -act(U,V)|event(U,V). % 3.27/3.85 0 [] -shot(U,V)|action(U,V). % 3.27/3.85 0 [] -group(U,V)|set(U,V). % 3.27/3.85 0 [] -set(U,V)|multiple(U,V). % 3.27/3.85 0 [] -six(U,V)|group(U,V). % 3.27/3.85 0 [] -fire(U,V)|event(U,V). % 3.27/3.85 0 [] -cannon(U,V)|weapon(U,V). % 3.27/3.85 0 [] -weapon(U,V)|weaponry(U,V). % 3.27/3.85 0 [] -weaponry(U,V)|instrumentality(U,V). % 3.27/3.85 0 [] -instrumentality(U,V)|artifact(U,V). % 3.27/3.85 0 [] -artifact(U,V)|object(U,V). % 3.27/3.85 0 [] -object(U,V)|entity(U,V). % 3.27/3.85 0 [] -entity(U,V)|thing(U,V). % 3.27/3.85 0 [] -entity(U,V)|specific(U,V). % 3.27/3.85 0 [] -entity(U,V)|existent(U,V). % 3.27/3.85 0 [] -object(U,V)|nonliving(U,V). % 3.27/3.85 0 [] -object(U,V)|impartial(U,V). % 3.27/3.85 0 [] -object(U,V)|unisex(U,V). % 3.27/3.85 0 [] -man(U,V)|human_person(U,V). % 3.27/3.85 0 [] -human_person(U,V)|organism(U,V). % 3.27/3.85 0 [] -organism(U,V)|entity(U,V). % 3.27/3.85 0 [] -organism(U,V)|impartial(U,V). % 3.27/3.85 0 [] -organism(U,V)|living(U,V). % 3.27/3.85 0 [] -human_person(U,V)|human(U,V). % 3.27/3.85 0 [] -human_person(U,V)|animate(U,V). % 3.27/3.85 0 [] -man(U,V)|male(U,V). % 3.27/3.85 0 [] -male(U,V)| -unisex(U,V). % 3.27/3.85 0 [] -multiple(U,V)| -singleton(U,V). % 3.27/3.85 0 [] -living(U,V)| -nonliving(U,V). % 3.27/3.85 0 [] -nonexistent(U,V)| -existent(U,V). % 3.27/3.85 0 [] -nonliving(U,V)| -animate(U,V). % 3.27/3.85 0 [] -six(U,V)|member(U,skf20(V,U),V). % 3.27/3.85 0 [] -six(U,V)|member(U,skf18(V,U),V). % 3.27/3.85 0 [] -six(U,V)|member(U,skf16(V,U),V). % 3.27/3.85 0 [] -six(U,V)|member(U,skf14(V,U),V). % 3.27/3.85 0 [] -six(U,V)|member(U,skf12(V,U),V). % 3.27/3.85 0 [] -six(U,V)|member(U,skf10(V,U),V). % 3.27/3.85 0 [] skf20(U,V)!=skf10(U,V)| -six(V,U). % 3.27/3.85 0 [] skf20(U,V)!=skf12(U,V)| -six(V,U). % 3.27/3.85 0 [] skf20(U,V)!=skf14(U,V)| -six(V,U). % 3.27/3.85 0 [] skf20(U,V)!=skf16(U,V)| -six(V,U). % 3.27/3.85 0 [] skf20(U,V)!=skf18(U,V)| -six(V,U). % 3.27/3.85 0 [] skf18(U,V)!=skf10(U,V)| -six(V,U). % 3.27/3.85 0 [] skf18(U,V)!=skf12(U,V)| -six(V,U). % 3.27/3.85 0 [] skf18(U,V)!=skf14(U,V)| -six(V,U). % 3.27/3.85 0 [] skf18(U,V)!=skf16(U,V)| -six(V,U). % 3.27/3.85 0 [] skf16(U,V)!=skf10(U,V)| -six(V,U). % 3.27/3.85 0 [] skf16(U,V)!=skf12(U,V)| -six(V,U). % 3.27/3.85 0 [] skf16(U,V)!=skf14(U,V)| -six(V,U). % 3.27/3.85 0 [] skf14(U,V)!=skf10(U,V)| -six(V,U). % 3.27/3.85 0 [] skf14(U,V)!=skf12(U,V)| -six(V,U). % 3.27/3.85 0 [] skf12(U,V)!=skf10(U,V)| -six(V,U). % 3.27/3.85 0 [] -nonreflexive(U,V)| -patient(U,V,W)| -agent(U,V,W). % 3.27/3.85 0 [] -member(U,V,W)| -six(U,W)|V=skf10(W,U)|V=skf12(W,U)|V=skf14(W,U)|V=skf16(W,U)|V=skf18(W,U)|V=skf20(W,U). % 3.27/3.85 0 [] skf21(U,V,W,X,Y,Z,X1,X2)!=Y| -member(X3,U,X4)| -member(X3,V,X4)| -member(X3,W,X4)| -member(X3,X,X4)| -member(X3,Y,X4)| -member(X3,X5,X4)|six(X3,X4)|U=X5|U=Y|U=X|U=W|U=V|V=X5|V=Y|V=X|V=W|W=X5|W=Y|W=X|X=X5|X=Y|Y=X5. % 3.27/3.85 0 [] skf21(U,V,W,X,Y,Z,X1,X2)!=X| -member(X3,U,X4)| -member(X3,V,X4)| -member(X3,W,X4)| -member(X3,X,X4)| -member(X3,X5,X4)| -member(X3,X6,X4)|six(X3,X4)|U=X6|U=X5|U=X|U=W|U=V|V=X6|V=X5|V=X|V=W|W=X6|W=X5|W=X|X=X6|X=X5|X5=X6. % 3.27/3.85 0 [] skf21(U,V,W,X,Y,Z,X1,X2)!=W| -member(X3,U,X4)| -member(X3,V,X4)| -member(X3,W,X4)| -member(X3,X5,X4)| -member(X3,X6,X4)| -member(X3,X7,X4)|six(X3,X4)|U=X7|U=X6|U=X5|U=W|U=V|V=X7|V=X6|V=X5|V=W|W=X7|W=X6|W=X5|X5=X7|X5=X6|X6=X7. % 3.27/3.85 0 [] skf21(U,V,W,X,Y,Z,X1,X2)!=V| -member(X3,U,X4)| -member(X3,V,X4)| -member(X3,X5,X4)| -member(X3,X6,X4)| -member(X3,X7,X4)| -member(X3,X8,X4)|six(X3,X4)|U=X8|U=X7|U=X6|U=X5|U=V|V=X8|V=X7|V=X6|V=X5|X5=X8|X5=X7|X5=X6|X6=X8|X6=X7|X7=X8. % 3.27/3.85 0 [] skf21(U,V,W,X,Y,Z,X1,X2)!=U| -member(X3,U,X4)| -member(X3,X5,X4)| -member(X3,X6,X4)| -member(X3,X7,X4)| -member(X3,X8,X4)| -member(X3,X9,X4)|six(X3,X4)|U=X9|U=X8|U=X7|U=X6|U=X5|X5=X9|X5=X8|X5=X7|X5=X6|X6=X9|X6=X8|X6=X7|X7=X9|X7=X8|X8=X9. % 3.27/3.85 0 [] -member(U,V,W)| -member(U,X,W)| -member(U,Y,W)| -member(U,Z,W)| -member(U,X1,W)| -member(U,X2,W)|six(U,W)|member(U,skf21(V,X,Y,Z,X1,X2,W,U),W)|V=X2|V=X1|V=Z|V=Y|V=X|X=X2|X=X1|X=Z|X=Y|Y=X2|Y=X1|Y=Z|Z=X2|Z=X1|X1=X2. % 3.27/3.85 0 [] skf21(U,V,W,X,Y,Z,X1,X2)!=Z| -member(X3,U,X4)| -member(X3,V,X4)| -member(X3,W,X4)| -member(X3,X,X4)| -member(X3,Y,X4)| -member(X3,Z,X4)|six(X3,X4)|U=Z|U=Y|U=X|U=W|U=V|V=Z|V=Y|V=X|V=W|W=Z|W=Y|W=X|X=Z|X=Y|Y=Z. % 3.27/3.85 0 [] actual_world(skc8). % 3.27/3.85 0 [] man(skc8,skc15). % 3.27/3.85 0 [] male(skc8,skc15). % 3.27/3.85 0 [] cannon(skc8,skc14). % 3.27/3.85 0 [] cry(skc8,skc12). % 3.27/3.85 0 [] male(skc8,skc11). % 3.27/3.85 0 [] revenge(skc8,skc10). % 3.27/3.85 0 [] event(skc8,skc9). % 3.27/3.85 0 [] present(skc8,skc9). % 3.27/3.85 0 [] nonreflexive(skc8,skc9). % 3.27/3.85 0 [] scream(skc8,skc9). % 3.27/3.85 0 [] group(skc8,skc13). % 3.27/3.85 0 [] six(skc8,skc13). % 3.27/3.85 0 [] of(skc8,skc14,skc15). % 3.27/3.85 0 [] of(skc8,skc9,skc10). % 3.27/3.85 0 [] agent(skc8,skc9,skc11). % 3.27/3.85 0 [] patient(skc8,skc9,skc12). % 3.27/3.85 0 [] -member(skc8,U,skc13)|shot(skc8,U). % 3.27/3.85 0 [] -member(skc8,U,skc13)|fire(skc8,skf8(V)). % 3.27/3.85 0 [] -member(skc8,U,skc13)|nonreflexive(skc8,skf8(V)). % 3.27/3.85 0 [] -member(skc8,U,skc13)|present(skc8,skf8(V)). % 3.27/3.85 0 [] -member(skc8,U,skc13)|event(skc8,skf8(V)). % 3.27/3.85 0 [] -member(skc8,U,skc13)|from_loc(skc8,skf8(V),skc14). % 3.27/3.85 0 [] -member(skc8,U,skc13)|patient(skc8,skf8(U),U). % 3.27/3.85 0 [] -member(skc8,U,skc13)|agent(skc8,skf8(V),skc15). % 3.27/3.85 end_of_list. % 3.27/3.85 % 3.27/3.85 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=23. % 3.27/3.85 % 3.27/3.85 This ia a non-Horn set with equality. The strategy will be % 3.27/3.85 Knuth-Bendix, ordered hyper_res, factoring, and unit % 3.27/3.85 deletion, with positive clauses in sos and nonpositive % 3.27/3.85 clauses in usable. % 3.27/3.85 % 3.27/3.85 dependent: set(knuth_bendix). % 3.27/3.85 dependent: set(anl_eq). % 3.27/3.85 dependent: set(para_from). % 3.27/3.85 dependent: set(para_into). % 3.27/3.85 dependent: clear(para_from_right). % 3.27/3.85 dependent: clear(para_into_right). % 3.27/3.85 dependent: set(para_from_vars). % 3.27/3.85 dependent: set(eq_units_both_ways). % 3.27/3.85 dependent: set(dynamic_demod_all). % 3.27/3.85 dependent: set(dynamic_demod). % 3.27/3.85 dependent: set(order_eq). % 3.27/3.85 dependent: set(back_demod). % 3.27/3.85 dependent: set(lrpo). % 3.27/3.85 dependent: set(hyper_res). % 3.27/3.85 dependent: set(unit_deletion). % 3.27/3.85 dependent: set(factor). % 3.27/3.85 % 3.27/3.85 ------------> process usable: % 3.27/3.85 ** KEPT (pick-wt=4): 1 [] -member(A,B,B). % 3.27/3.85 ** KEPT (pick-wt=6): 2 [] -scream(A,B)|sound(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 3 [] -sound(A,B)|event(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 4 [] -event(A,B)|eventuality(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 5 [] -eventuality(A,B)|thing(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 6 [] -thing(A,B)|singleton(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 7 [] -eventuality(A,B)|specific(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 8 [] -eventuality(A,B)|nonexistent(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 9 [] -eventuality(A,B)|unisex(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 10 [] -scream(A,B)|event(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 11 [] -cry(A,B)|event(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 12 [] -revenge(A,B)|action(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 13 [] -action(A,B)|act(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 14 [] -act(A,B)|event(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 15 [] -shot(A,B)|action(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 16 [] -group(A,B)|set(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 17 [] -set(A,B)|multiple(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 18 [] -six(A,B)|group(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 19 [] -fire(A,B)|event(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 20 [] -cannon(A,B)|weapon(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 21 [] -weapon(A,B)|weaponry(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 22 [] -weaponry(A,B)|instrumentality(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 23 [] -instrumentality(A,B)|artifact(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 24 [] -artifact(A,B)|object(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 25 [] -object(A,B)|entity(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 26 [] -entity(A,B)|thing(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 27 [] -entity(A,B)|specific(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 28 [] -entity(A,B)|existent(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 29 [] -object(A,B)|nonliving(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 30 [] -object(A,B)|impartial(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 31 [] -object(A,B)|unisex(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 32 [] -man(A,B)|human_person(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 33 [] -human_person(A,B)|organism(A,B). % 3.27/3.85 ** KEPT (pick-wt=6): 34 [] -organism(A,B)|entity(A,B). % 4.13/4.31 ** KEPT (pick-wt=6): 35 [] -organism(A,B)|impartial(A,B). % 4.13/4.31 ** KEPT (pick-wt=6): 36 [] -organism(A,B)|living(A,B). % 4.13/4.31 ** KEPT (pick-wt=6): 37 [] -human_person(A,B)|human(A,B). % 4.13/4.31 ** KEPT (pick-wt=6): 38 [] -human_person(A,B)|animate(A,B). % 4.13/4.31 ** KEPT (pick-wt=6): 39 [] -man(A,B)|male(A,B). % 4.13/4.31 ** KEPT (pick-wt=6): 40 [] -male(A,B)| -unisex(A,B). % 4.13/4.31 ** KEPT (pick-wt=6): 41 [] -multiple(A,B)| -singleton(A,B). % 4.13/4.31 ** KEPT (pick-wt=6): 42 [] -living(A,B)| -nonliving(A,B). % 4.13/4.31 ** KEPT (pick-wt=6): 43 [] -nonexistent(A,B)| -existent(A,B). % 4.13/4.31 ** KEPT (pick-wt=6): 44 [] -nonliving(A,B)| -animate(A,B). % 4.13/4.31 ** KEPT (pick-wt=9): 45 [] -six(A,B)|member(A,skf20(B,A),B). % 4.13/4.31 ** KEPT (pick-wt=9): 46 [] -six(A,B)|member(A,skf18(B,A),B). % 4.13/4.31 ** KEPT (pick-wt=9): 47 [] -six(A,B)|member(A,skf16(B,A),B). % 4.13/4.31 ** KEPT (pick-wt=9): 48 [] -six(A,B)|member(A,skf14(B,A),B). % 4.13/4.31 ** KEPT (pick-wt=9): 49 [] -six(A,B)|member(A,skf12(B,A),B). % 4.13/4.31 ** KEPT (pick-wt=9): 50 [] -six(A,B)|member(A,skf10(B,A),B). % 4.13/4.31 ** KEPT (pick-wt=10): 51 [] skf20(A,B)!=skf10(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 52 [] skf20(A,B)!=skf12(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 53 [] skf20(A,B)!=skf14(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 54 [] skf20(A,B)!=skf16(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 55 [] skf20(A,B)!=skf18(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 56 [] skf18(A,B)!=skf10(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 57 [] skf18(A,B)!=skf12(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 58 [] skf18(A,B)!=skf14(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 59 [] skf18(A,B)!=skf16(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 60 [] skf16(A,B)!=skf10(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 61 [] skf16(A,B)!=skf12(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 62 [] skf16(A,B)!=skf14(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 63 [] skf14(A,B)!=skf10(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 64 [] skf14(A,B)!=skf12(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=10): 65 [] skf12(A,B)!=skf10(A,B)| -six(B,A). % 4.13/4.31 ** KEPT (pick-wt=11): 66 [] -nonreflexive(A,B)| -patient(A,B,C)| -agent(A,B,C). % 4.13/4.31 ** KEPT (pick-wt=37): 67 [] -member(A,B,C)| -six(A,C)|B=skf10(C,A)|B=skf12(C,A)|B=skf14(C,A)|B=skf16(C,A)|B=skf18(C,A)|B=skf20(C,A). % 4.13/4.31 ** KEPT (pick-wt=83): 68 [] skf21(A,B,C,D,E,F,G,H)!=E| -member(I,A,J)| -member(I,B,J)| -member(I,C,J)| -member(I,D,J)| -member(I,E,J)| -member(I,K,J)|six(I,J)|A=K|A=E|A=D|A=C|A=B|B=K|B=E|B=D|B=C|C=K|C=E|C=D|D=K|D=E|E=K. % 4.13/4.31 ** KEPT (pick-wt=83): 69 [] skf21(A,B,C,D,E,F,G,H)!=D| -member(I,A,J)| -member(I,B,J)| -member(I,C,J)| -member(I,D,J)| -member(I,K,J)| -member(I,L,J)|six(I,J)|A=L|A=K|A=D|A=C|A=B|B=L|B=K|B=D|B=C|C=L|C=K|C=D|D=L|D=K|K=L. % 4.13/4.31 ** KEPT (pick-wt=83): 70 [] skf21(A,B,C,D,E,F,G,H)!=C| -member(I,A,J)| -member(I,B,J)| -member(I,C,J)| -member(I,K,J)| -member(I,L,J)| -member(I,M,J)|six(I,J)|A=M|A=L|A=K|A=C|A=B|B=M|B=L|B=K|B=C|C=M|C=L|C=K|K=M|K=L|L=M. % 4.13/4.31 ** KEPT (pick-wt=83): 71 [] skf21(A,B,C,D,E,F,G,H)!=B| -member(I,A,J)| -member(I,B,J)| -member(I,K,J)| -member(I,L,J)| -member(I,M,J)| -member(I,N,J)|six(I,J)|A=N|A=M|A=L|A=K|A=B|B=N|B=M|B=L|B=K|K=N|K=M|K=L|L=N|L=M|M=N. % 4.13/4.31 ** KEPT (pick-wt=83): 72 [] skf21(A,B,C,D,E,F,G,H)!=A| -member(I,A,J)| -member(I,K,J)| -member(I,L,J)| -member(I,M,J)| -member(I,N,J)| -member(I,O,J)|six(I,J)|A=O|A=N|A=M|A=L|A=K|K=O|K=N|K=M|K=L|L=O|L=N|L=M|M=O|M=N|N=O. % 4.13/4.31 ** KEPT (pick-wt=84): 73 [] -member(A,B,C)| -member(A,D,C)| -member(A,E,C)| -member(A,F,C)| -member(A,G,C)| -member(A,H,C)|six(A,C)|member(A,skf21(B,D,E,F,G,H,C,A),C)|B=H|B=G|B=F|B=E|B=D|D=H|D=G|D=F|D=E|E=H|E=G|E=F|F=H|F=G|G=H. % 4.13/4.31 ** KEPT (pick-wt=83): 74 [] skf21(A,B,C,D,E,F,G,H)!=F| -member(I,A,J)| -member(I,B,J)| -member(I,C,J)| -member(I,D,J)| -member(I,E,J)| -member(I,F,J)|six(I,J)|A=F|A=E|A=D|A=C|A=B|B=F|B=E|B=D|B=C|C=F|C=E|C=D|D=F|D=E|E=F. % 4.13/4.31 ** KEPT (pick-wt=7): 75 [] -member(skc8,A,skc13)|shot(skc8,A). % 4.13/4.31 ** KEPT (pick-wt=8): 76 [] -member(skc8,A,skc13)|fire(skc8,skf8(B)). % 4.13/4.31 ** KEPT (pick-wt=8): 77 [] -member(skc8,A,skc13)|nonreflexive(skc8,skf8(B)). % 4.13/4.31 ** KEPT (pick-wt=8): 78 [] -member(skc8,A,skc13)|present(skc8,skf8(B)). % 4.13/4.31 ** KEPT (pick-wt=8): 79 [] -member(skc8,A,skc13)|event(skc8,skf8(B)). % 4.13/4.31 ** KEPT (pick-wt=9): 80 [] -member(skc8,A,skc13)|from_loc(skc8,skf8(B),skc14). % 221.64/221.81 ** KEPT (pick-wt=9): 81 [] -member(skc8,A,skc13)|patient(skc8,skf8(A),A). % 221.64/221.81 ** KEPT (pick-wt=9): 82 [] -member(skc8,A,skc13)|agent(skc8,skf8(B),skc15). % 221.64/221.81 140 back subsumes 109. % 221.64/221.81 143 back subsumes 129. % 221.64/221.81 145 back subsumes 137. % 221.64/221.81 147 back subsumes 95. % 221.64/221.81 150 back subsumes 104. % 221.64/221.81 153 back subsumes 106. % 221.64/221.81 163 back subsumes 127. % 221.64/221.81 167 back subsumes 156. % 221.64/221.81 167 back subsumes 111. % 221.64/221.81 168 back subsumes 114. % 221.64/221.81 169 back subsumes 165. % 221.64/221.81 169 back subsumes 131. % 221.64/221.81 170 back subsumes 134. % 221.64/221.81 171 back subsumes 145. % 221.64/221.81 171 back subsumes 105. % 221.64/221.81 171 back subsumes 93. % 221.64/221.81 174 back subsumes 154. % 221.64/221.81 177 back subsumes 176. % 221.64/221.81 177 back subsumes 158. % 221.64/221.81 177 back subsumes 116. % 221.64/221.81 178 back subsumes 161. % 221.64/221.81 178 back subsumes 123. % 221.64/221.81 178 back subsumes 120. % 221.64/221.81 179 back subsumes 169. % 221.64/221.81 179 back subsumes 143. % 221.64/221.81 179 back subsumes 90. % 221.64/221.81 181 back subsumes 177. % 221.64/221.81 181 back subsumes 167. % 221.64/221.81 181 back subsumes 140. % 221.64/221.81 181 back subsumes 86. % 221.64/221.81 309 back subsumes 281. % 221.64/221.81 % 221.64/221.81 ------------> process sos: % 221.64/221.81 ** KEPT (pick-wt=3): 470 [] A=A. % 221.64/221.81 ** KEPT (pick-wt=2): 471 [] actual_world(skc8). % 221.64/221.81 ** KEPT (pick-wt=3): 472 [] man(skc8,skc15). % 221.64/221.81 ** KEPT (pick-wt=3): 473 [] male(skc8,skc15). % 221.64/221.81 ** KEPT (pick-wt=3): 474 [] cannon(skc8,skc14). % 221.64/221.81 ** KEPT (pick-wt=3): 475 [] cry(skc8,skc12). % 221.64/221.81 ** KEPT (pick-wt=3): 476 [] male(skc8,skc11). % 221.64/221.81 ** KEPT (pick-wt=3): 477 [] revenge(skc8,skc10). % 221.64/221.81 ** KEPT (pick-wt=3): 478 [] event(skc8,skc9). % 221.64/221.81 ** KEPT (pick-wt=3): 479 [] present(skc8,skc9). % 221.64/221.81 ** KEPT (pick-wt=3): 480 [] nonreflexive(skc8,skc9). % 221.64/221.81 ** KEPT (pick-wt=3): 481 [] scream(skc8,skc9). % 221.64/221.81 ** KEPT (pick-wt=3): 482 [] group(skc8,skc13). % 221.64/221.81 ** KEPT (pick-wt=3): 483 [] six(skc8,skc13). % 221.64/221.81 ** KEPT (pick-wt=4): 484 [] of(skc8,skc14,skc15). % 221.64/221.81 ** KEPT (pick-wt=4): 485 [] of(skc8,skc9,skc10). % 221.64/221.81 ** KEPT (pick-wt=4): 486 [] agent(skc8,skc9,skc11). % 221.64/221.81 ** KEPT (pick-wt=4): 487 [] patient(skc8,skc9,skc12). % 221.64/221.81 Following clause subsumed by 470 during input processing: 0 [copy,470,flip.1] A=A. % 221.64/221.81 470 back subsumes 469. % 221.64/221.81 470 back subsumes 468. % 221.64/221.81 470 back subsumes 467. % 221.64/221.81 470 back subsumes 466. % 221.64/221.81 470 back subsumes 465. % 221.64/221.81 470 back subsumes 464. % 221.64/221.81 470 back subsumes 463. % 221.64/221.81 470 back subsumes 462. % 221.64/221.81 470 back subsumes 461. % 221.64/221.81 470 back subsumes 460. % 221.64/221.81 470 back subsumes 459. % 221.64/221.81 470 back subsumes 458. % 221.64/221.81 470 back subsumes 457. % 221.64/221.81 470 back subsumes 456. % 221.64/221.81 470 back subsumes 455. % 221.64/221.81 470 back subsumes 454. % 221.64/221.81 470 back subsumes 453. % 221.64/221.81 470 back subsumes 452. % 221.64/221.81 470 back subsumes 451. % 221.64/221.81 470 back subsumes 450. % 221.64/221.81 470 back subsumes 449. % 221.64/221.81 470 back subsumes 448. % 221.64/221.81 470 back subsumes 447. % 221.64/221.81 470 back subsumes 446. % 221.64/221.81 470 back subsumes 445. % 221.64/221.81 470 back subsumes 444. % 221.64/221.81 470 back subsumes 443. % 221.64/221.81 470 back subsumes 442. % 221.64/221.81 470 back subsumes 441. % 221.64/221.81 470 back subsumes 440. % 221.64/221.81 470 back subsumes 439. % 221.64/221.81 470 back subsumes 438. % 221.64/221.81 470 back subsumes 437. % 221.64/221.81 470 back subsumes 436. % 221.64/221.81 470 back subsumes 435. % 221.64/221.81 470 back subsumes 434. % 221.64/221.81 470 back subsumes 433. % 221.64/221.81 470 back subsumes 432. % 221.64/221.81 470 back subsumes 431. % 221.64/221.81 470 back subsumes 430. % 221.64/221.81 470 back subsumes 429. % 221.64/221.81 470 back subsumes 428. % 221.64/221.81 470 back subsumes 427. % 221.64/221.81 470 back subsumes 426. % 221.64/221.81 470 back subsumes 425. % 221.64/221.81 470 back subsumes 424. % 221.64/221.81 470 back subsumes 423. % 221.64/221.81 470 back subsumes 422. % 221.64/221.81 470 back subsumes 421. % 221.64/221.81 470 back subsumes 420. % 221.64/221.81 470 back subsumes 419. % 221.64/221.81 470 back subsumes 418. % 221.64/221.81 470 back subsumes 417. % 221.64/221.81 470 back subsumes 416. % 221.64/221.81 470 back subsumes 415. % 221.64/221.81 470 back subsumes 414. % 221.64/221.81 470 back subsumes 413. % 221.64/221.81 470 back subsumes 412. % 221.64/221.81 470 back subsumes 411. % 221.64/221.81 470 back subsumes 410. % 221.64/221.81 470 back subsumes 409. % 221.64/221.81 470 back subsumes 408. % 221.64/221.81 470 back subsumes 407. % 221.64/221.81 470 back subsumes 406. % 221.64/221.81 470 back subsumes 405. % 221.64/221.81 470 back subsumes 404. % 221.64/221.81 470 back subsumes 403. % 221.64/221.81 470 back subsumes 402. % 221.64/221.81 470 back subsumes 401. % 221.64/221.81 470 back subsumes 400. % 221.64/221.81 470 back subsumes 399. % 221.64/221.81 470 back subsumes 398. % 221.64/221.81 470 back subsumes 397. % 221.64/221.81 470 back subsumes 396. % 221.64/221.81 470 back subsumes 395. % 221.64/221.81 470 back subsumes 394. % 221.64/221.81 470 back subsumes 393. % 221.64/221.81 470 back subsumes 392. % 221.64/221.81 470 back subsumes 391. % 221.64/221.81 470 back subsumes 390. % 221.64/221.81 470 back subsumes 389. % 221.64/221.81 470 back subsumes 388. % 221.64/221.81 470 back subsumes 387. % 221.64/221.81 470 back subsumes 386. % 221.64/221.81 470 back subsumes 385. % 221.64/221.81 470 back subsumes 384. % 221.64/221.81 470 back subsumes 383. % 221.64/221.81 470 back subsumes 382. % 221.64/221.81 470 back subsumes 381. % 221.64/221.81 470 back subsumes 380. % 221.64/221.81 470 back subsumes 379. % 221.64/221.81 470 back subsumes 378. % 221.64/221.81 470 back subsumes 377. % 221.64/221.81 470 back subsumes 376. % 221.64/221.81 470 back subsumes 375. % 221.64/221.81 470 back subsumes 374. % 221.64/221.81 470 back subsumes 373. % 221.64/221.81 470 back subsumes 372. % 221.64/221.81 470 back subsumes 371. % 221.64/221.81 470 back subsumes 370. % 221.64/221.81 470 back subsumes 369. % 221.64/221.81 470 back subsumes 368. % 221.64/221.81 470 back subsumes 367. % 221.64/221.81 470 back subsumes 366. % 221.64/221.81 470 back subsumes 365. % 221.64/221.81 470 back subsumes 364. % 221.64/221.81 470 back subsumes 363. % 221.64/221.81 470 back subsumes 362. % 221.64/221.81 470 back subsumes 361. % 221.64/221.81 470 back subsumes 360. % 221.64/221.81 470 back subsumes 359. % 221.64/221.81 470 back subsumes 358. % 221.64/221.81 470 back subsumes 357. % 221.64/221.81 470 back subsumes 356. % 221.64/221.81 470 back subsumes 355. % 221.64/221.81 470 back subsumes 354. % 221.64/221.81 470 back subsumes 353. % 221.64/221.81 470 back subsumes 352. % 221.64/221.81 470 back subsumes 351. % 221.64/221.81 470 back subsumes 350. % 221.64/221.81 470 back subsumes 349. % 221.64/221.81 470 back subsumes 348. % 221.64/221.81 470 back subsumes 347. % 221.64/221.81 470 back subsumes 346. % 221.64/221.81 470 back subsumes 345. % 221.64/221.81 470 back subsumes 344. % 221.64/221.81 470 back subsumes 343. % 221.64/221.81 470 back subsumes 342. % 221.64/221.81 470 back subsumes 341. % 221.64/221.81 470 back subsumes 340. % 221.64/221.81 470 back subsumes 339. % 221.64/221.81 470 back subsumes 338. % 221.64/221.81 470 back subsumes 337. % 221.64/221.81 470 back subsumes 336. % 221.64/221.81 470 back subsumes 335. % 221.64/221.81 470 back subsumes 334. % 221.64/221.81 470 back subsumes 333. % 221.64/221.81 470 back subsumes 332. % 221.64/221.81 470 back subsumes 331. % 221.64/221.81 470 back subsumes 330. % 221.64/221.81 470 back subsumes 329. % 221.64/221.81 470 back subsumes 328. % 221.64/221.81 470 back subsumes 327. % 221.64/221.81 470 back subsumes 326. % 221.64/221.81 470 back subsumes 325. % 221.64/221.81 470 back subsumes 324. % 221.64/221.81 470 back subsumes 323. % 221.64/221.81 470 back subsumes 322. % 221.64/221.81 470 back subsumes 321. % 221.64/221.81 470 back subsumes 320. % 221.64/221.81 470 back subsumes 319. % 221.64/221.81 470 back subsumes 318. % 221.64/221.81 470 back subsumes 317. % 221.64/221.81 470 back subsumes 316. % 221.64/221.81 470 back subsumes 315. % 221.64/221.81 470 back subsumes 314. % 221.64/221.81 470 back subsumes 313. % 221.64/221.81 470 back subsumes 312. % 221.64/221.81 470 back subsumes 311. % 221.64/221.81 470 back subsumes 310. % 221.64/221.81 470 back subsumes 309. % 221.64/221.81 470 back subsumes 308. % 221.64/221.81 470 back subsumes 307. % 221.64/221.81 470 back subsumes 306. % 221.64/221.81 470 back subsumes 305. % 221.64/221.81 470 back subsumes 304. % 221.64/221.81 470 back subsumes 303. % 221.64/221.81 470 back subsumes 302. % 221.64/221.81 470 back subsumes 301. % 221.64/221.81 470 back subsumes 300. % 221.64/221.81 470 back subsumes 299. % 221.64/221.81 470 back subsumes 298. % 221.64/221.81 470 back subsumes 297. % 221.64/221.81 470 back subsumes 296. % 221.64/221.81 470 back subsumes 295. % 221.64/221.81 470 back subsumes 294. % 221.64/221.81 470 back subsumes 293. % 221.64/221.81 470 back subsumes 292. % 221.64/221.81 470 back subsumes 291. % 221.64/221.81 470 back subsumes 290. % 221.64/221.81 470 back subsumes 289. % 221.64/221.81 470 back subsumes 288. % 221.64/221.81 470 back subsumes 287. % 221.64/221.81 470 back subsumes 286. % 221.64/221.81 470 back subsumes 285. % 221.64/221.81 470 back subsumes 284. % 221.64/221.81 470 back subsumes 283. % 221.64/221.81 470 back subsumes 282. % 221.64/221.81 470 back subsumes 280. % 221.64/221.81 470 back subsumes 279. % 221.64/221.81 470 back subsumes 278. % 221.64/221.81 470 back subsumes 277. % 221.64/221.81 470 back subsumes 276. % 221.64/221.81 470 back subsumes 275. % 221.64/221.81 470 back subsumes 274. % 221.64/221.81 470 back subsumes 273. % 221.64/221.81 470 back subsumes 272. % 221.64/221.81 470 back subsumes 271. % 221.64/221.81 470 back subsumes 270. % 221.64/221.81 470 back subsumes 269. % 221.64/221.81 470 back subsumes 268. % 221.64/221.81 470 back subsumes 267. % 221.64/221.81 470 back subsumes 266. % 221.64/221.81 470 back subsumes 265. % 221.64/221.81 470 back subsumes 264. % 221.64/221.81 470 back subsumes 263. % 221.64/221.81 470 back subsumes 262. % 221.64/221.81 470 back subsumes 261. % 221.64/221.81 470 back subsumes 260. % 221.64/221.81 470 back subsumes 259. % 221.64/221.81 470 back subsumes 258. % 221.64/221.81 470 back subsumes 257. % 221.64/221.81 470 back subsumes 256. % 221.64/221.81 470 back subsumes 255. % 221.64/221.81 470 back subsumes 254. % 221.64/221.81 470 back subsumes 253. % 221.64/221.81 470 back subsumes 252. % 221.64/221.81 470 back subsumes 251. % 221.64/221.81 470 back subsumes 250. % 221.64/221.81 470 back subsumes 249. % 221.64/221.81 470 back subsumes 248. % 221.64/221.81 470 back subsumes 247. % 221.64/221.81 470 back subsumes 246. % 221.64/221.81 470 back subsumes 245. % 221.64/221.81 470 back subsumes 244. % 221.64/221.81 470 back subsumes 243. % 221.64/221.81 470 back subsumes 242. % 221.64/221.81 470 back subsumes 241. % 221.64/221.81 470 back subsumes 240. % 221.64/221.81 470 back subsumes 239. % 221.64/221.81 470 back subsumes 238. % 221.64/221.81 470 back subsumes 237. % 221.64/221.81 470 back subsumes 236. % 221.64/221.81 470 back subsumes 235. % 221.64/221.81 470 back subsumes 234. % 221.64/221.81 470 back subsumes 233. % 221.64/221.81 470 back subsumes 232. % 221.64/221.81 470 back subsumes 231. % 221.64/221.81 470 back subsumes 230. % 221.64/221.81 470 back subsumes 229. % 221.64/221.81 470 back subsumes 228. % 221.64/221.81 470 back subsumes 227. % 221.64/221.81 470 back subsumes 226. % 221.64/221.81 470 back subsumes 225. % 221.64/221.81 470 back subsumes 224. % 221.64/221.81 470 back subsumes 223. % 221.64/221.81 470 back subsumes 222. % 221.64/221.81 470 back subsumes 221. % 221.64/221.81 470 back subsumes 220. % 221.64/221.81 470 back subsumes 219. % 221.64/221.81 470 back subsumes 218. % 221.64/221.81 470 back subsumes 217. % 221.64/221.81 470 back subsumes 216. % 221.64/221.81 470 back subsumes 215. % 221.64/221.81 470 back subsumes 214. % 221.64/221.81 470 back subsumes 213. % 221.64/221.81 470 back subsumes 212. % 221.64/221.81 470 back subsumes 211. % 221.64/221.81 470 back subsumes 210. % 221.64/221.81 470 back subsumes 209. % 221.64/221.81 470 back subsumes 208. % 221.64/221.81 470 back subsumes 207. % 221.64/221.81 470 back subsumes 206. % 221.64/221.81 470 back subsumes 205. % 221.64/221.81 470 back subsumes 204. % 221.64/221.81 470 back subsumes 203. % 221.64/221.81 470 back subsumes 202. % 221.64/221.81 470 back subsumes 201. % 221.64/221.81 470 back subsumes 200. % 221.64/221.81 470 back subsumes 199. % 221.64/221.81 470 back subsumes 198. % 221.64/221.81 470 back subsumes 197. % 221.64/221.81 470 back subsumes 196. % 221.64/221.81 470 back subsumes 195. % 221.64/221.81 470 back subsumes 194. % 221.64/221.81 470 back subsumes 193. % 221.64/221.81 470 back subsumAlarm clock % 299.89/300.03 Otter interrupted % 299.89/300.03 PROOF NOT FOUND %------------------------------------------------------------------------------