%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM283-1.005 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:42:28 PM UTC 2026
% Result : Unsatisfiable 0.18s 5.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM283-1.005 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/5.40 % Computer : n002.cluster.edu
% 0.14/5.40 % Model : x86_64 x86_64
% 0.14/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.40 % Memory : 8046.5625MB
% 0.14/5.40 % OS : Linux 6.8.0-71-generic
% 0.14/5.40 % CPULimit : 300
% 0.14/5.41 % WCLimit : 300
% 0.14/5.41 % DateTime : Mon Sep 21 02:22:53 UTC 2026
% 0.14/5.41 % CPUTime :
% 0.14/5.42 % Drodi V4.1.1
% 0.18/5.58 % Refutation found
% 0.18/5.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.18/5.58 % SZS output start CNFRefutation for theBenchmark
% 0.18/5.58 fof(f1,axiom,(
% 0.18/5.58 (![X]: (sum(X,n0,X) ))),
% 0.18/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.58 fof(f2,axiom,(
% 0.18/5.58 (![X,Y,Z]: (( ~ sum(X,Y,Z)| sum(X,s(Y),s(Z)) ) ))),
% 0.18/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.58 fof(f3,axiom,(
% 0.18/5.58 (![X]: (product(s(n0),X,X) ))),
% 0.18/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.58 fof(f4,axiom,(
% 0.18/5.58 (![R,Y,Z,X]: (( ~ sum(R,Y,Z)| ~ product(X,Y,R)| product(s(X),Y,Z) ) ))),
% 0.18/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.58 fof(f5,axiom,(
% 0.18/5.58 factorial(n0,s(n0)) ),
% 0.18/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.58 fof(f6,axiom,(
% 0.18/5.58 (![X,Z,Y]: (( ~ factorial(X,Z)| ~ product(s(X),Z,Y)| factorial(s(X),Y) ) ))),
% 0.18/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.58 fof(f7,negated_conjecture,(
% 0.18/5.58 (![Result]: (~ factorial(s(s(s(s(s(n0))))),Result) ))),
% 0.18/5.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.58 fof(f8,plain,(
% 0.18/5.58 ![X0]: (sum(X0,n0,X0))),
% 0.18/5.58 inference(cnf_transformation,[status(thm)],[f1])).
% 0.18/5.58 fof(f9,plain,(
% 0.18/5.58 ![X0,X1,X2]: (~sum(X0,X1,X2)|sum(X0,s(X1),s(X2)))),
% 0.18/5.58 inference(cnf_transformation,[status(thm)],[f2])).
% 0.18/5.58 fof(f10,plain,(
% 0.18/5.58 ![X0]: (product(s(n0),X0,X0))),
% 0.18/5.58 inference(cnf_transformation,[status(thm)],[f3])).
% 0.18/5.58 fof(f11,plain,(
% 0.18/5.58 ![Y,Z,X]: ((![R]: (~sum(R,Y,Z)|~product(X,Y,R)))|product(s(X),Y,Z))),
% 0.18/5.58 inference(miniscoping,[status(thm)],[f4])).
% 0.18/5.58 fof(f12,plain,(
% 0.18/5.58 ![X0,X1,X2,X3]: (~sum(X0,X1,X2)|~product(X3,X1,X0)|product(s(X3),X1,X2))),
% 0.18/5.58 inference(cnf_transformation,[status(thm)],[f11])).
% 0.18/5.58 fof(f13,plain,(
% 0.18/5.58 factorial(n0,s(n0))),
% 0.18/5.58 inference(cnf_transformation,[status(thm)],[f5])).
% 0.18/5.58 fof(f14,plain,(
% 0.18/5.58 ![X,Y]: ((![Z]: (~factorial(X,Z)|~product(s(X),Z,Y)))|factorial(s(X),Y))),
% 0.18/5.58 inference(miniscoping,[status(thm)],[f6])).
% 0.18/5.58 fof(f15,plain,(
% 0.18/5.58 ![X0,X1,X2]: (~factorial(X0,X1)|~product(s(X0),X1,X2)|factorial(s(X0),X2))),
% 0.18/5.58 inference(cnf_transformation,[status(thm)],[f14])).
% 0.18/5.58 fof(f16,plain,(
% 0.18/5.58 ![X0]: (~factorial(s(s(s(s(s(n0))))),X0))),
% 0.18/5.58 inference(cnf_transformation,[status(thm)],[f7])).
% 0.18/5.58 fof(f17,plain,(
% 0.18/5.58 ![X0]: (~product(s(n0),s(n0),X0)|factorial(s(n0),X0))),
% 0.18/5.58 inference(resolution,[status(thm)],[f15,f13])).
% 0.18/5.58 fof(f18,plain,(
% 0.18/5.58 factorial(s(n0),s(n0))),
% 0.18/5.58 inference(resolution,[status(thm)],[f10,f17])).
% 0.18/5.58 fof(f19,plain,(
% 0.18/5.58 ![X0]: (~product(s(s(n0)),s(n0),X0)|factorial(s(s(n0)),X0))),
% 0.18/5.58 inference(resolution,[status(thm)],[f18,f15])).
% 0.18/5.58 fof(f20,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(n0),s(X0)))),
% 0.18/5.58 inference(resolution,[status(thm)],[f9,f8])).
% 0.18/5.58 fof(f21,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(n0)),s(s(X0))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f20,f9])).
% 0.18/5.58 fof(f22,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(n0))),s(s(s(X0)))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f21,f9])).
% 0.18/5.58 fof(f23,plain,(
% 0.18/5.58 ![X0,X1]: (~product(X0,s(s(n0)),X1)|product(s(X0),s(s(n0)),s(s(X1))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f12,f21])).
% 0.18/5.58 fof(f24,plain,(
% 0.18/5.58 ![X0,X1]: (~product(X0,s(n0),X1)|product(s(X0),s(n0),s(X1)))),
% 0.18/5.58 inference(resolution,[status(thm)],[f12,f20])).
% 0.18/5.58 fof(f31,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(n0)))),s(s(s(s(X0))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f22,f9])).
% 0.18/5.58 fof(f33,plain,(
% 0.18/5.58 ![X0]: (~product(s(n0),s(n0),X0)|factorial(s(s(n0)),s(X0)))),
% 0.18/5.58 inference(resolution,[status(thm)],[f24,f19])).
% 0.18/5.58 fof(f36,plain,(
% 0.18/5.58 factorial(s(s(n0)),s(s(n0)))),
% 0.18/5.58 inference(resolution,[status(thm)],[f33,f10])).
% 0.18/5.58 fof(f38,plain,(
% 0.18/5.58 ![X0]: (~product(s(s(s(n0))),s(s(n0)),X0)|factorial(s(s(s(n0))),X0))),
% 0.18/5.58 inference(resolution,[status(thm)],[f36,f15])).
% 0.18/5.58 fof(f41,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(n0))))),s(s(s(s(s(X0)))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f31,f9])).
% 0.18/5.58 fof(f45,plain,(
% 0.18/5.58 product(s(s(n0)),s(s(n0)),s(s(s(s(n0)))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f23,f10])).
% 0.18/5.58 fof(f46,plain,(
% 0.18/5.58 product(s(s(s(n0))),s(s(n0)),s(s(s(s(s(s(n0)))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f45,f23])).
% 0.18/5.58 fof(f48,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(X0))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f41,f9])).
% 0.18/5.58 fof(f67,plain,(
% 0.18/5.58 factorial(s(s(s(n0))),s(s(s(s(s(s(n0)))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f46,f38])).
% 0.18/5.58 fof(f69,plain,(
% 0.18/5.58 ![X0]: (~product(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))),X0)|factorial(s(s(s(s(n0)))),X0))),
% 0.18/5.58 inference(resolution,[status(thm)],[f67,f15])).
% 0.18/5.58 fof(f70,plain,(
% 0.18/5.58 ![X0,X1]: (~product(X0,s(s(s(s(s(s(n0)))))),X1)|product(s(X0),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(X1))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f48,f12])).
% 0.18/5.58 fof(f71,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(X0)))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f48,f9])).
% 0.18/5.58 fof(f114,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(X0))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f71,f9])).
% 0.18/5.58 fof(f119,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(s(s(s(X0)))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f114,f9])).
% 0.18/5.58 fof(f140,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(s(X0))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f119,f9])).
% 0.18/5.58 fof(f145,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(n0))))))))))),s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f140,f9])).
% 0.18/5.58 fof(f149,plain,(
% 0.18/5.58 ![X0]: (~product(s(s(s(n0))),s(s(s(s(s(s(n0)))))),X0)|factorial(s(s(s(s(n0)))),s(s(s(s(s(s(X0))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f70,f69])).
% 0.18/5.58 fof(f167,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f145,f9])).
% 0.18/5.58 fof(f194,plain,(
% 0.18/5.58 ![X0,X1]: (~product(s(s(s(n0))),s(s(s(s(s(s(n0)))))),X0)|~product(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0)))))),X1)|factorial(s(s(s(s(s(n0))))),X1))),
% 0.18/5.58 inference(resolution,[status(thm)],[f149,f15])).
% 0.18/5.58 fof(f195,plain,(
% 0.18/5.58 ![X0,X1]: (~product(s(s(s(n0))),s(s(s(s(s(s(n0)))))),X0)|~product(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0)))))),X1))),
% 0.18/5.58 inference(forward_subsumption_resolution,[status(thm)],[f194,f16])).
% 0.18/5.58 fof(f228,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f167,f9])).
% 0.18/5.58 fof(f232,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f228,f9])).
% 0.18/5.58 fof(f267,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f232,f9])).
% 0.18/5.58 fof(f272,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f267,f9])).
% 0.18/5.58 fof(f335,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f272,f9])).
% 0.18/5.58 fof(f371,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f335,f9])).
% 0.18/5.58 fof(f376,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f371,f9])).
% 0.18/5.58 fof(f380,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f376,f9])).
% 0.18/5.58 fof(f417,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f380,f9])).
% 0.18/5.58 fof(f422,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f417,f9])).
% 0.18/5.58 fof(f457,plain,(
% 0.18/5.58 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))))),
% 0.18/5.58 inference(resolution,[status(thm)],[f422,f9])).
% 0.18/5.59 fof(f462,plain,(
% 0.18/5.59 ![X0]: (sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))))))),
% 0.18/5.59 inference(resolution,[status(thm)],[f457,f9])).
% 0.18/5.59 fof(f558,plain,(
% 0.18/5.59 ![X0,X1]: (~product(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1)|product(s(X0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))),
% 0.18/5.59 inference(resolution,[status(thm)],[f462,f12])).
% 0.18/5.59 fof(f780,plain,(
% 0.18/5.59 ![X0]: (~product(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)|~product(s(s(s(n0))),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))),
% 0.18/5.59 inference(resolution,[status(thm)],[f558,f195])).
% 0.18/5.59 fof(f783,definition,(
% 0.18/5.59 ![X0]: (sQ104_spl <=> (~product(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)))),
% 0.18/5.59 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.18/5.59 fof(f784,plain,(
% 0.18/5.59 ![X0]: (~product(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)|~sQ104_spl)),
% 0.18/5.59 inference(component_clause,[status(thm)],[f783])).
% 0.18/5.59 fof(f786,definition,(
% 0.18/5.59 sQ105_spl <=> (product(s(s(s(n0))),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))),
% 0.18/5.59 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.18/5.59 fof(f788,plain,(
% 0.18/5.59 ~product(s(s(s(n0))),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))|sQ105_spl),
% 0.18/5.59 inference(component_clause,[status(thm)],[f786])).
% 0.18/5.59 fof(f789,plain,(
% 0.18/5.59 sQ104_spl|~sQ105_spl),
% 0.18/5.59 inference(split_clause,[status(thm)],[f780,f783,f786])).
% 0.18/5.59 fof(f808,plain,(
% 0.18/5.59 ![X0]: (~product(s(s(s(n0))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)|~sQ104_spl)),
% 0.18/5.59 inference(resolution,[status(thm)],[f784,f558])).
% 0.18/5.59 fof(f816,plain,(
% 0.18/5.59 ![X0]: (~product(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)|~sQ104_spl)),
% 0.18/5.59 inference(resolution,[status(thm)],[f808,f558])).
% 0.18/5.59 fof(f817,plain,(
% 0.18/5.59 ![X0]: (~product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)|~sQ104_spl)),
% 0.18/5.59 inference(resolution,[status(thm)],[f816,f558])).
% 0.18/5.59 fof(f818,plain,(
% 0.18/5.59 $false|~sQ104_spl),
% 0.18/5.59 inference(resolution,[status(thm)],[f817,f10])).
% 0.18/5.59 fof(f820,plain,(
% 0.18/5.59 ~sQ104_spl),
% 0.18/5.59 inference(contradiction_clause,[status(thm)],[f818])).
% 0.18/5.59 fof(f821,plain,(
% 0.18/5.59 ~product(s(s(n0)),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))|sQ105_spl),
% 0.18/5.59 inference(resolution,[status(thm)],[f788,f70])).
% 0.18/5.59 fof(f822,plain,(
% 0.18/5.59 ~product(s(n0),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(n0)))))))|sQ105_spl),
% 0.18/5.59 inference(resolution,[status(thm)],[f821,f70])).
% 0.18/5.59 fof(f823,plain,(
% 0.18/5.59 $false|sQ105_spl),
% 0.18/5.59 inference(forward_subsumption_resolution,[status(thm)],[f822,f10])).
% 0.18/5.59 fof(f824,plain,(
% 0.18/5.59 sQ105_spl),
% 0.18/5.59 inference(contradiction_clause,[status(thm)],[f823])).
% 0.18/5.59 fof(f825,plain,(
% 0.18/5.59 $false),
% 0.18/5.59 inference(sat_refutation,[status(thm)],[f789,f820,f824])).
% 0.18/5.59 % SZS output end CNFRefutation for theBenchmark.p
% 1.56/6.81 % Elapsed time: 1.186736 seconds
% 1.56/6.81 % CPU time: 1.165216 seconds
% 1.56/6.81 % Total memory used: 67.340 MB
% 1.56/6.81 % Net memory used: 66.250 MB
%------------------------------------------------------------------------------