%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV902-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.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 : Fri Sep 25 03:14:27 PM UTC 2026
% Result : Unsatisfiable 112.77s 16.79s
% Output : Proof 112.77s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t182,axiom,
sF1 = c_Finite__Set_Ofinite(v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
introduced(definition) ).
cnf(t181,axiom,
sF0 = tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),
introduced(definition) ).
cnf(t209,plain,
tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate) = sF0,
inference(orient,[status(thm)],[t181]) ).
cnf(t17784,plain,
sF1 = c_Finite__Set_Ofinite(v_Fa,sF0),
inference(step,[status(thm)],[t182,t209]) ).
cnf(f680,negated_conjecture,
c_Finite__Set_Ofinite(v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f680_nnf,plain,
c_Finite__Set_Ofinite(v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(nnf_transformation,[status(thm)],[f680]) ).
cnf(c680,plain,
c_Finite__Set_Ofinite(v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(cnf_transformation,[status(esa)],[f680_nnf]) ).
cnf(t1,plain,
c_Finite__Set_Ofinite(v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)) = true,
inference(equality_encoding,[status(esa)],[c680]) ).
cnf(t17783,plain,
c_Finite__Set_Ofinite(v_Fa,sF0) = true,
inference(step,[status(thm)],[t1,t209]) ).
cnf(t219,plain,
c_Finite__Set_Ofinite(v_Fa,sF0) = true,
inference(orient,[status(thm)],[t17783]) ).
cnf(t17785,plain,
sF1 = true,
inference(step,[status(thm)],[t17784,t219]) ).
cnf(t221,plain,
true = sF1,
inference(orient,[status(thm)],[t17785]) ).
cnf(t187,axiom,
sF6 = hBOOL(c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate))),
introduced(definition) ).
cnf(t185,axiom,
sF4 = hAPP(c_Hoare__Mirabelle_OMGT,v_y),
introduced(definition) ).
cnf(t217,plain,
hAPP(c_Hoare__Mirabelle_OMGT,v_y) = sF4,
inference(orient,[status(thm)],[t185]) ).
cnf(t17825,plain,
sF6 = hBOOL(c_in(sF4,v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate))),
inference(step,[status(thm)],[t187,t217]) ).
cnf(t17826,plain,
sF6 = hBOOL(c_in(sF4,v_Fa,sF0)),
inference(step,[status(thm)],[t17825,t209]) ).
cnf(t186,axiom,
sF5 = c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
introduced(definition) ).
cnf(t17804,plain,
sF5 = c_in(sF4,v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(step,[status(thm)],[t186,t217]) ).
cnf(t17805,plain,
sF5 = c_in(sF4,v_Fa,sF0),
inference(step,[status(thm)],[t17804,t209]) ).
cnf(t250,plain,
c_in(sF4,v_Fa,sF0) = sF5,
inference(orient,[status(thm)],[t17805]) ).
cnf(t17827,plain,
sF6 = hBOOL(sF5),
inference(step,[status(thm)],[t17826,t250]) ).
cnf(f681,negated_conjecture,
~ hBOOL(c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f681_nnf,plain,
~ hBOOL(c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate))),
inference(nnf_transformation,[status(thm)],[f681]) ).
fof(f681_sk,plain,
~ hBOOL(c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate))),
inference(skolemisation,[status(esa)],[f681_nnf]) ).
cnf(c681,plain,
~ hBOOL(c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate))),
inference(cnf_transformation,[status(esa)],[f681_sk]) ).
cnf(t18,plain,
hBOOL(c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate))) = false,
inference(equality_encoding,[status(esa)],[c681]) ).
cnf(t17813,plain,
hBOOL(c_in(sF4,v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate))) = false,
inference(step,[status(thm)],[t18,t217]) ).
cnf(t17814,plain,
hBOOL(c_in(sF4,v_Fa,sF0)) = false,
inference(step,[status(thm)],[t17813,t209]) ).
cnf(t17815,plain,
hBOOL(sF5) = false,
inference(step,[status(thm)],[t17814,t250]) ).
cnf(t260,plain,
hBOOL(sF5) = false,
inference(orient,[status(thm)],[t17815]) ).
cnf(t17828,plain,
sF6 = false,
inference(step,[status(thm)],[t17827,t260]) ).
cnf(t274,plain,
false = sF6,
inference(orient,[status(thm)],[t17828]) ).
cnf(f669,axiom,
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_asm_0) ).
fof(f669_nnf,plain,
! [V_G,V_ts,T_a] :
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
inference(nnf_transformation,[status(thm)],[f669]) ).
fof(f669_sk,plain,
! [V_G,V_ts,T_a] :
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
inference(skolemisation,[status(esa)],[f669_nnf]) ).
cnf(c669,plain,
( ~ c_lessequals(X1,X0,tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f669_sk]) ).
cnf(t66,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),true,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c669]) ).
cnf(t17980,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),true) = true,
inference(step,[status(thm)],[t66,t221]) ).
cnf(t17981,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),sF1) = true,
inference(step,[status(thm)],[t17980,t221]) ).
cnf(t17982,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),sF1) = sF1,
inference(step,[status(thm)],[t17981,t221]) ).
cnf(t998,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),sF1) = sF1,
inference(orient,[status(thm)],[t17982]) ).
cnf(t999,plain,
sF1 = ifeq(c_lessequals(X1,X2,tc_fun(sF0,tc_bool)),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,tc_Com_Ostate),sF1),
inference(cp,[status(thm)],[t998,t209]) ).
cnf(t200,axiom,
sF19 = tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool),
introduced(definition) ).
cnf(t17790,plain,
sF19 = tc_fun(sF0,tc_bool),
inference(step,[status(thm)],[t200,t209]) ).
cnf(t227,plain,
tc_fun(sF0,tc_bool) = sF19,
inference(orient,[status(thm)],[t17790]) ).
cnf(t18072,plain,
sF1 = ifeq(c_lessequals(X1,X2,sF19),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,tc_Com_Ostate),sF1),
inference(step,[status(thm)],[t999,t227]) ).
cnf(t1605,plain,
ifeq(c_lessequals(X1,X2,sF19),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,tc_Com_Ostate),sF1) = sF1,
inference(orient,[status(thm)],[t18072]) ).
cnf(f576,axiom,
( ~ c_lessequals(V_C,V_D,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_a,V_C,T_a),c_Set_Oinsert(V_a,V_D,T_a),tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__mono_0) ).
fof(f576_nnf,plain,
! [V_a,V_C,T_a,V_D] :
( ~ c_lessequals(V_C,V_D,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_a,V_C,T_a),c_Set_Oinsert(V_a,V_D,T_a),tc_fun(T_a,tc_bool)) ),
inference(nnf_transformation,[status(thm)],[f576]) ).
fof(f576_sk,plain,
! [V_a,V_C,T_a,V_D] :
( ~ c_lessequals(V_C,V_D,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_a,V_C,T_a),c_Set_Oinsert(V_a,V_D,T_a),tc_fun(T_a,tc_bool)) ),
inference(skolemisation,[status(esa)],[f576_nnf]) ).
cnf(c576,plain,
( ~ c_lessequals(X1,X3,tc_fun(X2,tc_bool))
| c_lessequals(c_Set_Oinsert(X0,X1,X2),c_Set_Oinsert(X0,X3,X2),tc_fun(X2,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f576_sk]) ).
cnf(t123,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),true,c_lessequals(c_Set_Oinsert(X4,X1,X3),c_Set_Oinsert(X4,X2,X3),tc_fun(X3,tc_bool)),true) = true,
inference(equality_encoding,[status(esa)],[c576]) ).
cnf(t18436,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),sF1,c_lessequals(c_Set_Oinsert(X4,X1,X3),c_Set_Oinsert(X4,X2,X3),tc_fun(X3,tc_bool)),true) = true,
inference(step,[status(thm)],[t123,t221]) ).
cnf(t18437,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),sF1,c_lessequals(c_Set_Oinsert(X4,X1,X3),c_Set_Oinsert(X4,X2,X3),tc_fun(X3,tc_bool)),sF1) = true,
inference(step,[status(thm)],[t18436,t221]) ).
cnf(t18438,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),sF1,c_lessequals(c_Set_Oinsert(X4,X1,X3),c_Set_Oinsert(X4,X2,X3),tc_fun(X3,tc_bool)),sF1) = sF1,
inference(step,[status(thm)],[t18437,t221]) ).
cnf(t5207,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),sF1,c_lessequals(c_Set_Oinsert(X4,X1,X3),c_Set_Oinsert(X4,X2,X3),tc_fun(X3,tc_bool)),sF1) = sF1,
inference(orient,[status(thm)],[t18438]) ).
cnf(t205,axiom,
sF24 = c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
introduced(definition) ).
cnf(f605,axiom,
c_Set_Oimage(V_f,c_Set_Oinsert(V_a,V_B,T_b),T_b,T_a) = c_Set_Oinsert(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_B,T_b,T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_image__insert_0) ).
fof(f605_nnf,plain,
! [V_f,V_a,V_B,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oinsert(V_a,V_B,T_b),T_b,T_a) = c_Set_Oinsert(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_B,T_b,T_a),T_a),
inference(nnf_transformation,[status(thm)],[f605]) ).
fof(f605_sk,plain,
! [V_f,V_a,V_B,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oinsert(V_a,V_B,T_b),T_b,T_a) = c_Set_Oinsert(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_B,T_b,T_a),T_a),
inference(skolemisation,[status(esa)],[f605_nnf]) ).
cnf(c605,plain,
c_Set_Oimage(X0,c_Set_Oinsert(X1,X2,X3),X3,X4) = c_Set_Oinsert(hAPP(X0,X1),c_Set_Oimage(X0,X2,X3,X4),X4),
inference(cnf_transformation,[status(esa)],[f605_sk]) ).
cnf(t88,plain,
c_Set_Oinsert(hAPP(X1,X2),c_Set_Oimage(X1,X3,X4,X5),X5) = c_Set_Oimage(X1,c_Set_Oinsert(X2,X3,X4),X4,X5),
inference(equality_encoding,[status(esa)],[c605]) ).
cnf(t2318,plain,
c_Set_Oinsert(hAPP(X1,X2),c_Set_Oimage(X1,X3,X4,X5),X5) = c_Set_Oimage(X1,c_Set_Oinsert(X2,X3,X4),X4,X5),
inference(orient,[status(thm)],[t88]) ).
cnf(f655,axiom,
c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_image__empty_0) ).
fof(f655_nnf,plain,
! [V_f,T_b,T_a] : c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f655]) ).
fof(f655_sk,plain,
! [V_f,T_b,T_a] : c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f655_nnf]) ).
cnf(c655,plain,
c_Set_Oimage(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1,X2) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f655_sk]) ).
cnf(t32,plain,
c_Set_Oimage(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2,X3) = c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),
inference(equality_encoding,[status(esa)],[c655]) ).
cnf(t265,plain,
c_Set_Oimage(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2,X3) = c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),
inference(orient,[status(thm)],[t32]) ).
cnf(t266,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = c_Set_Oimage(X2,c_Orderings_Obot__class_Obot(sF19),sF0,X1),
inference(cp,[status(thm)],[t265,t227]) ).
cnf(t204,axiom,
sF23 = c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),
introduced(definition) ).
cnf(t17792,plain,
sF23 = c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)),
inference(step,[status(thm)],[t204,t209]) ).
cnf(t17793,plain,
sF23 = c_Orderings_Obot__class_Obot(sF19),
inference(step,[status(thm)],[t17792,t227]) ).
cnf(t229,plain,
c_Orderings_Obot__class_Obot(sF19) = sF23,
inference(orient,[status(thm)],[t17793]) ).
cnf(t17822,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = c_Set_Oimage(X2,sF23,sF0,X1),
inference(step,[status(thm)],[t266,t229]) ).
cnf(t267,plain,
c_Set_Oimage(X1,sF23,sF0,X2) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(orient,[status(thm)],[t17822]) ).
cnf(t2327,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF23,sF0),sF0,X3) = c_Set_Oinsert(hAPP(X1,X2),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3),
inference(cp,[status(thm)],[t2318,t267]) ).
cnf(t2374,plain,
c_Set_Oinsert(hAPP(X1,X2),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3) = c_Set_Oimage(X1,c_Set_Oinsert(X2,sF23,sF0),sF0,X3),
inference(orient,[status(thm)],[t2327]) ).
cnf(t19076,plain,
sF24 = c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oinsert(hAPP(c_Com_Ocom_OBODY,v_x),sF23,sF0),sF0,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(step,[status(thm)],[t205,t2374]) ).
cnf(f653,axiom,
hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R) = hAPP(V_P,hAPP(V_Q,V_R)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBB__def_0) ).
fof(f653_nnf,plain,
! [V_P,V_Q,T_b,T_a,T_c,V_R] : hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R) = hAPP(V_P,hAPP(V_Q,V_R)),
inference(nnf_transformation,[status(thm)],[f653]) ).
fof(f653_sk,plain,
! [V_P,V_Q,T_b,T_a,T_c,V_R] : hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R) = hAPP(V_P,hAPP(V_Q,V_R)),
inference(skolemisation,[status(esa)],[f653_nnf]) ).
cnf(c653,plain,
hAPP(c_COMBB(X0,X1,X2,X3,X4),X5) = hAPP(X0,hAPP(X1,X5)),
inference(cnf_transformation,[status(esa)],[f653_sk]) ).
cnf(t44,plain,
hAPP(c_COMBB(X1,X2,X3,X4,X5),X6) = hAPP(X1,hAPP(X2,X6)),
inference(equality_encoding,[status(esa)],[c653]) ).
cnf(t268,plain,
hAPP(c_COMBB(X1,X2,X3,X4,X5),X6) = hAPP(X1,hAPP(X2,X6)),
inference(orient,[status(thm)],[t44]) ).
cnf(t192,axiom,
sF11 = c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),
introduced(definition) ).
cnf(t17810,plain,
sF11 = c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,sF0,tc_Com_Opname),
inference(step,[status(thm)],[t192,t209]) ).
cnf(t255,plain,
c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,sF0,tc_Com_Opname) = sF11,
inference(orient,[status(thm)],[t17810]) ).
cnf(t269,plain,
hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,X1)) = hAPP(sF11,X1),
inference(cp,[status(thm)],[t268,t255]) ).
cnf(t270,plain,
hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,X1)) = hAPP(sF11,X1),
inference(orient,[status(thm)],[t269]) ).
cnf(t2384,plain,
c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oinsert(hAPP(c_Com_Ocom_OBODY,X1),sF23,sF0),sF0,X2) = c_Set_Oinsert(hAPP(sF11,X1),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),
inference(cp,[status(thm)],[t2374,t270]) ).
cnf(t18155,plain,
c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oinsert(hAPP(c_Com_Ocom_OBODY,X1),sF23,sF0),sF0,X2) = c_Set_Oimage(sF11,c_Set_Oinsert(X1,sF23,sF0),sF0,X2),
inference(step,[status(thm)],[t2384,t2374]) ).
cnf(t2406,plain,
c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oinsert(hAPP(c_Com_Ocom_OBODY,X1),sF23,sF0),sF0,X2) = c_Set_Oimage(sF11,c_Set_Oinsert(X1,sF23,sF0),sF0,X2),
inference(orient,[status(thm)],[t18155]) ).
cnf(t19077,plain,
sF24 = c_Set_Oimage(sF11,c_Set_Oinsert(v_x,sF23,sF0),sF0,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(step,[status(thm)],[t19076,t2406]) ).
cnf(t19078,plain,
sF24 = c_Set_Oimage(sF11,c_Set_Oinsert(v_x,sF23,sF0),sF0,sF0),
inference(step,[status(thm)],[t19077,t209]) ).
cnf(t2378,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF23,sF0),sF0,sF0) = c_Set_Oinsert(hAPP(X1,X2),c_Orderings_Obot__class_Obot(sF19),sF0),
inference(cp,[status(thm)],[t2374,t227]) ).
cnf(t18154,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF23,sF0),sF0,sF0) = c_Set_Oinsert(hAPP(X1,X2),sF23,sF0),
inference(step,[status(thm)],[t2378,t229]) ).
cnf(t2404,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF23,sF0),sF0,sF0) = c_Set_Oinsert(hAPP(X1,X2),sF23,sF0),
inference(orient,[status(thm)],[t18154]) ).
cnf(t19079,plain,
sF24 = c_Set_Oinsert(hAPP(sF11,v_x),sF23,sF0),
inference(step,[status(thm)],[t19078,t2404]) ).
cnf(t202,axiom,
sF21 = hAPP(c_Com_Ocom_OBODY,v_x),
introduced(definition) ).
cnf(t218,plain,
hAPP(c_Com_Ocom_OBODY,v_x) = sF21,
inference(orient,[status(thm)],[t202]) ).
cnf(t271,plain,
hAPP(sF11,v_x) = hAPP(c_Hoare__Mirabelle_OMGT,sF21),
inference(cp,[status(thm)],[t270,t218]) ).
cnf(t203,axiom,
sF22 = hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),
introduced(definition) ).
cnf(t17791,plain,
sF22 = hAPP(c_Hoare__Mirabelle_OMGT,sF21),
inference(step,[status(thm)],[t203,t218]) ).
cnf(t228,plain,
hAPP(c_Hoare__Mirabelle_OMGT,sF21) = sF22,
inference(orient,[status(thm)],[t17791]) ).
cnf(t17823,plain,
hAPP(sF11,v_x) = sF22,
inference(step,[status(thm)],[t271,t228]) ).
cnf(t272,plain,
hAPP(sF11,v_x) = sF22,
inference(orient,[status(thm)],[t17823]) ).
cnf(t19080,plain,
sF24 = c_Set_Oinsert(sF22,sF23,sF0),
inference(step,[status(thm)],[t19079,t272]) ).
cnf(t16944,plain,
c_Set_Oinsert(sF22,sF23,sF0) = sF24,
inference(orient,[status(thm)],[t19080]) ).
cnf(t16999,plain,
sF1 = ifeq(c_lessequals(sF23,X1,tc_fun(sF0,tc_bool)),sF1,c_lessequals(sF24,c_Set_Oinsert(sF22,X1,sF0),tc_fun(sF0,tc_bool)),sF1),
inference(cp,[status(thm)],[t5207,t16944]) ).
cnf(t19141,plain,
sF1 = ifeq(c_lessequals(sF23,X1,sF19),sF1,c_lessequals(sF24,c_Set_Oinsert(sF22,X1,sF0),tc_fun(sF0,tc_bool)),sF1),
inference(step,[status(thm)],[t16999,t227]) ).
cnf(f638,axiom,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__subsetI_0) ).
fof(f638_nnf,plain,
! [T_a,V_A] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f638]) ).
fof(f638_sk,plain,
! [T_a,V_A] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f638_nnf]) ).
cnf(c638,plain,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(esa)],[f638_sk]) ).
cnf(t28,plain,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,tc_fun(X1,tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c638]) ).
cnf(t17854,plain,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,tc_fun(X1,tc_bool)) = sF1,
inference(step,[status(thm)],[t28,t221]) ).
cnf(t306,plain,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,tc_fun(X1,tc_bool)) = sF1,
inference(orient,[status(thm)],[t17854]) ).
cnf(t307,plain,
sF1 = c_lessequals(c_Orderings_Obot__class_Obot(sF19),X1,tc_fun(sF0,tc_bool)),
inference(cp,[status(thm)],[t306,t227]) ).
cnf(t17855,plain,
sF1 = c_lessequals(sF23,X1,tc_fun(sF0,tc_bool)),
inference(step,[status(thm)],[t307,t229]) ).
cnf(t17856,plain,
sF1 = c_lessequals(sF23,X1,sF19),
inference(step,[status(thm)],[t17855,t227]) ).
cnf(t308,plain,
c_lessequals(sF23,X1,sF19) = sF1,
inference(orient,[status(thm)],[t17856]) ).
cnf(t19142,plain,
sF1 = ifeq(sF1,sF1,c_lessequals(sF24,c_Set_Oinsert(sF22,X1,sF0),tc_fun(sF0,tc_bool)),sF1),
inference(step,[status(thm)],[t19141,t308]) ).
cnf(t3,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t220,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t19143,plain,
sF1 = c_lessequals(sF24,c_Set_Oinsert(sF22,X1,sF0),tc_fun(sF0,tc_bool)),
inference(step,[status(thm)],[t19142,t220]) ).
cnf(t19144,plain,
sF1 = c_lessequals(sF24,c_Set_Oinsert(sF22,X1,sF0),sF19),
inference(step,[status(thm)],[t19143,t227]) ).
cnf(t17596,plain,
c_lessequals(sF24,c_Set_Oinsert(sF22,X1,sF0),sF19) = sF1,
inference(orient,[status(thm)],[t19144]) ).
cnf(f671,axiom,
( ~ hBOOL(c_in(V_a,V_A,T_a))
| c_Set_Oinsert(V_a,V_A,T_a) = V_A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__absorb_0) ).
fof(f671_nnf,plain,
! [V_a,V_A,T_a] :
( ~ hBOOL(c_in(V_a,V_A,T_a))
| c_Set_Oinsert(V_a,V_A,T_a) = V_A ),
inference(nnf_transformation,[status(thm)],[f671]) ).
fof(f671_sk,plain,
! [V_a,V_A,T_a] :
( ~ hBOOL(c_in(V_a,V_A,T_a))
| c_Set_Oinsert(V_a,V_A,T_a) = V_A ),
inference(skolemisation,[status(esa)],[f671_nnf]) ).
cnf(c671,plain,
( ~ hBOOL(c_in(X0,X1,X2))
| c_Set_Oinsert(X0,X1,X2) = X1 ),
inference(cnf_transformation,[status(esa)],[f671_sk]) ).
cnf(t48,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),true,c_Set_Oinsert(X1,X2,X3),X2) = X2,
inference(equality_encoding,[status(esa)],[c671]) ).
cnf(t17908,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),sF1,c_Set_Oinsert(X1,X2,X3),X2) = X2,
inference(step,[status(thm)],[t48,t221]) ).
cnf(t398,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),sF1,c_Set_Oinsert(X1,X2,X3),X2) = X2,
inference(orient,[status(thm)],[t17908]) ).
cnf(f195,axiom,
( ~ hBOOL(hAPP(V_P,V_a))
| hBOOL(c_in(V_a,c_Collect(V_P,T_a),T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CollectI_0) ).
fof(f195_nnf,plain,
! [V_a,V_P,T_a] :
( ~ hBOOL(hAPP(V_P,V_a))
| hBOOL(c_in(V_a,c_Collect(V_P,T_a),T_a)) ),
inference(nnf_transformation,[status(thm)],[f195]) ).
fof(f195_sk,plain,
! [V_a,V_P,T_a] :
( ~ hBOOL(hAPP(V_P,V_a))
| hBOOL(c_in(V_a,c_Collect(V_P,T_a),T_a)) ),
inference(skolemisation,[status(esa)],[f195_nnf]) ).
cnf(c195,plain,
( ~ hBOOL(hAPP(X1,X0))
| hBOOL(c_in(X0,c_Collect(X1,X2),X2)) ),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
cnf(u7,axiom,
ifeq(hBOOL(hAPP(X0,X1)),true,hBOOL(c_in(X1,c_Collect(X0,X2),X2)),true) = true,
inference(equality_encoding,[status(esa)],[c195]) ).
cnf(f111,axiom,
c_Collect(V_P,T_a) = V_P,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__def_0) ).
fof(f111_nnf,plain,
! [V_P,T_a] : c_Collect(V_P,T_a) = V_P,
inference(nnf_transformation,[status(thm)],[f111]) ).
fof(f111_sk,plain,
! [V_P,T_a] : c_Collect(V_P,T_a) = V_P,
inference(skolemisation,[status(esa)],[f111_nnf]) ).
cnf(c111,plain,
c_Collect(X0,X1) = X0,
inference(cnf_transformation,[status(esa)],[f111_sk]) ).
cnf(d1,axiom,
c_Collect(X0,X1) = X0,
inference(equality_encoding,[status(esa)],[c111]) ).
cnf(t55,plain,
ifeq(hBOOL(hAPP(X1,X2)),true,hBOOL(c_in(X2,X1,X3)),true) = true,
inference(definition_unfolding,[status(thm)],[u7,d1]) ).
cnf(t17916,plain,
ifeq(hBOOL(hAPP(X1,X2)),sF1,hBOOL(c_in(X2,X1,X3)),true) = true,
inference(step,[status(thm)],[t55,t221]) ).
cnf(t17917,plain,
ifeq(hBOOL(hAPP(X1,X2)),sF1,hBOOL(c_in(X2,X1,X3)),sF1) = true,
inference(step,[status(thm)],[t17916,t221]) ).
cnf(t17918,plain,
ifeq(hBOOL(hAPP(X1,X2)),sF1,hBOOL(c_in(X2,X1,X3)),sF1) = sF1,
inference(step,[status(thm)],[t17917,t221]) ).
cnf(t476,plain,
ifeq(hBOOL(hAPP(X1,X2)),sF1,hBOOL(c_in(X2,X1,X3)),sF1) = sF1,
inference(orient,[status(thm)],[t17918]) ).
cnf(f604,axiom,
hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__code_1) ).
fof(f604_nnf,plain,
! [V_x,V_A,T_a] : hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)),
inference(nnf_transformation,[status(thm)],[f604]) ).
fof(f604_sk,plain,
! [V_x,V_A,T_a] : hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)),
inference(skolemisation,[status(esa)],[f604_nnf]) ).
cnf(c604,plain,
hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t10,plain,
hBOOL(hAPP(c_Set_Oinsert(X1,X2,X3),X1)) = true,
inference(equality_encoding,[status(esa)],[c604]) ).
cnf(t17803,plain,
hBOOL(hAPP(c_Set_Oinsert(X1,X2,X3),X1)) = sF1,
inference(step,[status(thm)],[t10,t221]) ).
cnf(t248,plain,
hBOOL(hAPP(c_Set_Oinsert(X1,X2,X3),X1)) = sF1,
inference(orient,[status(thm)],[t17803]) ).
cnf(t486,plain,
sF1 = ifeq(sF1,sF1,hBOOL(c_in(X1,c_Set_Oinsert(X1,X2,X3),X4)),sF1),
inference(cp,[status(thm)],[t476,t248]) ).
cnf(t17922,plain,
sF1 = hBOOL(c_in(X1,c_Set_Oinsert(X1,X2,X3),X4)),
inference(step,[status(thm)],[t486,t220]) ).
cnf(t544,plain,
hBOOL(c_in(X1,c_Set_Oinsert(X1,X2,X3),X4)) = sF1,
inference(orient,[status(thm)],[t17922]) ).
cnf(t546,plain,
c_Set_Oinsert(X1,X2,X3) = ifeq(sF1,sF1,c_Set_Oinsert(X1,c_Set_Oinsert(X1,X2,X3),X4),c_Set_Oinsert(X1,X2,X3)),
inference(cp,[status(thm)],[t398,t544]) ).
cnf(t17924,plain,
c_Set_Oinsert(X1,X2,X3) = c_Set_Oinsert(X1,c_Set_Oinsert(X1,X2,X3),X4),
inference(step,[status(thm)],[t546,t220]) ).
cnf(t547,plain,
c_Set_Oinsert(X1,c_Set_Oinsert(X1,X2,X3),X4) = c_Set_Oinsert(X1,X2,X3),
inference(orient,[status(thm)],[t17924]) ).
cnf(f674,axiom,
( hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a))
| ~ hBOOL(c_in(V_x,V_A,T_aa)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_rev__image__eqI_0) ).
fof(f674_nnf,plain,
! [V_x,V_A,T_aa,V_f,T_a] :
( hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a))
| ~ hBOOL(c_in(V_x,V_A,T_aa)) ),
inference(nnf_transformation,[status(thm)],[f674]) ).
fof(f674_sk,plain,
! [V_x,V_A,T_aa,V_f,T_a] :
( hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a))
| ~ hBOOL(c_in(V_x,V_A,T_aa)) ),
inference(skolemisation,[status(esa)],[f674_nnf]) ).
cnf(c674,plain,
( hBOOL(c_in(hAPP(X3,X0),c_Set_Oimage(X3,X1,X2,X4),X4))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f674_sk]) ).
cnf(t109,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),true,hBOOL(c_in(hAPP(X4,X1),c_Set_Oimage(X4,X2,X3,X5),X5)),true) = true,
inference(equality_encoding,[status(esa)],[c674]) ).
cnf(t18309,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),sF1,hBOOL(c_in(hAPP(X4,X1),c_Set_Oimage(X4,X2,X3,X5),X5)),true) = true,
inference(step,[status(thm)],[t109,t221]) ).
cnf(t18310,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),sF1,hBOOL(c_in(hAPP(X4,X1),c_Set_Oimage(X4,X2,X3,X5),X5)),sF1) = true,
inference(step,[status(thm)],[t18309,t221]) ).
cnf(t18311,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),sF1,hBOOL(c_in(hAPP(X4,X1),c_Set_Oimage(X4,X2,X3,X5),X5)),sF1) = sF1,
inference(step,[status(thm)],[t18310,t221]) ).
cnf(t3685,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),sF1,hBOOL(c_in(hAPP(X4,X1),c_Set_Oimage(X4,X2,X3,X5),X5)),sF1) = sF1,
inference(orient,[status(thm)],[t18311]) ).
cnf(t189,axiom,
sF8 = c_in(v_x,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
introduced(definition) ).
cnf(t188,axiom,
sF7 = c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),
introduced(definition) ).
cnf(t226,plain,
c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom) = sF7,
inference(orient,[status(thm)],[t188]) ).
cnf(t17809,plain,
sF8 = c_in(v_x,sF7,tc_Com_Opname),
inference(step,[status(thm)],[t189,t226]) ).
cnf(t254,plain,
c_in(v_x,sF7,tc_Com_Opname) = sF8,
inference(orient,[status(thm)],[t17809]) ).
cnf(t400,plain,
sF7 = ifeq(hBOOL(sF8),sF1,c_Set_Oinsert(v_x,sF7,tc_Com_Opname),sF7),
inference(cp,[status(thm)],[t398,t254]) ).
cnf(f685,negated_conjecture,
hBOOL(c_in(v_x,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f685_nnf,plain,
hBOOL(c_in(v_x,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)),
inference(nnf_transformation,[status(thm)],[f685]) ).
cnf(c685,plain,
hBOOL(c_in(v_x,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)),
inference(cnf_transformation,[status(esa)],[f685_nnf]) ).
cnf(t19,plain,
hBOOL(c_in(v_x,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)) = true,
inference(equality_encoding,[status(esa)],[c685]) ).
cnf(t17816,plain,
hBOOL(c_in(v_x,sF7,tc_Com_Opname)) = true,
inference(step,[status(thm)],[t19,t226]) ).
cnf(t17817,plain,
hBOOL(sF8) = true,
inference(step,[status(thm)],[t17816,t254]) ).
cnf(t17818,plain,
hBOOL(sF8) = sF1,
inference(step,[status(thm)],[t17817,t221]) ).
cnf(t261,plain,
hBOOL(sF8) = sF1,
inference(orient,[status(thm)],[t17818]) ).
cnf(t17909,plain,
sF7 = ifeq(sF1,sF1,c_Set_Oinsert(v_x,sF7,tc_Com_Opname),sF7),
inference(step,[status(thm)],[t400,t261]) ).
cnf(t17910,plain,
sF7 = c_Set_Oinsert(v_x,sF7,tc_Com_Opname),
inference(step,[status(thm)],[t17909,t220]) ).
cnf(t403,plain,
c_Set_Oinsert(v_x,sF7,tc_Com_Opname) = sF7,
inference(orient,[status(thm)],[t17910]) ).
cnf(t404,plain,
sF1 = hBOOL(hAPP(sF7,v_x)),
inference(cp,[status(thm)],[t248,t403]) ).
cnf(t409,plain,
hBOOL(hAPP(sF7,v_x)) = sF1,
inference(orient,[status(thm)],[t404]) ).
cnf(t497,plain,
sF1 = ifeq(sF1,sF1,hBOOL(c_in(v_x,sF7,X1)),sF1),
inference(cp,[status(thm)],[t476,t409]) ).
cnf(t17919,plain,
sF1 = hBOOL(c_in(v_x,sF7,X1)),
inference(step,[status(thm)],[t497,t220]) ).
cnf(t500,plain,
hBOOL(c_in(v_x,sF7,X1)) = sF1,
inference(orient,[status(thm)],[t17919]) ).
cnf(t3703,plain,
sF1 = ifeq(sF1,sF1,hBOOL(c_in(hAPP(X1,v_x),c_Set_Oimage(X1,sF7,X2,X3),X3)),sF1),
inference(cp,[status(thm)],[t3685,t500]) ).
cnf(t18355,plain,
sF1 = hBOOL(c_in(hAPP(X1,v_x),c_Set_Oimage(X1,sF7,X2,X3),X3)),
inference(step,[status(thm)],[t3703,t220]) ).
cnf(t4458,plain,
hBOOL(c_in(hAPP(X1,v_x),c_Set_Oimage(X1,sF7,X2,X3),X3)) = sF1,
inference(orient,[status(thm)],[t18355]) ).
cnf(t4462,plain,
sF1 = hBOOL(c_in(sF22,c_Set_Oimage(sF11,sF7,X1,X2),X2)),
inference(cp,[status(thm)],[t4458,t272]) ).
cnf(t4557,plain,
hBOOL(c_in(sF22,c_Set_Oimage(sF11,sF7,X1,X2),X2)) = sF1,
inference(orient,[status(thm)],[t4462]) ).
cnf(t4558,plain,
c_Set_Oimage(sF11,sF7,X1,X2) = ifeq(sF1,sF1,c_Set_Oinsert(sF22,c_Set_Oimage(sF11,sF7,X1,X2),X2),c_Set_Oimage(sF11,sF7,X1,X2)),
inference(cp,[status(thm)],[t398,t4557]) ).
cnf(t18363,plain,
c_Set_Oimage(sF11,sF7,X1,X2) = c_Set_Oinsert(sF22,c_Set_Oimage(sF11,sF7,X1,X2),X2),
inference(step,[status(thm)],[t4558,t220]) ).
cnf(t4564,plain,
c_Set_Oinsert(sF22,c_Set_Oimage(sF11,sF7,X1,X2),X2) = c_Set_Oimage(sF11,sF7,X1,X2),
inference(orient,[status(thm)],[t18363]) ).
cnf(t4570,plain,
c_Set_Oinsert(sF22,c_Set_Oimage(sF11,sF7,X1,X2),X2) = c_Set_Oinsert(sF22,c_Set_Oimage(sF11,sF7,X1,X2),X3),
inference(cp,[status(thm)],[t547,t4564]) ).
cnf(t18366,plain,
c_Set_Oimage(sF11,sF7,X1,X2) = c_Set_Oinsert(sF22,c_Set_Oimage(sF11,sF7,X1,X2),X3),
inference(step,[status(thm)],[t4570,t4564]) ).
cnf(t4601,plain,
c_Set_Oinsert(sF22,c_Set_Oimage(sF11,sF7,X1,X2),X3) = c_Set_Oimage(sF11,sF7,X1,X2),
inference(orient,[status(thm)],[t18366]) ).
cnf(t193,axiom,
sF12 = c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
introduced(definition) ).
cnf(f602,axiom,
c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_image__image_0) ).
fof(f602_nnf,plain,
! [V_f,V_g,V_A,T_c,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a),
inference(nnf_transformation,[status(thm)],[f602]) ).
fof(f602_sk,plain,
! [V_f,V_g,V_A,T_c,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a),
inference(skolemisation,[status(esa)],[f602_nnf]) ).
cnf(c602,plain,
c_Set_Oimage(X0,c_Set_Oimage(X1,X2,X3,X4),X4,X5) = c_Set_Oimage(c_COMBB(X0,X1,X4,X5,X3),X2,X3,X5),
inference(cnf_transformation,[status(esa)],[f602_sk]) ).
cnf(t94,plain,
c_Set_Oimage(c_COMBB(X1,X2,X3,X4,X5),X6,X5,X4) = c_Set_Oimage(X1,c_Set_Oimage(X2,X6,X5,X3),X3,X4),
inference(equality_encoding,[status(esa)],[c602]) ).
cnf(t2653,plain,
c_Set_Oimage(c_COMBB(X1,X2,X3,X4,X5),X6,X5,X4) = c_Set_Oimage(X1,c_Set_Oimage(X2,X6,X5,X3),X3,X4),
inference(orient,[status(thm)],[t94]) ).
cnf(t19020,plain,
sF12 = c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(step,[status(thm)],[t193,t2653]) ).
cnf(t19021,plain,
sF12 = c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,sF7,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(step,[status(thm)],[t19020,t226]) ).
cnf(t19022,plain,
sF12 = c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,sF7,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,sF0),
inference(step,[status(thm)],[t19021,t209]) ).
cnf(t2654,plain,
c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,X1,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,sF0) = c_Set_Oimage(sF11,X1,tc_Com_Opname,sF0),
inference(cp,[status(thm)],[t2653,t255]) ).
cnf(t2659,plain,
c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,X1,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,sF0) = c_Set_Oimage(sF11,X1,tc_Com_Opname,sF0),
inference(orient,[status(thm)],[t2654]) ).
cnf(t19023,plain,
sF12 = c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0),
inference(step,[status(thm)],[t19022,t2659]) ).
cnf(t16132,plain,
c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0) = sF12,
inference(orient,[status(thm)],[t19023]) ).
cnf(t16143,plain,
c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0) = c_Set_Oinsert(sF22,sF12,X1),
inference(cp,[status(thm)],[t4601,t16132]) ).
cnf(t19028,plain,
sF12 = c_Set_Oinsert(sF22,sF12,X1),
inference(step,[status(thm)],[t16143,t16132]) ).
cnf(t16212,plain,
c_Set_Oinsert(sF22,sF12,X1) = sF12,
inference(orient,[status(thm)],[t19028]) ).
cnf(t17614,plain,
sF1 = c_lessequals(sF24,sF12,sF19),
inference(cp,[status(thm)],[t17596,t16212]) ).
cnf(t17619,plain,
c_lessequals(sF24,sF12,sF19) = sF1,
inference(orient,[status(thm)],[t17614]) ).
cnf(t17620,plain,
sF1 = ifeq(sF1,sF1,c_Hoare__Mirabelle_Ohoare__derivs(sF12,sF24,tc_Com_Ostate),sF1),
inference(cp,[status(thm)],[t1605,t17619]) ).
cnf(t19145,plain,
sF1 = c_Hoare__Mirabelle_Ohoare__derivs(sF12,sF24,tc_Com_Ostate),
inference(step,[status(thm)],[t17620,t220]) ).
cnf(f686,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f686_nnf,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(nnf_transformation,[status(thm)],[f686]) ).
fof(f686_sk,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(skolemisation,[status(esa)],[f686_nnf]) ).
cnf(c686,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(cnf_transformation,[status(esa)],[f686_sk]) ).
cnf(t158,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(equality_encoding,[status(esa)],[c686]) ).
cnf(t18781,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t158,t2653]) ).
cnf(t18782,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,sF7,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t18781,t226]) ).
cnf(t18783,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,sF7,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,sF0),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t18782,t209]) ).
cnf(t18784,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t18783,t2659]) ).
cnf(t18785,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oinsert(hAPP(c_Com_Ocom_OBODY,v_x),sF23,sF0),sF0,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t18784,t2374]) ).
cnf(t18786,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0),c_Set_Oimage(sF11,c_Set_Oinsert(v_x,sF23,sF0),sF0,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t18785,t2406]) ).
cnf(t18787,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0),c_Set_Oimage(sF11,c_Set_Oinsert(v_x,sF23,sF0),sF0,sF0),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t18786,t209]) ).
cnf(t18788,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0),c_Set_Oinsert(hAPP(sF11,v_x),sF23,sF0),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t18787,t2404]) ).
cnf(t18789,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0),c_Set_Oinsert(sF22,sF23,sF0),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t18788,t272]) ).
cnf(t18790,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0),c_Set_Oinsert(sF22,sF23,sF0),tc_Com_Ostate) = sF6,
inference(step,[status(thm)],[t18789,t274]) ).
cnf(t11314,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF11,sF7,tc_Com_Opname,sF0),c_Set_Oinsert(sF22,sF23,sF0),tc_Com_Ostate) = sF6,
inference(orient,[status(thm)],[t18790]) ).
cnf(t19025,plain,
c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(sF22,sF23,sF0),tc_Com_Ostate) = sF6,
inference(step,[status(thm)],[t11314,t16132]) ).
cnf(t16134,plain,
c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(sF22,sF23,sF0),tc_Com_Ostate) = sF6,
inference(rw,[status(thm)],[t19025]) ).
cnf(t16349,plain,
c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(sF22,sF23,sF0),tc_Com_Ostate) = sF6,
inference(orient,[status(thm)],[t16134]) ).
cnf(t19085,plain,
c_Hoare__Mirabelle_Ohoare__derivs(sF12,sF24,tc_Com_Ostate) = sF6,
inference(step,[status(thm)],[t16349,t16944]) ).
cnf(t16949,plain,
c_Hoare__Mirabelle_Ohoare__derivs(sF12,sF24,tc_Com_Ostate) = sF6,
inference(rw,[status(thm)],[t19085]) ).
cnf(t17043,plain,
c_Hoare__Mirabelle_Ohoare__derivs(sF12,sF24,tc_Com_Ostate) = sF6,
inference(orient,[status(thm)],[t16949]) ).
cnf(t19146,plain,
sF1 = sF6,
inference(step,[status(thm)],[t19145,t17043]) ).
cnf(t17621,plain,
sF6 = sF1,
inference(orient,[status(thm)],[t19146]) ).
cnf(t19157,plain,
false = sF1,
inference(step,[status(thm)],[t274,t17621]) ).
cnf(t17632,plain,
false = sF1,
inference(orient,[status(thm)],[t19157]) ).
cnf(f165,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_psubset__eq_1) ).
fof(f165_nnf,plain,
! [V_x,T_a] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f165]) ).
fof(f165_sk,plain,
! [V_x,T_a] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f165_nnf]) ).
cnf(c165,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f165_sk]) ).
cnf(f166,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f166_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f166]) ).
fof(f166_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f166_nnf]) ).
cnf(c166,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
cnf(f167,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f167_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f167]) ).
fof(f167_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f167_nnf]) ).
cnf(c167,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f167_sk]) ).
cnf(f168,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f168_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f168]) ).
fof(f168_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f168_nnf]) ).
cnf(c168,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f168_sk]) ).
cnf(f184,axiom,
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f184_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c184,plain,
( ~ hBOOL(c_in(X0,c_HOL_Ominus__class_Ominus(X3,X1,tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
cnf(f187,axiom,
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f187_nnf,plain,
! [V_c,V_A,T_a] :
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
inference(nnf_transformation,[status(thm)],[f187]) ).
fof(f187_sk,plain,
! [V_c,V_A,T_a] :
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
inference(skolemisation,[status(esa)],[f187_nnf]) ).
cnf(c187,plain,
( ~ hBOOL(c_in(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f187_sk]) ).
cnf(f248,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f248_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f248]) ).
fof(f248_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f248_nnf]) ).
cnf(c248,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f248_sk]) ).
cnf(f250,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f250_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f250]) ).
fof(f250_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f250_nnf]) ).
cnf(c250,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f250_sk]) ).
cnf(f252,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f252_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f252]) ).
fof(f252_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f252_nnf]) ).
cnf(c252,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f252_sk]) ).
cnf(f254,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f254_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f254]) ).
fof(f254_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f254_nnf]) ).
cnf(c254,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f254_sk]) ).
cnf(f331,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f331_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f331]) ).
fof(f331_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f331_nnf]) ).
cnf(c331,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f331_sk]) ).
cnf(f332,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f332_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f332]) ).
fof(f332_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f332_nnf]) ).
cnf(c332,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f332_sk]) ).
cnf(f333,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f333_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f333]) ).
fof(f333_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f333_nnf]) ).
cnf(c333,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f333_sk]) ).
cnf(f334,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f334_nnf,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f334]) ).
fof(f334_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f334_nnf]) ).
cnf(c334,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f334_sk]) ).
cnf(f347,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f347_nnf,plain,
! [V_x,V_B,T_a,V_A] :
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
inference(nnf_transformation,[status(thm)],[f347]) ).
fof(f347_sk,plain,
! [V_x,V_B,T_a,V_A] :
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
inference(skolemisation,[status(esa)],[f347_nnf]) ).
cnf(c347,plain,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X2,tc_bool)),X3),X1) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| ~ hBOOL(c_in(X0,X3,X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f347_sk]) ).
cnf(f350,axiom,
( ~ c_lessequals(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff2_0) ).
fof(f350_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f350]) ).
fof(f350_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f350_nnf]) ).
cnf(c350,plain,
( ~ c_lessequals(X1,X2,X0)
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f350_sk]) ).
cnf(f352,axiom,
( ~ c_lessequals(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff_0) ).
fof(f352_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f352]) ).
fof(f352_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f352_nnf]) ).
cnf(c352,plain,
( ~ c_lessequals(X1,X2,X0)
| c_SetInterval_Oord__class_OatLeastAtMost(X1,X2,X0) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f352_sk]) ).
cnf(f374,axiom,
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f374_nnf,plain,
! [V_f,V_a,V_A,T_a,T_b] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b)) ),
inference(nnf_transformation,[status(thm)],[f374]) ).
fof(f374_sk,plain,
! [V_f,V_a,V_A,T_a,T_b] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b)) ),
inference(skolemisation,[status(esa)],[f374_nnf]) ).
cnf(c374,plain,
( ~ c_Fun_Oinj__on(X0,c_Set_Oinsert(X1,X2,X3),X3,X4)
| ~ hBOOL(c_in(hAPP(X0,X1),c_Set_Oimage(X0,c_HOL_Ominus__class_Ominus(X2,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3),tc_fun(X3,tc_bool)),X3,X4),X4)) ),
inference(cnf_transformation,[status(esa)],[f374_sk]) ).
cnf(f398,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__Collect__eq_0) ).
fof(f398_nnf,plain,
! [T_a,V_P,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
inference(nnf_transformation,[status(thm)],[f398]) ).
fof(f398_sk,plain,
! [T_a,V_P,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
inference(skolemisation,[status(esa)],[f398_nnf]) ).
cnf(c398,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f398_sk]) ).
cnf(f399,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__empty__eq_0) ).
fof(f399_nnf,plain,
! [V_P,T_a,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(nnf_transformation,[status(thm)],[f399]) ).
fof(f399_sk,plain,
! [V_P,T_a,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(skolemisation,[status(esa)],[f399_nnf]) ).
cnf(c399,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f399_sk]) ).
cnf(f400,axiom,
~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__fold1SetE_0) ).
fof(f400_nnf,plain,
! [V_f,T_a,V_x] : ~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_x)),
inference(nnf_transformation,[status(thm)],[f400]) ).
fof(f400_sk,plain,
! [V_f,T_a,V_x] : ~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_x)),
inference(skolemisation,[status(esa)],[f400_nnf]) ).
cnf(c400,plain,
~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),X2)),
inference(cnf_transformation,[status(esa)],[f400_sk]) ).
cnf(f401,axiom,
c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_UNIV__not__empty_0) ).
fof(f401_nnf,plain,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f401]) ).
fof(f401_sk,plain,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f401_nnf]) ).
cnf(c401,plain,
c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(esa)],[f401_sk]) ).
cnf(f405,axiom,
~ c_HOL_Oord__class_Oless(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__psubset__empty_0) ).
fof(f405_nnf,plain,
! [V_A,T_a] : ~ c_HOL_Oord__class_Oless(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f405]) ).
fof(f405_sk,plain,
! [V_A,T_a] : ~ c_HOL_Oord__class_Oless(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f405_nnf]) ).
cnf(c405,plain,
~ c_HOL_Oord__class_Oless(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f405_sk]) ).
cnf(f428,axiom,
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__fun__def_1) ).
fof(f428_nnf,plain,
! [T_b,V_g,V_f,T_a] :
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
inference(nnf_transformation,[status(thm)],[f428]) ).
fof(f428_sk,plain,
! [T_b,V_g,V_f,T_a] :
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
inference(skolemisation,[status(esa)],[f428_nnf]) ).
cnf(c428,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,tc_fun(X3,X0))
| ~ c_lessequals(X1,X2,tc_fun(X3,X0))
| ~ class_HOL_Oord(X0) ),
inference(cnf_transformation,[status(esa)],[f428_sk]) ).
cnf(f469,axiom,
c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__None__eq_1) ).
fof(f469_nnf,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(nnf_transformation,[status(thm)],[f469]) ).
fof(f469_sk,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f469_nnf]) ).
cnf(c469,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f469_sk]) ).
cnf(f470,axiom,
c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Osimps_I3_J_0) ).
fof(f470_nnf,plain,
! [V_a_H,T_a] : c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
inference(nnf_transformation,[status(thm)],[f470]) ).
fof(f470_sk,plain,
! [V_a_H,T_a] : c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f470_nnf]) ).
cnf(c470,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f470_sk]) ).
cnf(f471,axiom,
c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Some__eq_1) ).
fof(f471_nnf,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(nnf_transformation,[status(thm)],[f471]) ).
fof(f471_sk,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(skolemisation,[status(esa)],[f471_nnf]) ).
cnf(c471,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f471_sk]) ).
cnf(f472,axiom,
c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Osimps_I2_J_0) ).
fof(f472_nnf,plain,
! [T_a,V_a_H] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a),
inference(nnf_transformation,[status(thm)],[f472]) ).
fof(f472_sk,plain,
! [T_a,V_a_H] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a),
inference(skolemisation,[status(esa)],[f472_nnf]) ).
cnf(c472,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f472_sk]) ).
cnf(f516,axiom,
( ~ hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_domIff_0) ).
fof(f516_nnf,plain,
! [V_m,V_a,T_b,T_a] :
( ~ hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
inference(nnf_transformation,[status(thm)],[f516]) ).
fof(f516_sk,plain,
! [V_m,V_a,T_b,T_a] :
( ~ hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
inference(skolemisation,[status(esa)],[f516_nnf]) ).
cnf(c516,plain,
( ~ hBOOL(c_in(X1,c_Map_Odom(X0,X3,X2),X3))
| hAPP(X0,X1) != c_Option_Ooption_ONone(X2) ),
inference(cnf_transformation,[status(esa)],[f516_sk]) ).
cnf(f607,axiom,
~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f607_nnf,plain,
! [V_x,T_a] : ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f607]) ).
fof(f607_sk,plain,
! [V_x,T_a] : ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f607_nnf]) ).
cnf(c607,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f607_sk]) ).
cnf(f609,axiom,
~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f609_nnf,plain,
! [V_c,T_a] : ~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f609]) ).
fof(f609_sk,plain,
! [V_c,T_a] : ~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f609_nnf]) ).
cnf(c609,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f609_sk]) ).
cnf(f610,axiom,
~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f610_nnf,plain,
! [V_a,T_a] : ~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f610]) ).
fof(f610_sk,plain,
! [V_a,T_a] : ~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f610_nnf]) ).
cnf(c610,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f610_sk]) ).
cnf(f611,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f611_nnf,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
inference(nnf_transformation,[status(thm)],[f611]) ).
fof(f611_sk,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
inference(skolemisation,[status(esa)],[f611_nnf]) ).
cnf(c611,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f611_sk]) ).
cnf(f626,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f626_nnf,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
inference(nnf_transformation,[status(thm)],[f626]) ).
fof(f626_sk,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
inference(skolemisation,[status(esa)],[f626_nnf]) ).
cnf(c626,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f626_sk]) ).
cnf(f636,axiom,
c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f636_nnf,plain,
! [V_a,V_A,T_a] : c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f636]) ).
fof(f636_sk,plain,
! [V_a,V_A,T_a] : c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f636_nnf]) ).
cnf(c636,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f636_sk]) ).
cnf(f658,axiom,
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f658_nnf,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(nnf_transformation,[status(thm)],[f658]) ).
fof(f658_sk,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(skolemisation,[status(esa)],[f658_nnf]) ).
cnf(c658,plain,
( ~ hBOOL(c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f658_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c165,c166,c167,c168,c184,c187,c248,c250,c252,c254,c331,c332,c333,c334,c347,c350,c352,c374,c398,c399,c400,c401,c405,c428,c469,c470,c471,c472,c516,c607,c609,c610,c611,c626,c636,c658,c681,c686]) ).
cnf(g0_0,plain,
sF1 != false,
inference(rw,[status(thm)],[goal_0,t221]) ).
cnf(g0_1,plain,
sF1 != sF1,
inference(rw,[status(thm)],[g0_0,t17632]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV902-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.43 % Computer : n004.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Thu Sep 24 21:16:20 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 112.77/16.79 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 112.77/16.79 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------