%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV889-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 : n014.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 16.05s 2.47s
% Output : Proof 16.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 65
% Syntax : Number of formulae : 270 ( 178 unt; 0 def)
% Number of atoms : 418 ( 170 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 546 ( 398 ~; 148 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 2 prp; 0-4 aty)
% Number of functors : 26 ( 26 usr; 7 con; 0-4 aty)
% Number of variables : 840 ( 268 sgn 414 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f600,axiom,
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_asm_0) ).
fof(f600_nnf,plain,
! [V_G,V_ts,T_a] :
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
inference(nnf_transformation,[status(thm)],[f600]) ).
fof(f600_sk,plain,
! [V_G,V_ts,T_a] :
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
inference(skolemisation,[status(esa)],[f600_nnf]) ).
cnf(c600,plain,
( ~ c_lessequals(X1,X0,tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f600_sk]) ).
cnf(t142,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),true,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c600]) ).
cnf(t304,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),true,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),true) = true,
inference(orient,[status(thm)],[t142]) ).
cnf(f606,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,tc_Com_Ostate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f606_nnf,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,tc_Com_Ostate),
inference(nnf_transformation,[status(thm)],[f606]) ).
fof(f606_sk,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,tc_Com_Ostate),
inference(skolemisation,[status(esa)],[f606_nnf]) ).
cnf(c606,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,tc_Com_Ostate),
inference(cnf_transformation,[status(esa)],[f606_sk]) ).
cnf(t10,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,tc_Com_Ostate) = false,
inference(equality_encoding,[status(esa)],[c606]) ).
cnf(t1492,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,tc_Com_Ostate) = false,
inference(orient,[status(thm)],[t10]) ).
cnf(t1498,plain,
true = ifeq(c_lessequals(v_ts,v_G,tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),true,false,true),
inference(cp,[status(thm)],[t304,t1492]) ).
cnf(f605,negated_conjecture,
c_lessequals(v_ts,v_G,tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f605_nnf,plain,
c_lessequals(v_ts,v_G,tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),
inference(nnf_transformation,[status(thm)],[f605]) ).
cnf(c605,plain,
c_lessequals(v_ts,v_G,tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),
inference(cnf_transformation,[status(esa)],[f605_nnf]) ).
cnf(t32,plain,
c_lessequals(v_ts,v_G,tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c605]) ).
cnf(t829,plain,
c_lessequals(v_ts,v_G,tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) = true,
inference(orient,[status(thm)],[t32]) ).
cnf(t2106,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t1498,t829]) ).
cnf(t17,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t232,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t17]) ).
cnf(t2107,plain,
true = false,
inference(step,[status(thm)],[t2106,t232]) ).
cnf(t1989,plain,
false = true,
inference(orient,[status(thm)],[t2107]) ).
cnf(f46,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(f46_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)],[f46]) ).
fof(f46_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)],[f46_nnf]) ).
cnf(c46,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OCond(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(f48,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(f48_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)],[f48]) ).
fof(f48_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)],[f48_nnf]) ).
cnf(c48,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(f53,axiom,
( ~ c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f53_nnf,plain,
! [V_c,V_A,T_a] :
( ~ c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
! [V_c,V_A,T_a] :
( ~ c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c53,plain,
( ~ c_in(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_fun(X2,tc_bool)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(f55,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(f55_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)],[f55]) ).
fof(f55_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)],[f55_nnf]) ).
cnf(c55,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(f63,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(f63_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)],[f63]) ).
fof(f63_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)],[f63_nnf]) ).
cnf(c63,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
cnf(f73,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(f73_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)],[f73]) ).
fof(f73_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)],[f73_nnf]) ).
cnf(c73,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
cnf(f83,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(f83_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)],[f83]) ).
fof(f83_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)],[f83_nnf]) ).
cnf(c83,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(f86,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(f86_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)],[f86]) ).
fof(f86_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)],[f86_nnf]) ).
cnf(c86,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f86_sk]) ).
cnf(f87,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(f87_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)],[f87]) ).
fof(f87_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)],[f87_nnf]) ).
cnf(c87,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f87_sk]) ).
cnf(f92,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(f92_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)],[f92]) ).
fof(f92_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)],[f92_nnf]) ).
cnf(c92,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(f95,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(f95_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)],[f95]) ).
fof(f95_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)],[f95_nnf]) ).
cnf(c95,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(f98,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(f98_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)],[f98]) ).
fof(f98_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)],[f98_nnf]) ).
cnf(c98,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OLocal(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(f99,axiom,
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f99_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f99]) ).
fof(f99_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f99_nnf]) ).
cnf(c99,plain,
( ~ c_in(X0,c_HOL_Ominus__class_Ominus(X3,X1,tc_fun(X2,tc_bool)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f99_sk]) ).
cnf(f118,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(f118_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)],[f118]) ).
fof(f118_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)],[f118_nnf]) ).
cnf(c118,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f118_sk]) ).
cnf(f127,axiom,
( ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f127_nnf,plain,
! [V_P,V_x,T_a] :
( ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(nnf_transformation,[status(thm)],[f127]) ).
fof(f127_sk,plain,
! [V_P,V_x,T_a] :
( ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(skolemisation,[status(esa)],[f127_nnf]) ).
cnf(c127,plain,
( ~ c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
cnf(f155,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(f155_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)],[f155]) ).
fof(f155_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)],[f155_nnf]) ).
cnf(c155,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f155_sk]) ).
cnf(f173,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff2_0) ).
fof(f173_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f173]) ).
fof(f173_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f173_nnf]) ).
cnf(c173,plain,
( ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f173_sk]) ).
cnf(f185,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(f185_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)],[f185]) ).
fof(f185_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)],[f185_nnf]) ).
cnf(c185,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f185_sk]) ).
cnf(f187,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(f187_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)],[f187]) ).
fof(f187_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)],[f187_nnf]) ).
cnf(c187,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f187_sk]) ).
cnf(f191,axiom,
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f191_nnf,plain,
! [V_f,V_a,V_A,T_a,T_b] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b) ),
inference(nnf_transformation,[status(thm)],[f191]) ).
fof(f191_sk,plain,
! [V_f,V_a,V_A,T_a,T_b] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b) ),
inference(skolemisation,[status(esa)],[f191_nnf]) ).
cnf(c191,plain,
( ~ c_Fun_Oinj__on(X0,c_Set_Oinsert(X1,X2,X3),X3,X4)
| ~ c_in(hAPP(X0,X1),c_Set_Oimage(X0,c_HOL_Ominus__class_Ominus(X2,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3),tc_fun(X3,tc_bool)),X3,X4),X4) ),
inference(cnf_transformation,[status(esa)],[f191_sk]) ).
cnf(f192,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(f192_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)],[f192]) ).
fof(f192_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)],[f192_nnf]) ).
cnf(c192,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f192_sk]) ).
cnf(f209,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(f209_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)],[f209]) ).
fof(f209_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)],[f209_nnf]) ).
cnf(c209,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
cnf(f226,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(f226_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)],[f226]) ).
fof(f226_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)],[f226_nnf]) ).
cnf(c226,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f226_sk]) ).
cnf(f227,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(f227_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)],[f227]) ).
fof(f227_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)],[f227_nnf]) ).
cnf(c227,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f227_sk]) ).
cnf(f228,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(f228_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)],[f228]) ).
fof(f228_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)],[f228_nnf]) ).
cnf(c228,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)],[f228_sk]) ).
cnf(f241,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(f241_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)],[f241]) ).
fof(f241_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)],[f241_nnf]) ).
cnf(c241,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f241_sk]) ).
cnf(f258,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(f258_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)],[f258]) ).
fof(f258_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)],[f258_nnf]) ).
cnf(c258,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f258_sk]) ).
cnf(f260,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(f260_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)],[f260]) ).
fof(f260_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)],[f260_nnf]) ).
cnf(c260,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(X0,X1),
inference(cnf_transformation,[status(esa)],[f260_sk]) ).
cnf(f265,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(f265_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)],[f265]) ).
fof(f265_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)],[f265_nnf]) ).
cnf(c265,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f265_sk]) ).
cnf(f270,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(f270_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)],[f270]) ).
fof(f270_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)],[f270_nnf]) ).
cnf(c270,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f270_sk]) ).
cnf(f271,axiom,
c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_UNIV__not__empty_0) ).
fof(f271_nnf,plain,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f271]) ).
fof(f271_sk,plain,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f271_nnf]) ).
cnf(c271,plain,
c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
cnf(f272,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))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f272_nnf,plain,
! [V_x,V_B,T_a,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))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f272]) ).
fof(f272_sk,plain,
! [V_x,V_B,T_a,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))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f272_nnf]) ).
cnf(c272,plain,
( c_Lattices_Olower__semilattice__class_Oinf(X3,X1,tc_fun(X2,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| ~ c_in(X0,X3,X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f272_sk]) ).
cnf(f283,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(f283_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)],[f283]) ).
fof(f283_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)],[f283_nnf]) ).
cnf(c283,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f283_sk]) ).
cnf(f284,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(f284_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)],[f284]) ).
fof(f284_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)],[f284_nnf]) ).
cnf(c284,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f284_sk]) ).
cnf(f285,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(f285_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)],[f285]) ).
fof(f285_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)],[f285_nnf]) ).
cnf(c285,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f285_sk]) ).
cnf(f286,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(f286_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)],[f286]) ).
fof(f286_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)],[f286_nnf]) ).
cnf(c286,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
cnf(f297,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(f297_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)],[f297]) ).
fof(f297_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)],[f297_nnf]) ).
cnf(c297,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OAss(X2,X3),
inference(cnf_transformation,[status(esa)],[f297_sk]) ).
cnf(f368,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(f368_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)],[f368]) ).
fof(f368_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)],[f368_nnf]) ).
cnf(c368,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f368_sk]) ).
cnf(f370,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(f370_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)],[f370]) ).
fof(f370_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)],[f370_nnf]) ).
cnf(c370,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f370_sk]) ).
cnf(f372,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(f372_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)],[f372]) ).
fof(f372_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)],[f372_nnf]) ).
cnf(c372,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f372_sk]) ).
cnf(f374,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(f374_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)],[f374]) ).
fof(f374_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)],[f374_nnf]) ).
cnf(c374,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f374_sk]) ).
cnf(f397,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(f397_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)],[f397]) ).
fof(f397_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)],[f397_nnf]) ).
cnf(c397,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)],[f397_sk]) ).
cnf(f403,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(f403_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)],[f403]) ).
fof(f403_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)],[f403_nnf]) ).
cnf(c403,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f403_sk]) ).
cnf(f416,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(f416_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)],[f416]) ).
fof(f416_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)],[f416_nnf]) ).
cnf(c416,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(X0,X1),
inference(cnf_transformation,[status(esa)],[f416_sk]) ).
cnf(f419,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(f419_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)],[f419]) ).
fof(f419_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)],[f419_nnf]) ).
cnf(c419,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OAss(X2,X3),
inference(cnf_transformation,[status(esa)],[f419_sk]) ).
cnf(f421,axiom,
( ~ c_lessequals(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff2_0) ).
fof(f421_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f421]) ).
fof(f421_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f421_nnf]) ).
cnf(c421,plain,
( ~ c_lessequals(X1,X2,X0)
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f421_sk]) ).
cnf(f422,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(f422_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)],[f422]) ).
fof(f422_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)],[f422_nnf]) ).
cnf(c422,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f422_sk]) ).
cnf(f423,axiom,
~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f423_nnf,plain,
! [V_a,T_a] : ~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f423]) ).
fof(f423_sk,plain,
! [V_a,T_a] : ~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f423_nnf]) ).
cnf(c423,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f423_sk]) ).
cnf(f424,axiom,
~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f424_nnf,plain,
! [V_c,T_a] : ~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f424]) ).
fof(f424_sk,plain,
! [V_c,T_a] : ~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f424_nnf]) ).
cnf(c424,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f424_sk]) ).
cnf(f426,axiom,
~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f426_nnf,plain,
! [V_x,T_a] : ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f426]) ).
fof(f426_sk,plain,
! [V_x,T_a] : ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f426_nnf]) ).
cnf(c426,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f426_sk]) ).
cnf(f434,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(f434_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)],[f434]) ).
fof(f434_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)],[f434_nnf]) ).
cnf(c434,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f434_sk]) ).
cnf(f452,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(f452_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)],[f452]) ).
fof(f452_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)],[f452_nnf]) ).
cnf(c452,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f452_sk]) ).
cnf(f460,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff_0) ).
fof(f460_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f460]) ).
fof(f460_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f460_nnf]) ).
cnf(c460,plain,
( ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,X0) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f460_sk]) ).
cnf(f467,axiom,
( ~ c_lessequals(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff_0) ).
fof(f467_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f467]) ).
fof(f467_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f467_nnf]) ).
cnf(c467,plain,
( ~ c_lessequals(X1,X2,X0)
| c_SetInterval_Oord__class_OatLeastAtMost(X1,X2,X0) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f467_sk]) ).
cnf(f488,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(f488_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)],[f488]) ).
fof(f488_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)],[f488_nnf]) ).
cnf(c488,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f488_sk]) ).
cnf(f497,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(f497_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)],[f497]) ).
fof(f497_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)],[f497_nnf]) ).
cnf(c497,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f497_sk]) ).
cnf(f498,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(f498_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)],[f498]) ).
fof(f498_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)],[f498_nnf]) ).
cnf(c498,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)],[f498_sk]) ).
cnf(f499,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(f499_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)],[f499]) ).
fof(f499_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)],[f499_nnf]) ).
cnf(c499,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)],[f499_sk]) ).
cnf(f500,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(f500_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)],[f500]) ).
fof(f500_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)],[f500_nnf]) ).
cnf(c500,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)],[f500_sk]) ).
cnf(f501,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(f501_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)],[f501]) ).
fof(f501_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)],[f501_nnf]) ).
cnf(c501,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)],[f501_sk]) ).
cnf(f564,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(f564_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)],[f564]) ).
fof(f564_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)],[f564_nnf]) ).
cnf(c564,plain,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X0) != X0 ),
inference(cnf_transformation,[status(esa)],[f564_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c46,c48,c53,c55,c63,c73,c83,c86,c87,c92,c95,c98,c99,c118,c127,c155,c173,c185,c187,c191,c192,c209,c226,c227,c228,c241,c258,c260,c265,c270,c271,c272,c283,c284,c285,c286,c297,c368,c370,c372,c374,c397,c403,c416,c419,c421,c422,c423,c424,c426,c434,c452,c460,c467,c488,c497,c498,c499,c500,c501,c564,c606]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1989]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV889-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.34 % Computer : n014.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Thu Sep 24 21:14:49 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.09/0.34 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 16.05/2.47 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.05/2.47 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------