%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : ITP004+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:45:21 AM UTC 2026
% Result : Theorem 166.04s 166.37s
% Output : Proof 167.15s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(bool_ne,axiom,
ne(bool),
file('ITP001+2.ax',bool_ne) ).
fof(ind_ne,axiom,
ne(ind),
file('ITP001+2.ax',ind_ne) ).
fof(arr_ne,axiom,
! [A] :
( ne(A)
=> ! [B] :
( ne(B)
=> ne(arr(A,B)) ) ),
file('ITP001+2.ax',arr_ne) ).
fof(ap_tp,axiom,
! [A,B,F] :
( mem(F,arr(A,B))
=> ! [X] :
( mem(X,A)
=> mem(ap(F,X),B) ) ),
file('ITP001+2.ax',ap_tp) ).
fof(boolext,axiom,
! [Q] :
( mem(Q,bool)
=> ! [R] :
( mem(R,bool)
=> ( ( p(Q)
<=> p(R) )
=> Q = R ) ) ),
file('ITP001+2.ax',boolext) ).
fof(funcext,axiom,
! [A,B,F] :
( mem(F,arr(A,B))
=> ! [G] :
( mem(G,arr(A,B))
=> ( ! [X] :
( mem(X,A)
=> ap(F,X) = ap(G,X) )
=> F = G ) ) ),
file('ITP001+2.ax',funcext) ).
fof(kbeta,axiom,
! [A,Y,X] :
( mem(X,A)
=> ap(k(A,Y),X) = Y ),
file('ITP001+2.ax',kbeta) ).
fof(ibeta,axiom,
! [A,X] :
( mem(X,A)
=> ap(i(A),X) = X ),
file('ITP001+2.ax',ibeta) ).
fof(mem_c_2Emin_2E_3D_3D_3E,axiom,
mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool))),
file('theBenchmark.p',mem_c_2Emin_2E_3D_3D_3E) ).
fof(ax_imp_p,axiom,
! [Q] :
( mem(Q,bool)
=> ! [R] :
( mem(R,bool)
=> ( p(ap(ap(c_2Emin_2E_3D_3D_3E,Q),R))
<=> ( p(Q)
=> p(R) ) ) ) ),
file('theBenchmark.p',ax_imp_p) ).
fof(mem_c_2Epred__set_2ESUBSET,axiom,
! [A_27a] :
( ne(A_27a)
=> mem(c_2Epred__set_2ESUBSET(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) ),
file('theBenchmark.p',mem_c_2Epred__set_2ESUBSET) ).
fof(mem_c_2Ebool_2E_7E,axiom,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
file('theBenchmark.p',mem_c_2Ebool_2E_7E) ).
fof(ax_neg_p,axiom,
! [Q] :
( mem(Q,bool)
=> ( p(ap(c_2Ebool_2E_7E,Q))
<=> ~ p(Q) ) ),
file('theBenchmark.p',ax_neg_p) ).
fof(mem_c_2Ebool_2E_2F_5C,axiom,
mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool))),
file('theBenchmark.p',mem_c_2Ebool_2E_2F_5C) ).
fof(ax_and_p,axiom,
! [Q] :
( mem(Q,bool)
=> ! [R] :
( mem(R,bool)
=> ( p(ap(ap(c_2Ebool_2E_2F_5C,Q),R))
<=> ( p(R)
& p(Q) ) ) ) ),
file('theBenchmark.p',ax_and_p) ).
fof(mem_c_2Ebool_2EIN,axiom,
! [A_27a] :
( ne(A_27a)
=> mem(c_2Ebool_2EIN(A_27a),arr(A_27a,arr(arr(A_27a,bool),bool))) ),
file('theBenchmark.p',mem_c_2Ebool_2EIN) ).
fof(mem_c_2Epred__set_2ECHOICE,axiom,
! [A_27a] :
( ne(A_27a)
=> mem(c_2Epred__set_2ECHOICE(A_27a),arr(arr(A_27a,bool),A_27a)) ),
file('theBenchmark.p',mem_c_2Epred__set_2ECHOICE) ).
fof(mem_c_2Epred__set_2EDELETE,axiom,
! [A_27a] :
( ne(A_27a)
=> mem(c_2Epred__set_2EDELETE(A_27a),arr(arr(A_27a,bool),arr(A_27a,arr(A_27a,bool)))) ),
file('theBenchmark.p',mem_c_2Epred__set_2EDELETE) ).
fof(mem_c_2Epred__set_2EREST,axiom,
! [A_27a] :
( ne(A_27a)
=> mem(c_2Epred__set_2EREST(A_27a),arr(arr(A_27a,bool),arr(A_27a,bool))) ),
file('theBenchmark.p',mem_c_2Epred__set_2EREST) ).
fof(mem_c_2Emin_2E_3D,axiom,
! [A_27a] :
( ne(A_27a)
=> mem(c_2Emin_2E_3D(A_27a),arr(A_27a,arr(A_27a,bool))) ),
file('theBenchmark.p',mem_c_2Emin_2E_3D) ).
fof(ax_eq_p,axiom,
! [A] :
( ne(A)
=> ! [X] :
( mem(X,A)
=> ! [Y] :
( mem(Y,A)
=> ( p(ap(ap(c_2Emin_2E_3D(A),X),Y))
<=> X = Y ) ) ) ),
file('theBenchmark.p',ax_eq_p) ).
fof(mem_c_2Ebool_2E_21,axiom,
! [A_27a] :
( ne(A_27a)
=> mem(c_2Ebool_2E_21(A_27a),arr(arr(A_27a,bool),bool)) ),
file('theBenchmark.p',mem_c_2Ebool_2E_21) ).
fof(ax_all_p,axiom,
! [A] :
( ne(A)
=> ! [Q] :
( mem(Q,arr(A,bool))
=> ( p(ap(c_2Ebool_2E_21(A),Q))
<=> ! [X] :
( mem(X,A)
=> p(ap(Q,X)) ) ) ) ),
file('theBenchmark.p',ax_all_p) ).
fof(ax_thm_2Epred__set_2ESUBSET__DEF,axiom,
! [A_27a] :
( ne(A_27a)
=> ! [V0s] :
( mem(V0s,arr(A_27a,bool))
=> ! [V1t] :
( mem(V1t,arr(A_27a,bool))
=> ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0s),V1t))
<=> ! [V2x] :
( mem(V2x,A_27a)
=> ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s))
=> p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t)) ) ) ) ) ) ),
file('theBenchmark.p',ax_thm_2Epred__set_2ESUBSET__DEF) ).
fof(conj_thm_2Epred__set_2EIN__DELETE,axiom,
! [A_27a] :
( ne(A_27a)
=> ! [V0s] :
( mem(V0s,arr(A_27a,bool))
=> ! [V1x] :
( mem(V1x,A_27a)
=> ! [V2y] :
( mem(V2y,A_27a)
=> ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),V2y)))
<=> ( V1x != V2y
& p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),V0s)) ) ) ) ) ) ),
file('theBenchmark.p',conj_thm_2Epred__set_2EIN__DELETE) ).
fof(ax_thm_2Epred__set_2EREST__DEF,axiom,
! [A_27a] :
( ne(A_27a)
=> ! [V0s] :
( mem(V0s,arr(A_27a,bool))
=> ap(c_2Epred__set_2EREST(A_27a),V0s) = ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),ap(c_2Epred__set_2ECHOICE(A_27a),V0s)) ) ),
file('theBenchmark.p',ax_thm_2Epred__set_2EREST__DEF) ).
fof(conj_thm_2Epred__set_2EREST__SUBSET,conjecture,
! [A_27a] :
( ne(A_27a)
=> ! [V0s] :
( mem(V0s,arr(A_27a,bool))
=> p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Epred__set_2EREST(A_27a),V0s)),V0s)) ) ),
file('theBenchmark.p',conj_thm_2Epred__set_2EREST__SUBSET) ).
fof(f_1_1,plain,
ne(bool),
inference(fof_nnf,[status(thm)],[bool_ne]) ).
cnf(f_1_2,plain,
ne(bool),
inference(clausify,[status(thm)],[f_1_1]) ).
fof(f_2_1,plain,
ne(ind),
inference(fof_nnf,[status(thm)],[ind_ne]) ).
cnf(f_2_2,plain,
ne(ind),
inference(clausify,[status(thm)],[f_2_1]) ).
fof(f_3_1,plain,
! [A] :
( ! [B] :
( ne(arr(A,B))
| ~ ne(B) )
| ~ ne(A) ),
inference(fof_nnf,[status(thm)],[arr_ne]) ).
fof(f_3_2,plain,
! [U_1] :
( ! [U_0] :
( ne(arr(U_1,U_0))
| ~ ne(U_0) )
| ~ ne(U_1) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( ne(arr(U_1,U_0))
| ~ ne(U_0)
| ~ ne(U_1) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [A,B,F] :
( ! [X] :
( mem(ap(F,X),B)
| ~ mem(X,A) )
| ~ mem(F,arr(A,B)) ),
inference(fof_nnf,[status(thm)],[ap_tp]) ).
fof(f_4_2,plain,
! [U_5,U_4,U_3] :
( ! [U_2] :
( mem(ap(U_3,U_2),U_4)
| ~ mem(U_2,U_5) )
| ~ mem(U_3,arr(U_5,U_4)) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
( mem(ap(U_3,U_2),U_4)
| ~ mem(U_2,U_5)
| ~ mem(U_3,arr(U_5,U_4)) ),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [Q] :
( ! [R] :
( Q = R
| ( ~ p(Q)
& p(R) )
| ( ~ p(R)
& p(Q) )
| ~ mem(R,bool) )
| ~ mem(Q,bool) ),
inference(fof_nnf,[status(thm)],[boolext]) ).
fof(f_5_2,plain,
! [U_7] :
( ! [U_6] :
( U_7 = U_6
| ( ~ p(U_7)
& p(U_6) )
| ( ~ p(U_6)
& p(U_7) )
| ~ mem(U_6,bool) )
| ~ mem(U_7,bool) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
( p(U_6)
| p(U_7)
| U_7 = U_6
| ~ mem(U_6,bool)
| ~ mem(U_7,bool) ),
inference(clausify,[status(thm)],[f_5_2]) ).
cnf(f_5_4,plain,
( ~ p(U_7)
| p(U_7)
| U_7 = U_6
| ~ mem(U_6,bool)
| ~ mem(U_7,bool) ),
inference(clausify,[status(thm)],[f_5_2]) ).
cnf(f_5_5,plain,
( p(U_6)
| ~ p(U_6)
| U_7 = U_6
| ~ mem(U_6,bool)
| ~ mem(U_7,bool) ),
inference(clausify,[status(thm)],[f_5_2]) ).
cnf(f_5_6,plain,
( ~ p(U_7)
| ~ p(U_6)
| U_7 = U_6
| ~ mem(U_6,bool)
| ~ mem(U_7,bool) ),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [A,B,F] :
( ! [G] :
( F = G
| ? [X] :
( ap(F,X) != ap(G,X)
& mem(X,A) )
| ~ mem(G,arr(A,B)) )
| ~ mem(F,arr(A,B)) ),
inference(fof_nnf,[status(thm)],[funcext]) ).
fof(f_6_2,plain,
! [U_12,U_11,U_10] :
( ! [U_9] :
( U_10 = U_9
| ? [U_8] :
( ap(U_10,U_8) != ap(U_9,U_8)
& mem(U_8,U_12) )
| ~ mem(U_9,arr(U_12,U_11)) )
| ~ mem(U_10,arr(U_12,U_11)) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
! [U_12,U_11,U_10] :
( ! [U_9] :
( U_10 = U_9
| ( ap(U_10,sK1(U_12,U_11,U_10,U_9)) != ap(U_9,sK1(U_12,U_11,U_10,U_9))
& mem(sK1(U_12,U_11,U_10,U_9),U_12) )
| ~ mem(U_9,arr(U_12,U_11)) )
| ~ mem(U_10,arr(U_12,U_11)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_8,sK1(U_12,U_11,U_10,U_9))],[f_6_2]) ).
cnf(f_6_4,plain,
( mem(sK1(U_12,U_11,U_10,U_9),U_12)
| U_10 = U_9
| ~ mem(U_9,arr(U_12,U_11))
| ~ mem(U_10,arr(U_12,U_11)) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_5,plain,
( ap(U_10,sK1(U_12,U_11,U_10,U_9)) != ap(U_9,sK1(U_12,U_11,U_10,U_9))
| U_10 = U_9
| ~ mem(U_9,arr(U_12,U_11))
| ~ mem(U_10,arr(U_12,U_11)) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,plain,
! [A,Y,X] :
( ap(k(A,Y),X) = Y
| ~ mem(X,A) ),
inference(fof_nnf,[status(thm)],[kbeta]) ).
fof(f_7_2,plain,
! [U_15,U_14,U_13] :
( ap(k(U_15,U_14),U_13) = U_14
| ~ mem(U_13,U_15) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
cnf(f_7_3,plain,
( ap(k(U_15,U_14),U_13) = U_14
| ~ mem(U_13,U_15) ),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
! [A,X] :
( ap(i(A),X) = X
| ~ mem(X,A) ),
inference(fof_nnf,[status(thm)],[ibeta]) ).
fof(f_8_2,plain,
! [U_17,U_16] :
( ap(i(U_17),U_16) = U_16
| ~ mem(U_16,U_17) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
( ap(i(U_17),U_16) = U_16
| ~ mem(U_16,U_17) ),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool))),
inference(fof_nnf,[status(thm)],[mem_c_2Emin_2E_3D_3D_3E]) ).
cnf(f_9_2,plain,
mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool))),
inference(clausify,[status(thm)],[f_9_1]) ).
fof(f_10_1,plain,
! [Q] :
( ! [R] :
( ( ( p(ap(ap(c_2Emin_2E_3D_3D_3E,Q),R))
| ( ~ p(R)
& p(Q) ) )
& ( p(R)
| ~ p(Q)
| ~ p(ap(ap(c_2Emin_2E_3D_3D_3E,Q),R)) ) )
| ~ mem(R,bool) )
| ~ mem(Q,bool) ),
inference(fof_nnf,[status(thm)],[ax_imp_p]) ).
fof(f_10_2,plain,
! [U_19] :
( ! [U_18] :
( ( ( p(ap(ap(c_2Emin_2E_3D_3D_3E,U_19),U_18))
| ( ~ p(U_18)
& p(U_19) ) )
& ( p(U_18)
| ~ p(U_19)
| ~ p(ap(ap(c_2Emin_2E_3D_3D_3E,U_19),U_18)) ) )
| ~ mem(U_18,bool) )
| ~ mem(U_19,bool) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
( p(U_18)
| ~ p(U_19)
| ~ p(ap(ap(c_2Emin_2E_3D_3D_3E,U_19),U_18))
| ~ mem(U_18,bool)
| ~ mem(U_19,bool) ),
inference(clausify,[status(thm)],[f_10_2]) ).
cnf(f_10_4,plain,
( p(U_19)
| p(ap(ap(c_2Emin_2E_3D_3D_3E,U_19),U_18))
| ~ mem(U_18,bool)
| ~ mem(U_19,bool) ),
inference(clausify,[status(thm)],[f_10_2]) ).
cnf(f_10_5,plain,
( ~ p(U_18)
| p(ap(ap(c_2Emin_2E_3D_3D_3E,U_19),U_18))
| ~ mem(U_18,bool)
| ~ mem(U_19,bool) ),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [A_27a] :
( mem(c_2Epred__set_2ESUBSET(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,bool),bool)))
| ~ ne(A_27a) ),
inference(fof_nnf,[status(thm)],[mem_c_2Epred__set_2ESUBSET]) ).
fof(f_11_2,plain,
! [U_20] :
( mem(c_2Epred__set_2ESUBSET(U_20),arr(arr(U_20,bool),arr(arr(U_20,bool),bool)))
| ~ ne(U_20) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
cnf(f_11_3,plain,
( mem(c_2Epred__set_2ESUBSET(U_20),arr(arr(U_20,bool),arr(arr(U_20,bool),bool)))
| ~ ne(U_20) ),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
inference(fof_nnf,[status(thm)],[mem_c_2Ebool_2E_7E]) ).
cnf(f_12_2,plain,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
inference(clausify,[status(thm)],[f_12_1]) ).
fof(f_13_1,plain,
! [Q] :
( ( ( p(ap(c_2Ebool_2E_7E,Q))
| p(Q) )
& ( ~ p(Q)
| ~ p(ap(c_2Ebool_2E_7E,Q)) ) )
| ~ mem(Q,bool) ),
inference(fof_nnf,[status(thm)],[ax_neg_p]) ).
fof(f_13_2,plain,
! [U_21] :
( ( ( p(ap(c_2Ebool_2E_7E,U_21))
| p(U_21) )
& ( ~ p(U_21)
| ~ p(ap(c_2Ebool_2E_7E,U_21)) ) )
| ~ mem(U_21,bool) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
cnf(f_13_3,plain,
( ~ p(U_21)
| ~ p(ap(c_2Ebool_2E_7E,U_21))
| ~ mem(U_21,bool) ),
inference(clausify,[status(thm)],[f_13_2]) ).
cnf(f_13_4,plain,
( p(ap(c_2Ebool_2E_7E,U_21))
| p(U_21)
| ~ mem(U_21,bool) ),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_14_1,plain,
mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool))),
inference(fof_nnf,[status(thm)],[mem_c_2Ebool_2E_2F_5C]) ).
cnf(f_14_2,plain,
mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool))),
inference(clausify,[status(thm)],[f_14_1]) ).
fof(f_15_1,plain,
! [Q] :
( ! [R] :
( ( ( p(ap(ap(c_2Ebool_2E_2F_5C,Q),R))
| ~ p(R)
| ~ p(Q) )
& ( ( p(R)
& p(Q) )
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,Q),R)) ) )
| ~ mem(R,bool) )
| ~ mem(Q,bool) ),
inference(fof_nnf,[status(thm)],[ax_and_p]) ).
fof(f_15_2,plain,
! [U_23] :
( ! [U_22] :
( ( ( p(ap(ap(c_2Ebool_2E_2F_5C,U_23),U_22))
| ~ p(U_22)
| ~ p(U_23) )
& ( ( p(U_22)
& p(U_23) )
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,U_23),U_22)) ) )
| ~ mem(U_22,bool) )
| ~ mem(U_23,bool) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
cnf(f_15_3,plain,
( p(U_23)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,U_23),U_22))
| ~ mem(U_22,bool)
| ~ mem(U_23,bool) ),
inference(clausify,[status(thm)],[f_15_2]) ).
cnf(f_15_4,plain,
( p(U_22)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,U_23),U_22))
| ~ mem(U_22,bool)
| ~ mem(U_23,bool) ),
inference(clausify,[status(thm)],[f_15_2]) ).
cnf(f_15_5,plain,
( p(ap(ap(c_2Ebool_2E_2F_5C,U_23),U_22))
| ~ p(U_22)
| ~ p(U_23)
| ~ mem(U_22,bool)
| ~ mem(U_23,bool) ),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
! [A_27a] :
( mem(c_2Ebool_2EIN(A_27a),arr(A_27a,arr(arr(A_27a,bool),bool)))
| ~ ne(A_27a) ),
inference(fof_nnf,[status(thm)],[mem_c_2Ebool_2EIN]) ).
fof(f_16_2,plain,
! [U_24] :
( mem(c_2Ebool_2EIN(U_24),arr(U_24,arr(arr(U_24,bool),bool)))
| ~ ne(U_24) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
cnf(f_16_3,plain,
( mem(c_2Ebool_2EIN(U_24),arr(U_24,arr(arr(U_24,bool),bool)))
| ~ ne(U_24) ),
inference(clausify,[status(thm)],[f_16_2]) ).
fof(f_17_1,plain,
! [A_27a] :
( mem(c_2Epred__set_2ECHOICE(A_27a),arr(arr(A_27a,bool),A_27a))
| ~ ne(A_27a) ),
inference(fof_nnf,[status(thm)],[mem_c_2Epred__set_2ECHOICE]) ).
fof(f_17_2,plain,
! [U_25] :
( mem(c_2Epred__set_2ECHOICE(U_25),arr(arr(U_25,bool),U_25))
| ~ ne(U_25) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
( mem(c_2Epred__set_2ECHOICE(U_25),arr(arr(U_25,bool),U_25))
| ~ ne(U_25) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [A_27a] :
( mem(c_2Epred__set_2EDELETE(A_27a),arr(arr(A_27a,bool),arr(A_27a,arr(A_27a,bool))))
| ~ ne(A_27a) ),
inference(fof_nnf,[status(thm)],[mem_c_2Epred__set_2EDELETE]) ).
fof(f_18_2,plain,
! [U_26] :
( mem(c_2Epred__set_2EDELETE(U_26),arr(arr(U_26,bool),arr(U_26,arr(U_26,bool))))
| ~ ne(U_26) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( mem(c_2Epred__set_2EDELETE(U_26),arr(arr(U_26,bool),arr(U_26,arr(U_26,bool))))
| ~ ne(U_26) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [A_27a] :
( mem(c_2Epred__set_2EREST(A_27a),arr(arr(A_27a,bool),arr(A_27a,bool)))
| ~ ne(A_27a) ),
inference(fof_nnf,[status(thm)],[mem_c_2Epred__set_2EREST]) ).
fof(f_19_2,plain,
! [U_27] :
( mem(c_2Epred__set_2EREST(U_27),arr(arr(U_27,bool),arr(U_27,bool)))
| ~ ne(U_27) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
cnf(f_19_3,plain,
( mem(c_2Epred__set_2EREST(U_27),arr(arr(U_27,bool),arr(U_27,bool)))
| ~ ne(U_27) ),
inference(clausify,[status(thm)],[f_19_2]) ).
fof(f_20_1,plain,
! [A_27a] :
( mem(c_2Emin_2E_3D(A_27a),arr(A_27a,arr(A_27a,bool)))
| ~ ne(A_27a) ),
inference(fof_nnf,[status(thm)],[mem_c_2Emin_2E_3D]) ).
fof(f_20_2,plain,
! [U_28] :
( mem(c_2Emin_2E_3D(U_28),arr(U_28,arr(U_28,bool)))
| ~ ne(U_28) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
( mem(c_2Emin_2E_3D(U_28),arr(U_28,arr(U_28,bool)))
| ~ ne(U_28) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [A] :
( ! [X] :
( ! [Y] :
( ( ( p(ap(ap(c_2Emin_2E_3D(A),X),Y))
| X != Y )
& ( X = Y
| ~ p(ap(ap(c_2Emin_2E_3D(A),X),Y)) ) )
| ~ mem(Y,A) )
| ~ mem(X,A) )
| ~ ne(A) ),
inference(fof_nnf,[status(thm)],[ax_eq_p]) ).
fof(f_21_2,plain,
! [U_31] :
( ! [U_30] :
( ! [U_29] :
( ( ( p(ap(ap(c_2Emin_2E_3D(U_31),U_30),U_29))
| U_30 != U_29 )
& ( U_30 = U_29
| ~ p(ap(ap(c_2Emin_2E_3D(U_31),U_30),U_29)) ) )
| ~ mem(U_29,U_31) )
| ~ mem(U_30,U_31) )
| ~ ne(U_31) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( U_30 = U_29
| ~ p(ap(ap(c_2Emin_2E_3D(U_31),U_30),U_29))
| ~ mem(U_29,U_31)
| ~ mem(U_30,U_31)
| ~ ne(U_31) ),
inference(clausify,[status(thm)],[f_21_2]) ).
cnf(f_21_4,plain,
( p(ap(ap(c_2Emin_2E_3D(U_31),U_30),U_29))
| U_30 != U_29
| ~ mem(U_29,U_31)
| ~ mem(U_30,U_31)
| ~ ne(U_31) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [A_27a] :
( mem(c_2Ebool_2E_21(A_27a),arr(arr(A_27a,bool),bool))
| ~ ne(A_27a) ),
inference(fof_nnf,[status(thm)],[mem_c_2Ebool_2E_21]) ).
fof(f_22_2,plain,
! [U_32] :
( mem(c_2Ebool_2E_21(U_32),arr(arr(U_32,bool),bool))
| ~ ne(U_32) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
( mem(c_2Ebool_2E_21(U_32),arr(arr(U_32,bool),bool))
| ~ ne(U_32) ),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_23_1,plain,
! [A] :
( ! [Q] :
( ( ( p(ap(c_2Ebool_2E_21(A),Q))
| ? [X] :
( ~ p(ap(Q,X))
& mem(X,A) ) )
& ( ! [X] :
( p(ap(Q,X))
| ~ mem(X,A) )
| ~ p(ap(c_2Ebool_2E_21(A),Q)) ) )
| ~ mem(Q,arr(A,bool)) )
| ~ ne(A) ),
inference(fof_nnf,[status(thm)],[ax_all_p]) ).
fof(f_23_2,plain,
! [U_36] :
( ! [U_35] :
( ( ( p(ap(c_2Ebool_2E_21(U_36),U_35))
| ? [U_34] :
( ~ p(ap(U_35,U_34))
& mem(U_34,U_36) ) )
& ( ! [U_33] :
( p(ap(U_35,U_33))
| ~ mem(U_33,U_36) )
| ~ p(ap(c_2Ebool_2E_21(U_36),U_35)) ) )
| ~ mem(U_35,arr(U_36,bool)) )
| ~ ne(U_36) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
! [U_36] :
( ! [U_35] :
( ( ( p(ap(c_2Ebool_2E_21(U_36),U_35))
| ( ~ p(ap(U_35,sK2(U_36,U_35)))
& mem(sK2(U_36,U_35),U_36) ) )
& ( ! [U_33] :
( p(ap(U_35,U_33))
| ~ mem(U_33,U_36) )
| ~ p(ap(c_2Ebool_2E_21(U_36),U_35)) ) )
| ~ mem(U_35,arr(U_36,bool)) )
| ~ ne(U_36) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_34,sK2(U_36,U_35))],[f_23_2]) ).
cnf(f_23_4,plain,
( p(ap(U_35,U_33))
| ~ mem(U_33,U_36)
| ~ p(ap(c_2Ebool_2E_21(U_36),U_35))
| ~ mem(U_35,arr(U_36,bool))
| ~ ne(U_36) ),
inference(clausify,[status(thm)],[f_23_3]) ).
cnf(f_23_5,plain,
( mem(sK2(U_36,U_35),U_36)
| p(ap(c_2Ebool_2E_21(U_36),U_35))
| ~ mem(U_35,arr(U_36,bool))
| ~ ne(U_36) ),
inference(clausify,[status(thm)],[f_23_3]) ).
cnf(f_23_6,plain,
( ~ p(ap(U_35,sK2(U_36,U_35)))
| p(ap(c_2Ebool_2E_21(U_36),U_35))
| ~ mem(U_35,arr(U_36,bool))
| ~ ne(U_36) ),
inference(clausify,[status(thm)],[f_23_3]) ).
fof(f_24_1,plain,
! [A_27a] :
( ! [V0s] :
( ! [V1t] :
( ( ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0s),V1t))
| ? [V2x] :
( ~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t))
& p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s))
& mem(V2x,A_27a) ) )
& ( ! [V2x] :
( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t))
| ~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s))
| ~ mem(V2x,A_27a) )
| ~ p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0s),V1t)) ) )
| ~ mem(V1t,arr(A_27a,bool)) )
| ~ mem(V0s,arr(A_27a,bool)) )
| ~ ne(A_27a) ),
inference(fof_nnf,[status(thm)],[ax_thm_2Epred__set_2ESUBSET__DEF]) ).
fof(f_24_2,plain,
! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ( ( p(ap(ap(c_2Epred__set_2ESUBSET(U_41),U_40),U_39))
| ? [U_38] :
( ~ p(ap(ap(c_2Ebool_2EIN(U_41),U_38),U_39))
& p(ap(ap(c_2Ebool_2EIN(U_41),U_38),U_40))
& mem(U_38,U_41) ) )
& ( ! [U_37] :
( p(ap(ap(c_2Ebool_2EIN(U_41),U_37),U_39))
| ~ p(ap(ap(c_2Ebool_2EIN(U_41),U_37),U_40))
| ~ mem(U_37,U_41) )
| ~ p(ap(ap(c_2Epred__set_2ESUBSET(U_41),U_40),U_39)) ) )
| ~ mem(U_39,arr(U_41,bool)) )
| ~ mem(U_40,arr(U_41,bool)) )
| ~ ne(U_41) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ( ( p(ap(ap(c_2Epred__set_2ESUBSET(U_41),U_40),U_39))
| ( ~ p(ap(ap(c_2Ebool_2EIN(U_41),sK3(U_41,U_40,U_39)),U_39))
& p(ap(ap(c_2Ebool_2EIN(U_41),sK3(U_41,U_40,U_39)),U_40))
& mem(sK3(U_41,U_40,U_39),U_41) ) )
& ( ! [U_37] :
( p(ap(ap(c_2Ebool_2EIN(U_41),U_37),U_39))
| ~ p(ap(ap(c_2Ebool_2EIN(U_41),U_37),U_40))
| ~ mem(U_37,U_41) )
| ~ p(ap(ap(c_2Epred__set_2ESUBSET(U_41),U_40),U_39)) ) )
| ~ mem(U_39,arr(U_41,bool)) )
| ~ mem(U_40,arr(U_41,bool)) )
| ~ ne(U_41) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_38,sK3(U_41,U_40,U_39))],[f_24_2]) ).
cnf(f_24_4,plain,
( p(ap(ap(c_2Ebool_2EIN(U_41),U_37),U_39))
| ~ p(ap(ap(c_2Ebool_2EIN(U_41),U_37),U_40))
| ~ mem(U_37,U_41)
| ~ p(ap(ap(c_2Epred__set_2ESUBSET(U_41),U_40),U_39))
| ~ mem(U_39,arr(U_41,bool))
| ~ mem(U_40,arr(U_41,bool))
| ~ ne(U_41) ),
inference(clausify,[status(thm)],[f_24_3]) ).
cnf(f_24_5,plain,
( mem(sK3(U_41,U_40,U_39),U_41)
| p(ap(ap(c_2Epred__set_2ESUBSET(U_41),U_40),U_39))
| ~ mem(U_39,arr(U_41,bool))
| ~ mem(U_40,arr(U_41,bool))
| ~ ne(U_41) ),
inference(clausify,[status(thm)],[f_24_3]) ).
cnf(f_24_6,plain,
( p(ap(ap(c_2Ebool_2EIN(U_41),sK3(U_41,U_40,U_39)),U_40))
| p(ap(ap(c_2Epred__set_2ESUBSET(U_41),U_40),U_39))
| ~ mem(U_39,arr(U_41,bool))
| ~ mem(U_40,arr(U_41,bool))
| ~ ne(U_41) ),
inference(clausify,[status(thm)],[f_24_3]) ).
cnf(f_24_7,plain,
( ~ p(ap(ap(c_2Ebool_2EIN(U_41),sK3(U_41,U_40,U_39)),U_39))
| p(ap(ap(c_2Epred__set_2ESUBSET(U_41),U_40),U_39))
| ~ mem(U_39,arr(U_41,bool))
| ~ mem(U_40,arr(U_41,bool))
| ~ ne(U_41) ),
inference(clausify,[status(thm)],[f_24_3]) ).
fof(f_25_1,plain,
! [A_27a] :
( ! [V0s] :
( ! [V1x] :
( ! [V2y] :
( ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),V2y)))
| V1x = V2y
| ~ p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),V0s)) )
& ( ( V1x != V2y
& p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),V0s)) )
| ~ p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),V2y))) ) )
| ~ mem(V2y,A_27a) )
| ~ mem(V1x,A_27a) )
| ~ mem(V0s,arr(A_27a,bool)) )
| ~ ne(A_27a) ),
inference(fof_nnf,[status(thm)],[conj_thm_2Epred__set_2EIN__DELETE]) ).
fof(f_25_2,plain,
! [U_45] :
( ! [U_44] :
( ! [U_43] :
( ! [U_42] :
( ( ( p(ap(ap(c_2Ebool_2EIN(U_45),U_43),ap(ap(c_2Epred__set_2EDELETE(U_45),U_44),U_42)))
| U_43 = U_42
| ~ p(ap(ap(c_2Ebool_2EIN(U_45),U_43),U_44)) )
& ( ( U_43 != U_42
& p(ap(ap(c_2Ebool_2EIN(U_45),U_43),U_44)) )
| ~ p(ap(ap(c_2Ebool_2EIN(U_45),U_43),ap(ap(c_2Epred__set_2EDELETE(U_45),U_44),U_42))) ) )
| ~ mem(U_42,U_45) )
| ~ mem(U_43,U_45) )
| ~ mem(U_44,arr(U_45,bool)) )
| ~ ne(U_45) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
cnf(f_25_3,plain,
( p(ap(ap(c_2Ebool_2EIN(U_45),U_43),U_44))
| ~ p(ap(ap(c_2Ebool_2EIN(U_45),U_43),ap(ap(c_2Epred__set_2EDELETE(U_45),U_44),U_42)))
| ~ mem(U_42,U_45)
| ~ mem(U_43,U_45)
| ~ mem(U_44,arr(U_45,bool))
| ~ ne(U_45) ),
inference(clausify,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
( U_43 != U_42
| ~ p(ap(ap(c_2Ebool_2EIN(U_45),U_43),ap(ap(c_2Epred__set_2EDELETE(U_45),U_44),U_42)))
| ~ mem(U_42,U_45)
| ~ mem(U_43,U_45)
| ~ mem(U_44,arr(U_45,bool))
| ~ ne(U_45) ),
inference(clausify,[status(thm)],[f_25_2]) ).
cnf(f_25_5,plain,
( p(ap(ap(c_2Ebool_2EIN(U_45),U_43),ap(ap(c_2Epred__set_2EDELETE(U_45),U_44),U_42)))
| U_43 = U_42
| ~ p(ap(ap(c_2Ebool_2EIN(U_45),U_43),U_44))
| ~ mem(U_42,U_45)
| ~ mem(U_43,U_45)
| ~ mem(U_44,arr(U_45,bool))
| ~ ne(U_45) ),
inference(clausify,[status(thm)],[f_25_2]) ).
fof(f_26_1,plain,
! [A_27a] :
( ! [V0s] :
( ap(c_2Epred__set_2EREST(A_27a),V0s) = ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),ap(c_2Epred__set_2ECHOICE(A_27a),V0s))
| ~ mem(V0s,arr(A_27a,bool)) )
| ~ ne(A_27a) ),
inference(fof_nnf,[status(thm)],[ax_thm_2Epred__set_2EREST__DEF]) ).
fof(f_26_2,plain,
! [U_47] :
( ! [U_46] :
( ap(c_2Epred__set_2EREST(U_47),U_46) = ap(ap(c_2Epred__set_2EDELETE(U_47),U_46),ap(c_2Epred__set_2ECHOICE(U_47),U_46))
| ~ mem(U_46,arr(U_47,bool)) )
| ~ ne(U_47) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
cnf(f_26_3,plain,
( ap(c_2Epred__set_2EREST(U_47),U_46) = ap(ap(c_2Epred__set_2EDELETE(U_47),U_46),ap(c_2Epred__set_2ECHOICE(U_47),U_46))
| ~ mem(U_46,arr(U_47,bool))
| ~ ne(U_47) ),
inference(clausify,[status(thm)],[f_26_2]) ).
fof(f_27_1,negated_conjecture,
~ ! [A_27a] :
( ne(A_27a)
=> ! [V0s] :
( mem(V0s,arr(A_27a,bool))
=> p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Epred__set_2EREST(A_27a),V0s)),V0s)) ) ),
inference(negate,[status(cth)],[conj_thm_2Epred__set_2EREST__SUBSET]) ).
fof(f_27_2,negated_conjecture,
? [A_27a] :
( ? [V0s] :
( ~ p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Epred__set_2EREST(A_27a),V0s)),V0s))
& mem(V0s,arr(A_27a,bool)) )
& ne(A_27a) ),
inference(fof_nnf,[status(thm)],[f_27_1]) ).
fof(f_27_3,negated_conjecture,
? [U_49] :
( ? [U_48] :
( ~ p(ap(ap(c_2Epred__set_2ESUBSET(U_49),ap(c_2Epred__set_2EREST(U_49),U_48)),U_48))
& mem(U_48,arr(U_49,bool)) )
& ne(U_49) ),
inference(variable_rename,[status(thm)],[f_27_2]) ).
fof(f_27_4,negated_conjecture,
( ? [U_48] :
( ~ p(ap(ap(c_2Epred__set_2ESUBSET(sK4),ap(c_2Epred__set_2EREST(sK4),U_48)),U_48))
& mem(U_48,arr(sK4,bool)) )
& ne(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_49,sK4)],[f_27_3]) ).
fof(f_27_5,negated_conjecture,
( ~ p(ap(ap(c_2Epred__set_2ESUBSET(sK4),ap(c_2Epred__set_2EREST(sK4),sK5)),sK5))
& mem(sK5,arr(sK4,bool))
& ne(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_48,sK5)],[f_27_4]) ).
cnf(f_27_6,negated_conjecture,
ne(sK4),
inference(clausify,[status(thm)],[f_27_5]) ).
cnf(f_27_7,negated_conjecture,
mem(sK5,arr(sK4,bool)),
inference(clausify,[status(thm)],[f_27_5]) ).
cnf(f_27_8,negated_conjecture,
~ p(ap(ap(c_2Epred__set_2ESUBSET(sK4),ap(c_2Epred__set_2EREST(sK4),sK5)),sK5)),
inference(clausify,[status(thm)],[f_27_5]) ).
cnf(f_5_4_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_5_4]) ).
cnf(f_5_5_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_5_5]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( arr(Eq_x_0,Eq_x_1) = arr(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( ap(Eq_x_0,Eq_x_1) = ap(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( k(Eq_x_0,Eq_x_1) = k(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( i(Eq_x_0) = i(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( c_2Epred__set_2ESUBSET(Eq_x_0) = c_2Epred__set_2ESUBSET(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( c_2Ebool_2EIN(Eq_x_0) = c_2Ebool_2EIN(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( c_2Epred__set_2ECHOICE(Eq_x_0) = c_2Epred__set_2ECHOICE(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( c_2Epred__set_2EDELETE(Eq_x_0) = c_2Epred__set_2EDELETE(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( c_2Epred__set_2EREST(Eq_x_0) = c_2Epred__set_2EREST(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( c_2Emin_2E_3D(Eq_x_0) = c_2Emin_2E_3D(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( c_2Ebool_2E_21(Eq_x_0) = c_2Ebool_2E_21(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( sK1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( sK2(Eq_x_0,Eq_x_1) = sK2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( sK3(Eq_x_0,Eq_x_1,Eq_x_2) = sK3(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( ne(Eq_y_0)
| ~ ne(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( mem(Eq_y_0,Eq_y_1)
| ~ mem(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( p(Eq_y_0)
| ~ p(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP004+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n007.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 19 11:17:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 166.04/166.37 % SZS status Theorem for theBenchmark
% 166.04/166.37 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------