%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV598-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 : n010.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:53 PM UTC 2026
% Result : Unsatisfiable 5.64s 6.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV598-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n010.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Mon Sep 21 09:13:17 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.14/5.47 % Drodi V4.1.1
% 5.64/6.31 % Refutation found
% 5.64/6.31 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.64/6.31 % SZS output start CNFRefutation for theBenchmark
% 5.64/6.31 fof(f111,axiom,(
% 5.64/6.31 (![V_x,V_y]: (( c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)| V_x = V_y| ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal) ) ))),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f114,axiom,(
% 5.64/6.31 (![T_a,V_x,V_y]: (( ~ class_Orderings_Olinorder(T_a)| V_x = V_y| ~ c_lessequals(V_x,V_y,T_a)| c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ))),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f394,axiom,(
% 5.64/6.31 (![V_z,V_w]: (c_HOL_Otimes__class_Otimes(V_z,V_w,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_w,V_z,tc_RealDef_Oreal) ))),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1113,axiom,(
% 5.64/6.31 (![V_w,V_z]: (( c_lessequals(V_w,V_z,tc_RealDef_Oreal)| c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1206,axiom,(
% 5.64/6.31 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x,tc_RealDef_Oreal) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1216,axiom,(
% 5.64/6.31 c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1218,axiom,(
% 5.64/6.31 ( c_Transcendental_Osin(v_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,v_x,tc_RealDef_Oreal) ) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1219,axiom,(
% 5.64/6.31 ( c_Transcendental_Ocos(v_x) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal)| v_x != c_Transcendental_Opi ) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1220,axiom,(
% 5.64/6.31 ( c_Transcendental_Osin(v_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x,tc_RealDef_Oreal) ) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1221,negated_conjecture,(
% 5.64/6.31 c_Transcendental_Osin(v_x) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1222,negated_conjecture,(
% 5.64/6.31 c_Transcendental_Ocos(v_x) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1224,axiom,(
% 5.64/6.31 class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1284,axiom,(
% 5.64/6.31 class_Ring__and__Field_Ofield(tc_RealDef_Oreal) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1288,axiom,(
% 5.64/6.31 class_Orderings_Opreorder(tc_RealDef_Oreal) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1289,axiom,(
% 5.64/6.31 class_Orderings_Olinorder(tc_RealDef_Oreal) ),
% 5.64/6.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.64/6.31 fof(f1522,plain,(
% 5.64/6.31 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|X0=X1|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f111])).
% 5.64/6.31 fof(f1526,plain,(
% 5.64/6.31 ![X0,X1,X2]: (~class_Orderings_Olinorder(X0)|X1=X2|~c_lessequals(X1,X2,X0)|c_HOL_Oord__class_Oless(X1,X2,X0))),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f114])).
% 5.64/6.31 fof(f1982,plain,(
% 5.64/6.31 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal))),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f394])).
% 5.64/6.31 fof(f3117,plain,(
% 5.64/6.31 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1113])).
% 5.64/6.31 fof(f3223,plain,(
% 5.64/6.31 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x,tc_RealDef_Oreal)),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1206])).
% 5.64/6.31 fof(f3233,plain,(
% 5.64/6.31 c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1216])).
% 5.64/6.31 fof(f3235,plain,(
% 5.64/6.31 ~c_Transcendental_Osin(v_x)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_Transcendental_Opi,v_x,tc_RealDef_Oreal)),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1218])).
% 5.64/6.31 fof(f3236,plain,(
% 5.64/6.31 ~c_Transcendental_Ocos(v_x)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)|~v_x=c_Transcendental_Opi),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1219])).
% 5.64/6.31 fof(f3237,plain,(
% 5.64/6.31 ~c_Transcendental_Osin(v_x)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x,tc_RealDef_Oreal)),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1220])).
% 5.64/6.31 fof(f3238,plain,(
% 5.64/6.31 c_Transcendental_Osin(v_x)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1221])).
% 5.64/6.31 fof(f3239,plain,(
% 5.64/6.31 c_Transcendental_Ocos(v_x)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1222])).
% 5.64/6.31 fof(f3241,plain,(
% 5.64/6.31 class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal)),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1224])).
% 5.64/6.31 fof(f3301,plain,(
% 5.64/6.31 class_Ring__and__Field_Ofield(tc_RealDef_Oreal)),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1284])).
% 5.64/6.31 fof(f3305,plain,(
% 5.64/6.31 class_Orderings_Opreorder(tc_RealDef_Oreal)),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1288])).
% 5.64/6.31 fof(f3306,plain,(
% 5.64/6.31 class_Orderings_Olinorder(tc_RealDef_Oreal)),
% 5.64/6.31 inference(cnf_transformation,[status(thm)],[f1289])).
% 5.64/6.31 fof(f3366,definition,(
% 5.64/6.31 sQ5_spl <=> (c_Transcendental_Osin(v_x)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 5.64/6.31 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 5.64/6.31 fof(f3368,plain,(
% 5.64/6.31 ~c_Transcendental_Osin(v_x)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|sQ5_spl),
% 5.64/6.31 inference(component_clause,[status(thm)],[f3366])).
% 5.64/6.31 fof(f3369,definition,(
% 5.64/6.31 sQ6_spl <=> (c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 5.64/6.31 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 5.64/6.31 fof(f3371,plain,(
% 5.64/6.31 ~c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ6_spl),
% 5.64/6.31 inference(component_clause,[status(thm)],[f3369])).
% 5.64/6.31 fof(f3372,definition,(
% 5.64/6.31 sQ7_spl <=> (c_HOL_Oord__class_Oless(c_Transcendental_Opi,v_x,tc_RealDef_Oreal))),
% 5.64/6.31 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 5.64/6.31 fof(f3375,plain,(
% 5.64/6.31 ~sQ5_spl|~sQ6_spl|~sQ7_spl),
% 5.64/6.31 inference(split_clause,[status(thm)],[f3235,f3366,f3369,f3372])).
% 5.64/6.31 fof(f3376,definition,(
% 5.64/6.31 sQ8_spl <=> (c_Transcendental_Ocos(v_x)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal))),
% 5.64/6.31 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 5.64/6.31 fof(f3378,plain,(
% 5.64/6.31 ~c_Transcendental_Ocos(v_x)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)|sQ8_spl),
% 5.64/6.31 inference(component_clause,[status(thm)],[f3376])).
% 5.64/6.31 fof(f3379,definition,(
% 5.64/6.31 sQ9_spl <=> (v_x=c_Transcendental_Opi)),
% 5.64/6.31 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 5.64/6.31 fof(f3382,plain,(
% 5.64/6.31 ~sQ8_spl|~sQ9_spl),
% 5.64/6.31 inference(split_clause,[status(thm)],[f3236,f3376,f3379])).
% 5.64/6.31 fof(f3383,definition,(
% 5.64/6.31 sQ10_spl <=> (c_HOL_Oord__class_Oless(v_x,c_Transcendental_Opi,tc_RealDef_Oreal))),
% 5.64/6.31 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 5.64/6.31 fof(f3385,plain,(
% 5.64/6.31 ~c_HOL_Oord__class_Oless(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)|sQ10_spl),
% 5.64/6.31 inference(component_clause,[status(thm)],[f3383])).
% 5.64/6.31 fof(f3386,definition,(
% 5.64/6.31 sQ11_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x,tc_RealDef_Oreal))),
% 5.64/6.31 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 5.64/6.31 fof(f3388,plain,(
% 5.64/6.31 ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x,tc_RealDef_Oreal)|sQ11_spl),
% 5.64/6.31 inference(component_clause,[status(thm)],[f3386])).
% 5.64/6.31 fof(f3389,plain,(
% 5.64/6.31 ~sQ5_spl|~sQ10_spl|~sQ11_spl),
% 5.64/6.31 inference(split_clause,[status(thm)],[f3237,f3366,f3383,f3386])).
% 5.64/6.31 fof(f3414,plain,(
% 5.64/6.31 c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 5.64/6.31 inference(forward_demodulation,[status(thm)],[f1982,f3233])).
% 5.64/6.31 fof(f3415,plain,(
% 5.64/6.31 ~c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|sQ5_spl),
% 5.64/6.31 inference(forward_demodulation,[status(thm)],[f3238,f3368])).
% 5.64/6.31 fof(f3416,plain,(
% 5.64/6.31 $false|sQ5_spl),
% 5.64/6.31 inference(trivial_equality_resolution,[status(thm)],[f3415])).
% 5.64/6.31 fof(f3417,plain,(
% 5.64/6.31 sQ5_spl),
% 5.64/6.31 inference(contradiction_clause,[status(thm)],[f3416])).
% 5.64/6.31 fof(f3418,plain,(
% 5.64/6.31 ~c_HOL_Oone__class_Oone(tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)|sQ8_spl),
% 5.64/6.31 inference(forward_demodulation,[status(thm)],[f3239,f3378])).
% 5.64/6.31 fof(f3419,plain,(
% 5.64/6.31 $false|sQ8_spl),
% 5.64/6.31 inference(trivial_equality_resolution,[status(thm)],[f3418])).
% 5.64/6.31 fof(f3420,plain,(
% 5.64/6.31 sQ8_spl),
% 5.64/6.31 inference(contradiction_clause,[status(thm)],[f3419])).
% 5.64/6.31 fof(f3426,plain,(
% 5.64/6.31 ~c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ6_spl),
% 5.64/6.31 inference(forward_demodulation,[status(thm)],[f1982,f3371])).
% 5.64/6.31 fof(f3427,plain,(
% 5.64/6.31 $false|sQ6_spl),
% 5.64/6.31 inference(forward_subsumption_resolution,[status(thm)],[f3426,f3414])).
% 5.64/6.31 fof(f3428,plain,(
% 5.64/6.31 sQ6_spl),
% 5.64/6.31 inference(contradiction_clause,[status(thm)],[f3427])).
% 5.64/6.31 fof(f3522,plain,(
% 5.64/6.31 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|X0=X1|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 5.64/6.31 inference(resolution,[status(thm)],[f1522,f3117])).
% 5.64/6.31 fof(f3548,definition,(
% 5.64/6.31 sQ24_spl <=> (class_Orderings_Olinorder(tc_RealDef_Oreal))),
% 5.64/6.31 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 5.64/6.31 fof(f3550,plain,(
% 5.64/6.31 ~class_Orderings_Olinorder(tc_RealDef_Oreal)|sQ24_spl),
% 5.64/6.31 inference(component_clause,[status(thm)],[f3548])).
% 5.64/6.31 fof(f3608,plain,(
% 5.64/6.31 $false|sQ24_spl),
% 5.64/6.31 inference(forward_subsumption_resolution,[status(thm)],[f3550,f3306])).
% 5.64/6.31 fof(f3609,plain,(
% 5.64/6.31 sQ24_spl),
% 5.64/6.31 inference(contradiction_clause,[status(thm)],[f3608])).
% 5.64/6.31 fof(f3789,plain,(
% 5.64/6.31 v_x=c_Transcendental_Opi|c_lessequals(c_Transcendental_Opi,v_x,tc_RealDef_Oreal)|sQ10_spl),
% 5.64/6.31 inference(resolution,[status(thm)],[f3385,f3522])).
% 5.64/6.31 fof(f3790,definition,(
% 5.64/6.31 sQ59_spl <=> (c_lessequals(c_Transcendental_Opi,v_x,tc_RealDef_Oreal))),
% 5.64/6.31 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 5.64/6.31 fof(f3791,plain,(
% 5.64/6.31 c_lessequals(c_Transcendental_Opi,v_x,tc_RealDef_Oreal)|~sQ59_spl),
% 5.64/6.31 inference(component_clause,[status(thm)],[f3790])).
% 5.64/6.31 fof(f3793,plain,(
% 5.64/6.31 sQ9_spl|sQ59_spl|sQ10_spl),
% 5.64/6.31 inference(split_clause,[status(thm)],[f3789,f3379,f3790,f3383])).
% 5.64/6.31 fof(f3794,plain,(
% 5.64/6.31 $false|sQ11_spl),
% 5.64/6.31 inference(forward_subsumption_resolution,[status(thm)],[f3388,f3223])).
% 5.64/6.31 fof(f3795,plain,(
% 5.64/6.31 sQ11_spl),
% 5.64/6.31 inference(contradiction_clause,[status(thm)],[f3794])).
% 5.64/6.31 fof(f3831,definition,(
% 5.64/6.31 sQ62_spl <=> (class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal))),
% 5.64/6.31 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 5.64/6.31 fof(f3833,plain,(
% 5.64/6.31 ~class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal)|sQ62_spl),
% 5.64/6.31 inference(component_clause,[status(thm)],[f3831])).
% 5.56/6.32 fof(f3852,plain,(
% 5.56/6.32 $false|sQ62_spl),
% 5.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f3833,f3241])).
% 5.56/6.32 fof(f3853,plain,(
% 5.56/6.32 sQ62_spl),
% 5.56/6.32 inference(contradiction_clause,[status(thm)],[f3852])).
% 5.56/6.32 fof(f4020,definition,(
% 5.56/6.32 sQ97_spl <=> (class_Ring__and__Field_Ofield(tc_RealDef_Oreal))),
% 5.56/6.32 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 5.56/6.32 fof(f4022,plain,(
% 5.56/6.32 ~class_Ring__and__Field_Ofield(tc_RealDef_Oreal)|sQ97_spl),
% 5.56/6.32 inference(component_clause,[status(thm)],[f4020])).
% 5.56/6.32 fof(f4031,plain,(
% 5.56/6.32 $false|sQ97_spl),
% 5.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f4022,f3301])).
% 5.56/6.32 fof(f4032,plain,(
% 5.56/6.32 sQ97_spl),
% 5.56/6.32 inference(contradiction_clause,[status(thm)],[f4031])).
% 5.56/6.32 fof(f4151,definition,(
% 5.56/6.32 sQ116_spl <=> (class_Orderings_Opreorder(tc_RealDef_Oreal))),
% 5.56/6.32 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 5.56/6.32 fof(f4153,plain,(
% 5.56/6.32 ~class_Orderings_Opreorder(tc_RealDef_Oreal)|sQ116_spl),
% 5.56/6.32 inference(component_clause,[status(thm)],[f4151])).
% 5.56/6.32 fof(f4172,plain,(
% 5.56/6.32 $false|sQ116_spl),
% 5.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f4153,f3305])).
% 5.56/6.32 fof(f4173,plain,(
% 5.56/6.32 sQ116_spl),
% 5.56/6.32 inference(contradiction_clause,[status(thm)],[f4172])).
% 5.56/6.32 fof(f4392,plain,(
% 5.56/6.32 ~class_Orderings_Olinorder(tc_RealDef_Oreal)|c_Transcendental_Opi=v_x|c_HOL_Oord__class_Oless(c_Transcendental_Opi,v_x,tc_RealDef_Oreal)|~sQ59_spl),
% 5.56/6.32 inference(resolution,[status(thm)],[f3791,f1526])).
% 5.56/6.32 fof(f4403,plain,(
% 5.56/6.32 ~sQ24_spl|sQ9_spl|sQ7_spl|~sQ59_spl),
% 5.56/6.32 inference(split_clause,[status(thm)],[f4392,f3548,f3379,f3372,f3790])).
% 5.56/6.32 fof(f4404,plain,(
% 5.56/6.32 $false),
% 5.56/6.32 inference(sat_refutation,[status(thm)],[f3375,f3382,f3389,f3417,f3420,f3428,f3609,f3793,f3795,f3853,f4032,f4173,f4403])).
% 5.56/6.32 % SZS output end CNFRefutation for theBenchmark.p
% 5.56/6.34 % Elapsed time: 0.946282 seconds
% 5.56/6.34 % CPU time: 6.721779 seconds
% 5.56/6.34 % Total memory used: 333.054 MB
% 5.56/6.34 % Net memory used: 330.419 MB
%------------------------------------------------------------------------------