%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS090+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:14 PM UTC 2026
% Result : Unsatisfiable 0.09s 5.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS090+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n019.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Sun Sep 20 22:53:42 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 % Drodi V4.1.1
% 0.09/5.39 % Refutation found
% 0.09/5.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/5.39 % SZS output start CNFRefutation for theBenchmark
% 0.09/5.39 fof(f4,axiom,(
% 0.09/5.39 (! [X] :( cC2(X)=> ( ( ~ cB(X)| cA(X) )& ( cB(X)| cA(X) ) ) ) )),
% 0.09/5.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.39 fof(f5,axiom,(
% 0.09/5.39 (! [X] :( cC3(X)=> ( ( ~ cB(X)| ~ cA(X) )& ( cB(X)| ~ cA(X) ) ) ) )),
% 0.09/5.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.39 fof(f6,axiom,(
% 0.09/5.39 (! [X] :( cC4(X)=> (? [Y] :( rR(X,Y)& cC2(Y) ) )) )),
% 0.09/5.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.39 fof(f7,axiom,(
% 0.09/5.39 (! [X] :( cC5(X)=> (! [Y] :( rR(X,Y)=> cC3(Y) ) )) )),
% 0.09/5.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.39 fof(f8,axiom,(
% 0.09/5.39 (! [X] :( cTEST(X)=> ( cC4(X)& cC1(X)& cC5(X) ) ) )),
% 0.09/5.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.39 fof(f9,axiom,(
% 0.09/5.39 cTEST(i2003_11_14_17_19_57994) ),
% 0.09/5.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.39 fof(f50,plain,(
% 0.09/5.39 ![X]: (~cC2(X)|((~cB(X)|cA(X))&(cB(X)|cA(X))))),
% 0.09/5.39 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.09/5.39 fof(f51,plain,(
% 0.09/5.39 ![X0]: (~cC2(X0)|~cB(X0)|cA(X0))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f50])).
% 0.09/5.39 fof(f52,plain,(
% 0.09/5.39 ![X0]: (~cC2(X0)|cB(X0)|cA(X0))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f50])).
% 0.09/5.39 fof(f53,plain,(
% 0.09/5.39 ![X]: (~cC3(X)|((~cB(X)|~cA(X))&(cB(X)|~cA(X))))),
% 0.09/5.39 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.09/5.39 fof(f54,plain,(
% 0.09/5.39 ![X0]: (~cC3(X0)|~cB(X0)|~cA(X0))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f53])).
% 0.09/5.39 fof(f55,plain,(
% 0.09/5.39 ![X0]: (~cC3(X0)|cB(X0)|~cA(X0))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f53])).
% 0.09/5.39 fof(f56,plain,(
% 0.09/5.39 ![X]: (~cC4(X)|(?[Y]: (rR(X,Y)&cC2(Y))))),
% 0.09/5.39 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.09/5.39 fof(f57,plain,(
% 0.09/5.39 ![X]: (~cC4(X)|(rR(X,sK0_skl(X))&cC2(sK0_skl(X))))),
% 0.09/5.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y,sK0_skl(X))],[f56])).
% 0.09/5.39 fof(f58,plain,(
% 0.09/5.39 ![X0]: (~cC4(X0)|rR(X0,sK0_skl(X0)))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f57])).
% 0.09/5.39 fof(f59,plain,(
% 0.09/5.39 ![X0]: (~cC4(X0)|cC2(sK0_skl(X0)))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f57])).
% 0.09/5.39 fof(f60,plain,(
% 0.09/5.39 ![X]: (~cC5(X)|(![Y]: (~rR(X,Y)|cC3(Y))))),
% 0.09/5.39 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.09/5.39 fof(f61,plain,(
% 0.09/5.39 ![X0,X1]: (~cC5(X0)|~rR(X0,X1)|cC3(X1))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f60])).
% 0.09/5.39 fof(f62,plain,(
% 0.09/5.39 ![X]: (~cTEST(X)|((cC4(X)&cC1(X))&cC5(X)))),
% 0.09/5.39 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.09/5.39 fof(f63,plain,(
% 0.09/5.39 ![X0]: (~cTEST(X0)|cC4(X0))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f62])).
% 0.09/5.39 fof(f65,plain,(
% 0.09/5.39 ![X0]: (~cTEST(X0)|cC5(X0))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f62])).
% 0.09/5.39 fof(f66,plain,(
% 0.09/5.39 cTEST(i2003_11_14_17_19_57994)),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f9])).
% 0.09/5.39 fof(f68,plain,(
% 0.09/5.39 cC4(i2003_11_14_17_19_57994)),
% 0.09/5.39 inference(resolution,[status(thm)],[f63,f66])).
% 0.09/5.39 fof(f70,plain,(
% 0.09/5.39 cC5(i2003_11_14_17_19_57994)),
% 0.09/5.39 inference(resolution,[status(thm)],[f65,f66])).
% 0.09/5.39 fof(f71,plain,(
% 0.09/5.39 ![X0]: (~cC2(X0)|cA(X0))),
% 0.09/5.39 inference(forward_subsumption_resolution,[status(thm)],[f52,f51])).
% 0.09/5.39 fof(f72,plain,(
% 0.09/5.39 ![X0]: (~cC3(X0)|~cA(X0))),
% 0.09/5.39 inference(forward_subsumption_resolution,[status(thm)],[f55,f54])).
% 0.09/5.39 fof(f73,plain,(
% 0.09/5.39 ![X0]: (~rR(i2003_11_14_17_19_57994,X0)|cC3(X0))),
% 0.09/5.39 inference(resolution,[status(thm)],[f61,f70])).
% 0.09/5.39 fof(f74,plain,(
% 0.09/5.39 cC3(sK0_skl(i2003_11_14_17_19_57994))|~cC4(i2003_11_14_17_19_57994)),
% 0.09/5.39 inference(resolution,[status(thm)],[f73,f58])).
% 0.09/5.39 fof(f75,definition,(
% 0.09/5.39 sQ0_spl <=> (cC3(sK0_skl(i2003_11_14_17_19_57994)))),
% 0.09/5.39 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.09/5.39 fof(f76,plain,(
% 0.09/5.39 cC3(sK0_skl(i2003_11_14_17_19_57994))|~sQ0_spl),
% 0.09/5.39 inference(component_clause,[status(thm)],[f75])).
% 0.09/5.39 fof(f78,definition,(
% 0.09/5.39 sQ1_spl <=> (cC4(i2003_11_14_17_19_57994))),
% 0.09/5.39 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.09/5.39 fof(f80,plain,(
% 0.09/5.39 ~cC4(i2003_11_14_17_19_57994)|sQ1_spl),
% 0.09/5.39 inference(component_clause,[status(thm)],[f78])).
% 0.09/5.39 fof(f81,plain,(
% 0.09/5.39 sQ0_spl|~sQ1_spl),
% 0.09/5.39 inference(split_clause,[status(thm)],[f74,f75,f78])).
% 0.09/5.39 fof(f82,plain,(
% 0.09/5.39 ~cA(sK0_skl(i2003_11_14_17_19_57994))|~sQ0_spl),
% 0.09/5.39 inference(resolution,[status(thm)],[f76,f72])).
% 0.09/5.39 fof(f83,plain,(
% 0.09/5.39 ~cC2(sK0_skl(i2003_11_14_17_19_57994))|~sQ0_spl),
% 0.09/5.39 inference(resolution,[status(thm)],[f82,f71])).
% 0.09/5.39 fof(f84,plain,(
% 0.09/5.39 ~cC4(i2003_11_14_17_19_57994)|~sQ0_spl),
% 0.09/5.39 inference(resolution,[status(thm)],[f83,f59])).
% 0.09/5.39 fof(f85,plain,(
% 0.09/5.39 $false|~sQ0_spl),
% 0.09/5.39 inference(forward_subsumption_resolution,[status(thm)],[f84,f68])).
% 0.09/5.39 fof(f86,plain,(
% 0.09/5.39 ~sQ0_spl),
% 0.09/5.39 inference(contradiction_clause,[status(thm)],[f85])).
% 0.09/5.39 fof(f87,plain,(
% 0.09/5.39 $false|sQ1_spl),
% 0.09/5.39 inference(forward_subsumption_resolution,[status(thm)],[f80,f68])).
% 0.09/5.39 fof(f88,plain,(
% 0.09/5.39 sQ1_spl),
% 0.09/5.39 inference(contradiction_clause,[status(thm)],[f87])).
% 0.09/5.39 fof(f89,plain,(
% 0.09/5.39 $false),
% 0.09/5.39 inference(sat_refutation,[status(thm)],[f81,f86,f88])).
% 0.09/5.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.40 % Elapsed time: 0.029739 seconds
% 0.14/5.40 % CPU time: 0.078489 seconds
% 0.14/5.40 % Total memory used: 3.563 MB
% 0.14/5.40 % Net memory used: 3.534 MB
%------------------------------------------------------------------------------