%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PRO010+4 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n017.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.35s 1.40s
% Output : Proof 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PRO010+4 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n017.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 00:50:52 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.35/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/1.41
% 0.43/1.41 %-----------------------------------------------------
% 0.43/1.41 fof(goals, conjecture, ! [_80546] : (occurrence_of(_80546, tptp0) => ? [_80564, _80567] : (leaf_occ(_80567, _80546) & (occurrence_of(_80567, tptp1) => ~ ? [_80597] : (occurrence_of(_80597, tptp2) & min_precedes(_80564, _80597, tptp0))) & (occurrence_of(_80567, tptp2) => ~ ? [_80640] : (occurrence_of(_80640, tptp1) & min_precedes(_80564, _80640, tptp0))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 0.43/1.41 fof(sos_09, axiom, ! [_81072, _81075, _81078] : (occurrence_of(_81072, _81078) & leaf_occ(_81075, _81072) => ~ ? [_81108] : min_precedes(_81075, _81108, _81078)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_09)).
% 0.43/1.41 fof(sos_32, axiom, ! [_81361] : (occurrence_of(_81361, tptp0) => ? [_81379, _81382, _81385] : (occurrence_of(_81379, tptp3) & root_occ(_81379, _81361) & occurrence_of(_81382, tptp4) & next_subocc(_81379, _81382, tptp0) & (occurrence_of(_81385, tptp1) | occurrence_of(_81385, tptp2)) & next_subocc(_81382, _81385, tptp0) & leaf_occ(_81385, _81361))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_32)).
% 0.43/1.41
% 0.43/1.41 cnf(1, plain, [-(20 ^ [_66165, _66160]), -(min_precedes(_66160, 19 ^ [_66165, _66160], tptp0))], clausify(goals)).
% 0.43/1.41 cnf(2, plain, [-(18 ^ [_66165, _66160]), -(min_precedes(_66160, 17 ^ [_66165, _66160], tptp0))], clausify(goals)).
% 0.43/1.41 cnf(3, plain, [-(occurrence_of(16 ^ [], tptp0))], clausify(goals)).
% 0.43/1.41 cnf(4, plain, [leaf_occ(_66165, 16 ^ []), 18 ^ [_66165, _66160], 20 ^ [_66165, _66160]], clausify(goals)).
% 0.43/1.41 cnf(5, plain, [-(_22974 = _22974)], theory(equality)).
% 0.43/1.41 cnf(6, plain, [-(leaf_occ(_27137, _27268)), leaf_occ(_27070, _27203), _27070 = _27137, _27203 = _27268], theory(equality)).
% 0.43/1.41 cnf(7, plain, [min_precedes(_40326, _40593, _40389), occurrence_of(_40262, _40389), leaf_occ(_40326, _40262)], clausify(sos_09)).
% 0.43/1.41 cnf(8, plain, [occurrence_of(_52157, tptp0), -(leaf_occ(15 ^ [_52157], _52157))], clausify(sos_32)).
% 0.43/1.41
% 0.43/1.41 cnf('1',plain,[leaf_occ(15 ^ [16 ^ []], 16 ^ []), 18 ^ [15 ^ [16 ^ []], 15 ^ [16 ^ []]], 20 ^ [15 ^ [16 ^ []], 15 ^ [16 ^ []]]],start(4,bind([[_66165, _66160], [15 ^ [16 ^ []], 15 ^ [16 ^ []]]]))).
% 0.43/1.41 cnf('1.1',plain,[-(leaf_occ(15 ^ [16 ^ []], 16 ^ [])), leaf_occ(15 ^ [16 ^ []], 16 ^ []), 15 ^ [16 ^ []] = 15 ^ [16 ^ []], 16 ^ [] = 16 ^ []],extension(6,bind([[_27070, _27137, _27203, _27268], [15 ^ [16 ^ []], 15 ^ [16 ^ []], 16 ^ [], 16 ^ []]]))).
% 0.43/1.41 cnf('1.1.1',plain,[-(leaf_occ(15 ^ [16 ^ []], 16 ^ [])), leaf_occ(15 ^ [16 ^ []], 16 ^ []), 15 ^ [16 ^ []] = 15 ^ [16 ^ []], 16 ^ [] = 16 ^ []],extension(6,bind([[_27070, _27137, _27203, _27268], [15 ^ [16 ^ []], 15 ^ [16 ^ []], 16 ^ [], 16 ^ []]]))).
% 0.43/1.41 cnf('1.1.1.1',plain,[-(leaf_occ(15 ^ [16 ^ []], 16 ^ [])), occurrence_of(16 ^ [], tptp0)],extension(8,bind([[_52157], [16 ^ []]]))).
% 0.43/1.41 cnf('1.1.1.1.1',plain,[-(occurrence_of(16 ^ [], tptp0))],extension(3)).
% 0.43/1.41 cnf('1.1.1.2',plain,[-(15 ^ [16 ^ []] = 15 ^ [16 ^ []])],extension(5,bind([[_22974], [15 ^ [16 ^ []]]]))).
% 0.43/1.41 cnf('1.1.1.3',plain,[-(16 ^ [] = 16 ^ [])],extension(5,bind([[_22974], [16 ^ []]]))).
% 0.43/1.41 cnf('1.1.2',plain,[-(15 ^ [16 ^ []] = 15 ^ [16 ^ []])],extension(5,bind([[_22974], [15 ^ [16 ^ []]]]))).
% 0.43/1.41 cnf('1.1.3',plain,[-(16 ^ [] = 16 ^ [])],extension(5,bind([[_22974], [16 ^ []]]))).
% 0.43/1.41 cnf('1.2',plain,[-(18 ^ [15 ^ [16 ^ []], 15 ^ [16 ^ []]]), -(min_precedes(15 ^ [16 ^ []], 17 ^ [15 ^ [16 ^ []], 15 ^ [16 ^ []]], tptp0))],extension(2,bind([[_66165, _66160], [15 ^ [16 ^ []], 15 ^ [16 ^ []]]]))).
% 0.43/1.41 cnf('1.2.1',plain,[min_precedes(15 ^ [16 ^ []], 17 ^ [15 ^ [16 ^ []], 15 ^ [16 ^ []]], tptp0), occurrence_of(16 ^ [], tptp0), leaf_occ(15 ^ [16 ^ []], 16 ^ [])],extension(7,bind([[_40593, _40389, _40326, _40262], [17 ^ [15 ^ [16 ^ []], 15 ^ [16 ^ []]], tptp0, 15 ^ [16 ^ []], 16 ^ []]]))).
% 0.43/1.41 cnf('1.2.1.1',plain,[-(occurrence_of(16 ^ [], tptp0))],extension(3)).
% 0.43/1.41 cnf('1.2.1.2',plain,[-(leaf_occ(15 ^ [16 ^ []], 16 ^ [])), occurrence_of(16 ^ [], tptp0)],extension(8,bind([[_52157], [16 ^ []]]))).
% 0.43/1.41 cnf('1.2.1.2.1',plain,[-(occurrence_of(16 ^ [], tptp0))],extension(3)).
% 0.43/1.41 cnf('1.3',plain,[-(20 ^ [15 ^ [16 ^ []], 15 ^ [16 ^ []]]), -(min_precedes(15 ^ [16 ^ []], 19 ^ [15 ^ [16 ^ []], 15 ^ [16 ^ []]], tptp0))],extension(1,bind([[_66165, _66160], [15 ^ [16 ^ []], 15 ^ [16 ^ []]]]))).
% 0.43/1.41 cnf('1.3.1',plain,[min_precedes(15 ^ [16 ^ []], 19 ^ [15 ^ [16 ^ []], 15 ^ [16 ^ []]], tptp0), occurrence_of(16 ^ [], tptp0), leaf_occ(15 ^ [16 ^ []], 16 ^ [])],extension(7,bind([[_40593, _40389, _40326, _40262], [19 ^ [15 ^ [16 ^ []], 15 ^ [16 ^ []]], tptp0, 15 ^ [16 ^ []], 16 ^ []]]))).
% 0.43/1.41 cnf('1.3.1.1',plain,[-(occurrence_of(16 ^ [], tptp0))],extension(3)).
% 0.43/1.41 cnf('1.3.1.2',plain,[-(leaf_occ(15 ^ [16 ^ []], 16 ^ []))],lemmata('1')).
% 0.43/1.41 %-----------------------------------------------------
% 0.43/1.42
% 0.43/1.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------