%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV901-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n006.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:26 PM UTC 2026
% Result : Unsatisfiable 30.40s 6.61s
% Output : Proof 30.40s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t178,axiom,
sF1 = c_Finite__Set_Ofinite(v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
introduced(definition) ).
cnf(t177,axiom,
sF0 = tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),
introduced(definition) ).
cnf(t201,plain,
tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate) = sF0,
inference(orient,[status(thm)],[t177]) ).
cnf(t12533,plain,
sF1 = c_Finite__Set_Ofinite(v_Fa,sF0),
inference(step,[status(thm)],[t178,t201]) ).
cnf(f667,negated_conjecture,
c_Finite__Set_Ofinite(v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f667_nnf,plain,
c_Finite__Set_Ofinite(v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(nnf_transformation,[status(thm)],[f667]) ).
cnf(c667,plain,
c_Finite__Set_Ofinite(v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(cnf_transformation,[status(esa)],[f667_nnf]) ).
cnf(t7,plain,
c_Finite__Set_Ofinite(v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)) = true,
inference(equality_encoding,[status(esa)],[c667]) ).
cnf(t12529,plain,
c_Finite__Set_Ofinite(v_Fa,sF0) = true,
inference(step,[status(thm)],[t7,t201]) ).
cnf(t209,plain,
c_Finite__Set_Ofinite(v_Fa,sF0) = true,
inference(orient,[status(thm)],[t12529]) ).
cnf(t12534,plain,
sF1 = true,
inference(step,[status(thm)],[t12533,t209]) ).
cnf(t216,plain,
true = sF1,
inference(orient,[status(thm)],[t12534]) ).
cnf(t182,axiom,
sF5 = c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
introduced(definition) ).
cnf(t181,axiom,
sF4 = hAPP(c_Hoare__Mirabelle_OMGT,v_y),
introduced(definition) ).
cnf(t215,plain,
hAPP(c_Hoare__Mirabelle_OMGT,v_y) = sF4,
inference(orient,[status(thm)],[t181]) ).
cnf(t12564,plain,
sF5 = c_in(sF4,v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(step,[status(thm)],[t182,t215]) ).
cnf(t12565,plain,
sF5 = c_in(sF4,v_Fa,sF0),
inference(step,[status(thm)],[t12564,t201]) ).
cnf(f668,negated_conjecture,
~ c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f668_nnf,plain,
~ c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(nnf_transformation,[status(thm)],[f668]) ).
fof(f668_sk,plain,
~ c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(skolemisation,[status(esa)],[f668_nnf]) ).
cnf(c668,plain,
~ c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(cnf_transformation,[status(esa)],[f668_sk]) ).
cnf(t22,plain,
c_in(hAPP(c_Hoare__Mirabelle_OMGT,v_y),v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)) = false,
inference(equality_encoding,[status(esa)],[c668]) ).
cnf(t12558,plain,
c_in(sF4,v_Fa,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)) = false,
inference(step,[status(thm)],[t22,t215]) ).
cnf(t12559,plain,
c_in(sF4,v_Fa,sF0) = false,
inference(step,[status(thm)],[t12558,t201]) ).
cnf(t252,plain,
c_in(sF4,v_Fa,sF0) = false,
inference(orient,[status(thm)],[t12559]) ).
cnf(t12566,plain,
sF5 = false,
inference(step,[status(thm)],[t12565,t252]) ).
cnf(t258,plain,
false = sF5,
inference(orient,[status(thm)],[t12566]) ).
cnf(f672,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,v_y),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/sandbox2/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f672_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,v_y),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)],[f672]) ).
fof(f672_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,v_y),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)],[f672_nnf]) ).
cnf(c672,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,v_y),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)],[f672_sk]) ).
cnf(t152,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,v_y),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)],[c672]) ).
cnf(f589,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/sandbox2/benchmark/theBenchmark.p',cls_image__image_0) ).
fof(f589_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)],[f589]) ).
fof(f589_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)],[f589_nnf]) ).
cnf(c589,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)],[f589_sk]) ).
cnf(t96,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)],[c589]) ).
cnf(t2399,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)],[t96]) ).
cnf(t13616,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,v_y),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)],[t152,t2399]) ).
cnf(t185,axiom,
sF8 = c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),
introduced(definition) ).
cnf(t229,plain,
c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom) = sF8,
inference(orient,[status(thm)],[t185]) ).
cnf(t13617,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,sF8,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),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)],[t13616,t229]) ).
cnf(t13618,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,sF8,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,sF0),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),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)],[t13617,t201]) ).
cnf(t184,axiom,
sF7 = 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(t12575,plain,
sF7 = c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,sF0,tc_Com_Opname),
inference(step,[status(thm)],[t184,t201]) ).
cnf(t269,plain,
c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,sF0,tc_Com_Opname) = sF7,
inference(orient,[status(thm)],[t12575]) ).
cnf(t2400,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(sF7,X1,tc_Com_Opname,sF0),
inference(cp,[status(thm)],[t2399,t269]) ).
cnf(t2422,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(sF7,X1,tc_Com_Opname,sF0),
inference(orient,[status(thm)],[t2400]) ).
cnf(t13619,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF7,sF8,tc_Com_Opname,sF0),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),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)],[t13618,t2422]) ).
cnf(f592,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/sandbox2/benchmark/theBenchmark.p',cls_image__insert_0) ).
fof(f592_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)],[f592]) ).
fof(f592_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)],[f592_nnf]) ).
cnf(c592,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)],[f592_sk]) ).
cnf(t87,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)],[c592]) ).
cnf(t1622,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)],[t87]) ).
cnf(f641,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/sandbox2/benchmark/theBenchmark.p',cls_image__empty_0) ).
fof(f641_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)],[f641]) ).
fof(f641_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)],[f641_nnf]) ).
cnf(c641,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)],[f641_sk]) ).
cnf(t40,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)],[c641]) ).
cnf(t273,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)],[t40]) ).
cnf(t188,axiom,
sF11 = tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool),
introduced(definition) ).
cnf(t12545,plain,
sF11 = tc_fun(sF0,tc_bool),
inference(step,[status(thm)],[t188,t201]) ).
cnf(t230,plain,
tc_fun(sF0,tc_bool) = sF11,
inference(orient,[status(thm)],[t12545]) ).
cnf(t274,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = c_Set_Oimage(X2,c_Orderings_Obot__class_Obot(sF11),sF0,X1),
inference(cp,[status(thm)],[t273,t230]) ).
cnf(t189,axiom,
sF12 = c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),
introduced(definition) ).
cnf(t12546,plain,
sF12 = c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)),
inference(step,[status(thm)],[t189,t201]) ).
cnf(t12547,plain,
sF12 = c_Orderings_Obot__class_Obot(sF11),
inference(step,[status(thm)],[t12546,t230]) ).
cnf(t232,plain,
c_Orderings_Obot__class_Obot(sF11) = sF12,
inference(orient,[status(thm)],[t12547]) ).
cnf(t12579,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = c_Set_Oimage(X2,sF12,sF0,X1),
inference(step,[status(thm)],[t274,t232]) ).
cnf(t275,plain,
c_Set_Oimage(X1,sF12,sF0,X2) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(orient,[status(thm)],[t12579]) ).
cnf(t1629,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF12,sF0),sF0,X3) = c_Set_Oinsert(hAPP(X1,X2),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3),
inference(cp,[status(thm)],[t1622,t275]) ).
cnf(t1680,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,sF12,sF0),sF0,X3),
inference(orient,[status(thm)],[t1629]) ).
cnf(t13620,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF7,sF8,tc_Com_Opname,sF0),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oinsert(v_y,sF12,sF0),sF0,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t13619,t1680]) ).
cnf(t13621,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF7,sF8,tc_Com_Opname,sF0),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oinsert(v_y,sF12,sF0),sF0,sF0),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t13620,t201]) ).
cnf(t1683,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF12,sF0),sF0,sF0) = c_Set_Oinsert(hAPP(X1,X2),c_Orderings_Obot__class_Obot(sF11),sF0),
inference(cp,[status(thm)],[t1680,t230]) ).
cnf(t12918,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF12,sF0),sF0,sF0) = c_Set_Oinsert(hAPP(X1,X2),sF12,sF0),
inference(step,[status(thm)],[t1683,t232]) ).
cnf(t1708,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF12,sF0),sF0,sF0) = c_Set_Oinsert(hAPP(X1,X2),sF12,sF0),
inference(orient,[status(thm)],[t12918]) ).
cnf(t13622,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF7,sF8,tc_Com_Opname,sF0),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),sF12,sF0),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t13621,t1708]) ).
cnf(t13623,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF7,sF8,tc_Com_Opname,sF0),c_Set_Oinsert(sF4,sF12,sF0),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t13622,t215]) ).
cnf(t190,axiom,
sF13 = c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),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(t12647,plain,
sF13 = c_Set_Oinsert(sF4,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(step,[status(thm)],[t190,t215]) ).
cnf(t12648,plain,
sF13 = c_Set_Oinsert(sF4,c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(step,[status(thm)],[t12647,t201]) ).
cnf(t12649,plain,
sF13 = c_Set_Oinsert(sF4,c_Orderings_Obot__class_Obot(sF11),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(step,[status(thm)],[t12648,t230]) ).
cnf(t12650,plain,
sF13 = c_Set_Oinsert(sF4,sF12,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(step,[status(thm)],[t12649,t232]) ).
cnf(t12651,plain,
sF13 = c_Set_Oinsert(sF4,sF12,sF0),
inference(step,[status(thm)],[t12650,t201]) ).
cnf(t376,plain,
c_Set_Oinsert(sF4,sF12,sF0) = sF13,
inference(orient,[status(thm)],[t12651]) ).
cnf(t13624,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF7,sF8,tc_Com_Opname,sF0),sF13,tc_Com_Ostate) = false,
inference(step,[status(thm)],[t13623,t376]) ).
cnf(t13625,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF7,sF8,tc_Com_Opname,sF0),sF13,tc_Com_Ostate) = sF5,
inference(step,[status(thm)],[t13624,t258]) ).
cnf(t10511,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(sF7,sF8,tc_Com_Opname,sF0),sF13,tc_Com_Ostate) = sF5,
inference(orient,[status(thm)],[t13625]) ).
cnf(f593,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_cut_0) ).
fof(f593_nnf,plain,
! [V_G,V_ts,T_a,V_G_H] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
inference(nnf_transformation,[status(thm)],[f593]) ).
fof(f593_sk,plain,
! [V_G,V_ts,T_a,V_G_H] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
inference(skolemisation,[status(esa)],[f593_nnf]) ).
cnf(c593,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X3,X1,X2)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X3,X2)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f593_sk]) ).
cnf(t99,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c593]) ).
cnf(t13013,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF1,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),true),true) = true,
inference(step,[status(thm)],[t99,t216]) ).
cnf(t13014,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF1,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),true),true) = true,
inference(step,[status(thm)],[t13013,t216]) ).
cnf(t13015,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF1,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),sF1),true) = true,
inference(step,[status(thm)],[t13014,t216]) ).
cnf(t13016,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF1,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),sF1),sF1) = true,
inference(step,[status(thm)],[t13015,t216]) ).
cnf(t13017,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF1,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),sF1),sF1) = sF1,
inference(step,[status(thm)],[t13016,t216]) ).
cnf(t3205,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF1,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),sF1,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),sF1),sF1) = sF1,
inference(orient,[status(thm)],[t13017]) ).
cnf(f559,axiom,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ~ c_Com_OWT(V_c)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,V_c),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/sandbox2/benchmark/theBenchmark.p',cls_MGF_0) ).
fof(f559_nnf,plain,
! [V_c] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ~ c_Com_OWT(V_c)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,V_c),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)],[f559]) ).
fof(f559_sk,plain,
! [V_c] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ~ c_Com_OWT(V_c)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,V_c),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)],[f559_nnf]) ).
cnf(c559,plain,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ~ c_Com_OWT(X0)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X0),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)],[f559_sk]) ).
cnf(t161,plain,
ifeq(c_Com_OWT(X1),true,ifeq(c_Com_OWT__bodies,true,ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c559]) ).
cnf(t13726,plain,
ifeq(c_Com_OWT(X1),sF1,ifeq(c_Com_OWT__bodies,true,ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true),true),true) = true,
inference(step,[status(thm)],[t161,t216]) ).
cnf(f666,negated_conjecture,
c_Com_OWT__bodies,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f666_nnf,plain,
c_Com_OWT__bodies,
inference(nnf_transformation,[status(thm)],[f666]) ).
cnf(c666,plain,
c_Com_OWT__bodies,
inference(cnf_transformation,[status(esa)],[f666_nnf]) ).
cnf(t0,plain,
true = c_Com_OWT__bodies,
inference(equality_encoding,[status(esa)],[c666]) ).
cnf(t199,plain,
c_Com_OWT__bodies = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t12535,plain,
c_Com_OWT__bodies = sF1,
inference(step,[status(thm)],[t199,t216]) ).
cnf(t217,plain,
c_Com_OWT__bodies = sF1,
inference(orient,[status(thm)],[t12535]) ).
cnf(t13727,plain,
ifeq(c_Com_OWT(X1),sF1,ifeq(sF1,true,ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true),true),true) = true,
inference(step,[status(thm)],[t13726,t217]) ).
cnf(t13728,plain,
ifeq(c_Com_OWT(X1),sF1,ifeq(sF1,sF1,ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true),true),true) = true,
inference(step,[status(thm)],[t13727,t216]) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t231,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t13729,plain,
ifeq(c_Com_OWT(X1),sF1,ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true),true) = true,
inference(step,[status(thm)],[t13728,t231]) ).
cnf(f665,negated_conjecture,
c_Hoare__Mirabelle_Ostate__not__singleton,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f665_nnf,plain,
c_Hoare__Mirabelle_Ostate__not__singleton,
inference(nnf_transformation,[status(thm)],[f665]) ).
cnf(c665,plain,
c_Hoare__Mirabelle_Ostate__not__singleton,
inference(cnf_transformation,[status(esa)],[f665_nnf]) ).
cnf(t1,plain,
true = c_Hoare__Mirabelle_Ostate__not__singleton,
inference(equality_encoding,[status(esa)],[c665]) ).
cnf(t200,plain,
c_Hoare__Mirabelle_Ostate__not__singleton = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t12537,plain,
c_Hoare__Mirabelle_Ostate__not__singleton = sF1,
inference(step,[status(thm)],[t200,t216]) ).
cnf(t219,plain,
c_Hoare__Mirabelle_Ostate__not__singleton = sF1,
inference(orient,[status(thm)],[t12537]) ).
cnf(t13730,plain,
ifeq(c_Com_OWT(X1),sF1,ifeq(sF1,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true),true) = true,
inference(step,[status(thm)],[t13729,t219]) ).
cnf(t13731,plain,
ifeq(c_Com_OWT(X1),sF1,ifeq(sF1,sF1,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true),true) = true,
inference(step,[status(thm)],[t13730,t216]) ).
cnf(t13732,plain,
ifeq(c_Com_OWT(X1),sF1,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true) = true,
inference(step,[status(thm)],[t13731,t231]) ).
cnf(t13733,plain,
ifeq(c_Com_OWT(X1),sF1,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true) = true,
inference(step,[status(thm)],[t13732,t201]) ).
cnf(t13734,plain,
ifeq(c_Com_OWT(X1),sF1,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(sF11),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true) = true,
inference(step,[status(thm)],[t13733,t230]) ).
cnf(t13735,plain,
ifeq(c_Com_OWT(X1),sF1,c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),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),true) = true,
inference(step,[status(thm)],[t13734,t232]) ).
cnf(t13736,plain,
ifeq(c_Com_OWT(X1),sF1,c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oinsert(X1,sF12,sF0),sF0,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true) = true,
inference(step,[status(thm)],[t13735,t1680]) ).
cnf(t13737,plain,
ifeq(c_Com_OWT(X1),sF1,c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oinsert(X1,sF12,sF0),sF0,sF0),tc_Com_Ostate),true) = true,
inference(step,[status(thm)],[t13736,t201]) ).
cnf(t13738,plain,
ifeq(c_Com_OWT(X1),sF1,c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),sF12,sF0),tc_Com_Ostate),true) = true,
inference(step,[status(thm)],[t13737,t1708]) ).
cnf(t13739,plain,
ifeq(c_Com_OWT(X1),sF1,c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),sF12,sF0),tc_Com_Ostate),sF1) = true,
inference(step,[status(thm)],[t13738,t216]) ).
cnf(t13740,plain,
ifeq(c_Com_OWT(X1),sF1,c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),sF12,sF0),tc_Com_Ostate),sF1) = sF1,
inference(step,[status(thm)],[t13739,t216]) ).
cnf(t12338,plain,
ifeq(c_Com_OWT(X1),sF1,c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X1),sF12,sF0),tc_Com_Ostate),sF1) = sF1,
inference(orient,[status(thm)],[t13740]) ).
cnf(t12339,plain,
sF1 = ifeq(c_Com_OWT(v_y),sF1,c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(sF4,sF12,sF0),tc_Com_Ostate),sF1),
inference(cp,[status(thm)],[t12338,t215]) ).
cnf(f555,axiom,
( c_Com_OWT(V_b)
| ~ c_Com_OWT__bodies
| hAPP(c_Com_Obody,V_pn) != c_Option_Ooption_OSome(V_b,tc_Com_Ocom) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_WT__bodiesD_0) ).
fof(f555_nnf,plain,
! [V_pn,V_b] :
( c_Com_OWT(V_b)
| ~ c_Com_OWT__bodies
| hAPP(c_Com_Obody,V_pn) != c_Option_Ooption_OSome(V_b,tc_Com_Ocom) ),
inference(nnf_transformation,[status(thm)],[f555]) ).
fof(f555_sk,plain,
! [V_pn,V_b] :
( c_Com_OWT(V_b)
| ~ c_Com_OWT__bodies
| hAPP(c_Com_Obody,V_pn) != c_Option_Ooption_OSome(V_b,tc_Com_Ocom) ),
inference(skolemisation,[status(esa)],[f555_nnf]) ).
cnf(c555,plain,
( c_Com_OWT(X1)
| ~ c_Com_OWT__bodies
| hAPP(c_Com_Obody,X0) != c_Option_Ooption_OSome(X1,tc_Com_Ocom) ),
inference(cnf_transformation,[status(esa)],[f555_sk]) ).
cnf(t73,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),ifeq(c_Com_OWT__bodies,true,c_Com_OWT(X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c555]) ).
cnf(t12811,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),ifeq(sF1,true,c_Com_OWT(X2),true),true) = true,
inference(step,[status(thm)],[t73,t217]) ).
cnf(t12812,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),ifeq(sF1,sF1,c_Com_OWT(X2),true),true) = true,
inference(step,[status(thm)],[t12811,t216]) ).
cnf(t12813,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),c_Com_OWT(X2),true) = true,
inference(step,[status(thm)],[t12812,t231]) ).
cnf(t12814,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),c_Com_OWT(X2),sF1) = true,
inference(step,[status(thm)],[t12813,t216]) ).
cnf(t12815,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),c_Com_OWT(X2),sF1) = sF1,
inference(step,[status(thm)],[t12814,t216]) ).
cnf(t917,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),c_Com_OWT(X2),sF1) = sF1,
inference(orient,[status(thm)],[t12815]) ).
cnf(f670,negated_conjecture,
hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(v_y,tc_Com_Ocom),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f670_nnf,plain,
hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(v_y,tc_Com_Ocom),
inference(nnf_transformation,[status(thm)],[f670]) ).
cnf(c670,plain,
hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(v_y,tc_Com_Ocom),
inference(cnf_transformation,[status(esa)],[f670_nnf]) ).
cnf(t8,plain,
hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(v_y,tc_Com_Ocom),
inference(equality_encoding,[status(esa)],[c670]) ).
cnf(t210,plain,
c_Option_Ooption_OSome(v_y,tc_Com_Ocom) = hAPP(c_Com_Obody,v_pn),
inference(orient,[status(thm)],[t8]) ).
cnf(t179,axiom,
sF2 = hAPP(c_Com_Obody,v_pn),
introduced(definition) ).
cnf(t211,plain,
hAPP(c_Com_Obody,v_pn) = sF2,
inference(orient,[status(thm)],[t179]) ).
cnf(t12530,plain,
c_Option_Ooption_OSome(v_y,tc_Com_Ocom) = sF2,
inference(step,[status(thm)],[t210,t211]) ).
cnf(t212,plain,
c_Option_Ooption_OSome(v_y,tc_Com_Ocom) = sF2,
inference(orient,[status(thm)],[t12530]) ).
cnf(t918,plain,
sF1 = ifeq(hAPP(c_Com_Obody,X1),sF2,c_Com_OWT(v_y),sF1),
inference(cp,[status(thm)],[t917,t212]) ).
cnf(t920,plain,
ifeq(hAPP(c_Com_Obody,X1),sF2,c_Com_OWT(v_y),sF1) = sF1,
inference(orient,[status(thm)],[t918]) ).
cnf(t921,plain,
sF1 = ifeq(sF2,sF2,c_Com_OWT(v_y),sF1),
inference(cp,[status(thm)],[t920,t211]) ).
cnf(t12816,plain,
sF1 = c_Com_OWT(v_y),
inference(step,[status(thm)],[t921,t231]) ).
cnf(t922,plain,
c_Com_OWT(v_y) = sF1,
inference(orient,[status(thm)],[t12816]) ).
cnf(t13741,plain,
sF1 = ifeq(sF1,sF1,c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(sF4,sF12,sF0),tc_Com_Ostate),sF1),
inference(step,[status(thm)],[t12339,t922]) ).
cnf(t13742,plain,
sF1 = c_Hoare__Mirabelle_Ohoare__derivs(sF12,c_Set_Oinsert(sF4,sF12,sF0),tc_Com_Ostate),
inference(step,[status(thm)],[t13741,t231]) ).
cnf(t13743,plain,
sF1 = c_Hoare__Mirabelle_Ohoare__derivs(sF12,sF13,tc_Com_Ostate),
inference(step,[status(thm)],[t13742,t376]) ).
cnf(t12342,plain,
c_Hoare__Mirabelle_Ohoare__derivs(sF12,sF13,tc_Com_Ostate) = sF1,
inference(orient,[status(thm)],[t13743]) ).
cnf(t12345,plain,
sF1 = ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,sF12,tc_Com_Ostate),sF1,ifeq(sF1,sF1,c_Hoare__Mirabelle_Ohoare__derivs(X1,sF13,tc_Com_Ostate),sF1),sF1),
inference(cp,[status(thm)],[t3205,t12342]) ).
cnf(f613,axiom,
c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty_0) ).
fof(f613_nnf,plain,
! [V_G,T_a] : c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f613]) ).
fof(f613_sk,plain,
! [V_G,T_a] : c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f613_nnf]) ).
cnf(c613,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f613_sk]) ).
cnf(t24,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)),X2) = true,
inference(equality_encoding,[status(esa)],[c613]) ).
cnf(t12561,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)),X2) = sF1,
inference(step,[status(thm)],[t24,t216]) ).
cnf(t254,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)),X2) = sF1,
inference(orient,[status(thm)],[t12561]) ).
cnf(t255,plain,
sF1 = c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)),tc_Com_Ostate),
inference(cp,[status(thm)],[t254,t201]) ).
cnf(t12562,plain,
sF1 = c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Orderings_Obot__class_Obot(sF11),tc_Com_Ostate),
inference(step,[status(thm)],[t255,t230]) ).
cnf(t12563,plain,
sF1 = c_Hoare__Mirabelle_Ohoare__derivs(X1,sF12,tc_Com_Ostate),
inference(step,[status(thm)],[t12562,t232]) ).
cnf(t256,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X1,sF12,tc_Com_Ostate) = sF1,
inference(orient,[status(thm)],[t12563]) ).
cnf(t13744,plain,
sF1 = ifeq(sF1,sF1,ifeq(sF1,sF1,c_Hoare__Mirabelle_Ohoare__derivs(X1,sF13,tc_Com_Ostate),sF1),sF1),
inference(step,[status(thm)],[t12345,t256]) ).
cnf(t13745,plain,
sF1 = ifeq(sF1,sF1,c_Hoare__Mirabelle_Ohoare__derivs(X1,sF13,tc_Com_Ostate),sF1),
inference(step,[status(thm)],[t13744,t231]) ).
cnf(t13746,plain,
sF1 = c_Hoare__Mirabelle_Ohoare__derivs(X1,sF13,tc_Com_Ostate),
inference(step,[status(thm)],[t13745,t231]) ).
cnf(t12348,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X1,sF13,tc_Com_Ostate) = sF1,
inference(orient,[status(thm)],[t13746]) ).
cnf(t13749,plain,
sF1 = sF5,
inference(step,[status(thm)],[t10511,t12348]) ).
cnf(t12351,plain,
sF1 = sF5,
inference(rw,[status(thm)],[t13749]) ).
cnf(t12357,plain,
sF5 = sF1,
inference(orient,[status(thm)],[t12351]) ).
cnf(t13758,plain,
false = sF1,
inference(step,[status(thm)],[t258,t12357]) ).
cnf(t12364,plain,
false = sF1,
inference(orient,[status(thm)],[t13758]) ).
cnf(f160,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_psubset__eq_1) ).
fof(f160_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)],[f160]) ).
fof(f160_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)],[f160_nnf]) ).
cnf(c160,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f160_sk]) ).
cnf(f161,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f161_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)],[f161]) ).
fof(f161_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)],[f161_nnf]) ).
cnf(c161,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f161_sk]) ).
cnf(f162,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f162_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)],[f162]) ).
fof(f162_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)],[f162_nnf]) ).
cnf(c162,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f162_sk]) ).
cnf(f163,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f163_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)],[f163]) ).
fof(f163_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)],[f163_nnf]) ).
cnf(c163,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f163_sk]) ).
cnf(f171,axiom,
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f171_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f171]) ).
fof(f171_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f171_nnf]) ).
cnf(c171,plain,
( ~ c_in(X0,c_HOL_Ominus__class_Ominus(X3,X1,tc_fun(X2,tc_bool)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f171_sk]) ).
cnf(f174,axiom,
( ~ c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f174_nnf,plain,
! [V_c,V_A,T_a] :
( ~ c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(nnf_transformation,[status(thm)],[f174]) ).
fof(f174_sk,plain,
! [V_c,V_A,T_a] :
( ~ c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(skolemisation,[status(esa)],[f174_nnf]) ).
cnf(c174,plain,
( ~ c_in(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_fun(X2,tc_bool)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f174_sk]) ).
cnf(f235,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f235_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)],[f235]) ).
fof(f235_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)],[f235_nnf]) ).
cnf(c235,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f235_sk]) ).
cnf(f237,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f237_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)],[f237]) ).
fof(f237_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)],[f237_nnf]) ).
cnf(c237,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f237_sk]) ).
cnf(f239,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f239_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)],[f239]) ).
fof(f239_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)],[f239_nnf]) ).
cnf(c239,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f239_sk]) ).
cnf(f241,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/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f241_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)],[f241]) ).
fof(f241_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)],[f241_nnf]) ).
cnf(c241,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f241_sk]) ).
cnf(f321,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/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f321_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)],[f321]) ).
fof(f321_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)],[f321_nnf]) ).
cnf(c321,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)],[f321_sk]) ).
cnf(f322,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/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f322_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)],[f322]) ).
fof(f322_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)],[f322_nnf]) ).
cnf(c322,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)],[f322_sk]) ).
cnf(f323,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/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f323_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)],[f323]) ).
fof(f323_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)],[f323_nnf]) ).
cnf(c323,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)],[f323_sk]) ).
cnf(f324,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/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f324_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)],[f324]) ).
fof(f324_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)],[f324_nnf]) ).
cnf(c324,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)],[f324_sk]) ).
cnf(f336,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))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f336_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))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f336]) ).
fof(f336_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))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f336_nnf]) ).
cnf(c336,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))
| ~ c_in(X0,X3,X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f336_sk]) ).
cnf(f339,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/sandbox2/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff2_0) ).
fof(f339_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)],[f339]) ).
fof(f339_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)],[f339_nnf]) ).
cnf(c339,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)],[f339_sk]) ).
cnf(f341,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/sandbox2/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff_0) ).
fof(f341_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)],[f341]) ).
fof(f341_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)],[f341_nnf]) ).
cnf(c341,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)],[f341_sk]) ).
cnf(f363,axiom,
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ 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/sandbox2/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f363_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)
| ~ 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)],[f363]) ).
fof(f363_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)
| ~ 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)],[f363_nnf]) ).
cnf(c363,plain,
( ~ c_Fun_Oinj__on(X0,c_Set_Oinsert(X1,X2,X3),X3,X4)
| ~ 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)],[f363_sk]) ).
cnf(f385,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/sandbox2/benchmark/theBenchmark.p',cls_empty__Collect__eq_0) ).
fof(f385_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)],[f385]) ).
fof(f385_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)],[f385_nnf]) ).
cnf(c385,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f385_sk]) ).
cnf(f386,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/sandbox2/benchmark/theBenchmark.p',cls_Collect__empty__eq_0) ).
fof(f386_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)],[f386]) ).
fof(f386_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)],[f386_nnf]) ).
cnf(c386,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f386_sk]) ).
cnf(f387,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/sandbox2/benchmark/theBenchmark.p',cls_empty__fold1SetE_0) ).
fof(f387_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)],[f387]) ).
fof(f387_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)],[f387_nnf]) ).
cnf(c387,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)],[f387_sk]) ).
cnf(f388,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/sandbox2/benchmark/theBenchmark.p',cls_UNIV__not__empty_0) ).
fof(f388_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)],[f388]) ).
fof(f388_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)],[f388_nnf]) ).
cnf(c388,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)],[f388_sk]) ).
cnf(f392,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/sandbox2/benchmark/theBenchmark.p',cls_not__psubset__empty_0) ).
fof(f392_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)],[f392]) ).
fof(f392_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)],[f392_nnf]) ).
cnf(c392,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)],[f392_sk]) ).
cnf(f415,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/sandbox2/benchmark/theBenchmark.p',cls_less__fun__def_1) ).
fof(f415_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)],[f415]) ).
fof(f415_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)],[f415_nnf]) ).
cnf(c415,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)],[f415_sk]) ).
cnf(f456,axiom,
c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__None__eq_1) ).
fof(f456_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)],[f456]) ).
fof(f456_sk,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f456_nnf]) ).
cnf(c456,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f456_sk]) ).
cnf(f457,axiom,
c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_option_Osimps_I3_J_0) ).
fof(f457_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)],[f457]) ).
fof(f457_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)],[f457_nnf]) ).
cnf(c457,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f457_sk]) ).
cnf(f458,axiom,
c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Some__eq_1) ).
fof(f458_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)],[f458]) ).
fof(f458_sk,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(skolemisation,[status(esa)],[f458_nnf]) ).
cnf(c458,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f458_sk]) ).
cnf(f459,axiom,
c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_option_Osimps_I2_J_0) ).
fof(f459_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)],[f459]) ).
fof(f459_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)],[f459_nnf]) ).
cnf(c459,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f459_sk]) ).
cnf(f505,axiom,
( ~ 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/sandbox2/benchmark/theBenchmark.p',cls_domIff_0) ).
fof(f505_nnf,plain,
! [V_m,V_a,T_b,T_a] :
( ~ 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)],[f505]) ).
fof(f505_sk,plain,
! [V_m,V_a,T_b,T_a] :
( ~ 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)],[f505_nnf]) ).
cnf(c505,plain,
( ~ c_in(X1,c_Map_Odom(X0,X3,X2),X3)
| hAPP(X0,X1) != c_Option_Ooption_ONone(X2) ),
inference(cnf_transformation,[status(esa)],[f505_sk]) ).
cnf(f594,axiom,
~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f594_nnf,plain,
! [V_x,T_a] : ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f594]) ).
fof(f594_sk,plain,
! [V_x,T_a] : ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f594_nnf]) ).
cnf(c594,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f594_sk]) ).
cnf(f596,axiom,
~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f596_nnf,plain,
! [V_c,T_a] : ~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f596]) ).
fof(f596_sk,plain,
! [V_c,T_a] : ~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f596_nnf]) ).
cnf(c596,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f596_sk]) ).
cnf(f597,axiom,
~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f597_nnf,plain,
! [V_a,T_a] : ~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f597]) ).
fof(f597_sk,plain,
! [V_a,T_a] : ~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f597_nnf]) ).
cnf(c597,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f597_sk]) ).
cnf(f598,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f598_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)],[f598]) ).
fof(f598_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)],[f598_nnf]) ).
cnf(c598,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f598_sk]) ).
cnf(f612,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f612_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)],[f612]) ).
fof(f612_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)],[f612_nnf]) ).
cnf(c612,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f612_sk]) ).
cnf(f623,axiom,
c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f623_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)],[f623]) ).
fof(f623_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)],[f623_nnf]) ).
cnf(c623,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f623_sk]) ).
cnf(f644,axiom,
( ~ 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/sandbox2/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f644_nnf,plain,
! [V_P,V_x,T_a] :
( ~ 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)],[f644]) ).
fof(f644_sk,plain,
! [V_P,V_x,T_a] :
( ~ 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)],[f644_nnf]) ).
cnf(c644,plain,
( ~ c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f644_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c160,c161,c162,c163,c171,c174,c235,c237,c239,c241,c321,c322,c323,c324,c336,c339,c341,c363,c385,c386,c387,c388,c392,c415,c456,c457,c458,c459,c505,c594,c596,c597,c598,c612,c623,c644,c668,c672]) ).
cnf(g0_0,plain,
sF1 != false,
inference(rw,[status(thm)],[goal_0,t216]) ).
cnf(g0_1,plain,
sF1 != sF1,
inference(rw,[status(thm)],[g0_0,t12364]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV901-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 21:16:10 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 30.40/6.61 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.40/6.61 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------