Drodi-SAT---4.1.1.UNS-Ass.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : SYN784-1 : TPTP v9.3.1. Released v2.5.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 03:20:32 PM UTC 2026

% Result   : Unsatisfiable 10.23s 1.75s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SYN784-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.37  % Computer : n019.cluster.edu
% 0.08/0.37  % Model    : x86_64 x86_64
% 0.08/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37  % Memory   : 8046.5625MB
% 0.08/0.37  % OS       : Linux 6.8.0-71-generic
% 0.08/0.37  % CPULimit : 300
% 0.08/0.37  % WCLimit  : 300
% 0.08/0.37  % DateTime : Mon Sep 21 11:16:49 UTC 2026
% 0.08/0.37  % CPUTime  : 
% 0.08/0.38  % Drodi V4.1.1
% 10.23/1.75  % Refutation found
% 10.23/1.75  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 10.23/1.75  % SZS output start CNFRefutation for theBenchmark
% 10.23/1.75  fof(f1,negated_conjecture,(
% 10.23/1.75    (![U]: (ssRr(skf3(U),U) ))),
% 10.23/1.75    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.75  fof(f2,negated_conjecture,(
% 10.23/1.75    (![U]: (ssRr(U,skf2(U)) ))),
% 10.23/1.75    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.75  fof(f3,negated_conjecture,(
% 10.23/1.75    (![U,V]: (( ~ ssRr(U,V)| ssPv4(U)| ssPv2(V)| ssPv3(V)| ssPv4(V) ) ))),
% 10.23/1.75    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.75  fof(f4,negated_conjecture,(
% 10.23/1.75    (![U,V]: (( ~ ssRr(U,V)| ~ ssPv4(V)| ssPv2(U)| ssPv2(V)| ssPv3(V) ) ))),
% 10.23/1.75    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.75  fof(f5,negated_conjecture,(
% 10.23/1.75    (![U,V]: (( ~ ssRr(U,V)| ~ ssPv1(V)| ~ ssPv4(V)| ssPv2(U)| ssPv2(V) ) ))),
% 10.23/1.75    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.75  fof(f6,negated_conjecture,(
% 10.23/1.75    (![U,V]: (( ~ ssRr(U,V)| ~ ssPv3(U)| ~ ssPv4(U)| ssPv1(V)| ssPv1(U) ) ))),
% 10.23/1.75    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f8,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssRr(U,W)| ssPv4(V)| ssPv3(W)| ssPv3(U)| ssPv4(U) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f9,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssRr(V,W)| ~ ssPv3(V)| ssPv2(U)| ssPv4(W)| ssPv4(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f10,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssRr(W,V)| ~ ssPv2(V)| ssPv3(U)| ssPv2(W)| ssPv3(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f14,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv2(V)| ~ ssRr(U,W)| ~ ssPv1(U)| ssPv4(W)| ssPv4(U) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f15,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv3(U)| ~ ssRr(W,V)| ~ ssPv4(V)| ssPv4(W)| ssPv3(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f16,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv4(V)| ~ ssRr(U,W)| ~ ssPv2(U)| ssPv1(W)| ssPv3(U) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f17,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv2(V)| ~ ssRr(U,W)| ~ ssPv1(U)| ssPv4(W)| ssPv3(U) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f18,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv1(U)| ~ ssRr(W,V)| ~ ssPv4(V)| ssPv3(W)| ssPv2(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f19,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv4(U)| ~ ssRr(V,W)| ~ ssPv3(W)| ssPv2(V)| ssPv4(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f20,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssRr(V,W)| ~ ssPv4(W)| ~ ssPv3(V)| ~ ssPv4(V)| ssPv3(U) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f21,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv2(V)| ~ ssRr(U,W)| ~ ssPv2(U)| ~ ssPv4(U)| ssPv4(W) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f22,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv3(U)| ~ ssRr(V,W)| ~ ssPv2(V)| ~ ssPv3(V)| ssPv2(W) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f23,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv4(U)| ~ ssRr(V,W)| ~ ssPv1(V)| ~ ssPv4(V)| ssPv1(W) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f24,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(U,W)| ~ ssPv2(W)| ~ ssPv3(U)| ssPv4(U) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f25,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv4(U)| ~ ssRr(V,W)| ~ ssPv3(W)| ~ ssPv3(V)| ssPv1(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f26,negated_conjecture,(
% 10.23/1.76    (![U,V,W]: (( ~ ssRr(U,V)| ~ ssPv2(U)| ~ ssRr(V,W)| ~ ssPv3(W)| ~ ssPv3(V)| ssPv1(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f27,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssRr(V,W)| ~ ssRr(V,X)| ssPv1(U)| ssPv4(W)| ssPv2(X)| ssPv3(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f29,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv2(U)| ~ ssRr(W,V)| ~ ssRr(X,V)| ssPv4(W)| ssPv2(X)| ssPv4(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f31,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv3(U)| ~ ssRr(V,W)| ~ ssPv2(W)| ~ ssRr(V,X)| ssPv4(X)| ssPv4(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f32,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv3(U)| ~ ssRr(W,V)| ~ ssRr(V,X)| ~ ssPv3(X)| ssPv4(W)| ssPv3(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f33,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv3(U)| ~ ssRr(V,W)| ~ ssPv2(W)| ~ ssRr(V,X)| ssPv2(X)| ssPv3(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f34,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv2(U)| ~ ssRr(V,W)| ~ ssRr(V,X)| ~ ssPv4(V)| ssPv4(W)| ssPv3(X) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f35,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv4(U)| ~ ssRr(W,V)| ~ ssPv2(W)| ~ ssRr(X,V)| ssPv1(X)| ssPv2(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f36,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssRr(V,W)| ~ ssPv4(W)| ~ ssRr(V,X)| ~ ssPv3(X)| ssPv4(U)| ssPv2(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f37,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv2(U)| ~ ssRr(V,W)| ~ ssPv4(W)| ~ ssRr(V,X)| ssPv3(X)| ssPv2(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f38,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv1(U)| ~ ssRr(V,W)| ~ ssPv3(W)| ~ ssRr(V,X)| ~ ssPv1(V)| ssPv2(X) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f39,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssRr(V,W)| ~ ssPv4(W)| ~ ssRr(V,X)| ~ ssPv2(X)| ~ ssPv1(V)| ssPv4(U) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f40,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv3(U)| ~ ssRr(W,V)| ~ ssPv1(W)| ~ ssRr(V,X)| ~ ssPv1(X)| ~ ssPv3(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f41,negated_conjecture,(
% 10.23/1.76    (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv2(U)| ~ ssRr(V,W)| ~ ssPv2(W)| ~ ssRr(V,X)| ~ ssPv1(X)| ~ ssPv1(V) ) ))),
% 10.23/1.76    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.23/1.76  fof(f43,plain,(
% 10.23/1.76    ![X0]: (ssRr(skf3(X0),X0))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f1])).
% 10.23/1.76  fof(f44,plain,(
% 10.23/1.76    ![X0]: (ssRr(X0,skf2(X0)))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f2])).
% 10.23/1.76  fof(f45,plain,(
% 10.23/1.76    ![V]: ((((![U]: (~ssRr(U,V)|ssPv4(U)))|ssPv2(V))|ssPv3(V))|ssPv4(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f3])).
% 10.23/1.76  fof(f46,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|ssPv4(X0)|ssPv2(X1)|ssPv3(X1)|ssPv4(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f45])).
% 10.23/1.76  fof(f47,plain,(
% 10.23/1.76    ![V]: (((![U]: ((~ssRr(U,V)|~ssPv4(V))|ssPv2(U)))|ssPv2(V))|ssPv3(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f4])).
% 10.23/1.76  fof(f48,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv4(X1)|ssPv2(X0)|ssPv2(X1)|ssPv3(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f47])).
% 10.23/1.76  fof(f49,plain,(
% 10.23/1.76    ![V]: ((![U]: (((~ssRr(U,V)|~ssPv1(V))|~ssPv4(V))|ssPv2(U)))|ssPv2(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f5])).
% 10.23/1.76  fof(f50,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv1(X1)|~ssPv4(X1)|ssPv2(X0)|ssPv2(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f49])).
% 10.23/1.76  fof(f51,plain,(
% 10.23/1.76    ![U]: ((![V]: (((~ssRr(U,V)|~ssPv3(U))|~ssPv4(U))|ssPv1(V)))|ssPv1(U))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f6])).
% 10.23/1.76  fof(f52,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssPv4(X0)|ssPv1(X1)|ssPv1(X0))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f51])).
% 10.23/1.76  fof(f55,plain,(
% 10.23/1.76    ![U]: (((![W]: ((![V]: ((~ssRr(U,V)|~ssRr(U,W))|ssPv4(V)))|ssPv3(W)))|ssPv3(U))|ssPv4(U))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f8])).
% 10.23/1.76  fof(f56,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssRr(X0,X2)|ssPv4(X1)|ssPv3(X2)|ssPv3(X0)|ssPv4(X0))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f55])).
% 10.23/1.76  fof(f57,plain,(
% 10.23/1.76    ![V]: ((![W]: ((![U]: (((~ssRr(U,V)|~ssRr(V,W))|~ssPv3(V))|ssPv2(U)))|ssPv4(W)))|ssPv4(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f9])).
% 10.23/1.76  fof(f58,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssRr(X1,X2)|~ssPv3(X1)|ssPv2(X0)|ssPv4(X2)|ssPv4(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f57])).
% 10.23/1.76  fof(f59,plain,(
% 10.23/1.76    ![V]: ((![W]: ((![U]: (((~ssRr(U,V)|~ssRr(W,V))|~ssPv2(V))|ssPv3(U)))|ssPv2(W)))|ssPv3(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f10])).
% 10.23/1.76  fof(f60,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssRr(X2,X1)|~ssPv2(X1)|ssPv3(X0)|ssPv2(X2)|ssPv3(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f59])).
% 10.23/1.76  fof(f67,plain,(
% 10.23/1.76    ![U]: ((![W]: ((((![V]: (~ssRr(U,V)|~ssPv2(V)))|~ssRr(U,W))|~ssPv1(U))|ssPv4(W)))|ssPv4(U))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f14])).
% 10.23/1.76  fof(f68,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X0,X2)|~ssPv1(X0)|ssPv4(X2)|ssPv4(X0))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f67])).
% 10.23/1.76  fof(f69,plain,(
% 10.23/1.76    ![V]: ((![W]: ((((![U]: (~ssRr(U,V)|~ssPv3(U)))|~ssRr(W,V))|~ssPv4(V))|ssPv4(W)))|ssPv3(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f15])).
% 10.23/1.76  fof(f70,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssRr(X2,X1)|~ssPv4(X1)|ssPv4(X2)|ssPv3(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f69])).
% 10.23/1.76  fof(f71,plain,(
% 10.23/1.76    ![U]: ((![W]: ((((![V]: (~ssRr(U,V)|~ssPv4(V)))|~ssRr(U,W))|~ssPv2(U))|ssPv1(W)))|ssPv3(U))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f16])).
% 10.23/1.76  fof(f72,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X0,X2)|~ssPv2(X0)|ssPv1(X2)|ssPv3(X0))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f71])).
% 10.23/1.76  fof(f73,plain,(
% 10.23/1.76    ![U]: ((![W]: ((((![V]: (~ssRr(U,V)|~ssPv2(V)))|~ssRr(U,W))|~ssPv1(U))|ssPv4(W)))|ssPv3(U))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f17])).
% 10.23/1.76  fof(f74,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X0,X2)|~ssPv1(X0)|ssPv4(X2)|ssPv3(X0))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f73])).
% 10.23/1.76  fof(f75,plain,(
% 10.23/1.76    ![V]: ((![W]: ((((![U]: (~ssRr(U,V)|~ssPv1(U)))|~ssRr(W,V))|~ssPv4(V))|ssPv3(W)))|ssPv2(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f18])).
% 10.23/1.76  fof(f76,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv1(X0)|~ssRr(X2,X1)|~ssPv4(X1)|ssPv3(X2)|ssPv2(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f75])).
% 10.23/1.76  fof(f77,plain,(
% 10.23/1.76    ![V]: (((![W]: (((![U]: (~ssRr(U,V)|~ssPv4(U)))|~ssRr(V,W))|~ssPv3(W)))|ssPv2(V))|ssPv4(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f19])).
% 10.23/1.76  fof(f78,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv4(X0)|~ssRr(X1,X2)|~ssPv3(X2)|ssPv2(X1)|ssPv4(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f77])).
% 10.23/1.76  fof(f79,plain,(
% 10.23/1.76    ![U]: ((![V]: (((![W]: ((~ssRr(U,V)|~ssRr(V,W))|~ssPv4(W)))|~ssPv3(V))|~ssPv4(V)))|ssPv3(U))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f20])).
% 10.23/1.76  fof(f80,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssRr(X1,X2)|~ssPv4(X2)|~ssPv3(X1)|~ssPv4(X1)|ssPv3(X0))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f79])).
% 10.23/1.76  fof(f81,plain,(
% 10.23/1.76    ![W]: ((![U]: ((((![V]: (~ssRr(U,V)|~ssPv2(V)))|~ssRr(U,W))|~ssPv2(U))|~ssPv4(U)))|ssPv4(W))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f21])).
% 10.23/1.76  fof(f82,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X0,X2)|~ssPv2(X0)|~ssPv4(X0)|ssPv4(X2))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f81])).
% 10.23/1.76  fof(f83,plain,(
% 10.23/1.76    ![W]: ((![V]: ((((![U]: (~ssRr(U,V)|~ssPv3(U)))|~ssRr(V,W))|~ssPv2(V))|~ssPv3(V)))|ssPv2(W))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f22])).
% 10.23/1.76  fof(f84,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssRr(X1,X2)|~ssPv2(X1)|~ssPv3(X1)|ssPv2(X2))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f83])).
% 10.23/1.76  fof(f85,plain,(
% 10.23/1.76    ![W]: ((![V]: ((((![U]: (~ssRr(U,V)|~ssPv4(U)))|~ssRr(V,W))|~ssPv1(V))|~ssPv4(V)))|ssPv1(W))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f23])).
% 10.23/1.76  fof(f86,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv4(X0)|~ssRr(X1,X2)|~ssPv1(X1)|~ssPv4(X1)|ssPv1(X2))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f85])).
% 10.23/1.76  fof(f87,plain,(
% 10.23/1.76    ![U]: (((![W]: (((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(U,W))|~ssPv2(W)))|~ssPv3(U))|ssPv4(U))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f24])).
% 10.23/1.76  fof(f88,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X0,X2)|~ssPv2(X2)|~ssPv3(X0)|ssPv4(X0))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f87])).
% 10.23/1.76  fof(f89,plain,(
% 10.23/1.76    ![V]: (((![W]: (((![U]: (~ssRr(U,V)|~ssPv4(U)))|~ssRr(V,W))|~ssPv3(W)))|~ssPv3(V))|ssPv1(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f25])).
% 10.23/1.76  fof(f90,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv4(X0)|~ssRr(X1,X2)|~ssPv3(X2)|~ssPv3(X1)|ssPv1(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f89])).
% 10.23/1.76  fof(f91,plain,(
% 10.23/1.76    ![V]: (((![W]: (((![U]: (~ssRr(U,V)|~ssPv2(U)))|~ssRr(V,W))|~ssPv3(W)))|~ssPv3(V))|ssPv1(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f26])).
% 10.23/1.76  fof(f92,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv2(X0)|~ssRr(X1,X2)|~ssPv3(X2)|~ssPv3(X1)|ssPv1(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f91])).
% 10.23/1.76  fof(f93,plain,(
% 10.23/1.76    ![V]: ((![X]: ((![W]: ((![U]: (((~ssRr(U,V)|~ssRr(V,W))|~ssRr(V,X))|ssPv1(U)))|ssPv4(W)))|ssPv2(X)))|ssPv3(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f27])).
% 10.23/1.76  fof(f94,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X1,X2)|~ssRr(X1,X3)|ssPv1(X0)|ssPv4(X2)|ssPv2(X3)|ssPv3(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f93])).
% 10.23/1.76  fof(f97,plain,(
% 10.23/1.76    ![V]: ((![X]: ((![W]: ((((![U]: (~ssRr(U,V)|~ssPv2(U)))|~ssRr(W,V))|~ssRr(X,V))|ssPv4(W)))|ssPv2(X)))|ssPv4(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f29])).
% 10.23/1.76  fof(f98,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv2(X0)|~ssRr(X2,X1)|~ssRr(X3,X1)|ssPv4(X2)|ssPv2(X3)|ssPv4(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f97])).
% 10.23/1.76  fof(f101,plain,(
% 10.23/1.76    ![V]: ((![X]: (((![W]: (((![U]: (~ssRr(U,V)|~ssPv3(U)))|~ssRr(V,W))|~ssPv2(W)))|~ssRr(V,X))|ssPv4(X)))|ssPv4(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f31])).
% 10.23/1.76  fof(f102,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssRr(X1,X2)|~ssPv2(X2)|~ssRr(X1,X3)|ssPv4(X3)|ssPv4(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f101])).
% 10.23/1.76  fof(f103,plain,(
% 10.23/1.76    ![V]: ((![W]: ((![X]: ((((![U]: (~ssRr(U,V)|~ssPv3(U)))|~ssRr(W,V))|~ssRr(V,X))|~ssPv3(X)))|ssPv4(W)))|ssPv3(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f32])).
% 10.23/1.76  fof(f104,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssRr(X2,X1)|~ssRr(X1,X3)|~ssPv3(X3)|ssPv4(X2)|ssPv3(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f103])).
% 10.23/1.76  fof(f105,plain,(
% 10.23/1.76    ![V]: ((![X]: (((![W]: (((![U]: (~ssRr(U,V)|~ssPv3(U)))|~ssRr(V,W))|~ssPv2(W)))|~ssRr(V,X))|ssPv2(X)))|ssPv3(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f33])).
% 10.23/1.76  fof(f106,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssRr(X1,X2)|~ssPv2(X2)|~ssRr(X1,X3)|ssPv2(X3)|ssPv3(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f105])).
% 10.23/1.76  fof(f107,plain,(
% 10.23/1.76    ![X]: ((![W]: ((![V]: ((((![U]: (~ssRr(U,V)|~ssPv2(U)))|~ssRr(V,W))|~ssRr(V,X))|~ssPv4(V)))|ssPv4(W)))|ssPv3(X))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f34])).
% 10.23/1.76  fof(f108,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv2(X0)|~ssRr(X1,X2)|~ssRr(X1,X3)|~ssPv4(X1)|ssPv4(X2)|ssPv3(X3))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f107])).
% 10.23/1.76  fof(f109,plain,(
% 10.23/1.76    ![V]: ((![X]: (((![W]: (((![U]: (~ssRr(U,V)|~ssPv4(U)))|~ssRr(W,V))|~ssPv2(W)))|~ssRr(X,V))|ssPv1(X)))|ssPv2(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f35])).
% 10.23/1.76  fof(f110,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv4(X0)|~ssRr(X2,X1)|~ssPv2(X2)|~ssRr(X3,X1)|ssPv1(X3)|ssPv2(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f109])).
% 10.23/1.76  fof(f111,plain,(
% 10.23/1.76    ![V]: ((![U]: ((![X]: (((![W]: ((~ssRr(U,V)|~ssRr(V,W))|~ssPv4(W)))|~ssRr(V,X))|~ssPv3(X)))|ssPv4(U)))|ssPv2(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f36])).
% 10.23/1.76  fof(f112,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X1,X2)|~ssPv4(X2)|~ssRr(X1,X3)|~ssPv3(X3)|ssPv4(X0)|ssPv2(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f111])).
% 10.23/1.76  fof(f113,plain,(
% 10.23/1.76    ![V]: ((![X]: (((![W]: (((![U]: (~ssRr(U,V)|~ssPv2(U)))|~ssRr(V,W))|~ssPv4(W)))|~ssRr(V,X))|ssPv3(X)))|ssPv2(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f37])).
% 10.23/1.76  fof(f114,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv2(X0)|~ssRr(X1,X2)|~ssPv4(X2)|~ssRr(X1,X3)|ssPv3(X3)|ssPv2(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f113])).
% 10.23/1.76  fof(f115,plain,(
% 10.23/1.76    ![X]: ((![V]: (((![W]: (((![U]: (~ssRr(U,V)|~ssPv1(U)))|~ssRr(V,W))|~ssPv3(W)))|~ssRr(V,X))|~ssPv1(V)))|ssPv2(X))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f38])).
% 10.23/1.76  fof(f116,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv1(X0)|~ssRr(X1,X2)|~ssPv3(X2)|~ssRr(X1,X3)|~ssPv1(X1)|ssPv2(X3))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f115])).
% 10.23/1.76  fof(f117,plain,(
% 10.23/1.76    ![U]: ((![V]: ((![X]: (((![W]: ((~ssRr(U,V)|~ssRr(V,W))|~ssPv4(W)))|~ssRr(V,X))|~ssPv2(X)))|~ssPv1(V)))|ssPv4(U))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f39])).
% 10.23/1.76  fof(f118,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X1,X2)|~ssPv4(X2)|~ssRr(X1,X3)|~ssPv2(X3)|~ssPv1(X1)|ssPv4(X0))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f117])).
% 10.23/1.76  fof(f119,plain,(
% 10.23/1.76    ![V]: ((![X]: (((![W]: (((![U]: (~ssRr(U,V)|~ssPv3(U)))|~ssRr(W,V))|~ssPv1(W)))|~ssRr(V,X))|~ssPv1(X)))|~ssPv3(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f40])).
% 10.23/1.76  fof(f120,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssRr(X2,X1)|~ssPv1(X2)|~ssRr(X1,X3)|~ssPv1(X3)|~ssPv3(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f119])).
% 10.23/1.76  fof(f121,plain,(
% 10.23/1.76    ![V]: ((![X]: (((![W]: (((![U]: (~ssRr(U,V)|~ssPv2(U)))|~ssRr(V,W))|~ssPv2(W)))|~ssRr(V,X))|~ssPv1(X)))|~ssPv1(V))),
% 10.23/1.76    inference(miniscoping,[status(thm)],[f41])).
% 10.23/1.76  fof(f122,plain,(
% 10.23/1.76    ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv2(X0)|~ssRr(X1,X2)|~ssPv2(X2)|~ssRr(X1,X3)|~ssPv1(X3)|~ssPv1(X1))),
% 10.23/1.76    inference(cnf_transformation,[status(thm)],[f121])).
% 10.23/1.76  fof(f125,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf3(X1))|~ssPv4(X1)|~ssPv3(skf3(X1))|~ssPv4(skf3(X1))|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f80,f43])).
% 10.23/1.76  fof(f129,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(skf3(X0),X1)|~ssPv2(X1)|~ssPv2(skf3(X0))|~ssPv4(skf3(X0))|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f82,f43])).
% 10.23/1.76  fof(f130,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssPv2(X0)|~ssPv4(X0)|ssPv4(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f82,f44])).
% 10.23/1.76  fof(f132,plain,(
% 10.23/1.76    ![X0]: (~ssPv2(skf2(X0))|~ssPv2(X0)|~ssPv4(X0)|ssPv4(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f130,f44])).
% 10.23/1.76  fof(f133,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf3(X1))|~ssPv3(X0)|~ssPv2(skf3(X1))|~ssPv3(skf3(X1))|ssPv2(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f84,f43])).
% 10.23/1.76  fof(f134,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssPv2(X1)|~ssPv3(X1)|ssPv2(skf2(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f84,f44])).
% 10.23/1.76  fof(f135,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf3(X1))|~ssPv4(X0)|~ssPv1(skf3(X1))|~ssPv4(skf3(X1))|ssPv1(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f86,f43])).
% 10.23/1.76  fof(f136,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv4(X0)|~ssPv1(X1)|~ssPv4(X1)|ssPv1(skf2(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f86,f44])).
% 10.23/1.76  fof(f137,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(skf3(X0))|~ssPv2(X0)|~ssPv3(X0)|ssPv2(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f134,f43])).
% 10.23/1.76  fof(f139,plain,(
% 10.23/1.76    ![X0]: (~ssPv4(skf3(X0))|~ssPv1(X0)|~ssPv4(X0)|ssPv1(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f136,f43])).
% 10.23/1.76  fof(f142,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssPv2(skf2(X0))|~ssPv3(X0)|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f88,f44])).
% 10.23/1.76  fof(f143,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf3(X1))|~ssPv4(X0)|~ssPv3(X1)|~ssPv3(skf3(X1))|ssPv1(skf3(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f90,f43])).
% 10.23/1.76  fof(f144,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv4(X0)|~ssPv3(skf2(X1))|~ssPv3(X1)|ssPv1(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f90,f44])).
% 10.23/1.76  fof(f145,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf3(X1))|~ssPv2(X0)|~ssPv3(X1)|~ssPv3(skf3(X1))|ssPv1(skf3(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f92,f43])).
% 10.23/1.76  fof(f146,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv2(X0)|~ssPv3(skf2(X1))|~ssPv3(X1)|ssPv1(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f92,f44])).
% 10.23/1.76  fof(f147,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf3(X1))|~ssPv1(X0)|~ssPv3(X1)|~ssPv1(skf3(X1))|ssPv2(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f116,f43])).
% 10.23/1.76  fof(f149,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv1(X0)|~ssPv3(skf2(X1))|~ssPv1(X1)|ssPv2(skf2(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f116,f44])).
% 10.23/1.76  fof(f153,plain,(
% 10.23/1.76    ![X0]: (ssPv4(skf3(X0))|ssPv2(X0)|ssPv3(X0)|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f46,f43])).
% 10.23/1.76  fof(f154,plain,(
% 10.23/1.76    ![X0]: (ssPv4(X0)|ssPv2(skf2(X0))|ssPv3(skf2(X0))|ssPv4(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f46,f44])).
% 10.23/1.76  fof(f156,plain,(
% 10.23/1.76    ![X0]: (~ssPv4(X0)|ssPv2(skf3(X0))|ssPv2(X0)|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f48,f43])).
% 10.23/1.76  fof(f157,plain,(
% 10.23/1.76    ![X0]: (~ssPv4(skf2(X0))|ssPv2(X0)|ssPv2(skf2(X0))|ssPv3(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f48,f44])).
% 10.23/1.76  fof(f160,plain,(
% 10.23/1.76    ![X0]: (~ssPv1(X0)|~ssPv4(X0)|ssPv2(skf3(X0))|ssPv2(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f50,f43])).
% 10.23/1.76  fof(f164,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(skf3(X0))|~ssPv4(skf3(X0))|ssPv1(X0)|ssPv1(skf3(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f52,f43])).
% 10.23/1.76  fof(f165,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(X0)|~ssPv4(X0)|ssPv1(skf2(X0))|ssPv1(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f52,f44])).
% 10.23/1.76  fof(f169,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(skf3(X0),X1)|ssPv4(X1)|ssPv3(X0)|ssPv3(skf3(X0))|ssPv4(skf3(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f56,f43])).
% 10.23/1.76  fof(f172,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv3(X1)|ssPv2(X0)|ssPv4(skf2(X1))|ssPv4(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f58,f44])).
% 10.23/1.76  fof(f173,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv2(X1)|ssPv3(X0)|ssPv2(skf3(X1))|ssPv3(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f60,f43])).
% 10.23/1.76  fof(f174,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf2(X1))|~ssPv2(skf2(X1))|ssPv3(X0)|ssPv2(X1)|ssPv3(skf2(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f60,f44])).
% 10.23/1.76  fof(f181,plain,(
% 10.23/1.76    ![X0]: (ssPv2(X0)|ssPv2(skf2(X0))|ssPv3(skf2(X0))|ssPv4(X0)|ssPv2(skf2(X0))|ssPv3(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f157,f154])).
% 10.23/1.76  fof(f182,plain,(
% 10.23/1.76    ![X0]: (ssPv2(X0)|ssPv2(skf2(X0))|ssPv3(skf2(X0))|ssPv4(X0))),
% 10.23/1.76    inference(duplicate_literals_removal,[status(thm)],[f181])).
% 10.23/1.76  fof(f198,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(X0)|ssPv2(skf3(X0))|ssPv4(skf2(X0))|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f172,f43])).
% 10.23/1.76  fof(f199,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(skf2(X0))|ssPv2(X0)|ssPv4(skf2(skf2(X0)))|ssPv4(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f172,f44])).
% 10.23/1.76  fof(f201,plain,(
% 10.23/1.76    ![X0]: (~ssPv2(X0)|ssPv3(skf3(X0))|ssPv2(skf3(X0))|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f173,f43])).
% 10.23/1.76  fof(f214,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(skf3(X0),X1)|~ssPv2(X1)|~ssPv1(skf3(X0))|ssPv4(X0)|ssPv4(skf3(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f68,f43])).
% 10.23/1.76  fof(f215,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssPv1(X0)|ssPv4(skf2(X0))|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f68,f44])).
% 10.23/1.76  fof(f216,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssPv4(X1)|ssPv4(skf3(X1))|ssPv3(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f70,f43])).
% 10.23/1.76  fof(f217,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf2(X1))|~ssPv3(X0)|~ssPv4(skf2(X1))|ssPv4(X1)|ssPv3(skf2(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f70,f44])).
% 10.23/1.76  fof(f218,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(skf3(X0),X1)|~ssPv4(X1)|~ssPv2(skf3(X0))|ssPv1(X0)|ssPv3(skf3(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f72,f43])).
% 10.23/1.76  fof(f219,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssPv2(X0)|ssPv1(skf2(X0))|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f72,f44])).
% 10.23/1.76  fof(f221,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssPv1(X0)|ssPv4(skf2(X0))|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f74,f44])).
% 10.23/1.76  fof(f222,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv1(X0)|~ssPv4(X1)|ssPv3(skf3(X1))|ssPv2(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f76,f43])).
% 10.23/1.76  fof(f223,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf2(X1))|~ssPv1(X0)|~ssPv4(skf2(X1))|ssPv3(X1)|ssPv2(skf2(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f76,f44])).
% 10.23/1.76  fof(f225,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv4(X0)|~ssPv3(skf2(X1))|ssPv2(X1)|ssPv4(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f78,f44])).
% 10.23/1.76  fof(f234,plain,(
% 10.23/1.76    ![X0]: (~ssPv2(skf2(X0))|~ssPv1(X0)|ssPv4(skf2(X0))|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f215,f44])).
% 10.23/1.76  fof(f235,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(skf3(X0))|~ssPv4(X0)|ssPv4(skf3(X0))|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f216,f43])).
% 10.23/1.76  fof(f238,plain,(
% 10.23/1.76    ![X0]: (~ssPv4(skf2(X0))|~ssPv2(X0)|ssPv1(skf2(X0))|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f219,f44])).
% 10.23/1.76  fof(f244,plain,(
% 10.23/1.76    ![X0]: (~ssPv2(skf2(X0))|~ssPv1(X0)|ssPv4(skf2(X0))|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f221,f44])).
% 10.23/1.76  fof(f245,plain,(
% 10.23/1.76    ![X0]: (~ssPv1(skf3(X0))|~ssPv4(X0)|ssPv3(skf3(X0))|ssPv2(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f222,f43])).
% 10.23/1.76  fof(f247,plain,(
% 10.23/1.76    ![X0]: (~ssPv4(skf3(X0))|~ssPv3(skf2(X0))|ssPv2(X0)|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f225,f43])).
% 10.23/1.76  fof(f248,plain,(
% 10.23/1.76    ![X0]: (~ssPv4(X0)|~ssPv3(skf2(skf2(X0)))|ssPv2(skf2(X0))|ssPv4(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f225,f44])).
% 10.23/1.76  fof(f249,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(skf2(X0))|ssPv2(X0)|ssPv4(X0)|ssPv2(X0)|ssPv3(X0)|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f247,f153])).
% 10.23/1.76  fof(f250,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(skf2(X0))|ssPv2(X0)|ssPv4(X0)|ssPv3(X0))),
% 10.23/1.76    inference(duplicate_literals_removal,[status(thm)],[f249])).
% 10.23/1.76  fof(f251,plain,(
% 10.23/1.76    ![X0]: (ssPv2(X0)|ssPv4(X0)|ssPv3(X0)|ssPv2(X0)|ssPv2(skf2(X0))|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f250,f182])).
% 10.23/1.76  fof(f252,plain,(
% 10.23/1.76    ![X0]: (ssPv2(X0)|ssPv4(X0)|ssPv3(X0)|ssPv2(skf2(X0)))),
% 10.23/1.76    inference(duplicate_literals_removal,[status(thm)],[f251])).
% 10.23/1.76  fof(f282,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf3(X1))|ssPv1(X0)|ssPv4(X1)|ssPv2(X1)|ssPv3(skf3(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f94,f43])).
% 10.23/1.76  fof(f284,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|ssPv1(X0)|ssPv4(skf2(X1))|ssPv2(skf2(X1))|ssPv3(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f94,f44])).
% 10.23/1.76  fof(f294,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf2(X1))|~ssPv2(X0)|ssPv4(X1)|ssPv2(X1)|ssPv4(skf2(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f98,f44])).
% 10.23/1.76  fof(f304,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf3(X1))|~ssPv3(X0)|~ssPv2(X1)|ssPv4(X1)|ssPv4(skf3(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f102,f43])).
% 10.23/1.76  fof(f306,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssPv2(skf2(X1))|ssPv4(skf2(X1))|ssPv4(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f102,f44])).
% 10.23/1.76  fof(f310,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssRr(X1,X2)|~ssPv3(X2)|ssPv4(skf3(X1))|ssPv3(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f104,f43])).
% 10.23/1.76  fof(f317,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssPv2(skf2(X1))|~ssRr(X1,X2)|ssPv2(X2)|ssPv3(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f106,f44])).
% 10.23/1.76  fof(f320,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf3(X1))|~ssPv2(X0)|~ssPv4(skf3(X1))|ssPv4(X1)|ssPv3(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f108,f43])).
% 10.23/1.76  fof(f322,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv2(X0)|~ssPv4(X1)|ssPv4(skf2(X1))|ssPv3(skf2(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f108,f44])).
% 10.23/1.76  fof(f326,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv4(X0)|~ssPv2(skf3(X1))|ssPv1(skf3(X1))|ssPv2(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f110,f43])).
% 10.23/1.76  fof(f328,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf2(X1))|~ssPv4(X0)|~ssPv2(X1)|ssPv1(X1)|ssPv2(skf2(X1)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f110,f44])).
% 10.23/1.76  fof(f334,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv4(skf2(X1))|~ssPv3(skf2(X1))|ssPv4(X0)|ssPv2(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f112,f44])).
% 10.23/1.76  fof(f340,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv2(X0)|~ssPv4(skf2(X1))|ssPv3(skf2(X1))|ssPv2(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f114,f44])).
% 10.23/1.76  fof(f344,plain,(
% 10.23/1.76    ![X0]: (ssPv4(X0)|ssPv3(X0)|ssPv3(skf3(X0))|ssPv4(skf3(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f169,f43])).
% 10.23/1.76  fof(f346,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(X0)|~ssPv2(skf2(skf3(X0)))|~ssPv3(skf3(X0))|ssPv4(skf3(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f142,f43])).
% 10.23/1.76  fof(f347,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(skf2(X0))|~ssPv2(skf2(X0))|~ssPv3(X0)|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f142,f44])).
% 10.23/1.76  fof(f352,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv4(skf2(X1))|~ssPv2(skf2(X1))|~ssPv1(X1)|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f118,f44])).
% 10.23/1.76  fof(f356,plain,(
% 10.23/1.76    ![X0]: (~ssPv4(skf3(X0))|~ssPv3(skf2(X0))|~ssPv3(X0)|ssPv1(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f144,f43])).
% 10.23/1.76  fof(f360,plain,(
% 10.23/1.76    ![X0]: (~ssPv2(skf3(X0))|~ssPv3(skf2(X0))|~ssPv3(X0)|ssPv1(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f146,f43])).
% 10.23/1.76  fof(f365,plain,(
% 10.23/1.76    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssPv1(skf3(X1))|~ssRr(X1,X2)|~ssPv1(X2)|~ssPv3(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f120,f43])).
% 10.23/1.76  fof(f371,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,X1)|~ssPv2(X0)|~ssPv2(skf2(X1))|~ssPv1(skf2(X1))|~ssPv1(X1))),
% 10.23/1.76    inference(resolution,[status(thm)],[f122,f44])).
% 10.23/1.76  fof(f383,plain,(
% 10.23/1.76    ![X0]: (~ssPv1(skf3(skf3(X0)))|~ssPv3(X0)|~ssPv1(skf3(X0))|ssPv2(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f147,f43])).
% 10.23/1.76  fof(f388,plain,(
% 10.23/1.76    ![X0]: (~ssPv4(X0)|~ssPv3(skf3(X0))|~ssPv4(skf3(X0))|ssPv3(skf3(skf3(X0))))),
% 10.23/1.76    inference(resolution,[status(thm)],[f125,f43])).
% 10.23/1.76  fof(f389,plain,(
% 10.23/1.76    ![X0]: (~ssPv2(X0)|~ssPv2(skf3(X0))|~ssPv4(skf3(X0))|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f129,f43])).
% 10.23/1.76  fof(f390,plain,(
% 10.23/1.76    ![X0]: (~ssPv2(skf2(skf3(X0)))|~ssPv2(skf3(X0))|~ssPv4(skf3(X0))|ssPv4(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f129,f44])).
% 10.23/1.76  fof(f421,plain,(
% 10.23/1.76    ![X0]: (~ssPv2(skf2(X0))|ssPv3(X0)|ssPv2(X0)|ssPv3(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f174,f44])).
% 10.23/1.76  fof(f425,plain,(
% 10.23/1.76    ![X0]: (ssPv3(X0)|ssPv2(X0)|ssPv3(skf2(X0))|ssPv2(X0)|ssPv4(X0)|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f421,f252])).
% 10.23/1.76  fof(f426,plain,(
% 10.23/1.76    ![X0]: (ssPv3(X0)|ssPv2(X0)|ssPv3(skf2(X0))|ssPv4(X0))),
% 10.23/1.76    inference(duplicate_literals_removal,[status(thm)],[f425])).
% 10.23/1.76  fof(f427,plain,(
% 10.23/1.76    ![X0]: (ssPv3(X0)|ssPv2(X0)|ssPv4(X0))),
% 10.23/1.76    inference(forward_subsumption_resolution,[status(thm)],[f426,f250])).
% 10.23/1.76  fof(f430,plain,(
% 10.23/1.76    ![X0]: (ssPv2(X0)|ssPv2(skf2(X0))|ssPv3(skf2(X0)))),
% 10.23/1.76    inference(backward_subsumption_resolution,[status(thm)],[f157,f427])).
% 10.23/1.76  fof(f431,plain,(
% 10.23/1.76    ![X0]: (ssPv2(skf3(X0))|ssPv2(X0)|ssPv3(X0))),
% 10.23/1.76    inference(backward_subsumption_resolution,[status(thm)],[f156,f427])).
% 10.23/1.76  fof(f433,plain,(
% 10.23/1.76    ![X0]: (ssPv3(skf3(X0))|ssPv2(skf3(X0))|~ssPv3(skf2(X0))|~ssPv3(X0)|ssPv1(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f427,f356])).
% 10.23/1.76  fof(f448,plain,(
% 10.23/1.76    ![X0]: (ssPv3(skf3(X0))|~ssPv3(skf2(X0))|~ssPv3(X0)|ssPv1(X0))),
% 10.23/1.76    inference(forward_subsumption_resolution,[status(thm)],[f433,f360])).
% 10.23/1.76  fof(f453,plain,(
% 10.23/1.76    ![X0]: (ssPv3(skf3(X0))|ssPv2(skf3(X0))|ssPv3(X0))),
% 10.23/1.76    inference(backward_subsumption_resolution,[status(thm)],[f201,f431])).
% 10.23/1.76  fof(f459,plain,(
% 10.23/1.76    ![X0,X1]: (~ssRr(X0,skf2(X1))|ssPv3(X0)|ssPv2(X1)|ssPv3(skf2(X1)))),
% 10.23/1.76    inference(backward_subsumption_resolution,[status(thm)],[f174,f430])).
% 10.23/1.76  fof(f460,plain,(
% 10.23/1.76    ![X0]: (ssPv3(X0)|ssPv2(X0)|ssPv3(skf2(X0)))),
% 10.23/1.76    inference(backward_subsumption_resolution,[status(thm)],[f421,f430])).
% 10.23/1.76  fof(f472,plain,(
% 10.23/1.76    ![X0]: (ssPv3(X0)|ssPv2(X0)|ssPv2(X0)|ssPv4(skf2(skf2(X0)))|ssPv4(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f460,f199])).
% 10.23/1.76  fof(f476,plain,(
% 10.23/1.76    ![X0]: (ssPv3(X0)|ssPv2(X0)|ssPv4(skf2(skf2(X0)))|ssPv4(skf2(X0)))),
% 10.23/1.76    inference(duplicate_literals_removal,[status(thm)],[f472])).
% 10.23/1.76  fof(f511,plain,(
% 10.23/1.76    ![X0]: (~ssPv2(X0)|~ssPv1(skf3(X0))|ssPv4(X0)|ssPv4(skf3(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f214,f43])).
% 10.23/1.76  fof(f513,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(skf3(skf2(X0)))|~ssPv4(skf2(X0))|ssPv4(X0)|ssPv3(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f217,f43])).
% 10.23/1.76  fof(f514,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(X0)|~ssPv4(skf2(X0))|ssPv4(X0)|ssPv3(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f217,f44])).
% 10.23/1.76  fof(f515,plain,(
% 10.23/1.76    ![X0]: (~ssPv4(X0)|~ssPv2(skf3(X0))|ssPv1(X0)|ssPv3(skf3(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f218,f43])).
% 10.23/1.76  fof(f520,plain,(
% 10.23/1.76    ![X0]: (~ssPv1(X0)|~ssPv4(skf2(X0))|ssPv3(X0)|ssPv2(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f223,f44])).
% 10.23/1.76  fof(f523,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(X0)|ssPv4(X0)|ssPv3(skf2(X0))|ssPv3(skf2(X0))|ssPv2(skf2(X0)))),
% 10.23/1.76    inference(resolution,[status(thm)],[f514,f427])).
% 10.23/1.76  fof(f524,plain,(
% 10.23/1.76    ![X0]: (~ssPv3(X0)|ssPv4(X0)|ssPv3(skf2(X0))|ssPv2(skf2(X0)))),
% 10.23/1.76    inference(duplicate_literals_removal,[status(thm)],[f523])).
% 10.23/1.76  fof(f526,plain,(
% 10.23/1.76    ![X0]: (~ssPv4(X0)|ssPv1(X0)|ssPv3(skf3(X0))|ssPv2(X0)|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f515,f431])).
% 10.23/1.76  fof(f527,plain,(
% 10.23/1.76    ![X0]: (ssPv1(X0)|ssPv3(skf3(X0))|ssPv2(X0)|ssPv3(X0))),
% 10.23/1.76    inference(forward_subsumption_resolution,[status(thm)],[f526,f427])).
% 10.23/1.76  fof(f528,plain,(
% 10.23/1.76    ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|~ssPv4(X0)|ssPv4(skf3(X0))|ssPv3(X0))),
% 10.23/1.76    inference(resolution,[status(thm)],[f527,f235])).
% 10.23/1.76  fof(f532,plain,(
% 10.23/1.76    ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|~ssPv4(X0)|ssPv4(skf3(X0)))),
% 10.23/1.76    inference(duplicate_literals_removal,[status(thm)],[f528])).
% 10.23/1.76  fof(f533,plain,(
% 10.23/1.76    ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv4(skf3(X0)))),
% 10.23/1.76    inference(forward_subsumption_resolution,[status(thm)],[f532,f427])).
% 10.23/1.76  fof(f538,plain,(
% 10.23/1.76    ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|~ssPv3(skf3(X0))|ssPv1(X0)|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f533,f164])).
% 10.23/1.77  fof(f546,plain,(
% 10.23/1.77    ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|~ssPv3(skf3(X0))|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f538])).
% 10.23/1.77  fof(f547,plain,(
% 10.23/1.77    ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f546,f527])).
% 10.23/1.77  fof(f556,plain,(
% 10.23/1.77    ![X0]: (~ssPv1(X0)|ssPv3(X0)|ssPv2(skf2(X0))|ssPv3(skf2(X0))|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f520,f427])).
% 10.23/1.77  fof(f558,plain,(
% 10.23/1.77    ![X0]: (~ssPv1(X0)|ssPv3(X0)|ssPv2(skf2(X0))|ssPv3(skf2(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f556])).
% 10.23/1.77  fof(f566,plain,(
% 10.23/1.77    ![X0]: (ssPv3(skf3(skf2(X0)))|ssPv2(X0)|ssPv3(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f459,f43])).
% 10.23/1.77  fof(f576,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|ssPv2(X0)|ssPv4(skf2(X0))|~ssPv3(skf2(X0))|ssPv4(skf2(X0))|ssPv3(skf2(skf2(X0))))),
% 10.23/1.77    inference(resolution,[status(thm)],[f476,f514])).
% 10.23/1.77  fof(f589,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|ssPv2(X0)|ssPv4(skf2(X0))|~ssPv3(skf2(X0))|ssPv3(skf2(skf2(X0))))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f576])).
% 10.23/1.77  fof(f590,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|ssPv2(X0)|ssPv4(skf2(X0))|ssPv3(skf2(skf2(X0))))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f589,f460])).
% 10.23/1.77  fof(f615,plain,(
% 10.23/1.77    ![X0]: (ssPv1(skf3(skf3(X0)))|ssPv4(X0)|ssPv2(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f282,f43])).
% 10.23/1.77  fof(f618,plain,(
% 10.23/1.77    ![X0]: (ssPv1(skf3(X0))|ssPv4(skf2(X0))|ssPv2(skf2(X0))|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f284,f43])).
% 10.23/1.77  fof(f637,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(X0)|~ssPv2(skf3(X0))|ssPv4(X0)|ssPv4(X0)|ssPv3(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f389,f344])).
% 10.23/1.77  fof(f639,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(X0)|~ssPv2(skf3(X0))|ssPv4(X0)|ssPv3(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f637])).
% 10.23/1.77  fof(f640,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf3(X0))|ssPv4(X0)|ssPv3(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f639,f427])).
% 10.23/1.77  fof(f641,plain,(
% 10.23/1.77    ![X0]: (~ssPv1(skf3(X0))|~ssPv3(skf2(X0))|~ssPv1(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f149,f43])).
% 10.23/1.77  fof(f643,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(skf3(skf3(X0)))|~ssPv2(skf3(X0))|~ssPv3(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f133,f43])).
% 10.23/1.77  fof(f653,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf3(skf3(X0)))|~ssPv1(skf3(X0))|~ssPv4(skf3(X0))|ssPv1(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f135,f43])).
% 10.23/1.77  fof(f661,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf2(skf2(X0)))|~ssPv2(skf2(skf2(X0)))|~ssPv1(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f352,f44])).
% 10.23/1.77  fof(f676,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf3(skf3(X0)))|~ssPv3(X0)|~ssPv3(skf3(X0))|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f143,f43])).
% 10.23/1.77  fof(f677,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf3(skf3(X0)))|~ssPv3(X0)|~ssPv3(skf3(X0))|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f145,f43])).
% 10.23/1.77  fof(f680,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv3(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f640,f453])).
% 10.23/1.77  fof(f688,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv2(X0)|ssPv3(skf3(X0))|~ssPv3(X0)|~ssPv1(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f615,f383])).
% 10.23/1.77  fof(f696,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv2(X0)|ssPv3(skf3(X0))|~ssPv3(X0)|~ssPv1(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f688])).
% 10.23/1.77  fof(f697,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(skf3(X0))|~ssPv3(X0)|~ssPv1(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f696,f245])).
% 10.23/1.77  fof(f706,plain,(
% 10.23/1.77    ![X0]: (ssPv1(skf3(X0))|ssPv2(skf2(X0))|ssPv3(X0)|~ssPv1(X0)|ssPv3(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f618,f520])).
% 10.23/1.77  fof(f720,plain,(
% 10.23/1.77    ![X0]: (ssPv1(skf3(X0))|ssPv2(skf2(X0))|ssPv3(X0)|~ssPv1(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f706])).
% 10.23/1.77  fof(f728,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf3(skf2(X0)))|ssPv4(X0)|ssPv2(X0)|ssPv4(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f294,f43])).
% 10.23/1.77  fof(f759,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(X0)|ssPv2(skf2(X0))|ssPv4(skf2(X0))|ssPv3(X0)|ssPv2(X0)|ssPv4(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f248,f590])).
% 10.23/1.77  fof(f763,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(X0)|ssPv2(skf2(X0))|ssPv4(skf2(X0))|ssPv3(X0)|ssPv2(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f759])).
% 10.23/1.77  fof(f764,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv4(skf2(X0))|ssPv3(X0)|ssPv2(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f763,f427])).
% 10.23/1.77  fof(f807,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(skf3(skf3(X0)))|~ssPv2(X0)|ssPv4(X0)|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f304,f43])).
% 10.23/1.77  fof(f824,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(skf3(X0))|~ssPv2(skf2(X0))|ssPv4(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f306,f43])).
% 10.23/1.77  fof(f833,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf2(X0))|ssPv4(skf2(X0))|ssPv4(X0)|ssPv4(X0)|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f824,f680])).
% 10.23/1.77  fof(f838,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf2(X0))|ssPv4(skf2(X0))|ssPv4(X0)|ssPv3(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f833])).
% 10.23/1.77  fof(f840,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf3(skf3(X0)))|~ssPv4(skf3(X0))|ssPv4(X0)|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f320,f43])).
% 10.23/1.77  fof(f847,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf3(X0))|~ssPv2(skf3(X0))|ssPv1(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f326,f43])).
% 10.23/1.77  fof(f852,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf3(skf2(X0)))|~ssPv2(X0)|ssPv1(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f328,f43])).
% 10.23/1.77  fof(f853,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(X0)|~ssPv2(X0)|ssPv1(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f328,f44])).
% 10.23/1.77  fof(f893,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf2(X0))|~ssPv3(skf2(X0))|ssPv4(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f334,f43])).
% 10.23/1.77  fof(f896,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(skf2(X0))|ssPv4(skf3(X0))|ssPv2(X0)|ssPv2(skf2(X0))|ssPv3(X0)|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f893,f764])).
% 10.23/1.77  fof(f900,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(skf2(X0))|ssPv4(skf3(X0))|ssPv2(X0)|ssPv2(skf2(X0))|ssPv3(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f896])).
% 10.23/1.77  fof(f901,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv2(X0)|ssPv2(skf2(X0))|ssPv3(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f900,f460])).
% 10.23/1.77  fof(f904,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf2(X0))|ssPv3(X0)|~ssPv2(skf3(X0))|ssPv1(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f901,f847])).
% 10.23/1.77  fof(f920,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf2(X0))|ssPv3(X0)|~ssPv2(skf3(X0))|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f904])).
% 10.23/1.77  fof(f921,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf2(X0))|ssPv3(X0)|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f920,f431])).
% 10.23/1.77  fof(f932,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv1(skf3(X0))|~ssPv1(X0)|ssPv4(skf2(X0))|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f921,f244])).
% 10.23/1.77  fof(f940,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv1(skf3(X0))|~ssPv1(X0)|ssPv4(skf2(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f932])).
% 10.23/1.77  fof(f941,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv1(skf3(X0))|ssPv4(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f940,f547])).
% 10.23/1.77  fof(f943,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv1(skf3(X0))|~ssPv3(skf2(X0))|ssPv4(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f941,f893])).
% 10.23/1.77  fof(f963,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv1(skf3(X0))|~ssPv3(skf2(X0))|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f943])).
% 10.23/1.77  fof(f964,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv1(skf3(X0))|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f963,f460])).
% 10.23/1.77  fof(f974,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv1(skf3(X0))|~ssPv2(skf3(X0))|ssPv1(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f964,f847])).
% 10.23/1.77  fof(f990,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv1(skf3(X0))|~ssPv2(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f974])).
% 10.23/1.77  fof(f991,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f990,f431])).
% 10.23/1.77  fof(f1008,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|~ssPv4(X0)|ssPv3(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f991,f245])).
% 10.23/1.77  fof(f1014,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|~ssPv4(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1008])).
% 10.23/1.77  fof(f1015,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1014,f680])).
% 10.23/1.77  fof(f1016,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(skf3(X0))|~ssPv1(skf3(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f697,f1015])).
% 10.23/1.77  fof(f1020,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|~ssPv4(X0)|ssPv4(skf3(X0))|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1015,f235])).
% 10.23/1.77  fof(f1025,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|~ssPv4(X0)|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1020])).
% 10.23/1.77  fof(f1026,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1025,f427])).
% 10.23/1.77  fof(f1030,plain,(
% 10.23/1.77    ![X0,X1]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssPv3(skf2(X1))|ssPv4(skf3(X1))|ssPv3(X1))),
% 10.23/1.77    inference(resolution,[status(thm)],[f310,f44])).
% 10.23/1.77  fof(f1050,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf3(X0))|~ssPv2(skf2(X0))|~ssPv1(skf2(X0))|~ssPv1(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f371,f43])).
% 10.23/1.77  fof(f1091,plain,(
% 10.23/1.77    ![X0,X1]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssPv1(skf3(X1))|~ssPv1(skf2(X1))|~ssPv3(X1))),
% 10.23/1.77    inference(resolution,[status(thm)],[f365,f44])).
% 10.23/1.77  fof(f1094,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv3(skf2(X0))|~ssPv2(X0)|ssPv1(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1026,f852])).
% 10.23/1.77  fof(f1095,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|~ssPv4(X0)|~ssPv3(skf3(X0))|ssPv3(skf3(skf3(X0))))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1026,f388])).
% 10.23/1.77  fof(f1111,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv3(skf2(X0))|~ssPv2(X0)|ssPv1(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1094])).
% 10.23/1.77  fof(f1112,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv3(skf2(X0))|ssPv1(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1111,f430])).
% 10.23/1.77  fof(f1113,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|~ssPv3(skf3(X0))|ssPv3(skf3(skf3(X0))))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1095,f427])).
% 10.23/1.77  fof(f1124,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|ssPv2(skf2(X0))|ssPv3(skf2(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f558,f1112])).
% 10.23/1.77  fof(f1146,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv3(skf2(X0))|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f524,f1124])).
% 10.23/1.77  fof(f1152,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|ssPv2(skf2(X0))|~ssPv1(skf3(X0))|~ssPv1(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1124,f641])).
% 10.23/1.77  fof(f1161,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|ssPv2(skf2(X0))|~ssPv1(skf3(X0))|~ssPv1(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1152])).
% 10.23/1.77  fof(f1162,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|ssPv2(skf2(X0))|~ssPv1(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1161,f720])).
% 10.23/1.77  fof(f1163,plain,(
% 10.23/1.77    ![X0]: (~ssPv1(X0)|ssPv4(skf2(X0))|ssPv3(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f244,f1162])).
% 10.23/1.77  fof(f1174,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv2(skf2(X0))|ssPv3(skf3(X0))|~ssPv3(X0)|ssPv1(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1146,f448])).
% 10.23/1.77  fof(f1185,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv2(skf2(X0))|ssPv3(skf3(X0))|ssPv1(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1174,f680])).
% 10.23/1.77  fof(f1220,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv2(skf2(X0))|ssPv1(X0)|~ssPv2(X0)|~ssPv3(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1185,f137])).
% 10.23/1.77  fof(f1228,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv2(skf2(X0))|ssPv1(X0)|~ssPv2(X0)|~ssPv3(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1220])).
% 10.23/1.77  fof(f1229,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv1(X0)|~ssPv2(X0)|~ssPv3(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1228,f853])).
% 10.23/1.77  fof(f1250,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|ssPv3(skf3(skf3(X0))))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1113,f1015])).
% 10.23/1.77  fof(f1251,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|~ssPv2(skf3(X0))|~ssPv3(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1250,f643])).
% 10.23/1.77  fof(f1261,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|~ssPv2(skf3(X0))|~ssPv3(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1251])).
% 10.23/1.77  fof(f1262,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0)|~ssPv3(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1261,f431])).
% 10.23/1.77  fof(f1265,plain,(
% 10.23/1.77    ![X0,X1]: (~ssRr(skf3(X0),X1)|~ssPv4(X1)|ssPv1(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f218,f1275])).
% 10.23/1.77  fof(f1266,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf2(X0))|ssPv1(skf2(X0))|ssPv3(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f238,f1275])).
% 10.23/1.77  fof(f1270,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(X0)|ssPv1(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f515,f1275])).
% 10.23/1.77  fof(f1275,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1262,f1015])).
% 10.23/1.77  fof(f1295,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf3(X0))|ssPv4(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1275,f198])).
% 10.23/1.77  fof(f1297,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv3(skf3(X0))|ssPv1(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f1185,f1270])).
% 10.23/1.77  fof(f1308,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv1(X0)|~ssPv4(X0)|ssPv4(skf3(X0))|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1297,f235])).
% 10.23/1.77  fof(f1314,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|~ssPv4(X0)|ssPv4(skf3(X0))|ssPv3(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1308,f1162])).
% 10.23/1.77  fof(f1349,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf3(X0))|ssPv4(X0)|~ssPv3(skf2(X0))|ssPv4(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1295,f893])).
% 10.23/1.77  fof(f1353,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf3(X0))|ssPv4(X0)|~ssPv3(X0)|ssPv4(X0)|ssPv3(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1295,f514])).
% 10.23/1.77  fof(f1369,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf3(X0))|ssPv4(X0)|~ssPv3(skf2(X0))|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1349])).
% 10.23/1.77  fof(f1370,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf3(X0))|ssPv4(X0)|~ssPv3(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1369,f247])).
% 10.23/1.77  fof(f1374,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf3(X0))|ssPv4(X0)|~ssPv3(X0)|ssPv3(skf2(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1353])).
% 10.23/1.77  fof(f1375,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf3(X0))|ssPv4(X0)|ssPv3(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1374,f1275])).
% 10.23/1.77  fof(f1389,plain,(
% 10.23/1.77    ![X0]: (~ssPv1(X0)|ssPv2(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f160,f1390])).
% 10.23/1.77  fof(f1390,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf3(X0))|ssPv4(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1375,f1370])).
% 10.23/1.77  fof(f1394,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv4(skf2(X0))|ssPv4(X0)|ssPv2(X0)|ssPv4(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1390,f728])).
% 10.23/1.77  fof(f1399,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv4(skf2(X0))|ssPv4(X0)|ssPv2(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1394])).
% 10.23/1.77  fof(f1428,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv4(X0)|ssPv2(X0)|~ssPv3(skf2(X0))|ssPv4(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1399,f893])).
% 10.23/1.77  fof(f1448,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv4(X0)|ssPv2(X0)|~ssPv3(skf2(X0))|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1428])).
% 10.23/1.77  fof(f1449,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv4(X0)|ssPv2(X0)|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1448,f1275])).
% 10.23/1.77  fof(f1466,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv4(X0)|ssPv2(X0)|~ssPv3(skf2(X0))|ssPv2(X0)|ssPv4(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1449,f247])).
% 10.23/1.77  fof(f1481,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv4(X0)|ssPv2(X0)|~ssPv3(skf2(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1466])).
% 10.23/1.77  fof(f1482,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv4(X0)|ssPv2(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1481,f1275])).
% 10.23/1.77  fof(f1485,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv2(skf3(X0))|~ssPv3(X0)|~ssPv3(skf3(X0))|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1482,f346])).
% 10.23/1.77  fof(f1494,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv2(skf3(X0))|~ssPv3(X0)|~ssPv3(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1485])).
% 10.23/1.77  fof(f1495,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv2(skf3(X0))|~ssPv3(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1494,f1275])).
% 10.23/1.77  fof(f1504,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(skf3(X0)))|ssPv2(skf3(skf3(X0)))|ssPv4(X0)|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1495,f680])).
% 10.23/1.77  fof(f1507,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv2(skf3(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1495,f1275])).
% 10.23/1.77  fof(f1511,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf3(skf3(X0)))|ssPv2(skf3(X0))|~ssPv3(X0)|~ssPv3(skf3(X0))|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1507,f676])).
% 10.23/1.77  fof(f1518,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf3(X0))|ssPv2(X0)|~ssPv3(skf2(X0))|~ssPv3(X0)|ssPv1(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1507,f356])).
% 10.23/1.77  fof(f1530,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf3(X0))|~ssPv3(X0)|~ssPv3(skf3(X0))|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1511,f677])).
% 10.23/1.77  fof(f1533,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|~ssPv3(skf2(X0))|~ssPv3(X0)|ssPv1(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1518,f360])).
% 10.23/1.77  fof(f1540,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|~ssPv3(skf2(X0))|ssPv1(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1533,f1275])).
% 10.23/1.77  fof(f1543,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv1(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1540,f1275])).
% 10.23/1.77  fof(f1553,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf2(skf3(X0)))|ssPv1(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1265,f44])).
% 10.23/1.77  fof(f1563,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(skf3(X0))|~ssPv1(skf3(X0))|~ssPv1(skf2(X0))|~ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1091,f43])).
% 10.23/1.77  fof(f1571,plain,(
% 10.23/1.77    ![X0]: (~ssPv1(skf3(X0))|~ssPv1(skf2(X0))|~ssPv3(X0)|ssPv2(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1563,f1275])).
% 10.23/1.77  fof(f1584,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv1(X0)|~ssPv3(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f1229,f1543])).
% 10.23/1.77  fof(f1586,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(X0)|ssPv1(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f853,f1543])).
% 10.23/1.77  fof(f1769,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf2(X0))|ssPv4(X0)|ssPv3(skf2(X0))|ssPv2(X0)|ssPv3(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f513,f566])).
% 10.23/1.77  fof(f1773,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf2(X0))|ssPv4(X0)|ssPv3(skf2(X0))|ssPv2(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f1769])).
% 10.23/1.77  fof(f1794,plain,(
% 10.23/1.77    ![X0]: (~ssPv1(skf2(X0))|~ssPv3(X0)|ssPv2(skf3(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f1571,f1795])).
% 10.23/1.77  fof(f1795,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf3(X0))|~ssPv3(X0)|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f1530,f1275])).
% 10.23/1.77  fof(f1999,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(skf3(X0))|~ssPv3(skf2(X0))|ssPv4(skf3(X0))|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1030,f43])).
% 10.23/1.77  fof(f2008,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(skf3(X0))|ssPv4(skf3(X0))|ssPv3(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1999,f1275])).
% 10.23/1.77  fof(f2071,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv3(X0)|ssPv2(skf2(X0))|ssPv2(skf2(X0))|ssPv1(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2008,f1297])).
% 10.23/1.77  fof(f2072,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv3(X0)|ssPv2(skf2(X0))|ssPv4(X0)|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2008,f680])).
% 10.23/1.77  fof(f2075,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv3(X0)|ssPv2(skf2(X0))|ssPv1(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f2071])).
% 10.23/1.77  fof(f2076,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv2(skf2(X0))|ssPv1(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2075,f1584])).
% 10.23/1.77  fof(f2077,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv3(X0)|ssPv2(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f2072])).
% 10.23/1.77  fof(f2078,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf3(X0))|ssPv3(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2077,f1314])).
% 10.23/1.77  fof(f2093,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv1(X0)|~ssPv3(skf3(X0))|ssPv1(X0)|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2076,f164])).
% 10.23/1.77  fof(f2111,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv1(X0)|~ssPv3(skf3(X0))|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f2093])).
% 10.23/1.77  fof(f2112,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv1(X0)|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2111,f1297])).
% 10.23/1.77  fof(f2396,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf3(skf3(X0)))|ssPv4(X0)|ssPv3(X0)|~ssPv1(skf3(X0))|~ssPv4(skf3(X0))|ssPv1(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f1504,f653])).
% 10.23/1.77  fof(f2419,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv3(X0)|~ssPv1(skf3(X0))|~ssPv4(skf3(X0))|ssPv1(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2396,f840])).
% 10.23/1.77  fof(f2430,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv3(X0)|~ssPv1(skf3(X0))|ssPv1(X0)|ssPv3(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2419,f2078])).
% 10.23/1.77  fof(f2436,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv3(X0)|~ssPv1(skf3(X0))|ssPv1(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f2430])).
% 10.23/1.77  fof(f2437,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|~ssPv1(skf3(X0))|ssPv1(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2436,f1586])).
% 10.23/1.77  fof(f2528,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv1(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f2112,f2530])).
% 10.23/1.77  fof(f2530,plain,(
% 10.23/1.77    ![X0]: (~ssPv1(skf3(X0))|ssPv1(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2437,f1584])).
% 10.23/1.77  fof(f2537,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f1162,f2528])).
% 10.23/1.77  fof(f2547,plain,(
% 10.23/1.77    ![X0]: (ssPv1(X0)|ssPv4(skf2(X0))|ssPv4(X0)|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2528,f838])).
% 10.23/1.77  fof(f2556,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf2(X0))|ssPv4(X0)|ssPv3(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2547,f1163])).
% 10.23/1.77  fof(f2559,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(skf3(X0))|~ssPv2(X0)|ssPv2(skf2(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f137,f2537])).
% 10.23/1.77  fof(f2564,plain,(
% 10.23/1.77    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssRr(X1,X2)|ssPv2(X2)|ssPv3(X1))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f317,f2537])).
% 10.23/1.77  fof(f2571,plain,(
% 10.23/1.77    ![X0]: (ssPv3(skf3(X0))|~ssPv2(skf3(X0))|~ssPv4(skf3(X0))|ssPv4(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2537,f390])).
% 10.23/1.77  fof(f2577,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|~ssPv2(X0)|~ssPv4(X0)|ssPv4(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2537,f132])).
% 10.23/1.77  fof(f2584,plain,(
% 10.23/1.77    ![X0]: (ssPv3(skf3(X0))|~ssPv4(skf3(X0))|ssPv4(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2571,f1275])).
% 10.23/1.77  fof(f2586,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|~ssPv4(X0)|ssPv4(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2577,f1275])).
% 10.23/1.77  fof(f2635,plain,(
% 10.23/1.77    ![X0]: (ssPv1(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f1553,f2637])).
% 10.23/1.77  fof(f2636,plain,(
% 10.23/1.77    ![X0]: (ssPv1(skf2(X0))|ssPv3(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f1266,f2637])).
% 10.23/1.77  fof(f2637,plain,(
% 10.23/1.77    ![X0]: (ssPv3(X0)|ssPv4(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2586,f2556])).
% 10.23/1.77  fof(f2640,plain,(
% 10.23/1.77    ![X0]: (ssPv3(skf2(X0))|~ssPv2(skf2(skf2(X0)))|~ssPv1(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2637,f661])).
% 10.23/1.77  fof(f2666,plain,(
% 10.23/1.77    ![X0]: (ssPv3(skf2(X0))|~ssPv1(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2640,f2537])).
% 10.23/1.77  fof(f2677,plain,(
% 10.23/1.77    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv3(X0)|~ssRr(X1,X2)|~ssPv2(X1)|ssPv2(X2))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f84,f2564])).
% 10.23/1.77  fof(f2689,plain,(
% 10.23/1.77    ![X0]: (ssPv1(skf3(X0))|~ssPv2(X0)|ssPv4(X0)|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2635,f807])).
% 10.23/1.77  fof(f2694,plain,(
% 10.23/1.77    ![X0]: (ssPv1(X0)|~ssPv2(skf2(X0))|ssPv4(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2635,f824])).
% 10.23/1.77  fof(f2702,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(X0)|ssPv4(X0)|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2689,f511])).
% 10.23/1.77  fof(f2703,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf2(X0))|ssPv4(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2694,f234])).
% 10.23/1.77  fof(f2704,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(X0)|ssPv1(skf2(X0))|ssPv1(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f165,f2636])).
% 10.23/1.77  fof(f2717,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(X0)|~ssPv2(skf3(X0))|ssPv4(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f389,f2702])).
% 10.23/1.77  fof(f2729,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf3(X0))|~ssPv4(X0)|ssPv1(skf2(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f139,f2704])).
% 10.23/1.77  fof(f2780,plain,(
% 10.23/1.77    ![X0]: (ssPv3(skf2(X0))|ssPv4(X0)|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2666,f2636])).
% 10.23/1.77  fof(f2832,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf2(X0))|~ssPv2(X0)|ssPv4(skf2(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f132,f2703])).
% 10.23/1.77  fof(f2834,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf2(X0))|ssPv4(X0)|ssPv1(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2703,f2528])).
% 10.23/1.77  fof(f2835,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf2(X0))|ssPv4(X0)|ssPv4(X0)|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2703,f1482])).
% 10.23/1.77  fof(f2836,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf2(X0))|ssPv4(X0)|ssPv2(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f2835])).
% 10.23/1.77  fof(f2846,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv1(X0)|ssPv4(X0)|ssPv3(skf2(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2834,f1773])).
% 10.23/1.77  fof(f2863,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv1(X0)|ssPv3(skf2(X0))|ssPv2(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f2846])).
% 10.23/1.77  fof(f2864,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv1(X0)|ssPv2(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2863,f1540])).
% 10.23/1.77  fof(f2900,plain,(
% 10.23/1.77    ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv1(skf2(X0))|ssPv1(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2864,f2704])).
% 10.23/1.77  fof(f2913,plain,(
% 10.23/1.77    ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv1(skf2(X0)))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f2900])).
% 10.23/1.77  fof(f2937,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv3(skf2(X0))|ssPv2(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f1773,f2836])).
% 10.23/1.77  fof(f2976,plain,(
% 10.23/1.77    ![X0]: (ssPv1(X0)|ssPv2(X0)|~ssPv3(X0)|ssPv2(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2913,f1794])).
% 10.23/1.77  fof(f2983,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|~ssPv3(X0)|ssPv2(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2976,f1389])).
% 10.23/1.77  fof(f2997,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv2(X0)|~ssPv2(skf2(X0))|~ssPv3(X0)|ssPv4(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2937,f347])).
% 10.23/1.77  fof(f3003,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv2(X0)|~ssPv2(skf2(X0))|~ssPv3(X0))),
% 10.23/1.77    inference(duplicate_literals_removal,[status(thm)],[f2997])).
% 10.23/1.77  fof(f3004,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv2(X0)|~ssPv3(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3003,f1482])).
% 10.23/1.77  fof(f3011,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f2703,f3013])).
% 10.23/1.77  fof(f3012,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv4(skf3(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f2702,f3013])).
% 10.23/1.77  fof(f3013,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv2(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3004,f1275])).
% 10.23/1.77  fof(f3054,plain,(
% 10.23/1.77    ![X0,X1]: (~ssRr(X0,skf2(X1))|~ssPv3(X0)|ssPv4(X1)|ssPv3(skf2(X1)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f217,f3011])).
% 10.23/1.77  fof(f3059,plain,(
% 10.23/1.77    ![X0,X1]: (~ssRr(X0,X1)|~ssPv2(X0)|ssPv4(skf2(X1))|ssPv3(skf2(X1)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f322,f3011])).
% 10.23/1.77  fof(f3092,plain,(
% 10.23/1.77    ![X0]: (ssPv3(skf3(X0))|ssPv4(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f2584,f3012])).
% 10.23/1.77  fof(f3127,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv2(skf3(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2983,f1275])).
% 10.23/1.77  fof(f3163,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(X0)|ssPv4(X0)|ssPv3(skf2(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f3054,f44])).
% 10.23/1.77  fof(f3164,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0)|ssPv3(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3163,f2780])).
% 10.23/1.77  fof(f3168,plain,(
% 10.23/1.77    ![X0,X1]: (~ssRr(X0,X1)|~ssPv2(X0)|ssPv3(skf2(X1))|ssPv2(X1))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f340,f3059])).
% 10.23/1.77  fof(f3177,plain,(
% 10.23/1.77    ![X0,X1]: (~ssRr(X0,skf3(X1))|~ssPv3(X0)|~ssPv2(skf3(X1))|ssPv2(X1))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2677,f43])).
% 10.23/1.77  fof(f3179,plain,(
% 10.23/1.77    ![X0,X1]: (~ssRr(X0,skf3(X1))|~ssPv3(X0)|ssPv2(X1))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3177,f3127])).
% 10.23/1.77  fof(f3185,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf3(X0))|ssPv4(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2717,f3013])).
% 10.23/1.77  fof(f3197,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(skf3(skf3(X0)))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f3179,f43])).
% 10.23/1.77  fof(f3199,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv1(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f3197,f2635])).
% 10.23/1.77  fof(f3202,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(X0)|ssPv2(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f2559,f3092])).
% 10.23/1.77  fof(f3205,plain,(
% 10.23/1.77    ![X0]: (ssPv2(skf2(X0))|ssPv4(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3202,f3013])).
% 10.23/1.77  fof(f3209,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(X0)|ssPv4(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f2832,f3013])).
% 10.23/1.77  fof(f3232,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf2(X0))|~ssPv3(X0)|ssPv4(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f347,f3164])).
% 10.23/1.77  fof(f3257,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f1016,f3199])).
% 10.23/1.77  fof(f3379,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf3(X0))|ssPv3(skf2(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f3168,f43])).
% 10.23/1.77  fof(f3381,plain,(
% 10.23/1.77    ![X0]: (ssPv3(skf2(X0))|ssPv2(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3379,f3127])).
% 10.23/1.77  fof(f3533,plain,(
% 10.23/1.77    ![X0,X1,X2]: (~ssRr(X0,X1)|~ssRr(X1,X2)|~ssPv4(X2)|~ssPv3(X1)|ssPv3(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f80,f3534])).
% 10.23/1.77  fof(f3534,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(X0)|ssPv4(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3232,f3205])).
% 10.23/1.77  fof(f3538,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf2(X0))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f3534,f3381])).
% 10.23/1.77  fof(f3541,plain,(
% 10.23/1.77    ![X0]: (ssPv4(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3538,f3209])).
% 10.23/1.77  fof(f3553,plain,(
% 10.23/1.77    ![X0,X1]: (~ssRr(X0,X1)|~ssPv4(skf2(X1))|~ssPv3(X1)|ssPv3(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f3533,f44])).
% 10.23/1.77  fof(f3554,plain,(
% 10.23/1.77    ![X0,X1]: (~ssRr(X0,X1)|~ssPv3(X1)|ssPv3(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3553,f3541])).
% 10.23/1.77  fof(f3567,plain,(
% 10.23/1.77    ![X0]: (~ssPv3(X0)|ssPv3(skf3(X0)))),
% 10.23/1.77    inference(resolution,[status(thm)],[f3554,f43])).
% 10.23/1.77  fof(f3571,plain,(
% 10.23/1.77    ![X0]: (ssPv3(skf3(skf3(X0)))|ssPv2(X0))),
% 10.23/1.77    inference(resolution,[status(thm)],[f3567,f3257])).
% 10.23/1.77  fof(f3577,plain,(
% 10.23/1.77    ![X0]: (ssPv2(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3571,f3197])).
% 10.23/1.77  fof(f3584,plain,(
% 10.23/1.77    ![X0]: (~ssPv2(skf2(X0))|~ssPv1(skf2(X0))|~ssPv1(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f1050,f3577])).
% 10.23/1.77  fof(f3614,plain,(
% 10.23/1.77    ![X0]: (ssPv4(X0))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f3185,f3577])).
% 10.23/1.77  fof(f3617,plain,(
% 10.23/1.77    ![X0]: (~ssPv1(skf2(X0))|~ssPv1(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3584,f3577])).
% 10.23/1.77  fof(f3636,plain,(
% 10.23/1.77    ![X0]: (~ssPv4(skf3(X0))|ssPv1(skf2(X0)))),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f2729,f3614])).
% 10.23/1.77  fof(f3643,plain,(
% 10.23/1.77    ![X0]: (ssPv1(skf2(X0)))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3636,f3614])).
% 10.23/1.77  fof(f3695,plain,(
% 10.23/1.77    ![X0]: (~ssPv1(X0))),
% 10.23/1.77    inference(forward_subsumption_resolution,[status(thm)],[f3617,f3643])).
% 10.23/1.77  fof(f3696,plain,(
% 10.23/1.77    $false),
% 10.23/1.77    inference(backward_subsumption_resolution,[status(thm)],[f3643,f3695])).
% 10.23/1.77  % SZS output end CNFRefutation for theBenchmark.p
% 10.23/1.77  % Elapsed time: 1.395088 seconds
% 10.23/1.77  % CPU time: 10.791531 seconds
% 10.23/1.77  % Total memory used: 56.951 MB
% 10.23/1.77  % Net memory used: 41.420 MB
%------------------------------------------------------------------------------