Vampire---5.0.1.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : NLP027-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n017.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 12:07:03 PM UTC 2026

% Result   : Satisfiable 2.77s 1.36s
% Output   : Saturation 4.06s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u58,negated_conjecture,
    ssSkC0 ).

cnf(u52,negated_conjecture,
    ( ~ young(X0,skf14(X0,X2))
    | ~ actual_world(X0)
    | ~ table(X0,X3)
    | ~ ssSkP2(X3,X1,X0)
    | ~ guy(X0,skf14(X0,X2))
    | ~ three(X0,X1)
    | ~ group(X0,X1) ) ).

cnf(u56,negated_conjecture,
    ( ~ table(X0,X2)
    | member(X0,skf14(X0,X1),X1)
    | ~ actual_world(X0)
    | ~ three(X0,X1)
    | ~ ssSkP2(X2,X1,X0)
    | ~ group(X0,X1) ) ).

cnf(u61,negated_conjecture,
    ( ~ actual_world(X0)
    | member(X0,skf34(X0,X1),X1)
    | ~ group(X0,X1)
    | ~ ssSkP3(X1,X0) ) ).

cnf(u69,negated_conjecture,
    ( hamburger(skc5,X0)
    | ~ member(skc5,X0,skc6) ) ).

cnf(u77,negated_conjecture,
    ( guy(skc63,X0)
    | ~ member(skc63,X0,skc64) ) ).

cnf(u287,negated_conjecture,
    ~ ssSkP2(skc65,skc64,skc63) ).

cnf(u85,negated_conjecture,
    ssSkP3(skc6,skc5) ).

cnf(u89,negated_conjecture,
    group(skc5,skc6) ).

cnf(u97,negated_conjecture,
    group(skc63,skc64) ).

cnf(u110,negated_conjecture,
    member(skc63,skf34(skc63,skc64),skc64) ).

cnf(u131,negated_conjecture,
    ( member(skc5,skf34(skc5,skf29(skc5,X2)),skf29(skc5,X2))
    | member(skc5,skf31(skc5,skf29(skc5,X2)),skf29(skc5,X2)) ) ).

cnf(u134,negated_conjecture,
    ( member(skc5,skf31(skc5,X1),X1)
    | ~ member(skc5,X0,X1) ) ).

cnf(u138,negated_conjecture,
    ( member(skc63,skf34(skc63,skf29(skc63,X2)),skf29(skc63,X2))
    | member(skc63,skf31(skc63,skf29(skc63,X2)),skf29(skc63,X2)) ) ).

cnf(u141,negated_conjecture,
    ( member(skc63,skf31(skc63,X1),X1)
    | ~ member(skc63,X0,X1) ) ).

cnf(u149,negated_conjecture,
    ( member(skc5,skf34(skc5,skf24(skc5,X3,X4)),skf24(skc5,X3,X4))
    | member(skc5,skf31(skc5,skf24(skc5,X3,X4)),skf24(skc5,X3,X4)) ) ).

cnf(u152,negated_conjecture,
    ( member(skc5,skf26(skc5,X2,X1),X1)
    | ~ member(skc5,X0,X1) ) ).

cnf(u195,negated_conjecture,
    ( member(skc63,skf26(skc63,X4,X3),X3)
    | ~ member(skc63,X2,X3) ) ).

cnf(u210,negated_conjecture,
    ( member(skc63,skf34(skc63,skf24(skc63,X3,X4)),skf24(skc63,X3,X4))
    | member(skc63,skf31(skc63,skf24(skc63,X3,X4)),skf24(skc63,X3,X4)) ) ).

cnf(u228,negated_conjecture,
    group(skc5,skf29(skc5,X1)) ).

cnf(u235,negated_conjecture,
    member(skc5,skf34(skc5,skc6),skc6) ).

cnf(u250,negated_conjecture,
    ~ member(skc5,skf27(skc5,X4),skc6) ).

cnf(u262,negated_conjecture,
    ( ~ three(skc63,X0)
    | ~ group(skc63,X0)
    | ~ ssSkP2(skc65,X0,skc63)
    | member(skc63,skf14(skc63,X0),X0) ) ).

cnf(u282,negated_conjecture,
    ( ~ ssSkP2(skc65,skf29(skc63,X0),skc63)
    | member(skc63,skf14(skc63,skf29(skc63,X0)),skf29(skc63,X0))
    | ~ group(skc63,skf29(skc63,X0)) ) ).

cnf(u297,negated_conjecture,
    ( ~ member(skc63,skf14(skc63,X4),skf29(skc63,X5))
    | ~ member(skc63,skf14(skc63,X4),skc64) ) ).

cnf(u305,negated_conjecture,
    ( ~ group(skc63,skf29(skc63,X2))
    | member(skc63,skf14(skc63,skf29(skc63,X2)),skf29(skc63,X2)) ) ).

cnf(u308,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X1,skc63)
    | member(skc63,skf27(skc63,X1),X1)
    | ~ group(skc63,X1) ) ).

cnf(u320,negated_conjecture,
    ( ~ ssSkP2(skf19(skc5,X1,X2),skf29(skc5,X0),skc5)
    | ~ group(skc5,skf29(skc5,X0))
    | member(skc5,skf14(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ) ).

cnf(u327,negated_conjecture,
    ( member(skc63,skf14(skc63,skf29(skc63,X0)),skf29(skc63,X0))
    | ~ group(skc63,skf29(skc63,X0))
    | ~ ssSkP2(skf19(skc63,X1,X2),skf29(skc63,X0),skc63) ) ).

cnf(u346,negated_conjecture,
    member(skc63,skf14(skc63,skf29(skc63,X0)),skf29(skc63,X0)) ).

cnf(u367,negated_conjecture,
    ( ~ ssSkP0(skf19(skc5,X1,X2),skf26(skc5,skf19(skc5,X1,X2),X3),X4,skc5)
    | member(skc5,skf27(skc5,X4),X4)
    | ~ group(skc5,X4) ) ).

cnf(u380,negated_conjecture,
    member(skc5,skf17(skc6,skc5,X0,X1),skc6) ).

cnf(u391,negated_conjecture,
    ( ~ member(skc5,skf14(skc5,X5),skf29(skc5,X6))
    | ~ member(skc5,skf14(skc5,X5),skf29(skc5,X9)) ) ).

cnf(u413,negated_conjecture,
    ~ member(skc5,skf27(skc5,X7),skf24(skc5,X8,X9)) ).

cnf(u422,negated_conjecture,
    ( ~ member(skc63,skf32(skc63,X5),skf29(skc63,X6))
    | ~ member(skc63,skf32(skc63,X5),skc64) ) ).

cnf(u425,negated_conjecture,
    ssSkP3(X2,skc63) ).

cnf(u440,negated_conjecture,
    group(skc63,skf29(skc63,X2)) ).

cnf(u454,negated_conjecture,
    member(skc63,skf34(skc63,skf29(skc63,X0)),skf29(skc63,X0)) ).

cnf(u480,negated_conjecture,
    ( ~ ssSkP2(skf19(skc63,X0,X1),skf29(skc63,X2),skc63)
    | ~ group(skc63,skf29(skc63,X2)) ) ).

cnf(u487,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3),X4,skc63)
    | member(skc63,skf27(skc63,X4),X4)
    | ~ group(skc63,X4) ) ).

cnf(u497,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3),X4,skc63)
    | ~ group(skc63,X4) ) ).

cnf(u513,negated_conjecture,
    member(skc63,skf17(skf29(skc63,X0),skc63,X1,X2),skf29(skc63,X0)) ).

cnf(u521,negated_conjecture,
    member(skc63,skf26(skc63,skf19(skc63,X0,X1),skf29(skc63,X2)),skf29(skc63,X2)) ).

cnf(u551,negated_conjecture,
    ( ~ group(skc5,X11)
    | member(skc5,skf34(skc5,X11),X11) ) ).

cnf(u581,negated_conjecture,
    ( ~ ssSkP0(X18,X19,X20,skc63)
    | ~ member(skc63,X21,X20) ) ).

cnf(u584,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X0,X1),X2,X3,skc63)
    | ~ ssSkP0(X7,X8,X9,skc63)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X5),X6,skc63)
    | ~ group(skc63,X4)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X5)),X6)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X5)),X9)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X5)),X3) ) ).

cnf(u588,negated_conjecture,
    ( ~ ssSkP0(X18,X19,X20,skc5)
    | ~ member(skc5,X21,X20) ) ).

cnf(u606,negated_conjecture,
    ( ~ ssSkP0(X2,skf26(skc63,X2,X5),X6,skc63)
    | ~ group(skc63,X6)
    | ~ member(skc63,X1,X10)
    | ~ member(skc63,X0,skf24(skc63,X1,X2)) ) ).

cnf(u652,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X0,X1),X4,X5,skc63)
    | ~ ssSkP0(X13,X14,X15,skc63)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X12,skc63)
    | ~ ssSkP0(skf19(skc63,X0,X1),X10,X11,skc63)
    | ~ ssSkP0(X6,X7,X8,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X11)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X12)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X5)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X8)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X15) ) ).

cnf(u656,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X2,X3),X4,X5,skc63)
    | ~ group(skc63,X12)
    | ~ member(skc63,X1,X16)
    | ~ ssSkP0(X0,skf26(skc63,X0,X11),X12,skc63)
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6)),X5)
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6)),X7)
    | ~ group(skc63,X8)
    | ~ ssSkP0(skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6),X7,skc63) ) ).

cnf(u661,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X3,X4),X5,X6,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X15)
    | ~ ssSkP0(X13,X14,X15,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X12)
    | ~ ssSkP0(X0,X1,X12,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X11)
    | ~ ssSkP0(X0,X10,X11,skc63)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7)),X6)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7)),X2)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7)),X8)
    | ~ group(skc63,X9)
    | ~ ssSkP0(skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7),X8,skc63) ) ).

cnf(u665,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X15)
    | ~ ssSkP0(X13,X14,X15,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X12)
    | ~ ssSkP0(skf19(skc63,X0,X1),X2,X12,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X11)
    | ~ ssSkP0(skf19(skc63,X0,X1),X10,X11,skc63)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X3)
    | ~ group(skc63,X9)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7),X8,skc63)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X6)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X8) ) ).

cnf(u711,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X4),X5,skc63)
    | ~ group(skc63,X10)
    | ~ member(skc63,X1,X14)
    | ~ ssSkP0(X0,skf26(skc63,X0,X9),X10,skc63)
    | ~ member(skc63,skf17(X6,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X4)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X6,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X4)),X5)
    | ~ group(skc63,X6) ) ).

cnf(u716,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5),X6,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X13)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X10)
    | ~ ssSkP0(X0,X1,X10,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X9)
    | ~ ssSkP0(X0,X8,X9,skc63)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X2)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X6)
    | ~ group(skc63,X7) ) ).

cnf(u720,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X13)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X10)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X10,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X9)
    | ~ ssSkP0(skf19(skc63,X0,X1),X8,X9,skc63)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X6) ) ).

cnf(u731,negated_conjecture,
    ( ~ ssSkP0(X8,X9,X10,skc63)
    | ~ ssSkP0(skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3),X7,skc63)
    | ~ ssSkP0(skf19(skc63,X1,X2),X5,X6,skc63)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X7)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X10)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X6)
    | ~ group(skc63,X0)
    | ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4) ) ).

cnf(u740,negated_conjecture,
    ( member(skc63,skf17(X4,skc63,X5,X6),X4)
    | ~ member(skc63,skf17(skf29(skc63,X0),skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4) ) ).

cnf(u796,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X2,X3),X4,X5,skc63)
    | ~ group(skc63,X18)
    | ~ member(skc63,X1,X22)
    | ~ ssSkP0(X0,skf26(skc63,X0,X17),X18,skc63)
    | ~ member(skc63,skf17(X13,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X9)),X8)
    | ~ group(skc63,X14)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X9)),X13)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X9)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X9)),X5)
    | ~ member(skc63,skf17(X13,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X9)),X10)
    | ~ member(skc63,skf17(X13,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X9)),X12)
    | ~ ssSkP0(skf19(skc63,X2,X3),X11,X12,skc63)
    | ~ ssSkP0(skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X9),X10,skc63)
    | ~ ssSkP0(X6,X7,X8,skc63) ) ).

cnf(u801,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X3,X4),X5,X6,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X21)
    | ~ ssSkP0(X19,X20,X21,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X18)
    | ~ ssSkP0(X0,X1,X18,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X17)
    | ~ ssSkP0(X0,X16,X17,skc63)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X10)),X9)
    | ~ group(skc63,X15)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X10)),X14)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X10)),X2)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X10)),X6)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X10)),X11)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X10)),X13)
    | ~ ssSkP0(skf19(skc63,X3,X4),X12,X13,skc63)
    | ~ ssSkP0(skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X10),X11,skc63)
    | ~ ssSkP0(X7,X8,X9,skc63) ) ).

cnf(u805,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X0,X1),X4,X5,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X21)
    | ~ ssSkP0(X19,X20,X21,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X18)
    | ~ ssSkP0(skf19(skc63,X0,X1),X2,X18,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X17)
    | ~ ssSkP0(skf19(skc63,X0,X1),X16,X17,skc63)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X9)),X8)
    | ~ group(skc63,X15)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X9)),X14)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X9)),X13)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X9)),X5)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X9)),X10)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X9)),X3)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X9),X10,skc63)
    | ~ ssSkP0(X6,X7,X8,skc63) ) ).

cnf(u809,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X0,X1),X4,X5,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X21)
    | ~ ssSkP0(X19,X20,X21,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X18)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X18,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X17)
    | ~ ssSkP0(skf19(skc63,X0,X1),X16,X17,skc63)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X8)
    | ~ group(skc63,X15)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X14)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X13)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X5)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X10)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ ssSkP0(skf19(skc63,X0,X1),X9,X10,skc63)
    | ~ ssSkP0(X6,X7,X8,skc63) ) ).

cnf(u813,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X2,X3),X4,X5,skc63)
    | ~ group(skc63,X18)
    | ~ member(skc63,X1,X22)
    | ~ ssSkP0(X0,skf26(skc63,X0,X17),X18,skc63)
    | ~ member(skc63,skf17(X13,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6)),skf24(skc63,X1,X0))
    | ~ group(skc63,X14)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6)),X13)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6)),X12)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6)),X5)
    | ~ member(skc63,skf17(X13,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6)),X7)
    | ~ member(skc63,skf17(X13,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6)),X9)
    | ~ ssSkP0(X10,X11,X12,skc63)
    | ~ ssSkP0(skf19(skc63,X2,X3),X8,X9,skc63)
    | ~ ssSkP0(skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X6),X7,skc63) ) ).

cnf(u818,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X3,X4),X5,X6,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X21)
    | ~ ssSkP0(X19,X20,X21,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X18)
    | ~ ssSkP0(X0,X1,X18,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X17)
    | ~ ssSkP0(X0,X16,X17,skc63)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7)),X2)
    | ~ group(skc63,X15)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7)),X14)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7)),X13)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7)),X6)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7)),X8)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7)),X10)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ ssSkP0(skf19(skc63,X3,X4),X9,X10,skc63)
    | ~ ssSkP0(skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X7),X8,skc63) ) ).

cnf(u822,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X21)
    | ~ ssSkP0(X19,X20,X21,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X18)
    | ~ ssSkP0(skf19(skc63,X0,X1),X2,X18,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X17)
    | ~ ssSkP0(skf19(skc63,X0,X1),X16,X17,skc63)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X3)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7),X8,skc63)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X6)
    | ~ group(skc63,X15)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X14)
    | ~ member(skc63,skf17(X15,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X13)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X8)
    | ~ member(skc63,skf17(X14,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X10)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ ssSkP0(skf19(skc63,X0,X1),X9,X10,skc63) ) ).

cnf(u854,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X16)
    | ~ ssSkP0(X14,X15,X16,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X13)
    | ~ ssSkP0(skf19(skc63,X0,X1),X2,X13,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X12)
    | ~ ssSkP0(skf19(skc63,X0,X1),X11,X12,skc63)
    | ~ member(skc63,skf17(X10,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X9)
    | ~ group(skc63,X10)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X3)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X8)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7),X8,skc63)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X6) ) ).

cnf(u858,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X16)
    | ~ ssSkP0(X14,X15,X16,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X13)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X13,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X12)
    | ~ ssSkP0(skf19(skc63,X0,X1),X11,X12,skc63)
    | ~ member(skc63,skf17(X10,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X9)
    | ~ group(skc63,X10)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X8)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ ssSkP0(skf19(skc63,X0,X1),X7,X8,skc63)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X6) ) ).

cnf(u862,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X4),X5,skc63)
    | ~ group(skc63,X13)
    | ~ member(skc63,X1,X17)
    | ~ ssSkP0(X0,skf26(skc63,X0,X12),X13,skc63)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X4)),X8)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X4)),X7)
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X4)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X2,X3),skf26(skc63,skf19(skc63,X2,X3),X4)),X5)
    | ~ ssSkP0(skf19(skc63,X2,X3),X6,X7,skc63) ) ).

cnf(u867,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5),X6,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X16)
    | ~ ssSkP0(X14,X15,X16,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X13)
    | ~ ssSkP0(X0,X1,X13,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X12)
    | ~ ssSkP0(X0,X11,X12,skc63)
    | ~ member(skc63,skf17(X10,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X9)
    | ~ group(skc63,X10)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X8)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X2)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X6)
    | ~ ssSkP0(skf19(skc63,X3,X4),X7,X8,skc63) ) ).

cnf(u893,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X14)
    | ~ ssSkP0(X12,X13,X14,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X11)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X11,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X10)
    | ~ ssSkP0(skf19(skc63,X0,X1),X9,X10,skc63)
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X7)
    | ~ group(skc63,X8)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X6) ) ).

cnf(u897,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5),X6,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X14)
    | ~ ssSkP0(X12,X13,X14,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X11)
    | ~ ssSkP0(X0,X1,X11,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X10)
    | ~ ssSkP0(X0,X9,X10,skc63)
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X7)
    | ~ group(skc63,X8)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X2)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X6) ) ).

cnf(u907,negated_conjecture,
    ( ~ ssSkP0(X9,X10,X11,skc63)
    | ~ ssSkP0(skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3),X8,skc63)
    | ~ ssSkP0(skf19(skc63,X1,X2),X6,X7,skc63)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X8)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X11)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X7)
    | ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4)
    | ~ member(skc63,skf17(X5,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X0)
    | ~ group(skc63,X5) ) ).

cnf(u917,negated_conjecture,
    ( member(skc63,skf27(skc63,X9),X9)
    | ~ ssSkP0(X10,X31,X12,skc63)
    | ~ member(skc63,skf17(X9,skc63,X10,skf26(skc63,X10,X11)),X12)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X9,skc63,X10,skf26(skc63,X10,X11)),X16)
    | ~ ssSkP0(X14,X15,X16,skc63)
    | ~ member(skc63,skf17(X9,skc63,X10,skf26(skc63,X10,X11)),X13)
    | ~ ssSkP0(X10,skf26(skc63,X10,X11),X13,skc63) ) ).

cnf(u920,negated_conjecture,
    ( member(skc63,skf17(X4,skc63,X7,X8),X4)
    | ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4)
    | ~ member(skc63,skf17(skf24(skc63,X5,X6),skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X0) ) ).

cnf(u924,negated_conjecture,
    ( member(skc63,skf17(X4,skc63,X6,X7),X4)
    | ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4)
    | ~ member(skc63,skf17(skf29(skc63,X5),skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X0) ) ).

cnf(u988,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X17)
    | ~ ssSkP0(X15,X16,X17,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X14)
    | ~ ssSkP0(skf19(skc63,X0,X1),X2,X14,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),X2),X13)
    | ~ ssSkP0(skf19(skc63,X0,X1),X12,X13,skc63)
    | ~ group(skc63,X11)
    | ~ member(skc63,skf17(X11,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X10)
    | ~ member(skc63,skf17(X10,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X9)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X3)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X8)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7),X8,skc63)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X7)),X6) ) ).

cnf(u992,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X17)
    | ~ ssSkP0(X15,X16,X17,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X14)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X14,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X13)
    | ~ ssSkP0(skf19(skc63,X0,X1),X12,X13,skc63)
    | ~ group(skc63,X11)
    | ~ member(skc63,skf17(X11,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X10)
    | ~ member(skc63,skf17(X10,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X9)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X8)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ ssSkP0(skf19(skc63,X0,X1),X7,X8,skc63)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X6) ) ).

cnf(u996,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5),X6,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X17)
    | ~ ssSkP0(X15,X16,X17,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X14)
    | ~ ssSkP0(X0,X1,X14,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X13)
    | ~ ssSkP0(X0,X12,X13,skc63)
    | ~ group(skc63,X11)
    | ~ member(skc63,skf17(X11,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X10)
    | ~ member(skc63,skf17(X10,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X9)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X8)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X2)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X6)
    | ~ ssSkP0(skf19(skc63,X3,X4),X7,X8,skc63) ) ).

cnf(u1015,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X15)
    | ~ ssSkP0(X13,X14,X15,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X12)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X12,skc63)
    | ~ member(skc63,skf17(X3,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X11)
    | ~ ssSkP0(skf19(skc63,X0,X1),X10,X11,skc63)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X8)
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X7)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X6) ) ).

cnf(u1019,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5),X6,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X15)
    | ~ ssSkP0(X13,X14,X15,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X12)
    | ~ ssSkP0(X0,X1,X12,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X11)
    | ~ ssSkP0(X0,X10,X11,skc63)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X8)
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X7)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X2)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X3,X4),skf26(skc63,skf19(skc63,X3,X4),X5)),X6) ) ).

cnf(u1029,negated_conjecture,
    ( ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X12)
    | ~ ssSkP0(X10,X11,X12,skc63)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X9)
    | ~ ssSkP0(skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3),X9,skc63)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X8)
    | ~ ssSkP0(skf19(skc63,X1,X2),X7,X8,skc63)
    | ~ group(skc63,X6)
    | ~ member(skc63,skf17(X6,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X5)
    | ~ member(skc63,skf17(X5,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X0) ) ).

cnf(u1066,negated_conjecture,
    ( member(skc63,skf27(skc63,X0),X0)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X3)),X7)
    | ~ ssSkP0(X5,X6,X7,skc63)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X3)),X4)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ ssSkP0(skc65,X1,X2,skc63)
    | ~ group(skc63,X0) ) ).

cnf(u1096,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X14)
    | ~ ssSkP0(X12,X13,X14,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X11)
    | ~ ssSkP0(skc65,X0,X11,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X10)
    | ~ ssSkP0(skc65,X9,X10,skc63)
    | ~ group(skc63,skf24(skc63,X7,X8))
    | ~ member(skc63,skf17(skf24(skc63,X7,X8),skc63,skc65,skf26(skc63,skc65,X5)),X6)
    | ~ member(skc63,skf17(skf24(skc63,X7,X8),skc63,skc65,skf26(skc63,skc65,X5)),X1)
    | ~ member(skc63,skf17(skf24(skc63,X7,X8),skc63,skc65,skf26(skc63,skc65,X5)),X4)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X5),X6,skc63) ) ).

cnf(u1100,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X14)
    | ~ ssSkP0(X12,X13,X14,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X11)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X11,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X10)
    | ~ ssSkP0(skc65,X9,X10,skc63)
    | ~ group(skc63,skf24(skc63,X7,X8))
    | ~ member(skc63,skf17(skf24(skc63,X7,X8),skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(skf24(skc63,X7,X8),skc63,skc65,skf26(skc63,skc65,X0)),X6)
    | ~ member(skc63,skf17(skf24(skc63,X7,X8),skc63,skc65,skf26(skc63,skc65,X0)),X4)
    | ~ ssSkP0(skc65,X5,X6,skc63) ) ).

cnf(u1104,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X14)
    | ~ ssSkP0(X12,X13,X14,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X11)
    | ~ ssSkP0(X0,X1,X11,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X10)
    | ~ ssSkP0(X0,X9,X10,skc63)
    | ~ group(skc63,skf24(skc63,X7,X8))
    | ~ member(skc63,skf17(skf24(skc63,X7,X8),skc63,skc65,skf26(skc63,skc65,X3)),X4)
    | ~ member(skc63,skf17(skf24(skc63,X7,X8),skc63,skc65,skf26(skc63,skc65,X3)),X6)
    | ~ member(skc63,skf17(skf24(skc63,X7,X8),skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ ssSkP0(skc65,X5,X6,skc63) ) ).

cnf(u1130,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X1,skc63)
    | ~ group(skc63,X1) ) ).

cnf(u1144,negated_conjecture,
    ( ~ ssSkP0(X5,X6,X7,skc63)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ ssSkP0(skc65,X1,X2,skc63)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X3)),X4)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X3)),X7)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ group(skc63,X0) ) ).

cnf(u1172,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X13)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X10)
    | ~ ssSkP0(skc65,X0,X10,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X9)
    | ~ ssSkP0(skc65,X8,X9,skc63)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X1)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X6)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X5),X6,skc63)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X4) ) ).

cnf(u1176,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X13)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X10)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X10,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X9)
    | ~ ssSkP0(skc65,X8,X9,skc63)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X6)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X4)
    | ~ ssSkP0(skc65,X5,X6,skc63) ) ).

cnf(u1180,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X2),X3,skc63)
    | ~ group(skc63,X10)
    | ~ member(skc63,X1,X14)
    | ~ ssSkP0(X0,skf26(skc63,X0,X9),X10,skc63)
    | ~ group(skc63,X6)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),X5)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),X3)
    | ~ ssSkP0(skc65,X4,X5,skc63) ) ).

cnf(u1184,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X13)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X10)
    | ~ ssSkP0(X0,X1,X10,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X9)
    | ~ ssSkP0(X0,X8,X9,skc63)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X6)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X4)
    | ~ ssSkP0(skc65,X5,X6,skc63) ) ).

cnf(u1202,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X11)
    | ~ ssSkP0(X9,X10,X11,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X8)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X8,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X7)
    | ~ ssSkP0(skc65,X6,X7,skc63)
    | ~ group(skc63,X5)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X4) ) ).

cnf(u1206,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X2),X3,skc63)
    | ~ group(skc63,X8)
    | ~ member(skc63,X1,X12)
    | ~ ssSkP0(X0,skf26(skc63,X0,X7),X8,skc63)
    | ~ group(skc63,X4)
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X2)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X2)),X3) ) ).

cnf(u1210,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X11)
    | ~ ssSkP0(X9,X10,X11,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X8)
    | ~ ssSkP0(X0,X1,X8,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X7)
    | ~ ssSkP0(X0,X6,X7,skc63)
    | ~ group(skc63,X5)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X3)),X4) ) ).

cnf(u1220,negated_conjecture,
    ( ~ ssSkP0(X6,X7,X8,skc63)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X1),X5,skc63)
    | ~ ssSkP0(skc65,X3,X4,skc63)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X5)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X8)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X4)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X1)),X2)
    | ~ group(skc63,X0) ) ).

cnf(u1253,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X14)
    | ~ ssSkP0(X12,X13,X14,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X11)
    | ~ ssSkP0(skc65,X0,X11,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X10)
    | ~ ssSkP0(skc65,X9,X10,skc63)
    | ~ group(skc63,X8)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X5)),X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X1)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X6)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X5),X6,skc63)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X4) ) ).

cnf(u1257,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X14)
    | ~ ssSkP0(X12,X13,X14,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X11)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X11,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X10)
    | ~ ssSkP0(skc65,X9,X10,skc63)
    | ~ group(skc63,X8)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X0)),X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X6)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X4)
    | ~ ssSkP0(skc65,X5,X6,skc63) ) ).

cnf(u1261,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X2),X3,skc63)
    | ~ group(skc63,X11)
    | ~ member(skc63,X1,X15)
    | ~ ssSkP0(X0,skf26(skc63,X0,X10),X11,skc63)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X2)),X6)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),X5)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),X3)
    | ~ ssSkP0(skc65,X4,X5,skc63) ) ).

cnf(u1265,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X14)
    | ~ ssSkP0(X12,X13,X14,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X11)
    | ~ ssSkP0(X0,X1,X11,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X10)
    | ~ ssSkP0(X0,X9,X10,skc63)
    | ~ group(skc63,X8)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X3)),X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X6)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X4)
    | ~ ssSkP0(skc65,X5,X6,skc63) ) ).

cnf(u1283,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X12)
    | ~ ssSkP0(X10,X11,X12,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X9)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X9,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X8)
    | ~ ssSkP0(skc65,X7,X8,skc63)
    | ~ group(skc63,X6)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X0)),X5)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X4) ) ).

cnf(u1287,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X2),X3,skc63)
    | ~ group(skc63,X9)
    | ~ member(skc63,X1,X13)
    | ~ ssSkP0(X0,skf26(skc63,X0,X8),X9,skc63)
    | ~ group(skc63,X5)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X2)),X4)
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X2)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X2)),X3) ) ).

cnf(u1291,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X12)
    | ~ ssSkP0(X10,X11,X12,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X9)
    | ~ ssSkP0(X0,X1,X9,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X8)
    | ~ ssSkP0(X0,X7,X8,skc63)
    | ~ group(skc63,X6)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X3)),X5)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X3)),X4) ) ).

cnf(u1301,negated_conjecture,
    ( ~ ssSkP0(X7,X8,X9,skc63)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X1),X6,skc63)
    | ~ ssSkP0(skc65,X4,X5,skc63)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X6)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X9)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X5)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X1)),X2)
    | ~ group(skc63,X3)
    | ~ member(skc63,skf17(X3,skc63,skc65,skf26(skc63,skc65,X1)),X0) ) ).

cnf(u1334,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X15)
    | ~ ssSkP0(X13,X14,X15,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X12)
    | ~ ssSkP0(skc65,X0,X12,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X11)
    | ~ ssSkP0(skc65,X10,X11,skc63)
    | ~ member(skc63,skf17(X9,skc63,skc65,skf26(skc63,skc65,X5)),X8)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X5)),X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X1)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X6)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X5),X6,skc63)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X4) ) ).

cnf(u1338,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X15)
    | ~ ssSkP0(X13,X14,X15,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X12)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X12,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X11)
    | ~ ssSkP0(skc65,X10,X11,skc63)
    | ~ member(skc63,skf17(X9,skc63,skc65,skf26(skc63,skc65,X0)),X8)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X0)),X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X6)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X4)
    | ~ ssSkP0(skc65,X5,X6,skc63) ) ).

cnf(u1342,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X2),X3,skc63)
    | ~ group(skc63,X12)
    | ~ member(skc63,X1,X16)
    | ~ ssSkP0(X0,skf26(skc63,X0,X11),X12,skc63)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X2)),X7)
    | ~ group(skc63,X8)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X2)),X6)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),X5)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),X3)
    | ~ ssSkP0(skc65,X4,X5,skc63) ) ).

cnf(u1346,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X15)
    | ~ ssSkP0(X13,X14,X15,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X12)
    | ~ ssSkP0(X0,X1,X12,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X11)
    | ~ ssSkP0(X0,X10,X11,skc63)
    | ~ member(skc63,skf17(X9,skc63,skc65,skf26(skc63,skc65,X3)),X8)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X3)),X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X6)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X4)
    | ~ ssSkP0(skc65,X5,X6,skc63) ) ).

cnf(u1364,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X13)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X10)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X10,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X9)
    | ~ ssSkP0(skc65,X8,X9,skc63)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X6)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X0)),X5)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X4) ) ).

cnf(u1368,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X2),X3,skc63)
    | ~ group(skc63,X10)
    | ~ member(skc63,X1,X14)
    | ~ ssSkP0(X0,skf26(skc63,X0,X9),X10,skc63)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),X5)
    | ~ group(skc63,X6)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X2)),X4)
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X2)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X2)),X3) ) ).

cnf(u1372,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X13)
    | ~ ssSkP0(X11,X12,X13,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X10)
    | ~ ssSkP0(X0,X1,X10,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X9)
    | ~ ssSkP0(X0,X8,X9,skc63)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X6)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X3)),X5)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X3)),X4) ) ).

cnf(u1382,negated_conjecture,
    ( ~ ssSkP0(X8,X9,X10,skc63)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X1),X7,skc63)
    | ~ ssSkP0(skc65,X5,X6,skc63)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X7)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X10)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X6)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X1)),X2)
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X1)),X3)
    | ~ group(skc63,X4)
    | ~ member(skc63,skf17(X3,skc63,skc65,skf26(skc63,skc65,X1)),X0) ) ).

cnf(u1415,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X16)
    | ~ ssSkP0(X14,X15,X16,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X13)
    | ~ ssSkP0(skc65,X0,X13,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,X0),X12)
    | ~ ssSkP0(skc65,X11,X12,skc63)
    | ~ member(skc63,skf17(X10,skc63,skc65,skf26(skc63,skc65,X5)),X8)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X9,skc63,skc65,skf26(skc63,skc65,X5)),X10)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X5)),X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X1)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X6)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X5),X6,skc63)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X5)),X4) ) ).

cnf(u1419,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X16)
    | ~ ssSkP0(X14,X15,X16,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X13)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X13,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X12)
    | ~ ssSkP0(skc65,X11,X12,skc63)
    | ~ member(skc63,skf17(X10,skc63,skc65,skf26(skc63,skc65,X0)),X8)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X9,skc63,skc65,skf26(skc63,skc65,X0)),X10)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X0)),X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X6)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X4)
    | ~ ssSkP0(skc65,X5,X6,skc63) ) ).

cnf(u1423,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X2),X3,skc63)
    | ~ group(skc63,X13)
    | ~ member(skc63,X1,X17)
    | ~ ssSkP0(X0,skf26(skc63,X0,X12),X13,skc63)
    | ~ member(skc63,skf17(X9,skc63,skc65,skf26(skc63,skc65,X2)),X7)
    | ~ group(skc63,X8)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X2)),X9)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X2)),X6)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),X5)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),X3)
    | ~ ssSkP0(skc65,X4,X5,skc63) ) ).

cnf(u1427,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X16)
    | ~ ssSkP0(X14,X15,X16,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X13)
    | ~ ssSkP0(X0,X1,X13,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X12)
    | ~ ssSkP0(X0,X11,X12,skc63)
    | ~ member(skc63,skf17(X10,skc63,skc65,skf26(skc63,skc65,X3)),X8)
    | ~ group(skc63,X9)
    | ~ member(skc63,skf17(X9,skc63,skc65,skf26(skc63,skc65,X3)),X10)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X3)),X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X6)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X4)
    | ~ ssSkP0(skc65,X5,X6,skc63) ) ).

cnf(u1445,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X14)
    | ~ ssSkP0(X12,X13,X14,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X11)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X11,skc63)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X10)
    | ~ ssSkP0(skc65,X9,X10,skc63)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X0)),X6)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X8)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X0)),X5)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X4) ) ).

cnf(u1449,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X2),X3,skc63)
    | ~ group(skc63,X11)
    | ~ member(skc63,X1,X15)
    | ~ ssSkP0(X0,skf26(skc63,X0,X10),X11,skc63)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X2)),X5)
    | ~ group(skc63,X6)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X2)),X7)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X2)),X4)
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X2)),skf24(skc63,X1,X0))
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X2)),X3) ) ).

cnf(u1453,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X3),X4,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X14)
    | ~ ssSkP0(X12,X13,X14,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X11)
    | ~ ssSkP0(X0,X1,X11,skc63)
    | ~ member(skc63,skf17(X2,skc63,X0,X1),X10)
    | ~ ssSkP0(X0,X9,X10,skc63)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X3)),X6)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X3)),X8)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X3)),X5)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X3)),X2)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X3)),X4) ) ).

cnf(u404,negated_conjecture,
    ( ~ agent(X0,skf18(X0,X1,X2),skf22(X3,X0,X4))
    | ~ present(X0,skf18(X0,X1,X2))
    | ~ sit(X0,skf18(X0,X1,X2))
    | ~ with(X0,skf18(X0,X1,X2),X3)
    | ~ event(X0,skf18(X0,X1,X2))
    | ~ table(X0,skf19(X0,X2,X1))
    | ssSkP1(X3,X5,X0)
    | ~ ssSkP1(X6,X7,X0)
    | ~ member(X0,X8,X7) ) ).

cnf(u534,negated_conjecture,
    ( ~ with(X0,skf15(X0,X1,X2,X3),skf17(X4,X0,X2,X3))
    | ~ present(X0,skf15(X0,X1,X2,X3))
    | ~ sit(X0,skf15(X0,X1,X2,X3))
    | ~ event(X0,skf15(X0,X1,X2,X3))
    | ssSkP0(X2,X3,X4,X0)
    | ~ ssSkP0(X2,X5,X6,X0)
    | ~ member(X0,X1,X6)
    | ~ ssSkP0(X2,X3,X7,X0)
    | ~ member(X0,X1,X7) ) ).

cnf(u578,negated_conjecture,
    ( group(X3,skf24(X3,X24,X25))
    | ~ member(X3,skf17(X4,X3,X0,skf26(X3,X0,X5)),X2)
    | ~ ssSkP0(X0,skf26(X3,X0,X5),X6,X3)
    | ~ member(X3,skf17(X4,X3,X0,skf26(X3,X0,X5)),X6)
    | ~ ssSkP0(X7,X8,X9,X3)
    | ~ member(X3,skf17(X4,X3,X0,skf26(X3,X0,X5)),X9)
    | ~ ssSkP0(X10,X11,X12,X3)
    | ~ member(X3,X13,X12)
    | ~ ssSkP0(X14,X15,X16,X3)
    | ~ member(X3,X17,X16)
    | ~ ssSkP0(X18,X19,X20,X3)
    | ~ member(X3,X21,X20)
    | ~ group(X3,X4)
    | member(X3,skf27(X3,X4),X4)
    | ~ member(X3,X22,X23)
    | ~ ssSkP0(X0,X1,X2,X3) ) ).

cnf(clause22,negated_conjecture,
    ( event(X0,skf18(X0,X4,X5))
    | ~ ssSkP1(X3,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u983,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X3,skc63)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X6)
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X7)
    | ~ member(skc63,skf17(X9,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X8)
    | ~ group(skc63,X9) ) ).

cnf(clause37,negated_conjecture,
    ( at(X0,skf18(X0,X4,X5),skf19(X0,X5,X4))
    | ~ ssSkP1(X3,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(clause40,negated_conjecture,
    ( ~ hamburger(X0,skf27(X0,X1))
    | ~ group(X0,X2)
    | ~ ssSkP0(X3,skf26(X0,X3,X4),X2,X0)
    | ssSkP2(X3,X5,X0) ) ).

cnf(u1410,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X1,skc63)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X4)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X0)),X5)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X8)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X8,skc63,skc65,skf26(skc63,skc65,X0)),X6) ) ).

cnf(u1294,negated_conjecture,
    ( ~ group(skc63,X3)
    | ~ member(skc63,skf17(X3,skc63,skc65,skf26(skc63,skc65,X1)),X0)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X1)),X2)
    | member(skc63,skf17(X2,skc63,X4,X5),X2) ) ).

cnf(clause25,negated_conjecture,
    ( agent(X0,skf18(X0,X1,X4),X1)
    | ~ ssSkP1(X3,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u573,negated_conjecture,
    ( ~ sit(X0,skf15(X0,skf17(X1,X0,X2,X3),X2,X3))
    | ssSkP0(X2,X3,X1,X0)
    | ~ ssSkP0(X2,X4,X5,X0)
    | ~ member(X0,skf17(X1,X0,X2,X3),X5)
    | ~ ssSkP0(X2,X3,X6,X0)
    | ~ member(X0,skf17(X1,X0,X2,X3),X6)
    | ~ ssSkP0(X7,X8,X9,X0)
    | ~ member(X0,skf17(X1,X0,X2,X3),X9)
    | ~ ssSkP0(X10,X11,X12,X0)
    | ~ member(X0,X13,X12)
    | ~ ssSkP0(X14,X15,X16,X0)
    | ~ member(X0,X17,X16) ) ).

cnf(u116,negated_conjecture,
    ( ssSkP1(X1,skf29(X0,X1),X0)
    | ~ member(X0,X1,X2)
    | member(X0,skf31(X0,X2),X2) ) ).

cnf(u568,negated_conjecture,
    ( ~ table(X0,X1)
    | ssSkP1(X2,X3,X0)
    | ~ ssSkP0(X1,X4,X5,X0)
    | ~ member(X0,X2,X5)
    | ~ ssSkP0(X1,skf22(X2,X0,X6),X7,X0)
    | ~ member(X0,X2,X7)
    | ~ ssSkP0(X8,X9,X10,X0)
    | ~ member(X0,X2,X10)
    | ~ ssSkP0(X11,X12,X13,X0)
    | ~ member(X0,X14,X13)
    | ~ ssSkP0(X15,X16,X17,X0)
    | ~ member(X0,X18,X17)
    | ~ ssSkP0(X19,X20,X21,X0)
    | ~ member(X0,X22,X21) ) ).

cnf(clause14,negated_conjecture,
    ( ssSkP2(X0,X1,X2)
    | member(X2,skf26(X2,X0,X1),X1) ) ).

cnf(u396,negated_conjecture,
    ~ member(skc5,skf14(skc5,X0),skf29(skc5,X1)) ).

cnf(u290,negated_conjecture,
    ( ~ actual_world(X0)
    | member(X0,skf14(X0,skf29(X0,X1)),skf29(X0,X1))
    | ~ ssSkP2(skf19(X0,X2,X3),skf29(X0,X1),X0)
    | ~ group(X0,skf29(X0,X1))
    | ~ ssSkP1(X4,X5,X0)
    | ~ member(X0,X6,X5)
    | ~ ssSkP3(X7,X0)
    | ~ member(X0,X8,X7) ) ).

cnf(u849,negated_conjecture,
    ( ~ ssSkP0(X4,X5,X6,skc63)
    | ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X3,skc63)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X6)
    | ~ group(skc63,X8)
    | ~ member(skc63,skf17(X8,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X7) ) ).

cnf(u246,negated_conjecture,
    ( ssSkP2(X2,X4,X0)
    | ~ ssSkP0(X2,skf26(X0,X2,X3),X1,X0)
    | ~ group(X0,X1)
    | ~ member(X0,X5,X6)
    | ~ ssSkP2(X7,X6,X0)
    | ~ member(X0,skf27(X0,X8),skf24(X0,X9,X10)) ) ).

cnf(clause1,negated_conjecture,
    actual_world(skc63) ).

cnf(clause29,negated_conjecture,
    ( ~ ssSkP2(X3,X2,X0)
    | ~ member(X0,X1,X2)
    | ssSkP0(X3,X1,skf24(X0,X1,X3),X0) ) ).

cnf(u1223,negated_conjecture,
    ( member(skc63,skf17(X2,skc63,X3,X4),X2)
    | ~ member(skc63,skf17(skf29(skc63,X0),skc63,skc65,skf26(skc63,skc65,X1)),X2) ) ).

cnf(u144,negated_conjecture,
    ( ssSkP0(X3,X1,skf24(X0,X1,X3),X0)
    | ~ member(X0,X1,X2)
    | member(X0,skf26(X0,X3,X2),X2) ) ).

cnf(u1303,negated_conjecture,
    ( member(skc63,skf17(X2,skc63,X3,X4),X2)
    | ~ member(skc63,skf17(X1,skc63,skc65,skf26(skc63,skc65,X0)),X2)
    | ~ member(skc63,skf17(skc64,skc63,skc65,skf26(skc63,skc65,X0)),X1) ) ).

cnf(clause32,negated_conjecture,
    ( agent(X0,skf15(X0,X1,X3,X4),X4)
    | ~ ssSkP0(X3,X4,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u544,negated_conjecture,
    ( ~ event(X0,skf15(X0,skf17(X1,X0,X2,X3),X2,X3))
    | ~ sit(X0,skf15(X0,skf17(X1,X0,X2,X3),X2,X3))
    | ~ present(X0,skf15(X0,skf17(X1,X0,X2,X3),X2,X3))
    | ssSkP0(X2,X3,X1,X0)
    | ~ ssSkP0(X2,X4,X5,X0)
    | ~ member(X0,skf17(X1,X0,X2,X3),X5)
    | ~ ssSkP0(X2,X3,X6,X0)
    | ~ member(X0,skf17(X1,X0,X2,X3),X6)
    | ~ ssSkP0(X7,X8,X9,X0)
    | ~ member(X0,skf17(X1,X0,X2,X3),X9) ) ).

cnf(u572,negated_conjecture,
    ( ~ table(X0,skf19(X0,X1,skf22(X1,X0,X2)))
    | ssSkP1(X1,X3,X0)
    | ~ ssSkP1(X4,X5,X0)
    | ~ member(X0,X6,X5)
    | ~ ssSkP1(X7,X8,X0)
    | ~ member(X0,skf22(X1,X0,X2),X8)
    | ~ ssSkP1(X1,X9,X0)
    | ~ member(X0,skf22(X1,X0,X2),X9)
    | ~ ssSkP1(X10,X11,X0)
    | ~ member(X0,X12,X11)
    | ~ ssSkP1(X13,X14,X0)
    | ~ member(X0,X15,X14)
    | ~ ssSkP1(X16,X17,X0)
    | ~ member(X0,X18,X17) ) ).

cnf(u435,negated_conjecture,
    ( ~ group(skc63,X0)
    | member(skc63,skf34(skc63,X0),X0) ) ).

cnf(u567,negated_conjecture,
    ( ~ present(X0,skf18(X0,skf22(X1,X0,X2),X1))
    | ~ sit(X0,skf18(X0,skf22(X1,X0,X2),X1))
    | ~ table(X0,skf19(X0,X1,skf22(X1,X0,X2)))
    | ssSkP1(X1,X3,X0)
    | ~ ssSkP1(X4,X5,X0)
    | ~ member(X0,X6,X5)
    | ~ ssSkP1(X7,X8,X0)
    | ~ member(X0,skf22(X1,X0,X2),X8)
    | ~ ssSkP1(X1,X9,X0)
    | ~ member(X0,skf22(X1,X0,X2),X9)
    | ~ ssSkP1(X10,X11,X0)
    | ~ member(X0,X12,X11) ) ).

cnf(u118,negated_conjecture,
    ( group(X0,skf24(X0,X3,X4))
    | ~ member(X0,X1,X2)
    | member(X0,skf26(X0,X5,X2),X2) ) ).

cnf(u294,negated_conjecture,
    ( ~ table(X0,X1)
    | ~ ssSkP2(X1,X2,X0)
    | ~ actual_world(X0)
    | ~ three(X0,X2)
    | ~ group(X0,X2)
    | ~ member(X0,X3,X4)
    | ~ ssSkP3(X4,X0)
    | ~ member(X0,skf14(X0,X5),skf29(X0,X6))
    | ~ member(X0,X7,X8)
    | ~ ssSkP3(X8,X0)
    | ~ member(X0,skf14(X0,X5),skf29(X0,X9)) ) ).

cnf(u398,negated_conjecture,
    ( ~ agent(X0,skf15(X0,X1,X2,X3),X5)
    | ~ sit(X0,skf15(X0,X1,X2,X3))
    | ~ present(X0,skf15(X0,X1,X2,X3))
    | ~ with(X0,skf15(X0,X1,X2,X3),skf17(X4,X0,X2,X5))
    | ~ event(X0,skf15(X0,X1,X2,X3))
    | ssSkP0(X2,X5,X4,X0)
    | ~ ssSkP0(X2,X6,X7,X0)
    | ~ member(X0,X1,X7) ) ).

cnf(clause36,negated_conjecture,
    ( guy(X0,X1)
    | ~ member(X0,X3,X4)
    | ~ ssSkP3(X4,X0)
    | ~ member(X0,X1,skf29(X0,X2)) ) ).

cnf(u372,negated_conjecture,
    ( ~ group(skc5,X0)
    | member(skc5,skf27(skc5,X0),X0)
    | member(skc5,skf17(X0,skc5,X1,X2),X0) ) ).

cnf(u256,negated_conjecture,
    ( ~ three(X0,X1)
    | ~ actual_world(X0)
    | member(X0,skf14(X0,X1),X1)
    | ~ ssSkP2(skf19(X0,X2,X3),X1,X0)
    | ~ group(X0,X1)
    | ~ ssSkP1(X4,X5,X0)
    | ~ member(X0,X6,X5) ) ).

cnf(clause43,negated_conjecture,
    ( ~ young(X0,skf32(X0,X1))
    | ~ guy(X0,skf32(X0,X1))
    | ~ group(X0,X2)
    | ~ three(X0,X2)
    | ~ ssSkP1(skf31(X0,X3),X2,X0)
    | ssSkP3(X4,X0) ) ).

cnf(u103,negated_conjecture,
    ( ~ ssSkP3(X0,skc63)
    | ~ group(skc63,X0)
    | member(skc63,skf34(skc63,X0),X0) ) ).

cnf(u900,negated_conjecture,
    ( ~ group(skc63,X5)
    | ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4)
    | ~ member(skc63,skf17(X5,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X0)
    | member(skc63,skf17(X4,skc63,X6,X7),X4) ) ).

cnf(clause34,negated_conjecture,
    ( with(X0,skf15(X0,X1,X5,X6),X1)
    | ~ ssSkP0(X3,X4,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u1222,negated_conjecture,
    ( member(skc63,skf17(X1,skc63,X2,X3),X1)
    | ~ member(skc63,skf17(skc64,skc63,skc65,skf26(skc63,skc65,X0)),X1) ) ).

cnf(u1248,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X1,skc63)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X4)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X0)),X5)
    | ~ group(skc63,X6) ) ).

cnf(u106,negated_conjecture,
    ( ~ group(skc5,X0)
    | member(skc5,skf31(skc5,X0),X0)
    | member(skc5,skf34(skc5,X0),X0) ) ).

cnf(u1199,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X1,skc63)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ group(skc63,X2) ) ).

cnf(u1384,negated_conjecture,
    ( member(skc63,skf17(X3,skc63,X4,X5),X3)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X3)
    | ~ member(skc63,skf17(skc64,skc63,skc65,skf26(skc63,skc65,X1)),X0)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X1)),X2) ) ).

cnf(u355,negated_conjecture,
    ~ member(skc63,skf14(skc63,skf29(skc63,X0)),skc64) ).

cnf(clause19,negated_conjecture,
    ( table(X0,skf19(X0,X4,X5))
    | ~ ssSkP1(X3,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u547,negated_conjecture,
    ( ssSkP1(X12,skf29(X0,X12),X0)
    | ~ group(X0,skf29(X0,X2))
    | ~ member(X0,X3,X4)
    | ~ ssSkP3(X4,X0)
    | ~ member(X0,skf32(X0,X5),skf29(X0,X6))
    | ~ member(X0,X7,X8)
    | ~ ssSkP3(X8,X0)
    | ~ member(X0,skf32(X0,X5),skf29(X0,X9))
    | ~ ssSkP3(X10,X0)
    | ~ member(X0,X11,X10)
    | ~ member(X0,X12,X13)
    | ~ ssSkP1(skf31(X0,X1),skf29(X0,X2),X0) ) ).

cnf(clause38,negated_conjecture,
    ( hamburger(X0,X1)
    | ~ member(X0,X4,X5)
    | ~ ssSkP2(X6,X5,X0)
    | ~ member(X0,X1,skf24(X0,X2,X3)) ) ).

cnf(u565,negated_conjecture,
    ( ~ present(X0,skf15(X0,X1,X2,skf22(X1,X0,X3)))
    | ~ sit(X0,skf15(X0,X1,X2,skf22(X1,X0,X3)))
    | ~ table(X0,X2)
    | ssSkP1(X1,X4,X0)
    | ~ ssSkP0(X2,X5,X6,X0)
    | ~ member(X0,X1,X6)
    | ~ ssSkP0(X2,skf22(X1,X0,X3),X7,X0)
    | ~ member(X0,X1,X7)
    | ~ ssSkP0(X8,X9,X10,X0)
    | ~ member(X0,X1,X10)
    | ~ ssSkP0(X11,X12,X13,X0)
    | ~ member(X0,X14,X13) ) ).

cnf(u1033,negated_conjecture,
    ( member(skc63,skf17(X6,skc63,X7,X8),X6)
    | ~ member(skc63,skf17(skf29(skc63,X5),skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X0)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X6)
    | ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4) ) ).

cnf(u364,negated_conjecture,
    ( ~ group(skc5,skf29(skc5,X0))
    | member(skc5,skf14(skc5,skf29(skc5,X0)),skf29(skc5,X0))
    | member(skc5,skf26(skc5,skf19(skc5,X1,X2),skf29(skc5,X0)),skf29(skc5,X0)) ) ).

cnf(u540,negated_conjecture,
    ( ~ with(X0,skf15(X0,X1,X2,skf22(X3,X0,X4)),X3)
    | ~ sit(X0,skf15(X0,X1,X2,skf22(X3,X0,X4)))
    | ~ present(X0,skf15(X0,X1,X2,skf22(X3,X0,X4)))
    | ~ event(X0,skf15(X0,X1,X2,skf22(X3,X0,X4)))
    | ~ table(X0,X2)
    | ssSkP1(X3,X5,X0)
    | ~ ssSkP0(X2,X6,X7,X0)
    | ~ member(X0,X1,X7)
    | ~ ssSkP0(X2,skf22(X3,X0,X4),X8,X0)
    | ~ member(X0,X1,X8) ) ).

cnf(clause23,negated_conjecture,
    ( ~ ssSkP2(X3,X2,X0)
    | ~ member(X0,X1,X2)
    | group(X0,skf24(X0,X4,X5)) ) ).

cnf(u403,negated_conjecture,
    ( ~ agent(X0,skf15(X0,X1,X2,X3),skf22(X4,X0,X5))
    | ~ present(X0,skf15(X0,X1,X2,X3))
    | ~ sit(X0,skf15(X0,X1,X2,X3))
    | ~ with(X0,skf15(X0,X1,X2,X3),X4)
    | ~ event(X0,skf15(X0,X1,X2,X3))
    | ~ table(X0,X2)
    | ssSkP1(X4,X6,X0)
    | ~ ssSkP0(X2,X7,X8,X0)
    | ~ member(X0,X1,X8) ) ).

cnf(u526,negated_conjecture,
    ( ssSkP0(X4,X9,skf24(X0,X9,X4),X0)
    | ~ member(X0,X2,X3)
    | ~ ssSkP0(X4,skf26(X0,X4,X5),X1,X0)
    | ~ member(X0,skf27(X0,X6),skf24(X0,X7,X8))
    | ~ member(X0,X9,X10)
    | ~ group(X0,X1)
    | ~ ssSkP0(X11,skf26(X0,X11,X12),X13,X0)
    | ~ group(X0,X13)
    | member(X0,skf27(X0,X13),X13) ) ).

cnf(u362,negated_conjecture,
    ( member(X0,skf32(X0,skf29(X0,X1)),skf29(X0,X1))
    | ~ ssSkP1(skf31(X0,X2),skf29(X0,X1),X0)
    | ssSkP3(X3,X0)
    | ~ group(X0,skf29(X0,X1))
    | ~ ssSkP3(X4,X0)
    | ~ member(X0,X5,X4) ) ).

cnf(clause26,negated_conjecture,
    ( event(X0,skf15(X0,X5,X6,X7))
    | ~ ssSkP0(X3,X4,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u613,negated_conjecture,
    ( ~ ssSkP0(X2,skf26(skc5,X2,X5),X3,skc5)
    | ~ group(skc5,X3)
    | member(skc5,skf27(skc5,X3),X3)
    | ~ member(skc5,X1,X4)
    | ~ member(skc5,X0,skf24(skc5,X1,X2)) ) ).

cnf(clause41,negated_conjecture,
    ( ~ three(X0,X1)
    | ~ group(X0,X1)
    | ~ ssSkP1(skf31(X0,X2),X1,X0)
    | ssSkP3(X3,X0)
    | member(X0,skf32(X0,X1),X1) ) ).

cnf(u506,negated_conjecture,
    member(skc63,skf17(skc64,skc63,X0,X1),skc64) ).

cnf(u104,negated_conjecture,
    ( ~ ssSkP3(X0,skc5)
    | ~ group(skc5,X0)
    | member(skc5,skf34(skc5,X0),X0) ) ).

cnf(u516,negated_conjecture,
    ( ~ with(X0,skf18(X0,skf22(X1,X0,X2),X3),X1)
    | ~ sit(X0,skf18(X0,skf22(X1,X0,X2),X3))
    | ~ present(X0,skf18(X0,skf22(X1,X0,X2),X3))
    | ~ event(X0,skf18(X0,skf22(X1,X0,X2),X3))
    | ~ table(X0,skf19(X0,X3,skf22(X1,X0,X2)))
    | ssSkP1(X1,X4,X0)
    | ~ ssSkP1(X5,X6,X0)
    | ~ member(X0,X7,X6)
    | ~ ssSkP1(X8,X9,X0)
    | ~ member(X0,skf22(X1,X0,X2),X9) ) ).

cnf(u570,negated_conjecture,
    ( ssSkP1(X0,X1,X2)
    | ~ ssSkP0(skf19(X2,X3,X4),X5,X6,X2)
    | ~ member(X2,X0,X6)
    | ~ ssSkP0(skf19(X2,X3,X4),skf22(X0,X2,X7),X8,X2)
    | ~ member(X2,X0,X8)
    | ~ ssSkP0(X9,X10,X11,X2)
    | ~ member(X2,X0,X11)
    | ~ ssSkP0(X12,X13,X14,X2)
    | ~ member(X2,X15,X14)
    | ~ ssSkP0(X16,X17,X18,X2)
    | ~ member(X2,X19,X18)
    | ~ ssSkP0(X20,X21,X22,X2)
    | ~ member(X2,X23,X22)
    | ~ ssSkP1(X24,X25,X2)
    | ~ member(X2,X26,X25) ) ).

cnf(u407,negated_conjecture,
    ( ~ ssSkP2(X6,X5,X1)
    | ~ group(X1,X3)
    | ~ member(X1,X4,X5)
    | ~ ssSkP0(X0,skf26(X1,X0,X2),X3,X1)
    | ~ member(X1,skf27(X1,X7),skf24(X1,X8,X9))
    | ~ member(X1,X10,X11)
    | ssSkP0(X0,X10,skf24(X1,X10,X0),X1) ) ).

cnf(clause2,negated_conjecture,
    actual_world(skc5) ).

cnf(clause17,negated_conjecture,
    ( ~ ssSkP3(X2,X0)
    | ~ member(X0,X1,X2)
    | group(X0,skf29(X0,X3)) ) ).

cnf(clause45,negated_conjecture,
    ( ~ at(X0,X1,X3)
    | ~ with(X0,X1,skf17(X2,X0,X3,X4))
    | ~ sit(X0,X1)
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ event(X0,X1)
    | ssSkP0(X3,X4,X2,X0) ) ).

cnf(u1361,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X1,skc63)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X3,skc63,skc65,skf26(skc63,skc65,X0)),X2)
    | ~ group(skc63,X4)
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X0)),X3) ) ).

cnf(u560,negated_conjecture,
    member(skc5,skf34(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ).

cnf(u224,negated_conjecture,
    ( ssSkP1(X0,skf29(skc5,X0),skc5)
    | ~ member(skc5,X0,skc6) ) ).

cnf(u909,negated_conjecture,
    ( member(skc63,skf17(X4,skc63,X5,X6),X4)
    | ~ member(skc63,skf17(skc64,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X0)
    | ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4) ) ).

cnf(u115,negated_conjecture,
    ( group(X0,skf29(X0,X3))
    | ~ member(X0,X1,X2)
    | member(X0,skf31(X0,X2),X2) ) ).

cnf(u574,negated_conjecture,
    ( ssSkP1(X0,X1,X2)
    | ~ ssSkP1(X3,X4,X2)
    | ~ member(X2,X5,X4)
    | ~ ssSkP1(X6,X7,X2)
    | ~ member(X2,skf22(X0,X2,X8),X7)
    | ~ ssSkP1(X0,X9,X2)
    | ~ member(X2,skf22(X0,X2,X8),X9)
    | ~ ssSkP1(X10,X11,X2)
    | ~ member(X2,X12,X11)
    | ~ ssSkP1(X13,X14,X2)
    | ~ member(X2,X15,X14)
    | ~ ssSkP1(X16,X17,X2)
    | ~ member(X2,X18,X17)
    | ~ ssSkP1(X19,X20,X2)
    | ~ member(X2,X21,X20) ) ).

cnf(u1056,negated_conjecture,
    member(skc63,skf26(skc63,skc65,skc64),skc64) ).

cnf(u527,negated_conjecture,
    ( ssSkP0(X4,X9,skf24(X0,X9,X4),X0)
    | ~ member(X0,X2,X3)
    | ~ ssSkP0(X4,skf26(X0,X4,X5),X1,X0)
    | ~ member(X0,skf27(X0,X6),skf24(X0,X7,X8))
    | ~ member(X0,X9,X10)
    | ~ group(X0,X1)
    | member(X0,skf26(X0,X11,X3),X3) ) ).

cnf(u1375,negated_conjecture,
    ( ~ group(skc63,X4)
    | ~ member(skc63,skf17(X3,skc63,skc65,skf26(skc63,skc65,X1)),X0)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X1)),X2)
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X1)),X3)
    | member(skc63,skf17(X2,skc63,X5,X6),X2) ) ).

cnf(u575,negated_conjecture,
    ( ssSkP0(X0,X1,X2,X3)
    | ~ ssSkP0(X0,X4,X5,X3)
    | ~ member(X3,skf17(X2,X3,X0,X1),X5)
    | ~ ssSkP0(X0,X1,X6,X3)
    | ~ member(X3,skf17(X2,X3,X0,X1),X6)
    | ~ ssSkP0(X7,X8,X9,X3)
    | ~ member(X3,skf17(X2,X3,X0,X1),X9)
    | ~ ssSkP0(X10,X11,X12,X3)
    | ~ member(X3,X13,X12)
    | ~ ssSkP0(X14,X15,X16,X3)
    | ~ member(X3,X17,X16)
    | ~ ssSkP0(X18,X19,X20,X3)
    | ~ member(X3,X21,X20) ) ).

cnf(u357,negated_conjecture,
    ( ~ actual_world(X0)
    | ~ ssSkP2(skf19(X0,X1,X2),skf29(X0,X3),X0)
    | ~ group(X0,skf29(X0,X3))
    | ~ member(X0,X4,X5)
    | ~ ssSkP3(X5,X0)
    | ~ member(X0,skf14(X0,X6),skf29(X0,X7))
    | ~ member(X0,X8,X9)
    | ~ ssSkP3(X9,X0)
    | ~ member(X0,skf14(X0,X6),skf29(X0,X10))
    | ~ ssSkP1(X11,X12,X0)
    | ~ member(X0,X13,X12)
    | ~ ssSkP3(X14,X0)
    | ~ member(X0,X15,X14) ) ).

cnf(clause21,negated_conjecture,
    ( present(X0,skf18(X0,X4,X5))
    | ~ ssSkP1(X3,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(clause33,negated_conjecture,
    ( at(X0,skf15(X0,X1,X3,X5),X3)
    | ~ ssSkP0(X3,X4,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(clause24,negated_conjecture,
    ( with(X0,skf18(X0,X1,X3),X3)
    | ~ ssSkP1(X3,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u1304,negated_conjecture,
    ( member(skc63,skf17(X3,skc63,X4,X5),X3)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X3)
    | ~ member(skc63,skf17(skf29(skc63,X0),skc63,skc65,skf26(skc63,skc65,X1)),X2) ) ).

cnf(u564,negated_conjecture,
    ( ~ event(X0,skf15(X0,X1,X2,skf22(X1,X0,X3)))
    | ~ present(X0,skf15(X0,X1,X2,skf22(X1,X0,X3)))
    | ~ sit(X0,skf15(X0,X1,X2,skf22(X1,X0,X3)))
    | ~ table(X0,X2)
    | ssSkP1(X1,X4,X0)
    | ~ ssSkP0(X2,X5,X6,X0)
    | ~ member(X0,X1,X6)
    | ~ ssSkP0(X2,skf22(X1,X0,X3),X7,X0)
    | ~ member(X0,X1,X7)
    | ~ ssSkP0(X8,X9,X10,X0)
    | ~ member(X0,X1,X10) ) ).

cnf(u267,negated_conjecture,
    ( ~ guy(X0,skf14(X0,X3))
    | ~ table(X0,X1)
    | ~ ssSkP2(X1,X2,X0)
    | ~ actual_world(X0)
    | ~ three(X0,X2)
    | ~ group(X0,X2)
    | ~ member(X0,X4,X5)
    | ~ ssSkP3(X5,X0)
    | ~ member(X0,skf14(X0,X3),skf29(X0,X6)) ) ).

cnf(u1167,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X1,skc63)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X4)
    | ~ group(skc63,X5) ) ).

cnf(u571,negated_conjecture,
    ( ~ sit(X0,skf18(X0,skf22(X1,X0,X2),X1))
    | ~ table(X0,skf19(X0,X1,skf22(X1,X0,X2)))
    | ssSkP1(X1,X3,X0)
    | ~ ssSkP1(X4,X5,X0)
    | ~ member(X0,X6,X5)
    | ~ ssSkP1(X7,X8,X0)
    | ~ member(X0,skf22(X1,X0,X2),X8)
    | ~ ssSkP1(X1,X9,X0)
    | ~ member(X0,skf22(X1,X0,X2),X9)
    | ~ ssSkP1(X10,X11,X0)
    | ~ member(X0,X12,X11)
    | ~ ssSkP1(X13,X14,X0)
    | ~ member(X0,X15,X14) ) ).

cnf(u399,negated_conjecture,
    ( ~ agent(X0,skf18(X0,X1,X2),X4)
    | ~ sit(X0,skf18(X0,X1,X2))
    | ~ present(X0,skf18(X0,X1,X2))
    | ~ with(X0,skf18(X0,X1,X2),skf17(X3,X0,skf19(X0,X2,X1),X4))
    | ~ event(X0,skf18(X0,X1,X2))
    | ssSkP0(skf19(X0,X2,X1),X4,X3,X0)
    | ~ ssSkP1(X5,X6,X0)
    | ~ member(X0,X7,X6) ) ).

cnf(u301,negated_conjecture,
    ( ~ ssSkP0(X0,skf26(X1,X0,X2),X3,X1)
    | ~ group(X1,X3)
    | member(X1,skf27(X1,X3),X3)
    | ~ member(X1,X4,X5)
    | group(X1,skf24(X1,X6,X7)) ) ).

cnf(clause9,negated_conjecture,
    ( ssSkP3(X0,X1)
    | member(X1,skf31(X1,X0),X0) ) ).

cnf(u1466,negated_conjecture,
    ( member(skc63,skf17(X1,skc63,X2,X3),X1)
    | ~ member(skc63,X0,X1) ) ).

cnf(clause28,negated_conjecture,
    ( sit(X0,skf15(X0,X5,X6,X7))
    | ~ ssSkP0(X3,X4,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u436,negated_conjecture,
    ( ssSkP1(X0,skf29(skc63,X0),skc63)
    | ~ member(skc63,X0,X1) ) ).

cnf(clause35,negated_conjecture,
    ( young(X0,X1)
    | ~ member(X0,X3,X4)
    | ~ ssSkP3(X4,X0)
    | ~ member(X0,X1,skf29(X0,X2)) ) ).

cnf(u333,negated_conjecture,
    ( ~ three(X0,X3)
    | ~ actual_world(X0)
    | ~ ssSkP2(skf19(X0,X1,X2),X3,X0)
    | ~ group(X0,X3)
    | ~ member(X0,X4,X5)
    | ~ ssSkP3(X5,X0)
    | ~ member(X0,skf14(X0,X6),skf29(X0,X7))
    | ~ member(X0,X8,X9)
    | ~ ssSkP3(X9,X0)
    | ~ member(X0,skf14(X0,X6),skf29(X0,X10))
    | ~ ssSkP1(X11,X12,X0)
    | ~ member(X0,X13,X12) ) ).

cnf(u538,negated_conjecture,
    ( ~ with(X0,skf18(X0,X1,X2),skf17(X3,X0,skf19(X0,X2,X1),X1))
    | ~ present(X0,skf18(X0,X1,X2))
    | ~ sit(X0,skf18(X0,X1,X2))
    | ~ event(X0,skf18(X0,X1,X2))
    | ssSkP0(skf19(X0,X2,X1),X1,X3,X0)
    | ~ ssSkP1(X4,X5,X0)
    | ~ member(X0,X6,X5)
    | ~ ssSkP1(X7,X8,X0)
    | ~ member(X0,X1,X8) ) ).

cnf(u566,negated_conjecture,
    ( ~ sit(X0,skf15(X0,X1,X2,skf22(X1,X0,X3)))
    | ~ table(X0,X2)
    | ssSkP1(X1,X4,X0)
    | ~ ssSkP0(X2,X5,X6,X0)
    | ~ member(X0,X1,X6)
    | ~ ssSkP0(X2,skf22(X1,X0,X3),X7,X0)
    | ~ member(X0,X1,X7)
    | ~ ssSkP0(X8,X9,X10,X0)
    | ~ member(X0,X1,X10)
    | ~ ssSkP0(X11,X12,X13,X0)
    | ~ member(X0,X14,X13)
    | ~ ssSkP0(X15,X16,X17,X0)
    | ~ member(X0,X18,X17) ) ).

cnf(u503,negated_conjecture,
    ( ~ group(skc63,X0)
    | member(skc63,skf17(X0,skc63,X1,X2),X0) ) ).

cnf(u610,negated_conjecture,
    ( member(skc5,skf17(X1,skc5,X2,X3),X1)
    | ~ member(skc5,X0,X1) ) ).

cnf(u1031,negated_conjecture,
    ( member(skc63,skf17(X5,skc63,X6,X7),X5)
    | ~ member(skc63,skf17(skc64,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X0)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X5)
    | ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4) ) ).

cnf(u723,negated_conjecture,
    ( ~ group(skc63,X0)
    | ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4)
    | member(skc63,skf17(X4,skc63,X5,X6),X4) ) ).

cnf(u1213,negated_conjecture,
    ( ~ group(skc63,X0)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X1)),X2)
    | member(skc63,skf17(X2,skc63,X3,X4),X2) ) ).

cnf(clause13,negated_conjecture,
    ( ssSkP1(X0,X1,X2)
    | member(X2,skf22(X0,X2,X1),X1) ) ).

cnf(u1442,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X1,skc63)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X3,skc63,skc65,skf26(skc63,skc65,X0)),X2)
    | ~ member(skc63,skf17(X4,skc63,skc65,skf26(skc63,skc65,X0)),X5)
    | ~ group(skc63,X4)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X3) ) ).

cnf(u1385,negated_conjecture,
    ( member(skc63,skf17(X3,skc63,X5,X6),X3)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X1)),X3)
    | ~ member(skc63,skf17(skf29(skc63,X4),skc63,skc65,skf26(skc63,skc65,X1)),X0)
    | ~ member(skc63,skf17(X0,skc63,skc65,skf26(skc63,skc65,X1)),X2) ) ).

cnf(clause16,negated_conjecture,
    ( three(X0,skf29(X0,X3))
    | ~ ssSkP3(X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u375,negated_conjecture,
    ( member(skc5,skf17(skf29(skc5,X0),skc5,X1,X2),skf29(skc5,X0))
    | member(skc5,skf27(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ) ).

cnf(clause39,negated_conjecture,
    ( ssSkP2(X2,X4,X0)
    | ~ ssSkP0(X2,skf26(X0,X2,X3),X1,X0)
    | ~ group(X0,X1)
    | member(X0,skf27(X0,X1),X1) ) ).

cnf(u484,negated_conjecture,
    ( ~ group(skc63,skf29(skc63,X0))
    | member(skc63,skf26(skc63,skf19(skc63,X1,X2),skf29(skc63,X0)),skf29(skc63,X0)) ) ).

cnf(u419,negated_conjecture,
    ( ~ three(X0,X1)
    | ~ group(X0,X1)
    | ~ ssSkP1(skf31(X0,X2),X1,X0)
    | ssSkP3(X3,X0)
    | ~ member(X0,X4,X5)
    | ~ ssSkP3(X5,X0)
    | ~ member(X0,skf32(X0,X6),skf29(X0,X7))
    | ~ member(X0,X8,X9)
    | ~ ssSkP3(X9,X0)
    | ~ member(X0,skf32(X0,X6),skf29(X0,X10)) ) ).

cnf(u563,negated_conjecture,
    ( ~ event(X0,skf18(X0,skf22(X1,X0,X2),X1))
    | ~ present(X0,skf18(X0,skf22(X1,X0,X2),X1))
    | ~ sit(X0,skf18(X0,skf22(X1,X0,X2),X1))
    | ~ table(X0,skf19(X0,X1,skf22(X1,X0,X2)))
    | ssSkP1(X1,X3,X0)
    | ~ ssSkP1(X4,X5,X0)
    | ~ member(X0,X6,X5)
    | ~ ssSkP1(X7,X8,X0)
    | ~ member(X0,skf22(X1,X0,X2),X8)
    | ~ ssSkP1(X1,X9,X0)
    | ~ member(X0,skf22(X1,X0,X2),X9) ) ).

cnf(u890,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X3,skc63)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ group(skc63,X5)
    | ~ member(skc63,skf17(X5,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X4) ) ).

cnf(u569,negated_conjecture,
    ( ~ present(X0,skf15(X0,skf17(X1,X0,X2,X3),X2,X3))
    | ~ sit(X0,skf15(X0,skf17(X1,X0,X2,X3),X2,X3))
    | ssSkP0(X2,X3,X1,X0)
    | ~ ssSkP0(X2,X4,X5,X0)
    | ~ member(X0,skf17(X1,X0,X2,X3),X5)
    | ~ ssSkP0(X2,X3,X6,X0)
    | ~ member(X0,skf17(X1,X0,X2,X3),X6)
    | ~ ssSkP0(X7,X8,X9,X0)
    | ~ member(X0,skf17(X1,X0,X2,X3),X9)
    | ~ ssSkP0(X10,X11,X12,X0)
    | ~ member(X0,X13,X12) ) ).

cnf(u1022,negated_conjecture,
    ( ~ group(skc63,X6)
    | ~ member(skc63,skf17(X5,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X0)
    | ~ member(skc63,skf17(X6,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X5)
    | ~ member(skc63,skf17(X0,skc63,skf19(skc63,X1,X2),skf26(skc63,skf19(skc63,X1,X2),X3)),X4)
    | member(skc63,skf17(X4,skc63,X7,X8),X4) ) ).

cnf(u733,negated_conjecture,
    ( member(skc63,skf17(X3,skc63,X4,X5),X3)
    | ~ member(skc63,skf17(skc64,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3) ) ).

cnf(u397,negated_conjecture,
    ( ~ guy(X0,skf32(X0,X1))
    | ~ group(X0,X2)
    | ~ three(X0,X2)
    | ~ ssSkP1(skf31(X0,X3),X2,X0)
    | ssSkP3(X4,X0)
    | ~ member(X0,X5,X6)
    | ~ ssSkP3(X6,X0)
    | ~ member(X0,skf32(X0,X1),skf29(X0,X7)) ) ).

cnf(u1329,negated_conjecture,
    ( ~ ssSkP0(X2,X3,X4,skc63)
    | ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X1,skc63)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X5,skc63,skc65,skf26(skc63,skc65,X0)),X4)
    | ~ member(skc63,skf17(X6,skc63,skc65,skf26(skc63,skc65,X0)),X5)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X7,skc63,skc65,skf26(skc63,skc65,X0)),X6) ) ).

cnf(clause20,negated_conjecture,
    ( sit(X0,skf18(X0,X4,X5))
    | ~ ssSkP1(X3,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u400,negated_conjecture,
    ( member(X0,skf17(X1,X0,X6,X7),X1)
    | member(X0,skf27(X0,X1),X1)
    | ~ member(X0,X2,X3)
    | group(X0,skf24(X0,X4,X5))
    | ~ group(X0,X1) ) ).

cnf(clause15,negated_conjecture,
    ( ssSkP0(X0,X1,X2,X3)
    | member(X3,skf17(X2,X3,X4,X5),X2) ) ).

cnf(clause27,negated_conjecture,
    ( present(X0,skf15(X0,X5,X6,X7))
    | ~ ssSkP0(X3,X4,X2,X0)
    | ~ member(X0,X1,X2) ) ).

cnf(u648,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X3,skc63)
    | ~ ssSkP0(X4,X5,X6,skc63)
    | ~ group(skc63,X7)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ member(skc63,skf17(X7,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X6) ) ).

cnf(u539,negated_conjecture,
    ( ssSkP3(X3,X0)
    | ~ ssSkP1(skf31(X0,X2),skf29(X0,X1),X0)
    | ~ group(X0,skf29(X0,X1))
    | ~ member(X0,X4,X5)
    | ~ ssSkP3(X5,X0)
    | ~ member(X0,skf32(X0,X6),skf29(X0,X7))
    | ~ member(X0,X8,X9)
    | ~ ssSkP3(X9,X0)
    | ~ member(X0,skf32(X0,X6),skf29(X0,X10))
    | ~ ssSkP3(X11,X0)
    | ~ member(X0,X12,X11) ) ).

cnf(u708,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X3,skc63)
    | ~ group(skc63,X4)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3) ) ).

cnf(clause18,negated_conjecture,
    ( ~ ssSkP3(X2,X0)
    | ~ member(X0,X1,X2)
    | ssSkP1(X1,skf29(X0,X1),X0) ) ).

cnf(clause46,negated_conjecture,
    ( ~ at(X0,X1,X4)
    | ~ agent(X0,X1,skf22(X2,X0,X3))
    | ~ present(X0,X1)
    | ~ sit(X0,X1)
    | ~ with(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ table(X0,X4)
    | ssSkP1(X2,X5,X0) ) ).

cnf(u1012,negated_conjecture,
    ( ~ ssSkP0(skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2),X3,skc63)
    | ~ member(skc63,skf17(X4,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X3)
    | ~ member(skc63,skf17(X5,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X4)
    | ~ member(skc63,skf17(X6,skc63,skf19(skc63,X0,X1),skf26(skc63,skf19(skc63,X0,X1),X2)),X5)
    | ~ group(skc63,X6) ) ).

cnf(u105,negated_conjecture,
    ( ~ group(skc63,X0)
    | member(skc63,skf31(skc63,X0),X0)
    | member(skc63,skf34(skc63,X0),X0) ) ).

cnf(u385,negated_conjecture,
    ( member(skc5,skf26(skc5,skf19(skc5,X1,X2),skf29(skc5,X0)),skf29(skc5,X0))
    | member(skc5,skf14(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ) ).

cnf(u1280,negated_conjecture,
    ( ~ ssSkP0(skc65,skf26(skc63,skc65,X0),X1,skc63)
    | ~ member(skc63,skf17(X2,skc63,skc65,skf26(skc63,skc65,X0)),X1)
    | ~ member(skc63,skf17(X3,skc63,skc65,skf26(skc63,skc65,X0)),X2)
    | ~ group(skc63,X3) ) ).

cnf(u300,negated_conjecture,
    ( ssSkP0(X0,X4,skf24(X1,X4,X0),X1)
    | ~ group(X1,X3)
    | member(X1,skf27(X1,X3),X3)
    | ~ member(X1,X4,X5)
    | ~ ssSkP0(X0,skf26(X1,X0,X2),X3,X1) ) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : NLP027-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.39  % Computer : n017.cluster.edu
% 0.14/0.39  % Model    : x86_64 x86_64
% 0.14/0.39  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39  % Memory   : 8046.5625MB
% 0.14/0.39  % OS       : Linux 6.8.0-71-generic
% 0.14/0.39  % CPULimit : 300
% 0.14/0.39  % WCLimit  : 300
% 0.14/0.39  % DateTime : Sun Sep 27 17:44:35 UTC 2026
% 0.14/0.39  % CPUTime  : 
% 0.14/0.39  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.43  Running first-order theorem proving
% 0.14/0.43  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
% 2.77/1.36  % (2840356)Input is clausal, will run a generic CNF schedule.
% 2.77/1.36  % (2840419)lrs+10_1_sil=8000:sp=occurrence:random_seed=3307066550:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.77/1.36  % (2840416)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=1024615911:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.77/1.36  % (2840418)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2503295181:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.77/1.36  % (2840417)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3790309060:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.77/1.36  % (2840419)Instruction limit reached! 
% 2.77/1.36  % (2840419)------------------------------
% 2.77/1.36  % (2840419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.77/1.36  % (2840419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/1.36  % (2840419)CaDiCaL version: 2.1.3
% 2.77/1.36  % (2840419)Termination reason: Instruction limit
% 2.77/1.36  % (2840419)Termination phase: Saturation
% 2.77/1.36  % (2840419)Time elapsed: 0.032 s
% 2.77/1.36  % (2840419)Peak memory usage: 89 MB
% 2.77/1.36  % (2840419)Instructions burned: 107 (million)
% 2.77/1.36  % (2840422)dis-21_1_sil=8000:lcm=predicate:random_seed=2509598979: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)
% 2.77/1.36  % (2840421)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4247382526:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.77/1.36  % (2840421)Refutation not found, incomplete strategy
% 2.77/1.36  % (2840421)------------------------------
% 2.77/1.36  % (2840421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.77/1.36  % (2840421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/1.36  % (2840421)CaDiCaL version: 2.1.3
% 2.77/1.36  % (2840421)Termination reason: Refutation not found, incomplete strategy
% 2.77/1.36  % (2840421)Time elapsed: 0.022 s
% 2.77/1.36  % (2840421)Peak memory usage: 88 MB
% 2.77/1.36  % (2840421)Instructions burned: 24 (million)
% 2.77/1.36  % (2840420)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2720425687:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.77/1.36  % (2840420)Refutation not found, incomplete strategy
% 2.77/1.36  % (2840420)------------------------------
% 2.77/1.36  % (2840420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.77/1.36  % (2840420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/1.36  % (2840420)CaDiCaL version: 2.1.3
% 2.77/1.36  % (2840420)Termination reason: Refutation not found, incomplete strategy
% 2.77/1.36  % (2840420)Time elapsed: 0.008 s
% 2.77/1.36  % (2840420)Peak memory usage: 88 MB
% 2.77/1.36  % (2840420)Instructions burned: 10 (million)
% 2.77/1.36  % (2840422)First to succeed.
% 2.77/1.36  % (2840422)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2840356"
% 2.77/1.36  % (2840427)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=2638900227:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 2.77/1.36  % (2840427)Refutation not found, incomplete strategy
% 2.77/1.36  % (2840427)------------------------------
% 2.77/1.36  % (2840427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.77/1.36  % (2840427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/1.36  % (2840427)CaDiCaL version: 2.1.3
% 2.77/1.36  % (2840427)Termination reason: Refutation not found, incomplete strategy
% 2.77/1.36  % (2840427)Time elapsed: 0.003 s
% 2.77/1.36  % (2840427)Peak memory usage: 88 MB
% 2.77/1.36  % (2840427)Instructions burned: 7 (million)
% 2.77/1.36  % (2840427)------------------------------
% 2.77/1.36  % (2840427)------------------------------
% 2.77/1.36  % (2840421)------------------------------
% 2.77/1.36  % (2840421)------------------------------
% 2.77/1.36  % (2840420)------------------------------
% 2.77/1.36  % (2840420)------------------------------
% 2.77/1.36  % SZS status Satisfiable for theBenchmark
% 2.77/1.36  % SZS output start Saturation.
% See solution above
% 4.06/1.56  % SZS output start Definitions and Model Updates.
% 4.06/1.56  % SZS output end Definitions and Model Updates.
% 4.06/1.56  % (2840422)------------------------------
% 4.06/1.56  % (2840422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.06/1.56  % (2840422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.06/1.56  % (2840422)CaDiCaL version: 2.1.3
% 4.06/1.56  % (2840422)Termination reason: Satisfiable
% 4.06/1.56  % (2840422)Time elapsed: 0.072 s
% 4.06/1.56  % (2840422)Peak memory usage: 89 MB
% 4.06/1.56  % (2840422)Instructions burned: 122 (million)
% 4.06/1.56  % (2840422)------------------------------
% 4.06/1.56  % (2840422)------------------------------
% 4.06/1.56  % (2840356)Success in time 0.483 s
% 4.06/1.56  % Vampire exiting
%------------------------------------------------------------------------------