%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV907-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 : n009.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:29 PM UTC 2026
% Result : Timeout 294.86s 43.56s
% Output : None
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 83
% Syntax : Number of formulae : 371 ( 347 unt; 0 def)
% Number of atoms : 411 ( 321 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 378 ( 338 ~; 40 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-3 aty)
% Number of functors : 37 ( 37 usr; 10 con; 0-5 aty)
% Number of variables : 1154 ( 490 sgn 558 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f480,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
| ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_MGT__Body_0) ).
fof(f480_nnf,plain,
! [V_G,V_Procs] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
| ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
inference(nnf_transformation,[status(thm)],[f480]) ).
fof(f480_sk,plain,
! [V_G,V_Procs] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
| ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
inference(skolemisation,[status(esa)],[f480_nnf]) ).
cnf(c480,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(X0,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
| ~ c_Finite__Set_Ofinite(X1,tc_Com_Opname)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
inference(cnf_transformation,[status(esa)],[f480_sk]) ).
cnf(t245,plain,
ifeq(c_Finite__Set_Ofinite(X1,tc_Com_Opname),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(X2,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true,c_Hoare__Mirabelle_Ohoare__derivs(X2,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true) = true,
inference(equality_encoding,[status(esa)],[c480]) ).
cnf(t459,plain,
ifeq(c_Finite__Set_Ofinite(X1,tc_Com_Opname),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(X2,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true,c_Hoare__Mirabelle_Ohoare__derivs(X2,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true) = true,
inference(orient,[status(thm)],[t245]) ).
cnf(f283,axiom,
c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Un__empty__left_0) ).
fof(f283_nnf,plain,
! [T_a,V_B] : c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B,
inference(nnf_transformation,[status(thm)],[f283]) ).
fof(f283_sk,plain,
! [T_a,V_B] : c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B,
inference(skolemisation,[status(esa)],[f283_nnf]) ).
cnf(c283,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,tc_fun(X0,tc_bool)) = X1,
inference(cnf_transformation,[status(esa)],[f283_sk]) ).
cnf(t49,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,tc_fun(X1,tc_bool)) = X2,
inference(equality_encoding,[status(esa)],[c283]) ).
cnf(t261,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,tc_fun(X1,tc_bool)) = X2,
inference(orient,[status(thm)],[t49]) ).
cnf(t460,plain,
true = ifeq(c_Finite__Set_Ofinite(X1,tc_Com_Opname),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true),
inference(cp,[status(thm)],[t459,t261]) ).
cnf(f497,axiom,
c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_image__image_0) ).
fof(f497_nnf,plain,
! [V_f,V_g,V_A,T_c,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a),
inference(nnf_transformation,[status(thm)],[f497]) ).
fof(f497_sk,plain,
! [V_f,V_g,V_A,T_c,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a),
inference(skolemisation,[status(esa)],[f497_nnf]) ).
cnf(c497,plain,
c_Set_Oimage(X0,c_Set_Oimage(X1,X2,X3,X4),X4,X5) = c_Set_Oimage(c_COMBB(X0,X1,X4,X5,X3),X2,X3,X5),
inference(cnf_transformation,[status(esa)],[f497_sk]) ).
cnf(t118,plain,
c_Set_Oimage(c_COMBB(X1,X2,X3,X4,X5),X6,X5,X4) = c_Set_Oimage(X1,c_Set_Oimage(X2,X6,X5,X3),X3,X4),
inference(equality_encoding,[status(esa)],[c497]) ).
cnf(t1588,plain,
c_Set_Oimage(X1,c_Set_Oimage(X2,X3,X4,X5),X5,X6) = c_Set_Oimage(c_COMBB(X1,X2,X5,X6,X4),X3,X4,X6),
inference(orient,[status(thm)],[t118]) ).
cnf(t126249,plain,
true = ifeq(c_Finite__Set_Ofinite(X1,tc_Com_Opname),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,X1,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true),
inference(step,[status(thm)],[t460,t1588]) ).
cnf(t126250,plain,
true = ifeq(c_Finite__Set_Ofinite(X1,tc_Com_Opname),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,X1,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),X1,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true),
inference(step,[status(thm)],[t126249,t1588]) ).
cnf(t126251,plain,
true = ifeq(c_Finite__Set_Ofinite(X1,tc_Com_Opname),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,X1,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Option_Othe(tc_Com_Ocom),c_Set_Oimage(c_Com_Obody,X1,tc_Com_Opname,tc_Option_Ooption(tc_Com_Ocom)),tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),X1,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true),
inference(step,[status(thm)],[t126250,t1588]) ).
cnf(t126252,plain,
true = ifeq(c_Finite__Set_Ofinite(X1,tc_Com_Opname),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,X1,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Option_Othe(tc_Com_Ocom),c_Set_Oimage(c_Com_Obody,X1,tc_Com_Opname,tc_Option_Ooption(tc_Com_Ocom)),tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,X1,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true),
inference(step,[status(thm)],[t126251,t1588]) ).
cnf(t22659,plain,
ifeq(c_Finite__Set_Ofinite(X1,tc_Com_Opname),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,X1,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Option_Othe(tc_Com_Ocom),c_Set_Oimage(c_Com_Obody,X1,tc_Com_Opname,tc_Option_Ooption(tc_Com_Ocom)),tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,X1,tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true) = true,
inference(orient,[status(thm)],[t126252]) ).
cnf(f492,axiom,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_MGF__lemma2__simult_0) ).
fof(f492_nnf,plain,
! [V_F] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate) ),
inference(nnf_transformation,[status(thm)],[f492]) ).
fof(f492_sk,plain,
! [V_F] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate) ),
inference(skolemisation,[status(esa)],[f492_nnf]) ).
cnf(c492,plain,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ~ c_lessequals(X0,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),X0,tc_Com_Ostate) ),
inference(cnf_transformation,[status(esa)],[f492_sk]) ).
cnf(t238,plain,
ifeq(c_lessequals(X1,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),true,ifeq(c_Com_OWT__bodies,true,ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),X1,tc_Com_Ostate),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c492]) ).
cnf(t425,plain,
ifeq(c_lessequals(X1,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),true,ifeq(c_Com_OWT__bodies,true,ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),X1,tc_Com_Ostate),true),true),true) = true,
inference(orient,[status(thm)],[t238]) ).
cnf(f373,axiom,
c_lessequals(V_x,V_x,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_equalityE_0) ).
fof(f373_nnf,plain,
! [V_x,T_a] : c_lessequals(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f373]) ).
fof(f373_sk,plain,
! [V_x,T_a] : c_lessequals(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f373_nnf]) ).
cnf(c373,plain,
c_lessequals(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f373_sk]) ).
cnf(t24,plain,
c_lessequals(X1,X1,tc_fun(X2,tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c373]) ).
cnf(t523,plain,
c_lessequals(X1,X1,tc_fun(X2,tc_bool)) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t558,plain,
true = ifeq(true,true,ifeq(c_Com_OWT__bodies,true,ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true),true),
inference(cp,[status(thm)],[t425,t523]) ).
cnf(t20,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t246,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t20]) ).
cnf(t126855,plain,
true = ifeq(c_Com_OWT__bodies,true,ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true),
inference(step,[status(thm)],[t558,t246]) ).
cnf(f509,negated_conjecture,
c_Com_OWT__bodies,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f509_nnf,plain,
c_Com_OWT__bodies,
inference(nnf_transformation,[status(thm)],[f509]) ).
cnf(c509,plain,
c_Com_OWT__bodies,
inference(cnf_transformation,[status(esa)],[f509_nnf]) ).
cnf(t0,plain,
true = c_Com_OWT__bodies,
inference(equality_encoding,[status(esa)],[c509]) ).
cnf(t933,plain,
c_Com_OWT__bodies = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t126856,plain,
true = ifeq(true,true,ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true),
inference(step,[status(thm)],[t126855,t933]) ).
cnf(t126857,plain,
true = ifeq(c_Hoare__Mirabelle_Ostate__not__singleton,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),
inference(step,[status(thm)],[t126856,t246]) ).
cnf(f508,negated_conjecture,
c_Hoare__Mirabelle_Ostate__not__singleton,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f508_nnf,plain,
c_Hoare__Mirabelle_Ostate__not__singleton,
inference(nnf_transformation,[status(thm)],[f508]) ).
cnf(c508,plain,
c_Hoare__Mirabelle_Ostate__not__singleton,
inference(cnf_transformation,[status(esa)],[f508_nnf]) ).
cnf(t1,plain,
true = c_Hoare__Mirabelle_Ostate__not__singleton,
inference(equality_encoding,[status(esa)],[c508]) ).
cnf(t939,plain,
c_Hoare__Mirabelle_Ostate__not__singleton = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t126858,plain,
true = ifeq(true,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),
inference(step,[status(thm)],[t126857,t939]) ).
cnf(t126859,plain,
true = c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(step,[status(thm)],[t126858,t246]) ).
cnf(t126860,plain,
true = c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(step,[status(thm)],[t126859,t1588]) ).
cnf(t126861,plain,
true = c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(step,[status(thm)],[t126860,t1588]) ).
cnf(t126862,plain,
true = c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Option_Othe(tc_Com_Ocom),c_Set_Oimage(c_Com_Obody,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Option_Ooption(tc_Com_Ocom)),tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(step,[status(thm)],[t126861,t1588]) ).
cnf(t125270,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Option_Othe(tc_Com_Ocom),c_Set_Oimage(c_Com_Obody,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Option_Ooption(tc_Com_Ocom)),tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = true,
inference(orient,[status(thm)],[t126862]) ).
cnf(t125285,plain,
true = ifeq(c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),true,ifeq(true,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true),
inference(cp,[status(thm)],[t22659,t125270]) ).
cnf(f487,axiom,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_finite__dom__body_0) ).
fof(f487_nnf,plain,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
inference(nnf_transformation,[status(thm)],[f487]) ).
cnf(c487,plain,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
inference(cnf_transformation,[status(esa)],[f487_nnf]) ).
cnf(t22,plain,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname) = true,
inference(equality_encoding,[status(esa)],[c487]) ).
cnf(t942,plain,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname) = true,
inference(orient,[status(thm)],[t22]) ).
cnf(t126863,plain,
true = ifeq(true,true,ifeq(true,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),true),
inference(step,[status(thm)],[t125285,t942]) ).
cnf(t126864,plain,
true = ifeq(true,true,c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),true),
inference(step,[status(thm)],[t126863,t246]) ).
cnf(t126865,plain,
true = c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(step,[status(thm)],[t126864,t246]) ).
cnf(f512,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f512_nnf,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(nnf_transformation,[status(thm)],[f512]) ).
fof(f512_sk,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(skolemisation,[status(esa)],[f512_nnf]) ).
cnf(c512,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(cnf_transformation,[status(esa)],[f512_sk]) ).
cnf(t152,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(equality_encoding,[status(esa)],[c512]) ).
cnf(t125787,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(step,[status(thm)],[t152,t1588]) ).
cnf(t1607,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) = false,
inference(orient,[status(thm)],[t125787]) ).
cnf(t126866,plain,
true = false,
inference(step,[status(thm)],[t126865,t1607]) ).
cnf(t125287,plain,
false = true,
inference(orient,[status(thm)],[t126866]) ).
cnf(f1,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(f1_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)],[f1]) ).
fof(f1_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)],[f1_nnf]) ).
cnf(c1,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(f7,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(f7_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)],[f7]) ).
fof(f7_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)],[f7_nnf]) ).
cnf(c7,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(f12,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(f12_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)],[f12]) ).
fof(f12_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)],[f12_nnf]) ).
cnf(c12,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(f13,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(f13_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)],[f13]) ).
fof(f13_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)],[f13_nnf]) ).
cnf(c13,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(f20,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(f20_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)],[f20]) ).
fof(f20_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)],[f20_nnf]) ).
cnf(c20,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(f24,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(f24_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)],[f24]) ).
fof(f24_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)],[f24_nnf]) ).
cnf(c24,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OCond(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(f25,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(f25_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)],[f25]) ).
fof(f25_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)],[f25_nnf]) ).
cnf(c25,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OCall(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(f41,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(f41_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)],[f41]) ).
fof(f41_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)],[f41_nnf]) ).
cnf(c41,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(f92,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(f92_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)],[f92]) ).
fof(f92_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)],[f92_nnf]) ).
cnf(c92,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(f94,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(f94_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)],[f94]) ).
fof(f94_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)],[f94_nnf]) ).
cnf(c94,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(f100,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(f100_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)],[f100]) ).
fof(f100_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)],[f100_nnf]) ).
cnf(c100,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OLocal(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f100_sk]) ).
cnf(f102,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(f102_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)],[f102]) ).
fof(f102_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)],[f102_nnf]) ).
cnf(c102,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f102_sk]) ).
cnf(f108,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(f108_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)],[f108]) ).
fof(f108_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)],[f108_nnf]) ).
cnf(c108,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OLocal(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f108_sk]) ).
cnf(f110,axiom,
c_Fun_Ofun__upd(V_t,V_k,hAPP(c_Option_Ooption_OSome(T_b),V_x),T_a,tc_Option_Ooption(T_b)) != c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_map__upd__nonempty_0) ).
fof(f110_nnf,plain,
! [V_t,V_k,T_b,V_x,T_a] : c_Fun_Ofun__upd(V_t,V_k,hAPP(c_Option_Ooption_OSome(T_b),V_x),T_a,tc_Option_Ooption(T_b)) != c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),
inference(nnf_transformation,[status(thm)],[f110]) ).
fof(f110_sk,plain,
! [V_t,V_k,T_b,V_x,T_a] : c_Fun_Ofun__upd(V_t,V_k,hAPP(c_Option_Ooption_OSome(T_b),V_x),T_a,tc_Option_Ooption(T_b)) != c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),
inference(skolemisation,[status(esa)],[f110_nnf]) ).
cnf(c110,plain,
c_Fun_Ofun__upd(X0,X1,hAPP(c_Option_Ooption_OSome(X2),X3),X4,tc_Option_Ooption(X2)) != c_COMBK(c_Option_Ooption_ONone(X2),tc_Option_Ooption(X2),X4),
inference(cnf_transformation,[status(esa)],[f110_sk]) ).
cnf(f112,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(f112_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)],[f112]) ).
fof(f112_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)],[f112_nnf]) ).
cnf(c112,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f112_sk]) ).
cnf(f114,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(f114_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)],[f114]) ).
fof(f114_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)],[f114_nnf]) ).
cnf(c114,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f114_sk]) ).
cnf(f117,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(f117_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)],[f117]) ).
fof(f117_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)],[f117_nnf]) ).
cnf(c117,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OLocal(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f117_sk]) ).
cnf(f121,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(f121_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)],[f121]) ).
fof(f121_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)],[f121_nnf]) ).
cnf(c121,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f121_sk]) ).
cnf(f134,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(f134_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)],[f134]) ).
fof(f134_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)],[f134_nnf]) ).
cnf(c134,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OCond(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f134_sk]) ).
cnf(f137,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(f137_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)],[f137]) ).
fof(f137_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)],[f137_nnf]) ).
cnf(c137,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f137_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/sandbox2/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(f154,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(f154_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)],[f154]) ).
fof(f154_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)],[f154_nnf]) ).
cnf(c154,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f154_sk]) ).
cnf(f155,axiom,
( ~ hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_domIff_0) ).
fof(f155_nnf,plain,
! [V_m,V_a,T_b,T_a] :
( ~ hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
inference(nnf_transformation,[status(thm)],[f155]) ).
fof(f155_sk,plain,
! [V_m,V_a,T_b,T_a] :
( ~ hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
inference(skolemisation,[status(esa)],[f155_nnf]) ).
cnf(c155,plain,
( ~ hBOOL(c_in(X1,c_Map_Odom(X0,X3,X2),X3))
| hAPP(X0,X1) != c_Option_Ooption_ONone(X2) ),
inference(cnf_transformation,[status(esa)],[f155_sk]) ).
cnf(f163,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(f163_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)],[f163]) ).
fof(f163_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)],[f163_nnf]) ).
cnf(c163,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f163_sk]) ).
cnf(f165,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(f165_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)],[f165]) ).
fof(f165_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)],[f165_nnf]) ).
cnf(c165,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(X0,X1),
inference(cnf_transformation,[status(esa)],[f165_sk]) ).
cnf(f166,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(f166_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)],[f166]) ).
fof(f166_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)],[f166_nnf]) ).
cnf(c166,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
cnf(f168,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(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f168_nnf,plain,
! [V_x,V_B,T_a,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(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
inference(nnf_transformation,[status(thm)],[f168]) ).
fof(f168_sk,plain,
! [V_x,V_B,T_a,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(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
inference(skolemisation,[status(esa)],[f168_nnf]) ).
cnf(c168,plain,
( c_Lattices_Olower__semilattice__class_Oinf(X3,X1,tc_fun(X2,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| ~ hBOOL(c_in(X0,X3,X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f168_sk]) ).
cnf(f178,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(f178_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)],[f178]) ).
fof(f178_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)],[f178_nnf]) ).
cnf(c178,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f178_sk]) ).
cnf(f180,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(f180_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)],[f180]) ).
fof(f180_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)],[f180_nnf]) ).
cnf(c180,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OAss(X2,X3),
inference(cnf_transformation,[status(esa)],[f180_sk]) ).
cnf(f187,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(f187_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)],[f187]) ).
fof(f187_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)],[f187_nnf]) ).
cnf(c187,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f187_sk]) ).
cnf(f200,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(f200_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)],[f200]) ).
fof(f200_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)],[f200_nnf]) ).
cnf(c200,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OAss(X0,X1),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
cnf(f221,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(f221_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)],[f221]) ).
fof(f221_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)],[f221_nnf]) ).
cnf(c221,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f221_sk]) ).
cnf(f235,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(f235_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)],[f235]) ).
fof(f235_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)],[f235_nnf]) ).
cnf(c235,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f235_sk]) ).
cnf(f236,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(f236_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)],[f236]) ).
fof(f236_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)],[f236_nnf]) ).
cnf(c236,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(f241,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(f241_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)],[f241]) ).
fof(f241_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)],[f241_nnf]) ).
cnf(c241,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCall(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f241_sk]) ).
cnf(f244,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(f244_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)],[f244]) ).
fof(f244_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)],[f244_nnf]) ).
cnf(c244,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f244_sk]) ).
cnf(f270,axiom,
~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f270_nnf,plain,
! [V_x,T_a] : ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f270]) ).
fof(f270_sk,plain,
! [V_x,T_a] : ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f270_nnf]) ).
cnf(c270,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f270_sk]) ).
cnf(f272,axiom,
~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f272_nnf,plain,
! [V_c,T_a] : ~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f272]) ).
fof(f272_sk,plain,
! [V_c,T_a] : ~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f272_nnf]) ).
cnf(c272,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f272_sk]) ).
cnf(f273,axiom,
~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f273_nnf,plain,
! [V_a,T_a] : ~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f273]) ).
fof(f273_sk,plain,
! [V_a,T_a] : ~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f273_nnf]) ).
cnf(c273,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
cnf(f274,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(f274_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)],[f274]) ).
fof(f274_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)],[f274_nnf]) ).
cnf(c274,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f274_sk]) ).
cnf(f281,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/sandbox2/benchmark/theBenchmark.p',cls_UNIV__not__empty_0) ).
fof(f281_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)],[f281]) ).
fof(f281_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)],[f281_nnf]) ).
cnf(c281,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)],[f281_sk]) ).
cnf(f287,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(f287_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)],[f287]) ).
fof(f287_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)],[f287_nnf]) ).
cnf(c287,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f287_sk]) ).
cnf(f292,axiom,
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f292_nnf,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(nnf_transformation,[status(thm)],[f292]) ).
fof(f292_sk,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(skolemisation,[status(esa)],[f292_nnf]) ).
cnf(c292,plain,
( ~ hBOOL(c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f292_sk]) ).
cnf(f309,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(f309_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)],[f309]) ).
fof(f309_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)],[f309_nnf]) ).
cnf(c309,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OAss(X2,X3),
inference(cnf_transformation,[status(esa)],[f309_sk]) ).
cnf(f333,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(f333_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)],[f333]) ).
fof(f333_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)],[f333_nnf]) ).
cnf(c333,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OAss(X3,X4),
inference(cnf_transformation,[status(esa)],[f333_sk]) ).
cnf(f334,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(f334_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)],[f334]) ).
fof(f334_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)],[f334_nnf]) ).
cnf(c334,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f334_sk]) ).
cnf(f351,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(f351_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)],[f351]) ).
fof(f351_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)],[f351_nnf]) ).
cnf(c351,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCall(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f351_sk]) ).
cnf(f352,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(f352_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)],[f352]) ).
fof(f352_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)],[f352_nnf]) ).
cnf(c352,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f352_sk]) ).
cnf(f386,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(f386_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)],[f386]) ).
fof(f386_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)],[f386_nnf]) ).
cnf(c386,plain,
c_Com_Ocom_OCall(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f386_sk]) ).
cnf(f398,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(f398_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)],[f398]) ).
fof(f398_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)],[f398_nnf]) ).
cnf(c398,plain,
c_Com_Ocom_OAss(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f398_sk]) ).
cnf(f403,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(f403_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)],[f403]) ).
fof(f403_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)],[f403_nnf]) ).
cnf(c403,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != c_Com_Ocom_OCall(X3,X4,X5),
inference(cnf_transformation,[status(esa)],[f403_sk]) ).
cnf(f406,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(f406_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)],[f406]) ).
fof(f406_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)],[f406_nnf]) ).
cnf(c406,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f406_sk]) ).
cnf(f418,axiom,
~ hBOOL(c_Option_Ois__none(hAPP(c_Option_Ooption_OSome(T_a),V_x),T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_is__none__code_I2_J_0) ).
fof(f418_nnf,plain,
! [T_a,V_x] : ~ hBOOL(c_Option_Ois__none(hAPP(c_Option_Ooption_OSome(T_a),V_x),T_a)),
inference(nnf_transformation,[status(thm)],[f418]) ).
fof(f418_sk,plain,
! [T_a,V_x] : ~ hBOOL(c_Option_Ois__none(hAPP(c_Option_Ooption_OSome(T_a),V_x),T_a)),
inference(skolemisation,[status(esa)],[f418_nnf]) ).
cnf(c418,plain,
~ hBOOL(c_Option_Ois__none(hAPP(c_Option_Ooption_OSome(X0),X1),X0)),
inference(cnf_transformation,[status(esa)],[f418_sk]) ).
cnf(f419,axiom,
hAPP(c_Option_Ooption_OSome(T_a),V_xa) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__None__eq_1) ).
fof(f419_nnf,plain,
! [T_a,V_xa] : hAPP(c_Option_Ooption_OSome(T_a),V_xa) != c_Option_Ooption_ONone(T_a),
inference(nnf_transformation,[status(thm)],[f419]) ).
fof(f419_sk,plain,
! [T_a,V_xa] : hAPP(c_Option_Ooption_OSome(T_a),V_xa) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f419_nnf]) ).
cnf(c419,plain,
hAPP(c_Option_Ooption_OSome(X0),X1) != c_Option_Ooption_ONone(X0),
inference(cnf_transformation,[status(esa)],[f419_sk]) ).
cnf(f420,axiom,
hAPP(c_Option_Ooption_OSome(T_a),V_a_H) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_option_Osimps_I3_J_0) ).
fof(f420_nnf,plain,
! [T_a,V_a_H] : hAPP(c_Option_Ooption_OSome(T_a),V_a_H) != c_Option_Ooption_ONone(T_a),
inference(nnf_transformation,[status(thm)],[f420]) ).
fof(f420_sk,plain,
! [T_a,V_a_H] : hAPP(c_Option_Ooption_OSome(T_a),V_a_H) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f420_nnf]) ).
cnf(c420,plain,
hAPP(c_Option_Ooption_OSome(X0),X1) != c_Option_Ooption_ONone(X0),
inference(cnf_transformation,[status(esa)],[f420_sk]) ).
cnf(f426,axiom,
c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Some__eq_1) ).
fof(f426_nnf,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_y),
inference(nnf_transformation,[status(thm)],[f426]) ).
fof(f426_sk,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_y),
inference(skolemisation,[status(esa)],[f426_nnf]) ).
cnf(c426,plain,
c_Option_Ooption_ONone(X0) != hAPP(c_Option_Ooption_OSome(X0),X1),
inference(cnf_transformation,[status(esa)],[f426_sk]) ).
cnf(f427,axiom,
c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_a_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_option_Osimps_I2_J_0) ).
fof(f427_nnf,plain,
! [T_a,V_a_H] : c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_a_H),
inference(nnf_transformation,[status(thm)],[f427]) ).
fof(f427_sk,plain,
! [T_a,V_a_H] : c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_a_H),
inference(skolemisation,[status(esa)],[f427_nnf]) ).
cnf(c427,plain,
c_Option_Ooption_ONone(X0) != hAPP(c_Option_Ooption_OSome(X0),X1),
inference(cnf_transformation,[status(esa)],[f427_sk]) ).
cnf(f434,axiom,
hAPP(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(f434_nnf,plain,
! [V_pname_H] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f434]) ).
fof(f434_sk,plain,
! [V_pname_H] : hAPP(c_Com_Ocom_OBODY,V_pname_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f434_nnf]) ).
cnf(c434,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f434_sk]) ).
cnf(f435,axiom,
c_Com_Ocom_OWhile(V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I58_J_0) ).
fof(f435_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)],[f435]) ).
fof(f435_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)],[f435_nnf]) ).
cnf(c435,plain,
c_Com_Ocom_OWhile(X0,X1) != hAPP(c_Com_Ocom_OBODY,X2),
inference(cnf_transformation,[status(esa)],[f435_sk]) ).
cnf(f437,axiom,
hAPP(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(f437_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)],[f437]) ).
fof(f437_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)],[f437_nnf]) ).
cnf(c437,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OCond(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f437_sk]) ).
cnf(f438,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I54_J_0) ).
fof(f438_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)],[f438]) ).
fof(f438_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)],[f438_nnf]) ).
cnf(c438,plain,
c_Com_Ocom_OCond(X0,X1,X2) != hAPP(c_Com_Ocom_OBODY,X3),
inference(cnf_transformation,[status(esa)],[f438_sk]) ).
cnf(f439,axiom,
hAPP(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(f439_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)],[f439]) ).
fof(f439_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)],[f439_nnf]) ).
cnf(c439,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OAss(X1,X2),
inference(cnf_transformation,[status(esa)],[f439_sk]) ).
cnf(f440,axiom,
c_Com_Ocom_OAss(V_vname,V_fun) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I30_J_0) ).
fof(f440_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)],[f440]) ).
fof(f440_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)],[f440_nnf]) ).
cnf(c440,plain,
c_Com_Ocom_OAss(X0,X1) != hAPP(c_Com_Ocom_OBODY,X2),
inference(cnf_transformation,[status(esa)],[f440_sk]) ).
cnf(f441,axiom,
hAPP(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(f441_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)],[f441]) ).
fof(f441_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)],[f441_nnf]) ).
cnf(c441,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OLocal(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f441_sk]) ).
cnf(f442,axiom,
hAPP(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(f442_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)],[f442]) ).
fof(f442_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)],[f442_nnf]) ).
cnf(c442,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OWhile(X1,X2),
inference(cnf_transformation,[status(esa)],[f442_sk]) ).
cnf(f443,axiom,
c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H) != hAPP(c_Com_Ocom_OBODY,V_pname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I63_J_0) ).
fof(f443_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)],[f443]) ).
fof(f443_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)],[f443_nnf]) ).
cnf(c443,plain,
c_Com_Ocom_OCall(X0,X1,X2) != hAPP(c_Com_Ocom_OBODY,X3),
inference(cnf_transformation,[status(esa)],[f443_sk]) ).
cnf(f444,axiom,
hAPP(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(f444_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)],[f444]) ).
fof(f444_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)],[f444_nnf]) ).
cnf(c444,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OSemi(X1,X2),
inference(cnf_transformation,[status(esa)],[f444_sk]) ).
cnf(f445,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I48_J_0) ).
fof(f445_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)],[f445]) ).
fof(f445_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)],[f445_nnf]) ).
cnf(c445,plain,
c_Com_Ocom_OSemi(X0,X1) != hAPP(c_Com_Ocom_OBODY,X2),
inference(cnf_transformation,[status(esa)],[f445_sk]) ).
cnf(f446,axiom,
c_Com_Ocom_OLocal(V_loc,V_fun,V_com) != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I40_J_0) ).
fof(f446_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)],[f446]) ).
fof(f446_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)],[f446_nnf]) ).
cnf(c446,plain,
c_Com_Ocom_OLocal(X0,X1,X2) != hAPP(c_Com_Ocom_OBODY,X3),
inference(cnf_transformation,[status(esa)],[f446_sk]) ).
cnf(f447,axiom,
hAPP(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(f447_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)],[f447]) ).
fof(f447_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)],[f447_nnf]) ).
cnf(c447,plain,
hAPP(c_Com_Ocom_OBODY,X0) != c_Com_Ocom_OCall(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f447_sk]) ).
cnf(f449,axiom,
c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I18_J_0) ).
fof(f449_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(nnf_transformation,[status(thm)],[f449]) ).
fof(f449_sk,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,V_pname_H),
inference(skolemisation,[status(esa)],[f449_nnf]) ).
cnf(c449,plain,
c_Com_Ocom_OSKIP != hAPP(c_Com_Ocom_OBODY,X0),
inference(cnf_transformation,[status(esa)],[f449_sk]) ).
cnf(f473,axiom,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t) != V_t ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_single__stateE_0) ).
fof(f473_nnf,plain,
! [V_t] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t) != V_t ),
inference(nnf_transformation,[status(thm)],[f473]) ).
fof(f473_sk,plain,
! [V_t] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t) != V_t ),
inference(skolemisation,[status(esa)],[f473_nnf]) ).
cnf(c473,plain,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X0) != X0 ),
inference(cnf_transformation,[status(esa)],[f473_sk]) ).
cnf(f499,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(f499_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)],[f499]) ).
fof(f499_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)],[f499_nnf]) ).
cnf(c499,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f499_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c1,c7,c12,c13,c20,c24,c25,c41,c92,c94,c100,c102,c108,c110,c112,c114,c117,c121,c134,c137,c139,c154,c155,c163,c165,c166,c168,c178,c180,c187,c200,c221,c235,c236,c241,c244,c270,c272,c273,c274,c281,c287,c292,c309,c333,c334,c351,c352,c386,c398,c403,c406,c418,c419,c420,c426,c427,c434,c435,c437,c438,c439,c440,c441,c442,c443,c444,c445,c446,c447,c449,c473,c499,c512]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t125287]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV907-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/5.45 % Computer : n009.cluster.edu
% 0.16/5.45 % Model : x86_64 x86_64
% 0.16/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.45 % Memory : 8046.5625MB
% 0.16/5.45 % OS : Linux 6.8.0-71-generic
% 0.16/5.45 % CPULimit : 300
% 0.16/5.45 % WCLimit : 300
% 0.16/5.45 % DateTime : Thu Sep 24 21:17:04 UTC 2026
% 0.16/5.45 % CPUTime :
% 0.16/5.45 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 294.86/43.56 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 294.86/43.56 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------