%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL777-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 01:11:06 PM UTC 2026
% Result : Unsatisfiable 0.22s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL777-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.47 % Computer : n003.cluster.edu
% 0.16/0.47 % Model : x86_64 x86_64
% 0.16/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.47 % Memory : 8046.5625MB
% 0.16/0.47 % OS : Linux 6.8.0-71-generic
% 0.16/0.47 % CPULimit : 300
% 0.16/0.47 % WCLimit : 300
% 0.16/0.47 % DateTime : Mon Sep 21 01:05:15 UTC 2026
% 0.16/0.48 % CPUTime :
% 0.22/0.54 % Drodi V4.1.1
% 0.22/0.58 % Refutation found
% 0.22/0.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.22/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.22/0.58 fof(f1,axiom,(
% 0.22/0.58 (![V_xs,V_x,V_ys,T_a,V_y]: (c_List_Olist__update(c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,V_ys,T_a),T_a),c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)),V_y,T_a) = c_List_Oappend(V_xs,c_List_Olist_OCons(V_y,V_ys,T_a),T_a) ))),
% 0.22/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.58 fof(f3,axiom,(
% 0.22/0.58 (![T_a,V_i,V_v]: (c_List_Olist__update(c_List_Olist_ONil(T_a),V_i,V_v,T_a) = c_List_Olist_ONil(T_a) ))),
% 0.22/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.58 fof(f50,axiom,(
% 0.22/0.58 (![V_nat_H]: (c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H) ))),
% 0.22/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.58 fof(f306,axiom,(
% 0.22/0.58 (![V_x,V_s,V_t]: (( c_List_Oappend(V_x,c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB) = c_List_Olist_ONil(tc_Lambda_OdB)| hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_x,tc_Lambda_OdB,tc_Lambda_OdB)),V_s) = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Oappend(V_x,c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ) ))),
% 0.22/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.58 fof(f309,axiom,(
% 0.22/0.58 (![V_xs,V_x,T_a,V_ys,V_y]: (( c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) != c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a)| V_x = V_y ) ))),
% 0.22/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.58 fof(f362,negated_conjecture,(
% 0.22/0.58 hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))) ),
% 0.22/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.58 fof(f365,negated_conjecture,(
% 0.22/0.58 ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Oappend(v_ss,c_List_Olist_OCons(c_Lambda_OdB_OVar(v_i),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))) ),
% 0.22/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.58 fof(f389,plain,(
% 0.22/0.58 ![X0,X1,X2,X3,X4]: (c_List_Olist__update(c_List_Oappend(X0,c_List_Olist_OCons(X1,X2,X3),X3),c_Nat_Osize__class_Osize(X0,tc_List_Olist(X3)),X4,X3)=c_List_Oappend(X0,c_List_Olist_OCons(X4,X2,X3),X3))),
% 0.22/0.58 inference(cnf_transformation,[status(thm)],[f1])).
% 0.22/0.58 fof(f392,plain,(
% 0.22/0.58 ![X0,X1,X2]: (c_List_Olist__update(c_List_Olist_ONil(X0),X1,X2,X0)=c_List_Olist_ONil(X0))),
% 0.22/0.58 inference(cnf_transformation,[status(thm)],[f3])).
% 0.22/0.58 fof(f452,plain,(
% 0.22/0.58 ![X0]: (~c_HOL_Ozero__class_Ozero(tc_nat)=c_Suc(X0))),
% 0.22/0.58 inference(cnf_transformation,[status(thm)],[f50])).
% 0.22/0.58 fof(f804,plain,(
% 0.22/0.58 ![V_x,V_s]: (c_List_Oappend(V_x,c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)=c_List_Olist_ONil(tc_Lambda_OdB)|(![V_t]: hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_x,tc_Lambda_OdB,tc_Lambda_OdB)),V_s)=c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Oappend(V_x,c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)))),
% 0.22/0.58 inference(miniscoping,[status(thm)],[f306])).
% 0.22/0.58 fof(f805,plain,(
% 0.22/0.58 ![X0,X1,X2]: (c_List_Oappend(X0,c_List_Olist_OCons(X1,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)=c_List_Olist_ONil(tc_Lambda_OdB)|hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,X2,X0,tc_Lambda_OdB,tc_Lambda_OdB)),X1)=c_List_Ofoldl(c_Lambda_OdB_OApp,X2,c_List_Oappend(X0,c_List_Olist_OCons(X1,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
% 0.22/0.58 inference(cnf_transformation,[status(thm)],[f804])).
% 0.22/0.58 fof(f808,plain,(
% 0.22/0.58 ![V_x,V_y]: ((![V_xs,T_a,V_ys]: ~c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a)=c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a))|V_x=V_y)),
% 0.22/0.58 inference(miniscoping,[status(thm)],[f309])).
% 0.22/0.58 fof(f809,plain,(
% 0.22/0.59 ![X0,X1,X2,X3,X4]: (~c_List_Oappend(X0,c_List_Olist_OCons(X1,c_List_Olist_ONil(X2),X2),X2)=c_List_Oappend(X3,c_List_Olist_OCons(X4,c_List_Olist_ONil(X2),X2),X2)|X1=X4)),
% 0.22/0.59 inference(cnf_transformation,[status(thm)],[f808])).
% 0.22/0.59 fof(f883,plain,(
% 0.22/0.59 hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i))))),
% 0.22/0.59 inference(cnf_transformation,[status(thm)],[f362])).
% 0.22/0.59 fof(f886,plain,(
% 0.22/0.59 ~hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Oappend(v_ss,c_List_Olist_OCons(c_Lambda_OdB_OVar(v_i),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)))),
% 0.22/0.59 inference(cnf_transformation,[status(thm)],[f365])).
% 0.22/0.59 fof(f1113,plain,(
% 0.22/0.59 ~hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i))))|c_List_Oappend(v_ss,c_List_Olist_OCons(c_Lambda_OdB_OVar(v_i),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)=c_List_Olist_ONil(tc_Lambda_OdB)),
% 0.22/0.59 inference(paramodulation,[status(thm)],[f805,f886])).
% 0.22/0.59 fof(f1119,definition,(
% 0.22/0.59 sQ4_spl <=> (hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))))),
% 0.22/0.59 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.22/0.59 fof(f1121,plain,(
% 0.22/0.59 ~hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i))))|sQ4_spl),
% 0.22/0.59 inference(component_clause,[status(thm)],[f1119])).
% 0.22/0.59 fof(f1122,definition,(
% 0.22/0.59 sQ5_spl <=> (c_List_Oappend(v_ss,c_List_Olist_OCons(c_Lambda_OdB_OVar(v_i),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)=c_List_Olist_ONil(tc_Lambda_OdB))),
% 0.22/0.59 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.22/0.59 fof(f1123,plain,(
% 0.22/0.59 c_List_Oappend(v_ss,c_List_Olist_OCons(c_Lambda_OdB_OVar(v_i),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)=c_List_Olist_ONil(tc_Lambda_OdB)|~sQ5_spl),
% 0.22/0.59 inference(component_clause,[status(thm)],[f1122])).
% 0.22/0.59 fof(f1125,plain,(
% 0.22/0.59 ~sQ4_spl|sQ5_spl),
% 0.22/0.59 inference(split_clause,[status(thm)],[f1113,f1119,f1122])).
% 0.22/0.59 fof(f1126,plain,(
% 0.22/0.59 $false|sQ4_spl),
% 0.22/0.59 inference(forward_subsumption_resolution,[status(thm)],[f1121,f883])).
% 0.22/0.59 fof(f1127,plain,(
% 0.22/0.59 sQ4_spl),
% 0.22/0.59 inference(contradiction_clause,[status(thm)],[f1126])).
% 0.22/0.59 fof(f1140,plain,(
% 0.22/0.59 ![X0]: (c_List_Olist__update(c_List_Olist_ONil(tc_Lambda_OdB),c_Nat_Osize__class_Osize(v_ss,tc_List_Olist(tc_Lambda_OdB)),X0,tc_Lambda_OdB)=c_List_Oappend(v_ss,c_List_Olist_OCons(X0,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)|~sQ5_spl)),
% 0.22/0.59 inference(paramodulation,[status(thm)],[f1123,f389])).
% 0.22/0.59 fof(f1149,plain,(
% 0.22/0.59 ![X0]: (c_List_Olist_ONil(tc_Lambda_OdB)=c_List_Oappend(v_ss,c_List_Olist_OCons(X0,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)|~sQ5_spl)),
% 0.22/0.59 inference(forward_demodulation,[status(thm)],[f392,f1140])).
% 0.22/0.59 fof(f1190,plain,(
% 0.22/0.59 ![X0,X1,X2]: (~c_List_Oappend(X0,c_List_Olist_OCons(X1,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB)=c_List_Olist_ONil(tc_Lambda_OdB)|X1=X2|~sQ5_spl)),
% 0.22/0.59 inference(paramodulation,[status(thm)],[f1149,f809])).
% 0.22/0.59 fof(f1232,plain,(
% 0.22/0.59 ![X0,X1]: (X0=X1|~sQ5_spl)),
% 0.22/0.59 inference(resolution,[status(thm)],[f1190,f1149])).
% 0.22/0.59 fof(f1257,plain,(
% 0.22/0.59 $false|~sQ5_spl),
% 0.22/0.59 inference(backward_subsumption_resolution,[status(thm)],[f452,f1232])).
% 0.22/0.59 fof(f1264,plain,(
% 0.22/0.59 ~sQ5_spl),
% 0.22/0.59 inference(contradiction_clause,[status(thm)],[f1257])).
% 0.22/0.59 fof(f1265,plain,(
% 0.22/0.59 $false),
% 0.22/0.59 inference(sat_refutation,[status(thm)],[f1125,f1127,f1264])).
% 0.22/0.59 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.63 % Elapsed time: 0.133530 seconds
% 0.22/0.63 % CPU time: 0.255302 seconds
% 0.22/0.63 % Total memory used: 46.024 MB
% 0.22/0.63 % Net memory used: 45.809 MB
%------------------------------------------------------------------------------