%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN755-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 : Sun Sep 27 09:39:16 AM UTC 2026
% Result : Unsatisfiable 1.56s 0.61s
% Output : CNFRefutation 1.56s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(clause1,axiom,
! [VAR_0] : ssRr(VAR_0,skf1(VAR_0)),
file('theBenchmark.p',clause1) ).
cnf(c_1,plain,
ssRr(A,skf1(A)),
inference(clausify,[status(thm)],[clause1]) ).
fof(clause2,axiom,
! [VAR_0,VAR_1] :
( ssPv3(VAR_0)
| ssPv2(VAR_0)
| ssPv1(VAR_0)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause2) ).
cnf(c_2,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv1(A)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause2]) ).
fof(clause3,axiom,
! [VAR_0,VAR_1] :
( ssPv4(VAR_0)
| ssPv3(VAR_0)
| ~ ssPv2(VAR_0)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause3) ).
cnf(c_3,plain,
( ssPv4(A)
| ssPv3(A)
| ~ ssPv2(A)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause3]) ).
fof(clause5,axiom,
! [VAR_0,VAR_1] :
( ssPv3(VAR_0)
| ssPv1(VAR_0)
| ~ ssPv2(VAR_0)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause5) ).
cnf(c_5,plain,
( ssPv3(A)
| ssPv1(A)
| ~ ssPv2(A)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause5]) ).
fof(clause6,axiom,
! [VAR_0,VAR_1] :
( ssPv3(VAR_1)
| ~ ssPv4(VAR_0)
| ~ ssPv2(VAR_0)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause6) ).
cnf(c_6,plain,
( ssPv3(B)
| ~ ssPv4(A)
| ~ ssPv2(A)
| ~ ssPv1(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause6]) ).
fof(clause7,axiom,
! [VAR_0,VAR_1] :
( ~ ssPv4(VAR_0)
| ~ ssPv3(VAR_0)
| ~ ssPv2(VAR_0)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause7) ).
cnf(c_7,plain,
( ~ ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv2(A)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause7]) ).
fof(clause8,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_0)
| ssPv2(VAR_0)
| ssPv1(VAR_2)
| ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause8) ).
cnf(c_8,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv1(C)
| ssPv4(B)
| ~ ssRr(A,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause8]) ).
fof(clause9,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_0)
| ssPv1(VAR_2)
| ssPv4(VAR_1)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause9) ).
cnf(c_9,plain,
( ssPv4(A)
| ssPv1(C)
| ssPv4(B)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause9]) ).
fof(clause10,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_0)
| ssPv2(VAR_2)
| ssPv3(VAR_1)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause10) ).
cnf(c_10,plain,
( ssPv3(A)
| ssPv2(C)
| ssPv3(B)
| ~ ssPv2(A)
| ~ ssRr(A,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause10]) ).
fof(clause11,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_0)
| ssPv3(VAR_0)
| ssPv3(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause11) ).
cnf(c_11,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(C)
| ~ ssRr(A,C)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause11]) ).
fof(clause12,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_0)
| ssPv2(VAR_0)
| ssPv4(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause12) ).
cnf(c_12,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv4(C)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause12]) ).
fof(clause15,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_0)
| ssPv1(VAR_0)
| ssPv3(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause15) ).
cnf(c_15,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(C)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause15]) ).
fof(clause16,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_0)
| ssPv1(VAR_0)
| ssPv3(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause16) ).
cnf(c_16,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(C)
| ~ ssRr(A,C)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause16]) ).
fof(clause19,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_0)
| ssPv2(VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause19) ).
cnf(c_19,plain,
( ssPv3(A)
| ssPv2(C)
| ~ ssPv2(A)
| ~ ssRr(A,C)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause19]) ).
fof(clause21,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_0)
| ssPv4(VAR_2)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause21) ).
cnf(c_21,plain,
( ssPv2(A)
| ssPv4(C)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause21]) ).
fof(clause22,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_0)
| ssPv2(VAR_2)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause22) ).
cnf(c_22,plain,
( ssPv2(A)
| ssPv2(C)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause22]) ).
fof(clause24,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_0)
| ssPv2(VAR_0)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause24) ).
cnf(c_24,plain,
( ssPv4(A)
| ssPv2(A)
| ~ ssPv3(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause24]) ).
fof(clause27,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_0)
| ssPv4(VAR_2)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause27) ).
cnf(c_27,plain,
( ssPv1(A)
| ssPv4(C)
| ~ ssPv3(A)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause27]) ).
fof(clause28,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_0)
| ssPv4(VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause28) ).
cnf(c_28,plain,
( ssPv1(A)
| ssPv4(C)
| ~ ssPv2(A)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause28]) ).
fof(clause31,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_2)
| ~ ssPv4(VAR_0)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause31) ).
cnf(c_31,plain,
( ssPv1(C)
| ~ ssPv4(A)
| ~ ssPv2(A)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause31]) ).
fof(clause33,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_0)
| ~ ssPv4(VAR_0)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause33) ).
cnf(c_33,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv3(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause33]) ).
fof(clause34,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_0)
| ~ ssPv4(VAR_0)
| ~ ssPv1(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause34) ).
cnf(c_34,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv1(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause34]) ).
fof(clause36,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_0)
| ~ ssPv3(VAR_0)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause36) ).
cnf(c_36,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv3(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause36]) ).
fof(clause37,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv4(VAR_0)
| ssPv1(VAR_3)
| ssPv3(VAR_2)
| ~ ssRr(VAR_0,VAR_3)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause37) ).
cnf(c_37,plain,
( ssPv4(A)
| ssPv1(D)
| ssPv3(C)
| ~ ssRr(A,D)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause37]) ).
fof(clause42,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv2(VAR_3)
| ssPv3(VAR_2)
| ~ ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_3)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause42) ).
cnf(c_42,plain,
( ssPv2(D)
| ssPv3(C)
| ~ ssPv4(A)
| ~ ssRr(A,D)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause42]) ).
fof(clause45,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv4(VAR_0)
| ssPv2(VAR_3)
| ~ ssRr(VAR_0,VAR_3)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause45) ).
cnf(c_45,plain,
( ssPv4(A)
| ssPv2(D)
| ~ ssRr(A,D)
| ~ ssPv3(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause45]) ).
fof(clause47,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv4(VAR_3)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_3)
| ~ ssPv2(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause47) ).
cnf(c_47,plain,
( ssPv4(D)
| ~ ssPv1(A)
| ~ ssRr(A,D)
| ~ ssPv2(C)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause47]) ).
fof(clause48,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv3(VAR_3)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_3)
| ~ ssPv2(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause48) ).
cnf(c_48,plain,
( ssPv3(D)
| ~ ssPv1(A)
| ~ ssRr(A,D)
| ~ ssPv2(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause48]) ).
fof(clause50,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv4(VAR_3)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_3)
| ~ ssPv1(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause50) ).
cnf(c_50,plain,
( ssPv4(D)
| ~ ssPv3(A)
| ~ ssRr(A,D)
| ~ ssPv1(C)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause50]) ).
fof(clause51,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ ssPv3(VAR_0)
| ~ ssPv1(VAR_3)
| ~ ssRr(VAR_0,VAR_3)
| ~ ssPv2(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause51) ).
cnf(c_51,plain,
( ~ ssPv3(A)
| ~ ssPv1(D)
| ~ ssRr(A,D)
| ~ ssPv2(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause51]) ).
cnf(c_52,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv1(B)
| ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_8]) ).
cnf(c_53,plain,
( ssPv4(A)
| ssPv1(B)
| ssPv4(B)
| ~ ssPv1(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_9]) ).
cnf(c_55,plain,
( ssPv3(A)
| ssPv2(B)
| ssPv3(B)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_10]) ).
cnf(c_57,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(B)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_11]) ).
cnf(c_59,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv4(B)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_12]) ).
cnf(c_63,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(B)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_15]) ).
cnf(c_64,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(B)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_16]) ).
cnf(c_67,plain,
( ssPv3(A)
| ssPv2(B)
| ~ ssPv2(A)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_19]) ).
cnf(c_69,plain,
( ssPv2(A)
| ssPv4(B)
| ~ ssPv1(A)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_21]) ).
cnf(c_70,plain,
( ssPv2(A)
| ssPv2(B)
| ~ ssPv1(A)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_22]) ).
cnf(c_73,plain,
( ssPv4(A)
| ssPv2(A)
| ~ ssPv3(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_24]) ).
cnf(c_75,plain,
( ssPv1(A)
| ssPv4(B)
| ~ ssPv3(A)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_27]) ).
cnf(c_77,plain,
( ssPv1(A)
| ssPv4(B)
| ~ ssPv2(A)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_28]) ).
cnf(c_79,plain,
( ssPv1(B)
| ~ ssPv4(A)
| ~ ssPv2(A)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_31]) ).
cnf(c_81,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv3(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_33]) ).
cnf(c_82,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv1(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_85,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv3(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_36]) ).
cnf(c_87,plain,
( ssPv4(A)
| ssPv1(C)
| ssPv3(B)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_37]) ).
cnf(c_99,plain,
( ssPv2(C)
| ssPv3(B)
| ~ ssPv4(A)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_42]) ).
cnf(c_108,plain,
( ssPv4(A)
| ssPv2(C)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_45]) ).
cnf(c_113,plain,
( ssPv4(C)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_47]) ).
cnf(c_116,plain,
( ssPv3(C)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_48]) ).
cnf(c_122,plain,
( ssPv4(C)
| ~ ssPv3(A)
| ~ ssRr(A,C)
| ~ ssPv1(B)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_50]) ).
cnf(c_126,plain,
( ~ ssPv3(A)
| ~ ssPv1(C)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_51]) ).
cnf(c_136,plain,
( ssPv4(A)
| ssPv1(B)
| ssPv3(B)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_87]) ).
cnf(c_137,plain,
( ssPv2(B)
| ssPv3(B)
| ~ ssPv4(A)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_99]) ).
cnf(c_142,plain,
( ssPv4(A)
| ssPv2(B)
| ~ ssPv3(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_108]) ).
cnf(c_143,plain,
( ssPv4(B)
| ~ ssPv1(A)
| ~ ssPv2(B)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_113]) ).
cnf(c_144,plain,
( ssPv3(B)
| ~ ssPv1(A)
| ~ ssPv2(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_116]) ).
cnf(c_147,plain,
( ssPv4(B)
| ~ ssPv3(A)
| ~ ssPv1(B)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_122]) ).
cnf(c_151,plain,
( ~ ssPv3(A)
| ~ ssPv1(B)
| ~ ssPv2(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_126]) ).
cnf(c_154,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv1(A)
| ~ ssPv1(skf1(A)) ),
inference(resolve,[status(thm)],[c_2,c_1]) ).
cnf(c_155,plain,
( ssPv4(A)
| ssPv3(A)
| ~ ssPv2(A)
| ~ ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_3,c_1]) ).
cnf(c_157,plain,
( ssPv3(A)
| ssPv1(A)
| ~ ssPv2(A)
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_5,c_1]) ).
cnf(c_158,plain,
( ssPv3(skf1(A))
| ~ ssPv4(A)
| ~ ssPv2(A)
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_6,c_1]) ).
cnf(c_159,plain,
( ~ ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv2(A)
| ~ ssPv1(skf1(A)) ),
inference(resolve,[status(thm)],[c_7,c_1]) ).
cnf(c_328,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv1(skf1(A))
| ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_52,c_1]) ).
cnf(c_329,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv4(skf1(A))
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_53,c_1]) ).
cnf(c_330,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(A))
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_55,c_1]) ).
cnf(c_331,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ~ ssPv1(skf1(A)) ),
inference(resolve,[status(thm)],[c_57,c_1]) ).
cnf(c_332,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ~ ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_59,c_1]) ).
cnf(c_334,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(skf1(A))
| ~ ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_63,c_1]) ).
cnf(c_335,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(skf1(A))
| ~ ssPv1(skf1(A)) ),
inference(resolve,[status(thm)],[c_64,c_1]) ).
cnf(c_337,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ~ ssPv2(A)
| ~ ssPv1(skf1(A)) ),
inference(resolve,[status(thm)],[c_67,c_1]) ).
cnf(c_338,plain,
( ssPv2(A)
| ssPv4(skf1(A))
| ~ ssPv1(A)
| ~ ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_69,c_1]) ).
cnf(c_339,plain,
( ssPv2(A)
| ssPv2(skf1(A))
| ~ ssPv1(A)
| ~ ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_70,c_1]) ).
cnf(c_340,plain,
( ssPv4(A)
| ssPv2(A)
| ~ ssPv3(skf1(A))
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_73,c_1]) ).
cnf(c_341,plain,
( ssPv1(A)
| ssPv4(skf1(A))
| ~ ssPv3(A)
| ~ ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_75,c_1]) ).
cnf(c_342,plain,
( ssPv1(A)
| ssPv4(skf1(A))
| ~ ssPv2(A)
| ~ ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_77,c_1]) ).
cnf(c_344,plain,
( ssPv1(skf1(A))
| ~ ssPv4(A)
| ~ ssPv2(A)
| ~ ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_79,c_1]) ).
cnf(c_345,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv3(skf1(A))
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_81,c_1]) ).
cnf(c_346,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv1(skf1(A))
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_82,c_1]) ).
cnf(c_348,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv3(skf1(A))
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_85,c_1]) ).
cnf(c_390,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv3(skf1(A))
| ~ ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_136,c_1]) ).
cnf(c_391,plain,
( ssPv2(skf1(A))
| ssPv3(skf1(A))
| ~ ssPv4(A)
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_137,c_1]) ).
cnf(c_393,plain,
( ssPv4(A)
| ssPv2(skf1(A))
| ~ ssPv3(skf1(A))
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_142,c_1]) ).
cnf(c_394,plain,
( ssPv4(skf1(A))
| ~ ssPv1(A)
| ~ ssPv2(skf1(A))
| ~ ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_143,c_1]) ).
cnf(c_395,plain,
( ssPv3(skf1(A))
| ~ ssPv1(A)
| ~ ssPv2(skf1(A))
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_144,c_1]) ).
cnf(c_396,plain,
( ssPv4(skf1(A))
| ~ ssPv3(A)
| ~ ssPv1(skf1(A))
| ~ ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_147,c_1]) ).
cnf(c_397,plain,
( ~ ssPv3(A)
| ~ ssPv1(skf1(A))
| ~ ssPv2(skf1(A))
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_151,c_1]) ).
cnf(c_967,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv1(A)
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_328,c_154]) ).
cnf(c_968,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A)) ),
inference(copy,[status(thm)],[c_967]) ).
cnf(c_398,plain,
( ssPv1(A)
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A)) ),
inference(copy,[status(thm)],[c_968]) ).
cnf(c_969,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv4(skf1(A))
| ssPv1(skf1(skf1(A)))
| ssPv4(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_329,c_328]) ).
cnf(c_401,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv1(skf1(skf1(A)))
| ssPv4(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_969]) ).
cnf(c_970,plain,
( ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_331,c_398]) ).
cnf(c_402,plain,
( ssPv2(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_970]) ).
cnf(c_971,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_331,c_328]) ).
cnf(c_403,plain,
( ssPv2(A)
| ssPv4(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_971]) ).
cnf(c_972,plain,
( ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_335,c_398]) ).
cnf(c_404,plain,
( ssPv2(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_972]) ).
cnf(c_973,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv2(A)
| ssPv4(skf1(A))
| ~ ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_338,c_398]) ).
cnf(c_974,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ~ ssPv2(skf1(A)) ),
inference(copy,[status(thm)],[c_973]) ).
cnf(c_405,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ~ ssPv2(skf1(A)) ),
inference(copy,[status(thm)],[c_974]) ).
cnf(c_975,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ~ ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_339,c_398]) ).
cnf(c_407,plain,
( ssPv3(A)
| ssPv4(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ~ ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_975]) ).
cnf(c_410,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(skf1(skf1(A)))
| ~ ssPv2(skf1(skf1(A)))
| ~ ssPv4(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_395,c_328]) ).
cnf(c_413,plain,
( ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ~ ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_402,c_391]) ).
cnf(c_976,plain,
( ssPv3(skf1(A))
| ~ ssPv4(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_402,c_345]) ).
cnf(c_414,plain,
( ~ ssPv4(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_976]) ).
cnf(c_977,plain,
( ssPv4(skf1(A))
| ssPv2(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_402,c_340]) ).
cnf(c_417,plain,
( ssPv4(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_977]) ).
cnf(c_422,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv4(skf1(skf1(skf1(A))))
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_404,c_331]) ).
cnf(c_978,plain,
( ssPv4(skf1(A))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv4(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_401,c_331]) ).
cnf(c_431,plain,
( ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv4(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_978]) ).
cnf(c_979,plain,
( ssPv2(A)
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_414,c_403]) ).
cnf(c_980,plain,
( ssPv2(A)
| ssPv4(A)
| ssPv3(A)
| ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_979]) ).
cnf(c_981,plain,
( ssPv2(A)
| ssPv4(A)
| ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_980]) ).
cnf(c_433,plain,
( ssPv2(A)
| ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_981]) ).
cnf(c_982,plain,
( ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(skf1(skf1(A)))
| ~ ssPv2(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_410,c_431]) ).
cnf(c_983,plain,
( ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(A)
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(skf1(skf1(A)))
| ~ ssPv2(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_982]) ).
cnf(c_984,plain,
( ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(skf1(skf1(A)))
| ~ ssPv2(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_983]) ).
cnf(c_985,plain,
( ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(skf1(skf1(A)))
| ~ ssPv2(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_984]) ).
cnf(c_436,plain,
( ssPv3(skf1(A))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(skf1(skf1(A)))
| ~ ssPv2(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_985]) ).
cnf(c_986,plain,
( ssPv2(A)
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_413,c_403]) ).
cnf(c_987,plain,
( ssPv2(A)
| ssPv4(A)
| ssPv3(A)
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_986]) ).
cnf(c_988,plain,
( ssPv2(A)
| ssPv4(A)
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_987]) ).
cnf(c_438,plain,
( ssPv2(A)
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_988]) ).
cnf(c_989,plain,
( ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_438,c_413]) ).
cnf(c_990,plain,
( ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_989]) ).
cnf(c_991,plain,
( ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv4(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_990]) ).
cnf(c_992,plain,
( ssPv2(skf1(skf1(A)))
| ssPv4(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_991]) ).
cnf(c_439,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_992]) ).
cnf(c_993,plain,
( ssPv2(skf1(A))
| ssPv3(skf1(A))
| ~ ssPv4(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_438,c_391]) ).
cnf(c_994,plain,
( ssPv2(skf1(A))
| ~ ssPv4(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_993]) ).
cnf(c_440,plain,
( ~ ssPv4(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_994]) ).
cnf(c_995,plain,
( ssPv3(skf1(skf1(A)))
| ~ ssPv4(skf1(skf1(A)))
| ~ ssPv3(skf1(skf1(skf1(A))))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_422,c_345]) ).
cnf(c_452,plain,
( ~ ssPv4(skf1(skf1(A)))
| ~ ssPv3(skf1(skf1(skf1(A))))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_995]) ).
cnf(c_996,plain,
( ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ~ ssPv3(skf1(skf1(skf1(A))))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_452,c_402]) ).
cnf(c_997,plain,
( ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ~ ssPv3(skf1(skf1(skf1(A))))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_996]) ).
cnf(c_998,plain,
( ssPv2(skf1(A))
| ssPv4(A)
| ~ ssPv3(skf1(skf1(skf1(A))))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_997]) ).
cnf(c_999,plain,
( ssPv2(skf1(A))
| ~ ssPv3(skf1(skf1(skf1(A))))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_998]) ).
cnf(c_465,plain,
( ~ ssPv3(skf1(skf1(skf1(A))))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_999]) ).
cnf(c_1000,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_440,c_439]) ).
cnf(c_1001,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1000]) ).
cnf(c_1002,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1001]) ).
cnf(c_1003,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1002]) ).
cnf(c_1004,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1003]) ).
cnf(c_1005,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1004]) ).
cnf(c_470,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(skf1(A))))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1005]) ).
cnf(c_1006,plain,
( ssPv3(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_470,c_436]) ).
cnf(c_1007,plain,
( ssPv3(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1006]) ).
cnf(c_1008,plain,
( ssPv3(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1007]) ).
cnf(c_1009,plain,
( ssPv3(skf1(skf1(A)))
| ssPv4(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1008]) ).
cnf(c_472,plain,
( ssPv4(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1009]) ).
cnf(c_1010,plain,
( ssPv2(skf1(skf1(A)))
| ssPv1(skf1(skf1(A)))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_470,c_334]) ).
cnf(c_1011,plain,
( ssPv2(skf1(skf1(A)))
| ssPv1(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1010]) ).
cnf(c_476,plain,
( ssPv1(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1011]) ).
cnf(c_1012,plain,
( ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ~ ssPv4(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_472,c_391]) ).
cnf(c_1013,plain,
( ssPv2(skf1(skf1(A)))
| ~ ssPv4(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1012]) ).
cnf(c_478,plain,
( ~ ssPv4(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1013]) ).
cnf(c_1014,plain,
( ssPv4(skf1(A))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_476,c_331]) ).
cnf(c_1015,plain,
( ssPv4(skf1(A))
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1014]) ).
cnf(c_481,plain,
( ssPv4(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1015]) ).
cnf(c_1016,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_481,c_478]) ).
cnf(c_1017,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1016]) ).
cnf(c_1018,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1017]) ).
cnf(c_1019,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1018]) ).
cnf(c_1020,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1019]) ).
cnf(c_1021,plain,
( ssPv3(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1020]) ).
cnf(c_496,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1021]) ).
cnf(c_1022,plain,
( ssPv3(skf1(A))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_496,c_436]) ).
cnf(c_1023,plain,
( ssPv3(skf1(A))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1022]) ).
cnf(c_1024,plain,
( ssPv3(skf1(A))
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1023]) ).
cnf(c_497,plain,
( ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1024]) ).
cnf(c_1025,plain,
( ssPv2(skf1(A))
| ssPv1(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_496,c_334]) ).
cnf(c_1026,plain,
( ssPv2(skf1(A))
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1025]) ).
cnf(c_501,plain,
( ssPv1(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1026]) ).
cnf(c_1027,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_501,c_331]) ).
cnf(c_1028,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1027]) ).
cnf(c_505,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1028]) ).
cnf(c_1029,plain,
( ssPv2(skf1(A))
| ssPv3(skf1(A))
| ~ ssPv4(A)
| ssPv2(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_497,c_391]) ).
cnf(c_1030,plain,
( ssPv2(skf1(A))
| ~ ssPv4(A)
| ssPv2(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1029]) ).
cnf(c_510,plain,
( ~ ssPv4(A)
| ssPv2(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1030]) ).
cnf(c_1031,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv2(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_510,c_505]) ).
cnf(c_1032,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1031]) ).
cnf(c_1033,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1032]) ).
cnf(c_1034,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1033]) ).
cnf(c_1035,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1034]) ).
cnf(c_511,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1035]) ).
cnf(c_1036,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_511,c_405]) ).
cnf(c_1037,plain,
( ssPv3(A)
| ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1036]) ).
cnf(c_514,plain,
( ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1037]) ).
cnf(c_1038,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_511,c_334]) ).
cnf(c_1039,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1038]) ).
cnf(c_516,plain,
( ssPv1(A)
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1039]) ).
cnf(c_1040,plain,
( ssPv3(skf1(A))
| ~ ssPv2(skf1(A))
| ~ ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_516,c_395]) ).
cnf(c_518,plain,
( ~ ssPv2(skf1(A))
| ~ ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1040]) ).
cnf(c_1041,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_518,c_514]) ).
cnf(c_1042,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1041]) ).
cnf(c_1043,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1042]) ).
cnf(c_1044,plain,
( ssPv2(A)
| ssPv3(A)
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1043]) ).
cnf(c_1045,plain,
( ssPv2(A)
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1044]) ).
cnf(c_529,plain,
( ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1045]) ).
cnf(c_1046,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_529,c_511]) ).
cnf(c_1047,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1046]) ).
cnf(c_1048,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1047]) ).
cnf(c_1049,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1048]) ).
cnf(c_1050,plain,
( ssPv2(A)
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1049]) ).
cnf(c_530,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1050]) ).
cnf(c_1051,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_530,c_330]) ).
cnf(c_1052,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1051]) ).
cnf(c_535,plain,
( ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1052]) ).
cnf(c_1053,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_535,c_390]) ).
cnf(c_538,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1053]) ).
cnf(c_1054,plain,
( ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_535,c_330]) ).
cnf(c_1055,plain,
( ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1054]) ).
cnf(c_539,plain,
( ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1055]) ).
cnf(c_1056,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_538,c_331]) ).
cnf(c_1057,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1056]) ).
cnf(c_1058,plain,
( ssPv4(A)
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1057]) ).
cnf(c_541,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1058]) ).
cnf(c_544,plain,
( ssPv1(skf1(A))
| ~ ssPv2(A)
| ~ ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_541,c_344]) ).
cnf(c_1059,plain,
( ssPv4(skf1(A))
| ssPv1(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_539,c_390]) ).
cnf(c_547,plain,
( ssPv4(skf1(A))
| ssPv1(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1059]) ).
cnf(c_1060,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_544,c_535]) ).
cnf(c_1061,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1060]) ).
cnf(c_1062,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1061]) ).
cnf(c_1063,plain,
( ssPv3(A)
| ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1062]) ).
cnf(c_550,plain,
( ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1063]) ).
cnf(c_1064,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_550,c_530]) ).
cnf(c_1065,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1064]) ).
cnf(c_1066,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1065]) ).
cnf(c_1067,plain,
( ssPv3(A)
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1066]) ).
cnf(c_553,plain,
( ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1067]) ).
cnf(c_1068,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_553,c_346]) ).
cnf(c_555,plain,
( ~ ssPv4(A)
| ~ ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1068]) ).
cnf(c_1069,plain,
( ssPv4(skf1(A))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_547,c_331]) ).
cnf(c_1070,plain,
( ssPv4(skf1(A))
| ssPv3(skf1(A))
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1069]) ).
cnf(c_1071,plain,
( ssPv4(skf1(A))
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1070]) ).
cnf(c_565,plain,
( ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1071]) ).
cnf(c_1072,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_565,c_555]) ).
cnf(c_1073,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1072]) ).
cnf(c_1074,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1073]) ).
cnf(c_1075,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1074]) ).
cnf(c_567,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1075]) ).
cnf(c_1076,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_567,c_541]) ).
cnf(c_1077,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1076]) ).
cnf(c_1078,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1077]) ).
cnf(c_1079,plain,
( ssPv3(A)
| ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1078]) ).
cnf(c_570,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(skf1(A))))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1079]) ).
cnf(c_1080,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_570,c_465]) ).
cnf(c_1081,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1080]) ).
cnf(c_1082,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1081]) ).
cnf(c_571,plain,
( ssPv4(A)
| ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1082]) ).
cnf(c_1083,plain,
( ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv4(skf1(A))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_570,c_433]) ).
cnf(c_1084,plain,
( ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv4(skf1(A))
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1083]) ).
cnf(c_574,plain,
( ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1084]) ).
cnf(c_1085,plain,
( ssPv2(skf1(A))
| ssPv3(skf1(A))
| ~ ssPv4(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_574,c_391]) ).
cnf(c_1086,plain,
( ssPv2(skf1(A))
| ~ ssPv4(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1085]) ).
cnf(c_582,plain,
( ~ ssPv4(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1086]) ).
cnf(c_1087,plain,
( ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_582,c_571]) ).
cnf(c_1088,plain,
( ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1087]) ).
cnf(c_1089,plain,
( ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1088]) ).
cnf(c_1090,plain,
( ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1089]) ).
cnf(c_1091,plain,
( ssPv2(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1090]) ).
cnf(c_583,plain,
( ssPv2(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1091]) ).
cnf(c_1092,plain,
( ssPv3(skf1(A))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_583,c_436]) ).
cnf(c_1093,plain,
( ssPv3(skf1(A))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1092]) ).
cnf(c_1094,plain,
( ssPv3(skf1(A))
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1093]) ).
cnf(c_584,plain,
( ssPv2(A)
| ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1094]) ).
cnf(c_1095,plain,
( ssPv2(skf1(A))
| ssPv1(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_583,c_334]) ).
cnf(c_1096,plain,
( ssPv2(skf1(A))
| ssPv1(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1095]) ).
cnf(c_590,plain,
( ssPv1(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1096]) ).
cnf(c_1097,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_590,c_331]) ).
cnf(c_1098,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1097]) ).
cnf(c_593,plain,
( ssPv4(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1098]) ).
cnf(c_1099,plain,
( ssPv2(skf1(A))
| ssPv3(skf1(A))
| ~ ssPv4(A)
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_584,c_391]) ).
cnf(c_1100,plain,
( ssPv2(skf1(A))
| ~ ssPv4(A)
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1099]) ).
cnf(c_598,plain,
( ~ ssPv4(A)
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1100]) ).
cnf(c_1101,plain,
( ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_598,c_593]) ).
cnf(c_1102,plain,
( ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1101]) ).
cnf(c_1103,plain,
( ssPv2(skf1(A))
| ssPv3(A)
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1102]) ).
cnf(c_1104,plain,
( ssPv2(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1103]) ).
cnf(c_599,plain,
( ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1104]) ).
cnf(c_1105,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_599,c_405]) ).
cnf(c_1106,plain,
( ssPv3(A)
| ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1105]) ).
cnf(c_601,plain,
( ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1106]) ).
cnf(c_1107,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_599,c_334]) ).
cnf(c_1108,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1107]) ).
cnf(c_603,plain,
( ssPv1(A)
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1108]) ).
cnf(c_1109,plain,
( ssPv3(skf1(A))
| ~ ssPv2(skf1(A))
| ~ ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_603,c_395]) ).
cnf(c_605,plain,
( ~ ssPv2(skf1(A))
| ~ ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1109]) ).
cnf(c_1110,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_605,c_601]) ).
cnf(c_1111,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1110]) ).
cnf(c_1112,plain,
( ssPv2(A)
| ssPv3(A)
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1111]) ).
cnf(c_1113,plain,
( ssPv2(A)
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1112]) ).
cnf(c_616,plain,
( ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1113]) ).
cnf(c_1114,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_616,c_599]) ).
cnf(c_1115,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1114]) ).
cnf(c_1116,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1115]) ).
cnf(c_1117,plain,
( ssPv2(A)
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1116]) ).
cnf(c_617,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1117]) ).
cnf(c_1118,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_617,c_330]) ).
cnf(c_1119,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1118]) ).
cnf(c_624,plain,
( ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1119]) ).
cnf(c_1120,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_624,c_390]) ).
cnf(c_626,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1120]) ).
cnf(c_1121,plain,
( ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_624,c_330]) ).
cnf(c_1122,plain,
( ssPv3(skf1(A))
| ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1121]) ).
cnf(c_627,plain,
( ssPv2(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1122]) ).
cnf(c_1123,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_626,c_331]) ).
cnf(c_1124,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1123]) ).
cnf(c_1125,plain,
( ssPv4(A)
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1124]) ).
cnf(c_629,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1125]) ).
cnf(c_632,plain,
( ssPv1(skf1(A))
| ~ ssPv2(A)
| ~ ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_629,c_344]) ).
cnf(c_1126,plain,
( ssPv4(skf1(A))
| ssPv1(skf1(skf1(A)))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_627,c_390]) ).
cnf(c_634,plain,
( ssPv4(skf1(A))
| ssPv1(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1126]) ).
cnf(c_1127,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_632,c_624]) ).
cnf(c_1128,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1127]) ).
cnf(c_1129,plain,
( ssPv3(A)
| ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1128]) ).
cnf(c_637,plain,
( ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1129]) ).
cnf(c_1130,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_637,c_617]) ).
cnf(c_1131,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1130]) ).
cnf(c_1132,plain,
( ssPv3(A)
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1131]) ).
cnf(c_638,plain,
( ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1132]) ).
cnf(c_1133,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_638,c_346]) ).
cnf(c_642,plain,
( ~ ssPv4(A)
| ~ ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1133]) ).
cnf(c_1134,plain,
( ssPv4(skf1(A))
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_634,c_331]) ).
cnf(c_1135,plain,
( ssPv4(skf1(A))
| ssPv3(skf1(A))
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1134]) ).
cnf(c_1136,plain,
( ssPv4(skf1(A))
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1135]) ).
cnf(c_645,plain,
( ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1136]) ).
cnf(c_1137,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_645,c_642]) ).
cnf(c_1138,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1137]) ).
cnf(c_1139,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1138]) ).
cnf(c_647,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1139]) ).
cnf(c_1140,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_647,c_629]) ).
cnf(c_1141,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1140]) ).
cnf(c_1142,plain,
( ssPv3(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1141]) ).
cnf(c_649,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1142]) ).
cnf(c_1143,plain,
( ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_649,c_417]) ).
cnf(c_1144,plain,
( ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1143]) ).
cnf(c_653,plain,
( ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1144]) ).
cnf(c_656,plain,
( ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_649,c_332]) ).
cnf(c_1145,plain,
( ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_653,c_414]) ).
cnf(c_1146,plain,
( ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1145]) ).
cnf(c_1147,plain,
( ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1146]) ).
cnf(c_1148,plain,
( ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1147]) ).
cnf(c_660,plain,
( ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1148]) ).
cnf(c_1149,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_660,c_649]) ).
cnf(c_1150,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1149]) ).
cnf(c_661,plain,
( ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1150]) ).
cnf(c_1151,plain,
( ssPv4(skf1(A))
| ssPv2(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_656,c_340]) ).
cnf(c_1152,plain,
( ssPv4(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1151]) ).
cnf(c_666,plain,
( ~ ssPv3(skf1(skf1(A)))
| ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1152]) ).
cnf(c_1153,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_666,c_649]) ).
cnf(c_1154,plain,
( ssPv3(A)
| ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1153]) ).
cnf(c_674,plain,
( ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1154]) ).
cnf(c_1155,plain,
( ssPv2(skf1(A))
| ssPv3(skf1(A))
| ~ ssPv4(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_674,c_391]) ).
cnf(c_1156,plain,
( ssPv2(skf1(A))
| ~ ssPv4(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1155]) ).
cnf(c_675,plain,
( ~ ssPv4(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1156]) ).
cnf(c_1157,plain,
( ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_675,c_661]) ).
cnf(c_1158,plain,
( ssPv2(skf1(A))
| ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1157]) ).
cnf(c_1159,plain,
( ssPv2(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1158]) ).
cnf(c_676,plain,
( ssPv2(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1159]) ).
cnf(c_1160,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_676,c_405]) ).
cnf(c_680,plain,
( ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1160]) ).
cnf(c_1161,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_676,c_390]) ).
cnf(c_681,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1161]) ).
cnf(c_1162,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_676,c_334]) ).
cnf(c_683,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1162]) ).
cnf(c_1163,plain,
( ssPv4(skf1(A))
| ssPv3(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_676,c_155]) ).
cnf(c_684,plain,
( ssPv4(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1163]) ).
cnf(c_1164,plain,
( ssPv3(skf1(A))
| ~ ssPv2(skf1(A))
| ~ ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_683,c_395]) ).
cnf(c_685,plain,
( ~ ssPv2(skf1(A))
| ~ ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1164]) ).
cnf(c_1165,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_681,c_331]) ).
cnf(c_1166,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1165]) ).
cnf(c_1167,plain,
( ssPv4(A)
| ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1166]) ).
cnf(c_697,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1167]) ).
cnf(c_1168,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A))
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_685,c_680]) ).
cnf(c_1169,plain,
( ssPv2(A)
| ssPv3(A)
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1168]) ).
cnf(c_1170,plain,
( ssPv2(A)
| ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1169]) ).
cnf(c_702,plain,
( ~ ssPv2(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1170]) ).
cnf(c_1171,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_702,c_676]) ).
cnf(c_1172,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1171]) ).
cnf(c_703,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1172]) ).
cnf(c_1173,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_684,c_649]) ).
cnf(c_1174,plain,
( ssPv3(A)
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1173]) ).
cnf(c_708,plain,
( ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1174]) ).
cnf(c_1175,plain,
( ssPv3(A)
| ssPv1(A)
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_708,c_157]) ).
cnf(c_712,plain,
( ssPv1(A)
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1175]) ).
cnf(c_1176,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv1(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_712,c_703]) ).
cnf(c_1177,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1176]) ).
cnf(c_713,plain,
( ssPv1(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1177]) ).
cnf(c_1178,plain,
( ssPv3(skf1(A))
| ~ ssPv4(A)
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_713,c_158]) ).
cnf(c_718,plain,
( ~ ssPv4(A)
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1178]) ).
cnf(c_1179,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_718,c_697]) ).
cnf(c_1180,plain,
( ssPv3(A)
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1179]) ).
cnf(c_719,plain,
( ~ ssPv2(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1180]) ).
cnf(c_1181,plain,
( ssPv3(A)
| ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_719,c_703]) ).
cnf(c_1182,plain,
( ssPv3(A)
| ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1181]) ).
cnf(c_720,plain,
( ssPv3(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1182]) ).
cnf(c_1183,plain,
( ssPv3(A)
| ssPv4(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_720,c_407]) ).
cnf(c_725,plain,
( ssPv4(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1183]) ).
cnf(c_726,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_720,c_332]) ).
cnf(c_1184,plain,
( ssPv4(A)
| ssPv2(A)
| ~ ssPv3(skf1(A))
| ssPv4(A)
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_726,c_340]) ).
cnf(c_1185,plain,
( ssPv4(A)
| ~ ssPv3(skf1(A))
| ssPv4(A)
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1184]) ).
cnf(c_738,plain,
( ~ ssPv3(skf1(A))
| ssPv4(A)
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1185]) ).
cnf(c_1186,plain,
( ssPv3(A)
| ssPv4(A)
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_738,c_720]) ).
cnf(c_739,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1186]) ).
cnf(c_1187,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv3(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_725,c_345]) ).
cnf(c_744,plain,
( ~ ssPv4(A)
| ~ ssPv3(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1187]) ).
cnf(c_1188,plain,
( ssPv2(A)
| ssPv3(A)
| ~ ssPv3(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_744,c_739]) ).
cnf(c_1189,plain,
( ssPv2(A)
| ~ ssPv3(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1188]) ).
cnf(c_750,plain,
( ~ ssPv3(skf1(A))
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1189]) ).
cnf(c_1190,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_750,c_720]) ).
cnf(c_751,plain,
( ssPv2(A)
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1190]) ).
cnf(c_1191,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_751,c_405]) ).
cnf(c_1192,plain,
( ssPv3(A)
| ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1191]) ).
cnf(c_753,plain,
( ssPv4(skf1(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1192]) ).
cnf(c_1193,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_753,c_345]) ).
cnf(c_756,plain,
( ~ ssPv4(A)
| ~ ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1193]) ).
cnf(c_1194,plain,
( ssPv2(A)
| ssPv3(A)
| ~ ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_756,c_739]) ).
cnf(c_1195,plain,
( ssPv2(A)
| ~ ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1194]) ).
cnf(c_759,plain,
( ~ ssPv3(skf1(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1195]) ).
cnf(c_1196,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_759,c_720]) ).
cnf(c_760,plain,
( ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1196]) ).
cnf(c_1197,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv3(skf1(A))
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_760,c_390]) ).
cnf(c_762,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1197]) ).
cnf(c_763,plain,
( ssPv1(A)
| ssPv4(skf1(A))
| ~ ssPv3(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_760,c_342]) ).
cnf(c_1198,plain,
( ssPv4(A)
| ssPv3(A)
| ~ ssPv3(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_760,c_155]) ).
cnf(c_765,plain,
( ssPv4(A)
| ~ ssPv3(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1198]) ).
cnf(c_767,plain,
( ~ ssPv3(A)
| ~ ssPv2(skf1(A))
| ~ ssPv4(skf1(A))
| ssPv4(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_762,c_397]) ).
cnf(c_1199,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv4(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_763,c_720]) ).
cnf(c_770,plain,
( ssPv1(A)
| ssPv4(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1199]) ).
cnf(c_1200,plain,
( ssPv3(A)
| ssPv4(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_765,c_720]) ).
cnf(c_777,plain,
( ssPv4(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1200]) ).
cnf(c_778,plain,
( ssPv1(skf1(A))
| ~ ssPv2(A)
| ~ ssPv2(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_777,c_344]) ).
cnf(c_1201,plain,
( ssPv4(skf1(A))
| ~ ssPv2(skf1(A))
| ~ ssPv3(skf1(A))
| ssPv4(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_770,c_394]) ).
cnf(c_780,plain,
( ~ ssPv2(skf1(A))
| ~ ssPv3(skf1(A))
| ssPv4(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1201]) ).
cnf(c_1202,plain,
( ssPv3(skf1(A))
| ~ ssPv3(A)
| ~ ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_767,c_777]) ).
cnf(c_784,plain,
( ~ ssPv3(A)
| ~ ssPv2(skf1(A))
| ssPv4(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1202]) ).
cnf(c_1203,plain,
( ssPv3(skf1(A))
| ~ ssPv3(A)
| ssPv4(A)
| ssPv3(skf1(A)) ),
inference(resolve,[status(thm)],[c_784,c_760]) ).
cnf(c_788,plain,
( ~ ssPv3(A)
| ssPv4(A)
| ssPv3(skf1(A)) ),
inference(copy,[status(thm)],[c_1203]) ).
cnf(c_789,plain,
( ssPv3(A)
| ssPv4(skf1(A))
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_788,c_720]) ).
cnf(c_1204,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_789,c_345]) ).
cnf(c_790,plain,
( ~ ssPv4(A)
| ~ ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1204]) ).
cnf(c_1205,plain,
( ssPv3(A)
| ~ ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_790,c_777]) ).
cnf(c_806,plain,
( ~ ssPv3(skf1(A))
| ssPv3(A)
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1205]) ).
cnf(c_1206,plain,
( ssPv3(A)
| ssPv3(A)
| ssPv3(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_806,c_720]) ).
cnf(c_807,plain,
( ssPv3(A)
| ssPv3(skf1(skf1(A))) ),
inference(copy,[status(thm)],[c_1206]) ).
cnf(c_811,plain,
( ssPv1(skf1(A))
| ssPv4(skf1(skf1(A)))
| ~ ssPv3(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_807,c_341]) ).
cnf(c_1207,plain,
( ssPv3(A)
| ssPv1(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_811,c_720]) ).
cnf(c_814,plain,
( ssPv1(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1207]) ).
cnf(c_1208,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ~ ssPv2(A)
| ssPv4(skf1(skf1(A)))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_814,c_337]) ).
cnf(c_819,plain,
( ssPv2(skf1(A))
| ~ ssPv2(A)
| ssPv4(skf1(skf1(A)))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1208]) ).
cnf(c_1209,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_819,c_760]) ).
cnf(c_821,plain,
( ssPv2(skf1(A))
| ssPv4(skf1(skf1(A)))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1209]) ).
cnf(c_1210,plain,
( ssPv4(skf1(A))
| ssPv2(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_821,c_340]) ).
cnf(c_838,plain,
( ssPv4(skf1(A))
| ~ ssPv3(skf1(skf1(A)))
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1210]) ).
cnf(c_1211,plain,
( ssPv3(A)
| ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_838,c_807]) ).
cnf(c_839,plain,
( ssPv4(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1211]) ).
cnf(c_1212,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_839,c_345]) ).
cnf(c_840,plain,
( ~ ssPv4(A)
| ~ ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1212]) ).
cnf(c_1213,plain,
( ssPv3(A)
| ~ ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_840,c_777]) ).
cnf(c_851,plain,
( ~ ssPv3(skf1(A))
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1213]) ).
cnf(c_1214,plain,
( ssPv3(A)
| ssPv2(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_851,c_720]) ).
cnf(c_852,plain,
( ssPv2(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1214]) ).
cnf(c_1215,plain,
( ~ ssPv3(skf1(A))
| ssPv4(skf1(A))
| ssPv3(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_852,c_780]) ).
cnf(c_853,plain,
( ~ ssPv3(skf1(A))
| ssPv4(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1215]) ).
cnf(c_1216,plain,
( ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_852,c_778]) ).
cnf(c_854,plain,
( ssPv1(skf1(A))
| ~ ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1216]) ).
cnf(c_1217,plain,
( ssPv3(A)
| ssPv1(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_854,c_760]) ).
cnf(c_855,plain,
( ssPv1(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1217]) ).
cnf(c_1218,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ~ ssPv4(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_855,c_346]) ).
cnf(c_856,plain,
( ~ ssPv4(A)
| ~ ssPv4(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1218]) ).
cnf(c_1219,plain,
( ssPv3(A)
| ssPv4(skf1(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_853,c_720]) ).
cnf(c_861,plain,
( ssPv4(skf1(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1219]) ).
cnf(c_1220,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_861,c_856]) ).
cnf(c_862,plain,
( ~ ssPv4(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_1220]) ).
cnf(c_1221,plain,
( ssPv3(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_862,c_777]) ).
cnf(c_866,plain,
ssPv3(A),
inference(copy,[status(thm)],[c_1221]) ).
cnf(c_867,plain,
( ~ ssPv1(skf1(A))
| ~ ssPv2(skf1(A))
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_397]) ).
cnf(c_1222,plain,
( ssPv4(skf1(A))
| ~ ssPv3(A)
| ~ ssPv1(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_396]) ).
cnf(c_868,plain,
( ssPv4(skf1(A))
| ~ ssPv1(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_1222]) ).
cnf(c_869,plain,
( ssPv4(skf1(A))
| ~ ssPv1(A)
| ~ ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_394]) ).
cnf(c_870,plain,
( ssPv4(A)
| ssPv2(skf1(A))
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_393]) ).
cnf(c_1223,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_348]) ).
cnf(c_885,plain,
( ssPv1(A)
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_1223]) ).
cnf(c_1224,plain,
( ssPv1(A)
| ssPv4(skf1(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_866,c_341]) ).
cnf(c_887,plain,
( ssPv1(A)
| ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_1224]) ).
cnf(c_888,plain,
( ssPv4(A)
| ssPv2(A)
| ~ ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_340]) ).
cnf(c_889,plain,
( ssPv2(A)
| ssPv2(skf1(A))
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_866,c_339]) ).
cnf(c_890,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_332]) ).
cnf(c_914,plain,
( ~ ssPv4(A)
| ~ ssPv2(A)
| ~ ssPv1(skf1(A)) ),
inference(resolve,[status(thm)],[c_866,c_159]) ).
cnf(c_1225,plain,
( ssPv4(skf1(A))
| ~ ssPv2(skf1(A))
| ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_887,c_869]) ).
cnf(c_922,plain,
( ~ ssPv2(skf1(A))
| ssPv4(skf1(A)) ),
inference(copy,[status(thm)],[c_1225]) ).
cnf(c_1226,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv4(skf1(A))
| ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_887,c_329]) ).
cnf(c_926,plain,
( ssPv4(A)
| ssPv1(skf1(A))
| ssPv4(skf1(A)) ),
inference(copy,[status(thm)],[c_1226]) ).
cnf(c_1227,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv4(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_890,c_888]) ).
cnf(c_1228,plain,
( ssPv4(A)
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_1227]) ).
cnf(c_928,plain,
( ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_1228]) ).
cnf(c_929,plain,
( ssPv1(A)
| ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_928,c_885]) ).
cnf(c_1229,plain,
( ssPv4(A)
| ssPv2(skf1(A))
| ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_928,c_870]) ).
cnf(c_930,plain,
( ssPv4(A)
| ssPv2(skf1(A)) ),
inference(copy,[status(thm)],[c_1229]) ).
cnf(c_1230,plain,
( ssPv2(A)
| ssPv2(skf1(A))
| ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_929,c_889]) ).
cnf(c_932,plain,
( ssPv2(A)
| ssPv2(skf1(A)) ),
inference(copy,[status(thm)],[c_1230]) ).
cnf(c_936,plain,
( ssPv4(skf1(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_932,c_922]) ).
cnf(c_937,plain,
( ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_936,c_885]) ).
cnf(c_939,plain,
( ~ ssPv4(A)
| ~ ssPv2(A)
| ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_937,c_914]) ).
cnf(c_1231,plain,
( ssPv2(skf1(A))
| ~ ssPv2(A)
| ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_939,c_930]) ).
cnf(c_941,plain,
( ~ ssPv2(A)
| ssPv2(skf1(A)) ),
inference(copy,[status(thm)],[c_1231]) ).
cnf(c_942,plain,
( ssPv2(A)
| ssPv2(skf1(skf1(A))) ),
inference(resolve,[status(thm)],[c_941,c_932]) ).
cnf(c_1232,plain,
( ssPv4(skf1(A))
| ssPv4(A)
| ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_926,c_868]) ).
cnf(c_943,plain,
( ssPv4(A)
| ssPv4(skf1(A)) ),
inference(copy,[status(thm)],[c_1232]) ).
cnf(c_944,plain,
( ssPv1(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_943,c_885]) ).
cnf(c_1233,plain,
( ssPv4(skf1(A))
| ssPv4(skf1(A)) ),
inference(resolve,[status(thm)],[c_944,c_868]) ).
cnf(c_951,plain,
ssPv4(skf1(A)),
inference(copy,[status(thm)],[c_1233]) ).
cnf(c_954,plain,
ssPv1(A),
inference(resolve,[status(thm)],[c_951,c_885]) ).
cnf(c_1234,plain,
( ~ ssPv1(skf1(A))
| ~ ssPv2(skf1(A)) ),
inference(resolve,[status(thm)],[c_951,c_867]) ).
cnf(c_958,plain,
~ ssPv2(skf1(A)),
inference(resolve,[status(thm)],[c_954,c_1234]) ).
cnf(c_965,plain,
ssPv2(A),
inference(resolve,[status(thm)],[c_958,c_942]) ).
cnf(c_966,plain,
$false,
inference(resolve,[status(thm)],[c_965,c_958]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN755-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 18:19:19 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 1368243 was started by sandbox2 on n017,
% 0.08/0.37 % Sat Sep 26 18:19:19 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.37
% 0.08/0.37 % From the command line: assign(max_seconds, 300).
% 1.56/0.61
% 1.56/0.61 % given #500 (A,wt=97): 486 ssPv3(skf1(skf1(skf1(skf1(A))))) | ssPv2(skf1(skf1(skf1(A)))) | ssPv4(skf1(skf1(skf1(skf1(skf1(A)))))) | ssPv2(skf1(skf1(skf1(skf1(A))))) | ssPv2(skf1(skf1(A))) | ssPv3(skf1(skf1(A))) | ssPv2(skf1(A)) | -ssPv2(A) | ssPv3(A). [resolve(444,g,337,a),merge(i)].
% 1.56/0.61
% 1.56/0.61 % SZS status Unsatisfiable for theBenchmark
% 1.56/0.61
% 1.56/0.61 % Proof 1 at 0.18 (+ 0.04) seconds.
% 1.56/0.61 % Length of proof is 255.
% 1.56/0.61 % Level of proof is 101.
% 1.56/0.61 % Maximum clause weight is 60.000.
% 1.56/0.61 % Given clauses 721.
% 1.56/0.61
% 1.56/0.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------