%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN982-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 03:21:39 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN982-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 11:37:45 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.14/0.43 % Refutation found
% 0.14/0.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.43 fof(f3,axiom,(
% 0.14/0.43 ssBf(na) ),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f4,axiom,(
% 0.14/0.43 ssP(b) ),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f5,axiom,(
% 0.14/0.43 ssP(a) ),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f14,axiom,(
% 0.14/0.43 (![U,V]: (( ~ ssIm(pair(U,V))| ssIm(V) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f16,axiom,(
% 0.14/0.43 ssM(sent(a,b,pair(a,na))) ),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f17,axiom,(
% 0.14/0.43 (![U,V,W]: (( ~ ssIm(triple(U,V,W))| ssIm(W) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f18,axiom,(
% 0.14/0.43 (![U,V,W]: (( ~ ssIm(triple(U,V,W))| ssIm(V) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f20,axiom,(
% 0.14/0.43 (![U,V,W]: (( ~ ssM(sent(U,V,W))| ssIm(W) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f25,axiom,(
% 0.14/0.43 (![U,V]: (( ~ ssIm(U)| ~ ssP(V)| ssIk(key(U,V)) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f26,axiom,(
% 0.14/0.43 (![U,V]: (( ~ ssIm(U)| ~ ssIm(V)| ssIm(pair(U,V)) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f27,axiom,(
% 0.14/0.43 (![U,V,W]: (( ~ ssIm(U)| ~ ssP(V)| ~ ssP(W)| ssM(sent(V,W,U)) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f29,axiom,(
% 0.14/0.43 (![U,V,W]: (( ~ ssIm(U)| ~ ssIk(key(V,W))| ~ ssP(W)| ssIm(encr(U,V)) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f30,axiom,(
% 0.14/0.43 (![U,V]: (( ~ ssM(sent(U,b,pair(U,V)))| ~ ssBf(V)| ssSb(pair(U,V)) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f33,axiom,(
% 0.14/0.43 (![U,V]: (( ~ ssM(sent(U,b,pair(U,V)))| ~ ssBf(V)| ssM(sent(b,t,triple(b,nb(V),encr(triple(U,V,tb(V)),bt)))) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f34,axiom,(
% 0.14/0.43 (![U,V,W]: (( ~ ssM(sent(U,b,pair(encr(triple(U,V,tb(W)),bt),encr(nb(W),V))))| ~ ssSb(pair(U,W))| ssBk(key(V,U)) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f37,negated_conjecture,(
% 0.14/0.43 (![U]: (( ~ ssIk(key(U,b))| ~ ssBk(key(U,a)) ) ))),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f40,plain,(
% 0.14/0.43 ssBf(na)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f3])).
% 0.14/0.43 fof(f41,plain,(
% 0.14/0.43 ssP(b)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.43 fof(f42,plain,(
% 0.14/0.43 ssP(a)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.43 fof(f51,plain,(
% 0.14/0.43 ![V]: ((![U]: ~ssIm(pair(U,V)))|ssIm(V))),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f14])).
% 0.14/0.43 fof(f52,plain,(
% 0.14/0.43 ![X0,X1]: (~ssIm(pair(X0,X1))|ssIm(X1))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f51])).
% 0.14/0.43 fof(f55,plain,(
% 0.14/0.43 ssM(sent(a,b,pair(a,na)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f16])).
% 0.14/0.43 fof(f56,plain,(
% 0.14/0.43 ![W]: ((![U,V]: ~ssIm(triple(U,V,W)))|ssIm(W))),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f17])).
% 0.14/0.43 fof(f57,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~ssIm(triple(X0,X1,X2))|ssIm(X2))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f56])).
% 0.14/0.43 fof(f58,plain,(
% 0.14/0.43 ![V]: ((![U,W]: ~ssIm(triple(U,V,W)))|ssIm(V))),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f18])).
% 0.14/0.43 fof(f59,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~ssIm(triple(X0,X1,X2))|ssIm(X1))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f58])).
% 0.14/0.43 fof(f62,plain,(
% 0.14/0.43 ![W]: ((![U,V]: ~ssM(sent(U,V,W)))|ssIm(W))),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f20])).
% 0.14/0.43 fof(f63,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~ssM(sent(X0,X1,X2))|ssIm(X2))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f62])).
% 0.14/0.43 fof(f72,plain,(
% 0.14/0.43 ![X0,X1]: (~ssIm(X0)|~ssP(X1)|ssIk(key(X0,X1)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f25])).
% 0.14/0.43 fof(f73,plain,(
% 0.14/0.43 ![X0,X1]: (~ssIm(X0)|~ssIm(X1)|ssIm(pair(X0,X1)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f26])).
% 0.14/0.43 fof(f74,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~ssIm(X0)|~ssP(X1)|~ssP(X2)|ssM(sent(X1,X2,X0)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f27])).
% 0.14/0.43 fof(f76,plain,(
% 0.14/0.43 ![U,V]: ((![W]: ((~ssIm(U)|~ssIk(key(V,W)))|~ssP(W)))|ssIm(encr(U,V)))),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f29])).
% 0.14/0.43 fof(f77,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~ssIm(X0)|~ssIk(key(X1,X2))|~ssP(X2)|ssIm(encr(X0,X1)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f76])).
% 0.14/0.43 fof(f78,plain,(
% 0.14/0.43 ![X0,X1]: (~ssM(sent(X0,b,pair(X0,X1)))|~ssBf(X1)|ssSb(pair(X0,X1)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f30])).
% 0.14/0.43 fof(f82,plain,(
% 0.14/0.43 ![X0,X1]: (~ssM(sent(X0,b,pair(X0,X1)))|~ssBf(X1)|ssM(sent(b,t,triple(b,nb(X1),encr(triple(X0,X1,tb(X1)),bt)))))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f33])).
% 0.14/0.43 fof(f83,plain,(
% 0.14/0.43 ![U,V]: ((![W]: (~ssM(sent(U,b,pair(encr(triple(U,V,tb(W)),bt),encr(nb(W),V))))|~ssSb(pair(U,W))))|ssBk(key(V,U)))),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f34])).
% 0.14/0.43 fof(f84,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~ssM(sent(X0,b,pair(encr(triple(X0,X1,tb(X2)),bt),encr(nb(X2),X1))))|~ssSb(pair(X0,X2))|ssBk(key(X1,X0)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f83])).
% 0.14/0.43 fof(f88,plain,(
% 0.14/0.43 ![X0]: (~ssIk(key(X0,b))|~ssBk(key(X0,a)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f37])).
% 0.14/0.43 fof(f89,plain,(
% 0.14/0.43 ssIm(pair(a,na))),
% 0.14/0.43 inference(resolution,[status(thm)],[f63,f55])).
% 0.14/0.43 fof(f91,plain,(
% 0.14/0.43 ssIm(na)),
% 0.14/0.43 inference(resolution,[status(thm)],[f89,f52])).
% 0.14/0.43 fof(f95,definition,(
% 0.14/0.43 sQ0_spl <=> (ssP(b))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f97,plain,(
% 0.14/0.43 ~ssP(b)|sQ0_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f95])).
% 0.14/0.43 fof(f102,definition,(
% 0.14/0.43 ![X0]: (sQ2_spl <=> (~ssP(X0)|~ssP(X0)))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f103,plain,(
% 0.14/0.43 ![X0]: (~ssP(X0)|~ssP(X0)|~sQ2_spl)),
% 0.14/0.43 inference(component_clause,[status(thm)],[f102])).
% 0.14/0.43 fof(f109,plain,(
% 0.14/0.43 ![X0]: (~ssP(X0)|~sQ2_spl)),
% 0.14/0.43 inference(duplicate_literals_removal,[status(thm)],[f103])).
% 0.14/0.43 fof(f110,plain,(
% 0.14/0.43 $false|sQ0_spl),
% 0.14/0.43 inference(forward_subsumption_resolution,[status(thm)],[f97,f41])).
% 0.14/0.43 fof(f111,plain,(
% 0.14/0.43 sQ0_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f110])).
% 0.14/0.43 fof(f112,plain,(
% 0.14/0.43 $false|~sQ2_spl),
% 0.14/0.43 inference(backward_subsumption_resolution,[status(thm)],[f42,f109])).
% 0.14/0.43 fof(f115,plain,(
% 0.14/0.43 ~sQ2_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f112])).
% 0.14/0.43 fof(f116,plain,(
% 0.14/0.43 ![X0]: (~ssIm(X0)|~ssP(b)|~ssBk(key(X0,a)))),
% 0.14/0.43 inference(resolution,[status(thm)],[f72,f88])).
% 0.14/0.43 fof(f117,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~ssIm(X0)|~ssP(X1)|~ssIm(X2)|~ssP(X1)|ssIm(encr(X2,X0)))),
% 0.14/0.43 inference(resolution,[status(thm)],[f72,f77])).
% 0.14/0.43 fof(f118,definition,(
% 0.14/0.43 ![X0]: (sQ4_spl <=> (~ssIm(X0)|~ssBk(key(X0,a))))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f119,plain,(
% 0.14/0.43 ![X0]: (~ssIm(X0)|~ssBk(key(X0,a))|~sQ4_spl)),
% 0.14/0.43 inference(component_clause,[status(thm)],[f118])).
% 0.14/0.43 fof(f121,plain,(
% 0.14/0.43 sQ4_spl|~sQ0_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f116,f118,f95])).
% 0.14/0.43 fof(f122,definition,(
% 0.14/0.43 ![X0,X2]: (sQ5_spl <=> (~ssIm(X0)|~ssIm(X2)|ssIm(encr(X2,X0))))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f123,plain,(
% 0.14/0.43 ![X0,X1]: (~ssIm(X0)|~ssIm(X1)|ssIm(encr(X1,X0))|~sQ5_spl)),
% 0.14/0.43 inference(component_clause,[status(thm)],[f122])).
% 0.14/0.43 fof(f125,plain,(
% 0.14/0.43 sQ5_spl|sQ2_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f117,f122,f102])).
% 0.14/0.43 fof(f151,plain,(
% 0.14/0.43 ![X0]: (~ssM(sent(X0,b,pair(X0,na)))|ssSb(pair(X0,na)))),
% 0.14/0.43 inference(resolution,[status(thm)],[f78,f40])).
% 0.14/0.43 fof(f152,plain,(
% 0.14/0.43 ssSb(pair(a,na))),
% 0.14/0.43 inference(resolution,[status(thm)],[f151,f55])).
% 0.14/0.43 fof(f167,plain,(
% 0.14/0.43 ![X0,X1]: (~ssM(sent(X0,b,pair(X0,X1)))|~ssBf(X1)|ssIm(triple(b,nb(X1),encr(triple(X0,X1,tb(X1)),bt))))),
% 0.14/0.43 inference(resolution,[status(thm)],[f82,f63])).
% 0.14/0.43 fof(f168,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~ssSb(pair(X0,X1))|ssBk(key(X2,X0))|~ssIm(pair(encr(triple(X0,X2,tb(X1)),bt),encr(nb(X1),X2)))|~ssP(X0)|~ssP(b))),
% 0.14/0.43 inference(resolution,[status(thm)],[f84,f74])).
% 0.14/0.43 fof(f169,definition,(
% 0.14/0.43 ![X0,X1,X2]: (sQ10_spl <=> (~ssSb(pair(X0,X1))|ssBk(key(X2,X0))|~ssIm(pair(encr(triple(X0,X2,tb(X1)),bt),encr(nb(X1),X2)))|~ssP(X0)))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f170,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~ssSb(pair(X0,X1))|ssBk(key(X2,X0))|~ssIm(pair(encr(triple(X0,X2,tb(X1)),bt),encr(nb(X1),X2)))|~ssP(X0)|~sQ10_spl)),
% 0.14/0.43 inference(component_clause,[status(thm)],[f169])).
% 0.14/0.43 fof(f172,plain,(
% 0.14/0.43 sQ10_spl|~sQ0_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f168,f169,f95])).
% 0.14/0.43 fof(f181,definition,(
% 0.14/0.43 sQ13_spl <=> (ssP(a))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f183,plain,(
% 0.14/0.43 ~ssP(a)|sQ13_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f181])).
% 0.14/0.43 fof(f185,plain,(
% 0.14/0.43 $false|sQ13_spl),
% 0.14/0.43 inference(forward_subsumption_resolution,[status(thm)],[f183,f42])).
% 0.14/0.43 fof(f186,plain,(
% 0.14/0.43 sQ13_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f185])).
% 0.14/0.43 fof(f233,plain,(
% 0.14/0.43 ![X0]: (~ssM(sent(X0,b,pair(X0,na)))|ssIm(triple(b,nb(na),encr(triple(X0,na,tb(na)),bt))))),
% 0.14/0.43 inference(resolution,[status(thm)],[f167,f40])).
% 0.14/0.43 fof(f254,definition,(
% 0.14/0.43 sQ20_spl <=> (ssIm(na))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f256,plain,(
% 0.14/0.43 ~ssIm(na)|sQ20_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f254])).
% 0.14/0.43 fof(f258,plain,(
% 0.14/0.43 $false|sQ20_spl),
% 0.14/0.43 inference(forward_subsumption_resolution,[status(thm)],[f256,f91])).
% 0.14/0.43 fof(f259,plain,(
% 0.14/0.43 sQ20_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f258])).
% 0.14/0.43 fof(f262,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~ssSb(pair(X0,X1))|ssBk(key(X2,X0))|~ssP(X0)|~ssIm(encr(triple(X0,X2,tb(X1)),bt))|~ssIm(encr(nb(X1),X2))|~sQ10_spl)),
% 0.14/0.43 inference(resolution,[status(thm)],[f170,f73])).
% 0.14/0.43 fof(f271,plain,(
% 0.14/0.43 ssIm(triple(b,nb(na),encr(triple(a,na,tb(na)),bt)))),
% 0.14/0.43 inference(resolution,[status(thm)],[f233,f55])).
% 0.14/0.43 fof(f278,plain,(
% 0.14/0.43 ssIm(encr(triple(a,na,tb(na)),bt))),
% 0.14/0.43 inference(resolution,[status(thm)],[f271,f57])).
% 0.14/0.43 fof(f279,plain,(
% 0.14/0.43 ssIm(nb(na))),
% 0.14/0.43 inference(resolution,[status(thm)],[f271,f59])).
% 0.14/0.43 fof(f281,plain,(
% 0.14/0.43 ![X0]: (ssBk(key(X0,a))|~ssP(a)|~ssIm(encr(triple(a,X0,tb(na)),bt))|~ssIm(encr(nb(na),X0))|~sQ10_spl)),
% 0.14/0.43 inference(resolution,[status(thm)],[f262,f152])).
% 0.14/0.43 fof(f283,definition,(
% 0.14/0.43 ![X0]: (sQ23_spl <=> (ssBk(key(X0,a))|~ssIm(encr(triple(a,X0,tb(na)),bt))|~ssIm(encr(nb(na),X0))))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f284,plain,(
% 0.14/0.43 ![X0]: (ssBk(key(X0,a))|~ssIm(encr(triple(a,X0,tb(na)),bt))|~ssIm(encr(nb(na),X0))|~sQ23_spl)),
% 0.14/0.43 inference(component_clause,[status(thm)],[f283])).
% 0.14/0.43 fof(f286,plain,(
% 0.14/0.43 sQ23_spl|~sQ13_spl|~sQ10_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f281,f283,f181,f169])).
% 0.14/0.43 fof(f293,plain,(
% 0.14/0.43 ssBk(key(na,a))|~ssIm(encr(nb(na),na))|~sQ23_spl),
% 0.14/0.43 inference(resolution,[status(thm)],[f284,f278])).
% 0.14/0.43 fof(f296,definition,(
% 0.14/0.43 sQ25_spl <=> (ssBk(key(na,a)))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f297,plain,(
% 0.14/0.43 ssBk(key(na,a))|~sQ25_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f296])).
% 0.14/0.43 fof(f299,definition,(
% 0.14/0.43 sQ26_spl <=> (ssIm(encr(nb(na),na)))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f301,plain,(
% 0.14/0.43 ~ssIm(encr(nb(na),na))|sQ26_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f299])).
% 0.14/0.43 fof(f302,plain,(
% 0.14/0.43 sQ25_spl|~sQ26_spl|~sQ23_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f293,f296,f299,f283])).
% 0.14/0.43 fof(f314,plain,(
% 0.14/0.43 ~ssIm(na)|~sQ25_spl|~sQ4_spl),
% 0.14/0.43 inference(resolution,[status(thm)],[f297,f119])).
% 0.14/0.43 fof(f315,plain,(
% 0.14/0.43 ~sQ20_spl|~sQ25_spl|~sQ4_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f314,f254,f296,f118])).
% 0.14/0.43 fof(f317,plain,(
% 0.14/0.43 ~ssIm(na)|~ssIm(nb(na))|sQ26_spl|~sQ5_spl),
% 0.14/0.43 inference(resolution,[status(thm)],[f301,f123])).
% 0.14/0.43 fof(f318,definition,(
% 0.14/0.43 sQ30_spl <=> (ssIm(nb(na)))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f320,plain,(
% 0.14/0.43 ~ssIm(nb(na))|sQ30_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f318])).
% 0.14/0.43 fof(f325,plain,(
% 0.14/0.43 ~sQ20_spl|~sQ30_spl|sQ26_spl|~sQ5_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f317,f254,f318,f299,f122])).
% 0.14/0.43 fof(f326,plain,(
% 0.14/0.43 $false|sQ30_spl),
% 0.14/0.43 inference(forward_subsumption_resolution,[status(thm)],[f320,f279])).
% 0.14/0.43 fof(f327,plain,(
% 0.14/0.43 sQ30_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f326])).
% 0.14/0.43 fof(f328,plain,(
% 0.14/0.43 $false),
% 0.14/0.43 inference(sat_refutation,[status(thm)],[f111,f115,f121,f125,f172,f186,f259,f286,f302,f315,f325,f327])).
% 0.14/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.45 % Elapsed time: 0.074079 seconds
% 0.14/0.45 % CPU time: 0.371217 seconds
% 0.14/0.45 % Total memory used: 52.158 MB
% 0.14/0.45 % Net memory used: 51.458 MB
%------------------------------------------------------------------------------