%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SCT042-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n019.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 02:39:52 PM UTC 2026
% Result : Unsatisfiable 23.50s 3.48s
% Output : Proof 23.50s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t101,axiom,
sF0 = ifeq(v_thesis____,true,false,true),
introduced(definition) ).
cnf(f608,negated_conjecture,
~ v_thesis____,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f608_nnf,plain,
~ v_thesis____,
inference(nnf_transformation,[status(thm)],[f608]) ).
fof(f608_sk,plain,
~ v_thesis____,
inference(skolemisation,[status(esa)],[f608_nnf]) ).
cnf(c608,plain,
~ v_thesis____,
inference(cnf_transformation,[status(esa)],[f608_sk]) ).
cnf(t0,plain,
v_thesis____ = false,
inference(equality_encoding,[status(esa)],[c608]) ).
cnf(t108,plain,
false = v_thesis____,
inference(orient,[status(thm)],[t0]) ).
cnf(t1290,plain,
sF0 = ifeq(v_thesis____,true,v_thesis____,true),
inference(step,[status(thm)],[t101,t108]) ).
cnf(t19,plain,
ifeq(v_thesis____,true,false,true) = true,
inference(equality_encoding,[status(esa)],[c608]) ).
cnf(t1289,plain,
ifeq(v_thesis____,true,v_thesis____,true) = true,
inference(step,[status(thm)],[t19,t108]) ).
cnf(t129,plain,
ifeq(v_thesis____,true,v_thesis____,true) = true,
inference(orient,[status(thm)],[t1289]) ).
cnf(t1291,plain,
sF0 = true,
inference(step,[status(thm)],[t1290,t129]) ).
cnf(t130,plain,
true = sF0,
inference(orient,[status(thm)],[t1291]) ).
cnf(f600,axiom,
( ~ c_List_Odistinct(c_List_Olist_OCons(v_a____,c_List_Olist_OCons(v_b____,c_List_Olist_OCons(V_c,c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt)
| v_thesis____ ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_that_0) ).
fof(f600_nnf,plain,
! [V_c] :
( ~ c_List_Odistinct(c_List_Olist_OCons(v_a____,c_List_Olist_OCons(v_b____,c_List_Olist_OCons(V_c,c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt)
| v_thesis____ ),
inference(nnf_transformation,[status(thm)],[f600]) ).
fof(f600_sk,plain,
! [V_c] :
( ~ c_List_Odistinct(c_List_Olist_OCons(v_a____,c_List_Olist_OCons(v_b____,c_List_Olist_OCons(V_c,c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt)
| v_thesis____ ),
inference(skolemisation,[status(esa)],[f600_nnf]) ).
cnf(c600,plain,
( ~ c_List_Odistinct(c_List_Olist_OCons(v_a____,c_List_Olist_OCons(v_b____,c_List_Olist_OCons(X0,c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt)
| v_thesis____ ),
inference(cnf_transformation,[status(esa)],[f600_sk]) ).
cnf(t89,plain,
ifeq(c_List_Odistinct(c_List_Olist_OCons(v_a____,c_List_Olist_OCons(v_b____,c_List_Olist_OCons(X1,c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),true,v_thesis____,true) = true,
inference(equality_encoding,[status(esa)],[c600]) ).
cnf(f435,axiom,
c_List_Olist_OCons(V_x,c_List_Oappend(V_xs1,V_zs,T_a),T_a) = c_List_Oappend(c_List_Olist_OCons(V_x,V_xs1,T_a),V_zs,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Cons__eq__appendI_0) ).
fof(f435_nnf,plain,
! [V_x,V_xs1,V_zs,T_a] : c_List_Olist_OCons(V_x,c_List_Oappend(V_xs1,V_zs,T_a),T_a) = c_List_Oappend(c_List_Olist_OCons(V_x,V_xs1,T_a),V_zs,T_a),
inference(nnf_transformation,[status(thm)],[f435]) ).
fof(f435_sk,plain,
! [V_x,V_xs1,V_zs,T_a] : c_List_Olist_OCons(V_x,c_List_Oappend(V_xs1,V_zs,T_a),T_a) = c_List_Oappend(c_List_Olist_OCons(V_x,V_xs1,T_a),V_zs,T_a),
inference(skolemisation,[status(esa)],[f435_nnf]) ).
cnf(c435,plain,
c_List_Olist_OCons(X0,c_List_Oappend(X1,X2,X3),X3) = c_List_Oappend(c_List_Olist_OCons(X0,X1,X3),X2,X3),
inference(cnf_transformation,[status(esa)],[f435_sk]) ).
cnf(t84,plain,
c_List_Olist_OCons(X1,c_List_Oappend(X2,X3,X4),X4) = c_List_Oappend(c_List_Olist_OCons(X1,X2,X4),X3,X4),
inference(equality_encoding,[status(esa)],[c435]) ).
cnf(t183,plain,
c_List_Oappend(c_List_Olist_OCons(X1,X2,X3),X4,X3) = c_List_Olist_OCons(X1,c_List_Oappend(X2,X4,X3),X3),
inference(orient,[status(thm)],[t84]) ).
cnf(t104,axiom,
sF3(X1) = c_List_Olist_OCons(v_b____,c_List_Olist_OCons(X1,c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition) ).
cnf(t102,axiom,
sF1 = c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition) ).
cnf(t109,plain,
c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt) = sF1,
inference(orient,[status(thm)],[t102]) ).
cnf(t1324,plain,
sF3(X1) = c_List_Olist_OCons(v_b____,c_List_Olist_OCons(X1,sF1,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),
inference(step,[status(thm)],[t104,t109]) ).
cnf(t103,axiom,
sF2(X1) = c_List_Olist_OCons(X1,c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition) ).
cnf(t1300,plain,
sF2(X1) = c_List_Olist_OCons(X1,sF1,tc_Arrow__Order__Mirabelle_Oalt),
inference(step,[status(thm)],[t103,t109]) ).
cnf(t143,plain,
c_List_Olist_OCons(X1,sF1,tc_Arrow__Order__Mirabelle_Oalt) = sF2(X1),
inference(orient,[status(thm)],[t1300]) ).
cnf(t1325,plain,
sF3(X1) = c_List_Olist_OCons(v_b____,sF2(X1),tc_Arrow__Order__Mirabelle_Oalt),
inference(step,[status(thm)],[t1324,t143]) ).
cnf(t194,plain,
c_List_Olist_OCons(v_b____,sF2(X1),tc_Arrow__Order__Mirabelle_Oalt) = sF3(X1),
inference(orient,[status(thm)],[t1325]) ).
cnf(t199,plain,
c_List_Olist_OCons(v_b____,c_List_Oappend(sF2(X1),X2,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt) = c_List_Oappend(sF3(X1),X2,tc_Arrow__Order__Mirabelle_Oalt),
inference(cp,[status(thm)],[t183,t194]) ).
cnf(t184,plain,
c_List_Olist_OCons(X1,c_List_Oappend(sF1,X2,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt) = c_List_Oappend(sF2(X1),X2,tc_Arrow__Order__Mirabelle_Oalt),
inference(cp,[status(thm)],[t183,t143]) ).
cnf(f546,axiom,
V_ys = c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_self__append__conv2_1) ).
fof(f546_nnf,plain,
! [V_ys,T_a] : V_ys = c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a),
inference(nnf_transformation,[status(thm)],[f546]) ).
fof(f546_sk,plain,
! [V_ys,T_a] : V_ys = c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a),
inference(skolemisation,[status(esa)],[f546_nnf]) ).
cnf(c546,plain,
X0 = c_List_Oappend(c_List_Olist_ONil(X1),X0,X1),
inference(cnf_transformation,[status(esa)],[f546_sk]) ).
cnf(t14,plain,
c_List_Oappend(c_List_Olist_ONil(X1),X2,X1) = X2,
inference(equality_encoding,[status(esa)],[c546]) ).
cnf(t124,plain,
c_List_Oappend(c_List_Olist_ONil(X1),X2,X1) = X2,
inference(orient,[status(thm)],[t14]) ).
cnf(t125,plain,
X1 = c_List_Oappend(sF1,X1,tc_Arrow__Order__Mirabelle_Oalt),
inference(cp,[status(thm)],[t124,t109]) ).
cnf(t126,plain,
c_List_Oappend(sF1,X1,tc_Arrow__Order__Mirabelle_Oalt) = X1,
inference(orient,[status(thm)],[t125]) ).
cnf(t1316,plain,
c_List_Olist_OCons(X1,X2,tc_Arrow__Order__Mirabelle_Oalt) = c_List_Oappend(sF2(X1),X2,tc_Arrow__Order__Mirabelle_Oalt),
inference(step,[status(thm)],[t184,t126]) ).
cnf(t185,plain,
c_List_Oappend(sF2(X1),X2,tc_Arrow__Order__Mirabelle_Oalt) = c_List_Olist_OCons(X1,X2,tc_Arrow__Order__Mirabelle_Oalt),
inference(orient,[status(thm)],[t1316]) ).
cnf(t1329,plain,
c_List_Olist_OCons(v_b____,c_List_Olist_OCons(X1,X2,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt) = c_List_Oappend(sF3(X1),X2,tc_Arrow__Order__Mirabelle_Oalt),
inference(step,[status(thm)],[t199,t185]) ).
cnf(t214,plain,
c_List_Olist_OCons(v_b____,c_List_Olist_OCons(X1,X2,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt) = c_List_Oappend(sF3(X1),X2,tc_Arrow__Order__Mirabelle_Oalt),
inference(orient,[status(thm)],[t1329]) ).
cnf(t1487,plain,
ifeq(c_List_Odistinct(c_List_Olist_OCons(v_a____,c_List_Oappend(sF3(X1),c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),true,v_thesis____,true) = true,
inference(step,[status(thm)],[t89,t214]) ).
cnf(t105,axiom,
sF4(X1) = c_List_Olist_OCons(v_a____,c_List_Olist_OCons(v_b____,c_List_Olist_OCons(X1,c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition) ).
cnf(t1467,plain,
sF4(X1) = c_List_Olist_OCons(v_a____,c_List_Oappend(sF3(X1),c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),
inference(step,[status(thm)],[t105,t214]) ).
cnf(f548,axiom,
V_xs = c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_self__append__conv_1) ).
fof(f548_nnf,plain,
! [V_xs,T_a] : V_xs = c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f548]) ).
fof(f548_sk,plain,
! [V_xs,T_a] : V_xs = c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f548_nnf]) ).
cnf(c548,plain,
X0 = c_List_Oappend(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f548_sk]) ).
cnf(t12,plain,
c_List_Oappend(X1,c_List_Olist_ONil(X2),X2) = X1,
inference(equality_encoding,[status(esa)],[c548]) ).
cnf(t121,plain,
c_List_Oappend(X1,c_List_Olist_ONil(X2),X2) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t1468,plain,
sF4(X1) = c_List_Olist_OCons(v_a____,sF3(X1),tc_Arrow__Order__Mirabelle_Oalt),
inference(step,[status(thm)],[t1467,t121]) ).
cnf(t678,plain,
c_List_Olist_OCons(v_a____,sF3(X1),tc_Arrow__Order__Mirabelle_Oalt) = sF4(X1),
inference(orient,[status(thm)],[t1468]) ).
cnf(t683,plain,
c_List_Olist_OCons(v_a____,c_List_Oappend(sF3(X1),X2,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt) = c_List_Oappend(sF4(X1),X2,tc_Arrow__Order__Mirabelle_Oalt),
inference(cp,[status(thm)],[t183,t678]) ).
cnf(t779,plain,
c_List_Olist_OCons(v_a____,c_List_Oappend(sF3(X1),X2,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt) = c_List_Oappend(sF4(X1),X2,tc_Arrow__Order__Mirabelle_Oalt),
inference(orient,[status(thm)],[t683]) ).
cnf(t1488,plain,
ifeq(c_List_Odistinct(c_List_Oappend(sF4(X1),c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),true,v_thesis____,true) = true,
inference(step,[status(thm)],[t1487,t779]) ).
cnf(t1489,plain,
ifeq(c_List_Odistinct(sF4(X1),tc_Arrow__Order__Mirabelle_Oalt),true,v_thesis____,true) = true,
inference(step,[status(thm)],[t1488,t121]) ).
cnf(t1490,plain,
ifeq(c_List_Odistinct(sF4(X1),tc_Arrow__Order__Mirabelle_Oalt),sF0,v_thesis____,true) = true,
inference(step,[status(thm)],[t1489,t130]) ).
cnf(t1491,plain,
ifeq(c_List_Odistinct(sF4(X1),tc_Arrow__Order__Mirabelle_Oalt),sF0,v_thesis____,sF0) = true,
inference(step,[status(thm)],[t1490,t130]) ).
cnf(t1492,plain,
ifeq(c_List_Odistinct(sF4(X1),tc_Arrow__Order__Mirabelle_Oalt),sF0,v_thesis____,sF0) = sF0,
inference(step,[status(thm)],[t1491,t130]) ).
cnf(t823,plain,
ifeq(c_List_Odistinct(sF4(X1),tc_Arrow__Order__Mirabelle_Oalt),sF0,v_thesis____,sF0) = sF0,
inference(orient,[status(thm)],[t1492]) ).
cnf(f595,axiom,
( V_a = V_b
| c_List_Odistinct(c_List_Olist_OCons(V_a,c_List_Olist_OCons(V_b,c_List_Olist_OCons(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(V_a,V_b),c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_third__alt_0) ).
fof(f595_nnf,plain,
! [V_a,V_b] :
( V_a = V_b
| c_List_Odistinct(c_List_Olist_OCons(V_a,c_List_Olist_OCons(V_b,c_List_Olist_OCons(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(V_a,V_b),c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt) ),
inference(nnf_transformation,[status(thm)],[f595]) ).
fof(f595_sk,plain,
! [V_a,V_b] :
( V_a = V_b
| c_List_Odistinct(c_List_Olist_OCons(V_a,c_List_Olist_OCons(V_b,c_List_Olist_OCons(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(V_a,V_b),c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt) ),
inference(skolemisation,[status(esa)],[f595_nnf]) ).
cnf(c595,plain,
( X0 = X1
| c_List_Odistinct(c_List_Olist_OCons(X0,c_List_Olist_OCons(X1,c_List_Olist_OCons(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(X0,X1),c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt) ),
inference(cnf_transformation,[status(esa)],[f595_sk]) ).
cnf(t96,plain,
or(c_List_Odistinct(c_List_Olist_OCons(X1,c_List_Olist_OCons(X2,c_List_Olist_OCons(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(X1,X2),c_List_Olist_ONil(tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),eq(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c595]) ).
cnf(t1564,plain,
or(c_List_Odistinct(c_List_Olist_OCons(X1,c_List_Olist_OCons(X2,c_List_Olist_OCons(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(X1,X2),sF1,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),eq(X1,X2)) = true,
inference(step,[status(thm)],[t96,t109]) ).
cnf(t1565,plain,
or(c_List_Odistinct(c_List_Olist_OCons(X1,c_List_Olist_OCons(X2,sF2(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(X1,X2)),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),eq(X1,X2)) = true,
inference(step,[status(thm)],[t1564,t143]) ).
cnf(t1566,plain,
or(c_List_Odistinct(c_List_Olist_OCons(X1,c_List_Olist_OCons(X2,sF2(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(X1,X2)),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),eq(X1,X2)) = sF0,
inference(step,[status(thm)],[t1565,t130]) ).
cnf(t1125,plain,
or(c_List_Odistinct(c_List_Olist_OCons(X1,c_List_Olist_OCons(X2,sF2(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(X1,X2)),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),eq(X1,X2)) = sF0,
inference(orient,[status(thm)],[t1566]) ).
cnf(f607,axiom,
v_a____ != v_b____,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f607_nnf,plain,
v_a____ != v_b____,
inference(nnf_transformation,[status(thm)],[f607]) ).
fof(f607_sk,plain,
v_a____ != v_b____,
inference(skolemisation,[status(esa)],[f607_nnf]) ).
cnf(c607,plain,
v_a____ != v_b____,
inference(cnf_transformation,[status(esa)],[f607_sk]) ).
cnf(t2,plain,
eq(v_a____,v_b____) = false,
inference(equality_encoding,[status(esa)],[c607]) ).
cnf(t1283,plain,
eq(v_a____,v_b____) = v_thesis____,
inference(step,[status(thm)],[t2,t108]) ).
cnf(t111,plain,
eq(v_a____,v_b____) = v_thesis____,
inference(orient,[status(thm)],[t1283]) ).
cnf(t1126,plain,
sF0 = or(c_List_Odistinct(c_List_Olist_OCons(v_a____,c_List_Olist_OCons(v_b____,sF2(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(v_a____,v_b____)),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),v_thesis____),
inference(cp,[status(thm)],[t1125,t111]) ).
cnf(t3,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t1284,plain,
or(X1,v_thesis____) = X1,
inference(step,[status(thm)],[t3,t108]) ).
cnf(t112,plain,
or(X1,v_thesis____) = X1,
inference(orient,[status(thm)],[t1284]) ).
cnf(t1567,plain,
sF0 = c_List_Odistinct(c_List_Olist_OCons(v_a____,c_List_Olist_OCons(v_b____,sF2(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(v_a____,v_b____)),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),
inference(step,[status(thm)],[t1126,t112]) ).
cnf(t1568,plain,
sF0 = c_List_Odistinct(c_List_Olist_OCons(v_a____,sF3(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(v_a____,v_b____)),tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt),
inference(step,[status(thm)],[t1567,t194]) ).
cnf(t1569,plain,
sF0 = c_List_Odistinct(sF4(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(v_a____,v_b____)),tc_Arrow__Order__Mirabelle_Oalt),
inference(step,[status(thm)],[t1568,t678]) ).
cnf(t1155,plain,
c_List_Odistinct(sF4(v_sko__Arrow__Order__Mirabelle__Xthird__alt__1(v_a____,v_b____)),tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(orient,[status(thm)],[t1569]) ).
cnf(t1159,plain,
sF0 = ifeq(sF0,sF0,v_thesis____,sF0),
inference(cp,[status(thm)],[t823,t1155]) ).
cnf(t17,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t127,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t17]) ).
cnf(t1570,plain,
sF0 = v_thesis____,
inference(step,[status(thm)],[t1159,t127]) ).
cnf(t1160,plain,
v_thesis____ = sF0,
inference(orient,[status(thm)],[t1570]) ).
cnf(t1571,plain,
false = sF0,
inference(step,[status(thm)],[t108,t1160]) ).
cnf(t1161,plain,
false = sF0,
inference(orient,[status(thm)],[t1571]) ).
cnf(f10,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f10_nnf,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(f11,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f11_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(f14,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f14_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)],[f14]) ).
fof(f14_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)],[f14_nnf]) ).
cnf(c14,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f16,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f16_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)],[f16]) ).
fof(f16_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)],[f16_nnf]) ).
cnf(c16,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(f18,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f18_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)],[f18]) ).
fof(f18_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)],[f18_nnf]) ).
cnf(c18,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(f20,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f20_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)],[f20]) ).
fof(f20_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)],[f20_nnf]) ).
cnf(c20,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(f34,axiom,
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f34_nnf,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( ~ c_HOL_Oord__class_Oless(X1,c_Suc(X0),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(f57,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_length__greater__0__conv_0) ).
fof(f57_nnf,plain,
! [T_a] : ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
! [T_a] : ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c57,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(X0),tc_List_Olist(X0)),tc_nat),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(f82,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f82_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c82,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(f83,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f83_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c83,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(f84,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f84_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)],[f84]) ).
fof(f84_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)],[f84_nnf]) ).
cnf(c84,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(f85,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f85_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)],[f85]) ).
fof(f85_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)],[f85_nnf]) ).
cnf(c85,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
cnf(f86,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f86_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)],[f86]) ).
fof(f86_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)],[f86_nnf]) ).
cnf(c86,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f86_sk]) ).
cnf(f106,axiom,
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_le__number__of__eq__not__less_0) ).
fof(f106_nnf,plain,
! [T_a,V_w,V_v] :
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f106]) ).
fof(f106_sk,plain,
! [T_a,V_w,V_v] :
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f106_nnf]) ).
cnf(c106,plain,
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(X2,X0),c_Int_Onumber__class_Onumber__of(X1,X0),X0)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(X1,X0),c_Int_Onumber__class_Onumber__of(X2,X0),X0)
| ~ class_Int_Onumber(X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f106_sk]) ).
cnf(f109,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
fof(f109_nnf,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f109]) ).
fof(f109_sk,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f109_nnf]) ).
cnf(c109,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f109_sk]) ).
cnf(f115,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__add__less1_0) ).
fof(f115_nnf,plain,
! [V_i,V_j] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f115]) ).
fof(f115_sk,plain,
! [V_i,V_j] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f115_nnf]) ).
cnf(c115,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f115_sk]) ).
cnf(f116,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__add__less2_0) ).
fof(f116_nnf,plain,
! [V_j,V_i] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f116]) ).
fof(f116_sk,plain,
! [V_j,V_i] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f116_nnf]) ).
cnf(c116,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat),
inference(cnf_transformation,[status(esa)],[f116_sk]) ).
cnf(f149,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f149_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)],[f149]) ).
fof(f149_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)],[f149_nnf]) ).
cnf(c149,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)],[f149_sk]) ).
cnf(f150,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f150_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)],[f150]) ).
fof(f150_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)],[f150_nnf]) ).
cnf(c150,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)],[f150_sk]) ).
cnf(f151,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f151_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)],[f151]) ).
fof(f151_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)],[f151_nnf]) ).
cnf(c151,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)],[f151_sk]) ).
cnf(f152,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f152_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)],[f152]) ).
fof(f152_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)],[f152_nnf]) ).
cnf(c152,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)],[f152_sk]) ).
cnf(f153,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__one__less__zero_0) ).
fof(f153_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f153]) ).
fof(f153_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f153_nnf]) ).
cnf(c153,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f153_sk]) ).
cnf(f193,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f193_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f193]) ).
fof(f193_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f193_nnf]) ).
cnf(c193,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f193_sk]) ).
cnf(f194,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f194_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f194]) ).
fof(f194_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c194,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
cnf(f238,axiom,
c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
fof(f238_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f238]) ).
fof(f238_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f238_nnf]) ).
cnf(c238,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
cnf(f239,axiom,
c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__neq__Zero_0) ).
fof(f239_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f239]) ).
fof(f239_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f239_nnf]) ).
cnf(c239,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f239_sk]) ).
cnf(f257,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f257_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f257]) ).
fof(f257_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f257_nnf]) ).
cnf(c257,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f257_sk]) ).
cnf(f258,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f258_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f258]) ).
fof(f258_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f258_nnf]) ).
cnf(c258,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f258_sk]) ).
cnf(f284,axiom,
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_power__eq__0__iff_1) ).
fof(f284_nnf,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f284]) ).
fof(f284_sk,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f284_nnf]) ).
cnf(c284,plain,
( c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Power_Opower(X0)
| ~ class_Ring__and__Field_Omult__zero(X0)
| ~ class_Ring__and__Field_Ono__zero__divisors(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f284_sk]) ).
cnf(f289,axiom,
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__one__le__zero_0) ).
fof(f289_nnf,plain,
! [T_a] :
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f289]) ).
fof(f289_sk,plain,
! [T_a] :
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f289_nnf]) ).
cnf(c289,plain,
( ~ c_lessequals(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f289_sk]) ).
cnf(f448,axiom,
~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_List_Onull_Osimps_I2_J_0) ).
fof(f448_nnf,plain,
! [V_x,V_xs,T_a] : ~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
inference(nnf_transformation,[status(thm)],[f448]) ).
fof(f448_sk,plain,
! [V_x,V_xs,T_a] : ~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
inference(skolemisation,[status(esa)],[f448_nnf]) ).
cnf(c448,plain,
~ c_List_Onull(c_List_Olist_OCons(X0,X1,X2),X2),
inference(cnf_transformation,[status(esa)],[f448_sk]) ).
cnf(f464,axiom,
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f464_nnf,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f464]) ).
fof(f464_sk,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f464_nnf]) ).
cnf(c464,plain,
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f464_sk]) ).
cnf(f479,axiom,
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f479_nnf,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f479]) ).
fof(f479_sk,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f479_nnf]) ).
cnf(c479,plain,
( c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f479_sk]) ).
cnf(f538,axiom,
~ c_List_Omember(V_x,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_List_Omember_Osimps_I1_J_0) ).
fof(f538_nnf,plain,
! [V_x,T_a] : ~ c_List_Omember(V_x,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f538]) ).
fof(f538_sk,plain,
! [V_x,T_a] : ~ c_List_Omember(V_x,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f538_nnf]) ).
cnf(c538,plain,
~ c_List_Omember(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f538_sk]) ).
cnf(f599,axiom,
c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).
fof(f599_nnf,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(nnf_transformation,[status(thm)],[f599]) ).
fof(f599_sk,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(skolemisation,[status(esa)],[f599_nnf]) ).
cnf(c599,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f599_sk]) ).
cnf(f601,axiom,
c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).
fof(f601_nnf,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f601]) ).
fof(f601_sk,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f601_nnf]) ).
cnf(c601,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f601_sk]) ).
cnf(f602,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).
fof(f602_nnf,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f602]) ).
fof(f602_sk,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f602_nnf]) ).
cnf(c602,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f602_sk]) ).
cnf(f603,axiom,
c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).
fof(f603_nnf,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(nnf_transformation,[status(thm)],[f603]) ).
fof(f603_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f603_nnf]) ).
cnf(c603,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f603_sk]) ).
cnf(f604,axiom,
V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f604_nnf,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(nnf_transformation,[status(thm)],[f604]) ).
fof(f604_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f604_nnf]) ).
cnf(c604,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c10,c11,c14,c16,c18,c20,c34,c57,c82,c83,c84,c85,c86,c106,c109,c115,c116,c149,c150,c151,c152,c153,c193,c194,c238,c239,c257,c258,c284,c289,c448,c464,c479,c538,c599,c601,c602,c603,c604,c607,c608]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t130]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t1161]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT042-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.40 % Computer : n019.cluster.edu
% 0.17/0.40 % Model : x86_64 x86_64
% 0.17/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.40 % Memory : 8046.5625MB
% 0.17/0.40 % OS : Linux 6.8.0-71-generic
% 0.17/0.40 % CPULimit : 300
% 0.17/0.40 % WCLimit : 300
% 0.17/0.40 % DateTime : Thu Sep 24 08:37:34 UTC 2026
% 0.17/0.41 % CPUTime :
% 0.17/0.41 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 23.50/3.48 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.50/3.48 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------