%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV860-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:14:15 PM UTC 2026
% Result : Unsatisfiable 7.24s 1.51s
% Output : Proof 7.24s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t132,axiom,
sF0 = c_Natural_Oevaln(c_Com_Ocom_OSKIP,v_xa,v_n,v_xb),
introduced(definition) ).
cnf(f485,negated_conjecture,
c_Natural_Oevaln(c_Com_Ocom_OSKIP,v_xa,v_n,v_xb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f485_nnf,plain,
c_Natural_Oevaln(c_Com_Ocom_OSKIP,v_xa,v_n,v_xb),
inference(nnf_transformation,[status(thm)],[f485]) ).
cnf(c485,plain,
c_Natural_Oevaln(c_Com_Ocom_OSKIP,v_xa,v_n,v_xb),
inference(cnf_transformation,[status(esa)],[f485_nnf]) ).
cnf(t15,plain,
c_Natural_Oevaln(c_Com_Ocom_OSKIP,v_xa,v_n,v_xb) = true,
inference(equality_encoding,[status(esa)],[c485]) ).
cnf(t165,plain,
c_Natural_Oevaln(c_Com_Ocom_OSKIP,v_xa,v_n,v_xb) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t344,plain,
sF0 = true,
inference(step,[status(thm)],[t132,t165]) ).
cnf(t172,plain,
true = sF0,
inference(orient,[status(thm)],[t344]) ).
cnf(t137,axiom,
sF5 = hBOOL(hAPP(hAPP(v_P,v_x),v_xb)),
introduced(definition) ).
cnf(t133,axiom,
sF1 = hAPP(v_P,v_x),
introduced(definition) ).
cnf(t158,plain,
hAPP(v_P,v_x) = sF1,
inference(orient,[status(thm)],[t133]) ).
cnf(t381,plain,
sF5 = hBOOL(hAPP(sF1,v_xb)),
inference(step,[status(thm)],[t137,t158]) ).
cnf(t136,axiom,
sF4 = hAPP(hAPP(v_P,v_x),v_xb),
introduced(definition) ).
cnf(t366,plain,
sF4 = hAPP(sF1,v_xb),
inference(step,[status(thm)],[t136,t158]) ).
cnf(t196,plain,
hAPP(sF1,v_xb) = sF4,
inference(orient,[status(thm)],[t366]) ).
cnf(t382,plain,
sF5 = hBOOL(sF4),
inference(step,[status(thm)],[t381,t196]) ).
cnf(f486,negated_conjecture,
~ hBOOL(hAPP(hAPP(v_P,v_x),v_xb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f486_nnf,plain,
~ hBOOL(hAPP(hAPP(v_P,v_x),v_xb)),
inference(nnf_transformation,[status(thm)],[f486]) ).
fof(f486_sk,plain,
~ hBOOL(hAPP(hAPP(v_P,v_x),v_xb)),
inference(skolemisation,[status(esa)],[f486_nnf]) ).
cnf(c486,plain,
~ hBOOL(hAPP(hAPP(v_P,v_x),v_xb)),
inference(cnf_transformation,[status(esa)],[f486_sk]) ).
cnf(t27,plain,
hBOOL(hAPP(hAPP(v_P,v_x),v_xb)) = false,
inference(equality_encoding,[status(esa)],[c486]) ).
cnf(t372,plain,
hBOOL(hAPP(sF1,v_xb)) = false,
inference(step,[status(thm)],[t27,t158]) ).
cnf(t373,plain,
hBOOL(sF4) = false,
inference(step,[status(thm)],[t372,t196]) ).
cnf(t203,plain,
hBOOL(sF4) = false,
inference(orient,[status(thm)],[t373]) ).
cnf(t383,plain,
sF5 = false,
inference(step,[status(thm)],[t382,t203]) ).
cnf(t207,plain,
false = sF5,
inference(orient,[status(thm)],[t383]) ).
cnf(t404,plain,
hBOOL(sF4) = sF5,
inference(step,[status(thm)],[t203,t207]) ).
cnf(t228,plain,
hBOOL(sF4) = sF5,
inference(orient,[status(thm)],[t404]) ).
cnf(t285,plain,
hBOOL(sF2) = sF5,
inference(rw,[status(thm)],[t228]) ).
cnf(f484,negated_conjecture,
hBOOL(hAPP(hAPP(v_P,v_x),v_xa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f484_nnf,plain,
hBOOL(hAPP(hAPP(v_P,v_x),v_xa)),
inference(nnf_transformation,[status(thm)],[f484]) ).
cnf(c484,plain,
hBOOL(hAPP(hAPP(v_P,v_x),v_xa)),
inference(cnf_transformation,[status(esa)],[f484_nnf]) ).
cnf(t26,plain,
hBOOL(hAPP(hAPP(v_P,v_x),v_xa)) = true,
inference(equality_encoding,[status(esa)],[c484]) ).
cnf(t369,plain,
hBOOL(hAPP(sF1,v_xa)) = true,
inference(step,[status(thm)],[t26,t158]) ).
cnf(t134,axiom,
sF2 = hAPP(hAPP(v_P,v_x),v_xa),
introduced(definition) ).
cnf(t365,plain,
sF2 = hAPP(sF1,v_xa),
inference(step,[status(thm)],[t134,t158]) ).
cnf(t195,plain,
hAPP(sF1,v_xa) = sF2,
inference(orient,[status(thm)],[t365]) ).
cnf(t370,plain,
hBOOL(sF2) = true,
inference(step,[status(thm)],[t369,t195]) ).
cnf(t371,plain,
hBOOL(sF2) = sF0,
inference(step,[status(thm)],[t370,t172]) ).
cnf(t202,plain,
hBOOL(sF2) = sF0,
inference(orient,[status(thm)],[t371]) ).
cnf(t457,plain,
sF0 = sF5,
inference(step,[status(thm)],[t285,t202]) ).
cnf(t287,plain,
sF5 = sF0,
inference(orient,[status(thm)],[t457]) ).
cnf(t476,plain,
false = sF0,
inference(step,[status(thm)],[t207,t287]) ).
cnf(t306,plain,
false = sF0,
inference(orient,[status(thm)],[t476]) ).
cnf(f4,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I39_J_0) ).
fof(f4_nnf,plain,
! [V_fun_H,V_com_H,V_loc,V_fun,V_com] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [V_fun_H,V_com_H,V_loc,V_fun,V_com] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(f7,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I41_J_0) ).
fof(f7_nnf,plain,
! [V_pname_H,V_loc,V_fun,V_com] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [V_pname_H,V_loc,V_fun,V_com] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OLocal(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(f8,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I59_J_0) ).
fof(f8_nnf,plain,
! [V_pname_H,V_fun,V_com] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [V_pname_H,V_fun,V_com] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OWhile(X1,X2),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(f16,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I24_J_0) ).
fof(f16_nnf,plain,
! [V_vname,V_fun,V_com1_H,V_com2_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [V_vname,V_fun,V_com1_H,V_com2_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(f17,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OBODY(V_pname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I63_J_0) ).
fof(f17_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_pname] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OBODY(V_pname),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_pname] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OBODY(V_pname),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OBODY(X3),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(f18,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I36_J_0) ).
fof(f18_nnf,plain,
! [V_loc,V_fun,V_com,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [V_loc,V_fun,V_com,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OCond(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(f21,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I56_J_0) ).
fof(f21_nnf,plain,
! [V_fun,V_com1,V_com2,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [V_fun,V_com1,V_com2,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OCall(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(f23,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I49_J_0) ).
fof(f23_nnf,plain,
! [V_pname_H,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [V_pname_H,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSemi(X1,X2),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(f37,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I51_J_0) ).
fof(f37_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_com1,V_com2] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_com1,V_com2] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(f45,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I48_J_0) ).
fof(f45_nnf,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(f83,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I32_J_0) ).
fof(f83_nnf,plain,
! [V_vname,V_fun,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [V_vname,V_fun,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c83,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(f85,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I30_J_0) ).
fof(f85_nnf,plain,
! [V_vname,V_fun,V_pname_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f85]) ).
fof(f85_sk,plain,
! [V_vname,V_fun,V_pname_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f85_nnf]) ).
cnf(c85,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
cnf(f89,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(f89_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)],[f89]) ).
fof(f89_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)],[f89_nnf]) ).
cnf(c89,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f89_sk]) ).
cnf(f92,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(f92_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)],[f92]) ).
fof(f92_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)],[f92_nnf]) ).
cnf(c92,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(f93,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(f93_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)],[f93]) ).
fof(f93_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)],[f93_nnf]) ).
cnf(c93,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
cnf(f94,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I35_J_0) ).
fof(f94_nnf,plain,
! [V_com1_H,V_com2_H,V_loc,V_fun,V_com] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f94]) ).
fof(f94_sk,plain,
! [V_com1_H,V_com2_H,V_loc,V_fun,V_com] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f94_nnf]) ).
cnf(c94,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(f99,axiom,
c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I23_J_0) ).
fof(f99_nnf,plain,
! [V_loc_H,V_fun_H,V_com_H,V_vname,V_fun] : c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f99]) ).
fof(f99_sk,plain,
! [V_loc_H,V_fun_H,V_com_H,V_vname,V_fun] : c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f99_nnf]) ).
cnf(c99,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f99_sk]) ).
cnf(f102,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I31_J_0) ).
fof(f102_nnf,plain,
! [V_pname_H,V_vname,V_fun] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f102]) ).
fof(f102_sk,plain,
! [V_pname_H,V_vname,V_fun] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f102_nnf]) ).
cnf(c102,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OAss(X1,X2),
inference(cnf_transformation,[status(esa)],[f102_sk]) ).
cnf(f103,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(f103_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)],[f103]) ).
fof(f103_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)],[f103_nnf]) ).
cnf(c103,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f103_sk]) ).
cnf(f105,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I37_J_0) ).
fof(f105_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_loc,V_fun,V_com] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f105]) ).
fof(f105_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_loc,V_fun,V_com] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f105_nnf]) ).
cnf(c105,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OLocal(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f105_sk]) ).
cnf(f110,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(f110_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)],[f110]) ).
fof(f110_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)],[f110_nnf]) ).
cnf(c110,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f110_sk]) ).
cnf(f117,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I57_J_0) ).
fof(f117_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f117]) ).
fof(f117_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(skolemisation,[status(esa)],[f117_nnf]) ).
cnf(c117,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OCond(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f117_sk]) ).
cnf(f124,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I28_J_0) ).
fof(f124_nnf,plain,
! [V_vname,V_fun,V_fun_H,V_com_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f124]) ).
fof(f124_sk,plain,
! [V_vname,V_fun,V_fun_H,V_com_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f124_nnf]) ).
cnf(c124,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f124_sk]) ).
cnf(f125,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I22_J_0) ).
fof(f125_nnf,plain,
! [V_vname,V_fun,V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f125]) ).
fof(f125_sk,plain,
! [V_vname,V_fun,V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f125_nnf]) ).
cnf(c125,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f125_sk]) ).
cnf(f131,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I54_J_0) ).
fof(f131_nnf,plain,
! [V_fun,V_com1,V_com2,V_pname_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f131]) ).
fof(f131_sk,plain,
! [V_fun,V_com1,V_com2,V_pname_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f131_nnf]) ).
cnf(c131,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OBODY(X3),
inference(cnf_transformation,[status(esa)],[f131_sk]) ).
cnf(f132,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I55_J_0) ).
fof(f132_nnf,plain,
! [V_pname_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f132]) ).
fof(f132_sk,plain,
! [V_pname_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(skolemisation,[status(esa)],[f132_nnf]) ).
cnf(c132,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OCond(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f132_sk]) ).
cnf(f139,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I38_J_0) ).
fof(f139_nnf,plain,
! [V_loc,V_fun,V_com,V_fun_H,V_com_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f139]) ).
fof(f139_sk,plain,
! [V_loc,V_fun,V_com,V_fun_H,V_com_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f139_nnf]) ).
cnf(c139,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f139_sk]) ).
cnf(f148,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I26_J_0) ).
fof(f148_nnf,plain,
! [V_vname,V_fun,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f148]) ).
fof(f148_sk,plain,
! [V_vname,V_fun,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f148_nnf]) ).
cnf(c148,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f148_sk]) ).
cnf(f149,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(f149_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)],[f149]) ).
fof(f149_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)],[f149_nnf]) ).
cnf(c149,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f149_sk]) ).
cnf(f152,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(f152_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)],[f152]) ).
fof(f152_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)],[f152_nnf]) ).
cnf(c152,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)],[f152_sk]) ).
cnf(f156,axiom,
c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I60_J_0) ).
fof(f156_nnf,plain,
! [V_fun,V_com,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f156]) ).
fof(f156_sk,plain,
! [V_fun,V_com,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f156_nnf]) ).
cnf(c156,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f156_sk]) ).
cnf(f157,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(f157_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)],[f157]) ).
fof(f157_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)],[f157_nnf]) ).
cnf(c157,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f157_sk]) ).
cnf(f158,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I25_J_0) ).
fof(f158_nnf,plain,
! [V_com1_H,V_com2_H,V_vname,V_fun] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f158]) ).
fof(f158_sk,plain,
! [V_com1_H,V_com2_H,V_vname,V_fun] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f158_nnf]) ).
cnf(c158,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OAss(X2,X3),
inference(cnf_transformation,[status(esa)],[f158_sk]) ).
cnf(f188,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I40_J_0) ).
fof(f188_nnf,plain,
! [V_loc,V_fun,V_com,V_pname_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f188]) ).
fof(f188_sk,plain,
! [V_loc,V_fun,V_com,V_pname_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f188_nnf]) ).
cnf(c188,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OBODY(X3),
inference(cnf_transformation,[status(esa)],[f188_sk]) ).
cnf(f189,axiom,
c_Com_Ocom_OBODY(V_pname) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I62_J_0) ).
fof(f189_nnf,plain,
! [V_pname,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OBODY(V_pname) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f189]) ).
fof(f189_sk,plain,
! [V_pname,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OBODY(V_pname) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f189_nnf]) ).
cnf(c189,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OCall(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f189_sk]) ).
cnf(f190,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I43_J_0) ).
fof(f190_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_loc,V_fun,V_com] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f190]) ).
fof(f190_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_loc,V_fun,V_com] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f190_nnf]) ).
cnf(c190,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OLocal(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f190_sk]) ).
cnf(f191,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(f191_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)],[f191]) ).
fof(f191_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)],[f191_nnf]) ).
cnf(c191,plain,
( ~ c_lessequals(c_Suc(X1),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f191_sk]) ).
cnf(f193,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OWhile(V_fun,V_com),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I61_J_0) ).
fof(f193_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_fun,V_com] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f193]) ).
fof(f193_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_fun,V_com] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(skolemisation,[status(esa)],[f193_nnf]) ).
cnf(c193,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f193_sk]) ).
cnf(f215,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I34_J_0) ).
fof(f215_nnf,plain,
! [V_loc,V_fun,V_com,V_com1_H,V_com2_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f215]) ).
fof(f215_sk,plain,
! [V_loc,V_fun,V_com,V_com1_H,V_com2_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f215_nnf]) ).
cnf(c215,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f215_sk]) ).
cnf(f238,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(f238_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)],[f238]) ).
fof(f238_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)],[f238_nnf]) ).
cnf(c238,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
cnf(f242,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I50_J_0) ).
fof(f242_nnf,plain,
! [V_com1,V_com2,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f242]) ).
fof(f242_sk,plain,
! [V_com1,V_com2,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f242_nnf]) ).
cnf(c242,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f242_sk]) ).
cnf(f244,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,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f244_nnf,plain,
! [T_b,V_f,V_a,V_A,T_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,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b))) ),
inference(nnf_transformation,[status(thm)],[f244]) ).
fof(f244_sk,plain,
! [T_b,V_f,V_a,V_A,T_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,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b))) ),
inference(skolemisation,[status(esa)],[f244_nnf]) ).
cnf(c244,plain,
( ~ c_Fun_Oinj__on(X1,c_Set_Oinsert(X2,X3,X4),X4,X0)
| ~ hBOOL(hAPP(hAPP(c_in(X0),hAPP(X1,X2)),c_Set_Oimage(X1,c_HOL_Ominus__class_Ominus(X3,c_Set_Oinsert(X2,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_bool)),X4),tc_fun(X4,tc_bool)),X4,X0))) ),
inference(cnf_transformation,[status(esa)],[f244_sk]) ).
cnf(f246,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I27_J_0) ).
fof(f246_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_vname,V_fun] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f246]) ).
fof(f246_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_vname,V_fun] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f246_nnf]) ).
cnf(c246,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f246_sk]) ).
cnf(f265,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(f265_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)],[f265]) ).
fof(f265_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)],[f265_nnf]) ).
cnf(c265,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f265_sk]) ).
cnf(f267,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(f267_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)],[f267]) ).
fof(f267_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)],[f267_nnf]) ).
cnf(c267,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f267_sk]) ).
cnf(f268,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(f268_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)],[f268]) ).
fof(f268_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)],[f268_nnf]) ).
cnf(c268,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f268_sk]) ).
cnf(f271,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f271_nnf,plain,
! [T_a,V_c,V_B,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
inference(nnf_transformation,[status(thm)],[f271]) ).
fof(f271_sk,plain,
! [T_a,V_c,V_B,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
inference(skolemisation,[status(esa)],[f271_nnf]) ).
cnf(c271,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_HOL_Ominus__class_Ominus(X3,X2,tc_fun(X0,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
cnf(f285,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I29_J_0) ).
fof(f285_nnf,plain,
! [V_fun_H,V_com_H,V_vname,V_fun] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f285]) ).
fof(f285_sk,plain,
! [V_fun_H,V_com_H,V_vname,V_fun] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f285_nnf]) ).
cnf(c285,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OAss(X2,X3),
inference(cnf_transformation,[status(esa)],[f285_sk]) ).
cnf(f287,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(f287_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)],[f287]) ).
fof(f287_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)],[f287_nnf]) ).
cnf(c287,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f287_sk]) ).
cnf(f305,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I33_J_0) ).
fof(f305_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_vname,V_fun] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f305]) ).
fof(f305_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H,V_vname,V_fun] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f305_nnf]) ).
cnf(c305,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f305_sk]) ).
cnf(f313,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(f313_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)],[f313]) ).
fof(f313_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)],[f313_nnf]) ).
cnf(c313,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f313_sk]) ).
cnf(f315,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(f315_nnf,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f315]) ).
fof(f315_sk,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f315_nnf]) ).
cnf(c315,plain,
~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f315_sk]) ).
cnf(f326,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(f326_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)],[f326]) ).
fof(f326_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)],[f326_nnf]) ).
cnf(c326,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f326_sk]) ).
cnf(f330,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f330_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f330]) ).
fof(f330_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f330_nnf]) ).
cnf(c330,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f330_sk]) ).
cnf(f331,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f331_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f331]) ).
fof(f331_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f331_nnf]) ).
cnf(c331,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f331_sk]) ).
cnf(f358,axiom,
c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I58_J_0) ).
fof(f358_nnf,plain,
! [V_fun,V_com,V_pname_H] : c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f358]) ).
fof(f358_sk,plain,
! [V_fun,V_com,V_pname_H] : c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f358_nnf]) ).
cnf(c358,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f358_sk]) ).
cnf(f374,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I42_J_0) ).
fof(f374_nnf,plain,
! [V_loc,V_fun,V_com,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f374]) ).
fof(f374_sk,plain,
! [V_loc,V_fun,V_com,V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f374_nnf]) ).
cnf(c374,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OCall(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f374_sk]) ).
cnf(f387,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(f387_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)],[f387]) ).
fof(f387_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)],[f387_nnf]) ).
cnf(c387,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)],[f387_sk]) ).
cnf(f437,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(f437_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)],[f437]) ).
fof(f437_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)],[f437_nnf]) ).
cnf(c437,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f437_sk]) ).
cnf(f438,axiom,
c_Com_Ocom_OAss(V_vname_H,V_fun_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I9_J_0) ).
fof(f438_nnf,plain,
! [V_vname_H,V_fun_H] : c_Com_Ocom_OAss(V_vname_H,V_fun_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f438]) ).
fof(f438_sk,plain,
! [V_vname_H,V_fun_H] : c_Com_Ocom_OAss(V_vname_H,V_fun_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f438_nnf]) ).
cnf(c438,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f438_sk]) ).
cnf(f439,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I19_J_0) ).
fof(f439_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f439]) ).
fof(f439_sk,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f439_nnf]) ).
cnf(c439,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f439_sk]) ).
cnf(f440,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I21_J_0) ).
fof(f440_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f440]) ).
fof(f440_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f440_nnf]) ).
cnf(c440,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f440_sk]) ).
cnf(f441,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I20_J_0) ).
fof(f441_nnf,plain,
! [V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f441]) ).
fof(f441_sk,plain,
! [V_vname_H,V_pname_H,V_fun_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f441_nnf]) ).
cnf(c441,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f441_sk]) ).
cnf(f442,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(f442_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)],[f442]) ).
fof(f442_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)],[f442_nnf]) ).
cnf(c442,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f442_sk]) ).
cnf(f443,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(V_vname_H,V_fun_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I8_J_0) ).
fof(f443_nnf,plain,
! [V_vname_H,V_fun_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(V_vname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f443]) ).
fof(f443_sk,plain,
! [V_vname_H,V_fun_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(V_vname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f443_nnf]) ).
cnf(c443,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(X0,X1),
inference(cnf_transformation,[status(esa)],[f443_sk]) ).
cnf(f444,axiom,
c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I11_J_0) ).
fof(f444_nnf,plain,
! [V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f444]) ).
fof(f444_sk,plain,
! [V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f444_nnf]) ).
cnf(c444,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f444_sk]) ).
cnf(f446,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I10_J_0) ).
fof(f446_nnf,plain,
! [V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f446]) ).
fof(f446_sk,plain,
! [V_loc_H,V_fun_H,V_com_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f446_nnf]) ).
cnf(c446,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f446_sk]) ).
cnf(f447,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(f447_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)],[f447]) ).
fof(f447_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)],[f447_nnf]) ).
cnf(c447,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(X0,X1),
inference(cnf_transformation,[status(esa)],[f447_sk]) ).
cnf(f449,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(f449_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)],[f449]) ).
fof(f449_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)],[f449_nnf]) ).
cnf(c449,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f449_sk]) ).
cnf(f452,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(f452_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)],[f452]) ).
fof(f452_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)],[f452_nnf]) ).
cnf(c452,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f452_sk]) ).
cnf(f453,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(f453_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)],[f453]) ).
fof(f453_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)],[f453_nnf]) ).
cnf(c453,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f453_sk]) ).
cnf(f454,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I18_J_0) ).
fof(f454_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f454]) ).
fof(f454_sk,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f454_nnf]) ).
cnf(c454,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(X0),
inference(cnf_transformation,[status(esa)],[f454_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c4,c7,c8,c16,c17,c18,c21,c23,c37,c45,c83,c85,c89,c92,c93,c94,c99,c102,c103,c105,c110,c117,c124,c125,c131,c132,c139,c148,c149,c152,c156,c157,c158,c188,c189,c190,c191,c193,c215,c238,c242,c244,c246,c265,c267,c268,c271,c285,c287,c305,c313,c315,c326,c330,c331,c358,c374,c387,c437,c438,c439,c440,c441,c442,c443,c444,c446,c447,c449,c452,c453,c454,c486]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t172]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t306]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV860-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 21:08:52 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.24/1.51 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.24/1.51 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------