%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PRO009+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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:48:59 EDT 2022
% Result : Theorem 10.41s 10.75s
% Output : Proof 10.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PRO009+1 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n018.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jun 13 03:38:57 EDT 2022
% 0.13/0.34 % CPUTime :
% 10.41/10.75 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.41/10.75 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.41/10.76
% 10.41/10.76 %-----------------------------------------------------
% 10.41/10.76 fof(goals, conjecture, ! [_115434] : (occurrence_of(_115434, tptp0) => ? [_115452, _115455] : (occurrence_of(_115452, tptp3) & root_occ(_115452, _115434) & (occurrence_of(_115455, tptp2) | occurrence_of(_115455, tptp1)) & min_precedes(_115452, _115455, tptp0) & leaf_occ(_115455, _115434))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 10.41/10.76 fof(sos_02, axiom, ! [_115891, _115894, _115897] : (occurrence_of(_115891, _115894) & occurrence_of(_115891, _115897) => _115894 = _115897), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_02)).
% 10.41/10.76 fof(sos_08, axiom, ! [_116078] : (legal(_116078) => arboreal(_116078)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_08)).
% 10.41/10.76 fof(sos_10, axiom, ! [_116201, _116204] : (precedes(_116201, _116204) <=> earlier(_116201, _116204) & legal(_116204)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_10)).
% 10.41/10.76 fof(sos_14, axiom, ! [_116377, _116380, _116383] : (min_precedes(_116377, _116380, _116383) => ~ root(_116380, _116383)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_14)).
% 10.41/10.76 fof(sos_15, axiom, ! [_116548, _116551, _116554] : (min_precedes(_116548, _116551, _116554) => precedes(_116548, _116551)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_15)).
% 10.41/10.76 fof(sos_16, axiom, ! [_116712, _116715] : (root(_116712, _116715) => legal(_116712)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_16)).
% 10.41/10.76 fof(sos_21, axiom, ! [_116855, _116858] : (leaf(_116855, _116858) <=> (root(_116855, _116858) | ? [_116886] : min_precedes(_116886, _116855, _116858)) & ~ ? [_116909] : min_precedes(_116855, _116909, _116858)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_21)).
% 10.41/10.76 fof(sos_22, axiom, ! [_117141, _117144, _117147] : (next_subocc(_117141, _117144, _117147) <=> min_precedes(_117141, _117144, _117147) & ~ ? [_117183] : (min_precedes(_117141, _117183, _117147) & min_precedes(_117183, _117144, _117147))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_22)).
% 10.41/10.76 fof(sos_28, axiom, ! [_117435, _117438, _117441, _117444] : (occurrence_of(_117438, _117435) & arboreal(_117441) & arboreal(_117444) & subactivity_occurrence(_117441, _117438) & subactivity_occurrence(_117444, _117438) => min_precedes(_117441, _117444, _117435) | min_precedes(_117444, _117441, _117435) | _117441 = _117444), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_28)).
% 10.41/10.76 fof(sos_29, axiom, ! [_117767, _117770, _117773, _117776] : (min_precedes(_117767, _117770, _117773) & occurrence_of(_117776, _117773) & subactivity_occurrence(_117770, _117776) => subactivity_occurrence(_117767, _117776)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_29)).
% 10.41/10.76 fof(sos_33, axiom, ! [_118002, _118005] : (root_occ(_118002, _118005) <=> ? [_118023] : (occurrence_of(_118005, _118023) & subactivity_occurrence(_118002, _118005) & root(_118002, _118023))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_33)).
% 10.41/10.76 fof(sos_35, axiom, ! [_118260] : (occurrence_of(_118260, tptp0) => ? [_118278, _118281, _118284] : (occurrence_of(_118278, tptp3) & root_occ(_118278, _118260) & occurrence_of(_118281, tptp4) & next_subocc(_118278, _118281, tptp0) & (occurrence_of(_118284, tptp2) | occurrence_of(_118284, tptp1)) & next_subocc(_118281, _118284, tptp0) & leaf_occ(_118284, _118260))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_35)).
% 10.41/10.76 fof(sos_34, axiom, ! [_118718, _118721] : (leaf_occ(_118718, _118721) <=> ? [_118739] : (occurrence_of(_118721, _118739) & subactivity_occurrence(_118718, _118721) & leaf(_118718, _118739))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_34)).
% 10.41/10.76
% 10.41/10.76 cnf(1, plain, [-(20 ^ [_67871, _67866]), occurrence_of(_67871, tptp1)], clausify(goals)).
% 10.41/10.76 cnf(2, plain, [-(20 ^ [_67871, _67866]), occurrence_of(_67871, tptp2)], clausify(goals)).
% 10.41/10.76 cnf(3, plain, [-(occurrence_of(19 ^ [], tptp0))], clausify(goals)).
% 10.41/10.76 cnf(4, plain, [occurrence_of(_67866, tptp3), root_occ(_67866, 19 ^ []), 20 ^ [_67871, _67866], min_precedes(_67866, _67871, tptp0), leaf_occ(_67871, 19 ^ [])], clausify(goals)).
% 10.41/10.76 cnf(5, plain, [-(_23584 = _23584)], theory(equality)).
% 10.41/10.76 cnf(6, plain, [_23737 = _23782, -(_23782 = _23737)], theory(equality)).
% 10.41/10.76 cnf(7, plain, [-(leaf(_27123, _27254)), leaf(_27056, _27189), _27056 = _27123, _27189 = _27254], theory(equality)).
% 10.41/10.76 cnf(8, plain, [-(leaf_occ(_27747, _27878)), leaf_occ(_27680, _27813), _27680 = _27747, _27813 = _27878], theory(equality)).
% 10.41/10.76 cnf(9, plain, [-(min_precedes(_28718, _28885, _29048)), min_precedes(_28633, _28802, _28967), _28633 = _28718, _28802 = _28885, _28967 = _29048], theory(equality)).
% 10.41/10.76 cnf(10, plain, [-(root(_31998, _32129)), root(_31931, _32064), _31931 = _31998, _32064 = _32129], theory(equality)).
% 10.41/10.76 cnf(11, plain, [-(root_occ(_32622, _32753)), root_occ(_32555, _32688), _32555 = _32622, _32688 = _32753], theory(equality)).
% 10.41/10.76 cnf(12, plain, [-(_35445 = _35500), occurrence_of(_35389, _35445), occurrence_of(_35389, _35500)], clausify(sos_02)).
% 10.41/10.76 cnf(13, plain, [legal(_37886), -(arboreal(_37886))], clausify(sos_08)).
% 10.41/10.76 cnf(14, plain, [precedes(_38446, _38496), -(legal(_38496))], clausify(sos_10)).
% 10.41/10.76 cnf(15, plain, [min_precedes(_40787, _40840, _40892), root(_40840, _40892)], clausify(sos_14)).
% 10.41/10.76 cnf(16, plain, [min_precedes(_41227, _41278, _41328), -(precedes(_41227, _41278))], clausify(sos_15)).
% 10.41/10.76 cnf(17, plain, [root(_41645, _41689), -(legal(_41645))], clausify(sos_16)).
% 10.41/10.76 cnf(18, plain, [leaf(_44275, _44346), min_precedes(_44275, _44708, _44346)], clausify(sos_21)).
% 10.41/10.76 cnf(19, plain, [next_subocc(_44983, _45056, _45128), -(min_precedes(_44983, _45056, _45128))], clausify(sos_22)).
% 10.41/10.76 cnf(20, plain, [-(_48647 = _48736), -(min_precedes(_48736, _48647, _48466)), -(min_precedes(_48647, _48736, _48466)), occurrence_of(_48557, _48466), arboreal(_48647), arboreal(_48736), subactivity_occurrence(_48647, _48557), subactivity_occurrence(_48736, _48557)], clausify(sos_28)).
% 10.41/10.76 cnf(21, plain, [-(subactivity_occurrence(_49541, _49742)), min_precedes(_49541, _49609, _49676), occurrence_of(_49742, _49676), subactivity_occurrence(_49609, _49742)], clausify(sos_29)).
% 10.41/10.76 cnf(22, plain, [root_occ(_52414, _52476), -(occurrence_of(_52476, 14 ^ [_52476, _52414]))], clausify(sos_33)).
% 10.41/10.76 cnf(23, plain, [root_occ(_52414, _52476), -(root(_52414, 14 ^ [_52476, _52414]))], clausify(sos_33)).
% 10.41/10.76 cnf(24, plain, [occurrence_of(_53522, tptp0), -(occurrence_of(16 ^ [_53522], tptp3))], clausify(sos_35)).
% 10.41/10.76 cnf(25, plain, [occurrence_of(_53522, tptp0), -(root_occ(16 ^ [_53522], _53522))], clausify(sos_35)).
% 10.41/10.76 cnf(26, plain, [occurrence_of(_53522, tptp0), -(next_subocc(16 ^ [_53522], 17 ^ [_53522], tptp0))], clausify(sos_35)).
% 10.41/10.76 cnf(27, plain, [occurrence_of(_53522, tptp0), -(next_subocc(17 ^ [_53522], 18 ^ [_53522], tptp0))], clausify(sos_35)).
% 10.41/10.76 cnf(28, plain, [occurrence_of(_53522, tptp0), -(leaf_occ(18 ^ [_53522], _53522))], clausify(sos_35)).
% 10.41/10.76 cnf(29, plain, [occurrence_of(_53522, tptp0), -(occurrence_of(18 ^ [_53522], tptp2)), -(occurrence_of(18 ^ [_53522], tptp1))], clausify(sos_35)).
% 10.41/10.76 cnf(30, plain, [leaf_occ(_52968, _53030), -(occurrence_of(_53030, 15 ^ [_53030, _52968]))], clausify(sos_34)).
% 10.41/10.76 cnf(31, plain, [leaf_occ(_52968, _53030), -(subactivity_occurrence(_52968, _53030))], clausify(sos_34)).
% 10.41/10.76 cnf(32, plain, [leaf_occ(_52968, _53030), -(leaf(_52968, 15 ^ [_53030, _52968]))], clausify(sos_34)).
% 10.41/10.76
% 10.41/10.76 cnf('1',plain,[occurrence_of(16 ^ [19 ^ []], tptp3), root_occ(16 ^ [19 ^ []], 19 ^ []), 20 ^ [18 ^ [19 ^ []], 16 ^ [19 ^ []]], min_precedes(16 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0), leaf_occ(18 ^ [19 ^ []], 19 ^ [])],start(4,bind([[_67866, _67871], [16 ^ [19 ^ []], 18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.1',plain,[-(occurrence_of(16 ^ [19 ^ []], tptp3)), occurrence_of(19 ^ [], tptp0)],extension(24,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.2',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ [])), root_occ(16 ^ [19 ^ []], 19 ^ []), 16 ^ [19 ^ []] = 16 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(11,bind([[_32555, _32622, _32688, _32753], [16 ^ [19 ^ []], 16 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.2.1',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ [])), root_occ(16 ^ [19 ^ []], 19 ^ []), 16 ^ [19 ^ []] = 16 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(11,bind([[_32555, _32622, _32688, _32753], [16 ^ [19 ^ []], 16 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.2.1.1',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ [])), root_occ(16 ^ [19 ^ []], 19 ^ []), 16 ^ [19 ^ []] = 16 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(11,bind([[_32555, _32622, _32688, _32753], [16 ^ [19 ^ []], 16 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.2.1.1.1',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ [])), root_occ(16 ^ [19 ^ []], 19 ^ []), 16 ^ [19 ^ []] = 16 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(11,bind([[_32555, _32622, _32688, _32753], [16 ^ [19 ^ []], 16 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.2.1.1.1.1',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ [])), root_occ(16 ^ [19 ^ []], 19 ^ []), 16 ^ [19 ^ []] = 16 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(11,bind([[_32555, _32622, _32688, _32753], [16 ^ [19 ^ []], 16 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.2.1.1.1.1.1',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ [])), occurrence_of(19 ^ [], tptp0)],extension(25,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.2.1.1.1.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.2.1.1.1.1.2',plain,[-(16 ^ [19 ^ []] = 16 ^ [19 ^ []])],extension(5,bind([[_23584], [16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.2.1.1.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.2.1.1.1.2',plain,[-(16 ^ [19 ^ []] = 16 ^ [19 ^ []])],extension(5,bind([[_23584], [16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.2.1.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.2.1.1.2',plain,[-(16 ^ [19 ^ []] = 16 ^ [19 ^ []])],extension(5,bind([[_23584], [16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.2.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.2.1.2',plain,[-(16 ^ [19 ^ []] = 16 ^ [19 ^ []])],extension(5,bind([[_23584], [16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.2.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.2.2',plain,[-(16 ^ [19 ^ []] = 16 ^ [19 ^ []])],extension(5,bind([[_23584], [16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.2.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.3',plain,[-(20 ^ [18 ^ [19 ^ []], 16 ^ [19 ^ []]]), occurrence_of(18 ^ [19 ^ []], tptp1)],extension(1,bind([[_67866, _67871], [16 ^ [19 ^ []], 18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.3.1',plain,[-(occurrence_of(18 ^ [19 ^ []], tptp1)), occurrence_of(19 ^ [], tptp0), -(occurrence_of(18 ^ [19 ^ []], tptp2))],extension(29,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.3.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.3.1.2',plain,[occurrence_of(18 ^ [19 ^ []], tptp2), -(20 ^ [18 ^ [19 ^ []], 16 ^ [19 ^ []]])],extension(2,bind([[_67871, _67866], [18 ^ [19 ^ []], 16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.3.1.2.1',plain,[20 ^ [18 ^ [19 ^ []], 16 ^ [19 ^ []]]],reduction('1')).
% 10.41/10.76 cnf('1.4',plain,[-(min_precedes(16 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)), -(18 ^ [19 ^ []] = 16 ^ [19 ^ []]), -(min_precedes(18 ^ [19 ^ []], 16 ^ [19 ^ []], tptp0)), occurrence_of(19 ^ [], tptp0), arboreal(18 ^ [19 ^ []]), arboreal(16 ^ [19 ^ []]), subactivity_occurrence(18 ^ [19 ^ []], 19 ^ []), subactivity_occurrence(16 ^ [19 ^ []], 19 ^ [])],extension(20,bind([[_48466, _48647, _48736, _48557], [tptp0, 18 ^ [19 ^ []], 16 ^ [19 ^ []], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.1',plain,[18 ^ [19 ^ []] = 16 ^ [19 ^ []], -(16 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(6,bind([[_23782, _23737], [16 ^ [19 ^ []], 18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.1.1',plain,[16 ^ [19 ^ []] = 18 ^ [19 ^ []], -(root(18 ^ [19 ^ []], tptp0)), root(16 ^ [19 ^ []], 14 ^ [19 ^ [], 16 ^ [19 ^ []]]), 14 ^ [19 ^ [], 16 ^ [19 ^ []]] = tptp0],extension(10,bind([[_31998, _31931, _32064, _32129], [18 ^ [19 ^ []], 16 ^ [19 ^ []], 14 ^ [19 ^ [], 16 ^ [19 ^ []]], tptp0]]))).
% 10.41/10.76 cnf('1.4.1.1.1',plain,[root(18 ^ [19 ^ []], tptp0), min_precedes(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)],extension(15,bind([[_40787, _40840, _40892], [17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0]]))).
% 10.41/10.76 cnf('1.4.1.1.1.1',plain,[-(min_precedes(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)), next_subocc(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)],extension(19,bind([[_44983, _45056, _45128], [17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0]]))).
% 10.41/10.76 cnf('1.4.1.1.1.1.1',plain,[-(next_subocc(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)), occurrence_of(19 ^ [], tptp0)],extension(27,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.1.1.1.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.1.1.2',plain,[-(root(16 ^ [19 ^ []], 14 ^ [19 ^ [], 16 ^ [19 ^ []]])), root_occ(16 ^ [19 ^ []], 19 ^ [])],extension(23,bind([[_52414, _52476], [16 ^ [19 ^ []], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.1.1.2.1',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ [])), root_occ(16 ^ [19 ^ []], 19 ^ []), 16 ^ [19 ^ []] = 16 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(11,bind([[_32555, _32622, _32688, _32753], [16 ^ [19 ^ []], 16 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.1.1.2.1.1',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ [])), occurrence_of(19 ^ [], tptp0)],extension(25,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.1.1.2.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.1.1.2.1.2',plain,[-(16 ^ [19 ^ []] = 16 ^ [19 ^ []])],extension(5,bind([[_23584], [16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.1.1.2.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.1.1.3',plain,[-(14 ^ [19 ^ [], 16 ^ [19 ^ []]] = tptp0), tptp0 = 14 ^ [19 ^ [], 16 ^ [19 ^ []]]],extension(6,bind([[_23737, _23782], [tptp0, 14 ^ [19 ^ [], 16 ^ [19 ^ []]]]]))).
% 10.41/10.76 cnf('1.4.1.1.3.1',plain,[-(tptp0 = 14 ^ [19 ^ [], 16 ^ [19 ^ []]]), occurrence_of(19 ^ [], tptp0), occurrence_of(19 ^ [], 14 ^ [19 ^ [], 16 ^ [19 ^ []]])],extension(12,bind([[_35445, _35389, _35500], [tptp0, 19 ^ [], 14 ^ [19 ^ [], 16 ^ [19 ^ []]]]]))).
% 10.41/10.76 cnf('1.4.1.1.3.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.1.1.3.1.2',plain,[-(occurrence_of(19 ^ [], 14 ^ [19 ^ [], 16 ^ [19 ^ []]])), root_occ(16 ^ [19 ^ []], 19 ^ [])],extension(22,bind([[_52414, _52476], [16 ^ [19 ^ []], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.1.1.3.1.2.1',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ []))],lemmata('1')).
% 10.41/10.76 cnf('1.4.2',plain,[min_precedes(18 ^ [19 ^ []], 16 ^ [19 ^ []], tptp0), leaf(18 ^ [19 ^ []], tptp0)],extension(18,bind([[_44708, _44275, _44346], [16 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0]]))).
% 10.41/10.76 cnf('1.4.2.1',plain,[-(leaf(18 ^ [19 ^ []], tptp0)), leaf(18 ^ [19 ^ []], 15 ^ [19 ^ [], 18 ^ [19 ^ []]]), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 15 ^ [19 ^ [], 18 ^ [19 ^ []]] = tptp0],extension(7,bind([[_27056, _27123, _27189, _27254], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 15 ^ [19 ^ [], 18 ^ [19 ^ []]], tptp0]]))).
% 10.41/10.76 cnf('1.4.2.1.1',plain,[-(leaf(18 ^ [19 ^ []], 15 ^ [19 ^ [], 18 ^ [19 ^ []]])), leaf(18 ^ [19 ^ []], 15 ^ [19 ^ [], 18 ^ [19 ^ []]]), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 15 ^ [19 ^ [], 18 ^ [19 ^ []]] = 15 ^ [19 ^ [], 18 ^ [19 ^ []]]],extension(7,bind([[_27056, _27123, _27189, _27254], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 15 ^ [19 ^ [], 18 ^ [19 ^ []]], 15 ^ [19 ^ [], 18 ^ [19 ^ []]]]]))).
% 10.41/10.76 cnf('1.4.2.1.1.1',plain,[-(leaf(18 ^ [19 ^ []], 15 ^ [19 ^ [], 18 ^ [19 ^ []]])), leaf_occ(18 ^ [19 ^ []], 19 ^ [])],extension(32,bind([[_52968, _53030], [18 ^ [19 ^ []], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.2.1.1.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), occurrence_of(19 ^ [], tptp0)],extension(28,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.2.1.1.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.2.1.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23584], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.2.1.1.3',plain,[-(15 ^ [19 ^ [], 18 ^ [19 ^ []]] = 15 ^ [19 ^ [], 18 ^ [19 ^ []]])],extension(5,bind([[_23584], [15 ^ [19 ^ [], 18 ^ [19 ^ []]]]]))).
% 10.41/10.76 cnf('1.4.2.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23584], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.2.1.3',plain,[-(15 ^ [19 ^ [], 18 ^ [19 ^ []]] = tptp0), occurrence_of(19 ^ [], 15 ^ [19 ^ [], 18 ^ [19 ^ []]]), occurrence_of(19 ^ [], tptp0)],extension(12,bind([[_35445, _35389, _35500], [15 ^ [19 ^ [], 18 ^ [19 ^ []]], 19 ^ [], tptp0]]))).
% 10.41/10.76 cnf('1.4.2.1.3.1',plain,[-(occurrence_of(19 ^ [], 15 ^ [19 ^ [], 18 ^ [19 ^ []]])), leaf_occ(18 ^ [19 ^ []], 19 ^ [])],extension(30,bind([[_52968, _53030], [18 ^ [19 ^ []], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.2.1.3.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), occurrence_of(19 ^ [], tptp0)],extension(28,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.2.1.3.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.2.1.3.2',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.3',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.4',plain,[-(arboreal(18 ^ [19 ^ []])), legal(18 ^ [19 ^ []])],extension(13,bind([[_37886], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.4.1',plain,[-(legal(18 ^ [19 ^ []])), precedes(17 ^ [19 ^ []], 18 ^ [19 ^ []])],extension(14,bind([[_38446, _38496], [17 ^ [19 ^ []], 18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.4.1.1',plain,[-(precedes(17 ^ [19 ^ []], 18 ^ [19 ^ []])), min_precedes(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)],extension(16,bind([[_41227, _41278, _41328], [17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0]]))).
% 10.41/10.76 cnf('1.4.4.1.1.1',plain,[-(min_precedes(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)), next_subocc(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)],extension(19,bind([[_44983, _45056, _45128], [17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0]]))).
% 10.41/10.76 cnf('1.4.4.1.1.1.1',plain,[-(next_subocc(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)), occurrence_of(19 ^ [], tptp0)],extension(27,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.4.1.1.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.5',plain,[-(arboreal(16 ^ [19 ^ []])), legal(16 ^ [19 ^ []])],extension(13,bind([[_37886], [16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.5.1',plain,[-(legal(16 ^ [19 ^ []])), root(16 ^ [19 ^ []], 14 ^ [19 ^ [], 16 ^ [19 ^ []]])],extension(17,bind([[_41645, _41689], [16 ^ [19 ^ []], 14 ^ [19 ^ [], 16 ^ [19 ^ []]]]]))).
% 10.41/10.76 cnf('1.4.5.1.1',plain,[-(root(16 ^ [19 ^ []], 14 ^ [19 ^ [], 16 ^ [19 ^ []]])), root_occ(16 ^ [19 ^ []], 19 ^ [])],extension(23,bind([[_52414, _52476], [16 ^ [19 ^ []], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.5.1.1.1',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ [])), root_occ(16 ^ [19 ^ []], 19 ^ []), 16 ^ [19 ^ []] = 16 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(11,bind([[_32555, _32622, _32688, _32753], [16 ^ [19 ^ []], 16 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.5.1.1.1.1',plain,[-(root_occ(16 ^ [19 ^ []], 19 ^ [])), occurrence_of(19 ^ [], tptp0)],extension(25,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.5.1.1.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.5.1.1.1.2',plain,[-(16 ^ [19 ^ []] = 16 ^ [19 ^ []])],extension(5,bind([[_23584], [16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.5.1.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.6',plain,[-(subactivity_occurrence(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ [])],extension(31,bind([[_52968, _53030], [18 ^ [19 ^ []], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.6.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(8,bind([[_27680, _27747, _27813, _27878], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.6.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(8,bind([[_27680, _27747, _27813, _27878], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.6.1.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(8,bind([[_27680, _27747, _27813, _27878], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.6.1.1.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), occurrence_of(19 ^ [], tptp0)],extension(28,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.6.1.1.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.6.1.1.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23584], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.6.1.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.6.1.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23584], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.6.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.6.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23584], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.6.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.7',plain,[-(subactivity_occurrence(16 ^ [19 ^ []], 19 ^ [])), min_precedes(16 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0), occurrence_of(19 ^ [], tptp0), subactivity_occurrence(17 ^ [19 ^ []], 19 ^ [])],extension(21,bind([[_49541, _49676, _49609, _49742], [16 ^ [19 ^ []], tptp0, 17 ^ [19 ^ []], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.7.1',plain,[-(min_precedes(16 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0)), min_precedes(16 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0), 16 ^ [19 ^ []] = 16 ^ [19 ^ []], 17 ^ [19 ^ []] = 17 ^ [19 ^ []], tptp0 = tptp0],extension(9,bind([[_28633, _28718, _28802, _28885, _28967, _29048], [16 ^ [19 ^ []], 16 ^ [19 ^ []], 17 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0, tptp0]]))).
% 10.41/10.76 cnf('1.4.7.1.1',plain,[-(min_precedes(16 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0)), min_precedes(16 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0), 16 ^ [19 ^ []] = 16 ^ [19 ^ []], 17 ^ [19 ^ []] = 17 ^ [19 ^ []], tptp0 = tptp0],extension(9,bind([[_28633, _28718, _28802, _28885, _28967, _29048], [16 ^ [19 ^ []], 16 ^ [19 ^ []], 17 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0, tptp0]]))).
% 10.41/10.76 cnf('1.4.7.1.1.1',plain,[-(min_precedes(16 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0)), next_subocc(16 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0)],extension(19,bind([[_44983, _45056, _45128], [16 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0]]))).
% 10.41/10.76 cnf('1.4.7.1.1.1.1',plain,[-(next_subocc(16 ^ [19 ^ []], 17 ^ [19 ^ []], tptp0)), occurrence_of(19 ^ [], tptp0)],extension(26,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.7.1.1.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.7.1.1.2',plain,[-(16 ^ [19 ^ []] = 16 ^ [19 ^ []])],extension(5,bind([[_23584], [16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.7.1.1.3',plain,[-(17 ^ [19 ^ []] = 17 ^ [19 ^ []])],extension(5,bind([[_23584], [17 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.7.1.1.4',plain,[-(tptp0 = tptp0)],extension(5,bind([[_23584], [tptp0]]))).
% 10.41/10.76 cnf('1.4.7.1.2',plain,[-(16 ^ [19 ^ []] = 16 ^ [19 ^ []])],extension(5,bind([[_23584], [16 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.7.1.3',plain,[-(17 ^ [19 ^ []] = 17 ^ [19 ^ []])],extension(5,bind([[_23584], [17 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.4.7.1.4',plain,[-(tptp0 = tptp0)],extension(5,bind([[_23584], [tptp0]]))).
% 10.41/10.76 cnf('1.4.7.2',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.7.3',plain,[-(subactivity_occurrence(17 ^ [19 ^ []], 19 ^ [])), min_precedes(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0), occurrence_of(19 ^ [], tptp0), subactivity_occurrence(18 ^ [19 ^ []], 19 ^ [])],extension(21,bind([[_49541, _49676, _49609, _49742], [17 ^ [19 ^ []], tptp0, 18 ^ [19 ^ []], 19 ^ []]]))).
% 10.41/10.76 cnf('1.4.7.3.1',plain,[-(min_precedes(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)), next_subocc(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)],extension(19,bind([[_44983, _45056, _45128], [17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0]]))).
% 10.41/10.76 cnf('1.4.7.3.1.1',plain,[-(next_subocc(17 ^ [19 ^ []], 18 ^ [19 ^ []], tptp0)), occurrence_of(19 ^ [], tptp0)],extension(27,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.4.7.3.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.7.3.2',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.4.7.3.3',plain,[-(subactivity_occurrence(18 ^ [19 ^ []], 19 ^ []))],lemmata('1.4')).
% 10.41/10.76 cnf('1.5',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(8,bind([[_27680, _27747, _27813, _27878], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.5.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(8,bind([[_27680, _27747, _27813, _27878], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.5.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(8,bind([[_27680, _27747, _27813, _27878], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.5.1.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(8,bind([[_27680, _27747, _27813, _27878], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.5.1.1.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(8,bind([[_27680, _27747, _27813, _27878], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 10.41/10.76 cnf('1.5.1.1.1.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), occurrence_of(19 ^ [], tptp0)],extension(28,bind([[_53522], [19 ^ []]]))).
% 10.41/10.76 cnf('1.5.1.1.1.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 10.41/10.76 cnf('1.5.1.1.1.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23584], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.5.1.1.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.5.1.1.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23584], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.5.1.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.5.1.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23584], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.5.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.5.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23584], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.5.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 cnf('1.5.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23584], [18 ^ [19 ^ []]]]))).
% 10.41/10.76 cnf('1.5.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23584], [19 ^ []]]))).
% 10.41/10.76 %-----------------------------------------------------
% 10.41/10.77
% 10.41/10.77 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------