%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV897-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 : n013.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:25 PM UTC 2026
% Result : Unsatisfiable 43.23s 5.96s
% Output : Proof 43.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 80
% Syntax : Number of formulae : 330 ( 314 unt; 0 def)
% Number of atoms : 346 ( 290 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 342 ( 326 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 32 ( 32 usr; 12 con; 0-4 aty)
% Number of variables : 1084 ( 488 sgn 536 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f430,axiom,
( ~ hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_pn))),V_s0),V_s1))
| hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,V_pn)),V_s0),V_s1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_evalc_OBody_0) ).
fof(f430_nnf,plain,
! [V_pn,V_s0,V_s1] :
( ~ hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_pn))),V_s0),V_s1))
| hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,V_pn)),V_s0),V_s1)) ),
inference(nnf_transformation,[status(thm)],[f430]) ).
fof(f430_sk,plain,
! [V_pn,V_s0,V_s1] :
( ~ hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_pn))),V_s0),V_s1))
| hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,V_pn)),V_s0),V_s1)) ),
inference(skolemisation,[status(esa)],[f430_nnf]) ).
cnf(c430,plain,
( ~ hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X0))),X1),X2))
| hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,X0)),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f430_sk]) ).
cnf(t174,plain,
ifeq(hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X1))),X2),X3)),true,hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,X1)),X2),X3)),true) = true,
inference(equality_encoding,[status(esa)],[c430]) ).
cnf(t268,plain,
ifeq(hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X1))),X2),X3)),true,hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,X1)),X2),X3)),true) = true,
inference(orient,[status(thm)],[t174]) ).
cnf(f461,negated_conjecture,
~ hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,v_pn)),v_x),v_xa)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f461_nnf,plain,
~ hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,v_pn)),v_x),v_xa)),
inference(nnf_transformation,[status(thm)],[f461]) ).
fof(f461_sk,plain,
~ hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,v_pn)),v_x),v_xa)),
inference(skolemisation,[status(esa)],[f461_nnf]) ).
cnf(c461,plain,
~ hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,v_pn)),v_x),v_xa)),
inference(cnf_transformation,[status(esa)],[f461_sk]) ).
cnf(t63,plain,
hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,v_pn)),v_x),v_xa)) = false,
inference(equality_encoding,[status(esa)],[c461]) ).
cnf(t1055,plain,
hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Com_Ocom_OBODY,v_pn)),v_x),v_xa)) = false,
inference(orient,[status(thm)],[t63]) ).
cnf(t1075,plain,
true = ifeq(hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_x),v_xa)),true,false,true),
inference(cp,[status(thm)],[t268,t1055]) ).
cnf(f460,negated_conjecture,
hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_x),v_xa)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f460_nnf,plain,
hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_x),v_xa)),
inference(nnf_transformation,[status(thm)],[f460]) ).
cnf(c460,plain,
hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_x),v_xa)),
inference(cnf_transformation,[status(esa)],[f460_nnf]) ).
cnf(t87,plain,
hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_x),v_xa)) = true,
inference(equality_encoding,[status(esa)],[c460]) ).
cnf(t411,plain,
hBOOL(hAPP(hAPP(hAPP(c_Natural_Oevalc,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_x),v_xa)) = true,
inference(orient,[status(thm)],[t87]) ).
cnf(t1709,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t1075,t411]) ).
cnf(t11,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t203,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t1710,plain,
true = false,
inference(step,[status(thm)],[t1709,t203]) ).
cnf(t1625,plain,
false = true,
inference(orient,[status(thm)],[t1710]) ).
cnf(f3,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I51_J_0) ).
fof(f3_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)],[f3]) ).
fof(f3_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)],[f3_nnf]) ).
cnf(c3,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(f20,axiom,
c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Some__eq_1) ).
fof(f20_nnf,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(f21,axiom,
c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Osimps_I2_J_0) ).
fof(f21_nnf,plain,
! [T_a,V_a_H] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [T_a,V_a_H] : c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
c_Option_Ooption_ONone(X0) != c_Option_Ooption_OSome(X1,X0),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(f37,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I14_J_0) ).
fof(f37_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)],[f37]) ).
fof(f37_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)],[f37_nnf]) ).
cnf(c37,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(f38,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I32_J_0) ).
fof(f38_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)],[f38]) ).
fof(f38_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)],[f38_nnf]) ).
cnf(c38,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(f42,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/sandbox/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f42_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)],[f42]) ).
fof(f42_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)],[f42_nnf]) ).
cnf(c42,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)],[f42_sk]) ).
cnf(f51,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I43_J_0) ).
fof(f51_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)],[f51]) ).
fof(f51_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)],[f51_nnf]) ).
cnf(c51,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OLocal(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(f54,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I61_J_0) ).
fof(f54_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)],[f54]) ).
fof(f54_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)],[f54_nnf]) ).
cnf(c54,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(f71,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I56_J_0) ).
fof(f71_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)],[f71]) ).
fof(f71_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)],[f71_nnf]) ).
cnf(c71,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OCall(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f71_sk]) ).
cnf(f73,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I36_J_0) ).
fof(f73_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)],[f73]) ).
fof(f73_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)],[f73_nnf]) ).
cnf(c73,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OCond(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
cnf(f77,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I24_J_0) ).
fof(f77_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)],[f77]) ).
fof(f77_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)],[f77_nnf]) ).
cnf(c77,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(f84,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I17_J_0) ).
fof(f84_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)],[f84]) ).
fof(f84_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)],[f84_nnf]) ).
cnf(c84,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(f86,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I39_J_0) ).
fof(f86_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)],[f86]) ).
fof(f86_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)],[f86_nnf]) ).
cnf(c86,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f86_sk]) ).
cnf(f88,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(f88_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f88]) ).
fof(f88_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f88_nnf]) ).
cnf(c88,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f88_sk]) ).
cnf(f89,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(f89_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f89]) ).
fof(f89_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f89_nnf]) ).
cnf(c89,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f89_sk]) ).
cnf(f98,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I46_J_0) ).
fof(f98_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)],[f98]) ).
fof(f98_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)],[f98_nnf]) ).
cnf(c98,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(f101,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I44_J_0) ).
fof(f101_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)],[f101]) ).
fof(f101_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)],[f101_nnf]) ).
cnf(c101,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f101_sk]) ).
cnf(f102,axiom,
c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f102_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)],[f102]) ).
fof(f102_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)],[f102_nnf]) ).
cnf(c102,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f102_sk]) ).
cnf(f103,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I35_J_0) ).
fof(f103_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)],[f103]) ).
fof(f103_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)],[f103_nnf]) ).
cnf(c103,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f103_sk]) ).
cnf(f109,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I23_J_0) ).
fof(f109_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)],[f109]) ).
fof(f109_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)],[f109_nnf]) ).
cnf(c109,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f109_sk]) ).
cnf(f111,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I52_J_0) ).
fof(f111_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)],[f111]) ).
fof(f111_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)],[f111_nnf]) ).
cnf(c111,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f111_sk]) ).
cnf(f113,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I37_J_0) ).
fof(f113_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)],[f113]) ).
fof(f113_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)],[f113_nnf]) ).
cnf(c113,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OLocal(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f113_sk]) ).
cnf(f114,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/sandbox/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f114_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)],[f114]) ).
fof(f114_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)],[f114_nnf]) ).
cnf(c114,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)],[f114_sk]) ).
cnf(f116,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I45_J_0) ).
fof(f116_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)],[f116]) ).
fof(f116_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)],[f116_nnf]) ).
cnf(c116,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f116_sk]) ).
cnf(f126,axiom,
c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_option_Osimps_I3_J_0) ).
fof(f126_nnf,plain,
! [V_a_H,T_a] : c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
inference(nnf_transformation,[status(thm)],[f126]) ).
fof(f126_sk,plain,
! [V_a_H,T_a] : c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f126_nnf]) ).
cnf(c126,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f126_sk]) ).
cnf(f127,axiom,
c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__None__eq_1) ).
fof(f127_nnf,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(nnf_transformation,[status(thm)],[f127]) ).
fof(f127_sk,plain,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f127_nnf]) ).
cnf(c127,plain,
c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
cnf(f128,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I57_J_0) ).
fof(f128_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)],[f128]) ).
fof(f128_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)],[f128_nnf]) ).
cnf(c128,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OCond(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
cnf(f138,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I28_J_0) ).
fof(f138_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)],[f138]) ).
fof(f138_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)],[f138_nnf]) ).
cnf(c138,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f138_sk]) ).
cnf(f139,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I22_J_0) ).
fof(f139_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)],[f139]) ).
fof(f139_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)],[f139_nnf]) ).
cnf(c139,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f139_sk]) ).
cnf(f144,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I38_J_0) ).
fof(f144_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)],[f144]) ).
fof(f144_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)],[f144_nnf]) ).
cnf(c144,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f144_sk]) ).
cnf(f147,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I26_J_0) ).
fof(f147_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)],[f147]) ).
fof(f147_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)],[f147_nnf]) ).
cnf(c147,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f147_sk]) ).
cnf(f149,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I16_J_0) ).
fof(f149_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)],[f149]) ).
fof(f149_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)],[f149_nnf]) ).
cnf(c149,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(X0,X1),
inference(cnf_transformation,[status(esa)],[f149_sk]) ).
cnf(f150,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f150_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)],[f150]) ).
fof(f150_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)],[f150_nnf]) ).
cnf(c150,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f150_sk]) ).
cnf(f151,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I10_J_0) ).
fof(f151_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)],[f151]) ).
fof(f151_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)],[f151_nnf]) ).
cnf(c151,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f151_sk]) ).
cnf(f152,axiom,
c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_UNIV__not__empty_0) ).
fof(f152_nnf,plain,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f152]) ).
fof(f152_sk,plain,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f152_nnf]) ).
cnf(c152,plain,
c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(esa)],[f152_sk]) ).
cnf(f168,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I34_J_0) ).
fof(f168_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)],[f168]) ).
fof(f168_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)],[f168_nnf]) ).
cnf(c168,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f168_sk]) ).
cnf(f186,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I15_J_0) ).
fof(f186_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)],[f186]) ).
fof(f186_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)],[f186_nnf]) ).
cnf(c186,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
cnf(f187,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I53_J_0) ).
fof(f187_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)],[f187]) ).
fof(f187_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)],[f187_nnf]) ).
cnf(c187,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f187_sk]) ).
cnf(f188,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I50_J_0) ).
fof(f188_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)],[f188]) ).
fof(f188_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)],[f188_nnf]) ).
cnf(c188,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f188_sk]) ).
cnf(f190,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/sandbox/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f190_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)],[f190]) ).
fof(f190_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)],[f190_nnf]) ).
cnf(c190,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)],[f190_sk]) ).
cnf(f192,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I27_J_0) ).
fof(f192_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)],[f192]) ).
fof(f192_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)],[f192_nnf]) ).
cnf(c192,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f192_sk]) ).
cnf(f262,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I60_J_0) ).
fof(f262_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)],[f262]) ).
fof(f262_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)],[f262_nnf]) ).
cnf(c262,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f262_sk]) ).
cnf(f263,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I25_J_0) ).
fof(f263_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)],[f263]) ).
fof(f263_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)],[f263_nnf]) ).
cnf(c263,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OAss(X2,X3),
inference(cnf_transformation,[status(esa)],[f263_sk]) ).
cnf(f271,axiom,
c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I11_J_0) ).
fof(f271_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)],[f271]) ).
fof(f271_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)],[f271_nnf]) ).
cnf(c271,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
cnf(f273,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(f273_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f273]) ).
fof(f273_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f273_nnf]) ).
cnf(c273,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
cnf(f274,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(f274_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f274]) ).
fof(f274_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f274_nnf]) ).
cnf(c274,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f274_sk]) ).
cnf(f281,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(V_vname_H,V_fun_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I8_J_0) ).
fof(f281_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)],[f281]) ).
fof(f281_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)],[f281_nnf]) ).
cnf(c281,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(X0,X1),
inference(cnf_transformation,[status(esa)],[f281_sk]) ).
cnf(f286,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I29_J_0) ).
fof(f286_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)],[f286]) ).
fof(f286_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)],[f286_nnf]) ).
cnf(c286,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OAss(X2,X3),
inference(cnf_transformation,[status(esa)],[f286_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/sandbox/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(f290,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f290_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)],[f290]) ).
fof(f290_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)],[f290_nnf]) ).
cnf(c290,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f290_sk]) ).
cnf(f291,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f291_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)],[f291]) ).
fof(f291_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)],[f291_nnf]) ).
cnf(c291,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f291_sk]) ).
cnf(f293,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f293_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)],[f293]) ).
fof(f293_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)],[f293_nnf]) ).
cnf(c293,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f293_sk]) ).
cnf(f302,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I33_J_0) ).
fof(f302_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)],[f302]) ).
fof(f302_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)],[f302_nnf]) ).
cnf(c302,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f302_sk]) ).
cnf(f303,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I13_J_0) ).
fof(f303_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)],[f303]) ).
fof(f303_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)],[f303_nnf]) ).
cnf(c303,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f303_sk]) ).
cnf(f311,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I20_J_0) ).
fof(f311_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)],[f311]) ).
fof(f311_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)],[f311_nnf]) ).
cnf(c311,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f311_sk]) ).
cnf(f314,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I47_J_0) ).
fof(f314_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)],[f314]) ).
fof(f314_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)],[f314_nnf]) ).
cnf(c314,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
cnf(f315,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f315_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f315]) ).
fof(f315_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f315_nnf]) ).
cnf(c315,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f315_sk]) ).
cnf(f316,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f316_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f316]) ).
fof(f316_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f316_nnf]) ).
cnf(c316,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f316_sk]) ).
cnf(f332,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I21_J_0) ).
fof(f332_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)],[f332]) ).
fof(f332_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)],[f332_nnf]) ).
cnf(c332,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f332_sk]) ).
cnf(f349,axiom,
c_Com_Ocom_OAss(V_vname_H,V_fun_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I9_J_0) ).
fof(f349_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)],[f349]) ).
fof(f349_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)],[f349_nnf]) ).
cnf(c349,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f349_sk]) ).
cnf(f353,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/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I42_J_0) ).
fof(f353_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)],[f353]) ).
fof(f353_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)],[f353_nnf]) ).
cnf(c353,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OCall(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f353_sk]) ).
cnf(f357,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I12_J_0) ).
fof(f357_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)],[f357]) ).
fof(f357_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)],[f357_nnf]) ).
cnf(c357,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f357_sk]) ).
cnf(f372,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I19_J_0) ).
fof(f372_nnf,plain,
! [V_pname_H] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f372]) ).
fof(f372_sk,plain,
! [V_pname_H] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f372_nnf]) ).
cnf(c372,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f372_sk]) ).
cnf(f373,axiom,
c_Com_Ocom_OWhile(V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I58_J_0) ).
fof(f373_nnf,plain,
! [V_fun,V_com,V_pname_H] : c_Com_Ocom_OWhile(V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f373]) ).
fof(f373_sk,plain,
! [V_fun,V_com,V_pname_H] : c_Com_Ocom_OWhile(V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f373_nnf]) ).
cnf(c373,plain,
c_Com_Ocom_OWhile(X0,X1) != hAPP(c_Com_Ocom_OBODY,X2),
inference(cnf_transformation,[status(esa)],[f373_sk]) ).
cnf(f375,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I55_J_0) ).
fof(f375_nnf,plain,
! [V_pname_H,V_fun,V_com1,V_com2] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f375]) ).
fof(f375_sk,plain,
! [V_pname_H,V_fun,V_com1,V_com2] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(skolemisation,[status(esa)],[f375_nnf]) ).
cnf(c375,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OCond(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f375_sk]) ).
cnf(f376,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I54_J_0) ).
fof(f376_nnf,plain,
! [V_fun,V_com1,V_com2,V_pname_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f376]) ).
fof(f376_sk,plain,
! [V_fun,V_com1,V_com2,V_pname_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f376_nnf]) ).
cnf(c376,plain,
c_Com_Ocom_OCond(X0,X1,X2) != hAPP(c_Com_Ocom_OBODY,X3),
inference(cnf_transformation,[status(esa)],[f376_sk]) ).
cnf(f377,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OAss(V_vname,V_fun),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I31_J_0) ).
fof(f377_nnf,plain,
! [V_pname_H,V_vname,V_fun] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(nnf_transformation,[status(thm)],[f377]) ).
fof(f377_sk,plain,
! [V_pname_H,V_vname,V_fun] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OAss(V_vname,V_fun),
inference(skolemisation,[status(esa)],[f377_nnf]) ).
cnf(c377,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OAss(X1,X2),
inference(cnf_transformation,[status(esa)],[f377_sk]) ).
cnf(f378,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I30_J_0) ).
fof(f378_nnf,plain,
! [V_vname,V_fun,V_pname_H] : c_Com_Ocom_OAss(V_vname,V_fun) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f378]) ).
fof(f378_sk,plain,
! [V_vname,V_fun,V_pname_H] : c_Com_Ocom_OAss(V_vname,V_fun) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f378_nnf]) ).
cnf(c378,plain,
c_Com_Ocom_OAss(X0,X1) != hAPP(c_Com_Ocom_OBODY,X2),
inference(cnf_transformation,[status(esa)],[f378_sk]) ).
cnf(f379,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I41_J_0) ).
fof(f379_nnf,plain,
! [V_pname_H,V_loc,V_fun,V_com] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f379]) ).
fof(f379_sk,plain,
! [V_pname_H,V_loc,V_fun,V_com] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OLocal(V_loc,V_fun,V_com),
inference(skolemisation,[status(esa)],[f379_nnf]) ).
cnf(c379,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OLocal(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f379_sk]) ).
cnf(f380,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I59_J_0) ).
fof(f380_nnf,plain,
! [V_pname_H,V_fun,V_com] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f380]) ).
fof(f380_sk,plain,
! [V_pname_H,V_fun,V_com] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(skolemisation,[status(esa)],[f380_nnf]) ).
cnf(c380,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OWhile(X1,X2),
inference(cnf_transformation,[status(esa)],[f380_sk]) ).
cnf(f381,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != hAPP(c_Com_Ocom_OBODY,V_pname),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I63_J_0) ).
fof(f381_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) != hAPP(c_Com_Ocom_OBODY,V_pname),
inference(nnf_transformation,[status(thm)],[f381]) ).
fof(f381_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) != hAPP(c_Com_Ocom_OBODY,V_pname),
inference(skolemisation,[status(esa)],[f381_nnf]) ).
cnf(c381,plain,
c_Com_Ocom_OCall(X0,X1,X2) != hAPP(c_Com_Ocom_OBODY,X3),
inference(cnf_transformation,[status(esa)],[f381_sk]) ).
cnf(f382,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I49_J_0) ).
fof(f382_nnf,plain,
! [V_pname_H,V_com1,V_com2] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f382]) ).
fof(f382_sk,plain,
! [V_pname_H,V_com1,V_com2] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f382_nnf]) ).
cnf(c382,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OSemi(X1,X2),
inference(cnf_transformation,[status(esa)],[f382_sk]) ).
cnf(f383,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I48_J_0) ).
fof(f383_nnf,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f383]) ).
fof(f383_sk,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f383_nnf]) ).
cnf(c383,plain,
c_Com_Ocom_OSemi(X0,X1) != hAPP(c_Com_Ocom_OBODY,X2),
inference(cnf_transformation,[status(esa)],[f383_sk]) ).
cnf(f384,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I40_J_0) ).
fof(f384_nnf,plain,
! [V_loc,V_fun,V_com,V_pname_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f384]) ).
fof(f384_sk,plain,
! [V_loc,V_fun,V_com,V_pname_H] : c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f384_nnf]) ).
cnf(c384,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != hAPP(c_Com_Ocom_OBODY,X3),
inference(cnf_transformation,[status(esa)],[f384_sk]) ).
cnf(f385,axiom,
hAPP(c_Com_Ocom_OBODY,V_pname) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I62_J_0) ).
fof(f385_nnf,plain,
! [V_pname,V_vname_H,V_pname_H,V_fun_H] : hAPP(c_Com_Ocom_OBODY,V_pname) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(nnf_transformation,[status(thm)],[f385]) ).
fof(f385_sk,plain,
! [V_pname,V_vname_H,V_pname_H,V_fun_H] : hAPP(c_Com_Ocom_OBODY,V_pname) != c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H),
inference(skolemisation,[status(esa)],[f385_nnf]) ).
cnf(c385,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OCall(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f385_sk]) ).
cnf(f387,axiom,
c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I18_J_0) ).
fof(f387_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f387]) ).
fof(f387_sk,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f387_nnf]) ).
cnf(c387,plain,
c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,X0),
inference(cnf_transformation,[status(esa)],[f387_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c3,c20,c21,c37,c38,c42,c51,c54,c71,c73,c77,c84,c86,c88,c89,c98,c101,c102,c103,c109,c111,c113,c114,c116,c126,c127,c128,c138,c139,c144,c147,c149,c150,c151,c152,c168,c186,c187,c188,c190,c192,c262,c263,c271,c273,c274,c281,c286,c287,c290,c291,c293,c302,c303,c311,c314,c315,c316,c332,c349,c353,c357,c372,c373,c375,c376,c377,c378,c379,c380,c381,c382,c383,c384,c385,c387,c461]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1625]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV897-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.41 % Computer : n013.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Thu Sep 24 21:15:21 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 43.23/5.96 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 43.23/5.96 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------