%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : PRO001+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n015.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:54 EDT 2022 % Result : Unknown 4.05s 4.21s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : PRO001+2 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n015.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 05:07:11 EDT 2022 % 0.12/0.33 % CPUTime : % 2.13/2.33 ----- Otter 3.3f, August 2004 ----- % 2.13/2.33 The process was started by sandbox2 on n015.cluster.edu, % 2.13/2.33 Wed Jul 27 05:07:11 2022 % 2.13/2.33 The command was "./otter". The process ID is 5472. % 2.13/2.33 % 2.13/2.33 set(prolog_style_variables). % 2.13/2.33 set(auto). % 2.13/2.33 dependent: set(auto1). % 2.13/2.33 dependent: set(process_input). % 2.13/2.33 dependent: clear(print_kept). % 2.13/2.33 dependent: clear(print_new_demod). % 2.13/2.33 dependent: clear(print_back_demod). % 2.13/2.33 dependent: clear(print_back_sub). % 2.13/2.33 dependent: set(control_memory). % 2.13/2.33 dependent: assign(max_mem, 12000). % 2.13/2.33 dependent: assign(pick_given_ratio, 4). % 2.13/2.33 dependent: assign(stats_level, 1). % 2.13/2.33 dependent: assign(max_seconds, 10800). % 2.13/2.33 clear(print_given). % 2.13/2.33 % 2.13/2.33 formula_list(usable). % 2.13/2.33 all A (A=A). % 2.13/2.33 all X0 X1 X2 X3 (min_precedes(X0,X1,X3)&min_precedes(X1,X2,X3)->min_precedes(X0,X2,X3)). % 2.13/2.33 all X4 X5 X6 (earlier(X4,X5)&earlier(X5,X6)->earlier(X4,X6)). % 2.13/2.33 all X7 X8 X9 X10 (occurrence_of(X9,X10)&root_occ(X7,X9)&root_occ(X8,X9)->X7=X8). % 2.13/2.33 all X11 X12 X13 X14 (occurrence_of(X13,X14)& -atomic(X14)&leaf_occ(X11,X13)&leaf_occ(X12,X13)->X11=X12). % 2.13/2.33 all X15 X16 X17 (next_subocc(X15,X16,X17)<->min_precedes(X15,X16,X17)& -(exists X18 (min_precedes(X15,X18,X17)&min_precedes(X18,X16,X17)))). % 2.13/2.33 all X19 X20 X21 (next_subocc(X19,X20,X21)->arboreal(X19)&arboreal(X20)). % 2.13/2.33 all X22 X23 X24 (min_precedes(X22,X23,X24)->precedes(X22,X23)). % 2.13/2.33 all X25 X26 X27 (min_precedes(X25,X26,X27)-> -root(X26,X27)). % 2.13/2.33 all X28 X29 (precedes(X28,X29)<->earlier(X28,X29)&legal(X29)). % 2.13/2.33 all X30 X31 (earlier(X30,X31)-> -earlier(X31,X30)). % 2.13/2.33 all X32 X33 (root_occ(X32,X33)<-> (exists X34 (occurrence_of(X33,X34)&subactivity_occurrence(X32,X33)&root(X32,X34)))). % 2.13/2.33 all X35 X36 (leaf_occ(X35,X36)<-> (exists X37 (occurrence_of(X36,X37)&subactivity_occurrence(X35,X36)&leaf(X35,X37)))). % 2.13/2.33 all X38 X39 (root(X38,X39)->legal(X38)). % 2.13/2.33 all X40 X41 (occurrence_of(X40,X41)-> (arboreal(X40)<->atomic(X41))). % 2.13/2.33 all X42 X43 (leaf(X42,X43)<-> (root(X42,X43)| (exists X44 min_precedes(X44,X42,X43)))& -(exists X45 min_precedes(X42,X45,X43))). % 2.13/2.33 all X46 X47 (atocc(X46,X47)<-> (exists X48 (subactivity(X47,X48)&atomic(X48)&occurrence_of(X46,X48)))). % 2.13/2.33 all X49 X50 (atocc(X49,X50)&legal(X49)->root(X49,X50)). % 2.13/2.33 all X51 (legal(X51)->arboreal(X51)). % 2.13/2.33 all X52 (activity_occurrence(X52)-> (exists X53 (activity(X53)&occurrence_of(X52,X53)))). % 2.13/2.33 all X54 X55 (subactivity_occurrence(X54,X55)->activity_occurrence(X54)&activity_occurrence(X55)). % 2.13/2.33 all X56 X57 X58 (occurrence_of(X56,X58)&root_occ(X57,X56)-> -(exists X59 min_precedes(X59,X57,X58))). % 2.13/2.33 all X60 X61 X62 (occurrence_of(X60,X62)&leaf_occ(X61,X60)-> -(exists X63 min_precedes(X61,X63,X62))). % 2.13/2.33 all X64 X65 X66 (occurrence_of(X64,X65)&occurrence_of(X64,X66)->X65=X66). % 2.13/2.33 all X67 X68 (leaf(X67,X68)& -atomic(X68)-> (exists X69 (occurrence_of(X69,X68)&leaf_occ(X67,X69)))). % 2.13/2.33 all X70 X71 X72 (min_precedes(X71,X72,X70)-> (exists X73 (occurrence_of(X73,X70)&subactivity_occurrence(X71,X73)&subactivity_occurrence(X72,X73)))). % 2.13/2.33 all X74 X75 (leaf(X74,X75)& -atomic(X75)-> (exists X76 (occurrence_of(X76,X75)&leaf_occ(X74,X76)))). % 2.13/2.33 all X77 X78 X79 (min_precedes(X78,X79,X77)-> (exists X80 X81 (subactivity(X80,X77)&subactivity(X81,X77)&atocc(X78,X80)&atocc(X79,X81)))). % 2.13/2.33 all X82 X83 (root(X83,X82)-> (exists X84 (subactivity(X84,X82)&atocc(X83,X84)))). % 2.13/2.33 all X85 X86 X87 X88 (occurrence_of(X86,X85)&arboreal(X87)&arboreal(X88)&subactivity_occurrence(X87,X86)&subactivity_occurrence(X88,X86)->min_precedes(X87,X88,X85)|min_precedes(X88,X87,X85)|X87=X88). % 2.13/2.33 all X89 X90 (occurrence_of(X90,X89)->activity(X89)&activity_occurrence(X90)). % 2.13/2.33 all X91 X92 (occurrence_of(X92,X91)& -atomic(X91)-> (exists X93 (root(X93,X91)&subactivity_occurrence(X93,X92)))). % 2.13/2.33 all X94 (activity(X94)->subactivity(X94,X94)). % 2.13/2.33 all X95 (occurrence_of(X95,tptp0)-> (exists X96 X97 (occurrence_of(X96,tptp4)&root_occ(X96,X95)& (occurrence_of(X97,tptp3)|occurrence_of(X97,tptp2))&leaf_occ(X97,X95)&next_subocc(X96,X97,tptp0)))). % 2.13/2.33 activity(tptp0). % 2.13/2.33 -atomic(tptp0). % 2.13/2.33 atomic(tptp4). % 2.13/2.33 atomic(tptp3). % 2.13/2.33 atomic(tptp2). % 2.13/2.33 atomic(tptp5). % 2.13/2.33 tptp4!=tptp5. % 2.13/2.33 tptp4!=tptp3. % 2.13/2.33 tptp4!=tptp2. % 2.13/2.33 tptp5!=tptp3. % 2.13/2.33 tptp5!=tptp2. % 2.13/2.33 tptp3!=tptp2. % 2.13/2.33 all X98 X99 X100 X101 X102 (send_message(X98,X99,X100,X101,X102)->activity(X98)&atomic(X98)&root(X99,X100)&root(X101,X102)). % 2.13/2.33 all X103 X104 X105 X106 X107 (send_message(X103,X104,X105,X106,X107)->X103!=tptp4&X103!=tptp3&X103!=tptp2). % 2.13/2.33 all X108 X109 X110 X111 X112 X113 (send_message(X108,X109,X110,X111,X112)&occurrence_of(X113,X108)->min_precedes(X111,X113,X112)). % 2.13/2.33 all X114 X115 X116 X117 X118 (transmit_message(X114,X115,X116,X117,X118)->activity(X114)& -atomic(X114)&root(X115,X116)&root(X117,X118)). % 2.13/2.33 all X119 X120 X121 X122 (-transmit_message(tptp0,X119,X120,X121,X122)). % 2.13/2.33 all X123 X124 X125 X126 X127 X128 X129 (transmit_message(X123,X124,X125,X126,X127)-> -tptp1(X123,X128,X129)). % 2.13/2.33 all X130 X131 X132 X133 X134 X135 (transmit_message(X130,X131,X132,X133,X134)&occurrence_of(X135,X130)-> (exists X136 X137 (send_message(X136,X131,X132,X133,X134)&occurrence_of(X137,X136)&root_occ(X137,X135)))). % 2.13/2.33 all X138 X139 X140 (tptp1(X138,X139,X140)->activity(X138)& -atomic(X138)& -atomic(X139)&root(X140,X139)). % 2.13/2.33 all X141 X142 X143 X144 (tptp1(X141,X142,X143)&occurrence_of(X144,X141)-> (exists X145 X146 X147 X148 (transmit_message(X145,X146,X147,X143,X142)&occurrence_of(X148,X145)&subactivity_occurrence(X148,X144)))). % 2.13/2.33 all X149 X150 (-tptp1(tptp0,X149,X150)). % 2.13/2.33 -(-(exists X151 X152 X153 (tptp1(X151,tptp0,X152)&occurrence_of(X153,X151)))). % 2.13/2.33 end_of_list. % 2.13/2.33 % 2.13/2.33 -------> usable clausifies to: % 2.13/2.33 % 2.13/2.33 list(usable). % 2.13/2.33 0 [] A=A. % 2.13/2.33 0 [] -min_precedes(X0,X1,X3)| -min_precedes(X1,X2,X3)|min_precedes(X0,X2,X3). % 2.13/2.33 0 [] -earlier(X4,X5)| -earlier(X5,X6)|earlier(X4,X6). % 2.13/2.33 0 [] -occurrence_of(X9,X10)| -root_occ(X7,X9)| -root_occ(X8,X9)|X7=X8. % 2.13/2.33 0 [] -occurrence_of(X13,X14)|atomic(X14)| -leaf_occ(X11,X13)| -leaf_occ(X12,X13)|X11=X12. % 2.13/2.33 0 [] -next_subocc(X15,X16,X17)|min_precedes(X15,X16,X17). % 2.13/2.33 0 [] -next_subocc(X15,X16,X17)| -min_precedes(X15,X18,X17)| -min_precedes(X18,X16,X17). % 2.13/2.33 0 [] next_subocc(X15,X16,X17)| -min_precedes(X15,X16,X17)|min_precedes(X15,$f1(X15,X16,X17),X17). % 2.13/2.33 0 [] next_subocc(X15,X16,X17)| -min_precedes(X15,X16,X17)|min_precedes($f1(X15,X16,X17),X16,X17). % 2.13/2.33 0 [] -next_subocc(X19,X20,X21)|arboreal(X19). % 2.13/2.33 0 [] -next_subocc(X19,X20,X21)|arboreal(X20). % 2.13/2.33 0 [] -min_precedes(X22,X23,X24)|precedes(X22,X23). % 2.13/2.33 0 [] -min_precedes(X25,X26,X27)| -root(X26,X27). % 2.13/2.33 0 [] -precedes(X28,X29)|earlier(X28,X29). % 2.13/2.33 0 [] -precedes(X28,X29)|legal(X29). % 2.13/2.33 0 [] precedes(X28,X29)| -earlier(X28,X29)| -legal(X29). % 2.13/2.33 0 [] -earlier(X30,X31)| -earlier(X31,X30). % 2.13/2.33 0 [] -root_occ(X32,X33)|occurrence_of(X33,$f2(X32,X33)). % 2.13/2.33 0 [] -root_occ(X32,X33)|subactivity_occurrence(X32,X33). % 2.13/2.33 0 [] -root_occ(X32,X33)|root(X32,$f2(X32,X33)). % 2.13/2.33 0 [] root_occ(X32,X33)| -occurrence_of(X33,X34)| -subactivity_occurrence(X32,X33)| -root(X32,X34). % 2.13/2.33 0 [] -leaf_occ(X35,X36)|occurrence_of(X36,$f3(X35,X36)). % 2.13/2.33 0 [] -leaf_occ(X35,X36)|subactivity_occurrence(X35,X36). % 2.13/2.33 0 [] -leaf_occ(X35,X36)|leaf(X35,$f3(X35,X36)). % 2.13/2.33 0 [] leaf_occ(X35,X36)| -occurrence_of(X36,X37)| -subactivity_occurrence(X35,X36)| -leaf(X35,X37). % 2.13/2.33 0 [] -root(X38,X39)|legal(X38). % 2.13/2.33 0 [] -occurrence_of(X40,X41)| -arboreal(X40)|atomic(X41). % 2.13/2.33 0 [] -occurrence_of(X40,X41)|arboreal(X40)| -atomic(X41). % 2.13/2.33 0 [] -leaf(X42,X43)|root(X42,X43)|min_precedes($f4(X42,X43),X42,X43). % 2.13/2.33 0 [] -leaf(X42,X43)| -min_precedes(X42,X45,X43). % 2.13/2.33 0 [] leaf(X42,X43)| -root(X42,X43)|min_precedes(X42,$f5(X42,X43),X43). % 2.13/2.33 0 [] leaf(X42,X43)| -min_precedes(X44,X42,X43)|min_precedes(X42,$f5(X42,X43),X43). % 2.13/2.33 0 [] -atocc(X46,X47)|subactivity(X47,$f6(X46,X47)). % 2.13/2.33 0 [] -atocc(X46,X47)|atomic($f6(X46,X47)). % 2.13/2.33 0 [] -atocc(X46,X47)|occurrence_of(X46,$f6(X46,X47)). % 2.13/2.33 0 [] atocc(X46,X47)| -subactivity(X47,X48)| -atomic(X48)| -occurrence_of(X46,X48). % 2.13/2.33 0 [] -atocc(X49,X50)| -legal(X49)|root(X49,X50). % 2.13/2.33 0 [] -legal(X51)|arboreal(X51). % 2.13/2.33 0 [] -activity_occurrence(X52)|activity($f7(X52)). % 2.13/2.33 0 [] -activity_occurrence(X52)|occurrence_of(X52,$f7(X52)). % 2.13/2.33 0 [] -subactivity_occurrence(X54,X55)|activity_occurrence(X54). % 2.13/2.33 0 [] -subactivity_occurrence(X54,X55)|activity_occurrence(X55). % 2.13/2.33 0 [] -occurrence_of(X56,X58)| -root_occ(X57,X56)| -min_precedes(X59,X57,X58). % 2.13/2.33 0 [] -occurrence_of(X60,X62)| -leaf_occ(X61,X60)| -min_precedes(X61,X63,X62). % 2.13/2.33 0 [] -occurrence_of(X64,X65)| -occurrence_of(X64,X66)|X65=X66. % 2.13/2.33 0 [] -leaf(X67,X68)|atomic(X68)|occurrence_of($f8(X67,X68),X68). % 2.13/2.33 0 [] -leaf(X67,X68)|atomic(X68)|leaf_occ(X67,$f8(X67,X68)). % 2.13/2.34 0 [] -min_precedes(X71,X72,X70)|occurrence_of($f9(X70,X71,X72),X70). % 2.13/2.34 0 [] -min_precedes(X71,X72,X70)|subactivity_occurrence(X71,$f9(X70,X71,X72)). % 2.13/2.34 0 [] -min_precedes(X71,X72,X70)|subactivity_occurrence(X72,$f9(X70,X71,X72)). % 2.13/2.34 0 [] -leaf(X74,X75)|atomic(X75)|occurrence_of($f10(X74,X75),X75). % 2.13/2.34 0 [] -leaf(X74,X75)|atomic(X75)|leaf_occ(X74,$f10(X74,X75)). % 2.13/2.34 0 [] -min_precedes(X78,X79,X77)|subactivity($f12(X77,X78,X79),X77). % 2.13/2.34 0 [] -min_precedes(X78,X79,X77)|subactivity($f11(X77,X78,X79),X77). % 2.13/2.34 0 [] -min_precedes(X78,X79,X77)|atocc(X78,$f12(X77,X78,X79)). % 2.13/2.34 0 [] -min_precedes(X78,X79,X77)|atocc(X79,$f11(X77,X78,X79)). % 2.13/2.34 0 [] -root(X83,X82)|subactivity($f13(X82,X83),X82). % 2.13/2.34 0 [] -root(X83,X82)|atocc(X83,$f13(X82,X83)). % 2.13/2.34 0 [] -occurrence_of(X86,X85)| -arboreal(X87)| -arboreal(X88)| -subactivity_occurrence(X87,X86)| -subactivity_occurrence(X88,X86)|min_precedes(X87,X88,X85)|min_precedes(X88,X87,X85)|X87=X88. % 2.13/2.34 0 [] -occurrence_of(X90,X89)|activity(X89). % 2.13/2.34 0 [] -occurrence_of(X90,X89)|activity_occurrence(X90). % 2.13/2.34 0 [] -occurrence_of(X92,X91)|atomic(X91)|root($f14(X91,X92),X91). % 2.13/2.34 0 [] -occurrence_of(X92,X91)|atomic(X91)|subactivity_occurrence($f14(X91,X92),X92). % 2.13/2.34 0 [] -activity(X94)|subactivity(X94,X94). % 2.13/2.34 0 [] -occurrence_of(X95,tptp0)|occurrence_of($f16(X95),tptp4). % 2.13/2.34 0 [] -occurrence_of(X95,tptp0)|root_occ($f16(X95),X95). % 2.13/2.34 0 [] -occurrence_of(X95,tptp0)|occurrence_of($f15(X95),tptp3)|occurrence_of($f15(X95),tptp2). % 2.13/2.34 0 [] -occurrence_of(X95,tptp0)|leaf_occ($f15(X95),X95). % 2.13/2.34 0 [] -occurrence_of(X95,tptp0)|next_subocc($f16(X95),$f15(X95),tptp0). % 2.13/2.34 0 [] activity(tptp0). % 2.13/2.34 0 [] -atomic(tptp0). % 2.13/2.34 0 [] atomic(tptp4). % 2.13/2.34 0 [] atomic(tptp3). % 2.13/2.34 0 [] atomic(tptp2). % 2.13/2.34 0 [] atomic(tptp5). % 2.13/2.34 0 [] tptp4!=tptp5. % 2.13/2.34 0 [] tptp4!=tptp3. % 2.13/2.34 0 [] tptp4!=tptp2. % 2.13/2.34 0 [] tptp5!=tptp3. % 2.13/2.34 0 [] tptp5!=tptp2. % 2.13/2.34 0 [] tptp3!=tptp2. % 2.13/2.34 0 [] -send_message(X98,X99,X100,X101,X102)|activity(X98). % 2.13/2.34 0 [] -send_message(X98,X99,X100,X101,X102)|atomic(X98). % 2.13/2.34 0 [] -send_message(X98,X99,X100,X101,X102)|root(X99,X100). % 2.13/2.34 0 [] -send_message(X98,X99,X100,X101,X102)|root(X101,X102). % 2.13/2.34 0 [] -send_message(X103,X104,X105,X106,X107)|X103!=tptp4. % 2.13/2.34 0 [] -send_message(X103,X104,X105,X106,X107)|X103!=tptp3. % 2.13/2.34 0 [] -send_message(X103,X104,X105,X106,X107)|X103!=tptp2. % 2.13/2.34 0 [] -send_message(X108,X109,X110,X111,X112)| -occurrence_of(X113,X108)|min_precedes(X111,X113,X112). % 2.13/2.34 0 [] -transmit_message(X114,X115,X116,X117,X118)|activity(X114). % 2.13/2.34 0 [] -transmit_message(X114,X115,X116,X117,X118)| -atomic(X114). % 2.13/2.34 0 [] -transmit_message(X114,X115,X116,X117,X118)|root(X115,X116). % 2.13/2.34 0 [] -transmit_message(X114,X115,X116,X117,X118)|root(X117,X118). % 2.13/2.34 0 [] -transmit_message(tptp0,X119,X120,X121,X122). % 2.13/2.34 0 [] -transmit_message(X123,X124,X125,X126,X127)| -tptp1(X123,X128,X129). % 2.13/2.34 0 [] -transmit_message(X130,X131,X132,X133,X134)| -occurrence_of(X135,X130)|send_message($f18(X130,X131,X132,X133,X134,X135),X131,X132,X133,X134). % 2.13/2.34 0 [] -transmit_message(X130,X131,X132,X133,X134)| -occurrence_of(X135,X130)|occurrence_of($f17(X130,X131,X132,X133,X134,X135),$f18(X130,X131,X132,X133,X134,X135)). % 2.13/2.34 0 [] -transmit_message(X130,X131,X132,X133,X134)| -occurrence_of(X135,X130)|root_occ($f17(X130,X131,X132,X133,X134,X135),X135). % 2.13/2.34 0 [] -tptp1(X138,X139,X140)|activity(X138). % 2.13/2.34 0 [] -tptp1(X138,X139,X140)| -atomic(X138). % 2.13/2.34 0 [] -tptp1(X138,X139,X140)| -atomic(X139). % 2.13/2.34 0 [] -tptp1(X138,X139,X140)|root(X140,X139). % 2.13/2.34 0 [] -tptp1(X141,X142,X143)| -occurrence_of(X144,X141)|transmit_message($f22(X141,X142,X143,X144),$f21(X141,X142,X143,X144),$f20(X141,X142,X143,X144),X143,X142). % 2.13/2.34 0 [] -tptp1(X141,X142,X143)| -occurrence_of(X144,X141)|occurrence_of($f19(X141,X142,X143,X144),$f22(X141,X142,X143,X144)). % 2.13/2.34 0 [] -tptp1(X141,X142,X143)| -occurrence_of(X144,X141)|subactivity_occurrence($f19(X141,X142,X143,X144),X144). % 2.13/2.34 0 [] -tptp1(tptp0,X149,X150). % 2.13/2.34 0 [] tptp1($c3,tptp0,$c2). % 2.13/2.34 0 [] occurrence_of($c1,$c3). % 2.13/2.34 end_of_list. % 2.13/2.34 % 2.13/2.34 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=8. % 2.13/2.34 % 2.13/2.34 This ia a non-Horn set with equality. The strategy will be % 2.13/2.34 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.13/2.34 deletion, with positive clauses in sos and nonpositive % 2.13/2.34 clauses in usable. % 2.13/2.34 % 2.13/2.34 dependent: set(knuth_bendix). % 2.13/2.34 dependent: set(anl_eq). % 2.13/2.34 dependent: set(para_from). % 2.13/2.34 dependent: set(para_into). % 2.13/2.34 dependent: clear(para_from_right). % 2.13/2.34 dependent: clear(para_into_right). % 2.13/2.34 dependent: set(para_from_vars). % 2.13/2.34 dependent: set(eq_units_both_ways). % 2.13/2.34 dependent: set(dynamic_demod_all). % 2.13/2.34 dependent: set(dynamic_demod). % 2.13/2.34 dependent: set(order_eq). % 2.13/2.34 dependent: set(back_demod). % 2.13/2.34 dependent: set(lrpo). % 2.13/2.34 dependent: set(hyper_res). % 2.13/2.34 dependent: set(unit_deletion). % 2.13/2.34 dependent: set(factor). % 2.13/2.34 % 2.13/2.34 ------------> process usable: % 2.13/2.34 ** KEPT (pick-wt=12): 1 [] -min_precedes(A,B,C)| -min_precedes(B,D,C)|min_precedes(A,D,C). % 2.13/2.34 ** KEPT (pick-wt=9): 2 [] -earlier(A,B)| -earlier(B,C)|earlier(A,C). % 2.13/2.34 ** KEPT (pick-wt=12): 3 [] -occurrence_of(A,B)| -root_occ(C,A)| -root_occ(D,A)|C=D. % 2.13/2.34 ** KEPT (pick-wt=14): 4 [] -occurrence_of(A,B)|atomic(B)| -leaf_occ(C,A)| -leaf_occ(D,A)|C=D. % 2.13/2.34 ** KEPT (pick-wt=8): 5 [] -next_subocc(A,B,C)|min_precedes(A,B,C). % 2.13/2.34 ** KEPT (pick-wt=12): 6 [] -next_subocc(A,B,C)| -min_precedes(A,D,C)| -min_precedes(D,B,C). % 2.13/2.34 ** KEPT (pick-wt=15): 7 [] next_subocc(A,B,C)| -min_precedes(A,B,C)|min_precedes(A,$f1(A,B,C),C). % 2.13/2.34 ** KEPT (pick-wt=15): 8 [] next_subocc(A,B,C)| -min_precedes(A,B,C)|min_precedes($f1(A,B,C),B,C). % 2.13/2.34 ** KEPT (pick-wt=6): 9 [] -next_subocc(A,B,C)|arboreal(A). % 2.13/2.34 ** KEPT (pick-wt=6): 10 [] -next_subocc(A,B,C)|arboreal(B). % 2.13/2.34 ** KEPT (pick-wt=7): 11 [] -min_precedes(A,B,C)|precedes(A,B). % 2.13/2.34 ** KEPT (pick-wt=7): 12 [] -min_precedes(A,B,C)| -root(B,C). % 2.13/2.34 ** KEPT (pick-wt=6): 13 [] -precedes(A,B)|earlier(A,B). % 2.13/2.34 ** KEPT (pick-wt=5): 14 [] -precedes(A,B)|legal(B). % 2.13/2.34 ** KEPT (pick-wt=8): 15 [] precedes(A,B)| -earlier(A,B)| -legal(B). % 2.13/2.34 ** KEPT (pick-wt=6): 16 [] -earlier(A,B)| -earlier(B,A). % 2.13/2.34 ** KEPT (pick-wt=8): 17 [] -root_occ(A,B)|occurrence_of(B,$f2(A,B)). % 2.13/2.34 ** KEPT (pick-wt=6): 18 [] -root_occ(A,B)|subactivity_occurrence(A,B). % 2.13/2.34 ** KEPT (pick-wt=8): 19 [] -root_occ(A,B)|root(A,$f2(A,B)). % 2.13/2.34 ** KEPT (pick-wt=12): 20 [] root_occ(A,B)| -occurrence_of(B,C)| -subactivity_occurrence(A,B)| -root(A,C). % 2.13/2.34 ** KEPT (pick-wt=8): 21 [] -leaf_occ(A,B)|occurrence_of(B,$f3(A,B)). % 2.13/2.34 ** KEPT (pick-wt=6): 22 [] -leaf_occ(A,B)|subactivity_occurrence(A,B). % 2.13/2.34 ** KEPT (pick-wt=8): 23 [] -leaf_occ(A,B)|leaf(A,$f3(A,B)). % 2.13/2.34 ** KEPT (pick-wt=12): 24 [] leaf_occ(A,B)| -occurrence_of(B,C)| -subactivity_occurrence(A,B)| -leaf(A,C). % 2.13/2.34 ** KEPT (pick-wt=5): 25 [] -root(A,B)|legal(A). % 2.13/2.34 ** KEPT (pick-wt=7): 26 [] -occurrence_of(A,B)| -arboreal(A)|atomic(B). % 2.13/2.34 ** KEPT (pick-wt=7): 27 [] -occurrence_of(A,B)|arboreal(A)| -atomic(B). % 2.13/2.34 ** KEPT (pick-wt=12): 28 [] -leaf(A,B)|root(A,B)|min_precedes($f4(A,B),A,B). % 2.13/2.34 ** KEPT (pick-wt=7): 29 [] -leaf(A,B)| -min_precedes(A,C,B). % 2.13/2.34 ** KEPT (pick-wt=12): 30 [] leaf(A,B)| -root(A,B)|min_precedes(A,$f5(A,B),B). % 2.13/2.34 ** KEPT (pick-wt=13): 31 [] leaf(A,B)| -min_precedes(C,A,B)|min_precedes(A,$f5(A,B),B). % 2.13/2.34 ** KEPT (pick-wt=8): 32 [] -atocc(A,B)|subactivity(B,$f6(A,B)). % 2.13/2.34 ** KEPT (pick-wt=7): 33 [] -atocc(A,B)|atomic($f6(A,B)). % 2.13/2.34 ** KEPT (pick-wt=8): 34 [] -atocc(A,B)|occurrence_of(A,$f6(A,B)). % 2.13/2.34 ** KEPT (pick-wt=11): 35 [] atocc(A,B)| -subactivity(B,C)| -atomic(C)| -occurrence_of(A,C). % 2.13/2.34 ** KEPT (pick-wt=8): 36 [] -atocc(A,B)| -legal(A)|root(A,B). % 2.13/2.34 ** KEPT (pick-wt=4): 37 [] -legal(A)|arboreal(A). % 2.13/2.34 ** KEPT (pick-wt=5): 38 [] -activity_occurrence(A)|activity($f7(A)). % 2.13/2.34 ** KEPT (pick-wt=6): 39 [] -activity_occurrence(A)|occurrence_of(A,$f7(A)). % 2.13/2.34 ** KEPT (pick-wt=5): 40 [] -subactivity_occurrence(A,B)|activity_occurrence(A). % 2.13/2.34 ** KEPT (pick-wt=5): 41 [] -subactivity_occurrence(A,B)|activity_occurrence(B). % 2.13/2.34 ** KEPT (pick-wt=10): 42 [] -occurrence_of(A,B)| -root_occ(C,A)| -min_precedes(D,C,B). % 2.13/2.34 ** KEPT (pick-wt=10): 43 [] -occurrence_of(A,B)| -leaf_occ(C,A)| -min_precedes(C,D,B). % 2.13/2.34 ** KEPT (pick-wt=9): 44 [] -occurrence_of(A,B)| -occurrence_of(A,C)|B=C. % 2.13/2.34 ** KEPT (pick-wt=10): 45 [] -leaf(A,B)|atomic(B)|occurrence_of($f8(A,B),B). % 2.13/2.34 ** KEPT (pick-wt=10): 46 [] -leaf(A,B)|atomic(B)|leaf_occ(A,$f8(A,B)). % 2.13/2.34 ** KEPT (pick-wt=10): 47 [] -min_precedes(A,B,C)|occurrence_of($f9(C,A,B),C). % 2.13/2.34 ** KEPT (pick-wt=10): 48 [] -min_precedes(A,B,C)|subactivity_occurrence(A,$f9(C,A,B)). % 2.13/2.34 ** KEPT (pick-wt=10): 49 [] -min_precedes(A,B,C)|subactivity_occurrence(B,$f9(C,A,B)). % 2.13/2.34 ** KEPT (pick-wt=10): 50 [] -leaf(A,B)|atomic(B)|occurrence_of($f10(A,B),B). % 2.13/2.34 ** KEPT (pick-wt=10): 51 [] -leaf(A,B)|atomic(B)|leaf_occ(A,$f10(A,B)). % 2.13/2.34 ** KEPT (pick-wt=10): 52 [] -min_precedes(A,B,C)|subactivity($f12(C,A,B),C). % 2.13/2.34 ** KEPT (pick-wt=10): 53 [] -min_precedes(A,B,C)|subactivity($f11(C,A,B),C). % 2.13/2.34 ** KEPT (pick-wt=10): 54 [] -min_precedes(A,B,C)|atocc(A,$f12(C,A,B)). % 2.13/2.34 ** KEPT (pick-wt=10): 55 [] -min_precedes(A,B,C)|atocc(B,$f11(C,A,B)). % 2.13/2.34 ** KEPT (pick-wt=8): 56 [] -root(A,B)|subactivity($f13(B,A),B). % 2.13/2.34 ** KEPT (pick-wt=8): 57 [] -root(A,B)|atocc(A,$f13(B,A)). % 2.13/2.34 ** KEPT (pick-wt=24): 58 [] -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.13/2.34 ** KEPT (pick-wt=5): 59 [] -occurrence_of(A,B)|activity(B). % 2.13/2.34 ** KEPT (pick-wt=5): 60 [] -occurrence_of(A,B)|activity_occurrence(A). % 2.13/2.34 ** KEPT (pick-wt=10): 61 [] -occurrence_of(A,B)|atomic(B)|root($f14(B,A),B). % 2.13/2.34 ** KEPT (pick-wt=10): 62 [] -occurrence_of(A,B)|atomic(B)|subactivity_occurrence($f14(B,A),A). % 2.13/2.34 ** KEPT (pick-wt=5): 63 [] -activity(A)|subactivity(A,A). % 2.13/2.34 ** KEPT (pick-wt=7): 64 [] -occurrence_of(A,tptp0)|occurrence_of($f16(A),tptp4). % 2.13/2.34 ** KEPT (pick-wt=7): 65 [] -occurrence_of(A,tptp0)|root_occ($f16(A),A). % 2.13/2.34 ** KEPT (pick-wt=11): 66 [] -occurrence_of(A,tptp0)|occurrence_of($f15(A),tptp3)|occurrence_of($f15(A),tptp2). % 2.13/2.34 ** KEPT (pick-wt=7): 67 [] -occurrence_of(A,tptp0)|leaf_occ($f15(A),A). % 2.13/2.34 ** KEPT (pick-wt=9): 68 [] -occurrence_of(A,tptp0)|next_subocc($f16(A),$f15(A),tptp0). % 2.13/2.34 ** KEPT (pick-wt=2): 69 [] -atomic(tptp0). % 2.13/2.34 ** KEPT (pick-wt=3): 71 [copy,70,flip.1] tptp5!=tptp4. % 2.13/2.34 ** KEPT (pick-wt=3): 72 [] tptp4!=tptp3. % 2.13/2.34 ** KEPT (pick-wt=3): 73 [] tptp4!=tptp2. % 2.13/2.34 ** KEPT (pick-wt=3): 74 [] tptp5!=tptp3. % 2.13/2.34 ** KEPT (pick-wt=3): 75 [] tptp5!=tptp2. % 2.13/2.34 ** KEPT (pick-wt=3): 76 [] tptp3!=tptp2. % 2.13/2.34 ** KEPT (pick-wt=8): 77 [] -send_message(A,B,C,D,E)|activity(A). % 2.13/2.34 ** KEPT (pick-wt=8): 78 [] -send_message(A,B,C,D,E)|atomic(A). % 2.13/2.34 ** KEPT (pick-wt=9): 79 [] -send_message(A,B,C,D,E)|root(B,C). % 2.13/2.34 ** KEPT (pick-wt=9): 80 [] -send_message(A,B,C,D,E)|root(D,E). % 2.13/2.34 ** KEPT (pick-wt=9): 81 [] -send_message(A,B,C,D,E)|A!=tptp4. % 2.13/2.34 ** KEPT (pick-wt=9): 82 [] -send_message(A,B,C,D,E)|A!=tptp3. % 2.13/2.34 ** KEPT (pick-wt=9): 83 [] -send_message(A,B,C,D,E)|A!=tptp2. % 2.13/2.34 ** KEPT (pick-wt=13): 84 [] -send_message(A,B,C,D,E)| -occurrence_of(F,A)|min_precedes(D,F,E). % 2.13/2.34 ** KEPT (pick-wt=8): 85 [] -transmit_message(A,B,C,D,E)|activity(A). % 2.13/2.34 ** KEPT (pick-wt=8): 86 [] -transmit_message(A,B,C,D,E)| -atomic(A). % 2.13/2.34 ** KEPT (pick-wt=9): 87 [] -transmit_message(A,B,C,D,E)|root(B,C). % 2.13/2.34 ** KEPT (pick-wt=9): 88 [] -transmit_message(A,B,C,D,E)|root(D,E). % 2.13/2.34 ** KEPT (pick-wt=6): 89 [] -transmit_message(tptp0,A,B,C,D). % 2.13/2.34 ** KEPT (pick-wt=10): 90 [] -transmit_message(A,B,C,D,E)| -tptp1(A,F,G). % 2.13/2.34 ** KEPT (pick-wt=21): 91 [] -transmit_message(A,B,C,D,E)| -occurrence_of(F,A)|send_message($f18(A,B,C,D,E,F),B,C,D,E). % 2.13/2.34 ** KEPT (pick-wt=24): 92 [] -transmit_message(A,B,C,D,E)| -occurrence_of(F,A)|occurrence_of($f17(A,B,C,D,E,F),$f18(A,B,C,D,E,F)). % 2.13/2.34 ** KEPT (pick-wt=18): 93 [] -transmit_message(A,B,C,D,E)| -occurrence_of(F,A)|root_occ($f17(A,B,C,D,E,F),F). % 2.13/2.34 ** KEPT (pick-wt=6): 94 [] -tptp1(A,B,C)|activity(A). % 2.13/2.34 ** KEPT (pick-wt=6): 95 [] -tptp1(A,B,C)| -atomic(A). % 2.13/2.34 ** KEPT (pick-wt=6): 96 [] -tptp1(A,B,C)| -atomic(B). % 2.13/2.34 ** KEPT (pick-wt=7): 97 [] -tptp1(A,B,C)|root(C,B). % 2.13/2.34 ** KEPT (pick-wt=25): 98 [] -tptp1(A,B,C)| -occurrence_of(D,A)|transmit_message($f22(A,B,C,D),$f21(A,B,C,D),$f20(A,B,C,D),C,B). % 2.13/2.34 ** KEPT (pick-wt=18): 99 [] -tptp1(A,B,C)| -occurrence_of(D,A)|occurrence_of($f19(A,B,C,D),$f22(A,B,C,D)). % 2.13/2.34 ** KEPT (pick-wt=14): 100 [] -tptp1(A,B,C)| -occurrence_of(D,A)|subactivity_occurrence($f19(A,B,C,D),D). % 2.13/2.34 ** KEPT (pick-wt=4): 101 [] -tptp1(tptp0,A,B). % 2.13/2.34 % 2.13/2.34 ------------> process sos: % 2.13/2.34 ** KEPT (pick-wt=3): 108 [] A=A. % 2.13/2.34 ** KEPT (pick-wt=2): 109 [] activity(tptp0). % 2.13/2.34 ** KEPT (pick-wt=2): 110 [] atomic(tptp4). % 2.13/2.34 ** KEPT (pick-wt=2): 111 [] atomic(tptp3). % 2.13/2.34 ** KEPT (pick-wt=2): 112 [] atomic(tptp2). % 2.13/2.34 ** KEPT (pick-wt=2): 113 [] atomic(tptp5). % 2.13/2.34 ** KEPT (pick-wt=4): 114 [] tptp1($c3,tptp0,$c2). % 4.05/4.21 ** KEPT (pick-wt=3): 115 [] occurrence_of($c1,$c3). % 4.05/4.21 Following clause subsumed by 108 during input processing: 0 [copy,108,flip.1] A=A. % 4.05/4.21 108 back subsumes 107. % 4.05/4.21 108 back subsumes 106. % 4.05/4.21 108 back subsumes 103. % 4.05/4.21 108 back subsumes 102. % 4.05/4.21 % 4.05/4.21 ======= end of input processing ======= % 4.05/4.21 % 4.05/4.21 =========== start of search =========== % 4.05/4.21 % 4.05/4.21 % 4.05/4.21 Resetting weight limit to 11. % 4.05/4.21 % 4.05/4.21 % 4.05/4.21 Resetting weight limit to 11. % 4.05/4.21 % 4.05/4.21 sos_size=1149 % 4.05/4.21 % 4.05/4.21 Search stopped because sos empty. % 4.05/4.21 % 4.05/4.21 % 4.05/4.21 Search stopped because sos empty. % 4.05/4.21 % 4.05/4.21 ============ end of search ============ % 4.05/4.21 % 4.05/4.21 -------------- statistics ------------- % 4.05/4.21 clauses given 1271 % 4.05/4.21 clauses generated 32586 % 4.05/4.21 clauses kept 1395 % 4.05/4.21 clauses forward subsumed 3411 % 4.05/4.21 clauses back subsumed 8 % 4.05/4.21 Kbytes malloced 5859 % 4.05/4.21 % 4.05/4.21 ----------- times (seconds) ----------- % 4.05/4.21 user CPU time 1.88 (0 hr, 0 min, 1 sec) % 4.05/4.21 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 4.05/4.21 wall-clock time 4 (0 hr, 0 min, 4 sec) % 4.05/4.21 % 4.05/4.21 Process 5472 finished Wed Jul 27 05:07:15 2022 % 4.05/4.21 Otter interrupted % 4.05/4.21 PROOF NOT FOUND %------------------------------------------------------------------------------