%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : PRO006+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n013.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:10:56 EDT 2022 % Result : Unknown 13.46s 13.66s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : PRO006+4 : TPTP v8.1.0. Released v4.0.0. % 0.10/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n013.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 04:53:15 EDT 2022 % 0.12/0.33 % CPUTime : % 2.16/2.34 ----- Otter 3.3f, August 2004 ----- % 2.16/2.34 The process was started by sandbox2 on n013.cluster.edu, % 2.16/2.34 Wed Jul 27 04:53:15 2022 % 2.16/2.34 The command was "./otter". The process ID is 8952. % 2.16/2.34 % 2.16/2.34 set(prolog_style_variables). % 2.16/2.34 set(auto). % 2.16/2.34 dependent: set(auto1). % 2.16/2.34 dependent: set(process_input). % 2.16/2.34 dependent: clear(print_kept). % 2.16/2.34 dependent: clear(print_new_demod). % 2.16/2.34 dependent: clear(print_back_demod). % 2.16/2.34 dependent: clear(print_back_sub). % 2.16/2.34 dependent: set(control_memory). % 2.16/2.34 dependent: assign(max_mem, 12000). % 2.16/2.34 dependent: assign(pick_given_ratio, 4). % 2.16/2.34 dependent: assign(stats_level, 1). % 2.16/2.34 dependent: assign(max_seconds, 10800). % 2.16/2.34 clear(print_given). % 2.16/2.34 % 2.16/2.34 formula_list(usable). % 2.16/2.34 all A (A=A). % 2.16/2.34 all X0 X1 (occurrence_of(X1,X0)& -atomic(X0)-> (exists X2 (root(X2,X0)&subactivity_occurrence(X2,X1)))). % 2.16/2.34 all X3 X4 X5 X6 X7 (occurrence_of(X4,X3)&root_occ(X6,X4)&leaf_occ(X7,X4)&subactivity_occurrence(X5,X4)&min_precedes(X6,X5,X3)&X5!=X7->min_precedes(X5,X7,X3)). % 2.16/2.34 all X8 X9 X10 X11 (occurrence_of(X9,X8)&subactivity_occurrence(X10,X9)&leaf_occ(X11,X9)&arboreal(X10)& -min_precedes(X10,X11,X8)->X11=X10). % 2.16/2.34 all X12 X13 (occurrence_of(X13,X12)->activity(X12)&activity_occurrence(X13)). % 2.16/2.34 all X14 X15 X16 X17 (occurrence_of(X15,X14)&arboreal(X16)&arboreal(X17)&subactivity_occurrence(X16,X15)&subactivity_occurrence(X17,X15)->min_precedes(X16,X17,X14)|min_precedes(X17,X16,X14)|X16=X17). % 2.16/2.34 all X18 X19 (root(X19,X18)-> (exists X20 (subactivity(X20,X18)&atocc(X19,X20)))). % 2.16/2.34 all X21 X22 X23 (min_precedes(X22,X23,X21)-> (exists X24 (occurrence_of(X24,X21)&subactivity_occurrence(X22,X24)&subactivity_occurrence(X23,X24)))). % 2.16/2.34 all X25 X26 (leaf(X25,X26)& -atomic(X26)-> (exists X27 (occurrence_of(X27,X26)&leaf_occ(X25,X27)))). % 2.16/2.34 all X28 X29 X30 (occurrence_of(X28,X29)&occurrence_of(X28,X30)->X29=X30). % 2.16/2.34 all X31 X32 X33 (occurrence_of(X31,X33)&leaf_occ(X32,X31)-> -(exists X34 min_precedes(X32,X34,X33))). % 2.16/2.34 all X35 X36 X37 (occurrence_of(X35,X37)&root_occ(X36,X35)-> -(exists X38 min_precedes(X38,X36,X37))). % 2.16/2.34 all X39 X40 (subactivity_occurrence(X39,X40)->activity_occurrence(X39)&activity_occurrence(X40)). % 2.16/2.34 all X41 (activity_occurrence(X41)-> (exists X42 (activity(X42)&occurrence_of(X41,X42)))). % 2.16/2.34 all X43 (legal(X43)->arboreal(X43)). % 2.16/2.34 all X44 X45 (atocc(X44,X45)<-> (exists X46 (subactivity(X45,X46)&atomic(X46)&occurrence_of(X44,X46)))). % 2.16/2.34 all X47 X48 (leaf(X47,X48)<-> (root(X47,X48)| (exists X49 min_precedes(X49,X47,X48)))& -(exists X50 min_precedes(X47,X50,X48))). % 2.16/2.34 all X51 X52 (occurrence_of(X51,X52)-> (arboreal(X51)<->atomic(X52))). % 2.16/2.34 all X53 X54 (root(X53,X54)->legal(X53)). % 2.16/2.34 all X55 X56 (leaf_occ(X55,X56)<-> (exists X57 (occurrence_of(X56,X57)&subactivity_occurrence(X55,X56)&leaf(X55,X57)))). % 2.16/2.34 all X58 X59 (root_occ(X58,X59)<-> (exists X60 (occurrence_of(X59,X60)&subactivity_occurrence(X58,X59)&root(X58,X60)))). % 2.16/2.34 all X61 X62 (earlier(X61,X62)-> -earlier(X62,X61)). % 2.16/2.34 all X63 X64 (precedes(X63,X64)<->earlier(X63,X64)&legal(X64)). % 2.16/2.34 all X65 X66 X67 (min_precedes(X65,X66,X67)-> -root(X66,X67)). % 2.16/2.34 all X68 X69 X70 (min_precedes(X68,X69,X70)-> (exists X71 (root(X71,X70)&min_precedes(X71,X69,X70)))). % 2.16/2.34 all X72 X73 X74 (min_precedes(X72,X73,X74)->precedes(X72,X73)). % 2.16/2.34 all X75 X76 X77 (next_subocc(X75,X76,X77)->arboreal(X75)&arboreal(X76)). % 2.16/2.34 all X78 X79 X80 (next_subocc(X78,X79,X80)<->min_precedes(X78,X79,X80)& -(exists X81 (min_precedes(X78,X81,X80)&min_precedes(X81,X79,X80)))). % 2.16/2.34 all X82 X83 X84 X85 (min_precedes(X82,X83,X84)&occurrence_of(X85,X84)&subactivity_occurrence(X83,X85)->subactivity_occurrence(X82,X85)). % 2.16/2.34 all X86 X87 X88 X89 (occurrence_of(X88,X89)& -atomic(X89)&leaf_occ(X86,X88)&leaf_occ(X87,X88)->X86=X87). % 2.16/2.34 all X90 X91 X92 X93 (occurrence_of(X92,X93)&root_occ(X90,X92)&root_occ(X91,X92)->X90=X91). % 2.16/2.34 all X94 X95 X96 (earlier(X94,X95)&earlier(X95,X96)->earlier(X94,X96)). % 2.16/2.34 all X97 X98 X99 X100 (min_precedes(X97,X98,X100)&min_precedes(X97,X99,X100)&precedes(X98,X99)->min_precedes(X98,X99,X100)). % 2.16/2.34 all X101 (occurrence_of(X101,tptp0)-> (exists X102 X103 (occurrence_of(X102,tptp4)&root_occ(X102,X101)&occurrence_of(X103,tptp3)&leaf_occ(X103,X101)&next_subocc(X102,X103,tptp0)))). % 2.16/2.34 activity(tptp0). % 2.16/2.34 -atomic(tptp0). % 2.16/2.34 atomic(tptp4). % 2.16/2.34 atomic(tptp3). % 2.16/2.34 atomic(tptp2). % 2.16/2.34 atomic(tptp1). % 2.16/2.34 tptp4!=tptp1. % 2.16/2.34 tptp4!=tptp3. % 2.16/2.34 tptp4!=tptp2. % 2.16/2.34 tptp1!=tptp3. % 2.16/2.34 tptp1!=tptp2. % 2.16/2.34 tptp3!=tptp2. % 2.16/2.34 all X104 X105 (occurrence_of(X105,tptp0)&subactivity_occurrence(X104,X105)&arboreal(X104)& -leaf_occ(X104,X105)-> (exists X106 (occurrence_of(X106,tptp1)&next_subocc(X104,X106,tptp0)))). % 2.16/2.34 -(-(exists X107 occurrence_of(X107,tptp0))). % 2.16/2.34 end_of_list. % 2.16/2.34 % 2.16/2.34 -------> usable clausifies to: % 2.16/2.34 % 2.16/2.34 list(usable). % 2.16/2.34 0 [] A=A. % 2.16/2.34 0 [] -occurrence_of(X1,X0)|atomic(X0)|root($f1(X0,X1),X0). % 2.16/2.34 0 [] -occurrence_of(X1,X0)|atomic(X0)|subactivity_occurrence($f1(X0,X1),X1). % 2.16/2.34 0 [] -occurrence_of(X4,X3)| -root_occ(X6,X4)| -leaf_occ(X7,X4)| -subactivity_occurrence(X5,X4)| -min_precedes(X6,X5,X3)|X5=X7|min_precedes(X5,X7,X3). % 2.16/2.34 0 [] -occurrence_of(X9,X8)| -subactivity_occurrence(X10,X9)| -leaf_occ(X11,X9)| -arboreal(X10)|min_precedes(X10,X11,X8)|X11=X10. % 2.16/2.34 0 [] -occurrence_of(X13,X12)|activity(X12). % 2.16/2.34 0 [] -occurrence_of(X13,X12)|activity_occurrence(X13). % 2.16/2.34 0 [] -occurrence_of(X15,X14)| -arboreal(X16)| -arboreal(X17)| -subactivity_occurrence(X16,X15)| -subactivity_occurrence(X17,X15)|min_precedes(X16,X17,X14)|min_precedes(X17,X16,X14)|X16=X17. % 2.16/2.34 0 [] -root(X19,X18)|subactivity($f2(X18,X19),X18). % 2.16/2.34 0 [] -root(X19,X18)|atocc(X19,$f2(X18,X19)). % 2.16/2.34 0 [] -min_precedes(X22,X23,X21)|occurrence_of($f3(X21,X22,X23),X21). % 2.16/2.34 0 [] -min_precedes(X22,X23,X21)|subactivity_occurrence(X22,$f3(X21,X22,X23)). % 2.16/2.34 0 [] -min_precedes(X22,X23,X21)|subactivity_occurrence(X23,$f3(X21,X22,X23)). % 2.16/2.34 0 [] -leaf(X25,X26)|atomic(X26)|occurrence_of($f4(X25,X26),X26). % 2.16/2.34 0 [] -leaf(X25,X26)|atomic(X26)|leaf_occ(X25,$f4(X25,X26)). % 2.16/2.34 0 [] -occurrence_of(X28,X29)| -occurrence_of(X28,X30)|X29=X30. % 2.16/2.34 0 [] -occurrence_of(X31,X33)| -leaf_occ(X32,X31)| -min_precedes(X32,X34,X33). % 2.16/2.34 0 [] -occurrence_of(X35,X37)| -root_occ(X36,X35)| -min_precedes(X38,X36,X37). % 2.16/2.34 0 [] -subactivity_occurrence(X39,X40)|activity_occurrence(X39). % 2.16/2.34 0 [] -subactivity_occurrence(X39,X40)|activity_occurrence(X40). % 2.16/2.34 0 [] -activity_occurrence(X41)|activity($f5(X41)). % 2.16/2.34 0 [] -activity_occurrence(X41)|occurrence_of(X41,$f5(X41)). % 2.16/2.34 0 [] -legal(X43)|arboreal(X43). % 2.16/2.34 0 [] -atocc(X44,X45)|subactivity(X45,$f6(X44,X45)). % 2.16/2.34 0 [] -atocc(X44,X45)|atomic($f6(X44,X45)). % 2.16/2.34 0 [] -atocc(X44,X45)|occurrence_of(X44,$f6(X44,X45)). % 2.16/2.34 0 [] atocc(X44,X45)| -subactivity(X45,X46)| -atomic(X46)| -occurrence_of(X44,X46). % 2.16/2.34 0 [] -leaf(X47,X48)|root(X47,X48)|min_precedes($f7(X47,X48),X47,X48). % 2.16/2.34 0 [] -leaf(X47,X48)| -min_precedes(X47,X50,X48). % 2.16/2.34 0 [] leaf(X47,X48)| -root(X47,X48)|min_precedes(X47,$f8(X47,X48),X48). % 2.16/2.34 0 [] leaf(X47,X48)| -min_precedes(X49,X47,X48)|min_precedes(X47,$f8(X47,X48),X48). % 2.16/2.34 0 [] -occurrence_of(X51,X52)| -arboreal(X51)|atomic(X52). % 2.16/2.34 0 [] -occurrence_of(X51,X52)|arboreal(X51)| -atomic(X52). % 2.16/2.34 0 [] -root(X53,X54)|legal(X53). % 2.16/2.34 0 [] -leaf_occ(X55,X56)|occurrence_of(X56,$f9(X55,X56)). % 2.16/2.34 0 [] -leaf_occ(X55,X56)|subactivity_occurrence(X55,X56). % 2.16/2.34 0 [] -leaf_occ(X55,X56)|leaf(X55,$f9(X55,X56)). % 2.16/2.34 0 [] leaf_occ(X55,X56)| -occurrence_of(X56,X57)| -subactivity_occurrence(X55,X56)| -leaf(X55,X57). % 2.16/2.34 0 [] -root_occ(X58,X59)|occurrence_of(X59,$f10(X58,X59)). % 2.16/2.34 0 [] -root_occ(X58,X59)|subactivity_occurrence(X58,X59). % 2.16/2.34 0 [] -root_occ(X58,X59)|root(X58,$f10(X58,X59)). % 2.16/2.34 0 [] root_occ(X58,X59)| -occurrence_of(X59,X60)| -subactivity_occurrence(X58,X59)| -root(X58,X60). % 2.16/2.34 0 [] -earlier(X61,X62)| -earlier(X62,X61). % 2.16/2.34 0 [] -precedes(X63,X64)|earlier(X63,X64). % 2.16/2.34 0 [] -precedes(X63,X64)|legal(X64). % 2.16/2.34 0 [] precedes(X63,X64)| -earlier(X63,X64)| -legal(X64). % 2.16/2.34 0 [] -min_precedes(X65,X66,X67)| -root(X66,X67). % 2.16/2.34 0 [] -min_precedes(X68,X69,X70)|root($f11(X68,X69,X70),X70). % 2.16/2.34 0 [] -min_precedes(X68,X69,X70)|min_precedes($f11(X68,X69,X70),X69,X70). % 2.16/2.34 0 [] -min_precedes(X72,X73,X74)|precedes(X72,X73). % 2.16/2.34 0 [] -next_subocc(X75,X76,X77)|arboreal(X75). % 2.16/2.34 0 [] -next_subocc(X75,X76,X77)|arboreal(X76). % 2.16/2.34 0 [] -next_subocc(X78,X79,X80)|min_precedes(X78,X79,X80). % 2.16/2.34 0 [] -next_subocc(X78,X79,X80)| -min_precedes(X78,X81,X80)| -min_precedes(X81,X79,X80). % 2.16/2.34 0 [] next_subocc(X78,X79,X80)| -min_precedes(X78,X79,X80)|min_precedes(X78,$f12(X78,X79,X80),X80). % 2.16/2.34 0 [] next_subocc(X78,X79,X80)| -min_precedes(X78,X79,X80)|min_precedes($f12(X78,X79,X80),X79,X80). % 2.16/2.34 0 [] -min_precedes(X82,X83,X84)| -occurrence_of(X85,X84)| -subactivity_occurrence(X83,X85)|subactivity_occurrence(X82,X85). % 2.16/2.34 0 [] -occurrence_of(X88,X89)|atomic(X89)| -leaf_occ(X86,X88)| -leaf_occ(X87,X88)|X86=X87. % 2.16/2.34 0 [] -occurrence_of(X92,X93)| -root_occ(X90,X92)| -root_occ(X91,X92)|X90=X91. % 2.16/2.34 0 [] -earlier(X94,X95)| -earlier(X95,X96)|earlier(X94,X96). % 2.16/2.34 0 [] -min_precedes(X97,X98,X100)| -min_precedes(X97,X99,X100)| -precedes(X98,X99)|min_precedes(X98,X99,X100). % 2.16/2.34 0 [] -occurrence_of(X101,tptp0)|occurrence_of($f14(X101),tptp4). % 2.16/2.34 0 [] -occurrence_of(X101,tptp0)|root_occ($f14(X101),X101). % 2.16/2.34 0 [] -occurrence_of(X101,tptp0)|occurrence_of($f13(X101),tptp3). % 2.16/2.34 0 [] -occurrence_of(X101,tptp0)|leaf_occ($f13(X101),X101). % 2.16/2.34 0 [] -occurrence_of(X101,tptp0)|next_subocc($f14(X101),$f13(X101),tptp0). % 2.16/2.34 0 [] activity(tptp0). % 2.16/2.34 0 [] -atomic(tptp0). % 2.16/2.34 0 [] atomic(tptp4). % 2.16/2.34 0 [] atomic(tptp3). % 2.16/2.34 0 [] atomic(tptp2). % 2.16/2.34 0 [] atomic(tptp1). % 2.16/2.34 0 [] tptp4!=tptp1. % 2.16/2.34 0 [] tptp4!=tptp3. % 2.16/2.34 0 [] tptp4!=tptp2. % 2.16/2.34 0 [] tptp1!=tptp3. % 2.16/2.34 0 [] tptp1!=tptp2. % 2.16/2.34 0 [] tptp3!=tptp2. % 2.16/2.34 0 [] -occurrence_of(X105,tptp0)| -subactivity_occurrence(X104,X105)| -arboreal(X104)|leaf_occ(X104,X105)|occurrence_of($f15(X104,X105),tptp1). % 2.16/2.34 0 [] -occurrence_of(X105,tptp0)| -subactivity_occurrence(X104,X105)| -arboreal(X104)|leaf_occ(X104,X105)|next_subocc(X104,$f15(X104,X105),tptp0). % 2.16/2.34 0 [] occurrence_of($c1,tptp0). % 2.16/2.34 end_of_list. % 2.16/2.34 % 2.16/2.34 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=8. % 2.16/2.34 % 2.16/2.34 This ia a non-Horn set with equality. The strategy will be % 2.16/2.34 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.16/2.34 deletion, with positive clauses in sos and nonpositive % 2.16/2.34 clauses in usable. % 2.16/2.34 % 2.16/2.34 dependent: set(knuth_bendix). % 2.16/2.34 dependent: set(anl_eq). % 2.16/2.34 dependent: set(para_from). % 2.16/2.34 dependent: set(para_into). % 2.16/2.34 dependent: clear(para_from_right). % 2.16/2.34 dependent: clear(para_into_right). % 2.16/2.34 dependent: set(para_from_vars). % 2.16/2.34 dependent: set(eq_units_both_ways). % 2.16/2.34 dependent: set(dynamic_demod_all). % 2.16/2.34 dependent: set(dynamic_demod). % 2.16/2.34 dependent: set(order_eq). % 2.16/2.34 dependent: set(back_demod). % 2.16/2.34 dependent: set(lrpo). % 2.16/2.34 dependent: set(hyper_res). % 2.16/2.34 dependent: set(unit_deletion). % 2.16/2.34 dependent: set(factor). % 2.16/2.34 % 2.16/2.34 ------------> process usable: % 2.16/2.34 ** KEPT (pick-wt=10): 1 [] -occurrence_of(A,B)|atomic(B)|root($f1(B,A),B). % 2.16/2.34 ** KEPT (pick-wt=10): 2 [] -occurrence_of(A,B)|atomic(B)|subactivity_occurrence($f1(B,A),A). % 2.16/2.34 ** KEPT (pick-wt=23): 3 [] -occurrence_of(A,B)| -root_occ(C,A)| -leaf_occ(D,A)| -subactivity_occurrence(E,A)| -min_precedes(C,E,B)|E=D|min_precedes(E,D,B). % 2.16/2.34 ** KEPT (pick-wt=18): 4 [] -occurrence_of(A,B)| -subactivity_occurrence(C,A)| -leaf_occ(D,A)| -arboreal(C)|min_precedes(C,D,B)|D=C. % 2.16/2.34 ** KEPT (pick-wt=5): 5 [] -occurrence_of(A,B)|activity(B). % 2.16/2.34 ** KEPT (pick-wt=5): 6 [] -occurrence_of(A,B)|activity_occurrence(A). % 2.16/2.34 ** KEPT (pick-wt=24): 7 [] -occurrence_of(A,B)| -arboreal(C)| -arboreal(D)| -subactivity_occurrence(C,A)| -subactivity_occurrence(D,A)|min_precedes(C,D,B)|min_precedes(D,C,B)|C=D. % 2.16/2.34 ** KEPT (pick-wt=8): 8 [] -root(A,B)|subactivity($f2(B,A),B). % 2.16/2.34 ** KEPT (pick-wt=8): 9 [] -root(A,B)|atocc(A,$f2(B,A)). % 2.16/2.34 ** KEPT (pick-wt=10): 10 [] -min_precedes(A,B,C)|occurrence_of($f3(C,A,B),C). % 2.16/2.34 ** KEPT (pick-wt=10): 11 [] -min_precedes(A,B,C)|subactivity_occurrence(A,$f3(C,A,B)). % 2.16/2.34 ** KEPT (pick-wt=10): 12 [] -min_precedes(A,B,C)|subactivity_occurrence(B,$f3(C,A,B)). % 2.16/2.34 ** KEPT (pick-wt=10): 13 [] -leaf(A,B)|atomic(B)|occurrence_of($f4(A,B),B). % 2.16/2.34 ** KEPT (pick-wt=10): 14 [] -leaf(A,B)|atomic(B)|leaf_occ(A,$f4(A,B)). % 2.16/2.34 ** KEPT (pick-wt=9): 15 [] -occurrence_of(A,B)| -occurrence_of(A,C)|B=C. % 2.16/2.34 ** KEPT (pick-wt=10): 16 [] -occurrence_of(A,B)| -leaf_occ(C,A)| -min_precedes(C,D,B). % 2.16/2.34 ** KEPT (pick-wt=10): 17 [] -occurrence_of(A,B)| -root_occ(C,A)| -min_precedes(D,C,B). % 2.16/2.34 ** KEPT (pick-wt=5): 18 [] -subactivity_occurrence(A,B)|activity_occurrence(A). % 2.16/2.34 ** KEPT (pick-wt=5): 19 [] -subactivity_occurrence(A,B)|activity_occurrence(B). % 2.16/2.34 ** KEPT (pick-wt=5): 20 [] -activity_occurrence(A)|activity($f5(A)). % 2.16/2.34 ** KEPT (pick-wt=6): 21 [] -activity_occurrence(A)|occurrence_of(A,$f5(A)). % 2.16/2.34 ** KEPT (pick-wt=4): 22 [] -legal(A)|arboreal(A). % 2.16/2.34 ** KEPT (pick-wt=8): 23 [] -atocc(A,B)|subactivity(B,$f6(A,B)). % 2.16/2.34 ** KEPT (pick-wt=7): 24 [] -atocc(A,B)|atomic($f6(A,B)). % 2.16/2.34 ** KEPT (pick-wt=8): 25 [] -atocc(A,B)|occurrence_of(A,$f6(A,B)). % 2.16/2.34 ** KEPT (pick-wt=11): 26 [] atocc(A,B)| -subactivity(B,C)| -atomic(C)| -occurrence_of(A,C). % 2.16/2.34 ** KEPT (pick-wt=12): 27 [] -leaf(A,B)|root(A,B)|min_precedes($f7(A,B),A,B). % 2.16/2.34 ** KEPT (pick-wt=7): 28 [] -leaf(A,B)| -min_precedes(A,C,B). % 2.16/2.34 ** KEPT (pick-wt=12): 29 [] leaf(A,B)| -root(A,B)|min_precedes(A,$f8(A,B),B). % 2.16/2.34 ** KEPT (pick-wt=13): 30 [] leaf(A,B)| -min_precedes(C,A,B)|min_precedes(A,$f8(A,B),B). % 2.16/2.34 ** KEPT (pick-wt=7): 31 [] -occurrence_of(A,B)| -arboreal(A)|atomic(B). % 2.16/2.34 ** KEPT (pick-wt=7): 32 [] -occurrence_of(A,B)|arboreal(A)| -atomic(B). % 2.16/2.34 ** KEPT (pick-wt=5): 33 [] -root(A,B)|legal(A). % 2.16/2.34 ** KEPT (pick-wt=8): 34 [] -leaf_occ(A,B)|occurrence_of(B,$f9(A,B)). % 2.16/2.34 ** KEPT (pick-wt=6): 35 [] -leaf_occ(A,B)|subactivity_occurrence(A,B). % 2.16/2.34 ** KEPT (pick-wt=8): 36 [] -leaf_occ(A,B)|leaf(A,$f9(A,B)). % 2.16/2.34 ** KEPT (pick-wt=12): 37 [] leaf_occ(A,B)| -occurrence_of(B,C)| -subactivity_occurrence(A,B)| -leaf(A,C). % 2.16/2.34 ** KEPT (pick-wt=8): 38 [] -root_occ(A,B)|occurrence_of(B,$f10(A,B)). % 2.16/2.34 ** KEPT (pick-wt=6): 39 [] -root_occ(A,B)|subactivity_occurrence(A,B). % 2.16/2.34 ** KEPT (pick-wt=8): 40 [] -root_occ(A,B)|root(A,$f10(A,B)). % 2.16/2.34 ** KEPT (pick-wt=12): 41 [] root_occ(A,B)| -occurrence_of(B,C)| -subactivity_occurrence(A,B)| -root(A,C). % 2.16/2.34 ** KEPT (pick-wt=6): 42 [] -earlier(A,B)| -earlier(B,A). % 2.16/2.34 ** KEPT (pick-wt=6): 43 [] -precedes(A,B)|earlier(A,B). % 2.16/2.34 ** KEPT (pick-wt=5): 44 [] -precedes(A,B)|legal(B). % 2.16/2.34 ** KEPT (pick-wt=8): 45 [] precedes(A,B)| -earlier(A,B)| -legal(B). % 2.16/2.34 ** KEPT (pick-wt=7): 46 [] -min_precedes(A,B,C)| -root(B,C). % 2.16/2.34 ** KEPT (pick-wt=10): 47 [] -min_precedes(A,B,C)|root($f11(A,B,C),C). % 2.16/2.34 ** KEPT (pick-wt=11): 48 [] -min_precedes(A,B,C)|min_precedes($f11(A,B,C),B,C). % 2.16/2.34 ** KEPT (pick-wt=7): 49 [] -min_precedes(A,B,C)|precedes(A,B). % 2.16/2.34 ** KEPT (pick-wt=6): 50 [] -next_subocc(A,B,C)|arboreal(A). % 2.16/2.34 ** KEPT (pick-wt=6): 51 [] -next_subocc(A,B,C)|arboreal(B). % 2.16/2.34 ** KEPT (pick-wt=8): 52 [] -next_subocc(A,B,C)|min_precedes(A,B,C). % 2.16/2.34 ** KEPT (pick-wt=12): 53 [] -next_subocc(A,B,C)| -min_precedes(A,D,C)| -min_precedes(D,B,C). % 2.16/2.34 ** KEPT (pick-wt=15): 54 [] next_subocc(A,B,C)| -min_precedes(A,B,C)|min_precedes(A,$f12(A,B,C),C). % 2.16/2.34 ** KEPT (pick-wt=15): 55 [] next_subocc(A,B,C)| -min_precedes(A,B,C)|min_precedes($f12(A,B,C),B,C). % 2.16/2.34 ** KEPT (pick-wt=13): 56 [] -min_precedes(A,B,C)| -occurrence_of(D,C)| -subactivity_occurrence(B,D)|subactivity_occurrence(A,D). % 2.16/2.34 ** KEPT (pick-wt=14): 57 [] -occurrence_of(A,B)|atomic(B)| -leaf_occ(C,A)| -leaf_occ(D,A)|C=D. % 2.16/2.34 ** KEPT (pick-wt=12): 58 [] -occurrence_of(A,B)| -root_occ(C,A)| -root_occ(D,A)|C=D. % 2.16/2.34 ** KEPT (pick-wt=9): 59 [] -earlier(A,B)| -earlier(B,C)|earlier(A,C). % 2.16/2.34 ** KEPT (pick-wt=15): 60 [] -min_precedes(A,B,C)| -min_precedes(A,D,C)| -precedes(B,D)|min_precedes(B,D,C). % 2.16/2.34 ** KEPT (pick-wt=7): 61 [] -occurrence_of(A,tptp0)|occurrence_of($f14(A),tptp4). % 2.16/2.34 ** KEPT (pick-wt=7): 62 [] -occurrence_of(A,tptp0)|root_occ($f14(A),A). % 2.16/2.34 ** KEPT (pick-wt=7): 63 [] -occurrence_of(A,tptp0)|occurrence_of($f13(A),tptp3). % 2.16/2.34 ** KEPT (pick-wt=7): 64 [] -occurrence_of(A,tptp0)|leaf_occ($f13(A),A). % 2.16/2.34 ** KEPT (pick-wt=9): 65 [] -occurrence_of(A,tptp0)|next_subocc($f14(A),$f13(A),tptp0). % 2.16/2.34 ** KEPT (pick-wt=2): 66 [] -atomic(tptp0). % 2.16/2.34 ** KEPT (pick-wt=3): 67 [] tptp4!=tptp1. % 2.16/2.34 ** KEPT (pick-wt=3): 68 [] tptp4!=tptp3. % 2.16/2.34 ** KEPT (pick-wt=3): 69 [] tptp4!=tptp2. % 2.16/2.34 ** KEPT (pick-wt=3): 71 [copy,70,flip.1] tptp3!=tptp1. % 2.16/2.34 ** KEPT (pick-wt=3): 73 [copy,72,flip.1] tptp2!=tptp1. % 2.16/2.34 ** KEPT (pick-wt=3): 74 [] tptp3!=tptp2. % 2.16/2.34 ** KEPT (pick-wt=16): 75 [] -occurrence_of(A,tptp0)| -subactivity_occurrence(B,A)| -arboreal(B)|leaf_occ(B,A)|occurrence_of($f15(B,A),tptp1). % 2.16/2.34 ** KEPT (pick-wt=17): 76 [] -occurrence_of(A,tptp0)| -subactivity_occurrence(B,A)| -arboreal(B)|leaf_occ(B,A)|next_subocc(B,$f15(B,A),tptp0). % 2.16/2.34 % 2.16/2.34 ------------> process sos: % 2.16/2.34 ** KEPT (pick-wt=3): 84 [] A=A. % 2.16/2.34 ** KEPT (pick-wt=2): 85 [] activity(tptp0). % 2.16/2.34 ** KEPT (pick-wt=2): 86 [] atomic(tptp4). % 2.16/2.34 ** KEPT (pick-wt=2): 87 [] atomic(tptp3). % 2.16/2.34 ** KEPT (pick-wt=2): 88 [] atomic(tptp2). % 2.16/2.34 ** KEPT (pick-wt=2): 89 [] atomic(tptp1). % 2.16/2.34 ** KEPT (pick-wt=3): 90 [] occurrence_of($c1,tptp0). % 13.46/13.66 Following clause subsumed by 84 during input processing: 0 [copy,84,flip.1] A=A. % 13.46/13.66 84 back subsumes 82. % 13.46/13.66 84 back subsumes 81. % 13.46/13.66 84 back subsumes 78. % 13.46/13.66 84 back subsumes 77. % 13.46/13.66 % 13.46/13.66 ======= end of input processing ======= % 13.46/13.66 % 13.46/13.66 =========== start of search =========== % 13.46/13.66 % 13.46/13.66 % 13.46/13.66 Resetting weight limit to 11. % 13.46/13.66 % 13.46/13.66 % 13.46/13.66 Resetting weight limit to 11. % 13.46/13.66 % 13.46/13.66 sos_size=1544 % 13.46/13.66 % 13.46/13.66 Search stopped because sos empty. % 13.46/13.66 % 13.46/13.66 % 13.46/13.66 Search stopped because sos empty. % 13.46/13.66 % 13.46/13.66 ============ end of search ============ % 13.46/13.66 % 13.46/13.66 -------------- statistics ------------- % 13.46/13.66 clauses given 1627 % 13.46/13.66 clauses generated 136268 % 13.46/13.66 clauses kept 1914 % 13.46/13.66 clauses forward subsumed 4560 % 13.46/13.66 clauses back subsumed 27 % 13.46/13.66 Kbytes malloced 5859 % 13.46/13.66 % 13.46/13.66 ----------- times (seconds) ----------- % 13.46/13.66 user CPU time 11.32 (0 hr, 0 min, 11 sec) % 13.46/13.66 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 13.46/13.66 wall-clock time 13 (0 hr, 0 min, 13 sec) % 13.46/13.66 % 13.46/13.66 Process 8952 finished Wed Jul 27 04:53:28 2022 % 13.46/13.66 Otter interrupted % 13.46/13.66 PROOF NOT FOUND %------------------------------------------------------------------------------