%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ITP019+4 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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 12:52:01 PM UTC 2026
% Result : Theorem 21.99s 11.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP019+4 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.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 : Sun Sep 20 21:57:17 UTC 2026
% 0.09/0.37 % CPUTime :
% 8.95/9.23 % Drodi V4.1.1
% 21.99/11.00 % Refutation found
% 21.99/11.00 % SZS status Theorem for theBenchmark: Theorem is valid
% 21.99/11.00 % SZS output start CNFRefutation for theBenchmark
% 21.99/11.00 fof(f23394,axiom,(
% 21.99/11.00 s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ),
% 21.99/11.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.99/11.00 fof(f23396,axiom,(
% 21.99/11.00 (! [V0z_2E0] : s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0))))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0) )),
% 21.99/11.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.99/11.00 fof(f23399,conjecture,(
% 21.99/11.00 (! [V0z_2E0] :( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))=> s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0))) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ) )),
% 21.99/11.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.99/11.00 fof(f23400,negated_conjecture,(
% 21.99/11.00 ~((! [V0z_2E0] :( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))=> s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0))) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ) ))),
% 21.99/11.00 inference(negated_conjecture,[status(cth)],[f23399])).
% 21.99/11.00 fof(f88404,plain,(
% 21.99/11.00 s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))))=s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))),
% 21.99/11.00 inference(cnf_transformation,[status(thm)],[f23394])).
% 21.99/11.00 fof(f88406,plain,(
% 21.99/11.00 ![X0]: (s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X0)))))=s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X0))),
% 21.99/11.00 inference(cnf_transformation,[status(thm)],[f23396])).
% 21.99/11.00 fof(f88412,plain,(
% 21.99/11.00 (?[V0z_2E0]: (~s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0)=s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))&s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0)))=s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))))),
% 21.99/11.00 inference(pre_NNF_transformation,[status(thm)],[f23400])).
% 21.99/11.00 fof(f88413,plain,(
% 21.99/11.00 (~s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),sK24757_skl)=s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))&s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),sK24757_skl)))=s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))))),
% 20.52/11.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK24757_skl]),skolemize(V0z_2E0,sK24757_skl)],[f88412])).
% 20.52/11.74 fof(f88414,plain,(
% 20.52/11.74 ~s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),sK24757_skl)=s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))),
% 20.52/11.74 inference(cnf_transformation,[status(thm)],[f88413])).
% 20.52/11.74 fof(f88415,plain,(
% 20.52/11.74 s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),sK24757_skl)))=s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))),
% 20.52/11.74 inference(cnf_transformation,[status(thm)],[f88413])).
% 20.52/11.74 fof(f99751,plain,(
% 20.52/11.74 s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))))=s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),sK24757_skl)),
% 20.52/11.74 inference(paramodulation,[status(thm)],[f88415,f88406])).
% 20.52/11.74 fof(f99782,plain,(
% 20.52/11.74 s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),sK24757_skl)=s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))),
% 20.52/11.74 inference(forward_demodulation,[status(thm)],[f99751,f88404])).
% 20.52/11.74 fof(f99783,plain,(
% 20.52/11.74 $false),
% 20.52/11.74 inference(forward_subsumption_resolution,[status(thm)],[f99782,f88414])).
% 20.52/11.74 % SZS output end CNFRefutation for theBenchmark.p
% 9.54/11.94 % Elapsed time: 11.439630 seconds
% 9.54/11.94 % CPU time: 23.416235 seconds
% 9.54/11.94 % Total memory used: 7.051 GB
% 9.54/11.94 % Net memory used: 7.032 GB
%------------------------------------------------------------------------------