%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SYN550+1 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n016.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 : Thu Jul 21 08:19:37 EDT 2022
% Result : Theorem 0.80s 1.35s
% Output : Proof 0.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : SYN550+1 : TPTP v8.1.0. Released v2.2.0.
% 0.05/0.09 % Command : leancop_casc.sh %s %d
% 0.09/0.29 % Computer : n016.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 600
% 0.09/0.29 % DateTime : Tue Jul 12 04:15:59 EDT 2022
% 0.09/0.29 % CPUTime :
% 0.80/1.35 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.80/1.36 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.80/1.36
% 0.80/1.36 %-----------------------------------------------------
% 0.80/1.36 fof(prove_this, conjecture, ? [_17100] : (reachable(initial_world, _17100) & ! [_17118] : (reachable(_17100, _17118) => p(_17118))) <=> ? [_17100] : (reachable(initial_world, _17100) & ! [_17118] : (reachable(_17100, _17118) => ? [_17177] : (reachable(_17118, _17177) & ! [_17195] : (reachable(_17177, _17195) => p(_17195))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_this)).
% 0.80/1.36 fof(reflexivity_of_reachable, axiom, ! [_17691] : reachable(_17691, _17691), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity_of_reachable)).
% 0.80/1.36 fof(transitivity_of_reachable, axiom, ! [_17798, _17801, _17804] : (reachable(_17798, _17801) & reachable(_17801, _17804) => reachable(_17798, _17804)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', transitivity_of_reachable)).
% 0.80/1.36
% 0.80/1.36 cnf(1, plain, [-(11 ^ [_4184]), p(10 ^ [_4184])], clausify(prove_this)).
% 0.80/1.36 cnf(2, plain, [-(11 ^ [_4184]), -(reachable(_4184, 10 ^ [_4184]))], clausify(prove_this)).
% 0.80/1.36 cnf(3, plain, [-(9 ^ [_5571]), reachable(8 ^ [_5571], _5673), -(p(_5673))], clausify(prove_this)).
% 0.80/1.36 cnf(4, plain, [-(9 ^ [_5571]), -(reachable(_5571, 8 ^ [_5571]))], clausify(prove_this)).
% 0.80/1.36 cnf(5, plain, [-(12 ^ []), reachable(7 ^ [], _5571), 9 ^ [_5571]], clausify(prove_this)).
% 0.80/1.36 cnf(6, plain, [-(12 ^ []), -(reachable(initial_world, 7 ^ []))], clausify(prove_this)).
% 0.80/1.36 cnf(7, plain, [-(12 ^ []), reachable(initial_world, _4184), 11 ^ [_4184]], clausify(prove_this)).
% 0.80/1.36 cnf(8, plain, [-(4 ^ [_5385, _4468]), p(3 ^ [_5385, _4468])], clausify(prove_this)).
% 0.80/1.36 cnf(9, plain, [-(4 ^ [_5385, _4468]), -(reachable(_5385, 3 ^ [_5385, _4468]))], clausify(prove_this)).
% 0.80/1.36 cnf(10, plain, [-(5 ^ [_4468]), reachable(2 ^ [_4468], _5385), 4 ^ [_5385, _4468]], clausify(prove_this)).
% 0.80/1.36 cnf(11, plain, [-(5 ^ [_4468]), -(reachable(_4468, 2 ^ [_4468]))], clausify(prove_this)).
% 0.80/1.36 cnf(12, plain, [-(6 ^ []), reachable(initial_world, _4468), 5 ^ [_4468]], clausify(prove_this)).
% 0.80/1.36 cnf(13, plain, [-(6 ^ []), reachable(1 ^ [], _5307), -(p(_5307))], clausify(prove_this)).
% 0.80/1.36 cnf(14, plain, [-(6 ^ []), -(reachable(initial_world, 1 ^ []))], clausify(prove_this)).
% 0.80/1.36 cnf(15, plain, [6 ^ [], 12 ^ []], clausify(prove_this)).
% 0.80/1.36 cnf(16, plain, [-(reachable(_3537, _3537))], clausify(reflexivity_of_reachable)).
% 0.80/1.36 cnf(17, plain, [-(reachable(_3701, _3812)), reachable(_3701, _3757), reachable(_3757, _3812)], clausify(transitivity_of_reachable)).
% 0.80/1.36
% 0.80/1.36 cnf('1',plain,[6 ^ [], 12 ^ []],start(15)).
% 0.80/1.36 cnf('1.1',plain,[-(6 ^ []), reachable(1 ^ [], 3 ^ [2 ^ [1 ^ []], 1 ^ []]), -(p(3 ^ [2 ^ [1 ^ []], 1 ^ []]))],extension(13,bind([[_5307], [3 ^ [2 ^ [1 ^ []], 1 ^ []]]]))).
% 0.80/1.36 cnf('1.1.1',plain,[-(reachable(1 ^ [], 3 ^ [2 ^ [1 ^ []], 1 ^ []])), reachable(1 ^ [], 2 ^ [1 ^ []]), reachable(2 ^ [1 ^ []], 3 ^ [2 ^ [1 ^ []], 1 ^ []])],extension(17,bind([[_3701, _3757, _3812], [1 ^ [], 2 ^ [1 ^ []], 3 ^ [2 ^ [1 ^ []], 1 ^ []]]]))).
% 0.80/1.36 cnf('1.1.1.1',plain,[-(reachable(1 ^ [], 2 ^ [1 ^ []])), -(5 ^ [1 ^ []])],extension(11,bind([[_4468], [1 ^ []]]))).
% 0.80/1.36 cnf('1.1.1.1.1',plain,[5 ^ [1 ^ []], -(6 ^ []), reachable(initial_world, 1 ^ [])],extension(12,bind([[_4468], [1 ^ []]]))).
% 0.80/1.36 cnf('1.1.1.1.1.1',plain,[6 ^ []],reduction('1')).
% 0.80/1.36 cnf('1.1.1.1.1.2',plain,[-(reachable(initial_world, 1 ^ [])), -(6 ^ [])],extension(14)).
% 0.80/1.36 cnf('1.1.1.1.1.2.1',plain,[6 ^ []],lemmata('1.1.1.1.1')).
% 0.80/1.36 cnf('1.1.1.2',plain,[-(reachable(2 ^ [1 ^ []], 3 ^ [2 ^ [1 ^ []], 1 ^ []])), -(4 ^ [2 ^ [1 ^ []], 1 ^ []])],extension(9,bind([[_5385, _4468], [2 ^ [1 ^ []], 1 ^ []]]))).
% 0.80/1.36 cnf('1.1.1.2.1',plain,[4 ^ [2 ^ [1 ^ []], 1 ^ []], -(5 ^ [1 ^ []]), reachable(2 ^ [1 ^ []], 2 ^ [1 ^ []])],extension(10,bind([[_4468, _5385], [1 ^ [], 2 ^ [1 ^ []]]]))).
% 0.80/1.36 cnf('1.1.1.2.1.1',plain,[5 ^ [1 ^ []], -(6 ^ []), reachable(initial_world, 1 ^ [])],extension(12,bind([[_4468], [1 ^ []]]))).
% 0.80/1.36 cnf('1.1.1.2.1.1.1',plain,[6 ^ []],reduction('1')).
% 0.80/1.36 cnf('1.1.1.2.1.1.2',plain,[-(reachable(initial_world, 1 ^ [])), -(6 ^ [])],extension(14)).
% 0.80/1.36 cnf('1.1.1.2.1.1.2.1',plain,[6 ^ []],lemmata('1.1.1.2.1.1')).
% 0.80/1.36 cnf('1.1.1.2.1.2',plain,[-(reachable(2 ^ [1 ^ []], 2 ^ [1 ^ []]))],extension(16,bind([[_3537], [2 ^ [1 ^ []]]]))).
% 0.80/1.36 cnf('1.1.2',plain,[p(3 ^ [2 ^ [1 ^ []], 1 ^ []]), -(4 ^ [2 ^ [1 ^ []], 1 ^ []])],extension(8,bind([[_5385, _4468], [2 ^ [1 ^ []], 1 ^ []]]))).
% 0.80/1.36 cnf('1.1.2.1',plain,[4 ^ [2 ^ [1 ^ []], 1 ^ []], -(5 ^ [1 ^ []]), reachable(2 ^ [1 ^ []], 2 ^ [1 ^ []])],extension(10,bind([[_4468, _5385], [1 ^ [], 2 ^ [1 ^ []]]]))).
% 0.80/1.36 cnf('1.1.2.1.1',plain,[5 ^ [1 ^ []], -(6 ^ []), reachable(initial_world, 1 ^ [])],extension(12,bind([[_4468], [1 ^ []]]))).
% 0.80/1.36 cnf('1.1.2.1.1.1',plain,[6 ^ []],reduction('1')).
% 0.80/1.36 cnf('1.1.2.1.1.2',plain,[-(reachable(initial_world, 1 ^ [])), -(6 ^ [])],extension(14)).
% 0.80/1.36 cnf('1.1.2.1.1.2.1',plain,[6 ^ []],lemmata('1.1.2.1.1')).
% 0.80/1.36 cnf('1.1.2.1.2',plain,[-(reachable(2 ^ [1 ^ []], 2 ^ [1 ^ []]))],extension(16,bind([[_3537], [2 ^ [1 ^ []]]]))).
% 0.80/1.36 cnf('1.2',plain,[-(12 ^ []), reachable(initial_world, 8 ^ [7 ^ []]), 11 ^ [8 ^ [7 ^ []]]],extension(7,bind([[_4184], [8 ^ [7 ^ []]]]))).
% 0.80/1.36 cnf('1.2.1',plain,[-(reachable(initial_world, 8 ^ [7 ^ []])), reachable(initial_world, 7 ^ []), reachable(7 ^ [], 8 ^ [7 ^ []])],extension(17,bind([[_3701, _3757, _3812], [initial_world, 7 ^ [], 8 ^ [7 ^ []]]]))).
% 0.80/1.36 cnf('1.2.1.1',plain,[-(reachable(initial_world, 7 ^ [])), -(12 ^ [])],extension(6)).
% 0.80/1.36 cnf('1.2.1.1.1',plain,[12 ^ []],reduction('1')).
% 0.80/1.36 cnf('1.2.1.2',plain,[-(reachable(7 ^ [], 8 ^ [7 ^ []])), -(9 ^ [7 ^ []])],extension(4,bind([[_5571], [7 ^ []]]))).
% 0.80/1.36 cnf('1.2.1.2.1',plain,[9 ^ [7 ^ []], -(12 ^ []), reachable(7 ^ [], 7 ^ [])],extension(5,bind([[_5571], [7 ^ []]]))).
% 0.80/1.36 cnf('1.2.1.2.1.1',plain,[12 ^ []],reduction('1')).
% 0.80/1.36 cnf('1.2.1.2.1.2',plain,[-(reachable(7 ^ [], 7 ^ []))],extension(16,bind([[_3537], [7 ^ []]]))).
% 0.80/1.36 cnf('1.2.2',plain,[-(11 ^ [8 ^ [7 ^ []]]), p(10 ^ [8 ^ [7 ^ []]])],extension(1,bind([[_4184], [8 ^ [7 ^ []]]]))).
% 0.80/1.36 cnf('1.2.2.1',plain,[-(p(10 ^ [8 ^ [7 ^ []]])), -(9 ^ [7 ^ []]), reachable(8 ^ [7 ^ []], 10 ^ [8 ^ [7 ^ []]])],extension(3,bind([[_5571, _5673], [7 ^ [], 10 ^ [8 ^ [7 ^ []]]]]))).
% 0.80/1.36 cnf('1.2.2.1.1',plain,[9 ^ [7 ^ []], -(12 ^ []), reachable(7 ^ [], 7 ^ [])],extension(5,bind([[_5571], [7 ^ []]]))).
% 0.80/1.36 cnf('1.2.2.1.1.1',plain,[12 ^ []],reduction('1')).
% 0.80/1.36 cnf('1.2.2.1.1.2',plain,[-(reachable(7 ^ [], 7 ^ []))],extension(16,bind([[_3537], [7 ^ []]]))).
% 0.80/1.36 cnf('1.2.2.1.2',plain,[-(reachable(8 ^ [7 ^ []], 10 ^ [8 ^ [7 ^ []]])), -(11 ^ [8 ^ [7 ^ []]])],extension(2,bind([[_4184], [8 ^ [7 ^ []]]]))).
% 0.80/1.36 cnf('1.2.2.1.2.1',plain,[11 ^ [8 ^ [7 ^ []]]],reduction('1.2')).
% 0.80/1.36 %-----------------------------------------------------
% 0.80/1.36
% 0.85/1.37 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------