%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL795-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 : n014.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:03 PM UTC 2026
% Result : Unsatisfiable 22.10s 3.19s
% Output : Proof 22.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 60
% Syntax : Number of formulae : 266 ( 190 unt; 0 def)
% Number of atoms : 386 ( 150 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 438 ( 318 ~; 120 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 36 ( 36 usr; 19 con; 0-5 aty)
% Number of variables : 506 ( 113 sgn 232 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f879,negated_conjecture,
~ c_Type_Otyping(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),v_T_H_H____,tc_Type_Otype),c_Lambda_Olift(v_u____,c_HOL_Ozero__class_Ozero(tc_nat)),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f879_nnf,plain,
~ c_Type_Otyping(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),v_T_H_H____,tc_Type_Otype),c_Lambda_Olift(v_u____,c_HOL_Ozero__class_Ozero(tc_nat)),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
inference(nnf_transformation,[status(thm)],[f879]) ).
fof(f879_sk,plain,
~ c_Type_Otyping(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),v_T_H_H____,tc_Type_Otype),c_Lambda_Olift(v_u____,c_HOL_Ozero__class_Ozero(tc_nat)),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
inference(skolemisation,[status(esa)],[f879_nnf]) ).
cnf(c879,plain,
~ c_Type_Otyping(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),v_T_H_H____,tc_Type_Otype),c_Lambda_Olift(v_u____,c_HOL_Ozero__class_Ozero(tc_nat)),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
inference(cnf_transformation,[status(esa)],[f879_sk]) ).
cnf(t95,plain,
c_Type_Otyping(c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),v_T_H_H____,tc_Type_Otype),c_Lambda_Olift(v_u____,c_HOL_Ozero__class_Ozero(tc_nat)),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) = false,
inference(equality_encoding,[status(esa)],[c879]) ).
cnf(t102,axiom,
sF0 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition) ).
cnf(t111,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = sF0,
inference(orient,[status(thm)],[t102]) ).
cnf(t1104,plain,
c_Type_Otyping(c_Type_Oshift(v_e____,sF0,v_T_H_H____,tc_Type_Otype),c_Lambda_Olift(v_u____,c_HOL_Ozero__class_Ozero(tc_nat)),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) = false,
inference(step,[status(thm)],[t95,t111]) ).
cnf(t103,axiom,
sF1 = c_Type_Oshift(v_e____,c_HOL_Ozero__class_Ozero(tc_nat),v_T_H_H____,tc_Type_Otype),
introduced(definition) ).
cnf(t1008,plain,
sF1 = c_Type_Oshift(v_e____,sF0,v_T_H_H____,tc_Type_Otype),
inference(step,[status(thm)],[t103,t111]) ).
cnf(t134,plain,
c_Type_Oshift(v_e____,sF0,v_T_H_H____,tc_Type_Otype) = sF1,
inference(orient,[status(thm)],[t1008]) ).
cnf(t1105,plain,
c_Type_Otyping(sF1,c_Lambda_Olift(v_u____,c_HOL_Ozero__class_Ozero(tc_nat)),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) = false,
inference(step,[status(thm)],[t1104,t134]) ).
cnf(t1106,plain,
c_Type_Otyping(sF1,c_Lambda_Olift(v_u____,sF0),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) = false,
inference(step,[status(thm)],[t1105,t111]) ).
cnf(t104,axiom,
sF2 = c_Lambda_Olift(v_u____,c_HOL_Ozero__class_Ozero(tc_nat)),
introduced(definition) ).
cnf(t1005,plain,
sF2 = c_Lambda_Olift(v_u____,sF0),
inference(step,[status(thm)],[t104,t111]) ).
cnf(t120,plain,
c_Lambda_Olift(v_u____,sF0) = sF2,
inference(orient,[status(thm)],[t1005]) ).
cnf(t1107,plain,
c_Type_Otyping(sF1,sF2,hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) = false,
inference(step,[status(thm)],[t1106,t120]) ).
cnf(f847,axiom,
c_List_Ofoldr(V_f,c_List_Olist_OCons(V_x,V_xs,T_b),V_a,T_b,T_a) = hAPP(hAPP(V_f,V_x),c_List_Ofoldr(V_f,V_xs,V_a,T_b,T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_foldr_Osimps_I2_J_0) ).
fof(f847_nnf,plain,
! [V_f,V_x,V_xs,T_b,V_a,T_a] : c_List_Ofoldr(V_f,c_List_Olist_OCons(V_x,V_xs,T_b),V_a,T_b,T_a) = hAPP(hAPP(V_f,V_x),c_List_Ofoldr(V_f,V_xs,V_a,T_b,T_a)),
inference(nnf_transformation,[status(thm)],[f847]) ).
fof(f847_sk,plain,
! [V_f,V_x,V_xs,T_b,V_a,T_a] : c_List_Ofoldr(V_f,c_List_Olist_OCons(V_x,V_xs,T_b),V_a,T_b,T_a) = hAPP(hAPP(V_f,V_x),c_List_Ofoldr(V_f,V_xs,V_a,T_b,T_a)),
inference(skolemisation,[status(esa)],[f847_nnf]) ).
cnf(c847,plain,
c_List_Ofoldr(X0,c_List_Olist_OCons(X1,X2,X3),X4,X3,X5) = hAPP(hAPP(X0,X1),c_List_Ofoldr(X0,X2,X4,X3,X5)),
inference(cnf_transformation,[status(esa)],[f847_sk]) ).
cnf(t90,plain,
hAPP(hAPP(X1,X2),c_List_Ofoldr(X1,X3,X4,X5,X6)) = c_List_Ofoldr(X1,c_List_Olist_OCons(X2,X3,X5),X4,X5,X6),
inference(equality_encoding,[status(esa)],[c847]) ).
cnf(t775,plain,
hAPP(hAPP(X1,X2),c_List_Ofoldr(X1,X3,X4,X5,X6)) = c_List_Ofoldr(X1,c_List_Olist_OCons(X2,X3,X5),X4,X5,X6),
inference(orient,[status(thm)],[t90]) ).
cnf(t1108,plain,
c_Type_Otyping(sF1,sF2,c_List_Ofoldr(c_Type_Otype_OFun,c_List_Olist_OCons(v_T_H_H____,v_Ts____,tc_Type_Otype),v_T_H____,tc_Type_Otype,tc_Type_Otype)) = false,
inference(step,[status(thm)],[t1107,t775]) ).
cnf(t105,axiom,
sF3 = hAPP(c_Type_Otype_OFun,v_T_H_H____),
introduced(definition) ).
cnf(t113,plain,
hAPP(c_Type_Otype_OFun,v_T_H_H____) = sF3,
inference(orient,[status(thm)],[t105]) ).
cnf(t776,plain,
c_List_Ofoldr(c_Type_Otype_OFun,c_List_Olist_OCons(v_T_H_H____,X1,X2),X3,X2,X4) = hAPP(sF3,c_List_Ofoldr(c_Type_Otype_OFun,X1,X3,X2,X4)),
inference(cp,[status(thm)],[t775,t113]) ).
cnf(t868,plain,
c_List_Ofoldr(c_Type_Otype_OFun,c_List_Olist_OCons(v_T_H_H____,X1,X2),X3,X2,X4) = hAPP(sF3,c_List_Ofoldr(c_Type_Otype_OFun,X1,X3,X2,X4)),
inference(orient,[status(thm)],[t776]) ).
cnf(t1109,plain,
c_Type_Otyping(sF1,sF2,hAPP(sF3,c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) = false,
inference(step,[status(thm)],[t1108,t868]) ).
cnf(t106,axiom,
sF4 = c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype),
introduced(definition) ).
cnf(t135,plain,
c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype) = sF4,
inference(orient,[status(thm)],[t106]) ).
cnf(t1110,plain,
c_Type_Otyping(sF1,sF2,hAPP(sF3,sF4)) = false,
inference(step,[status(thm)],[t1109,t135]) ).
cnf(f873,axiom,
v_T____ = hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_T_0) ).
fof(f873_nnf,plain,
v_T____ = hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)),
inference(nnf_transformation,[status(thm)],[f873]) ).
cnf(c873,plain,
v_T____ = hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)),
inference(cnf_transformation,[status(esa)],[f873_nnf]) ).
cnf(t56,plain,
hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)) = v_T____,
inference(equality_encoding,[status(esa)],[c873]) ).
cnf(t1020,plain,
hAPP(sF3,c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)) = v_T____,
inference(step,[status(thm)],[t56,t113]) ).
cnf(t1021,plain,
hAPP(sF3,sF4) = v_T____,
inference(step,[status(thm)],[t1020,t135]) ).
cnf(t223,plain,
hAPP(sF3,sF4) = v_T____,
inference(orient,[status(thm)],[t1021]) ).
cnf(t107,axiom,
sF5 = hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)),
introduced(definition) ).
cnf(t1022,plain,
sF5 = hAPP(sF3,c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)),
inference(step,[status(thm)],[t107,t113]) ).
cnf(t1023,plain,
sF5 = hAPP(sF3,sF4),
inference(step,[status(thm)],[t1022,t135]) ).
cnf(t1024,plain,
sF5 = v_T____,
inference(step,[status(thm)],[t1023,t223]) ).
cnf(t237,plain,
v_T____ = sF5,
inference(orient,[status(thm)],[t1024]) ).
cnf(t1026,plain,
hAPP(sF3,sF4) = sF5,
inference(step,[status(thm)],[t223,t237]) ).
cnf(t239,plain,
hAPP(sF3,sF4) = sF5,
inference(orient,[status(thm)],[t1026]) ).
cnf(t1111,plain,
c_Type_Otyping(sF1,sF2,sF5) = false,
inference(step,[status(thm)],[t1110,t239]) ).
cnf(f874,axiom,
( ~ c_Type_Otyping(V_e,V_t,V_T)
| c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_U,tc_Type_Otype),c_Lambda_Olift(V_t,V_i),V_T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_lift__type_0) ).
fof(f874_nnf,plain,
! [V_e,V_i,V_U,V_t,V_T] :
( ~ c_Type_Otyping(V_e,V_t,V_T)
| c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_U,tc_Type_Otype),c_Lambda_Olift(V_t,V_i),V_T) ),
inference(nnf_transformation,[status(thm)],[f874]) ).
fof(f874_sk,plain,
! [V_e,V_i,V_U,V_t,V_T] :
( ~ c_Type_Otyping(V_e,V_t,V_T)
| c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_U,tc_Type_Otype),c_Lambda_Olift(V_t,V_i),V_T) ),
inference(skolemisation,[status(esa)],[f874_nnf]) ).
cnf(c874,plain,
( ~ c_Type_Otyping(X0,X3,X4)
| c_Type_Otyping(c_Type_Oshift(X0,X1,X2,tc_Type_Otype),c_Lambda_Olift(X3,X1),X4) ),
inference(cnf_transformation,[status(esa)],[f874_sk]) ).
cnf(t89,plain,
ifeq(c_Type_Otyping(X1,X2,X3),true,c_Type_Otyping(c_Type_Oshift(X1,X4,X5,tc_Type_Otype),c_Lambda_Olift(X2,X4),X3),true) = true,
inference(equality_encoding,[status(esa)],[c874]) ).
cnf(t720,plain,
ifeq(c_Type_Otyping(X1,X2,X3),true,c_Type_Otyping(c_Type_Oshift(X1,X4,X5,tc_Type_Otype),c_Lambda_Olift(X2,X4),X3),true) = true,
inference(orient,[status(thm)],[t89]) ).
cnf(f871,axiom,
c_Type_Otyping(v_e____,v_u____,v_T____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_uT_0) ).
fof(f871_nnf,plain,
c_Type_Otyping(v_e____,v_u____,v_T____),
inference(nnf_transformation,[status(thm)],[f871]) ).
cnf(c871,plain,
c_Type_Otyping(v_e____,v_u____,v_T____),
inference(cnf_transformation,[status(esa)],[f871_nnf]) ).
cnf(t5,plain,
c_Type_Otyping(v_e____,v_u____,v_T____) = true,
inference(equality_encoding,[status(esa)],[c871]) ).
cnf(t116,plain,
c_Type_Otyping(v_e____,v_u____,v_T____) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t1025,plain,
c_Type_Otyping(v_e____,v_u____,sF5) = true,
inference(step,[status(thm)],[t116,t237]) ).
cnf(t238,plain,
c_Type_Otyping(v_e____,v_u____,sF5) = true,
inference(rw,[status(thm)],[t1025]) ).
cnf(t248,plain,
c_Type_Otyping(v_e____,v_u____,sF5) = true,
inference(orient,[status(thm)],[t238]) ).
cnf(t729,plain,
true = ifeq(true,true,c_Type_Otyping(c_Type_Oshift(v_e____,X1,X2,tc_Type_Otype),c_Lambda_Olift(v_u____,X1),sF5),true),
inference(cp,[status(thm)],[t720,t248]) ).
cnf(t17,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t126,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t17]) ).
cnf(t1096,plain,
true = c_Type_Otyping(c_Type_Oshift(v_e____,X1,X2,tc_Type_Otype),c_Lambda_Olift(v_u____,X1),sF5),
inference(step,[status(thm)],[t729,t126]) ).
cnf(t746,plain,
c_Type_Otyping(c_Type_Oshift(v_e____,X1,X2,tc_Type_Otype),c_Lambda_Olift(v_u____,X1),sF5) = true,
inference(orient,[status(thm)],[t1096]) ).
cnf(t748,plain,
true = c_Type_Otyping(sF1,c_Lambda_Olift(v_u____,sF0),sF5),
inference(cp,[status(thm)],[t746,t134]) ).
cnf(t1097,plain,
true = c_Type_Otyping(sF1,sF2,sF5),
inference(step,[status(thm)],[t748,t120]) ).
cnf(t750,plain,
c_Type_Otyping(sF1,sF2,sF5) = true,
inference(orient,[status(thm)],[t1097]) ).
cnf(t1112,plain,
true = false,
inference(step,[status(thm)],[t1111,t750]) ).
cnf(t896,plain,
false = true,
inference(orient,[status(thm)],[t1112]) ).
cnf(f156,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I6_J_0) ).
fof(f156_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)],[f156]) ).
fof(f156_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f156_nnf]) ).
cnf(c156,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f156_sk]) ).
cnf(f205,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f205_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)],[f205]) ).
fof(f205_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)],[f205_nnf]) ).
cnf(c205,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f205_sk]) ).
cnf(f207,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f207_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)],[f207]) ).
fof(f207_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)],[f207_nnf]) ).
cnf(c207,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f207_sk]) ).
cnf(f209,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f209_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)],[f209]) ).
fof(f209_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)],[f209_nnf]) ).
cnf(c209,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
cnf(f211,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/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f211_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)],[f211]) ).
fof(f211_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)],[f211_nnf]) ).
cnf(c211,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f211_sk]) ).
cnf(f296,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/sandbox2/benchmark/theBenchmark.p',cls_Var__apps__neq__Abs__apps_0) ).
fof(f296_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)],[f296]) ).
fof(f296_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)],[f296_nnf]) ).
cnf(c296,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)],[f296_sk]) ).
cnf(f301,axiom,
( ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Otimes__class_Otimes(V_x,V_x,T_a)),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a)),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__sum__squares__lt__zero_0) ).
fof(f301_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Otimes__class_Otimes(V_x,V_x,T_a)),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a)),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f301]) ).
fof(f301_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Otimes__class_Otimes(V_x,V_x,T_a)),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a)),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f301_nnf]) ).
cnf(c301,plain,
( ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),c_HOL_Otimes__class_Otimes(X1,X1,X0)),c_HOL_Otimes__class_Otimes(X2,X2,X0)),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f301_sk]) ).
cnf(f315,axiom,
c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I4_J_0) ).
fof(f315_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)],[f315]) ).
fof(f315_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)],[f315_nnf]) ).
cnf(c315,plain,
c_Lambda_OdB_OVar(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f315_sk]) ).
cnf(f336,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f336_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f336]) ).
fof(f336_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f336_nnf]) ).
cnf(c336,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f336_sk]) ).
cnf(f337,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f337_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f337]) ).
fof(f337_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f337_nnf]) ).
cnf(c337,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f337_sk]) ).
cnf(f338,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f338_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)],[f338]) ).
fof(f338_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)],[f338_nnf]) ).
cnf(c338,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f338_sk]) ).
cnf(f339,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f339_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)],[f339]) ).
fof(f339_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)],[f339_nnf]) ).
cnf(c339,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f339_sk]) ).
cnf(f340,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f340_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)],[f340]) ).
fof(f340_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)],[f340_nnf]) ).
cnf(c340,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f340_sk]) ).
cnf(f378,axiom,
c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).
fof(f378_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)],[f378]) ).
fof(f378_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)],[f378_nnf]) ).
cnf(c378,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f378_sk]) ).
cnf(f395,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__square__less__zero_0) ).
fof(f395_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f395]) ).
fof(f395_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f395_nnf]) ).
cnf(c395,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f395_sk]) ).
cnf(f399,axiom,
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq__eq_1) ).
fof(f399_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)],[f399]) ).
fof(f399_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)],[f399_nnf]) ).
cnf(c399,plain,
( ~ c_lessequals(c_Suc(X1),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f399_sk]) ).
cnf(f412,axiom,
c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).
fof(f412_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)],[f412]) ).
fof(f412_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)],[f412_nnf]) ).
cnf(c412,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f412_sk]) ).
cnf(f413,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).
fof(f413_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)],[f413]) ).
fof(f413_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)],[f413_nnf]) ).
cnf(c413,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f413_sk]) ).
cnf(f462,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/sandbox2/benchmark/theBenchmark.p',cls_of__nat__less__0__iff_0) ).
fof(f462_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)],[f462]) ).
fof(f462_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)],[f462_nnf]) ).
cnf(c462,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)],[f462_sk]) ).
cnf(f478,axiom,
c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).
fof(f478_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)],[f478]) ).
fof(f478_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f478_nnf]) ).
cnf(c478,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f478_sk]) ).
cnf(f479,axiom,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_beta__cases_I1_J_0) ).
fof(f479_nnf,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(nnf_transformation,[status(thm)],[f479]) ).
fof(f479_sk,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(skolemisation,[status(esa)],[f479_nnf]) ).
cnf(c479,plain,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(X0),X1),
inference(cnf_transformation,[status(esa)],[f479_sk]) ).
cnf(f532,axiom,
~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f532_nnf,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f532]) ).
fof(f532_sk,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f532_nnf]) ).
cnf(c532,plain,
~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f532_sk]) ).
cnf(f540,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/sandbox2/benchmark/theBenchmark.p',cls_not__add__less1_0) ).
fof(f540_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)],[f540]) ).
fof(f540_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)],[f540_nnf]) ).
cnf(c540,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)],[f540_sk]) ).
cnf(f541,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/sandbox2/benchmark/theBenchmark.p',cls_not__add__less2_0) ).
fof(f541_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)],[f541]) ).
fof(f541_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)],[f541_nnf]) ).
cnf(c541,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)],[f541_sk]) ).
cnf(f559,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f559_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f559]) ).
fof(f559_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f559_nnf]) ).
cnf(c559,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(f560,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f560_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f560]) ).
fof(f560_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f560_nnf]) ).
cnf(c560,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f560_sk]) ).
cnf(f579,axiom,
V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f579_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)],[f579]) ).
fof(f579_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f579_nnf]) ).
cnf(c579,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f579_sk]) ).
cnf(f583,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/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f583_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)],[f583]) ).
fof(f583_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)],[f583_nnf]) ).
cnf(c583,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)],[f583_sk]) ).
cnf(f616,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/sandbox2/benchmark/theBenchmark.p',cls_Abs__App__neq__Var__apps_0) ).
fof(f616_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)],[f616]) ).
fof(f616_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)],[f616_nnf]) ).
cnf(c616,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)],[f616_sk]) ).
cnf(f619,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sum__squares__gt__zero__iff_0) ).
fof(f619_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f619]) ).
fof(f619_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f619_nnf]) ).
cnf(c619,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0)),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0)),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f619_sk]) ).
cnf(f634,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I5_J_0) ).
fof(f634_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)],[f634]) ).
fof(f634_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)],[f634_nnf]) ).
cnf(c634,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f634_sk]) ).
cnf(f677,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/sandbox2/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
fof(f677_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)],[f677]) ).
fof(f677_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)],[f677_nnf]) ).
cnf(c677,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)],[f677_sk]) ).
cnf(f689,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I9_J_0) ).
fof(f689_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)],[f689]) ).
fof(f689_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)],[f689_nnf]) ).
cnf(c689,plain,
c_Lambda_OdB_OAbs(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f689_sk]) ).
cnf(f698,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I8_J_0) ).
fof(f698_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)],[f698]) ).
fof(f698_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)],[f698_nnf]) ).
cnf(c698,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f698_sk]) ).
cnf(f699,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I7_J_0) ).
fof(f699_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)],[f699]) ).
fof(f699_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f699_nnf]) ).
cnf(c699,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f699_sk]) ).
cnf(f773,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/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f773_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)],[f773]) ).
fof(f773_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)],[f773_nnf]) ).
cnf(c773,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)],[f773_sk]) ).
cnf(f774,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/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f774_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)],[f774]) ).
fof(f774_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)],[f774_nnf]) ).
cnf(c774,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)],[f774_sk]) ).
cnf(f777,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/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f777_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)],[f777]) ).
fof(f777_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)],[f777_nnf]) ).
cnf(c777,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)],[f777_sk]) ).
cnf(f778,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/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f778_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)],[f778]) ).
fof(f778_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)],[f778_nnf]) ).
cnf(c778,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)],[f778_sk]) ).
cnf(f781,axiom,
c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__neq__Zero_0) ).
fof(f781_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f781]) ).
fof(f781_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f781_nnf]) ).
cnf(c781,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f781_sk]) ).
cnf(f782,axiom,
c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
fof(f782_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f782]) ).
fof(f782_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f782_nnf]) ).
cnf(c782,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f782_sk]) ).
cnf(f803,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f803_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f803]) ).
fof(f803_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f803_nnf]) ).
cnf(c803,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f803_sk]) ).
cnf(f804,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f804_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f804]) ).
fof(f804_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f804_nnf]) ).
cnf(c804,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f804_sk]) ).
cnf(f812,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f812_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)],[f812]) ).
fof(f812_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f812_nnf]) ).
cnf(c812,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f812_sk]) ).
cnf(f813,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f813_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)],[f813]) ).
fof(f813_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f813_nnf]) ).
cnf(c813,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f813_sk]) ).
cnf(f839,axiom,
hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) != c_Type_Otype_OAtom(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_type_Osimps_I4_J_0) ).
fof(f839_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)],[f839]) ).
fof(f839_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)],[f839_nnf]) ).
cnf(c839,plain,
hAPP(hAPP(c_Type_Otype_OFun,X0),X1) != c_Type_Otype_OAtom(X2),
inference(cnf_transformation,[status(esa)],[f839_sk]) ).
cnf(f846,axiom,
c_Type_Otype_OAtom(V_nat) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_type_Osimps_I3_J_0) ).
fof(f846_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)],[f846]) ).
fof(f846_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)],[f846_nnf]) ).
cnf(c846,plain,
c_Type_Otype_OAtom(X0) != hAPP(hAPP(c_Type_Otype_OFun,X1),X2),
inference(cnf_transformation,[status(esa)],[f846_sk]) ).
cnf(f865,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/sandbox2/benchmark/theBenchmark.p',cls_power__eq__0__iff_1) ).
fof(f865_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)],[f865]) ).
fof(f865_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)],[f865_nnf]) ).
cnf(c865,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)],[f865_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c156,c205,c207,c209,c211,c296,c301,c315,c336,c337,c338,c339,c340,c378,c395,c399,c412,c413,c462,c478,c479,c532,c540,c541,c559,c560,c579,c583,c616,c619,c634,c677,c689,c698,c699,c773,c774,c777,c778,c781,c782,c803,c804,c812,c813,c839,c846,c865,c879]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t896]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL795-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 00:30:33 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 22.10/3.19 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.10/3.19 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------