%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS010-1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:00:05 PM UTC 2026
% Result : Unsatisfiable 0.23s 5.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : KRS010-1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/5.46 % Computer : n015.cluster.edu
% 0.19/5.46 % Model : x86_64 x86_64
% 0.19/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.46 % Memory : 8046.5625MB
% 0.19/5.46 % OS : Linux 6.8.0-71-generic
% 0.19/5.46 % CPULimit : 300
% 0.19/5.46 % WCLimit : 300
% 0.19/5.46 % DateTime : Sun Sep 20 22:53:25 UTC 2026
% 0.19/5.46 % CPUTime :
% 0.19/5.47 % Drodi V4.1.1
% 0.23/5.51 % Refutation found
% 0.23/5.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.23/5.51 % SZS output start CNFRefutation for theBenchmark
% 0.23/5.51 fof(f1,negated_conjecture,(
% 0.23/5.51 e(exist) ),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f2,negated_conjecture,(
% 0.23/5.51 ~ f(exist) ),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f3,axiom,(
% 0.23/5.51 (![X1]: (( c(X1)| d(X1)| ~ a(X1) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f6,axiom,(
% 0.23/5.51 (![X4,X3,X1]: (( equalish(X4,X3)| ~ e(X1)| ~ r(X1,X4)| ~ r(X1,X3)| ~ c(X4)| ~ c(X3) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f7,axiom,(
% 0.23/5.51 (![X1]: (( r3least(X1)| ~ e(X1) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f8,axiom,(
% 0.23/5.51 (![X2,X1]: (( a(X2)| ~ e(X1)| ~ r(X1,X2) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f19,axiom,(
% 0.23/5.51 (![X1]: (( ~ r3least(X1)| ~ equalish(u2r2(X1),u2r1(X1)) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f20,axiom,(
% 0.23/5.51 (![X1]: (( ~ r3least(X1)| ~ equalish(u2r3(X1),u2r1(X1)) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f21,axiom,(
% 0.23/5.51 (![X1]: (( ~ r3least(X1)| ~ equalish(u2r3(X1),u2r2(X1)) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f22,axiom,(
% 0.23/5.51 (![X1]: (( r(X1,u2r1(X1))| ~ r3least(X1) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f23,axiom,(
% 0.23/5.51 (![X1]: (( r(X1,u2r2(X1))| ~ r3least(X1) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f24,axiom,(
% 0.23/5.51 (![X1]: (( r(X1,u2r3(X1))| ~ r3least(X1) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f31,axiom,(
% 0.23/5.51 (![X1,X3,X2]: (( f(X1)| equalish(X3,X2)| ~ r(X1,X3)| ~ r(X1,X2)| ~ d(X3)| ~ d(X2) ) ))),
% 0.23/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.51 fof(f32,plain,(
% 0.23/5.51 e(exist)),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f1])).
% 0.23/5.51 fof(f33,plain,(
% 0.23/5.51 ~f(exist)),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f2])).
% 0.23/5.51 fof(f34,plain,(
% 0.23/5.51 ![X0]: (c(X0)|d(X0)|~a(X0))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f3])).
% 0.23/5.51 fof(f37,plain,(
% 0.23/5.51 ![X3]: ((![X4]: ((![X1]: (((equalish(X4,X3)|~e(X1))|~r(X1,X4))|~r(X1,X3)))|~c(X4)))|~c(X3))),
% 0.23/5.51 inference(miniscoping,[status(thm)],[f6])).
% 0.23/5.51 fof(f38,plain,(
% 0.23/5.51 ![X0,X1,X2]: (equalish(X0,X1)|~e(X2)|~r(X2,X0)|~r(X2,X1)|~c(X0)|~c(X1))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f37])).
% 0.23/5.51 fof(f39,plain,(
% 0.23/5.51 ![X0]: (r3least(X0)|~e(X0))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f7])).
% 0.23/5.51 fof(f40,plain,(
% 0.23/5.51 ![X0,X1]: (a(X0)|~e(X1)|~r(X1,X0))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.23/5.51 fof(f51,plain,(
% 0.23/5.51 ![X0]: (~r3least(X0)|~equalish(u2r2(X0),u2r1(X0)))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f19])).
% 0.23/5.51 fof(f52,plain,(
% 0.23/5.51 ![X0]: (~r3least(X0)|~equalish(u2r3(X0),u2r1(X0)))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f20])).
% 0.23/5.51 fof(f53,plain,(
% 0.23/5.51 ![X0]: (~r3least(X0)|~equalish(u2r3(X0),u2r2(X0)))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f21])).
% 0.23/5.51 fof(f54,plain,(
% 0.23/5.51 ![X0]: (r(X0,u2r1(X0))|~r3least(X0))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f22])).
% 0.23/5.51 fof(f55,plain,(
% 0.23/5.51 ![X0]: (r(X0,u2r2(X0))|~r3least(X0))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f23])).
% 0.23/5.51 fof(f56,plain,(
% 0.23/5.51 ![X0]: (r(X0,u2r3(X0))|~r3least(X0))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f24])).
% 0.23/5.51 fof(f64,plain,(
% 0.23/5.51 ![X2]: ((![X3]: ((![X1]: (((f(X1)|equalish(X3,X2))|~r(X1,X3))|~r(X1,X2)))|~d(X3)))|~d(X2))),
% 0.23/5.51 inference(miniscoping,[status(thm)],[f31])).
% 0.23/5.51 fof(f65,plain,(
% 0.23/5.51 ![X0,X1,X2]: (f(X0)|equalish(X1,X2)|~r(X0,X1)|~r(X0,X2)|~d(X1)|~d(X2))),
% 0.23/5.51 inference(cnf_transformation,[status(thm)],[f64])).
% 0.23/5.51 fof(f66,plain,(
% 0.23/5.51 r3least(exist)),
% 0.23/5.51 inference(resolution,[status(thm)],[f39,f32])).
% 0.23/5.51 fof(f67,plain,(
% 0.23/5.51 ![X0]: (a(X0)|~r(exist,X0))),
% 0.23/5.51 inference(resolution,[status(thm)],[f40,f32])).
% 0.23/5.51 fof(f68,plain,(
% 0.23/5.51 a(u2r1(exist))|~r3least(exist)),
% 0.23/5.51 inference(resolution,[status(thm)],[f67,f54])).
% 0.23/5.51 fof(f69,definition,(
% 0.23/5.51 sQ0_spl <=> (a(u2r1(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f70,plain,(
% 0.23/5.51 a(u2r1(exist))|~sQ0_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f69])).
% 0.23/5.51 fof(f72,definition,(
% 0.23/5.51 sQ1_spl <=> (r3least(exist))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f74,plain,(
% 0.23/5.51 ~r3least(exist)|sQ1_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f72])).
% 0.23/5.51 fof(f75,plain,(
% 0.23/5.51 sQ0_spl|~sQ1_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f68,f69,f72])).
% 0.23/5.51 fof(f76,plain,(
% 0.23/5.51 c(u2r1(exist))|d(u2r1(exist))|~sQ0_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f70,f34])).
% 0.23/5.51 fof(f77,definition,(
% 0.23/5.51 sQ2_spl <=> (c(u2r1(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f78,plain,(
% 0.23/5.51 c(u2r1(exist))|~sQ2_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f77])).
% 0.23/5.51 fof(f80,definition,(
% 0.23/5.51 sQ3_spl <=> (d(u2r1(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f81,plain,(
% 0.23/5.51 d(u2r1(exist))|~sQ3_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f80])).
% 0.23/5.51 fof(f83,plain,(
% 0.23/5.51 sQ2_spl|sQ3_spl|~sQ0_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f76,f77,f80,f69])).
% 0.23/5.51 fof(f84,plain,(
% 0.23/5.51 $false|sQ1_spl),
% 0.23/5.51 inference(forward_subsumption_resolution,[status(thm)],[f74,f66])).
% 0.23/5.51 fof(f85,plain,(
% 0.23/5.51 sQ1_spl),
% 0.23/5.51 inference(contradiction_clause,[status(thm)],[f84])).
% 0.23/5.51 fof(f86,plain,(
% 0.23/5.51 ![X0,X1]: (equalish(X0,u2r1(exist))|~e(X1)|~r(X1,X0)|~r(X1,u2r1(exist))|~c(X0)|~sQ2_spl)),
% 0.23/5.51 inference(resolution,[status(thm)],[f78,f38])).
% 0.23/5.51 fof(f90,plain,(
% 0.23/5.51 ~r3least(exist)|a(u2r2(exist))),
% 0.23/5.51 inference(resolution,[status(thm)],[f55,f67])).
% 0.23/5.51 fof(f91,definition,(
% 0.23/5.51 sQ4_spl <=> (a(u2r2(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f92,plain,(
% 0.23/5.51 a(u2r2(exist))|~sQ4_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f91])).
% 0.23/5.51 fof(f94,plain,(
% 0.23/5.51 ~sQ1_spl|sQ4_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f90,f72,f91])).
% 0.23/5.51 fof(f95,plain,(
% 0.23/5.51 c(u2r2(exist))|d(u2r2(exist))|~sQ4_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f92,f34])).
% 0.23/5.51 fof(f96,definition,(
% 0.23/5.51 sQ5_spl <=> (c(u2r2(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f97,plain,(
% 0.23/5.51 c(u2r2(exist))|~sQ5_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f96])).
% 0.23/5.51 fof(f99,definition,(
% 0.23/5.51 sQ6_spl <=> (d(u2r2(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f100,plain,(
% 0.23/5.51 d(u2r2(exist))|~sQ6_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f99])).
% 0.23/5.51 fof(f102,plain,(
% 0.23/5.51 sQ5_spl|sQ6_spl|~sQ4_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f95,f96,f99,f91])).
% 0.23/5.51 fof(f103,plain,(
% 0.23/5.51 ![X0,X1]: (equalish(X0,u2r2(exist))|~e(X1)|~r(X1,X0)|~r(X1,u2r2(exist))|~c(X0)|~sQ5_spl)),
% 0.23/5.51 inference(resolution,[status(thm)],[f97,f38])).
% 0.23/5.51 fof(f105,plain,(
% 0.23/5.51 ~r3least(exist)|a(u2r3(exist))),
% 0.23/5.51 inference(resolution,[status(thm)],[f56,f67])).
% 0.23/5.51 fof(f106,definition,(
% 0.23/5.51 sQ7_spl <=> (a(u2r3(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f107,plain,(
% 0.23/5.51 a(u2r3(exist))|~sQ7_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f106])).
% 0.23/5.51 fof(f109,plain,(
% 0.23/5.51 ~sQ1_spl|sQ7_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f105,f72,f106])).
% 0.23/5.51 fof(f110,plain,(
% 0.23/5.51 c(u2r3(exist))|d(u2r3(exist))|~sQ7_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f107,f34])).
% 0.23/5.51 fof(f111,definition,(
% 0.23/5.51 sQ8_spl <=> (c(u2r3(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f114,definition,(
% 0.23/5.51 sQ9_spl <=> (d(u2r3(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f117,plain,(
% 0.23/5.51 sQ8_spl|sQ9_spl|~sQ7_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f110,f111,f114,f106])).
% 0.23/5.51 fof(f120,plain,(
% 0.23/5.51 ![X0]: (~r3least(exist)|~e(X0)|~r(X0,u2r2(exist))|~r(X0,u2r1(exist))|~c(u2r2(exist))|~sQ2_spl)),
% 0.23/5.51 inference(resolution,[status(thm)],[f51,f86])).
% 0.23/5.51 fof(f121,definition,(
% 0.23/5.51 ![X0]: (sQ10_spl <=> (~e(X0)|~r(X0,u2r2(exist))|~r(X0,u2r1(exist))))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f122,plain,(
% 0.23/5.51 ![X0]: (~e(X0)|~r(X0,u2r2(exist))|~r(X0,u2r1(exist))|~sQ10_spl)),
% 0.23/5.51 inference(component_clause,[status(thm)],[f121])).
% 0.23/5.51 fof(f124,plain,(
% 0.23/5.51 ~sQ1_spl|sQ10_spl|~sQ5_spl|~sQ2_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f120,f72,f121,f96,f77])).
% 0.23/5.51 fof(f127,plain,(
% 0.23/5.51 ~r(exist,u2r2(exist))|~r(exist,u2r1(exist))|~sQ10_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f122,f32])).
% 0.23/5.51 fof(f128,definition,(
% 0.23/5.51 sQ11_spl <=> (r(exist,u2r2(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f129,plain,(
% 0.23/5.51 r(exist,u2r2(exist))|~sQ11_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f128])).
% 0.23/5.51 fof(f130,plain,(
% 0.23/5.51 ~r(exist,u2r2(exist))|sQ11_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f128])).
% 0.23/5.51 fof(f131,definition,(
% 0.23/5.51 sQ12_spl <=> (r(exist,u2r1(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f132,plain,(
% 0.23/5.51 r(exist,u2r1(exist))|~sQ12_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f131])).
% 0.23/5.51 fof(f133,plain,(
% 0.23/5.51 ~r(exist,u2r1(exist))|sQ12_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f131])).
% 0.23/5.51 fof(f134,plain,(
% 0.23/5.51 ~sQ11_spl|~sQ12_spl|~sQ10_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f127,f128,f131,f121])).
% 0.23/5.51 fof(f136,plain,(
% 0.23/5.51 ~r3least(exist)|sQ12_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f133,f54])).
% 0.23/5.51 fof(f137,plain,(
% 0.23/5.51 ~sQ1_spl|sQ12_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f136,f72,f131])).
% 0.23/5.51 fof(f138,plain,(
% 0.23/5.51 ~r3least(exist)|sQ11_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f130,f55])).
% 0.23/5.51 fof(f139,plain,(
% 0.23/5.51 ~sQ1_spl|sQ11_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f138,f72,f128])).
% 0.23/5.51 fof(f253,definition,(
% 0.23/5.51 sQ26_spl <=> (r(exist,u2r3(exist)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f255,plain,(
% 0.23/5.51 ~r(exist,u2r3(exist))|sQ26_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f253])).
% 0.23/5.51 fof(f363,plain,(
% 0.23/5.51 ~r3least(exist)|sQ26_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f255,f56])).
% 0.23/5.51 fof(f364,plain,(
% 0.23/5.51 ~sQ1_spl|sQ26_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f363,f72,f253])).
% 0.23/5.51 fof(f423,plain,(
% 0.23/5.51 ![X0,X1]: (f(X0)|equalish(X1,u2r1(exist))|~r(X0,X1)|~r(X0,u2r1(exist))|~d(X1)|~sQ3_spl)),
% 0.23/5.51 inference(resolution,[status(thm)],[f65,f81])).
% 0.23/5.51 fof(f424,plain,(
% 0.23/5.51 ![X0,X1]: (f(X0)|equalish(X1,u2r2(exist))|~r(X0,X1)|~r(X0,u2r2(exist))|~d(X1)|~sQ6_spl)),
% 0.23/5.51 inference(resolution,[status(thm)],[f65,f100])).
% 0.23/5.51 fof(f425,plain,(
% 0.23/5.51 ![X0]: (f(X0)|~r(X0,u2r3(exist))|~r(X0,u2r1(exist))|~d(u2r3(exist))|~r3least(exist)|~sQ3_spl)),
% 0.23/5.51 inference(resolution,[status(thm)],[f423,f52])).
% 0.23/5.51 fof(f426,plain,(
% 0.23/5.51 ![X0]: (f(X0)|~r(X0,u2r2(exist))|~r(X0,u2r1(exist))|~d(u2r2(exist))|~r3least(exist)|~sQ3_spl)),
% 0.23/5.51 inference(resolution,[status(thm)],[f423,f51])).
% 0.23/5.51 fof(f427,definition,(
% 0.23/5.51 ![X0]: (sQ48_spl <=> (f(X0)|~r(X0,u2r3(exist))|~r(X0,u2r1(exist))))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f428,plain,(
% 0.23/5.51 ![X0]: (f(X0)|~r(X0,u2r3(exist))|~r(X0,u2r1(exist))|~sQ48_spl)),
% 0.23/5.51 inference(component_clause,[status(thm)],[f427])).
% 0.23/5.51 fof(f430,plain,(
% 0.23/5.51 sQ48_spl|~sQ9_spl|~sQ1_spl|~sQ3_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f425,f427,f114,f72,f80])).
% 0.23/5.51 fof(f431,definition,(
% 0.23/5.51 ![X0]: (sQ49_spl <=> (f(X0)|~r(X0,u2r2(exist))|~r(X0,u2r1(exist))))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f432,plain,(
% 0.23/5.51 ![X0]: (f(X0)|~r(X0,u2r2(exist))|~r(X0,u2r1(exist))|~sQ49_spl)),
% 0.23/5.51 inference(component_clause,[status(thm)],[f431])).
% 0.23/5.51 fof(f434,plain,(
% 0.23/5.51 sQ49_spl|~sQ6_spl|~sQ1_spl|~sQ3_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f426,f431,f99,f72,f80])).
% 0.23/5.51 fof(f438,plain,(
% 0.23/5.51 f(exist)|~r(exist,u2r1(exist))|~r3least(exist)|~sQ49_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f432,f55])).
% 0.23/5.51 fof(f439,definition,(
% 0.23/5.51 sQ50_spl <=> (f(exist))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f440,plain,(
% 0.23/5.51 f(exist)|~sQ50_spl),
% 0.23/5.51 inference(component_clause,[status(thm)],[f439])).
% 0.23/5.51 fof(f443,plain,(
% 0.23/5.51 sQ50_spl|~sQ12_spl|~sQ1_spl|~sQ49_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f438,f439,f131,f72,f431])).
% 0.23/5.51 fof(f444,plain,(
% 0.23/5.51 $false|~sQ50_spl),
% 0.23/5.51 inference(forward_subsumption_resolution,[status(thm)],[f440,f33])).
% 0.23/5.51 fof(f445,plain,(
% 0.23/5.51 ~sQ50_spl),
% 0.23/5.51 inference(contradiction_clause,[status(thm)],[f444])).
% 0.23/5.51 fof(f448,plain,(
% 0.23/5.51 f(exist)|~r(exist,u2r3(exist))|~sQ48_spl|~sQ12_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f428,f132])).
% 0.23/5.51 fof(f450,plain,(
% 0.23/5.51 sQ50_spl|~sQ26_spl|~sQ48_spl|~sQ12_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f448,f439,f253,f427,f131])).
% 0.23/5.51 fof(f452,plain,(
% 0.23/5.51 ![X0]: (f(X0)|~r(X0,u2r3(exist))|~r(X0,u2r2(exist))|~d(u2r3(exist))|~r3least(exist)|~sQ6_spl)),
% 0.23/5.51 inference(resolution,[status(thm)],[f424,f53])).
% 0.23/5.51 fof(f453,definition,(
% 0.23/5.51 ![X0]: (sQ51_spl <=> (f(X0)|~r(X0,u2r3(exist))|~r(X0,u2r2(exist))))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f454,plain,(
% 0.23/5.51 ![X0]: (f(X0)|~r(X0,u2r3(exist))|~r(X0,u2r2(exist))|~sQ51_spl)),
% 0.23/5.51 inference(component_clause,[status(thm)],[f453])).
% 0.23/5.51 fof(f456,plain,(
% 0.23/5.51 sQ51_spl|~sQ9_spl|~sQ1_spl|~sQ6_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f452,f453,f114,f72,f99])).
% 0.23/5.51 fof(f457,plain,(
% 0.23/5.51 f(exist)|~r(exist,u2r3(exist))|~sQ51_spl|~sQ11_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f454,f129])).
% 0.23/5.51 fof(f459,plain,(
% 0.23/5.51 sQ50_spl|~sQ26_spl|~sQ51_spl|~sQ11_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f457,f439,f253,f453,f128])).
% 0.23/5.51 fof(f461,plain,(
% 0.23/5.51 ![X0]: (equalish(X0,u2r1(exist))|~r(exist,X0)|~r(exist,u2r1(exist))|~c(X0)|~sQ2_spl)),
% 0.23/5.51 inference(resolution,[status(thm)],[f86,f32])).
% 0.23/5.51 fof(f462,definition,(
% 0.23/5.51 ![X0]: (sQ52_spl <=> (equalish(X0,u2r1(exist))|~r(exist,X0)|~c(X0)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f463,plain,(
% 0.23/5.51 ![X0]: (equalish(X0,u2r1(exist))|~r(exist,X0)|~c(X0)|~sQ52_spl)),
% 0.23/5.51 inference(component_clause,[status(thm)],[f462])).
% 0.23/5.51 fof(f465,plain,(
% 0.23/5.51 sQ52_spl|~sQ12_spl|~sQ2_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f461,f462,f131,f77])).
% 0.23/5.51 fof(f470,plain,(
% 0.23/5.51 ~r(exist,u2r3(exist))|~c(u2r3(exist))|~r3least(exist)|~sQ52_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f463,f52])).
% 0.23/5.51 fof(f472,plain,(
% 0.23/5.51 ~sQ26_spl|~sQ8_spl|~sQ1_spl|~sQ52_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f470,f253,f111,f72,f462])).
% 0.23/5.51 fof(f478,plain,(
% 0.23/5.51 ![X0]: (equalish(X0,u2r2(exist))|~r(exist,X0)|~r(exist,u2r2(exist))|~c(X0)|~sQ5_spl)),
% 0.23/5.51 inference(resolution,[status(thm)],[f103,f32])).
% 0.23/5.51 fof(f479,definition,(
% 0.23/5.51 ![X0]: (sQ53_spl <=> (equalish(X0,u2r2(exist))|~r(exist,X0)|~c(X0)))),
% 0.23/5.51 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.23/5.51 fof(f480,plain,(
% 0.23/5.51 ![X0]: (equalish(X0,u2r2(exist))|~r(exist,X0)|~c(X0)|~sQ53_spl)),
% 0.23/5.51 inference(component_clause,[status(thm)],[f479])).
% 0.23/5.51 fof(f482,plain,(
% 0.23/5.51 sQ53_spl|~sQ11_spl|~sQ5_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f478,f479,f128,f96])).
% 0.23/5.51 fof(f483,plain,(
% 0.23/5.51 ~r(exist,u2r3(exist))|~c(u2r3(exist))|~r3least(exist)|~sQ53_spl),
% 0.23/5.51 inference(resolution,[status(thm)],[f480,f53])).
% 0.23/5.51 fof(f484,plain,(
% 0.23/5.51 ~sQ26_spl|~sQ8_spl|~sQ1_spl|~sQ53_spl),
% 0.23/5.51 inference(split_clause,[status(thm)],[f483,f253,f111,f72,f479])).
% 0.23/5.51 fof(f485,plain,(
% 0.23/5.51 $false),
% 0.23/5.51 inference(sat_refutation,[status(thm)],[f75,f83,f85,f94,f102,f109,f117,f124,f134,f137,f139,f364,f430,f434,f443,f445,f450,f456,f459,f465,f472,f482,f484])).
% 0.23/5.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/5.53 % Elapsed time: 0.066109 seconds
% 0.23/5.53 % CPU time: 0.052577 seconds
% 0.23/5.53 % Total memory used: 1.451 MB
% 0.23/5.53 % Net memory used: 1.442 MB
%------------------------------------------------------------------------------