%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PRO010+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n021.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 0.31s 1.40s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : PRO010+2 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.33 % Computer : n021.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 : 600
% 0.11/0.33 % DateTime : Mon Jun 13 02:23:11 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.31/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/1.41
% 0.31/1.41 %-----------------------------------------------------
% 0.31/1.41 fof(goals, conjecture, ! [_78122] : (occurrence_of(_78122, tptp0) => ? [_78140, _78143] : (leaf_occ(_78143, _78122) & (occurrence_of(_78143, tptp1) => ~ ? [_78173] : (occurrence_of(_78173, tptp2) & min_precedes(_78140, _78173, tptp0))) & (occurrence_of(_78143, tptp2) => ~ ? [_78216] : (occurrence_of(_78216, tptp1) & min_precedes(_78140, _78216, tptp0))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 0.31/1.41 fof(sos_21, axiom, ! [_78675, _78678, _78681] : (occurrence_of(_78675, _78681) & leaf_occ(_78678, _78675) => ~ ? [_78711] : min_precedes(_78678, _78711, _78681)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_21)).
% 0.31/1.41 fof(sos_32, axiom, ! [_78941] : (occurrence_of(_78941, tptp0) => ? [_78959, _78962, _78965] : (occurrence_of(_78959, tptp3) & root_occ(_78959, _78941) & occurrence_of(_78962, tptp4) & next_subocc(_78959, _78962, tptp0) & (occurrence_of(_78965, tptp1) | occurrence_of(_78965, tptp2)) & next_subocc(_78962, _78965, tptp0) & leaf_occ(_78965, _78941))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_32)).
% 0.31/1.41
% 0.31/1.41 cnf(1, plain, [-(22 ^ [_63885, _63880]), -(min_precedes(_63880, 21 ^ [_63885, _63880], tptp0))], clausify(goals)).
% 0.31/1.41 cnf(2, plain, [-(20 ^ [_63885, _63880]), -(min_precedes(_63880, 19 ^ [_63885, _63880], tptp0))], clausify(goals)).
% 0.31/1.41 cnf(3, plain, [-(occurrence_of(18 ^ [], tptp0))], clausify(goals)).
% 0.31/1.41 cnf(4, plain, [leaf_occ(_63885, 18 ^ []), 20 ^ [_63885, _63880], 22 ^ [_63885, _63880]], clausify(goals)).
% 0.31/1.41 cnf(5, plain, [-(_22021 = _22021)], theory(equality)).
% 0.31/1.41 cnf(6, plain, [-(leaf_occ(_26184, _26315)), leaf_occ(_26117, _26250), _26117 = _26184, _26250 = _26315], theory(equality)).
% 0.31/1.41 cnf(7, plain, [min_precedes(_43444, _43711, _43507), occurrence_of(_43380, _43507), leaf_occ(_43444, _43380)], clausify(sos_21)).
% 0.31/1.41 cnf(8, plain, [occurrence_of(_49763, tptp0), -(leaf_occ(17 ^ [_49763], _49763))], clausify(sos_32)).
% 0.31/1.41
% 0.31/1.41 cnf('1',plain,[leaf_occ(17 ^ [18 ^ []], 18 ^ []), 20 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], 22 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]]],start(4,bind([[_63885, _63880], [17 ^ [18 ^ []], 17 ^ [18 ^ []]]]))).
% 0.31/1.41 cnf('1.1',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), leaf_occ(17 ^ [18 ^ []], 18 ^ []), 17 ^ [18 ^ []] = 17 ^ [18 ^ []], 18 ^ [] = 18 ^ []],extension(6,bind([[_26117, _26184, _26250, _26315], [17 ^ [18 ^ []], 17 ^ [18 ^ []], 18 ^ [], 18 ^ []]]))).
% 0.31/1.41 cnf('1.1.1',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), leaf_occ(17 ^ [18 ^ []], 18 ^ []), 17 ^ [18 ^ []] = 17 ^ [18 ^ []], 18 ^ [] = 18 ^ []],extension(6,bind([[_26117, _26184, _26250, _26315], [17 ^ [18 ^ []], 17 ^ [18 ^ []], 18 ^ [], 18 ^ []]]))).
% 0.31/1.41 cnf('1.1.1.1',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), occurrence_of(18 ^ [], tptp0)],extension(8,bind([[_49763], [18 ^ []]]))).
% 0.31/1.41 cnf('1.1.1.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.31/1.41 cnf('1.1.1.2',plain,[-(17 ^ [18 ^ []] = 17 ^ [18 ^ []])],extension(5,bind([[_22021], [17 ^ [18 ^ []]]]))).
% 0.31/1.41 cnf('1.1.1.3',plain,[-(18 ^ [] = 18 ^ [])],extension(5,bind([[_22021], [18 ^ []]]))).
% 0.31/1.41 cnf('1.1.2',plain,[-(17 ^ [18 ^ []] = 17 ^ [18 ^ []])],extension(5,bind([[_22021], [17 ^ [18 ^ []]]]))).
% 0.31/1.41 cnf('1.1.3',plain,[-(18 ^ [] = 18 ^ [])],extension(5,bind([[_22021], [18 ^ []]]))).
% 0.31/1.41 cnf('1.2',plain,[-(20 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]]), -(min_precedes(17 ^ [18 ^ []], 19 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], tptp0))],extension(2,bind([[_63885, _63880], [17 ^ [18 ^ []], 17 ^ [18 ^ []]]]))).
% 0.31/1.41 cnf('1.2.1',plain,[min_precedes(17 ^ [18 ^ []], 19 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], tptp0), occurrence_of(18 ^ [], tptp0), leaf_occ(17 ^ [18 ^ []], 18 ^ [])],extension(7,bind([[_43711, _43507, _43444, _43380], [19 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], tptp0, 17 ^ [18 ^ []], 18 ^ []]]))).
% 0.31/1.41 cnf('1.2.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.31/1.41 cnf('1.2.1.2',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), occurrence_of(18 ^ [], tptp0)],extension(8,bind([[_49763], [18 ^ []]]))).
% 0.31/1.41 cnf('1.2.1.2.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.31/1.41 cnf('1.3',plain,[-(22 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]]), -(min_precedes(17 ^ [18 ^ []], 21 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], tptp0))],extension(1,bind([[_63885, _63880], [17 ^ [18 ^ []], 17 ^ [18 ^ []]]]))).
% 0.31/1.41 cnf('1.3.1',plain,[min_precedes(17 ^ [18 ^ []], 21 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], tptp0), occurrence_of(18 ^ [], tptp0), leaf_occ(17 ^ [18 ^ []], 18 ^ [])],extension(7,bind([[_43711, _43507, _43444, _43380], [21 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], tptp0, 17 ^ [18 ^ []], 18 ^ []]]))).
% 0.31/1.41 cnf('1.3.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.31/1.41 cnf('1.3.1.2',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ []))],lemmata('1')).
% 0.31/1.41 %-----------------------------------------------------
% 0.31/1.42
% 0.31/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------