%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV592-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:52:52 PM UTC 2026
% Result : Unsatisfiable 0.21s 0.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV592-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.46 % Computer : n026.cluster.edu
% 0.16/0.46 % Model : x86_64 x86_64
% 0.16/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.46 % Memory : 8046.5625MB
% 0.16/0.46 % OS : Linux 6.8.0-71-generic
% 0.16/0.46 % CPULimit : 300
% 0.16/0.46 % WCLimit : 300
% 0.16/0.46 % DateTime : Mon Sep 21 09:15:22 UTC 2026
% 0.16/0.46 % CPUTime :
% 0.21/0.60 % Drodi V4.1.1
% 0.21/0.74 % Refutation found
% 0.21/0.74 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.21/0.74 % SZS output start CNFRefutation for theBenchmark
% 0.21/0.74 fof(f446,axiom,(
% 0.21/0.74 (![V_x]: (c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ))),
% 0.21/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/0.74 fof(f823,axiom,(
% 0.21/0.74 (![V_y,V_z]: (V_y = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_y,V_z,tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) ))),
% 0.21/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/0.74 fof(f824,axiom,(
% 0.21/0.74 (![V_x,V_z]: (V_x = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_x,V_z,tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) ))),
% 0.21/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/0.74 fof(f846,axiom,(
% 0.21/0.74 (![V_r,V_s]: (c_HOL_Ominus__class_Ominus(V_r,V_s,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(V_r,c_HOL_Ouminus__class_Ouminus(V_s,tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 0.21/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/0.74 fof(f847,axiom,(
% 0.21/0.74 c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 0.21/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/0.74 fof(f849,axiom,(
% 0.21/0.74 (![V_x]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal) ))),
% 0.21/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/0.74 fof(f851,axiom,(
% 0.21/0.74 (![V_x]: (c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal) ))),
% 0.21/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/0.74 fof(f862,negated_conjecture,(
% 0.21/0.74 c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)) != c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(v_x),tc_RealDef_Oreal) ),
% 0.21/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/0.74 fof(f1650,plain,(
% 0.21/0.74 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 0.21/0.74 inference(cnf_transformation,[status(thm)],[f446])).
% 0.21/0.74 fof(f2252,plain,(
% 0.21/0.74 ![X0,X1]: (X0=c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal))),
% 0.21/0.74 inference(cnf_transformation,[status(thm)],[f823])).
% 0.21/0.74 fof(f2253,plain,(
% 0.21/0.74 ![X0,X1]: (X0=c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal))),
% 0.21/0.74 inference(cnf_transformation,[status(thm)],[f824])).
% 0.21/0.74 fof(f2292,plain,(
% 0.21/0.74 ![X0,X1]: (c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.21/0.74 inference(cnf_transformation,[status(thm)],[f846])).
% 0.21/0.74 fof(f2293,plain,(
% 0.21/0.74 c_Transcendental_Osin(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.21/0.74 inference(cnf_transformation,[status(thm)],[f847])).
% 0.21/0.74 fof(f2295,plain,(
% 0.21/0.74 ![X0]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Opi,tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal))),
% 0.21/0.74 inference(cnf_transformation,[status(thm)],[f849])).
% 0.21/0.74 fof(f2298,plain,(
% 0.21/0.74 ![X0]: (c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal))),
% 0.21/0.74 inference(cnf_transformation,[status(thm)],[f851])).
% 0.21/0.74 fof(f2319,plain,(
% 0.21/0.74 ~c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(v_x),tc_RealDef_Oreal)),
% 0.21/0.74 inference(cnf_transformation,[status(thm)],[f862])).
% 0.21/0.74 fof(f2454,plain,(
% 0.21/0.74 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_Transcendental_Osin(c_Transcendental_Opi))),
% 0.21/0.74 inference(forward_demodulation,[status(thm)],[f2293,f1650])).
% 0.21/0.74 fof(f2456,plain,(
% 0.21/0.74 ![X0]: (X0=c_HOL_Ominus__class_Ominus(c_Transcendental_Osin(c_Transcendental_Opi),c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.21/0.75 inference(paramodulation,[status(thm)],[f2454,f2253])).
% 0.21/0.75 fof(f2457,plain,(
% 0.21/0.75 ~c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal))),
% 0.21/0.75 inference(backward_demodulation,[status(thm)],[f2298,f2319])).
% 0.21/0.75 fof(f2588,plain,(
% 0.21/0.75 ![X0]: (c_HOL_Ominus__class_Ominus(X0,X0,tc_RealDef_Oreal)=c_Transcendental_Osin(c_Transcendental_Opi))),
% 0.21/0.75 inference(backward_demodulation,[status(thm)],[f2292,f2454])).
% 0.21/0.75 fof(f2597,plain,(
% 0.21/0.75 ![X0]: (X0=c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal))),
% 0.21/0.75 inference(paramodulation,[status(thm)],[f2588,f2252])).
% 0.21/0.75 fof(f2600,plain,(
% 0.21/0.75 ![X0]: (c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)=c_HOL_Ominus__class_Ominus(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal))),
% 0.21/0.75 inference(paramodulation,[status(thm)],[f2292,f2597])).
% 0.21/0.75 fof(f2665,plain,(
% 0.21/0.75 ![X0]: (X0=c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.21/0.75 inference(backward_demodulation,[status(thm)],[f2600,f2456])).
% 0.21/0.75 fof(f2771,plain,(
% 0.21/0.75 ![X0]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Opi,tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)))),
% 0.21/0.75 inference(forward_demodulation,[status(thm)],[f2298,f2295])).
% 0.21/0.75 fof(f2775,plain,(
% 0.21/0.75 ![X0]: (c_Transcendental_Osin(X0)=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)))),
% 0.21/0.75 inference(paramodulation,[status(thm)],[f2252,f2771])).
% 0.21/0.75 fof(f2869,plain,(
% 0.21/0.75 ![X0]: (c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal))),
% 0.21/0.75 inference(paramodulation,[status(thm)],[f2775,f2298])).
% 0.21/0.75 fof(f2874,plain,(
% 0.21/0.75 ![X0]: (c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal))),
% 0.21/0.75 inference(forward_demodulation,[status(thm)],[f2665,f2869])).
% 0.21/0.75 fof(f2875,plain,(
% 0.21/0.75 ![X0]: (c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)))),
% 0.21/0.75 inference(forward_demodulation,[status(thm)],[f2298,f2874])).
% 0.21/0.75 fof(f2951,plain,(
% 0.21/0.75 ~c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal))),
% 0.21/0.75 inference(backward_demodulation,[status(thm)],[f2875,f2457])).
% 0.21/0.75 fof(f2960,plain,(
% 0.21/0.75 $false),
% 0.21/0.75 inference(trivial_equality_resolution,[status(thm)],[f2951])).
% 0.21/0.75 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/0.80 % Elapsed time: 0.323101 seconds
% 0.21/0.80 % CPU time: 1.069711 seconds
% 0.21/0.80 % Total memory used: 156.297 MB
% 0.21/0.80 % Net memory used: 155.462 MB
%------------------------------------------------------------------------------