%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV861-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 : n010.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:16 PM UTC 2026
% Result : Unsatisfiable 12.73s 2.14s
% Output : Proof 12.73s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t75,axiom,
sF0 = c_Natural_Oevaln(v_c,v_s,v_n,v_s1),
introduced(definition) ).
cnf(f569,negated_conjecture,
c_Natural_Oevaln(v_c,v_s,v_n,v_s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f569_nnf,plain,
c_Natural_Oevaln(v_c,v_s,v_n,v_s1),
inference(nnf_transformation,[status(thm)],[f569]) ).
cnf(c569,plain,
c_Natural_Oevaln(v_c,v_s,v_n,v_s1),
inference(cnf_transformation,[status(esa)],[f569_nnf]) ).
cnf(t11,plain,
c_Natural_Oevaln(v_c,v_s,v_n,v_s1) = true,
inference(equality_encoding,[status(esa)],[c569]) ).
cnf(t129,plain,
c_Natural_Oevaln(v_c,v_s,v_n,v_s1) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t1634,plain,
sF0 = true,
inference(step,[status(thm)],[t75,t129]) ).
cnf(t133,plain,
true = sF0,
inference(orient,[status(thm)],[t1634]) ).
cnf(t82,axiom,
sF7 = hBOOL(hAPP(hAPP(v_R,v_Z),v_s_H)),
introduced(definition) ).
cnf(t101,axiom,
sF26(X1) = hAPP(v_R,X1),
introduced(definition) ).
cnf(t124,plain,
hAPP(v_R,X1) = sF26(X1),
inference(orient,[status(thm)],[t101]) ).
cnf(t1682,plain,
sF7 = hBOOL(hAPP(sF26(v_Z),v_s_H)),
inference(step,[status(thm)],[t82,t124]) ).
cnf(t102,axiom,
sF27(X1,X2) = hAPP(hAPP(v_R,X1),X2),
introduced(definition) ).
cnf(t1665,plain,
sF27(X1,X2) = hAPP(sF26(X1),X2),
inference(step,[status(thm)],[t102,t124]) ).
cnf(t169,plain,
hAPP(sF26(X1),X2) = sF27(X1,X2),
inference(orient,[status(thm)],[t1665]) ).
cnf(t1683,plain,
sF7 = hBOOL(sF27(v_Z,v_s_H)),
inference(step,[status(thm)],[t1682,t169]) ).
cnf(t81,axiom,
sF6 = hAPP(hAPP(v_R,v_Z),v_s_H),
introduced(definition) ).
cnf(t1656,plain,
sF6 = hAPP(sF26(v_Z),v_s_H),
inference(step,[status(thm)],[t81,t124]) ).
cnf(t80,axiom,
sF5 = hAPP(v_R,v_Z),
introduced(definition) ).
cnf(t118,plain,
hAPP(v_R,v_Z) = sF5,
inference(orient,[status(thm)],[t80]) ).
cnf(t1633,plain,
sF26(v_Z) = sF5,
inference(step,[status(thm)],[t118,t124]) ).
cnf(t125,plain,
sF26(v_Z) = sF5,
inference(rw,[status(thm)],[t1633]) ).
cnf(t126,plain,
sF26(v_Z) = sF5,
inference(orient,[status(thm)],[t125]) ).
cnf(t1657,plain,
sF6 = hAPP(sF5,v_s_H),
inference(step,[status(thm)],[t1656,t126]) ).
cnf(t154,plain,
hAPP(sF5,v_s_H) = sF6,
inference(orient,[status(thm)],[t1657]) ).
cnf(t170,plain,
sF27(v_Z,X1) = hAPP(sF5,X1),
inference(cp,[status(thm)],[t169,t126]) ).
cnf(t171,plain,
hAPP(sF5,X1) = sF27(v_Z,X1),
inference(orient,[status(thm)],[t170]) ).
cnf(t1666,plain,
sF27(v_Z,v_s_H) = sF6,
inference(step,[status(thm)],[t154,t171]) ).
cnf(t172,plain,
sF27(v_Z,v_s_H) = sF6,
inference(rw,[status(thm)],[t1666]) ).
cnf(t173,plain,
sF27(v_Z,v_s_H) = sF6,
inference(orient,[status(thm)],[t172]) ).
cnf(t1684,plain,
sF7 = hBOOL(sF6),
inference(step,[status(thm)],[t1683,t173]) ).
cnf(f571,negated_conjecture,
~ hBOOL(hAPP(hAPP(v_R,v_Z),v_s_H)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f571_nnf,plain,
~ hBOOL(hAPP(hAPP(v_R,v_Z),v_s_H)),
inference(nnf_transformation,[status(thm)],[f571]) ).
fof(f571_sk,plain,
~ hBOOL(hAPP(hAPP(v_R,v_Z),v_s_H)),
inference(skolemisation,[status(esa)],[f571_nnf]) ).
cnf(c571,plain,
~ hBOOL(hAPP(hAPP(v_R,v_Z),v_s_H)),
inference(cnf_transformation,[status(esa)],[f571_sk]) ).
cnf(t18,plain,
hBOOL(hAPP(hAPP(v_R,v_Z),v_s_H)) = false,
inference(equality_encoding,[status(esa)],[c571]) ).
cnf(t1671,plain,
hBOOL(hAPP(sF26(v_Z),v_s_H)) = false,
inference(step,[status(thm)],[t18,t124]) ).
cnf(t1672,plain,
hBOOL(sF27(v_Z,v_s_H)) = false,
inference(step,[status(thm)],[t1671,t169]) ).
cnf(t1673,plain,
hBOOL(sF6) = false,
inference(step,[status(thm)],[t1672,t173]) ).
cnf(t176,plain,
hBOOL(sF6) = false,
inference(orient,[status(thm)],[t1673]) ).
cnf(t1685,plain,
sF7 = false,
inference(step,[status(thm)],[t1684,t176]) ).
cnf(t180,plain,
false = sF7,
inference(orient,[status(thm)],[t1685]) ).
cnf(f574,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(v_Q,V_Z),V_s))
| ~ c_Natural_Oevaln(v_d,V_s,v_n,V_s_H)
| hBOOL(hAPP(hAPP(v_R,V_Z),V_s_H)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f574_nnf,plain,
! [V_Z,V_s_H,V_s] :
( ~ hBOOL(hAPP(hAPP(v_Q,V_Z),V_s))
| ~ c_Natural_Oevaln(v_d,V_s,v_n,V_s_H)
| hBOOL(hAPP(hAPP(v_R,V_Z),V_s_H)) ),
inference(nnf_transformation,[status(thm)],[f574]) ).
fof(f574_sk,plain,
! [V_Z,V_s_H,V_s] :
( ~ hBOOL(hAPP(hAPP(v_Q,V_Z),V_s))
| ~ c_Natural_Oevaln(v_d,V_s,v_n,V_s_H)
| hBOOL(hAPP(hAPP(v_R,V_Z),V_s_H)) ),
inference(skolemisation,[status(esa)],[f574_nnf]) ).
cnf(c574,plain,
( ~ hBOOL(hAPP(hAPP(v_Q,X0),X2))
| ~ c_Natural_Oevaln(v_d,X2,v_n,X1)
| hBOOL(hAPP(hAPP(v_R,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f574_sk]) ).
cnf(t66,plain,
ifeq(c_Natural_Oevaln(v_d,X1,v_n,X2),true,ifeq(hBOOL(hAPP(hAPP(v_Q,X3),X1)),true,hBOOL(hAPP(hAPP(v_R,X3),X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c574]) ).
cnf(t100,axiom,
sF25(X1,X2) = c_Natural_Oevaln(v_d,X1,v_n,X2),
introduced(definition) ).
cnf(t166,plain,
c_Natural_Oevaln(v_d,X1,v_n,X2) = sF25(X1,X2),
inference(orient,[status(thm)],[t100]) ).
cnf(t2053,plain,
ifeq(sF25(X1,X2),true,ifeq(hBOOL(hAPP(hAPP(v_Q,X3),X1)),true,hBOOL(hAPP(hAPP(v_R,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t66,t166]) ).
cnf(t2054,plain,
ifeq(sF25(X1,X2),sF0,ifeq(hBOOL(hAPP(hAPP(v_Q,X3),X1)),true,hBOOL(hAPP(hAPP(v_R,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2053,t133]) ).
cnf(t95,axiom,
sF20(X1) = hAPP(v_Q,X1),
introduced(definition) ).
cnf(t123,plain,
hAPP(v_Q,X1) = sF20(X1),
inference(orient,[status(thm)],[t95]) ).
cnf(t2055,plain,
ifeq(sF25(X1,X2),sF0,ifeq(hBOOL(hAPP(sF20(X3),X1)),true,hBOOL(hAPP(hAPP(v_R,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2054,t123]) ).
cnf(t96,axiom,
sF21(X1,X2) = hAPP(hAPP(v_Q,X1),X2),
introduced(definition) ).
cnf(t1663,plain,
sF21(X1,X2) = hAPP(sF20(X1),X2),
inference(step,[status(thm)],[t96,t123]) ).
cnf(t165,plain,
hAPP(sF20(X1),X2) = sF21(X1,X2),
inference(orient,[status(thm)],[t1663]) ).
cnf(t2056,plain,
ifeq(sF25(X1,X2),sF0,ifeq(hBOOL(sF21(X3,X1)),true,hBOOL(hAPP(hAPP(v_R,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2055,t165]) ).
cnf(t97,axiom,
sF22(X1,X2) = hBOOL(hAPP(hAPP(v_Q,X1),X2)),
introduced(definition) ).
cnf(t1703,plain,
sF22(X1,X2) = hBOOL(hAPP(sF20(X1),X2)),
inference(step,[status(thm)],[t97,t123]) ).
cnf(t1704,plain,
sF22(X1,X2) = hBOOL(sF21(X1,X2)),
inference(step,[status(thm)],[t1703,t165]) ).
cnf(t200,plain,
hBOOL(sF21(X1,X2)) = sF22(X1,X2),
inference(orient,[status(thm)],[t1704]) ).
cnf(t2057,plain,
ifeq(sF25(X1,X2),sF0,ifeq(sF22(X3,X1),true,hBOOL(hAPP(hAPP(v_R,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2056,t200]) ).
cnf(t2058,plain,
ifeq(sF25(X1,X2),sF0,ifeq(sF22(X3,X1),sF0,hBOOL(hAPP(hAPP(v_R,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2057,t133]) ).
cnf(t2059,plain,
ifeq(sF25(X1,X2),sF0,ifeq(sF22(X3,X1),sF0,hBOOL(hAPP(sF26(X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2058,t124]) ).
cnf(t2060,plain,
ifeq(sF25(X1,X2),sF0,ifeq(sF22(X3,X1),sF0,hBOOL(sF27(X3,X2)),true),true) = true,
inference(step,[status(thm)],[t2059,t169]) ).
cnf(t103,axiom,
sF28(X1,X2) = hBOOL(hAPP(hAPP(v_R,X1),X2)),
introduced(definition) ).
cnf(t1706,plain,
sF28(X1,X2) = hBOOL(hAPP(sF26(X1),X2)),
inference(step,[status(thm)],[t103,t124]) ).
cnf(t1707,plain,
sF28(X1,X2) = hBOOL(sF27(X1,X2)),
inference(step,[status(thm)],[t1706,t169]) ).
cnf(t202,plain,
hBOOL(sF27(X1,X2)) = sF28(X1,X2),
inference(orient,[status(thm)],[t1707]) ).
cnf(t2061,plain,
ifeq(sF25(X1,X2),sF0,ifeq(sF22(X3,X1),sF0,sF28(X3,X2),true),true) = true,
inference(step,[status(thm)],[t2060,t202]) ).
cnf(t2062,plain,
ifeq(sF25(X1,X2),sF0,ifeq(sF22(X3,X1),sF0,sF28(X3,X2),sF0),true) = true,
inference(step,[status(thm)],[t2061,t133]) ).
cnf(t2063,plain,
ifeq(sF25(X1,X2),sF0,ifeq(sF22(X3,X1),sF0,sF28(X3,X2),sF0),sF0) = true,
inference(step,[status(thm)],[t2062,t133]) ).
cnf(t2064,plain,
ifeq(sF25(X1,X2),sF0,ifeq(sF22(X3,X1),sF0,sF28(X3,X2),sF0),sF0) = sF0,
inference(step,[status(thm)],[t2063,t133]) ).
cnf(t1480,plain,
ifeq(sF25(X1,X2),sF0,ifeq(sF22(X3,X1),sF0,sF28(X3,X2),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t2064]) ).
cnf(f570,negated_conjecture,
c_Natural_Oevaln(v_d,v_s1,v_n,v_s_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f570_nnf,plain,
c_Natural_Oevaln(v_d,v_s1,v_n,v_s_H),
inference(nnf_transformation,[status(thm)],[f570]) ).
cnf(c570,plain,
c_Natural_Oevaln(v_d,v_s1,v_n,v_s_H),
inference(cnf_transformation,[status(esa)],[f570_nnf]) ).
cnf(t12,plain,
c_Natural_Oevaln(v_d,v_s1,v_n,v_s_H) = true,
inference(equality_encoding,[status(esa)],[c570]) ).
cnf(t130,plain,
c_Natural_Oevaln(v_d,v_s1,v_n,v_s_H) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t1651,plain,
c_Natural_Oevaln(v_d,v_s1,v_n,v_s_H) = sF0,
inference(step,[status(thm)],[t130,t133]) ).
cnf(t150,plain,
c_Natural_Oevaln(v_d,v_s1,v_n,v_s_H) = sF0,
inference(orient,[status(thm)],[t1651]) ).
cnf(t1664,plain,
sF25(v_s1,v_s_H) = sF0,
inference(step,[status(thm)],[t150,t166]) ).
cnf(t167,plain,
sF25(v_s1,v_s_H) = sF0,
inference(rw,[status(thm)],[t1664]) ).
cnf(t168,plain,
sF25(v_s1,v_s_H) = sF0,
inference(orient,[status(thm)],[t167]) ).
cnf(t1481,plain,
sF0 = ifeq(sF0,sF0,ifeq(sF22(X1,v_s1),sF0,sF28(X1,v_s_H),sF0),sF0),
inference(cp,[status(thm)],[t1480,t168]) ).
cnf(t14,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t132,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t14]) ).
cnf(t2083,plain,
sF0 = ifeq(sF22(X1,v_s1),sF0,sF28(X1,v_s_H),sF0),
inference(step,[status(thm)],[t1481,t132]) ).
cnf(t1553,plain,
ifeq(sF22(X1,v_s1),sF0,sF28(X1,v_s_H),sF0) = sF0,
inference(orient,[status(thm)],[t2083]) ).
cnf(t203,plain,
sF28(v_Z,v_s_H) = hBOOL(sF6),
inference(cp,[status(thm)],[t202,t173]) ).
cnf(t1696,plain,
hBOOL(sF6) = sF7,
inference(step,[status(thm)],[t176,t180]) ).
cnf(t191,plain,
hBOOL(sF6) = sF7,
inference(orient,[status(thm)],[t1696]) ).
cnf(t1708,plain,
sF28(v_Z,v_s_H) = sF7,
inference(step,[status(thm)],[t203,t191]) ).
cnf(t204,plain,
sF28(v_Z,v_s_H) = sF7,
inference(orient,[status(thm)],[t1708]) ).
cnf(t1554,plain,
sF0 = ifeq(sF22(v_Z,v_s1),sF0,sF7,sF0),
inference(cp,[status(thm)],[t1553,t204]) ).
cnf(f573,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| ~ c_Natural_Oevaln(v_c,V_s,v_n,V_s_H)
| hBOOL(hAPP(hAPP(v_Q,V_Z),V_s_H)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f573_nnf,plain,
! [V_Z,V_s_H,V_s] :
( ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| ~ c_Natural_Oevaln(v_c,V_s,v_n,V_s_H)
| hBOOL(hAPP(hAPP(v_Q,V_Z),V_s_H)) ),
inference(nnf_transformation,[status(thm)],[f573]) ).
fof(f573_sk,plain,
! [V_Z,V_s_H,V_s] :
( ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| ~ c_Natural_Oevaln(v_c,V_s,v_n,V_s_H)
| hBOOL(hAPP(hAPP(v_Q,V_Z),V_s_H)) ),
inference(skolemisation,[status(esa)],[f573_nnf]) ).
cnf(c573,plain,
( ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ c_Natural_Oevaln(v_c,X2,v_n,X1)
| hBOOL(hAPP(hAPP(v_Q,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f573_sk]) ).
cnf(t65,plain,
ifeq(c_Natural_Oevaln(v_c,X1,v_n,X2),true,ifeq(hBOOL(hAPP(hAPP(v_P,X3),X1)),true,hBOOL(hAPP(hAPP(v_Q,X3),X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c573]) ).
cnf(t91,axiom,
sF16(X1,X2) = c_Natural_Oevaln(v_c,X1,v_n,X2),
introduced(definition) ).
cnf(t156,plain,
c_Natural_Oevaln(v_c,X1,v_n,X2) = sF16(X1,X2),
inference(orient,[status(thm)],[t91]) ).
cnf(t2029,plain,
ifeq(sF16(X1,X2),true,ifeq(hBOOL(hAPP(hAPP(v_P,X3),X1)),true,hBOOL(hAPP(hAPP(v_Q,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t65,t156]) ).
cnf(t2030,plain,
ifeq(sF16(X1,X2),sF0,ifeq(hBOOL(hAPP(hAPP(v_P,X3),X1)),true,hBOOL(hAPP(hAPP(v_Q,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2029,t133]) ).
cnf(t92,axiom,
sF17(X1) = hAPP(v_P,X1),
introduced(definition) ).
cnf(t120,plain,
hAPP(v_P,X1) = sF17(X1),
inference(orient,[status(thm)],[t92]) ).
cnf(t2031,plain,
ifeq(sF16(X1,X2),sF0,ifeq(hBOOL(hAPP(sF17(X3),X1)),true,hBOOL(hAPP(hAPP(v_Q,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2030,t120]) ).
cnf(t93,axiom,
sF18(X1,X2) = hAPP(hAPP(v_P,X1),X2),
introduced(definition) ).
cnf(t1661,plain,
sF18(X1,X2) = hAPP(sF17(X1),X2),
inference(step,[status(thm)],[t93,t120]) ).
cnf(t160,plain,
hAPP(sF17(X1),X2) = sF18(X1,X2),
inference(orient,[status(thm)],[t1661]) ).
cnf(t2032,plain,
ifeq(sF16(X1,X2),sF0,ifeq(hBOOL(sF18(X3,X1)),true,hBOOL(hAPP(hAPP(v_Q,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2031,t160]) ).
cnf(t94,axiom,
sF19(X1,X2) = hBOOL(hAPP(hAPP(v_P,X1),X2)),
introduced(definition) ).
cnf(t1700,plain,
sF19(X1,X2) = hBOOL(hAPP(sF17(X1),X2)),
inference(step,[status(thm)],[t94,t120]) ).
cnf(t1701,plain,
sF19(X1,X2) = hBOOL(sF18(X1,X2)),
inference(step,[status(thm)],[t1700,t160]) ).
cnf(t197,plain,
hBOOL(sF18(X1,X2)) = sF19(X1,X2),
inference(orient,[status(thm)],[t1701]) ).
cnf(t2033,plain,
ifeq(sF16(X1,X2),sF0,ifeq(sF19(X3,X1),true,hBOOL(hAPP(hAPP(v_Q,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2032,t197]) ).
cnf(t2034,plain,
ifeq(sF16(X1,X2),sF0,ifeq(sF19(X3,X1),sF0,hBOOL(hAPP(hAPP(v_Q,X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2033,t133]) ).
cnf(t2035,plain,
ifeq(sF16(X1,X2),sF0,ifeq(sF19(X3,X1),sF0,hBOOL(hAPP(sF20(X3),X2)),true),true) = true,
inference(step,[status(thm)],[t2034,t123]) ).
cnf(t2036,plain,
ifeq(sF16(X1,X2),sF0,ifeq(sF19(X3,X1),sF0,hBOOL(sF21(X3,X2)),true),true) = true,
inference(step,[status(thm)],[t2035,t165]) ).
cnf(t2037,plain,
ifeq(sF16(X1,X2),sF0,ifeq(sF19(X3,X1),sF0,sF22(X3,X2),true),true) = true,
inference(step,[status(thm)],[t2036,t200]) ).
cnf(t2038,plain,
ifeq(sF16(X1,X2),sF0,ifeq(sF19(X3,X1),sF0,sF22(X3,X2),sF0),true) = true,
inference(step,[status(thm)],[t2037,t133]) ).
cnf(t2039,plain,
ifeq(sF16(X1,X2),sF0,ifeq(sF19(X3,X1),sF0,sF22(X3,X2),sF0),sF0) = true,
inference(step,[status(thm)],[t2038,t133]) ).
cnf(t2040,plain,
ifeq(sF16(X1,X2),sF0,ifeq(sF19(X3,X1),sF0,sF22(X3,X2),sF0),sF0) = sF0,
inference(step,[status(thm)],[t2039,t133]) ).
cnf(t1465,plain,
ifeq(sF16(X1,X2),sF0,ifeq(sF19(X3,X1),sF0,sF22(X3,X2),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t2040]) ).
cnf(t1649,plain,
c_Natural_Oevaln(v_c,v_s,v_n,v_s1) = sF0,
inference(step,[status(thm)],[t129,t133]) ).
cnf(t148,plain,
c_Natural_Oevaln(v_c,v_s,v_n,v_s1) = sF0,
inference(orient,[status(thm)],[t1649]) ).
cnf(t1660,plain,
sF16(v_s,v_s1) = sF0,
inference(step,[status(thm)],[t148,t156]) ).
cnf(t157,plain,
sF16(v_s,v_s1) = sF0,
inference(rw,[status(thm)],[t1660]) ).
cnf(t158,plain,
sF16(v_s,v_s1) = sF0,
inference(orient,[status(thm)],[t157]) ).
cnf(t1466,plain,
sF0 = ifeq(sF0,sF0,ifeq(sF19(X1,v_s),sF0,sF22(X1,v_s1),sF0),sF0),
inference(cp,[status(thm)],[t1465,t158]) ).
cnf(t2076,plain,
sF0 = ifeq(sF19(X1,v_s),sF0,sF22(X1,v_s1),sF0),
inference(step,[status(thm)],[t1466,t132]) ).
cnf(t1515,plain,
ifeq(sF19(X1,v_s),sF0,sF22(X1,v_s1),sF0) = sF0,
inference(orient,[status(thm)],[t2076]) ).
cnf(t78,axiom,
sF3 = hAPP(hAPP(v_P,v_Z),v_s),
introduced(definition) ).
cnf(t1654,plain,
sF3 = hAPP(sF17(v_Z),v_s),
inference(step,[status(thm)],[t78,t120]) ).
cnf(t77,axiom,
sF2 = hAPP(v_P,v_Z),
introduced(definition) ).
cnf(t117,plain,
hAPP(v_P,v_Z) = sF2,
inference(orient,[status(thm)],[t77]) ).
cnf(t1632,plain,
sF17(v_Z) = sF2,
inference(step,[status(thm)],[t117,t120]) ).
cnf(t121,plain,
sF17(v_Z) = sF2,
inference(rw,[status(thm)],[t1632]) ).
cnf(t122,plain,
sF17(v_Z) = sF2,
inference(orient,[status(thm)],[t121]) ).
cnf(t1655,plain,
sF3 = hAPP(sF2,v_s),
inference(step,[status(thm)],[t1654,t122]) ).
cnf(t153,plain,
hAPP(sF2,v_s) = sF3,
inference(orient,[status(thm)],[t1655]) ).
cnf(t161,plain,
sF18(v_Z,X1) = hAPP(sF2,X1),
inference(cp,[status(thm)],[t160,t122]) ).
cnf(t162,plain,
hAPP(sF2,X1) = sF18(v_Z,X1),
inference(orient,[status(thm)],[t161]) ).
cnf(t1662,plain,
sF18(v_Z,v_s) = sF3,
inference(step,[status(thm)],[t153,t162]) ).
cnf(t163,plain,
sF18(v_Z,v_s) = sF3,
inference(rw,[status(thm)],[t1662]) ).
cnf(t164,plain,
sF18(v_Z,v_s) = sF3,
inference(orient,[status(thm)],[t163]) ).
cnf(t198,plain,
sF19(v_Z,v_s) = hBOOL(sF3),
inference(cp,[status(thm)],[t197,t164]) ).
cnf(f568,negated_conjecture,
hBOOL(hAPP(hAPP(v_P,v_Z),v_s)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f568_nnf,plain,
hBOOL(hAPP(hAPP(v_P,v_Z),v_s)),
inference(nnf_transformation,[status(thm)],[f568]) ).
cnf(c568,plain,
hBOOL(hAPP(hAPP(v_P,v_Z),v_s)),
inference(cnf_transformation,[status(esa)],[f568_nnf]) ).
cnf(t17,plain,
hBOOL(hAPP(hAPP(v_P,v_Z),v_s)) = true,
inference(equality_encoding,[status(esa)],[c568]) ).
cnf(t1667,plain,
hBOOL(hAPP(sF17(v_Z),v_s)) = true,
inference(step,[status(thm)],[t17,t120]) ).
cnf(t1668,plain,
hBOOL(sF18(v_Z,v_s)) = true,
inference(step,[status(thm)],[t1667,t160]) ).
cnf(t1669,plain,
hBOOL(sF3) = true,
inference(step,[status(thm)],[t1668,t164]) ).
cnf(t1670,plain,
hBOOL(sF3) = sF0,
inference(step,[status(thm)],[t1669,t133]) ).
cnf(t175,plain,
hBOOL(sF3) = sF0,
inference(orient,[status(thm)],[t1670]) ).
cnf(t1702,plain,
sF19(v_Z,v_s) = sF0,
inference(step,[status(thm)],[t198,t175]) ).
cnf(t199,plain,
sF19(v_Z,v_s) = sF0,
inference(orient,[status(thm)],[t1702]) ).
cnf(t1516,plain,
sF0 = ifeq(sF0,sF0,sF22(v_Z,v_s1),sF0),
inference(cp,[status(thm)],[t1515,t199]) ).
cnf(t2077,plain,
sF0 = sF22(v_Z,v_s1),
inference(step,[status(thm)],[t1516,t132]) ).
cnf(t1517,plain,
sF22(v_Z,v_s1) = sF0,
inference(orient,[status(thm)],[t2077]) ).
cnf(t2084,plain,
sF0 = ifeq(sF0,sF0,sF7,sF0),
inference(step,[status(thm)],[t1554,t1517]) ).
cnf(t2085,plain,
sF0 = sF7,
inference(step,[status(thm)],[t2084,t132]) ).
cnf(t1555,plain,
sF7 = sF0,
inference(orient,[status(thm)],[t2085]) ).
cnf(t2096,plain,
false = sF0,
inference(step,[status(thm)],[t180,t1555]) ).
cnf(t1566,plain,
false = sF0,
inference(orient,[status(thm)],[t2096]) ).
cnf(f114,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(f114_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)],[f114]) ).
fof(f114_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)],[f114_nnf]) ).
cnf(c114,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)],[f114_sk]) ).
cnf(f187,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I17_J_0) ).
fof(f187_nnf,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f187]) ).
fof(f187_sk,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f187_nnf]) ).
cnf(c187,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f187_sk]) ).
cnf(f197,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I46_J_0) ).
fof(f197_nnf,plain,
! [V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f197]) ).
fof(f197_sk,plain,
! [V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f197_nnf]) ).
cnf(c197,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f197_sk]) ).
cnf(f200,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I44_J_0) ).
fof(f200_nnf,plain,
! [V_com1,V_com2,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f200]) ).
fof(f200_sk,plain,
! [V_com1,V_com2,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f200_nnf]) ).
cnf(c200,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
cnf(f201,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(f201_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)],[f201]) ).
fof(f201_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)],[f201_nnf]) ).
cnf(c201,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f201_sk]) ).
cnf(f208,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I52_J_0) ).
fof(f208_nnf,plain,
! [V_fun,V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f208]) ).
fof(f208_sk,plain,
! [V_fun,V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f208_nnf]) ).
cnf(c208,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f208_sk]) ).
cnf(f213,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I45_J_0) ).
fof(f213_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_com1,V_com2] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f213]) ).
fof(f213_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_com1,V_com2] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f213_nnf]) ).
cnf(c213,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
cnf(f223,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(f223_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)],[f223]) ).
fof(f223_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)],[f223_nnf]) ).
cnf(c223,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)],[f223_sk]) ).
cnf(f233,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I16_J_0) ).
fof(f233_nnf,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f233]) ).
fof(f233_sk,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f233_nnf]) ).
cnf(c233,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(X0,X1),
inference(cnf_transformation,[status(esa)],[f233_sk]) ).
cnf(f234,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(f234_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)],[f234]) ).
fof(f234_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)],[f234_nnf]) ).
cnf(c234,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f234_sk]) ).
cnf(f240,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(f240_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)],[f240]) ).
fof(f240_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)],[f240_nnf]) ).
cnf(c240,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)],[f240_sk]) ).
cnf(f243,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(f243_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)],[f243]) ).
fof(f243_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)],[f243_nnf]) ).
cnf(c243,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f243_sk]) ).
cnf(f244,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(f244_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)],[f244]) ).
fof(f244_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)],[f244_nnf]) ).
cnf(c244,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f244_sk]) ).
cnf(f245,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(f245_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)],[f245]) ).
fof(f245_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)],[f245_nnf]) ).
cnf(c245,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f245_sk]) ).
cnf(f246,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(f246_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)],[f246]) ).
fof(f246_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)],[f246_nnf]) ).
cnf(c246,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f246_sk]) ).
cnf(f247,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(f247_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)],[f247]) ).
fof(f247_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)],[f247_nnf]) ).
cnf(c247,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f247_sk]) ).
cnf(f287,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(f287_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)],[f287]) ).
fof(f287_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)],[f287_nnf]) ).
cnf(c287,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f287_sk]) ).
cnf(f289,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(f289_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)],[f289]) ).
fof(f289_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)],[f289_nnf]) ).
cnf(c289,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f289_sk]) ).
cnf(f291,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(f291_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)],[f291]) ).
fof(f291_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)],[f291_nnf]) ).
cnf(c291,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f291_sk]) ).
cnf(f293,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(f293_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)],[f293]) ).
fof(f293_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)],[f293_nnf]) ).
cnf(c293,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f293_sk]) ).
cnf(f310,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I14_J_0) ).
fof(f310_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f310]) ).
fof(f310_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f310_nnf]) ).
cnf(c310,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f310_sk]) ).
cnf(f315,axiom,
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq__eq_1) ).
fof(f315_nnf,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f315]) ).
fof(f315_sk,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f315_nnf]) ).
cnf(c315,plain,
( ~ c_lessequals(c_Suc(X1),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f315_sk]) ).
cnf(f332,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I15_J_0) ).
fof(f332_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f332]) ).
fof(f332_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f332_nnf]) ).
cnf(c332,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f332_sk]) ).
cnf(f334,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I53_J_0) ).
fof(f334_nnf,plain,
! [V_fun_H,V_com_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f334]) ).
fof(f334_sk,plain,
! [V_fun_H,V_com_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(skolemisation,[status(esa)],[f334_nnf]) ).
cnf(c334,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f334_sk]) ).
cnf(f337,axiom,
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(hAPP(hAPP(c_in(T_b),hAPP(V_f,V_a)),c_Set_Oimage(V_f,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),T_a,T_b))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f337_nnf,plain,
! [T_b,V_f,V_a,T_a,V_A] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(hAPP(hAPP(c_in(T_b),hAPP(V_f,V_a)),c_Set_Oimage(V_f,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),T_a,T_b))) ),
inference(nnf_transformation,[status(thm)],[f337]) ).
fof(f337_sk,plain,
! [T_b,V_f,V_a,T_a,V_A] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(hAPP(hAPP(c_in(T_b),hAPP(V_f,V_a)),c_Set_Oimage(V_f,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),T_a,T_b))) ),
inference(skolemisation,[status(esa)],[f337_nnf]) ).
cnf(c337,plain,
( ~ c_Fun_Oinj__on(X1,c_Set_Oinsert(X2,X4,X3),X3,X0)
| ~ hBOOL(hAPP(hAPP(c_in(X0),hAPP(X1,X2)),c_Set_Oimage(X1,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X3,tc_bool)),X4),c_Set_Oinsert(X2,c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3)),X3,X0))) ),
inference(cnf_transformation,[status(esa)],[f337_sk]) ).
cnf(f356,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(f356_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)],[f356]) ).
fof(f356_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)],[f356_nnf]) ).
cnf(c356,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f356_sk]) ).
cnf(f358,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(f358_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)],[f358]) ).
fof(f358_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)],[f358_nnf]) ).
cnf(c358,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f358_sk]) ).
cnf(f359,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(f359_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)],[f359]) ).
fof(f359_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)],[f359_nnf]) ).
cnf(c359,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f359_sk]) ).
cnf(f363,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),V_B)))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f363_nnf,plain,
! [T_a,V_c,V_B,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),V_B)))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
inference(nnf_transformation,[status(thm)],[f363]) ).
fof(f363_sk,plain,
! [T_a,V_c,V_B,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),V_B)))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
inference(skolemisation,[status(esa)],[f363_nnf]) ).
cnf(c363,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X0,tc_bool)),X3),X2)))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f363_sk]) ).
cnf(f390,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(f390_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)],[f390]) ).
fof(f390_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)],[f390_nnf]) ).
cnf(c390,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f390_sk]) ).
cnf(f403,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(f403_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)],[f403]) ).
fof(f403_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)],[f403_nnf]) ).
cnf(c403,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f403_sk]) ).
cnf(f406,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(f406_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)],[f406]) ).
fof(f406_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)],[f406_nnf]) ).
cnf(c406,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f406_sk]) ).
cnf(f408,axiom,
~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f408_nnf,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f408]) ).
fof(f408_sk,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f408_nnf]) ).
cnf(c408,plain,
~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f408_sk]) ).
cnf(f413,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I47_J_0) ).
fof(f413_nnf,plain,
! [V_fun_H,V_com_H,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f413]) ).
fof(f413_sk,plain,
! [V_fun_H,V_com_H,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f413_nnf]) ).
cnf(c413,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f413_sk]) ).
cnf(f417,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f417_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f417]) ).
fof(f417_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f417_nnf]) ).
cnf(c417,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f417_sk]) ).
cnf(f418,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f418_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f418]) ).
fof(f418_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f418_nnf]) ).
cnf(c418,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f418_sk]) ).
cnf(f461,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(f461_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)],[f461]) ).
fof(f461_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)],[f461_nnf]) ).
cnf(c461,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f461_sk]) ).
cnf(f462,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(f462_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)],[f462]) ).
fof(f462_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)],[f462_nnf]) ).
cnf(c462,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)],[f462_sk]) ).
cnf(f463,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(f463_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)],[f463]) ).
fof(f463_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)],[f463_nnf]) ).
cnf(c463,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)],[f463_sk]) ).
cnf(f466,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(f466_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)],[f466]) ).
fof(f466_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)],[f466_nnf]) ).
cnf(c466,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)],[f466_sk]) ).
cnf(f467,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(f467_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)],[f467]) ).
fof(f467_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)],[f467_nnf]) ).
cnf(c467,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)],[f467_sk]) ).
cnf(f490,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(f490_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)],[f490]) ).
fof(f490_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)],[f490_nnf]) ).
cnf(c490,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)],[f490_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c114,c187,c197,c200,c201,c208,c213,c223,c233,c234,c240,c243,c244,c245,c246,c247,c287,c289,c291,c293,c310,c315,c332,c334,c337,c356,c358,c359,c363,c390,c403,c406,c408,c413,c417,c418,c461,c462,c463,c466,c467,c490,c571]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t133]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t1566]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV861-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n010.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 21:12:13 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 12.73/2.14 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.73/2.14 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------