%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ056-2.005 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 02:00:24 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ056-2.005 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 03:51:20 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.60 % Refutation found
% 0.10/0.60 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.60 fof(f1,axiom,(
% 0.10/0.60 (![I,T1,T2,T3,T4,J]: (( ~ p(I,T1,T2,T3,T4)| p(J,T1,T2,T3,T4) ) ))),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f2,axiom,(
% 0.10/0.60 (![T0,I,T2,T3,T4,J]: (( ~ p(T0,I,T2,T3,T4)| ~ neq(T0,I)| ~ neq(T0,J)| p(T0,J,T2,T3,T4) ) ))),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f3,axiom,(
% 0.10/0.60 (![T0,T1,I,T3,T4,J]: (( ~ p(T0,T1,I,T3,T4)| ~ neq(T0,I)| ~ neq(T0,J)| ~ neq(T1,I)| ~ neq(T1,J)| p(T0,T1,J,T3,T4) ) ))),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f4,axiom,(
% 0.10/0.60 (![T0,T1,T2,I,T4,J]: (( ~ p(T0,T1,T2,I,T4)| ~ neq(T0,I)| ~ neq(T0,J)| ~ neq(T1,I)| ~ neq(T1,J)| ~ neq(T2,I)| ~ neq(T2,J)| p(T0,T1,T2,J,T4) ) ))),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f5,axiom,(
% 0.10/0.60 (![T0,T1,T2,T3,I,J]: (( ~ p(T0,T1,T2,T3,I)| ~ neq(T0,I)| ~ neq(T0,J)| ~ neq(T1,I)| ~ neq(T1,J)| ~ neq(T2,I)| ~ neq(T2,J)| ~ neq(T3,I)| ~ neq(T3,J)| p(T0,T1,T2,T3,J) ) ))),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f7,axiom,(
% 0.10/0.60 neq(s0,s1) ),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f8,axiom,(
% 0.10/0.60 neq(s0,s2) ),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f9,axiom,(
% 0.10/0.60 neq(s1,s0) ),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f11,axiom,(
% 0.10/0.60 neq(s1,s2) ),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f12,axiom,(
% 0.10/0.60 neq(s2,s0) ),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f13,axiom,(
% 0.10/0.60 neq(s2,s1) ),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f15,axiom,(
% 0.10/0.60 p(s0,s0,s0,s0,s0) ),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f16,negated_conjecture,(
% 0.10/0.60 ~ p(s2,s2,s2,s2,s2) ),
% 0.10/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.60 fof(f17,plain,(
% 0.10/0.60 ![T1,T2,T3,T4]: ((![I]: ~p(I,T1,T2,T3,T4))|(![J]: p(J,T1,T2,T3,T4)))),
% 0.10/0.60 inference(miniscoping,[status(thm)],[f1])).
% 0.10/0.60 fof(f18,plain,(
% 0.10/0.60 ![X0,X1,X2,X3,X4,X5]: (~p(X0,X1,X2,X3,X4)|p(X5,X1,X2,X3,X4))),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f17])).
% 0.10/0.60 fof(f19,plain,(
% 0.10/0.60 ![T0,T2,T3,T4,J]: (((![I]: (~p(T0,I,T2,T3,T4)|~neq(T0,I)))|~neq(T0,J))|p(T0,J,T2,T3,T4))),
% 0.10/0.60 inference(miniscoping,[status(thm)],[f2])).
% 0.10/0.60 fof(f20,plain,(
% 0.10/0.60 ![X0,X1,X2,X3,X4,X5]: (~p(X0,X1,X2,X3,X4)|~neq(X0,X1)|~neq(X0,X5)|p(X0,X5,X2,X3,X4))),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f19])).
% 0.10/0.60 fof(f21,plain,(
% 0.10/0.60 ![T0,T1,T3,T4,J]: (((![I]: (((~p(T0,T1,I,T3,T4)|~neq(T0,I))|~neq(T0,J))|~neq(T1,I)))|~neq(T1,J))|p(T0,T1,J,T3,T4))),
% 0.10/0.60 inference(miniscoping,[status(thm)],[f3])).
% 0.10/0.60 fof(f22,plain,(
% 0.10/0.60 ![X0,X1,X2,X3,X4,X5]: (~p(X0,X1,X2,X3,X4)|~neq(X0,X2)|~neq(X0,X5)|~neq(X1,X2)|~neq(X1,X5)|p(X0,X1,X5,X3,X4))),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f21])).
% 0.10/0.60 fof(f23,plain,(
% 0.10/0.60 ![T0,T1,T2,T4,J]: (((![I]: (((((~p(T0,T1,T2,I,T4)|~neq(T0,I))|~neq(T0,J))|~neq(T1,I))|~neq(T1,J))|~neq(T2,I)))|~neq(T2,J))|p(T0,T1,T2,J,T4))),
% 0.10/0.60 inference(miniscoping,[status(thm)],[f4])).
% 0.10/0.60 fof(f24,plain,(
% 0.10/0.60 ![X0,X1,X2,X3,X4,X5]: (~p(X0,X1,X2,X3,X4)|~neq(X0,X3)|~neq(X0,X5)|~neq(X1,X3)|~neq(X1,X5)|~neq(X2,X3)|~neq(X2,X5)|p(X0,X1,X2,X5,X4))),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f23])).
% 0.10/0.60 fof(f25,plain,(
% 0.10/0.60 ![T0,T1,T2,T3,J]: (((![I]: (((((((~p(T0,T1,T2,T3,I)|~neq(T0,I))|~neq(T0,J))|~neq(T1,I))|~neq(T1,J))|~neq(T2,I))|~neq(T2,J))|~neq(T3,I)))|~neq(T3,J))|p(T0,T1,T2,T3,J))),
% 0.10/0.60 inference(miniscoping,[status(thm)],[f5])).
% 0.10/0.60 fof(f26,plain,(
% 0.10/0.60 ![X0,X1,X2,X3,X4,X5]: (~p(X0,X1,X2,X3,X4)|~neq(X0,X4)|~neq(X0,X5)|~neq(X1,X4)|~neq(X1,X5)|~neq(X2,X4)|~neq(X2,X5)|~neq(X3,X4)|~neq(X3,X5)|p(X0,X1,X2,X3,X5))),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f25])).
% 0.10/0.60 fof(f28,plain,(
% 0.10/0.60 neq(s0,s1)),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.60 fof(f29,plain,(
% 0.10/0.60 neq(s0,s2)),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.60 fof(f30,plain,(
% 0.10/0.60 neq(s1,s0)),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/0.60 fof(f32,plain,(
% 0.10/0.60 neq(s1,s2)),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f11])).
% 0.10/0.60 fof(f33,plain,(
% 0.10/0.60 neq(s2,s0)),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f12])).
% 0.10/0.60 fof(f34,plain,(
% 0.10/0.60 neq(s2,s1)),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f13])).
% 0.10/0.60 fof(f36,plain,(
% 0.10/0.60 p(s0,s0,s0,s0,s0)),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.60 fof(f37,plain,(
% 0.10/0.60 ~p(s2,s2,s2,s2,s2)),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f16])).
% 0.10/0.60 fof(f38,plain,(
% 0.10/0.60 ![X0,X1,X2,X3]: (~p(s0,X0,X1,X2,X3)|~neq(s0,X0)|p(s0,s1,X1,X2,X3))),
% 0.10/0.60 inference(resolution,[status(thm)],[f28,f20])).
% 0.10/0.60 fof(f39,plain,(
% 0.10/0.60 ![X0,X1,X2,X3]: (~p(s0,X0,X1,X2,X3)|~neq(s0,X0)|p(s0,s2,X1,X2,X3))),
% 0.10/0.60 inference(resolution,[status(thm)],[f29,f20])).
% 0.10/0.60 fof(f40,plain,(
% 0.10/0.60 ![X0,X1,X2,X3]: (~p(s1,X0,X1,X2,X3)|~neq(s1,X0)|p(s1,s0,X1,X2,X3))),
% 0.10/0.60 inference(resolution,[status(thm)],[f30,f20])).
% 0.10/0.60 fof(f42,plain,(
% 0.10/0.60 ![X0,X1,X2,X3]: (~p(s2,X0,X1,X2,X3)|~neq(s2,X0)|p(s2,s0,X1,X2,X3))),
% 0.10/0.60 inference(resolution,[status(thm)],[f33,f20])).
% 0.10/0.60 fof(f43,plain,(
% 0.10/0.60 ![X0,X1,X2,X3]: (~p(s2,X0,X1,X2,X3)|~neq(s2,X0)|p(s2,s1,X1,X2,X3))),
% 0.10/0.60 inference(resolution,[status(thm)],[f34,f20])).
% 0.10/0.60 fof(f47,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s2,s2,s2,s2))),
% 0.10/0.60 inference(resolution,[status(thm)],[f37,f18])).
% 0.10/0.60 fof(f63,plain,(
% 0.10/0.60 ![X0]: (~p(s0,X0,s2,s2,s2)|~neq(s0,X0))),
% 0.10/0.60 inference(resolution,[status(thm)],[f47,f39])).
% 0.10/0.60 fof(f82,plain,(
% 0.10/0.60 ~p(s0,s1,s2,s2,s2)),
% 0.10/0.60 inference(resolution,[status(thm)],[f63,f28])).
% 0.10/0.60 fof(f87,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s1,s2,s2,s2))),
% 0.10/0.60 inference(resolution,[status(thm)],[f82,f18])).
% 0.10/0.60 fof(f91,definition,(
% 0.10/0.60 sQ8_spl <=> (neq(s0,s2))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f93,plain,(
% 0.10/0.60 ~neq(s0,s2)|sQ8_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f91])).
% 0.10/0.60 fof(f94,definition,(
% 0.10/0.60 sQ9_spl <=> (neq(s1,s2))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f96,plain,(
% 0.10/0.60 ~neq(s1,s2)|sQ9_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f94])).
% 0.10/0.60 fof(f106,plain,(
% 0.10/0.60 $false|sQ9_spl),
% 0.10/0.60 inference(forward_subsumption_resolution,[status(thm)],[f96,f32])).
% 0.10/0.60 fof(f107,plain,(
% 0.10/0.60 sQ9_spl),
% 0.10/0.60 inference(contradiction_clause,[status(thm)],[f106])).
% 0.10/0.60 fof(f108,plain,(
% 0.10/0.60 $false|sQ8_spl),
% 0.10/0.60 inference(forward_subsumption_resolution,[status(thm)],[f93,f29])).
% 0.10/0.60 fof(f109,plain,(
% 0.10/0.60 sQ8_spl),
% 0.10/0.60 inference(contradiction_clause,[status(thm)],[f108])).
% 0.10/0.60 fof(f133,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s1,X1,s2,s2)|~neq(X0,X1)|~neq(X0,s2)|~neq(s1,X1)|~neq(s1,s2))),
% 0.10/0.60 inference(resolution,[status(thm)],[f87,f22])).
% 0.10/0.60 fof(f143,definition,(
% 0.10/0.60 ![X0,X1]: (sQ17_spl <=> (~p(X0,s1,X1,s2,s2)|~neq(X0,X1)|~neq(X0,s2)|~neq(s1,X1)))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f144,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s1,X1,s2,s2)|~neq(X0,X1)|~neq(X0,s2)|~neq(s1,X1)|~sQ17_spl)),
% 0.10/0.60 inference(component_clause,[status(thm)],[f143])).
% 0.10/0.60 fof(f146,plain,(
% 0.10/0.60 sQ17_spl|~sQ9_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f133,f143,f94])).
% 0.10/0.60 fof(f153,definition,(
% 0.10/0.60 sQ19_spl <=> (p(s0,s1,s0,s2,s2))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f154,plain,(
% 0.10/0.60 p(s0,s1,s0,s2,s2)|~sQ19_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f153])).
% 0.10/0.60 fof(f155,plain,(
% 0.10/0.60 ~p(s0,s1,s0,s2,s2)|sQ19_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f153])).
% 0.10/0.60 fof(f182,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s1,s0,s2,s2)|sQ19_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f155,f18])).
% 0.10/0.60 fof(f191,definition,(
% 0.10/0.60 sQ26_spl <=> (neq(s1,s0))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f193,plain,(
% 0.10/0.60 ~neq(s1,s0)|sQ26_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f191])).
% 0.10/0.60 fof(f209,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s1,s0,s2,s2)|~neq(X0,s0)|~neq(X0,s2)|~sQ17_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f144,f30])).
% 0.10/0.60 fof(f214,plain,(
% 0.10/0.60 ~p(s1,s1,s0,s2,s2)|~neq(s1,s0)|~sQ17_spl),
% 0.10/0.60 inference(resolution,[status(thm)],[f209,f32])).
% 0.10/0.60 fof(f216,definition,(
% 0.10/0.60 sQ29_spl <=> (p(s1,s1,s0,s2,s2))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f218,plain,(
% 0.10/0.60 ~p(s1,s1,s0,s2,s2)|sQ29_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f216])).
% 0.10/0.60 fof(f219,plain,(
% 0.10/0.60 ~sQ29_spl|~sQ26_spl|~sQ17_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f214,f216,f191,f143])).
% 0.10/0.60 fof(f221,plain,(
% 0.10/0.60 $false|sQ26_spl),
% 0.10/0.60 inference(forward_subsumption_resolution,[status(thm)],[f193,f30])).
% 0.10/0.60 fof(f222,plain,(
% 0.10/0.60 sQ26_spl),
% 0.10/0.60 inference(contradiction_clause,[status(thm)],[f221])).
% 0.10/0.60 fof(f240,plain,(
% 0.10/0.60 ![X0]: (~p(s2,X0,s0,s2,s2)|~neq(s2,X0)|sQ19_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f182,f43])).
% 0.10/0.60 fof(f277,definition,(
% 0.10/0.60 sQ39_spl <=> (neq(s0,s1))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f279,plain,(
% 0.10/0.60 ~neq(s0,s1)|sQ39_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f277])).
% 0.10/0.60 fof(f286,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s1,s0,s2,s2)|sQ29_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f218,f18])).
% 0.10/0.60 fof(f299,plain,(
% 0.10/0.60 $false|sQ29_spl|~sQ19_spl),
% 0.10/0.60 inference(backward_subsumption_resolution,[status(thm)],[f154,f286])).
% 0.10/0.60 fof(f300,plain,(
% 0.10/0.60 sQ29_spl|~sQ19_spl),
% 0.10/0.60 inference(contradiction_clause,[status(thm)],[f299])).
% 0.10/0.60 fof(f323,plain,(
% 0.10/0.60 $false|sQ39_spl),
% 0.10/0.60 inference(forward_subsumption_resolution,[status(thm)],[f279,f28])).
% 0.10/0.60 fof(f324,plain,(
% 0.10/0.60 sQ39_spl),
% 0.10/0.60 inference(contradiction_clause,[status(thm)],[f323])).
% 0.10/0.60 fof(f363,plain,(
% 0.10/0.60 ~p(s2,s0,s0,s2,s2)|sQ19_spl),
% 0.10/0.60 inference(resolution,[status(thm)],[f240,f33])).
% 0.10/0.60 fof(f380,definition,(
% 0.10/0.60 sQ53_spl <=> (neq(s2,s0))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f382,plain,(
% 0.10/0.60 ~neq(s2,s0)|sQ53_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f380])).
% 0.10/0.60 fof(f416,plain,(
% 0.10/0.60 $false|sQ53_spl),
% 0.10/0.60 inference(forward_subsumption_resolution,[status(thm)],[f382,f33])).
% 0.10/0.60 fof(f417,plain,(
% 0.10/0.60 sQ53_spl),
% 0.10/0.60 inference(contradiction_clause,[status(thm)],[f416])).
% 0.10/0.60 fof(f426,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s0,s0,s2,s2)|sQ19_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f363,f18])).
% 0.10/0.60 fof(f445,definition,(
% 0.10/0.60 sQ63_spl <=> (p(s0,s1,s0,s1,s2))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f446,plain,(
% 0.10/0.60 p(s0,s1,s0,s1,s2)|~sQ63_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f445])).
% 0.10/0.60 fof(f447,plain,(
% 0.10/0.60 ~p(s0,s1,s0,s1,s2)|sQ63_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f445])).
% 0.10/0.60 fof(f454,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s0,s0,X1,s2)|~neq(X0,X1)|~neq(X0,s2)|~neq(s0,X1)|~neq(s0,s2)|~neq(s0,X1)|~neq(s0,s2)|sQ19_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f426,f24])).
% 0.10/0.60 fof(f461,definition,(
% 0.10/0.60 ![X0,X1]: (sQ65_spl <=> (~p(X0,s0,s0,X1,s2)|~neq(X0,X1)|~neq(X0,s2)|~neq(s0,X1)|~neq(s0,X1)))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f462,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s0,s0,X1,s2)|~neq(X0,X1)|~neq(X0,s2)|~neq(s0,X1)|~neq(s0,X1)|~sQ65_spl)),
% 0.10/0.60 inference(component_clause,[status(thm)],[f461])).
% 0.10/0.60 fof(f464,plain,(
% 0.10/0.60 sQ65_spl|~sQ8_spl|sQ19_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f454,f461,f91,f153])).
% 0.10/0.60 fof(f469,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s0,s0,X1,s2)|~neq(X0,X1)|~neq(X0,s2)|~neq(s0,X1)|~sQ65_spl)),
% 0.10/0.60 inference(duplicate_literals_removal,[status(thm)],[f462])).
% 0.10/0.60 fof(f490,plain,(
% 0.10/0.60 ![X0]: (~p(s0,X0,s0,s1,s2)|~neq(s0,X0)|sQ63_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f447,f38])).
% 0.10/0.60 fof(f525,definition,(
% 0.10/0.60 sQ75_spl <=> (neq(s2,s1))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f527,plain,(
% 0.10/0.60 ~neq(s2,s1)|sQ75_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f525])).
% 0.10/0.60 fof(f552,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s0,s0,s1,s2)|~neq(X0,s1)|~neq(X0,s2)|~sQ65_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f469,f28])).
% 0.10/0.60 fof(f589,plain,(
% 0.10/0.60 $false|sQ75_spl),
% 0.10/0.60 inference(forward_subsumption_resolution,[status(thm)],[f527,f34])).
% 0.10/0.60 fof(f590,plain,(
% 0.10/0.60 sQ75_spl),
% 0.10/0.60 inference(contradiction_clause,[status(thm)],[f589])).
% 0.10/0.60 fof(f592,plain,(
% 0.10/0.60 ~p(s0,s0,s0,s1,s2)|~neq(s0,s2)|~sQ65_spl),
% 0.10/0.60 inference(resolution,[status(thm)],[f552,f28])).
% 0.10/0.60 fof(f597,definition,(
% 0.10/0.60 sQ86_spl <=> (p(s0,s0,s0,s1,s2))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f599,plain,(
% 0.10/0.60 ~p(s0,s0,s0,s1,s2)|sQ86_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f597])).
% 0.10/0.60 fof(f600,plain,(
% 0.10/0.60 ~sQ86_spl|~sQ8_spl|~sQ65_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f592,f597,f91,f461])).
% 0.10/0.60 fof(f606,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s0,s0,s1,s2)|sQ86_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f599,f18])).
% 0.10/0.60 fof(f627,plain,(
% 0.10/0.60 ![X0]: (~p(s2,X0,s0,s1,s2)|~neq(s2,X0)|sQ86_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f606,f42])).
% 0.10/0.60 fof(f656,plain,(
% 0.10/0.60 ~p(s2,s1,s0,s1,s2)|sQ86_spl),
% 0.10/0.60 inference(resolution,[status(thm)],[f627,f34])).
% 0.10/0.60 fof(f674,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s1,s0,s1,s2)|sQ86_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f656,f18])).
% 0.10/0.60 fof(f687,plain,(
% 0.10/0.60 $false|sQ86_spl|~sQ63_spl),
% 0.10/0.60 inference(backward_subsumption_resolution,[status(thm)],[f446,f674])).
% 0.10/0.60 fof(f688,plain,(
% 0.10/0.60 sQ86_spl|~sQ63_spl),
% 0.10/0.60 inference(contradiction_clause,[status(thm)],[f687])).
% 0.10/0.60 fof(f697,plain,(
% 0.10/0.60 ~p(s0,s2,s0,s1,s2)|sQ63_spl),
% 0.10/0.60 inference(resolution,[status(thm)],[f490,f29])).
% 0.10/0.60 fof(f722,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s2,s0,s1,s2)|sQ63_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f697,f18])).
% 0.10/0.60 fof(f747,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s2,X1,s1,s2)|~neq(X0,X1)|~neq(X0,s0)|~neq(s2,X1)|~neq(s2,s0)|sQ63_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f722,f22])).
% 0.10/0.60 fof(f757,definition,(
% 0.10/0.60 ![X0,X1]: (sQ109_spl <=> (~p(X0,s2,X1,s1,s2)|~neq(X0,X1)|~neq(X0,s0)|~neq(s2,X1)))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f758,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s2,X1,s1,s2)|~neq(X0,X1)|~neq(X0,s0)|~neq(s2,X1)|~sQ109_spl)),
% 0.10/0.60 inference(component_clause,[status(thm)],[f757])).
% 0.10/0.60 fof(f760,plain,(
% 0.10/0.60 sQ109_spl|~sQ53_spl|sQ63_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f747,f757,f380,f445])).
% 0.10/0.60 fof(f779,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s2,s1,s1,s2)|~neq(X0,s1)|~neq(X0,s0)|~sQ109_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f758,f34])).
% 0.10/0.60 fof(f841,plain,(
% 0.10/0.60 ~p(s2,s2,s1,s1,s2)|~neq(s2,s0)|~sQ109_spl),
% 0.10/0.60 inference(resolution,[status(thm)],[f779,f34])).
% 0.10/0.60 fof(f843,definition,(
% 0.10/0.60 sQ122_spl <=> (p(s2,s2,s1,s1,s2))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f845,plain,(
% 0.10/0.60 ~p(s2,s2,s1,s1,s2)|sQ122_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f843])).
% 0.10/0.60 fof(f846,plain,(
% 0.10/0.60 ~sQ122_spl|~sQ53_spl|~sQ109_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f841,f843,f380,f757])).
% 0.10/0.60 fof(f861,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s2,s1,s1,s2)|sQ122_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f845,f18])).
% 0.10/0.60 fof(f885,plain,(
% 0.10/0.60 ![X0]: (~p(s0,X0,s1,s1,s2)|~neq(s0,X0)|sQ122_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f861,f39])).
% 0.10/0.60 fof(f1024,plain,(
% 0.10/0.60 ~p(s0,s1,s1,s1,s2)|sQ122_spl),
% 0.10/0.60 inference(resolution,[status(thm)],[f885,f28])).
% 0.10/0.60 fof(f1096,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s1,s1,s1,s2)|sQ122_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f1024,f18])).
% 0.10/0.60 fof(f1109,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s1,s1,s1,X1)|~neq(X0,X1)|~neq(X0,s2)|~neq(s1,X1)|~neq(s1,s2)|~neq(s1,X1)|~neq(s1,s2)|~neq(s1,X1)|~neq(s1,s2)|sQ122_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f1096,f26])).
% 0.10/0.60 fof(f1113,definition,(
% 0.10/0.60 ![X0,X1]: (sQ163_spl <=> (~p(X0,s1,s1,s1,X1)|~neq(X0,X1)|~neq(X0,s2)|~neq(s1,X1)|~neq(s1,X1)|~neq(s1,X1)))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f1114,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s1,s1,s1,X1)|~neq(X0,X1)|~neq(X0,s2)|~neq(s1,X1)|~neq(s1,X1)|~neq(s1,X1)|~sQ163_spl)),
% 0.10/0.60 inference(component_clause,[status(thm)],[f1113])).
% 0.10/0.60 fof(f1116,plain,(
% 0.10/0.60 sQ163_spl|~sQ9_spl|sQ122_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f1109,f1113,f94,f843])).
% 0.10/0.60 fof(f1125,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s1,s1,s1,X1)|~neq(X0,X1)|~neq(X0,s2)|~neq(s1,X1)|~sQ163_spl)),
% 0.10/0.60 inference(duplicate_literals_removal,[status(thm)],[f1114])).
% 0.10/0.60 fof(f1251,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s1,s1,s1,s0)|~neq(X0,s0)|~neq(X0,s2)|~sQ163_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f1125,f30])).
% 0.10/0.60 fof(f1313,plain,(
% 0.10/0.60 ~p(s1,s1,s1,s1,s0)|~neq(s1,s0)|~sQ163_spl),
% 0.10/0.60 inference(resolution,[status(thm)],[f1251,f32])).
% 0.10/0.60 fof(f1315,definition,(
% 0.10/0.60 sQ194_spl <=> (p(s1,s1,s1,s1,s0))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f1317,plain,(
% 0.10/0.60 ~p(s1,s1,s1,s1,s0)|sQ194_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f1315])).
% 0.10/0.60 fof(f1318,plain,(
% 0.10/0.60 ~sQ194_spl|~sQ26_spl|~sQ163_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f1313,f1315,f191,f1113])).
% 0.10/0.60 fof(f1408,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s1,s1,s1,s0)|sQ194_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f1317,f18])).
% 0.10/0.60 fof(f1452,plain,(
% 0.10/0.60 ![X0]: (~p(s2,X0,s1,s1,s0)|~neq(s2,X0)|sQ194_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f1408,f43])).
% 0.10/0.60 fof(f1634,plain,(
% 0.10/0.60 ~p(s2,s0,s1,s1,s0)|sQ194_spl),
% 0.10/0.60 inference(resolution,[status(thm)],[f1452,f33])).
% 0.10/0.60 fof(f1708,plain,(
% 0.10/0.60 ![X0]: (~p(X0,s0,s1,s1,s0)|sQ194_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f1634,f18])).
% 0.10/0.60 fof(f1749,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s0,X1,s1,s0)|~neq(X0,X1)|~neq(X0,s1)|~neq(s0,X1)|~neq(s0,s1)|sQ194_spl)),
% 0.10/0.60 inference(resolution,[status(thm)],[f1708,f22])).
% 0.10/0.60 fof(f1759,definition,(
% 0.10/0.60 ![X0,X1]: (sQ262_spl <=> (~p(X0,s0,X1,s1,s0)|~neq(X0,X1)|~neq(X0,s1)|~neq(s0,X1)))),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f1760,plain,(
% 0.10/0.60 ![X0,X1]: (~p(X0,s0,X1,s1,s0)|~neq(X0,X1)|~neq(X0,s1)|~neq(s0,X1)|~sQ262_spl)),
% 0.10/0.60 inference(component_clause,[status(thm)],[f1759])).
% 0.10/0.60 fof(f1762,plain,(
% 0.10/0.60 sQ262_spl|~sQ39_spl|sQ194_spl),
% 1.30/0.60 inference(split_clause,[status(thm)],[f1749,f1759,f277,f1315])).
% 1.30/0.60 fof(f1856,plain,(
% 1.30/0.60 ![X0]: (~p(X0,s0,s2,s1,s0)|~neq(X0,s2)|~neq(X0,s1)|~sQ262_spl)),
% 1.30/0.60 inference(resolution,[status(thm)],[f1760,f29])).
% 1.30/0.60 fof(f1891,plain,(
% 1.30/0.60 ~p(s0,s0,s2,s1,s0)|~neq(s0,s2)|~sQ262_spl),
% 1.30/0.60 inference(resolution,[status(thm)],[f1856,f28])).
% 1.30/0.60 fof(f1896,definition,(
% 1.30/0.60 sQ282_spl <=> (p(s0,s0,s2,s1,s0))),
% 1.30/0.60 introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition])).
% 1.30/0.60 fof(f1898,plain,(
% 1.30/0.60 ~p(s0,s0,s2,s1,s0)|sQ282_spl),
% 1.30/0.60 inference(component_clause,[status(thm)],[f1896])).
% 1.30/0.60 fof(f1899,plain,(
% 1.30/0.60 ~sQ282_spl|~sQ8_spl|~sQ262_spl),
% 1.30/0.60 inference(split_clause,[status(thm)],[f1891,f1896,f91,f1759])).
% 1.30/0.60 fof(f1927,plain,(
% 1.30/0.60 ![X0]: (~p(X0,s0,s2,s1,s0)|sQ282_spl)),
% 1.30/0.60 inference(resolution,[status(thm)],[f1898,f18])).
% 1.30/0.60 fof(f1982,plain,(
% 1.30/0.60 ![X0]: (~p(s1,X0,s2,s1,s0)|~neq(s1,X0)|sQ282_spl)),
% 1.30/0.60 inference(resolution,[status(thm)],[f1927,f40])).
% 1.30/0.60 fof(f2096,plain,(
% 1.30/0.60 ~p(s1,s2,s2,s1,s0)|sQ282_spl),
% 1.30/0.60 inference(resolution,[status(thm)],[f1982,f32])).
% 1.30/0.60 fof(f2214,plain,(
% 1.30/0.60 ![X0]: (~p(X0,s2,s2,s1,s0)|sQ282_spl)),
% 1.30/0.60 inference(resolution,[status(thm)],[f2096,f18])).
% 1.30/0.60 fof(f2258,plain,(
% 1.30/0.60 ![X0,X1]: (~p(X0,s2,s2,X1,s0)|~neq(X0,X1)|~neq(X0,s1)|~neq(s2,X1)|~neq(s2,s1)|~neq(s2,X1)|~neq(s2,s1)|sQ282_spl)),
% 1.30/0.60 inference(resolution,[status(thm)],[f2214,f24])).
% 1.30/0.60 fof(f2265,definition,(
% 1.30/0.60 ![X0,X1]: (sQ339_spl <=> (~p(X0,s2,s2,X1,s0)|~neq(X0,X1)|~neq(X0,s1)|~neq(s2,X1)|~neq(s2,X1)))),
% 1.30/0.60 introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition])).
% 1.30/0.60 fof(f2266,plain,(
% 1.30/0.60 ![X0,X1]: (~p(X0,s2,s2,X1,s0)|~neq(X0,X1)|~neq(X0,s1)|~neq(s2,X1)|~neq(s2,X1)|~sQ339_spl)),
% 1.30/0.60 inference(component_clause,[status(thm)],[f2265])).
% 1.30/0.60 fof(f2268,plain,(
% 1.30/0.60 sQ339_spl|~sQ75_spl|sQ282_spl),
% 1.30/0.60 inference(split_clause,[status(thm)],[f2258,f2265,f525,f1896])).
% 1.30/0.60 fof(f2274,plain,(
% 1.30/0.60 ![X0,X1]: (~p(X0,s2,s2,X1,s0)|~neq(X0,X1)|~neq(X0,s1)|~neq(s2,X1)|~sQ339_spl)),
% 1.30/0.60 inference(duplicate_literals_removal,[status(thm)],[f2266])).
% 1.30/0.60 fof(f2420,plain,(
% 1.30/0.60 ![X0]: (~p(X0,s2,s2,s0,s0)|~neq(X0,s0)|~neq(X0,s1)|~sQ339_spl)),
% 1.30/0.60 inference(resolution,[status(thm)],[f2274,f33])).
% 1.30/0.60 fof(f2474,plain,(
% 1.30/0.60 ~p(s2,s2,s2,s0,s0)|~neq(s2,s0)|~sQ339_spl),
% 1.30/0.60 inference(resolution,[status(thm)],[f2420,f34])).
% 1.30/0.60 fof(f2476,definition,(
% 1.30/0.60 sQ370_spl <=> (p(s2,s2,s2,s0,s0))),
% 1.30/0.60 introduced(definition,[new_symbols(definition,[sQ370_spl])],[split_symbol_definition])).
% 1.30/0.60 fof(f2478,plain,(
% 1.30/0.60 ~p(s2,s2,s2,s0,s0)|sQ370_spl),
% 1.30/0.60 inference(component_clause,[status(thm)],[f2476])).
% 1.30/0.60 fof(f2479,plain,(
% 1.30/0.60 ~sQ370_spl|~sQ53_spl|~sQ339_spl),
% 1.30/0.60 inference(split_clause,[status(thm)],[f2474,f2476,f380,f2265])).
% 1.30/0.60 fof(f2542,plain,(
% 1.30/0.60 ![X0]: (~p(X0,s2,s2,s0,s0)|sQ370_spl)),
% 1.30/0.60 inference(resolution,[status(thm)],[f2478,f18])).
% 1.30/0.60 fof(f2574,plain,(
% 1.30/0.60 ![X0]: (~p(s0,X0,s2,s0,s0)|~neq(s0,X0)|sQ370_spl)),
% 1.30/0.60 inference(resolution,[status(thm)],[f2542,f39])).
% 1.30/0.60 fof(f2763,plain,(
% 1.30/0.60 ~p(s0,s1,s2,s0,s0)|sQ370_spl),
% 1.30/0.60 inference(resolution,[status(thm)],[f2574,f28])).
% 1.30/0.60 fof(f2866,plain,(
% 1.30/0.60 ![X0]: (~p(X0,s1,s2,s0,s0)|sQ370_spl)),
% 1.30/0.60 inference(resolution,[status(thm)],[f2763,f18])).
% 1.30/0.61 fof(f2937,plain,(
% 1.30/0.61 ![X0,X1]: (~p(X0,s1,X1,s0,s0)|~neq(X0,X1)|~neq(X0,s2)|~neq(s1,X1)|~neq(s1,s2)|sQ370_spl)),
% 1.30/0.61 inference(resolution,[status(thm)],[f2866,f22])).
% 1.30/0.61 fof(f2947,definition,(
% 1.30/0.61 ![X0,X1]: (sQ442_spl <=> (~p(X0,s1,X1,s0,s0)|~neq(X0,X1)|~neq(X0,s2)|~neq(s1,X1)))),
% 1.30/0.61 introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition])).
% 1.30/0.61 fof(f2948,plain,(
% 1.30/0.61 ![X0,X1]: (~p(X0,s1,X1,s0,s0)|~neq(X0,X1)|~neq(X0,s2)|~neq(s1,X1)|~sQ442_spl)),
% 1.30/0.61 inference(component_clause,[status(thm)],[f2947])).
% 1.30/0.61 fof(f2950,plain,(
% 1.30/0.61 sQ442_spl|~sQ9_spl|sQ370_spl),
% 1.30/0.61 inference(split_clause,[status(thm)],[f2937,f2947,f94,f2476])).
% 1.30/0.61 fof(f3104,plain,(
% 1.30/0.61 ![X0]: (~p(X0,s1,s0,s0,s0)|~neq(X0,s0)|~neq(X0,s2)|~sQ442_spl)),
% 1.30/0.61 inference(resolution,[status(thm)],[f2948,f30])).
% 1.30/0.61 fof(f3200,plain,(
% 1.30/0.61 ~p(s1,s1,s0,s0,s0)|~neq(s1,s0)|~sQ442_spl),
% 1.30/0.61 inference(resolution,[status(thm)],[f3104,f32])).
% 1.30/0.61 fof(f3202,definition,(
% 1.30/0.61 sQ480_spl <=> (p(s1,s1,s0,s0,s0))),
% 1.30/0.61 introduced(definition,[new_symbols(definition,[sQ480_spl])],[split_symbol_definition])).
% 1.30/0.61 fof(f3204,plain,(
% 1.30/0.61 ~p(s1,s1,s0,s0,s0)|sQ480_spl),
% 1.30/0.61 inference(component_clause,[status(thm)],[f3202])).
% 1.30/0.61 fof(f3205,plain,(
% 1.30/0.61 ~sQ480_spl|~sQ26_spl|~sQ442_spl),
% 1.30/0.61 inference(split_clause,[status(thm)],[f3200,f3202,f191,f2947])).
% 1.30/0.61 fof(f3270,plain,(
% 1.30/0.61 ![X0]: (~p(X0,s1,s0,s0,s0)|sQ480_spl)),
% 1.30/0.61 inference(resolution,[status(thm)],[f3204,f18])).
% 1.30/0.61 fof(f3338,plain,(
% 1.30/0.61 ![X0]: (~p(s2,X0,s0,s0,s0)|~neq(s2,X0)|sQ480_spl)),
% 1.30/0.61 inference(resolution,[status(thm)],[f3270,f43])).
% 1.30/0.61 fof(f3525,plain,(
% 1.30/0.61 ~p(s2,s0,s0,s0,s0)|sQ480_spl),
% 1.30/0.61 inference(resolution,[status(thm)],[f3338,f33])).
% 1.30/0.61 fof(f3735,plain,(
% 1.30/0.61 ![X0]: (~p(X0,s0,s0,s0,s0)|sQ480_spl)),
% 1.30/0.61 inference(resolution,[status(thm)],[f3525,f18])).
% 1.30/0.61 fof(f3748,plain,(
% 1.30/0.61 $false|sQ480_spl),
% 1.30/0.61 inference(backward_subsumption_resolution,[status(thm)],[f36,f3735])).
% 1.30/0.61 fof(f3749,plain,(
% 1.30/0.61 sQ480_spl),
% 1.30/0.61 inference(contradiction_clause,[status(thm)],[f3748])).
% 1.30/0.61 fof(f3750,plain,(
% 1.30/0.61 $false),
% 1.30/0.61 inference(sat_refutation,[status(thm)],[f107,f109,f146,f219,f222,f300,f324,f417,f464,f590,f600,f688,f760,f846,f1116,f1318,f1762,f1899,f2268,f2479,f2950,f3205,f3749])).
% 1.30/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 1.30/0.61 % Elapsed time: 0.239890 seconds
% 1.30/0.61 % CPU time: 1.625430 seconds
% 1.30/0.61 % Total memory used: 78.749 MB
% 1.30/0.61 % Net memory used: 74.586 MB
%------------------------------------------------------------------------------