%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV841-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 : n001.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:11 PM UTC 2026
% Result : Unsatisfiable 26.07s 3.86s
% Output : Proof 26.07s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t126,axiom,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts),t_a),
introduced(definition) ).
cnf(t122,axiom,
sF0 = tc_Hoare__Mirabelle_Otriple(t_a),
introduced(definition) ).
cnf(t139,plain,
tc_Hoare__Mirabelle_Otriple(t_a) = sF0,
inference(orient,[status(thm)],[t122]) ).
cnf(t5407,plain,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(sF0),v_t),v_ts),t_a),
inference(step,[status(thm)],[t126,t139]) ).
cnf(t123,axiom,
sF1 = c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),
introduced(definition) ).
cnf(t5387,plain,
sF1 = c_Set_Oinsert(sF0),
inference(step,[status(thm)],[t123,t139]) ).
cnf(t145,plain,
c_Set_Oinsert(sF0) = sF1,
inference(orient,[status(thm)],[t5387]) ).
cnf(t5408,plain,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(sF1,v_t),v_ts),t_a),
inference(step,[status(thm)],[t5407,t145]) ).
cnf(t124,axiom,
sF2 = hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),
introduced(definition) ).
cnf(t5389,plain,
sF2 = hAPP(c_Set_Oinsert(sF0),v_t),
inference(step,[status(thm)],[t124,t139]) ).
cnf(t5390,plain,
sF2 = hAPP(sF1,v_t),
inference(step,[status(thm)],[t5389,t145]) ).
cnf(t149,plain,
hAPP(sF1,v_t) = sF2,
inference(orient,[status(thm)],[t5390]) ).
cnf(t5409,plain,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(sF2,v_ts),t_a),
inference(step,[status(thm)],[t5408,t149]) ).
cnf(t125,axiom,
sF3 = hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts),
introduced(definition) ).
cnf(t5395,plain,
sF3 = hAPP(hAPP(c_Set_Oinsert(sF0),v_t),v_ts),
inference(step,[status(thm)],[t125,t139]) ).
cnf(t5396,plain,
sF3 = hAPP(hAPP(sF1,v_t),v_ts),
inference(step,[status(thm)],[t5395,t145]) ).
cnf(t5397,plain,
sF3 = hAPP(sF2,v_ts),
inference(step,[status(thm)],[t5396,t149]) ).
cnf(t164,plain,
hAPP(sF2,v_ts) = sF3,
inference(orient,[status(thm)],[t5397]) ).
cnf(t5410,plain,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF3,t_a),
inference(step,[status(thm)],[t5409,t164]) ).
cnf(f499,negated_conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts),t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f499_nnf,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts),t_a),
inference(nnf_transformation,[status(thm)],[f499]) ).
cnf(c499,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts),t_a),
inference(cnf_transformation,[status(esa)],[f499_nnf]) ).
cnf(t20,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts),t_a) = true,
inference(equality_encoding,[status(esa)],[c499]) ).
cnf(t5403,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(sF0),v_t),v_ts),t_a) = true,
inference(step,[status(thm)],[t20,t139]) ).
cnf(t5404,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(sF1,v_t),v_ts),t_a) = true,
inference(step,[status(thm)],[t5403,t145]) ).
cnf(t5405,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(sF2,v_ts),t_a) = true,
inference(step,[status(thm)],[t5404,t149]) ).
cnf(t5406,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF3,t_a) = true,
inference(step,[status(thm)],[t5405,t164]) ).
cnf(t184,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF3,t_a) = true,
inference(orient,[status(thm)],[t5406]) ).
cnf(t5411,plain,
sF4 = true,
inference(step,[status(thm)],[t5410,t184]) ).
cnf(t192,plain,
true = sF4,
inference(orient,[status(thm)],[t5411]) ).
cnf(t128,axiom,
sF6 = not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,t_a)),
introduced(definition) ).
cnf(t127,axiom,
sF5 = c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,t_a),
introduced(definition) ).
cnf(t146,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,t_a) = sF5,
inference(orient,[status(thm)],[t127]) ).
cnf(t5391,plain,
sF6 = not(sF5),
inference(step,[status(thm)],[t128,t146]) ).
cnf(t150,plain,
not(sF5) = sF6,
inference(orient,[status(thm)],[t5391]) ).
cnf(t1041,plain,
not(sF4) = sF6,
inference(rw,[status(thm)],[t150]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t138,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t5414,plain,
not(sF4) = false,
inference(step,[status(thm)],[t138,t192]) ).
cnf(t195,plain,
not(sF4) = false,
inference(rw,[status(thm)],[t5414]) ).
cnf(t234,plain,
not(sF4) = false,
inference(orient,[status(thm)],[t195]) ).
cnf(t5714,plain,
false = sF6,
inference(step,[status(thm)],[t1041,t234]) ).
cnf(t1046,plain,
false = sF6,
inference(orient,[status(thm)],[t5714]) ).
cnf(f435,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts_H,T_a)
| ~ c_lessequals(V_ts,V_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_weaken_0) ).
fof(f435_nnf,plain,
! [V_G,V_ts,T_a,V_ts_H] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts_H,T_a)
| ~ c_lessequals(V_ts,V_ts_H,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)],[f435]) ).
fof(f435_sk,plain,
! [V_G,V_ts,T_a,V_ts_H] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts_H,T_a)
| ~ c_lessequals(V_ts,V_ts_H,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)],[f435_nnf]) ).
cnf(c435,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X3,X2)
| ~ c_lessequals(X1,X3,tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f435_sk]) ).
cnf(t77,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X4,X2,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(X4,X1,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c435]) ).
cnf(t6001,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X4,X2,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(X4,X1,X3),true),true) = true,
inference(step,[status(thm)],[t77,t192]) ).
cnf(t6002,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X4,X2,X3),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X4,X1,X3),true),true) = true,
inference(step,[status(thm)],[t6001,t192]) ).
cnf(t6003,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X4,X2,X3),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X4,X1,X3),sF4),true) = true,
inference(step,[status(thm)],[t6002,t192]) ).
cnf(t6004,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X4,X2,X3),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X4,X1,X3),sF4),sF4) = true,
inference(step,[status(thm)],[t6003,t192]) ).
cnf(t6005,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X4,X2,X3),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X4,X1,X3),sF4),sF4) = sF4,
inference(step,[status(thm)],[t6004,t192]) ).
cnf(t1900,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X4,X2,X3),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X4,X1,X3),sF4),sF4) = sF4,
inference(orient,[status(thm)],[t6005]) ).
cnf(t5442,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF3,t_a) = sF4,
inference(step,[status(thm)],[t184,t192]) ).
cnf(t224,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF3,t_a) = sF4,
inference(orient,[status(thm)],[t5442]) ).
cnf(t1905,plain,
sF4 = ifeq(c_lessequals(X1,sF3,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),sF4,ifeq(sF4,sF4,c_Hoare__Mirabelle_Ohoare__derivs(v_G,X1,t_a),sF4),sF4),
inference(cp,[status(thm)],[t1900,t224]) ).
cnf(t6086,plain,
sF4 = ifeq(c_lessequals(X1,sF3,tc_fun(sF0,tc_bool)),sF4,ifeq(sF4,sF4,c_Hoare__Mirabelle_Ohoare__derivs(v_G,X1,t_a),sF4),sF4),
inference(step,[status(thm)],[t1905,t139]) ).
cnf(t129,axiom,
sF7 = tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool),
introduced(definition) ).
cnf(t5388,plain,
sF7 = tc_fun(sF0,tc_bool),
inference(step,[status(thm)],[t129,t139]) ).
cnf(t148,plain,
tc_fun(sF0,tc_bool) = sF7,
inference(orient,[status(thm)],[t5388]) ).
cnf(t6087,plain,
sF4 = ifeq(c_lessequals(X1,sF3,sF7),sF4,ifeq(sF4,sF4,c_Hoare__Mirabelle_Ohoare__derivs(v_G,X1,t_a),sF4),sF4),
inference(step,[status(thm)],[t6086,t148]) ).
cnf(t7,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t147,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t7]) ).
cnf(t6088,plain,
sF4 = ifeq(c_lessequals(X1,sF3,sF7),sF4,c_Hoare__Mirabelle_Ohoare__derivs(v_G,X1,t_a),sF4),
inference(step,[status(thm)],[t6087,t147]) ).
cnf(t2259,plain,
ifeq(c_lessequals(X1,sF3,sF7),sF4,c_Hoare__Mirabelle_Ohoare__derivs(v_G,X1,t_a),sF4) = sF4,
inference(orient,[status(thm)],[t6088]) ).
cnf(f171,axiom,
( c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B) != V_B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subset__Un__eq_1) ).
fof(f171_nnf,plain,
! [T_a,V_A,V_B] :
( c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B) != V_B ),
inference(nnf_transformation,[status(thm)],[f171]) ).
fof(f171_sk,plain,
! [T_a,V_A,V_B] :
( c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B) != V_B ),
inference(skolemisation,[status(esa)],[f171_nnf]) ).
cnf(c171,plain,
( c_lessequals(X1,X2,tc_fun(X0,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),X1),X2) != X2 ),
inference(cnf_transformation,[status(esa)],[f171_sk]) ).
cnf(t55,plain,
ifeq(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X2),X3),X3,c_lessequals(X2,X3,tc_fun(X1,tc_bool)),true) = true,
inference(equality_encoding,[status(esa)],[c171]) ).
cnf(t5615,plain,
ifeq(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X2),X3),X3,c_lessequals(X2,X3,tc_fun(X1,tc_bool)),sF4) = true,
inference(step,[status(thm)],[t55,t192]) ).
cnf(t5616,plain,
ifeq(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X2),X3),X3,c_lessequals(X2,X3,tc_fun(X1,tc_bool)),sF4) = sF4,
inference(step,[status(thm)],[t5615,t192]) ).
cnf(t749,plain,
ifeq(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X2),X3),X3,c_lessequals(X2,X3,tc_fun(X1,tc_bool)),sF4) = sF4,
inference(orient,[status(thm)],[t5616]) ).
cnf(t750,plain,
sF4 = ifeq(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2),X2,c_lessequals(X1,X2,tc_fun(sF0,tc_bool)),sF4),
inference(cp,[status(thm)],[t749,t148]) ).
cnf(t6352,plain,
sF4 = ifeq(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2),X2,c_lessequals(X1,X2,sF7),sF4),
inference(step,[status(thm)],[t750,t148]) ).
cnf(t4996,plain,
ifeq(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2),X2,c_lessequals(X1,X2,sF7),sF4) = sF4,
inference(orient,[status(thm)],[t6352]) ).
cnf(f223,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Un__left__absorb_0) ).
fof(f223_nnf,plain,
! [T_a,V_A,V_B] : hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),
inference(nnf_transformation,[status(thm)],[f223]) ).
fof(f223_sk,plain,
! [T_a,V_A,V_B] : hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),
inference(skolemisation,[status(esa)],[f223_nnf]) ).
cnf(c223,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),X1),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),X1),X2)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),X1),X2),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
cnf(t87,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X2),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X2),X3)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X2),X3),
inference(equality_encoding,[status(esa)],[c223]) ).
cnf(t2403,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X2),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X2),X3)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X2),X3),
inference(orient,[status(thm)],[t87]) ).
cnf(t2404,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(sF0,tc_bool)),X1),X2) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(sF0,tc_bool)),X1),X2)),
inference(cp,[status(thm)],[t2403,t148]) ).
cnf(t6108,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(sF0,tc_bool)),X1),X2)),
inference(step,[status(thm)],[t2404,t148]) ).
cnf(t6109,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2)),
inference(step,[status(thm)],[t6108,t148]) ).
cnf(t2435,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2),
inference(orient,[status(thm)],[t6109]) ).
cnf(t5000,plain,
sF4 = ifeq(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2),c_lessequals(X1,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2),sF7),sF4),
inference(cp,[status(thm)],[t4996,t2435]) ).
cnf(t6354,plain,
sF4 = c_lessequals(X1,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2),sF7),
inference(step,[status(thm)],[t5000,t147]) ).
cnf(t5018,plain,
c_lessequals(X1,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),X1),X2),sF7) = sF4,
inference(orient,[status(thm)],[t6354]) ).
cnf(f480,axiom,
hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),V_A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__is__Un_0) ).
fof(f480_nnf,plain,
! [T_a,V_a,V_A] : hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),V_A),
inference(nnf_transformation,[status(thm)],[f480]) ).
fof(f480_sk,plain,
! [T_a,V_a,V_A] : hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),V_A),
inference(skolemisation,[status(esa)],[f480_nnf]) ).
cnf(c480,plain,
hAPP(hAPP(c_Set_Oinsert(X0),X1),X2) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),X2),
inference(cnf_transformation,[status(esa)],[f480_sk]) ).
cnf(t74,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),hAPP(hAPP(c_Set_Oinsert(X1),X2),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),X3) = hAPP(hAPP(c_Set_Oinsert(X1),X2),X3),
inference(equality_encoding,[status(esa)],[c480]) ).
cnf(t1768,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),hAPP(hAPP(c_Set_Oinsert(X1),X2),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),X3) = hAPP(hAPP(c_Set_Oinsert(X1),X2),X3),
inference(orient,[status(thm)],[t74]) ).
cnf(t1769,plain,
hAPP(hAPP(c_Set_Oinsert(sF0),X1),X2) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(sF0,tc_bool)),hAPP(hAPP(sF1,X1),c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)))),X2),
inference(cp,[status(thm)],[t1768,t145]) ).
cnf(t5985,plain,
hAPP(hAPP(sF1,X1),X2) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(sF0,tc_bool)),hAPP(hAPP(sF1,X1),c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)))),X2),
inference(step,[status(thm)],[t1769,t145]) ).
cnf(t5986,plain,
hAPP(hAPP(sF1,X1),X2) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),hAPP(hAPP(sF1,X1),c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)))),X2),
inference(step,[status(thm)],[t5985,t148]) ).
cnf(t5987,plain,
hAPP(hAPP(sF1,X1),X2) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),hAPP(hAPP(sF1,X1),c_Orderings_Obot__class_Obot(sF7))),X2),
inference(step,[status(thm)],[t5986,t148]) ).
cnf(t130,axiom,
sF8 = c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),
introduced(definition) ).
cnf(t5392,plain,
sF8 = c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)),
inference(step,[status(thm)],[t130,t139]) ).
cnf(t5393,plain,
sF8 = c_Orderings_Obot__class_Obot(sF7),
inference(step,[status(thm)],[t5392,t148]) ).
cnf(t151,plain,
c_Orderings_Obot__class_Obot(sF7) = sF8,
inference(orient,[status(thm)],[t5393]) ).
cnf(t5988,plain,
hAPP(hAPP(sF1,X1),X2) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),hAPP(hAPP(sF1,X1),sF8)),X2),
inference(step,[status(thm)],[t5987,t151]) ).
cnf(t1844,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),hAPP(hAPP(sF1,X1),sF8)),X2) = hAPP(hAPP(sF1,X1),X2),
inference(orient,[status(thm)],[t5988]) ).
cnf(t1845,plain,
hAPP(hAPP(sF1,v_t),X1) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),hAPP(sF2,sF8)),X1),
inference(cp,[status(thm)],[t1844,t149]) ).
cnf(t5989,plain,
hAPP(sF2,X1) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),hAPP(sF2,sF8)),X1),
inference(step,[status(thm)],[t1845,t149]) ).
cnf(t131,axiom,
sF9 = hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),
introduced(definition) ).
cnf(t5473,plain,
sF9 = hAPP(hAPP(c_Set_Oinsert(sF0),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),
inference(step,[status(thm)],[t131,t139]) ).
cnf(t5474,plain,
sF9 = hAPP(hAPP(sF1,v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),
inference(step,[status(thm)],[t5473,t145]) ).
cnf(t5475,plain,
sF9 = hAPP(sF2,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),
inference(step,[status(thm)],[t5474,t149]) ).
cnf(t5476,plain,
sF9 = hAPP(sF2,c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool))),
inference(step,[status(thm)],[t5475,t139]) ).
cnf(t5477,plain,
sF9 = hAPP(sF2,c_Orderings_Obot__class_Obot(sF7)),
inference(step,[status(thm)],[t5476,t148]) ).
cnf(t5478,plain,
sF9 = hAPP(sF2,sF8),
inference(step,[status(thm)],[t5477,t151]) ).
cnf(t290,plain,
hAPP(sF2,sF8) = sF9,
inference(orient,[status(thm)],[t5478]) ).
cnf(t5990,plain,
hAPP(sF2,X1) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),sF9),X1),
inference(step,[status(thm)],[t5989,t290]) ).
cnf(t1859,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF7),sF9),X1) = hAPP(sF2,X1),
inference(orient,[status(thm)],[t5990]) ).
cnf(t5019,plain,
sF4 = c_lessequals(sF9,hAPP(sF2,X1),sF7),
inference(cp,[status(thm)],[t5018,t1859]) ).
cnf(t5031,plain,
c_lessequals(sF9,hAPP(sF2,X1),sF7) = sF4,
inference(orient,[status(thm)],[t5019]) ).
cnf(t5032,plain,
sF4 = c_lessequals(sF9,sF3,sF7),
inference(cp,[status(thm)],[t5031,t164]) ).
cnf(t5041,plain,
c_lessequals(sF9,sF3,sF7) = sF4,
inference(orient,[status(thm)],[t5032]) ).
cnf(t5045,plain,
sF4 = ifeq(sF4,sF4,c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF9,t_a),sF4),
inference(cp,[status(thm)],[t2259,t5041]) ).
cnf(t6355,plain,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF9,t_a),
inference(step,[status(thm)],[t5045,t147]) ).
cnf(t10,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t155,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t10]) ).
cnf(t5421,plain,
ifeq(not(X1),sF4,X1,false) = false,
inference(step,[status(thm)],[t155,t192]) ).
cnf(t204,plain,
ifeq(not(X1),sF4,X1,false) = false,
inference(rw,[status(thm)],[t5421]) ).
cnf(t239,plain,
ifeq(not(X1),sF4,X1,false) = false,
inference(orient,[status(thm)],[t204]) ).
cnf(t1061,plain,
ifeq(not(X1),sF4,X1,sF6) = false,
inference(rw,[status(thm)],[t239]) ).
cnf(t5882,plain,
ifeq(not(X1),sF4,X1,sF6) = sF6,
inference(step,[status(thm)],[t1061,t1046]) ).
cnf(t1238,plain,
ifeq(not(X1),sF4,X1,sF6) = sF6,
inference(orient,[status(thm)],[t5882]) ).
cnf(f500,negated_conjecture,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f500_nnf,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,t_a) ),
inference(nnf_transformation,[status(thm)],[f500]) ).
fof(f500_sk,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,t_a) ),
inference(skolemisation,[status(esa)],[f500_nnf]) ).
cnf(c500,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,t_a) ),
inference(cnf_transformation,[status(esa)],[f500_sk]) ).
cnf(t81,plain,
or(not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,t_a)),not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a))) = true,
inference(equality_encoding,[status(esa)],[c500]) ).
cnf(f484,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_cut_0) ).
fof(f484_nnf,plain,
! [V_G,V_ts,T_a,V_G_H] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
inference(nnf_transformation,[status(thm)],[f484]) ).
fof(f484_sk,plain,
! [V_G,V_ts,T_a,V_G_H] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
inference(skolemisation,[status(esa)],[f484_nnf]) ).
cnf(c484,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X3,X1,X2)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X3,X2)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f484_sk]) ).
cnf(t58,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c484]) ).
cnf(t5660,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),true,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),true),true) = true,
inference(step,[status(thm)],[t58,t192]) ).
cnf(t5661,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),true),true) = true,
inference(step,[status(thm)],[t5660,t192]) ).
cnf(t5662,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),sF4),true) = true,
inference(step,[status(thm)],[t5661,t192]) ).
cnf(t5663,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),sF4),sF4) = true,
inference(step,[status(thm)],[t5662,t192]) ).
cnf(t5664,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),sF4),sF4) = sF4,
inference(step,[status(thm)],[t5663,t192]) ).
cnf(t835,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X2,X4,X3),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3),sF4),sF4) = sF4,
inference(orient,[status(thm)],[t5664]) ).
cnf(t842,plain,
sF4 = ifeq(sF4,sF4,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(sF3,X1,t_a),sF4,c_Hoare__Mirabelle_Ohoare__derivs(v_G,X1,t_a),sF4),sF4),
inference(cp,[status(thm)],[t835,t224]) ).
cnf(t5707,plain,
sF4 = ifeq(c_Hoare__Mirabelle_Ohoare__derivs(sF3,X1,t_a),sF4,c_Hoare__Mirabelle_Ohoare__derivs(v_G,X1,t_a),sF4),
inference(step,[status(thm)],[t842,t147]) ).
cnf(t1036,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(sF3,X1,t_a),sF4,c_Hoare__Mirabelle_Ohoare__derivs(v_G,X1,t_a),sF4) = sF4,
inference(orient,[status(thm)],[t5707]) ).
cnf(t1037,plain,
sF4 = ifeq(c_Hoare__Mirabelle_Ohoare__derivs(sF3,v_ts,t_a),sF4,sF5,sF4),
inference(cp,[status(thm)],[t1036,t146]) ).
cnf(f437,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/sandbox2/benchmark/theBenchmark.p',cls_asm_0) ).
fof(f437_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)],[f437]) ).
fof(f437_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)],[f437_nnf]) ).
cnf(c437,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)],[f437_sk]) ).
cnf(t42,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)],[c437]) ).
cnf(t5522,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),true) = true,
inference(step,[status(thm)],[t42,t192]) ).
cnf(t5523,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),sF4) = true,
inference(step,[status(thm)],[t5522,t192]) ).
cnf(t5524,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),sF4) = sF4,
inference(step,[status(thm)],[t5523,t192]) ).
cnf(t440,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),sF4,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),sF4) = sF4,
inference(orient,[status(thm)],[t5524]) ).
cnf(f422,axiom,
c_lessequals(V_B,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subset__insertI_0) ).
fof(f422_nnf,plain,
! [V_B,T_a,V_a] : c_lessequals(V_B,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B),tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f422]) ).
fof(f422_sk,plain,
! [V_B,T_a,V_a] : c_lessequals(V_B,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B),tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f422_nnf]) ).
cnf(c422,plain,
c_lessequals(X0,hAPP(hAPP(c_Set_Oinsert(X1),X2),X0),tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f422_sk]) ).
cnf(t24,plain,
c_lessequals(X1,hAPP(hAPP(c_Set_Oinsert(X2),X3),X1),tc_fun(X2,tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c422]) ).
cnf(t5454,plain,
c_lessequals(X1,hAPP(hAPP(c_Set_Oinsert(X2),X3),X1),tc_fun(X2,tc_bool)) = sF4,
inference(step,[status(thm)],[t24,t192]) ).
cnf(t241,plain,
c_lessequals(X1,hAPP(hAPP(c_Set_Oinsert(X2),X3),X1),tc_fun(X2,tc_bool)) = sF4,
inference(orient,[status(thm)],[t5454]) ).
cnf(t445,plain,
sF4 = ifeq(sF4,sF4,c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X1)),X2),X3),X3,X1),sF4),
inference(cp,[status(thm)],[t440,t241]) ).
cnf(t5540,plain,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X1)),X2),X3),X3,X1),
inference(step,[status(thm)],[t445,t147]) ).
cnf(t503,plain,
c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X1)),X2),X3),X3,X1) = sF4,
inference(orient,[status(thm)],[t5540]) ).
cnf(t504,plain,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(c_Set_Oinsert(sF0),X1),X2),X2,t_a),
inference(cp,[status(thm)],[t503,t139]) ).
cnf(t5541,plain,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(sF1,X1),X2),X2,t_a),
inference(step,[status(thm)],[t504,t145]) ).
cnf(t505,plain,
c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(sF1,X1),X2),X2,t_a) = sF4,
inference(orient,[status(thm)],[t5541]) ).
cnf(t506,plain,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(hAPP(sF2,X1),X1,t_a),
inference(cp,[status(thm)],[t505,t149]) ).
cnf(t507,plain,
c_Hoare__Mirabelle_Ohoare__derivs(hAPP(sF2,X1),X1,t_a) = sF4,
inference(orient,[status(thm)],[t506]) ).
cnf(t508,plain,
sF4 = c_Hoare__Mirabelle_Ohoare__derivs(sF3,v_ts,t_a),
inference(cp,[status(thm)],[t507,t164]) ).
cnf(t509,plain,
c_Hoare__Mirabelle_Ohoare__derivs(sF3,v_ts,t_a) = sF4,
inference(orient,[status(thm)],[t508]) ).
cnf(t5708,plain,
sF4 = ifeq(sF4,sF4,sF5,sF4),
inference(step,[status(thm)],[t1037,t509]) ).
cnf(t5709,plain,
sF4 = sF5,
inference(step,[status(thm)],[t5708,t147]) ).
cnf(t1038,plain,
sF5 = sF4,
inference(orient,[status(thm)],[t5709]) ).
cnf(t5710,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,t_a) = sF4,
inference(step,[status(thm)],[t146,t1038]) ).
cnf(t1039,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,v_ts,t_a) = sF4,
inference(orient,[status(thm)],[t5710]) ).
cnf(t6041,plain,
or(not(sF4),not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a))) = true,
inference(step,[status(thm)],[t81,t1039]) ).
cnf(t5726,plain,
not(sF4) = sF6,
inference(step,[status(thm)],[t234,t1046]) ).
cnf(t1058,plain,
not(sF4) = sF6,
inference(orient,[status(thm)],[t5726]) ).
cnf(t6042,plain,
or(sF6,not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a))) = true,
inference(step,[status(thm)],[t6041,t1058]) ).
cnf(t5,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t143,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t5717,plain,
or(sF6,X1) = X1,
inference(step,[status(thm)],[t143,t1046]) ).
cnf(t1049,plain,
or(sF6,X1) = X1,
inference(rw,[status(thm)],[t5717]) ).
cnf(t1212,plain,
or(sF6,X1) = X1,
inference(orient,[status(thm)],[t1049]) ).
cnf(t6043,plain,
not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)) = true,
inference(step,[status(thm)],[t6042,t1212]) ).
cnf(t6044,plain,
not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(sF0),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)) = true,
inference(step,[status(thm)],[t6043,t139]) ).
cnf(t6045,plain,
not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(sF1,v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)) = true,
inference(step,[status(thm)],[t6044,t145]) ).
cnf(t6046,plain,
not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(sF2,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)) = true,
inference(step,[status(thm)],[t6045,t149]) ).
cnf(t6047,plain,
not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(sF2,c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool))),t_a)) = true,
inference(step,[status(thm)],[t6046,t139]) ).
cnf(t6048,plain,
not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(sF2,c_Orderings_Obot__class_Obot(sF7)),t_a)) = true,
inference(step,[status(thm)],[t6047,t148]) ).
cnf(t6049,plain,
not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(sF2,sF8),t_a)) = true,
inference(step,[status(thm)],[t6048,t151]) ).
cnf(t6050,plain,
not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF9,t_a)) = true,
inference(step,[status(thm)],[t6049,t290]) ).
cnf(t6051,plain,
not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF9,t_a)) = sF4,
inference(step,[status(thm)],[t6050,t192]) ).
cnf(t2026,plain,
not(c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF9,t_a)) = sF4,
inference(orient,[status(thm)],[t6051]) ).
cnf(t2027,plain,
sF6 = ifeq(sF4,sF4,c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF9,t_a),sF6),
inference(cp,[status(thm)],[t1238,t2026]) ).
cnf(t6052,plain,
sF6 = c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF9,t_a),
inference(step,[status(thm)],[t2027,t147]) ).
cnf(t2028,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,sF9,t_a) = sF6,
inference(orient,[status(thm)],[t6052]) ).
cnf(t6356,plain,
sF4 = sF6,
inference(step,[status(thm)],[t6355,t2028]) ).
cnf(t5046,plain,
sF6 = sF4,
inference(orient,[status(thm)],[t6356]) ).
cnf(t6457,plain,
false = sF4,
inference(step,[status(thm)],[t1046,t5046]) ).
cnf(t5147,plain,
false = sF4,
inference(orient,[status(thm)],[t6457]) ).
cnf(f19,axiom,
( ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order_Oless__le_1) ).
fof(f19_nnf,plain,
! [V_less,V_x,V_less__eq,T_a] :
( ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [V_less,V_x,V_less__eq,T_a] :
( ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( ~ c_Orderings_Oorder(X2,X0,X3)
| ~ hBOOL(hAPP(hAPP(X0,X1),X1)) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(f37,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_Oneq__iff_1) ).
fof(f37_nnf,plain,
! [V_less,V_x,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [V_less,V_x,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( ~ c_Orderings_Olinorder(X2,X0,X3)
| ~ hBOOL(hAPP(hAPP(X0,X1),X1)) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(f38,axiom,
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_Onot__less__iff__gr__or__eq_2) ).
fof(f38_nnf,plain,
! [V_less__eq,V_less,T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [V_less__eq,V_less,T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( ~ hBOOL(hAPP(hAPP(X1,X3),X3))
| ~ c_Orderings_Olinorder(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(f114,axiom,
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order_OatLeastatMost__empty__iff2_0) ).
fof(f114_nnf,plain,
! [T_a,V_less__eq,V_a,V_b,V_less] :
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) ),
inference(nnf_transformation,[status(thm)],[f114]) ).
fof(f114_sk,plain,
! [T_a,V_less__eq,V_a,V_b,V_less] :
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) ),
inference(skolemisation,[status(esa)],[f114_nnf]) ).
cnf(c114,plain,
( ~ hBOOL(hAPP(hAPP(X1,X2),X3))
| ~ c_Orderings_Oorder(X1,X4,X0)
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_SetInterval_Oord_OatLeastAtMost(X1,X2,X3,X0) ),
inference(cnf_transformation,[status(esa)],[f114_sk]) ).
cnf(f119,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/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f119_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)],[f119]) ).
fof(f119_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)],[f119_nnf]) ).
cnf(c119,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)],[f119_sk]) ).
cnf(f154,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != 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/sandbox2/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f154_nnf,plain,
! [V_x,V_B,T_a,V_A] :
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != 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)],[f154]) ).
fof(f154_sk,plain,
! [V_x,V_B,T_a,V_A] :
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != 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)],[f154_nnf]) ).
cnf(c154,plain,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X2,tc_bool)),X3),X1) != 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)],[f154_sk]) ).
cnf(f176,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_Onot__less__iff__gr__or__eq_1) ).
fof(f176_nnf,plain,
! [V_less,V_x,V_y,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
inference(nnf_transformation,[status(thm)],[f176]) ).
fof(f176_sk,plain,
! [V_less,V_x,V_y,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
inference(skolemisation,[status(esa)],[f176_nnf]) ).
cnf(c176,plain,
( ~ c_Orderings_Olinorder(X3,X0,X4)
| ~ hBOOL(hAPP(hAPP(X0,X2),X1))
| ~ hBOOL(hAPP(hAPP(X0,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f176_sk]) ).
cnf(f177,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_OleD_0) ).
fof(f177_nnf,plain,
! [V_less,V_x,V_y,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
inference(nnf_transformation,[status(thm)],[f177]) ).
fof(f177_sk,plain,
! [V_less,V_x,V_y,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
inference(skolemisation,[status(esa)],[f177_nnf]) ).
cnf(c177,plain,
( ~ c_Orderings_Olinorder(X3,X0,X4)
| ~ hBOOL(hAPP(hAPP(X3,X2),X1))
| ~ hBOOL(hAPP(hAPP(X0,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f177_sk]) ).
cnf(f181,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_Onot__le_1) ).
fof(f181_nnf,plain,
! [V_less__eq,V_x,V_y,V_less,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y)) ),
inference(nnf_transformation,[status(thm)],[f181]) ).
fof(f181_sk,plain,
! [V_less__eq,V_x,V_y,V_less,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y)) ),
inference(skolemisation,[status(esa)],[f181_nnf]) ).
cnf(c181,plain,
( ~ c_Orderings_Olinorder(X0,X3,X4)
| ~ hBOOL(hAPP(hAPP(X3,X2),X1))
| ~ hBOOL(hAPP(hAPP(X0,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f181_sk]) ).
cnf(f184,axiom,
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_Oantisym__conv2_1) ).
fof(f184_nnf,plain,
! [V_less__eq,V_x,V_less,T_a] :
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_x)) ),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [V_less__eq,V_x,V_less,T_a] :
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_x)) ),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c184,plain,
( ~ hBOOL(hAPP(hAPP(X2,X1),X1))
| ~ c_Orderings_Olinorder(X0,X2,X3)
| ~ hBOOL(hAPP(hAPP(X0,X1),X1)) ),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
cnf(f197,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(f197_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)],[f197]) ).
fof(f197_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)],[f197_nnf]) ).
cnf(c197,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)],[f197_sk]) ).
cnf(f237,axiom,
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),hAPP(c_Set_Oimage(V_f,T_a,T_b),c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool))),T_b)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f237_nnf,plain,
! [V_f,V_a,T_a,T_b,V_A] :
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),hAPP(c_Set_Oimage(V_f,T_a,T_b),c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool))),T_b)) ),
inference(nnf_transformation,[status(thm)],[f237]) ).
fof(f237_sk,plain,
! [V_f,V_a,T_a,T_b,V_A] :
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),hAPP(c_Set_Oimage(V_f,T_a,T_b),c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool))),T_b)) ),
inference(skolemisation,[status(esa)],[f237_nnf]) ).
cnf(c237,plain,
( ~ c_Fun_Oinj__on(X0,hAPP(hAPP(c_Set_Oinsert(X2),X1),X4),X2,X3)
| ~ hBOOL(c_in(hAPP(X0,X1),hAPP(c_Set_Oimage(X0,X2,X3),c_HOL_Ominus__class_Ominus(X4,hAPP(hAPP(c_Set_Oinsert(X2),X1),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))),tc_fun(X2,tc_bool))),X3)) ),
inference(cnf_transformation,[status(esa)],[f237_sk]) ).
cnf(f269,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__Collect__eq_0) ).
fof(f269_nnf,plain,
! [T_a,V_P,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
inference(nnf_transformation,[status(thm)],[f269]) ).
fof(f269_sk,plain,
! [T_a,V_P,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
inference(skolemisation,[status(esa)],[f269_nnf]) ).
cnf(c269,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f269_sk]) ).
cnf(f270,axiom,
~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f270_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)],[f270]) ).
fof(f270_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)],[f270_nnf]) ).
cnf(c270,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f270_sk]) ).
cnf(f272,axiom,
~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f272_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)],[f272]) ).
fof(f272_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)],[f272_nnf]) ).
cnf(c272,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f272_sk]) ).
cnf(f273,axiom,
~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f273_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)],[f273]) ).
fof(f273_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)],[f273_nnf]) ).
cnf(c273,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
cnf(f276,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Collect__empty__eq_0) ).
fof(f276_nnf,plain,
! [V_P,T_a,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(nnf_transformation,[status(thm)],[f276]) ).
fof(f276_sk,plain,
! [V_P,T_a,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(skolemisation,[status(esa)],[f276_nnf]) ).
cnf(c276,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f276_sk]) ).
cnf(f277,axiom,
~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__fold1SetE_0) ).
fof(f277_nnf,plain,
! [V_f,T_a,V_x] : ~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_x)),
inference(nnf_transformation,[status(thm)],[f277]) ).
fof(f277_sk,plain,
! [V_f,T_a,V_x] : ~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_x)),
inference(skolemisation,[status(esa)],[f277_nnf]) ).
cnf(c277,plain,
~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),X2)),
inference(cnf_transformation,[status(esa)],[f277_sk]) ).
cnf(f290,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/sandbox2/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f290_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)],[f290]) ).
fof(f290_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)],[f290_nnf]) ).
cnf(c290,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)],[f290_sk]) ).
cnf(f313,axiom,
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order_OatLeastatMost__empty__iff_0) ).
fof(f313_nnf,plain,
! [V_less__eq,V_a,V_b,T_a,V_less] :
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(nnf_transformation,[status(thm)],[f313]) ).
fof(f313_sk,plain,
! [V_less__eq,V_a,V_b,T_a,V_less] :
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(skolemisation,[status(esa)],[f313_nnf]) ).
cnf(c313,plain,
( ~ hBOOL(hAPP(hAPP(X0,X1),X2))
| ~ c_Orderings_Oorder(X0,X4,X3)
| c_SetInterval_Oord_OatLeastAtMost(X0,X1,X2,X3) != c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f313_sk]) ).
cnf(f314,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I13_J_0) ).
fof(f314_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)],[f314]) ).
fof(f314_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)],[f314_nnf]) ).
cnf(c314,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
cnf(f365,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(f365_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)],[f365]) ).
fof(f365_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)],[f365_nnf]) ).
cnf(c365,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)],[f365_sk]) ).
cnf(f397,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I12_J_0) ).
fof(f397_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)],[f397]) ).
fof(f397_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)],[f397_nnf]) ).
cnf(c397,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f397_sk]) ).
cnf(f485,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f485_nnf,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),
inference(nnf_transformation,[status(thm)],[f485]) ).
fof(f485_sk,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),
inference(skolemisation,[status(esa)],[f485_nnf]) ).
cnf(c485,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != hAPP(hAPP(c_Set_Oinsert(X0),X1),X2),
inference(cnf_transformation,[status(esa)],[f485_sk]) ).
cnf(f490,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(f490_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)],[f490]) ).
fof(f490_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)],[f490_nnf]) ).
cnf(c490,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f490_sk]) ).
cnf(f494,axiom,
hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_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(f494_nnf,plain,
! [T_a,V_a,V_A] : hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f494]) ).
fof(f494_sk,plain,
! [T_a,V_a,V_A] : hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f494_nnf]) ).
cnf(c494,plain,
hAPP(hAPP(c_Set_Oinsert(X0),X1),X2) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(esa)],[f494_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c19,c37,c38,c114,c119,c154,c176,c177,c181,c184,c197,c237,c269,c270,c272,c273,c276,c277,c290,c313,c314,c365,c397,c485,c490,c494,c500]) ).
cnf(g0_0,plain,
sF4 != false,
inference(rw,[status(thm)],[goal_0,t192]) ).
cnf(g0_1,plain,
sF4 != sF4,
inference(rw,[status(thm)],[g0_0,t5147]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV841-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 21:14:38 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 26.07/3.86 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.07/3.86 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------