%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL830-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 : n012.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:10 PM UTC 2026
% Result : Unsatisfiable 16.18s 2.42s
% Output : Proof 16.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 26
% Syntax : Number of formulae : 122 ( 118 unt; 0 def)
% Number of atoms : 126 ( 91 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 103 ( 99 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 25 ( 25 usr; 12 con; 0-5 aty)
% Number of variables : 300 ( 102 sgn 136 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f451,negated_conjecture,
~ c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f451_nnf,plain,
~ c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f451]) ).
fof(f451_sk,plain,
~ c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
inference(skolemisation,[status(esa)],[f451_nnf]) ).
cnf(c451,plain,
~ c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f451_sk]) ).
cnf(t161,plain,
ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c451]) ).
cnf(t381,plain,
ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),true,false,true) = true,
inference(orient,[status(thm)],[t161]) ).
cnf(f450,axiom,
c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f450_nnf,plain,
c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f450]) ).
cnf(c450,plain,
c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f450_nnf]) ).
cnf(t166,plain,
c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB) = true,
inference(equality_encoding,[status(esa)],[c450]) ).
cnf(t513,plain,
c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB) = true,
inference(orient,[status(thm)],[t166]) ).
cnf(f443,axiom,
c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Cons_I3_J_0) ).
fof(f443_nnf,plain,
c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f443]) ).
cnf(c443,plain,
c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f443_nnf]) ).
cnf(t149,plain,
c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB) = true,
inference(equality_encoding,[status(esa)],[c443]) ).
cnf(t521,plain,
c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB) = true,
inference(orient,[status(thm)],[t149]) ).
cnf(f444,axiom,
c_List_Omap(V_f,c_List_Olist_OCons(V_x,V_xa,T_b),T_b,T_a) = c_List_Olist_OCons(hAPP(V_f,V_x),c_List_Omap(V_f,V_xa,T_b,T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_map__eq__Cons__conv_3) ).
fof(f444_nnf,plain,
! [V_f,V_x,V_xa,T_b,T_a] : c_List_Omap(V_f,c_List_Olist_OCons(V_x,V_xa,T_b),T_b,T_a) = c_List_Olist_OCons(hAPP(V_f,V_x),c_List_Omap(V_f,V_xa,T_b,T_a),T_a),
inference(nnf_transformation,[status(thm)],[f444]) ).
fof(f444_sk,plain,
! [V_f,V_x,V_xa,T_b,T_a] : c_List_Omap(V_f,c_List_Olist_OCons(V_x,V_xa,T_b),T_b,T_a) = c_List_Olist_OCons(hAPP(V_f,V_x),c_List_Omap(V_f,V_xa,T_b,T_a),T_a),
inference(skolemisation,[status(esa)],[f444_nnf]) ).
cnf(c444,plain,
c_List_Omap(X0,c_List_Olist_OCons(X1,X2,X3),X3,X4) = c_List_Olist_OCons(hAPP(X0,X1),c_List_Omap(X0,X2,X3,X4),X4),
inference(cnf_transformation,[status(esa)],[f444_sk]) ).
cnf(t114,plain,
c_List_Olist_OCons(hAPP(X1,X2),c_List_Omap(X1,X3,X4,X5),X5) = c_List_Omap(X1,c_List_Olist_OCons(X2,X3,X4),X4,X5),
inference(equality_encoding,[status(esa)],[c444]) ).
cnf(t834,plain,
c_List_Olist_OCons(hAPP(X1,X2),c_List_Omap(X1,X3,X4,X5),X5) = c_List_Omap(X1,c_List_Olist_OCons(X2,X3,X4),X4,X5),
inference(orient,[status(thm)],[t114]) ).
cnf(f442,axiom,
hAPP(c_COMBC(V_P,V_Q,T_b,T_c,T_a),V_R) = hAPP(hAPP(V_P,V_R),V_Q),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBC__def_0) ).
fof(f442_nnf,plain,
! [V_P,V_Q,T_b,T_c,T_a,V_R] : hAPP(c_COMBC(V_P,V_Q,T_b,T_c,T_a),V_R) = hAPP(hAPP(V_P,V_R),V_Q),
inference(nnf_transformation,[status(thm)],[f442]) ).
fof(f442_sk,plain,
! [V_P,V_Q,T_b,T_c,T_a,V_R] : hAPP(c_COMBC(V_P,V_Q,T_b,T_c,T_a),V_R) = hAPP(hAPP(V_P,V_R),V_Q),
inference(skolemisation,[status(esa)],[f442_nnf]) ).
cnf(c442,plain,
hAPP(c_COMBC(X0,X1,X2,X3,X4),X5) = hAPP(hAPP(X0,X5),X1),
inference(cnf_transformation,[status(esa)],[f442_sk]) ).
cnf(t76,plain,
hAPP(c_COMBC(X1,X2,X3,X4,X5),X6) = hAPP(hAPP(X1,X6),X2),
inference(equality_encoding,[status(esa)],[c442]) ).
cnf(t529,plain,
hAPP(c_COMBC(X1,X2,X3,X4,X5),X6) = hAPP(hAPP(X1,X6),X2),
inference(orient,[status(thm)],[t76]) ).
cnf(t20,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t192,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t20]) ).
cnf(f12,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(f12_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)],[f12]) ).
fof(f12_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)],[f12_nnf]) ).
cnf(c12,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)],[f12_sk]) ).
cnf(f120,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(f120_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)],[f120]) ).
fof(f120_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f120_nnf]) ).
cnf(c120,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
cnf(f122,axiom,
~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Nil__step1_0) ).
fof(f122_nnf,plain,
! [V_r,T_a,V_xs] : ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
inference(nnf_transformation,[status(thm)],[f122]) ).
fof(f122_sk,plain,
! [V_r,T_a,V_xs] : ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c122,plain,
~ c_ListOrder_Ostep1(X0,c_List_Olist_ONil(X1),X2,X1),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
cnf(f123,axiom,
~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__step1__Nil_0) ).
fof(f123_nnf,plain,
! [V_r,V_xs,T_a] : ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f123]) ).
fof(f123_sk,plain,
! [V_r,V_xs,T_a] : ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f123_nnf]) ).
cnf(c123,plain,
~ c_ListOrder_Ostep1(X0,X1,c_List_Olist_ONil(X2),X2),
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
cnf(f128,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(f128_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)],[f128]) ).
fof(f128_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)],[f128_nnf]) ).
cnf(c128,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)],[f128_sk]) ).
cnf(f162,axiom,
~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list__ex_Osimps_I1_J_0) ).
fof(f162_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)],[f162]) ).
fof(f162_sk,plain,
! [V_P,T_a] : ~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f162_nnf]) ).
cnf(c162,plain,
~ c_List_Olist__ex(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f162_sk]) ).
cnf(f223,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(f223_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)],[f223]) ).
fof(f223_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)],[f223_nnf]) ).
cnf(c223,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)],[f223_sk]) ).
cnf(f232,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(f232_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)],[f232]) ).
fof(f232_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)],[f232_nnf]) ).
cnf(c232,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f232_sk]) ).
cnf(f245,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(f245_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)],[f245]) ).
fof(f245_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)],[f245_nnf]) ).
cnf(c245,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f245_sk]) ).
cnf(f260,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(f260_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)],[f260]) ).
fof(f260_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)],[f260_nnf]) ).
cnf(c260,plain,
c_Lambda_OdB_OVar(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f260_sk]) ).
cnf(f280,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(f280_nnf,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(nnf_transformation,[status(thm)],[f280]) ).
fof(f280_sk,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(skolemisation,[status(esa)],[f280_nnf]) ).
cnf(c280,plain,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(X0),X1),
inference(cnf_transformation,[status(esa)],[f280_sk]) ).
cnf(f319,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(f319_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)],[f319]) ).
fof(f319_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)],[f319_nnf]) ).
cnf(c319,plain,
c_Lambda_OdB_OAbs(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f319_sk]) ).
cnf(f325,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(f325_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)],[f325]) ).
fof(f325_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)],[f325_nnf]) ).
cnf(c325,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f325_sk]) ).
cnf(f326,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(f326_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)],[f326]) ).
fof(f326_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f326_nnf]) ).
cnf(c326,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f326_sk]) ).
cnf(f358,axiom,
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dropWhile__eq__Cons__conv_1) ).
fof(f358_nnf,plain,
! [V_P,V_xs,T_a,V_y,V_ys] :
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
inference(nnf_transformation,[status(thm)],[f358]) ).
fof(f358_sk,plain,
! [V_P,V_xs,T_a,V_y,V_ys] :
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
inference(skolemisation,[status(esa)],[f358_nnf]) ).
cnf(c358,plain,
( ~ hBOOL(hAPP(X0,X3))
| c_List_OdropWhile(X0,X1,X2) != c_List_Olist_OCons(X3,X4,X2) ),
inference(cnf_transformation,[status(esa)],[f358_sk]) ).
cnf(f377,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(f377_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)],[f377]) ).
fof(f377_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)],[f377_nnf]) ).
cnf(c377,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f377_sk]) ).
cnf(f378,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(f378_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)],[f378]) ).
fof(f378_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)],[f378_nnf]) ).
cnf(c378,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f378_sk]) ).
cnf(f427,axiom,
v_n____ != v_i____,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_False_0) ).
fof(f427_nnf,plain,
v_n____ != v_i____,
inference(nnf_transformation,[status(thm)],[f427]) ).
fof(f427_sk,plain,
v_n____ != v_i____,
inference(skolemisation,[status(esa)],[f427_nnf]) ).
cnf(c427,plain,
v_n____ != v_i____,
inference(cnf_transformation,[status(esa)],[f427_sk]) ).
cnf(f448,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(f448_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)],[f448]) ).
fof(f448_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f448_nnf]) ).
cnf(c448,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f448_sk]) ).
cnf(f449,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(f449_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)],[f449]) ).
fof(f449_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f449_nnf]) ).
cnf(c449,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f449_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c12,c120,c122,c123,c128,c162,c223,c232,c245,c260,c280,c319,c325,c326,c358,c377,c378,c427,c448,c449,c451]) ).
cnf(g0_0,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),true,false,true),
inference(rw,[status(thm)],[goal_0,t381]) ).
cnf(g0_1,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),true,false,c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)),
inference(rw,[status(thm)],[g0_0,t513]) ).
cnf(g0_2,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),false,c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)),
inference(rw,[status(thm)],[g0_1,t521]) ).
cnf(g0_3,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_a____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),false,c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)),
inference(rw,[status(thm)],[g0_2,t834]) ).
cnf(g0_4,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_a____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),false,c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)),
inference(rw,[status(thm)],[g0_3,t529]) ).
cnf(g0_5,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_a____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),false,true),
inference(rw,[status(thm)],[g0_4,t513]) ).
cnf(g0_6,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_a____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),true,false,true),
inference(rw,[status(thm)],[g0_5,t521]) ).
cnf(g0_7,plain,
true != ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),true,false,true),
inference(rw,[status(thm)],[g0_6,t529]) ).
cnf(g0_8,plain,
true != ifeq(true,true,false,true),
inference(rw,[status(thm)],[g0_7,t513]) ).
cnf(g0_9,plain,
true != false,
inference(rw,[status(thm)],[g0_8,t192]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL830-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n012.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 00:33:36 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 16.18/2.42 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.18/2.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------