%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG439-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 : 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 : Thu Sep 24 11:50:11 AM UTC 2026
% Result : Unsatisfiable 0.10s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG439-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.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 13:21:25 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.43 % Drodi V4.1.1
% 0.10/0.46 % Refutation found
% 0.10/0.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.46 fof(f715,axiom,(
% 0.10/0.46 (![V_x]: (c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),V_x,tc_Complex_Ocomplex) ))),
% 0.10/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.46 fof(f717,axiom,(
% 0.10/0.46 (![V_p,V_x]: (( c_Polynomial_Opoly(V_p,V_x,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)| c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),V_p,tc_Complex_Ocomplex),V_x,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ) ))),
% 0.10/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.46 fof(f733,axiom,(
% 0.10/0.46 (![V_c,V_x]: (c_Polynomial_Opoly(c_Polynomial_OpCons(V_c,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),V_x,tc_Complex_Ocomplex) = V_c ))),
% 0.10/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.46 fof(f735,negated_conjecture,(
% 0.10/0.46 ( v_c != v_y| c_Polynomial_Opoly(c_Polynomial_OpCons(v_c,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) != v_y ) ),
% 0.10/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.46 fof(f736,negated_conjecture,(
% 0.10/0.46 ( c_Polynomial_Opoly(c_Polynomial_OpCons(v_c,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) = v_y| v_c = v_y ) ),
% 0.10/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.46 fof(f2133,plain,(
% 0.10/0.46 ![X0]: (c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex))),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f715])).
% 0.10/0.46 fof(f2135,plain,(
% 0.10/0.46 ![X0,X1]: (~c_Polynomial_Opoly(X0,X1,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f717])).
% 0.10/0.46 fof(f2160,plain,(
% 0.10/0.46 ![X0,X1]: (c_Polynomial_Opoly(c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=X0)),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f733])).
% 0.10/0.46 fof(f2162,plain,(
% 0.10/0.46 ~v_c=v_y|~c_Polynomial_Opoly(c_Polynomial_OpCons(v_c,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex)=v_y),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f735])).
% 0.10/0.46 fof(f2163,plain,(
% 0.10/0.46 c_Polynomial_Opoly(c_Polynomial_OpCons(v_c,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex)=v_y|v_c=v_y),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f736])).
% 0.10/0.46 fof(f2385,definition,(
% 0.10/0.46 sQ11_spl <=> (v_c=v_y)),
% 0.10/0.46 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.10/0.46 fof(f2386,plain,(
% 0.10/0.46 v_c=v_y|~sQ11_spl),
% 0.10/0.46 inference(component_clause,[status(thm)],[f2385])).
% 0.10/0.46 fof(f2387,plain,(
% 0.10/0.46 ~v_c=v_y|sQ11_spl),
% 0.10/0.46 inference(component_clause,[status(thm)],[f2385])).
% 0.10/0.46 fof(f2388,definition,(
% 0.10/0.46 sQ12_spl <=> (c_Polynomial_Opoly(c_Polynomial_OpCons(v_c,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex)=v_y)),
% 0.10/0.46 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.10/0.46 fof(f2389,plain,(
% 0.10/0.46 c_Polynomial_Opoly(c_Polynomial_OpCons(v_c,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex)=v_y|~sQ12_spl),
% 0.10/0.46 inference(component_clause,[status(thm)],[f2388])).
% 0.10/0.46 fof(f2390,plain,(
% 0.10/0.46 ~c_Polynomial_Opoly(c_Polynomial_OpCons(v_c,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex)=v_y|sQ12_spl),
% 0.10/0.46 inference(component_clause,[status(thm)],[f2388])).
% 0.10/0.46 fof(f2391,plain,(
% 0.10/0.46 ~sQ11_spl|~sQ12_spl),
% 0.10/0.46 inference(split_clause,[status(thm)],[f2162,f2385,f2388])).
% 0.10/0.47 fof(f2392,plain,(
% 0.10/0.47 sQ12_spl|sQ11_spl),
% 0.10/0.47 inference(split_clause,[status(thm)],[f2163,f2388,f2385])).
% 0.10/0.47 fof(f2395,plain,(
% 0.10/0.47 ![X0]: (~c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 0.10/0.47 inference(paramodulation,[status(thm)],[f2133,f2135])).
% 0.10/0.47 fof(f2397,definition,(
% 0.10/0.47 sQ13_spl <=> (c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 0.10/0.47 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.10/0.47 fof(f2399,plain,(
% 0.10/0.47 ~c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|sQ13_spl),
% 0.10/0.47 inference(component_clause,[status(thm)],[f2397])).
% 0.10/0.47 fof(f2400,definition,(
% 0.10/0.47 ![X0]: (sQ14_spl <=> (c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)))),
% 0.10/0.47 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.10/0.47 fof(f2403,plain,(
% 0.10/0.47 ~sQ13_spl|sQ14_spl),
% 0.10/0.47 inference(split_clause,[status(thm)],[f2395,f2397,f2400])).
% 0.10/0.47 fof(f2411,plain,(
% 0.10/0.47 $false|sQ13_spl),
% 0.10/0.47 inference(trivial_equality_resolution,[status(thm)],[f2399])).
% 0.10/0.47 fof(f2412,plain,(
% 0.10/0.47 sQ13_spl),
% 0.10/0.47 inference(contradiction_clause,[status(thm)],[f2411])).
% 0.10/0.47 fof(f2416,plain,(
% 0.10/0.47 ~v_c=v_y|sQ12_spl),
% 0.10/0.47 inference(forward_demodulation,[status(thm)],[f2160,f2390])).
% 0.10/0.47 fof(f2417,plain,(
% 0.10/0.47 ~v_y=v_y|~sQ11_spl|sQ12_spl),
% 0.10/0.47 inference(forward_demodulation,[status(thm)],[f2386,f2416])).
% 0.10/0.47 fof(f2418,plain,(
% 0.10/0.47 $false|~sQ11_spl|sQ12_spl),
% 0.10/0.47 inference(trivial_equality_resolution,[status(thm)],[f2417])).
% 0.10/0.47 fof(f2419,plain,(
% 0.10/0.47 ~sQ11_spl|sQ12_spl),
% 0.10/0.47 inference(contradiction_clause,[status(thm)],[f2418])).
% 0.10/0.47 fof(f2420,plain,(
% 0.10/0.47 v_c=v_y|~sQ12_spl),
% 0.10/0.47 inference(forward_demodulation,[status(thm)],[f2160,f2389])).
% 0.10/0.47 fof(f2421,plain,(
% 0.10/0.47 $false|sQ11_spl|~sQ12_spl),
% 0.10/0.47 inference(forward_subsumption_resolution,[status(thm)],[f2420,f2387])).
% 0.10/0.47 fof(f2422,plain,(
% 0.10/0.47 sQ11_spl|~sQ12_spl),
% 0.10/0.47 inference(contradiction_clause,[status(thm)],[f2421])).
% 0.10/0.47 fof(f2423,plain,(
% 0.10/0.47 $false),
% 0.10/0.47 inference(sat_refutation,[status(thm)],[f2391,f2392,f2403,f2412,f2419,f2422])).
% 0.10/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.51 % Elapsed time: 0.134320 seconds
% 0.10/0.51 % CPU time: 0.216665 seconds
% 0.10/0.51 % Total memory used: 59.897 MB
% 0.10/0.51 % Net memory used: 59.641 MB
%------------------------------------------------------------------------------