%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PRO009+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n011.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 : 600s
% DateTime : Mon Jul 18 17:49:00 EDT 2022
% Result : Theorem 6.99s 7.62s
% Output : Proof 6.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PRO009+3 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n011.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Mon Jun 13 01:42:18 EDT 2022
% 0.13/0.34 % CPUTime :
% 6.99/7.62 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.99/7.63 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.99/7.63
% 6.99/7.63 %-----------------------------------------------------
% 6.99/7.63 fof(goals, conjecture, ! [_132946] : (occurrence_of(_132946, tptp0) => ? [_132964, _132967] : (occurrence_of(_132964, tptp3) & root_occ(_132964, _132946) & (occurrence_of(_132967, tptp2) | occurrence_of(_132967, tptp1)) & min_precedes(_132964, _132967, tptp0) & leaf_occ(_132967, _132946))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 6.99/7.63 fof(sos_02, axiom, ! [_133403, _133406, _133409] : (occurrence_of(_133403, _133406) & occurrence_of(_133403, _133409) => _133406 = _133409), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_02)).
% 6.99/7.63 fof(sos_07, axiom, ! [_133589, _133592] : (occurrence_of(_133589, _133592) => (arboreal(_133589) <=> atomic(_133592))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_07)).
% 6.99/7.63 fof(sos_08, axiom, ! [_133749] : (legal(_133749) => arboreal(_133749)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_08)).
% 6.99/7.63 fof(sos_16, axiom, ! [_133884, _133887] : (root(_133884, _133887) => legal(_133884)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_16)).
% 6.99/7.63 fof(sos_21, axiom, ! [_134027, _134030] : (leaf(_134027, _134030) <=> (root(_134027, _134030) | ? [_134058] : min_precedes(_134058, _134027, _134030)) & ~ ? [_134081] : min_precedes(_134027, _134081, _134030)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_21)).
% 6.99/7.63 fof(sos_22, axiom, ! [_134313, _134316, _134319] : (next_subocc(_134313, _134316, _134319) <=> min_precedes(_134313, _134316, _134319) & ~ ? [_134355] : (min_precedes(_134313, _134355, _134319) & min_precedes(_134355, _134316, _134319))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_22)).
% 6.99/7.63 fof(sos_27, axiom, ! [_134605, _134608] : (occurrence_of(_134608, _134605) & ~ atomic(_134605) => ? [_134635] : (root(_134635, _134605) & subactivity_occurrence(_134635, _134608))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_27)).
% 6.99/7.63 fof(sos_28, axiom, ! [_134849, _134852, _134855, _134858] : (occurrence_of(_134852, _134849) & arboreal(_134855) & arboreal(_134858) & subactivity_occurrence(_134855, _134852) & subactivity_occurrence(_134858, _134852) => min_precedes(_134855, _134858, _134849) | min_precedes(_134858, _134855, _134849) | _134855 = _134858), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_28)).
% 6.99/7.63 fof(sos_33, axiom, ! [_135188, _135191] : (root_occ(_135188, _135191) <=> ? [_135209] : (occurrence_of(_135191, _135209) & subactivity_occurrence(_135188, _135191) & root(_135188, _135209))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_33)).
% 6.99/7.63 fof(sos_34, axiom, ! [_135432, _135435] : (leaf_occ(_135432, _135435) <=> ? [_135453] : (occurrence_of(_135435, _135453) & subactivity_occurrence(_135432, _135435) & leaf(_135432, _135453))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_34)).
% 6.99/7.63 fof(sos_35, axiom, ! [_135689, _135692, _135695, _135698] : (occurrence_of(_135695, _135698) & root_occ(_135689, _135695) & root_occ(_135692, _135695) => _135689 = _135692), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_35)).
% 6.99/7.63 fof(sos_41, axiom, ! [_135914, _135917, _135920, _135923] : (occurrence_of(_135914, _135923) & leaf_occ(_135917, _135914) & root_occ(_135920, _135914) & (! _135917) = _135920 => min_precedes(_135920, _135917, _135923)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_41)).
% 6.99/7.63 fof(sos_51, axiom, ~ atomic(tptp0), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_51)).
% 6.99/7.63 fof(sos_53, axiom, atomic(tptp2), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_53)).
% 6.99/7.63 fof(sos_54, axiom, atomic(tptp1), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_54)).
% 6.99/7.63 fof(sos_49, axiom, ! [_136336] : (occurrence_of(_136336, tptp0) => ? [_136354, _136357, _136360] : (occurrence_of(_136354, tptp3) & root_occ(_136354, _136336) & occurrence_of(_136357, tptp4) & next_subocc(_136354, _136357, tptp0) & (occurrence_of(_136360, tptp2) | occurrence_of(_136360, tptp1)) & next_subocc(_136357, _136360, tptp0) & leaf_occ(_136360, _136336))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_49)).
% 6.99/7.63
% 6.99/7.63 cnf(1, plain, [-(21 ^ [_89226, _89221]), occurrence_of(_89226, tptp1)], clausify(goals)).
% 6.99/7.63 cnf(2, plain, [-(21 ^ [_89226, _89221]), occurrence_of(_89226, tptp2)], clausify(goals)).
% 6.99/7.63 cnf(3, plain, [-(occurrence_of(20 ^ [], tptp0))], clausify(goals)).
% 6.99/7.63 cnf(4, plain, [occurrence_of(_89221, tptp3), root_occ(_89221, 20 ^ []), 21 ^ [_89226, _89221], min_precedes(_89221, _89226, tptp0), leaf_occ(_89226, 20 ^ [])], clausify(goals)).
% 6.99/7.63 cnf(5, plain, [-(_32083 = _32083)], theory(equality)).
% 6.99/7.63 cnf(6, plain, [_32236 = _32281, -(_32281 = _32236)], theory(equality)).
% 6.99/7.63 cnf(7, plain, [-(leaf(_35622, _35753)), leaf(_35555, _35688), _35555 = _35622, _35688 = _35753], theory(equality)).
% 6.99/7.63 cnf(8, plain, [-(leaf_occ(_36246, _36377)), leaf_occ(_36179, _36312), _36179 = _36246, _36312 = _36377], theory(equality)).
% 6.99/7.63 cnf(9, plain, [-(min_precedes(_37217, _37384, _37547)), min_precedes(_37132, _37301, _37466), _37132 = _37217, _37301 = _37384, _37466 = _37547], theory(equality)).
% 6.99/7.63 cnf(10, plain, [-(root_occ(_41121, _41252)), root_occ(_41054, _41187), _41054 = _41121, _41187 = _41252], theory(equality)).
% 6.99/7.63 cnf(11, plain, [-(subactivity_occurrence(_42359, _42490)), subactivity_occurrence(_42292, _42425), _42292 = _42359, _42425 = _42490], theory(equality)).
% 6.99/7.63 cnf(12, plain, [-(_43944 = _43999), occurrence_of(_43888, _43944), occurrence_of(_43888, _43999)], clausify(sos_02)).
% 6.99/7.63 cnf(13, plain, [occurrence_of(_46035, _46084), -(arboreal(_46035)), atomic(_46084)], clausify(sos_07)).
% 6.99/7.63 cnf(14, plain, [legal(_46385), -(arboreal(_46385))], clausify(sos_08)).
% 6.99/7.63 cnf(15, plain, [root(_50144, _50188), -(legal(_50144))], clausify(sos_16)).
% 6.99/7.63 cnf(16, plain, [leaf(_52774, _52845), min_precedes(_52774, _53207, _52845)], clausify(sos_21)).
% 6.99/7.63 cnf(17, plain, [next_subocc(_53482, _53555, _53627), -(min_precedes(_53482, _53555, _53627))], clausify(sos_22)).
% 6.99/7.63 cnf(18, plain, [-(root(12 ^ [_56483, _56420], _56420)), occurrence_of(_56483, _56420), -(atomic(_56420))], clausify(sos_27)).
% 6.99/7.63 cnf(19, plain, [-(subactivity_occurrence(12 ^ [_56483, _56420], _56483)), occurrence_of(_56483, _56420), -(atomic(_56420))], clausify(sos_27)).
% 6.99/7.63 cnf(20, plain, [-(_57146 = _57235), -(min_precedes(_57235, _57146, _56965)), -(min_precedes(_57146, _57235, _56965)), occurrence_of(_57056, _56965), arboreal(_57146), arboreal(_57235), subactivity_occurrence(_57146, _57056), subactivity_occurrence(_57235, _57056)], clausify(sos_28)).
% 6.99/7.63 cnf(21, plain, [root_occ(_60913, _60975), -(root(_60913, 14 ^ [_60975, _60913]))], clausify(sos_33)).
% 6.99/7.63 cnf(22, plain, [-(root_occ(_60913, _60975)), occurrence_of(_60975, _61096), subactivity_occurrence(_60913, _60975), root(_60913, _61096)], clausify(sos_33)).
% 6.99/7.63 cnf(23, plain, [leaf_occ(_61467, _61529), -(occurrence_of(_61529, 15 ^ [_61529, _61467]))], clausify(sos_34)).
% 6.99/7.63 cnf(24, plain, [leaf_occ(_61467, _61529), -(subactivity_occurrence(_61467, _61529))], clausify(sos_34)).
% 6.99/7.63 cnf(25, plain, [leaf_occ(_61467, _61529), -(leaf(_61467, 15 ^ [_61529, _61467]))], clausify(sos_34)).
% 6.99/7.63 cnf(26, plain, [-(_62021 = _62088), occurrence_of(_62154, _62219), root_occ(_62021, _62154), root_occ(_62088, _62154)], clausify(sos_35)).
% 6.99/7.63 cnf(27, plain, [-(min_precedes(_66436, _66361, _66510)), occurrence_of(_66285, _66510), leaf_occ(_66361, _66285), root_occ(_66436, _66285), -(_66361 = _66436)], clausify(sos_41)).
% 6.99/7.63 cnf(28, plain, [atomic(tptp0)], clausify(sos_51)).
% 6.99/7.63 cnf(29, plain, [-(atomic(tptp2))], clausify(sos_53)).
% 6.99/7.63 cnf(30, plain, [-(atomic(tptp1))], clausify(sos_54)).
% 6.99/7.63 cnf(31, plain, [occurrence_of(_72601, tptp0), -(occurrence_of(17 ^ [_72601], tptp3))], clausify(sos_49)).
% 6.99/7.63 cnf(32, plain, [occurrence_of(_72601, tptp0), -(root_occ(17 ^ [_72601], _72601))], clausify(sos_49)).
% 6.99/7.63 cnf(33, plain, [occurrence_of(_72601, tptp0), -(next_subocc(17 ^ [_72601], 18 ^ [_72601], tptp0))], clausify(sos_49)).
% 6.99/7.63 cnf(34, plain, [occurrence_of(_72601, tptp0), -(leaf_occ(19 ^ [_72601], _72601))], clausify(sos_49)).
% 6.99/7.63 cnf(35, plain, [occurrence_of(_72601, tptp0), -(occurrence_of(19 ^ [_72601], tptp2)), -(occurrence_of(19 ^ [_72601], tptp1))], clausify(sos_49)).
% 6.99/7.63
% 6.99/7.63 cnf('1',plain,[occurrence_of(17 ^ [20 ^ []], tptp3), root_occ(17 ^ [20 ^ []], 20 ^ []), 21 ^ [19 ^ [20 ^ []], 17 ^ [20 ^ []]], min_precedes(17 ^ [20 ^ []], 19 ^ [20 ^ []], tptp0), leaf_occ(19 ^ [20 ^ []], 20 ^ [])],start(4,bind([[_89221, _89226], [17 ^ [20 ^ []], 19 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.1',plain,[-(occurrence_of(17 ^ [20 ^ []], tptp3)), occurrence_of(20 ^ [], tptp0)],extension(31,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.2',plain,[-(root_occ(17 ^ [20 ^ []], 20 ^ [])), root_occ(17 ^ [20 ^ []], 20 ^ []), 17 ^ [20 ^ []] = 17 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(10,bind([[_41054, _41121, _41187, _41252], [17 ^ [20 ^ []], 17 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.2.1',plain,[-(root_occ(17 ^ [20 ^ []], 20 ^ [])), root_occ(17 ^ [20 ^ []], 20 ^ []), 17 ^ [20 ^ []] = 17 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(10,bind([[_41054, _41121, _41187, _41252], [17 ^ [20 ^ []], 17 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.2.1.1',plain,[-(root_occ(17 ^ [20 ^ []], 20 ^ [])), root_occ(17 ^ [20 ^ []], 20 ^ []), 17 ^ [20 ^ []] = 17 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(10,bind([[_41054, _41121, _41187, _41252], [17 ^ [20 ^ []], 17 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.2.1.1.1',plain,[-(root_occ(17 ^ [20 ^ []], 20 ^ [])), root_occ(17 ^ [20 ^ []], 20 ^ []), 17 ^ [20 ^ []] = 17 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(10,bind([[_41054, _41121, _41187, _41252], [17 ^ [20 ^ []], 17 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.2.1.1.1.1',plain,[-(root_occ(17 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(32,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.2.1.1.1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.2.1.1.1.2',plain,[-(17 ^ [20 ^ []] = 17 ^ [20 ^ []])],extension(5,bind([[_32083], [17 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.2.1.1.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.2.1.1.2',plain,[-(17 ^ [20 ^ []] = 17 ^ [20 ^ []])],extension(5,bind([[_32083], [17 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.2.1.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.2.1.2',plain,[-(17 ^ [20 ^ []] = 17 ^ [20 ^ []])],extension(5,bind([[_32083], [17 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.2.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.2.2',plain,[-(17 ^ [20 ^ []] = 17 ^ [20 ^ []])],extension(5,bind([[_32083], [17 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.2.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.3',plain,[-(21 ^ [19 ^ [20 ^ []], 17 ^ [20 ^ []]]), occurrence_of(19 ^ [20 ^ []], tptp1)],extension(1,bind([[_89221, _89226], [17 ^ [20 ^ []], 19 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.3.1',plain,[-(occurrence_of(19 ^ [20 ^ []], tptp1)), occurrence_of(20 ^ [], tptp0), -(occurrence_of(19 ^ [20 ^ []], tptp2))],extension(35,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.3.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.3.1.2',plain,[occurrence_of(19 ^ [20 ^ []], tptp2), -(21 ^ [19 ^ [20 ^ []], 17 ^ [20 ^ []]])],extension(2,bind([[_89226, _89221], [19 ^ [20 ^ []], 17 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.3.1.2.1',plain,[21 ^ [19 ^ [20 ^ []], 17 ^ [20 ^ []]]],reduction('1')).
% 6.99/7.63 cnf('1.4',plain,[-(min_precedes(17 ^ [20 ^ []], 19 ^ [20 ^ []], tptp0)), -(19 ^ [20 ^ []] = 17 ^ [20 ^ []]), -(min_precedes(19 ^ [20 ^ []], 17 ^ [20 ^ []], tptp0)), occurrence_of(20 ^ [], tptp0), arboreal(19 ^ [20 ^ []]), arboreal(17 ^ [20 ^ []]), subactivity_occurrence(19 ^ [20 ^ []], 20 ^ []), subactivity_occurrence(17 ^ [20 ^ []], 20 ^ [])],extension(20,bind([[_56965, _57146, _57235, _57056], [tptp0, 19 ^ [20 ^ []], 17 ^ [20 ^ []], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.1',plain,[19 ^ [20 ^ []] = 17 ^ [20 ^ []], -(leaf(17 ^ [20 ^ []], tptp0)), leaf(19 ^ [20 ^ []], 15 ^ [20 ^ [], 19 ^ [20 ^ []]]), 15 ^ [20 ^ [], 19 ^ [20 ^ []]] = tptp0],extension(7,bind([[_35622, _35555, _35688, _35753], [17 ^ [20 ^ []], 19 ^ [20 ^ []], 15 ^ [20 ^ [], 19 ^ [20 ^ []]], tptp0]]))).
% 6.99/7.63 cnf('1.4.1.1',plain,[leaf(17 ^ [20 ^ []], tptp0), min_precedes(17 ^ [20 ^ []], 18 ^ [20 ^ []], tptp0)],extension(16,bind([[_52774, _53207, _52845], [17 ^ [20 ^ []], 18 ^ [20 ^ []], tptp0]]))).
% 6.99/7.63 cnf('1.4.1.1.1',plain,[-(min_precedes(17 ^ [20 ^ []], 18 ^ [20 ^ []], tptp0)), next_subocc(17 ^ [20 ^ []], 18 ^ [20 ^ []], tptp0)],extension(17,bind([[_53482, _53555, _53627], [17 ^ [20 ^ []], 18 ^ [20 ^ []], tptp0]]))).
% 6.99/7.63 cnf('1.4.1.1.1.1',plain,[-(next_subocc(17 ^ [20 ^ []], 18 ^ [20 ^ []], tptp0)), occurrence_of(20 ^ [], tptp0)],extension(33,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.1.1.1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.1.2',plain,[-(leaf(19 ^ [20 ^ []], 15 ^ [20 ^ [], 19 ^ [20 ^ []]])), leaf(19 ^ [20 ^ []], 15 ^ [20 ^ [], 19 ^ [20 ^ []]]), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 15 ^ [20 ^ [], 19 ^ [20 ^ []]] = 15 ^ [20 ^ [], 19 ^ [20 ^ []]]],extension(7,bind([[_35555, _35622, _35688, _35753], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 15 ^ [20 ^ [], 19 ^ [20 ^ []]], 15 ^ [20 ^ [], 19 ^ [20 ^ []]]]]))).
% 6.99/7.63 cnf('1.4.1.2.1',plain,[-(leaf(19 ^ [20 ^ []], 15 ^ [20 ^ [], 19 ^ [20 ^ []]])), leaf_occ(19 ^ [20 ^ []], 20 ^ [])],extension(25,bind([[_61467, _61529], [19 ^ [20 ^ []], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.1.2.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(34,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.1.2.1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.1.2.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32083], [19 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.4.1.2.3',plain,[-(15 ^ [20 ^ [], 19 ^ [20 ^ []]] = 15 ^ [20 ^ [], 19 ^ [20 ^ []]])],extension(5,bind([[_32083], [15 ^ [20 ^ [], 19 ^ [20 ^ []]]]]))).
% 6.99/7.63 cnf('1.4.1.3',plain,[-(15 ^ [20 ^ [], 19 ^ [20 ^ []]] = tptp0), occurrence_of(20 ^ [], 15 ^ [20 ^ [], 19 ^ [20 ^ []]]), occurrence_of(20 ^ [], tptp0)],extension(12,bind([[_43944, _43888, _43999], [15 ^ [20 ^ [], 19 ^ [20 ^ []]], 20 ^ [], tptp0]]))).
% 6.99/7.63 cnf('1.4.1.3.1',plain,[-(occurrence_of(20 ^ [], 15 ^ [20 ^ [], 19 ^ [20 ^ []]])), leaf_occ(19 ^ [20 ^ []], 20 ^ [])],extension(23,bind([[_61467, _61529], [19 ^ [20 ^ []], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.1.3.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(34,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.1.3.1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.1.3.2',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.2',plain,[min_precedes(19 ^ [20 ^ []], 17 ^ [20 ^ []], tptp0), -(min_precedes(17 ^ [20 ^ []], 19 ^ [20 ^ []], tptp0)), 19 ^ [20 ^ []] = 17 ^ [20 ^ []], 17 ^ [20 ^ []] = 19 ^ [20 ^ []], tptp0 = tptp0],extension(9,bind([[_37132, _37217, _37301, _37384, _37466, _37547], [19 ^ [20 ^ []], 17 ^ [20 ^ []], 17 ^ [20 ^ []], 19 ^ [20 ^ []], tptp0, tptp0]]))).
% 6.99/7.63 cnf('1.4.2.1',plain,[min_precedes(17 ^ [20 ^ []], 19 ^ [20 ^ []], tptp0)],reduction('1')).
% 6.99/7.63 cnf('1.4.2.2',plain,[-(19 ^ [20 ^ []] = 17 ^ [20 ^ []]), -(min_precedes(17 ^ [20 ^ []], 19 ^ [20 ^ []], tptp0)), occurrence_of(20 ^ [], tptp0), leaf_occ(19 ^ [20 ^ []], 20 ^ []), root_occ(17 ^ [20 ^ []], 20 ^ [])],extension(27,bind([[_66510, _66361, _66436, _66285], [tptp0, 19 ^ [20 ^ []], 17 ^ [20 ^ []], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.2.2.1',plain,[min_precedes(17 ^ [20 ^ []], 19 ^ [20 ^ []], tptp0)],lemmata('1.4.2')).
% 6.99/7.63 cnf('1.4.2.2.2',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.2.2.3',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(8,bind([[_36179, _36246, _36312, _36377], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.2.2.3.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(34,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.2.2.3.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.2.2.3.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32083], [19 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.4.2.2.3.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.2.2.4',plain,[-(root_occ(17 ^ [20 ^ []], 20 ^ []))],lemmata('1')).
% 6.99/7.63 cnf('1.4.2.3',plain,[-(17 ^ [20 ^ []] = 19 ^ [20 ^ []]), 19 ^ [20 ^ []] = 17 ^ [20 ^ []]],extension(6,bind([[_32236, _32281], [19 ^ [20 ^ []], 17 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.4.2.3.1',plain,[-(19 ^ [20 ^ []] = 17 ^ [20 ^ []])],lemmata('1.4.2')).
% 6.99/7.63 cnf('1.4.2.4',plain,[-(tptp0 = tptp0)],extension(5,bind([[_32083], [tptp0]]))).
% 6.99/7.63 cnf('1.4.3',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.4',plain,[-(arboreal(19 ^ [20 ^ []])), occurrence_of(19 ^ [20 ^ []], tptp2), atomic(tptp2)],extension(13,bind([[_46035, _46084], [19 ^ [20 ^ []], tptp2]]))).
% 6.99/7.63 cnf('1.4.4.1',plain,[-(occurrence_of(19 ^ [20 ^ []], tptp2)), occurrence_of(20 ^ [], tptp0), -(occurrence_of(19 ^ [20 ^ []], tptp1))],extension(35,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.4.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.4.1.2',plain,[occurrence_of(19 ^ [20 ^ []], tptp1), -(arboreal(19 ^ [20 ^ []])), atomic(tptp1)],extension(13,bind([[_46035, _46084], [19 ^ [20 ^ []], tptp1]]))).
% 6.99/7.63 cnf('1.4.4.1.2.1',plain,[arboreal(19 ^ [20 ^ []])],reduction('1.4')).
% 6.99/7.63 cnf('1.4.4.1.2.2',plain,[-(atomic(tptp1))],extension(30)).
% 6.99/7.63 cnf('1.4.4.2',plain,[-(atomic(tptp2))],extension(29)).
% 6.99/7.63 cnf('1.4.5',plain,[-(arboreal(17 ^ [20 ^ []])), legal(17 ^ [20 ^ []])],extension(14,bind([[_46385], [17 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.4.5.1',plain,[-(legal(17 ^ [20 ^ []])), root(17 ^ [20 ^ []], 14 ^ [20 ^ [], 17 ^ [20 ^ []]])],extension(15,bind([[_50144, _50188], [17 ^ [20 ^ []], 14 ^ [20 ^ [], 17 ^ [20 ^ []]]]]))).
% 6.99/7.63 cnf('1.4.5.1.1',plain,[-(root(17 ^ [20 ^ []], 14 ^ [20 ^ [], 17 ^ [20 ^ []]])), root_occ(17 ^ [20 ^ []], 20 ^ [])],extension(21,bind([[_60913, _60975], [17 ^ [20 ^ []], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.5.1.1.1',plain,[-(root_occ(17 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(32,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.5.1.1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.6',plain,[-(subactivity_occurrence(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ [])],extension(24,bind([[_61467, _61529], [19 ^ [20 ^ []], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.6.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(8,bind([[_36179, _36246, _36312, _36377], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.6.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(8,bind([[_36179, _36246, _36312, _36377], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.6.1.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(34,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.6.1.1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.6.1.1.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32083], [19 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.4.6.1.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.6.1.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32083], [19 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.4.6.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.7',plain,[-(subactivity_occurrence(17 ^ [20 ^ []], 20 ^ [])), subactivity_occurrence(12 ^ [20 ^ [], tptp0], 20 ^ []), 12 ^ [20 ^ [], tptp0] = 17 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(11,bind([[_42292, _42359, _42425, _42490], [12 ^ [20 ^ [], tptp0], 17 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.7.1',plain,[-(subactivity_occurrence(12 ^ [20 ^ [], tptp0], 20 ^ [])), subactivity_occurrence(12 ^ [20 ^ [], tptp0], 20 ^ []), 12 ^ [20 ^ [], tptp0] = 12 ^ [20 ^ [], tptp0], 20 ^ [] = 20 ^ []],extension(11,bind([[_42292, _42359, _42425, _42490], [12 ^ [20 ^ [], tptp0], 12 ^ [20 ^ [], tptp0], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.7.1.1',plain,[-(subactivity_occurrence(12 ^ [20 ^ [], tptp0], 20 ^ [])), subactivity_occurrence(12 ^ [20 ^ [], tptp0], 20 ^ []), 12 ^ [20 ^ [], tptp0] = 12 ^ [20 ^ [], tptp0], 20 ^ [] = 20 ^ []],extension(11,bind([[_42292, _42359, _42425, _42490], [12 ^ [20 ^ [], tptp0], 12 ^ [20 ^ [], tptp0], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.7.1.1.1',plain,[-(subactivity_occurrence(12 ^ [20 ^ [], tptp0], 20 ^ [])), occurrence_of(20 ^ [], tptp0), -(atomic(tptp0))],extension(19,bind([[_56483, _56420], [20 ^ [], tptp0]]))).
% 6.99/7.63 cnf('1.4.7.1.1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.7.1.1.1.2',plain,[atomic(tptp0)],extension(28)).
% 6.99/7.63 cnf('1.4.7.1.1.2',plain,[-(12 ^ [20 ^ [], tptp0] = 12 ^ [20 ^ [], tptp0])],extension(5,bind([[_32083], [12 ^ [20 ^ [], tptp0]]]))).
% 6.99/7.63 cnf('1.4.7.1.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.7.1.2',plain,[-(12 ^ [20 ^ [], tptp0] = 12 ^ [20 ^ [], tptp0])],extension(5,bind([[_32083], [12 ^ [20 ^ [], tptp0]]]))).
% 6.99/7.63 cnf('1.4.7.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.4.7.2',plain,[-(12 ^ [20 ^ [], tptp0] = 17 ^ [20 ^ []]), occurrence_of(20 ^ [], tptp0), root_occ(12 ^ [20 ^ [], tptp0], 20 ^ []), root_occ(17 ^ [20 ^ []], 20 ^ [])],extension(26,bind([[_62219, _62021, _62088, _62154], [tptp0, 12 ^ [20 ^ [], tptp0], 17 ^ [20 ^ []], 20 ^ []]]))).
% 6.99/7.63 cnf('1.4.7.2.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.7.2.2',plain,[-(root_occ(12 ^ [20 ^ [], tptp0], 20 ^ [])), occurrence_of(20 ^ [], tptp0), subactivity_occurrence(12 ^ [20 ^ [], tptp0], 20 ^ []), root(12 ^ [20 ^ [], tptp0], tptp0)],extension(22,bind([[_60975, _60913, _61096], [20 ^ [], 12 ^ [20 ^ [], tptp0], tptp0]]))).
% 6.99/7.63 cnf('1.4.7.2.2.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.7.2.2.2',plain,[-(subactivity_occurrence(12 ^ [20 ^ [], tptp0], 20 ^ []))],lemmata('1.4.7')).
% 6.99/7.63 cnf('1.4.7.2.2.3',plain,[-(root(12 ^ [20 ^ [], tptp0], tptp0)), occurrence_of(20 ^ [], tptp0), -(atomic(tptp0))],extension(18,bind([[_56483, _56420], [20 ^ [], tptp0]]))).
% 6.99/7.63 cnf('1.4.7.2.2.3.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.4.7.2.2.3.2',plain,[atomic(tptp0)],extension(28)).
% 6.99/7.63 cnf('1.4.7.2.3',plain,[-(root_occ(17 ^ [20 ^ []], 20 ^ []))],lemmata('1')).
% 6.99/7.63 cnf('1.4.7.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.5',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(8,bind([[_36179, _36246, _36312, _36377], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.5.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(8,bind([[_36179, _36246, _36312, _36377], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.5.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(8,bind([[_36179, _36246, _36312, _36377], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.5.1.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(8,bind([[_36179, _36246, _36312, _36377], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 6.99/7.63 cnf('1.5.1.1.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(34,bind([[_72601], [20 ^ []]]))).
% 6.99/7.63 cnf('1.5.1.1.1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 6.99/7.63 cnf('1.5.1.1.1.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32083], [19 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.5.1.1.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.5.1.1.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32083], [19 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.5.1.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.5.1.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32083], [19 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.5.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 cnf('1.5.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32083], [19 ^ [20 ^ []]]]))).
% 6.99/7.63 cnf('1.5.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32083], [20 ^ []]]))).
% 6.99/7.63 %-----------------------------------------------------
% 6.99/7.64
% 6.99/7.64 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------