%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : NLP092-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n016.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:45 EDT 2022 % Result : Timeout 299.87s 300.03s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NLP092-1 : TPTP v8.1.0. Released v2.4.0. % 0.06/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n016.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 09:14:37 EDT 2022 % 0.12/0.33 % CPUTime : % 4.90/5.13 % 4.90/5.13 % 4.90/5.13 WARNING, multiple arity: set/1, set/2. % 4.90/5.13 % 4.90/5.13 ----- Otter 3.3f, August 2004 ----- % 4.90/5.13 The process was started by sandbox2 on n016.cluster.edu, % 4.90/5.13 Wed Jul 27 09:14:37 2022 % 4.90/5.13 The command was "./otter". The process ID is 6723. % 4.90/5.13 % 4.90/5.13 set(prolog_style_variables). % 4.90/5.13 set(auto). % 4.90/5.13 dependent: set(auto1). % 4.90/5.13 dependent: set(process_input). % 4.90/5.13 dependent: clear(print_kept). % 4.90/5.13 dependent: clear(print_new_demod). % 4.90/5.13 dependent: clear(print_back_demod). % 4.90/5.13 dependent: clear(print_back_sub). % 4.90/5.13 dependent: set(control_memory). % 4.90/5.13 dependent: assign(max_mem, 12000). % 4.90/5.13 dependent: assign(pick_given_ratio, 4). % 4.90/5.13 dependent: assign(stats_level, 1). % 4.90/5.13 dependent: assign(max_seconds, 10800). % 4.90/5.13 clear(print_given). % 4.90/5.13 % 4.90/5.13 list(usable). % 4.90/5.13 0 [] A=A. % 4.90/5.13 0 [] -member(U,V,V). % 4.90/5.13 0 [] -scream(U,V)|sound(U,V). % 4.90/5.13 0 [] -sound(U,V)|event(U,V). % 4.90/5.13 0 [] -event(U,V)|eventuality(U,V). % 4.90/5.13 0 [] -eventuality(U,V)|thing(U,V). % 4.90/5.13 0 [] -thing(U,V)|singleton(U,V). % 4.90/5.13 0 [] -eventuality(U,V)|specific(U,V). % 4.90/5.13 0 [] -eventuality(U,V)|nonexistent(U,V). % 4.90/5.13 0 [] -eventuality(U,V)|unisex(U,V). % 4.90/5.13 0 [] -scream(U,V)|event(U,V). % 4.90/5.13 0 [] -cry(U,V)|event(U,V). % 4.90/5.13 0 [] -revenge(U,V)|action(U,V). % 4.90/5.13 0 [] -action(U,V)|act(U,V). % 4.90/5.13 0 [] -act(U,V)|event(U,V). % 4.90/5.13 0 [] -shot(U,V)|action(U,V). % 4.90/5.13 0 [] -group(U,V)|set(U,V). % 4.90/5.13 0 [] -set(U,V)|multiple(U,V). % 4.90/5.13 0 [] -six(U,V)|group(U,V). % 4.90/5.13 0 [] -fire(U,V)|event(U,V). % 4.90/5.13 0 [] -cannon(U,V)|weapon(U,V). % 4.90/5.13 0 [] -weapon(U,V)|weaponry(U,V). % 4.90/5.13 0 [] -weaponry(U,V)|instrumentality(U,V). % 4.90/5.13 0 [] -instrumentality(U,V)|artifact(U,V). % 4.90/5.13 0 [] -artifact(U,V)|object(U,V). % 4.90/5.13 0 [] -object(U,V)|entity(U,V). % 4.90/5.13 0 [] -entity(U,V)|thing(U,V). % 4.90/5.13 0 [] -entity(U,V)|specific(U,V). % 4.90/5.13 0 [] -entity(U,V)|existent(U,V). % 4.90/5.13 0 [] -object(U,V)|nonliving(U,V). % 4.90/5.13 0 [] -object(U,V)|impartial(U,V). % 4.90/5.13 0 [] -object(U,V)|unisex(U,V). % 4.90/5.13 0 [] -man(U,V)|human_person(U,V). % 4.90/5.13 0 [] -human_person(U,V)|organism(U,V). % 4.90/5.13 0 [] -organism(U,V)|entity(U,V). % 4.90/5.13 0 [] -organism(U,V)|impartial(U,V). % 4.90/5.13 0 [] -organism(U,V)|living(U,V). % 4.90/5.13 0 [] -human_person(U,V)|human(U,V). % 4.90/5.13 0 [] -human_person(U,V)|animate(U,V). % 4.90/5.13 0 [] -man(U,V)|male(U,V). % 4.90/5.13 0 [] -male(U,V)| -unisex(U,V). % 4.90/5.13 0 [] -multiple(U,V)| -singleton(U,V). % 4.90/5.13 0 [] -living(U,V)| -nonliving(U,V). % 4.90/5.13 0 [] -nonexistent(U,V)| -existent(U,V). % 4.90/5.13 0 [] -nonliving(U,V)| -animate(U,V). % 4.90/5.13 0 [] -six(U,V)|member(U,skf25(V,U),V). % 4.90/5.13 0 [] -six(U,V)|member(U,skf23(V,U),V). % 4.90/5.13 0 [] -six(U,V)|member(U,skf21(V,U),V). % 4.90/5.13 0 [] -six(U,V)|member(U,skf19(V,U),V). % 4.90/5.13 0 [] -six(U,V)|member(U,skf17(V,U),V). % 4.90/5.13 0 [] -six(U,V)|member(U,skf15(V,U),V). % 4.90/5.13 0 [] skf25(U,V)!=skf15(U,V)| -six(V,U). % 4.90/5.13 0 [] skf25(U,V)!=skf17(U,V)| -six(V,U). % 4.90/5.13 0 [] skf25(U,V)!=skf19(U,V)| -six(V,U). % 4.90/5.13 0 [] skf25(U,V)!=skf21(U,V)| -six(V,U). % 4.90/5.13 0 [] skf25(U,V)!=skf23(U,V)| -six(V,U). % 4.90/5.13 0 [] skf23(U,V)!=skf15(U,V)| -six(V,U). % 4.90/5.13 0 [] skf23(U,V)!=skf17(U,V)| -six(V,U). % 4.90/5.13 0 [] skf23(U,V)!=skf19(U,V)| -six(V,U). % 4.90/5.13 0 [] skf23(U,V)!=skf21(U,V)| -six(V,U). % 4.90/5.13 0 [] skf21(U,V)!=skf15(U,V)| -six(V,U). % 4.90/5.13 0 [] skf21(U,V)!=skf17(U,V)| -six(V,U). % 4.90/5.13 0 [] skf21(U,V)!=skf19(U,V)| -six(V,U). % 4.90/5.13 0 [] skf19(U,V)!=skf15(U,V)| -six(V,U). % 4.90/5.13 0 [] skf19(U,V)!=skf17(U,V)| -six(V,U). % 4.90/5.13 0 [] skf17(U,V)!=skf15(U,V)| -six(V,U). % 4.90/5.13 0 [] -nonreflexive(U,V)| -patient(U,V,W)| -agent(U,V,W). % 4.90/5.13 0 [] -member(U,V,W)| -six(U,W)|V=skf15(W,U)|V=skf17(W,U)|V=skf19(W,U)|V=skf21(W,U)|V=skf23(W,U)|V=skf25(W,U). % 4.90/5.13 0 [] skf26(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. % 4.90/5.13 0 [] skf26(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. % 4.90/5.13 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,skf26(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. % 4.90/5.13 0 [] skf26(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. % 4.90/5.13 0 [] skf26(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. % 4.90/5.13 0 [] skf26(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. % 4.90/5.13 0 [] skf26(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. % 4.90/5.13 0 [] actual_world(skc4). % 4.90/5.13 0 [] male(skc4,skc7). % 4.90/5.13 0 [] man(skc4,skc7). % 4.90/5.13 0 [] cannon(skc4,skc6). % 4.90/5.13 0 [] six(skc4,skc5). % 4.90/5.13 0 [] group(skc4,skc5). % 4.90/5.13 0 [] of(skc4,skc6,skc7). % 4.90/5.13 0 [] ssSkP0(skc6,skc7,skc5,skc4). % 4.90/5.13 0 [] -member(skc4,U,skc5)|shot(skc4,U). % 4.90/5.13 0 [] ssSkP0(U,V,W,X)|member(X,skf13(U,V,W,X),W). % 4.90/5.13 0 [] -member(U,V,W)| -ssSkP0(X,Y,W,U)|event(U,skf11(U,Z,X1,X2)). % 4.90/5.13 0 [] -member(U,V,W)| -ssSkP0(X,Y,W,U)|present(U,skf11(U,Z,X1,X2)). % 4.90/5.13 0 [] -member(U,V,W)| -ssSkP0(X,Y,W,U)|nonreflexive(U,skf11(U,Z,X1,X2)). % 4.90/5.13 0 [] -member(U,V,W)| -ssSkP0(X,Y,W,U)|fire(U,skf11(U,Z,X1,X2)). % 4.90/5.13 0 [] -member(U,V,W)| -ssSkP0(X,Y,W,U)|agent(U,skf11(U,V,X,Y),Y). % 4.90/5.13 0 [] -member(U,V,W)| -ssSkP0(X,Y,W,U)|patient(U,skf11(U,V,Z,X1),V). % 4.90/5.13 0 [] -member(U,V,W)| -ssSkP0(X,Y,W,U)|from_loc(U,skf11(U,V,X,Z),X). % 4.90/5.13 0 [] -from_loc(U,V,W)| -fire(U,V)| -nonreflexive(U,V)| -present(U,V)| -patient(U,V,skf13(W,X,Y,U))| -agent(U,V,X)| -event(U,V). % 4.90/5.13 0 [] -cry(U,V)| -patient(U,W,V)| -event(U,W)| -present(U,W)| -nonreflexive(U,W)| -scream(U,W)| -shot(U,skf10(U,X))| -group(U,Y)| -six(U,Y)| -cannon(U,Z)| -agent(U,W,X1)| -ssSkP0(Z,X1,Y,U)| -of(U,Z,X1)| -man(U,X1)| -male(U,X1)| -of(U,W,X2)| -revenge(U,X2)| -actual_world(U). % 4.90/5.13 0 [] -cry(U,V)| -patient(U,W,V)| -event(U,W)| -present(U,W)| -nonreflexive(U,W)| -scream(U,W)| -group(U,X)| -six(U,X)| -cannon(U,Y)| -agent(U,W,Z)| -ssSkP0(Y,Z,X,U)| -of(U,Y,Z)| -man(U,Z)| -male(U,Z)| -of(U,W,X1)| -revenge(U,X1)| -actual_world(U)|member(U,skf10(U,X),X). % 4.90/5.13 end_of_list. % 4.90/5.13 % 4.90/5.13 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=23. % 4.90/5.13 % 4.90/5.13 This ia a non-Horn set with equality. The strategy will be % 4.90/5.13 Knuth-Bendix, ordered hyper_res, factoring, and unit % 4.90/5.13 deletion, with positive clauses in sos and nonpositive % 4.90/5.13 clauses in usable. % 4.90/5.13 % 4.90/5.13 dependent: set(knuth_bendix). % 4.90/5.13 dependent: set(anl_eq). % 4.90/5.13 dependent: set(para_from). % 4.90/5.13 dependent: set(para_into). % 4.90/5.13 dependent: clear(para_from_right). % 4.90/5.13 dependent: clear(para_into_right). % 4.90/5.13 dependent: set(para_from_vars). % 4.90/5.13 dependent: set(eq_units_both_ways). % 4.90/5.13 dependent: set(dynamic_demod_all). % 4.90/5.13 dependent: set(dynamic_demod). % 4.90/5.13 dependent: set(order_eq). % 4.90/5.13 dependent: set(back_demod). % 4.90/5.13 dependent: set(lrpo). % 4.90/5.13 dependent: set(hyper_res). % 4.90/5.13 dependent: set(unit_deletion). % 4.90/5.13 dependent: set(factor). % 4.90/5.13 % 4.90/5.13 ------------> process usable: % 4.90/5.13 ** KEPT (pick-wt=4): 1 [] -member(A,B,B). % 4.90/5.13 ** KEPT (pick-wt=6): 2 [] -scream(A,B)|sound(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 3 [] -sound(A,B)|event(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 4 [] -event(A,B)|eventuality(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 5 [] -eventuality(A,B)|thing(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 6 [] -thing(A,B)|singleton(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 7 [] -eventuality(A,B)|specific(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 8 [] -eventuality(A,B)|nonexistent(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 9 [] -eventuality(A,B)|unisex(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 10 [] -scream(A,B)|event(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 11 [] -cry(A,B)|event(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 12 [] -revenge(A,B)|action(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 13 [] -action(A,B)|act(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 14 [] -act(A,B)|event(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 15 [] -shot(A,B)|action(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 16 [] -group(A,B)|set(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 17 [] -set(A,B)|multiple(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 18 [] -six(A,B)|group(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 19 [] -fire(A,B)|event(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 20 [] -cannon(A,B)|weapon(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 21 [] -weapon(A,B)|weaponry(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 22 [] -weaponry(A,B)|instrumentality(A,B). % 4.90/5.13 ** KEPT (pick-wt=6): 23 [] -instrumentality(A,B)|artifact(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 24 [] -artifact(A,B)|object(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 25 [] -object(A,B)|entity(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 26 [] -entity(A,B)|thing(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 27 [] -entity(A,B)|specific(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 28 [] -entity(A,B)|existent(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 29 [] -object(A,B)|nonliving(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 30 [] -object(A,B)|impartial(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 31 [] -object(A,B)|unisex(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 32 [] -man(A,B)|human_person(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 33 [] -human_person(A,B)|organism(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 34 [] -organism(A,B)|entity(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 35 [] -organism(A,B)|impartial(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 36 [] -organism(A,B)|living(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 37 [] -human_person(A,B)|human(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 38 [] -human_person(A,B)|animate(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 39 [] -man(A,B)|male(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 40 [] -male(A,B)| -unisex(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 41 [] -multiple(A,B)| -singleton(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 42 [] -living(A,B)| -nonliving(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 43 [] -nonexistent(A,B)| -existent(A,B). % 225.50/225.75 ** KEPT (pick-wt=6): 44 [] -nonliving(A,B)| -animate(A,B). % 225.50/225.75 ** KEPT (pick-wt=9): 45 [] -six(A,B)|member(A,skf25(B,A),B). % 225.50/225.75 ** KEPT (pick-wt=9): 46 [] -six(A,B)|member(A,skf23(B,A),B). % 225.50/225.75 ** KEPT (pick-wt=9): 47 [] -six(A,B)|member(A,skf21(B,A),B). % 225.50/225.75 ** KEPT (pick-wt=9): 48 [] -six(A,B)|member(A,skf19(B,A),B). % 225.50/225.75 ** KEPT (pick-wt=9): 49 [] -six(A,B)|member(A,skf17(B,A),B). % 225.50/225.75 ** KEPT (pick-wt=9): 50 [] -six(A,B)|member(A,skf15(B,A),B). % 225.50/225.75 ** KEPT (pick-wt=10): 51 [] skf25(A,B)!=skf15(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 52 [] skf25(A,B)!=skf17(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 53 [] skf25(A,B)!=skf19(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 54 [] skf25(A,B)!=skf21(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 55 [] skf25(A,B)!=skf23(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 56 [] skf23(A,B)!=skf15(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 57 [] skf23(A,B)!=skf17(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 58 [] skf23(A,B)!=skf19(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 59 [] skf23(A,B)!=skf21(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 60 [] skf21(A,B)!=skf15(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 61 [] skf21(A,B)!=skf17(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 62 [] skf21(A,B)!=skf19(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 63 [] skf19(A,B)!=skf15(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 64 [] skf19(A,B)!=skf17(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=10): 65 [] skf17(A,B)!=skf15(A,B)| -six(B,A). % 225.50/225.75 ** KEPT (pick-wt=11): 66 [] -nonreflexive(A,B)| -patient(A,B,C)| -agent(A,B,C). % 225.50/225.75 ** KEPT (pick-wt=37): 67 [] -member(A,B,C)| -six(A,C)|B=skf15(C,A)|B=skf17(C,A)|B=skf19(C,A)|B=skf21(C,A)|B=skf23(C,A)|B=skf25(C,A). % 225.50/225.75 ** KEPT (pick-wt=83): 68 [] skf26(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. % 225.50/225.75 ** KEPT (pick-wt=83): 69 [] skf26(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. % 225.50/225.75 ** KEPT (pick-wt=84): 70 [] -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,skf26(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. % 225.50/225.75 ** KEPT (pick-wt=83): 71 [] skf26(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. % 225.50/225.75 ** KEPT (pick-wt=83): 72 [] skf26(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. % 225.50/225.75 ** KEPT (pick-wt=83): 73 [] skf26(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. % 225.50/225.75 ** KEPT (pick-wt=83): 74 [] skf26(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. % 225.50/225.75 ** KEPT (pick-wt=7): 75 [] -member(skc4,A,skc5)|shot(skc4,A). % 225.50/225.75 ** KEPT (pick-wt=16): 76 [] -member(A,B,C)| -ssSkP0(D,E,C,A)|event(A,skf11(A,F,G,H)). % 225.50/225.75 ** KEPT (pick-wt=16): 77 [] -member(A,B,C)| -ssSkP0(D,E,C,A)|present(A,skf11(A,F,G,H)). % 225.50/225.75 ** KEPT (pick-wt=16): 78 [] -member(A,B,C)| -ssSkP0(D,E,C,A)|nonreflexive(A,skf11(A,F,G,H)). % 225.50/225.75 ** KEPT (pick-wt=16): 79 [] -member(A,B,C)| -ssSkP0(D,E,C,A)|fire(A,skf11(A,F,G,H)). % 225.50/225.75 ** KEPT (pick-wt=17): 80 [] -member(A,B,C)| -ssSkP0(D,E,C,A)|agent(A,skf11(A,B,D,E),E). % 225.50/225.75 ** KEPT (pick-wt=17): 81 [] -member(A,B,C)| -ssSkP0(D,E,C,A)|patient(A,skf11(A,B,F,G),B). % 225.50/225.75 ** KEPT (pick-wt=17): 82 [] -member(A,B,C)| -ssSkP0(D,E,C,A)|from_loc(A,skf11(A,B,D,F),D). % 225.50/225.75 ** KEPT (pick-wt=28): 83 [] -from_loc(A,B,C)| -fire(A,B)| -nonreflexive(A,B)| -present(A,B)| -patient(A,B,skf13(C,D,E,A))| -agent(A,B,D)| -event(A,B). % 225.50/225.75 ** KEPT (pick-wt=61): 84 [] -cry(A,B)| -patient(A,C,B)| -event(A,C)| -present(A,C)| -nonreflexive(A,C)| -scream(A,C)| -shot(A,skf10(A,D))| -group(A,E)| -six(A,E)| -cannon(A,F)| -agent(A,C,G)| -ssSkP0(F,G,E,A)| -of(A,F,G)| -man(A,G)| -male(A,G)| -of(A,C,H)| -revenge(A,H)| -actual_world(A). % 225.50/225.75 ** KEPT (pick-wt=62): 85 [] -cry(A,B)| -patient(A,C,B)| -event(A,C)| -present(A,C)| -nonreflexive(A,C)| -scream(A,C)| -group(A,D)| -six(A,D)| -cannon(A,E)| -agent(A,C,F)| -ssSkP0(E,F,D,A)| -of(A,E,F)| -man(A,F)| -male(A,F)| -of(A,C,G)| -revenge(A,G)| -actual_world(A)|member(A,skf10(A,D),D). % 225.50/225.75 90 back subsumes 86. % 225.50/225.75 218 back subsumes 205. % 225.50/225.75 220 back subsumes 209. % 225.50/225.75 222 back subsumes 169. % 225.50/225.75 223 back subsumes 170. % 225.50/225.75 226 back subsumes 173. % 225.50/225.75 228 back subsumes 175. % 225.50/225.75 244 back subsumes 193. % 225.50/225.75 246 back subsumes 195. % 225.50/225.75 253 back subsumes 204. % 225.50/225.75 258 back subsumes 181. % 225.50/225.75 260 back subsumes 198. % 225.50/225.75 261 back subsumes 255. % 225.50/225.75 261 back subsumes 206. % 225.50/225.75 262 back subsumes 208. % 225.50/225.75 263 back subsumes 220. % 225.50/225.75 263 back subsumes 194. % 225.50/225.75 263 back subsumes 174. % 225.50/225.75 263 back subsumes 171. % 225.50/225.75 263 back subsumes 168. % 225.50/225.75 266 back subsumes 229. % 225.50/225.75 269 back subsumes 231. % 225.50/225.75 276 back subsumes 247. % 225.50/225.75 279 back subsumes 237. % 225.50/225.75 279 back subsumes 186. % 225.50/225.75 279 back subsumes 184. % 225.50/225.75 280 back subsumes 252. % 225.50/225.75 280 back subsumes 203. % 225.50/225.75 280 back subsumes 201. % 225.50/225.75 281 back subsumes 261. % 225.50/225.75 281 back subsumes 230. % 225.50/225.75 281 back subsumes 218. % 225.50/225.75 281 back subsumes 172. % 225.50/225.75 281 back subsumes 166. % 225.50/225.75 284 back subsumes 270. % 225.50/225.75 453 back subsumes 422. % 225.50/225.75 455 back subsumes 423. % 225.50/225.75 456 back subsumes 449. % 225.50/225.75 461 back subsumes 429. % 225.50/225.75 463 back subsumes 431. % 225.50/225.75 466 back subsumes 434. % 225.50/225.75 470 back subsumes 438. % 225.50/225.75 478 back subsumes 446. % 225.50/225.75 481 back subsumes 450. % 225.50/225.75 484 back subsumes 456. % 225.50/225.75 484 back subsumes 451. % 225.50/225.75 % 225.50/225.75 ------------> process sos: % 225.50/225.75 ** KEPT (pick-wt=3): 490 [] A=A. % 225.50/225.75 ** KEPT (pick-wt=2): 491 [] actual_world(skc4). % 225.50/225.75 ** KEPT (pick-wt=3): 492 [] male(skc4,skc7). % 225.50/225.75 ** KEPT (pick-wt=3): 493 [] man(skc4,skc7). % 225.50/225.75 ** KEPT (pick-wt=3): 494 [] cannon(skc4,skc6). % 225.50/225.75 ** KEPT (pick-wt=3): 495 [] six(skc4,skc5). % 225.50/225.75 ** KEPT (pick-wt=3): 496 [] group(skc4,skc5). % 225.50/225.75 ** KEPT (pick-wt=4): 497 [] of(skc4,skc6,skc7). % 225.50/225.75 ** KEPT (pick-wt=5): 498 [] ssSkP0(skc6,skc7,skc5,skc4). % 225.50/225.75 ** KEPT (pick-wt=13): 499 [] ssSkP0(A,B,C,D)|member(D,skf13(A,B,C,D),C). % 225.50/225.75 Following clause subsumed by 490 during input processing: 0 [copy,490,flip.1] A=A. % 225.50/225.75 490 back subsumes 489. % 225.50/225.75 490 back subsumes 488. % 225.50/225.75 490 back subsumes 487. % 225.50/225.75 490 back subsumes 486. % 225.50/225.75 490 back subsumes 485. % 225.50/225.75 490 back subsumes 484. % 225.50/225.75 490 back subsumes 483. % 225.50/225.75 490 back subsumes 482. % 225.50/225.75 490 back subsumes 481. % 225.50/225.75 490 back subsumes 480. % 225.50/225.75 490 back subsumes 479. % 225.50/225.75 490 back subsumes 478. % 225.50/225.75 490 back subsumes 477. % 225.50/225.75 490 back subsumes 476. % 225.50/225.75 490 back subsumes 475. % 225.50/225.75 490 back subsumes 474. % 225.50/225.75 490 back subsumes 473. % 225.50/225.75 490 back subsumes 472. % 225.50/225.75 490 back subsumes 471. % 225.50/225.75 490 back subsumes 470. % 225.50/225.75 490 back subsumes 469. % 225.50/225.75 490 back subsumes 468. % 225.50/225.75 490 back subsumes 467. % 225.50/225.75 490 back subsumes 466. % 225.50/225.75 490 back subsumes 465. % 225.50/225.75 490 back subsumes 464. % 225.50/225.75 490 back subsumes 463. % 225.50/225.75 490 back subsumes 462. % 225.50/225.75 490 back subsumes 461. % 225.50/225.75 490 back subsumes 460. % 225.50/225.75 490 back subsumes 459. % 225.50/225.75 490 back subsumes 458. % 225.50/225.75 490 back subsumes 457. % 225.50/225.75 490 back subsumes 455. % 225.50/225.75 490 back subsumes 454. % 225.50/225.75 490 back subsumes 453. % 225.50/225.75 490 back subsumes 452. % 225.50/225.75 490 back subsumes 448. % 225.50/225.75 490 back subsumes 447. % 225.50/225.75 490 back subsumes 445. % 225.50/225.75 490 back subsumes 444. % 225.50/225.75 490 back subsumes 443. % 225.50/225.75 490 back subsumes 442. % 225.50/225.75 490 back subsumes 441. % 225.50/225.75 490 back subsumes 440. % 225.50/225.75 490 back subsumes 439. % 225.50/225.75 490 back subsumes 437. % 225.50/225.75 490 back subsumes 436. % 225.50/225.75 490 back subsumes 435. % 225.50/225.75 490 back subsumes 433. % 225.50/225.75 490 back subsumes 432. % 225.50/225.75 490 back subsumes 430. % 225.50/225.75 490 back subsumes 428. % 225.50/225.75 490 back subsumes 427. % 225.50/225.75 490 back subsumes 426. % 225.50/225.75 490 back subsumes 425. % 225.50/225.75 490 back subsumes 424. % 225.50/225.75 490 back subsumes 421. % 225.50/225.75 490 back subsumes 420. % 225.50/225.75 490 back subsumes 419. % 225.50/225.75 490 back subsumes 418. % 225.50/225.75 490 back subsumes 417. % 225.50/225.75 490 back subsumes 416. % 225.50/225.75 490 back subsumes 415. % 225.50/225.75 490 back subsumes 414. % 225.50/225.75 490 back subsumes 413. % 225.50/225.75 490 back subsumes 412. % 225.50/225.75 490 back subsumes 411. % 225.50/225.75 490 back subsumes 410. % 225.50/225.75 490 back subsumes 409. % 225.50/225.75 490 back subsumes 408. % 225.50/225.75 490 back subsumes 407. % 225.50/225.75 490 back subsumes 406. % 225.50/225.75 490 back subsumes 405. % 225.50/225.75 490 back subsumes 404. % 225.50/225.75 490 back subsumes 403. % 225.50/225.75 490 back subsumes 402. % 225.50/225.75 490 back subsumes 401. % 225.50/225.75 490 back subsumes 400. % 225.50/225.75 490 back subsumes 399. % 225.50/225.75 490 back subsumes 398. % 225.50/225.75 490 back subsumes 397. % 225.50/225.75 490 back subsumes 396. % 225.50/225.75 490 back subsumes 395. % 225.50/225.75 490 back subsumes 394. % 225.50/225.75 490 back subsumes 393. % 225.50/225.75 490 back subsumes 392. % 225.50/225.75 490 back subsumes 391. % 225.50/225.75 490 back subsumes 390. % 225.50/225.75 490 back subsumes 389. % 225.50/225.75 490 back subsumes 388. % 225.50/225.75 490 back subsumes 387. % 225.50/225.75 490 back subsumes 386. % 225.50/225.75 490 back subsumes 385. % 225.50/225.75 490 back subsumes 384. % 225.50/225.75 490 back subsumes 383. % 225.50/225.75 490 back subsumes 382. % 225.50/225.75 490 back subsumes 381. % 225.50/225.75 490 back subsumes 380. % 225.50/225.75 490 back subsumes 379. % 225.50/225.75 490 back subsumes 378. % 225.50/225.75 490 back subsumes 377. % 225.50/225.75 490 back subsumes 376. % 225.50/225.75 490 back subsumes 375. % 225.50/225.75 490 back subsumes 374. % 225.50/225.75 490 back subsumes 373. % 225.50/225.75 490 back subsumes 372. % 225.50/225.75 490 back subsumes 371. % 225.50/225.75 490 back subsumes 370. % 225.50/225.75 490 back subsumes 369. % 225.50/225.75 490 back subsumes 368. % 225.50/225.75 490 back subsumes 367. % 225.50/225.75 490 back subsumes 366. % 225.50/225.75 490 back subsumes 365. % 225.50/225.75 490 back subsumes 364. % 225.50/225.75 490 back subsumes 363. % 225.50/225.75 490 back subsumes 362. % 225.50/225.75 490 back subsumes 361. % 225.50/225.75 490 back subsumes 360. % 225.50/225.75 490 back subsumes 359. % 225.50/225.75 490 back subsumes 358. % 225.50/225.75 490 back subsumes 357. % 225.50/225.75 490 back subsumes 356. % 225.50/225.75 490 back subsumes 355. % 225.50/225.75 490 back subsumes 354. % 225.50/225.75 490 back subsumes 353. % 225.50/225.75 490 back subsumes 352. % 225.50/225.75 490 back subsumes 351. % 225.50/225.75 490 back subsumes 350. % 225.50/225.75 490 back subsumes 349. % 225.50/225.75 490 back subsumes 348. % 225.50/225.75 490 back subsumes 347. % 225.50/225.75 490 back subsumes 346. % 225.50/225.75 490 back subsumes 345. % 225.50/225.75 490 back subsumes 344. % 225.50/225.75 490 back subsumes 343. % 225.50/225.75 490 back subsumes 342. % 225.50/225.75 490 back subsumes 341. % 225.50/225.75 490 back subsumes 340. % 225.50/225.75 490 back subsumes 339. % 225.50/225.75 490 back subsumes 338. % 225.50/225.75 490 back subsumes 337. % 225.50/225.75 490 back subsumes 336. % 225.50/225.75 490 back subsumes 335. % 225.50/225.75 490 back subsumes 334. % 225.50/225.75 490 back subsumes 333. % 225.50/225.75 490 back subsumes 332. % 225.50/225.75 490 back subsumes 331. % 225.50/225.75 490 back subsumes 330. % 225.50/225.75 490 back subsumes 329. % 225.50/225.75 490 back subsumes 328. % 225.50/225.75 490 back subsumes 327. % 225.50/225.75 490 back subsumes 326. % 225.50/225.75 490 back subsumes 325. % 225.50/225.75 490 back subsumes 324. % 225.50/225.75 490 back subsumes 323. % 225.50/225.75 490 back subsumes 322. % 225.50/225.75 490 back subsumes 321. % 225.50/225.75 490 back subsumes 320. % 225.50/225.75 490 back subsumes 319. % 225.50/225.75 490 back subsumes 318. % 225.50/225.75 490 back subsumes 317. % 225.50/225.75 490 back subsumes 316. % 225.50/225.75 490 back subsumes 315. % 225.50/225.75 490 back subsumes 314. % 225.50/225.75 490 back subsumes 313. % 225.50/225.75 490 back subsumes 312. % 225.50/225.75 490 back subsumes 311. % 225.50/225.75 490 back subsumes 310. % 225.50/225.75 490 back subsumes 309. % 225.50/225.75 490 back subsumes 308. % 225.50/225.75 490 back subsumes 307. % 225.50/225.75 490 back subsumes 306. % 225.50/225.75 490 back subsumes 305. % 225.50/225.75 490 back subsumes 304. % 225.50/225.75 490 back subsumes 303. % 225.50/225.75 490 back subsumes 302. % 225.50/225.75 490 back subsumes 301. % 225.50/225.75 490 back subsumes 300. % 225.50/225.75 490 back subsumes 299. % 225.50/225.75 490 back subsumes 298. % 225.50/225.75 490 back subsumes 297. % 225.50/225.75 490 back subsumes 296. % 225.50/225.75 490 back subsumes 295. % 225.50/225.75 490 back subsumes 294. % 225.50/225.75 490 back subsumes 293. % 225.50/225.75 490 back subsumes 292. % 225.50/225.75 490 back subsumes 291. % 225.50/225.75 490 back subsumes 290. % 225.50/225.75 490 back subsumes 289. % 225.50/225.75 490 back subsumes 288. % 225.50/225.75 490 back subsumes 285. % 225.50/225.75 490 back subsumes 284. % 225.50/225.75 490 back subsumes 283. % 225.50/225.75 490 back subsumes 282. % 225.50/225.75 490 back subsumes 281. % 225.50/225.75 490 back subsumes 280. % 225.50/225.75 490 back subsumes 279. % 225.50/225.75 490 back subsumes 278. % 225.50/225.75 490 back subsumes 277. % 225.50/225.75 490 back subsumes 276. % 225.50/225.75 490 back subsumes 275. % 225.50/225.75 490 back subsumes 274. % 225.50/225.75 490 back subsumes 273. % 225.50/225.75 490 back subsumes 272. % 225.50/225.75 490 back subsumes 271. % 225.50/225.75 490 back subsumes 269. % 225.50/225.75 490 back subsumes 268. % 225.50/225.75 490 back subsumes 267. % 225.50/225.75 490 back subsumes 266. % 225.50/225.75 490 back subsumes 265. % 225.50/225.75 490 back subsumes 264. % 225.50/225.75 490 back subsumes 263. % 225.50/225.75 490 back subsumes 262. % 225.50/225.75 490 back subsumes 260. % 225.50/225.75 490 bacAlarm clock % 299.87/300.03 Otter interrupted % 299.87/300.03 PROOF NOT FOUND %------------------------------------------------------------------------------