%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PRO011+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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:01 EDT 2022
% Result : Theorem 0.36s 1.40s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PRO011+2 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n027.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:22:16 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.36/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.42
% 0.36/1.42 %-----------------------------------------------------
% 0.36/1.42 fof(goals, conjecture, ! [_78744] : (occurrence_of(_78744, tptp0) => ? [_78762, _78765] : (leaf_occ(_78765, _78744) & (occurrence_of(_78765, tptp1) => ~ ? [_78795] : (occurrence_of(_78795, tptp2) & subactivity_occurrence(_78795, _78744) & min_precedes(_78762, _78795, tptp0))) & (occurrence_of(_78765, tptp2) => ~ ? [_78848] : (occurrence_of(_78848, tptp1) & subactivity_occurrence(_78848, _78744) & min_precedes(_78762, _78848, tptp0))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 0.36/1.42 fof(sos_21, axiom, ! [_79355, _79358, _79361] : (occurrence_of(_79355, _79361) & leaf_occ(_79358, _79355) => ~ ? [_79391] : min_precedes(_79358, _79391, _79361)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_21)).
% 0.36/1.42 fof(sos_32, axiom, ! [_79621] : (occurrence_of(_79621, tptp0) => ? [_79639, _79642, _79645] : (occurrence_of(_79639, tptp3) & root_occ(_79639, _79621) & occurrence_of(_79642, tptp4) & next_subocc(_79639, _79642, tptp0) & (occurrence_of(_79645, tptp1) | occurrence_of(_79645, tptp2)) & next_subocc(_79642, _79645, tptp0) & leaf_occ(_79645, _79621))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_32)).
% 0.36/1.42
% 0.36/1.42 cnf(1, plain, [-(22 ^ [_64299, _64294]), -(min_precedes(_64294, 21 ^ [_64299, _64294], tptp0))], clausify(goals)).
% 0.36/1.42 cnf(2, plain, [-(20 ^ [_64299, _64294]), -(min_precedes(_64294, 19 ^ [_64299, _64294], tptp0))], clausify(goals)).
% 0.36/1.42 cnf(3, plain, [-(occurrence_of(18 ^ [], tptp0))], clausify(goals)).
% 0.36/1.42 cnf(4, plain, [leaf_occ(_64299, 18 ^ []), 20 ^ [_64299, _64294], 22 ^ [_64299, _64294]], clausify(goals)).
% 0.36/1.42 cnf(5, plain, [-(_22239 = _22239)], theory(equality)).
% 0.36/1.42 cnf(6, plain, [-(leaf_occ(_26402, _26533)), leaf_occ(_26335, _26468), _26335 = _26402, _26468 = _26533], theory(equality)).
% 0.36/1.42 cnf(7, plain, [min_precedes(_43662, _43929, _43725), occurrence_of(_43598, _43725), leaf_occ(_43662, _43598)], clausify(sos_21)).
% 0.36/1.42 cnf(8, plain, [occurrence_of(_49981, tptp0), -(leaf_occ(17 ^ [_49981], _49981))], clausify(sos_32)).
% 0.36/1.42
% 0.36/1.42 cnf('1',plain,[leaf_occ(17 ^ [18 ^ []], 18 ^ []), 20 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], 22 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]]],start(4,bind([[_64299, _64294], [17 ^ [18 ^ []], 17 ^ [18 ^ []]]]))).
% 0.36/1.42 cnf('1.1',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), leaf_occ(17 ^ [18 ^ []], 18 ^ []), 17 ^ [18 ^ []] = 17 ^ [18 ^ []], 18 ^ [] = 18 ^ []],extension(6,bind([[_26335, _26402, _26468, _26533], [17 ^ [18 ^ []], 17 ^ [18 ^ []], 18 ^ [], 18 ^ []]]))).
% 0.36/1.42 cnf('1.1.1',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), leaf_occ(17 ^ [18 ^ []], 18 ^ []), 17 ^ [18 ^ []] = 17 ^ [18 ^ []], 18 ^ [] = 18 ^ []],extension(6,bind([[_26335, _26402, _26468, _26533], [17 ^ [18 ^ []], 17 ^ [18 ^ []], 18 ^ [], 18 ^ []]]))).
% 0.36/1.42 cnf('1.1.1.1',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), occurrence_of(18 ^ [], tptp0)],extension(8,bind([[_49981], [18 ^ []]]))).
% 0.36/1.42 cnf('1.1.1.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.36/1.42 cnf('1.1.1.2',plain,[-(17 ^ [18 ^ []] = 17 ^ [18 ^ []])],extension(5,bind([[_22239], [17 ^ [18 ^ []]]]))).
% 0.36/1.42 cnf('1.1.1.3',plain,[-(18 ^ [] = 18 ^ [])],extension(5,bind([[_22239], [18 ^ []]]))).
% 0.36/1.42 cnf('1.1.2',plain,[-(17 ^ [18 ^ []] = 17 ^ [18 ^ []])],extension(5,bind([[_22239], [17 ^ [18 ^ []]]]))).
% 0.36/1.42 cnf('1.1.3',plain,[-(18 ^ [] = 18 ^ [])],extension(5,bind([[_22239], [18 ^ []]]))).
% 0.36/1.42 cnf('1.2',plain,[-(20 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]]), -(min_precedes(17 ^ [18 ^ []], 19 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], tptp0))],extension(2,bind([[_64299, _64294], [17 ^ [18 ^ []], 17 ^ [18 ^ []]]]))).
% 0.36/1.42 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([[_43929, _43725, _43662, _43598], [19 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], tptp0, 17 ^ [18 ^ []], 18 ^ []]]))).
% 0.36/1.42 cnf('1.2.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.36/1.42 cnf('1.2.1.2',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), occurrence_of(18 ^ [], tptp0)],extension(8,bind([[_49981], [18 ^ []]]))).
% 0.36/1.42 cnf('1.2.1.2.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.36/1.42 cnf('1.3',plain,[-(22 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]]), -(min_precedes(17 ^ [18 ^ []], 21 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], tptp0))],extension(1,bind([[_64299, _64294], [17 ^ [18 ^ []], 17 ^ [18 ^ []]]]))).
% 0.36/1.42 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([[_43929, _43725, _43662, _43598], [21 ^ [17 ^ [18 ^ []], 17 ^ [18 ^ []]], tptp0, 17 ^ [18 ^ []], 18 ^ []]]))).
% 0.36/1.42 cnf('1.3.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.36/1.42 cnf('1.3.1.2',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ []))],lemmata('1')).
% 0.36/1.42 %-----------------------------------------------------
% 0.36/1.42
% 0.36/1.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------