%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PRO010+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n005.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.44s 1.40s
% Output : Proof 0.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : PRO010+3 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n005.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 : 600
% 0.12/0.33 % DateTime : Mon Jun 13 02:56:24 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.44/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/1.42
% 0.44/1.42 %-----------------------------------------------------
% 0.44/1.42 fof(goals, conjecture, ! [_106386] : (occurrence_of(_106386, tptp0) => ? [_106404, _106407] : (leaf_occ(_106407, _106386) & (occurrence_of(_106407, tptp1) => ~ ? [_106437] : (occurrence_of(_106437, tptp2) & min_precedes(_106404, _106437, tptp0))) & (occurrence_of(_106407, tptp2) => ~ ? [_106480] : (occurrence_of(_106480, tptp1) & min_precedes(_106404, _106480, tptp0))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 0.44/1.42 fof(sos_37, axiom, ! [_106965, _106968, _106971] : (occurrence_of(_106965, _106971) & leaf_occ(_106968, _106965) => ~ ? [_107001] : min_precedes(_106968, _107001, _106971)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_37)).
% 0.44/1.42 fof(sos_49, axiom, ! [_107223] : (occurrence_of(_107223, tptp0) => ? [_107241, _107244, _107247] : (occurrence_of(_107241, tptp3) & root_occ(_107241, _107223) & occurrence_of(_107244, tptp4) & next_subocc(_107241, _107244, tptp0) & (occurrence_of(_107247, tptp1) | occurrence_of(_107247, tptp2)) & next_subocc(_107244, _107247, tptp0) & leaf_occ(_107247, _107223))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_49)).
% 0.44/1.42
% 0.44/1.42 cnf(1, plain, [-(24 ^ [_89762, _89757]), -(min_precedes(_89757, 23 ^ [_89762, _89757], tptp0))], clausify(goals)).
% 0.44/1.42 cnf(2, plain, [-(22 ^ [_89762, _89757]), -(min_precedes(_89757, 21 ^ [_89762, _89757], tptp0))], clausify(goals)).
% 0.44/1.42 cnf(3, plain, [-(occurrence_of(20 ^ [], tptp0))], clausify(goals)).
% 0.44/1.42 cnf(4, plain, [leaf_occ(_89762, 20 ^ []), 22 ^ [_89762, _89757], 24 ^ [_89762, _89757]], clausify(goals)).
% 0.44/1.42 cnf(5, plain, [-(_32288 = _32288)], theory(equality)).
% 0.44/1.42 cnf(6, plain, [-(leaf_occ(_36451, _36582)), leaf_occ(_36384, _36517), _36384 = _36451, _36517 = _36582], theory(equality)).
% 0.44/1.42 cnf(7, plain, [min_precedes(_63677, _63944, _63740), occurrence_of(_63613, _63740), leaf_occ(_63677, _63613)], clausify(sos_37)).
% 0.44/1.42 cnf(8, plain, [occurrence_of(_72806, tptp0), -(leaf_occ(19 ^ [_72806], _72806))], clausify(sos_49)).
% 0.44/1.42
% 0.44/1.42 cnf('1',plain,[leaf_occ(19 ^ [20 ^ []], 20 ^ []), 22 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], 24 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]]],start(4,bind([[_89762, _89757], [19 ^ [20 ^ []], 19 ^ [20 ^ []]]]))).
% 0.44/1.42 cnf('1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(6,bind([[_36384, _36451, _36517, _36582], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 0.44/1.42 cnf('1.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(6,bind([[_36384, _36451, _36517, _36582], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 0.44/1.42 cnf('1.1.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(8,bind([[_72806], [20 ^ []]]))).
% 0.44/1.42 cnf('1.1.1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 0.44/1.42 cnf('1.1.1.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32288], [19 ^ [20 ^ []]]]))).
% 0.44/1.42 cnf('1.1.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32288], [20 ^ []]]))).
% 0.44/1.42 cnf('1.1.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32288], [19 ^ [20 ^ []]]]))).
% 0.44/1.42 cnf('1.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32288], [20 ^ []]]))).
% 0.44/1.42 cnf('1.2',plain,[-(22 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]]), -(min_precedes(19 ^ [20 ^ []], 21 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], tptp0))],extension(2,bind([[_89762, _89757], [19 ^ [20 ^ []], 19 ^ [20 ^ []]]]))).
% 0.44/1.42 cnf('1.2.1',plain,[min_precedes(19 ^ [20 ^ []], 21 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], tptp0), occurrence_of(20 ^ [], tptp0), leaf_occ(19 ^ [20 ^ []], 20 ^ [])],extension(7,bind([[_63944, _63740, _63677, _63613], [21 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], tptp0, 19 ^ [20 ^ []], 20 ^ []]]))).
% 0.44/1.42 cnf('1.2.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 0.44/1.42 cnf('1.2.1.2',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(8,bind([[_72806], [20 ^ []]]))).
% 0.44/1.42 cnf('1.2.1.2.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 0.44/1.42 cnf('1.3',plain,[-(24 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]]), -(min_precedes(19 ^ [20 ^ []], 23 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], tptp0))],extension(1,bind([[_89762, _89757], [19 ^ [20 ^ []], 19 ^ [20 ^ []]]]))).
% 0.44/1.42 cnf('1.3.1',plain,[min_precedes(19 ^ [20 ^ []], 23 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], tptp0), occurrence_of(20 ^ [], tptp0), leaf_occ(19 ^ [20 ^ []], 20 ^ [])],extension(7,bind([[_63944, _63740, _63677, _63613], [23 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], tptp0, 19 ^ [20 ^ []], 20 ^ []]]))).
% 0.44/1.42 cnf('1.3.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 0.44/1.42 cnf('1.3.1.2',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ []))],lemmata('1')).
% 0.44/1.42 %-----------------------------------------------------
% 0.44/1.42
% 0.44/1.43 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------