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