%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL825-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 : n011.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:09 PM UTC 2026
% Result : Unsatisfiable 18.57s 3.04s
% Output : Proof 18.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 24
% Syntax : Number of formulae : 110 ( 110 unt; 0 def)
% Number of atoms : 110 ( 79 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 85 ( 85 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 11 con; 0-5 aty)
% Number of variables : 232 ( 90 sgn 108 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f461,axiom,
class_Lattices_Olattice(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_nat__Lattices_Olattice) ).
fof(f461_nnf,plain,
class_Lattices_Olattice(tc_nat),
inference(nnf_transformation,[status(thm)],[f461]) ).
cnf(c461,plain,
class_Lattices_Olattice(tc_nat),
inference(cnf_transformation,[status(esa)],[f461_nnf]) ).
cnf(t1,plain,
class_Lattices_Olattice(tc_nat) = true,
inference(equality_encoding,[status(esa)],[c461]) ).
cnf(t608,plain,
class_Lattices_Olattice(tc_nat) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(f465,axiom,
class_Lattices_Olattice(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Lattices_Olattice) ).
fof(f465_nnf,plain,
class_Lattices_Olattice(tc_bool),
inference(nnf_transformation,[status(thm)],[f465]) ).
cnf(c465,plain,
class_Lattices_Olattice(tc_bool),
inference(cnf_transformation,[status(esa)],[f465_nnf]) ).
cnf(t0,plain,
class_Lattices_Olattice(tc_bool) = true,
inference(equality_encoding,[status(esa)],[c465]) ).
cnf(t613,plain,
class_Lattices_Olattice(tc_bool) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(f449,axiom,
c_List_Omap(V_f,c_List_Olist_ONil(T_b),T_b,T_a) = c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_map__is__Nil__conv_1) ).
fof(f449_nnf,plain,
! [V_f,T_b,T_a] : c_List_Omap(V_f,c_List_Olist_ONil(T_b),T_b,T_a) = c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f449]) ).
fof(f449_sk,plain,
! [V_f,T_b,T_a] : c_List_Omap(V_f,c_List_Olist_ONil(T_b),T_b,T_a) = c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f449_nnf]) ).
cnf(c449,plain,
c_List_Omap(X0,c_List_Olist_ONil(X1),X1,X2) = c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f449_sk]) ).
cnf(t41,plain,
c_List_Omap(X1,c_List_Olist_ONil(X2),X2,X3) = c_List_Olist_ONil(X3),
inference(equality_encoding,[status(esa)],[c449]) ).
cnf(t867,plain,
c_List_Omap(X1,c_List_Olist_ONil(X2),X2,X3) = c_List_Olist_ONil(X3),
inference(orient,[status(thm)],[t41]) ).
cnf(f447,axiom,
c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_listsp_ONil_0) ).
fof(f447_nnf,plain,
! [V_A,T_a] : c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f447]) ).
fof(f447_sk,plain,
! [V_A,T_a] : c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f447_nnf]) ).
cnf(c447,plain,
c_List_Olistsp(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f447_sk]) ).
cnf(t18,plain,
c_List_Olistsp(X1,c_List_Olist_ONil(X2),X2) = true,
inference(equality_encoding,[status(esa)],[c447]) ).
cnf(t591,plain,
c_List_Olistsp(X1,c_List_Olist_ONil(X2),X2) = true,
inference(orient,[status(thm)],[t18]) ).
cnf(t28,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t241,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t28]) ).
cnf(f11,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/sandbox2/benchmark/theBenchmark.p',cls_impossible__Cons_0) ).
fof(f11_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)],[f11]) ).
fof(f11_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)],[f11_nnf]) ).
cnf(c11,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)],[f11_sk]) ).
cnf(f122,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(f122_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)],[f122]) ).
fof(f122_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c122,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
cnf(f206,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(f206_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)],[f206]) ).
fof(f206_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f206_nnf]) ).
cnf(c206,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f206_sk]) ).
cnf(f207,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(f207_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)],[f207]) ).
fof(f207_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f207_nnf]) ).
cnf(c207,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f207_sk]) ).
cnf(f222,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(f222_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)],[f222]) ).
fof(f222_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)],[f222_nnf]) ).
cnf(c222,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)],[f222_sk]) ).
cnf(f229,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(f229_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)],[f229]) ).
fof(f229_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)],[f229_nnf]) ).
cnf(c229,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f229_sk]) ).
cnf(f244,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(f244_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)],[f244]) ).
fof(f244_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)],[f244_nnf]) ).
cnf(c244,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f244_sk]) ).
cnf(f256,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(f256_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)],[f256]) ).
fof(f256_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)],[f256_nnf]) ).
cnf(c256,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)],[f256_sk]) ).
cnf(f270,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(f270_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)],[f270]) ).
fof(f270_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)],[f270_nnf]) ).
cnf(c270,plain,
c_Lambda_OdB_OVar(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f270_sk]) ).
cnf(f287,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(f287_nnf,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(nnf_transformation,[status(thm)],[f287]) ).
fof(f287_sk,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(skolemisation,[status(esa)],[f287_nnf]) ).
cnf(c287,plain,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(X0),X1),
inference(cnf_transformation,[status(esa)],[f287_sk]) ).
cnf(f302,axiom,
~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_List_Onull_Osimps_I2_J_0) ).
fof(f302_nnf,plain,
! [V_x,V_xs,T_a] : ~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
inference(nnf_transformation,[status(thm)],[f302]) ).
fof(f302_sk,plain,
! [V_x,V_xs,T_a] : ~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
inference(skolemisation,[status(esa)],[f302_nnf]) ).
cnf(c302,plain,
~ c_List_Onull(c_List_Olist_OCons(X0,X1,X2),X2),
inference(cnf_transformation,[status(esa)],[f302_sk]) ).
cnf(f321,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(f321_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)],[f321]) ).
fof(f321_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)],[f321_nnf]) ).
cnf(c321,plain,
c_Lambda_OdB_OAbs(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f321_sk]) ).
cnf(f328,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(f328_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)],[f328]) ).
fof(f328_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)],[f328_nnf]) ).
cnf(c328,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f328_sk]) ).
cnf(f329,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(f329_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)],[f329]) ).
fof(f329_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f329_nnf]) ).
cnf(c329,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f329_sk]) ).
cnf(f365,axiom,
~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list__ex_Osimps_I1_J_0) ).
fof(f365_nnf,plain,
! [V_P,T_a] : ~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f365]) ).
fof(f365_sk,plain,
! [V_P,T_a] : ~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f365_nnf]) ).
cnf(c365,plain,
~ c_List_Olist__ex(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f365_sk]) ).
cnf(f383,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(f383_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)],[f383]) ).
fof(f383_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)],[f383_nnf]) ).
cnf(c383,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f383_sk]) ).
cnf(f384,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(f384_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)],[f384]) ).
fof(f384_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)],[f384_nnf]) ).
cnf(c384,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f384_sk]) ).
cnf(f441,axiom,
v_n____ != v_i____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_False_0) ).
fof(f441_nnf,plain,
v_n____ != v_i____,
inference(nnf_transformation,[status(thm)],[f441]) ).
fof(f441_sk,plain,
v_n____ != v_i____,
inference(skolemisation,[status(esa)],[f441_nnf]) ).
cnf(c441,plain,
v_n____ != v_i____,
inference(cnf_transformation,[status(esa)],[f441_sk]) ).
cnf(f452,negated_conjecture,
~ c_List_Olistsp(c_InductTermi_OIT,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____),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f452_nnf,plain,
~ c_List_Olistsp(c_InductTermi_OIT,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____),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f452]) ).
fof(f452_sk,plain,
~ c_List_Olistsp(c_InductTermi_OIT,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____),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
inference(skolemisation,[status(esa)],[f452_nnf]) ).
cnf(c452,plain,
~ c_List_Olistsp(c_InductTermi_OIT,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____),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f452_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c11,c122,c206,c207,c222,c229,c244,c256,c270,c287,c302,c321,c328,c329,c365,c383,c384,c441,c452]) ).
cnf(g0_0,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,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____),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),true,false,true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,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____),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),true,false,class_Lattices_Olattice(tc_nat)),
inference(rw,[status(thm)],[g0_0,t608]) ).
cnf(g0_2,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,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____),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),class_Lattices_Olattice(tc_bool),false,class_Lattices_Olattice(tc_nat)),
inference(rw,[status(thm)],[g0_1,t613]) ).
cnf(g0_3,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),class_Lattices_Olattice(tc_bool),false,class_Lattices_Olattice(tc_nat)),
inference(rw,[status(thm)],[g0_2,t867]) ).
cnf(g0_4,plain,
true != ifeq(true,class_Lattices_Olattice(tc_bool),false,class_Lattices_Olattice(tc_nat)),
inference(rw,[status(thm)],[g0_3,t591]) ).
cnf(g0_5,plain,
true != ifeq(true,class_Lattices_Olattice(tc_bool),false,true),
inference(rw,[status(thm)],[g0_4,t608]) ).
cnf(g0_6,plain,
true != ifeq(true,true,false,true),
inference(rw,[status(thm)],[g0_5,t613]) ).
cnf(g0_7,plain,
true != false,
inference(rw,[status(thm)],[g0_6,t241]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL825-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 : n011.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.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 00:33:27 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 18.57/3.04 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.57/3.04 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------