%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL764-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 : n005.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:02:53 PM UTC 2026
% Result : Unsatisfiable 8.06s 1.44s
% Output : Proof 8.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 15
% Syntax : Number of formulae : 67 ( 63 unt; 0 def)
% Number of atoms : 71 ( 38 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 66 ( 62 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-4 aty)
% Number of variables : 150 ( 43 sgn 74 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f319,negated_conjecture,
~ c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f319_nnf,plain,
~ c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f319]) ).
fof(f319_sk,plain,
~ c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),
inference(skolemisation,[status(esa)],[f319_nnf]) ).
cnf(c319,plain,
~ c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f319_sk]) ).
cnf(hi328,negated_conjecture,
ifeq(c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c319]) ).
cnf(f318,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(f318_nnf,plain,
! [V_A,T_a] : c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f318]) ).
fof(f318_sk,plain,
! [V_A,T_a] : c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f318_nnf]) ).
cnf(c318,plain,
c_List_Olistsp(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f318_sk]) ).
cnf(hi305,axiom,
c_List_Olistsp(X0,c_List_Olist_ONil(X1),X1) = true,
inference(equality_encoding,[status(esa)],[c318]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi328,hi305]) ).
cnf(t626,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
cnf(f5,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f5_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(f6,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f6_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(f90,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(f90_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)],[f90]) ).
fof(f90_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f90_nnf]) ).
cnf(c90,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f90_sk]) ).
cnf(f91,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(f91_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)],[f91]) ).
fof(f91_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f91_nnf]) ).
cnf(c91,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
cnf(f143,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/sandbox2/benchmark/theBenchmark.p',cls_dropWhile__eq__Cons__conv_1) ).
fof(f143_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)],[f143]) ).
fof(f143_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)],[f143_nnf]) ).
cnf(c143,plain,
( ~ hBOOL(hAPP(X0,X3))
| c_List_OdropWhile(X0,X1,X2) != c_List_Olist_OCons(X3,X4,X2) ),
inference(cnf_transformation,[status(esa)],[f143_sk]) ).
cnf(f179,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(f179_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)],[f179]) ).
fof(f179_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)],[f179_nnf]) ).
cnf(c179,plain,
~ c_List_Onull(c_List_Olist_OCons(X0,X1,X2),X2),
inference(cnf_transformation,[status(esa)],[f179_sk]) ).
cnf(f233,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(f233_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)],[f233]) ).
fof(f233_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)],[f233_nnf]) ).
cnf(c233,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f233_sk]) ).
cnf(f236,axiom,
~ c_List_Omember(V_x,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_List_Omember_Osimps_I1_J_0) ).
fof(f236_nnf,plain,
! [V_x,T_a] : ~ c_List_Omember(V_x,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f236]) ).
fof(f236_sk,plain,
! [V_x,T_a] : ~ c_List_Omember(V_x,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f236_nnf]) ).
cnf(c236,plain,
~ c_List_Omember(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(f246,axiom,
~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__step1__Nil_0) ).
fof(f246_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)],[f246]) ).
fof(f246_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)],[f246_nnf]) ).
cnf(c246,plain,
~ c_ListOrder_Ostep1(X0,X1,c_List_Olist_ONil(X2),X2),
inference(cnf_transformation,[status(esa)],[f246_sk]) ).
cnf(f247,axiom,
~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Nil__step1_0) ).
fof(f247_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)],[f247]) ).
fof(f247_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)],[f247_nnf]) ).
cnf(c247,plain,
~ c_ListOrder_Ostep1(X0,c_List_Olist_ONil(X1),X2,X1),
inference(cnf_transformation,[status(esa)],[f247_sk]) ).
cnf(f267,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(f267_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)],[f267]) ).
fof(f267_sk,plain,
! [V_P,T_a] : ~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f267_nnf]) ).
cnf(c267,plain,
~ c_List_Olist__ex(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f267_sk]) ).
cnf(f286,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(f286_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)],[f286]) ).
fof(f286_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)],[f286_nnf]) ).
cnf(c286,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
cnf(f287,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(f287_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)],[f287]) ).
fof(f287_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)],[f287_nnf]) ).
cnf(c287,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f287_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c5,c6,c90,c91,c143,c179,c233,c236,c246,c247,c267,c286,c287,c319]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t626]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL764-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 00:27:48 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.06/1.44 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.06/1.44 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------