%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV892-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 : n013.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:25 PM UTC 2026
% Result : Unsatisfiable 90.57s 22.05s
% Output : Proof 90.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 84
% Syntax : Number of formulae : 380 ( 284 unt; 0 def)
% Number of atoms : 520 ( 285 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 578 ( 438 ~; 140 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 3 prp; 0-4 aty)
% Number of functors : 33 ( 33 usr; 8 con; 0-4 aty)
% Number of variables : 1051 ( 365 sgn 504 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f661,axiom,
( c_Com_OWT(V_b)
| ~ c_Com_OWT__bodies
| hAPP(c_Com_Obody,V_pn) != c_Option_Ooption_OSome(V_b,tc_Com_Ocom) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WT__bodiesD_0) ).
fof(f661_nnf,plain,
! [V_pn,V_b] :
( c_Com_OWT(V_b)
| ~ c_Com_OWT__bodies
| hAPP(c_Com_Obody,V_pn) != c_Option_Ooption_OSome(V_b,tc_Com_Ocom) ),
inference(nnf_transformation,[status(thm)],[f661]) ).
fof(f661_sk,plain,
! [V_pn,V_b] :
( c_Com_OWT(V_b)
| ~ c_Com_OWT__bodies
| hAPP(c_Com_Obody,V_pn) != c_Option_Ooption_OSome(V_b,tc_Com_Ocom) ),
inference(skolemisation,[status(esa)],[f661_nnf]) ).
cnf(c661,plain,
( c_Com_OWT(X1)
| ~ c_Com_OWT__bodies
| hAPP(c_Com_Obody,X0) != c_Option_Ooption_OSome(X1,tc_Com_Ocom) ),
inference(cnf_transformation,[status(esa)],[f661_sk]) ).
cnf(t120,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),ifeq(c_Com_OWT__bodies,true,c_Com_OWT(X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c661]) ).
cnf(t286,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),ifeq(c_Com_OWT__bodies,true,c_Com_OWT(X2),true),true) = true,
inference(orient,[status(thm)],[t120]) ).
cnf(f666,negated_conjecture,
c_Com_OWT__bodies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f666_nnf,plain,
c_Com_OWT__bodies,
inference(nnf_transformation,[status(thm)],[f666]) ).
cnf(c666,plain,
c_Com_OWT__bodies,
inference(cnf_transformation,[status(esa)],[f666_nnf]) ).
cnf(t0,plain,
true = c_Com_OWT__bodies,
inference(equality_encoding,[status(esa)],[c666]) ).
cnf(t1117,plain,
c_Com_OWT__bodies = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t10057,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),ifeq(true,true,c_Com_OWT(X2),true),true) = true,
inference(step,[status(thm)],[t286,t1117]) ).
cnf(t27,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t27]) ).
cnf(t10058,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),c_Com_OWT(X2),true) = true,
inference(step,[status(thm)],[t10057,t256]) ).
cnf(t1118,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),c_Com_OWT(X2),true) = true,
inference(rw,[status(thm)],[t10058]) ).
cnf(t9537,plain,
ifeq(hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(X2,tc_Com_Ocom),c_Com_OWT(X2),true) = true,
inference(orient,[status(thm)],[t1118]) ).
cnf(f344,axiom,
( ~ c_Com_OWT(c_Com_Ocom_OBODY(V_P))
| hAPP(c_Com_Obody,V_P) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(V_P),tc_Com_Ocom) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WTs__elim__cases_I7_J_0) ).
fof(f344_nnf,plain,
! [V_P] :
( ~ c_Com_OWT(c_Com_Ocom_OBODY(V_P))
| hAPP(c_Com_Obody,V_P) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(V_P),tc_Com_Ocom) ),
inference(nnf_transformation,[status(thm)],[f344]) ).
fof(f344_sk,plain,
! [V_P] :
( ~ c_Com_OWT(c_Com_Ocom_OBODY(V_P))
| hAPP(c_Com_Obody,V_P) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(V_P),tc_Com_Ocom) ),
inference(skolemisation,[status(esa)],[f344_nnf]) ).
cnf(c344,plain,
( ~ c_Com_OWT(c_Com_Ocom_OBODY(X0))
| hAPP(c_Com_Obody,X0) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(X0),tc_Com_Ocom) ),
inference(cnf_transformation,[status(esa)],[f344_sk]) ).
cnf(t132,plain,
ifeq(c_Com_OWT(c_Com_Ocom_OBODY(X1)),true,hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(X1),tc_Com_Ocom)) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(X1),tc_Com_Ocom),
inference(equality_encoding,[status(esa)],[c344]) ).
cnf(t1151,plain,
ifeq(c_Com_OWT(c_Com_Ocom_OBODY(X1)),true,hAPP(c_Com_Obody,X1),c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(X1),tc_Com_Ocom)) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(X1),tc_Com_Ocom),
inference(orient,[status(thm)],[t132]) ).
cnf(f635,axiom,
( hAPP(c_Com_Obody,V_pn) = c_Option_Ooption_ONone(tc_Com_Ocom)
| c_Com_OWT(c_Com_Ocom_OBODY(V_pn)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WT_OBody_0) ).
fof(f635_nnf,plain,
! [V_pn] :
( hAPP(c_Com_Obody,V_pn) = c_Option_Ooption_ONone(tc_Com_Ocom)
| c_Com_OWT(c_Com_Ocom_OBODY(V_pn)) ),
inference(nnf_transformation,[status(thm)],[f635]) ).
fof(f635_sk,plain,
! [V_pn] :
( hAPP(c_Com_Obody,V_pn) = c_Option_Ooption_ONone(tc_Com_Ocom)
| c_Com_OWT(c_Com_Ocom_OBODY(V_pn)) ),
inference(skolemisation,[status(esa)],[f635_nnf]) ).
cnf(c635,plain,
( hAPP(c_Com_Obody,X0) = c_Option_Ooption_ONone(tc_Com_Ocom)
| c_Com_OWT(c_Com_Ocom_OBODY(X0)) ),
inference(cnf_transformation,[status(esa)],[f635_sk]) ).
cnf(t103,plain,
or(c_Com_OWT(c_Com_Ocom_OBODY(X1)),eq(hAPP(c_Com_Obody,X1),c_Option_Ooption_ONone(tc_Com_Ocom))) = true,
inference(equality_encoding,[status(esa)],[c635]) ).
cnf(t1110,plain,
or(c_Com_OWT(c_Com_Ocom_OBODY(X1)),eq(hAPP(c_Com_Obody,X1),c_Option_Ooption_ONone(tc_Com_Ocom))) = true,
inference(orient,[status(thm)],[t103]) ).
cnf(f322,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(f322_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)],[f322]) ).
fof(f322_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)],[f322_nnf]) ).
cnf(c322,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f322_sk]) ).
cnf(t43,plain,
eq(c_Option_Ooption_OSome(X1,X2),c_Option_Ooption_ONone(X2)) = false,
inference(equality_encoding,[status(esa)],[c322]) ).
cnf(t1534,plain,
eq(c_Option_Ooption_OSome(X1,X2),c_Option_Ooption_ONone(X2)) = false,
inference(orient,[status(thm)],[t43]) ).
cnf(f633,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Map_Odom(V_m,T_a,T_b)))
| hAPP(V_m,V_a) = c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(V_a,V_m,T_a,T_b),T_b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_domD_0) ).
fof(f633_nnf,plain,
! [V_m,V_a,T_a,T_b] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Map_Odom(V_m,T_a,T_b)))
| hAPP(V_m,V_a) = c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(V_a,V_m,T_a,T_b),T_b) ),
inference(nnf_transformation,[status(thm)],[f633]) ).
fof(f633_sk,plain,
! [V_m,V_a,T_a,T_b] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Map_Odom(V_m,T_a,T_b)))
| hAPP(V_m,V_a) = c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(V_a,V_m,T_a,T_b),T_b) ),
inference(skolemisation,[status(esa)],[f633_nnf]) ).
cnf(c633,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),c_Map_Odom(X0,X2,X3)))
| hAPP(X0,X1) = c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(X1,X0,X2,X3),X3) ),
inference(cnf_transformation,[status(esa)],[f633_sk]) ).
cnf(t207,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(X1),X2),c_Map_Odom(X3,X1,X4))),true,hAPP(X3,X2),c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(X2,X3,X1,X4),X4)) = c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(X2,X3,X1,X4),X4),
inference(equality_encoding,[status(esa)],[c633]) ).
cnf(t1145,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(X1),X2),c_Map_Odom(X3,X1,X4))),true,hAPP(X3,X2),c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(X2,X3,X1,X4),X4)) = c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(X2,X3,X1,X4),X4),
inference(orient,[status(thm)],[t207]) ).
cnf(f668,negated_conjecture,
hBOOL(hAPP(hAPP(c_in(tc_Com_Opname),v_pn),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f668_nnf,plain,
hBOOL(hAPP(hAPP(c_in(tc_Com_Opname),v_pn),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom))),
inference(nnf_transformation,[status(thm)],[f668]) ).
cnf(c668,plain,
hBOOL(hAPP(hAPP(c_in(tc_Com_Opname),v_pn),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom))),
inference(cnf_transformation,[status(esa)],[f668_nnf]) ).
cnf(t95,plain,
hBOOL(hAPP(hAPP(c_in(tc_Com_Opname),v_pn),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom))) = true,
inference(equality_encoding,[status(esa)],[c668]) ).
cnf(t542,plain,
hBOOL(hAPP(hAPP(c_in(tc_Com_Opname),v_pn),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom))) = true,
inference(orient,[status(thm)],[t95]) ).
cnf(t1146,plain,
c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(v_pn,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom) = ifeq(true,true,hAPP(c_Com_Obody,v_pn),c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(v_pn,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom)),
inference(cp,[status(thm)],[t1145,t542]) ).
cnf(t10086,plain,
c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(v_pn,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom) = hAPP(c_Com_Obody,v_pn),
inference(step,[status(thm)],[t1146,t256]) ).
cnf(t1861,plain,
c_Option_Ooption_OSome(c_Map_Osko__Map__XdomD__1__1(v_pn,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom) = hAPP(c_Com_Obody,v_pn),
inference(orient,[status(thm)],[t10086]) ).
cnf(t1863,plain,
false = eq(hAPP(c_Com_Obody,v_pn),c_Option_Ooption_ONone(tc_Com_Ocom)),
inference(cp,[status(thm)],[t1534,t1861]) ).
cnf(t1873,plain,
eq(hAPP(c_Com_Obody,v_pn),c_Option_Ooption_ONone(tc_Com_Ocom)) = false,
inference(orient,[status(thm)],[t1863]) ).
cnf(t1875,plain,
true = or(c_Com_OWT(c_Com_Ocom_OBODY(v_pn)),false),
inference(cp,[status(thm)],[t1110,t1873]) ).
cnf(t5,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t281,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t10087,plain,
true = c_Com_OWT(c_Com_Ocom_OBODY(v_pn)),
inference(step,[status(thm)],[t1875,t281]) ).
cnf(t1879,plain,
c_Com_OWT(c_Com_Ocom_OBODY(v_pn)) = true,
inference(orient,[status(thm)],[t10087]) ).
cnf(t1880,plain,
c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),tc_Com_Ocom) = ifeq(true,true,hAPP(c_Com_Obody,v_pn),c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),tc_Com_Ocom)),
inference(cp,[status(thm)],[t1151,t1879]) ).
cnf(t10088,plain,
c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),tc_Com_Ocom) = hAPP(c_Com_Obody,v_pn),
inference(step,[status(thm)],[t1880,t256]) ).
cnf(t1891,plain,
c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),tc_Com_Ocom) = hAPP(c_Com_Obody,v_pn),
inference(orient,[status(thm)],[t10088]) ).
cnf(t9538,plain,
true = ifeq(hAPP(c_Com_Obody,X1),hAPP(c_Com_Obody,v_pn),c_Com_OWT(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn)),true),
inference(cp,[status(thm)],[t9537,t1891]) ).
cnf(f669,negated_conjecture,
~ c_Com_OWT(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f669_nnf,plain,
~ c_Com_OWT(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom)),
inference(nnf_transformation,[status(thm)],[f669]) ).
fof(f669_sk,plain,
~ c_Com_OWT(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom)),
inference(skolemisation,[status(esa)],[f669_nnf]) ).
cnf(c669,plain,
~ c_Com_OWT(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom)),
inference(cnf_transformation,[status(esa)],[f669_sk]) ).
cnf(t29,plain,
c_Com_OWT(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom)) = false,
inference(equality_encoding,[status(esa)],[c669]) ).
cnf(t1542,plain,
c_Com_OWT(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom)) = false,
inference(orient,[status(thm)],[t29]) ).
cnf(f638,axiom,
c_Option_Othe(c_Option_Ooption_OSome(V_x,T_a),T_a) = V_x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_the_Osimps_0) ).
fof(f638_nnf,plain,
! [V_x,T_a] : c_Option_Othe(c_Option_Ooption_OSome(V_x,T_a),T_a) = V_x,
inference(nnf_transformation,[status(thm)],[f638]) ).
fof(f638_sk,plain,
! [V_x,T_a] : c_Option_Othe(c_Option_Ooption_OSome(V_x,T_a),T_a) = V_x,
inference(skolemisation,[status(esa)],[f638_nnf]) ).
cnf(c638,plain,
c_Option_Othe(c_Option_Ooption_OSome(X0,X1),X1) = X0,
inference(cnf_transformation,[status(esa)],[f638_sk]) ).
cnf(t22,plain,
c_Option_Othe(c_Option_Ooption_OSome(X1,X2),X2) = X1,
inference(equality_encoding,[status(esa)],[c638]) ).
cnf(t283,plain,
c_Option_Othe(c_Option_Ooption_OSome(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t22]) ).
cnf(t1866,plain,
c_Map_Osko__Map__XdomD__1__1(v_pn,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom) = c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom),
inference(cp,[status(thm)],[t283,t1861]) ).
cnf(t1908,plain,
c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom) = c_Map_Osko__Map__XdomD__1__1(v_pn,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),
inference(orient,[status(thm)],[t1866]) ).
cnf(t10090,plain,
c_Com_OWT(c_Map_Osko__Map__XdomD__1__1(v_pn,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom)) = false,
inference(step,[status(thm)],[t1542,t1908]) ).
cnf(t1914,plain,
c_Com_OWT(c_Map_Osko__Map__XdomD__1__1(v_pn,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom)) = false,
inference(rw,[status(thm)],[t10090]) ).
cnf(t1894,plain,
c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn) = c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom),
inference(cp,[status(thm)],[t283,t1891]) ).
cnf(t10091,plain,
c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn) = c_Map_Osko__Map__XdomD__1__1(v_pn,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),
inference(step,[status(thm)],[t1894,t1908]) ).
cnf(t1915,plain,
c_Map_Osko__Map__XdomD__1__1(v_pn,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom) = c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),
inference(orient,[status(thm)],[t10091]) ).
cnf(t10098,plain,
c_Com_OWT(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn)) = false,
inference(step,[status(thm)],[t1914,t1915]) ).
cnf(t1955,plain,
c_Com_OWT(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn)) = false,
inference(orient,[status(thm)],[t10098]) ).
cnf(t10492,plain,
true = ifeq(hAPP(c_Com_Obody,X1),hAPP(c_Com_Obody,v_pn),false,true),
inference(step,[status(thm)],[t9538,t1955]) ).
cnf(t9934,plain,
ifeq(hAPP(c_Com_Obody,X1),hAPP(c_Com_Obody,v_pn),false,true) = true,
inference(orient,[status(thm)],[t10492]) ).
cnf(t9935,plain,
true = false,
inference(cp,[status(thm)],[t9934,t256]) ).
cnf(t9936,plain,
false = true,
inference(orient,[status(thm)],[t9935]) ).
cnf(f177,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f177_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f177]) ).
fof(f177_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f177_nnf]) ).
cnf(c177,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f177_sk]) ).
cnf(f179,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f179_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f179]) ).
fof(f179_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f179_nnf]) ).
cnf(c179,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f179_sk]) ).
cnf(f181,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f181_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f181]) ).
fof(f181_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f181_nnf]) ).
cnf(c181,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f181_sk]) ).
cnf(f183,axiom,
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__fun__def_1) ).
fof(f183_nnf,plain,
! [T_b,V_g,V_f,T_a] :
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
inference(nnf_transformation,[status(thm)],[f183]) ).
fof(f183_sk,plain,
! [T_b,V_g,V_f,T_a] :
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
inference(skolemisation,[status(esa)],[f183_nnf]) ).
cnf(c183,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,tc_fun(X3,X0))
| ~ c_lessequals(X1,X2,tc_fun(X3,X0))
| ~ class_HOL_Oord(X0) ),
inference(cnf_transformation,[status(esa)],[f183_sk]) ).
cnf(f184,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f184_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c184,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
cnf(f273,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(f273_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)],[f273]) ).
fof(f273_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)],[f273_nnf]) ).
cnf(c273,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
cnf(f274,axiom,
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(f274_nnf,plain,
! [V_pname_H,V_fun,V_com] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f274]) ).
fof(f274_sk,plain,
! [V_pname_H,V_fun,V_com] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(skolemisation,[status(esa)],[f274_nnf]) ).
cnf(c274,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OWhile(X1,X2),
inference(cnf_transformation,[status(esa)],[f274_sk]) ).
cnf(f276,axiom,
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(f276_nnf,plain,
! [V_pname_H,V_loc,V_fun,V_com] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f276]) ).
fof(f276_sk,plain,
! [V_pname_H,V_loc,V_fun,V_com] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f276_nnf]) ).
cnf(c276,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OLocal(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f276_sk]) ).
cnf(f279,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(f279_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)],[f279]) ).
fof(f279_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)],[f279_nnf]) ).
cnf(c279,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f279_sk]) ).
cnf(f284,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I30_J_0) ).
fof(f284_nnf,plain,
! [V_vname,V_fun,V_pname_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f284]) ).
fof(f284_sk,plain,
! [V_vname,V_fun,V_pname_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f284_nnf]) ).
cnf(c284,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f284_sk]) ).
cnf(f287,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(f287_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)],[f287]) ).
fof(f287_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)],[f287_nnf]) ).
cnf(c287,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f287_sk]) ).
cnf(f290,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(f290_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)],[f290]) ).
fof(f290_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)],[f290_nnf]) ).
cnf(c290,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f290_sk]) ).
cnf(f293,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(f293_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)],[f293]) ).
fof(f293_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)],[f293_nnf]) ).
cnf(c293,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f293_sk]) ).
cnf(f294,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(f294_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)],[f294]) ).
fof(f294_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)],[f294_nnf]) ).
cnf(c294,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f294_sk]) ).
cnf(f302,axiom,
c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I23_J_0) ).
fof(f302_nnf,plain,
! [V_loc_H,V_fun_H,V_com_H,V_vname,V_fun] : c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f302]) ).
fof(f302_sk,plain,
! [V_loc_H,V_fun_H,V_com_H,V_vname,V_fun] : c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f302_nnf]) ).
cnf(c302,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f302_sk]) ).
cnf(f305,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I31_J_0) ).
fof(f305_nnf,plain,
! [V_pname_H,V_vname,V_fun] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f305]) ).
fof(f305_sk,plain,
! [V_pname_H,V_vname,V_fun] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f305_nnf]) ).
cnf(c305,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OAss(X1,X2),
inference(cnf_transformation,[status(esa)],[f305_sk]) ).
cnf(f306,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(f306_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)],[f306]) ).
fof(f306_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)],[f306_nnf]) ).
cnf(c306,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f306_sk]) ).
cnf(f307,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(f307_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)],[f307]) ).
fof(f307_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)],[f307_nnf]) ).
cnf(c307,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OLocal(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f307_sk]) ).
cnf(f315,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(f315_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)],[f315]) ).
fof(f315_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)],[f315_nnf]) ).
cnf(c315,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f315_sk]) ).
cnf(f323,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(f323_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)],[f323]) ).
fof(f323_sk,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f323_nnf]) ).
cnf(c323,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f323_sk]) ).
cnf(f327,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I28_J_0) ).
fof(f327_nnf,plain,
! [V_vname,V_fun,V_fun_H,V_com_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f327]) ).
fof(f327_sk,plain,
! [V_vname,V_fun,V_fun_H,V_com_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f327_nnf]) ).
cnf(c327,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f327_sk]) ).
cnf(f329,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I22_J_0) ).
fof(f329_nnf,plain,
! [V_vname,V_fun,V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f329]) ).
fof(f329_sk,plain,
! [V_vname,V_fun,V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f329_nnf]) ).
cnf(c329,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f329_sk]) ).
cnf(f330,axiom,
~ c_HOL_Oord__class_Oless(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__psubset__empty_0) ).
fof(f330_nnf,plain,
! [V_A,T_a] : ~ c_HOL_Oord__class_Oless(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f330]) ).
fof(f330_sk,plain,
! [V_A,T_a] : ~ c_HOL_Oord__class_Oless(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f330_nnf]) ).
cnf(c330,plain,
~ c_HOL_Oord__class_Oless(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f330_sk]) ).
cnf(f331,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I54_J_0) ).
fof(f331_nnf,plain,
! [V_fun,V_com1,V_com2,V_pname_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f331]) ).
fof(f331_sk,plain,
! [V_fun,V_com1,V_com2,V_pname_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f331_nnf]) ).
cnf(c331,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OBODY(X3),
inference(cnf_transformation,[status(esa)],[f331_sk]) ).
cnf(f332,axiom,
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(f332_nnf,plain,
! [V_pname_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f332]) ).
fof(f332_sk,plain,
! [V_pname_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(skolemisation,[status(esa)],[f332_nnf]) ).
cnf(c332,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OCond(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f332_sk]) ).
cnf(f339,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(f339_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)],[f339]) ).
fof(f339_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)],[f339_nnf]) ).
cnf(c339,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f339_sk]) ).
cnf(f367,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I24_J_0) ).
fof(f367_nnf,plain,
! [V_vname,V_fun,V_com1_H,V_com2_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f367]) ).
fof(f367_sk,plain,
! [V_vname,V_fun,V_com1_H,V_com2_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f367_nnf]) ).
cnf(c367,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f367_sk]) ).
cnf(f369,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(f369_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)],[f369]) ).
fof(f369_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)],[f369_nnf]) ).
cnf(c369,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OCond(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f369_sk]) ).
cnf(f372,axiom,
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(f372_nnf,plain,
! [V_pname_H,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f372]) ).
fof(f372_sk,plain,
! [V_pname_H,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f372_nnf]) ).
cnf(c372,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSemi(X1,X2),
inference(cnf_transformation,[status(esa)],[f372_sk]) ).
cnf(f383,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I48_J_0) ).
fof(f383_nnf,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f383]) ).
fof(f383_sk,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f383_nnf]) ).
cnf(c383,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f383_sk]) ).
cnf(f385,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(f385_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)],[f385]) ).
fof(f385_sk,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(skolemisation,[status(esa)],[f385_nnf]) ).
cnf(c385,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f385_sk]) ).
cnf(f386,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(f386_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)],[f386]) ).
fof(f386_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)],[f386_nnf]) ).
cnf(c386,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f386_sk]) ).
cnf(f402,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(f402_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)],[f402]) ).
fof(f402_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)],[f402_nnf]) ).
cnf(c402,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f402_sk]) ).
cnf(f411,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I40_J_0) ).
fof(f411_nnf,plain,
! [V_loc,V_fun,V_com,V_pname_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f411]) ).
fof(f411_sk,plain,
! [V_loc,V_fun,V_com,V_pname_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f411_nnf]) ).
cnf(c411,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OBODY(X3),
inference(cnf_transformation,[status(esa)],[f411_sk]) ).
cnf(f416,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(f416_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)],[f416]) ).
fof(f416_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)],[f416_nnf]) ).
cnf(c416,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f416_sk]) ).
cnf(f421,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(f421_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)],[f421]) ).
fof(f421_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)],[f421_nnf]) ).
cnf(c421,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f421_sk]) ).
cnf(f423,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(f423_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)],[f423]) ).
fof(f423_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)],[f423_nnf]) ).
cnf(c423,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f423_sk]) ).
cnf(f429,axiom,
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(hAPP(hAPP(c_in(T_b),hAPP(V_f,V_a)),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f429_nnf,plain,
! [T_b,V_f,V_a,V_A,T_a] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(hAPP(hAPP(c_in(T_b),hAPP(V_f,V_a)),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b))) ),
inference(nnf_transformation,[status(thm)],[f429]) ).
fof(f429_sk,plain,
! [T_b,V_f,V_a,V_A,T_a] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(hAPP(hAPP(c_in(T_b),hAPP(V_f,V_a)),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b))) ),
inference(skolemisation,[status(esa)],[f429_nnf]) ).
cnf(c429,plain,
( ~ c_Fun_Oinj__on(X1,c_Set_Oinsert(X2,X3,X4),X4,X0)
| ~ hBOOL(hAPP(hAPP(c_in(X0),hAPP(X1,X2)),c_Set_Oimage(X1,c_HOL_Ominus__class_Ominus(X3,c_Set_Oinsert(X2,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_bool)),X4),tc_fun(X4,tc_bool)),X4,X0))) ),
inference(cnf_transformation,[status(esa)],[f429_sk]) ).
cnf(f430,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I27_J_0) ).
fof(f430_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_vname,V_fun] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f430]) ).
fof(f430_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_vname,V_fun] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f430_nnf]) ).
cnf(c430,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f430_sk]) ).
cnf(f431,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I18_J_0) ).
fof(f431_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f431]) ).
fof(f431_sk,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f431_nnf]) ).
cnf(c431,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(X0),
inference(cnf_transformation,[status(esa)],[f431_sk]) ).
cnf(f454,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f454_nnf,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(nnf_transformation,[status(thm)],[f454]) ).
fof(f454_sk,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(skolemisation,[status(esa)],[f454_nnf]) ).
cnf(c454,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f454_sk]) ).
cnf(f456,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f456_nnf,plain,
! [T_a,V_c] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(nnf_transformation,[status(thm)],[f456]) ).
fof(f456_sk,plain,
! [T_a,V_c] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(skolemisation,[status(esa)],[f456_nnf]) ).
cnf(c456,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f456_sk]) ).
cnf(f457,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f457_nnf,plain,
! [T_a,V_a] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(nnf_transformation,[status(thm)],[f457]) ).
fof(f457_sk,plain,
! [T_a,V_a] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(skolemisation,[status(esa)],[f457_nnf]) ).
cnf(c457,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f457_sk]) ).
cnf(f461,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f461_nnf,plain,
! [T_a,V_c,V_B,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
inference(nnf_transformation,[status(thm)],[f461]) ).
fof(f461_sk,plain,
! [T_a,V_c,V_B,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
inference(skolemisation,[status(esa)],[f461_nnf]) ).
cnf(c461,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_HOL_Ominus__class_Ominus(X3,X2,tc_fun(X0,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f461_sk]) ).
cnf(f467,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I26_J_0) ).
fof(f467_nnf,plain,
! [V_vname,V_fun,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f467]) ).
fof(f467_sk,plain,
! [V_vname,V_fun,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f467_nnf]) ).
cnf(c467,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f467_sk]) ).
cnf(f469,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(f469_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)],[f469]) ).
fof(f469_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)],[f469_nnf]) ).
cnf(c469,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(X0,X1),
inference(cnf_transformation,[status(esa)],[f469_sk]) ).
cnf(f472,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(f472_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)],[f472]) ).
fof(f472_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)],[f472_nnf]) ).
cnf(c472,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f472_sk]) ).
cnf(f477,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(f477_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)],[f477]) ).
fof(f477_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)],[f477_nnf]) ).
cnf(c477,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f477_sk]) ).
cnf(f478,axiom,
( c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_A))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f478_nnf,plain,
! [T_a,V_x,V_B,V_A] :
( c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_A))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_B)) ),
inference(nnf_transformation,[status(thm)],[f478]) ).
fof(f478_sk,plain,
! [T_a,V_x,V_B,V_A] :
( c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_A))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_B)) ),
inference(skolemisation,[status(esa)],[f478_nnf]) ).
cnf(c478,plain,
( c_Lattices_Olower__semilattice__class_Oinf(X3,X2,tc_fun(X0,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X3))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f478_sk]) ).
cnf(f480,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_psubset__eq_1) ).
fof(f480_nnf,plain,
! [V_x,T_a] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f480]) ).
fof(f480_sk,plain,
! [V_x,T_a] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f480_nnf]) ).
cnf(c480,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f480_sk]) ).
cnf(f481,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f481_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f481]) ).
fof(f481_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f481_nnf]) ).
cnf(c481,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f481_sk]) ).
cnf(f482,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f482_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f482]) ).
fof(f482_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f482_nnf]) ).
cnf(c482,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f482_sk]) ).
cnf(f483,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f483_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f483]) ).
fof(f483_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f483_nnf]) ).
cnf(c483,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f483_sk]) ).
cnf(f484,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(f484_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)],[f484]) ).
fof(f484_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)],[f484_nnf]) ).
cnf(c484,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f484_sk]) ).
cnf(f486,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I25_J_0) ).
fof(f486_nnf,plain,
! [V_com1_H,V_com2_H,V_vname,V_fun] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f486]) ).
fof(f486_sk,plain,
! [V_com1_H,V_com2_H,V_vname,V_fun] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f486_nnf]) ).
cnf(c486,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OAss(X2,X3),
inference(cnf_transformation,[status(esa)],[f486_sk]) ).
cnf(f494,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(f494_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)],[f494]) ).
fof(f494_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)],[f494_nnf]) ).
cnf(c494,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f494_sk]) ).
cnf(f505,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(V_vname_H,V_fun_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I8_J_0) ).
fof(f505_nnf,plain,
! [V_vname_H,V_fun_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(V_vname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f505]) ).
fof(f505_sk,plain,
! [V_vname_H,V_fun_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(V_vname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f505_nnf]) ).
cnf(c505,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(X0,X1),
inference(cnf_transformation,[status(esa)],[f505_sk]) ).
cnf(f508,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I29_J_0) ).
fof(f508_nnf,plain,
! [V_fun_H,V_com_H,V_vname,V_fun] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f508]) ).
fof(f508_sk,plain,
! [V_fun_H,V_com_H,V_vname,V_fun] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f508_nnf]) ).
cnf(c508,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OAss(X2,X3),
inference(cnf_transformation,[status(esa)],[f508_sk]) ).
cnf(f510,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(f510_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)],[f510]) ).
fof(f510_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)],[f510_nnf]) ).
cnf(c510,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f510_sk]) ).
cnf(f520,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(f520_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)],[f520]) ).
fof(f520_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)],[f520_nnf]) ).
cnf(c520,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f520_sk]) ).
cnf(f521,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(f521_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)],[f521]) ).
fof(f521_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)],[f521_nnf]) ).
cnf(c521,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f521_sk]) ).
cnf(f531,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(f531_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)],[f531]) ).
fof(f531_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)],[f531_nnf]) ).
cnf(c531,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f531_sk]) ).
cnf(f544,axiom,
c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I58_J_0) ).
fof(f544_nnf,plain,
! [V_fun,V_com,V_pname_H] : c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f544]) ).
fof(f544_sk,plain,
! [V_fun,V_com,V_pname_H] : c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f544_nnf]) ).
cnf(c544,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f544_sk]) ).
cnf(f546,axiom,
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(f546_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f546]) ).
fof(f546_sk,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f546_nnf]) ).
cnf(c546,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f546_sk]) ).
cnf(f554,axiom,
c_Com_Ocom_OAss(V_vname_H,V_fun_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I9_J_0) ).
fof(f554_nnf,plain,
! [V_vname_H,V_fun_H] : c_Com_Ocom_OAss(V_vname_H,V_fun_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f554]) ).
fof(f554_sk,plain,
! [V_vname_H,V_fun_H] : c_Com_Ocom_OAss(V_vname_H,V_fun_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f554_nnf]) ).
cnf(c554,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f554_sk]) ).
cnf(f560,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(f560_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)],[f560]) ).
fof(f560_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)],[f560_nnf]) ).
cnf(c560,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f560_sk]) ).
cnf(f561,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f561_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f561]) ).
fof(f561_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f561_nnf]) ).
cnf(c561,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f561_sk]) ).
cnf(f562,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f562_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f562]) ).
fof(f562_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f562_nnf]) ).
cnf(c562,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f562_sk]) ).
cnf(f563,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f563_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f563]) ).
fof(f563_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f563_nnf]) ).
cnf(c563,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f563_sk]) ).
cnf(f564,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f564_nnf,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f564]) ).
fof(f564_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f564_nnf]) ).
cnf(c564,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f564_sk]) ).
cnf(f588,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f588_nnf,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(nnf_transformation,[status(thm)],[f588]) ).
fof(f588_sk,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(skolemisation,[status(esa)],[f588_nnf]) ).
cnf(c588,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f588_sk]) ).
cnf(f652,axiom,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t) != V_t ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_single__stateE_0) ).
fof(f652_nnf,plain,
! [V_t] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t) != V_t ),
inference(nnf_transformation,[status(thm)],[f652]) ).
fof(f652_sk,plain,
! [V_t] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t) != V_t ),
inference(skolemisation,[status(esa)],[f652_nnf]) ).
cnf(c652,plain,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X0) != X0 ),
inference(cnf_transformation,[status(esa)],[f652_sk]) ).
cnf(f656,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Map_Odom(V_m,T_a,T_b)))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_domIff_0) ).
fof(f656_nnf,plain,
! [V_m,V_a,T_b,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Map_Odom(V_m,T_a,T_b)))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
inference(nnf_transformation,[status(thm)],[f656]) ).
fof(f656_sk,plain,
! [V_m,V_a,T_b,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Map_Odom(V_m,T_a,T_b)))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
inference(skolemisation,[status(esa)],[f656_nnf]) ).
cnf(c656,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X3),X1),c_Map_Odom(X0,X3,X2)))
| hAPP(X0,X1) != c_Option_Ooption_ONone(X2) ),
inference(cnf_transformation,[status(esa)],[f656_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c177,c179,c181,c183,c184,c273,c274,c276,c279,c284,c287,c290,c293,c294,c302,c305,c306,c307,c315,c322,c323,c327,c329,c330,c331,c332,c339,c367,c369,c372,c383,c385,c386,c402,c411,c416,c421,c423,c429,c430,c431,c454,c456,c457,c461,c467,c469,c472,c477,c478,c480,c481,c482,c483,c484,c486,c494,c505,c508,c510,c520,c521,c531,c544,c546,c554,c560,c561,c562,c563,c564,c588,c652,c656,c669]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t9936]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV892-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/10.45 % Computer : n013.cluster.edu
% 0.16/10.45 % Model : x86_64 x86_64
% 0.16/10.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/10.45 % Memory : 8046.5625MB
% 0.16/10.45 % OS : Linux 6.8.0-71-generic
% 0.16/10.46 % CPULimit : 300
% 0.16/10.46 % WCLimit : 300
% 0.16/10.46 % DateTime : Thu Sep 24 21:14:36 UTC 2026
% 0.16/10.46 % CPUTime :
% 0.16/10.46 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 90.57/22.05 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 90.57/22.05 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------