%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV900-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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:14:26 PM UTC 2026
% Result : Unsatisfiable 15.25s 2.47s
% Output : Proof 15.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 23
% Syntax : Number of formulae : 100 ( 68 unt; 0 def)
% Number of atoms : 144 ( 63 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 178 ( 134 ~; 44 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 2 prp; 0-3 aty)
% Number of functors : 28 ( 28 usr; 9 con; 0-5 aty)
% Number of variables : 212 ( 34 sgn 104 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f534,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Com_Ostate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f534_nnf,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Com_Ostate),
inference(nnf_transformation,[status(thm)],[f534]) ).
fof(f534_sk,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Com_Ostate),
inference(skolemisation,[status(esa)],[f534_nnf]) ).
cnf(c534,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Com_Ostate),
inference(cnf_transformation,[status(esa)],[f534_sk]) ).
cnf(t114,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Com_Ostate) = false,
inference(equality_encoding,[status(esa)],[c534]) ).
cnf(f520,axiom,
c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty_0) ).
fof(f520_nnf,plain,
! [V_G,T_a] : c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f520]) ).
fof(f520_sk,plain,
! [V_G,T_a] : c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f520_nnf]) ).
cnf(c520,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f520_sk]) ).
cnf(t23,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)),X2) = true,
inference(equality_encoding,[status(esa)],[c520]) ).
cnf(t243,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)),X2) = true,
inference(orient,[status(thm)],[t23]) ).
cnf(t3028,plain,
true = false,
inference(step,[status(thm)],[t114,t243]) ).
cnf(t2455,plain,
false = true,
inference(orient,[status(thm)],[t3028]) ).
cnf(f26,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(f26_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)],[f26]) ).
fof(f26_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)],[f26_nnf]) ).
cnf(c26,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(f27,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(f27_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)],[f27]) ).
fof(f27_sk,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(f162,axiom,
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f162_nnf,plain,
! [V_c,V_A,T_a] :
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
inference(nnf_transformation,[status(thm)],[f162]) ).
fof(f162_sk,plain,
! [V_c,V_A,T_a] :
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
inference(skolemisation,[status(esa)],[f162_nnf]) ).
cnf(c162,plain,
( ~ hBOOL(c_in(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f162_sk]) ).
cnf(f194,axiom,
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f194_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
inference(nnf_transformation,[status(thm)],[f194]) ).
fof(f194_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c194,plain,
( ~ hBOOL(c_in(X0,c_HOL_Ominus__class_Ominus(X3,X1,tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
cnf(f206,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(f206_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)],[f206]) ).
fof(f206_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)],[f206_nnf]) ).
cnf(c206,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f206_sk]) ).
cnf(f207,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(f207_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)],[f207]) ).
fof(f207_sk,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f207_nnf]) ).
cnf(c207,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f207_sk]) ).
cnf(f224,axiom,
( ~ hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_domIff_0) ).
fof(f224_nnf,plain,
! [V_m,V_a,T_b,T_a] :
( ~ hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
inference(nnf_transformation,[status(thm)],[f224]) ).
fof(f224_sk,plain,
! [V_m,V_a,T_b,T_a] :
( ~ hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
inference(skolemisation,[status(esa)],[f224_nnf]) ).
cnf(c224,plain,
( ~ hBOOL(c_in(X1,c_Map_Odom(X0,X3,X2),X3))
| hAPP(X0,X1) != c_Option_Ooption_ONone(X2) ),
inference(cnf_transformation,[status(esa)],[f224_sk]) ).
cnf(f255,axiom,
~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f255_nnf,plain,
! [V_x,T_a] : ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f255]) ).
fof(f255_sk,plain,
! [V_x,T_a] : ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f255_nnf]) ).
cnf(c255,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f255_sk]) ).
cnf(f257,axiom,
~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f257_nnf,plain,
! [V_c,T_a] : ~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f257]) ).
fof(f257_sk,plain,
! [V_c,T_a] : ~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f257_nnf]) ).
cnf(c257,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f257_sk]) ).
cnf(f258,axiom,
~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f258_nnf,plain,
! [V_a,T_a] : ~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f258]) ).
fof(f258_sk,plain,
! [V_a,T_a] : ~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f258_nnf]) ).
cnf(c258,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f258_sk]) ).
cnf(f259,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(f259_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)],[f259]) ).
fof(f259_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)],[f259_nnf]) ).
cnf(c259,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f259_sk]) ).
cnf(f264,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(f264_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)],[f264]) ).
fof(f264_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)],[f264_nnf]) ).
cnf(c264,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)],[f264_sk]) ).
cnf(f273,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(f273_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)],[f273]) ).
fof(f273_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)],[f273_nnf]) ).
cnf(c273,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
cnf(f276,axiom,
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f276_nnf,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(nnf_transformation,[status(thm)],[f276]) ).
fof(f276_sk,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(skolemisation,[status(esa)],[f276_nnf]) ).
cnf(c276,plain,
( ~ hBOOL(c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f276_sk]) ).
cnf(f342,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(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f342_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))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
inference(nnf_transformation,[status(thm)],[f342]) ).
fof(f342_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))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
inference(skolemisation,[status(esa)],[f342_nnf]) ).
cnf(c342,plain,
( c_Lattices_Olower__semilattice__class_Oinf(X3,X1,tc_fun(X2,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| ~ hBOOL(c_in(X0,X3,X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f342_sk]) ).
cnf(f397,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f397_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f397]) ).
fof(f397_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f397_nnf]) ).
cnf(c397,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f397_sk]) ).
cnf(f398,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f398_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f398]) ).
fof(f398_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f398_nnf]) ).
cnf(c398,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f398_sk]) ).
cnf(f438,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(f438_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)],[f438]) ).
fof(f438_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)],[f438_nnf]) ).
cnf(c438,plain,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X0) != X0 ),
inference(cnf_transformation,[status(esa)],[f438_sk]) ).
cnf(f445,axiom,
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| 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(f445_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| 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)],[f445]) ).
fof(f445_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| 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)],[f445_nnf]) ).
cnf(c445,plain,
( ~ hBOOL(hAPP(hAPP(c_lessequals(X0),X1),X2))
| 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)],[f445_sk]) ).
cnf(f447,axiom,
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| 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(f447_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| 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)],[f447]) ).
fof(f447_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| 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)],[f447_nnf]) ).
cnf(c447,plain,
( ~ hBOOL(hAPP(hAPP(c_lessequals(X0),X1),X2))
| 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)],[f447_sk]) ).
cnf(f519,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(f519_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)],[f519]) ).
fof(f519_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)],[f519_nnf]) ).
cnf(c519,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f519_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c26,c27,c162,c194,c206,c207,c224,c255,c257,c258,c259,c264,c273,c276,c342,c397,c398,c438,c445,c447,c519,c534]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2455]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV900-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.43 % Computer : n004.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Thu Sep 24 21:16:05 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 15.25/2.47 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.25/2.47 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------