%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN759-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:20:29 PM UTC 2026
% Result : Unsatisfiable 122.32s 16.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN759-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n002.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 11:18:01 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 122.32/16.03 % Refutation found
% 122.32/16.03 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 122.32/16.03 % SZS output start CNFRefutation for theBenchmark
% 122.32/16.03 fof(f1,negated_conjecture,(
% 122.32/16.03 (![U]: (ssRr(U,skf1(U)) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f2,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ssPv1(V)| ssPv2(X)| ssPv2(W)| ssPv3(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f3,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv1(X)| ssPv1(V)| ssPv3(W)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f5,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv3(X)| ssPv2(V)| ssPv2(W)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f6,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv3(W)| ssPv3(V)| ssPv3(X)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f7,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv4(X)| ~ ssPv1(W)| ssPv3(V)| ssPv2(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f8,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv3(X)| ~ ssPv4(W)| ssPv4(V)| ssPv1(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f9,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv2(V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv1(X)| ~ ssPv4(W)| ssPv3(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f10,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X]: (( ~ ssRr(U,V)| ~ ssPv4(V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv2(X)| ~ ssPv3(W)| ssPv1(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f11,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssPv1(W)| ssPv3(V)| ssPv2(Y)| ssPv3(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f12,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssPv3(W)| ssPv4(V)| ssPv1(Y)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f13,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssPv1(V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssRr(W,Y)| ssPv3(X)| ssPv2(Y)| ssPv1(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f14,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv2(X)| ~ ssRr(W,Y)| ssPv4(V)| ssPv3(Y)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f15,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv3(X)| ~ ssRr(W,Y)| ssPv2(V)| ssPv2(Y)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f16,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssPv4(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ssPv3(Y)| ssPv1(W)| ssPv2(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f17,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv2(X)| ~ ssRr(W,Y)| ~ ssPv4(W)| ssPv3(V)| ssPv3(Y) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f19,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssPv1(W)| ssPv1(Y)| ssPv3(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f20,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv3(X)| ~ ssRr(W,Y)| ssPv1(Y)| ssPv1(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f21,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssPv2(W)| ~ ssPv3(W)| ssPv4(V)| ssPv2(Y) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f22,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssPv1(W)| ~ ssPv4(W)| ssPv3(V)| ssPv2(Y) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f23,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssPv2(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssPv2(W)| ssPv3(Y)| ssPv1(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f24,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssPv2(Y)| ~ ssRr(W,X)| ssPv1(W)| ssPv3(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f25,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssPv2(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssPv1(W)| ssPv3(Y)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f26,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssPv1(V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv4(X)| ~ ssRr(W,Y)| ~ ssPv3(Y)| ssPv2(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f28,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssPv4(V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv4(X)| ~ ssRr(W,Y)| ~ ssPv3(Y)| ssPv2(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f29,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(W,X)| ~ ssPv4(X)| ~ ssRr(W,Y)| ~ ssPv3(Y)| ~ ssPv1(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f30,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ssPv3(V)| ssPv2(Y)| ssPv1(Z)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f32,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ssPv4(Y)| ssPv2(Z)| ssPv2(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f33,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv1(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ssPv4(Y)| ssPv3(Z)| ssPv1(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f34,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ~ ssPv2(Z)| ssPv2(V)| ssPv1(Y)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f35,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ssPv2(Y)| ssPv1(Z)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f36,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv2(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssPv1(Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ssPv4(Z)| ssPv2(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f37,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssPv2(Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ssPv1(Z)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f39,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ~ ssPv1(Z)| ssPv4(Y)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f41,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv4(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssPv3(Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ssPv4(Z)| ssPv2(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f43,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv4(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ~ ssPv4(Z)| ssPv3(Y)| ssPv1(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f44,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssPv1(Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ~ ssPv1(W)| ssPv3(Z) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f45,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ~ ssPv3(Z)| ~ ssPv2(W)| ssPv2(Y) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f46,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z]: (( ~ ssRr(U,V)| ~ ssPv4(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssPv2(Y)| ~ ssRr(W,X)| ~ ssRr(W,Z)| ~ ssPv1(Z)| ssPv4(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f48,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z,X1]: (( ~ ssRr(U,V)| ~ ssPv3(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssPv2(Y)| ~ ssRr(W,X)| ~ ssRr(Z,X1)| ~ ssRr(W,Z)| ssPv1(X1)| ssPv1(W) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f50,negated_conjecture,(
% 122.32/16.03 (![U,V,W,X,Y,Z,X1]: (( ~ ssRr(U,V)| ~ ssPv2(V)| ~ ssRr(W,U)| ~ ssRr(X,Y)| ~ ssPv1(Y)| ~ ssRr(W,X)| ~ ssRr(Z,X1)| ~ ssRr(W,Z)| ~ ssPv3(W)| ssPv2(X1) ) ))),
% 122.32/16.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.32/16.03 fof(f52,plain,(
% 122.32/16.03 ![X0]: (ssRr(X0,skf1(X0)))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f1])).
% 122.32/16.03 fof(f53,plain,(
% 122.32/16.03 ![W]: (((![X]: ((![V]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(W,X))|ssPv1(V)))|ssPv2(X)))|ssPv2(W))|ssPv3(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f2])).
% 122.32/16.03 fof(f54,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|ssPv1(X1)|ssPv2(X3)|ssPv2(X2)|ssPv3(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f53])).
% 122.32/16.03 fof(f55,plain,(
% 122.32/16.03 ![W]: (((![V]: ((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(W,X))|~ssPv1(X)))|ssPv1(V)))|ssPv3(W))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f3])).
% 122.32/16.03 fof(f56,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv1(X3)|ssPv1(X1)|ssPv3(X2)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f55])).
% 122.32/16.03 fof(f59,plain,(
% 122.32/16.03 ![W]: (((![V]: ((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(W,X))|~ssPv3(X)))|ssPv2(V)))|ssPv2(W))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f5])).
% 122.32/16.03 fof(f60,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv3(X3)|ssPv2(X1)|ssPv2(X2)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f59])).
% 122.32/16.03 fof(f61,plain,(
% 122.32/16.03 ![W]: ((![X]: ((![V]: ((((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(W,X))|~ssPv3(W))|ssPv3(V)))|ssPv3(X)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f6])).
% 122.32/16.03 fof(f62,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv3(X2)|ssPv3(X1)|ssPv3(X3)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f61])).
% 122.32/16.03 fof(f63,plain,(
% 122.32/16.03 ![W]: ((![V]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(W,X))|~ssPv4(X)))|~ssPv1(W))|ssPv3(V)))|ssPv2(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f7])).
% 122.32/16.03 fof(f64,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv4(X3)|~ssPv1(X2)|ssPv3(X1)|ssPv2(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f63])).
% 122.32/16.03 fof(f65,plain,(
% 122.32/16.03 ![W]: ((![V]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(W,X))|~ssPv3(X)))|~ssPv4(W))|ssPv4(V)))|ssPv1(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f8])).
% 122.32/16.03 fof(f66,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv3(X3)|~ssPv4(X2)|ssPv4(X1)|ssPv1(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f65])).
% 122.32/16.03 fof(f67,plain,(
% 122.32/16.03 ![W]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv2(V)))|~ssRr(W,U)))|~ssRr(W,X))|~ssPv1(X)))|~ssPv4(W))|ssPv3(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f9])).
% 122.32/16.03 fof(f68,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv1(X3)|~ssPv4(X2)|ssPv3(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f67])).
% 122.32/16.03 fof(f69,plain,(
% 122.32/16.03 ![W]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv4(V)))|~ssRr(W,U)))|~ssRr(W,X))|~ssPv2(X)))|~ssPv3(W))|ssPv1(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f10])).
% 122.32/16.03 fof(f70,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv2(X3)|~ssPv3(X2)|ssPv1(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f69])).
% 122.32/16.03 fof(f71,plain,(
% 122.32/16.03 ![W]: ((![Y]: ((![V]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssPv1(W))|ssPv3(V)))|ssPv2(Y)))|ssPv3(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f11])).
% 122.32/16.03 fof(f72,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssPv1(X2)|ssPv3(X1)|ssPv2(X4)|ssPv3(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f71])).
% 122.32/16.03 fof(f73,plain,(
% 122.32/16.03 ![W]: ((![Y]: ((![V]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssPv3(W))|ssPv4(V)))|ssPv1(Y)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f12])).
% 122.32/16.03 fof(f74,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssPv3(X2)|ssPv4(X1)|ssPv1(X4)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f73])).
% 122.32/16.03 fof(f75,plain,(
% 122.32/16.03 ![W]: ((![Y]: ((![X]: ((((![U]: ((![V]: (~ssRr(U,V)|~ssPv1(V)))|~ssRr(W,U)))|~ssRr(W,X))|~ssRr(W,Y))|ssPv3(X)))|ssPv2(Y)))|ssPv1(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f13])).
% 122.32/16.03 fof(f76,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv1(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssRr(X2,X4)|ssPv3(X3)|ssPv2(X4)|ssPv1(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f75])).
% 122.32/16.03 fof(f77,plain,(
% 122.32/16.03 ![W]: ((![Y]: ((![V]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(W,X))|~ssPv2(X)))|~ssRr(W,Y))|ssPv4(V)))|ssPv3(Y)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f14])).
% 122.32/16.03 fof(f78,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv2(X3)|~ssRr(X2,X4)|ssPv4(X1)|ssPv3(X4)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f77])).
% 122.32/16.03 fof(f79,plain,(
% 122.32/16.03 ![W]: ((![Y]: ((![V]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(W,X))|~ssPv3(X)))|~ssRr(W,Y))|ssPv2(V)))|ssPv2(Y)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f15])).
% 122.32/16.03 fof(f80,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv3(X3)|~ssRr(X2,X4)|ssPv2(X1)|ssPv2(X4)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f79])).
% 122.32/16.03 fof(f81,plain,(
% 122.32/16.03 ![W]: (((![Y]: ((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv4(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|ssPv3(Y)))|ssPv1(W))|ssPv2(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f16])).
% 122.32/16.03 fof(f82,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|ssPv3(X4)|ssPv1(X2)|ssPv2(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f81])).
% 122.32/16.03 fof(f83,plain,(
% 122.32/16.03 ![Y]: ((![V]: ((![W]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(W,X))|~ssPv2(X)))|~ssRr(W,Y))|~ssPv4(W)))|ssPv3(V)))|ssPv3(Y))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f17])).
% 122.32/16.03 fof(f84,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv2(X3)|~ssRr(X2,X4)|~ssPv4(X2)|ssPv3(X1)|ssPv3(X4))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f83])).
% 122.32/16.03 fof(f87,plain,(
% 122.32/16.03 ![W]: ((![Y]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssPv1(W))|ssPv1(Y)))|ssPv3(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f19])).
% 122.32/16.03 fof(f88,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssPv1(X2)|ssPv1(X4)|ssPv3(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f87])).
% 122.32/16.03 fof(f89,plain,(
% 122.32/16.03 ![W]: ((![Y]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(W,X))|~ssPv3(X)))|~ssRr(W,Y))|ssPv1(Y)))|ssPv1(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f20])).
% 122.32/16.03 fof(f90,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv3(X3)|~ssRr(X2,X4)|ssPv1(X4)|ssPv1(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f89])).
% 122.32/16.03 fof(f91,plain,(
% 122.32/16.03 ![Y]: ((![V]: ((![W]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssPv2(W))|~ssPv3(W)))|ssPv4(V)))|ssPv2(Y))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f21])).
% 122.32/16.03 fof(f92,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssPv2(X2)|~ssPv3(X2)|ssPv4(X1)|ssPv2(X4))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f91])).
% 122.32/16.03 fof(f93,plain,(
% 122.32/16.03 ![Y]: ((![V]: ((![W]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssPv1(W))|~ssPv4(W)))|ssPv3(V)))|ssPv2(Y))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f22])).
% 122.32/16.03 fof(f94,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssPv1(X2)|~ssPv4(X2)|ssPv3(X1)|ssPv2(X4))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f93])).
% 122.32/16.03 fof(f95,plain,(
% 122.32/16.03 ![W]: ((![Y]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv2(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssPv2(W))|ssPv3(Y)))|ssPv1(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f23])).
% 122.32/16.03 fof(f96,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssPv2(X2)|ssPv3(X4)|ssPv1(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f95])).
% 122.32/16.03 fof(f97,plain,(
% 122.32/16.03 ![W]: (((![X]: ((![Y]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssPv2(Y)))|~ssRr(W,X)))|ssPv1(W))|ssPv3(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f24])).
% 122.32/16.03 fof(f98,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv2(X4)|~ssRr(X2,X3)|ssPv1(X2)|ssPv3(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f97])).
% 122.32/16.03 fof(f99,plain,(
% 122.32/16.03 ![W]: ((![Y]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv2(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssPv1(W))|ssPv3(Y)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f25])).
% 122.32/16.03 fof(f100,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssPv1(X2)|ssPv3(X4)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f99])).
% 122.32/16.03 fof(f101,plain,(
% 122.32/16.03 ![W]: ((![Y]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv1(V)))|~ssRr(W,U)))|~ssRr(W,X))|~ssPv4(X)))|~ssRr(W,Y))|~ssPv3(Y)))|ssPv2(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f26])).
% 122.32/16.03 fof(f102,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv1(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv4(X3)|~ssRr(X2,X4)|~ssPv3(X4)|ssPv2(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f101])).
% 122.32/16.03 fof(f105,plain,(
% 122.32/16.03 ![W]: ((![Y]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv4(V)))|~ssRr(W,U)))|~ssRr(W,X))|~ssPv4(X)))|~ssRr(W,Y))|~ssPv3(Y)))|ssPv2(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f28])).
% 122.32/16.03 fof(f106,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv4(X3)|~ssRr(X2,X4)|~ssPv3(X4)|ssPv2(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f105])).
% 122.32/16.03 fof(f107,plain,(
% 122.32/16.03 ![W]: ((![Y]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(W,X))|~ssPv4(X)))|~ssRr(W,Y))|~ssPv3(Y)))|~ssPv1(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f29])).
% 122.32/16.03 fof(f108,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv4(X3)|~ssRr(X2,X4)|~ssPv3(X4)|~ssPv1(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f107])).
% 122.32/16.03 fof(f109,plain,(
% 122.32/16.03 ![W]: ((![Z]: ((![Y]: ((![V]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssRr(W,Z))|ssPv3(V)))|ssPv2(Y)))|ssPv1(Z)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f30])).
% 122.32/16.03 fof(f110,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|ssPv3(X1)|ssPv2(X4)|ssPv1(X5)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f109])).
% 122.32/16.03 fof(f113,plain,(
% 122.32/16.03 ![W]: ((![Z]: ((![Y]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssRr(W,Z))|ssPv4(Y)))|ssPv2(Z)))|ssPv2(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f32])).
% 122.32/16.03 fof(f114,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|ssPv4(X4)|ssPv2(X5)|ssPv2(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f113])).
% 122.32/16.03 fof(f115,plain,(
% 122.32/16.03 ![W]: ((![Z]: ((![Y]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv1(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssRr(W,Z))|ssPv4(Y)))|ssPv3(Z)))|ssPv1(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f33])).
% 122.32/16.03 fof(f116,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv1(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|ssPv4(X4)|ssPv3(X5)|ssPv1(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f115])).
% 122.32/16.03 fof(f117,plain,(
% 122.32/16.03 ![W]: ((![Y]: ((![V]: ((![Z]: (((![X]: (((![U]: (~ssRr(U,V)|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssRr(W,Z))|~ssPv2(Z)))|ssPv2(V)))|ssPv1(Y)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f34])).
% 122.32/16.03 fof(f118,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|~ssPv2(X5)|ssPv2(X1)|ssPv1(X4)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f117])).
% 122.32/16.03 fof(f119,plain,(
% 122.32/16.03 ![W]: ((![Z]: ((![Y]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssRr(W,Z))|ssPv2(Y)))|ssPv1(Z)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f35])).
% 122.32/16.03 fof(f120,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|ssPv2(X4)|ssPv1(X5)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f119])).
% 122.32/16.03 fof(f121,plain,(
% 122.32/16.03 ![W]: ((![Z]: (((![X]: ((![Y]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv2(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssPv1(Y)))|~ssRr(W,X)))|~ssRr(W,Z))|ssPv4(Z)))|ssPv2(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f36])).
% 122.32/16.03 fof(f122,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv1(X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|ssPv4(X5)|ssPv2(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f121])).
% 122.32/16.03 fof(f123,plain,(
% 122.32/16.03 ![W]: ((![Z]: (((![X]: ((![Y]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssPv2(Y)))|~ssRr(W,X)))|~ssRr(W,Z))|ssPv1(Z)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f37])).
% 122.32/16.03 fof(f124,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv2(X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|ssPv1(X5)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f123])).
% 122.32/16.03 fof(f127,plain,(
% 122.32/16.03 ![W]: ((![Y]: ((![Z]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssRr(W,Z))|~ssPv1(Z)))|ssPv4(Y)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f39])).
% 122.32/16.03 fof(f128,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|~ssPv1(X5)|ssPv4(X4)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f127])).
% 122.32/16.03 fof(f131,plain,(
% 122.32/16.03 ![W]: ((![Z]: (((![X]: ((![Y]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv4(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssPv3(Y)))|~ssRr(W,X)))|~ssRr(W,Z))|ssPv4(Z)))|ssPv2(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f41])).
% 122.32/16.03 fof(f132,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv3(X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|ssPv4(X5)|ssPv2(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f131])).
% 122.32/16.03 fof(f135,plain,(
% 122.32/16.03 ![W]: ((![Y]: ((![Z]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv4(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssRr(W,Z))|~ssPv4(Z)))|ssPv3(Y)))|ssPv1(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f43])).
% 122.32/16.03 fof(f136,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|~ssPv4(X5)|ssPv3(X4)|ssPv1(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f135])).
% 122.32/16.03 fof(f137,plain,(
% 122.32/16.03 ![Z]: ((![W]: (((![X]: ((![Y]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssPv1(Y)))|~ssRr(W,X)))|~ssRr(W,Z))|~ssPv1(W)))|ssPv3(Z))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f44])).
% 122.32/16.03 fof(f138,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv1(X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|~ssPv1(X2)|ssPv3(X5))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f137])).
% 122.32/16.03 fof(f139,plain,(
% 122.32/16.03 ![Y]: ((![W]: ((![Z]: (((![X]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssRr(W,X)))|~ssRr(W,Z))|~ssPv3(Z)))|~ssPv2(W)))|ssPv2(Y))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f45])).
% 122.32/16.03 fof(f140,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|~ssPv3(X5)|~ssPv2(X2)|ssPv2(X4))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f139])).
% 122.32/16.03 fof(f141,plain,(
% 122.32/16.03 ![W]: ((![Z]: (((![X]: ((![Y]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv4(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssPv2(Y)))|~ssRr(W,X)))|~ssRr(W,Z))|~ssPv1(Z)))|ssPv4(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f46])).
% 122.32/16.03 fof(f142,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv2(X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|~ssPv1(X5)|ssPv4(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f141])).
% 122.32/16.03 fof(f145,plain,(
% 122.32/16.03 ![W]: ((![X1]: ((![Z]: (((![X]: ((![Y]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv3(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssPv2(Y)))|~ssRr(W,X)))|~ssRr(Z,X1))|~ssRr(W,Z)))|ssPv1(X1)))|ssPv1(W))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f48])).
% 122.32/16.03 fof(f146,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5,X6]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv2(X4)|~ssRr(X2,X3)|~ssRr(X5,X6)|~ssRr(X2,X5)|ssPv1(X6)|ssPv1(X2))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f145])).
% 122.32/16.03 fof(f149,plain,(
% 122.32/16.03 ![X1]: ((![W]: ((![Z]: (((![X]: ((![Y]: (((![U]: ((![V]: (~ssRr(U,V)|~ssPv2(V)))|~ssRr(W,U)))|~ssRr(X,Y))|~ssPv1(Y)))|~ssRr(W,X)))|~ssRr(Z,X1))|~ssRr(W,Z)))|~ssPv3(W)))|ssPv2(X1))),
% 122.32/16.03 inference(miniscoping,[status(thm)],[f50])).
% 122.32/16.03 fof(f150,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5,X6]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv1(X4)|~ssRr(X2,X3)|~ssRr(X5,X6)|~ssRr(X2,X5)|~ssPv3(X2)|ssPv2(X6))),
% 122.32/16.03 inference(cnf_transformation,[status(thm)],[f149])).
% 122.32/16.03 fof(f153,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv2(X1)|~ssPv1(skf1(X0))|~ssPv4(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f68,f52])).
% 122.32/16.03 fof(f156,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv4(X1)|~ssPv2(skf1(X0))|~ssPv3(X0)|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f70,f52])).
% 122.32/16.03 fof(f159,plain,(
% 122.32/16.03 ![X0]: (~ssPv2(skf1(skf1(X0)))|~ssPv1(skf1(X0))|~ssPv4(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f153,f52])).
% 122.32/16.03 fof(f160,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(skf1(X0)))|~ssPv2(skf1(X0))|~ssPv3(X0)|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f156,f52])).
% 122.32/16.03 fof(f161,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv1(X1)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f102,f52])).
% 122.32/16.03 fof(f174,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv4(X1)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f106,f52])).
% 122.32/16.03 fof(f179,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X1)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|~ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f108,f52])).
% 122.32/16.03 fof(f187,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssPv1(skf1(X3))|~ssRr(X2,X3)|~ssRr(X2,X4)|~ssPv1(X2)|ssPv3(X4))),
% 122.32/16.03 inference(resolution,[status(thm)],[f138,f52])).
% 122.32/16.03 fof(f191,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|ssPv1(X1)|ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f54,f52])).
% 122.32/16.03 fof(f194,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f191,f52])).
% 122.32/16.03 fof(f198,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv1(skf1(X0))|ssPv1(X1)|ssPv3(X0)|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f56,f52])).
% 122.32/16.03 fof(f201,plain,(
% 122.32/16.03 ![X0]: (~ssPv1(skf1(X0))|ssPv1(skf1(skf1(X0)))|ssPv3(X0)|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f198,f52])).
% 122.32/16.03 fof(f205,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(skf1(X0))|ssPv2(X1)|ssPv2(X0)|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f60,f52])).
% 122.32/16.03 fof(f208,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X0)|ssPv3(X1)|ssPv3(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f62,f52])).
% 122.32/16.03 fof(f211,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv4(skf1(X0))|~ssPv1(X0)|ssPv3(X1)|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f64,f52])).
% 122.32/16.03 fof(f216,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(X0))|ssPv2(skf1(skf1(X0)))|ssPv2(X0)|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f205,f52])).
% 122.32/16.03 fof(f217,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(X0)|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f208,f52])).
% 122.32/16.03 fof(f218,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(X0))|~ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f211,f52])).
% 122.32/16.03 fof(f226,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(skf1(X0))|~ssPv4(X0)|ssPv4(X1)|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f66,f52])).
% 122.32/16.03 fof(f231,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv1(X2)|ssPv3(X1)|ssPv2(skf1(X3))|ssPv3(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f72,f52])).
% 122.32/16.03 fof(f235,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv3(X2)|ssPv4(X1)|ssPv1(skf1(X3))|ssPv4(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f74,f52])).
% 122.32/16.03 fof(f237,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv1(X1)|ssPv3(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f76,f52])).
% 122.32/16.03 fof(f242,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv2(skf1(X0))|ssPv4(X1)|ssPv3(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f78,f52])).
% 122.32/16.03 fof(f247,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(skf1(X0))|ssPv2(X1)|ssPv2(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f80,f52])).
% 122.32/16.03 fof(f253,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(skf1(X0),X1)|~ssPv4(X1)|~ssRr(X2,X3)|~ssRr(X0,X2)|ssPv3(X3)|ssPv1(X0)|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f82,f52])).
% 122.32/16.03 fof(f254,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|ssPv3(skf1(X3))|ssPv1(X2)|ssPv2(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f82,f52])).
% 122.32/16.03 fof(f256,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv2(skf1(X0))|~ssPv4(X0)|ssPv3(X1)|ssPv3(skf1(X0)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f84,f52])).
% 122.32/16.03 fof(f262,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(X0))|~ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f226,f52])).
% 122.32/16.03 fof(f273,plain,(
% 122.32/16.03 ![X0]: (~ssPv1(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f237,f52])).
% 122.32/16.03 fof(f274,plain,(
% 122.32/16.03 ![X0]: (ssPv3(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f273,f194])).
% 122.32/16.03 fof(f275,plain,(
% 122.32/16.03 ![X0]: (ssPv3(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f274])).
% 122.32/16.03 fof(f276,plain,(
% 122.32/16.03 ![X0]: (ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|~ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f275,f262])).
% 122.32/16.03 fof(f277,plain,(
% 122.32/16.03 ![X0]: (ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv2(skf1(skf1(X0)))|ssPv2(X0)|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f275,f216])).
% 122.32/16.03 fof(f280,plain,(
% 122.32/16.03 ![X0]: (ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|~ssPv4(X0)|ssPv4(skf1(skf1(X0))))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f276])).
% 122.32/16.03 fof(f281,plain,(
% 122.32/16.03 ![X0]: (ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv2(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f277])).
% 122.32/16.03 fof(f283,plain,(
% 122.32/16.03 ![X0]: (~ssPv2(skf1(X0))|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f242,f52])).
% 122.32/16.03 fof(f284,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(X0))|ssPv2(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f247,f52])).
% 122.32/16.03 fof(f287,plain,(
% 122.32/16.03 ![X0]: (~ssPv2(skf1(X0))|~ssPv4(X0)|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f256,f52])).
% 122.32/16.03 fof(f296,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv1(X2)|ssPv1(skf1(X3))|ssPv3(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f88,f52])).
% 122.32/16.03 fof(f298,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X1)|~ssPv3(skf1(X0))|ssPv1(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f90,f52])).
% 122.32/16.03 fof(f305,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv2(X2)|~ssPv3(X2)|ssPv4(X1)|ssPv2(skf1(X3)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f92,f52])).
% 122.32/16.03 fof(f309,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv1(X2)|~ssPv4(X2)|ssPv3(X1)|ssPv2(skf1(X3)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f94,f52])).
% 122.32/16.03 fof(f313,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv2(X2)|ssPv3(skf1(X3))|ssPv1(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f96,f52])).
% 122.32/16.03 fof(f317,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssPv2(skf1(X3))|~ssRr(X2,X3)|ssPv1(X2)|ssPv3(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f98,f52])).
% 122.32/16.03 fof(f321,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssPv1(X2)|ssPv3(skf1(X3))|ssPv4(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f100,f52])).
% 122.32/16.03 fof(f342,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssRr(X2,X4)|ssPv4(skf1(X3))|ssPv2(X4)|ssPv2(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f114,f52])).
% 122.32/16.03 fof(f349,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv1(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssRr(X2,X4)|ssPv4(skf1(X3))|ssPv3(X4)|ssPv1(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f116,f52])).
% 122.32/16.03 fof(f353,plain,(
% 122.32/16.03 ![X0]: (~ssPv1(skf1(skf1(X0)))|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f161,f52])).
% 122.32/16.03 fof(f354,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0)|ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f353,f194])).
% 122.32/16.03 fof(f355,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0)|ssPv2(skf1(X0))|ssPv3(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f354])).
% 122.32/16.03 fof(f359,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssRr(X2,X4)|~ssPv3(X4)|~ssPv2(X2)|ssPv2(skf1(X3)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f140,f52])).
% 122.32/16.03 fof(f363,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(skf1(X0)))|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f174,f52])).
% 122.32/16.03 fof(f364,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(skf1(X0)))|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|~ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f179,f52])).
% 122.32/16.03 fof(f369,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssPv2(skf1(X3))|~ssRr(X2,X3)|~ssRr(X2,X4)|~ssPv1(X4)|ssPv4(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f142,f52])).
% 122.32/16.03 fof(f372,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv2(X4)|~ssRr(X2,X3)|~ssPv1(skf1(X2))|ssPv4(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f142,f52])).
% 122.32/16.03 fof(f375,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssPv1(skf1(X3))|~ssRr(X2,X3)|~ssRr(X2,X3)|~ssPv3(X2)|ssPv2(skf1(X3)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f150,f52])).
% 122.32/16.03 fof(f382,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssPv1(skf1(X3))|~ssRr(X2,X3)|~ssPv3(X2)|ssPv2(skf1(X3)))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f375])).
% 122.32/16.03 fof(f405,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(X0))|ssPv2(X0)|ssPv2(skf1(X0))|ssPv3(X0)|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f355,f275])).
% 122.32/16.03 fof(f406,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(X0))|ssPv2(X0)|ssPv2(skf1(X0))|ssPv3(X0)|ssPv1(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f405])).
% 122.32/16.03 fof(f408,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(skf1(X0)))|~ssPv3(skf1(X0))|ssPv1(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f298,f52])).
% 122.32/16.03 fof(f413,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssRr(X2,X4)|~ssPv2(X4)|ssPv2(X1)|ssPv1(skf1(X3))|ssPv4(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f118,f52])).
% 122.32/16.03 fof(f417,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|ssPv2(X4)|ssPv1(X5)|ssPv4(X2))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f120,f110])).
% 122.32/16.03 fof(f422,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(skf1(X2),X3)|ssPv2(X3)|ssPv1(skf1(X2))|ssPv4(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f417,f52])).
% 122.32/16.03 fof(f428,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssPv1(skf1(X3))|~ssRr(X2,X3)|~ssRr(X2,X4)|ssPv4(X4)|ssPv2(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f122,f52])).
% 122.32/16.03 fof(f432,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|ssPv1(X5)|ssPv4(X2))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f124,f417])).
% 122.32/16.03 fof(f436,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssRr(X2,X4)|ssPv1(X4)|ssPv4(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f432,f52])).
% 122.32/16.03 fof(f468,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4,X5]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|~ssRr(X2,X5)|ssPv4(X4)|ssPv4(X2))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f128,f432])).
% 122.32/16.03 fof(f473,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssRr(skf1(X2),X3)|ssPv4(X3)|ssPv4(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f468,f52])).
% 122.32/16.03 fof(f486,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssPv3(skf1(X3))|~ssRr(X2,X3)|~ssRr(X2,X4)|ssPv4(X4)|ssPv2(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f132,f52])).
% 122.32/16.03 fof(f502,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|~ssRr(X2,X4)|~ssPv4(X4)|ssPv3(skf1(X3))|ssPv1(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f136,f52])).
% 122.32/16.03 fof(f516,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssPv2(skf1(X3))|~ssRr(X2,X3)|~ssRr(X2,X3)|ssPv1(skf1(X3))|ssPv1(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f146,f52])).
% 122.32/16.03 fof(f523,plain,(
% 122.32/16.03 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssPv2(skf1(X3))|~ssRr(X2,X3)|ssPv1(skf1(X3))|ssPv1(X2))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f516])).
% 122.32/16.03 fof(f527,plain,(
% 122.32/16.03 ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|ssPv4(skf1(skf1(X2)))|ssPv4(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f473,f52])).
% 122.32/16.03 fof(f528,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X1)|ssPv4(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f527,f52])).
% 122.32/16.03 fof(f529,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f528,f52])).
% 122.32/16.03 fof(f556,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv1(X0)|ssPv3(X1)|ssPv2(skf1(skf1(X0)))|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f231,f52])).
% 122.32/16.03 fof(f561,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X0)|ssPv4(X1)|ssPv1(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f235,f52])).
% 122.32/16.03 fof(f605,plain,(
% 122.32/16.03 ![X0]: (~ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv2(skf1(skf1(X0)))|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f556,f52])).
% 122.32/16.03 fof(f607,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f561,f52])).
% 122.32/16.03 fof(f636,plain,(
% 122.32/16.03 ![X0,X1,X2]: (~ssPv4(skf1(skf1(X0)))|~ssRr(X1,X2)|~ssRr(X0,X1)|ssPv3(X2)|ssPv1(X0)|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f253,f52])).
% 122.32/16.03 fof(f637,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv4(X1)|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f254,f52])).
% 122.32/16.03 fof(f655,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(skf1(X0)))|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f637,f52])).
% 122.32/16.03 fof(f677,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X1)|~ssPv1(X0)|ssPv1(skf1(skf1(X0)))|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f296,f52])).
% 122.32/16.03 fof(f689,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv2(X0)|~ssPv3(X0)|ssPv4(X1)|ssPv2(skf1(skf1(X0))))),
% 122.32/16.03 inference(resolution,[status(thm)],[f305,f52])).
% 122.32/16.03 fof(f694,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv1(X0)|~ssPv4(X0)|ssPv3(X1)|ssPv2(skf1(skf1(X0))))),
% 122.32/16.03 inference(resolution,[status(thm)],[f309,f52])).
% 122.32/16.03 fof(f715,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(skf1(X0)))|~ssPv1(X0)|ssPv1(skf1(skf1(X0)))|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f677,f52])).
% 122.32/16.03 fof(f717,plain,(
% 122.32/16.03 ![X0]: (~ssPv2(X0)|~ssPv3(X0)|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(skf1(X0))))),
% 122.32/16.03 inference(resolution,[status(thm)],[f689,f52])).
% 122.32/16.03 fof(f719,plain,(
% 122.32/16.03 ![X0]: (~ssPv1(X0)|~ssPv4(X0)|ssPv3(skf1(skf1(X0)))|ssPv2(skf1(skf1(X0))))),
% 122.32/16.03 inference(resolution,[status(thm)],[f694,f52])).
% 122.32/16.03 fof(f725,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv2(X1)|~ssPv2(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f313,f52])).
% 122.32/16.03 fof(f729,plain,(
% 122.32/16.03 ![X0]: (~ssPv2(skf1(skf1(X0)))|~ssPv2(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f725,f52])).
% 122.32/16.03 fof(f746,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X1)|~ssPv2(skf1(skf1(X0)))|ssPv1(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f317,f52])).
% 122.32/16.03 fof(f751,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv2(X1)|~ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f321,f52])).
% 122.32/16.03 fof(f757,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(skf1(X0)))|~ssPv2(skf1(skf1(X0)))|ssPv1(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f746,f52])).
% 122.32/16.03 fof(f759,plain,(
% 122.32/16.03 ![X0]: (~ssPv2(skf1(skf1(X0)))|~ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f751,f52])).
% 122.32/16.03 fof(f806,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X1)|~ssPv1(skf1(skf1(X0)))|~ssPv1(X0)|ssPv3(skf1(X0)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f187,f52])).
% 122.32/16.03 fof(f808,plain,(
% 122.32/16.03 ![X0,X1,X2]: (~ssRr(X0,X1)|~ssPv3(X1)|~ssRr(X2,X0)|~ssPv1(skf1(skf1(X2)))|~ssPv1(X2)|ssPv3(skf1(X2)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f187,f52])).
% 122.32/16.03 fof(f812,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(skf1(X0)))|~ssPv1(skf1(skf1(X0)))|~ssPv1(X0)|ssPv3(skf1(X0)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f806,f52])).
% 122.32/16.03 fof(f876,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X1)|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f342,f52])).
% 122.32/16.03 fof(f926,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f876,f52])).
% 122.32/16.03 fof(f931,plain,(
% 122.32/16.03 ![X0,X1,X2]: (~ssRr(X0,X1)|~ssRr(X2,X0)|ssPv2(skf1(skf1(X2)))|ssPv1(skf1(X2))|ssPv4(X2))),
% 122.32/16.03 inference(resolution,[status(thm)],[f422,f52])).
% 122.32/16.03 fof(f932,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|ssPv2(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f931,f52])).
% 122.32/16.03 fof(f933,plain,(
% 122.32/16.03 ![X0]: (ssPv2(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f932,f52])).
% 122.32/16.03 fof(f941,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(X0))|ssPv4(X0)|~ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f933,f759])).
% 122.32/16.03 fof(f942,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(X0))|ssPv4(X0)|~ssPv2(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f933,f729])).
% 122.32/16.03 fof(f953,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(X0))|ssPv4(X0)|~ssPv1(X0)|ssPv3(skf1(skf1(X0))))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f941])).
% 122.32/16.03 fof(f961,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv1(X1)|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f349,f52])).
% 122.32/16.03 fof(f974,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(X0))|ssPv4(X0)|~ssPv2(X0)|ssPv3(skf1(skf1(X0))))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f942,f953])).
% 122.32/16.03 fof(f982,plain,(
% 122.32/16.03 ![X0]: (~ssPv1(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f961,f52])).
% 122.32/16.03 fof(f985,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X1)|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f436,f52])).
% 122.32/16.03 fof(f990,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f985,f52])).
% 122.32/16.03 fof(f991,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(X0))|ssPv4(X0)|~ssPv2(X0))),
% 122.32/16.03 inference(backward_subsumption_resolution,[status(thm)],[f974,f990])).
% 122.32/16.03 fof(f992,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(X0))|ssPv4(X0)|~ssPv1(X0))),
% 122.32/16.03 inference(backward_subsumption_resolution,[status(thm)],[f953,f990])).
% 122.32/16.03 fof(f995,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(skf1(skf1(X0))))|ssPv4(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f991,f933])).
% 122.32/16.03 fof(f1008,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0)|ssPv4(skf1(skf1(skf1(X0))))|ssPv3(skf1(skf1(X0)))|ssPv1(skf1(X0)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f995,f982])).
% 122.32/16.03 fof(f1024,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0)|ssPv4(skf1(skf1(skf1(X0))))|ssPv3(skf1(skf1(X0))))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1008])).
% 122.32/16.03 fof(f1025,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0)|ssPv4(skf1(skf1(skf1(X0)))))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1024,f990])).
% 122.32/16.03 fof(f1047,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0)|~ssPv2(skf1(skf1(X0)))|~ssPv3(skf1(X0))|ssPv1(skf1(X0)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1025,f160])).
% 122.32/16.03 fof(f1056,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0)|~ssPv2(skf1(skf1(X0)))|~ssPv3(skf1(X0)))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1047])).
% 122.32/16.03 fof(f1057,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0)|~ssPv3(skf1(X0)))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1056,f933])).
% 122.32/16.03 fof(f1066,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv2(skf1(X0))|ssPv2(X1)|ssPv1(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f413,f52])).
% 122.32/16.03 fof(f1090,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X1)|~ssPv3(skf1(X0))|~ssPv2(X0)|ssPv2(skf1(skf1(X0))))),
% 122.32/16.03 inference(resolution,[status(thm)],[f359,f52])).
% 122.32/16.03 fof(f1095,plain,(
% 122.32/16.03 ![X0]: (~ssPv3(skf1(skf1(X0)))|~ssPv3(skf1(X0))|~ssPv2(X0)|ssPv2(skf1(skf1(X0))))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1090,f52])).
% 122.32/16.03 fof(f1109,plain,(
% 122.32/16.03 ![X0,X1,X2]: (~ssRr(skf1(X0),X1)|~ssPv2(X1)|~ssPv1(skf1(X2))|~ssRr(X0,X2)|~ssPv3(X0)|ssPv2(skf1(X2)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f382,f52])).
% 122.32/16.03 fof(f1112,plain,(
% 122.32/16.03 ![X0,X1]: (~ssPv2(skf1(skf1(X0)))|~ssPv1(skf1(X1))|~ssRr(X0,X1)|~ssPv3(X0)|ssPv2(skf1(X1)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1109,f52])).
% 122.32/16.03 fof(f1114,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv4(X1)|~ssPv2(skf1(skf1(X0)))|~ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f369,f52])).
% 122.32/16.03 fof(f1127,plain,(
% 122.32/16.03 ![X0]: (~ssPv2(skf1(X0))|ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1066,f52])).
% 122.32/16.03 fof(f1137,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv2(X1)|~ssPv1(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f428,f52])).
% 122.32/16.03 fof(f1143,plain,(
% 122.32/16.03 ![X0]: (~ssPv2(skf1(skf1(X0)))|~ssPv1(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1137,f52])).
% 122.32/16.03 fof(f1144,plain,(
% 122.32/16.03 ![X0]: (~ssPv1(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1143,f933])).
% 122.32/16.03 fof(f1145,plain,(
% 122.32/16.03 ![X0]: (~ssPv1(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0)|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1143,f281])).
% 122.32/16.03 fof(f1146,plain,(
% 122.32/16.03 ![X0]: (~ssPv1(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1144,f991])).
% 122.32/16.03 fof(f1147,plain,(
% 122.32/16.03 ![X0]: (~ssPv1(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0)|ssPv2(skf1(X0))|ssPv1(X0)|ssPv3(X0)|ssPv4(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1145])).
% 122.32/16.03 fof(f1148,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv2(skf1(X0))|ssPv1(X0)|ssPv3(X0)|ssPv4(X0))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1147,f194])).
% 122.32/16.03 fof(f1150,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv4(X0)|ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1146,f194])).
% 122.32/16.03 fof(f1153,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv4(X0)|ssPv2(skf1(X0))|ssPv3(X0))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1150,f991])).
% 122.32/16.03 fof(f1200,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv4(X0)|ssPv3(X0)|ssPv1(skf1(skf1(X0)))|ssPv4(skf1(X0)))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1153,f991])).
% 122.32/16.03 fof(f1213,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv4(X0)|ssPv3(X0)|ssPv1(skf1(skf1(X0))))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1200])).
% 122.32/16.03 fof(f1214,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv4(X0)|ssPv3(X0)|ssPv1(skf1(skf1(X0))))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1213,f201])).
% 122.32/16.03 fof(f1215,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv4(X0)|ssPv3(X0)|ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1214,f1146])).
% 122.32/16.03 fof(f1232,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv4(X0)|ssPv3(X0)|ssPv1(skf1(X0)))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1215])).
% 122.32/16.03 fof(f1237,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv3(skf1(X0))|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1232,f982])).
% 122.32/16.03 fof(f1254,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv3(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1237])).
% 122.32/16.03 fof(f1269,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv3(skf1(X0))|ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1254,f655])).
% 122.32/16.03 fof(f1281,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv3(skf1(X0))|ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv2(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1269])).
% 122.32/16.03 fof(f1292,plain,(
% 122.32/16.03 ![X0]: (ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv4(skf1(skf1(X0))))),
% 122.32/16.03 inference(backward_subsumption_resolution,[status(thm)],[f280,f1293])).
% 122.32/16.03 fof(f1293,plain,(
% 122.32/16.03 ![X0]: (ssPv2(X0)|ssPv2(skf1(X0))|ssPv1(X0)|ssPv3(X0)|ssPv4(X0))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1148,f406])).
% 122.32/16.03 fof(f1315,plain,(
% 122.32/16.03 ![X0]: (ssPv2(X0)|ssPv1(X0)|ssPv3(X0)|ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1293,f283])).
% 122.32/16.03 fof(f1324,plain,(
% 122.32/16.03 ![X0]: (ssPv2(X0)|ssPv1(X0)|ssPv3(X0)|ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1315])).
% 122.32/16.03 fof(f1331,plain,(
% 122.32/16.03 ![X0]: (ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1292,f655])).
% 122.32/16.03 fof(f1345,plain,(
% 122.32/16.03 ![X0]: (ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv3(skf1(skf1(X0))))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1331])).
% 122.32/16.03 fof(f1724,plain,(
% 122.32/16.03 ![X0]: (ssPv2(X0)|ssPv1(X0)|ssPv3(X0)|ssPv4(X0)|ssPv3(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1324,f655])).
% 122.32/16.03 fof(f1739,plain,(
% 122.32/16.03 ![X0]: (ssPv2(X0)|ssPv1(X0)|ssPv3(X0)|ssPv4(X0)|ssPv3(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1724])).
% 122.32/16.03 fof(f1740,plain,(
% 122.32/16.03 ![X0]: (ssPv2(X0)|ssPv1(X0)|ssPv4(X0)|ssPv3(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1739,f217])).
% 122.32/16.03 fof(f1745,plain,(
% 122.32/16.03 ![X0]: (ssPv2(X0)|ssPv1(X0)|ssPv4(X0)|ssPv3(skf1(X0))|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1740,f990])).
% 122.32/16.03 fof(f1778,plain,(
% 122.32/16.03 ![X0]: (ssPv2(X0)|ssPv1(X0)|ssPv4(X0)|ssPv3(skf1(X0))|ssPv1(skf1(X0)))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f1745])).
% 122.32/16.03 fof(f1779,plain,(
% 122.32/16.03 ![X0]: (ssPv1(X0)|ssPv4(X0)|ssPv3(skf1(X0))|ssPv1(skf1(X0)))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1778,f991])).
% 122.32/16.03 fof(f1797,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(backward_subsumption_resolution,[status(thm)],[f1057,f1798])).
% 122.32/16.03 fof(f1798,plain,(
% 122.32/16.03 ![X0]: (ssPv4(X0)|ssPv3(skf1(X0))|ssPv1(skf1(X0)))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1779,f992])).
% 122.32/16.03 fof(f1801,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1798,f990])).
% 122.32/16.03 fof(f1832,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1801,f1146])).
% 122.32/16.03 fof(f1877,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(skf1(X0)))|~ssPv2(skf1(skf1(X0)))|~ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1114,f52])).
% 122.32/16.03 fof(f1980,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(X0))|ssPv4(X0)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f1797,f363])).
% 122.32/16.03 fof(f1993,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(X0))|ssPv4(X0)|~ssPv3(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1980,f1832])).
% 122.32/16.03 fof(f2023,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(backward_subsumption_resolution,[status(thm)],[f991,f2024])).
% 122.32/16.03 fof(f2024,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(X0))|ssPv4(X0)|ssPv2(X0))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f1993,f1798])).
% 122.32/16.03 fof(f2036,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv3(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f2024,f273])).
% 122.32/16.03 fof(f2045,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv3(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f2036])).
% 122.32/16.03 fof(f2047,plain,(
% 122.32/16.03 ![X0]: (~ssPv2(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(backward_subsumption_resolution,[status(thm)],[f1143,f2023])).
% 122.32/16.03 fof(f2049,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(skf1(X0)))|~ssPv2(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(backward_subsumption_resolution,[status(thm)],[f1877,f2023])).
% 122.32/16.03 fof(f2050,plain,(
% 122.32/16.03 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv2(X4)|~ssRr(X2,X3)|ssPv4(X2))),
% 122.32/16.03 inference(backward_subsumption_resolution,[status(thm)],[f372,f2023])).
% 122.32/16.03 fof(f2057,plain,(
% 122.32/16.03 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv3(X0)|ssPv4(X0))),
% 122.32/16.03 inference(backward_subsumption_resolution,[status(thm)],[f201,f2023])).
% 122.32/16.03 fof(f2075,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(backward_subsumption_resolution,[status(thm)],[f607,f2057])).
% 122.32/16.03 fof(f2086,plain,(
% 122.32/16.03 ![X0]: (ssPv3(X0)|ssPv4(X0)|ssPv3(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f2057,f273])).
% 122.32/16.03 fof(f2114,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f2075,f982])).
% 122.32/16.03 fof(f2122,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv4(X0)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f2075,f353])).
% 122.32/16.03 fof(f2126,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv4(X0)|ssPv3(skf1(X0))|ssPv1(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f2114])).
% 122.32/16.03 fof(f2133,plain,(
% 122.32/16.03 ![X0]: (ssPv4(X0)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f2122,f363])).
% 122.32/16.03 fof(f2139,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|~ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f2133,f1345])).
% 122.32/16.03 fof(f2145,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|~ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f2139])).
% 122.32/16.03 fof(f2146,plain,(
% 122.32/16.03 ![X0]: (~ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f2145,f406])).
% 122.32/16.03 fof(f2176,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f2045,f284])).
% 122.32/16.03 fof(f2177,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|~ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f2045,f262])).
% 122.32/16.03 fof(f2178,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0)))|ssPv2(X0)|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f2045,f216])).
% 122.32/16.03 fof(f2190,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0)))|ssPv4(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f2176])).
% 122.32/16.03 fof(f2191,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|~ssPv4(X0)|ssPv4(skf1(skf1(X0))))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f2177])).
% 122.32/16.03 fof(f2192,plain,(
% 122.32/16.03 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv4(X0))),
% 122.32/16.03 inference(forward_subsumption_resolution,[status(thm)],[f2178,f2047])).
% 122.32/16.03 fof(f2205,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv4(X1)|~ssPv3(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f486,f52])).
% 122.32/16.03 fof(f2232,plain,(
% 122.32/16.03 ![X0]: (ssPv4(X0)|ssPv3(skf1(X0))|ssPv1(X0)|~ssPv2(skf1(X0))|~ssPv3(X0)|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f2126,f160])).
% 122.32/16.03 fof(f2241,plain,(
% 122.32/16.03 ![X0]: (ssPv4(X0)|ssPv3(skf1(X0))|ssPv1(X0)|~ssPv2(skf1(X0))|~ssPv3(X0))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f2232])).
% 122.32/16.03 fof(f2274,plain,(
% 122.32/16.03 ![X0]: (ssPv3(X0)|ssPv4(X0)|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv4(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f2086,f284])).
% 122.32/16.03 fof(f2291,plain,(
% 122.32/16.03 ![X0]: (ssPv3(X0)|ssPv4(X0)|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0))))),
% 122.32/16.03 inference(duplicate_literals_removal,[status(thm)],[f2274])).
% 122.32/16.03 fof(f2351,plain,(
% 122.32/16.03 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv4(X1)|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 122.32/16.03 inference(resolution,[status(thm)],[f502,f52])).
% 122.32/16.03 fof(f2397,plain,(
% 119.47/16.05 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssPv4(X1)|~ssRr(X2,X0)|~ssPv2(skf1(X3))|~ssRr(X2,X3)|ssPv4(X2))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2050,f52])).
% 119.47/16.05 fof(f2405,plain,(
% 119.47/16.05 ![X0,X1,X2]: (~ssRr(skf1(X0),X1)|~ssPv4(X1)|~ssPv2(skf1(X2))|~ssRr(X0,X2)|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2397,f52])).
% 119.47/16.05 fof(f2407,plain,(
% 119.47/16.05 ![X0,X1]: (~ssPv4(skf1(skf1(X0)))|~ssPv2(skf1(X1))|~ssRr(X0,X1)|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2405,f52])).
% 119.47/16.05 fof(f2440,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f2146,f1292])).
% 119.47/16.05 fof(f2460,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|~ssPv4(X0)|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2440,f287])).
% 119.47/16.05 fof(f2466,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f2460,f1740])).
% 119.47/16.05 fof(f2469,plain,(
% 119.47/16.05 ![X0,X1]: (~ssRr(skf1(X0),X1)|~ssPv3(X1)|~ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f523,f52])).
% 119.47/16.05 fof(f2500,plain,(
% 119.47/16.05 ![X0]: (ssPv3(X0)|ssPv4(X0)|ssPv2(skf1(X0))|ssPv1(X0)|~ssPv2(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2291,f729])).
% 119.47/16.05 fof(f2517,plain,(
% 119.47/16.05 ![X0]: (ssPv3(X0)|ssPv4(X0)|ssPv2(skf1(X0))|ssPv1(X0)|~ssPv2(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2500])).
% 119.47/16.05 fof(f2518,plain,(
% 119.47/16.05 ![X0]: (ssPv3(X0)|ssPv4(X0)|ssPv2(skf1(X0))|ssPv1(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f2517,f2440])).
% 119.47/16.05 fof(f2531,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv3(skf1(X0))|~ssPv2(skf1(skf1(X0)))|ssPv1(X0)|ssPv3(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2466,f757])).
% 119.47/16.05 fof(f2560,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|ssPv3(skf1(X0))|~ssPv2(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2531])).
% 119.47/16.05 fof(f2581,plain,(
% 119.47/16.05 ![X0]: (ssPv3(X0)|ssPv4(X0)|ssPv2(skf1(X0))|ssPv1(X0)|~ssPv2(skf1(skf1(X0)))|ssPv1(X0)|ssPv3(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2518,f757])).
% 119.47/16.05 fof(f2613,plain,(
% 119.47/16.05 ![X0]: (ssPv3(X0)|ssPv4(X0)|ssPv2(skf1(X0))|ssPv1(X0)|~ssPv2(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2581])).
% 119.47/16.05 fof(f2614,plain,(
% 119.47/16.05 ![X0]: (ssPv3(X0)|ssPv4(X0)|ssPv2(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f2613,f2291])).
% 119.47/16.05 fof(f2631,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2614,f2047])).
% 119.47/16.05 fof(f2650,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2631])).
% 119.47/16.05 fof(f2662,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2650,f926])).
% 119.47/16.05 fof(f2686,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv2(X0)|~ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2650,f262])).
% 119.47/16.05 fof(f2695,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2662])).
% 119.47/16.05 fof(f2702,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv2(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f2686,f2023])).
% 119.47/16.05 fof(f2735,plain,(
% 119.47/16.05 ![X0,X1]: (~ssPv2(skf1(X0))|~ssRr(X1,X0)|ssPv4(X1)|ssPv4(X1)|ssPv3(skf1(X1))|ssPv1(X1))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2407,f2126])).
% 119.47/16.05 fof(f2737,plain,(
% 119.47/16.05 ![X0,X1]: (~ssPv2(skf1(X0))|~ssRr(X1,X0)|ssPv4(X1)|ssPv3(skf1(X1))|ssPv1(X1))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2735])).
% 119.47/16.05 fof(f2777,plain,(
% 119.47/16.05 ![X0]: (~ssPv2(skf1(skf1(X0)))|ssPv4(X0)|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2737,f52])).
% 119.47/16.05 fof(f2786,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv2(X0)|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2695,f982])).
% 119.47/16.05 fof(f2794,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv2(X0)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2695,f353])).
% 119.47/16.05 fof(f2798,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2786])).
% 119.47/16.05 fof(f2806,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv2(X0)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2794])).
% 119.47/16.05 fof(f2807,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f2806,f363])).
% 119.47/16.05 fof(f2857,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv4(X0)|~ssPv2(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2190,f729])).
% 119.47/16.05 fof(f2878,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv4(X0)|~ssPv2(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2857])).
% 119.47/16.05 fof(f2879,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv4(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f2878,f2192])).
% 119.47/16.05 fof(f2899,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2702,f655])).
% 119.47/16.05 fof(f2912,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2899])).
% 119.47/16.05 fof(f2926,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2798,f655])).
% 119.47/16.05 fof(f2939,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2926])).
% 119.47/16.05 fof(f2981,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2879,f529])).
% 119.47/16.05 fof(f3011,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv4(X0)|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f2981])).
% 119.47/16.05 fof(f3012,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3011,f2191])).
% 119.47/16.05 fof(f3029,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3012,f655])).
% 119.47/16.05 fof(f3039,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv2(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3029])).
% 119.47/16.05 fof(f3200,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv2(X0)|ssPv1(X0)|~ssPv3(skf1(X0))|ssPv1(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2912,f408])).
% 119.47/16.05 fof(f3223,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv2(X0)|ssPv1(X0)|~ssPv3(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3200])).
% 119.47/16.05 fof(f3224,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv1(skf1(X0))|ssPv2(X0)|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3223,f2650])).
% 119.47/16.05 fof(f3284,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0)))|ssPv2(skf1(X0))|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2939,f2807])).
% 119.47/16.05 fof(f3304,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0)))|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3284])).
% 119.47/16.05 fof(f3305,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3304,f2798])).
% 119.47/16.05 fof(f3361,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|ssPv4(skf1(X0))|~ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3039,f2133])).
% 119.47/16.05 fof(f3386,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0)|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3361])).
% 119.47/16.05 fof(f3387,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3386,f3012])).
% 119.47/16.05 fof(f3439,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv4(X0)|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3305,f2777])).
% 119.47/16.05 fof(f3463,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv4(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3439])).
% 119.47/16.05 fof(f3503,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv4(X0)|ssPv2(skf1(X0))|ssPv2(X0)|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3463,f2807])).
% 119.47/16.05 fof(f3532,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv4(X0)|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3503])).
% 119.47/16.05 fof(f3533,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv4(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3532,f3387])).
% 119.47/16.05 fof(f3546,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3533,f2047])).
% 119.47/16.05 fof(f3555,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv1(skf1(X0))|ssPv4(skf1(X0))|~ssPv2(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3533,f729])).
% 119.47/16.05 fof(f3568,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3546])).
% 119.47/16.05 fof(f3571,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3555,f3387])).
% 119.47/16.05 fof(f3606,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|~ssPv1(skf1(X0))|~ssPv4(X0)|ssPv3(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3568,f159])).
% 119.47/16.05 fof(f3618,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|~ssPv4(X0)|ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3606,f3224])).
% 119.47/16.05 fof(f3727,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(skf1(X0)))|~ssPv3(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2205,f52])).
% 119.47/16.05 fof(f3731,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0)|ssPv4(skf1(X0))|ssPv3(skf1(X0))|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3727,f1281])).
% 119.47/16.05 fof(f3739,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3731])).
% 119.47/16.05 fof(f3740,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3739,f1254])).
% 119.47/16.05 fof(f3860,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0)|~ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3740,f262])).
% 119.47/16.05 fof(f3861,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv2(skf1(skf1(X0)))|ssPv2(X0)|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3740,f216])).
% 119.47/16.05 fof(f3882,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0)|~ssPv4(X0)|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3860])).
% 119.47/16.05 fof(f3883,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv2(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3861])).
% 119.47/16.05 fof(f3884,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv4(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3883,f2047])).
% 119.47/16.05 fof(f3929,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3882,f3884])).
% 119.47/16.05 fof(f3938,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3929,f655])).
% 119.47/16.05 fof(f3950,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3938])).
% 119.47/16.05 fof(f3957,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0)|~ssPv4(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3950,f3727])).
% 119.47/16.05 fof(f4005,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0)|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f3957])).
% 119.47/16.05 fof(f4006,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f4005,f3929])).
% 119.47/16.05 fof(f4158,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(skf1(X0)))|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2351,f52])).
% 119.47/16.05 fof(f4164,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f4158,f4006])).
% 119.47/16.05 fof(f4629,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv1(X0)|~ssPv3(skf1(X0))|ssPv1(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f3571,f408])).
% 119.47/16.05 fof(f4662,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv1(X0)|~ssPv3(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f4629])).
% 119.47/16.05 fof(f4663,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f4662,f2045])).
% 119.47/16.05 fof(f4727,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f3618,f2075])).
% 119.47/16.05 fof(f4738,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv3(X0)|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f4727,f982])).
% 119.47/16.05 fof(f4750,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv3(X0)|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f4738])).
% 119.47/16.05 fof(f4776,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv3(skf1(X0))|ssPv1(X0)|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f4750,f4158])).
% 119.47/16.05 fof(f4795,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv3(skf1(X0))|ssPv1(X0)|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f4776])).
% 119.47/16.05 fof(f4796,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f4795,f2045])).
% 119.47/16.05 fof(f4829,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv3(skf1(X0))|ssPv1(X0)|~ssPv2(skf1(skf1(X0)))|ssPv1(X0)|ssPv3(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f4796,f757])).
% 119.47/16.05 fof(f4843,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0)))|ssPv2(skf1(X0))|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f4796,f2807])).
% 119.47/16.05 fof(f4863,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv3(skf1(X0))|ssPv1(X0)|~ssPv2(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f4829])).
% 119.47/16.05 fof(f4867,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0)))|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f4843])).
% 119.47/16.05 fof(f4868,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv3(skf1(X0))|ssPv1(X0)|ssPv2(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f4867,f4750])).
% 119.47/16.05 fof(f4961,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f4868,f4863])).
% 119.47/16.05 fof(f5005,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv1(X0)|~ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f4961,f262])).
% 119.47/16.05 fof(f5029,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv1(X0)|~ssPv4(X0)|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5005])).
% 119.47/16.05 fof(f5030,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv1(X0)|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f5029,f2614])).
% 119.47/16.05 fof(f5036,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv1(X0)|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5030,f4158])).
% 119.47/16.05 fof(f5055,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv1(X0)|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5036])).
% 119.47/16.05 fof(f5235,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f4164,f4663])).
% 119.47/16.05 fof(f5278,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0))|~ssPv4(skf1(X0))|ssPv4(skf1(skf1(skf1(X0))))|ssPv1(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5235,f262])).
% 119.47/16.05 fof(f5306,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0))|~ssPv4(skf1(X0))|ssPv4(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5278])).
% 119.47/16.05 fof(f5307,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0))|ssPv4(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f5306,f4663])).
% 119.47/16.05 fof(f5501,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0))|~ssPv4(skf1(skf1(X0)))|ssPv3(skf1(skf1(skf1(X0))))|ssPv1(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5307,f4158])).
% 119.47/16.05 fof(f5513,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0))|~ssPv4(skf1(skf1(X0)))|~ssPv3(skf1(skf1(X0)))|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5307,f363])).
% 119.47/16.05 fof(f5524,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0))|~ssPv4(skf1(skf1(X0)))|ssPv3(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5501])).
% 119.47/16.05 fof(f5525,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|~ssPv4(skf1(skf1(X0)))|ssPv3(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f5524,f218])).
% 119.47/16.05 fof(f5538,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0))|~ssPv4(skf1(skf1(X0)))|~ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5513])).
% 119.47/16.05 fof(f5539,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0))|~ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f5538,f4006])).
% 119.47/16.05 fof(f5543,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv1(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f5539,f5235])).
% 119.47/16.05 fof(f5581,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|~ssPv4(X0)|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5543,f287])).
% 119.47/16.05 fof(f5588,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f5581,f2023])).
% 119.47/16.05 fof(f5615,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|~ssPv2(skf1(skf1(X0)))|ssPv1(X0)|ssPv3(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5588,f757])).
% 119.47/16.05 fof(f5648,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|~ssPv2(skf1(skf1(X0)))|ssPv3(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5615])).
% 119.47/16.05 fof(f5674,plain,(
% 119.47/16.05 ![X0]: (~ssPv3(skf1(skf1(X0)))|~ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f2469,f52])).
% 119.47/16.05 fof(f5677,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|ssPv3(X0)|ssPv1(skf1(X0))|ssPv1(skf1(skf1(X0))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5648,f5543])).
% 119.47/16.05 fof(f5684,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|ssPv3(X0)|ssPv1(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5677])).
% 119.47/16.05 fof(f5818,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|ssPv3(X0)|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5684,f982])).
% 119.47/16.05 fof(f5832,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|ssPv3(X0)|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5818])).
% 119.47/16.05 fof(f5876,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(skf1(skf1(X0))))|ssPv2(skf1(X0))|ssPv3(X0)|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5525,f5030])).
% 119.47/16.05 fof(f5878,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(skf1(skf1(X0))))|ssPv4(skf1(X0))|ssPv2(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5525,f3012])).
% 119.47/16.05 fof(f5885,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(skf1(skf1(X0))))|ssPv3(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5876])).
% 119.47/16.05 fof(f5886,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(skf1(skf1(X0))))|ssPv4(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5878])).
% 119.47/16.05 fof(f5930,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(X0)|~ssPv4(skf1(skf1(X0)))|~ssPv3(skf1(skf1(X0)))|~ssPv1(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5885,f364])).
% 119.47/16.05 fof(f5959,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(X0)|~ssPv3(skf1(skf1(X0)))|~ssPv1(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f5930,f5030])).
% 119.47/16.05 fof(f5998,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(skf1(X0))|ssPv4(skf1(skf1(skf1(X0))))|ssPv4(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5886,f529])).
% 119.47/16.05 fof(f6030,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(skf1(X0))|ssPv4(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f5998])).
% 119.47/16.05 fof(f6069,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(X0)|ssPv1(X0)|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f5055,f6070])).
% 119.47/16.05 fof(f6070,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(X0)|~ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f5959,f5543])).
% 119.47/16.05 fof(f6089,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(skf1(X0))|ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|ssPv3(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6069,f5832])).
% 119.47/16.05 fof(f6098,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(skf1(X0))|ssPv1(X0)|ssPv3(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6089])).
% 119.47/16.05 fof(f6099,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv1(skf1(X0))|ssPv1(X0)|ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6098,f5648])).
% 119.47/16.05 fof(f6180,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv3(skf1(X0))|~ssPv1(X0)|ssPv1(skf1(skf1(X0)))|ssPv3(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6099,f715])).
% 119.47/16.05 fof(f6209,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv3(skf1(X0))|~ssPv1(X0)|ssPv3(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6180])).
% 119.47/16.05 fof(f6210,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv3(skf1(X0))|ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6209,f6099])).
% 119.47/16.05 fof(f6348,plain,(
% 119.47/16.05 ![X0]: (~ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv1(X0)|ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5674,f5588])).
% 119.47/16.05 fof(f6355,plain,(
% 119.47/16.05 ![X0]: (~ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv1(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f5674,f2650])).
% 119.47/16.05 fof(f6357,plain,(
% 119.47/16.05 ![X0]: (~ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6348])).
% 119.47/16.05 fof(f6358,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6357,f5543])).
% 119.47/16.05 fof(f6367,plain,(
% 119.47/16.05 ![X0]: (~ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv1(X0)|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6355])).
% 119.47/16.05 fof(f6368,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv1(X0)|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6367,f3568])).
% 119.47/16.05 fof(f6379,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6358,f982])).
% 119.47/16.05 fof(f6396,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6379])).
% 119.47/16.05 fof(f6421,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|~ssPv2(skf1(X0))|~ssPv3(X0)|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6396,f160])).
% 119.47/16.05 fof(f6438,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|~ssPv2(skf1(X0))|~ssPv3(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6421])).
% 119.47/16.05 fof(f6439,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0))|~ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6438,f5543])).
% 119.47/16.05 fof(f6444,plain,(
% 119.47/16.05 ![X0]: (~ssPv3(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f408,f6446])).
% 119.47/16.05 fof(f6446,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6439,f6099])).
% 119.47/16.05 fof(f6491,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|~ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6446,f262])).
% 119.47/16.05 fof(f6511,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|~ssPv4(X0)|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6491])).
% 119.47/16.05 fof(f6512,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6511,f2023])).
% 119.47/16.05 fof(f6572,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6512,f4158])).
% 119.47/16.05 fof(f6581,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6512,f655])).
% 119.47/16.05 fof(f6586,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|~ssPv2(skf1(X0))|~ssPv3(X0)|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6512,f160])).
% 119.47/16.05 fof(f6593,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6572])).
% 119.47/16.05 fof(f6594,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6593,f6444])).
% 119.47/16.05 fof(f6600,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv2(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6581])).
% 119.47/16.05 fof(f6601,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6600,f6444])).
% 119.47/16.05 fof(f6606,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|~ssPv2(skf1(X0))|~ssPv3(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6586])).
% 119.47/16.05 fof(f6607,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv1(skf1(X0))|~ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6606,f5543])).
% 119.47/16.05 fof(f6631,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(skf1(X0))))|ssPv2(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6601,f719])).
% 119.47/16.05 fof(f6640,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(skf1(skf1(skf1(X0))))|ssPv2(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6631,f4006])).
% 119.47/16.05 fof(f6641,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv3(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f6210,f6607])).
% 119.47/16.05 fof(f6713,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv3(X0)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6641,f353])).
% 119.47/16.05 fof(f6784,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6368,f982])).
% 119.47/16.05 fof(f6800,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6784])).
% 119.47/16.05 fof(f6810,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(X0))|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6800,f4158])).
% 119.47/16.05 fof(f6832,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(X0))|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6810])).
% 119.47/16.05 fof(f6833,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6832,f2045])).
% 119.47/16.05 fof(f6846,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(X0))|~ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6833,f5674])).
% 119.47/16.05 fof(f6885,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(X0))|ssPv1(skf1(skf1(X0)))|ssPv3(skf1(X0))|~ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6833,f6713])).
% 119.47/16.05 fof(f6899,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(X0))|~ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6846])).
% 119.47/16.05 fof(f6900,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(X0))|~ssPv2(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6899,f273])).
% 119.47/16.05 fof(f6913,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(X0))|ssPv1(skf1(skf1(X0)))|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6885])).
% 119.47/16.05 fof(f6914,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(X0))|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6913,f273])).
% 119.47/16.05 fof(f6921,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f3305,f6900])).
% 119.47/16.05 fof(f6975,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv1(X0)|ssPv2(skf1(X0))|ssPv2(X0)|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6921,f2807])).
% 119.47/16.05 fof(f7005,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv1(X0)|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f6975])).
% 119.47/16.05 fof(f7006,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv2(X0)|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f7005,f4006])).
% 119.47/16.05 fof(f7057,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|ssPv1(X0)|~ssPv4(X0)|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7006,f287])).
% 119.47/16.05 fof(f7074,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|ssPv1(X0)|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f7057,f1740])).
% 119.47/16.05 fof(f7163,plain,(
% 119.47/16.05 ![X0]: (ssPv4(X0)|ssPv3(skf1(X0))|ssPv1(X0)|~ssPv3(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f2241,f7164])).
% 119.47/16.05 fof(f7164,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f6914,f6800])).
% 119.47/16.05 fof(f7209,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv2(skf1(skf1(X0)))|ssPv2(skf1(X0))|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7164,f284])).
% 119.47/16.05 fof(f7210,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|~ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7164,f262])).
% 119.47/16.05 fof(f7233,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv2(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f7209])).
% 119.47/16.05 fof(f7234,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|~ssPv4(X0)|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f7210])).
% 119.47/16.05 fof(f7242,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv1(X0)|ssPv1(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7163,f6446])).
% 119.47/16.05 fof(f7245,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f7242])).
% 119.47/16.05 fof(f7246,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(skf1(X0)))|ssPv1(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f7245,f6594])).
% 119.47/16.05 fof(f7305,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f7246,f6444])).
% 119.47/16.05 fof(f7317,plain,(
% 119.47/16.05 ![X0,X1,X2]: (ssPv1(skf1(X0))|~ssRr(X1,X2)|~ssPv3(X2)|~ssRr(X0,X1)|~ssPv1(X0)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7305,f808])).
% 119.47/16.05 fof(f7324,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7305,f353])).
% 119.47/16.05 fof(f7331,plain,(
% 119.47/16.05 ![X0,X1,X2]: (ssPv1(skf1(X0))|~ssRr(X1,X2)|~ssPv3(X2)|~ssRr(X0,X1)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f7317,f7305])).
% 119.47/16.05 fof(f7356,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(X0)|~ssPv4(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7233,f2049])).
% 119.47/16.05 fof(f7366,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(X0)|~ssPv2(X0)|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7233,f729])).
% 119.47/16.05 fof(f7392,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(X0)|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f7356])).
% 119.47/16.05 fof(f7399,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(X0)|~ssPv2(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f7366])).
% 119.47/16.05 fof(f7400,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f7399,f7006])).
% 119.47/16.05 fof(f7469,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7400,f529])).
% 119.47/16.05 fof(f7502,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(X0)|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f7469])).
% 119.47/16.05 fof(f7503,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f7502,f7234])).
% 119.47/16.05 fof(f7510,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f7392,f7503])).
% 119.47/16.05 fof(f7511,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f5525,f7503])).
% 119.47/16.05 fof(f7516,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7503,f4158])).
% 119.47/16.05 fof(f7536,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f7516])).
% 119.47/16.05 fof(f7570,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7510,f2047])).
% 119.47/16.05 fof(f7584,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv4(X0)|ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7510,f1127])).
% 119.47/16.05 fof(f7593,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f7570])).
% 119.47/16.05 fof(f7598,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv4(X0)|ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f7584])).
% 119.47/16.05 fof(f7600,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f7324,f7593])).
% 119.47/16.05 fof(f7673,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|~ssPv4(skf1(skf1(X0)))|~ssPv3(skf1(skf1(X0)))|~ssPv1(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7511,f364])).
% 119.47/16.05 fof(f7700,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|~ssPv3(skf1(skf1(X0)))|~ssPv1(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f7673,f7503])).
% 119.47/16.05 fof(f7893,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv4(X0)|ssPv1(skf1(skf1(X0)))|~ssPv4(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7598,f2049])).
% 119.47/16.05 fof(f7926,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv4(X0)|ssPv1(skf1(skf1(X0)))|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f7893])).
% 119.47/16.05 fof(f7927,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv4(X0)|ssPv1(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f7926,f2075])).
% 119.47/16.05 fof(f7967,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f7536,f7968])).
% 119.47/16.05 fof(f7968,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|~ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f7700,f7305])).
% 119.47/16.05 fof(f7973,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv4(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f6030,f7967])).
% 119.47/16.05 fof(f8079,plain,(
% 119.47/16.05 ![X0,X1]: (ssPv1(skf1(X0))|~ssPv3(skf1(X1))|~ssRr(X0,X1)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f7331,f52])).
% 119.47/16.05 fof(f8080,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|~ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8079,f52])).
% 119.47/16.05 fof(f8258,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv2(skf1(skf1(skf1(X0))))|~ssPv3(skf1(skf1(X0)))|~ssPv2(skf1(X0))|ssPv2(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f6640,f1095])).
% 119.47/16.05 fof(f8298,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv2(skf1(skf1(skf1(X0))))|~ssPv3(skf1(skf1(X0)))|~ssPv2(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f8258])).
% 119.47/16.05 fof(f8299,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv2(skf1(skf1(skf1(X0))))|~ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f8298,f7968])).
% 119.47/16.05 fof(f8312,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv2(skf1(skf1(skf1(X0))))|ssPv2(X0)|ssPv1(X0)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8299,f7074])).
% 119.47/16.05 fof(f8315,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv2(skf1(skf1(skf1(X0))))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f8312])).
% 119.47/16.05 fof(f8357,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(skf1(X0))|~ssPv1(skf1(skf1(X0)))|~ssPv4(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8315,f159])).
% 119.47/16.05 fof(f8375,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(skf1(X0))|~ssPv1(skf1(skf1(X0)))|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f8357])).
% 119.47/16.05 fof(f8376,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|~ssPv1(skf1(skf1(X0)))|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f8375,f353])).
% 119.47/16.05 fof(f8378,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|~ssPv1(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f8376,f4006])).
% 119.47/16.05 fof(f8380,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv1(X0)|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8378,f7927])).
% 119.47/16.05 fof(f8388,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv4(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f8380])).
% 119.47/16.05 fof(f8431,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|~ssPv1(skf1(X0))|~ssPv4(X0)|ssPv3(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8388,f159])).
% 119.47/16.05 fof(f8434,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv4(skf1(X0))|~ssPv4(X0)|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8388,f287])).
% 119.47/16.05 fof(f8443,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|~ssPv4(X0)|ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f8431,f7305])).
% 119.47/16.05 fof(f8445,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f8434,f2023])).
% 119.47/16.05 fof(f8489,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f8443,f2075])).
% 119.47/16.05 fof(f8490,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv3(X0)|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8489,f8378])).
% 119.47/16.05 fof(f8547,plain,(
% 119.47/16.05 ![X0]: (ssPv3(X0)|ssPv1(X0)|ssPv2(X0)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8490,f363])).
% 119.47/16.05 fof(f8583,plain,(
% 119.47/16.05 ![X0]: (ssPv3(X0)|ssPv1(X0)|ssPv2(X0)|~ssPv4(skf1(X0))|~ssPv3(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f8547])).
% 119.47/16.05 fof(f8584,plain,(
% 119.47/16.05 ![X0]: (ssPv3(X0)|ssPv1(X0)|ssPv2(X0)|~ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f8583,f4006])).
% 119.47/16.05 fof(f8588,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv3(X0)|~ssPv2(skf1(skf1(X0))))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f2560,f8584])).
% 119.47/16.05 fof(f8846,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv4(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f8445,f8080])).
% 119.47/16.05 fof(f8859,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|~ssPv2(skf1(skf1(X0)))|ssPv1(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8846,f5674])).
% 119.47/16.05 fof(f8910,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|~ssPv2(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f8859])).
% 119.47/16.05 fof(f8911,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f8910,f8388])).
% 119.47/16.05 fof(f8925,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f982,f8911])).
% 119.47/16.05 fof(f8926,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(X0)|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8911,f8378])).
% 119.47/16.05 fof(f8950,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f8926])).
% 119.47/16.05 fof(f8961,plain,(
% 119.47/16.05 ![X0,X1,X2]: (~ssRr(X0,X1)|~ssRr(X2,X0)|ssPv3(X1)|ssPv1(X2)|ssPv2(X2))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f636,f8950])).
% 119.47/16.05 fof(f8962,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f655,f8950])).
% 119.47/16.05 fof(f8977,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8950,f4158])).
% 119.47/16.05 fof(f8987,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|~ssPv2(skf1(X0))|~ssPv3(X0)|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8950,f160])).
% 119.47/16.05 fof(f9004,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f8977])).
% 119.47/16.05 fof(f9005,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|~ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9004,f218])).
% 119.47/16.05 fof(f9016,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|~ssPv2(skf1(X0))|~ssPv3(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f8987])).
% 119.47/16.05 fof(f9017,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|~ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9016,f7006])).
% 119.47/16.05 fof(f9026,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|~ssPv2(skf1(skf1(X0))))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f8588,f9017])).
% 119.47/16.05 fof(f9045,plain,(
% 119.47/16.05 ![X0,X1,X2,X3,X4]: (~ssRr(X0,X1)|~ssPv2(X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssRr(X2,X3)|ssPv3(X4)|ssPv1(X2))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f96,f8961])).
% 119.47/16.05 fof(f9053,plain,(
% 119.47/16.05 ![X0,X1,X2,X3,X4,X5,X6]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X3,X4)|~ssPv2(X4)|~ssRr(X2,X3)|~ssRr(X5,X6)|~ssRr(X2,X5)|ssPv1(X6)|ssPv1(X2))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f146,f9045])).
% 119.47/16.05 fof(f9062,plain,(
% 119.47/16.05 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssPv2(skf1(X3))|~ssRr(X2,X3)|~ssRr(X2,X3)|ssPv1(skf1(X3))|ssPv1(X2))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9053,f52])).
% 119.47/16.05 fof(f9069,plain,(
% 119.47/16.05 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssPv2(skf1(X3))|~ssRr(X2,X3)|ssPv1(skf1(X3))|ssPv1(X2))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f9062])).
% 119.47/16.05 fof(f9101,plain,(
% 119.47/16.05 ![X0]: (~ssPv2(skf1(skf1(X0)))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f729,f8962])).
% 119.47/16.05 fof(f9157,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv1(skf1(skf1(X0)))|ssPv2(skf1(skf1(X0))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8962,f9017])).
% 119.47/16.05 fof(f9185,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0)|ssPv2(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9157,f8378])).
% 119.47/16.05 fof(f9198,plain,(
% 119.47/16.05 ![X0,X1]: (~ssPv2(skf1(skf1(X0)))|~ssRr(X0,X1)|~ssPv3(X0)|ssPv2(skf1(X1)))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f1112,f9213])).
% 119.47/16.05 fof(f9213,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9185,f9026])).
% 119.47/16.05 fof(f9252,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|~ssPv4(X0)|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9213,f287])).
% 119.47/16.05 fof(f9264,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9252,f2023])).
% 119.47/16.05 fof(f9311,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(X0)|ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f262,f8925])).
% 119.47/16.05 fof(f9334,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv1(X0)|~ssPv2(skf1(X0))|~ssPv3(X0)|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f8925,f160])).
% 119.47/16.05 fof(f9346,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv1(X0)|~ssPv2(skf1(X0))|~ssPv3(X0))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f9334])).
% 119.47/16.05 fof(f9347,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv1(X0)|~ssPv3(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9346,f7164])).
% 119.47/16.05 fof(f9386,plain,(
% 119.47/16.05 ![X0,X1,X2,X3]: (~ssRr(X0,X1)|~ssRr(X2,X0)|~ssRr(X2,X3)|ssPv1(skf1(X3))|ssPv1(X2))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9069,f9213])).
% 119.47/16.05 fof(f9387,plain,(
% 119.47/16.05 ![X0,X1]: (~ssRr(skf1(X0),X1)|ssPv1(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9386,f52])).
% 119.47/16.05 fof(f9439,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9387,f52])).
% 119.47/16.05 fof(f9550,plain,(
% 119.47/16.05 ![X0]: (~ssPv2(skf1(skf1(X0)))|ssPv3(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f759,f9101])).
% 119.47/16.05 fof(f9577,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f7600,f9578])).
% 119.47/16.05 fof(f9578,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9264,f8080])).
% 119.47/16.05 fof(f9618,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|~ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9578,f364])).
% 119.47/16.05 fof(f9624,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9578,f9347])).
% 119.47/16.05 fof(f9626,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|~ssPv2(skf1(X0))|ssPv4(skf1(skf1(skf1(X0))))|ssPv2(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9578,f717])).
% 119.47/16.05 fof(f9635,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|~ssPv3(skf1(X0))|~ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9618,f2023])).
% 119.47/16.05 fof(f9637,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f9624])).
% 119.47/16.05 fof(f9639,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv4(skf1(skf1(skf1(X0))))|ssPv2(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9626,f9213])).
% 119.47/16.05 fof(f9648,plain,(
% 119.47/16.05 ![X0,X1,X2]: (ssPv2(skf1(X0))|~ssRr(X1,X2)|~ssPv3(X2)|~ssRr(X0,X1)|~ssPv1(X0)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9577,f808])).
% 119.47/16.05 fof(f9656,plain,(
% 119.47/16.05 ![X0,X1,X2]: (ssPv2(skf1(X0))|~ssRr(X1,X2)|~ssPv3(X2)|~ssRr(X0,X1)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9648,f7164])).
% 119.47/16.05 fof(f9696,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|~ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9637,f364])).
% 119.47/16.05 fof(f9715,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|~ssPv4(skf1(X0))|~ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9696,f9578])).
% 119.47/16.05 fof(f9733,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9715,f7305])).
% 119.47/16.05 fof(f9738,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(X0))|~ssPv3(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f353,f9739])).
% 119.47/16.05 fof(f9739,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(skf1(X0)))|~ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9635,f9439])).
% 119.47/16.05 fof(f9747,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(skf1(skf1(X0))))|ssPv2(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9738,f7511])).
% 119.47/16.05 fof(f9751,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(skf1(X0)))|ssPv1(X0)|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9747,f7973])).
% 119.47/16.05 fof(f9778,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9751,f9101])).
% 119.47/16.05 fof(f9807,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f9778])).
% 119.47/16.05 fof(f9808,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0)|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f9807,f7968])).
% 119.47/16.05 fof(f9817,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(skf1(X0)))|~ssPv3(X0)|ssPv1(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f160,f9808])).
% 119.47/16.05 fof(f9994,plain,(
% 119.47/16.05 ![X0,X1]: (ssPv2(skf1(X0))|~ssPv3(skf1(X1))|~ssRr(X0,X1)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9656,f52])).
% 119.47/16.05 fof(f9995,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|~ssPv3(skf1(skf1(X0)))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9994,f52])).
% 119.47/16.05 fof(f10200,plain,(
% 119.47/16.05 ![X0,X1]: (ssPv1(skf1(X0))|ssPv4(skf1(skf1(skf1(X0))))|~ssRr(skf1(X0),X1)|~ssPv3(skf1(X0))|ssPv2(skf1(X1)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f9639,f9198])).
% 119.47/16.05 fof(f10224,plain,(
% 119.47/16.05 ![X0,X1]: (ssPv1(skf1(X0))|~ssRr(skf1(X0),X1)|~ssPv3(skf1(X0))|ssPv2(skf1(X1)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10200,f9817])).
% 119.47/16.05 fof(f10230,plain,(
% 119.47/16.05 ![X0,X1]: (ssPv1(skf1(X0))|~ssRr(skf1(X0),X1)|ssPv2(skf1(X1)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10224,f9578])).
% 119.47/16.05 fof(f10231,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv2(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10230,f52])).
% 119.47/16.05 fof(f10243,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv3(skf1(skf1(skf1(X0))))|ssPv4(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10231,f9550])).
% 119.47/16.05 fof(f10267,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv3(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10243,f9733])).
% 119.47/16.05 fof(f10309,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv4(skf1(skf1(skf1(X0))))|ssPv4(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10267,f529])).
% 119.47/16.05 fof(f10331,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|ssPv4(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10309,f9733])).
% 119.47/16.05 fof(f10338,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|~ssPv3(skf1(X0))|ssPv1(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10331,f9817])).
% 119.47/16.05 fof(f10358,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0))|~ssPv3(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f10338])).
% 119.47/16.05 fof(f10359,plain,(
% 119.47/16.05 ![X0]: (ssPv1(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10358,f9578])).
% 119.47/16.05 fof(f10398,plain,(
% 119.47/16.05 ![X0]: (~ssPv3(skf1(skf1(X0)))|~ssPv1(X0)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f812,f10359])).
% 119.47/16.05 fof(f10410,plain,(
% 119.47/16.05 ![X0]: (~ssPv2(skf1(skf1(X0)))|~ssPv4(X0)|ssPv3(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f159,f10359])).
% 119.47/16.05 fof(f10415,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(skf1(skf1(X0))))|ssPv2(skf1(skf1(skf1(X0))))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10359,f605])).
% 119.47/16.05 fof(f10420,plain,(
% 119.47/16.05 ![X0]: (~ssPv3(skf1(skf1(X0)))|~ssPv4(skf1(X0))|~ssPv1(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f364,f10398])).
% 119.47/16.05 fof(f10491,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(skf1(skf1(X0))))|ssPv3(skf1(X0))|~ssPv4(skf1(skf1(X0)))|~ssPv1(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10415,f10420])).
% 119.47/16.05 fof(f10492,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(skf1(skf1(X0))))|ssPv3(skf1(X0))|~ssPv1(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10415,f10398])).
% 119.47/16.05 fof(f10523,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(skf1(skf1(X0))))|ssPv3(skf1(X0))|~ssPv4(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10491,f10359])).
% 119.47/16.05 fof(f10524,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(skf1(skf1(X0))))|ssPv3(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10492,f10359])).
% 119.47/16.05 fof(f10597,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv3(skf1(skf1(X0)))|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10524,f2047])).
% 119.47/16.05 fof(f10611,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv4(skf1(skf1(X0)))|ssPv2(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10597,f9995])).
% 119.47/16.05 fof(f10613,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv3(skf1(X0))|ssPv4(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f283,f10611])).
% 119.47/16.05 fof(f10643,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv4(X0)|ssPv2(skf1(skf1(skf1(X0))))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10613,f10523])).
% 119.47/16.05 fof(f10669,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv4(X0)|ssPv2(skf1(skf1(skf1(X0)))))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f10643])).
% 119.47/16.05 fof(f10676,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv4(X0)|~ssPv4(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10669,f10410])).
% 119.47/16.05 fof(f10699,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(X0))|ssPv4(X0)|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f10676])).
% 119.47/16.05 fof(f10704,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f3727,f10699])).
% 119.47/16.05 fof(f10712,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0)|ssPv3(skf1(X0))|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10704,f10613])).
% 119.47/16.05 fof(f10715,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|ssPv3(skf1(X0))|ssPv4(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10712,f10699])).
% 119.47/16.05 fof(f10745,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(skf1(X0)))|ssPv2(X0)|ssPv4(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f216,f10715])).
% 119.47/16.05 fof(f10770,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|ssPv4(X0)|~ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10715,f9738])).
% 119.47/16.05 fof(f10784,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|ssPv4(X0)|~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f10770])).
% 119.47/16.05 fof(f10816,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|ssPv4(X0)|ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10745,f2047])).
% 119.47/16.05 fof(f10835,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|ssPv4(X0)|ssPv4(skf1(X0)))),
% 119.47/16.05 inference(duplicate_literals_removal,[status(thm)],[f10816])).
% 119.47/16.05 fof(f10836,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|ssPv4(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10835,f10784])).
% 119.47/16.05 fof(f10858,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv3(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10836,f9550])).
% 119.47/16.05 fof(f10867,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10836,f2047])).
% 119.47/16.05 fof(f10870,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10858,f529])).
% 119.47/16.05 fof(f10872,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv2(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10867,f10704])).
% 119.47/16.05 fof(f10879,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f9005,f10872])).
% 119.47/16.05 fof(f10908,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv1(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f9311,f10870])).
% 119.47/16.05 fof(f10983,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|~ssPv4(skf1(X0))|~ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10879,f10420])).
% 119.47/16.05 fof(f10984,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|~ssPv1(X0)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f10879,f10398])).
% 119.47/16.05 fof(f11004,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|~ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10983,f10872])).
% 119.47/16.05 fof(f11005,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f10984,f9213])).
% 119.47/16.05 fof(f11044,plain,(
% 119.47/16.05 ![X0]: (ssPv2(skf1(X0))|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f9995,f11005])).
% 119.47/16.05 fof(f11097,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(skf1(X0)))|ssPv4(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f9550,f11044])).
% 119.47/16.05 fof(f11126,plain,(
% 119.47/16.05 ![X0]: (ssPv4(X0)|~ssPv1(X0)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f11097,f10398])).
% 119.47/16.05 fof(f11148,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f11126,f10359])).
% 119.47/16.05 fof(f11169,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(X0))|~ssPv1(X0)|ssPv3(skf1(X0)))),
% 119.47/16.05 inference(resolution,[status(thm)],[f11148,f10398])).
% 119.47/16.05 fof(f11243,plain,(
% 119.47/16.05 ![X0]: (ssPv4(skf1(skf1(X0)))|ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(resolution,[status(thm)],[f11169,f10359])).
% 119.47/16.05 fof(f11338,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(X0)|ssPv3(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f10410,f11343])).
% 119.47/16.05 fof(f11343,plain,(
% 119.47/16.05 ![X0]: (ssPv2(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f11004,f9213])).
% 119.47/16.05 fof(f11350,plain,(
% 119.47/16.05 ![X0]: (ssPv3(skf1(skf1(X0))))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f11243,f11338])).
% 119.47/16.05 fof(f11359,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(X0))|~ssPv1(X0))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f10420,f11350])).
% 119.47/16.05 fof(f11364,plain,(
% 119.47/16.05 ![X0]: (~ssPv1(skf1(X0))|ssPv1(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f11359,f10908])).
% 119.47/16.05 fof(f11365,plain,(
% 119.47/16.05 ![X0]: (~ssPv1(skf1(X0))|ssPv4(X0))),
% 119.47/16.05 inference(resolution,[status(thm)],[f11359,f10870])).
% 119.47/16.05 fof(f11367,plain,(
% 119.47/16.05 ![X0]: (ssPv1(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f11364,f10359])).
% 119.47/16.05 fof(f11368,plain,(
% 119.47/16.05 ![X0]: (ssPv4(X0))),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f11365,f10359])).
% 119.47/16.05 fof(f11384,plain,(
% 119.47/16.05 ![X0]: (~ssPv4(skf1(X0)))),
% 119.47/16.05 inference(backward_subsumption_resolution,[status(thm)],[f11359,f11367])).
% 119.47/16.05 fof(f11392,plain,(
% 119.47/16.05 $false),
% 119.47/16.05 inference(forward_subsumption_resolution,[status(thm)],[f11384,f11368])).
% 119.47/16.05 % SZS output end CNFRefutation for theBenchmark.p
% 119.47/16.07 % Elapsed time: 15.620541 seconds
% 119.47/16.07 % CPU time: 123.261341 seconds
% 119.47/16.07 % Total memory used: 94.361 MB
% 119.47/16.07 % Net memory used: 64.069 MB
%------------------------------------------------------------------------------