%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PRO009+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n014.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:48:59 EDT 2022
% Result : Theorem 0.36s 1.42s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : PRO009+2 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n014.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jun 13 03:21:07 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.36/1.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.43 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.43
% 0.36/1.43 %-----------------------------------------------------
% 0.36/1.43 fof(goals, conjecture, ! [_81241] : (occurrence_of(_81241, tptp0) => ? [_81259, _81262] : (occurrence_of(_81259, tptp3) & root_occ(_81259, _81241) & (occurrence_of(_81262, tptp2) | occurrence_of(_81262, tptp1)) & min_precedes(_81259, _81262, tptp0) & leaf_occ(_81262, _81241))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 0.36/1.43 fof(sos, axiom, ! [_81650, _81653, _81656, _81659] : (min_precedes(_81650, _81653, _81659) & min_precedes(_81653, _81656, _81659) => min_precedes(_81650, _81656, _81659)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos)).
% 0.36/1.43 fof(sos_04, axiom, ! [_81870, _81873, _81876] : (next_subocc(_81870, _81873, _81876) <=> min_precedes(_81870, _81873, _81876) & ~ ? [_81912] : (min_precedes(_81870, _81912, _81876) & min_precedes(_81912, _81873, _81876))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_04)).
% 0.36/1.43 fof(sos_32, axiom, ! [_82218] : (occurrence_of(_82218, tptp0) => ? [_82236, _82239, _82242] : (occurrence_of(_82236, tptp3) & root_occ(_82236, _82218) & occurrence_of(_82239, tptp4) & next_subocc(_82236, _82239, tptp0) & (occurrence_of(_82242, tptp2) | occurrence_of(_82242, tptp1)) & next_subocc(_82239, _82242, tptp0) & leaf_occ(_82242, _82218))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_32)).
% 0.36/1.43
% 0.36/1.43 cnf(1, plain, [-(19 ^ [_63349, _63344]), occurrence_of(_63349, tptp1)], clausify(goals)).
% 0.36/1.43 cnf(2, plain, [-(19 ^ [_63349, _63344]), occurrence_of(_63349, tptp2)], clausify(goals)).
% 0.36/1.43 cnf(3, plain, [-(occurrence_of(18 ^ [], tptp0))], clausify(goals)).
% 0.36/1.43 cnf(4, plain, [occurrence_of(_63344, tptp3), root_occ(_63344, 18 ^ []), 19 ^ [_63349, _63344], min_precedes(_63344, _63349, tptp0), leaf_occ(_63349, 18 ^ [])], clausify(goals)).
% 0.36/1.43 cnf(5, plain, [-(_21816 = _21816)], theory(equality)).
% 0.36/1.43 cnf(6, plain, [-(leaf_occ(_25979, _26110)), leaf_occ(_25912, _26045), _25912 = _25979, _26045 = _26110], theory(equality)).
% 0.36/1.43 cnf(7, plain, [-(root_occ(_30854, _30985)), root_occ(_30787, _30920), _30787 = _30854, _30920 = _30985], theory(equality)).
% 0.36/1.43 cnf(8, plain, [-(min_precedes(_32925, _33052, _33114)), min_precedes(_32925, _32989, _33114), min_precedes(_32989, _33052, _33114)], clausify(sos)).
% 0.36/1.43 cnf(9, plain, [next_subocc(_35458, _35531, _35603), -(min_precedes(_35458, _35531, _35603))], clausify(sos_04)).
% 0.36/1.43 cnf(10, plain, [occurrence_of(_49558, tptp0), -(occurrence_of(15 ^ [_49558], tptp3))], clausify(sos_32)).
% 0.36/1.43 cnf(11, plain, [occurrence_of(_49558, tptp0), -(root_occ(15 ^ [_49558], _49558))], clausify(sos_32)).
% 0.36/1.43 cnf(12, plain, [occurrence_of(_49558, tptp0), -(next_subocc(15 ^ [_49558], 16 ^ [_49558], tptp0))], clausify(sos_32)).
% 0.36/1.43 cnf(13, plain, [occurrence_of(_49558, tptp0), -(next_subocc(16 ^ [_49558], 17 ^ [_49558], tptp0))], clausify(sos_32)).
% 0.36/1.43 cnf(14, plain, [occurrence_of(_49558, tptp0), -(leaf_occ(17 ^ [_49558], _49558))], clausify(sos_32)).
% 0.36/1.43 cnf(15, plain, [occurrence_of(_49558, tptp0), -(occurrence_of(17 ^ [_49558], tptp2)), -(occurrence_of(17 ^ [_49558], tptp1))], clausify(sos_32)).
% 0.36/1.43
% 0.36/1.43 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), leaf_occ(17 ^ [18 ^ []], 18 ^ [])],start(4,bind([[_63344, _63349], [15 ^ [18 ^ []], 17 ^ [18 ^ []]]]))).
% 0.36/1.43 cnf('1.1',plain,[-(occurrence_of(15 ^ [18 ^ []], tptp3)), occurrence_of(18 ^ [], tptp0)],extension(10,bind([[_49558], [18 ^ []]]))).
% 0.36/1.43 cnf('1.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.36/1.43 cnf('1.2',plain,[-(root_occ(15 ^ [18 ^ []], 18 ^ [])), root_occ(15 ^ [18 ^ []], 18 ^ []), 15 ^ [18 ^ []] = 15 ^ [18 ^ []], 18 ^ [] = 18 ^ []],extension(7,bind([[_30787, _30854, _30920, _30985], [15 ^ [18 ^ []], 15 ^ [18 ^ []], 18 ^ [], 18 ^ []]]))).
% 0.36/1.43 cnf('1.2.1',plain,[-(root_occ(15 ^ [18 ^ []], 18 ^ [])), root_occ(15 ^ [18 ^ []], 18 ^ []), 15 ^ [18 ^ []] = 15 ^ [18 ^ []], 18 ^ [] = 18 ^ []],extension(7,bind([[_30787, _30854, _30920, _30985], [15 ^ [18 ^ []], 15 ^ [18 ^ []], 18 ^ [], 18 ^ []]]))).
% 0.36/1.43 cnf('1.2.1.1',plain,[-(root_occ(15 ^ [18 ^ []], 18 ^ [])), occurrence_of(18 ^ [], tptp0)],extension(11,bind([[_49558], [18 ^ []]]))).
% 0.36/1.43 cnf('1.2.1.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.36/1.43 cnf('1.2.1.2',plain,[-(15 ^ [18 ^ []] = 15 ^ [18 ^ []])],extension(5,bind([[_21816], [15 ^ [18 ^ []]]]))).
% 0.36/1.43 cnf('1.2.1.3',plain,[-(18 ^ [] = 18 ^ [])],extension(5,bind([[_21816], [18 ^ []]]))).
% 0.36/1.43 cnf('1.2.2',plain,[-(15 ^ [18 ^ []] = 15 ^ [18 ^ []])],extension(5,bind([[_21816], [15 ^ [18 ^ []]]]))).
% 0.36/1.43 cnf('1.2.3',plain,[-(18 ^ [] = 18 ^ [])],extension(5,bind([[_21816], [18 ^ []]]))).
% 0.36/1.43 cnf('1.3',plain,[-(19 ^ [17 ^ [18 ^ []], 15 ^ [18 ^ []]]), occurrence_of(17 ^ [18 ^ []], tptp1)],extension(1,bind([[_63344, _63349], [15 ^ [18 ^ []], 17 ^ [18 ^ []]]]))).
% 0.36/1.43 cnf('1.3.1',plain,[-(occurrence_of(17 ^ [18 ^ []], tptp1)), occurrence_of(18 ^ [], tptp0), -(occurrence_of(17 ^ [18 ^ []], tptp2))],extension(15,bind([[_49558], [18 ^ []]]))).
% 0.36/1.43 cnf('1.3.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.36/1.43 cnf('1.3.1.2',plain,[occurrence_of(17 ^ [18 ^ []], tptp2), -(19 ^ [17 ^ [18 ^ []], 15 ^ [18 ^ []]])],extension(2,bind([[_63349, _63344], [17 ^ [18 ^ []], 15 ^ [18 ^ []]]]))).
% 0.36/1.43 cnf('1.3.1.2.1',plain,[19 ^ [17 ^ [18 ^ []], 15 ^ [18 ^ []]]],reduction('1')).
% 0.36/1.43 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([[_32925, _32989, _33052, _33114], [15 ^ [18 ^ []], 16 ^ [18 ^ []], 17 ^ [18 ^ []], tptp0]]))).
% 0.36/1.43 cnf('1.4.1',plain,[-(min_precedes(15 ^ [18 ^ []], 16 ^ [18 ^ []], tptp0)), next_subocc(15 ^ [18 ^ []], 16 ^ [18 ^ []], tptp0)],extension(9,bind([[_35458, _35531, _35603], [15 ^ [18 ^ []], 16 ^ [18 ^ []], tptp0]]))).
% 0.36/1.43 cnf('1.4.1.1',plain,[-(next_subocc(15 ^ [18 ^ []], 16 ^ [18 ^ []], tptp0)), occurrence_of(18 ^ [], tptp0)],extension(12,bind([[_49558], [18 ^ []]]))).
% 0.36/1.43 cnf('1.4.1.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.36/1.43 cnf('1.4.2',plain,[-(min_precedes(16 ^ [18 ^ []], 17 ^ [18 ^ []], tptp0)), next_subocc(16 ^ [18 ^ []], 17 ^ [18 ^ []], tptp0)],extension(9,bind([[_35458, _35531, _35603], [16 ^ [18 ^ []], 17 ^ [18 ^ []], tptp0]]))).
% 0.36/1.43 cnf('1.4.2.1',plain,[-(next_subocc(16 ^ [18 ^ []], 17 ^ [18 ^ []], tptp0)), occurrence_of(18 ^ [], tptp0)],extension(13,bind([[_49558], [18 ^ []]]))).
% 0.36/1.43 cnf('1.4.2.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.36/1.43 cnf('1.5',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), leaf_occ(17 ^ [18 ^ []], 18 ^ []), 17 ^ [18 ^ []] = 17 ^ [18 ^ []], 18 ^ [] = 18 ^ []],extension(6,bind([[_25912, _25979, _26045, _26110], [17 ^ [18 ^ []], 17 ^ [18 ^ []], 18 ^ [], 18 ^ []]]))).
% 0.36/1.43 cnf('1.5.1',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), leaf_occ(17 ^ [18 ^ []], 18 ^ []), 17 ^ [18 ^ []] = 17 ^ [18 ^ []], 18 ^ [] = 18 ^ []],extension(6,bind([[_25912, _25979, _26045, _26110], [17 ^ [18 ^ []], 17 ^ [18 ^ []], 18 ^ [], 18 ^ []]]))).
% 0.36/1.43 cnf('1.5.1.1',plain,[-(leaf_occ(17 ^ [18 ^ []], 18 ^ [])), occurrence_of(18 ^ [], tptp0)],extension(14,bind([[_49558], [18 ^ []]]))).
% 0.36/1.43 cnf('1.5.1.1.1',plain,[-(occurrence_of(18 ^ [], tptp0))],extension(3)).
% 0.36/1.43 cnf('1.5.1.2',plain,[-(17 ^ [18 ^ []] = 17 ^ [18 ^ []])],extension(5,bind([[_21816], [17 ^ [18 ^ []]]]))).
% 0.36/1.43 cnf('1.5.1.3',plain,[-(18 ^ [] = 18 ^ [])],extension(5,bind([[_21816], [18 ^ []]]))).
% 0.36/1.43 cnf('1.5.2',plain,[-(17 ^ [18 ^ []] = 17 ^ [18 ^ []])],extension(5,bind([[_21816], [17 ^ [18 ^ []]]]))).
% 0.36/1.43 cnf('1.5.3',plain,[-(18 ^ [] = 18 ^ [])],extension(5,bind([[_21816], [18 ^ []]]))).
% 0.36/1.43 %-----------------------------------------------------
% 0.36/1.44
% 0.36/1.44 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------