%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PRO010+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n012.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:00 EDT 2022
% Result : Theorem 1.05s 1.39s
% Output : Proof 1.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PRO010+1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n012.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 03:43:40 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.05/1.39 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.05/1.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.05/1.41
% 1.05/1.41 %-----------------------------------------------------
% 1.05/1.41 fof(goals, conjecture, ! [_88457] : (occurrence_of(_88457, tptp0) => ? [_88475, _88478] : (leaf_occ(_88478, _88457) & (occurrence_of(_88478, tptp1) => ~ ? [_88508] : (occurrence_of(_88508, tptp2) & min_precedes(_88475, _88508, tptp0))) & (occurrence_of(_88478, tptp2) => ~ ? [_88551] : (occurrence_of(_88551, tptp1) & min_precedes(_88475, _88551, tptp0))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 1.05/1.41 fof(sos_07, axiom, ! [_88977, _88980] : (occurrence_of(_88977, _88980) => (arboreal(_88977) <=> atomic(_88980))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_07)).
% 1.05/1.41 fof(sos_11, axiom, ! [_89156, _89159, _89162] : (min_precedes(_89159, _89162, _89156) => ? [_89183, _89186] : (subactivity(_89183, _89156) & subactivity(_89186, _89156) & atocc(_89159, _89183) & atocc(_89162, _89186))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_11)).
% 1.05/1.41 fof(sos_23, axiom, ! [_89466, _89469] : (atocc(_89466, _89469) <=> ? [_89487] : (subactivity(_89469, _89487) & atomic(_89487) & occurrence_of(_89466, _89487))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_23)).
% 1.05/1.41 fof(sos_37, axiom, ~ atomic(tptp0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_37)).
% 1.05/1.41 fof(sos_35, axiom, ! [_89788] : (occurrence_of(_89788, tptp0) => ? [_89806, _89809, _89812] : (occurrence_of(_89806, tptp3) & root_occ(_89806, _89788) & occurrence_of(_89809, tptp4) & next_subocc(_89806, _89809, tptp0) & (occurrence_of(_89812, tptp1) | occurrence_of(_89812, tptp2)) & next_subocc(_89809, _89812, tptp0) & leaf_occ(_89812, _89788))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_35)).
% 1.05/1.41
% 1.05/1.41 cnf(1, plain, [-(23 ^ [_68407, _68402]), -(min_precedes(_68402, 22 ^ [_68407, _68402], tptp0))], clausify(goals)).
% 1.05/1.41 cnf(2, plain, [-(21 ^ [_68407, _68402]), -(min_precedes(_68402, 20 ^ [_68407, _68402], tptp0))], clausify(goals)).
% 1.05/1.41 cnf(3, plain, [-(occurrence_of(19 ^ [], tptp0))], clausify(goals)).
% 1.05/1.41 cnf(4, plain, [leaf_occ(_68407, 19 ^ []), 21 ^ [_68407, _68402], 23 ^ [_68407, _68402]], clausify(goals)).
% 1.05/1.41 cnf(5, plain, [-(_23789 = _23789)], theory(equality)).
% 1.05/1.41 cnf(6, plain, [-(leaf_occ(_27952, _28083)), leaf_occ(_27885, _28018), _27885 = _27952, _28018 = _28083], theory(equality)).
% 1.05/1.41 cnf(7, plain, [occurrence_of(_37741, _37790), arboreal(_37741), -(atomic(_37790))], clausify(sos_07)).
% 1.05/1.41 cnf(8, plain, [occurrence_of(_37741, _37790), -(arboreal(_37741)), atomic(_37790)], clausify(sos_07)).
% 1.05/1.41 cnf(9, plain, [min_precedes(_39103, _39181, _39024), -(atocc(_39103, 2 ^ [_39181, _39103, _39024]))], clausify(sos_11)).
% 1.05/1.41 cnf(10, plain, [atocc(_46018, _46079), -(atomic(9 ^ [_46079, _46018]))], clausify(sos_23)).
% 1.05/1.41 cnf(11, plain, [atocc(_46018, _46079), -(occurrence_of(_46018, 9 ^ [_46079, _46018]))], clausify(sos_23)).
% 1.05/1.41 cnf(12, plain, [atomic(tptp0)], clausify(sos_37)).
% 1.05/1.41 cnf(13, plain, [occurrence_of(_53727, tptp0), -(leaf_occ(18 ^ [_53727], _53727))], clausify(sos_35)).
% 1.05/1.41
% 1.05/1.41 cnf('1',plain,[leaf_occ(18 ^ [19 ^ []], 19 ^ []), 21 ^ [18 ^ [19 ^ []], 19 ^ []], 23 ^ [18 ^ [19 ^ []], 19 ^ []]],start(4,bind([[_68407, _68402], [18 ^ [19 ^ []], 19 ^ []]]))).
% 1.05/1.41 cnf('1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(6,bind([[_27885, _27952, _28018, _28083], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 1.05/1.41 cnf('1.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(6,bind([[_27885, _27952, _28018, _28083], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 1.05/1.41 cnf('1.1.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(6,bind([[_27885, _27952, _28018, _28083], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 1.05/1.41 cnf('1.1.1.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), leaf_occ(18 ^ [19 ^ []], 19 ^ []), 18 ^ [19 ^ []] = 18 ^ [19 ^ []], 19 ^ [] = 19 ^ []],extension(6,bind([[_27885, _27952, _28018, _28083], [18 ^ [19 ^ []], 18 ^ [19 ^ []], 19 ^ [], 19 ^ []]]))).
% 1.05/1.41 cnf('1.1.1.1.1.1',plain,[-(leaf_occ(18 ^ [19 ^ []], 19 ^ [])), occurrence_of(19 ^ [], tptp0)],extension(13,bind([[_53727], [19 ^ []]]))).
% 1.05/1.41 cnf('1.1.1.1.1.1.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 1.05/1.41 cnf('1.1.1.1.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23789], [18 ^ [19 ^ []]]]))).
% 1.05/1.41 cnf('1.1.1.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23789], [19 ^ []]]))).
% 1.05/1.41 cnf('1.1.1.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23789], [18 ^ [19 ^ []]]]))).
% 1.05/1.41 cnf('1.1.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23789], [19 ^ []]]))).
% 1.05/1.41 cnf('1.1.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23789], [18 ^ [19 ^ []]]]))).
% 1.05/1.41 cnf('1.1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23789], [19 ^ []]]))).
% 1.05/1.41 cnf('1.1.2',plain,[-(18 ^ [19 ^ []] = 18 ^ [19 ^ []])],extension(5,bind([[_23789], [18 ^ [19 ^ []]]]))).
% 1.05/1.41 cnf('1.1.3',plain,[-(19 ^ [] = 19 ^ [])],extension(5,bind([[_23789], [19 ^ []]]))).
% 1.05/1.41 cnf('1.2',plain,[-(21 ^ [18 ^ [19 ^ []], 19 ^ []]), -(min_precedes(19 ^ [], 20 ^ [18 ^ [19 ^ []], 19 ^ []], tptp0))],extension(2,bind([[_68407, _68402], [18 ^ [19 ^ []], 19 ^ []]]))).
% 1.05/1.41 cnf('1.2.1',plain,[min_precedes(19 ^ [], 20 ^ [18 ^ [19 ^ []], 19 ^ []], tptp0), -(atocc(19 ^ [], 2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0]))],extension(9,bind([[_39181, _39103, _39024], [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0]]))).
% 1.05/1.41 cnf('1.2.1.1',plain,[atocc(19 ^ [], 2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0]), -(atomic(9 ^ [2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []]))],extension(10,bind([[_46079, _46018], [2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []]]))).
% 1.05/1.41 cnf('1.2.1.1.1',plain,[atomic(9 ^ [2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []]), occurrence_of(19 ^ [], 9 ^ [2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []]), -(arboreal(19 ^ []))],extension(8,bind([[_37790, _37741], [9 ^ [2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []], 19 ^ []]]))).
% 1.05/1.41 cnf('1.2.1.1.1.1',plain,[-(occurrence_of(19 ^ [], 9 ^ [2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []])), atocc(19 ^ [], 2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0])],extension(11,bind([[_46018, _46079], [19 ^ [], 2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0]]]))).
% 1.05/1.41 cnf('1.2.1.1.1.1.1',plain,[-(atocc(19 ^ [], 2 ^ [20 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0]))],reduction('1.2.1')).
% 1.05/1.41 cnf('1.2.1.1.1.2',plain,[arboreal(19 ^ []), occurrence_of(19 ^ [], tptp0), -(atomic(tptp0))],extension(7,bind([[_37741, _37790], [19 ^ [], tptp0]]))).
% 1.05/1.41 cnf('1.2.1.1.1.2.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 1.05/1.41 cnf('1.2.1.1.1.2.2',plain,[atomic(tptp0)],extension(12)).
% 1.05/1.41 cnf('1.3',plain,[-(23 ^ [18 ^ [19 ^ []], 19 ^ []]), -(min_precedes(19 ^ [], 22 ^ [18 ^ [19 ^ []], 19 ^ []], tptp0))],extension(1,bind([[_68407, _68402], [18 ^ [19 ^ []], 19 ^ []]]))).
% 1.05/1.41 cnf('1.3.1',plain,[min_precedes(19 ^ [], 22 ^ [18 ^ [19 ^ []], 19 ^ []], tptp0), -(atocc(19 ^ [], 2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0]))],extension(9,bind([[_39181, _39103, _39024], [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0]]))).
% 1.05/1.41 cnf('1.3.1.1',plain,[atocc(19 ^ [], 2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0]), -(atomic(9 ^ [2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []]))],extension(10,bind([[_46079, _46018], [2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []]]))).
% 1.05/1.41 cnf('1.3.1.1.1',plain,[atomic(9 ^ [2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []]), occurrence_of(19 ^ [], 9 ^ [2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []]), -(arboreal(19 ^ []))],extension(8,bind([[_37790, _37741], [9 ^ [2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []], 19 ^ []]]))).
% 1.05/1.41 cnf('1.3.1.1.1.1',plain,[-(occurrence_of(19 ^ [], 9 ^ [2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0], 19 ^ []])), atocc(19 ^ [], 2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0])],extension(11,bind([[_46018, _46079], [19 ^ [], 2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0]]]))).
% 1.05/1.41 cnf('1.3.1.1.1.1.1',plain,[-(atocc(19 ^ [], 2 ^ [22 ^ [18 ^ [19 ^ []], 19 ^ []], 19 ^ [], tptp0]))],reduction('1.3.1')).
% 1.05/1.41 cnf('1.3.1.1.1.2',plain,[arboreal(19 ^ []), occurrence_of(19 ^ [], tptp0), -(atomic(tptp0))],extension(7,bind([[_37741, _37790], [19 ^ [], tptp0]]))).
% 1.05/1.41 cnf('1.3.1.1.1.2.1',plain,[-(occurrence_of(19 ^ [], tptp0))],extension(3)).
% 1.05/1.41 cnf('1.3.1.1.1.2.2',plain,[atomic(tptp0)],extension(12)).
% 1.05/1.41 %-----------------------------------------------------
% 1.05/1.41
% 1.05/1.41 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------