%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PRO011+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n022.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.43s 1.44s
% Output : Proof 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : PRO011+3 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.14 % Command : leancop_casc.sh %s %d
% 0.14/0.36 % Computer : n022.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Mon Jun 13 02:14:03 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.43/1.44 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.43/1.45 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.43/1.45
% 0.43/1.45 %-----------------------------------------------------
% 0.43/1.45 fof(goals, conjecture, ! [_106952] : (occurrence_of(_106952, tptp0) => ? [_106970, _106973] : (leaf_occ(_106973, _106952) & (occurrence_of(_106973, tptp1) => ~ ? [_107003] : (occurrence_of(_107003, tptp2) & subactivity_occurrence(_107003, _106952) & min_precedes(_106970, _107003, tptp0))) & (occurrence_of(_106973, tptp2) => ~ ? [_107056] : (occurrence_of(_107056, tptp1) & subactivity_occurrence(_107056, _106952) & min_precedes(_106970, _107056, tptp0))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 0.43/1.45 fof(sos_37, axiom, ! [_107589, _107592, _107595] : (occurrence_of(_107589, _107595) & leaf_occ(_107592, _107589) => ~ ? [_107625] : min_precedes(_107592, _107625, _107595)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_37)).
% 0.43/1.45 fof(sos_49, axiom, ! [_107847] : (occurrence_of(_107847, tptp0) => ? [_107865, _107868, _107871] : (occurrence_of(_107865, tptp3) & root_occ(_107865, _107847) & occurrence_of(_107868, tptp4) & next_subocc(_107865, _107868, tptp0) & (occurrence_of(_107871, tptp1) | occurrence_of(_107871, tptp2)) & next_subocc(_107868, _107871, tptp0) & leaf_occ(_107871, _107847))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_49)).
% 0.43/1.45
% 0.43/1.45 cnf(1, plain, [-(24 ^ [_90120, _90115]), -(min_precedes(_90115, 23 ^ [_90120, _90115], tptp0))], clausify(goals)).
% 0.43/1.45 cnf(2, plain, [-(22 ^ [_90120, _90115]), -(min_precedes(_90115, 21 ^ [_90120, _90115], tptp0))], clausify(goals)).
% 0.43/1.45 cnf(3, plain, [-(occurrence_of(20 ^ [], tptp0))], clausify(goals)).
% 0.43/1.45 cnf(4, plain, [leaf_occ(_90120, 20 ^ []), 22 ^ [_90120, _90115], 24 ^ [_90120, _90115]], clausify(goals)).
% 0.43/1.45 cnf(5, plain, [-(_32450 = _32450)], theory(equality)).
% 0.43/1.45 cnf(6, plain, [-(leaf_occ(_36613, _36744)), leaf_occ(_36546, _36679), _36546 = _36613, _36679 = _36744], theory(equality)).
% 0.43/1.45 cnf(7, plain, [min_precedes(_63839, _64106, _63902), occurrence_of(_63775, _63902), leaf_occ(_63839, _63775)], clausify(sos_37)).
% 0.43/1.45 cnf(8, plain, [occurrence_of(_72968, tptp0), -(leaf_occ(19 ^ [_72968], _72968))], clausify(sos_49)).
% 0.43/1.45
% 0.43/1.45 cnf('1',plain,[leaf_occ(19 ^ [20 ^ []], 20 ^ []), 22 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], 24 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]]],start(4,bind([[_90120, _90115], [19 ^ [20 ^ []], 19 ^ [20 ^ []]]]))).
% 0.43/1.45 cnf('1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(6,bind([[_36546, _36613, _36679, _36744], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 0.43/1.45 cnf('1.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), leaf_occ(19 ^ [20 ^ []], 20 ^ []), 19 ^ [20 ^ []] = 19 ^ [20 ^ []], 20 ^ [] = 20 ^ []],extension(6,bind([[_36546, _36613, _36679, _36744], [19 ^ [20 ^ []], 19 ^ [20 ^ []], 20 ^ [], 20 ^ []]]))).
% 0.43/1.45 cnf('1.1.1.1',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(8,bind([[_72968], [20 ^ []]]))).
% 0.43/1.45 cnf('1.1.1.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 0.43/1.45 cnf('1.1.1.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32450], [19 ^ [20 ^ []]]]))).
% 0.43/1.45 cnf('1.1.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32450], [20 ^ []]]))).
% 0.43/1.45 cnf('1.1.2',plain,[-(19 ^ [20 ^ []] = 19 ^ [20 ^ []])],extension(5,bind([[_32450], [19 ^ [20 ^ []]]]))).
% 0.43/1.45 cnf('1.1.3',plain,[-(20 ^ [] = 20 ^ [])],extension(5,bind([[_32450], [20 ^ []]]))).
% 0.43/1.45 cnf('1.2',plain,[-(22 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]]), -(min_precedes(19 ^ [20 ^ []], 21 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], tptp0))],extension(2,bind([[_90120, _90115], [19 ^ [20 ^ []], 19 ^ [20 ^ []]]]))).
% 0.43/1.45 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([[_64106, _63902, _63839, _63775], [21 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], tptp0, 19 ^ [20 ^ []], 20 ^ []]]))).
% 0.43/1.45 cnf('1.2.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 0.43/1.45 cnf('1.2.1.2',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ [])), occurrence_of(20 ^ [], tptp0)],extension(8,bind([[_72968], [20 ^ []]]))).
% 0.43/1.45 cnf('1.2.1.2.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 0.43/1.45 cnf('1.3',plain,[-(24 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]]), -(min_precedes(19 ^ [20 ^ []], 23 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], tptp0))],extension(1,bind([[_90120, _90115], [19 ^ [20 ^ []], 19 ^ [20 ^ []]]]))).
% 0.43/1.45 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([[_64106, _63902, _63839, _63775], [23 ^ [19 ^ [20 ^ []], 19 ^ [20 ^ []]], tptp0, 19 ^ [20 ^ []], 20 ^ []]]))).
% 0.43/1.45 cnf('1.3.1.1',plain,[-(occurrence_of(20 ^ [], tptp0))],extension(3)).
% 0.43/1.45 cnf('1.3.1.2',plain,[-(leaf_occ(19 ^ [20 ^ []], 20 ^ []))],lemmata('1')).
% 0.43/1.45 %-----------------------------------------------------
% 0.53/1.46
% 0.53/1.46 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------