%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : ITP006+2 : TPTP v8.1.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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 : Sat Jul 16 23:40:17 EDT 2022
% Result : Theorem 2.55s 3.43s
% Output : Proof 2.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : ITP006+2 : TPTP v8.1.0. Bugfixed v7.5.0.
% 0.00/0.11 % Command : leancop_casc.sh %s %d
% 0.11/0.30 % Computer : n032.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 600
% 0.11/0.30 % DateTime : Thu Jun 2 20:59:31 EDT 2022
% 0.11/0.30 % CPUTime :
% 2.55/3.43 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.55/3.44 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.58/3.44
% 2.58/3.44 %-----------------------------------------------------
% 2.58/3.44 fof(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT, conjecture, ! [_237537] : (ne(_237537) => ! [_237552] : (ne(_237552) => ! [_237567] : (mem(_237567, arr(_237552, _237537)) => ! [_237592] : (mem(_237592, arr(_237537, bool)) => ! [_237617] : (mem(_237617, arr(_237537, bool)) => ! [_237642] : (mem(_237642, _237537) => p(ap(_237617, _237642)) => p(ap(_237592, _237642))) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(_237552, _237537), _237567), _237592)) => p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(_237552, _237537), _237567), _237617))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 2.58/3.44 fof(ap_tp, axiom, ! [_238279, _238282, _238285] : (mem(_238285, arr(_238279, _238282)) => ! [_238310] : (mem(_238310, _238279) => mem(ap(_238285, _238310), _238282))), file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax', ap_tp)).
% 2.58/3.44 fof(conj_thm_2EquantHeuristics_2EGUESS__REWRITES, axiom, ! [_238583] : (ne(_238583) => ! [_238598] : (ne(_238598) => ! [_238613] : (mem(_238613, arr(_238583, _238598)) => ! [_238638] : (mem(_238638, arr(_238598, bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(_238583, _238598), _238613), _238638)) <=> ! [_238691] : (mem(_238691, _238598) => p(ap(_238638, _238691)) => ? [_238723] : (mem(_238723, _238583) & p(ap(_238638, ap(_238613, _238723)))))) & (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(_238583, _238598), _238613), _238638)) <=> ! [_238790] : (mem(_238790, _238598) => ~ p(ap(_238638, _238790)) => ? [_238824] : (mem(_238824, _238583) & ~ p(ap(_238638, ap(_238613, _238824)))))) & ! [_238865] : (mem(_238865, arr(_238583, _238598)) => ! [_238890] : (mem(_238890, arr(_238598, bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(_238583, _238598), _238865), _238890)) <=> ! [_238943] : (mem(_238943, _238583) => p(ap(_238890, ap(_238865, _238943))))))) & ! [_238982] : (mem(_238982, arr(_238583, _238598)) => ! [_239007] : (mem(_239007, arr(_238598, bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(_238583, _238598), _238982), _239007)) <=> ! [_239060] : (mem(_239060, _238583) => ~ p(ap(_239007, ap(_238982, _239060))))))) & ! [_239101] : (mem(_239101, arr(_238583, _238598)) => ! [_239126] : (mem(_239126, arr(_238598, bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(_238583, _238598), _239101), _239126)) <=> ! [_239179] : (mem(_239179, _238598) => p(ap(_239126, _239179)) => ? [_239211] : (mem(_239211, _238583) & _239179 = ap(_239101, _239211)))))) & ! [_239242] : (mem(_239242, arr(_238583, _238598)) => ! [_239267] : (mem(_239267, arr(_238598, bool)) => (p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(_238583, _238598), _239242), _239267)) <=> ! [_239320] : (mem(_239320, _238598) => ~ p(ap(_239267, _239320)) => ? [_239354] : (mem(_239354, _238583) & _239320 = ap(_239242, _239354)))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conj_thm_2EquantHeuristics_2EGUESS__REWRITES)).
% 2.58/3.44
% 2.58/3.44 cnf(1, plain, [-(ne(14 ^ []))], clausify(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 2.58/3.44 cnf(2, plain, [-(ne(15 ^ []))], clausify(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 2.58/3.44 cnf(3, plain, [-(mem(16 ^ [], arr(15 ^ [], 14 ^ [])))], clausify(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 2.58/3.44 cnf(4, plain, [-(mem(17 ^ [], arr(14 ^ [], bool)))], clausify(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 2.58/3.44 cnf(5, plain, [-(mem(18 ^ [], arr(14 ^ [], bool)))], clausify(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 2.58/3.44 cnf(6, plain, [-(p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(15 ^ [], 14 ^ []), 16 ^ []), 17 ^ [])))], clausify(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 2.58/3.44 cnf(7, plain, [p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(15 ^ [], 14 ^ []), 16 ^ []), 18 ^ []))], clausify(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 2.58/3.44 cnf(8, plain, [mem(_215594, 14 ^ []), p(ap(18 ^ [], _215594)), -(p(ap(17 ^ [], _215594)))], clausify(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 2.58/3.44 cnf(9, plain, [mem(_47635, arr(_47502, _47569)), mem(_47796, _47502), -(mem(ap(_47635, _47796), _47569))], clausify(ap_tp)).
% 2.58/3.44 cnf(10, plain, [ne(_66256), ne(_66773), mem(_67284, arr(_66256, _66773)), mem(_67847, arr(_66773, bool)), mem(_70654, arr(_66256, _66773)), mem(_70855, arr(_66773, bool)), -(p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(_66256, _66773), _70654), _70855))), -(mem(9 ^ [_70855, _70654, _67847, _67284, _66773, _66256], _66256))], clausify(conj_thm_2EquantHeuristics_2EGUESS__REWRITES)).
% 2.58/3.44 cnf(11, plain, [ne(_66256), ne(_66773), mem(_67284, arr(_66256, _66773)), mem(_67847, arr(_66773, bool)), mem(_70654, arr(_66256, _66773)), mem(_70855, arr(_66773, bool)), -(p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(_66256, _66773), _70654), _70855))), -(p(ap(_70855, ap(_70654, 9 ^ [_70855, _70654, _67847, _67284, _66773, _66256]))))], clausify(conj_thm_2EquantHeuristics_2EGUESS__REWRITES)).
% 2.58/3.44 cnf(12, plain, [ne(_66256), ne(_66773), mem(_67284, arr(_66256, _66773)), mem(_67847, arr(_66773, bool)), mem(_70654, arr(_66256, _66773)), mem(_70855, arr(_66773, bool)), p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(_66256, _66773), _70654), _70855)), mem(_71195, _66256), p(ap(_70855, ap(_70654, _71195)))], clausify(conj_thm_2EquantHeuristics_2EGUESS__REWRITES)).
% 2.58/3.44
% 2.58/3.44 cnf('1',plain,[p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(15 ^ [], 14 ^ []), 16 ^ []), 18 ^ []))],start(7)).
% 2.58/3.44 cnf('1.1',plain,[-(p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(15 ^ [], 14 ^ []), 16 ^ []), 18 ^ []))), ne(15 ^ []), ne(14 ^ []), mem(16 ^ [], arr(15 ^ [], 14 ^ [])), mem(17 ^ [], arr(14 ^ [], bool)), mem(16 ^ [], arr(15 ^ [], 14 ^ [])), mem(18 ^ [], arr(14 ^ [], bool)), -(mem(9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []], 15 ^ []))],extension(10,bind([[_70855, _70654, _67847, _67284, _66773, _66256], [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []]]))).
% 2.58/3.44 cnf('1.1.1',plain,[-(ne(15 ^ []))],extension(2)).
% 2.58/3.44 cnf('1.1.2',plain,[-(ne(14 ^ []))],extension(1)).
% 2.58/3.44 cnf('1.1.3',plain,[-(mem(16 ^ [], arr(15 ^ [], 14 ^ [])))],extension(3)).
% 2.58/3.44 cnf('1.1.4',plain,[-(mem(17 ^ [], arr(14 ^ [], bool)))],extension(4)).
% 2.58/3.44 cnf('1.1.5',plain,[-(mem(16 ^ [], arr(15 ^ [], 14 ^ [])))],extension(3)).
% 2.58/3.44 cnf('1.1.6',plain,[-(mem(18 ^ [], arr(14 ^ [], bool)))],extension(5)).
% 2.58/3.44 cnf('1.1.7',plain,[mem(9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []], 15 ^ []), ne(15 ^ []), ne(14 ^ []), mem(16 ^ [], arr(15 ^ [], 14 ^ [])), mem(17 ^ [], arr(14 ^ [], bool)), mem(16 ^ [], arr(15 ^ [], 14 ^ [])), mem(17 ^ [], arr(14 ^ [], bool)), p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(15 ^ [], 14 ^ []), 16 ^ []), 17 ^ [])), p(ap(17 ^ [], ap(16 ^ [], 9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []])))],extension(12,bind([[_67284, _67847, _66256, _66773, _70855, _70654, _71195], [16 ^ [], 17 ^ [], 15 ^ [], 14 ^ [], 17 ^ [], 16 ^ [], 9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []]]]))).
% 2.58/3.44 cnf('1.1.7.1',plain,[-(ne(15 ^ []))],extension(2)).
% 2.58/3.44 cnf('1.1.7.2',plain,[-(ne(14 ^ []))],extension(1)).
% 2.58/3.44 cnf('1.1.7.3',plain,[-(mem(16 ^ [], arr(15 ^ [], 14 ^ [])))],extension(3)).
% 2.58/3.44 cnf('1.1.7.4',plain,[-(mem(17 ^ [], arr(14 ^ [], bool)))],extension(4)).
% 2.58/3.44 cnf('1.1.7.5',plain,[-(mem(16 ^ [], arr(15 ^ [], 14 ^ [])))],extension(3)).
% 2.58/3.44 cnf('1.1.7.6',plain,[-(mem(17 ^ [], arr(14 ^ [], bool)))],extension(4)).
% 2.58/3.44 cnf('1.1.7.7',plain,[-(p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(15 ^ [], 14 ^ []), 16 ^ []), 17 ^ [])))],extension(6)).
% 2.58/3.44 cnf('1.1.7.8',plain,[-(p(ap(17 ^ [], ap(16 ^ [], 9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []])))), mem(ap(16 ^ [], 9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []]), 14 ^ []), p(ap(18 ^ [], ap(16 ^ [], 9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []])))],extension(8,bind([[_215594], [ap(16 ^ [], 9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []])]]))).
% 2.58/3.44 cnf('1.1.7.8.1',plain,[-(mem(ap(16 ^ [], 9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []]), 14 ^ [])), mem(16 ^ [], arr(15 ^ [], 14 ^ [])), mem(9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []], 15 ^ [])],extension(9,bind([[_47635, _47569, _47796, _47502], [16 ^ [], 14 ^ [], 9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []], 15 ^ []]]))).
% 2.58/3.44 cnf('1.1.7.8.1.1',plain,[-(mem(16 ^ [], arr(15 ^ [], 14 ^ [])))],extension(3)).
% 2.58/3.44 cnf('1.1.7.8.1.2',plain,[-(mem(9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []], 15 ^ []))],reduction('1.1')).
% 2.58/3.44 cnf('1.1.7.8.2',plain,[-(p(ap(18 ^ [], ap(16 ^ [], 9 ^ [18 ^ [], 16 ^ [], 17 ^ [], 16 ^ [], 14 ^ [], 15 ^ []])))), ne(15 ^ []), ne(14 ^ []), mem(16 ^ [], arr(15 ^ [], 14 ^ [])), mem(17 ^ [], arr(14 ^ [], bool)), mem(16 ^ [], arr(15 ^ [], 14 ^ [])), mem(18 ^ [], arr(14 ^ [], bool)), -(p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(15 ^ [], 14 ^ []), 16 ^ []), 18 ^ [])))],extension(11,bind([[_67284, _67847, _66256, _66773, _70654, _70855], [16 ^ [], 17 ^ [], 15 ^ [], 14 ^ [], 16 ^ [], 18 ^ []]]))).
% 2.58/3.44 cnf('1.1.7.8.2.1',plain,[-(ne(15 ^ []))],extension(2)).
% 2.58/3.44 cnf('1.1.7.8.2.2',plain,[-(ne(14 ^ []))],extension(1)).
% 2.58/3.44 cnf('1.1.7.8.2.3',plain,[-(mem(16 ^ [], arr(15 ^ [], 14 ^ [])))],extension(3)).
% 2.58/3.44 cnf('1.1.7.8.2.4',plain,[-(mem(17 ^ [], arr(14 ^ [], bool)))],extension(4)).
% 2.58/3.44 cnf('1.1.7.8.2.5',plain,[-(mem(16 ^ [], arr(15 ^ [], 14 ^ [])))],extension(3)).
% 2.58/3.44 cnf('1.1.7.8.2.6',plain,[-(mem(18 ^ [], arr(14 ^ [], bool)))],extension(5)).
% 2.58/3.44 cnf('1.1.7.8.2.7',plain,[p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(15 ^ [], 14 ^ []), 16 ^ []), 18 ^ []))],extension(7)).
% 2.58/3.44 %-----------------------------------------------------
% 2.58/3.44
% 2.58/3.44 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------