%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN796-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:39:39 AM UTC 2026
% Result : Unsatisfiable 7.03s 11.34s
% Output : CNFRefutation 7.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 143
% Number of leaves : 42
% Syntax : Number of formulae : 621 ( 10 unt; 0 def)
% Number of atoms : 2791 ( 0 equ)
% Maximal formula atoms : 7 ( 4 avg)
% Number of connectives : 2988 ( 818 ~;2170 |; 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 : 851 ( 5 sgn 128 !; 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_0)
| ssPv3(VAR_0)
| ssPv1(VAR_0)
| ssPv3(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause3) ).
cnf(c_3,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv1(A)
| ssPv3(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause3]) ).
fof(clause4,axiom,
! [VAR_0,VAR_1] :
( ssPv3(VAR_0)
| ssPv2(VAR_0)
| ssPv1(VAR_1)
| ~ ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause4) ).
cnf(c_4,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv1(B)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause4]) ).
fof(clause5,axiom,
! [VAR_0,VAR_1] :
( ssPv4(VAR_1)
| ssPv1(VAR_1)
| ssPv2(VAR_0)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause5) ).
cnf(c_5,plain,
( ssPv4(B)
| ssPv1(B)
| ssPv2(A)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause5]) ).
fof(clause6,axiom,
! [VAR_0,VAR_1] :
( ssPv3(VAR_1)
| ssPv1(VAR_1)
| ssPv2(VAR_0)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause6) ).
cnf(c_6,plain,
( ssPv3(B)
| ssPv1(B)
| ssPv2(A)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause6]) ).
fof(clause7,axiom,
! [VAR_0,VAR_1] :
( ssPv2(VAR_1)
| ~ ssPv4(VAR_1)
| ~ ssPv1(VAR_1)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause7) ).
cnf(c_7,plain,
( ssPv2(B)
| ~ ssPv4(B)
| ~ ssPv1(B)
| ~ ssPv1(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause7]) ).
fof(clause8,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_1)
| ssPv1(VAR_1)
| ssPv2(VAR_2)
| ssPv4(VAR_0)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause8) ).
cnf(c_8,plain,
( ssPv2(B)
| ssPv1(B)
| ssPv2(C)
| ssPv4(A)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause8]) ).
fof(clause9,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_1)
| ssPv1(VAR_2)
| ssPv4(VAR_0)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause9) ).
cnf(c_9,plain,
( ssPv4(B)
| ssPv1(C)
| ssPv4(A)
| ~ ssPv1(B)
| ~ ssRr(C,B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause9]) ).
fof(clause10,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_1)
| ssPv3(VAR_1)
| ssPv3(VAR_2)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause10) ).
cnf(c_10,plain,
( ssPv4(B)
| ssPv3(B)
| ssPv3(C)
| ~ ssRr(C,B)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause10]) ).
fof(clause11,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_0)
| ssPv3(VAR_0)
| ssPv2(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)
| ssPv2(C)
| ~ ssRr(A,C)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause11]) ).
fof(clause12,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_1)
| ssPv2(VAR_1)
| ssPv2(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause12) ).
cnf(c_12,plain,
( ssPv3(B)
| ssPv2(B)
| ssPv2(C)
| ~ ssRr(B,C)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause12]) ).
fof(clause13,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_1)
| ssPv2(VAR_2)
| ssPv4(VAR_0)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause13) ).
cnf(c_13,plain,
( ssPv1(B)
| ssPv2(C)
| ssPv4(A)
| ~ ssPv3(B)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause13]) ).
fof(clause14,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_1)
| ssPv4(VAR_2)
| ssPv1(VAR_0)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause14) ).
cnf(c_14,plain,
( ssPv1(B)
| ssPv4(C)
| ssPv1(A)
| ~ ssPv2(B)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause14]) ).
fof(clause15,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_1)
| ssPv1(VAR_1)
| ssPv4(VAR_2)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause15) ).
cnf(c_15,plain,
( ssPv4(B)
| ssPv1(B)
| ssPv4(C)
| ~ ssRr(C,B)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause15]) ).
fof(clause17,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_1)
| ssPv1(VAR_1)
| ssPv2(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause17) ).
cnf(c_17,plain,
( ssPv3(B)
| ssPv1(B)
| ssPv2(C)
| ~ ssRr(B,C)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause17]) ).
fof(clause18,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_2)
| ssPv4(VAR_0)
| ~ ssPv3(VAR_1)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause18) ).
cnf(c_18,plain,
( ssPv2(C)
| ssPv4(A)
| ~ ssPv3(B)
| ~ ssPv2(B)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause18]) ).
fof(clause19,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_2)
| ssPv4(VAR_1)
| ~ ssPv4(VAR_0)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause19) ).
cnf(c_19,plain,
( ssPv3(C)
| ssPv4(B)
| ~ ssPv4(A)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause19]) ).
fof(clause20,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_2)
| ssPv3(VAR_0)
| ~ ssPv2(VAR_1)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause20) ).
cnf(c_20,plain,
( ssPv2(C)
| ssPv3(A)
| ~ ssPv2(B)
| ~ ssPv1(B)
| ~ ssRr(C,B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause20]) ).
fof(clause21,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_1)
| ssPv2(VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause21) ).
cnf(c_21,plain,
( ssPv3(B)
| ssPv2(C)
| ~ ssPv4(B)
| ~ ssRr(B,C)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause21]) ).
fof(clause22,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_0)
| ssPv1(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,
( ssPv3(A)
| ssPv1(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] :
( ssPv2(VAR_1)
| ssPv2(VAR_0)
| ~ ssPv3(VAR_1)
| ~ ssPv2(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause24) ).
cnf(c_24,plain,
( ssPv2(B)
| ssPv2(A)
| ~ ssPv3(B)
| ~ ssPv2(C)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause24]) ).
fof(clause25,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_1)
| ssPv2(VAR_0)
| ~ ssPv1(VAR_1)
| ~ ssPv4(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause25) ).
cnf(c_25,plain,
( ssPv2(B)
| ssPv2(A)
| ~ ssPv1(B)
| ~ ssPv4(C)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause25]) ).
fof(clause27,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_1)
| ssPv1(VAR_0)
| ~ ssPv2(VAR_1)
| ~ ssPv4(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause27) ).
cnf(c_27,plain,
( ssPv1(B)
| ssPv1(A)
| ~ ssPv2(B)
| ~ ssPv4(C)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause27]) ).
fof(clause28,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv2(VAR_0)
| ssPv1(VAR_0)
| ~ ssPv2(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause28) ).
cnf(c_28,plain,
( ssPv2(A)
| ssPv1(A)
| ~ ssPv2(C)
| ~ ssRr(A,C)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause28]) ).
fof(clause29,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_0)
| ~ ssPv4(VAR_1)
| ~ ssPv3(VAR_1)
| ~ ssPv4(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause29) ).
cnf(c_29,plain,
( ssPv4(A)
| ~ ssPv4(B)
| ~ ssPv3(B)
| ~ ssPv4(C)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause29]) ).
fof(clause30,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv4(VAR_2)
| ~ ssPv3(VAR_0)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause30) ).
cnf(c_30,plain,
( ssPv4(C)
| ~ ssPv3(A)
| ~ ssPv2(A)
| ~ ssRr(A,C)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause30]) ).
fof(clause31,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv3(VAR_0)
| ~ ssPv3(VAR_1)
| ~ ssPv1(VAR_1)
| ~ ssPv1(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause31) ).
cnf(c_31,plain,
( ssPv3(A)
| ~ ssPv3(B)
| ~ ssPv1(B)
| ~ ssPv1(C)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause31]) ).
fof(clause32,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_2)
| ~ ssPv3(VAR_0)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause32) ).
cnf(c_32,plain,
( ssPv1(C)
| ~ ssPv3(A)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause32]) ).
fof(clause33,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ssPv1(VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv3(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause33) ).
cnf(c_33,plain,
( ssPv1(C)
| ~ ssPv2(A)
| ~ ssPv1(A)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause33]) ).
fof(clause34,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ ssPv4(VAR_0)
| ~ ssPv1(VAR_0)
| ~ ssPv1(VAR_2)
| ~ ssRr(VAR_0,VAR_2)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause34) ).
cnf(c_34,plain,
( ~ ssPv4(A)
| ~ ssPv1(A)
| ~ ssPv1(C)
| ~ ssRr(A,C)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause34]) ).
fof(clause35,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv4(VAR_3)
| ssPv2(VAR_2)
| ssPv3(VAR_0)
| ~ ssPv1(VAR_1)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause35) ).
cnf(c_35,plain,
( ssPv4(D)
| ssPv2(C)
| ssPv3(A)
| ~ ssPv1(B)
| ~ ssRr(B,D)
| ~ ssRr(C,B)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause35]) ).
fof(clause37,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv2(VAR_1)
| ssPv4(VAR_3)
| ssPv4(VAR_2)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause37) ).
cnf(c_37,plain,
( ssPv2(B)
| ssPv4(D)
| ssPv4(C)
| ~ ssRr(B,D)
| ~ ssRr(C,B)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause37]) ).
fof(clause38,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv2(VAR_1)
| ssPv4(VAR_3)
| ssPv4(VAR_0)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv1(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause38) ).
cnf(c_38,plain,
( ssPv2(B)
| ssPv4(D)
| ssPv4(A)
| ~ ssRr(B,D)
| ~ ssPv1(C)
| ~ ssRr(B,C)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause38]) ).
fof(clause40,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv3(VAR_1)
| ssPv4(VAR_2)
| ~ ssPv2(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv3(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause40) ).
cnf(c_40,plain,
( ssPv3(B)
| ssPv4(C)
| ~ ssPv2(D)
| ~ ssRr(B,D)
| ~ ssRr(C,B)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause40]) ).
fof(clause42,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv2(VAR_1)
| ssPv4(VAR_2)
| ~ ssPv4(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv1(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause42) ).
cnf(c_42,plain,
( ssPv2(B)
| ssPv4(C)
| ~ ssPv4(D)
| ~ ssRr(B,D)
| ~ ssRr(C,B)
| ~ ssPv1(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause42]) ).
fof(clause44,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv3(VAR_2)
| ~ ssPv2(VAR_1)
| ~ ssPv1(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause44) ).
cnf(c_44,plain,
( ssPv3(C)
| ~ ssPv2(B)
| ~ ssPv1(D)
| ~ ssRr(B,D)
| ~ ssRr(C,B)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause44]) ).
fof(clause45,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv1(VAR_3)
| ~ ssPv2(VAR_1)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_1,VAR_2)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause45) ).
cnf(c_45,plain,
( ssPv1(D)
| ~ ssPv2(B)
| ~ ssRr(B,D)
| ~ ssPv3(C)
| ~ ssRr(B,C)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause45]) ).
fof(clause46,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv2(VAR_1)
| ~ ssPv1(VAR_3)
| ~ ssRr(VAR_3,VAR_1)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause46) ).
cnf(c_46,plain,
( ssPv2(B)
| ~ ssPv1(D)
| ~ ssRr(D,B)
| ~ ssPv3(C)
| ~ ssRr(C,B)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause46]) ).
fof(clause48,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv3(VAR_3)
| ~ ssPv4(VAR_1)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv2(VAR_2)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause48) ).
cnf(c_48,plain,
( ssPv3(D)
| ~ ssPv4(B)
| ~ ssRr(B,D)
| ~ ssPv2(C)
| ~ ssRr(C,B)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause48]) ).
fof(clause50,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ssPv1(VAR_1)
| ~ ssPv3(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv3(VAR_2)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv4(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause50) ).
cnf(c_50,plain,
( ssPv1(B)
| ~ ssPv3(D)
| ~ ssRr(B,D)
| ~ ssPv3(C)
| ~ ssRr(C,B)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause50]) ).
fof(clause52,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ ssPv1(VAR_1)
| ~ ssPv1(VAR_3)
| ~ ssRr(VAR_1,VAR_3)
| ~ ssPv1(VAR_2)
| ~ ssRr(VAR_2,VAR_1)
| ~ ssPv2(VAR_0)
| ~ ssRr(VAR_0,VAR_1) ),
file('theBenchmark.p',clause52) ).
cnf(c_52,plain,
( ~ ssPv1(B)
| ~ ssPv1(D)
| ~ ssRr(B,D)
| ~ ssPv1(C)
| ~ ssRr(C,B)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(clausify,[status(thm)],[clause52]) ).
cnf(c_57,plain,
( ssPv4(B)
| ssPv1(A)
| ssPv4(A)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_9]) ).
cnf(c_59,plain,
( ssPv4(B)
| ssPv3(B)
| ssPv3(A)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_10]) ).
cnf(c_61,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv2(B)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_11]) ).
cnf(c_65,plain,
( ssPv4(B)
| ssPv1(B)
| ssPv4(A)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_15]) ).
cnf(c_68,plain,
( ssPv3(B)
| ssPv4(B)
| ~ ssPv4(A)
| ~ ssPv1(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_19]) ).
cnf(c_69,plain,
( ssPv2(A)
| ssPv3(A)
| ~ ssPv2(B)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_20]) ).
cnf(c_70,plain,
( ssPv3(A)
| ssPv1(B)
| ~ ssPv1(A)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_22]) ).
cnf(c_76,plain,
( ssPv2(A)
| ssPv1(A)
| ~ ssPv2(B)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_28]) ).
cnf(c_78,plain,
( ssPv4(B)
| ~ ssPv3(A)
| ~ ssPv2(A)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_30]) ).
cnf(c_80,plain,
( ssPv1(B)
| ~ ssPv3(A)
| ~ ssPv1(A)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_32]) ).
cnf(c_81,plain,
( ssPv1(B)
| ~ ssPv2(A)
| ~ ssPv1(A)
| ~ ssPv3(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_33]) ).
cnf(c_82,plain,
( ~ ssPv4(A)
| ~ ssPv1(A)
| ~ ssPv1(B)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_113,plain,
( ssPv2(B)
| ~ ssPv1(C)
| ~ ssRr(C,B)
| ~ ssPv3(A)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_46]) ).
cnf(c_146,plain,
( ssPv2(B)
| ~ ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_113]) ).
cnf(c_156,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_3,c_2]) ).
cnf(c_158,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv1(skf2(A))
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_4,c_2]) ).
cnf(c_159,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A)
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_4,c_1]) ).
cnf(c_160,plain,
( ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv2(A)
| ~ ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_5,c_2]) ).
cnf(c_161,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_5,c_1]) ).
cnf(c_163,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_6,c_1]) ).
cnf(c_164,plain,
( ssPv2(skf2(A))
| ~ ssPv4(skf2(A))
| ~ ssPv1(skf2(A))
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_7,c_2]) ).
cnf(c_167,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv2(B)
| ssPv4(skf3(A))
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_8,c_1]) ).
cnf(c_189,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv2(B)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_12,c_1]) ).
cnf(c_195,plain,
( ssPv1(A)
| ssPv2(B)
| ssPv4(skf3(A))
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_13,c_1]) ).
cnf(c_199,plain,
( ssPv1(A)
| ssPv4(B)
| ssPv1(skf3(A))
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_14,c_1]) ).
cnf(c_217,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv2(B)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_17,c_1]) ).
cnf(c_221,plain,
( ssPv2(B)
| ssPv4(skf3(A))
| ~ ssPv3(A)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_18,c_1]) ).
cnf(c_233,plain,
( ssPv3(A)
| ssPv2(B)
| ~ ssPv4(A)
| ~ ssRr(A,B)
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_21,c_1]) ).
cnf(c_247,plain,
( ssPv2(A)
| ssPv2(skf3(A))
| ~ ssPv3(A)
| ~ ssPv2(B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_24,c_1]) ).
cnf(c_253,plain,
( ssPv2(A)
| ssPv2(skf3(A))
| ~ ssPv1(A)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_25,c_1]) ).
cnf(c_263,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ~ ssPv2(A)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_27,c_1]) ).
cnf(c_264,plain,
( ssPv1(B)
| ssPv1(A)
| ~ ssPv2(B)
| ~ ssPv4(skf2(B))
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_27,c_2]) ).
cnf(c_273,plain,
( ssPv4(skf3(A))
| ~ ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv4(B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_29,c_1]) ).
cnf(c_283,plain,
( ssPv3(skf3(A))
| ~ ssPv3(A)
| ~ ssPv1(A)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_31,c_1]) ).
cnf(c_288,plain,
( ssPv1(B)
| ~ ssPv3(A)
| ~ ssPv1(A)
| ~ ssRr(A,B)
| ~ ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_32,c_2]) ).
cnf(c_306,plain,
( ssPv4(skf2(B))
| ssPv2(C)
| ssPv3(A)
| ~ ssPv1(B)
| ~ ssRr(C,B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_35,c_2]) ).
cnf(c_310,plain,
( ssPv4(skf2(B))
| ssPv2(A)
| ssPv3(A)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_306]) ).
cnf(c_326,plain,
( ssPv2(B)
| ssPv4(skf2(B))
| ssPv4(C)
| ~ ssRr(C,B)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_37,c_2]) ).
cnf(c_334,plain,
( ssPv2(B)
| ssPv4(skf2(B))
| ssPv4(A)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_326]) ).
cnf(c_341,plain,
( ssPv2(A)
| ssPv4(C)
| ssPv4(skf3(A))
| ~ ssRr(A,C)
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_38,c_1]) ).
cnf(c_348,plain,
( ssPv2(A)
| ssPv4(B)
| ssPv4(skf3(A))
| ~ ssPv1(B)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_341]) ).
cnf(c_376,plain,
( ssPv3(B)
| ssPv4(C)
| ~ ssPv2(skf2(B))
| ~ ssRr(C,B)
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_40,c_2]) ).
cnf(c_380,plain,
( ssPv3(B)
| ssPv4(A)
| ~ ssPv2(skf2(B))
| ~ ssPv3(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_376]) ).
cnf(c_400,plain,
( ssPv2(B)
| ssPv4(C)
| ~ ssPv4(skf2(B))
| ~ ssRr(C,B)
| ~ ssPv1(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_42,c_2]) ).
cnf(c_402,plain,
( ssPv2(B)
| ssPv4(A)
| ~ ssPv4(skf2(B))
| ~ ssPv1(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_400]) ).
cnf(c_418,plain,
( ssPv3(C)
| ~ ssPv2(B)
| ~ ssPv1(skf2(B))
| ~ ssRr(C,B)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_44,c_2]) ).
cnf(c_422,plain,
( ssPv3(A)
| ~ ssPv2(B)
| ~ ssPv1(skf2(B))
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_418]) ).
cnf(c_429,plain,
( ssPv1(C)
| ~ ssPv2(A)
| ~ ssRr(A,C)
| ~ ssPv3(B)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_45,c_1]) ).
cnf(c_435,plain,
( ssPv1(B)
| ~ ssPv2(A)
| ~ ssPv3(B)
| ~ ssRr(A,B)
| ~ ssPv2(skf3(A)) ),
inference(factor,[status(thm)],[c_429]) ).
cnf(c_474,plain,
( ssPv3(skf2(B))
| ~ ssPv4(B)
| ~ ssPv2(C)
| ~ ssRr(C,B)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_48,c_2]) ).
cnf(c_480,plain,
( ssPv3(skf2(B))
| ~ ssPv4(B)
| ~ ssPv2(A)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_474]) ).
cnf(c_506,plain,
( ssPv1(B)
| ~ ssPv3(skf2(B))
| ~ ssPv3(C)
| ~ ssRr(C,B)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_50,c_2]) ).
cnf(c_514,plain,
( ssPv1(B)
| ~ ssPv3(skf2(B))
| ~ ssPv3(A)
| ~ ssPv4(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_506]) ).
cnf(c_540,plain,
( ~ ssPv1(B)
| ~ ssPv1(skf2(B))
| ~ ssPv1(C)
| ~ ssRr(C,B)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(resolve,[status(thm)],[c_52,c_2]) ).
cnf(c_548,plain,
( ~ ssPv1(B)
| ~ ssPv1(skf2(B))
| ~ ssPv1(A)
| ~ ssPv2(A)
| ~ ssRr(A,B) ),
inference(factor,[status(thm)],[c_540]) ).
cnf(c_554,plain,
( ssPv4(skf2(A))
| ssPv1(A)
| ssPv4(A)
| ~ ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_57,c_2]) ).
cnf(c_555,plain,
( ssPv4(A)
| ssPv1(skf3(A))
| ssPv4(skf3(A))
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_57,c_1]) ).
cnf(c_556,plain,
( ssPv4(skf2(A))
| ssPv3(skf2(A))
| ssPv3(A)
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_59,c_2]) ).
cnf(c_557,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf3(A))
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_59,c_1]) ).
cnf(c_558,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv2(skf2(A))
| ~ ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_61,c_2]) ).
cnf(c_559,plain,
( ssPv4(skf3(A))
| ssPv3(skf3(A))
| ssPv2(A)
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_61,c_1]) ).
cnf(c_560,plain,
( ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv4(A)
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_65,c_2]) ).
cnf(c_561,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv4(skf3(A))
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_65,c_1]) ).
cnf(c_563,plain,
( ssPv3(A)
| ssPv4(A)
| ~ ssPv4(skf3(A))
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_68,c_1]) ).
cnf(c_564,plain,
( ssPv2(A)
| ssPv3(A)
| ~ ssPv2(skf2(A))
| ~ ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_69,c_2]) ).
cnf(c_565,plain,
( ssPv2(skf3(A))
| ssPv3(skf3(A))
| ~ ssPv2(A)
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_69,c_1]) ).
cnf(c_566,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ~ ssPv1(A)
| ~ ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_70,c_2]) ).
cnf(c_567,plain,
( ssPv3(skf3(A))
| ssPv1(A)
| ~ ssPv1(skf3(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_70,c_1]) ).
cnf(c_568,plain,
( ssPv2(A)
| ssPv1(A)
| ~ ssPv2(skf2(A))
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_76,c_2]) ).
cnf(c_569,plain,
( ssPv2(skf3(A))
| ssPv1(skf3(A))
| ~ ssPv2(A)
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_76,c_1]) ).
cnf(c_571,plain,
( ssPv4(A)
| ~ ssPv3(skf3(A))
| ~ ssPv2(skf3(A))
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_78,c_1]) ).
cnf(c_572,plain,
( ssPv1(skf2(A))
| ~ ssPv3(A)
| ~ ssPv1(A)
| ~ ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_80,c_2]) ).
cnf(c_573,plain,
( ssPv1(A)
| ~ ssPv3(skf3(A))
| ~ ssPv1(skf3(A))
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_80,c_1]) ).
cnf(c_575,plain,
( ssPv1(A)
| ~ ssPv2(skf3(A))
| ~ ssPv1(skf3(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_81,c_1]) ).
cnf(c_576,plain,
( ~ ssPv4(A)
| ~ ssPv1(A)
| ~ ssPv1(skf2(A))
| ~ ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_82,c_2]) ).
cnf(c_634,plain,
( ssPv2(skf2(A))
| ~ ssPv1(A)
| ~ ssPv3(A)
| ~ ssPv4(A) ),
inference(resolve,[status(thm)],[c_146,c_2]) ).
cnf(c_635,plain,
( ssPv2(A)
| ~ ssPv1(skf3(A))
| ~ ssPv3(skf3(A))
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_146,c_1]) ).
cnf(c_5315,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv3(A)
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_163,c_156]) ).
cnf(c_5316,plain,
( ssPv3(A)
| ssPv3(skf2(A))
| ssPv3(A)
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5315]) ).
cnf(c_639,plain,
( ssPv3(skf2(A))
| ssPv3(A)
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5316]) ).
cnf(c_647,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv2(skf2(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_167,c_2]) ).
cnf(c_651,plain,
( ~ ssPv1(A)
| ~ ssPv1(skf2(A))
| ~ ssPv1(skf3(A))
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_548,c_1]) ).
cnf(c_5317,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A))
| ssPv3(skf2(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_556,c_156]) ).
cnf(c_5318,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv4(skf2(A))
| ssPv3(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5317]) ).
cnf(c_668,plain,
( ssPv1(A)
| ssPv4(skf2(A))
| ssPv3(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5318]) ).
cnf(c_5319,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_560,c_156]) ).
cnf(c_683,plain,
( ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_5319]) ).
cnf(c_5320,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv1(A)
| ~ ssPv2(skf3(A))
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_575,c_156]) ).
cnf(c_705,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv1(A)
| ~ ssPv2(skf3(A))
| ~ ssPv1(skf3(A)) ),
inference(copy,[status(thm)],[c_5320]) ).
cnf(c_707,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv2(skf2(A))
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_189,c_2]) ).
cnf(c_5321,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv2(A)
| ssPv1(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_647,c_159]) ).
cnf(c_733,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv1(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5321]) ).
cnf(c_5322,plain,
( ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv2(A)
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_647,c_160]) ).
cnf(c_738,plain,
( ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5322]) ).
cnf(c_5323,plain,
( ssPv2(A)
| ssPv1(A)
| ~ ssPv2(skf2(A))
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_668,c_568]) ).
cnf(c_758,plain,
( ssPv2(A)
| ~ ssPv2(skf2(A))
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5323]) ).
cnf(c_796,plain,
( ssPv1(A)
| ssPv2(skf2(A))
| ssPv4(skf3(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_195,c_2]) ).
cnf(c_845,plain,
( ssPv1(A)
| ssPv4(skf2(A))
| ssPv1(skf3(A))
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_199,c_2]) ).
cnf(c_855,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv2(skf2(A))
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_217,c_2]) ).
cnf(c_856,plain,
( ssPv3(skf3(A))
| ssPv1(skf3(A))
| ssPv2(A)
| ~ ssPv2(skf3(skf3(A))) ),
inference(resolve,[status(thm)],[c_217,c_1]) ).
cnf(c_5324,plain,
( ssPv3(skf2(A))
| ssPv3(A)
| ssPv1(A)
| ssPv3(A)
| ssPv1(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_855,c_639]) ).
cnf(c_5325,plain,
( ssPv3(skf2(A))
| ssPv3(A)
| ssPv3(A)
| ssPv1(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5324]) ).
cnf(c_859,plain,
( ssPv3(skf2(A))
| ssPv3(A)
| ssPv1(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5325]) ).
cnf(c_897,plain,
( ssPv2(skf2(A))
| ssPv4(skf3(A))
| ~ ssPv3(A)
| ~ ssPv2(A) ),
inference(resolve,[status(thm)],[c_221,c_2]) ).
cnf(c_910,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ~ ssPv4(A)
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_233,c_2]) ).
cnf(c_929,plain,
( ssPv2(A)
| ssPv2(skf3(A))
| ~ ssPv3(A)
| ~ ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_247,c_2]) ).
cnf(c_941,plain,
( ssPv2(A)
| ssPv2(skf3(A))
| ~ ssPv1(A)
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_253,c_2]) ).
cnf(c_947,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ~ ssPv2(A)
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_263,c_2]) ).
cnf(c_952,plain,
( ssPv1(skf2(A))
| ssPv1(A)
| ~ ssPv2(skf2(A))
| ~ ssPv4(skf2(skf2(A))) ),
inference(resolve,[status(thm)],[c_264,c_2]) ).
cnf(c_955,plain,
( ssPv4(skf3(A))
| ~ ssPv4(A)
| ~ ssPv3(A)
| ~ ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_273,c_2]) ).
cnf(c_967,plain,
( ssPv3(skf3(A))
| ~ ssPv3(A)
| ~ ssPv1(A)
| ~ ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_283,c_2]) ).
cnf(c_978,plain,
( ssPv1(A)
| ~ ssPv3(skf3(A))
| ~ ssPv1(skf3(A))
| ~ ssPv2(skf2(skf3(A))) ),
inference(resolve,[status(thm)],[c_288,c_1]) ).
cnf(c_983,plain,
( ssPv4(skf2(A))
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ~ ssPv1(A) ),
inference(resolve,[status(thm)],[c_310,c_1]) ).
cnf(c_992,plain,
( ssPv2(A)
| ssPv4(skf2(A))
| ssPv4(skf3(A))
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_334,c_1]) ).
cnf(c_995,plain,
( ssPv2(A)
| ssPv4(skf2(A))
| ssPv4(skf3(A))
| ~ ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_348,c_2]) ).
cnf(c_1012,plain,
( ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv2(skf2(A))
| ~ ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_380,c_1]) ).
cnf(c_1034,plain,
( ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv4(skf2(A))
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_402,c_1]) ).
cnf(c_1040,plain,
( ssPv3(skf3(A))
| ~ ssPv2(A)
| ~ ssPv1(skf2(A))
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_422,c_1]) ).
cnf(c_1044,plain,
( ssPv1(skf2(A))
| ~ ssPv2(A)
| ~ ssPv3(skf2(A))
| ~ ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_435,c_2]) ).
cnf(c_1045,plain,
( ssPv1(A)
| ~ ssPv2(skf3(A))
| ~ ssPv3(A)
| ~ ssPv2(skf3(skf3(A))) ),
inference(resolve,[status(thm)],[c_435,c_1]) ).
cnf(c_1063,plain,
( ssPv3(skf2(A))
| ~ ssPv4(A)
| ~ ssPv2(skf3(A))
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_480,c_1]) ).
cnf(c_1074,plain,
( ssPv1(A)
| ~ ssPv3(skf2(A))
| ~ ssPv3(skf3(A))
| ~ ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_514,c_1]) ).
cnf(c_5326,plain,
( ssPv3(skf2(A))
| ssPv3(A)
| ssPv1(A)
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_758,c_859]) ).
cnf(c_5327,plain,
( ssPv3(skf2(A))
| ssPv3(A)
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5326]) ).
cnf(c_5328,plain,
( ssPv3(skf2(A))
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5327]) ).
cnf(c_1170,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5328]) ).
cnf(c_5329,plain,
( ssPv4(skf2(A))
| ssPv1(A)
| ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_683,c_554]) ).
cnf(c_5330,plain,
( ssPv4(skf2(A))
| ssPv1(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_5329]) ).
cnf(c_5331,plain,
( ssPv4(skf2(A))
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_5330]) ).
cnf(c_1424,plain,
( ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_5331]) ).
cnf(c_5332,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ~ ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_1424,c_947]) ).
cnf(c_1453,plain,
( ssPv1(skf3(A))
| ~ ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_5332]) ).
cnf(c_5333,plain,
( ssPv2(A)
| ssPv1(A)
| ~ ssPv2(skf2(A))
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_1424,c_568]) ).
cnf(c_1458,plain,
( ssPv2(A)
| ~ ssPv2(skf2(A))
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_5333]) ).
cnf(c_5334,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv1(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_733,c_855]) ).
cnf(c_5335,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv1(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5334]) ).
cnf(c_1581,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv1(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5335]) ).
cnf(c_5336,plain,
( ssPv2(A)
| ssPv3(A)
| ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_1581,c_564]) ).
cnf(c_5337,plain,
( ssPv2(A)
| ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5336]) ).
cnf(c_1599,plain,
( ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5337]) ).
cnf(c_5338,plain,
( ssPv2(A)
| ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_738,c_995]) ).
cnf(c_5339,plain,
( ssPv2(A)
| ssPv4(skf2(A))
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5338]) ).
cnf(c_5340,plain,
( ssPv2(A)
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5339]) ).
cnf(c_1655,plain,
( ssPv4(skf2(A))
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5340]) ).
cnf(c_5341,plain,
( ssPv1(A)
| ssPv4(skf2(A))
| ssPv1(skf3(A))
| ssPv4(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1655,c_845]) ).
cnf(c_5342,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ssPv4(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5341]) ).
cnf(c_1687,plain,
( ssPv1(skf3(A))
| ssPv4(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5342]) ).
cnf(c_5343,plain,
( ssPv2(A)
| ssPv1(A)
| ~ ssPv2(skf2(A))
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1655,c_568]) ).
cnf(c_5344,plain,
( ssPv2(A)
| ~ ssPv2(skf2(A))
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5343]) ).
cnf(c_1697,plain,
( ~ ssPv2(skf2(A))
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5344]) ).
cnf(c_5345,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A))
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1697,c_647]) ).
cnf(c_5346,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5345]) ).
cnf(c_5347,plain,
( ssPv2(A)
| ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5346]) ).
cnf(c_1755,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5347]) ).
cnf(c_1757,plain,
( ssPv3(skf2(A))
| ~ ssPv4(A)
| ~ ssPv2(skf3(A))
| ssPv2(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_1755,c_1063]) ).
cnf(c_5348,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv2(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_1755,c_159]) ).
cnf(c_1766,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5348]) ).
cnf(c_5349,plain,
( ssPv4(skf3(A))
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1755,c_559]) ).
cnf(c_5350,plain,
( ssPv4(skf3(A))
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5349]) ).
cnf(c_1770,plain,
( ssPv3(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5350]) ).
cnf(c_5351,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1755,c_161]) ).
cnf(c_1781,plain,
( ssPv4(A)
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5351]) ).
cnf(c_5352,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1770,c_557]) ).
cnf(c_1792,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5352]) ).
cnf(c_5353,plain,
( ssPv3(A)
| ssPv4(skf3(A))
| ~ ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1770,c_1012]) ).
cnf(c_1811,plain,
( ssPv3(A)
| ~ ssPv2(skf2(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5353]) ).
cnf(c_5354,plain,
( ssPv4(A)
| ~ ssPv2(skf3(A))
| ~ ssPv1(A)
| ssPv4(A)
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1792,c_571]) ).
cnf(c_1839,plain,
( ~ ssPv2(skf3(A))
| ~ ssPv1(A)
| ssPv4(A)
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5354]) ).
cnf(c_5355,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1792,c_158]) ).
cnf(c_5356,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5355]) ).
cnf(c_1868,plain,
( ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5356]) ).
cnf(c_5357,plain,
( ssPv4(skf2(A))
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1766,c_983]) ).
cnf(c_5358,plain,
( ssPv4(skf2(A))
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5357]) ).
cnf(c_1873,plain,
( ssPv4(skf2(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5358]) ).
cnf(c_5359,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_1766,c_161]) ).
cnf(c_5360,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5359]) ).
cnf(c_1886,plain,
( ssPv4(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5360]) ).
cnf(c_5361,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1781,c_163]) ).
cnf(c_5362,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5361]) ).
cnf(c_1947,plain,
( ssPv3(A)
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5362]) ).
cnf(c_5363,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv1(A)
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1868,c_1599]) ).
cnf(c_5364,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5363]) ).
cnf(c_5365,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5364]) ).
cnf(c_1991,plain,
( ssPv1(A)
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5365]) ).
cnf(c_5366,plain,
( ssPv1(A)
| ~ ssPv3(skf2(A))
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1991,c_1074]) ).
cnf(c_2001,plain,
( ~ ssPv3(skf2(A))
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5366]) ).
cnf(c_5367,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_1886,c_163]) ).
cnf(c_5368,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5367]) ).
cnf(c_2051,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5368]) ).
cnf(c_5369,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv2(skf2(A))
| ssPv3(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1947,c_855]) ).
cnf(c_5370,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ssPv3(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5369]) ).
cnf(c_2062,plain,
( ssPv2(skf2(A))
| ssPv3(A)
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5370]) ).
cnf(c_5371,plain,
( ssPv3(skf3(A))
| ssPv1(A)
| ~ ssPv1(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2051,c_567]) ).
cnf(c_5372,plain,
( ssPv3(skf3(A))
| ~ ssPv1(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5371]) ).
cnf(c_2107,plain,
( ~ ssPv1(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5372]) ).
cnf(c_5373,plain,
( ssPv1(A)
| ssPv2(skf2(A))
| ssPv4(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_2062,c_796]) ).
cnf(c_5374,plain,
( ssPv1(A)
| ssPv2(skf2(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5373]) ).
cnf(c_5375,plain,
( ssPv1(A)
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5374]) ).
cnf(c_2123,plain,
( ssPv2(skf2(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5375]) ).
cnf(c_5376,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_1687,c_947]) ).
cnf(c_5377,plain,
( ssPv1(A)
| ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5376]) ).
cnf(c_2216,plain,
( ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5377]) ).
cnf(c_5378,plain,
( ssPv1(A)
| ssPv4(skf3(A))
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_2216,c_1755]) ).
cnf(c_5379,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5378]) ).
cnf(c_2227,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5379]) ).
cnf(c_5380,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv1(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2227,c_159]) ).
cnf(c_2233,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5380]) ).
cnf(c_5381,plain,
( ssPv4(A)
| ssPv1(skf3(A))
| ssPv4(skf3(A))
| ssPv1(skf3(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_2227,c_555]) ).
cnf(c_5382,plain,
( ssPv4(A)
| ssPv1(skf3(A))
| ssPv1(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5381]) ).
cnf(c_2237,plain,
( ssPv4(A)
| ssPv1(skf3(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5382]) ).
cnf(c_5383,plain,
( ssPv2(A)
| ssPv2(skf3(A))
| ~ ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_1873,c_941]) ).
cnf(c_5384,plain,
( ssPv2(A)
| ~ ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5383]) ).
cnf(c_2295,plain,
( ~ ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5384]) ).
cnf(c_5385,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2295,c_1766]) ).
cnf(c_5386,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5385]) ).
cnf(c_5387,plain,
( ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5386]) ).
cnf(c_2312,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5387]) ).
cnf(c_5388,plain,
( ssPv2(skf3(A))
| ssPv3(skf3(A))
| ~ ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_2312,c_565]) ).
cnf(c_5389,plain,
( ssPv2(skf3(A))
| ~ ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5388]) ).
cnf(c_2332,plain,
( ~ ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5389]) ).
cnf(c_5390,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2312,c_707]) ).
cnf(c_2334,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5390]) ).
cnf(c_5391,plain,
( ssPv2(A)
| ~ ssPv1(skf3(A))
| ~ ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2312,c_635]) ).
cnf(c_2344,plain,
( ~ ssPv1(skf3(A))
| ~ ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5391]) ).
cnf(c_5392,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_2332,c_2051]) ).
cnf(c_5393,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5392]) ).
cnf(c_2350,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5393]) ).
cnf(c_5394,plain,
( ssPv3(skf3(A))
| ~ ssPv2(A)
| ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_2350,c_1040]) ).
cnf(c_2354,plain,
( ~ ssPv2(A)
| ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_5394]) ).
cnf(c_5395,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ~ ssPv4(A)
| ssPv3(A)
| ssPv2(skf2(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2334,c_910]) ).
cnf(c_5396,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ssPv3(A)
| ssPv2(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5395]) ).
cnf(c_2407,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv2(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5396]) ).
cnf(c_5397,plain,
( ssPv2(A)
| ssPv3(A)
| ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2334,c_564]) ).
cnf(c_5398,plain,
( ssPv2(A)
| ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5397]) ).
cnf(c_2414,plain,
( ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5398]) ).
cnf(c_5399,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2414,c_1868]) ).
cnf(c_5400,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5399]) ).
cnf(c_5401,plain,
( ssPv3(A)
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5400]) ).
cnf(c_2448,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5401]) ).
cnf(c_5402,plain,
( ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_2448,c_2354]) ).
cnf(c_5403,plain,
( ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(A)
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_5402]) ).
cnf(c_2449,plain,
( ~ ssPv1(skf2(A))
| ssPv3(A)
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_5403]) ).
cnf(c_5404,plain,
( ssPv3(skf3(A))
| ~ ssPv1(A)
| ~ ssPv1(skf2(A))
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2448,c_967]) ).
cnf(c_2469,plain,
( ~ ssPv1(A)
| ~ ssPv1(skf2(A))
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5404]) ).
cnf(c_5405,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2233,c_2107]) ).
cnf(c_5406,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5405]) ).
cnf(c_5407,plain,
( ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5406]) ).
cnf(c_2569,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5407]) ).
cnf(c_5408,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_2569,c_2332]) ).
cnf(c_5409,plain,
( ssPv3(skf3(A))
| ssPv3(skf3(A))
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5408]) ).
cnf(c_2578,plain,
( ssPv3(skf3(A))
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5409]) ).
cnf(c_5410,plain,
( ssPv1(A)
| ~ ssPv3(skf2(A))
| ~ ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2569,c_1074]) ).
cnf(c_2582,plain,
( ~ ssPv3(skf2(A))
| ~ ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5410]) ).
cnf(c_5411,plain,
( ssPv1(A)
| ~ ssPv1(skf3(A))
| ~ ssPv2(A)
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2569,c_573]) ).
cnf(c_2586,plain,
( ~ ssPv1(skf3(A))
| ~ ssPv2(A)
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5411]) ).
cnf(c_5412,plain,
( ssPv3(skf3(A))
| ~ ssPv2(A)
| ~ ssPv1(skf2(A))
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_2578,c_1040]) ).
cnf(c_2589,plain,
( ~ ssPv2(A)
| ~ ssPv1(skf2(A))
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_5412]) ).
cnf(c_5413,plain,
( ssPv1(A)
| ssPv4(skf3(A))
| ~ ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2586,c_1755]) ).
cnf(c_2630,plain,
( ssPv4(skf3(A))
| ~ ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5413]) ).
cnf(c_5414,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ~ ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2582,c_639]) ).
cnf(c_5415,plain,
( ssPv3(A)
| ssPv1(A)
| ~ ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5414]) ).
cnf(c_2661,plain,
( ssPv3(A)
| ~ ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5415]) ).
cnf(c_5416,plain,
( ssPv3(A)
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2661,c_1947]) ).
cnf(c_5417,plain,
( ssPv3(A)
| ssPv2(skf3(A))
| ssPv3(A)
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5416]) ).
cnf(c_5418,plain,
( ssPv3(A)
| ssPv3(A)
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5417]) ).
cnf(c_2671,plain,
( ssPv3(A)
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5418]) ).
cnf(c_5419,plain,
( ssPv3(A)
| ssPv1(A)
| ssPv2(skf2(A))
| ssPv3(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2671,c_855]) ).
cnf(c_5420,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ssPv3(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5419]) ).
cnf(c_2685,plain,
( ssPv2(skf2(A))
| ssPv3(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5420]) ).
cnf(c_5421,plain,
( ssPv1(A)
| ~ ssPv2(skf3(A))
| ~ ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2685,c_575]) ).
cnf(c_2713,plain,
( ~ ssPv2(skf3(A))
| ~ ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5421]) ).
cnf(c_5422,plain,
( ssPv1(A)
| ssPv4(skf3(A))
| ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_2630,c_2227]) ).
cnf(c_5423,plain,
( ssPv1(A)
| ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5422]) ).
cnf(c_2741,plain,
( ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5423]) ).
cnf(c_5424,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(A)
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2001,c_1170]) ).
cnf(c_5425,plain,
( ssPv2(A)
| ssPv1(A)
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5424]) ).
cnf(c_5426,plain,
( ssPv2(A)
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5425]) ).
cnf(c_2768,plain,
( ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5426]) ).
cnf(c_5427,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv1(A)
| ssPv3(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2768,c_1755]) ).
cnf(c_5428,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5427]) ).
cnf(c_2777,plain,
( ssPv1(A)
| ssPv3(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5428]) ).
cnf(c_5429,plain,
( ssPv1(A)
| ssPv4(skf2(A))
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_2777,c_845]) ).
cnf(c_2782,plain,
( ssPv4(skf2(A))
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5429]) ).
cnf(c_5430,plain,
( ssPv1(A)
| ~ ssPv2(skf3(A))
| ~ ssPv1(skf3(A))
| ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2777,c_575]) ).
cnf(c_2787,plain,
( ~ ssPv2(skf3(A))
| ~ ssPv1(skf3(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5430]) ).
cnf(c_5431,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ~ ssPv1(A)
| ssPv1(skf2(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_2777,c_566]) ).
cnf(c_2789,plain,
( ssPv3(A)
| ~ ssPv1(A)
| ssPv1(skf2(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5431]) ).
cnf(c_5432,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_2782,c_947]) ).
cnf(c_5433,plain,
( ssPv1(A)
| ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5432]) ).
cnf(c_2814,plain,
( ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5433]) ).
cnf(c_5434,plain,
( ssPv1(A)
| ssPv3(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_2814,c_2777]) ).
cnf(c_5435,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5434]) ).
cnf(c_2818,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5435]) ).
cnf(c_5436,plain,
( ssPv2(skf2(A))
| ssPv3(A)
| ssPv3(A)
| ssPv1(skf2(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_2789,c_2685]) ).
cnf(c_5437,plain,
( ssPv2(skf2(A))
| ssPv3(A)
| ssPv1(skf2(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5436]) ).
cnf(c_2847,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5437]) ).
cnf(c_5438,plain,
( ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv2(A)
| ssPv3(A)
| ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_2847,c_160]) ).
cnf(c_2857,plain,
( ssPv4(skf2(A))
| ssPv2(A)
| ssPv3(A)
| ssPv1(skf2(A)) ),
inference(copy,[status(thm)],[c_5438]) ).
cnf(c_5439,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_2847,c_2449]) ).
cnf(c_2859,plain,
( ssPv3(skf3(A))
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5439]) ).
cnf(c_5440,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv2(skf2(A))
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_2847,c_558]) ).
cnf(c_5441,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5440]) ).
cnf(c_2861,plain,
( ssPv4(A)
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5441]) ).
cnf(c_5442,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ssPv2(A)
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_2861,c_2407]) ).
cnf(c_5443,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5442]) ).
cnf(c_2895,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5443]) ).
cnf(c_5444,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(skf3(A))
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_2895,c_1811]) ).
cnf(c_5445,plain,
( ssPv3(A)
| ssPv4(skf3(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5444]) ).
cnf(c_2913,plain,
( ssPv4(skf3(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5445]) ).
cnf(c_5446,plain,
( ssPv2(A)
| ssPv3(A)
| ~ ssPv1(skf2(A))
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_2895,c_564]) ).
cnf(c_5447,plain,
( ssPv2(A)
| ~ ssPv1(skf2(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5446]) ).
cnf(c_2916,plain,
( ~ ssPv1(skf2(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5447]) ).
cnf(c_5448,plain,
( ssPv4(skf3(A))
| ~ ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_2913,c_955]) ).
cnf(c_2931,plain,
( ~ ssPv4(A)
| ~ ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5448]) ).
cnf(c_5449,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ~ ssPv4(A)
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_2859,c_910]) ).
cnf(c_5450,plain,
( ssPv3(A)
| ~ ssPv4(A)
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5449]) ).
cnf(c_2978,plain,
( ~ ssPv4(A)
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5450]) ).
cnf(c_5451,plain,
( ssPv3(A)
| ssPv2(skf2(A))
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_2978,c_2861]) ).
cnf(c_5452,plain,
( ssPv3(A)
| ssPv3(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5451]) ).
cnf(c_2986,plain,
( ssPv3(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5452]) ).
cnf(c_5453,plain,
( ssPv2(skf2(A))
| ssPv4(skf3(A))
| ~ ssPv2(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_2986,c_897]) ).
cnf(c_2999,plain,
( ssPv4(skf3(A))
| ~ ssPv2(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5453]) ).
cnf(c_5454,plain,
( ssPv2(skf2(A))
| ~ ssPv1(A)
| ~ ssPv4(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_2986,c_634]) ).
cnf(c_3001,plain,
( ~ ssPv1(A)
| ~ ssPv4(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5454]) ).
cnf(c_5455,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_2857,c_2916]) ).
cnf(c_5456,plain,
( ssPv2(A)
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5455]) ).
cnf(c_3084,plain,
( ssPv4(skf2(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5456]) ).
cnf(c_5457,plain,
( ssPv4(skf2(A))
| ssPv1(skf2(A))
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_2857,c_560]) ).
cnf(c_5458,plain,
( ssPv4(skf2(A))
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv1(skf2(A)) ),
inference(copy,[status(thm)],[c_5457]) ).
cnf(c_3087,plain,
( ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv1(skf2(A)) ),
inference(copy,[status(thm)],[c_5458]) ).
cnf(c_5459,plain,
( ssPv2(A)
| ssPv2(skf3(A))
| ~ ssPv1(A)
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3084,c_941]) ).
cnf(c_3100,plain,
( ssPv2(skf3(A))
| ~ ssPv1(A)
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5459]) ).
cnf(c_5460,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3100,c_2777]) ).
cnf(c_5461,plain,
( ssPv3(A)
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5460]) ).
cnf(c_3103,plain,
( ssPv2(skf3(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5461]) ).
cnf(c_5462,plain,
( ssPv2(A)
| ssPv2(skf3(A))
| ~ ssPv2(skf2(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3103,c_929]) ).
cnf(c_5463,plain,
( ssPv2(A)
| ~ ssPv2(skf2(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5462]) ).
cnf(c_3106,plain,
( ~ ssPv2(skf2(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5463]) ).
cnf(c_5464,plain,
( ~ ssPv1(A)
| ssPv4(A)
| ssPv3(A)
| ssPv2(A)
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3103,c_1839]) ).
cnf(c_5465,plain,
( ~ ssPv1(A)
| ssPv4(A)
| ssPv3(A)
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5464]) ).
cnf(c_3113,plain,
( ~ ssPv1(A)
| ssPv4(A)
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5465]) ).
cnf(c_5466,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv4(A)
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3113,c_2777]) ).
cnf(c_5467,plain,
( ssPv3(A)
| ssPv4(A)
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5466]) ).
cnf(c_3117,plain,
( ssPv4(A)
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5467]) ).
cnf(c_5468,plain,
( ssPv3(A)
| ssPv2(A)
| ssPv1(skf2(A))
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3117,c_158]) ).
cnf(c_5469,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5468]) ).
cnf(c_3127,plain,
( ssPv1(skf2(A))
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5469]) ).
cnf(c_5470,plain,
( ssPv1(skf2(A))
| ~ ssPv1(A)
| ~ ssPv2(skf2(A))
| ssPv1(skf2(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3127,c_572]) ).
cnf(c_3130,plain,
( ~ ssPv1(A)
| ~ ssPv2(skf2(A))
| ssPv1(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5470]) ).
cnf(c_5471,plain,
( ssPv2(A)
| ssPv3(A)
| ssPv2(A)
| ssPv3(A) ),
inference(resolve,[status(thm)],[c_3127,c_2916]) ).
cnf(c_5472,plain,
( ssPv2(A)
| ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5471]) ).
cnf(c_3132,plain,
( ssPv2(A)
| ssPv3(A) ),
inference(copy,[status(thm)],[c_5472]) ).
cnf(c_5473,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_3132,c_1458]) ).
cnf(c_3135,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5473]) ).
cnf(c_3145,plain,
( ssPv3(skf2(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3106,c_3132]) ).
cnf(c_5474,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv3(skf2(A))
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_3145,c_161]) ).
cnf(c_3164,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5474]) ).
cnf(c_5475,plain,
( ~ ssPv4(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3145,c_2582]) ).
cnf(c_3181,plain,
( ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5475]) ).
cnf(c_5476,plain,
( ssPv3(skf2(A))
| ~ ssPv2(skf3(A))
| ssPv2(A)
| ssPv1(A)
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_3135,c_1757]) ).
cnf(c_5477,plain,
( ssPv3(skf2(A))
| ~ ssPv2(skf3(A))
| ssPv2(A)
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5476]) ).
cnf(c_5478,plain,
( ssPv3(skf2(A))
| ~ ssPv2(skf3(A))
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5477]) ).
cnf(c_3193,plain,
( ~ ssPv2(skf3(A))
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5478]) ).
cnf(c_5479,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv4(A)
| ssPv1(A)
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_3135,c_1453]) ).
cnf(c_5480,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv3(skf2(A))
| ssPv1(A)
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5479]) ).
cnf(c_5481,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv1(A)
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5480]) ).
cnf(c_3204,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5481]) ).
cnf(c_5482,plain,
( ssPv2(A)
| ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3087,c_995]) ).
cnf(c_5483,plain,
( ssPv2(A)
| ssPv4(skf3(A))
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5482]) ).
cnf(c_3219,plain,
( ssPv4(skf3(A))
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5483]) ).
cnf(c_5484,plain,
( ssPv4(skf2(A))
| ssPv1(A)
| ssPv4(A)
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3087,c_554]) ).
cnf(c_5485,plain,
( ssPv4(skf2(A))
| ssPv1(A)
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5484]) ).
cnf(c_3220,plain,
( ssPv1(A)
| ssPv4(A)
| ssPv4(skf2(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5485]) ).
cnf(c_5486,plain,
( ssPv1(A)
| ssPv4(skf2(A))
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(A)
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_3220,c_845]) ).
cnf(c_5487,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(A)
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_5486]) ).
cnf(c_3247,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(A)
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_5487]) ).
cnf(c_5488,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ssPv1(A)
| ~ ssPv1(skf3(A))
| ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_3164,c_705]) ).
cnf(c_5489,plain,
( ssPv4(A)
| ssPv3(skf2(A))
| ~ ssPv1(skf3(A))
| ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5488]) ).
cnf(c_5490,plain,
( ssPv4(A)
| ~ ssPv1(skf3(A))
| ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5489]) ).
cnf(c_3278,plain,
( ~ ssPv1(skf3(A))
| ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5490]) ).
cnf(c_5491,plain,
( ssPv2(skf3(A))
| ssPv1(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3181,c_2741]) ).
cnf(c_5492,plain,
( ssPv2(skf3(A))
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5491]) ).
cnf(c_3305,plain,
( ssPv1(A)
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5492]) ).
cnf(c_5493,plain,
( ~ ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_3305,c_2586]) ).
cnf(c_5494,plain,
( ~ ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5493]) ).
cnf(c_3309,plain,
( ~ ssPv1(skf3(A))
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5494]) ).
cnf(c_5495,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_3305,c_161]) ).
cnf(c_5496,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5495]) ).
cnf(c_3315,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5496]) ).
cnf(c_5497,plain,
( ~ ssPv1(skf3(A))
| ssPv1(A)
| ssPv2(A)
| ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3305,c_2787]) ).
cnf(c_5498,plain,
( ~ ssPv1(skf3(A))
| ssPv1(A)
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5497]) ).
cnf(c_3317,plain,
( ~ ssPv1(skf3(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5498]) ).
cnf(c_5499,plain,
( ssPv2(skf3(A))
| ssPv1(skf3(A))
| ~ ssPv2(A)
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_3315,c_569]) ).
cnf(c_3347,plain,
( ssPv1(skf3(A))
| ~ ssPv2(A)
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5499]) ).
cnf(c_5500,plain,
( ssPv1(A)
| ssPv2(A)
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_3193,c_3305]) ).
cnf(c_5501,plain,
( ssPv1(A)
| ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5500]) ).
cnf(c_3355,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5501]) ).
cnf(c_5502,plain,
( ssPv2(A)
| ssPv4(skf3(A))
| ~ ssPv1(skf3(A))
| ssPv4(skf3(A))
| ssPv4(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3219,c_1034]) ).
cnf(c_5503,plain,
( ssPv2(A)
| ~ ssPv1(skf3(A))
| ssPv4(skf3(A))
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5502]) ).
cnf(c_3404,plain,
( ~ ssPv1(skf3(A))
| ssPv4(skf3(A))
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5503]) ).
cnf(c_5504,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_3247,c_947]) ).
cnf(c_5505,plain,
( ssPv1(A)
| ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_5504]) ).
cnf(c_3448,plain,
( ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(A) ),
inference(copy,[status(thm)],[c_5505]) ).
cnf(c_5506,plain,
( ssPv1(A)
| ssPv4(A)
| ssPv3(skf2(A))
| ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(resolve,[status(thm)],[c_3278,c_3204]) ).
cnf(c_5507,plain,
( ssPv1(A)
| ssPv4(A)
| ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5506]) ).
cnf(c_5508,plain,
( ssPv1(A)
| ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5507]) ).
cnf(c_3491,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv3(skf2(A)) ),
inference(copy,[status(thm)],[c_5508]) ).
cnf(c_3493,plain,
( ssPv1(skf2(A))
| ~ ssPv2(A)
| ~ ssPv2(skf3(A))
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_3491,c_1044]) ).
cnf(c_5509,plain,
( ssPv1(A)
| ssPv2(skf3(A))
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_3347,c_3305]) ).
cnf(c_5510,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5509]) ).
cnf(c_3519,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5510]) ).
cnf(c_5511,plain,
( ssPv1(A)
| ssPv2(skf3(A))
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_3519,c_3309]) ).
cnf(c_5512,plain,
( ssPv1(A)
| ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5511]) ).
cnf(c_3530,plain,
( ssPv1(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5512]) ).
cnf(c_5513,plain,
( ~ ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_3530,c_2713]) ).
cnf(c_3534,plain,
( ~ ssPv1(skf3(A))
| ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5513]) ).
cnf(c_5514,plain,
( ssPv4(A)
| ssPv4(skf3(A))
| ssPv4(skf3(A))
| ssPv4(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3404,c_2237]) ).
cnf(c_5515,plain,
( ssPv4(A)
| ssPv4(skf3(A))
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5514]) ).
cnf(c_3552,plain,
( ssPv4(skf3(A))
| ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5515]) ).
cnf(c_5516,plain,
( ssPv4(skf3(A))
| ssPv2(skf2(A))
| ssPv4(skf3(A))
| ssPv4(A) ),
inference(resolve,[status(thm)],[c_3552,c_2999]) ).
cnf(c_3554,plain,
( ssPv2(skf2(A))
| ssPv4(skf3(A))
| ssPv4(A) ),
inference(copy,[status(thm)],[c_5516]) ).
cnf(c_5517,plain,
( ~ ssPv1(A)
| ssPv2(skf2(A))
| ssPv2(skf2(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3554,c_3001]) ).
cnf(c_3583,plain,
( ~ ssPv1(A)
| ssPv2(skf2(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5517]) ).
cnf(c_5518,plain,
( ssPv2(skf2(A))
| ssPv4(skf3(A))
| ssPv2(skf2(A))
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3583,c_2123]) ).
cnf(c_5519,plain,
( ssPv2(skf2(A))
| ssPv2(skf2(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5518]) ).
cnf(c_3606,plain,
( ssPv2(skf2(A))
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5519]) ).
cnf(c_3643,plain,
( ssPv2(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3606,c_3106]) ).
cnf(c_5520,plain,
( ~ ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A)
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_3643,c_2344]) ).
cnf(c_5521,plain,
( ~ ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5520]) ).
cnf(c_3657,plain,
( ~ ssPv1(skf3(A))
| ssPv2(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5521]) ).
cnf(c_5522,plain,
( ssPv2(A)
| ssPv4(skf2(A))
| ssPv4(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3643,c_992]) ).
cnf(c_5523,plain,
( ssPv2(A)
| ssPv4(skf2(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5522]) ).
cnf(c_3670,plain,
( ssPv4(skf2(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5523]) ).
cnf(c_5524,plain,
( ~ ssPv4(A)
| ssPv4(skf3(A))
| ssPv2(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3670,c_2931]) ).
cnf(c_5525,plain,
( ~ ssPv4(A)
| ssPv4(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5524]) ).
cnf(c_3691,plain,
( ~ ssPv4(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5525]) ).
cnf(c_5526,plain,
( ssPv4(skf3(A))
| ssPv2(A)
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(resolve,[status(thm)],[c_3691,c_3552]) ).
cnf(c_5527,plain,
( ssPv4(skf3(A))
| ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5526]) ).
cnf(c_3698,plain,
( ssPv2(A)
| ssPv4(skf3(A)) ),
inference(copy,[status(thm)],[c_5527]) ).
cnf(c_5528,plain,
( ssPv1(A)
| ssPv1(skf2(A))
| ~ ssPv2(A)
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_3493,c_3530]) ).
cnf(c_4105,plain,
( ssPv1(skf2(A))
| ~ ssPv2(A)
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5528]) ).
cnf(c_4113,plain,
( ssPv3(A)
| ssPv1(skf2(A))
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4105,c_3132]) ).
cnf(c_5529,plain,
( ssPv3(A)
| ssPv3(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4113,c_2449]) ).
cnf(c_4126,plain,
( ssPv3(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5529]) ).
cnf(c_5530,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv4(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4126,c_561]) ).
cnf(c_5531,plain,
( ssPv4(A)
| ssPv4(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5530]) ).
cnf(c_4211,plain,
( ssPv4(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5531]) ).
cnf(c_5532,plain,
( ssPv3(A)
| ssPv4(A)
| ~ ssPv1(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4211,c_563]) ).
cnf(c_5533,plain,
( ssPv3(A)
| ~ ssPv1(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5532]) ).
cnf(c_4243,plain,
( ~ ssPv1(skf3(A))
| ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5533]) ).
cnf(c_5534,plain,
( ssPv1(A)
| ssPv3(A)
| ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4243,c_2818]) ).
cnf(c_5535,plain,
( ssPv1(A)
| ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5534]) ).
cnf(c_4247,plain,
( ssPv3(A)
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5535]) ).
cnf(c_5536,plain,
( ssPv1(A)
| ~ ssPv2(skf3(A))
| ~ ssPv1(skf3(A))
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4247,c_575]) ).
cnf(c_4255,plain,
( ~ ssPv2(skf3(A))
| ~ ssPv1(skf3(A))
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5536]) ).
cnf(c_5537,plain,
( ssPv1(skf3(A))
| ssPv3(skf3(A))
| ssPv1(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_856,c_3530]) ).
cnf(c_4374,plain,
( ssPv3(skf3(A))
| ssPv1(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5537]) ).
cnf(c_5538,plain,
( ssPv1(A)
| ssPv2(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4374,c_3317]) ).
cnf(c_4394,plain,
( ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5538]) ).
cnf(c_5539,plain,
( ssPv1(A)
| ~ ssPv3(skf2(A))
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4394,c_1074]) ).
cnf(c_4415,plain,
( ~ ssPv3(skf2(A))
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5539]) ).
cnf(c_5540,plain,
( ssPv1(A)
| ~ ssPv1(skf3(A))
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4255,c_3530]) ).
cnf(c_4445,plain,
( ~ ssPv1(skf3(A))
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5540]) ).
cnf(c_5541,plain,
( ssPv2(A)
| ssPv1(A)
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4415,c_3355]) ).
cnf(c_5542,plain,
( ssPv2(A)
| ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5541]) ).
cnf(c_4694,plain,
( ~ ssPv4(skf3(A))
| ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5542]) ).
cnf(c_5543,plain,
( ssPv2(A)
| ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4694,c_3698]) ).
cnf(c_4700,plain,
( ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5543]) ).
cnf(c_5544,plain,
( ssPv1(skf3(A))
| ssPv1(A)
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4700,c_3448]) ).
cnf(c_4702,plain,
( ssPv1(skf3(A))
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5544]) ).
cnf(c_5545,plain,
( ~ ssPv1(A)
| ssPv1(skf2(A))
| ssPv2(A)
| ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_4700,c_3130]) ).
cnf(c_4703,plain,
( ~ ssPv1(A)
| ssPv2(A)
| ssPv1(skf2(A)) ),
inference(copy,[status(thm)],[c_5545]) ).
cnf(c_5546,plain,
( ssPv1(A)
| ssPv4(skf2(A))
| ssPv1(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4700,c_845]) ).
cnf(c_4707,plain,
( ssPv4(skf2(A))
| ssPv1(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5546]) ).
cnf(c_5547,plain,
( ssPv2(skf3(A))
| ssPv2(A)
| ssPv2(skf3(A)) ),
inference(resolve,[status(thm)],[c_4700,c_3657]) ).
cnf(c_4715,plain,
( ssPv2(A)
| ssPv2(skf3(A)) ),
inference(copy,[status(thm)],[c_5547]) ).
cnf(c_5548,plain,
( ssPv4(A)
| ssPv1(A)
| ssPv4(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4702,c_4445]) ).
cnf(c_5549,plain,
( ssPv4(A)
| ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5548]) ).
cnf(c_4753,plain,
( ssPv4(A)
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5549]) ).
cnf(c_5550,plain,
( ssPv2(A)
| ssPv2(A)
| ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_4703,c_4700]) ).
cnf(c_4770,plain,
( ssPv2(A)
| ssPv1(skf2(A)) ),
inference(copy,[status(thm)],[c_5550]) ).
cnf(c_5551,plain,
( ~ ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4770,c_2469]) ).
cnf(c_4771,plain,
( ~ ssPv1(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5551]) ).
cnf(c_5552,plain,
( ssPv2(A)
| ssPv3(skf3(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4771,c_4700]) ).
cnf(c_4801,plain,
( ssPv3(skf3(A))
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5552]) ).
cnf(c_5553,plain,
( ~ ssPv1(skf2(A))
| ssPv3(skf3(A))
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_4801,c_2589]) ).
cnf(c_4814,plain,
( ~ ssPv1(skf2(A))
| ssPv3(skf3(A)) ),
inference(copy,[status(thm)],[c_5553]) ).
cnf(c_4825,plain,
( ssPv4(A)
| ~ ssPv2(skf3(A))
| ~ ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4801,c_571]) ).
cnf(c_4827,plain,
( ssPv4(skf2(A))
| ssPv3(skf3(A)) ),
inference(resolve,[status(thm)],[c_4814,c_4753]) ).
cnf(c_5554,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4707,c_947]) ).
cnf(c_5555,plain,
( ssPv1(A)
| ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5554]) ).
cnf(c_4854,plain,
( ~ ssPv2(A)
| ssPv1(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5555]) ).
cnf(c_5556,plain,
( ssPv1(A)
| ssPv1(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4854,c_4700]) ).
cnf(c_4863,plain,
( ssPv1(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5556]) ).
cnf(c_5557,plain,
( ssPv2(skf2(A))
| ssPv1(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_4863,c_3534]) ).
cnf(c_4869,plain,
( ssPv2(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5557]) ).
cnf(c_5558,plain,
( ssPv2(A)
| ssPv4(A)
| ~ ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4825,c_4715]) ).
cnf(c_4946,plain,
( ssPv4(A)
| ~ ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5558]) ).
cnf(c_5559,plain,
( ssPv4(A)
| ssPv4(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4946,c_4753]) ).
cnf(c_4950,plain,
( ssPv4(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5559]) ).
cnf(c_4964,plain,
( ~ ssPv1(A)
| ~ ssPv1(skf2(A))
| ~ ssPv2(skf2(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4950,c_576]) ).
cnf(c_5560,plain,
( ssPv2(skf2(A))
| ~ ssPv1(skf2(A))
| ~ ssPv1(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_4950,c_164]) ).
cnf(c_4966,plain,
( ~ ssPv1(skf2(A))
| ~ ssPv1(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5560]) ).
cnf(c_4974,plain,
( ssPv4(skf2(A))
| ssPv1(A)
| ~ ssPv1(skf3(A))
| ~ ssPv2(skf2(skf3(A))) ),
inference(resolve,[status(thm)],[c_978,c_4827]) ).
cnf(c_5561,plain,
( ssPv2(skf2(A))
| ~ ssPv1(A)
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_4966,c_4700]) ).
cnf(c_4995,plain,
( ~ ssPv1(A)
| ssPv2(skf2(A)) ),
inference(copy,[status(thm)],[c_5561]) ).
cnf(c_5562,plain,
( ssPv2(skf2(A))
| ssPv2(skf2(A)) ),
inference(resolve,[status(thm)],[c_4995,c_4869]) ).
cnf(c_4997,plain,
ssPv2(skf2(A)),
inference(copy,[status(thm)],[c_5562]) ).
cnf(c_5001,plain,
( ssPv4(skf2(A))
| ssPv1(A)
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_4997,c_4974]) ).
cnf(c_5003,plain,
( ~ ssPv1(A)
| ~ ssPv1(skf2(A))
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_4997,c_4964]) ).
cnf(c_5043,plain,
( ssPv1(A)
| ~ ssPv3(skf3(A))
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_4997,c_978]) ).
cnf(c_5044,plain,
( ssPv1(skf2(A))
| ssPv1(A)
| ~ ssPv4(skf2(skf2(A))) ),
inference(resolve,[status(thm)],[c_4997,c_952]) ).
cnf(c_5050,plain,
( ~ ssPv4(A)
| ~ ssPv1(A)
| ~ ssPv1(skf2(A)) ),
inference(resolve,[status(thm)],[c_4997,c_576]) ).
cnf(c_5563,plain,
( ssPv2(A)
| ~ ssPv1(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_5003,c_4770]) ).
cnf(c_5089,plain,
( ~ ssPv1(A)
| ssPv2(A) ),
inference(copy,[status(thm)],[c_5563]) ).
cnf(c_5564,plain,
( ssPv2(A)
| ssPv2(A) ),
inference(resolve,[status(thm)],[c_5089,c_4700]) ).
cnf(c_5091,plain,
ssPv2(A),
inference(copy,[status(thm)],[c_5564]) ).
cnf(c_5565,plain,
( ssPv1(A)
| ~ ssPv2(skf3(A))
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_5091,c_1045]) ).
cnf(c_5146,plain,
( ssPv1(A)
| ~ ssPv3(A) ),
inference(resolve,[status(thm)],[c_5091,c_5565]) ).
cnf(c_5164,plain,
( ~ ssPv1(A)
| ~ ssPv1(skf2(A))
| ~ ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_5091,c_651]) ).
cnf(c_5206,plain,
( ssPv4(skf2(A))
| ssPv1(skf3(A)) ),
inference(resolve,[status(thm)],[c_5146,c_4827]) ).
cnf(c_5208,plain,
( ~ ssPv1(A)
| ~ ssPv1(skf2(A))
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_5206,c_5164]) ).
cnf(c_5566,plain,
( ssPv4(skf2(A))
| ssPv4(skf2(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_5001,c_5206]) ).
cnf(c_5241,plain,
( ssPv4(skf2(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5566]) ).
cnf(c_5567,plain,
( ssPv4(skf2(A))
| ~ ssPv1(A)
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_5208,c_4753]) ).
cnf(c_5276,plain,
( ~ ssPv1(A)
| ssPv4(skf2(A)) ),
inference(copy,[status(thm)],[c_5567]) ).
cnf(c_5568,plain,
( ssPv4(skf2(A))
| ssPv4(skf2(A)) ),
inference(resolve,[status(thm)],[c_5276,c_5241]) ).
cnf(c_5278,plain,
ssPv4(skf2(A)),
inference(copy,[status(thm)],[c_5568]) ).
cnf(c_5283,plain,
( ssPv1(skf2(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_5278,c_5044]) ).
cnf(c_5289,plain,
( ~ ssPv1(skf2(A))
| ~ ssPv1(skf2(skf2(A))) ),
inference(resolve,[status(thm)],[c_5278,c_5050]) ).
cnf(c_5297,plain,
( ssPv3(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_5283,c_4814]) ).
cnf(c_5569,plain,
( ssPv1(A)
| ~ ssPv1(skf3(A))
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_5297,c_5043]) ).
cnf(c_5304,plain,
( ~ ssPv1(skf3(A))
| ssPv1(A) ),
inference(copy,[status(thm)],[c_5569]) ).
cnf(c_5570,plain,
( ssPv1(A)
| ssPv1(A) ),
inference(resolve,[status(thm)],[c_5304,c_4863]) ).
cnf(c_5311,plain,
ssPv1(A),
inference(copy,[status(thm)],[c_5570]) ).
cnf(c_5571,plain,
~ ssPv1(skf2(A)),
inference(resolve,[status(thm)],[c_5311,c_5289]) ).
cnf(c_5314,plain,
$false,
inference(resolve,[status(thm)],[c_5311,c_5571]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN796-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/10.37 % Computer : n019.cluster.edu
% 0.10/10.37 % Model : x86_64 x86_64
% 0.10/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.37 % Memory : 8046.5625MB
% 0.10/10.37 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Sat Sep 26 18:30:59 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.10/10.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/10.38 % Process 1927987 was started by sandbox on n019,
% 0.10/10.38 % Sat Sep 26 18:30:59 2026
% 0.10/10.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/10.39
% 0.10/10.39 % From the command line: assign(max_seconds, 300).
% 7.03/11.34
% 7.03/11.34 % given #500 (T,wt=23): 393 -ssRr(A,A) | -ssPv1(A) | -ssRr(A,B) | ssPv3(B) | ssPv1(skf2(A)). [factor(386,b,d)].
% 7.03/11.34
% 7.03/11.34 % given #1000 (W,wt=19): 4710 ssPv1(skf3(A)) | ssPv3(A) | ssPv4(A) | -ssPv1(A). [resolve(4700,a,767,e),merge(d)].
% 7.03/11.34
% 7.03/11.34 % SZS status Unsatisfiable for theBenchmark
% 7.03/11.34
% 7.03/11.34 % Proof 1 at 0.70 (+ 0.21) seconds.
% 7.03/11.34 % Length of proof is 322.
% 7.03/11.34 % Level of proof is 61.
% 7.03/11.34 % Maximum clause weight is 27.000.
% 7.03/11.34 % Given clauses 1121.
% 7.03/11.34
% 7.03/11.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------