%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL815-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 : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:03:07 PM UTC 2026
% Result : Unsatisfiable 103.43s 13.45s
% Output : Proof 103.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 55
% Syntax : Number of formulae : 230 ( 150 unt; 0 def)
% Number of atoms : 354 ( 110 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 458 ( 334 ~; 124 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 8 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 36 ( 36 usr; 15 con; 0-5 aty)
% Number of variables : 464 ( 112 sgn 224 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f782,axiom,
( ~ c_Type_Otypings(V_e,V_ts,V_Ts)
| c_Type_Otypings(c_Type_Oshift(V_e,V_i,V_U,tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_Ts) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lift__types_0) ).
fof(f782_nnf,plain,
! [V_e,V_i,V_U,V_ts,V_Ts] :
( ~ c_Type_Otypings(V_e,V_ts,V_Ts)
| c_Type_Otypings(c_Type_Oshift(V_e,V_i,V_U,tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_Ts) ),
inference(nnf_transformation,[status(thm)],[f782]) ).
fof(f782_sk,plain,
! [V_e,V_i,V_U,V_ts,V_Ts] :
( ~ c_Type_Otypings(V_e,V_ts,V_Ts)
| c_Type_Otypings(c_Type_Oshift(V_e,V_i,V_U,tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_Ts) ),
inference(skolemisation,[status(esa)],[f782_nnf]) ).
cnf(c782,plain,
( ~ c_Type_Otypings(X0,X3,X4)
| c_Type_Otypings(c_Type_Oshift(X0,X1,X2,tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),X1),X3,tc_Lambda_OdB,tc_Lambda_OdB),X4) ),
inference(cnf_transformation,[status(esa)],[f782_sk]) ).
cnf(t219,plain,
ifeq(c_Type_Otypings(X1,X2,X3),true,c_Type_Otypings(c_Type_Oshift(X1,X4,X5,tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),X4),X2,tc_Lambda_OdB,tc_Lambda_OdB),X3),true) = true,
inference(equality_encoding,[status(esa)],[c782]) ).
cnf(t793,plain,
ifeq(c_Type_Otypings(X1,X2,X3),true,c_Type_Otypings(c_Type_Oshift(X1,X4,X5,tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),X4),X2,tc_Lambda_OdB,tc_Lambda_OdB),X3),true) = true,
inference(orient,[status(thm)],[t219]) ).
cnf(f785,negated_conjecture,
~ c_Type_Otypings(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype),tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f785_nnf,plain,
~ c_Type_Otypings(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype),tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
inference(nnf_transformation,[status(thm)],[f785]) ).
fof(f785_sk,plain,
~ c_Type_Otypings(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype),tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
inference(skolemisation,[status(esa)],[f785_nnf]) ).
cnf(c785,plain,
~ c_Type_Otypings(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype),tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
inference(cnf_transformation,[status(esa)],[f785_sk]) ).
cnf(t247,plain,
c_Type_Otypings(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype),tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____) = false,
inference(equality_encoding,[status(esa)],[c785]) ).
cnf(t1604,plain,
c_Type_Otypings(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype),tc_Type_Otype),c_List_Omap(hAPP(c_COMBC(c_Lambda_Olift,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____) = false,
inference(orient,[status(thm)],[t247]) ).
cnf(t1607,plain,
true = ifeq(c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),true,false,true),
inference(cp,[status(thm)],[t793,t1604]) ).
cnf(f784,axiom,
c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f784_nnf,plain,
c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
inference(nnf_transformation,[status(thm)],[f784]) ).
cnf(c784,plain,
c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
inference(cnf_transformation,[status(esa)],[f784_nnf]) ).
cnf(t210,plain,
c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____) = true,
inference(equality_encoding,[status(esa)],[c784]) ).
cnf(t945,plain,
c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____) = true,
inference(orient,[status(thm)],[t210]) ).
cnf(t2027,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t1607,t945]) ).
cnf(t28,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t261,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t28]) ).
cnf(t2028,plain,
true = false,
inference(step,[status(thm)],[t2027,t261]) ).
cnf(t1931,plain,
false = true,
inference(orient,[status(thm)],[t2028]) ).
cnf(f142,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f142_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f142]) ).
fof(f142_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f142_nnf]) ).
cnf(c142,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f142_sk]) ).
cnf(f144,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f144_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f144]) ).
fof(f144_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f144_nnf]) ).
cnf(c144,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f144_sk]) ).
cnf(f146,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f146_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f146]) ).
fof(f146_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f146_nnf]) ).
cnf(c146,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f146_sk]) ).
cnf(f148,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f148_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f148]) ).
fof(f148_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f148_nnf]) ).
cnf(c148,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f148_sk]) ).
cnf(f198,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I6_J_0) ).
fof(f198_nnf,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(nnf_transformation,[status(thm)],[f198]) ).
fof(f198_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f198_nnf]) ).
cnf(c198,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f198_sk]) ).
cnf(f225,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__one__less__zero_0) ).
fof(f225_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f225]) ).
fof(f225_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f225_nnf]) ).
cnf(c225,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f225_sk]) ).
cnf(f226,axiom,
c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Var__apps__neq__Abs__apps_0) ).
fof(f226_nnf,plain,
! [V_n,V_ts,V_r,V_ss] : c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f226]) ).
fof(f226_sk,plain,
! [V_n,V_ts,V_r,V_ss] : c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(skolemisation,[status(esa)],[f226_nnf]) ).
cnf(c226,plain,
c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X0),X1,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X2),X3,tc_Lambda_OdB,tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f226_sk]) ).
cnf(f230,axiom,
~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_impossible__Cons_0) ).
fof(f230_nnf,plain,
! [V_x,V_ys,T_a] : ~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
inference(nnf_transformation,[status(thm)],[f230]) ).
fof(f230_sk,plain,
! [V_x,V_ys,T_a] : ~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
inference(skolemisation,[status(esa)],[f230_nnf]) ).
cnf(c230,plain,
~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(X0,X1,X2),tc_List_Olist(X2)),c_Nat_Osize__class_Osize(X1,tc_List_Olist(X2)),tc_nat),
inference(cnf_transformation,[status(esa)],[f230_sk]) ).
cnf(f237,axiom,
c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I4_J_0) ).
fof(f237_nnf,plain,
! [V_nat,V_dB1_H,V_dB2_H] : c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
inference(nnf_transformation,[status(thm)],[f237]) ).
fof(f237_sk,plain,
! [V_nat,V_dB1_H,V_dB2_H] : c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
inference(skolemisation,[status(esa)],[f237_nnf]) ).
cnf(c237,plain,
c_Lambda_OdB_OVar(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f237_sk]) ).
cnf(f258,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f258_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f258]) ).
fof(f258_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f258_nnf]) ).
cnf(c258,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f258_sk]) ).
cnf(f259,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f259_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f259]) ).
fof(f259_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f259_nnf]) ).
cnf(c259,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f259_sk]) ).
cnf(f260,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f260_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f260]) ).
fof(f260_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f260_nnf]) ).
cnf(c260,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f260_sk]) ).
cnf(f261,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f261_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f261]) ).
fof(f261_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f261_nnf]) ).
cnf(c261,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f261_sk]) ).
cnf(f262,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f262_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f262]) ).
fof(f262_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f262_nnf]) ).
cnf(c262,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f262_sk]) ).
cnf(f274,axiom,
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__one__le__zero_0) ).
fof(f274_nnf,plain,
! [T_a] :
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f274]) ).
fof(f274_sk,plain,
! [T_a] :
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f274_nnf]) ).
cnf(c274,plain,
( ~ c_lessequals(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f274_sk]) ).
cnf(f308,axiom,
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq__eq_1) ).
fof(f308_nnf,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f308]) ).
fof(f308_sk,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f308_nnf]) ).
cnf(c308,plain,
( ~ c_lessequals(c_Suc(X1),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f308_sk]) ).
cnf(f320,axiom,
c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).
fof(f320_nnf,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f320]) ).
fof(f320_sk,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f320_nnf]) ).
cnf(c320,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f320_sk]) ).
cnf(f321,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).
fof(f321_nnf,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f321]) ).
fof(f321_sk,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f321_nnf]) ).
cnf(c321,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f321_sk]) ).
cnf(f372,axiom,
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_of__nat__less__0__iff_0) ).
fof(f372_nnf,plain,
! [T_a,V_m] :
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f372]) ).
fof(f372_sk,plain,
! [T_a,V_m] :
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f372_nnf]) ).
cnf(c372,plain,
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f372_sk]) ).
cnf(f409,axiom,
c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).
fof(f409_nnf,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(nnf_transformation,[status(thm)],[f409]) ).
fof(f409_sk,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(skolemisation,[status(esa)],[f409_nnf]) ).
cnf(c409,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f409_sk]) ).
cnf(f414,axiom,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_beta__cases_I1_J_0) ).
fof(f414_nnf,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(nnf_transformation,[status(thm)],[f414]) ).
fof(f414_sk,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(skolemisation,[status(esa)],[f414_nnf]) ).
cnf(c414,plain,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(X0),X1),
inference(cnf_transformation,[status(esa)],[f414_sk]) ).
cnf(f471,axiom,
~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f471_nnf,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f471]) ).
fof(f471_sk,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f471_nnf]) ).
cnf(c471,plain,
~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f471_sk]) ).
cnf(f491,axiom,
c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).
fof(f491_nnf,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(nnf_transformation,[status(thm)],[f491]) ).
fof(f491_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f491_nnf]) ).
cnf(c491,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f491_sk]) ).
cnf(f492,axiom,
V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f492_nnf,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(nnf_transformation,[status(thm)],[f492]) ).
fof(f492_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f492_nnf]) ).
cnf(c492,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f492_sk]) ).
cnf(f498,axiom,
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f498_nnf,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f498]) ).
fof(f498_sk,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f498_nnf]) ).
cnf(c498,plain,
( ~ c_HOL_Oord__class_Oless(X1,c_Suc(X0),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f498_sk]) ).
cnf(f512,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Abs__App__neq__Var__apps_0) ).
fof(f512_nnf,plain,
! [V_s,V_t,V_n,V_ss] : hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f512]) ).
fof(f512_sk,plain,
! [V_s,V_t,V_n,V_ss] : hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(skolemisation,[status(esa)],[f512_nnf]) ).
cnf(c512,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X0)),X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X2),X3,tc_Lambda_OdB,tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f512_sk]) ).
cnf(f531,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_length__greater__0__conv_0) ).
fof(f531_nnf,plain,
! [T_a] : ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat),
inference(nnf_transformation,[status(thm)],[f531]) ).
fof(f531_sk,plain,
! [T_a] : ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat),
inference(skolemisation,[status(esa)],[f531_nnf]) ).
cnf(c531,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(X0),tc_List_Olist(X0)),tc_nat),
inference(cnf_transformation,[status(esa)],[f531_sk]) ).
cnf(f535,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I5_J_0) ).
fof(f535_nnf,plain,
! [V_dB1_H,V_dB2_H,V_nat] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
inference(nnf_transformation,[status(thm)],[f535]) ).
fof(f535_sk,plain,
! [V_dB1_H,V_dB2_H,V_nat] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f535_nnf]) ).
cnf(c535,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f535_sk]) ).
cnf(f546,axiom,
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f546_nnf,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f546]) ).
fof(f546_sk,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f546_nnf]) ).
cnf(c546,plain,
( c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f546_sk]) ).
cnf(f555,axiom,
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f555_nnf,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f555]) ).
fof(f555_sk,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f555_nnf]) ).
cnf(c555,plain,
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f555_sk]) ).
cnf(f569,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
fof(f569_nnf,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f569]) ).
fof(f569_sk,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f569_nnf]) ).
cnf(c569,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f569_sk]) ).
cnf(f572,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(f572_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f572]) ).
fof(f572_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f572_nnf]) ).
cnf(c572,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f572_sk]) ).
cnf(f573,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(f573_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f573]) ).
fof(f573_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f573_nnf]) ).
cnf(c573,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f573_sk]) ).
cnf(f582,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(f582_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f582]) ).
fof(f582_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f582_nnf]) ).
cnf(c582,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f582_sk]) ).
cnf(f583,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(f583_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f583]) ).
fof(f583_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f583_nnf]) ).
cnf(c583,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f583_sk]) ).
cnf(f585,axiom,
~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_j),V_i,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__add__less1_0) ).
fof(f585_nnf,plain,
! [V_i,V_j] : ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_j),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f585]) ).
fof(f585_sk,plain,
! [V_i,V_j] : ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_j),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f585_nnf]) ).
cnf(c585,plain,
~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f585_sk]) ).
cnf(f586,axiom,
~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_i),V_i,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__add__less2_0) ).
fof(f586_nnf,plain,
! [V_j,V_i] : ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_i),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f586]) ).
fof(f586_sk,plain,
! [V_j,V_i] : ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_i),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f586_nnf]) ).
cnf(c586,plain,
~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),X1,tc_nat),
inference(cnf_transformation,[status(esa)],[f586_sk]) ).
cnf(f595,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f595_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f595]) ).
fof(f595_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f595_nnf]) ).
cnf(c595,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f595_sk]) ).
cnf(f596,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f596_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f596]) ).
fof(f596_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f596_nnf]) ).
cnf(c596,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f596_sk]) ).
cnf(f625,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I9_J_0) ).
fof(f625_nnf,plain,
! [V_dB_H,V_dB1,V_dB2] : c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
inference(nnf_transformation,[status(thm)],[f625]) ).
fof(f625_sk,plain,
! [V_dB_H,V_dB1,V_dB2] : c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
inference(skolemisation,[status(esa)],[f625_nnf]) ).
cnf(c625,plain,
c_Lambda_OdB_OAbs(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f625_sk]) ).
cnf(f631,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I8_J_0) ).
fof(f631_nnf,plain,
! [V_dB1,V_dB2,V_dB_H] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
inference(nnf_transformation,[status(thm)],[f631]) ).
fof(f631_sk,plain,
! [V_dB1,V_dB2,V_dB_H] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f631_nnf]) ).
cnf(c631,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f631_sk]) ).
cnf(f632,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I7_J_0) ).
fof(f632_nnf,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(nnf_transformation,[status(thm)],[f632]) ).
fof(f632_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f632_nnf]) ).
cnf(c632,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f632_sk]) ).
cnf(f678,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f678_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f678]) ).
fof(f678_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f678_nnf]) ).
cnf(c678,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f678_sk]) ).
cnf(f679,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f679_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f679]) ).
fof(f679_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f679_nnf]) ).
cnf(c679,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f679_sk]) ).
cnf(f682,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f682_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f682]) ).
fof(f682_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f682_nnf]) ).
cnf(c682,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f682_sk]) ).
cnf(f683,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f683_nnf,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f683]) ).
fof(f683_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f683_nnf]) ).
cnf(c683,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f683_sk]) ).
cnf(f686,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f686_nnf,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f686]) ).
fof(f686_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f686_nnf]) ).
cnf(c686,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f686_sk]) ).
cnf(f687,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f687_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f687]) ).
fof(f687_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f687_nnf]) ).
cnf(c687,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f687_sk]) ).
cnf(f737,axiom,
hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) != c_Type_Otype_OAtom(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_type_Osimps_I4_J_0) ).
fof(f737_nnf,plain,
! [V_type1_H,V_type2_H,V_nat] : hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) != c_Type_Otype_OAtom(V_nat),
inference(nnf_transformation,[status(thm)],[f737]) ).
fof(f737_sk,plain,
! [V_type1_H,V_type2_H,V_nat] : hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) != c_Type_Otype_OAtom(V_nat),
inference(skolemisation,[status(esa)],[f737_nnf]) ).
cnf(c737,plain,
hAPP(hAPP(c_Type_Otype_OFun,X0),X1) != c_Type_Otype_OAtom(X2),
inference(cnf_transformation,[status(esa)],[f737_sk]) ).
cnf(f744,axiom,
c_Type_Otype_OAtom(V_nat) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_type_Osimps_I3_J_0) ).
fof(f744_nnf,plain,
! [V_nat,V_type1_H,V_type2_H] : c_Type_Otype_OAtom(V_nat) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H),
inference(nnf_transformation,[status(thm)],[f744]) ).
fof(f744_sk,plain,
! [V_nat,V_type1_H,V_type2_H] : c_Type_Otype_OAtom(V_nat) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H),
inference(skolemisation,[status(esa)],[f744_nnf]) ).
cnf(c744,plain,
c_Type_Otype_OAtom(X0) != hAPP(hAPP(c_Type_Otype_OFun,X1),X2),
inference(cnf_transformation,[status(esa)],[f744_sk]) ).
cnf(f762,axiom,
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_power__eq__0__iff_1) ).
fof(f762_nnf,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f762]) ).
fof(f762_sk,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f762_nnf]) ).
cnf(c762,plain,
( c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Power_Opower(X0)
| ~ class_Ring__and__Field_Omult__zero(X0)
| ~ class_Ring__and__Field_Ono__zero__divisors(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f762_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c142,c144,c146,c148,c198,c225,c226,c230,c237,c258,c259,c260,c261,c262,c274,c308,c320,c321,c372,c409,c414,c471,c491,c492,c498,c512,c531,c535,c546,c555,c569,c572,c573,c582,c583,c585,c586,c595,c596,c625,c631,c632,c678,c679,c682,c683,c686,c687,c737,c744,c762,c785]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1931]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL815-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n015.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 00:35:26 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 103.43/13.45 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 103.43/13.45 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------