%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV938-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 : n011.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:32 PM UTC 2026
% Result : Unsatisfiable 79.47s 10.60s
% Output : Proof 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 84
% Syntax : Number of formulae : 360 ( 348 unt; 0 def)
% Number of atoms : 376 ( 328 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 343 ( 327 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-5 aty)
% Number of functors : 38 ( 38 usr; 17 con; 0-5 aty)
% Number of variables : 1298 ( 470 sgn 610 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f470,axiom,
( ~ c_WellType_OWT(V_P,V_E,V_e,V_T)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_WT__implies__WTrt_0) ).
fof(f470_nnf,plain,
! [V_P,V_h,V_E,V_e,V_T] :
( ~ c_WellType_OWT(V_P,V_E,V_e,V_T)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T) ),
inference(nnf_transformation,[status(thm)],[f470]) ).
fof(f470_sk,plain,
! [V_P,V_h,V_E,V_e,V_T] :
( ~ c_WellType_OWT(V_P,V_E,V_e,V_T)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T) ),
inference(skolemisation,[status(esa)],[f470_nnf]) ).
cnf(c470,plain,
( ~ c_WellType_OWT(X0,X2,X3,X4)
| c_WellTypeRT_OWTrt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f470_sk]) ).
cnf(t153,plain,
ifeq(c_WellType_OWT(X1,X2,X3,X4),true,c_WellTypeRT_OWTrt(X1,X5,X2,X3,X4),true) = true,
inference(equality_encoding,[status(esa)],[c470]) ).
cnf(t401,plain,
ifeq(c_WellType_OWT(X1,X2,X3,X4),true,c_WellTypeRT_OWTrt(X1,X5,X2,X3,X4),true) = true,
inference(orient,[status(thm)],[t153]) ).
cnf(f168,axiom,
( ~ c_WellType_OWT(V_P,V_E,V_e,V_T)
| ~ c_Map_Omap__le(V_E,V_E_H,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellType_OWT(V_P,V_E_H,V_e,V_T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_wt__env__mono_0) ).
fof(f168_nnf,plain,
! [V_P,V_E_H,V_e,V_T,V_E] :
( ~ c_WellType_OWT(V_P,V_E,V_e,V_T)
| ~ c_Map_Omap__le(V_E,V_E_H,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellType_OWT(V_P,V_E_H,V_e,V_T) ),
inference(nnf_transformation,[status(thm)],[f168]) ).
fof(f168_sk,plain,
! [V_P,V_E_H,V_e,V_T,V_E] :
( ~ c_WellType_OWT(V_P,V_E,V_e,V_T)
| ~ c_Map_Omap__le(V_E,V_E_H,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellType_OWT(V_P,V_E_H,V_e,V_T) ),
inference(skolemisation,[status(esa)],[f168_nnf]) ).
cnf(c168,plain,
( ~ c_WellType_OWT(X0,X4,X2,X3)
| ~ c_Map_Omap__le(X4,X1,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellType_OWT(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f168_sk]) ).
cnf(t187,plain,
ifeq(c_Map_Omap__le(X1,X2,tc_List_Olist(tc_String_Ochar),tc_Type_Oty),true,ifeq(c_WellType_OWT(X3,X1,X4,X5),true,c_WellType_OWT(X3,X2,X4,X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c168]) ).
cnf(t382,plain,
ifeq(c_Map_Omap__le(X1,X2,tc_List_Olist(tc_String_Ochar),tc_Type_Oty),true,ifeq(c_WellType_OWT(X3,X1,X4,X5),true,c_WellType_OWT(X3,X2,X4,X5),true),true) = true,
inference(orient,[status(thm)],[t187]) ).
cnf(f289,axiom,
c_Map_Omap__le(V_f,c_Map_Omap__add(V_g,V_f,T_a,T_b),T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_map__le__map__add_0) ).
fof(f289_nnf,plain,
! [V_f,V_g,T_a,T_b] : c_Map_Omap__le(V_f,c_Map_Omap__add(V_g,V_f,T_a,T_b),T_a,T_b),
inference(nnf_transformation,[status(thm)],[f289]) ).
fof(f289_sk,plain,
! [V_f,V_g,T_a,T_b] : c_Map_Omap__le(V_f,c_Map_Omap__add(V_g,V_f,T_a,T_b),T_a,T_b),
inference(skolemisation,[status(esa)],[f289_nnf]) ).
cnf(c289,plain,
c_Map_Omap__le(X0,c_Map_Omap__add(X1,X0,X2,X3),X2,X3),
inference(cnf_transformation,[status(esa)],[f289_sk]) ).
cnf(t50,plain,
c_Map_Omap__le(X1,c_Map_Omap__add(X2,X1,X3,X4),X3,X4) = true,
inference(equality_encoding,[status(esa)],[c289]) ).
cnf(t428,plain,
c_Map_Omap__le(X1,c_Map_Omap__add(X2,X1,X3,X4),X3,X4) = true,
inference(orient,[status(thm)],[t50]) ).
cnf(t432,plain,
true = ifeq(true,true,ifeq(c_WellType_OWT(X1,X2,X3,X4),true,c_WellType_OWT(X1,c_Map_Omap__add(X5,X2,tc_List_Olist(tc_String_Ochar),tc_Type_Oty),X3,X4),true),true),
inference(cp,[status(thm)],[t382,t428]) ).
cnf(t13,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t221,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t13]) ).
cnf(t4167,plain,
true = ifeq(c_WellType_OWT(X1,X2,X3,X4),true,c_WellType_OWT(X1,c_Map_Omap__add(X5,X2,tc_List_Olist(tc_String_Ochar),tc_Type_Oty),X3,X4),true),
inference(step,[status(thm)],[t432,t221]) ).
cnf(t2010,plain,
ifeq(c_WellType_OWT(X1,X2,X3,X4),true,c_WellType_OWT(X1,c_Map_Omap__add(X5,X2,tc_List_Olist(tc_String_Ochar),tc_Type_Oty),X3,X4),true) = true,
inference(orient,[status(thm)],[t4167]) ).
cnf(f483,axiom,
c_WellType_OWT(v_P,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_wtabody_0) ).
fof(f483_nnf,plain,
c_WellType_OWT(v_P,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(nnf_transformation,[status(thm)],[f483]) ).
cnf(c483,plain,
c_WellType_OWT(v_P,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(cnf_transformation,[status(esa)],[f483_nnf]) ).
cnf(t195,plain,
c_WellType_OWT(v_P,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____) = true,
inference(equality_encoding,[status(esa)],[c483]) ).
cnf(t491,plain,
c_WellType_OWT(v_P,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____) = true,
inference(orient,[status(thm)],[t195]) ).
cnf(t2011,plain,
true = ifeq(true,true,c_WellType_OWT(v_P,c_Map_Omap__add(X1,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),true),
inference(cp,[status(thm)],[t2010,t491]) ).
cnf(t4215,plain,
true = c_WellType_OWT(v_P,c_Map_Omap__add(X1,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(step,[status(thm)],[t2011,t221]) ).
cnf(f434,axiom,
c_Map_Omap__add(V_m1,c_Map_Omap__upds(V_m2,V_xs,V_ys,T_a,T_b),T_a,T_b) = c_Map_Omap__upds(c_Map_Omap__add(V_m1,V_m2,T_a,T_b),V_xs,V_ys,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_map__add__upds_0) ).
fof(f434_nnf,plain,
! [V_m1,V_m2,V_xs,V_ys,T_a,T_b] : c_Map_Omap__add(V_m1,c_Map_Omap__upds(V_m2,V_xs,V_ys,T_a,T_b),T_a,T_b) = c_Map_Omap__upds(c_Map_Omap__add(V_m1,V_m2,T_a,T_b),V_xs,V_ys,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f434]) ).
fof(f434_sk,plain,
! [V_m1,V_m2,V_xs,V_ys,T_a,T_b] : c_Map_Omap__add(V_m1,c_Map_Omap__upds(V_m2,V_xs,V_ys,T_a,T_b),T_a,T_b) = c_Map_Omap__upds(c_Map_Omap__add(V_m1,V_m2,T_a,T_b),V_xs,V_ys,T_a,T_b),
inference(skolemisation,[status(esa)],[f434_nnf]) ).
cnf(c434,plain,
c_Map_Omap__add(X0,c_Map_Omap__upds(X1,X2,X3,X4,X5),X4,X5) = c_Map_Omap__upds(c_Map_Omap__add(X0,X1,X4,X5),X2,X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f434_sk]) ).
cnf(t175,plain,
c_Map_Omap__upds(c_Map_Omap__add(X1,X2,X3,X4),X5,X6,X3,X4) = c_Map_Omap__add(X1,c_Map_Omap__upds(X2,X5,X6,X3,X4),X3,X4),
inference(equality_encoding,[status(esa)],[c434]) ).
cnf(t957,plain,
c_Map_Omap__add(X1,c_Map_Omap__upds(X2,X3,X4,X5,X6),X5,X6) = c_Map_Omap__upds(c_Map_Omap__add(X1,X2,X5,X6),X3,X4,X5,X6),
inference(orient,[status(thm)],[t175]) ).
cnf(t4216,plain,
true = c_WellType_OWT(v_P,c_Map_Omap__upds(c_Map_Omap__add(X1,c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(step,[status(thm)],[t4215,t957]) ).
cnf(f236,axiom,
c_Map_Omap__add(V_m,c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),T_a,T_b) = V_m,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_map__add__empty_0) ).
fof(f236_nnf,plain,
! [V_m,T_b,T_a] : c_Map_Omap__add(V_m,c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),T_a,T_b) = V_m,
inference(nnf_transformation,[status(thm)],[f236]) ).
fof(f236_sk,plain,
! [V_m,T_b,T_a] : c_Map_Omap__add(V_m,c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),T_a,T_b) = V_m,
inference(skolemisation,[status(esa)],[f236_nnf]) ).
cnf(c236,plain,
c_Map_Omap__add(X0,c_COMBK(c_Option_Ooption_ONone(X1),tc_Option_Ooption(X1),X2),X2,X1) = X0,
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(t62,plain,
c_Map_Omap__add(X1,c_COMBK(c_Option_Ooption_ONone(X2),tc_Option_Ooption(X2),X3),X3,X2) = X1,
inference(equality_encoding,[status(esa)],[c236]) ).
cnf(t274,plain,
c_Map_Omap__add(X1,c_COMBK(c_Option_Ooption_ONone(X2),tc_Option_Ooption(X2),X3),X3,X2) = X1,
inference(orient,[status(thm)],[t62]) ).
cnf(t4217,plain,
true = c_WellType_OWT(v_P,c_Map_Omap__upds(X1,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(step,[status(thm)],[t4216,t274]) ).
cnf(t2967,plain,
c_WellType_OWT(v_P,c_Map_Omap__upds(X1,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____) = true,
inference(orient,[status(thm)],[t4217]) ).
cnf(t2969,plain,
true = ifeq(true,true,c_WellTypeRT_OWTrt(v_P,X1,c_Map_Omap__upds(X2,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),true),
inference(cp,[status(thm)],[t401,t2967]) ).
cnf(t4260,plain,
true = c_WellTypeRT_OWTrt(v_P,X1,c_Map_Omap__upds(X2,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(step,[status(thm)],[t2969,t221]) ).
cnf(t4099,plain,
c_WellTypeRT_OWTrt(v_P,X1,c_Map_Omap__upds(X2,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____) = true,
inference(orient,[status(thm)],[t4260]) ).
cnf(f24,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I187_J_0) ).
fof(f24_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OCall(X3,X4,X5,X2),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(f26,axiom,
c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I31_J_0) ).
fof(f26_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != c_Expr_Oexp_Onew(X4,X3),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(f27,axiom,
hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I78_J_0) ).
fof(f27_nnf,plain,
! [T_a,V_val,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [T_a,V_val,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
hAPP(c_Expr_Oexp_OVal(X0),X1) != c_Expr_Oexp_OFAss(X2,X3,X4,X5,X0),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(f28,axiom,
hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I80_J_0) ).
fof(f28_nnf,plain,
! [T_a,V_val,V_exp_H,V_list1_H,V_list2_H] : hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [T_a,V_val,V_exp_H,V_list1_H,V_list2_H] : hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
hAPP(c_Expr_Oexp_OVal(X0),X1) != c_Expr_Oexp_OCall(X2,X3,X4,X0),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(f29,axiom,
c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I154_J_0) ).
fof(f29_nnf,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OFAss(X4,X5,X6,X7,X3),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(f30,axiom,
c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I156_J_0) ).
fof(f30_nnf,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OCall(X4,X5,X6,X3),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f31,axiom,
c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I55_J_0) ).
fof(f31_nnf,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OCast(X5,X6,X4),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(f32,axiom,
c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I170_J_0) ).
fof(f32_nnf,plain,
! [V_exp1,V_list1,V_list2,V_exp2,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [V_exp1,V_list1,V_list2,V_exp2,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OCall(X5,X6,X7,X4),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(f33,axiom,
c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I155_J_0) ).
fof(f33_nnf,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OFAcc(X5,X6,X7,X4),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(f36,axiom,
c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I174_J_0) ).
fof(f36_nnf,plain,
! [V_exp1,V_list1,V_list2,V_exp2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [V_exp1,V_list1,V_list2,V_exp2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_OSeq(X5,X6,X4),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(f43,axiom,
c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I186_J_0) ).
fof(f43_nnf,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OCall(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != c_Expr_Oexp_OSeq(X4,X5,X3),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(f44,axiom,
c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I54_J_0) ).
fof(f44_nnf,plain,
! [V_list,V_exp,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [V_list,V_exp,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OFAss(X3,X4,X5,X6,X2),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(f46,axiom,
c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I79_J_0) ).
fof(f46_nnf,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_val] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_val] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != hAPP(c_Expr_Oexp_OVal(X4),X5),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(f47,axiom,
c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I56_J_0) ).
fof(f47_nnf,plain,
! [V_list,V_exp,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [V_list,V_exp,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c47,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OCall(X3,X4,X5,X2),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(f53,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I28_J_0) ).
fof(f53_nnf,plain,
! [V_list,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
! [V_list,T_a,V_exp1_H,V_list1_H,V_list2_H,V_exp2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c53,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OFAss(X2,X3,X4,X5,X1),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(f54,axiom,
c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I29_J_0) ).
fof(f54_nnf,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_list] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
! [V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a,V_list] : c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c54,plain,
c_Expr_Oexp_OFAss(X0,X1,X2,X3,X4) != c_Expr_Oexp_Onew(X5,X4),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(f55,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I30_J_0) ).
fof(f55_nnf,plain,
! [V_list,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
! [V_list,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c55,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OCall(X2,X3,X4,X1),
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(f56,axiom,
c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I81_J_0) ).
fof(f56_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_val] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_val] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c56,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != hAPP(c_Expr_Oexp_OVal(X3),X4),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(f57,axiom,
c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I171_J_0) ).
fof(f57_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_exp1,V_list1,V_list2,V_exp2] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_exp1,V_list1,V_list2,V_exp2] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c57,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != c_Expr_Oexp_OFAss(X4,X5,X6,X7,X3),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(f58,axiom,
c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I57_J_0) ).
fof(f58_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c58,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != c_Expr_Oexp_OCast(X4,X5,X3),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(f59,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I175_J_0) ).
fof(f59_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp1,V_list1,V_list2,V_exp2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp1,V_list1,V_list2,V_exp2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c59,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OFAss(X3,X4,X5,X6,X2),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(f60,axiom,
c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I157_J_0) ).
fof(f60_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(nnf_transformation,[status(thm)],[f60]) ).
fof(f60_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OCall(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(skolemisation,[status(esa)],[f60_nnf]) ).
cnf(c60,plain,
c_Expr_Oexp_OCall(X0,X1,X2,X3) != c_Expr_Oexp_OFAcc(X4,X5,X6,X3),
inference(cnf_transformation,[status(esa)],[f60_sk]) ).
cnf(f160,axiom,
c_Fun_Ofun__upd(V_t,V_k,c_Option_Ooption_OSome(V_x,T_b),T_a,tc_Option_Ooption(T_b)) != c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_map__upd__nonempty_0) ).
fof(f160_nnf,plain,
! [V_t,V_k,V_x,T_b,T_a] : c_Fun_Ofun__upd(V_t,V_k,c_Option_Ooption_OSome(V_x,T_b),T_a,tc_Option_Ooption(T_b)) != c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),
inference(nnf_transformation,[status(thm)],[f160]) ).
fof(f160_sk,plain,
! [V_t,V_k,V_x,T_b,T_a] : c_Fun_Ofun__upd(V_t,V_k,c_Option_Ooption_OSome(V_x,T_b),T_a,tc_Option_Ooption(T_b)) != c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),
inference(skolemisation,[status(esa)],[f160_nnf]) ).
cnf(c160,plain,
c_Fun_Ofun__upd(X0,X1,c_Option_Ooption_OSome(X2,X3),X4,tc_Option_Ooption(X3)) != c_COMBK(c_Option_Ooption_ONone(X3),tc_Option_Ooption(X3),X4),
inference(cnf_transformation,[status(esa)],[f160_sk]) ).
cnf(f171,axiom,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I2_J_0) ).
fof(f171_nnf,plain,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f171]) ).
fof(f171_sk,plain,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f171_nnf]) ).
cnf(c171,plain,
c_Type_Oty_OVoid != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f171_sk]) ).
cnf(f173,axiom,
hAPP(c_Expr_Oexp_OVal(T_a),V_val_H) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I19_J_0) ).
fof(f173_nnf,plain,
! [T_a,V_val_H,V_list] : hAPP(c_Expr_Oexp_OVal(T_a),V_val_H) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f173]) ).
fof(f173_sk,plain,
! [T_a,V_val_H,V_list] : hAPP(c_Expr_Oexp_OVal(T_a),V_val_H) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f173_nnf]) ).
cnf(c173,plain,
hAPP(c_Expr_Oexp_OVal(X0),X1) != c_Expr_Oexp_Onew(X2,X0),
inference(cnf_transformation,[status(esa)],[f173_sk]) ).
cnf(f178,axiom,
c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I160_J_0) ).
fof(f178_nnf,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f178]) ).
fof(f178_sk,plain,
! [V_exp,V_list1,V_list2,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f178_nnf]) ).
cnf(c178,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OSeq(X4,X5,X3),
inference(cnf_transformation,[status(esa)],[f178_sk]) ).
cnf(f183,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(f183_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)],[f183]) ).
fof(f183_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)],[f183_nnf]) ).
cnf(c183,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f183_sk]) ).
cnf(f184,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(f184_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)],[f184]) ).
fof(f184_sk,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c184,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
cnf(f187,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I18_J_0) ).
fof(f187_nnf,plain,
! [V_list,T_a,V_val_H] : c_Expr_Oexp_Onew(V_list,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val_H),
inference(nnf_transformation,[status(thm)],[f187]) ).
fof(f187_sk,plain,
! [V_list,T_a,V_val_H] : c_Expr_Oexp_Onew(V_list,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val_H),
inference(skolemisation,[status(esa)],[f187_nnf]) ).
cnf(c187,plain,
c_Expr_Oexp_Onew(X0,X1) != hAPP(c_Expr_Oexp_OVal(X1),X2),
inference(cnf_transformation,[status(esa)],[f187_sk]) ).
cnf(f194,axiom,
c_Expr_Oexp_OCast(V_list,V_exp,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I44_J_0) ).
fof(f194_nnf,plain,
! [V_list,V_exp,T_a,V_val_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val_H),
inference(nnf_transformation,[status(thm)],[f194]) ).
fof(f194_sk,plain,
! [V_list,V_exp,T_a,V_val_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val_H),
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c194,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != hAPP(c_Expr_Oexp_OVal(X2),X3),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
cnf(f209,axiom,
c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I17_J_0) ).
fof(f209_nnf,plain,
! [V_list_H,V_exp_H,T_a,V_list] : c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f209]) ).
fof(f209_sk,plain,
! [V_list_H,V_exp_H,T_a,V_list] : c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f209_nnf]) ).
cnf(c209,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_Onew(X3,X2),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
cnf(f213,axiom,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I16_J_0) ).
fof(f213_nnf,plain,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f213]) ).
fof(f213_sk,plain,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f213_nnf]) ).
cnf(c213,plain,
c_Type_Oty_OInteger != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
cnf(f215,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I5_J_0) ).
fof(f215_nnf,plain,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f215]) ).
fof(f215_sk,plain,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f215_nnf]) ).
cnf(c215,plain,
c_Type_Oty_OInteger != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f215_sk]) ).
cnf(f219,axiom,
~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list__ex_Osimps_I1_J_0) ).
fof(f219_nnf,plain,
! [V_P,T_a] : ~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f219]) ).
fof(f219_sk,plain,
! [V_P,T_a] : ~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f219_nnf]) ).
cnf(c219,plain,
~ c_List_Olist__ex(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f219_sk]) ).
cnf(f223,axiom,
c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I52_J_0) ).
fof(f223_nnf,plain,
! [V_list,V_exp,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f223]) ).
fof(f223_sk,plain,
! [V_list,V_exp,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f223_nnf]) ).
cnf(c223,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OFAcc(X3,X4,X5,X2),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
cnf(f228,axiom,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I13_J_0) ).
fof(f228_nnf,plain,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f228]) ).
fof(f228_sk,plain,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f228_nnf]) ).
cnf(c228,plain,
c_Type_Oty_ONT != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f228_sk]) ).
cnf(f230,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(f230_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)],[f230]) ).
fof(f230_sk,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(skolemisation,[status(esa)],[f230_nnf]) ).
cnf(c230,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f230_sk]) ).
cnf(f231,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(f231_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)],[f231]) ).
fof(f231_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)],[f231_nnf]) ).
cnf(c231,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f231_sk]) ).
cnf(f234,axiom,
c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I77_J_0) ).
fof(f234_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_val] : c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
inference(nnf_transformation,[status(thm)],[f234]) ).
fof(f234_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_val] : c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
inference(skolemisation,[status(esa)],[f234_nnf]) ).
cnf(c234,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != hAPP(c_Expr_Oexp_OVal(X3),X4),
inference(cnf_transformation,[status(esa)],[f234_sk]) ).
cnf(f258,axiom,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I4_J_0) ).
fof(f258_nnf,plain,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f258]) ).
fof(f258_sk,plain,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f258_nnf]) ).
cnf(c258,plain,
c_Type_Oty_OVoid != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f258_sk]) ).
cnf(f259,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I16_J_0) ).
fof(f259_nnf,plain,
! [V_list,T_a,V_list_H,V_exp_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a),
inference(nnf_transformation,[status(thm)],[f259]) ).
fof(f259_sk,plain,
! [V_list,T_a,V_list_H,V_exp_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a),
inference(skolemisation,[status(esa)],[f259_nnf]) ).
cnf(c259,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OCast(X2,X3,X1),
inference(cnf_transformation,[status(esa)],[f259_sk]) ).
cnf(f260,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I11_J_0) ).
fof(f260_nnf,plain,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f260]) ).
fof(f260_sk,plain,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f260_nnf]) ).
cnf(c260,plain,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f260_sk]) ).
cnf(f262,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I26_J_0) ).
fof(f262_nnf,plain,
! [V_list,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f262]) ).
fof(f262_sk,plain,
! [V_list,T_a,V_exp_H,V_list1_H,V_list2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f262_nnf]) ).
cnf(c262,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OFAcc(X2,X3,X4,X1),
inference(cnf_transformation,[status(esa)],[f262_sk]) ).
cnf(f266,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I12_J_0) ).
fof(f266_nnf,plain,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f266]) ).
fof(f266_sk,plain,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f266_nnf]) ).
cnf(c266,plain,
c_Type_Oty_OBoolean != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f266_sk]) ).
cnf(f267,axiom,
c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I27_J_0) ).
fof(f267_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list] : c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f267]) ).
fof(f267_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list] : c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f267_nnf]) ).
cnf(c267,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_Onew(X4,X3),
inference(cnf_transformation,[status(esa)],[f267_sk]) ).
cnf(f268,axiom,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I6_J_0) ).
fof(f268_nnf,plain,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f268]) ).
fof(f268_sk,plain,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f268_nnf]) ).
cnf(c268,plain,
c_Type_Oty_OVoid != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f268_sk]) ).
cnf(f275,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I85_J_0) ).
fof(f275_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_val] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
inference(nnf_transformation,[status(thm)],[f275]) ).
fof(f275_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_val] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != hAPP(c_Expr_Oexp_OVal(T_a),V_val),
inference(skolemisation,[status(esa)],[f275_nnf]) ).
cnf(c275,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != hAPP(c_Expr_Oexp_OVal(X2),X3),
inference(cnf_transformation,[status(esa)],[f275_sk]) ).
cnf(f291,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I61_J_0) ).
fof(f291_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(nnf_transformation,[status(thm)],[f291]) ).
fof(f291_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(skolemisation,[status(esa)],[f291_nnf]) ).
cnf(c291,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OCast(X3,X4,X2),
inference(cnf_transformation,[status(esa)],[f291_sk]) ).
cnf(f314,axiom,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I7_J_0) ).
fof(f314_nnf,plain,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f314]) ).
fof(f314_sk,plain,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f314_nnf]) ).
cnf(c314,plain,
c_Type_Oty_ONT != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
cnf(f315,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I10_J_0) ).
fof(f315_nnf,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f315]) ).
fof(f315_sk,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f315_nnf]) ).
cnf(c315,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f315_sk]) ).
cnf(f320,axiom,
~ c_List_Omember(V_x,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_List_Omember_Osimps_I1_J_0) ).
fof(f320_nnf,plain,
! [V_x,T_a] : ~ c_List_Omember(V_x,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f320]) ).
fof(f320_sk,plain,
! [V_x,T_a] : ~ c_List_Omember(V_x,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f320_nnf]) ).
cnf(c320,plain,
~ c_List_Omember(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f320_sk]) ).
cnf(f342,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I3_J_0) ).
fof(f342_nnf,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f342]) ).
fof(f342_sk,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f342_nnf]) ).
cnf(c342,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f342_sk]) ).
cnf(f345,axiom,
c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I53_J_0) ).
fof(f345_nnf,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(nnf_transformation,[status(thm)],[f345]) ).
fof(f345_sk,plain,
! [V_exp_H,V_list1_H,V_list2_H,T_a,V_list,V_exp] : c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(skolemisation,[status(esa)],[f345_nnf]) ).
cnf(c345,plain,
c_Expr_Oexp_OFAcc(X0,X1,X2,X3) != c_Expr_Oexp_OCast(X4,X5,X3),
inference(cnf_transformation,[status(esa)],[f345_sk]) ).
cnf(f357,axiom,
c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I34_J_0) ).
fof(f357_nnf,plain,
! [V_list,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f357]) ).
fof(f357_sk,plain,
! [V_list,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_Onew(V_list,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f357_nnf]) ).
cnf(c357,plain,
c_Expr_Oexp_Onew(X0,X1) != c_Expr_Oexp_OSeq(X2,X3,X1),
inference(cnf_transformation,[status(esa)],[f357_sk]) ).
cnf(f359,axiom,
hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I76_J_0) ).
fof(f359_nnf,plain,
! [T_a,V_val,V_exp_H,V_list1_H,V_list2_H] : hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(nnf_transformation,[status(thm)],[f359]) ).
fof(f359_sk,plain,
! [T_a,V_val,V_exp_H,V_list1_H,V_list2_H] : hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a),
inference(skolemisation,[status(esa)],[f359_nnf]) ).
cnf(c359,plain,
hAPP(c_Expr_Oexp_OVal(X0),X1) != c_Expr_Oexp_OFAcc(X2,X3,X4,X0),
inference(cnf_transformation,[status(esa)],[f359_sk]) ).
cnf(f362,axiom,
c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I60_J_0) ).
fof(f362_nnf,plain,
! [V_list,V_exp,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f362]) ).
fof(f362_sk,plain,
! [V_list,V_exp,T_a,V_exp1_H,V_exp2_H] : c_Expr_Oexp_OCast(V_list,V_exp,T_a) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f362_nnf]) ).
cnf(c362,plain,
c_Expr_Oexp_OCast(X0,X1,X2) != c_Expr_Oexp_OSeq(X3,X4,X2),
inference(cnf_transformation,[status(esa)],[f362_sk]) ).
cnf(f365,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I35_J_0) ).
fof(f365_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_list] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(nnf_transformation,[status(thm)],[f365]) ).
fof(f365_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_list] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_Onew(V_list,T_a),
inference(skolemisation,[status(esa)],[f365_nnf]) ).
cnf(c365,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_Onew(X3,X2),
inference(cnf_transformation,[status(esa)],[f365_sk]) ).
cnf(f369,axiom,
hAPP(c_Expr_Oexp_OVal(T_a),V_val_H) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I45_J_0) ).
fof(f369_nnf,plain,
! [T_a,V_val_H,V_list,V_exp] : hAPP(c_Expr_Oexp_OVal(T_a),V_val_H) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(nnf_transformation,[status(thm)],[f369]) ).
fof(f369_sk,plain,
! [T_a,V_val_H,V_list,V_exp] : hAPP(c_Expr_Oexp_OVal(T_a),V_val_H) != c_Expr_Oexp_OCast(V_list,V_exp,T_a),
inference(skolemisation,[status(esa)],[f369_nnf]) ).
cnf(c369,plain,
hAPP(c_Expr_Oexp_OVal(X0),X1) != c_Expr_Oexp_OCast(X2,X3,X0),
inference(cnf_transformation,[status(esa)],[f369_sk]) ).
cnf(f375,axiom,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I17_J_0) ).
fof(f375_nnf,plain,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f375]) ).
fof(f375_sk,plain,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f375_nnf]) ).
cnf(c375,plain,
c_Type_Oty_ONT != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f375_sk]) ).
cnf(f388,axiom,
hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I84_J_0) ).
fof(f388_nnf,plain,
! [T_a,V_val,V_exp1_H,V_exp2_H] : hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(nnf_transformation,[status(thm)],[f388]) ).
fof(f388_sk,plain,
! [T_a,V_val,V_exp1_H,V_exp2_H] : hAPP(c_Expr_Oexp_OVal(T_a),V_val) != c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a),
inference(skolemisation,[status(esa)],[f388_nnf]) ).
cnf(c388,plain,
hAPP(c_Expr_Oexp_OVal(X0),X1) != c_Expr_Oexp_OSeq(X2,X3,X0),
inference(cnf_transformation,[status(esa)],[f388_sk]) ).
cnf(f391,axiom,
c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp_Osimps_I161_J_0) ).
fof(f391_nnf,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(nnf_transformation,[status(thm)],[f391]) ).
fof(f391_sk,plain,
! [V_exp1_H,V_exp2_H,T_a,V_exp,V_list1,V_list2] : c_Expr_Oexp_OSeq(V_exp1_H,V_exp2_H,T_a) != c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a),
inference(skolemisation,[status(esa)],[f391_nnf]) ).
cnf(c391,plain,
c_Expr_Oexp_OSeq(X0,X1,X2) != c_Expr_Oexp_OFAcc(X3,X4,X5,X2),
inference(cnf_transformation,[status(esa)],[f391_sk]) ).
cnf(f401,axiom,
c_Type_Oty_OVoid != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I8_J_0) ).
fof(f401_nnf,plain,
! [V_list_H] : c_Type_Oty_OVoid != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f401]) ).
fof(f401_sk,plain,
! [V_list_H] : c_Type_Oty_OVoid != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f401_nnf]) ).
cnf(c401,plain,
c_Type_Oty_OVoid != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f401_sk]) ).
cnf(f410,axiom,
c_Type_Oty_ONT != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I20_J_0) ).
fof(f410_nnf,plain,
! [V_list_H] : c_Type_Oty_ONT != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f410]) ).
fof(f410_sk,plain,
! [V_list_H] : c_Type_Oty_ONT != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f410_nnf]) ).
cnf(c410,plain,
c_Type_Oty_ONT != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f410_sk]) ).
cnf(f412,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I18_J_0) ).
fof(f412_nnf,plain,
! [V_list_H] : c_Type_Oty_OInteger != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f412]) ).
fof(f412_sk,plain,
! [V_list_H] : c_Type_Oty_OInteger != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f412_nnf]) ).
cnf(c412,plain,
c_Type_Oty_OInteger != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f412_sk]) ).
cnf(f413,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OBoolean,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I15_J_0) ).
fof(f413_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OBoolean,
inference(nnf_transformation,[status(thm)],[f413]) ).
fof(f413_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OBoolean,
inference(skolemisation,[status(esa)],[f413_nnf]) ).
cnf(c413,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_OBoolean,
inference(cnf_transformation,[status(esa)],[f413_sk]) ).
cnf(f415,axiom,
~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_List_Onull_Osimps_I2_J_0) ).
fof(f415_nnf,plain,
! [V_x,V_xs,T_a] : ~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
inference(nnf_transformation,[status(thm)],[f415]) ).
fof(f415_sk,plain,
! [V_x,V_xs,T_a] : ~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
inference(skolemisation,[status(esa)],[f415_nnf]) ).
cnf(c415,plain,
~ c_List_Onull(c_List_Olist_OCons(X0,X1,X2),X2),
inference(cnf_transformation,[status(esa)],[f415_sk]) ).
cnf(f419,axiom,
c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).
fof(f419_nnf,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(nnf_transformation,[status(thm)],[f419]) ).
fof(f419_sk,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(skolemisation,[status(esa)],[f419_nnf]) ).
cnf(c419,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f419_sk]) ).
cnf(f443,axiom,
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dropWhile__eq__Cons__conv_1) ).
fof(f443_nnf,plain,
! [V_P,V_xs,T_a,V_y,V_ys] :
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
inference(nnf_transformation,[status(thm)],[f443]) ).
fof(f443_sk,plain,
! [V_P,V_xs,T_a,V_y,V_ys] :
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
inference(skolemisation,[status(esa)],[f443_nnf]) ).
cnf(c443,plain,
( ~ hBOOL(hAPP(X0,X3))
| c_List_OdropWhile(X0,X1,X2) != c_List_Olist_OCons(X3,X4,X2) ),
inference(cnf_transformation,[status(esa)],[f443_sk]) ).
cnf(f444,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OVoid,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I9_J_0) ).
fof(f444_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OVoid,
inference(nnf_transformation,[status(thm)],[f444]) ).
fof(f444_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OVoid,
inference(skolemisation,[status(esa)],[f444_nnf]) ).
cnf(c444,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_OVoid,
inference(cnf_transformation,[status(esa)],[f444_sk]) ).
cnf(f451,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OInteger,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I19_J_0) ).
fof(f451_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OInteger,
inference(nnf_transformation,[status(thm)],[f451]) ).
fof(f451_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_OInteger,
inference(skolemisation,[status(esa)],[f451_nnf]) ).
cnf(c451,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_OInteger,
inference(cnf_transformation,[status(esa)],[f451_sk]) ).
cnf(f457,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_OClass(V_list_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I14_J_0) ).
fof(f457_nnf,plain,
! [V_list_H] : c_Type_Oty_OBoolean != c_Type_Oty_OClass(V_list_H),
inference(nnf_transformation,[status(thm)],[f457]) ).
fof(f457_sk,plain,
! [V_list_H] : c_Type_Oty_OBoolean != c_Type_Oty_OClass(V_list_H),
inference(skolemisation,[status(esa)],[f457_nnf]) ).
cnf(c457,plain,
c_Type_Oty_OBoolean != c_Type_Oty_OClass(X0),
inference(cnf_transformation,[status(esa)],[f457_sk]) ).
cnf(f463,axiom,
c_Type_Oty_OClass(V_list_H) != c_Type_Oty_ONT,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ty_Osimps_I21_J_0) ).
fof(f463_nnf,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_ONT,
inference(nnf_transformation,[status(thm)],[f463]) ).
fof(f463_sk,plain,
! [V_list_H] : c_Type_Oty_OClass(V_list_H) != c_Type_Oty_ONT,
inference(skolemisation,[status(esa)],[f463_nnf]) ).
cnf(c463,plain,
c_Type_Oty_OClass(X0) != c_Type_Oty_ONT,
inference(cnf_transformation,[status(esa)],[f463_sk]) ).
cnf(f478,axiom,
c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).
fof(f478_nnf,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f478]) ).
fof(f478_sk,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f478_nnf]) ).
cnf(c478,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f478_sk]) ).
cnf(f479,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).
fof(f479_nnf,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f479]) ).
fof(f479_sk,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f479_nnf]) ).
cnf(c479,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f479_sk]) ).
cnf(f490,axiom,
c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).
fof(f490_nnf,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(nnf_transformation,[status(thm)],[f490]) ).
fof(f490_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f490_nnf]) ).
cnf(c490,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f490_sk]) ).
cnf(f491,axiom,
V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f491_nnf,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(nnf_transformation,[status(thm)],[f491]) ).
fof(f491_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f491_nnf]) ).
cnf(c491,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f491_sk]) ).
cnf(f497,negated_conjecture,
~ c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(v_E____,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f497_nnf,plain,
~ c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(v_E____,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(nnf_transformation,[status(thm)],[f497]) ).
fof(f497_sk,plain,
~ c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(v_E____,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(skolemisation,[status(esa)],[f497_nnf]) ).
cnf(c497,plain,
~ c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(v_E____,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(cnf_transformation,[status(esa)],[f497_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c24,c26,c27,c28,c29,c30,c31,c32,c33,c36,c43,c44,c46,c47,c53,c54,c55,c56,c57,c58,c59,c60,c160,c171,c173,c178,c183,c184,c187,c194,c209,c213,c215,c219,c223,c228,c230,c231,c234,c258,c259,c260,c262,c266,c267,c268,c275,c291,c314,c315,c320,c342,c345,c357,c359,c362,c365,c369,c375,c388,c391,c401,c410,c412,c413,c415,c419,c443,c444,c451,c457,c463,c478,c479,c490,c491,c497]) ).
cnf(g0_0,plain,
c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(v_E____,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____) != false,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != false,
inference(rw,[status(thm)],[g0_0,t4099]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV938-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.42 % Computer : n011.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Thu Sep 24 21:21:29 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 79.47/10.60 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 79.47/10.60 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------