%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV858-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n007.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:15 PM UTC 2026
% Result : Unsatisfiable 33.09s 5.07s
% Output : Proof 33.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 42
% Syntax : Number of formulae : 215 ( 107 unt; 0 def)
% Number of atoms : 387 ( 96 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 466 ( 294 ~; 172 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 9 con; 0-4 aty)
% Number of variables : 447 ( 53 sgn 194 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f554,negated_conjecture,
( ~ c_Hoare__Mirabelle_Otriple__valid(V_na,v_n(V_na),t_a)
| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_nc),v_ts_H))
| c_Hoare__Mirabelle_Otriple__valid(V_na,V_nc,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f554_nnf,plain,
! [V_na,V_nc] :
( ~ c_Hoare__Mirabelle_Otriple__valid(V_na,v_n(V_na),t_a)
| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_nc),v_ts_H))
| c_Hoare__Mirabelle_Otriple__valid(V_na,V_nc,t_a) ),
inference(nnf_transformation,[status(thm)],[f554]) ).
fof(f554_sk,plain,
! [V_na,V_nc] :
( ~ c_Hoare__Mirabelle_Otriple__valid(V_na,v_n(V_na),t_a)
| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_nc),v_ts_H))
| c_Hoare__Mirabelle_Otriple__valid(V_na,V_nc,t_a) ),
inference(skolemisation,[status(esa)],[f554_nnf]) ).
cnf(c554,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(X0,v_n(X0),t_a)
| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_ts_H))
| c_Hoare__Mirabelle_Otriple__valid(X0,X1,t_a) ),
inference(cnf_transformation,[status(esa)],[f554_sk]) ).
cnf(t123,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_ts_H)),true,ifeq(c_Hoare__Mirabelle_Otriple__valid(X2,v_n(X2),t_a),true,c_Hoare__Mirabelle_Otriple__valid(X2,X1,t_a),true),true) = true,
inference(equality_encoding,[status(esa)],[c554]) ).
cnf(t329,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_ts_H)),true,ifeq(c_Hoare__Mirabelle_Otriple__valid(X2,v_n(X2),t_a),true,c_Hoare__Mirabelle_Otriple__valid(X2,X1,t_a),true),true) = true,
inference(orient,[status(thm)],[t123]) ).
cnf(f544,axiom,
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f544_nnf,plain,
! [T_a,V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ),
inference(nnf_transformation,[status(thm)],[f544]) ).
fof(f544_sk,plain,
! [T_a,V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ),
inference(skolemisation,[status(esa)],[f544_nnf]) ).
cnf(c544,plain,
( ~ hBOOL(hAPP(X2,X1))
| hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f544_sk]) ).
cnf(t66,plain,
ifeq(hBOOL(hAPP(X1,X2)),true,hBOOL(hAPP(hAPP(c_in(X3),X2),X1)),true) = true,
inference(equality_encoding,[status(esa)],[c544]) ).
cnf(t275,plain,
ifeq(hBOOL(hAPP(X1,X2)),true,hBOOL(hAPP(hAPP(c_in(X3),X2),X1)),true) = true,
inference(orient,[status(thm)],[t66]) ).
cnf(f218,axiom,
( ~ hBOOL(hAPP(V_A,V_x))
| hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup1CI_1) ).
fof(f218_nnf,plain,
! [V_A,V_B,T_a,V_x] :
( ~ hBOOL(hAPP(V_A,V_x))
| hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ),
inference(nnf_transformation,[status(thm)],[f218]) ).
fof(f218_sk,plain,
! [V_A,V_B,T_a,V_x] :
( ~ hBOOL(hAPP(V_A,V_x))
| hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ),
inference(skolemisation,[status(esa)],[f218_nnf]) ).
cnf(c218,plain,
( ~ hBOOL(hAPP(X0,X3))
| hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),X3)) ),
inference(cnf_transformation,[status(esa)],[f218_sk]) ).
cnf(t84,plain,
ifeq(hBOOL(hAPP(X1,X2)),true,hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,X3,tc_fun(X4,tc_bool)),X2)),true) = true,
inference(equality_encoding,[status(esa)],[c218]) ).
cnf(t284,plain,
ifeq(hBOOL(hAPP(X1,X2)),true,hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,X3,tc_fun(X4,tc_bool)),X2)),true) = true,
inference(orient,[status(thm)],[t84]) ).
cnf(f545,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))
| hBOOL(hAPP(V_S,V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_0) ).
fof(f545_nnf,plain,
! [V_S,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))
| hBOOL(hAPP(V_S,V_x)) ),
inference(nnf_transformation,[status(thm)],[f545]) ).
fof(f545_sk,plain,
! [V_S,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))
| hBOOL(hAPP(V_S,V_x)) ),
inference(skolemisation,[status(esa)],[f545_nnf]) ).
cnf(c545,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X0))
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f545_sk]) ).
cnf(t68,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(X1),X2),X3)),true,hBOOL(hAPP(X3,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c545]) ).
cnf(t299,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(X1),X2),X3)),true,hBOOL(hAPP(X3,X2)),true) = true,
inference(orient,[status(thm)],[t68]) ).
cnf(f550,negated_conjecture,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f550_nnf,plain,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)),
inference(nnf_transformation,[status(thm)],[f550]) ).
cnf(c550,plain,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)),
inference(cnf_transformation,[status(esa)],[f550_nnf]) ).
cnf(t24,plain,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)) = true,
inference(equality_encoding,[status(esa)],[c550]) ).
cnf(t864,plain,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t876,plain,
true = ifeq(true,true,hBOOL(hAPP(v_tsa,v_xa)),true),
inference(cp,[status(thm)],[t299,t864]) ).
cnf(t12,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t172,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t8299,plain,
true = hBOOL(hAPP(v_tsa,v_xa)),
inference(step,[status(thm)],[t876,t172]) ).
cnf(t1905,plain,
hBOOL(hAPP(v_tsa,v_xa)) = true,
inference(orient,[status(thm)],[t8299]) ).
cnf(t1913,plain,
true = ifeq(true,true,hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(v_tsa,X1,tc_fun(X2,tc_bool)),v_xa)),true),
inference(cp,[status(thm)],[t284,t1905]) ).
cnf(t8348,plain,
true = hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(v_tsa,X1,tc_fun(X2,tc_bool)),v_xa)),
inference(step,[status(thm)],[t1913,t172]) ).
cnf(t2366,plain,
hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(v_tsa,X1,tc_fun(X2,tc_bool)),v_xa)) = true,
inference(orient,[status(thm)],[t8348]) ).
cnf(f347,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)) = V_B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Un__absorb1_0) ).
fof(f347_nnf,plain,
! [V_A,V_B,T_a] :
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)) = V_B ),
inference(nnf_transformation,[status(thm)],[f347]) ).
fof(f347_sk,plain,
! [V_A,V_B,T_a] :
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)) = V_B ),
inference(skolemisation,[status(esa)],[f347_nnf]) ).
cnf(c347,plain,
( ~ c_lessequals(X0,X1,tc_fun(X2,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)) = X1 ),
inference(cnf_transformation,[status(esa)],[f347_sk]) ).
cnf(t78,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),true,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),X2) = X2,
inference(equality_encoding,[status(esa)],[c347]) ).
cnf(t174,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),true,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),X2) = X2,
inference(orient,[status(thm)],[t78]) ).
cnf(f549,negated_conjecture,
c_lessequals(v_tsa,v_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f549_nnf,plain,
c_lessequals(v_tsa,v_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),
inference(nnf_transformation,[status(thm)],[f549]) ).
cnf(c549,plain,
c_lessequals(v_tsa,v_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),
inference(cnf_transformation,[status(esa)],[f549_nnf]) ).
cnf(t19,plain,
c_lessequals(v_tsa,v_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c549]) ).
cnf(t785,plain,
c_lessequals(v_tsa,v_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)) = true,
inference(orient,[status(thm)],[t19]) ).
cnf(t786,plain,
v_ts_H = ifeq(true,true,c_Lattices_Oupper__semilattice__class_Osup(v_tsa,v_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),v_ts_H),
inference(cp,[status(thm)],[t174,t785]) ).
cnf(t8311,plain,
v_ts_H = c_Lattices_Oupper__semilattice__class_Osup(v_tsa,v_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),
inference(step,[status(thm)],[t786,t172]) ).
cnf(t1976,plain,
c_Lattices_Oupper__semilattice__class_Osup(v_tsa,v_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)) = v_ts_H,
inference(orient,[status(thm)],[t8311]) ).
cnf(t2367,plain,
true = hBOOL(hAPP(v_ts_H,v_xa)),
inference(cp,[status(thm)],[t2366,t1976]) ).
cnf(t2378,plain,
hBOOL(hAPP(v_ts_H,v_xa)) = true,
inference(orient,[status(thm)],[t2367]) ).
cnf(t2385,plain,
true = ifeq(true,true,hBOOL(hAPP(hAPP(c_in(X1),v_xa),v_ts_H)),true),
inference(cp,[status(thm)],[t275,t2378]) ).
cnf(t8349,plain,
true = hBOOL(hAPP(hAPP(c_in(X1),v_xa),v_ts_H)),
inference(step,[status(thm)],[t2385,t172]) ).
cnf(t2388,plain,
hBOOL(hAPP(hAPP(c_in(X1),v_xa),v_ts_H)) = true,
inference(orient,[status(thm)],[t8349]) ).
cnf(t2406,plain,
true = ifeq(true,true,ifeq(c_Hoare__Mirabelle_Otriple__valid(X1,v_n(X1),t_a),true,c_Hoare__Mirabelle_Otriple__valid(X1,v_xa,t_a),true),true),
inference(cp,[status(thm)],[t329,t2388]) ).
cnf(t8470,plain,
true = ifeq(c_Hoare__Mirabelle_Otriple__valid(X1,v_n(X1),t_a),true,c_Hoare__Mirabelle_Otriple__valid(X1,v_xa,t_a),true),
inference(step,[status(thm)],[t2406,t172]) ).
cnf(t4447,plain,
ifeq(c_Hoare__Mirabelle_Otriple__valid(X1,v_n(X1),t_a),true,c_Hoare__Mirabelle_Otriple__valid(X1,v_xa,t_a),true) = true,
inference(orient,[status(thm)],[t8470]) ).
cnf(f552,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_xb),v_Ga))
| c_Hoare__Mirabelle_Otriple__valid(v_x,V_xb,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f552_nnf,plain,
! [V_xb] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_xb),v_Ga))
| c_Hoare__Mirabelle_Otriple__valid(v_x,V_xb,t_a) ),
inference(nnf_transformation,[status(thm)],[f552]) ).
fof(f552_sk,plain,
! [V_xb] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_xb),v_Ga))
| c_Hoare__Mirabelle_Otriple__valid(v_x,V_xb,t_a) ),
inference(skolemisation,[status(esa)],[f552_nnf]) ).
cnf(c552,plain,
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_Ga))
| c_Hoare__Mirabelle_Otriple__valid(v_x,X0,t_a) ),
inference(cnf_transformation,[status(esa)],[f552_sk]) ).
cnf(t80,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_Ga)),true,c_Hoare__Mirabelle_Otriple__valid(v_x,X1,t_a),true) = true,
inference(equality_encoding,[status(esa)],[c552]) ).
cnf(t331,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_Ga)),true,c_Hoare__Mirabelle_Otriple__valid(v_x,X1,t_a),true) = true,
inference(orient,[status(thm)],[t80]) ).
cnf(f553,negated_conjecture,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(V_na)),v_Ga))
| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_nb),v_ts_H))
| c_Hoare__Mirabelle_Otriple__valid(V_na,V_nb,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f553_nnf,plain,
! [V_na,V_nb] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(V_na)),v_Ga))
| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_nb),v_ts_H))
| c_Hoare__Mirabelle_Otriple__valid(V_na,V_nb,t_a) ),
inference(nnf_transformation,[status(thm)],[f553]) ).
fof(f553_sk,plain,
! [V_na,V_nb] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(V_na)),v_Ga))
| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_nb),v_ts_H))
| c_Hoare__Mirabelle_Otriple__valid(V_na,V_nb,t_a) ),
inference(skolemisation,[status(esa)],[f553_nnf]) ).
cnf(c553,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X0)),v_Ga))
| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_ts_H))
| c_Hoare__Mirabelle_Otriple__valid(X0,X1,t_a) ),
inference(cnf_transformation,[status(esa)],[f553_sk]) ).
cnf(t131,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_ts_H)),true,or(c_Hoare__Mirabelle_Otriple__valid(X2,X1,t_a),hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X2)),v_Ga))),true) = true,
inference(equality_encoding,[status(esa)],[c553]) ).
cnf(t330,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_ts_H)),true,or(c_Hoare__Mirabelle_Otriple__valid(X2,X1,t_a),hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X2)),v_Ga))),true) = true,
inference(orient,[status(thm)],[t131]) ).
cnf(t2421,plain,
true = ifeq(true,true,or(c_Hoare__Mirabelle_Otriple__valid(X1,v_xa,t_a),hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X1)),v_Ga))),true),
inference(cp,[status(thm)],[t330,t2388]) ).
cnf(t8571,plain,
true = or(c_Hoare__Mirabelle_Otriple__valid(X1,v_xa,t_a),hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X1)),v_Ga))),
inference(step,[status(thm)],[t2421,t172]) ).
cnf(t8207,plain,
or(c_Hoare__Mirabelle_Otriple__valid(X1,v_xa,t_a),hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X1)),v_Ga))) = true,
inference(orient,[status(thm)],[t8571]) ).
cnf(f551,negated_conjecture,
~ c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f551_nnf,plain,
~ c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),
inference(nnf_transformation,[status(thm)],[f551]) ).
fof(f551_sk,plain,
~ c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),
inference(skolemisation,[status(esa)],[f551_nnf]) ).
cnf(c551,plain,
~ c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),
inference(cnf_transformation,[status(esa)],[f551_sk]) ).
cnf(t9,plain,
c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a) = false,
inference(equality_encoding,[status(esa)],[c551]) ).
cnf(t1871,plain,
c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a) = false,
inference(orient,[status(thm)],[t9]) ).
cnf(t8208,plain,
true = or(false,hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(v_x)),v_Ga))),
inference(cp,[status(thm)],[t8207,t1871]) ).
cnf(t6,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t215,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t8572,plain,
true = hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(v_x)),v_Ga)),
inference(step,[status(thm)],[t8208,t215]) ).
cnf(t8209,plain,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(v_x)),v_Ga)) = true,
inference(orient,[status(thm)],[t8572]) ).
cnf(t8225,plain,
true = ifeq(true,true,c_Hoare__Mirabelle_Otriple__valid(v_x,v_n(v_x),t_a),true),
inference(cp,[status(thm)],[t331,t8209]) ).
cnf(t8574,plain,
true = c_Hoare__Mirabelle_Otriple__valid(v_x,v_n(v_x),t_a),
inference(step,[status(thm)],[t8225,t172]) ).
cnf(t8246,plain,
c_Hoare__Mirabelle_Otriple__valid(v_x,v_n(v_x),t_a) = true,
inference(orient,[status(thm)],[t8574]) ).
cnf(t8247,plain,
true = ifeq(true,true,c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),true),
inference(cp,[status(thm)],[t4447,t8246]) ).
cnf(t8577,plain,
true = c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),
inference(step,[status(thm)],[t8247,t172]) ).
cnf(t8578,plain,
true = false,
inference(step,[status(thm)],[t8577,t1871]) ).
cnf(t8251,plain,
false = true,
inference(orient,[status(thm)],[t8578]) ).
cnf(f60,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/sandbox2/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff2_0) ).
fof(f60_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)],[f60]) ).
fof(f60_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)],[f60_nnf]) ).
cnf(c60,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)],[f60_sk]) ).
cnf(f114,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f114_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)],[f114]) ).
fof(f114_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)],[f114_nnf]) ).
cnf(c114,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f114_sk]) ).
cnf(f116,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f116_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)],[f116]) ).
fof(f116_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)],[f116_nnf]) ).
cnf(c116,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f116_sk]) ).
cnf(f117,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f117_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)],[f117]) ).
fof(f117_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)],[f117_nnf]) ).
cnf(c117,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f117_sk]) ).
cnf(f123,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/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f123_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)],[f123]) ).
fof(f123_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)],[f123_nnf]) ).
cnf(c123,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)],[f123_sk]) ).
cnf(f126,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f126_nnf,plain,
! [T_a,V_c,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_A)) ),
inference(nnf_transformation,[status(thm)],[f126]) ).
fof(f126_sk,plain,
! [T_a,V_c,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_A)) ),
inference(skolemisation,[status(esa)],[f126_nnf]) ).
cnf(c126,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_HOL_Ouminus__class_Ouminus(X2,tc_fun(X0,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f126_sk]) ).
cnf(f133,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/sandbox2/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f133_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)],[f133]) ).
fof(f133_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)],[f133_nnf]) ).
cnf(c133,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)],[f133_sk]) ).
cnf(f190,axiom,
c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f190_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)],[f190]) ).
fof(f190_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)],[f190_nnf]) ).
cnf(c190,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f190_sk]) ).
cnf(f215,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/sandbox2/benchmark/theBenchmark.p',cls_not__psubset__empty_0) ).
fof(f215_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)],[f215]) ).
fof(f215_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)],[f215_nnf]) ).
cnf(c215,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)],[f215_sk]) ).
cnf(f238,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f238_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)],[f238]) ).
fof(f238_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)],[f238_nnf]) ).
cnf(c238,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
cnf(f243,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/sandbox2/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f243_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)],[f243]) ).
fof(f243_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)],[f243_nnf]) ).
cnf(c243,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)],[f243_sk]) ).
cnf(f290,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f290_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)],[f290]) ).
fof(f290_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)],[f290_nnf]) ).
cnf(c290,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f290_sk]) ).
cnf(f292,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f292_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)],[f292]) ).
fof(f292_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)],[f292_nnf]) ).
cnf(c292,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f292_sk]) ).
cnf(f294,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f294_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)],[f294]) ).
fof(f294_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)],[f294_nnf]) ).
cnf(c294,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f294_sk]) ).
cnf(f296,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/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f296_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)],[f296]) ).
fof(f296_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)],[f296_nnf]) ).
cnf(c296,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f296_sk]) ).
cnf(f325,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/sandbox2/benchmark/theBenchmark.p',cls_less__fun__def_1) ).
fof(f325_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)],[f325]) ).
fof(f325_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)],[f325_nnf]) ).
cnf(c325,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)],[f325_sk]) ).
cnf(f349,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_psubset__eq_1) ).
fof(f349_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)],[f349]) ).
fof(f349_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)],[f349_nnf]) ).
cnf(c349,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f349_sk]) ).
cnf(f350,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f350_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)],[f350]) ).
fof(f350_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)],[f350_nnf]) ).
cnf(c350,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f350_sk]) ).
cnf(f351,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f351_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)],[f351]) ).
fof(f351_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)],[f351_nnf]) ).
cnf(c351,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f351_sk]) ).
cnf(f352,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f352_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)],[f352]) ).
fof(f352_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)],[f352_nnf]) ).
cnf(c352,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f352_sk]) ).
cnf(f378,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/sandbox2/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff2_0) ).
fof(f378_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)],[f378]) ).
fof(f378_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)],[f378_nnf]) ).
cnf(c378,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)],[f378_sk]) ).
cnf(f379,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f379_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)],[f379]) ).
fof(f379_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)],[f379_nnf]) ).
cnf(c379,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f379_sk]) ).
cnf(f400,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f400_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f400]) ).
fof(f400_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f400_nnf]) ).
cnf(c400,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f400_sk]) ).
cnf(f401,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f401_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f401]) ).
fof(f401_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f401_nnf]) ).
cnf(c401,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f401_sk]) ).
cnf(f408,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/sandbox2/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff_0) ).
fof(f408_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)],[f408]) ).
fof(f408_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)],[f408_nnf]) ).
cnf(c408,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)],[f408_sk]) ).
cnf(f413,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/sandbox2/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff_0) ).
fof(f413_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)],[f413]) ).
fof(f413_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)],[f413_nnf]) ).
cnf(c413,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)],[f413_sk]) ).
cnf(f444,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/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f444_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)],[f444]) ).
fof(f444_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)],[f444_nnf]) ).
cnf(c444,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)],[f444_sk]) ).
cnf(f445,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/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f445_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)],[f445]) ).
fof(f445_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)],[f445_nnf]) ).
cnf(c445,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)],[f445_sk]) ).
cnf(f446,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/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f446_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)],[f446]) ).
fof(f446_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)],[f446_nnf]) ).
cnf(c446,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)],[f446_sk]) ).
cnf(f447,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/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f447_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)],[f447]) ).
fof(f447_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)],[f447_nnf]) ).
cnf(c447,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)],[f447_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c60,c114,c116,c117,c123,c126,c133,c190,c215,c238,c243,c290,c292,c294,c296,c325,c349,c350,c351,c352,c378,c379,c400,c401,c408,c413,c444,c445,c446,c447,c551]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t8251]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV858-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.36 % Computer : n007.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Thu Sep 24 21:09:08 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 33.09/5.07 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 33.09/5.07 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------