%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PRO012+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n028.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:02 EDT 2022
% Result : Theorem 0.37s 1.43s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : PRO012+2 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.35 % Computer : n028.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Mon Jun 13 03:26:07 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.37/1.43 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.43 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.44
% 0.37/1.44 %-----------------------------------------------------
% 0.37/1.44 fof(goals, conjecture, ! [_79630] : (occurrence_of(_79630, tptp0) => ? [_79648, _79651] : (occurrence_of(_79648, tptp3) & root_occ(_79648, _79630) & (occurrence_of(_79651, tptp2) | occurrence_of(_79651, tptp1)) & min_precedes(_79648, _79651, tptp0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 0.37/1.44 fof(sos, axiom, ! [_80011, _80014, _80017, _80020] : (min_precedes(_80011, _80014, _80020) & min_precedes(_80014, _80017, _80020) => min_precedes(_80011, _80017, _80020)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos)).
% 0.37/1.44 fof(sos_32, axiom, ! [_80302] : (occurrence_of(_80302, tptp0) => ? [_80320, _80323, _80326] : (occurrence_of(_80320, tptp3) & root_occ(_80320, _80302) & occurrence_of(_80323, tptp4) & min_precedes(_80320, _80323, tptp0) & (occurrence_of(_80326, tptp2) | occurrence_of(_80326, tptp1)) & min_precedes(_80323, _80326, tptp0) & ! [_80410] : (min_precedes(_80320, _80410, tptp0) => _80410 = _80323 | _80410 = _80326))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_32)).
% 0.37/1.44
% 0.37/1.44 cnf(1, plain, [-(19 ^ [_63688, _63683]), occurrence_of(_63688, tptp1)], clausify(goals)).
% 0.37/1.44 cnf(2, plain, [-(19 ^ [_63688, _63683]), occurrence_of(_63688, tptp2)], clausify(goals)).
% 0.37/1.44 cnf(3, plain, [-(occurrence_of(18 ^ [], tptp0))], clausify(goals)).
% 0.37/1.44 cnf(4, plain, [occurrence_of(_63683, tptp3), root_occ(_63683, 18 ^ []), 19 ^ [_63688, _63683], min_precedes(_63683, _63688, tptp0)], clausify(goals)).
% 0.37/1.44 cnf(5, plain, [-(_21792 = _21792)], theory(equality)).
% 0.37/1.44 cnf(6, plain, [-(min_precedes(_26926, _27093, _27256)), min_precedes(_26841, _27010, _27175), _26841 = _26926, _27010 = _27093, _27175 = _27256], theory(equality)).
% 0.37/1.44 cnf(7, plain, [-(root_occ(_30830, _30961)), root_occ(_30763, _30896), _30763 = _30830, _30896 = _30961], theory(equality)).
% 0.37/1.44 cnf(8, plain, [-(min_precedes(_32901, _33028, _33090)), min_precedes(_32901, _32965, _33090), min_precedes(_32965, _33028, _33090)], clausify(sos)).
% 0.37/1.44 cnf(9, plain, [occurrence_of(_49534, tptp0), -(occurrence_of(15 ^ [_49534], tptp3))], clausify(sos_32)).
% 0.37/1.44 cnf(10, plain, [occurrence_of(_49534, tptp0), -(root_occ(15 ^ [_49534], _49534))], clausify(sos_32)).
% 0.37/1.44 cnf(11, plain, [occurrence_of(_49534, tptp0), -(min_precedes(15 ^ [_49534], 16 ^ [_49534], tptp0))], clausify(sos_32)).
% 0.37/1.44 cnf(12, plain, [occurrence_of(_49534, tptp0), -(occurrence_of(17 ^ [_49534], tptp2)), -(occurrence_of(17 ^ [_49534], tptp1))], clausify(sos_32)).
% 0.37/1.44 cnf(13, plain, [occurrence_of(_49534, tptp0), -(min_precedes(16 ^ [_49534], 17 ^ [_49534], tptp0))], clausify(sos_32)).
% 0.37/1.44
% 0.37/1.44 cnf('1',plain,[occurrence_of(15 ^ [18 ^ []], tptp3), root_occ(15 ^ [18 ^ []], 18 ^ []), 19 ^ [17 ^ [18 ^ []], 15 ^ [18 ^ []]], min_precedes(15 ^ [18 ^ []], 17 ^ [18 ^ []], tptp0)],start(4,bind([[_63683, _63688], [15 ^ [18 ^ []], 17 ^ [18 ^ []]]]))).
% 0.37/1.44 cnf('1.1',plain,[-(occurrence_of(15 ^ [18 ^ []], tptp3)), occurrence_of(18 ^ [], tptp0)],extension(9,bind([[_49534], [18 ^ []]]))).
% 0.37/1.44 cnf('1.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.37/1.44 cnf('1.2',plain,[-(root_occ(15 ^ [18 ^ []], 18 ^ [])), root_occ(15 ^ [18 ^ []], 18 ^ []), 15 ^ [18 ^ []] = 15 ^ [18 ^ []], 18 ^ [] = 18 ^ []],extension(7,bind([[_30763, _30830, _30896, _30961], [15 ^ [18 ^ []], 15 ^ [18 ^ []], 18 ^ [], 18 ^ []]]))).
% 0.37/1.44 cnf('1.2.1',plain,[-(root_occ(15 ^ [18 ^ []], 18 ^ [])), root_occ(15 ^ [18 ^ []], 18 ^ []), 15 ^ [18 ^ []] = 15 ^ [18 ^ []], 18 ^ [] = 18 ^ []],extension(7,bind([[_30763, _30830, _30896, _30961], [15 ^ [18 ^ []], 15 ^ [18 ^ []], 18 ^ [], 18 ^ []]]))).
% 0.37/1.44 cnf('1.2.1.1',plain,[-(root_occ(15 ^ [18 ^ []], 18 ^ [])), occurrence_of(18 ^ [], tptp0)],extension(10,bind([[_49534], [18 ^ []]]))).
% 0.37/1.44 cnf('1.2.1.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.37/1.44 cnf('1.2.1.2',plain,[-(15 ^ [18 ^ []] = 15 ^ [18 ^ []])],extension(5,bind([[_21792], [15 ^ [18 ^ []]]]))).
% 0.37/1.44 cnf('1.2.1.3',plain,[-(18 ^ [] = 18 ^ [])],extension(5,bind([[_21792], [18 ^ []]]))).
% 0.37/1.44 cnf('1.2.2',plain,[-(15 ^ [18 ^ []] = 15 ^ [18 ^ []])],extension(5,bind([[_21792], [15 ^ [18 ^ []]]]))).
% 0.37/1.44 cnf('1.2.3',plain,[-(18 ^ [] = 18 ^ [])],extension(5,bind([[_21792], [18 ^ []]]))).
% 0.37/1.44 cnf('1.3',plain,[-(19 ^ [17 ^ [18 ^ []], 15 ^ [18 ^ []]]), occurrence_of(17 ^ [18 ^ []], tptp1)],extension(1,bind([[_63683, _63688], [15 ^ [18 ^ []], 17 ^ [18 ^ []]]]))).
% 0.37/1.44 cnf('1.3.1',plain,[-(occurrence_of(17 ^ [18 ^ []], tptp1)), occurrence_of(18 ^ [], tptp0), -(occurrence_of(17 ^ [18 ^ []], tptp2))],extension(12,bind([[_49534], [18 ^ []]]))).
% 0.37/1.44 cnf('1.3.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.37/1.44 cnf('1.3.1.2',plain,[occurrence_of(17 ^ [18 ^ []], tptp2), -(19 ^ [17 ^ [18 ^ []], 15 ^ [18 ^ []]])],extension(2,bind([[_63688, _63683], [17 ^ [18 ^ []], 15 ^ [18 ^ []]]]))).
% 0.37/1.44 cnf('1.3.1.2.1',plain,[19 ^ [17 ^ [18 ^ []], 15 ^ [18 ^ []]]],reduction('1')).
% 0.37/1.44 cnf('1.4',plain,[-(min_precedes(15 ^ [18 ^ []], 17 ^ [18 ^ []], tptp0)), min_precedes(15 ^ [18 ^ []], 16 ^ [18 ^ []], tptp0), min_precedes(16 ^ [18 ^ []], 17 ^ [18 ^ []], tptp0)],extension(8,bind([[_32901, _32965, _33028, _33090], [15 ^ [18 ^ []], 16 ^ [18 ^ []], 17 ^ [18 ^ []], tptp0]]))).
% 0.37/1.44 cnf('1.4.1',plain,[-(min_precedes(15 ^ [18 ^ []], 16 ^ [18 ^ []], tptp0)), min_precedes(15 ^ [18 ^ []], 16 ^ [18 ^ []], tptp0), 15 ^ [18 ^ []] = 15 ^ [18 ^ []], 16 ^ [18 ^ []] = 16 ^ [18 ^ []], tptp0 = tptp0],extension(6,bind([[_26841, _26926, _27010, _27093, _27175, _27256], [15 ^ [18 ^ []], 15 ^ [18 ^ []], 16 ^ [18 ^ []], 16 ^ [18 ^ []], tptp0, tptp0]]))).
% 0.37/1.44 cnf('1.4.1.1',plain,[-(min_precedes(15 ^ [18 ^ []], 16 ^ [18 ^ []], tptp0)), occurrence_of(18 ^ [], tptp0)],extension(11,bind([[_49534], [18 ^ []]]))).
% 0.37/1.44 cnf('1.4.1.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.37/1.44 cnf('1.4.1.2',plain,[-(15 ^ [18 ^ []] = 15 ^ [18 ^ []])],extension(5,bind([[_21792], [15 ^ [18 ^ []]]]))).
% 0.37/1.44 cnf('1.4.1.3',plain,[-(16 ^ [18 ^ []] = 16 ^ [18 ^ []])],extension(5,bind([[_21792], [16 ^ [18 ^ []]]]))).
% 0.37/1.44 cnf('1.4.1.4',plain,[-(tptp0 = tptp0)],extension(5,bind([[_21792], [tptp0]]))).
% 0.37/1.44 cnf('1.4.2',plain,[-(min_precedes(16 ^ [18 ^ []], 17 ^ [18 ^ []], tptp0)), occurrence_of(18 ^ [], tptp0)],extension(13,bind([[_49534], [18 ^ []]]))).
% 0.37/1.44 cnf('1.4.2.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.37/1.44 %-----------------------------------------------------
% 0.37/1.45
% 0.37/1.45 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------