%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : ITP006+2 : TPTP v9.2.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n029.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 : 300s
% DateTime : Tue May 5 04:31:26 PM UTC 2026
% Result : Theorem 2.89s 5.63s
% Output : CNFRefutation 3.07s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_37)
% Comments :
%------------------------------------------------------------------------------
fof(conj_thm_2Esat_2Edc__eq,axiom,
! [X42] :
( mem(X42,bool)
=> ! [X43] :
( mem(X43,bool)
=> ! [X44] :
( mem(X44,bool)
=> ( ( p(X42)
<=> ( p(X43)
<=> p(X44) ) )
<=> ( ( p(X42)
| p(X43)
| p(X44) )
& ( p(X42)
| ~ p(X44)
| ~ p(X43) )
& ( p(X43)
| ~ p(X44)
| ~ p(X42) )
& ( p(X44)
| ~ p(X43)
| ~ p(X42) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Esat_2Edc__eq) ).
fof(conj_thm_2EquantHeuristics_2EGUESS__REWRITES,axiom,
! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> ! [X20] :
( mem(X20,arr(X9,X10))
=> ! [X21] :
( mem(X21,arr(X10,bool))
=> ( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X9,X10),X20),X21))
<=> ! [X22] :
( mem(X22,X10)
=> ( p(ap(X21,X22))
=> ? [X23] :
( mem(X23,X9)
& p(ap(X21,ap(X20,X23))) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X9,X10),X20),X21))
<=> ! [X24] :
( mem(X24,X10)
=> ( ~ p(ap(X21,X24))
=> ? [X25] :
( mem(X25,X9)
& ~ p(ap(X21,ap(X20,X25))) ) ) ) )
& ! [X26] :
( mem(X26,arr(X9,X10))
=> ! [X27] :
( mem(X27,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X9,X10),X26),X27))
<=> ! [X28] :
( mem(X28,X9)
=> p(ap(X27,ap(X26,X28))) ) ) ) )
& ! [X29] :
( mem(X29,arr(X9,X10))
=> ! [X30] :
( mem(X30,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X9,X10),X29),X30))
<=> ! [X31] :
( mem(X31,X9)
=> ~ p(ap(X30,ap(X29,X31))) ) ) ) )
& ! [X32] :
( mem(X32,arr(X9,X10))
=> ! [X33] :
( mem(X33,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X9,X10),X32),X33))
<=> ! [X34] :
( mem(X34,X10)
=> ( p(ap(X33,X34))
=> ? [X35] :
( mem(X35,X9)
& X34 = ap(X32,X35) ) ) ) ) ) )
& ! [X36] :
( mem(X36,arr(X9,X10))
=> ! [X37] :
( mem(X37,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X9,X10),X36),X37))
<=> ! [X38] :
( mem(X38,X10)
=> ( ~ p(ap(X37,X38))
=> ? [X39] :
( mem(X39,X9)
& X38 = ap(X36,X39) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2EquantHeuristics_2EGUESS__REWRITES) ).
fof(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT,conjecture,
! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> ! [X20] :
( mem(X20,arr(X10,X9))
=> ! [X21] :
( mem(X21,arr(X9,bool))
=> ! [X45] :
( mem(X45,arr(X9,bool))
=> ( ! [X46] :
( mem(X46,X9)
=> ( p(ap(X45,X46))
=> p(ap(X21,X46)) ) )
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X10,X9),X20),X21))
=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X10,X9),X20),X45)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT) ).
fof(conj_thm_2Esat_2Edc__imp,axiom,
! [X42] :
( mem(X42,bool)
=> ! [X43] :
( mem(X43,bool)
=> ! [X44] :
( mem(X44,bool)
=> ( ( p(X42)
<=> ( p(X43)
=> p(X44) ) )
<=> ( ( p(X42)
| p(X43) )
& ( p(X42)
| ~ p(X44) )
& ( ~ p(X43)
| p(X44)
| ~ p(X42) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Esat_2Edc__imp) ).
fof(conj_thm_2Esat_2Edc__disj,axiom,
! [X42] :
( mem(X42,bool)
=> ! [X43] :
( mem(X43,bool)
=> ! [X44] :
( mem(X44,bool)
=> ( ( p(X42)
<=> ( p(X43)
| p(X44) ) )
<=> ( ( p(X42)
| ~ p(X43) )
& ( p(X42)
| ~ p(X44) )
& ( p(X43)
| p(X44)
| ~ p(X42) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Esat_2Edc__disj) ).
fof(ax_neg_p,axiom,
! [X5] :
( mem(X5,bool)
=> ( p(ap(c_2Ebool_2E_7E,X5))
<=> ~ p(X5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_neg_p) ).
fof(funcext,axiom,
! [X1,X2,X3] :
( mem(X3,arr(X1,X2))
=> ! [X7] :
( mem(X7,arr(X1,X2))
=> ( ! [X4] :
( mem(X4,X1)
=> ap(X3,X4) = ap(X7,X4) )
=> X3 = X7 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',funcext) ).
fof(mem_c_2EquantHeuristics_2EGUESS__EXISTS,axiom,
! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> mem(c_2EquantHeuristics_2EGUESS__EXISTS(X9,X10),arr(arr(X9,X10),arr(arr(X10,bool),bool))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2EquantHeuristics_2EGUESS__EXISTS) ).
fof(mem_c_2EquantHeuristics_2EGUESS__FORALL,axiom,
! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> mem(c_2EquantHeuristics_2EGUESS__FORALL(X9,X10),arr(arr(X9,X10),arr(arr(X10,bool),bool))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2EquantHeuristics_2EGUESS__FORALL) ).
fof(mem_c_2EquantHeuristics_2EGUESS__EXISTS__POINT,axiom,
! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> mem(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X9,X10),arr(arr(X9,X10),arr(arr(X10,bool),bool))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2EquantHeuristics_2EGUESS__EXISTS__POINT) ).
fof(mem_c_2EquantHeuristics_2EGUESS__FORALL__POINT,axiom,
! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> mem(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X9,X10),arr(arr(X9,X10),arr(arr(X10,bool),bool))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2EquantHeuristics_2EGUESS__FORALL__POINT) ).
fof(mem_c_2EquantHeuristics_2EGUESS__EXISTS__GAP,axiom,
! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> mem(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X9,X10),arr(arr(X9,X10),arr(arr(X10,bool),bool))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2EquantHeuristics_2EGUESS__EXISTS__GAP) ).
fof(mem_c_2EquantHeuristics_2EGUESS__FORALL__GAP,axiom,
! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> mem(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X9,X10),arr(arr(X9,X10),arr(arr(X10,bool),bool))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2EquantHeuristics_2EGUESS__FORALL__GAP) ).
fof(ax_all_p,axiom,
! [X1] :
( ne(X1)
=> ! [X5] :
( mem(X5,arr(X1,bool))
=> ( p(ap(c_2Ebool_2E_21(X1),X5))
<=> ! [X4] :
( mem(X4,X1)
=> p(ap(X5,X4)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_all_p) ).
fof(ax_eq_p,axiom,
! [X1] :
( ne(X1)
=> ! [X4] :
( mem(X4,X1)
=> ! [X8] :
( mem(X8,X1)
=> ( p(ap(ap(c_2Emin_2E_3D(X1),X4),X8))
<=> X4 = X8 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_eq_p) ).
fof(ax_ex_p,axiom,
! [X1] :
( ne(X1)
=> ! [X5] :
( mem(X5,arr(X1,bool))
=> ( p(ap(c_2Ebool_2E_3F(X1),X5))
<=> ? [X4] :
( mem(X4,X1)
& p(ap(X5,X4)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_ex_p) ).
fof(ax_imp_p,axiom,
! [X5] :
( mem(X5,bool)
=> ! [X6] :
( mem(X6,bool)
=> ( p(ap(ap(c_2Emin_2E_3D_3D_3E,X5),X6))
<=> ( p(X5)
=> p(X6) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_imp_p) ).
fof(ax_or_p,axiom,
! [X5] :
( mem(X5,bool)
=> ! [X6] :
( mem(X6,bool)
=> ( p(ap(ap(c_2Ebool_2E_5C_2F,X5),X6))
<=> ( p(X5)
| p(X6) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_or_p) ).
fof(ax_and_p,axiom,
! [X5] :
( mem(X5,bool)
=> ! [X6] :
( mem(X6,bool)
=> ( p(ap(ap(c_2Ebool_2E_2F_5C,X5),X6))
<=> ( p(X5)
& p(X6) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_and_p) ).
fof(ap_tp,axiom,
! [X1,X2,X3] :
( mem(X3,arr(X1,X2))
=> ! [X4] :
( mem(X4,X1)
=> mem(ap(X3,X4),X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
fof(mem_c_2Emin_2E_3D,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Emin_2E_3D(X9),arr(X9,arr(X9,bool))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Emin_2E_3D) ).
fof(mem_c_2Ebool_2E_21,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Ebool_2E_21(X9),arr(arr(X9,bool),bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2E_21) ).
fof(mem_c_2Ebool_2E_3F,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Ebool_2E_3F(X9),arr(arr(X9,bool),bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2E_3F) ).
fof(kbeta,axiom,
! [X1,X8,X4] :
( mem(X4,X1)
=> ap(k(X1,X8),X4) = X8 ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',kbeta) ).
fof(boolext,axiom,
! [X5] :
( mem(X5,bool)
=> ! [X6] :
( mem(X6,bool)
=> ( ( p(X5)
<=> p(X6) )
=> X5 = X6 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',boolext) ).
fof(arr_ne,axiom,
! [X1] :
( ne(X1)
=> ! [X2] :
( ne(X2)
=> ne(arr(X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',arr_ne) ).
fof(ibeta,axiom,
! [X1,X4] :
( mem(X4,X1)
=> ap(i(X1),X4) = X4 ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',ibeta) ).
fof(ax_false_p,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_false_p) ).
fof(mem_c_2Emin_2E_3D_3D_3E,axiom,
mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Emin_2E_3D_3D_3E) ).
fof(mem_c_2Ebool_2E_2F_5C,axiom,
mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2E_2F_5C) ).
fof(mem_c_2Ebool_2E_5C_2F,axiom,
mem(c_2Ebool_2E_5C_2F,arr(bool,arr(bool,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2E_5C_2F) ).
fof(mem_c_2Ebool_2E_7E,axiom,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2E_7E) ).
fof(mem_c_2Ebool_2EF,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
fof(mem_c_2Ebool_2ET,axiom,
mem(c_2Ebool_2ET,bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2ET) ).
fof(ax_true_p,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_true_p) ).
fof(ind_ne,axiom,
ne(ind),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',ind_ne) ).
fof(bool_ne,axiom,
ne(bool),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',bool_ne) ).
fof(i_0_37,plain,
! [X44,X43,X42] :
( epred2_3(X42,X43,X44)
<=> ( ( p(X42)
| p(X43)
| p(X44) )
& ( p(X42)
| ~ p(X44)
| ~ p(X43) )
& ( p(X43)
| ~ p(X44)
| ~ p(X42) ) ) ),
introduced(definition) ).
fof(i_0_38,plain,
! [X21,X20,X10,X9] :
( epred1_4(X9,X10,X20,X21)
<=> ( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X9,X10),X20),X21))
<=> ! [X22] :
( mem(X22,X10)
=> ( p(ap(X21,X22))
=> ? [X23] :
( mem(X23,X9)
& p(ap(X21,ap(X20,X23))) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X9,X10),X20),X21))
<=> ! [X24] :
( mem(X24,X10)
=> ( ~ p(ap(X21,X24))
=> ? [X25] :
( mem(X25,X9)
& ~ p(ap(X21,ap(X20,X25))) ) ) ) )
& ! [X26] :
( mem(X26,arr(X9,X10))
=> ! [X27] :
( mem(X27,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X9,X10),X26),X27))
<=> ! [X28] :
( mem(X28,X9)
=> p(ap(X27,ap(X26,X28))) ) ) ) )
& ! [X29] :
( mem(X29,arr(X9,X10))
=> ! [X30] :
( mem(X30,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X9,X10),X29),X30))
<=> ! [X31] :
( mem(X31,X9)
=> ~ p(ap(X30,ap(X29,X31))) ) ) ) )
& ! [X32] :
( mem(X32,arr(X9,X10))
=> ! [X33] :
( mem(X33,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X9,X10),X32),X33))
<=> ! [X34] :
( mem(X34,X10)
=> ( p(ap(X33,X34))
=> ? [X35] :
( mem(X35,X9)
& X34 = ap(X32,X35) ) ) ) ) ) )
& ! [X36] :
( mem(X36,arr(X9,X10))
=> ! [X37] :
( mem(X37,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X9,X10),X36),X37))
<=> ! [X38] :
( mem(X38,X10)
=> ( ~ p(ap(X37,X38))
=> ? [X39] :
( mem(X39,X9)
& X38 = ap(X36,X39) ) ) ) ) ) ) ) ),
introduced(definition) ).
fof(i_0_39,plain,
! [X42] :
( mem(X42,bool)
=> ! [X43] :
( mem(X43,bool)
=> ! [X44] :
( mem(X44,bool)
=> ( ( p(X42)
<=> ( p(X43)
<=> p(X44) ) )
<=> ( epred2_3(X42,X43,X44)
& ( p(X44)
| ~ p(X43)
| ~ p(X42) ) ) ) ) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[conj_thm_2Esat_2Edc__eq]),c_0_37]) ).
fof(i_0_40,plain,
! [X44,X43,X42] :
( epred4_3(X42,X43,X44)
<=> ( ( p(X42)
<=> ( p(X43)
=> p(X44) ) )
<=> ( ( p(X42)
| p(X43) )
& ( p(X42)
| ~ p(X44) )
& ( ~ p(X43)
| p(X44)
| ~ p(X42) ) ) ) ),
introduced(definition) ).
fof(i_0_41,plain,
! [X44,X43,X42] :
( epred3_3(X42,X43,X44)
<=> ( ( p(X42)
<=> ( p(X43)
| p(X44) ) )
<=> ( ( p(X42)
| ~ p(X43) )
& ( p(X42)
| ~ p(X44) )
& ( p(X43)
| p(X44)
| ~ p(X42) ) ) ) ),
introduced(definition) ).
fof(i_0_42,plain,
! [X21,X20,X10,X9] :
( epred1_4(X9,X10,X20,X21)
=> ( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X9,X10),X20),X21))
<=> ! [X22] :
( mem(X22,X10)
=> ( p(ap(X21,X22))
=> ? [X23] :
( mem(X23,X9)
& p(ap(X21,ap(X20,X23))) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X9,X10),X20),X21))
<=> ! [X24] :
( mem(X24,X10)
=> ( ~ p(ap(X21,X24))
=> ? [X25] :
( mem(X25,X9)
& ~ p(ap(X21,ap(X20,X25))) ) ) ) )
& ! [X26] :
( mem(X26,arr(X9,X10))
=> ! [X27] :
( mem(X27,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X9,X10),X26),X27))
<=> ! [X28] :
( mem(X28,X9)
=> p(ap(X27,ap(X26,X28))) ) ) ) )
& ! [X29] :
( mem(X29,arr(X9,X10))
=> ! [X30] :
( mem(X30,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X9,X10),X29),X30))
<=> ! [X31] :
( mem(X31,X9)
=> ~ p(ap(X30,ap(X29,X31))) ) ) ) )
& ! [X32] :
( mem(X32,arr(X9,X10))
=> ! [X33] :
( mem(X33,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X9,X10),X32),X33))
<=> ! [X34] :
( mem(X34,X10)
=> ( p(ap(X33,X34))
=> ? [X35] :
( mem(X35,X9)
& X34 = ap(X32,X35) ) ) ) ) ) )
& ! [X36] :
( mem(X36,arr(X9,X10))
=> ! [X37] :
( mem(X37,arr(X10,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X9,X10),X36),X37))
<=> ! [X38] :
( mem(X38,X10)
=> ( ~ p(ap(X37,X38))
=> ? [X39] :
( mem(X39,X9)
& X38 = ap(X36,X39) ) ) ) ) ) ) ) ),
inference(split_equiv,[status(thm)],[i_0_38]) ).
fof(i_0_43,plain,
! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> ! [X20] :
( mem(X20,arr(X9,X10))
=> ! [X21] :
( mem(X21,arr(X10,bool))
=> epred1_4(X9,X10,X20,X21) ) ) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[conj_thm_2EquantHeuristics_2EGUESS__REWRITES]),c_0_38]) ).
fof(i_0_44,negated_conjecture,
~ ! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> ! [X20] :
( mem(X20,arr(X10,X9))
=> ! [X21] :
( mem(X21,arr(X9,bool))
=> ! [X45] :
( mem(X45,arr(X9,bool))
=> ( ! [X46] :
( mem(X46,X9)
=> ( p(ap(X45,X46))
=> p(ap(X21,X46)) ) )
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X10,X9),X20),X21))
=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X10,X9),X20),X45)) ) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT]) ).
fof(i_0_45,plain,
! [X228,X229,X230] :
( ( epred2_3(X228,X229,X230)
| ~ p(X229)
| ~ p(X230)
| ~ p(X228)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( p(X230)
| ~ p(X229)
| ~ p(X228)
| ~ p(X229)
| ~ p(X230)
| ~ p(X228)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( epred2_3(X228,X229,X230)
| p(X229)
| p(X230)
| ~ p(X228)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( p(X230)
| ~ p(X229)
| ~ p(X228)
| p(X229)
| p(X230)
| ~ p(X228)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( epred2_3(X228,X229,X230)
| ~ p(X229)
| p(X230)
| p(X228)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( p(X230)
| ~ p(X229)
| ~ p(X228)
| ~ p(X229)
| p(X230)
| p(X228)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( epred2_3(X228,X229,X230)
| ~ p(X230)
| p(X229)
| p(X228)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( p(X230)
| ~ p(X229)
| ~ p(X228)
| ~ p(X230)
| p(X229)
| p(X228)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( ~ p(X229)
| p(X230)
| ~ p(X228)
| ~ p(X230)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( ~ p(X230)
| p(X229)
| ~ p(X228)
| ~ p(X230)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( ~ p(X229)
| ~ p(X230)
| p(X228)
| ~ p(X230)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( p(X229)
| p(X230)
| p(X228)
| ~ p(X230)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( ~ p(X229)
| p(X230)
| ~ p(X228)
| p(X229)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( ~ p(X230)
| p(X229)
| ~ p(X228)
| p(X229)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( ~ p(X229)
| ~ p(X230)
| p(X228)
| p(X229)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( p(X229)
| p(X230)
| p(X228)
| p(X229)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( ~ p(X229)
| p(X230)
| ~ p(X228)
| p(X228)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( ~ p(X230)
| p(X229)
| ~ p(X228)
| p(X228)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( ~ p(X229)
| ~ p(X230)
| p(X228)
| p(X228)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) )
& ( p(X229)
| p(X230)
| p(X228)
| p(X228)
| ~ epred2_3(X228,X229,X230)
| ~ mem(X230,bool)
| ~ mem(X229,bool)
| ~ mem(X228,bool) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_39])])])]) ).
fof(i_0_46,plain,
! [X42] :
( mem(X42,bool)
=> ! [X43] :
( mem(X43,bool)
=> ! [X44] :
( mem(X44,bool)
=> epred4_3(X42,X43,X44) ) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[conj_thm_2Esat_2Edc__imp]),c_0_40]) ).
fof(i_0_47,plain,
! [X42] :
( mem(X42,bool)
=> ! [X43] :
( mem(X43,bool)
=> ! [X44] :
( mem(X44,bool)
=> epred3_3(X42,X43,X44) ) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[conj_thm_2Esat_2Edc__disj]),c_0_41]) ).
fof(i_0_48,plain,
! [X5] :
( mem(X5,bool)
=> ( p(ap(c_2Ebool_2E_7E,X5))
<=> ~ p(X5) ) ),
inference(fof_simplification,[status(thm)],[ax_neg_p]) ).
fof(i_0_49,plain,
! [X281,X282,X283] :
( ( p(X283)
| p(X282)
| p(X281)
| ~ epred2_3(X283,X282,X281) )
& ( p(X283)
| ~ p(X281)
| ~ p(X282)
| ~ epred2_3(X283,X282,X281) )
& ( p(X282)
| ~ p(X281)
| ~ p(X283)
| ~ epred2_3(X283,X282,X281) )
& ( ~ p(X282)
| ~ p(X283)
| ~ p(X283)
| epred2_3(X283,X282,X281) )
& ( p(X281)
| ~ p(X283)
| ~ p(X283)
| epred2_3(X283,X282,X281) )
& ( p(X283)
| ~ p(X283)
| ~ p(X283)
| epred2_3(X283,X282,X281) )
& ( ~ p(X282)
| p(X281)
| ~ p(X283)
| epred2_3(X283,X282,X281) )
& ( p(X281)
| p(X281)
| ~ p(X283)
| epred2_3(X283,X282,X281) )
& ( p(X283)
| p(X281)
| ~ p(X283)
| epred2_3(X283,X282,X281) )
& ( ~ p(X282)
| p(X282)
| ~ p(X283)
| epred2_3(X283,X282,X281) )
& ( p(X281)
| p(X282)
| ~ p(X283)
| epred2_3(X283,X282,X281) )
& ( p(X283)
| p(X282)
| ~ p(X283)
| epred2_3(X283,X282,X281) )
& ( ~ p(X282)
| ~ p(X283)
| ~ p(X282)
| epred2_3(X283,X282,X281) )
& ( p(X281)
| ~ p(X283)
| ~ p(X282)
| epred2_3(X283,X282,X281) )
& ( p(X283)
| ~ p(X283)
| ~ p(X282)
| epred2_3(X283,X282,X281) )
& ( ~ p(X282)
| p(X281)
| ~ p(X282)
| epred2_3(X283,X282,X281) )
& ( p(X281)
| p(X281)
| ~ p(X282)
| epred2_3(X283,X282,X281) )
& ( p(X283)
| p(X281)
| ~ p(X282)
| epred2_3(X283,X282,X281) )
& ( ~ p(X282)
| p(X282)
| ~ p(X282)
| epred2_3(X283,X282,X281) )
& ( p(X281)
| p(X282)
| ~ p(X282)
| epred2_3(X283,X282,X281) )
& ( p(X283)
| p(X282)
| ~ p(X282)
| epred2_3(X283,X282,X281) )
& ( ~ p(X282)
| ~ p(X283)
| ~ p(X281)
| epred2_3(X283,X282,X281) )
& ( p(X281)
| ~ p(X283)
| ~ p(X281)
| epred2_3(X283,X282,X281) )
& ( p(X283)
| ~ p(X283)
| ~ p(X281)
| epred2_3(X283,X282,X281) )
& ( ~ p(X282)
| p(X281)
| ~ p(X281)
| epred2_3(X283,X282,X281) )
& ( p(X281)
| p(X281)
| ~ p(X281)
| epred2_3(X283,X282,X281) )
& ( p(X283)
| p(X281)
| ~ p(X281)
| epred2_3(X283,X282,X281) )
& ( ~ p(X282)
| p(X282)
| ~ p(X281)
| epred2_3(X283,X282,X281) )
& ( p(X281)
| p(X282)
| ~ p(X281)
| epred2_3(X283,X282,X281) )
& ( p(X283)
| p(X282)
| ~ p(X281)
| epred2_3(X283,X282,X281) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_37])])]) ).
fof(i_0_50,plain,
! [X249,X250,X251,X252,X253,X256,X257,X260,X261,X262,X263,X265,X266,X267,X269,X270,X271,X274,X275,X276,X277,X280] :
( ( mem(esk9_5(X249,X250,X251,X252,X253),X252)
| ~ p(ap(X249,X253))
| ~ mem(X253,X251)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X252,X251),X250),X249))
| ~ epred1_4(X252,X251,X250,X249) )
& ( p(ap(X249,ap(X250,esk9_5(X249,X250,X251,X252,X253))))
| ~ p(ap(X249,X253))
| ~ mem(X253,X251)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X252,X251),X250),X249))
| ~ epred1_4(X252,X251,X250,X249) )
& ( mem(esk10_4(X249,X250,X251,X252),X251)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X252,X251),X250),X249))
| ~ epred1_4(X252,X251,X250,X249) )
& ( p(ap(X249,esk10_4(X249,X250,X251,X252)))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X252,X251),X250),X249))
| ~ epred1_4(X252,X251,X250,X249) )
& ( ~ mem(X256,X252)
| ~ p(ap(X249,ap(X250,X256)))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X252,X251),X250),X249))
| ~ epred1_4(X252,X251,X250,X249) )
& ( mem(esk11_5(X249,X250,X251,X252,X257),X252)
| p(ap(X249,X257))
| ~ mem(X257,X251)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X252,X251),X250),X249))
| ~ epred1_4(X252,X251,X250,X249) )
& ( ~ p(ap(X249,ap(X250,esk11_5(X249,X250,X251,X252,X257))))
| p(ap(X249,X257))
| ~ mem(X257,X251)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X252,X251),X250),X249))
| ~ epred1_4(X252,X251,X250,X249) )
& ( mem(esk12_4(X249,X250,X251,X252),X251)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X252,X251),X250),X249))
| ~ epred1_4(X252,X251,X250,X249) )
& ( ~ p(ap(X249,esk12_4(X249,X250,X251,X252)))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X252,X251),X250),X249))
| ~ epred1_4(X252,X251,X250,X249) )
& ( ~ mem(X260,X252)
| p(ap(X249,ap(X250,X260)))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X252,X251),X250),X249))
| ~ epred1_4(X252,X251,X250,X249) )
& ( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X252,X251),X261),X262))
| ~ mem(X263,X252)
| p(ap(X262,ap(X261,X263)))
| ~ mem(X262,arr(X251,bool))
| ~ mem(X261,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( mem(esk13_6(X249,X250,X251,X252,X261,X262),X252)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X252,X251),X261),X262))
| ~ mem(X262,arr(X251,bool))
| ~ mem(X261,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( ~ p(ap(X262,ap(X261,esk13_6(X249,X250,X251,X252,X261,X262))))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X252,X251),X261),X262))
| ~ mem(X262,arr(X251,bool))
| ~ mem(X261,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X252,X251),X265),X266))
| ~ mem(X267,X252)
| ~ p(ap(X266,ap(X265,X267)))
| ~ mem(X266,arr(X251,bool))
| ~ mem(X265,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( mem(esk14_6(X249,X250,X251,X252,X265,X266),X252)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X252,X251),X265),X266))
| ~ mem(X266,arr(X251,bool))
| ~ mem(X265,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( p(ap(X266,ap(X265,esk14_6(X249,X250,X251,X252,X265,X266))))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X252,X251),X265),X266))
| ~ mem(X266,arr(X251,bool))
| ~ mem(X265,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( mem(esk15_7(X249,X250,X251,X252,X269,X270,X271),X252)
| ~ p(ap(X270,X271))
| ~ mem(X271,X251)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X252,X251),X269),X270))
| ~ mem(X270,arr(X251,bool))
| ~ mem(X269,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( X271 = ap(X269,esk15_7(X249,X250,X251,X252,X269,X270,X271))
| ~ p(ap(X270,X271))
| ~ mem(X271,X251)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X252,X251),X269),X270))
| ~ mem(X270,arr(X251,bool))
| ~ mem(X269,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( mem(esk16_6(X249,X250,X251,X252,X269,X270),X251)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X252,X251),X269),X270))
| ~ mem(X270,arr(X251,bool))
| ~ mem(X269,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( p(ap(X270,esk16_6(X249,X250,X251,X252,X269,X270)))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X252,X251),X269),X270))
| ~ mem(X270,arr(X251,bool))
| ~ mem(X269,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( ~ mem(X274,X252)
| esk16_6(X249,X250,X251,X252,X269,X270) != ap(X269,X274)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X252,X251),X269),X270))
| ~ mem(X270,arr(X251,bool))
| ~ mem(X269,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( mem(esk17_7(X249,X250,X251,X252,X275,X276,X277),X252)
| p(ap(X276,X277))
| ~ mem(X277,X251)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X252,X251),X275),X276))
| ~ mem(X276,arr(X251,bool))
| ~ mem(X275,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( X277 = ap(X275,esk17_7(X249,X250,X251,X252,X275,X276,X277))
| p(ap(X276,X277))
| ~ mem(X277,X251)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X252,X251),X275),X276))
| ~ mem(X276,arr(X251,bool))
| ~ mem(X275,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( mem(esk18_6(X249,X250,X251,X252,X275,X276),X251)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X252,X251),X275),X276))
| ~ mem(X276,arr(X251,bool))
| ~ mem(X275,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( ~ p(ap(X276,esk18_6(X249,X250,X251,X252,X275,X276)))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X252,X251),X275),X276))
| ~ mem(X276,arr(X251,bool))
| ~ mem(X275,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) )
& ( ~ mem(X280,X252)
| esk18_6(X249,X250,X251,X252,X275,X276) != ap(X275,X280)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X252,X251),X275),X276))
| ~ mem(X276,arr(X251,bool))
| ~ mem(X275,arr(X252,X251))
| ~ epred1_4(X252,X251,X250,X249) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_42])])])])]) ).
fof(i_0_51,plain,
! [X167,X168,X169,X170] :
( ( mem(esk1_4(X167,X168,X169,X170),X167)
| X169 = X170
| ~ mem(X170,arr(X167,X168))
| ~ mem(X169,arr(X167,X168)) )
& ( ap(X169,esk1_4(X167,X168,X169,X170)) != ap(X170,esk1_4(X167,X168,X169,X170))
| X169 = X170
| ~ mem(X170,arr(X167,X168))
| ~ mem(X169,arr(X167,X168)) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[funcext])])])])]) ).
fof(i_0_52,plain,
! [X220,X221,X222,X223] :
( ~ ne(X220)
| ~ ne(X221)
| ~ mem(X222,arr(X220,X221))
| ~ mem(X223,arr(X221,bool))
| epred1_4(X220,X221,X222,X223) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_43])])]) ).
fof(i_0_53,plain,
! [X192,X193] :
( ~ ne(X192)
| ~ ne(X193)
| mem(c_2EquantHeuristics_2EGUESS__EXISTS(X192,X193),arr(arr(X192,X193),arr(arr(X193,bool),bool))) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2EquantHeuristics_2EGUESS__EXISTS])])]) ).
fof(i_0_54,plain,
! [X185,X186] :
( ~ ne(X185)
| ~ ne(X186)
| mem(c_2EquantHeuristics_2EGUESS__FORALL(X185,X186),arr(arr(X185,X186),arr(arr(X186,bool),bool))) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2EquantHeuristics_2EGUESS__FORALL])])]) ).
fof(i_0_55,plain,
! [X183,X184] :
( ~ ne(X183)
| ~ ne(X184)
| mem(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X183,X184),arr(arr(X183,X184),arr(arr(X184,bool),bool))) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2EquantHeuristics_2EGUESS__EXISTS__POINT])])]) ).
fof(i_0_56,plain,
! [X181,X182] :
( ~ ne(X181)
| ~ ne(X182)
| mem(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X181,X182),arr(arr(X181,X182),arr(arr(X182,bool),bool))) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2EquantHeuristics_2EGUESS__FORALL__POINT])])]) ).
fof(i_0_57,plain,
! [X179,X180] :
( ~ ne(X179)
| ~ ne(X180)
| mem(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X179,X180),arr(arr(X179,X180),arr(arr(X180,bool),bool))) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2EquantHeuristics_2EGUESS__EXISTS__GAP])])]) ).
fof(i_0_58,plain,
! [X177,X178] :
( ~ ne(X177)
| ~ ne(X178)
| mem(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X177,X178),arr(arr(X177,X178),arr(arr(X178,bool),bool))) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2EquantHeuristics_2EGUESS__FORALL__GAP])])]) ).
fof(i_0_59,negated_conjecture,
! [X248] :
( ne(esk4_0)
& ne(esk5_0)
& mem(esk6_0,arr(esk5_0,esk4_0))
& mem(esk7_0,arr(esk4_0,bool))
& mem(esk8_0,arr(esk4_0,bool))
& ( ~ mem(X248,esk4_0)
| ~ p(ap(esk8_0,X248))
| p(ap(esk7_0,X248)) )
& p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk7_0))
& ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk8_0)) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_44])])])]) ).
fof(i_0_60,plain,
! [X206,X207,X208] :
( ( ~ p(ap(c_2Ebool_2E_21(X206),X207))
| ~ mem(X208,X206)
| p(ap(X207,X208))
| ~ mem(X207,arr(X206,bool))
| ~ ne(X206) )
& ( mem(esk3_2(X206,X207),X206)
| p(ap(c_2Ebool_2E_21(X206),X207))
| ~ mem(X207,arr(X206,bool))
| ~ ne(X206) )
& ( ~ p(ap(X207,esk3_2(X206,X207)))
| p(ap(c_2Ebool_2E_21(X206),X207))
| ~ mem(X207,arr(X206,bool))
| ~ ne(X206) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_all_p])])])])]) ).
fof(i_0_61,plain,
! [X199,X200,X201] :
( ( ~ p(ap(ap(c_2Emin_2E_3D(X199),X200),X201))
| X200 = X201
| ~ mem(X201,X199)
| ~ mem(X200,X199)
| ~ ne(X199) )
& ( X200 != X201
| p(ap(ap(c_2Emin_2E_3D(X199),X200),X201))
| ~ mem(X201,X199)
| ~ mem(X200,X199)
| ~ ne(X199) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_eq_p])])])]) ).
fof(i_0_62,plain,
! [X188,X189,X191] :
( ( mem(esk2_2(X188,X189),X188)
| ~ p(ap(c_2Ebool_2E_3F(X188),X189))
| ~ mem(X189,arr(X188,bool))
| ~ ne(X188) )
& ( p(ap(X189,esk2_2(X188,X189)))
| ~ p(ap(c_2Ebool_2E_3F(X188),X189))
| ~ mem(X189,arr(X188,bool))
| ~ ne(X188) )
& ( ~ mem(X191,X188)
| ~ p(ap(X189,X191))
| p(ap(c_2Ebool_2E_3F(X188),X189))
| ~ mem(X189,arr(X188,bool))
| ~ ne(X188) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_ex_p])])])])]) ).
fof(i_0_63,plain,
! [X203,X204] :
( ( ~ p(ap(ap(c_2Emin_2E_3D_3D_3E,X203),X204))
| ~ p(X203)
| p(X204)
| ~ mem(X204,bool)
| ~ mem(X203,bool) )
& ( p(X203)
| p(ap(ap(c_2Emin_2E_3D_3D_3E,X203),X204))
| ~ mem(X204,bool)
| ~ mem(X203,bool) )
& ( ~ p(X204)
| p(ap(ap(c_2Emin_2E_3D_3D_3E,X203),X204))
| ~ mem(X204,bool)
| ~ mem(X203,bool) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_imp_p])])])]) ).
fof(i_0_64,plain,
! [X194,X195] :
( ( ~ p(ap(ap(c_2Ebool_2E_5C_2F,X194),X195))
| p(X194)
| p(X195)
| ~ mem(X195,bool)
| ~ mem(X194,bool) )
& ( ~ p(X194)
| p(ap(ap(c_2Ebool_2E_5C_2F,X194),X195))
| ~ mem(X195,bool)
| ~ mem(X194,bool) )
& ( ~ p(X195)
| p(ap(ap(c_2Ebool_2E_5C_2F,X194),X195))
| ~ mem(X195,bool)
| ~ mem(X194,bool) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_or_p])])])]) ).
cnf(i_0_65,plain,
( p(X2)
| ~ p(X1)
| ~ p(X3)
| ~ p(X1)
| ~ epred2_3(X3,X2,X1)
| ~ mem(X1,bool)
| ~ mem(X2,bool)
| ~ mem(X3,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]) ).
cnf(i_0_66,plain,
( p(X2)
| p(X2)
| ~ p(X1)
| ~ p(X3)
| ~ epred2_3(X3,X2,X1)
| ~ mem(X1,bool)
| ~ mem(X2,bool)
| ~ mem(X3,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]) ).
cnf(i_0_67,plain,
( p(X3)
| ~ p(X1)
| ~ p(X2)
| ~ p(X2)
| ~ epred2_3(X3,X1,X2)
| ~ mem(X2,bool)
| ~ mem(X1,bool)
| ~ mem(X3,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]) ).
cnf(i_0_68,plain,
( p(X3)
| p(X3)
| ~ p(X1)
| ~ p(X2)
| ~ epred2_3(X3,X1,X2)
| ~ mem(X2,bool)
| ~ mem(X1,bool)
| ~ mem(X3,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]) ).
fof(i_0_69,plain,
! [X196,X197] :
( ( p(X196)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,X196),X197))
| ~ mem(X197,bool)
| ~ mem(X196,bool) )
& ( p(X197)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,X196),X197))
| ~ mem(X197,bool)
| ~ mem(X196,bool) )
& ( ~ p(X196)
| ~ p(X197)
| p(ap(ap(c_2Ebool_2E_2F_5C,X196),X197))
| ~ mem(X197,bool)
| ~ mem(X196,bool) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_and_p])])])]) ).
cnf(i_0_70,plain,
( p(X1)
| p(X2)
| p(X3)
| p(X1)
| ~ epred2_3(X3,X1,X2)
| ~ mem(X2,bool)
| ~ mem(X1,bool)
| ~ mem(X3,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]) ).
cnf(i_0_71,plain,
( p(X1)
| p(X2)
| p(X3)
| p(X3)
| ~ epred2_3(X3,X1,X2)
| ~ mem(X2,bool)
| ~ mem(X1,bool)
| ~ mem(X3,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]) ).
fof(i_0_72,plain,
! [X161,X162,X163,X164] :
( ~ mem(X163,arr(X161,X162))
| ~ mem(X164,X161)
| mem(ap(X163,X164),X162) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ap_tp])])]) ).
fof(i_0_73,plain,
! [X234,X235,X236] :
( ~ mem(X234,bool)
| ~ mem(X235,bool)
| ~ mem(X236,bool)
| epred4_3(X234,X235,X236) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_46])])]) ).
fof(i_0_74,plain,
! [X231,X232,X233] :
( ~ mem(X231,bool)
| ~ mem(X232,bool)
| ~ mem(X233,bool)
| epred3_3(X231,X232,X233) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_47])])]) ).
fof(i_0_75,plain,
! [X198] :
( ~ ne(X198)
| mem(c_2Emin_2E_3D(X198),arr(X198,arr(X198,bool))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Emin_2E_3D])]) ).
fof(i_0_76,plain,
! [X205] :
( ~ ne(X205)
| mem(c_2Ebool_2E_21(X205),arr(arr(X205,bool),bool)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Ebool_2E_21])]) ).
fof(i_0_77,plain,
! [X187] :
( ~ ne(X187)
| mem(c_2Ebool_2E_3F(X187),arr(arr(X187,bool),bool)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Ebool_2E_3F])]) ).
fof(i_0_78,plain,
! [X202] :
( ( ~ p(ap(c_2Ebool_2E_7E,X202))
| ~ p(X202)
| ~ mem(X202,bool) )
& ( p(X202)
| p(ap(c_2Ebool_2E_7E,X202))
| ~ mem(X202,bool) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_48])])]) ).
cnf(i_0_79,plain,
( epred2_3(X2,X1,X3)
| ~ p(X1)
| ~ p(X2)
| ~ p(X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]) ).
cnf(i_0_80,plain,
( epred2_3(X2,X1,X3)
| ~ p(X1)
| ~ p(X2)
| ~ p(X1) ),
inference(split_conjunct,[status(thm)],[i_0_49]) ).
cnf(i_0_81,plain,
( p(X1)
| epred2_3(X2,X3,X1)
| ~ p(X2)
| ~ p(X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]) ).
cnf(i_0_82,plain,
( p(X1)
| p(X1)
| epred2_3(X2,X3,X1)
| ~ p(X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]) ).
cnf(i_0_83,plain,
( p(X1)
| p(X1)
| epred2_3(X3,X2,X1)
| ~ p(X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]) ).
cnf(i_0_84,plain,
( p(X2)
| epred2_3(X3,X1,X2)
| ~ p(X1)
| ~ p(X1) ),
inference(split_conjunct,[status(thm)],[i_0_49]) ).
fof(i_0_85,plain,
! [X172,X173,X174] :
( ~ mem(X174,X172)
| ap(k(X172,X173),X174) = X173 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kbeta])]) ).
fof(i_0_86,plain,
! [X165,X166] :
( ( ~ p(X165)
| ~ p(X166)
| X165 = X166
| ~ mem(X166,bool)
| ~ mem(X165,bool) )
& ( p(X165)
| p(X166)
| X165 = X166
| ~ mem(X166,bool)
| ~ mem(X165,bool) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[boolext])])])]) ).
fof(i_0_87,plain,
! [X159,X160] :
( ~ ne(X159)
| ~ ne(X160)
| ne(arr(X159,X160)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arr_ne])])]) ).
fof(i_0_88,plain,
! [X175,X176] :
( ~ mem(X176,X175)
| ap(i(X175),X176) = X176 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ibeta])]) ).
fof(i_0_89,plain,
~ p(c_2Ebool_2EF),
inference(fof_simplification,[status(thm)],[ax_false_p]) ).
cnf(i_0_90,plain,
( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X6,X5),X2),X1))
| ~ p(ap(X1,ap(X2,esk13_6(X3,X4,X5,X6,X2,X1))))
| ~ mem(X1,arr(X5,bool))
| ~ mem(X2,arr(X6,X5))
| ~ epred1_4(X6,X5,X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_91,plain,
( X1 = ap(X2,esk15_7(X3,X4,X5,X6,X2,X7,X1))
| ~ p(ap(X7,X1))
| ~ mem(X1,X5)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X6,X5),X2),X7))
| ~ mem(X7,arr(X5,bool))
| ~ mem(X2,arr(X6,X5))
| ~ epred1_4(X6,X5,X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_92,plain,
( mem(esk15_7(X1,X2,X3,X4,X5,X6,X7),X4)
| ~ p(ap(X6,X7))
| ~ mem(X7,X3)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X4,X3),X5),X6))
| ~ mem(X6,arr(X3,bool))
| ~ mem(X5,arr(X4,X3))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_93,plain,
( X1 = ap(X2,esk17_7(X3,X4,X5,X6,X2,X7,X1))
| p(ap(X7,X1))
| ~ mem(X1,X5)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X6,X5),X2),X7))
| ~ mem(X7,arr(X5,bool))
| ~ mem(X2,arr(X6,X5))
| ~ epred1_4(X6,X5,X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_94,plain,
( mem(esk17_7(X1,X2,X3,X4,X5,X6,X7),X4)
| p(ap(X6,X7))
| ~ mem(X7,X3)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X4,X3),X5),X6))
| ~ mem(X6,arr(X3,bool))
| ~ mem(X5,arr(X4,X3))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_95,plain,
( p(ap(X1,ap(X2,esk14_6(X3,X4,X5,X6,X2,X1))))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X6,X5),X2),X1))
| ~ mem(X1,arr(X5,bool))
| ~ mem(X2,arr(X6,X5))
| ~ epred1_4(X6,X5,X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_96,plain,
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X5,X4),X6),X1))
| ~ p(ap(X1,esk18_6(X2,X3,X4,X5,X6,X1)))
| ~ mem(X1,arr(X4,bool))
| ~ mem(X6,arr(X5,X4))
| ~ epred1_4(X5,X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_97,plain,
( p(ap(X1,esk16_6(X2,X3,X4,X5,X6,X1)))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X5,X4),X6),X1))
| ~ mem(X1,arr(X4,bool))
| ~ mem(X6,arr(X5,X4))
| ~ epred1_4(X5,X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_98,plain,
( p(ap(X1,X5))
| ~ p(ap(X1,ap(X2,esk11_5(X1,X2,X3,X4,X5))))
| ~ mem(X5,X3)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X4,X3),X2),X1))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_99,plain,
( mem(esk18_6(X1,X2,X3,X4,X5,X6),X3)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X4,X3),X5),X6))
| ~ mem(X6,arr(X3,bool))
| ~ mem(X5,arr(X4,X3))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_100,plain,
( mem(esk16_6(X1,X2,X3,X4,X5,X6),X3)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X4,X3),X5),X6))
| ~ mem(X6,arr(X3,bool))
| ~ mem(X5,arr(X4,X3))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_101,plain,
( mem(esk14_6(X1,X2,X3,X4,X5,X6),X4)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X4,X3),X5),X6))
| ~ mem(X6,arr(X3,bool))
| ~ mem(X5,arr(X4,X3))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_102,plain,
( mem(esk13_6(X1,X2,X3,X4,X5,X6),X4)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X4,X3),X5),X6))
| ~ mem(X6,arr(X3,bool))
| ~ mem(X5,arr(X4,X3))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_103,plain,
( p(ap(X1,ap(X2,esk9_5(X1,X2,X3,X4,X5))))
| ~ p(ap(X1,X5))
| ~ mem(X5,X3)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X4,X3),X2),X1))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_104,plain,
( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X2,X5),X6),X7))
| ~ mem(X1,X2)
| esk16_6(X3,X4,X5,X2,X6,X7) != ap(X6,X1)
| ~ mem(X7,arr(X5,bool))
| ~ mem(X6,arr(X2,X5))
| ~ epred1_4(X2,X5,X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_105,plain,
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X2,X5),X6),X7))
| ~ mem(X1,X2)
| esk18_6(X3,X4,X5,X2,X6,X7) != ap(X6,X1)
| ~ mem(X7,arr(X5,bool))
| ~ mem(X6,arr(X2,X5))
| ~ epred1_4(X2,X5,X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_106,plain,
( mem(esk9_5(X1,X2,X3,X4,X5),X4)
| ~ p(ap(X1,X5))
| ~ mem(X5,X3)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X4,X3),X2),X1))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_107,plain,
( mem(esk11_5(X1,X2,X3,X4,X5),X4)
| p(ap(X1,X5))
| ~ mem(X5,X3)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X4,X3),X2),X1))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_108,plain,
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X4,X3),X2),X1))
| ~ p(ap(X1,esk12_4(X1,X2,X3,X4)))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_109,plain,
( X1 = X4
| ap(X1,esk1_4(X2,X3,X1,X4)) != ap(X4,esk1_4(X2,X3,X1,X4))
| ~ mem(X4,arr(X2,X3))
| ~ mem(X1,arr(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_110,plain,
( p(ap(X1,esk10_4(X1,X2,X3,X4)))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X4,X3),X2),X1))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_111,plain,
( mem(esk12_4(X1,X2,X3,X4),X3)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X4,X3),X2),X1))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_112,plain,
( mem(esk10_4(X1,X2,X3,X4),X3)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X4,X3),X2),X1))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_113,plain,
( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),X3),X4))
| ~ mem(X5,X1)
| ~ p(ap(X4,ap(X3,X5)))
| ~ mem(X4,arr(X2,bool))
| ~ mem(X3,arr(X1,X2))
| ~ epred1_4(X1,X2,X6,X7) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_114,plain,
( p(ap(X4,ap(X3,X5)))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X1,X2),X3),X4))
| ~ mem(X5,X1)
| ~ mem(X4,arr(X2,bool))
| ~ mem(X3,arr(X1,X2))
| ~ epred1_4(X1,X2,X6,X7) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_115,plain,
( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X2,X5),X4),X3))
| ~ mem(X1,X2)
| ~ p(ap(X3,ap(X4,X1)))
| ~ epred1_4(X2,X5,X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_116,plain,
( p(ap(X3,ap(X4,X1)))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X2,X5),X4),X3))
| ~ mem(X1,X2)
| ~ epred1_4(X2,X5,X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_117,plain,
( mem(esk1_4(X1,X2,X3,X4),X1)
| X3 = X4
| ~ mem(X4,arr(X1,X2))
| ~ mem(X3,arr(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_118,plain,
( epred1_4(X1,X2,X3,X4)
| ~ ne(X1)
| ~ ne(X2)
| ~ mem(X3,arr(X1,X2))
| ~ mem(X4,arr(X2,bool)) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_119,plain,
( mem(c_2EquantHeuristics_2EGUESS__EXISTS(X1,X2),arr(arr(X1,X2),arr(arr(X2,bool),bool)))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_120,plain,
( mem(c_2EquantHeuristics_2EGUESS__FORALL(X1,X2),arr(arr(X1,X2),arr(arr(X2,bool),bool)))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_121,plain,
( mem(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X1,X2),arr(arr(X1,X2),arr(arr(X2,bool),bool)))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_122,plain,
( mem(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),arr(arr(X1,X2),arr(arr(X2,bool),bool)))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_123,plain,
( mem(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X1,X2),arr(arr(X1,X2),arr(arr(X2,bool),bool)))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_124,plain,
( mem(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X1,X2),arr(arr(X1,X2),arr(arr(X2,bool),bool)))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_125,negated_conjecture,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk8_0)),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_126,plain,
( p(ap(c_2Ebool_2E_21(X2),X1))
| ~ p(ap(X1,esk3_2(X2,X1)))
| ~ mem(X1,arr(X2,bool))
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_127,plain,
( X2 = X3
| ~ p(ap(ap(c_2Emin_2E_3D(X1),X2),X3))
| ~ mem(X3,X1)
| ~ mem(X2,X1)
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_128,plain,
( p(ap(X1,esk2_2(X2,X1)))
| ~ p(ap(c_2Ebool_2E_3F(X2),X1))
| ~ mem(X1,arr(X2,bool))
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_129,plain,
( p(ap(X2,X3))
| ~ p(ap(c_2Ebool_2E_21(X1),X2))
| ~ mem(X3,X1)
| ~ mem(X2,arr(X1,bool))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_130,plain,
( p(ap(c_2Ebool_2E_3F(X2),X3))
| ~ mem(X1,X2)
| ~ p(ap(X3,X1))
| ~ mem(X3,arr(X2,bool))
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_131,plain,
( mem(esk2_2(X1,X2),X1)
| ~ p(ap(c_2Ebool_2E_3F(X1),X2))
| ~ mem(X2,arr(X1,bool))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_132,plain,
( p(X2)
| ~ p(ap(ap(c_2Emin_2E_3D_3D_3E,X1),X2))
| ~ p(X1)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_133,plain,
( p(X1)
| p(X2)
| ~ p(ap(ap(c_2Ebool_2E_5C_2F,X1),X2))
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_134,plain,
( p(X2)
| ~ p(X3)
| ~ p(X1)
| ~ mem(X3,bool)
| ~ mem(X2,bool)
| ~ mem(X1,bool)
| ~ epred2_3(X3,X2,X1) ),
inference(cn,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_135,plain,
( p(X2)
| ~ p(X3)
| ~ p(X1)
| ~ mem(X3,bool)
| ~ mem(X2,bool)
| ~ mem(X1,bool)
| ~ epred2_3(X3,X2,X1) ),
inference(cn,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_136,plain,
( p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ mem(X3,bool)
| ~ mem(X2,bool)
| ~ mem(X1,bool)
| ~ epred2_3(X3,X1,X2) ),
inference(cn,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_137,plain,
( p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ mem(X3,bool)
| ~ mem(X2,bool)
| ~ mem(X1,bool)
| ~ epred2_3(X3,X1,X2) ),
inference(cn,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_138,plain,
( p(X1)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,X1),X2))
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_139,plain,
( p(X1)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,X2),X1))
| ~ mem(X1,bool)
| ~ mem(X2,bool) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_140,plain,
( p(ap(ap(c_2Emin_2E_3D(X3),X1),X2))
| X1 != X2
| ~ mem(X2,X3)
| ~ mem(X1,X3)
| ~ ne(X3) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_141,plain,
( p(X3)
| p(X2)
| p(X1)
| ~ mem(X3,bool)
| ~ mem(X2,bool)
| ~ mem(X1,bool)
| ~ epred2_3(X3,X1,X2) ),
inference(cn,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_142,plain,
( p(X3)
| p(X2)
| p(X1)
| ~ mem(X3,bool)
| ~ mem(X2,bool)
| ~ mem(X1,bool)
| ~ epred2_3(X3,X1,X2) ),
inference(cn,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_143,negated_conjecture,
p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk7_0)),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_144,plain,
( mem(esk3_2(X1,X2),X1)
| p(ap(c_2Ebool_2E_21(X1),X2))
| ~ mem(X2,arr(X1,bool))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_145,plain,
( epred2_3(X1,X2,X3)
| ~ p(X2)
| ~ p(X3)
| ~ p(X1)
| ~ mem(X3,bool)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_146,plain,
( epred2_3(X1,X2,X3)
| p(X2)
| p(X1)
| ~ p(X3)
| ~ mem(X3,bool)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_147,plain,
( epred2_3(X1,X2,X3)
| p(X3)
| p(X1)
| ~ p(X2)
| ~ mem(X3,bool)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_148,plain,
( epred2_3(X1,X2,X3)
| p(X2)
| p(X3)
| ~ p(X1)
| ~ mem(X3,bool)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_149,plain,
( p(ap(ap(c_2Ebool_2E_2F_5C,X1),X2))
| ~ p(X1)
| ~ p(X2)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_150,plain,
( mem(ap(X1,X4),X3)
| ~ mem(X1,arr(X2,X3))
| ~ mem(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_151,plain,
( p(ap(ap(c_2Emin_2E_3D_3D_3E,X2),X1))
| ~ p(X1)
| ~ mem(X1,bool)
| ~ mem(X2,bool) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_152,plain,
( p(ap(ap(c_2Ebool_2E_5C_2F,X1),X2))
| ~ p(X1)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_153,plain,
( p(ap(ap(c_2Ebool_2E_5C_2F,X2),X1))
| ~ p(X1)
| ~ mem(X1,bool)
| ~ mem(X2,bool) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_154,plain,
( p(X1)
| p(ap(ap(c_2Emin_2E_3D_3D_3E,X1),X2))
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_155,plain,
( epred4_3(X1,X2,X3)
| ~ mem(X1,bool)
| ~ mem(X2,bool)
| ~ mem(X3,bool) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_156,plain,
( epred3_3(X1,X2,X3)
| ~ mem(X1,bool)
| ~ mem(X2,bool)
| ~ mem(X3,bool) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_157,plain,
( p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ epred2_3(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_158,plain,
( p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ epred2_3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_159,plain,
( p(X1)
| p(X2)
| p(X3)
| ~ epred2_3(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_160,plain,
( mem(c_2Emin_2E_3D(X1),arr(X1,arr(X1,bool)))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_161,plain,
( mem(c_2Ebool_2E_21(X1),arr(arr(X1,bool),bool))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_162,plain,
( mem(c_2Ebool_2E_3F(X1),arr(arr(X1,bool),bool))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_163,negated_conjecture,
( p(ap(esk7_0,X1))
| ~ mem(X1,esk4_0)
| ~ p(ap(esk8_0,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_164,plain,
( epred2_3(X2,X1,X3)
| ~ p(X1)
| ~ p(X2)
| ~ p(X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_165,plain,
mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool))),
inference(split_conjunct,[status(thm)],[mem_c_2Emin_2E_3D_3D_3E]),
[final] ).
cnf(i_0_166,plain,
mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool))),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2E_2F_5C]),
[final] ).
cnf(i_0_167,plain,
mem(c_2Ebool_2E_5C_2F,arr(bool,arr(bool,bool))),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2E_5C_2F]),
[final] ).
cnf(i_0_168,plain,
( p(X1)
| epred2_3(X2,X3,X1)
| ~ p(X2)
| ~ p(X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_169,plain,
( p(X2)
| epred2_3(X3,X1,X2)
| ~ p(X1)
| ~ p(X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_170,plain,
( p(X1)
| p(X2)
| epred2_3(X1,X2,X3)
| ~ p(X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_171,plain,
( p(X1)
| p(X2)
| epred2_3(X1,X3,X2)
| ~ p(X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_172,plain,
( p(X1)
| p(X2)
| epred2_3(X3,X2,X1)
| ~ p(X3) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_173,plain,
( ~ p(ap(c_2Ebool_2E_7E,X1))
| ~ p(X1)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_174,plain,
( epred2_3(X2,X1,X3)
| ~ p(X2)
| ~ p(X1) ),
inference(cn,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_175,plain,
( epred2_3(X2,X1,X3)
| ~ p(X2)
| ~ p(X1) ),
inference(cn,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_176,plain,
( p(X1)
| epred2_3(X2,X3,X1)
| ~ p(X2) ),
inference(cn,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_177,plain,
( p(X1)
| epred2_3(X2,X3,X1)
| ~ p(X2) ),
inference(cn,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_178,plain,
( p(X1)
| epred2_3(X3,X2,X1)
| ~ p(X2) ),
inference(cn,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_179,plain,
( p(X2)
| epred2_3(X3,X1,X2)
| ~ p(X1) ),
inference(cn,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_180,plain,
( ap(k(X2,X3),X1) = X3
| ~ mem(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_181,plain,
( X1 = X2
| ~ p(X1)
| ~ p(X2)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_182,plain,
( p(X1)
| p(ap(c_2Ebool_2E_7E,X1))
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_183,plain,
( p(X1)
| p(X2)
| X1 = X2
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_184,plain,
( ne(arr(X1,X2))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_185,plain,
( ap(i(X2),X1) = X1
| ~ mem(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_186,negated_conjecture,
mem(esk8_0,arr(esk4_0,bool)),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_187,negated_conjecture,
mem(esk7_0,arr(esk4_0,bool)),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_188,negated_conjecture,
mem(esk6_0,arr(esk5_0,esk4_0)),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_189,plain,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2E_7E]),
[final] ).
cnf(i_0_190,plain,
mem(c_2Ebool_2EF,bool),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2EF]),
[final] ).
cnf(i_0_191,plain,
mem(c_2Ebool_2ET,bool),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2ET]),
[final] ).
cnf(i_0_192,plain,
~ p(c_2Ebool_2EF),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_193,plain,
p(c_2Ebool_2ET),
inference(split_conjunct,[status(thm)],[ax_true_p]),
[final] ).
cnf(i_0_194,negated_conjecture,
ne(esk5_0),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_195,negated_conjecture,
ne(esk4_0),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_196,plain,
ne(ind),
inference(split_conjunct,[status(thm)],[ind_ne]),
[final] ).
cnf(i_0_197,plain,
ne(bool),
inference(split_conjunct,[status(thm)],[bool_ne]),
[final] ).
cnf(i_0_198,axiom,
X1 = X1 ).
cnf(i_0_199,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_200,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_201,axiom,
( X1 != X2
| ap(X1,X3) = ap(X2,X3) ) ).
cnf(i_0_202,axiom,
( X1 != X2
| ap(X3,X1) = ap(X3,X2) ) ).
cnf(i_0_203,axiom,
( X1 != X2
| esk18_6(X1,X3,X4,X5,X6,X7) = esk18_6(X2,X3,X4,X5,X6,X7) ) ).
cnf(i_0_204,axiom,
( X1 != X2
| esk18_6(X3,X1,X4,X5,X6,X7) = esk18_6(X3,X2,X4,X5,X6,X7) ) ).
cnf(i_0_205,axiom,
( X1 != X2
| esk18_6(X3,X4,X1,X5,X6,X7) = esk18_6(X3,X4,X2,X5,X6,X7) ) ).
cnf(i_0_206,axiom,
( X1 != X2
| esk18_6(X3,X4,X5,X1,X6,X7) = esk18_6(X3,X4,X5,X2,X6,X7) ) ).
cnf(i_0_207,axiom,
( X1 != X2
| esk18_6(X3,X4,X5,X6,X1,X7) = esk18_6(X3,X4,X5,X6,X2,X7) ) ).
cnf(i_0_208,axiom,
( X1 != X2
| esk18_6(X3,X4,X5,X6,X7,X1) = esk18_6(X3,X4,X5,X6,X7,X2) ) ).
cnf(i_0_209,axiom,
( X1 != X2
| esk16_6(X1,X3,X4,X5,X6,X7) = esk16_6(X2,X3,X4,X5,X6,X7) ) ).
cnf(i_0_210,axiom,
( X1 != X2
| esk16_6(X3,X1,X4,X5,X6,X7) = esk16_6(X3,X2,X4,X5,X6,X7) ) ).
cnf(i_0_211,axiom,
( X1 != X2
| esk16_6(X3,X4,X1,X5,X6,X7) = esk16_6(X3,X4,X2,X5,X6,X7) ) ).
cnf(i_0_212,axiom,
( X1 != X2
| esk16_6(X3,X4,X5,X1,X6,X7) = esk16_6(X3,X4,X5,X2,X6,X7) ) ).
cnf(i_0_213,axiom,
( X1 != X2
| esk16_6(X3,X4,X5,X6,X1,X7) = esk16_6(X3,X4,X5,X6,X2,X7) ) ).
cnf(i_0_214,axiom,
( X1 != X2
| esk16_6(X3,X4,X5,X6,X7,X1) = esk16_6(X3,X4,X5,X6,X7,X2) ) ).
cnf(i_0_215,axiom,
( X1 != X2
| ~ p(X1)
| p(X2) ) ).
cnf(i_0_216,axiom,
( X1 != X2
| ~ mem(X1,X3)
| mem(X2,X3) ) ).
cnf(i_0_217,axiom,
( X1 != X2
| ~ mem(X3,X1)
| mem(X3,X2) ) ).
cnf(i_0_218,axiom,
( X1 != X2
| ~ epred1_4(X1,X3,X4,X5)
| epred1_4(X2,X3,X4,X5) ) ).
cnf(i_0_219,axiom,
( X1 != X2
| ~ epred1_4(X3,X1,X4,X5)
| epred1_4(X3,X2,X4,X5) ) ).
cnf(i_0_220,axiom,
( X1 != X2
| ~ epred1_4(X3,X4,X1,X5)
| epred1_4(X3,X4,X2,X5) ) ).
cnf(i_0_221,axiom,
( X1 != X2
| ~ epred1_4(X3,X4,X5,X1)
| epred1_4(X3,X4,X5,X2) ) ).
cnf(i_0_222,axiom,
( X1 != X2
| ~ ne(X1)
| ne(X2) ) ).
cnf(i_0_223,axiom,
( X1 != X2
| ~ epred2_3(X1,X3,X4)
| epred2_3(X2,X3,X4) ) ).
cnf(i_0_224,axiom,
( X1 != X2
| ~ epred2_3(X3,X1,X4)
| epred2_3(X3,X2,X4) ) ).
cnf(i_0_225,axiom,
( X1 != X2
| ~ epred2_3(X3,X4,X1)
| epred2_3(X3,X4,X2) ) ).
cnf(i_0_226,axiom,
( X1 != X2
| ~ epred4_3(X1,X3,X4)
| epred4_3(X2,X3,X4) ) ).
cnf(i_0_227,axiom,
( X1 != X2
| ~ epred4_3(X3,X1,X4)
| epred4_3(X3,X2,X4) ) ).
cnf(i_0_228,axiom,
( X1 != X2
| ~ epred4_3(X3,X4,X1)
| epred4_3(X3,X4,X2) ) ).
cnf(i_0_229,axiom,
( X1 != X2
| ~ epred3_3(X1,X3,X4)
| epred3_3(X2,X3,X4) ) ).
cnf(i_0_230,axiom,
( X1 != X2
| ~ epred3_3(X3,X1,X4)
| epred3_3(X3,X2,X4) ) ).
cnf(i_0_231,axiom,
( X1 != X2
| ~ epred3_3(X3,X4,X1)
| epred3_3(X3,X4,X2) ) ).
cnf(i_0_198_001,axiom,
X1 = X1 ).
cnf(i_0_199_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_200_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_201_004,axiom,
( X1 != X2
| ap(X1,X3) = ap(X2,X3) ) ).
cnf(i_0_202_005,axiom,
( X1 != X2
| ap(X3,X1) = ap(X3,X2) ) ).
cnf(i_0_203_006,axiom,
( X1 != X2
| esk18_6(X1,X3,X4,X5,X6,X7) = esk18_6(X2,X3,X4,X5,X6,X7) ) ).
cnf(i_0_204_007,axiom,
( X1 != X2
| esk18_6(X3,X1,X4,X5,X6,X7) = esk18_6(X3,X2,X4,X5,X6,X7) ) ).
cnf(i_0_205_008,axiom,
( X1 != X2
| esk18_6(X3,X4,X1,X5,X6,X7) = esk18_6(X3,X4,X2,X5,X6,X7) ) ).
cnf(i_0_206_009,axiom,
( X1 != X2
| esk18_6(X3,X4,X5,X1,X6,X7) = esk18_6(X3,X4,X5,X2,X6,X7) ) ).
cnf(i_0_207_010,axiom,
( X1 != X2
| esk18_6(X3,X4,X5,X6,X1,X7) = esk18_6(X3,X4,X5,X6,X2,X7) ) ).
cnf(i_0_208_011,axiom,
( X1 != X2
| esk18_6(X3,X4,X5,X6,X7,X1) = esk18_6(X3,X4,X5,X6,X7,X2) ) ).
cnf(i_0_209_012,axiom,
( X1 != X2
| esk16_6(X1,X3,X4,X5,X6,X7) = esk16_6(X2,X3,X4,X5,X6,X7) ) ).
cnf(i_0_210_013,axiom,
( X1 != X2
| esk16_6(X3,X1,X4,X5,X6,X7) = esk16_6(X3,X2,X4,X5,X6,X7) ) ).
cnf(i_0_211_014,axiom,
( X1 != X2
| esk16_6(X3,X4,X1,X5,X6,X7) = esk16_6(X3,X4,X2,X5,X6,X7) ) ).
cnf(i_0_212_015,axiom,
( X1 != X2
| esk16_6(X3,X4,X5,X1,X6,X7) = esk16_6(X3,X4,X5,X2,X6,X7) ) ).
cnf(i_0_213_016,axiom,
( X1 != X2
| esk16_6(X3,X4,X5,X6,X1,X7) = esk16_6(X3,X4,X5,X6,X2,X7) ) ).
cnf(i_0_214_017,axiom,
( X1 != X2
| esk16_6(X3,X4,X5,X6,X7,X1) = esk16_6(X3,X4,X5,X6,X7,X2) ) ).
cnf(i_0_215_018,axiom,
( X1 != X2
| ~ p(X1)
| p(X2) ) ).
cnf(i_0_216_019,axiom,
( X1 != X2
| ~ mem(X1,X3)
| mem(X2,X3) ) ).
cnf(i_0_217_020,axiom,
( X1 != X2
| ~ mem(X3,X1)
| mem(X3,X2) ) ).
cnf(i_0_218_021,axiom,
( X1 != X2
| ~ epred1_4(X1,X3,X4,X5)
| epred1_4(X2,X3,X4,X5) ) ).
cnf(i_0_219_022,axiom,
( X1 != X2
| ~ epred1_4(X3,X1,X4,X5)
| epred1_4(X3,X2,X4,X5) ) ).
cnf(i_0_220_023,axiom,
( X1 != X2
| ~ epred1_4(X3,X4,X1,X5)
| epred1_4(X3,X4,X2,X5) ) ).
cnf(i_0_221_024,axiom,
( X1 != X2
| ~ epred1_4(X3,X4,X5,X1)
| epred1_4(X3,X4,X5,X2) ) ).
cnf(i_0_222_025,axiom,
( X1 != X2
| ~ ne(X1)
| ne(X2) ) ).
cnf(i_0_223_026,axiom,
( X1 != X2
| ~ epred2_3(X1,X3,X4)
| epred2_3(X2,X3,X4) ) ).
cnf(i_0_224_027,axiom,
( X1 != X2
| ~ epred2_3(X3,X1,X4)
| epred2_3(X3,X2,X4) ) ).
cnf(i_0_225_028,axiom,
( X1 != X2
| ~ epred2_3(X3,X4,X1)
| epred2_3(X3,X4,X2) ) ).
cnf(i_0_226_029,axiom,
( X1 != X2
| ~ epred4_3(X1,X3,X4)
| epred4_3(X2,X3,X4) ) ).
cnf(i_0_227_030,axiom,
( X1 != X2
| ~ epred4_3(X3,X1,X4)
| epred4_3(X3,X2,X4) ) ).
cnf(i_0_228_031,axiom,
( X1 != X2
| ~ epred4_3(X3,X4,X1)
| epred4_3(X3,X4,X2) ) ).
cnf(i_0_229_032,axiom,
( X1 != X2
| ~ epred3_3(X1,X3,X4)
| epred3_3(X2,X3,X4) ) ).
cnf(i_0_230_033,axiom,
( X1 != X2
| ~ epred3_3(X3,X1,X4)
| epred3_3(X3,X2,X4) ) ).
cnf(i_0_231_034,axiom,
( X1 != X2
| ~ epred3_3(X3,X4,X1)
| epred3_3(X3,X4,X2) ) ).
cnf(i_0_232,plain,
( X1 = X1
| ~ mem(X1,arr(X2,X3))
| ~ mem(X1,arr(X2,X3)) ),
inference(equality_inference,[],[109]) ).
cnf(i_0_233,plain,
( ~ mem(X1,X2)
| ~ mem(X1,X2)
| ~ ne(X2)
| p(ap(ap(c_2Emin_2E_3D(X2),X1),X1)) ),
inference(equality_inference,[],[140]) ).
cnf(i_0_234,plain,
c_2Ebool_2ET != ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk8_0),
inference(scs_inference,[],[i_0_125,i_0_193,i_0_215]) ).
cnf(i_0_235,plain,
epred2_3(c_2Ebool_2ET,c_2Ebool_2ET,X1),
inference(scs_inference,[],[i_0_125,i_0_193,i_0_215,i_0_175]) ).
cnf(i_0_236,plain,
( ~ p(X1)
| ~ p(X2)
| epred2_3(X1,X2,X3) ),
inference(rename_variables,[],[i_0_175]) ).
cnf(i_0_237,plain,
epred2_3(c_2Ebool_2ET,X1,ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk8_0)),
inference(scs_inference,[],[i_0_125,i_0_193,i_0_215,i_0_175,i_0_177]) ).
cnf(i_0_238,plain,
( ~ p(X1)
| p(X2)
| epred2_3(X1,X3,X2) ),
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_239,plain,
epred2_3(X1,c_2Ebool_2ET,ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk8_0)),
inference(scs_inference,[],[i_0_125,i_0_193,i_0_215,i_0_175,i_0_177,i_0_179]) ).
cnf(i_0_240,plain,
( ~ p(X1)
| p(X2)
| epred2_3(X3,X1,X2) ),
inference(rename_variables,[],[i_0_179]) ).
cnf(i_0_241,plain,
p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2EF),c_2Ebool_2EF)),
inference(scs_inference,[],[i_0_125,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233]) ).
cnf(i_0_242,plain,
( ~ ne(X1)
| p(ap(ap(c_2Emin_2E_3D(X1),X2),X2))
| ~ mem(X2,X1)
| ~ mem(X2,X1) ),
inference(rename_variables,[],[i_0_233]) ).
cnf(i_0_243,plain,
epred4_3(c_2Ebool_2EF,c_2Ebool_2EF,c_2Ebool_2EF),
inference(scs_inference,[],[i_0_125,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233,i_0_155]) ).
cnf(i_0_244,plain,
( ~ mem(X1,bool)
| ~ mem(X2,bool)
| ~ mem(X3,bool)
| epred4_3(X1,X2,X3) ),
inference(rename_variables,[],[i_0_155]) ).
cnf(i_0_245,plain,
epred3_3(c_2Ebool_2EF,c_2Ebool_2EF,c_2Ebool_2EF),
inference(scs_inference,[],[i_0_125,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233,i_0_155,i_0_156]) ).
cnf(i_0_246,plain,
( ~ mem(X1,bool)
| ~ mem(X2,bool)
| ~ mem(X3,bool)
| epred3_3(X1,X2,X3) ),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_247,plain,
epred1_4(esk5_0,esk4_0,esk6_0,esk7_0),
inference(scs_inference,[],[i_0_125,i_0_194,i_0_195,i_0_187,i_0_188,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233,i_0_155,i_0_156,i_0_118]) ).
cnf(i_0_248,plain,
( ~ mem(X1,arr(X2,bool))
| ~ mem(X3,arr(X4,X2))
| ~ ne(X4)
| ~ ne(X2)
| epred1_4(X4,X2,X3,X1) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_249,plain,
( ne(X1)
| esk5_0 != X1 ),
inference(scs_inference,[],[i_0_125,i_0_194,i_0_195,i_0_187,i_0_188,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233,i_0_155,i_0_156,i_0_118,i_0_222]) ).
cnf(i_0_250,plain,
p(ap(esk8_0,ap(esk6_0,esk14_6(esk7_0,esk6_0,esk4_0,esk5_0,esk6_0,esk8_0)))),
inference(scs_inference,[],[i_0_125,i_0_194,i_0_195,i_0_187,i_0_186,i_0_188,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233,i_0_155,i_0_156,i_0_118,i_0_222,i_0_95]) ).
cnf(i_0_251,plain,
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),X3),X4))
| p(ap(X4,ap(X3,esk14_6(X5,X6,X2,X1,X3,X4))))
| ~ mem(X4,arr(X2,bool))
| ~ mem(X3,arr(X1,X2))
| ~ epred1_4(X1,X2,X6,X5) ),
inference(rename_variables,[],[i_0_95]) ).
cnf(i_0_252,plain,
mem(esk14_6(esk7_0,esk6_0,esk4_0,esk5_0,esk6_0,esk8_0),esk5_0),
inference(scs_inference,[],[i_0_125,i_0_194,i_0_195,i_0_187,i_0_186,i_0_188,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233,i_0_155,i_0_156,i_0_118,i_0_222,i_0_95,i_0_101]) ).
cnf(i_0_253,plain,
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),X3),X4))
| ~ mem(X4,arr(X2,bool))
| ~ mem(X3,arr(X1,X2))
| mem(esk14_6(X5,X6,X2,X1,X3,X4),X1)
| ~ epred1_4(X1,X2,X6,X5) ),
inference(rename_variables,[],[i_0_101]) ).
cnf(i_0_254,plain,
~ p(ap(esk7_0,ap(esk6_0,esk14_6(esk7_0,esk6_0,esk4_0,esk5_0,esk6_0,esk8_0)))),
inference(scs_inference,[],[i_0_125,i_0_194,i_0_195,i_0_187,i_0_186,i_0_188,i_0_143,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233,i_0_155,i_0_156,i_0_118,i_0_222,i_0_95,i_0_101,i_0_113]) ).
cnf(i_0_255,plain,
( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),X3),X4))
| ~ p(ap(X4,ap(X3,X5)))
| ~ mem(X4,arr(X2,bool))
| ~ mem(X3,arr(X1,X2))
| ~ epred1_4(X1,X2,X6,X7)
| ~ mem(X5,X1) ),
inference(rename_variables,[],[i_0_113]) ).
cnf(i_0_256,plain,
~ mem(ap(esk6_0,esk14_6(esk7_0,esk6_0,esk4_0,esk5_0,esk6_0,esk8_0)),esk4_0),
inference(scs_inference,[],[i_0_125,i_0_194,i_0_195,i_0_187,i_0_186,i_0_188,i_0_143,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233,i_0_155,i_0_156,i_0_118,i_0_222,i_0_95,i_0_101,i_0_113,i_0_163]) ).
cnf(i_0_257,plain,
( ~ p(ap(esk8_0,X1))
| p(ap(esk7_0,X1))
| ~ mem(X1,esk4_0) ),
inference(rename_variables,[],[i_0_163]) ).
cnf(i_0_258,plain,
( X1 != ap(esk6_0,esk14_6(esk7_0,esk6_0,esk4_0,esk5_0,esk6_0,esk8_0))
| ~ mem(X1,esk4_0) ),
inference(scs_inference,[],[i_0_125,i_0_194,i_0_195,i_0_187,i_0_186,i_0_188,i_0_143,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233,i_0_155,i_0_156,i_0_118,i_0_222,i_0_95,i_0_101,i_0_113,i_0_163,i_0_150,i_0_216]) ).
cnf(i_0_259,plain,
( X1 != esk4_0
| ~ mem(ap(esk6_0,esk14_6(esk7_0,esk6_0,esk4_0,esk5_0,esk6_0,esk8_0)),X1) ),
inference(scs_inference,[],[i_0_125,i_0_194,i_0_195,i_0_187,i_0_186,i_0_188,i_0_143,i_0_190,i_0_193,i_0_197,i_0_215,i_0_175,i_0_177,i_0_179,i_0_233,i_0_155,i_0_156,i_0_118,i_0_222,i_0_95,i_0_101,i_0_113,i_0_163,i_0_150,i_0_216,i_0_217]) ).
cnf(i_0_260,plain,
ne(esk5_0),
inference(equality_inference,[],[249]) ).
cnf(i_0_261,plain,
~ mem(ap(esk6_0,esk14_6(esk7_0,esk6_0,esk4_0,esk5_0,esk6_0,esk8_0)),esk4_0),
inference(equality_inference,[],[258]) ).
cnf(i_0_262,plain,
~ mem(ap(esk6_0,esk14_6(esk7_0,esk6_0,esk4_0,esk5_0,esk6_0,esk8_0)),esk4_0),
inference(equality_inference,[],[259]) ).
cnf(i_0_263,plain,
$false,
inference(scs_inference,[],[i_0_256,i_0_188,i_0_252,i_0_150]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ITP006+2 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n029.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 19:36:29 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 2.89/5.63 % Version : CSE_E---1.7
% 2.89/5.63 % Problem : theBenchmark.p
% 2.89/5.63 % SZS status Theorem for theBenchmark.p
% 2.89/5.63 % SZS output start CNFRefutation
% See solution above
% 3.07/5.73 % Total time : 5.281s
%------------------------------------------------------------------------------