%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV840-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 : n012.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:10 PM UTC 2026
% Result : Unsatisfiable 65.76s 8.65s
% Output : Proof 65.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 70
% Syntax : Number of formulae : 295 ( 267 unt; 0 def)
% Number of atoms : 335 ( 251 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 346 ( 306 ~; 40 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 35 ( 35 usr; 13 con; 0-4 aty)
% Number of variables : 932 ( 391 sgn 450 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f354,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_lessequals(V_G_H,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_thin_0) ).
fof(f354_nnf,plain,
! [V_G,V_ts,T_a,V_G_H] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_lessequals(V_G_H,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)],[f354]) ).
fof(f354_sk,plain,
! [V_G,V_ts,T_a,V_G_H] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_lessequals(V_G_H,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)],[f354_nnf]) ).
cnf(c354,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X3,X1,X2)
| ~ c_lessequals(X3,X0,tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f354_sk]) ).
cnf(t180,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c354]) ).
cnf(t486,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),true),true) = true,
inference(orient,[status(thm)],[t180]) ).
cnf(f224,axiom,
c_lessequals(V_B,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subset__insertI_0) ).
fof(f224_nnf,plain,
! [V_B,V_a,T_a] : c_lessequals(V_B,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f224]) ).
fof(f224_sk,plain,
! [V_B,V_a,T_a] : c_lessequals(V_B,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f224_nnf]) ).
cnf(c224,plain,
c_lessequals(X0,c_Set_Oinsert(X1,X0,X2),tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f224_sk]) ).
cnf(t67,plain,
c_lessequals(X1,c_Set_Oinsert(X2,X1,X3),tc_fun(X3,tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c224]) ).
cnf(t639,plain,
c_lessequals(X1,c_Set_Oinsert(X2,X1,X3),tc_fun(X3,tc_bool)) = true,
inference(orient,[status(thm)],[t67]) ).
cnf(t658,plain,
true = ifeq(true,true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(X4,X1,tc_Hoare__Mirabelle_Otriple(X3)),X2,X3),true),true),
inference(cp,[status(thm)],[t486,t639]) ).
cnf(t16,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t262,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t16]) ).
cnf(t5507,plain,
true = ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(X4,X1,tc_Hoare__Mirabelle_Otriple(X3)),X2,X3),true),
inference(step,[status(thm)],[t658,t262]) ).
cnf(t5274,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(X4,X1,tc_Hoare__Mirabelle_Otriple(X3)),X2,X3),true) = true,
inference(orient,[status(thm)],[t5507]) ).
cnf(f440,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q),v_G,tc_Hoare__Mirabelle_Otriple(t_a)),c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f440_nnf,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q),v_G,tc_Hoare__Mirabelle_Otriple(t_a)),c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(nnf_transformation,[status(thm)],[f440]) ).
fof(f440_sk,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q),v_G,tc_Hoare__Mirabelle_Otriple(t_a)),c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(skolemisation,[status(esa)],[f440_nnf]) ).
cnf(c440,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q),v_G,tc_Hoare__Mirabelle_Otriple(t_a)),c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(cnf_transformation,[status(esa)],[f440_sk]) ).
cnf(t231,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q),v_G,tc_Hoare__Mirabelle_Otriple(t_a)),c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a) = false,
inference(equality_encoding,[status(esa)],[c440]) ).
cnf(t3092,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q),v_G,tc_Hoare__Mirabelle_Otriple(t_a)),c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a) = false,
inference(orient,[status(thm)],[t231]) ).
cnf(t5282,plain,
true = ifeq(c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),true,false,true),
inference(cp,[status(thm)],[t5274,t3092]) ).
cnf(f439,negated_conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f439_nnf,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(nnf_transformation,[status(thm)],[f439]) ).
cnf(c439,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(cnf_transformation,[status(esa)],[f439_nnf]) ).
cnf(t193,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a) = true,
inference(equality_encoding,[status(esa)],[c439]) ).
cnf(t1383,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a) = true,
inference(orient,[status(thm)],[t193]) ).
cnf(t5508,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t5282,t1383]) ).
cnf(t5509,plain,
true = false,
inference(step,[status(thm)],[t5508,t262]) ).
cnf(t5286,plain,
false = true,
inference(orient,[status(thm)],[t5509]) ).
cnf(f19,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I14_J_0) ).
fof(f19_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(f29,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I43_J_0) ).
fof(f29_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_loc,V_fun,V_com] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_loc,V_fun,V_com] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OLocal(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(f33,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OWhile(V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I61_J_0) ).
fof(f33_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_fun,V_com] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_fun,V_com] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(f50,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(f50_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)],[f50]) ).
fof(f50_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)],[f50_nnf]) ).
cnf(c50,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(f51,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(f51_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)],[f51]) ).
fof(f51_sk,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(f65,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I51_J_0) ).
fof(f65_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_com1,V_com2] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_com1,V_com2] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c65,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(f76,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I56_J_0) ).
fof(f76_nnf,plain,
! [V_fun,V_com1,V_com2,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f76]) ).
fof(f76_sk,plain,
! [V_fun,V_com1,V_com2,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f76_nnf]) ).
cnf(c76,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OCall(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f76_sk]) ).
cnf(f80,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I36_J_0) ).
fof(f80_nnf,plain,
! [V_loc,V_fun,V_com,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f80]) ).
fof(f80_sk,plain,
! [V_loc,V_fun,V_com,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f80_nnf]) ).
cnf(c80,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OCond(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f80_sk]) ).
cnf(f85,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I17_J_0) ).
fof(f85_nnf,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f85]) ).
fof(f85_sk,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f85_nnf]) ).
cnf(c85,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
cnf(f86,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I39_J_0) ).
fof(f86_nnf,plain,
! [V_fun_H,V_com_H,V_loc,V_fun,V_com] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f86]) ).
fof(f86_sk,plain,
! [V_fun_H,V_com_H,V_loc,V_fun,V_com] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f86_nnf]) ).
cnf(c86,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f86_sk]) ).
cnf(f88,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f88_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f88]) ).
fof(f88_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f88_nnf]) ).
cnf(c88,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f88_sk]) ).
cnf(f89,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f89_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f89]) ).
fof(f89_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f89_nnf]) ).
cnf(c89,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f89_sk]) ).
cnf(f93,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I46_J_0) ).
fof(f93_nnf,plain,
! [V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f93]) ).
fof(f93_sk,plain,
! [V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f93_nnf]) ).
cnf(c93,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
cnf(f95,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I44_J_0) ).
fof(f95_nnf,plain,
! [V_com1,V_com2,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f95]) ).
fof(f95_sk,plain,
! [V_com1,V_com2,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f95_nnf]) ).
cnf(c95,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(f96,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I35_J_0) ).
fof(f96_nnf,plain,
! [V_com1_H,V_com2_H,V_loc,V_fun,V_com] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f96]) ).
fof(f96_sk,plain,
! [V_com1_H,V_com2_H,V_loc,V_fun,V_com] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f96_nnf]) ).
cnf(c96,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f96_sk]) ).
cnf(f99,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I52_J_0) ).
fof(f99_nnf,plain,
! [V_fun,V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f99]) ).
fof(f99_sk,plain,
! [V_fun,V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f99_nnf]) ).
cnf(c99,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f99_sk]) ).
cnf(f101,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I37_J_0) ).
fof(f101_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_loc,V_fun,V_com] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f101]) ).
fof(f101_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_loc,V_fun,V_com] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f101_nnf]) ).
cnf(c101,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OLocal(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f101_sk]) ).
cnf(f102,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(f102_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)],[f102]) ).
fof(f102_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)],[f102_nnf]) ).
cnf(c102,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)],[f102_sk]) ).
cnf(f106,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I45_J_0) ).
fof(f106_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_com1,V_com2] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f106]) ).
fof(f106_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_com1,V_com2] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f106_nnf]) ).
cnf(c106,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f106_sk]) ).
cnf(f119,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(f119_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)],[f119]) ).
fof(f119_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)],[f119_nnf]) ).
cnf(c119,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f119_sk]) ).
cnf(f120,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(f120_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)],[f120]) ).
fof(f120_sk,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f120_nnf]) ).
cnf(c120,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
cnf(f121,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I57_J_0) ).
fof(f121_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f121]) ).
fof(f121_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(skolemisation,[status(esa)],[f121_nnf]) ).
cnf(c121,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OCond(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f121_sk]) ).
cnf(f134,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I38_J_0) ).
fof(f134_nnf,plain,
! [V_loc,V_fun,V_com,V_fun_H,V_com_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f134]) ).
fof(f134_sk,plain,
! [V_loc,V_fun,V_com,V_fun_H,V_com_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f134_nnf]) ).
cnf(c134,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f134_sk]) ).
cnf(f138,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I16_J_0) ).
fof(f138_nnf,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f138]) ).
fof(f138_sk,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f138_nnf]) ).
cnf(c138,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(X0,X1),
inference(cnf_transformation,[status(esa)],[f138_sk]) ).
cnf(f147,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I34_J_0) ).
fof(f147_nnf,plain,
! [V_loc,V_fun,V_com,V_com1_H,V_com2_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f147]) ).
fof(f147_sk,plain,
! [V_loc,V_fun,V_com,V_com1_H,V_com2_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f147_nnf]) ).
cnf(c147,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f147_sk]) ).
cnf(f163,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I15_J_0) ).
fof(f163_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f163]) ).
fof(f163_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f163_nnf]) ).
cnf(c163,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f163_sk]) ).
cnf(f166,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I53_J_0) ).
fof(f166_nnf,plain,
! [V_fun_H,V_com_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f166]) ).
fof(f166_sk,plain,
! [V_fun_H,V_com_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(skolemisation,[status(esa)],[f166_nnf]) ).
cnf(c166,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
cnf(f167,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I50_J_0) ).
fof(f167_nnf,plain,
! [V_com1,V_com2,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f167]) ).
fof(f167_sk,plain,
! [V_com1,V_com2,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f167_nnf]) ).
cnf(c167,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f167_sk]) ).
cnf(f190,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(f190_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)],[f190]) ).
fof(f190_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)],[f190_nnf]) ).
cnf(c190,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f190_sk]) ).
cnf(f191,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(f191_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)],[f191]) ).
fof(f191_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)],[f191_nnf]) ).
cnf(c191,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f191_sk]) ).
cnf(f193,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(f193_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)],[f193]) ).
fof(f193_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)],[f193_nnf]) ).
cnf(c193,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f193_sk]) ).
cnf(f194,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(f194_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)],[f194]) ).
fof(f194_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)],[f194_nnf]) ).
cnf(c194,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
cnf(f197,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(f197_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)],[f197]) ).
fof(f197_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)],[f197_nnf]) ).
cnf(c197,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f197_sk]) ).
cnf(f198,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(f198_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)],[f198]) ).
fof(f198_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)],[f198_nnf]) ).
cnf(c198,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)],[f198_sk]) ).
cnf(f207,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(f207_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)],[f207]) ).
fof(f207_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)],[f207_nnf]) ).
cnf(c207,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)],[f207_sk]) ).
cnf(f235,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I19_J_0) ).
fof(f235_nnf,plain,
! [V_pname_H] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f235]) ).
fof(f235_sk,plain,
! [V_pname_H] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f235_nnf]) ).
cnf(c235,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f235_sk]) ).
cnf(f236,axiom,
c_Com_Ocom_OWhile(V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I58_J_0) ).
fof(f236_nnf,plain,
! [V_fun,V_com,V_pname_H] : c_Com_Ocom_OWhile(V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f236]) ).
fof(f236_sk,plain,
! [V_fun,V_com,V_pname_H] : c_Com_Ocom_OWhile(V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f236_nnf]) ).
cnf(c236,plain,
c_Com_Ocom_OWhile(X0,X1) != hAPP(c_Com_Ocom_OBODY,X2),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(f237,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I55_J_0) ).
fof(f237_nnf,plain,
! [V_pname_H,V_fun,V_com1,V_com2] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f237]) ).
fof(f237_sk,plain,
! [V_pname_H,V_fun,V_com1,V_com2] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(skolemisation,[status(esa)],[f237_nnf]) ).
cnf(c237,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OCond(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f237_sk]) ).
cnf(f238,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I54_J_0) ).
fof(f238_nnf,plain,
! [V_fun,V_com1,V_com2,V_pname_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f238]) ).
fof(f238_sk,plain,
! [V_fun,V_com1,V_com2,V_pname_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f238_nnf]) ).
cnf(c238,plain,
c_Com_Ocom_OCond(X0,X1,X2) != hAPP(c_Com_Ocom_OBODY,X3),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
cnf(f239,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I10_J_0) ).
fof(f239_nnf,plain,
! [V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f239]) ).
fof(f239_sk,plain,
! [V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f239_nnf]) ).
cnf(c239,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f239_sk]) ).
cnf(f244,axiom,
c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I60_J_0) ).
fof(f244_nnf,plain,
! [V_fun,V_com,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f244]) ).
fof(f244_sk,plain,
! [V_fun,V_com,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f244_nnf]) ).
cnf(c244,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f244_sk]) ).
cnf(f254,axiom,
c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I11_J_0) ).
fof(f254_nnf,plain,
! [V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f254]) ).
fof(f254_sk,plain,
! [V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f254_nnf]) ).
cnf(c254,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f254_sk]) ).
cnf(f262,axiom,
c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
fof(f262_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f262]) ).
fof(f262_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f262_nnf]) ).
cnf(c262,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f262_sk]) ).
cnf(f263,axiom,
c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__neq__Zero_0) ).
fof(f263_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f263]) ).
fof(f263_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f263_nnf]) ).
cnf(c263,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f263_sk]) ).
cnf(f273,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(f273_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)],[f273]) ).
fof(f273_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)],[f273_nnf]) ).
cnf(c273,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)],[f273_sk]) ).
cnf(f278,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I13_J_0) ).
fof(f278_nnf,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f278]) ).
fof(f278_sk,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f278_nnf]) ).
cnf(c278,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f278_sk]) ).
cnf(f286,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I20_J_0) ).
fof(f286_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f286]) ).
fof(f286_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f286_nnf]) ).
cnf(c286,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
cnf(f288,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I47_J_0) ).
fof(f288_nnf,plain,
! [V_fun_H,V_com_H,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f288]) ).
fof(f288_sk,plain,
! [V_fun_H,V_com_H,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f288_nnf]) ).
cnf(c288,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f288_sk]) ).
cnf(f293,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f293_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f293]) ).
fof(f293_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f293_nnf]) ).
cnf(c293,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f293_sk]) ).
cnf(f294,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f294_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f294]) ).
fof(f294_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f294_nnf]) ).
cnf(c294,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f294_sk]) ).
cnf(f316,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I21_J_0) ).
fof(f316_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f316]) ).
fof(f316_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f316_nnf]) ).
cnf(c316,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f316_sk]) ).
cnf(f318,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(f318_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)],[f318]) ).
fof(f318_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)],[f318_nnf]) ).
cnf(c318,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)],[f318_sk]) ).
cnf(f332,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I42_J_0) ).
fof(f332_nnf,plain,
! [V_loc,V_fun,V_com,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f332]) ).
fof(f332_sk,plain,
! [V_loc,V_fun,V_com,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f332_nnf]) ).
cnf(c332,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OCall(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f332_sk]) ).
cnf(f337,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I12_J_0) ).
fof(f337_nnf,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f337]) ).
fof(f337_sk,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f337_nnf]) ).
cnf(c337,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f337_sk]) ).
cnf(f339,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I41_J_0) ).
fof(f339_nnf,plain,
! [V_pname_H,V_loc,V_fun,V_com] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f339]) ).
fof(f339_sk,plain,
! [V_pname_H,V_loc,V_fun,V_com] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f339_nnf]) ).
cnf(c339,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OLocal(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f339_sk]) ).
cnf(f340,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I59_J_0) ).
fof(f340_nnf,plain,
! [V_pname_H,V_fun,V_com] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f340]) ).
fof(f340_sk,plain,
! [V_pname_H,V_fun,V_com] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(skolemisation,[status(esa)],[f340_nnf]) ).
cnf(c340,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OWhile(X1,X2),
inference(cnf_transformation,[status(esa)],[f340_sk]) ).
cnf(f341,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != hAPP(c_Com_Ocom_OBODY,V_pname),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I63_J_0) ).
fof(f341_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_pname] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != hAPP(c_Com_Ocom_OBODY,V_pname),
inference(nnf_transformation,[status(thm)],[f341]) ).
fof(f341_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_pname] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != hAPP(c_Com_Ocom_OBODY,V_pname),
inference(skolemisation,[status(esa)],[f341_nnf]) ).
cnf(c341,plain,
c_Com_Ocom_OCall(X0,X1,X2) != hAPP(c_Com_Ocom_OBODY,X3),
inference(cnf_transformation,[status(esa)],[f341_sk]) ).
cnf(f342,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I49_J_0) ).
fof(f342_nnf,plain,
! [V_pname_H,V_com1,V_com2] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f342]) ).
fof(f342_sk,plain,
! [V_pname_H,V_com1,V_com2] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f342_nnf]) ).
cnf(c342,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OSemi(X1,X2),
inference(cnf_transformation,[status(esa)],[f342_sk]) ).
cnf(f343,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I48_J_0) ).
fof(f343_nnf,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f343]) ).
fof(f343_sk,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f343_nnf]) ).
cnf(c343,plain,
c_Com_Ocom_OSemi(X0,X1) != hAPP(c_Com_Ocom_OBODY,X2),
inference(cnf_transformation,[status(esa)],[f343_sk]) ).
cnf(f344,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I40_J_0) ).
fof(f344_nnf,plain,
! [V_loc,V_fun,V_com,V_pname_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f344]) ).
fof(f344_sk,plain,
! [V_loc,V_fun,V_com,V_pname_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f344_nnf]) ).
cnf(c344,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != hAPP(c_Com_Ocom_OBODY,X3),
inference(cnf_transformation,[status(esa)],[f344_sk]) ).
cnf(f345,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I62_J_0) ).
fof(f345_nnf,plain,
! [V_pname,V_vname_H,V_pname_H,V_fun_H] : hAPP(c_Com_Ocom_OBODY,V_pname) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f345]) ).
fof(f345_sk,plain,
! [V_pname,V_vname_H,V_pname_H,V_fun_H] : hAPP(c_Com_Ocom_OBODY,V_pname) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f345_nnf]) ).
cnf(c345,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OCall(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f345_sk]) ).
cnf(f347,axiom,
c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I18_J_0) ).
fof(f347_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f347]) ).
fof(f347_sk,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f347_nnf]) ).
cnf(c347,plain,
c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,X0),
inference(cnf_transformation,[status(esa)],[f347_sk]) ).
cnf(f420,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(f420_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)],[f420]) ).
fof(f420_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)],[f420_nnf]) ).
cnf(c420,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f420_sk]) ).
cnf(f428,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(f428_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)],[f428]) ).
fof(f428_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)],[f428_nnf]) ).
cnf(c428,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f428_sk]) ).
cnf(f433,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(f433_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)],[f433]) ).
fof(f433_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)],[f433_nnf]) ).
cnf(c433,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f433_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c19,c29,c33,c50,c51,c65,c76,c80,c85,c86,c88,c89,c93,c95,c96,c99,c101,c102,c106,c119,c120,c121,c134,c138,c147,c163,c166,c167,c190,c191,c193,c194,c197,c198,c207,c235,c236,c237,c238,c239,c244,c254,c262,c263,c273,c278,c286,c288,c293,c294,c316,c318,c332,c337,c339,c340,c341,c342,c343,c344,c345,c347,c420,c428,c433,c440]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t5286]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV840-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.02/0.30 % Computer : n012.cluster.edu
% 0.02/0.30 % Model : x86_64 x86_64
% 0.02/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.30 % Memory : 8046.5625MB
% 0.02/0.30 % OS : Linux 6.8.0-71-generic
% 0.02/0.30 % CPULimit : 300
% 0.02/0.30 % WCLimit : 300
% 0.02/0.30 % DateTime : Thu Sep 24 21:08:52 UTC 2026
% 0.02/0.30 % CPUTime :
% 0.02/0.30 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 65.76/8.65 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 65.76/8.65 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------