%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN784-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 : n018.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:38 AM UTC 2026
% Result : Unsatisfiable 6.10s 1.31s
% Output : CNFRefutation 6.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 165
% Number of leaves : 37
% Syntax : Number of formulae : 623 ( 9 unt; 0 def)
% Number of atoms : 2822 ( 0 equ)
% Maximal formula atoms : 7 ( 4 avg)
% Number of connectives : 3040 ( 841 ~;2199 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 0 con; 1-1 aty)
% Number of variables : 843 ( 4 sgn 116 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clause1,axiom,
! [VAR_0] : ssRr(skf3(VAR_0),VAR_0),
file('theBenchmark.p',clause1) ).
cnf(c_1,plain,
ssRr(skf3(A),A),
inference(clausify,[status(thm)],[clause1]) ).
fof(clause2,axiom,
! [VAR_0] : ssRr(VAR_0,skf2(VAR_0)),
file('theBenchmark.p',clause2) ).
cnf(c_2,plain,
ssRr(A,skf2(A)),
inference(clausify,[status(thm)],[clause2]) ).
fof(clause3,axiom,
! [VAR_0,VAR_1] :
( ssPv4(VAR_1)
| ssPv3(VAR_1)
| ssPv2(VAR_1)
| ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause3) ).
cnf(c_3,plain,
( ssPv4(B)
| ssPv3(B)
| ssPv2(B)
| ssPv4(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause3]) ).
fof(clause4,axiom,
! [VAR_0,VAR_1] :
( ssPv3(VAR_1)
| ssPv2(VAR_1)
| ssPv2(VAR_0)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause4) ).
cnf(c_4,plain,
( ssPv3(B)
| ssPv2(B)
| ssPv2(A)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause4]) ).
fof(clause6,axiom,
! [VAR_0,VAR_1] :
( ssPv1(VAR_0)
| ssPv1(VAR_1)
| ~ ssPv4(VAR_0)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause6) ).
cnf(c_6,plain,
( ssPv1(A)
| ssPv1(B)
| ~ ssPv4(A)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause6]) ).
fof(clause7,axiom,
! [VAR_0,VAR_1] :
( ssPv1(VAR_1)
| ssPv1(VAR_0)
| ~ ssPv3(VAR_1)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause7) ).
cnf(c_7,plain,
( ssPv1(B)
| ssPv1(A)
| ~ ssPv3(B)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause7]) ).
fof(clause8,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_0)
| ssPv3(VAR_0)
| ssPv3(VAR_2)
| ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause8) ).
cnf(c_8,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(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_1)
| ssPv4(VAR_2)
| ssPv2(VAR_0)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause9) ).
cnf(c_9,plain,
( ssPv4(B)
| ssPv4(C)
| ssPv2(A)
| ~ ssPv3(B)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause9]) ).
fof(clause10,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_1)
| ssPv2(VAR_2)
| ssPv3(VAR_0)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause10) ).
cnf(c_10,plain,
( ssPv3(B)
| ssPv2(C)
| ssPv3(A)
| ~ ssPv2(B)
| ~ ssRr(C,B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause10]) ).
fof(clause11,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_1)
| ssPv2(VAR_2)
| ssPv1(VAR_0)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause11) ).
cnf(c_11,plain,
( ssPv1(B)
| ssPv2(C)
| ssPv1(A)
| ~ ssPv4(B)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause11]) ).
fof(clause12,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_2)
| ssPv4(VAR_0)
| ~ ssPv4(VAR_1)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause12) ).
cnf(c_12,plain,
( ssPv2(C)
| ssPv4(A)
| ~ ssPv4(B)
| ~ ssPv1(B)
| ~ ssRr(C,B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause12]) ).
fof(clause14,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_0)
| ssPv4(VAR_2)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause14) ).
cnf(c_14,plain,
( ssPv4(A)
| ssPv4(C)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause14]) ).
fof(clause15,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_1)
| ssPv4(VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause15) ).
cnf(c_15,plain,
( ssPv3(B)
| ssPv4(C)
| ~ ssPv4(B)
| ~ ssRr(C,B)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause15]) ).
fof(clause16,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_0)
| ssPv1(VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause16) ).
cnf(c_16,plain,
( ssPv3(A)
| ssPv1(C)
| ~ ssPv2(A)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause16]) ).
fof(clause17,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_0)
| ssPv4(VAR_2)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause17) ).
cnf(c_17,plain,
( ssPv3(A)
| ssPv4(C)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause17]) ).
fof(clause18,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_1)
| ssPv3(VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause18) ).
cnf(c_18,plain,
( ssPv2(B)
| ssPv3(C)
| ~ ssPv4(B)
| ~ ssRr(C,B)
| ~ ssPv1(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause18]) ).
fof(clause19,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_1)
| ssPv2(VAR_1)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause19) ).
cnf(c_19,plain,
( ssPv4(B)
| ssPv2(B)
| ~ ssPv3(C)
| ~ ssRr(B,C)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause19]) ).
fof(clause20,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_0)
| ~ ssPv4(VAR_1)
| ~ ssPv3(VAR_1)
| ~ ssPv4(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause20) ).
cnf(c_20,plain,
( ssPv3(A)
| ~ ssPv4(B)
| ~ ssPv3(B)
| ~ ssPv4(C)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause20]) ).
fof(clause21,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_2)
| ~ ssPv4(VAR_0)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause21) ).
cnf(c_21,plain,
( ssPv4(C)
| ~ ssPv4(A)
| ~ ssPv2(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_2)
| ~ ssPv3(VAR_1)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause22) ).
cnf(c_22,plain,
( ssPv2(C)
| ~ ssPv3(B)
| ~ ssPv2(B)
| ~ ssRr(B,C)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause22]) ).
fof(clause23,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause23) ).
cnf(c_23,plain,
( ssPv1(C)
| ~ ssPv4(B)
| ~ ssPv1(B)
| ~ ssRr(B,C)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause23]) ).
fof(clause24,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_0)
| ~ ssPv3(VAR_0)
| ~ ssPv2(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause24) ).
cnf(c_24,plain,
( ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv2(C)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause24]) ).
fof(clause25,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_1)
| ~ ssPv3(VAR_1)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause25) ).
cnf(c_25,plain,
( ssPv1(B)
| ~ ssPv3(B)
| ~ ssPv3(C)
| ~ ssRr(B,C)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause25]) ).
fof(clause26,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_1)
| ~ ssPv3(VAR_1)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause26) ).
cnf(c_26,plain,
( ssPv1(B)
| ~ ssPv3(B)
| ~ ssPv3(C)
| ~ ssRr(B,C)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause26]) ).
fof(clause27,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv3(VAR_1)
| ssPv2(VAR_3)
| ssPv4(VAR_2)
| ssPv1(VAR_0)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause27) ).
cnf(c_27,plain,
( ssPv3(B)
| ssPv2(D)
| ssPv4(C)
| ssPv1(A)
| ~ ssRr(B,D)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause27]) ).
fof(clause28,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv4(VAR_1)
| ssPv3(VAR_2)
| ssPv4(VAR_0)
| ~ ssPv4(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause28) ).
cnf(c_28,plain,
( ssPv4(B)
| ssPv3(C)
| ssPv4(A)
| ~ ssPv4(D)
| ~ ssRr(B,D)
| ~ ssRr(C,B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause28]) ).
fof(clause29,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv4(VAR_1)
| ssPv2(VAR_3)
| ssPv4(VAR_2)
| ~ ssRr(VAR_3,VAR_1)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause29) ).
cnf(c_29,plain,
( ssPv4(B)
| ssPv2(D)
| ssPv4(C)
| ~ ssRr(D,B)
| ~ ssRr(C,B)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause29]) ).
fof(clause31,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv4(VAR_1)
| ssPv4(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv2(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause31) ).
cnf(c_31,plain,
( ssPv4(B)
| ssPv4(D)
| ~ ssRr(B,D)
| ~ ssPv2(C)
| ~ ssRr(B,C)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause31]) ).
fof(clause32,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv3(VAR_1)
| ssPv4(VAR_2)
| ~ ssPv3(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause32) ).
cnf(c_32,plain,
( ssPv3(B)
| ssPv4(C)
| ~ ssPv3(D)
| ~ ssRr(B,D)
| ~ ssRr(C,B)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause32]) ).
fof(clause34,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv3(VAR_3)
| ssPv4(VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause34) ).
cnf(c_34,plain,
( ssPv3(D)
| ssPv4(C)
| ~ ssPv4(B)
| ~ ssRr(B,D)
| ~ ssRr(B,C)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause34]) ).
fof(clause35,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv2(VAR_1)
| ssPv1(VAR_3)
| ~ ssRr(VAR_3,VAR_1)
| ~ ssPv2(VAR_2)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause35) ).
cnf(c_35,plain,
( ssPv2(B)
| ssPv1(D)
| ~ ssRr(D,B)
| ~ ssPv2(C)
| ~ ssRr(C,B)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause35]) ).
fof(clause36,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv2(VAR_1)
| ssPv4(VAR_0)
| ~ ssPv3(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv4(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause36) ).
cnf(c_36,plain,
( ssPv2(B)
| ssPv4(A)
| ~ ssPv3(D)
| ~ ssRr(B,D)
| ~ ssPv4(C)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause36]) ).
fof(clause37,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv2(VAR_1)
| ssPv3(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv4(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause37) ).
cnf(c_37,plain,
( ssPv2(B)
| ssPv3(D)
| ~ ssRr(B,D)
| ~ ssPv4(C)
| ~ ssRr(B,C)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause37]) ).
fof(clause38,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv2(VAR_3)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause38) ).
cnf(c_38,plain,
( ssPv2(D)
| ~ ssPv1(B)
| ~ ssRr(B,D)
| ~ ssPv3(C)
| ~ ssRr(B,C)
| ~ ssPv1(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause38]) ).
fof(clause39,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv4(VAR_0)
| ~ ssPv1(VAR_1)
| ~ ssPv2(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv4(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause39) ).
cnf(c_39,plain,
( ssPv4(A)
| ~ ssPv1(B)
| ~ ssPv2(D)
| ~ ssRr(B,D)
| ~ ssPv4(C)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause39]) ).
fof(clause40,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ ssPv3(VAR_1)
| ~ ssPv1(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv1(VAR_2)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause40) ).
cnf(c_40,plain,
( ~ ssPv3(B)
| ~ ssPv1(D)
| ~ ssRr(B,D)
| ~ ssPv1(C)
| ~ ssRr(C,B)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause40]) ).
fof(clause41,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ ssPv1(VAR_1)
| ~ ssPv1(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv2(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause41) ).
cnf(c_41,plain,
( ~ ssPv1(B)
| ~ ssPv1(D)
| ~ ssRr(B,D)
| ~ ssPv2(C)
| ~ ssRr(B,C)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause41]) ).
cnf(c_48,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(B)
| ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_8]) ).
cnf(c_53,plain,
( ssPv3(B)
| ssPv2(A)
| ssPv3(A)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_10]) ).
cnf(c_57,plain,
( ssPv2(A)
| ssPv4(A)
| ~ ssPv4(B)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_12]) ).
cnf(c_59,plain,
( ssPv4(A)
| ssPv4(B)
| ~ ssPv1(A)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_14]) ).
cnf(c_61,plain,
( ssPv3(B)
| ssPv4(A)
| ~ ssPv4(B)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_15]) ).
cnf(c_62,plain,
( ssPv3(A)
| ssPv1(B)
| ~ ssPv2(A)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_16]) ).
cnf(c_63,plain,
( ssPv3(A)
| ssPv4(B)
| ~ ssPv1(A)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_17]) ).
cnf(c_64,plain,
( ssPv2(B)
| ssPv3(A)
| ~ ssPv4(B)
| ~ ssPv1(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_18]) ).
cnf(c_66,plain,
( ssPv4(B)
| ~ ssPv4(A)
| ~ ssPv2(A)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_21]) ).
cnf(c_70,plain,
( ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv2(B)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_24]) ).
cnf(c_89,plain,
( ssPv2(B)
| ssPv1(C)
| ~ ssRr(C,B)
| ~ ssPv2(A)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_35]) ).
cnf(c_119,plain,
( ssPv2(B)
| ssPv1(A)
| ~ ssPv2(A)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_89]) ).
cnf(c_128,plain,
( ssPv4(skf2(A))
| ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_3,c_2]) ).
cnf(c_129,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3,c_1]) ).
cnf(c_130,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv2(A)
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_4,c_2]) ).
cnf(c_131,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv2(skf3(A))
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_4,c_1]) ).
cnf(c_134,plain,
( ssPv1(A)
| ssPv1(skf2(A))
| ~ ssPv4(A)
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_6,c_2]) ).
cnf(c_135,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ~ ssPv4(skf3(A))
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_6,c_1]) ).
cnf(c_137,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ~ ssPv3(A)
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_7,c_1]) ).
cnf(c_143,plain,
( ssPv4(A)
| ssPv4(B)
| ssPv2(skf3(A))
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_9,c_1]) ).
cnf(c_155,plain,
( ssPv1(A)
| ssPv2(B)
| ssPv1(skf3(A))
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_11,c_1]) ).
cnf(c_177,plain,
( ssPv3(A)
| ssPv4(B)
| ~ ssPv4(A)
| ~ ssRr(B,A)
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_15,c_1]) ).
cnf(c_193,plain,
( ssPv4(A)
| ssPv2(A)
| ~ ssPv3(B)
| ~ ssRr(A,B)
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_19,c_1]) ).
cnf(c_197,plain,
( ssPv3(skf3(A))
| ~ ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_20,c_1]) ).
cnf(c_209,plain,
( ssPv2(B)
| ~ ssPv3(A)
| ~ ssPv2(A)
| ~ ssRr(A,B)
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_22,c_1]) ).
cnf(c_215,plain,
( ssPv1(B)
| ~ ssPv4(A)
| ~ ssPv1(A)
| ~ ssRr(A,B)
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_23,c_1]) ).
cnf(c_222,plain,
( ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv2(skf2(A))
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_24,c_2]) ).
cnf(c_227,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv3(B)
| ~ ssRr(A,B)
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_25,c_1]) ).
cnf(c_228,plain,
( ssPv1(B)
| ~ ssPv3(B)
| ~ ssPv3(skf2(B))
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_25,c_2]) ).
cnf(c_233,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv3(B)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_26,c_1]) ).
cnf(c_239,plain,
( ssPv3(A)
| ssPv2(C)
| ssPv4(B)
| ssPv1(skf3(A))
| ~ ssRr(A,C)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_27,c_1]) ).
cnf(c_245,plain,
( ssPv3(A)
| ssPv2(B)
| ssPv4(B)
| ssPv1(skf3(A))
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_239]) ).
cnf(c_252,plain,
( ssPv4(B)
| ssPv3(C)
| ssPv4(A)
| ~ ssPv4(skf2(B))
| ~ ssRr(C,B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_28,c_2]) ).
cnf(c_256,plain,
( ssPv4(B)
| ssPv3(A)
| ssPv4(A)
| ~ ssPv4(skf2(B))
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_252]) ).
cnf(c_261,plain,
( ssPv4(A)
| ssPv2(C)
| ssPv4(B)
| ~ ssRr(C,A)
| ~ ssRr(B,A)
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_29,c_1]) ).
cnf(c_268,plain,
( ssPv4(A)
| ssPv2(B)
| ssPv4(B)
| ~ ssRr(B,A)
| ~ ssPv2(skf3(A)) ),
inference(factor,[status(thm)],[c_261]) ).
cnf(c_289,plain,
( ssPv4(A)
| ssPv4(C)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B)
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_31,c_1]) ).
cnf(c_296,plain,
( ssPv4(A)
| ssPv4(B)
| ~ ssPv2(B)
| ~ ssRr(A,B)
| ~ ssPv3(skf3(A)) ),
inference(factor,[status(thm)],[c_289]) ).
cnf(c_306,plain,
( ssPv3(B)
| ssPv4(C)
| ~ ssPv3(skf2(B))
| ~ ssRr(C,B)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_32,c_2]) ).
cnf(c_312,plain,
( ssPv3(B)
| ssPv4(A)
| ~ ssPv3(skf2(B))
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_306]) ).
cnf(c_325,plain,
( ssPv3(C)
| ssPv4(B)
| ~ ssPv4(A)
| ~ ssRr(A,C)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_34,c_1]) ).
cnf(c_331,plain,
( ssPv3(B)
| ssPv4(B)
| ~ ssPv4(A)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(factor,[status(thm)],[c_325]) ).
cnf(c_345,plain,
( ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv3(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_36,c_1]) ).
cnf(c_351,plain,
( ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv3(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_345]) ).
cnf(c_353,plain,
( ssPv2(A)
| ssPv3(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_37,c_1]) ).
cnf(c_359,plain,
( ssPv2(A)
| ssPv3(B)
| ~ ssPv4(B)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(factor,[status(thm)],[c_353]) ).
cnf(c_361,plain,
( ssPv2(C)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssRr(A,B)
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_38,c_1]) ).
cnf(c_367,plain,
( ssPv2(B)
| ~ ssPv1(A)
| ~ ssPv3(B)
| ~ ssRr(A,B)
| ~ ssPv1(skf3(A)) ),
inference(factor,[status(thm)],[c_361]) ).
cnf(c_375,plain,
( ssPv4(skf3(A))
| ~ ssPv1(A)
| ~ ssPv2(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_39,c_1]) ).
cnf(c_381,plain,
( ssPv4(skf3(A))
| ~ ssPv1(A)
| ~ ssPv2(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_375]) ).
cnf(c_386,plain,
( ~ ssPv3(B)
| ~ ssPv1(skf2(B))
| ~ ssPv1(C)
| ~ ssRr(C,B)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_40,c_2]) ).
cnf(c_394,plain,
( ~ ssPv3(B)
| ~ ssPv1(skf2(B))
| ~ ssPv1(A)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_386]) ).
cnf(c_406,plain,
( ~ ssPv1(skf2(A))
| ~ ssPv1(C)
| ~ ssRr(skf2(A),C)
| ~ ssPv2(B)
| ~ ssRr(skf2(A),B)
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_41,c_2]) ).
cnf(c_407,plain,
( ~ ssPv1(A)
| ~ ssPv1(C)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_41,c_1]) ).
cnf(c_413,plain,
( ~ ssPv1(skf2(A))
| ~ ssPv1(B)
| ~ ssPv2(B)
| ~ ssRr(skf2(A),B)
| ~ ssPv2(A) ),
inference(factor,[status(thm)],[c_406]) ).
cnf(c_416,plain,
( ~ ssPv1(A)
| ~ ssPv1(B)
| ~ ssPv2(B)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(factor,[status(thm)],[c_407]) ).
cnf(c_438,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_48,c_2]) ).
cnf(c_439,plain,
( ssPv4(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_48,c_1]) ).
cnf(c_440,plain,
( ssPv3(skf2(A))
| ssPv2(A)
| ssPv3(A)
| ~ ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_53,c_2]) ).
cnf(c_441,plain,
( ssPv3(A)
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_53,c_1]) ).
cnf(c_443,plain,
( ssPv2(skf3(A))
| ssPv4(skf3(A))
| ~ ssPv4(A)
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_57,c_1]) ).
cnf(c_444,plain,
( ssPv4(A)
| ssPv4(skf2(A))
| ~ ssPv1(A)
| ~ ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_59,c_2]) ).
cnf(c_446,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv4(skf2(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_61,c_2]) ).
cnf(c_447,plain,
( ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv4(A)
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_61,c_1]) ).
cnf(c_448,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ~ ssPv2(A)
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_62,c_2]) ).
cnf(c_449,plain,
( ssPv3(skf3(A))
| ssPv1(A)
| ~ ssPv2(skf3(A))
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_62,c_1]) ).
cnf(c_450,plain,
( ssPv3(A)
| ssPv4(skf2(A))
| ~ ssPv1(A)
| ~ ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_63,c_2]) ).
cnf(c_451,plain,
( ssPv3(skf3(A))
| ssPv4(A)
| ~ ssPv1(skf3(A))
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_63,c_1]) ).
cnf(c_452,plain,
( ssPv2(skf2(A))
| ssPv3(A)
| ~ ssPv4(skf2(A))
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_64,c_2]) ).
cnf(c_453,plain,
( ssPv2(A)
| ssPv3(skf3(A))
| ~ ssPv4(A)
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_64,c_1]) ).
cnf(c_454,plain,
( ssPv4(skf2(A))
| ~ ssPv4(A)
| ~ ssPv2(A)
| ~ ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_66,c_2]) ).
cnf(c_455,plain,
( ssPv4(A)
| ~ ssPv4(skf3(A))
| ~ ssPv2(skf3(A))
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_66,c_1]) ).
cnf(c_456,plain,
( ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv2(skf2(A))
| ~ ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_70,c_2]) ).
cnf(c_457,plain,
( ssPv4(skf3(A))
| ~ ssPv3(skf3(A))
| ~ ssPv2(A)
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_70,c_1]) ).
cnf(c_504,plain,
( ssPv2(skf2(A))
| ssPv1(A)
| ~ ssPv2(A)
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_119,c_2]) ).
cnf(c_505,plain,
( ssPv2(A)
| ssPv1(skf3(A))
| ~ ssPv2(skf3(A))
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_119,c_1]) ).
cnf(c_9216,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_130,c_128]) ).
cnf(c_9217,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9216]) ).
cnf(c_507,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9217]) ).
cnf(c_514,plain,
( ~ ssPv3(A)
| ~ ssPv1(skf2(A))
| ~ ssPv1(skf3(A))
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_394,c_1]) ).
cnf(c_517,plain,
( ~ ssPv1(A)
| ~ ssPv1(skf2(A))
| ~ ssPv2(skf2(A))
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_416,c_2]) ).
cnf(c_520,plain,
( ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(skf3(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_143,c_2]) ).
cnf(c_550,plain,
( ~ ssPv1(skf2(A))
| ~ ssPv1(skf2(skf2(A)))
| ~ ssPv2(skf2(skf2(A)))
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_413,c_2]) ).
cnf(c_9218,plain,
( ssPv3(skf2(A))
| ssPv2(A)
| ssPv3(A)
| ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_507,c_440]) ).
cnf(c_9219,plain,
( ssPv3(skf2(A))
| ssPv3(A)
| ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9218]) ).
cnf(c_567,plain,
( ssPv3(A)
| ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9219]) ).
cnf(c_571,plain,
( ssPv1(A)
| ssPv2(skf2(A))
| ssPv1(skf3(A))
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_155,c_2]) ).
cnf(c_9220,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_567,c_446]) ).
cnf(c_9221,plain,
( ssPv3(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9220]) ).
cnf(c_586,plain,
( ~ ssPv4(skf2(A))
| ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9221]) ).
cnf(c_9222,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A))
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_520,c_438]) ).
cnf(c_9223,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_9222]) ).
cnf(c_607,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_9223]) ).
cnf(c_9224,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(A)
| ssPv3(skf2(A))
| ssPv4(A)
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_607,c_586]) ).
cnf(c_9225,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv3(skf2(A))
| ssPv4(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_9224]) ).
cnf(c_668,plain,
( ssPv2(A)
| ssPv3(skf2(A))
| ssPv4(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_9225]) ).
cnf(c_702,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv4(skf2(A))
| ~ ssPv3(skf3(skf2(A))) ),
inference(resolve,[status(thm)],[c_177,c_2]) ).
cnf(c_717,plain,
( ssPv4(A)
| ssPv2(A)
| ~ ssPv3(skf2(A))
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_193,c_2]) ).
cnf(c_9226,plain,
( ssPv2(A)
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv4(A)
| ssPv2(A)
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_717,c_668]) ).
cnf(c_9227,plain,
( ssPv2(A)
| ssPv2(skf3(A))
| ssPv4(A)
| ssPv2(A)
| ~ ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9226]) ).
cnf(c_719,plain,
( ssPv2(skf3(A))
| ssPv4(A)
| ssPv2(A)
| ~ ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9227]) ).
cnf(c_9228,plain,
( ssPv3(A)
| ssPv4(A)
| ssPv2(A)
| ssPv4(A)
| ssPv2(A)
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_717,c_567]) ).
cnf(c_9229,plain,
( ssPv3(A)
| ssPv4(A)
| ssPv4(A)
| ssPv2(A)
| ~ ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9228]) ).
cnf(c_724,plain,
( ssPv3(A)
| ssPv4(A)
| ssPv2(A)
| ~ ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9229]) ).
cnf(c_9230,plain,
( ssPv4(A)
| ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(A)
| ssPv2(A)
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_717,c_507]) ).
cnf(c_9231,plain,
( ssPv4(A)
| ssPv2(skf2(A))
| ssPv4(A)
| ssPv2(A)
| ~ ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9230]) ).
cnf(c_726,plain,
( ssPv2(skf2(A))
| ssPv4(A)
| ssPv2(A)
| ~ ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9231]) ).
cnf(c_9232,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv2(A)
| ssPv3(A)
| ssPv4(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_724,c_129]) ).
cnf(c_9233,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(A)
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9232]) ).
cnf(c_9234,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9233]) ).
cnf(c_734,plain,
( ssPv3(A)
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9234]) ).
cnf(c_9235,plain,
( ssPv4(skf2(A))
| ~ ssPv4(A)
| ~ ssPv2(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_734,c_454]) ).
cnf(c_738,plain,
( ~ ssPv4(A)
| ~ ssPv2(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9235]) ).
cnf(c_9236,plain,
( ssPv3(skf3(A))
| ssPv1(A)
| ~ ssPv4(A)
| ssPv3(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_734,c_449]) ).
cnf(c_739,plain,
( ssPv1(A)
| ~ ssPv4(A)
| ssPv3(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9236]) ).
cnf(c_9237,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv3(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_734,c_448]) ).
cnf(c_740,plain,
( ssPv1(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv3(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9237]) ).
cnf(c_9238,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv2(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_734,c_131]) ).
cnf(c_9239,plain,
( ssPv3(A)
| ssPv2(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9238]) ).
cnf(c_744,plain,
( ssPv2(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9239]) ).
cnf(c_9240,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv2(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_734,c_130]) ).
cnf(c_9241,plain,
( ssPv3(skf2(A))
| ssPv2(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_9240]) ).
cnf(c_745,plain,
( ssPv2(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_9241]) ).
cnf(c_9242,plain,
( ssPv3(A)
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_744,c_441]) ).
cnf(c_9243,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9242]) ).
cnf(c_752,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9243]) ).
cnf(c_9244,plain,
( ssPv2(A)
| ssPv1(skf3(A))
| ~ ssPv4(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_744,c_505]) ).
cnf(c_756,plain,
( ssPv1(skf3(A))
| ~ ssPv4(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9244]) ).
cnf(c_9245,plain,
( ssPv3(skf2(A))
| ssPv2(A)
| ssPv3(A)
| ssPv2(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_745,c_440]) ).
cnf(c_9246,plain,
( ssPv3(skf2(A))
| ssPv3(A)
| ssPv2(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9245]) ).
cnf(c_763,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9246]) ).
cnf(c_9247,plain,
( ssPv2(skf2(A))
| ssPv1(A)
| ~ ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_745,c_504]) ).
cnf(c_766,plain,
( ssPv1(A)
| ~ ssPv4(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_9247]) ).
cnf(c_9248,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv3(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_763,c_448]) ).
cnf(c_780,plain,
( ssPv1(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv3(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9248]) ).
cnf(c_789,plain,
( ssPv4(A)
| ~ ssPv4(skf3(A))
| ~ ssPv2(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_752,c_455]) ).
cnf(c_9249,plain,
( ssPv3(skf3(A))
| ssPv1(A)
| ~ ssPv4(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_752,c_449]) ).
cnf(c_790,plain,
( ssPv1(A)
| ~ ssPv4(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9249]) ).
cnf(c_9250,plain,
( ssPv4(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv1(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_790,c_439]) ).
cnf(c_9251,plain,
( ssPv4(skf3(A))
| ssPv3(skf3(A))
| ssPv1(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9250]) ).
cnf(c_797,plain,
( ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9251]) ).
cnf(c_9252,plain,
( ssPv3(A)
| ssPv3(skf2(A))
| ~ ssPv4(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_738,c_763]) ).
cnf(c_823,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9252]) ).
cnf(c_9253,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv3(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_740,c_438]) ).
cnf(c_9254,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv3(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9253]) ).
cnf(c_832,plain,
( ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv3(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9254]) ).
cnf(c_884,plain,
( ssPv3(skf3(A))
| ~ ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_197,c_2]) ).
cnf(c_9255,plain,
( ssPv3(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A))
| ssPv3(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_823,c_438]) ).
cnf(c_9256,plain,
( ssPv3(A)
| ssPv3(skf2(A))
| ssPv3(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9255]) ).
cnf(c_9257,plain,
( ssPv3(A)
| ssPv3(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9256]) ).
cnf(c_919,plain,
( ssPv3(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9257]) ).
cnf(c_9258,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_832,c_446]) ).
cnf(c_9259,plain,
( ssPv3(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9258]) ).
cnf(c_939,plain,
( ~ ssPv4(skf2(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9259]) ).
cnf(c_9260,plain,
( ssPv3(A)
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_780,c_919]) ).
cnf(c_9261,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9260]) ).
cnf(c_961,plain,
( ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9261]) ).
cnf(c_9262,plain,
( ssPv1(A)
| ssPv1(skf2(A))
| ~ ssPv4(A)
| ssPv1(skf2(A))
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_961,c_134]) ).
cnf(c_967,plain,
( ssPv1(A)
| ~ ssPv4(A)
| ssPv1(skf2(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9262]) ).
cnf(c_9263,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_939,c_607]) ).
cnf(c_9264,plain,
( ssPv3(skf2(A))
| ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9263]) ).
cnf(c_994,plain,
( ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9264]) ).
cnf(c_9265,plain,
( ssPv1(A)
| ssPv1(skf2(A))
| ssPv3(skf2(A))
| ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_994,c_967]) ).
cnf(c_9266,plain,
( ssPv1(A)
| ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A)) ),
inference(copy,[status(thm)],[c_9265]) ).
cnf(c_1021,plain,
( ssPv1(A)
| ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A)) ),
inference(copy,[status(thm)],[c_9266]) ).
cnf(c_1068,plain,
( ssPv2(skf2(A))
| ~ ssPv3(A)
| ~ ssPv2(A)
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_209,c_2]) ).
cnf(c_9267,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv2(skf2(A))
| ~ ssPv3(A)
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_1068,c_745]) ).
cnf(c_1080,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ~ ssPv3(A)
| ~ ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_9267]) ).
cnf(c_1095,plain,
( ssPv1(skf2(A))
| ~ ssPv4(A)
| ~ ssPv1(A)
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_215,c_2]) ).
cnf(c_1096,plain,
( ssPv1(A)
| ~ ssPv4(skf3(A))
| ~ ssPv1(skf3(A))
| ~ ssPv4(skf3(skf3(A))) ),
inference(resolve,[status(thm)],[c_215,c_1]) ).
cnf(c_9268,plain,
( ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv1(skf2(A))
| ~ ssPv4(A)
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1095,c_1021]) ).
cnf(c_1097,plain,
( ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ~ ssPv4(A)
| ~ ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9268]) ).
cnf(c_1108,plain,
( ssPv4(skf3(A))
| ~ ssPv3(skf3(A))
| ~ ssPv2(skf2(skf3(A)))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_222,c_1]) ).
cnf(c_1110,plain,
( ssPv1(skf3(A))
| ~ ssPv3(skf3(A))
| ~ ssPv3(A)
| ~ ssPv4(skf3(skf3(A))) ),
inference(resolve,[status(thm)],[c_227,c_1]) ).
cnf(c_1122,plain,
( ssPv1(skf2(A))
| ~ ssPv3(skf2(A))
| ~ ssPv3(skf2(skf2(A)))
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_228,c_2]) ).
cnf(c_1123,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv3(skf2(A))
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_233,c_2]) ).
cnf(c_1139,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ssPv4(skf2(A))
| ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_245,c_2]) ).
cnf(c_1168,plain,
( ssPv4(A)
| ssPv3(skf3(A))
| ssPv4(skf3(A))
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_256,c_1]) ).
cnf(c_1185,plain,
( ssPv4(skf2(A))
| ssPv2(A)
| ssPv4(A)
| ~ ssPv2(skf3(skf2(A))) ),
inference(resolve,[status(thm)],[c_268,c_2]) ).
cnf(c_1189,plain,
( ssPv4(A)
| ssPv4(skf2(A))
| ~ ssPv2(skf2(A))
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_296,c_2]) ).
cnf(c_1226,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv3(skf2(skf2(A)))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_312,c_2]) ).
cnf(c_1227,plain,
( ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv3(skf2(A))
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_312,c_1]) ).
cnf(c_9269,plain,
( ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_1227,c_797]) ).
cnf(c_9270,plain,
( ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9269]) ).
cnf(c_1233,plain,
( ssPv1(A)
| ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9270]) ).
cnf(c_9271,plain,
( ssPv4(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_1227,c_439]) ).
cnf(c_9272,plain,
( ssPv4(skf3(A))
| ssPv4(A)
| ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9271]) ).
cnf(c_1240,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9272]) ).
cnf(c_9273,plain,
( ssPv1(skf2(A))
| ssPv3(A)
| ssPv1(A)
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1233,c_961]) ).
cnf(c_1246,plain,
( ssPv1(skf2(A))
| ssPv1(A)
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9273]) ).
cnf(c_9274,plain,
( ssPv3(A)
| ssPv4(skf2(A))
| ssPv1(A)
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1233,c_919]) ).
cnf(c_1248,plain,
( ssPv4(skf2(A))
| ssPv1(A)
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9274]) ).
cnf(c_9275,plain,
( ssPv3(A)
| ssPv4(skf2(A))
| ssPv4(A)
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1240,c_919]) ).
cnf(c_1258,plain,
( ssPv4(skf2(A))
| ssPv4(A)
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9275]) ).
cnf(c_9276,plain,
( ssPv1(A)
| ssPv1(skf2(A))
| ~ ssPv4(A)
| ssPv1(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1246,c_134]) ).
cnf(c_9277,plain,
( ssPv1(A)
| ~ ssPv4(A)
| ssPv1(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9276]) ).
cnf(c_1296,plain,
( ~ ssPv4(A)
| ssPv1(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9277]) ).
cnf(c_9278,plain,
( ssPv3(A)
| ssPv4(skf2(A))
| ~ ssPv2(skf2(A))
| ssPv4(skf2(A))
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1248,c_450]) ).
cnf(c_9279,plain,
( ssPv3(A)
| ~ ssPv2(skf2(A))
| ssPv4(skf2(A))
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9278]) ).
cnf(c_1339,plain,
( ~ ssPv2(skf2(A))
| ssPv4(skf2(A))
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9279]) ).
cnf(c_9280,plain,
( ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf2(A))
| ssPv4(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1258,c_520]) ).
cnf(c_9281,plain,
( ssPv4(A)
| ssPv2(skf3(A))
| ssPv4(skf2(A))
| ssPv4(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9280]) ).
cnf(c_1372,plain,
( ssPv2(skf3(A))
| ssPv4(skf2(A))
| ssPv4(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9281]) ).
cnf(c_9282,plain,
( ssPv3(A)
| ssPv4(skf2(A))
| ssPv1(skf3(A))
| ssPv4(skf2(A))
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1339,c_1139]) ).
cnf(c_9283,plain,
( ssPv3(A)
| ssPv1(skf3(A))
| ssPv4(skf2(A))
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9282]) ).
cnf(c_1399,plain,
( ssPv1(skf3(A))
| ssPv4(skf2(A))
| ssPv3(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9283]) ).
cnf(c_9284,plain,
( ssPv1(skf3(A))
| ssPv3(A)
| ssPv2(A)
| ssPv1(skf3(A))
| ssPv4(skf2(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1399,c_756]) ).
cnf(c_9285,plain,
( ssPv1(skf3(A))
| ssPv2(A)
| ssPv1(skf3(A))
| ssPv4(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9284]) ).
cnf(c_1461,plain,
( ssPv2(A)
| ssPv1(skf3(A))
| ssPv4(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9285]) ).
cnf(c_1503,plain,
( ssPv3(skf2(A))
| ssPv4(skf2(A))
| ~ ssPv4(A)
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_331,c_2]) ).
cnf(c_1524,plain,
( ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv3(skf2(A))
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_351,c_2]) ).
cnf(c_9286,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_1524,c_763]) ).
cnf(c_1543,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9286]) ).
cnf(c_9287,plain,
( ssPv2(A)
| ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_1524,c_745]) ).
cnf(c_1545,plain,
( ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9287]) ).
cnf(c_9288,plain,
( ssPv2(A)
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_1524,c_668]) ).
cnf(c_1546,plain,
( ssPv4(A)
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9288]) ).
cnf(c_9289,plain,
( ssPv2(A)
| ssPv1(skf3(A))
| ssPv3(A)
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1543,c_1461]) ).
cnf(c_9290,plain,
( ssPv2(A)
| ssPv1(skf3(A))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9289]) ).
cnf(c_1547,plain,
( ssPv1(skf3(A))
| ssPv3(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9290]) ).
cnf(c_9291,plain,
( ssPv1(skf3(A))
| ssPv3(A)
| ssPv2(A)
| ssPv1(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1547,c_756]) ).
cnf(c_9292,plain,
( ssPv1(skf3(A))
| ssPv3(A)
| ssPv1(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9291]) ).
cnf(c_9293,plain,
( ssPv1(skf3(A))
| ssPv1(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9292]) ).
cnf(c_1561,plain,
( ssPv1(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9293]) ).
cnf(c_9294,plain,
( ssPv2(A)
| ssPv3(skf3(A))
| ~ ssPv4(A)
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1561,c_453]) ).
cnf(c_1592,plain,
( ssPv3(skf3(A))
| ~ ssPv4(A)
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9294]) ).
cnf(c_9295,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1592,c_734]) ).
cnf(c_9296,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9295]) ).
cnf(c_1606,plain,
( ssPv3(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9296]) ).
cnf(c_9297,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1606,c_448]) ).
cnf(c_1617,plain,
( ssPv1(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9297]) ).
cnf(c_9298,plain,
( ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv4(A)
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1606,c_447]) ).
cnf(c_1627,plain,
( ssPv4(skf3(A))
| ~ ssPv4(A)
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9298]) ).
cnf(c_9299,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1627,c_734]) ).
cnf(c_9300,plain,
( ssPv3(A)
| ssPv4(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9299]) ).
cnf(c_1639,plain,
( ssPv4(skf3(A))
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9300]) ).
cnf(c_9301,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1639,c_448]) ).
cnf(c_1644,plain,
( ssPv1(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9301]) ).
cnf(c_1747,plain,
( ssPv2(A)
| ssPv3(skf2(A))
| ~ ssPv4(skf2(A))
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_359,c_2]) ).
cnf(c_1761,plain,
( ssPv2(skf2(A))
| ~ ssPv1(A)
| ~ ssPv3(skf2(A))
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_367,c_2]) ).
cnf(c_1762,plain,
( ssPv2(A)
| ~ ssPv1(skf3(A))
| ~ ssPv3(A)
| ~ ssPv1(skf3(skf3(A))) ),
inference(resolve,[status(thm)],[c_367,c_1]) ).
cnf(c_1772,plain,
( ssPv4(skf3(A))
| ~ ssPv1(A)
| ~ ssPv2(skf2(A))
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_381,c_2]) ).
cnf(c_9302,plain,
( ssPv3(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ~ ssPv4(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_789,c_1606]) ).
cnf(c_9303,plain,
( ssPv3(skf3(A))
| ssPv4(A)
| ~ ssPv4(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9302]) ).
cnf(c_1808,plain,
( ssPv4(A)
| ~ ssPv4(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9303]) ).
cnf(c_9304,plain,
( ssPv3(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv4(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1808,c_439]) ).
cnf(c_9305,plain,
( ssPv3(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9304]) ).
cnf(c_9306,plain,
( ssPv3(skf3(A))
| ssPv4(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9305]) ).
cnf(c_1816,plain,
( ssPv4(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9306]) ).
cnf(c_9307,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv4(A)
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_1816,c_446]) ).
cnf(c_1823,plain,
( ssPv3(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv4(A)
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_9307]) ).
cnf(c_9308,plain,
( ssPv1(A)
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1816,c_790]) ).
cnf(c_9309,plain,
( ssPv1(A)
| ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9308]) ).
cnf(c_1831,plain,
( ssPv1(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9309]) ).
cnf(c_9310,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1831,c_135]) ).
cnf(c_1844,plain,
( ssPv1(skf3(A))
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9310]) ).
cnf(c_9311,plain,
( ssPv2(skf2(A))
| ssPv3(A)
| ~ ssPv4(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1831,c_452]) ).
cnf(c_1861,plain,
( ssPv2(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9311]) ).
cnf(c_9312,plain,
( ssPv3(A)
| ssPv4(skf2(A))
| ~ ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1831,c_450]) ).
cnf(c_1863,plain,
( ssPv4(skf2(A))
| ~ ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9312]) ).
cnf(c_9313,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf2(A))
| ssPv4(A)
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_1823,c_734]) ).
cnf(c_1972,plain,
( ssPv2(skf2(A))
| ssPv3(skf2(A))
| ssPv4(A)
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_9313]) ).
cnf(c_9314,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1861,c_1139]) ).
cnf(c_9315,plain,
( ssPv3(A)
| ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9314]) ).
cnf(c_1975,plain,
( ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9315]) ).
cnf(c_9316,plain,
( ssPv3(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1861,c_919]) ).
cnf(c_1977,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9316]) ).
cnf(c_9317,plain,
( ssPv2(skf2(A))
| ~ ssPv1(A)
| ~ ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_1975,c_1761]) ).
cnf(c_2107,plain,
( ~ ssPv1(A)
| ~ ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9317]) ).
cnf(c_9318,plain,
( ssPv2(skf3(A))
| ssPv4(A)
| ssPv4(skf3(A))
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1546,c_1372]) ).
cnf(c_9319,plain,
( ssPv2(skf3(A))
| ssPv4(A)
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9318]) ).
cnf(c_9320,plain,
( ssPv2(skf3(A))
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9319]) ).
cnf(c_2442,plain,
( ssPv4(A)
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9320]) ).
cnf(c_9321,plain,
( ssPv2(skf3(A))
| ssPv4(A)
| ssPv2(A)
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2442,c_719]) ).
cnf(c_9322,plain,
( ssPv2(skf3(A))
| ssPv4(A)
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9321]) ).
cnf(c_9323,plain,
( ssPv2(skf3(A))
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9322]) ).
cnf(c_2450,plain,
( ssPv4(A)
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9323]) ).
cnf(c_9324,plain,
( ssPv4(skf3(A))
| ~ ssPv3(skf3(A))
| ~ ssPv3(A)
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_2442,c_457]) ).
cnf(c_2458,plain,
( ~ ssPv3(skf3(A))
| ~ ssPv3(A)
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9324]) ).
cnf(c_2493,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv3(skf2(A))
| ssPv4(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2450,c_1123]) ).
cnf(c_9325,plain,
( ssPv2(A)
| ssPv2(skf2(A))
| ssPv1(A)
| ~ ssPv3(A)
| ssPv4(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2493,c_745]) ).
cnf(c_2615,plain,
( ssPv2(skf2(A))
| ssPv1(A)
| ~ ssPv3(A)
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9325]) ).
cnf(c_9326,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv4(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2615,c_734]) ).
cnf(c_9327,plain,
( ssPv4(A)
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9326]) ).
cnf(c_2646,plain,
( ssPv2(skf2(A))
| ssPv1(A)
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9327]) ).
cnf(c_9328,plain,
( ssPv1(A)
| ssPv2(skf2(A))
| ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2646,c_571]) ).
cnf(c_9329,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9328]) ).
cnf(c_2671,plain,
( ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9329]) ).
cnf(c_9330,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ~ ssPv3(A)
| ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2671,c_137]) ).
cnf(c_9331,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9330]) ).
cnf(c_2695,plain,
( ~ ssPv3(A)
| ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9331]) ).
cnf(c_9332,plain,
( ssPv2(A)
| ssPv3(skf3(A))
| ~ ssPv4(A)
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2671,c_453]) ).
cnf(c_2725,plain,
( ssPv3(skf3(A))
| ~ ssPv4(A)
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9332]) ).
cnf(c_9333,plain,
( ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2695,c_1975]) ).
cnf(c_9334,plain,
( ssPv1(skf3(A))
| ssPv3(skf3(A))
| ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9333]) ).
cnf(c_2735,plain,
( ssPv3(skf3(A))
| ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9334]) ).
cnf(c_9335,plain,
( ssPv3(skf3(A))
| ssPv4(A)
| ~ ssPv2(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2735,c_451]) ).
cnf(c_2866,plain,
( ssPv4(A)
| ~ ssPv2(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9335]) ).
cnf(c_9336,plain,
( ssPv2(skf2(A))
| ssPv1(A)
| ssPv2(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2725,c_2646]) ).
cnf(c_9337,plain,
( ssPv2(skf2(A))
| ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9336]) ).
cnf(c_9338,plain,
( ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9337]) ).
cnf(c_3014,plain,
( ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_9338]) ).
cnf(c_9339,plain,
( ssPv2(skf2(A))
| ssPv1(A)
| ~ ssPv4(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_3014,c_504]) ).
cnf(c_9340,plain,
( ssPv2(skf2(A))
| ~ ssPv4(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9339]) ).
cnf(c_3019,plain,
( ~ ssPv4(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9340]) ).
cnf(c_9341,plain,
( ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv4(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2866,c_3014]) ).
cnf(c_9342,plain,
( ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv4(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9341]) ).
cnf(c_9343,plain,
( ssPv3(skf3(A))
| ssPv4(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9342]) ).
cnf(c_3066,plain,
( ssPv4(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9343]) ).
cnf(c_9344,plain,
( ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv3(skf2(A))
| ssPv4(A)
| ssPv3(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_3066,c_456]) ).
cnf(c_3090,plain,
( ~ ssPv3(A)
| ~ ssPv3(skf2(A))
| ssPv4(A)
| ssPv3(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9344]) ).
cnf(c_9345,plain,
( ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_3066,c_3019]) ).
cnf(c_9346,plain,
( ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9345]) ).
cnf(c_9347,plain,
( ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9346]) ).
cnf(c_3098,plain,
( ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_9347]) ).
cnf(c_9348,plain,
( ssPv3(skf3(A))
| ssPv2(skf2(A))
| ~ ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_2107,c_3098]) ).
cnf(c_9349,plain,
( ssPv3(skf3(A))
| ~ ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9348]) ).
cnf(c_3321,plain,
( ~ ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9349]) ).
cnf(c_9350,plain,
( ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3321,c_1977]) ).
cnf(c_9351,plain,
( ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9350]) ).
cnf(c_9352,plain,
( ssPv2(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9351]) ).
cnf(c_3324,plain,
( ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9352]) ).
cnf(c_9353,plain,
( ssPv3(skf3(A))
| ~ ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_3324,c_884]) ).
cnf(c_3336,plain,
( ~ ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_9353]) ).
cnf(c_9354,plain,
( ssPv4(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3324,c_1863]) ).
cnf(c_9355,plain,
( ssPv4(skf2(A))
| ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9354]) ).
cnf(c_3346,plain,
( ssPv4(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9355]) ).
cnf(c_9356,plain,
( ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv4(A)
| ssPv4(skf2(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3346,c_447]) ).
cnf(c_3367,plain,
( ssPv4(skf3(A))
| ~ ssPv4(A)
| ssPv4(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9356]) ).
cnf(c_9357,plain,
( ssPv1(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3346,c_1617]) ).
cnf(c_9358,plain,
( ssPv1(skf2(A))
| ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9357]) ).
cnf(c_3372,plain,
( ssPv1(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9358]) ).
cnf(c_3402,plain,
( ~ ssPv1(A)
| ~ ssPv2(skf2(A))
| ~ ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3372,c_517]) ).
cnf(c_9359,plain,
( ssPv4(skf2(A))
| ssPv3(A)
| ssPv4(skf3(A))
| ssPv4(skf3(A))
| ssPv4(skf2(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3367,c_1258]) ).
cnf(c_9360,plain,
( ssPv4(skf2(A))
| ssPv3(A)
| ssPv4(skf3(A))
| ssPv4(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9359]) ).
cnf(c_9361,plain,
( ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv4(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9360]) ).
cnf(c_3421,plain,
( ssPv4(skf3(A))
| ssPv4(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9361]) ).
cnf(c_9362,plain,
( ssPv1(skf2(A))
| ssPv4(skf3(A))
| ssPv3(A)
| ssPv4(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3421,c_1644]) ).
cnf(c_9363,plain,
( ssPv1(skf2(A))
| ssPv4(skf3(A))
| ssPv4(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9362]) ).
cnf(c_3436,plain,
( ssPv1(skf2(A))
| ssPv4(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9363]) ).
cnf(c_9364,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ~ ssPv4(A)
| ssPv2(skf2(A))
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_3336,c_734]) ).
cnf(c_3463,plain,
( ssPv3(skf2(A))
| ~ ssPv4(A)
| ssPv2(skf2(A))
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_9364]) ).
cnf(c_9365,plain,
( ssPv2(skf2(A))
| ssPv3(skf2(A))
| ssPv3(skf3(A))
| ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_3463,c_1972]) ).
cnf(c_9366,plain,
( ssPv2(skf2(A))
| ssPv3(skf2(A))
| ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_9365]) ).
cnf(c_9367,plain,
( ssPv2(skf2(A))
| ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_9366]) ).
cnf(c_3494,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_9367]) ).
cnf(c_9368,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ~ ssPv3(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_3494,c_1080]) ).
cnf(c_9369,plain,
( ssPv3(skf2(A))
| ~ ssPv3(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_9368]) ).
cnf(c_3505,plain,
( ~ ssPv3(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_9369]) ).
cnf(c_9370,plain,
( ssPv4(skf3(A))
| ssPv2(skf3(A))
| ~ ssPv3(A)
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_2458,c_734]) ).
cnf(c_9371,plain,
( ssPv4(skf3(A))
| ~ ssPv3(A)
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9370]) ).
cnf(c_3673,plain,
( ~ ssPv3(A)
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9371]) ).
cnf(c_9372,plain,
( ssPv1(skf2(A))
| ssPv4(skf3(A))
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3673,c_3436]) ).
cnf(c_3687,plain,
( ssPv1(skf2(A))
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9372]) ).
cnf(c_9373,plain,
( ssPv1(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A))
| ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3687,c_1296]) ).
cnf(c_9374,plain,
( ssPv1(skf2(A))
| ssPv1(A)
| ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9373]) ).
cnf(c_3719,plain,
( ssPv1(A)
| ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9374]) ).
cnf(c_9375,plain,
( ssPv2(skf3(A))
| ssPv4(skf3(A))
| ~ ssPv4(A)
| ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3719,c_443]) ).
cnf(c_9376,plain,
( ssPv2(skf3(A))
| ~ ssPv4(A)
| ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9375]) ).
cnf(c_3760,plain,
( ~ ssPv4(A)
| ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9376]) ).
cnf(c_9377,plain,
( ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A))
| ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3760,c_3687]) ).
cnf(c_9378,plain,
( ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9377]) ).
cnf(c_9379,plain,
( ssPv1(skf2(A))
| ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9378]) ).
cnf(c_3761,plain,
( ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9379]) ).
cnf(c_9380,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_702,c_1606]) ).
cnf(c_4194,plain,
( ssPv2(skf2(A))
| ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9380]) ).
cnf(c_9381,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_4194,c_734]) ).
cnf(c_9382,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9381]) ).
cnf(c_4210,plain,
( ssPv2(skf2(A))
| ssPv3(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9382]) ).
cnf(c_9383,plain,
( ssPv1(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_4210,c_766]) ).
cnf(c_9384,plain,
( ssPv1(A)
| ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9383]) ).
cnf(c_4223,plain,
( ssPv1(A)
| ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9384]) ).
cnf(c_9385,plain,
( ssPv2(skf2(A))
| ssPv3(A)
| ~ ssPv4(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_4223,c_452]) ).
cnf(c_4244,plain,
( ssPv3(A)
| ~ ssPv4(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9385]) ).
cnf(c_9386,plain,
( ssPv3(A)
| ssPv3(skf2(A))
| ssPv3(A)
| ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_4244,c_919]) ).
cnf(c_9387,plain,
( ssPv3(A)
| ssPv3(A)
| ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9386]) ).
cnf(c_4467,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9387]) ).
cnf(c_9388,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_4467,c_3505]) ).
cnf(c_9389,plain,
( ssPv3(skf2(A))
| ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9388]) ).
cnf(c_4469,plain,
( ssPv2(skf2(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9389]) ).
cnf(c_9390,plain,
( ssPv3(skf3(A))
| ssPv3(A)
| ~ ssPv2(skf2(A))
| ~ ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3402,c_1831]) ).
cnf(c_9391,plain,
( ssPv3(skf3(A))
| ~ ssPv2(skf2(A))
| ~ ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9390]) ).
cnf(c_4627,plain,
( ~ ssPv2(skf2(A))
| ~ ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9391]) ).
cnf(c_9392,plain,
( ssPv3(skf3(A))
| ssPv3(A)
| ~ ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_4627,c_752]) ).
cnf(c_9393,plain,
( ssPv3(skf3(A))
| ~ ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9392]) ).
cnf(c_4635,plain,
( ~ ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9393]) ).
cnf(c_9394,plain,
( ssPv3(skf3(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_4635,c_3324]) ).
cnf(c_9395,plain,
( ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9394]) ).
cnf(c_4641,plain,
( ssPv3(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9395]) ).
cnf(c_9396,plain,
( ssPv3(skf3(A))
| ~ ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_4641,c_884]) ).
cnf(c_4654,plain,
( ~ ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_9396]) ).
cnf(c_9397,plain,
( ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv3(skf2(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_4641,c_1227]) ).
cnf(c_4662,plain,
( ssPv4(skf3(A))
| ~ ssPv3(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9397]) ).
cnf(c_9398,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_4641,c_702]) ).
cnf(c_4666,plain,
( ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9398]) ).
cnf(c_9399,plain,
( ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv4(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_4641,c_447]) ).
cnf(c_4667,plain,
( ssPv4(skf3(A))
| ~ ssPv4(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9399]) ).
cnf(c_9400,plain,
( ssPv3(A)
| ssPv3(skf2(A))
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_4666,c_919]) ).
cnf(c_4718,plain,
( ssPv3(A)
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9400]) ).
cnf(c_9401,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ssPv2(skf3(A))
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_4666,c_607]) ).
cnf(c_9402,plain,
( ssPv3(skf2(A))
| ssPv2(skf3(A))
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9401]) ).
cnf(c_4720,plain,
( ssPv2(skf3(A))
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9402]) ).
cnf(c_9403,plain,
( ssPv4(skf3(A))
| ssPv3(A)
| ssPv3(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_4718,c_4662]) ).
cnf(c_4721,plain,
( ssPv4(skf3(A))
| ssPv3(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9403]) ).
cnf(c_9404,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv3(skf2(A))
| ssPv3(skf2(skf2(A))) ),
inference(resolve,[status(thm)],[c_4718,c_4666]) ).
cnf(c_4724,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv3(skf2(skf2(A))) ),
inference(copy,[status(thm)],[c_9404]) ).
cnf(c_9405,plain,
( ssPv4(skf3(A))
| ssPv3(A)
| ssPv4(skf3(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_4721,c_4667]) ).
cnf(c_9406,plain,
( ssPv4(skf3(A))
| ssPv4(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9405]) ).
cnf(c_4743,plain,
( ssPv4(skf3(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9406]) ).
cnf(c_9407,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_4743,c_1844]) ).
cnf(c_4808,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_9407]) ).
cnf(c_9408,plain,
( ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_1097,c_3761]) ).
cnf(c_9409,plain,
( ssPv1(skf2(A))
| ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ~ ssPv4(A) ),
inference(copy,[status(thm)],[c_9408]) ).
cnf(c_5253,plain,
( ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ~ ssPv4(A) ),
inference(copy,[status(thm)],[c_9409]) ).
cnf(c_9410,plain,
( ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_5253,c_4720]) ).
cnf(c_9411,plain,
( ssPv2(skf3(A))
| ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A)) ),
inference(copy,[status(thm)],[c_9410]) ).
cnf(c_5266,plain,
( ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A)) ),
inference(copy,[status(thm)],[c_9411]) ).
cnf(c_9412,plain,
( ssPv3(skf2(A))
| ssPv4(skf2(A))
| ~ ssPv4(A)
| ssPv3(skf2(A))
| ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_5266,c_1503]) ).
cnf(c_5291,plain,
( ssPv4(skf2(A))
| ~ ssPv4(A)
| ssPv3(skf2(A))
| ssPv1(skf2(A)) ),
inference(copy,[status(thm)],[c_9412]) ).
cnf(c_9413,plain,
( ssPv1(A)
| ssPv3(A)
| ssPv1(A)
| ~ ssPv4(skf3(A))
| ~ ssPv4(skf3(skf3(A))) ),
inference(resolve,[status(thm)],[c_1096,c_4808]) ).
cnf(c_5740,plain,
( ssPv3(A)
| ssPv1(A)
| ~ ssPv4(skf3(A))
| ~ ssPv4(skf3(skf3(A))) ),
inference(copy,[status(thm)],[c_9413]) ).
cnf(c_9414,plain,
( ssPv1(skf3(A))
| ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A))
| ~ ssPv3(skf3(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_1108,c_2646]) ).
cnf(c_5888,plain,
( ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A))
| ~ ssPv3(skf3(A))
| ~ ssPv3(A) ),
inference(copy,[status(thm)],[c_9414]) ).
cnf(c_9415,plain,
( ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_5888,c_734]) ).
cnf(c_9416,plain,
( ssPv4(skf3(A))
| ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A))
| ~ ssPv3(A) ),
inference(copy,[status(thm)],[c_9415]) ).
cnf(c_5913,plain,
( ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A))
| ~ ssPv3(A) ),
inference(copy,[status(thm)],[c_9416]) ).
cnf(c_9417,plain,
( ssPv4(skf3(A))
| ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_5913,c_4743]) ).
cnf(c_5922,plain,
( ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9417]) ).
cnf(c_5953,plain,
( ~ ssPv3(A)
| ~ ssPv1(skf2(A))
| ~ ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_5922,c_514]) ).
cnf(c_9418,plain,
( ssPv2(skf3(A))
| ssPv4(skf3(A))
| ~ ssPv3(A)
| ~ ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_5953,c_3761]) ).
cnf(c_9419,plain,
( ssPv2(skf3(A))
| ~ ssPv3(A)
| ~ ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9418]) ).
cnf(c_6032,plain,
( ~ ssPv3(A)
| ~ ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9419]) ).
cnf(c_9420,plain,
( ssPv4(skf3(A))
| ssPv2(skf3(A))
| ~ ssPv3(A)
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_6032,c_734]) ).
cnf(c_9421,plain,
( ssPv4(skf3(A))
| ~ ssPv3(A)
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9420]) ).
cnf(c_6043,plain,
( ~ ssPv3(A)
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9421]) ).
cnf(c_9422,plain,
( ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_6043,c_4743]) ).
cnf(c_6051,plain,
( ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9422]) ).
cnf(c_6058,plain,
( ssPv2(A)
| ssPv3(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_6051,c_1747]) ).
cnf(c_6059,plain,
( ssPv3(skf2(A))
| ssPv4(skf2(A))
| ~ ssPv4(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_6051,c_1503]) ).
cnf(c_6060,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv3(skf2(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_6051,c_1123]) ).
cnf(c_9423,plain,
( ssPv4(skf2(A))
| ssPv2(skf2(A))
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_1185,c_2450]) ).
cnf(c_6226,plain,
( ssPv2(skf2(A))
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9423]) ).
cnf(c_9424,plain,
( ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(skf3(A))
| ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_6226,c_1545]) ).
cnf(c_9425,plain,
( ssPv2(skf2(A))
| ssPv4(skf3(A))
| ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9424]) ).
cnf(c_6341,plain,
( ssPv4(skf3(A))
| ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9425]) ).
cnf(c_9426,plain,
( ssPv2(skf2(A))
| ssPv4(A)
| ssPv2(A)
| ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_6341,c_726]) ).
cnf(c_9427,plain,
( ssPv2(skf2(A))
| ssPv4(A)
| ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9426]) ).
cnf(c_9428,plain,
( ssPv2(skf2(A))
| ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9427]) ).
cnf(c_6383,plain,
( ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9428]) ).
cnf(c_9429,plain,
( ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv3(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_6383,c_456]) ).
cnf(c_6409,plain,
( ~ ssPv3(A)
| ~ ssPv3(skf2(A))
| ssPv2(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9429]) ).
cnf(c_9430,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_1226,c_4724]) ).
cnf(c_9431,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv3(A) ),
inference(copy,[status(thm)],[c_9430]) ).
cnf(c_6793,plain,
( ssPv3(skf2(A))
| ssPv4(A)
| ~ ssPv3(A) ),
inference(copy,[status(thm)],[c_9431]) ).
cnf(c_9432,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv3(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_6793,c_4718]) ).
cnf(c_9433,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9432]) ).
cnf(c_6808,plain,
( ssPv3(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9433]) ).
cnf(c_9434,plain,
( ssPv3(skf2(A))
| ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_6808,c_6059]) ).
cnf(c_6810,plain,
( ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9434]) ).
cnf(c_9435,plain,
( ssPv4(skf2(A))
| ssPv3(skf2(A))
| ssPv1(skf2(A))
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_6808,c_5291]) ).
cnf(c_6811,plain,
( ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9435]) ).
cnf(c_9436,plain,
( ~ ssPv3(A)
| ssPv2(A)
| ssPv4(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_6808,c_6409]) ).
cnf(c_6834,plain,
( ~ ssPv3(A)
| ssPv2(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9436]) ).
cnf(c_6835,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ssPv4(skf3(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_6808,c_6060]) ).
cnf(c_9437,plain,
( ~ ssPv3(A)
| ssPv4(A)
| ssPv3(skf3(A))
| ssPv1(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_6808,c_3090]) ).
cnf(c_6843,plain,
( ~ ssPv3(A)
| ssPv3(skf3(A))
| ssPv1(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9437]) ).
cnf(c_6848,plain,
( ssPv1(skf2(A))
| ~ ssPv3(skf2(A))
| ~ ssPv4(A)
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_6808,c_1122]) ).
cnf(c_9438,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv2(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_6834,c_734]) ).
cnf(c_9439,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9438]) ).
cnf(c_6871,plain,
( ssPv2(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9439]) ).
cnf(c_6873,plain,
( ~ ssPv4(A)
| ssPv3(skf3(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_6871,c_4654]) ).
cnf(c_9440,plain,
( ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(skf3(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_6871,c_1545]) ).
cnf(c_6876,plain,
( ssPv2(A)
| ssPv4(skf3(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_9440]) ).
cnf(c_9441,plain,
( ssPv4(A)
| ssPv4(skf2(A))
| ~ ssPv3(skf3(A))
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_6871,c_1189]) ).
cnf(c_6892,plain,
( ssPv4(A)
| ~ ssPv3(skf3(A))
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9441]) ).
cnf(c_9442,plain,
( ssPv2(skf2(A))
| ~ ssPv3(A)
| ~ ssPv3(skf3(A))
| ssPv4(skf3(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_6876,c_1068]) ).
cnf(c_7014,plain,
( ~ ssPv3(A)
| ~ ssPv3(skf3(A))
| ssPv4(skf3(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_9442]) ).
cnf(c_9443,plain,
( ssPv2(A)
| ssPv3(skf2(A))
| ssPv4(skf3(A))
| ssPv4(skf3(A))
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_6810,c_6058]) ).
cnf(c_9444,plain,
( ssPv2(A)
| ssPv3(skf2(A))
| ssPv4(skf3(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9443]) ).
cnf(c_7319,plain,
( ssPv2(A)
| ssPv4(skf3(A))
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_9444]) ).
cnf(c_9445,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ssPv4(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_7319,c_6060]) ).
cnf(c_7324,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9445]) ).
cnf(c_9446,plain,
( ssPv4(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_6835,c_4743]) ).
cnf(c_7471,plain,
( ssPv1(A)
| ssPv4(skf3(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9446]) ).
cnf(c_9447,plain,
( ssPv1(A)
| ssPv3(skf3(A))
| ssPv4(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_7471,c_739]) ).
cnf(c_9448,plain,
( ssPv1(A)
| ssPv3(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9447]) ).
cnf(c_7480,plain,
( ssPv3(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9448]) ).
cnf(c_9449,plain,
( ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv1(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_6843,c_4641]) ).
cnf(c_7617,plain,
( ssPv3(skf3(A))
| ssPv1(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9449]) ).
cnf(c_9450,plain,
( ssPv4(A)
| ssPv4(skf2(A))
| ssPv1(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_7617,c_6892]) ).
cnf(c_7647,plain,
( ssPv4(skf2(A))
| ssPv1(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9450]) ).
cnf(c_9451,plain,
( ssPv4(A)
| ssPv4(skf2(A))
| ~ ssPv2(skf2(A))
| ssPv4(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_7647,c_444]) ).
cnf(c_9452,plain,
( ssPv4(A)
| ~ ssPv2(skf2(A))
| ssPv4(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9451]) ).
cnf(c_7670,plain,
( ~ ssPv2(skf2(A))
| ssPv4(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9452]) ).
cnf(c_9453,plain,
( ssPv4(skf2(A))
| ssPv4(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_7670,c_6871]) ).
cnf(c_7679,plain,
( ssPv4(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9453]) ).
cnf(c_9454,plain,
( ssPv4(A)
| ssPv3(skf3(A))
| ssPv4(skf3(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_7679,c_1168]) ).
cnf(c_7689,plain,
( ssPv3(skf3(A))
| ssPv4(skf3(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_9454]) ).
cnf(c_9455,plain,
( ssPv3(skf3(A))
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_7689,c_6873]) ).
cnf(c_7691,plain,
( ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9455]) ).
cnf(c_9456,plain,
( ssPv4(skf3(A))
| ssPv1(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_7324,c_4743]) ).
cnf(c_7764,plain,
( ssPv1(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9456]) ).
cnf(c_9457,plain,
( ssPv4(skf3(A))
| ~ ssPv3(skf3(A))
| ~ ssPv3(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_7764,c_457]) ).
cnf(c_7786,plain,
( ~ ssPv3(skf3(A))
| ~ ssPv3(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9457]) ).
cnf(c_9458,plain,
( ssPv1(A)
| ssPv4(skf3(A))
| ~ ssPv3(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_7786,c_7480]) ).
cnf(c_9459,plain,
( ssPv1(A)
| ~ ssPv3(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9458]) ).
cnf(c_8038,plain,
( ~ ssPv3(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9459]) ).
cnf(c_9460,plain,
( ssPv4(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_8038,c_4743]) ).
cnf(c_8050,plain,
( ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9460]) ).
cnf(c_9461,plain,
( ssPv4(skf3(A))
| ~ ssPv2(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_8050,c_1772]) ).
cnf(c_8057,plain,
( ~ ssPv2(skf2(A))
| ~ ssPv4(skf2(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9461]) ).
cnf(c_9462,plain,
( ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv1(skf2(A))
| ~ ssPv4(A)
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_6848,c_6811]) ).
cnf(c_9463,plain,
( ssPv4(skf2(A))
| ssPv1(skf2(A))
| ~ ssPv4(A)
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9462]) ).
cnf(c_8181,plain,
( ssPv1(skf2(A))
| ~ ssPv4(A)
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9463]) ).
cnf(c_9464,plain,
( ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_8181,c_7679]) ).
cnf(c_8213,plain,
( ssPv1(skf2(A))
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_9464]) ).
cnf(c_9465,plain,
( ssPv2(skf2(A))
| ssPv4(skf3(A))
| ~ ssPv3(A)
| ssPv4(skf3(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_7014,c_7691]) ).
cnf(c_9466,plain,
( ssPv2(skf2(A))
| ~ ssPv3(A)
| ssPv4(skf3(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_9465]) ).
cnf(c_8392,plain,
( ~ ssPv3(A)
| ssPv4(skf3(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_9466]) ).
cnf(c_9467,plain,
( ssPv4(skf3(A))
| ssPv4(skf3(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_8392,c_4743]) ).
cnf(c_8407,plain,
( ssPv4(skf3(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_9467]) ).
cnf(c_9468,plain,
( ~ ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_8407,c_8057]) ).
cnf(c_8408,plain,
( ~ ssPv4(skf2(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9468]) ).
cnf(c_8423,plain,
( ssPv1(skf2(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_8408,c_8213]) ).
cnf(c_8442,plain,
( ~ ssPv1(A)
| ~ ssPv2(skf2(A))
| ~ ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_8423,c_517]) ).
cnf(c_9469,plain,
( ssPv4(skf3(A))
| ~ ssPv2(skf2(A))
| ~ ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_8442,c_8050]) ).
cnf(c_8529,plain,
( ~ ssPv2(skf2(A))
| ~ ssPv2(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9469]) ).
cnf(c_9470,plain,
( ssPv4(skf3(A))
| ~ ssPv2(skf2(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_8529,c_6871]) ).
cnf(c_8548,plain,
( ~ ssPv2(skf2(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_9470]) ).
cnf(c_9471,plain,
( ssPv4(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_8548,c_8407]) ).
cnf(c_8549,plain,
ssPv4(skf3(A)),
inference(copy,[status(thm)],[c_9471]) ).
cnf(c_9472,plain,
( ssPv3(A)
| ssPv1(A)
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_8549,c_5740]) ).
cnf(c_8727,plain,
( ssPv3(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_8549,c_9472]) ).
cnf(c_8786,plain,
( ssPv1(skf3(A))
| ~ ssPv3(skf3(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_8549,c_1110]) ).
cnf(c_9473,plain,
( ssPv1(A)
| ~ ssPv4(skf3(A))
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_8549,c_1096]) ).
cnf(c_8788,plain,
( ssPv1(A)
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_8549,c_9473]) ).
cnf(c_9474,plain,
( ssPv1(skf3(A))
| ssPv1(skf3(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_8786,c_8727]) ).
cnf(c_9042,plain,
( ssPv1(skf3(A))
| ~ ssPv3(A) ),
inference(copy,[status(thm)],[c_9474]) ).
cnf(c_9051,plain,
( ssPv1(A)
| ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_9042,c_8727]) ).
cnf(c_9475,plain,
( ssPv1(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_9051,c_8788]) ).
cnf(c_9069,plain,
ssPv1(A),
inference(copy,[status(thm)],[c_9475]) ).
cnf(c_9476,plain,
( ssPv2(A)
| ~ ssPv1(skf3(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_9069,c_1762]) ).
cnf(c_9131,plain,
( ssPv2(A)
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_9069,c_9476]) ).
cnf(c_9477,plain,
( ~ ssPv1(skf2(A))
| ~ ssPv2(skf2(skf2(A)))
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_9069,c_550]) ).
cnf(c_9152,plain,
( ~ ssPv2(skf2(skf2(A)))
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_9069,c_9477]) ).
cnf(c_9478,plain,
( ssPv2(skf2(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_9131,c_4469]) ).
cnf(c_9203,plain,
ssPv2(skf2(A)),
inference(copy,[status(thm)],[c_9478]) ).
cnf(c_9214,plain,
~ ssPv2(A),
inference(resolve,[status(thm)],[c_9203,c_9152]) ).
cnf(c_9215,plain,
$false,
inference(resolve,[status(thm)],[c_9214,c_9203]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN784-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 : n018.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:31:52 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1140870 was started by sandbox2 on n018,
% 0.08/0.36 % Sat Sep 26 18:31:52 2026
% 0.08/0.36 % 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).
% 6.10/1.31
% 6.10/1.31 % given #500 (T,wt=22): 367 -ssPv1(skf3(A)) | -ssRr(A,B) | -ssPv3(B) | -ssPv1(A) | ssPv2(B). [factor(361,b,d)].
% 6.10/1.31
% 6.10/1.31 % given #1000 (W,wt=18): 6892 ssPv4(skf2(A)) | -ssPv3(skf3(A)) | ssPv4(A). [resolve(6871,b,1189,b),merge(c)].
% 6.10/1.31
% 6.10/1.31 % SZS status Unsatisfiable for theBenchmark
% 6.10/1.31
% 6.10/1.31 % Proof 1 at 0.73 (+ 0.18) seconds.
% 6.10/1.31 % Length of proof is 323.
% 6.10/1.31 % Level of proof is 67.
% 6.10/1.31 % Maximum clause weight is 28.000.
% 6.10/1.31 % Given clauses 1180.
% 6.10/1.31
% 6.10/1.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------