%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV254-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 : Thu Sep 24 02:47:02 PM UTC 2026
% Result : Unsatisfiable 3.09s 0.94s
% Output : CNFRefutation 3.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 16
% Syntax : Number of formulae : 54 ( 36 unt; 2 def)
% Number of atoms : 72 ( 49 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 33 ( 15 ~; 16 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-3 aty)
% Number of variables : 118 ( 118 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1532,axiom,
! [V_ys,T_a] : c_append(c_List_Olist_ONil,V_ys,T_a) = V_ys,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1534,axiom,
! [V_xs,T_a] : c_append(V_xs,c_List_Olist_ONil,T_a) = V_xs,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1535,axiom,
! [V_n,V_y,T_a] : c_append(c_List_Otake(V_n,V_y,T_a),c_List_Odrop(V_n,V_y,T_a),T_a) = V_y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1537,axiom,
! [V_x,T_a__1] : c_List_Obutlast(c_List_Olist_OCons(V_x,c_List_Olist_ONil,T_a__1),T_a__1) = c_List_Olist_ONil,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1539,axiom,
! [V_y,V_x,T_a] : c_List_Obutlast(c_append(V_y,c_List_Olist_OCons(V_x,c_List_Olist_ONil,T_a),T_a),T_a) = V_y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1569,axiom,
! [V_y,T_a] : c_List_Odrop(c_0,V_y,T_a) = V_y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1573,axiom,
! [V_n,V_xs,V_ys,T_a] : c_List_Odrop(V_n,c_append(V_xs,V_ys,T_a),T_a) = c_append(c_List_Odrop(V_n,V_xs,T_a),c_List_Odrop(c_minus(V_n,c_Nat_Osize(V_xs,tc_List_Olist(T_a)),tc_nat),V_ys,T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1576,axiom,
! [V_xs,T_a,V_n] :
( c_List_Odrop(V_n,V_xs,T_a) = c_List_Olist_ONil
| ~ c_lessequals(c_Nat_Osize(V_xs,tc_List_Olist(T_a)),V_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1577,axiom,
! [V_i,V_k,V_x,T_a] : c_List_Odrop(V_i,c_List_Oreplicate(V_k,V_x,T_a),T_a) = c_List_Oreplicate(c_minus(V_k,V_i,tc_nat),V_x,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1583,axiom,
! [V_n,V_y,T_a] :
( c_List_Ohd(c_List_Oreplicate(V_n,V_y,T_a),T_a) = V_y
| V_n = c_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1607,axiom,
! [V_y,V_x,T_a] : c_Nat_Osize(c_List_Oreplicate(V_y,V_x,T_a),tc_List_Olist(T_a)) = V_y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1689,axiom,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2788,negated_conjecture,
! [V_U] : c_lessequals(V_U,v_x(V_U),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2789,negated_conjecture,
! [V_U] : v_x(V_U) = v_nat,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4472,plain,
! [X0,X1] : c_append(c_List_Olist_ONil,X0,X1) = X0,
inference(cnf_transformation,[status(thm)],[f1532]) ).
fof(f4475,plain,
! [X0,X1] : c_append(X0,c_List_Olist_ONil,X1) = X0,
inference(cnf_transformation,[status(thm)],[f1534]) ).
fof(f4476,plain,
! [X0,X1,X2] : c_append(c_List_Otake(X0,X1,X2),c_List_Odrop(X0,X1,X2),X2) = X1,
inference(cnf_transformation,[status(thm)],[f1535]) ).
fof(f4478,plain,
! [X0,X1] : c_List_Obutlast(c_List_Olist_OCons(X0,c_List_Olist_ONil,X1),X1) = c_List_Olist_ONil,
inference(cnf_transformation,[status(thm)],[f1537]) ).
fof(f4481,plain,
! [X0,X1,X2] : c_List_Obutlast(c_append(X0,c_List_Olist_OCons(X1,c_List_Olist_ONil,X2),X2),X2) = X0,
inference(cnf_transformation,[status(thm)],[f1539]) ).
fof(f4523,plain,
! [X0,X1] : c_List_Odrop(c_0,X0,X1) = X0,
inference(cnf_transformation,[status(thm)],[f1569]) ).
fof(f4529,plain,
! [X0,X1,X2,X3] : c_List_Odrop(X0,c_append(X1,X2,X3),X3) = c_append(c_List_Odrop(X0,X1,X3),c_List_Odrop(c_minus(X0,c_Nat_Osize(X1,tc_List_Olist(X3)),tc_nat),X2,X3),X3),
inference(cnf_transformation,[status(thm)],[f1573]) ).
fof(f4532,plain,
! [X0,X1,X2] :
( c_List_Odrop(X2,X0,X1) = c_List_Olist_ONil
| ~ c_lessequals(c_Nat_Osize(X0,tc_List_Olist(X1)),X2,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f1576]) ).
fof(f4533,plain,
! [X0,X1,X2,X3] : c_List_Odrop(X0,c_List_Oreplicate(X1,X2,X3),X3) = c_List_Oreplicate(c_minus(X1,X0,tc_nat),X2,X3),
inference(cnf_transformation,[status(thm)],[f1577]) ).
fof(f4542,plain,
! [V_n] :
( ! [V_y,T_a] : c_List_Ohd(c_List_Oreplicate(V_n,V_y,T_a),T_a) = V_y
| V_n = c_0 ),
inference(miniscoping,[status(thm)],[f1583]) ).
fof(f4543,plain,
! [X0,X1,X2] :
( c_List_Ohd(c_List_Oreplicate(X0,X1,X2),X2) = X1
| X0 = c_0 ),
inference(cnf_transformation,[status(thm)],[f4542]) ).
fof(f4573,plain,
! [X0,X1,X2] : c_Nat_Osize(c_List_Oreplicate(X0,X1,X2),tc_List_Olist(X2)) = X0,
inference(cnf_transformation,[status(thm)],[f1607]) ).
fof(f4666,plain,
! [X0,X1,X2] : X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(thm)],[f1689]) ).
fof(f6201,plain,
! [X0] : c_lessequals(X0,v_x(X0),tc_nat),
inference(cnf_transformation,[status(thm)],[f2788]) ).
fof(f6202,plain,
! [X0] : v_x(X0) = v_nat,
inference(cnf_transformation,[status(thm)],[f2789]) ).
fof(f6212,plain,
! [X0] : c_lessequals(X0,v_nat,tc_nat),
inference(forward_demodulation,[status(thm)],[f6202,f6201]) ).
fof(f12261,plain,
! [X0,X1] : c_List_Odrop(v_nat,X0,X1) = c_List_Olist_ONil,
inference(resolution,[status(thm)],[f4532,f6212]) ).
fof(f12282,plain,
! [X0,X1,X2] : c_List_Oreplicate(c_minus(X0,v_nat,tc_nat),X1,X2) = c_List_Olist_ONil,
inference(paramodulation,[status(thm)],[f4533,f12261]) ).
fof(f12289,plain,
! [X0,X1,X2] : c_List_Odrop(v_nat,c_append(X0,X1,X2),X2) = c_append(c_List_Olist_ONil,c_List_Odrop(c_minus(v_nat,c_Nat_Osize(X0,tc_List_Olist(X2)),tc_nat),X1,X2),X2),
inference(paramodulation,[status(thm)],[f12261,f4529]) ).
fof(f12293,plain,
! [X0,X1,X2] : c_List_Olist_ONil = c_append(c_List_Olist_ONil,c_List_Odrop(c_minus(v_nat,c_Nat_Osize(X0,tc_List_Olist(X1)),tc_nat),X2,X1),X1),
inference(forward_demodulation,[status(thm)],[f12261,f12289]) ).
fof(f12294,plain,
! [X0,X1,X2] : c_List_Olist_ONil = c_List_Odrop(c_minus(v_nat,c_Nat_Osize(X0,tc_List_Olist(X1)),tc_nat),X2,X1),
inference(forward_demodulation,[status(thm)],[f4472,f12293]) ).
fof(f12387,plain,
! [X0,X1,X2] : c_append(c_List_Otake(c_minus(v_nat,c_Nat_Osize(X0,tc_List_Olist(X1)),tc_nat),X2,X1),c_List_Olist_ONil,X1) = X2,
inference(paramodulation,[status(thm)],[f12294,f4476]) ).
fof(f12393,plain,
! [X0,X1,X2] : c_List_Otake(c_minus(v_nat,c_Nat_Osize(X0,tc_List_Olist(X1)),tc_nat),X2,X1) = X2,
inference(forward_demodulation,[status(thm)],[f4475,f12387]) ).
fof(f12415,plain,
! [X0,X1,X2] :
( c_List_Ohd(c_List_Olist_ONil,X1) = X2
| c_minus(X0,v_nat,tc_nat) = c_0 ),
inference(paramodulation,[status(thm)],[f12282,f4543]) ).
fof(f12419,definition,
! [X0] :
( sQ441_spl
<=> c_minus(X0,v_nat,tc_nat) = c_0 ),
introduced(definition,[new_symbols(definition,[sQ441_spl])],[split_symbol_definition]) ).
fof(f12420,plain,
! [X0] :
( ~ sQ441_spl
| c_minus(X0,v_nat,tc_nat) = c_0 ),
inference(component_clause,[status(thm)],[f12419]) ).
fof(f12422,definition,
! [X1,X2] :
( sQ442_spl
<=> c_List_Ohd(c_List_Olist_ONil,X1) = X2 ),
introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition]) ).
fof(f12423,plain,
! [X0,X1] :
( ~ sQ442_spl
| c_List_Ohd(c_List_Olist_ONil,X0) = X1 ),
inference(component_clause,[status(thm)],[f12422]) ).
fof(f12425,plain,
( sQ442_spl
| sQ441_spl ),
inference(split_clause,[status(thm)],[f12415,f12419,f12422]) ).
fof(f12426,plain,
( ~ sQ442_spl
| $false ),
inference(resolution,[status(thm)],[f12423,f4666]) ).
fof(f12432,plain,
~ sQ442_spl,
inference(contradiction_clause,[status(thm)],[f12426]) ).
fof(f13430,plain,
! [X0,X1,X2] : c_List_Otake(c_minus(v_nat,X0,tc_nat),X1,X2) = X1,
inference(paramodulation,[status(thm)],[f4573,f12393]) ).
fof(f13614,plain,
! [X0,X1] :
( ~ sQ441_spl
| c_List_Otake(c_0,X0,X1) = X0 ),
inference(paramodulation,[status(thm)],[f12420,f13430]) ).
fof(f13636,plain,
! [X0,X1] :
( ~ sQ441_spl
| c_append(X0,c_List_Odrop(c_0,X0,X1),X1) = X0 ),
inference(paramodulation,[status(thm)],[f13614,f4476]) ).
fof(f13637,plain,
! [X0,X1] :
( ~ sQ441_spl
| c_append(X0,X0,X1) = X0 ),
inference(forward_demodulation,[status(thm)],[f4523,f13636]) ).
fof(f13660,plain,
! [X0,X1] :
( ~ sQ441_spl
| c_List_Obutlast(c_List_Olist_OCons(X0,c_List_Olist_ONil,X1),X1) = c_List_Olist_OCons(X0,c_List_Olist_ONil,X1) ),
inference(paramodulation,[status(thm)],[f13637,f4481]) ).
fof(f13688,plain,
! [X0,X1] :
( ~ sQ441_spl
| c_List_Olist_ONil = c_List_Olist_OCons(X0,c_List_Olist_ONil,X1) ),
inference(forward_demodulation,[status(thm)],[f4478,f13660]) ).
fof(f13689,plain,
( ~ sQ441_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13688,f4666]) ).
fof(f13690,plain,
~ sQ441_spl,
inference(contradiction_clause,[status(thm)],[f13689]) ).
fof(f13691,plain,
$false,
inference(sat_refutation,[status(thm)],[f12425,f12432,f13690]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV254-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n006.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 08:36:28 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.28/0.52 % Drodi V4.1.1
% 3.09/0.94 % Refutation found
% 3.09/0.94 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.09/0.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.09/1.01 % Elapsed time: 0.563092 seconds
% 3.09/1.01 % CPU time: 3.478673 seconds
% 3.09/1.01 % Total memory used: 258.506 MB
% 3.09/1.01 % Net memory used: 257.261 MB
%------------------------------------------------------------------------------