%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN797-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 : Tue Sep 29 02:02:02 PM UTC 2026
% Result : Satisfiable 12.01s 2.45s
% Output : Saturation 13.36s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u106,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv4(X0)
| ssPv4(X1)
| ssPv2(skf2(X0))
| ssPv1(X0) ) ).
cnf(u248,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv4(X1) ) ).
cnf(u4489,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ssPv1(X0)
| ssPv2(X0)
| ~ ssPv4(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u518,negated_conjecture,
( ssPv3(skf3(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u2075,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv1(skf2(X0))
| ~ ssPv2(X0) ) ).
cnf(u550,negated_conjecture,
( ssPv3(skf2(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(skf3(X0))
| ssPv2(X0) ) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ssPv2(X2)
| ssPv4(X1) ) ).
cnf(u5648,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv1(X1)
| ~ ssPv3(X0)
| ssPv3(skf3(skf2(X0))) ) ).
cnf(u151,negated_conjecture,
( ~ ssRr(skf3(X0),X1)
| ~ ssPv3(X1)
| ~ ssRr(X2,skf3(X0))
| ~ ssPv1(X0)
| ssPv1(X2)
| ssPv1(skf3(X0)) ) ).
cnf(u3105,negated_conjecture,
( ssPv1(skf3(skf3(X0)))
| ssPv2(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0)) ) ).
cnf(u279,negated_conjecture,
( ~ ssRr(skf3(X0),X2)
| ~ ssPv1(X0)
| ssPv2(X0)
| ~ ssRr(X1,skf3(X0))
| ~ ssPv3(X1)
| ~ ssPv1(skf3(X0))
| ~ ssPv3(X2)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u2945,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ssPv1(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0)) ) ).
cnf(u301,negated_conjecture,
( ~ ssRr(X0,skf2(X1))
| ~ ssPv1(skf2(X1))
| ssPv3(X0)
| ssPv2(X1)
| ~ ssPv2(skf2(X1))
| ssPv1(skf3(skf2(X1))) ) ).
cnf(clause32,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X2)
| ~ ssPv1(X1)
| ~ ssPv3(X1)
| ssPv2(X0) ) ).
cnf(u535,negated_conjecture,
( ~ ssPv1(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv4(skf2(X0)) ) ).
cnf(clause51,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssRr(X1,X3)
| ~ ssPv4(X3)
| ~ ssPv2(X1)
| ssPv4(X2) ) ).
cnf(u1156,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv2(skf3(skf2(X0)))
| ssPv3(X0) ) ).
cnf(u149,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv3(X1)
| ssPv3(X0)
| ssPv1(skf3(X1)) ) ).
cnf(clause38,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X2)
| ~ ssPv4(X1)
| ssPv1(X1) ) ).
cnf(u4141,negated_conjecture,
( ~ ssPv3(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u160,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssRr(X1,X0)
| ssPv3(X2)
| ssPv1(skf2(X1))
| ssPv4(X1) ) ).
cnf(u61,negated_conjecture,
( ssPv4(skf3(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0) ) ).
cnf(u824,negated_conjecture,
( ssPv1(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(X0) ) ).
cnf(u1839,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv1(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(X0)) ) ).
cnf(u561,negated_conjecture,
( ssPv3(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv3(skf3(X0)) ) ).
cnf(u2715,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ssPv4(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv1(X0) ) ).
cnf(u166,negated_conjecture,
( ssPv1(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u3501,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(X0)) ) ).
cnf(u1953,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ~ ssPv1(X1)
| ~ ssPv3(X0) ) ).
cnf(u6527,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv3(X1)
| ssPv2(skf3(X0)) ) ).
cnf(u6059,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv2(X0) ) ).
cnf(u189,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv4(skf2(X0)) ) ).
cnf(u952,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv4(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv3(skf2(X0)) ) ).
cnf(u5606,negated_conjecture,
( ~ ssPv2(skf2(skf2(X0)))
| ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf2(skf2(X0)))
| ~ ssPv1(skf2(X0)) ) ).
cnf(u164,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u3645,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X2)
| ~ ssPv3(X2) ) ).
cnf(u2396,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ~ ssPv3(X0)
| ssPv4(skf3(X0))
| ~ ssPv3(X1) ) ).
cnf(u5718,negated_conjecture,
( ~ ssPv1(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ssPv3(skf3(skf2(X0))) ) ).
cnf(u1460,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv1(X0) ) ).
cnf(u179,negated_conjecture,
( ~ ssPv4(skf2(X1))
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ssPv4(skf3(X1)) ) ).
cnf(u434,negated_conjecture,
( ssPv1(skf2(skf3(X0)))
| ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u386,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv1(X1)
| ssPv4(skf2(X0)) ) ).
cnf(u3399,negated_conjecture,
( ~ ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0) ) ).
cnf(u177,negated_conjecture,
( ~ ssPv4(skf2(X1))
| ~ ssPv1(X0)
| ~ ssRr(X0,X1)
| ~ ssPv4(X1)
| ssPv3(skf3(X1)) ) ).
cnf(u3922,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X0))
| ssPv4(X1) ) ).
cnf(u1215,negated_conjecture,
( ssPv1(skf3(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv1(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u76,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv4(skf2(X0)) ) ).
cnf(u1987,negated_conjecture,
( ~ ssPv1(skf3(skf2(X0)))
| ssPv4(X0)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u206,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ssPv4(skf3(X0))
| ssPv4(X0) ) ).
cnf(u1117,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ssPv2(X0) ) ).
cnf(u1349,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv1(skf3(X0))
| ssPv4(X0)
| ~ ssPv1(X1) ) ).
cnf(u847,negated_conjecture,
( ~ ssPv3(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ~ ssPv2(skf2(skf3(X0))) ) ).
cnf(u6601,negated_conjecture,
( ssPv3(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u91,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv2(X1) ) ).
cnf(u636,negated_conjecture,
( ~ ssPv3(skf3(skf3(X0)))
| ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u461,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0) ) ).
cnf(u5210,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ssPv3(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv2(X0) ) ).
cnf(u3612,negated_conjecture,
( ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(X0) ) ).
cnf(u66,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssPv2(X1)
| ssPv3(skf2(X1)) ) ).
cnf(u1353,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ssPv1(skf3(X0))
| ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssPv3(skf3(X0)) ) ).
cnf(u204,negated_conjecture,
( ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u1477,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(X1) ) ).
cnf(u2647,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv2(skf2(X0))
| ~ ssPv1(skf2(X0))
| ssPv4(skf2(X0))
| ssPv3(X1)
| ssPv2(X0) ) ).
cnf(u2513,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv3(X1)
| ~ ssPv1(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u868,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u2669,negated_conjecture,
( ssPv2(skf2(skf3(X0)))
| ssPv2(skf3(X0))
| ssPv4(skf3(X0))
| ssPv1(X0) ) ).
cnf(u2256,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv1(skf2(X0))
| ~ ssPv3(X1)
| ssPv4(skf2(X0))
| ssPv4(X0) ) ).
cnf(u474,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u116,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ssPv3(X0)
| ssPv2(skf2(X1))
| ssPv1(X1) ) ).
cnf(u194,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv4(X0) ) ).
cnf(u603,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X2)
| ~ ssPv3(X2)
| ~ ssPv2(X0) ) ).
cnf(u95,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv3(X0)
| ~ ssPv2(X1)
| ~ ssPv3(skf3(X1))
| ssPv1(skf3(X1)) ) ).
cnf(u217,negated_conjecture,
( ssPv2(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv1(skf2(skf3(X0)))
| ssPv3(skf3(X0)) ) ).
cnf(u3812,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(X0)
| ~ ssPv1(X0)
| ssPv1(X1) ) ).
cnf(u716,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(X0)) ) ).
cnf(u350,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ssPv4(X0)
| ~ ssPv3(X0)
| ssPv1(X0) ) ).
cnf(u472,negated_conjecture,
( ~ ssRr(skf2(X0),X2)
| ~ ssPv2(skf2(X0))
| ~ ssPv4(X0)
| ~ ssRr(X1,skf2(X0))
| ~ ssPv3(X1)
| ~ ssPv1(skf2(X0))
| ~ ssPv3(X2) ) ).
cnf(u6511,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ) ).
cnf(u3810,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv2(skf3(X0))
| ssPv4(X0) ) ).
cnf(u4329,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ssPv2(skf3(X0))
| ssPv4(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u5719,negated_conjecture,
( ssPv3(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ~ ssPv1(X0) ) ).
cnf(u2431,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(X1) ) ).
cnf(u223,negated_conjecture,
( ~ ssPv1(skf2(skf3(X0)))
| ~ ssRr(X1,skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv2(X1)
| ssPv2(X0) ) ).
cnf(u1918,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u517,negated_conjecture,
( ~ ssPv4(skf3(skf3(X0)))
| ssPv3(X0)
| ssPv1(skf2(skf3(X0)))
| ssPv4(skf3(X0)) ) ).
cnf(u256,negated_conjecture,
( ssPv3(skf2(skf2(X0)))
| ~ ssPv4(X0)
| ssPv1(skf2(skf2(X0)))
| ssPv4(skf2(X0)) ) ).
cnf(u104,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ~ ssRr(X1,X0)
| ~ ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssPv4(X1) ) ).
cnf(u515,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv1(X1)
| ssPv1(X0)
| ~ ssPv3(skf3(X1))
| ssPv4(skf3(X1)) ) ).
cnf(u2429,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv2(skf2(X0)) ) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ssPv3(X0) ) ).
cnf(u5505,negated_conjecture,
( ~ ssPv1(skf3(skf2(X0)))
| ssPv1(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv3(X0) ) ).
cnf(u489,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ssPv4(X1) ) ).
cnf(u756,negated_conjecture,
( ~ ssPv4(skf3(skf3(X0)))
| ssPv3(skf2(skf3(X0)))
| ssPv1(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u262,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u1142,negated_conjecture,
( ~ ssPv3(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv3(X0)
| ~ ssPv2(skf2(skf2(X0))) ) ).
cnf(u3863,negated_conjecture,
( ~ ssPv1(X0)
| ssPv4(X0) ) ).
cnf(u1005,negated_conjecture,
( ~ ssPv4(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv4(skf2(X0))
| ~ ssPv2(skf2(X0)) ) ).
cnf(u232,negated_conjecture,
( ~ ssPv4(skf2(X0))
| ssPv2(skf2(X0))
| ssPv1(X0)
| ssPv4(X0) ) ).
cnf(u2059,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv1(skf2(X0))
| ssPv4(X1) ) ).
cnf(u534,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u7197,negated_conjecture,
( ssPv2(skf3(skf2(X0)))
| ~ ssPv4(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u5878,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv1(X0) ) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ssPv2(X0)
| ssPv1(X1)
| ssPv4(X1) ) ).
cnf(u135,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ~ ssPv2(X1)
| ssPv4(skf3(X1))
| ssPv4(X1) ) ).
cnf(u5098,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv3(X1)
| ~ ssPv4(X0)
| ssPv4(skf3(skf2(X0))) ) ).
cnf(u1770,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv3(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u260,negated_conjecture,
( ssPv2(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv2(skf3(skf3(X0)))
| ~ ssPv1(X0) ) ).
cnf(u5627,negated_conjecture,
( ssPv2(skf3(skf2(X0)))
| ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(u390,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv3(X1)
| ssPv2(X0) ) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1)
| ssPv2(X2)
| ssPv1(X0)
| ssPv4(X0) ) ).
cnf(u73,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ~ ssPv4(X2)
| ~ ssPv4(X1)
| ssPv3(skf3(X1)) ) ).
cnf(u263,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv4(skf2(X0)) ) ).
cnf(u133,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ssPv4(X0) ) ).
cnf(u2315,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ~ ssPv3(X1)
| ssPv4(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u401,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u761,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv1(skf3(skf2(X0))) ) ).
cnf(u5764,negated_conjecture,
( ssPv3(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ) ).
cnf(u2435,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ssPv1(X2)
| ssPv4(X0) ) ).
cnf(u144,negated_conjecture,
( ~ ssRr(X0,skf2(X1))
| ~ ssPv3(X0)
| ~ ssPv3(skf2(X1))
| ssPv2(X1)
| ssPv4(skf2(X1)) ) ).
cnf(u6154,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u4625,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ssPv2(X0) ) ).
cnf(u1684,negated_conjecture,
( ssPv3(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u2331,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv1(skf2(skf2(X0))) ) ).
cnf(clause45,negated_conjecture,
( ~ ssRr(X0,X3)
| ~ ssPv3(X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1)
| ssPv3(X2)
| ssPv1(X3)
| ssPv4(X0) ) ).
cnf(u2776,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv4(skf3(X0))
| ssPv3(X0) ) ).
cnf(u407,negated_conjecture,
( ~ ssPv3(X0)
| ssPv4(X0)
| ssPv1(X0) ) ).
cnf(u1682,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(skf3(X0))
| ssPv4(skf3(X0)) ) ).
cnf(u545,negated_conjecture,
( ~ ssPv3(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ssPv1(X0)
| ssPv3(skf2(X0)) ) ).
cnf(u150,negated_conjecture,
( ~ ssRr(X0,skf2(X1))
| ~ ssPv1(skf2(X1))
| ~ ssPv3(skf2(X1))
| ssPv3(X0)
| ssPv1(X1) ) ).
cnf(u2097,negated_conjecture,
( ssPv3(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf3(X0)) ) ).
cnf(u6425,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ssPv4(X0) ) ).
cnf(clause35,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv2(X1)
| ssPv3(X2) ) ).
cnf(u173,negated_conjecture,
( ~ ssRr(skf2(X1),X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf2(X1))
| ssPv2(X1)
| ssPv2(skf2(skf2(X1))) ) ).
cnf(u405,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv4(X0) ) ).
cnf(u6049,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv3(X1) ) ).
cnf(u62,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv4(skf2(X0)) ) ).
cnf(u148,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv2(X0)
| ~ ssPv3(X1)
| ssPv1(skf2(X1))
| ssPv4(X1) ) ).
cnf(u3610,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0)) ) ).
cnf(u163,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv3(X0) ) ).
cnf(u568,negated_conjecture,
( ssPv4(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv2(X0) ) ).
cnf(u60,negated_conjecture,
( ~ ssRr(skf2(X1),X2)
| ~ ssRr(X0,skf2(X1))
| ~ ssPv2(X1)
| ~ ssPv3(X0)
| ~ ssPv3(X2)
| ~ ssPv2(skf2(X1)) ) ).
cnf(u190,negated_conjecture,
( ~ ssPv4(skf2(skf2(X1)))
| ~ ssPv1(X0)
| ~ ssRr(X0,skf2(X1))
| ~ ssPv4(skf2(X1))
| ssPv3(X1) ) ).
cnf(u2216,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u690,negated_conjecture,
( ssPv1(skf3(X0))
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u3908,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv1(X0) ) ).
cnf(u161,negated_conjecture,
( ~ ssRr(skf3(X1),X2)
| ~ ssPv1(X0)
| ~ ssRr(skf3(X1),X0)
| ssPv2(X2)
| ssPv1(X1)
| ssPv3(skf3(X1)) ) ).
cnf(u307,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv1(skf3(X1))
| ssPv2(X0)
| ssPv2(X1)
| ~ ssPv2(skf3(X1))
| ssPv1(skf3(skf3(X1))) ) ).
cnf(clause50,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1)
| ~ ssRr(X1,X3)
| ~ ssPv4(X3)
| ~ ssPv4(X1)
| ssPv3(X2) ) ).
cnf(u188,negated_conjecture,
( ~ ssPv3(skf3(skf2(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(skf2(X0))
| ~ ssPv4(skf2(X0)) ) ).
cnf(u1101,negated_conjecture,
( ssPv3(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv3(X0) ) ).
cnf(u1461,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ssPv1(skf2(skf3(X0)))
| ~ ssPv1(X0) ) ).
cnf(u75,negated_conjecture,
( ssPv2(skf3(X0))
| ~ ssPv2(X0)
| ssPv1(X0)
| ssPv4(X0) ) ).
cnf(u4667,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ssPv3(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u330,negated_conjecture,
( ssPv2(skf3(X0))
| ssPv2(X0)
| ~ ssPv3(X0)
| ssPv4(X0) ) ).
cnf(u178,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv3(X0)
| ~ ssPv4(X1)
| ~ ssPv2(skf3(X1))
| ssPv4(skf3(skf3(X1))) ) ).
cnf(u2901,negated_conjecture,
( ssPv2(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv1(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u2497,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0)) ) ).
cnf(u4300,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ssPv4(skf2(X0))
| ssPv2(X0) ) ).
cnf(u3666,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u857,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv3(skf3(X0)) ) ).
cnf(u100,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv4(X1)
| ssPv4(X0) ) ).
cnf(u7233,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv1(X1)
| ~ ssPv4(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u2500,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u2430,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ssPv4(skf2(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ~ ssPv1(X0)
| ssPv1(X1) ) ).
cnf(u79,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ~ ssPv2(X1) ) ).
cnf(u201,negated_conjecture,
( ~ ssPv1(skf3(skf3(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u1116,negated_conjecture,
( ssPv1(skf3(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv1(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u5211,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ~ ssPv4(X0)
| ssPv1(skf2(skf2(X0)))
| ssPv4(skf2(X0)) ) ).
cnf(u1323,negated_conjecture,
( ssPv3(skf2(skf2(X0)))
| ssPv1(skf2(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u8109,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ssPv3(skf2(X0)) ) ).
cnf(u1497,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(skf2(skf2(X0)))
| ~ ssPv3(X1)
| ~ ssPv3(skf2(X0))
| ssPv4(X0) ) ).
cnf(u715,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv1(X0) ) ).
cnf(u606,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u207,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u612,negated_conjecture,
( ssPv4(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X0) ) ).
cnf(u475,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ssPv2(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u1902,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv3(X0) ) ).
cnf(u629,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv3(skf2(X0))
| ~ ssPv2(skf2(X0)) ) ).
cnf(u368,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv1(skf3(X0))
| ssPv3(X0) ) ).
cnf(u3278,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0) ) ).
cnf(u88,negated_conjecture,
( ~ ssRr(skf2(X1),X2)
| ~ ssRr(X0,skf2(X1))
| ~ ssPv3(X0)
| ~ ssPv4(X2)
| ~ ssPv2(skf2(X1))
| ssPv4(X1) ) ).
cnf(u2260,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv1(X0)
| ssPv4(X0) ) ).
cnf(u6629,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u119,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv4(X0)
| ssPv4(X1)
| ssPv2(skf3(X1))
| ssPv4(skf3(X1)) ) ).
cnf(u1906,negated_conjecture,
( ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ssPv2(X0)
| ssPv4(skf2(X0))
| ssPv1(X0) ) ).
cnf(u473,negated_conjecture,
( ssPv3(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(u989,negated_conjecture,
( ssPv1(skf2(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ssPv2(skf3(X0)) ) ).
cnf(u216,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv4(skf2(X0))
| ssPv3(X0)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u2530,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u2257,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv3(X1)
| ssPv4(X0) ) ).
cnf(u117,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X1))
| ~ ssPv4(skf3(X1))
| ssPv1(X1) ) ).
cnf(u1805,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u247,negated_conjecture,
( ~ ssRr(X0,X1)
| ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssPv4(X0) ) ).
cnf(u5633,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ~ ssPv3(X0)
| ssPv4(skf2(skf2(X0))) ) ).
cnf(u6155,negated_conjecture,
( ~ ssPv2(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u5099,negated_conjecture,
( ~ ssPv3(skf3(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv4(X0) ) ).
cnf(u502,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv3(X0) ) ).
cnf(u631,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u1777,negated_conjecture,
( ~ ssPv2(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ssPv1(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(u3075,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv2(X0)
| ~ ssPv1(skf3(X0)) ) ).
cnf(u6421,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv1(X1)
| ssPv2(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u430,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ssPv4(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0) ) ).
cnf(u245,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv1(X1)
| ssPv4(X0) ) ).
cnf(u1791,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0)) ) ).
cnf(u385,negated_conjecture,
( ~ ssPv3(skf2(skf2(X0)))
| ssPv1(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0)) ) ).
cnf(u6001,negated_conjecture,
( ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv3(X0)
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u1365,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv1(skf2(skf2(X0)))
| ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv1(skf2(X0)) ) ).
cnf(u128,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv3(X0)
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u3095,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv2(X0) ) ).
cnf(u5874,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u899,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ssPv2(X0)
| ssPv1(skf3(X0))
| ssPv2(skf3(X0)) ) ).
cnf(u2509,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv1(skf2(X0))
| ~ ssPv3(X1)
| ~ ssPv2(skf2(X0))
| ssPv4(X0) ) ).
cnf(clause29,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ssPv4(X2) ) ).
cnf(u7207,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv4(X0) ) ).
cnf(u261,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv2(skf3(X0))
| ssPv2(skf2(X0)) ) ).
cnf(u5506,negated_conjecture,
( ~ ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ) ).
cnf(u2185,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u1574,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv1(X1)
| ssPv1(skf2(X0))
| ~ ssPv4(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u134,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv3(X1)
| ~ ssPv2(skf3(X1))
| ssPv4(X0) ) ).
cnf(u1672,negated_conjecture,
( ~ ssRr(skf3(X0),X2)
| ssPv3(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssRr(X1,skf3(X0))
| ~ ssPv3(X1)
| ~ ssPv1(skf3(X0))
| ~ ssPv3(X2)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u4090,negated_conjecture,
( ssPv1(skf2(skf3(X0)))
| ssPv3(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv3(X1)
| ssPv3(X0)
| ssPv1(X2) ) ).
cnf(u157,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv1(skf3(X1))
| ~ ssPv2(skf3(X1))
| ssPv1(X0)
| ssPv1(X1) ) ).
cnf(u303,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv1(X0)
| ssPv2(skf2(skf3(X1)))
| ssPv1(X1)
| ssPv3(skf3(X1)) ) ).
cnf(u389,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv4(X1) ) ).
cnf(clause46,negated_conjecture,
( ~ ssRr(X0,X3)
| ~ ssPv1(X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1)
| ssPv2(X2)
| ssPv1(X3)
| ssPv3(X0) ) ).
cnf(u6037,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv4(X0) ) ).
cnf(u8080,negated_conjecture,
~ ssPv1(X0) ).
cnf(u508,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ) ).
cnf(u546,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf2(X0)) ) ).
cnf(u3892,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u3594,negated_conjecture,
( ssPv4(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1)
| ssPv2(X2)
| ssPv1(X1)
| ssPv3(X1) ) ).
cnf(u796,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ssPv2(skf3(X0)) ) ).
cnf(u147,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv2(X0)
| ~ ssPv3(skf3(X1))
| ssPv1(X1)
| ssPv4(skf3(X1)) ) ).
cnf(u2718,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u5285,negated_conjecture,
( ssPv3(skf2(skf3(X0)))
| ssPv4(skf3(X0))
| ssPv2(skf3(X0)) ) ).
cnf(u552,negated_conjecture,
( ssPv3(skf2(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u569,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv4(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0) ) ).
cnf(u402,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ssPv4(X0)
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0) ) ).
cnf(u1177,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(skf2(X0))
| ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssPv4(skf2(X0)) ) ).
cnf(clause44,negated_conjecture,
( ~ ssRr(X1,X3)
| ~ ssPv4(X0)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ssPv3(X2)
| ssPv1(X3)
| ssPv4(X1) ) ).
cnf(u1955,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u174,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv1(X1)
| ~ ssPv1(skf3(X1))
| ssPv3(X0)
| ssPv2(skf3(skf3(X1))) ) ).
cnf(u815,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u2398,negated_conjecture,
( ~ ssPv3(skf3(skf3(X0)))
| ssPv4(skf3(X0))
| ~ ssPv3(X0) ) ).
cnf(u59,negated_conjecture,
( ~ ssPv2(skf3(X1))
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ~ ssPv2(X1) ) ).
cnf(u145,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv4(X1)
| ~ ssPv1(skf3(X1))
| ssPv4(X0)
| ssPv2(skf3(X1)) ) ).
cnf(u1190,negated_conjecture,
( ssPv3(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u429,negated_conjecture,
( ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv2(X0) ) ).
cnf(u680,negated_conjecture,
( ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv2(X0) ) ).
cnf(u400,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ssPv4(X0)
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0) ) ).
cnf(u6559,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv1(X1)
| ~ ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(clause34,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv2(X1)
| ssPv2(X2) ) ).
cnf(u1679,negated_conjecture,
( ssPv3(skf2(skf3(X0)))
| ssPv3(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0)) ) ).
cnf(u172,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ~ ssPv1(X1)
| ssPv2(skf3(X1))
| ssPv2(skf2(X1)) ) ).
cnf(u3646,negated_conjecture,
( ~ ssPv1(X0)
| ~ ssPv2(X0) ) ).
cnf(u1064,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ssPv4(X0)
| ~ ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0)) ) ).
cnf(u4338,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(X0)
| ~ ssPv1(X1)
| ssPv2(X0)
| ~ ssPv4(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u57,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf3(X0)) ) ).
cnf(u187,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv2(skf2(X0))
| ssPv2(X0) ) ).
cnf(u573,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv4(skf2(X0))
| ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u442,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv2(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u2662,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u162,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(X0)
| ~ ssRr(X1,X0)
| ssPv2(X2)
| ssPv1(skf2(X1))
| ssPv3(X1) ) ).
cnf(u3889,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(X0) ) ).
cnf(u101,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv2(X0)
| ssPv2(X1)
| ssPv1(skf3(X1))
| ssPv3(skf3(X1)) ) ).
cnf(u5996,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssPv2(X0) ) ).
cnf(u6520,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv1(skf2(X0))
| ssPv3(X1)
| ssPv2(X0) ) ).
cnf(u63,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(skf3(X0))
| ssPv4(skf3(X0)) ) ).
cnf(u185,negated_conjecture,
( ~ ssPv4(skf2(skf2(X1)))
| ~ ssPv3(X0)
| ~ ssRr(X0,skf2(X1))
| ~ ssPv2(skf2(X1))
| ssPv4(X1) ) ).
cnf(u6067,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ) ).
cnf(u84,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv3(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv3(X0) ) ).
cnf(u3667,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ssPv4(X0)
| ~ ssPv1(X0) ) ).
cnf(u699,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ssPv4(X0)
| ssPv2(X0)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u855,negated_conjecture,
( ~ ssPv3(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv3(skf3(X0))
| ssPv2(X0) ) ).
cnf(u191,negated_conjecture,
( ssPv1(skf2(X0))
| ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u142,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ssPv1(X0)
| ssPv4(X1) ) ).
cnf(u74,negated_conjecture,
( ~ ssRr(skf2(X1),X2)
| ~ ssRr(X0,skf2(X1))
| ~ ssPv1(X0)
| ~ ssPv4(X2)
| ~ ssPv4(skf2(X1))
| ssPv3(X1) ) ).
cnf(u1115,negated_conjecture,
( ssPv2(skf3(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u6211,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ssPv4(X0) ) ).
cnf(u590,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv4(skf2(X0))
| ssPv2(X0) ) ).
cnf(u1886,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ssPv4(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u7269,negated_conjecture,
( ssPv1(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u72,negated_conjecture,
( ~ ssPv2(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ~ ssPv4(X1)
| ssPv1(X1) ) ).
cnf(u202,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv3(X0)
| ssPv3(X1)
| ssPv1(skf2(skf3(X1)))
| ssPv4(skf3(X1)) ) ).
cnf(u611,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv2(X0) ) ).
cnf(u592,negated_conjecture,
( ssPv2(skf3(X0))
| ~ ssPv3(X0)
| ssPv4(X0) ) ).
cnf(u103,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssPv1(skf3(X1))
| ~ ssPv4(skf3(X1)) ) ).
cnf(u6235,negated_conjecture,
( ssPv1(skf2(X0))
| ssPv4(X0)
| ssPv2(X0) ) ).
cnf(u358,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv4(X0)
| ssPv3(X1)
| ssPv1(X1)
| ssPv4(skf3(X1)) ) ).
cnf(u3014,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ssPv1(skf2(skf3(X0)))
| ssPv2(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u6605,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ssPv3(X0) ) ).
cnf(u200,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ssPv2(skf2(X1))
| ssPv1(skf2(X1))
| ssPv3(X1) ) ).
cnf(u9988,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv4(X0) ) ).
cnf(u8153,negated_conjecture,
( ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u630,negated_conjecture,
( ~ ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ) ).
cnf(u2525,negated_conjecture,
( ssPv1(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv1(skf2(X0)) ) ).
cnf(u864,negated_conjecture,
( ~ ssPv3(skf3(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ~ ssPv3(skf2(X0))
| ssPv3(X0) ) ).
cnf(u231,negated_conjecture,
( ssPv2(skf2(skf3(X0)))
| ~ ssPv4(X0)
| ssPv1(skf3(X0))
| ssPv4(skf3(X0)) ) ).
cnf(u2496,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv2(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X2)
| ~ ssPv3(X2) ) ).
cnf(u463,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ~ ssPv3(X0) ) ).
cnf(u356,negated_conjecture,
( ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf2(X0))
| ssPv4(X0) ) ).
cnf(u486,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv4(skf2(X0)) ) ).
cnf(u1917,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv4(X0) ) ).
cnf(u112,negated_conjecture,
( ~ ssRr(X0,skf2(X1))
| ~ ssPv3(X0)
| ~ ssPv1(X1)
| ~ ssPv3(skf2(X1))
| ~ ssPv4(skf2(X1)) ) ).
cnf(u1744,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ssPv4(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv3(X0) ) ).
cnf(u3886,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ssPv3(skf2(X0)) ) ).
cnf(u4468,negated_conjecture,
( ssPv3(skf2(skf2(X0)))
| ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv1(skf2(skf2(X0))) ) ).
cnf(u758,negated_conjecture,
( ssPv1(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u229,negated_conjecture,
( ssPv2(skf2(skf3(X0)))
| ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ssPv1(skf3(X0)) ) ).
cnf(u1775,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u1650,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ssPv2(X0)
| ~ ssPv3(skf3(X0))
| ssPv1(skf3(skf3(X0))) ) ).
cnf(u497,negated_conjecture,
( ~ ssPv4(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv2(skf3(X0)) ) ).
cnf(u1747,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X2)
| ~ ssPv3(X2) ) ).
cnf(u484,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ssPv1(skf2(skf2(X0))) ) ).
cnf(u118,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssPv4(X1)
| ssPv1(skf2(X1)) ) ).
cnf(u7265,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv1(X0) ) ).
cnf(u5634,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv3(X0) ) ).
cnf(u5999,negated_conjecture,
( ssPv3(skf3(skf2(X0)))
| ~ ssPv3(skf2(X0)) ) ).
cnf(u1780,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ssPv4(X2)
| ssPv2(X1)
| ssPv3(X1) ) ).
cnf(u219,negated_conjecture,
( ~ ssPv3(skf3(skf3(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u4796,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv1(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u503,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv4(skf3(X0)) ) ).
cnf(u1778,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u268,negated_conjecture,
( ~ ssPv1(skf3(skf3(X0)))
| ~ ssPv2(X0)
| ~ ssPv4(skf3(X0))
| ssPv1(skf3(X0)) ) ).
cnf(u246,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X0) ) ).
cnf(u898,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X1)
| ~ ssPv4(skf2(X0))
| ssPv4(X0) ) ).
cnf(u1180,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv2(skf2(X0))
| ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u7060,negated_conjecture,
( ~ ssPv2(skf2(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv4(X0) ) ).
cnf(u10333,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ssPv4(X0) ) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X0,X1)
| ssPv4(X0)
| ssPv2(X1)
| ssPv3(X1)
| ssPv4(X1) ) ).
cnf(u141,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv1(X1)
| ~ ssPv2(skf3(X1))
| ssPv1(X0)
| ssPv4(skf3(X1)) ) ).
cnf(u287,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(skf3(X0))
| ~ ssPv3(X1)
| ~ ssPv3(X0) ) ).
cnf(u253,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u258,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv4(skf3(X0))
| ssPv1(X0)
| ssPv2(X0) ) ).
cnf(u6539,negated_conjecture,
( ssPv2(skf3(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X2)
| ~ ssPv1(X1)
| ~ ssPv4(X1)
| ssPv4(X0) ) ).
cnf(u244,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0) ) ).
cnf(u9990,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u56,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssPv3(X1) ) ).
cnf(clause1,negated_conjecture,
ssRr(skf3(X0),X0) ).
cnf(u536,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u4642,negated_conjecture,
( ~ ssRr(skf2(X0),X1)
| ~ ssPv3(X0)
| ssPv4(skf3(skf2(X0)))
| ~ ssPv3(X1) ) ).
cnf(u553,negated_conjecture,
( ssPv3(skf2(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u10119,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv2(X0) ) ).
cnf(u10035,negated_conjecture,
( ssPv3(skf3(X0))
| ~ ssPv3(X0) ) ).
cnf(u1161,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv3(X0) ) ).
cnf(clause28,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv4(X2)
| ssPv1(X1)
| ssPv4(X1) ) ).
cnf(u158,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv2(X1)
| ssPv1(X0)
| ssPv1(skf2(X1)) ) ).
cnf(u1301,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv4(skf2(X0))
| ~ ssPv1(skf2(X0)) ) ).
cnf(u2184,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ssPv4(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u1324,negated_conjecture,
( ssPv3(skf2(skf2(X0)))
| ssPv1(skf2(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(clause43,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1)
| ~ ssPv4(X2)
| ~ ssPv1(X1)
| ~ ssPv3(X1) ) ).
cnf(u129,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv2(X1)
| ssPv1(skf3(X1))
| ssPv3(X1) ) ).
cnf(u413,negated_conjecture,
( ssPv4(skf3(X0))
| ssPv1(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X0) ) ).
cnf(u384,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv3(X1)
| ssPv2(skf3(skf2(X0))) ) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ~ ssPv4(X1)
| ssPv3(X0)
| ssPv4(X2) ) ).
cnf(u156,negated_conjecture,
( ~ ssPv4(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ssPv1(X1)
| ssPv4(X1) ) ).
cnf(u814,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv2(X0) ) ).
cnf(clause41,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv1(X2)
| ~ ssPv3(X1)
| ~ ssPv4(X1) ) ).
cnf(u171,negated_conjecture,
( ssPv2(skf3(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv4(X0) ) ).
cnf(u403,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u296,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv4(X0)
| ssPv1(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X1) ) ).
cnf(u3503,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u146,negated_conjecture,
( ~ ssPv4(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ssPv4(X0)
| ssPv2(X1) ) ).
cnf(u4249,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u1702,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ssPv1(X0)
| ssPv2(skf3(X0))
| ~ ssPv3(skf3(X0)) ) ).
cnf(clause47,negated_conjecture,
( ~ ssRr(X1,X3)
| ~ ssRr(X1,X2)
| ~ ssPv1(X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ssPv2(X0)
| ssPv2(X3) ) ).
cnf(u169,negated_conjecture,
( ssPv3(skf2(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv2(X0) ) ).
cnf(u1084,negated_conjecture,
( ssPv1(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0)) ) ).
cnf(u1214,negated_conjecture,
( ssPv2(skf3(skf2(X0)))
| ~ ssPv1(X0)
| ssPv4(skf2(X0))
| ~ ssPv2(skf2(X0)) ) ).
cnf(u302,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv1(X0)
| ssPv2(X1)
| ssPv1(X1)
| ssPv3(skf3(X1)) ) ).
cnf(u58,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X0) ) ).
cnf(u10036,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ssPv4(X0) ) ).
cnf(u2237,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv4(X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u1060,negated_conjecture,
( ssPv1(skf3(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ssPv3(skf3(X0)) ) ).
cnf(u6048,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0) ) ).
cnf(u175,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ssPv3(X0)
| ssPv2(skf3(X1)) ) ).
cnf(u2870,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv2(X0)
| ssPv4(skf3(X0))
| ~ ssPv3(X1)
| ~ ssPv4(X0) ) ).
cnf(u1968,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ~ ssPv3(skf2(X0))
| ~ ssPv2(skf2(X0)) ) ).
cnf(u186,negated_conjecture,
( ~ ssPv4(skf3(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv2(X0) ) ).
cnf(u1099,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv3(X0)
| ~ ssPv3(X1) ) ).
cnf(u1705,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ssPv1(X0)
| ssPv2(skf3(X0))
| ~ ssPv3(skf3(X0)) ) ).
cnf(u2876,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ssPv4(skf3(X0))
| ~ ssPv2(X0) ) ).
cnf(u827,negated_conjecture,
( ssPv4(skf3(X0))
| ssPv1(skf3(X0))
| ssPv2(X0) ) ).
cnf(u3141,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u5319,negated_conjecture,
( ssPv2(skf3(X0))
| ssPv4(skf3(X0))
| ssPv3(X0) ) ).
cnf(u5559,negated_conjecture,
( ssPv1(skf2(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u441,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ssPv2(skf3(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv1(X0) ) ).
cnf(u4675,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ~ ssPv1(X1)
| ~ ssPv4(X0) ) ).
cnf(u184,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv3(X0) ) ).
cnf(u1216,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv2(X0) ) ).
cnf(u87,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv4(X2)
| ~ ssPv2(X1)
| ssPv4(skf3(X1)) ) ).
cnf(u2498,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0) ) ).
cnf(u85,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssPv4(skf3(X1))
| ssPv1(skf3(X1)) ) ).
cnf(u215,negated_conjecture,
( ssPv3(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u2433,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X1)
| ~ ssPv2(X0) ) ).
cnf(u5630,negated_conjecture,
( ~ ssRr(skf2(X0),X1)
| ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv4(X1) ) ).
cnf(u3009,negated_conjecture,
( ssPv1(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv3(skf3(X0))
| ~ ssPv4(skf3(X0)) ) ).
cnf(u96,negated_conjecture,
( ~ ssPv2(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ssPv1(X1) ) ).
cnf(u1544,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv1(skf2(X0))
| ~ ssPv4(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u6233,negated_conjecture,
( ssPv1(skf2(skf2(X0)))
| ~ ssPv4(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u867,negated_conjecture,
( ~ ssPv3(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv1(X0) ) ).
cnf(u1653,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ssPv2(X0)
| ~ ssPv3(skf3(X0)) ) ).
cnf(u6595,negated_conjecture,
( ssPv3(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u359,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv4(X0)
| ssPv3(skf2(skf3(X1)))
| ssPv1(X1)
| ssPv4(skf3(X1)) ) ).
cnf(u849,negated_conjecture,
( ~ ssPv3(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u1651,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ssPv2(X0)
| ~ ssPv3(skf3(X0)) ) ).
cnf(u713,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(X1)
| ssPv1(X0) ) ).
cnf(u5637,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv1(skf2(X0))
| ssPv4(X1) ) ).
cnf(u2515,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u102,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv2(X0)
| ssPv2(skf2(X1))
| ssPv1(X1)
| ssPv3(X1) ) ).
cnf(u224,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(X0) ) ).
cnf(u1519,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ~ ssPv3(skf2(X0))
| ssPv1(skf2(skf2(X0))) ) ).
cnf(u602,negated_conjecture,
( ~ ssPv3(X0)
| ssPv4(X0) ) ).
cnf(u5995,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(X1) ) ).
cnf(u4214,negated_conjecture,
( ssPv1(skf3(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u125,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X2)
| ~ ssPv1(X1)
| ssPv3(X0)
| ssPv2(skf3(X1)) ) ).
cnf(u203,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv3(X0)
| ssPv3(skf2(X1))
| ssPv1(skf2(X1))
| ssPv4(X1) ) ).
cnf(u357,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv3(X0)
| ssPv3(skf3(X0))
| ~ ssPv1(X1)
| ~ ssPv4(X0) ) ).
cnf(u3288,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u487,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv3(X1) ) ).
cnf(u1762,negated_conjecture,
( ~ ssPv1(skf3(skf2(X0)))
| ssPv3(X0)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u3441,negated_conjecture,
( ssPv4(skf3(X0))
| ssPv2(X0) ) ).
cnf(u4810,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv1(X1)
| ssPv1(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv3(skf3(skf2(X0))) ) ).
cnf(u230,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ssPv1(X0) ) ).
cnf(u5096,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv3(X1) ) ).
cnf(u639,negated_conjecture,
( ~ ssRr(skf2(X0),X1)
| ~ ssPv3(X0)
| ~ ssPv3(skf2(X0))
| ~ ssPv3(X1)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u762,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv1(X0) ) ).
cnf(u115,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv3(skf3(X1))
| ssPv3(X0)
| ssPv2(X1)
| ssPv1(skf3(X1)) ) ).
cnf(u2728,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssPv4(skf3(X0))
| ssPv3(skf3(skf3(X0))) ) ).
cnf(u271,negated_conjecture,
( ~ ssPv3(skf2(skf3(X0)))
| ~ ssRr(X1,skf3(X0))
| ~ ssPv1(X0)
| ssPv1(X1)
| ssPv1(skf3(X0)) ) ).
cnf(u485,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv1(X1) ) ).
cnf(u370,negated_conjecture,
( ~ ssPv1(skf2(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv2(skf2(skf2(X0))) ) ).
cnf(u2564,negated_conjecture,
( ~ ssPv4(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv1(X0) ) ).
cnf(u6205,negated_conjecture,
( ~ ssPv2(skf3(skf2(X0)))
| ~ ssPv3(skf2(X0)) ) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X0,X2)
| ~ ssRr(X0,X1)
| ~ ssPv4(X0)
| ssPv4(X1)
| ssPv2(X2)
| ssPv1(X0) ) ).
cnf(u886,negated_conjecture,
( ~ ssPv3(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u3312,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv4(X0) ) ).
cnf(clause27,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv4(X2)
| ~ ssPv1(X1)
| ssPv4(X0)
| ssPv2(X1) ) ).
cnf(u3860,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ssPv4(skf2(X0))
| ssPv4(X0) ) ).
cnf(u113,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv3(skf3(X1))
| ssPv3(X0)
| ssPv1(X1)
| ssPv2(skf3(X1)) ) ).
cnf(u4378,negated_conjecture,
( ~ ssPv2(skf3(skf2(X0)))
| ssPv2(X0)
| ~ ssPv4(skf3(skf2(X0)))
| ssPv4(skf2(X0)) ) ).
cnf(u243,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv3(X1)
| ssPv2(skf3(X0)) ) ).
cnf(u1030,negated_conjecture,
( ~ ssPv3(skf3(skf3(X0)))
| ~ ssPv4(X0)
| ssPv1(skf3(X0))
| ssPv4(skf3(X0)) ) ).
cnf(u269,negated_conjecture,
( ~ ssPv3(skf3(skf3(X0)))
| ~ ssPv2(X0)
| ~ ssPv3(skf3(X0))
| ssPv1(skf3(X0)) ) ).
cnf(u399,negated_conjecture,
( ~ ssPv4(skf2(X0))
| ssPv1(X0)
| ssPv4(X0)
| ~ ssPv3(X0) ) ).
cnf(u1151,negated_conjecture,
( ~ ssRr(skf2(X0),X1)
| ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ~ ssPv3(X1)
| ~ ssRr(X2,skf2(X0))
| ssPv3(X0)
| ssPv1(skf2(X0)) ) ).
cnf(u498,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv1(X0)
| ~ ssPv2(skf3(X0))
| ssPv4(skf3(X0)) ) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ssPv4(X2)
| ssPv2(X1)
| ssPv4(X1) ) ).
cnf(u6422,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ssPv4(X1) ) ).
cnf(u254,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ssPv1(skf3(X0)) ) ).
cnf(u6144,negated_conjecture,
( ~ ssPv2(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X0) ) ).
cnf(u6537,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ssPv3(skf2(X0))
| ssPv2(X0) ) ).
cnf(u3818,negated_conjecture,
( ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ssPv4(X0) ) ).
cnf(clause40,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X2)
| ~ ssPv3(X1)
| ssPv1(X1) ) ).
cnf(u259,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ssPv4(X0)
| ssPv1(skf2(X0))
| ssPv2(skf2(X0)) ) ).
cnf(u1158,negated_conjecture,
( ~ ssRr(skf2(X0),X1)
| ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv3(X0)
| ~ ssPv2(X1) ) ).
cnf(u397,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(X0)
| ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv1(X1)
| ~ ssPv2(X0) ) ).
cnf(u282,negated_conjecture,
( ssPv3(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv2(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0)) ) ).
cnf(clause2,negated_conjecture,
ssRr(X0,skf2(X0)) ).
cnf(u897,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv1(X1)
| ~ ssPv4(skf2(X0)) ) ).
cnf(u140,negated_conjecture,
( ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ssPv2(X2)
| ssPv2(skf2(X0)) ) ).
cnf(u1181,negated_conjecture,
( ssPv3(skf2(skf2(X0)))
| ssPv2(skf2(X0))
| ~ ssPv3(skf2(X0))
| ssPv4(X0) ) ).
cnf(u4621,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u6423,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u4490,negated_conjecture,
( ssPv3(skf3(skf2(X0)))
| ~ ssPv1(X0)
| ssPv2(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv1(skf2(X0)) ) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X2)
| ~ ssPv2(X1)
| ssPv1(X0)
| ssPv4(X1) ) ).
cnf(u155,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv3(X0)
| ~ ssPv4(X1)
| ssPv1(skf3(X1))
| ssPv4(skf3(X1)) ) ).
cnf(u305,negated_conjecture,
( ~ ssPv1(skf2(skf3(X0)))
| ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u309,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv3(X0)
| ssPv3(skf2(skf3(X1)))
| ssPv1(X1)
| ssPv4(skf3(X1)) ) ).
cnf(u387,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv3(skf2(X0)) ) ).
cnf(u1814,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv3(skf2(X0))
| ssPv3(X0) ) ).
cnf(u541,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv4(X0)
| ssPv2(skf3(X0)) ) ).
cnf(u1063,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ssPv1(skf3(skf3(X0))) ) ).
cnf(clause52,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X2)
| ~ ssRr(X1,X3)
| ~ ssPv3(X3)
| ~ ssPv2(X1) ) ).
cnf(u130,negated_conjecture,
( ~ ssRr(X0,skf2(X1))
| ~ ssPv3(X0)
| ~ ssPv2(skf2(X1))
| ssPv1(X1)
| ssPv3(skf2(X1)) ) ).
cnf(u2697,negated_conjecture,
( ~ ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u1171,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv3(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv3(skf2(X0)) ) ).
cnf(u2981,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ssPv4(skf3(X0)) ) ).
cnf(clause31,negated_conjecture,
( ~ ssRr(X0,X2)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(X0)
| ~ ssPv4(X0)
| ssPv1(X2) ) ).
cnf(u153,negated_conjecture,
( ~ ssRr(skf3(X1),X2)
| ~ ssPv4(X0)
| ~ ssRr(X0,skf3(X1))
| ssPv3(X2)
| ssPv1(X1)
| ssPv4(skf3(X1)) ) ).
cnf(u1068,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ssPv4(X0)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u299,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv3(skf2(X0))
| ~ ssPv4(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u1198,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ssPv4(skf3(X0))
| ssPv4(skf2(skf3(X0))) ) ).
cnf(u2877,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv1(X0)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u2872,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv4(skf3(skf2(X0)))
| ~ ssPv1(X1)
| ~ ssPv2(skf2(X0))
| ssPv3(X0) ) ).
cnf(u286,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(skf3(X0))
| ~ ssPv1(X1)
| ~ ssPv4(X0) ) ).
cnf(u408,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv1(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u1191,negated_conjecture,
( ssPv3(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0)) ) ).
cnf(clause42,negated_conjecture,
( ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(X2)
| ~ ssPv1(X0)
| ~ ssPv4(X0) ) ).
cnf(u4377,negated_conjecture,
( ~ ssPv2(skf3(skf2(X0)))
| ssPv2(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u1948,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv4(skf3(skf2(X0)))
| ~ ssPv3(X1)
| ~ ssPv3(skf2(X0))
| ssPv4(X0) ) ).
cnf(u558,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u3125,negated_conjecture,
( ~ ssRr(skf3(X0),X2)
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0))
| ~ ssRr(X1,skf3(X0))
| ~ ssPv3(X1)
| ssPv2(X0)
| ~ ssPv3(X2) ) ).
cnf(u951,negated_conjecture,
( ssPv1(skf2(skf2(X0)))
| ssPv4(X0)
| ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0)) ) ).
cnf(u159,negated_conjecture,
( ~ ssRr(skf3(X1),X2)
| ~ ssPv3(X0)
| ~ ssRr(skf3(X1),X0)
| ssPv3(X2)
| ssPv1(X1)
| ssPv4(skf3(X1)) ) ).
cnf(u3106,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ssPv2(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0)) ) ).
cnf(u297,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv4(X0)
| ssPv1(X0)
| ssPv4(skf2(X0))
| ~ ssPv3(X1)
| ~ ssPv3(X0) ) ).
cnf(u3380,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(X0) ) ).
cnf(u427,negated_conjecture,
( ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv1(X0) ) ).
cnf(u6333,negated_conjecture,
( ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u1952,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv4(skf3(skf2(X0)))
| ~ ssPv1(X1)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u170,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv2(skf3(X0)) ) ).
cnf(u3129,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv2(X0) ) ).
cnf(u1369,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ssPv1(skf2(skf3(X0)))
| ssPv2(skf3(X0))
| ssPv4(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u2212,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u7237,negated_conjecture,
( ssPv3(skf3(skf2(X0)))
| ~ ssPv1(X0) ) ).
cnf(u320,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u1560,negated_conjecture,
( ssPv3(skf3(skf2(X0)))
| ssPv1(skf2(X0))
| ~ ssPv3(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u168,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv3(skf2(X0)) ) ).
cnf(u826,negated_conjecture,
( ~ ssPv4(skf2(skf3(X0)))
| ssPv2(X0)
| ssPv1(skf3(X0))
| ssPv4(skf3(X0)) ) ).
cnf(u5081,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv4(skf2(X0))
| ssPv1(skf2(skf2(X0)))
| ~ ssPv1(X1)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u2209,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv3(skf2(X0))
| ~ ssPv3(X1)
| ssPv1(skf2(X0)) ) ).
cnf(u3609,negated_conjecture,
( ssPv2(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0) ) ).
cnf(u71,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssPv4(skf3(X1))
| ssPv1(skf3(X1)) ) ).
cnf(u2236,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv4(skf2(X0))
| ssPv1(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(u7359,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv1(X0) ) ).
cnf(u1601,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv4(X0) ) ).
cnf(u1988,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ~ ssPv1(X0)
| ssPv4(X0) ) ).
cnf(u69,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssPv2(X1)
| ssPv2(skf3(X1)) ) ).
cnf(u199,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv1(X0)
| ssPv2(X1)
| ssPv1(skf2(skf3(X1)))
| ssPv3(skf3(X1)) ) ).
cnf(u6594,negated_conjecture,
( ssPv3(skf3(skf2(X0)))
| ssPv3(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(u337,negated_conjecture,
( ~ ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0) ) ).
cnf(u2176,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ssPv1(skf3(X0))
| ~ ssPv2(X0) ) ).
cnf(u80,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssPv2(skf3(X1)) ) ).
cnf(u5615,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv1(skf2(X0))
| ssPv3(X1)
| ssPv2(skf3(skf2(X0))) ) ).
cnf(u600,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ssPv4(X0)
| ~ ssPv3(X0) ) ).
cnf(u828,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ssPv2(X0)
| ssPv1(skf3(X0))
| ssPv3(skf3(X0)) ) ).
cnf(u1620,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ssPv1(skf3(X0))
| ~ ssPv1(X1)
| ~ ssPv4(skf3(X0))
| ssPv3(skf3(skf3(X0))) ) ).
cnf(u1065,negated_conjecture,
( ~ ssRr(skf3(X0),X1)
| ssPv4(X0)
| ~ ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv3(X1) ) ).
cnf(u1946,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ~ ssPv3(X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ) ).
cnf(u197,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv4(X0)
| ssPv3(X1)
| ssPv1(skf2(skf3(X1)))
| ssPv4(skf3(X1)) ) ).
cnf(u465,negated_conjecture,
( ssPv1(skf3(skf3(X0)))
| ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv2(X0)
| ~ ssPv1(skf3(X0)) ) ).
cnf(u2916,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv2(X0)
| ~ ssPv1(X0) ) ).
cnf(u86,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ~ ssRr(X1,X0)
| ~ ssPv2(X0)
| ~ ssPv4(X1)
| ssPv1(X1) ) ).
cnf(u208,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ssPv2(skf2(X0))
| ssPv1(X0)
| ssPv3(X0) ) ).
cnf(u1082,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0)) ) ).
cnf(u979,negated_conjecture,
( ~ ssPv1(skf3(skf3(X0)))
| ~ ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ssPv3(skf3(skf3(X0))) ) ).
cnf(u1382,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u109,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv3(X1) ) ).
cnf(u3920,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ~ ssPv3(X1)
| ~ ssPv1(X0)
| ssPv4(skf3(skf3(X0))) ) ).
cnf(u471,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u1746,negated_conjecture,
( ssPv3(skf2(X0))
| ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ssPv4(X0) ) ).
cnf(u4299,negated_conjecture,
( ssPv1(skf3(skf2(X0)))
| ssPv4(skf2(X0))
| ssPv2(X0) ) ).
cnf(u214,negated_conjecture,
( ~ ssPv1(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv1(X0) ) ).
cnf(u714,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(X0) ) ).
cnf(u3292,negated_conjecture,
( ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv1(X0) ) ).
cnf(u99,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv1(X1)
| ~ ssPv1(skf3(X1))
| ~ ssPv4(skf3(X1))
| ssPv4(X0) ) ).
cnf(u2670,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u383,negated_conjecture,
( ~ ssPv3(skf2(skf2(X0)))
| ssPv1(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ssPv4(skf2(skf2(X0)))
| ssPv2(skf2(skf2(X0))) ) ).
cnf(u2904,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u181,negated_conjecture,
( ~ ssPv4(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0)) ) ).
cnf(u7004,negated_conjecture,
( ssPv3(skf3(skf2(X0)))
| ssPv2(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u126,negated_conjecture,
( ~ ssRr(skf2(X1),X2)
| ~ ssRr(X0,skf2(X1))
| ~ ssPv1(X2)
| ~ ssPv1(skf2(X1))
| ssPv3(X0)
| ssPv2(X1) ) ).
cnf(u212,negated_conjecture,
( ~ ssPv1(skf2(skf2(X1)))
| ~ ssRr(X0,skf2(X1))
| ~ ssPv1(skf2(X1))
| ssPv3(X0)
| ssPv2(X1) ) ).
cnf(u3795,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(X0)
| ~ ssPv1(X0)
| ssPv3(X1)
| ssPv2(skf3(X0)) ) ).
cnf(u2526,negated_conjecture,
( ssPv2(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv1(skf2(X0)) ) ).
cnf(u3296,negated_conjecture,
( ssPv2(skf3(X0))
| ~ ssPv1(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u626,negated_conjecture,
( ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X0) ) ).
cnf(u3844,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ssPv4(X0)
| ~ ssPv1(X0) ) ).
cnf(u97,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv3(X0)
| ssPv4(X1)
| ssPv2(skf3(X1))
| ssPv3(skf3(X1)) ) ).
cnf(u227,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ssPv3(X0)
| ~ ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ) ).
cnf(u3817,negated_conjecture,
( ssPv2(skf2(skf3(X0)))
| ssPv4(skf3(X0)) ) ).
cnf(u7068,negated_conjecture,
( ~ ssPv1(skf3(skf2(X0)))
| ~ ssPv4(skf2(X0))
| ssPv3(X0) ) ).
cnf(u511,negated_conjecture,
( ssPv3(skf2(skf3(X0)))
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u3092,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ssPv2(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ssPv4(X1) ) ).
cnf(u124,negated_conjecture,
( ~ ssRr(X0,skf2(X1))
| ~ ssPv3(X0)
| ~ ssPv3(skf2(X1))
| ~ ssPv4(skf2(X1))
| ssPv4(X1) ) ).
cnf(u6910,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ssPv3(X0) ) ).
cnf(u3804,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ssPv2(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u895,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv1(X1)
| ~ ssPv4(skf2(X0))
| ssPv3(skf3(skf2(X0))) ) ).
cnf(clause36,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X2)
| ~ ssPv2(X1)
| ssPv4(X1) ) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ssPv3(X0)
| ssPv1(X2)
| ssPv2(X1) ) ).
cnf(u225,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u1004,negated_conjecture,
( ~ ssPv3(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv2(skf3(skf2(X0))) ) ).
cnf(u3819,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ssPv4(skf2(X0))
| ssPv1(X0) ) ).
cnf(u1270,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssPv4(skf2(X0)) ) ).
cnf(u266,negated_conjecture,
( ~ ssPv3(skf3(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv4(X0) ) ).
cnf(u114,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ssPv3(X0)
| ssPv1(skf2(X1))
| ssPv2(X1) ) ).
cnf(u1009,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u3440,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ssPv2(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u6389,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv2(X0) ) ).
cnf(u1023,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ssPv4(skf3(X0))
| ~ ssPv3(X0) ) ).
cnf(u3330,negated_conjecture,
( ~ ssPv2(skf3(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv4(X0) ) ).
cnf(u6420,negated_conjecture,
( ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ) ).
cnf(u139,negated_conjecture,
( ~ ssRr(skf3(X0),X1)
| ~ ssPv1(X1)
| ~ ssRr(X2,skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv2(X2)
| ssPv2(X0) ) ).
cnf(u264,negated_conjecture,
( ssPv3(skf2(skf3(X0)))
| ~ ssPv3(X0)
| ssPv1(skf2(skf3(X0)))
| ssPv4(skf3(X0)) ) ).
cnf(u793,negated_conjecture,
( ~ ssPv3(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv2(skf2(skf3(X0))) ) ).
cnf(u6903,negated_conjecture,
( ~ ssPv2(skf3(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ssPv3(X0) ) ).
cnf(u3619,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u1529,negated_conjecture,
( ssPv1(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(u1309,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv1(skf3(X0)) ) ).
cnf(u4376,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ssPv2(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u807,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv2(skf3(X0)) ) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ssPv3(X0)
| ssPv2(X2)
| ssPv1(X1) ) ).
cnf(u137,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv2(skf3(X1))
| ~ ssPv4(skf3(X1))
| ssPv3(X0)
| ssPv4(X1) ) ).
cnf(u5022,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ssPv4(X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X1)
| ssPv2(skf3(X0))
| ssPv3(skf3(skf3(X0))) ) ).
cnf(u270,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ssPv1(X1)
| ssPv1(skf3(X0)) ) ).
cnf(u9991,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ~ ssPv2(skf2(X0)) ) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ssPv1(X2)
| ssPv3(X1) ) ).
cnf(u3747,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X0)) ) ).
cnf(u542,negated_conjecture,
( ssPv3(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv4(X0) ) ).
cnf(u1056,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ssPv4(X0)
| ~ ssPv4(skf3(X0)) ) ).
cnf(u226,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ) ).
cnf(clause49,negated_conjecture,
( ~ ssRr(X1,X3)
| ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X3)
| ssPv1(X0)
| ssPv1(X1) ) ).
cnf(u143,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ssPv2(skf3(X1))
| ssPv4(X1) ) ).
cnf(u6418,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv1(X1)
| ~ ssPv4(skf2(X0))
| ssPv3(X0) ) ).
cnf(u281,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ~ ssPv3(skf3(X0)) ) ).
cnf(u255,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv4(X0) ) ).
cnf(u4643,negated_conjecture,
( ~ ssPv3(skf2(skf2(X0)))
| ssPv4(skf3(skf2(X0)))
| ~ ssPv3(X0) ) ).
cnf(u3750,negated_conjecture,
( ssPv1(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X0)) ) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv3(X2)
| ~ ssPv2(X1)
| ssPv4(X0)
| ssPv4(X1) ) ).
cnf(u2719,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv3(X0)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u154,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ssPv3(X2)
| ssPv1(skf2(X1))
| ssPv4(X1) ) ).
cnf(u3891,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u5060,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(skf2(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u795,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv4(skf2(skf3(X0))) ) ).
cnf(u409,negated_conjecture,
( ssPv4(skf3(X0))
| ssPv1(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv2(X0) ) ).
cnf(u5676,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv3(X0)
| ssPv3(skf2(X0)) ) ).
cnf(u980,negated_conjecture,
( ~ ssPv3(skf3(skf3(X0)))
| ssPv4(X0)
| ssPv2(skf3(X0))
| ssPv3(skf3(X0)) ) ).
cnf(u2616,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ssPv4(skf3(X0))
| ssPv1(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv1(X1) ) ).
cnf(u152,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv3(X1)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1)
| ssPv1(X2)
| ssPv1(X0) ) ).
cnf(u4677,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv1(X0)
| ~ ssPv4(skf2(X0)) ) ).
cnf(u3238,negated_conjecture,
( ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(X0) ) ).
cnf(u53,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv3(X1) ) ).
cnf(u6056,negated_conjecture,
( ssPv4(skf3(X0))
| ~ ssPv3(X0) ) ).
cnf(u183,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ~ ssPv4(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u2362,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u308,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv3(X0)
| ssPv3(X1)
| ssPv1(X1)
| ssPv4(skf3(X1)) ) ).
cnf(u438,negated_conjecture,
( ~ ssPv3(skf2(skf3(X0)))
| ssPv3(X0)
| ssPv1(skf2(skf3(X0)))
| ssPv4(skf3(X0)) ) ).
cnf(u1433,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv1(X0) ) ).
cnf(u3385,negated_conjecture,
( ~ ssPv2(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ssPv3(skf2(X0)) ) ).
cnf(u123,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ssPv4(skf3(X1)) ) ).
cnf(u1454,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv3(X1)
| ssPv1(X0) ) ).
cnf(u5045,negated_conjecture,
( ~ ssPv3(skf2(skf2(X0)))
| ssPv3(X0)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u321,negated_conjecture,
( ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0) ) ).
cnf(u436,negated_conjecture,
( ssPv1(skf3(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv1(X0) ) ).
cnf(u64,negated_conjecture,
( ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ) ).
cnf(u1359,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv1(skf2(skf2(X0)))
| ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv3(skf2(X0)) ) ).
cnf(u1458,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv2(X0) ) ).
cnf(u1604,negated_conjecture,
( ~ ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ~ ssPv4(X0) ) ).
cnf(u3139,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u1621,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ssPv1(skf3(X0))
| ~ ssPv3(X1)
| ssPv2(X0)
| ssPv4(skf3(skf3(X0))) ) ).
cnf(u327,negated_conjecture,
( ssPv1(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv4(skf2(X0)) ) ).
cnf(u1602,negated_conjecture,
( ssPv2(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u2900,negated_conjecture,
( ssPv1(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv1(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u70,negated_conjecture,
( ~ ssRr(X0,skf2(X1))
| ~ ssPv4(X0)
| ~ ssPv1(skf2(X1))
| ~ ssPv2(skf2(X1))
| ssPv2(X1) ) ).
cnf(u192,negated_conjecture,
( ssPv1(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ssPv1(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(u3331,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ssPv4(skf3(X0))
| ssPv2(X0) ) ).
cnf(u1366,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv4(skf3(X0))
| ssPv1(X0) ) ).
cnf(u455,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ~ ssPv3(X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv3(X1) ) ).
cnf(u3409,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv4(skf2(skf3(X0)))
| ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u348,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv1(X0)
| ssPv4(X0)
| ~ ssPv2(X0)
| ssPv3(X0) ) ).
cnf(u5075,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv4(X0) ) ).
cnf(u3294,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0) ) ).
cnf(u68,negated_conjecture,
( ~ ssRr(X0,X1)
| ssPv4(X0)
| ssPv2(skf2(X1))
| ssPv1(X1)
| ssPv2(X1) ) ).
cnf(u198,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv4(X0)
| ssPv3(skf2(X1))
| ssPv1(skf2(X1))
| ssPv4(X1) ) ).
cnf(u1370,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0) ) ).
cnf(u1985,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u1364,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ssPv1(skf2(skf3(X0)))
| ssPv4(skf2(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv2(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u83,negated_conjecture,
( ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv1(X0) ) ).
cnf(u2713,negated_conjecture,
( ssPv2(skf3(skf2(X0)))
| ssPv4(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ssPv3(skf2(X0)) ) ).
cnf(u221,negated_conjecture,
( ssPv1(skf2(skf2(X0)))
| ssPv3(X0)
| ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0)) ) ).
cnf(u453,negated_conjecture,
( ~ ssPv3(skf3(skf3(X0)))
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(skf3(skf3(X0)))
| ssPv2(skf3(skf3(X0))) ) ).
cnf(u6151,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv4(X0) ) ).
cnf(u4815,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ssPv3(skf3(X0))
| ~ ssPv3(X0) ) ).
cnf(u338,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0) ) ).
cnf(u110,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv1(X1)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(skf3(X1)) ) ).
cnf(u196,negated_conjecture,
( ssPv1(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ssPv3(skf2(X0)) ) ).
cnf(u6512,negated_conjecture,
( ~ ssPv2(skf2(X0))
| ssPv3(X0)
| ~ ssPv4(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u2510,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv4(skf3(X0)) ) ).
cnf(u1498,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(skf2(X0))
| ~ ssPv3(X1)
| ~ ssPv3(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u4833,negated_conjecture,
( ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X0) ) ).
cnf(u211,negated_conjecture,
( ssPv2(skf3(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u2696,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ssPv2(skf2(X0))
| ssPv4(skf2(X0))
| ssPv3(X0) ) ).
cnf(u3435,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ssPv2(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u1149,negated_conjecture,
( ~ ssPv2(skf2(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv3(X0) ) ).
cnf(u982,negated_conjecture,
( ssPv2(skf3(X0))
| ssPv4(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u3801,negated_conjecture,
( ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u7114,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u209,negated_conjecture,
( ssPv2(skf2(skf2(X0)))
| ~ ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv3(skf2(X0)) ) ).
cnf(u355,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf3(X0))
| ~ ssPv3(X1) ) ).
cnf(u2295,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv4(X0)
| ~ ssPv1(X0) ) ).
cnf(u98,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ssPv4(skf2(X1))
| ssPv2(X1)
| ssPv3(X1) ) ).
cnf(u4321,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv1(skf2(X0)) ) ).
cnf(u894,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X1)
| ~ ssPv4(skf2(X0))
| ssPv4(skf3(skf2(X0))) ) ).
cnf(u1007,negated_conjecture,
( ~ ssPv3(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0)) ) ).
cnf(u121,negated_conjecture,
( ~ ssRr(skf3(X1),X0)
| ~ ssPv4(X0)
| ssPv2(X1)
| ssPv1(skf3(X1))
| ssPv4(skf3(X1)) ) ).
cnf(u4332,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv2(skf2(X0))
| ~ ssPv2(X0)
| ssPv1(skf2(X0)) ) ).
cnf(u506,negated_conjecture,
( ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv3(X0) ) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ~ ssPv1(X1)
| ~ ssPv2(X1)
| ssPv1(X0)
| ssPv1(X2) ) ).
cnf(u2666,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X1) ) ).
cnf(u1916,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ssPv4(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u635,negated_conjecture,
( ~ ssPv3(skf3(skf3(X0)))
| ~ ssPv2(skf3(skf3(X0)))
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv1(X0) ) ).
cnf(u1022,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ssPv4(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(skf3(X0))) ) ).
cnf(u2949,negated_conjecture,
( ssPv1(skf2(skf3(X0)))
| ssPv1(X0)
| ~ ssPv1(skf3(X0))
| ssPv4(skf3(X0)) ) ).
cnf(u3592,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv3(X0) ) ).
cnf(u2672,negated_conjecture,
( ssPv2(skf3(X0))
| ssPv4(skf3(X0))
| ssPv2(X0) ) ).
cnf(u127,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(skf3(X0))
| ssPv4(skf3(X0)) ) ).
cnf(u1914,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ) ).
cnf(u249,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ) ).
cnf(u267,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf2(X0))
| ssPv4(X0) ) ).
cnf(clause39,negated_conjecture,
( ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(X2)
| ~ ssPv4(X0)
| ssPv1(X0) ) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1)
| ssPv4(X0)
| ssPv2(X2)
| ssPv1(X1)
| ssPv2(X1) ) ).
cnf(u4335,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv1(X0) ) ).
cnf(u272,negated_conjecture,
( ssPv1(skf3(skf3(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u4629,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ~ ssPv3(X1)
| ~ ssRr(X0,X2)
| ~ ssPv3(X2) ) ).
cnf(u5409,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv3(X1)
| ssPv1(skf2(X0))
| ssPv4(skf3(X0)) ) ).
cnf(u1543,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ssPv1(X0)
| ssPv4(skf2(X0))
| ~ ssPv4(X0) ) ).
cnf(u532,negated_conjecture,
( ssPv4(skf3(X0))
| ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X0) ) ).
cnf(u395,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(X0)
| ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssPv2(X0) ) ).
cnf(u7205,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv4(X0)
| ssPv4(skf2(X0)) ) ).
cnf(clause48,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssRr(X0,X1)
| ~ ssRr(X1,X3)
| ~ ssPv1(X3)
| ~ ssPv1(X1)
| ssPv3(X0)
| ssPv2(X2) ) ).
cnf(u9992,negated_conjecture,
( ~ ssPv3(X0)
| ~ ssPv2(X0) ) ).
cnf(u2703,negated_conjecture,
( ssPv2(skf2(skf3(X0)))
| ssPv4(skf2(skf3(X0)))
| ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u138,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ~ ssPv4(X1)
| ssPv3(X0)
| ssPv4(skf2(X1)) ) ).
cnf(u289,negated_conjecture,
( ssPv4(skf3(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u4757,negated_conjecture,
( ~ ssPv3(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv4(X0) ) ).
cnf(u1400,negated_conjecture,
( ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(X0) ) ).
cnf(u5632,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ssPv2(X0) ) ).
cnf(u393,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv1(X0)
| ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(X1) ) ).
cnf(u4766,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv4(skf2(X0))
| ssPv4(X0)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u5115,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv3(X0) ) ).
cnf(u2950,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ssPv1(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u6541,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ssPv3(skf3(X0)) ) ).
cnf(u136,negated_conjecture,
( ~ ssRr(X0,skf2(X1))
| ~ ssPv1(X0)
| ~ ssPv2(skf2(X1))
| ssPv4(X1)
| ssPv4(skf2(X1)) ) ).
cnf(u4247,negated_conjecture,
( ~ ssPv3(skf3(skf2(X0)))
| ~ ssPv3(X0)
| ssPv4(skf2(X0)) ) ).
cnf(u675,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv2(X0)
| ssPv4(X0)
| ~ ssPv1(X0)
| ssPv4(X1) ) ).
cnf(u1310,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ssPv4(X0) ) ).
cnf(clause37,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X2)
| ~ ssPv2(X1)
| ssPv4(X1) ) ).
cnf(u6562,negated_conjecture,
( ~ ssPv1(X0)
| ssPv3(X0) ) ).
cnf(u2432,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssPv2(X0) ) ).
cnf(u572,negated_conjecture,
( ~ ssPv2(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv4(skf2(skf2(X0)))
| ssPv1(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(u292,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(X0) ) ).
cnf(u3376,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0)) ) ).
cnf(u1588,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(skf2(X0))
| ~ ssPv1(X1)
| ssPv1(skf2(skf2(X0)))
| ~ ssPv4(skf2(X0))
| ssPv3(X0) ) ).
cnf(u10110,negated_conjecture,
( ~ ssPv2(skf3(X0))
| ~ ssPv3(X0) ) ).
cnf(u1837,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ssPv1(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0)) ) ).
cnf(u311,negated_conjecture,
( ~ ssPv3(skf2(skf3(X0)))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u433,negated_conjecture,
( ~ ssPv1(skf2(skf3(X0)))
| ssPv2(skf2(skf3(X0)))
| ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u2603,negated_conjecture,
( ssPv1(skf2(X0))
| ssPv4(X0)
| ssPv2(X0)
| ~ ssPv1(X0) ) ).
cnf(u54,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ) ).
cnf(u949,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ssPv4(X0)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u176,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv1(X0)
| ~ ssPv4(X1)
| ~ ssPv4(skf3(X1))
| ssPv3(skf3(skf3(X1))) ) ).
cnf(u679,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ssPv4(skf2(X0))
| ssPv2(skf2(X0))
| ssPv4(X0) ) ).
cnf(u560,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(skf3(X0)) ) ).
cnf(u1714,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ssPv1(X0)
| ssPv2(skf3(X0))
| ~ ssPv2(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u2731,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssPv4(skf3(X0))
| ssPv4(skf3(skf3(X0))) ) ).
cnf(u182,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv4(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u2889,negated_conjecture,
( ssPv4(skf3(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X0) ) ).
cnf(u5061,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv1(skf2(skf2(X0)))
| ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv2(skf2(X0))
| ssPv4(X1) ) ).
cnf(u840,negated_conjecture,
( ~ ssPv3(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv2(X0) ) ).
cnf(u2903,negated_conjecture,
( ssPv3(skf2(skf2(X0)))
| ~ ssPv1(X0)
| ssPv1(skf2(skf2(X0)))
| ssPv4(skf2(X0)) ) ).
cnf(u688,negated_conjecture,
( ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv4(X0) ) ).
cnf(u1983,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u577,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ssPv4(X0) ) ).
cnf(u180,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv4(skf3(X0)) ) ).
cnf(u2875,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ~ ssPv1(X1)
| ~ ssPv2(X0) ) ).
cnf(u962,negated_conjecture,
( ssPv2(skf3(X0))
| ssPv1(X0)
| ssPv4(skf3(X0))
| ssPv3(X0) ) ).
cnf(u67,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ssPv4(X0)
| ssPv2(X1)
| ssPv1(skf3(X1))
| ssPv2(skf3(X1)) ) ).
cnf(u205,negated_conjecture,
( ssPv1(skf3(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(u1354,negated_conjecture,
( ssPv3(skf2(skf3(X0)))
| ssPv1(skf3(X0))
| ~ ssPv3(skf3(X0))
| ssPv4(X0) ) ).
cnf(u6603,negated_conjecture,
( ssPv3(skf3(skf3(X0)))
| ~ ssPv1(X0) ) ).
cnf(u5989,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ssPv3(skf3(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ~ ssPv1(X0)
| ssPv1(X1) ) ).
cnf(u5620,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv1(skf2(X0))
| ssPv3(X1)
| ssPv2(X0) ) ).
cnf(u1352,negated_conjecture,
( ~ ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv1(skf3(X0))
| ~ ssPv1(X0) ) ).
cnf(u6231,negated_conjecture,
( ssPv2(skf3(X0))
| ssPv4(skf3(X0)) ) ).
cnf(u2659,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ssPv2(skf3(X0))
| ssPv4(skf3(X0))
| ssPv2(X1)
| ssPv2(X0) ) ).
cnf(u65,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv2(X0)
| ~ ssPv1(skf3(X1))
| ~ ssPv2(skf3(X1))
| ssPv3(X1) ) ).
cnf(u844,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv4(skf2(skf3(X0))) ) ).
cnf(u195,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ssPv3(X0) ) ).
cnf(u2005,negated_conjecture,
( ~ ssPv3(skf3(skf2(X0)))
| ssPv4(X0)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u1325,negated_conjecture,
( ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv4(X0)
| ssPv2(X0) ) ).
cnf(u4706,negated_conjecture,
( ssPv1(skf2(skf3(X0)))
| ssPv3(X0)
| ssPv4(skf3(X0))
| ssPv2(skf3(X0)) ) ).
cnf(u1103,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv3(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(X1) ) ).
cnf(u2890,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv1(X0) ) ).
cnf(u3665,negated_conjecture,
( ~ ssPv2(skf2(skf3(X0)))
| ~ ssPv1(X0)
| ssPv3(skf3(X0)) ) ).
cnf(u92,negated_conjecture,
( ~ ssRr(X0,skf3(X1))
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssPv2(skf3(X1)) ) ).
cnf(u222,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X0))
| ssPv2(X1)
| ssPv2(X0) ) ).
cnf(u5997,negated_conjecture,
( ~ ssRr(X1,X0)
| ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X1)
| ~ ssPv2(X0) ) ).
cnf(u3789,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv1(skf2(X0))
| ssPv3(X1)
| ssPv2(X0) ) ).
cnf(u3608,negated_conjecture,
( ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0) ) ).
cnf(u193,negated_conjecture,
( ssPv1(skf2(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u477,negated_conjecture,
( ssPv1(skf3(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0) ) ).
cnf(u5192,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv3(X0) ) ).
cnf(u9425,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv3(X0) ) ).
cnf(u220,negated_conjecture,
( ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv2(X0) ) ).
cnf(u885,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ssPv1(X0)
| ssPv3(skf2(X0))
| ~ ssPv4(skf2(X0))
| ~ ssPv2(skf2(X0)) ) ).
cnf(u388,negated_conjecture,
( ~ ssRr(skf2(X0),X1)
| ssPv1(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv4(X1)
| ~ ssPv4(skf2(X0)) ) ).
cnf(u991,negated_conjecture,
( ssPv4(skf2(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv2(X0) ) ).
cnf(u105,negated_conjecture,
( ~ ssRr(skf3(X0),X1)
| ~ ssPv4(skf3(X0))
| ssPv4(X1)
| ssPv2(X0)
| ssPv1(skf3(X0)) ) ).
cnf(u6516,negated_conjecture,
( ~ ssRr(X1,skf3(X0))
| ssPv3(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv2(X1)
| ssPv2(X0) ) ).
cnf(u5605,negated_conjecture,
( ~ ssPv2(skf2(skf2(X0)))
| ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(u360,negated_conjecture,
( ~ ssPv4(skf3(skf3(X0)))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ) ).
cnf(u2423,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ) ).
cnf(u490,negated_conjecture,
( ssPv2(skf3(skf3(X0)))
| ~ ssPv1(skf3(X0))
| ssPv3(skf3(skf3(X0)))
| ~ ssPv1(X0) ) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ssPv3(X1)
| ssPv1(X0)
| ssPv4(X0) ) ).
cnf(u210,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ssPv2(skf3(X0))
| ssPv4(X0) ) ).
cnf(u2777,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ssPv2(skf3(X0))
| ssPv2(X0) ) ).
cnf(u111,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssPv4(X1) ) ).
cnf(u7264,negated_conjecture,
( ~ ssPv2(skf3(skf2(X0)))
| ~ ssPv1(X0)
| ~ ssPv2(skf2(X0)) ) ).
cnf(u366,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv3(skf2(X0)) ) ).
cnf(u122,negated_conjecture,
( ~ ssRr(X1,X0)
| ~ ssPv4(X0)
| ssPv2(skf2(X1))
| ssPv1(X1)
| ssPv4(X1) ) ).
cnf(u2778,negated_conjecture,
( ssPv4(skf3(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ~ ssPv3(X0) ) ).
cnf(u638,negated_conjecture,
( ~ ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X1)
| ~ ssPv2(X0) ) ).
cnf(u4352,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv1(X1)
| ssPv1(skf2(X0))
| ~ ssPv4(skf2(X0))
| ssPv3(X0) ) ).
cnf(u6535,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ssPv3(skf3(X0))
| ssPv2(X0) ) ).
cnf(u1655,negated_conjecture,
( ~ ssRr(skf3(X0),X1)
| ssPv2(X0)
| ~ ssPv3(skf3(X0))
| ~ ssPv3(X1)
| ~ ssPv2(skf3(X0)) ) ).
cnf(u516,negated_conjecture,
( ssPv3(skf3(skf3(X0)))
| ~ ssPv3(skf3(X0))
| ssPv1(X0)
| ssPv2(skf3(X0)) ) ).
cnf(u507,negated_conjecture,
( ssPv3(skf3(skf2(X0)))
| ~ ssPv3(skf2(X0))
| ~ ssPv1(skf2(X0))
| ssPv1(X0) ) ).
cnf(u1763,negated_conjecture,
( ~ ssPv3(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ) ).
cnf(u120,negated_conjecture,
( ~ ssRr(X0,X1)
| ~ ssPv4(X0)
| ssPv4(skf2(X1))
| ssPv2(X1)
| ssPv4(X1) ) ).
cnf(u250,negated_conjecture,
( ssPv4(skf2(skf2(X0)))
| ~ ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ) ).
cnf(u6540,negated_conjecture,
( ~ ssRr(X0,X1)
| ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(X1) ) ).
cnf(u1769,negated_conjecture,
( ~ ssPv1(skf2(X0))
| ~ ssPv2(skf2(X0))
| ~ ssPv2(X0) ) ).
cnf(u6533,negated_conjecture,
( ssPv4(skf2(X0))
| ~ ssPv1(X0) ) ).
cnf(u1152,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ~ ssPv3(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(skf2(X0)) ) ).
cnf(clause23,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1)
| ~ ssPv2(X1)
| ssPv4(X2)
| ssPv4(X1) ) ).
cnf(u2729,negated_conjecture,
( ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv4(skf3(X0)) ) ).
cnf(u2060,negated_conjecture,
( ~ ssRr(X1,skf2(X0))
| ssPv2(skf2(X0))
| ~ ssPv1(X1)
| ~ ssPv3(X0)
| ~ ssPv4(skf2(X0))
| ssPv3(skf3(skf2(X0))) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN797-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n008.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 16:57:25 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.30/2.09 % (2394512)Input is clausal, will run a generic CNF schedule.
% 10.30/2.09 % (2394522)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=978847657:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.30/2.09 % (2394520)lrs+10_1_sil=8000:sp=occurrence:random_seed=3518237041:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.30/2.09 % (2394517)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3233618351:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.30/2.09 % (2394518)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2470385647:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.30/2.09 % (2394519)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3928493386:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.30/2.09 % (2394521)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1133566670:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.30/2.09 % (2394523)dis-21_1_sil=8000:lcm=predicate:random_seed=2903696311:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.30/2.09 % (2394522)Instruction limit reached!
% 10.30/2.09 % (2394522)------------------------------
% 10.30/2.09 % (2394522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.09 % (2394522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.09 % (2394522)CaDiCaL version: 2.1.3
% 10.30/2.09 % (2394522)Termination reason: Instruction limit
% 10.30/2.09 % (2394522)Termination phase: Saturation
% 10.30/2.09 % (2394522)Time elapsed: 0.057 s
% 10.30/2.09 % (2394522)Peak memory usage: 88 MB
% 10.30/2.09 % (2394522)Instructions burned: 183 (million)
% 10.30/2.09 % (2394520)Instruction limit reached!
% 10.30/2.09 % (2394520)------------------------------
% 10.30/2.09 % (2394520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.09 % (2394520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.09 % (2394520)CaDiCaL version: 2.1.3
% 10.30/2.09 % (2394520)Termination reason: Instruction limit
% 10.30/2.09 % (2394520)Termination phase: Saturation
% 10.30/2.09 % (2394520)Time elapsed: 0.063 s
% 10.30/2.09 % (2394520)Peak memory usage: 88 MB
% 10.30/2.09 % (2394520)Instructions burned: 109 (million)
% 10.30/2.09 % (2394523)Instruction limit reached!
% 10.30/2.09 % (2394523)------------------------------
% 10.30/2.09 % (2394523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.09 % (2394523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.09 % (2394523)CaDiCaL version: 2.1.3
% 10.30/2.09 % (2394523)Termination reason: Instruction limit
% 10.30/2.09 % (2394523)Termination phase: Saturation
% 10.30/2.09 % (2394523)Time elapsed: 0.057 s
% 10.30/2.09 % (2394523)Peak memory usage: 87 MB
% 10.30/2.09 % (2394523)Instructions burned: 117 (million)
% 10.30/2.09 % (2394521)Instruction limit reached!
% 10.30/2.09 % (2394521)------------------------------
% 10.30/2.09 % (2394521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.09 % (2394521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.09 % (2394521)CaDiCaL version: 2.1.3
% 10.30/2.09 % (2394521)Termination reason: Instruction limit
% 10.30/2.09 % (2394521)Termination phase: Saturation
% 10.30/2.09 % (2394521)Time elapsed: 0.066 s
% 10.30/2.09 % (2394521)Peak memory usage: 87 MB
% 10.30/2.09 % (2394521)Instructions burned: 115 (million)
% 10.30/2.09 % (2394531)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3642047053:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.30/2.09 % (2394531)Refutation not found, incomplete strategy
% 10.30/2.09 % (2394531)------------------------------
% 10.30/2.09 % (2394531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.09 % (2394531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.09 % (2394531)CaDiCaL version: 2.1.3
% 10.30/2.09 % (2394531)Termination reason: Refutation not found, incomplete strategy
% 10.30/2.09 % (2394531)Time elapsed: 0.040 s
% 10.30/2.09 % (2394531)Peak memory usage: 88 MB
% 10.30/2.09 % (2394531)Instructions burned: 134 (million)
% 10.30/2.09 % (2394532)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1950832033:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 12.01/2.45 % (2394532)Refutation not found, incomplete strategy
% 12.01/2.45 % (2394532)------------------------------
% 12.01/2.45 % (2394532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394532)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394532)Termination reason: Refutation not found, incomplete strategy
% 12.01/2.45 % (2394532)Time elapsed: 0.008 s
% 12.01/2.45 % (2394532)Peak memory usage: 88 MB
% 12.01/2.45 % (2394532)Instructions burned: 14 (million)
% 12.01/2.45 % (2394533)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3480881668:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 12.01/2.45 % (2394534)lrs+10_64_to=lpo:sil=8000:random_seed=2353914128:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 12.01/2.45 % (2394531)------------------------------
% 12.01/2.45 % (2394531)------------------------------
% 12.01/2.45 % (2394533)Instruction limit reached!
% 12.01/2.45 % (2394533)------------------------------
% 12.01/2.45 % (2394533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394533)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394533)Termination reason: Instruction limit
% 12.01/2.45 % (2394533)Termination phase: Saturation
% 12.01/2.45 % (2394533)Time elapsed: 0.125 s
% 12.01/2.45 % (2394533)Peak memory usage: 88 MB
% 12.01/2.45 % (2394533)Instructions burned: 220 (million)
% 12.01/2.45 % (2394534)Instruction limit reached!
% 12.01/2.45 % (2394534)------------------------------
% 12.01/2.45 % (2394534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394534)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394534)Termination reason: Instruction limit
% 12.01/2.45 % (2394534)Termination phase: Saturation
% 12.01/2.45 % (2394534)Time elapsed: 0.120 s
% 12.01/2.45 % (2394534)Peak memory usage: 87 MB
% 12.01/2.45 % (2394534)Instructions burned: 126 (million)
% 12.01/2.45 % (2394539)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3170381365:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 12.01/2.45 % (2394532)------------------------------
% 12.01/2.45 % (2394532)------------------------------
% 12.01/2.45 % (2394540)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1156151993:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 12.01/2.45 % (2394539)Instruction limit reached!
% 12.01/2.45 % (2394539)------------------------------
% 12.01/2.45 % (2394539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394539)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394539)Termination reason: Instruction limit
% 12.01/2.45 % (2394539)Termination phase: Saturation
% 12.01/2.45 % (2394539)Time elapsed: 0.056 s
% 12.01/2.45 % (2394539)Peak memory usage: 88 MB
% 12.01/2.45 % (2394539)Instructions burned: 195 (million)
% 12.01/2.45 % (2394541)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=565106148:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 12.01/2.45 % (2394545)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=872010703:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 12.01/2.45 % (2394540)Instruction limit reached!
% 12.01/2.45 % (2394540)------------------------------
% 12.01/2.45 % (2394540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394540)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394540)Termination reason: Instruction limit
% 12.01/2.45 % (2394540)Termination phase: Saturation
% 12.01/2.45 % (2394540)Time elapsed: 0.099 s
% 12.01/2.45 % (2394540)Peak memory usage: 88 MB
% 12.01/2.45 % (2394540)Instructions burned: 157 (million)
% 12.01/2.45 % (2394545)Instruction limit reached!
% 12.01/2.45 % (2394545)------------------------------
% 12.01/2.45 % (2394545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394545)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394545)Termination reason: Instruction limit
% 12.01/2.45 % (2394545)Termination phase: Saturation
% 12.01/2.45 % (2394545)Time elapsed: 0.050 s
% 12.01/2.45 % (2394545)Peak memory usage: 88 MB
% 12.01/2.45 % (2394545)Instructions burned: 107 (million)
% 12.01/2.45 % (2394543)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2731162936:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 12.01/2.45 % (2394543)Refutation not found, incomplete strategy
% 12.01/2.45 % (2394543)------------------------------
% 12.01/2.45 % (2394543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394543)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394543)Termination reason: Refutation not found, incomplete strategy
% 12.01/2.45 % (2394543)Time elapsed: 0.006 s
% 12.01/2.45 % (2394543)Peak memory usage: 88 MB
% 12.01/2.45 % (2394543)Instructions burned: 5 (million)
% 12.01/2.45 % (2394518)Refutation not found, incomplete strategy
% 12.01/2.45 % (2394518)------------------------------
% 12.01/2.45 % (2394518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394518)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394518)Termination reason: Refutation not found, incomplete strategy
% 12.01/2.45 % (2394518)Time elapsed: 0.618 s
% 12.01/2.45 % (2394518)Peak memory usage: 128 MB
% 12.01/2.45 % (2394518)Instructions burned: 870 (million)
% 12.01/2.45 % (2394561)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1126294280:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 12.01/2.45 % (2394561)Refutation not found, incomplete strategy
% 12.01/2.45 % (2394561)------------------------------
% 12.01/2.45 % (2394561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394561)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394561)Termination reason: Refutation not found, incomplete strategy
% 12.01/2.45 % (2394561)Time elapsed: 0.003 s
% 12.01/2.45 % (2394561)Peak memory usage: 87 MB
% 12.01/2.45 % (2394561)Instructions burned: 4 (million)
% 12.01/2.45 % (2394564)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2468333226:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 12.01/2.45 % (2394543)------------------------------
% 12.01/2.45 % (2394543)------------------------------
% 12.01/2.45 % (2394518)------------------------------
% 12.01/2.45 % (2394518)------------------------------
% 12.01/2.45 % (2394561)------------------------------
% 12.01/2.45 % (2394561)------------------------------
% 12.01/2.45 % (2394580)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2713729542:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 12.01/2.45 % (2394579)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3765386018:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 12.01/2.45 % (2394581)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1254178256:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 12.01/2.45 % (2394519)Refutation not found, incomplete strategy
% 12.01/2.45 % (2394519)------------------------------
% 12.01/2.45 % (2394519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394519)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394519)Termination reason: Refutation not found, incomplete strategy
% 12.01/2.45 % (2394519)Time elapsed: 1.226 s
% 12.01/2.45 % (2394519)Peak memory usage: 130 MB
% 12.01/2.45 % (2394519)Instructions burned: 1496 (million)
% 12.01/2.45 % (2394517)First to succeed.
% 12.01/2.45 % (2394517)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2394512"
% 12.01/2.45 % (2394579)Instruction limit reached!
% 12.01/2.45 % (2394579)------------------------------
% 12.01/2.45 % (2394579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394579)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394579)Termination reason: Instruction limit
% 12.01/2.45 % (2394579)Termination phase: Saturation
% 12.01/2.45 % (2394579)Time elapsed: 0.115 s
% 12.01/2.45 % (2394579)Peak memory usage: 88 MB
% 12.01/2.45 % (2394579)Instructions burned: 134 (million)
% 12.01/2.45 % (2394581)Instruction limit reached!
% 12.01/2.45 % (2394581)------------------------------
% 12.01/2.45 % (2394581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394581)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394581)Termination reason: Instruction limit
% 12.01/2.45 % (2394581)Termination phase: Saturation
% 12.01/2.45 % (2394581)Time elapsed: 0.121 s
% 12.01/2.45 % (2394581)Peak memory usage: 88 MB
% 12.01/2.45 % (2394581)Instructions burned: 192 (million)
% 12.01/2.45 % (2394580)Instruction limit reached!
% 12.01/2.45 % (2394580)------------------------------
% 12.01/2.45 % (2394580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394580)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394580)Termination reason: Instruction limit
% 12.01/2.45 % (2394580)Termination phase: Saturation
% 12.01/2.45 % (2394580)Time elapsed: 0.219 s
% 12.01/2.45 % (2394580)Peak memory usage: 89 MB
% 12.01/2.45 % (2394580)Instructions burned: 501 (million)
% 12.01/2.45 % (2394591)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1174478417:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 12.01/2.45 % (2394592)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2018219990:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 12.01/2.45 % (2394519)------------------------------
% 12.01/2.45 % (2394519)------------------------------
% 12.01/2.45 % (2394593)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3918595738:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 12.01/2.45 % (2394591)Instruction limit reached!
% 12.01/2.45 % (2394591)------------------------------
% 12.01/2.45 % (2394591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394591)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394591)Termination reason: Instruction limit
% 12.01/2.45 % (2394591)Termination phase: Saturation
% 12.01/2.45 % (2394591)Time elapsed: 0.128 s
% 12.01/2.45 % (2394591)Peak memory usage: 90 MB
% 12.01/2.45 % (2394591)Instructions burned: 265 (million)
% 12.01/2.45 % (2394592)Instruction limit reached!
% 12.01/2.45 % (2394592)------------------------------
% 12.01/2.45 % (2394592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.45 % (2394592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.45 % (2394592)CaDiCaL version: 2.1.3
% 12.01/2.45 % (2394592)Termination reason: Instruction limit
% 12.01/2.45 % (2394592)Termination phase: Saturation
% 12.01/2.45 % (2394592)Time elapsed: 0.133 s
% 12.01/2.45 % (2394592)Peak memory usage: 88 MB
% 12.01/2.45 % (2394592)Instructions burned: 156 (million)
% 12.01/2.45 % SZS status Satisfiable for theBenchmark
% 12.01/2.45 % SZS output start Saturation.
% See solution above
% 13.36/2.75 % SZS output start Definitions and Model Updates.
% 13.36/2.75 % SZS output end Definitions and Model Updates.
% 13.36/2.75 % (2394517)------------------------------
% 13.36/2.75 % (2394517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.36/2.75 % (2394517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.75 % (2394517)CaDiCaL version: 2.1.3
% 13.36/2.75 % (2394517)Termination reason: Satisfiable
% 13.36/2.75 % (2394517)Time elapsed: 1.247 s
% 13.36/2.75 % (2394517)Peak memory usage: 131 MB
% 13.36/2.75 % (2394517)Instructions burned: 1453 (million)
% 13.36/2.75 % (2394517)------------------------------
% 13.36/2.75 % (2394517)------------------------------
% 13.36/2.75 % (2394512)Success in time 1.799 s
% 13.36/2.75 % Vampire exiting
%------------------------------------------------------------------------------