%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP026-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 : n004.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.92s 1.50s
% Output : Saturation 5.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u49,negated_conjecture,
ssSkC0 ).
cnf(u53,negated_conjecture,
( ~ hamburger(X0,skf14(X0,X2))
| ~ actual_world(X0)
| ~ table(X0,X3)
| ~ ssSkP2(X3,X1,X0)
| ~ group(X0,X1) ) ).
cnf(u57,negated_conjecture,
( ~ ssSkP2(X2,X1,X0)
| member(X0,skf14(X0,X1),X1)
| ~ actual_world(X0)
| ~ table(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u61,negated_conjecture,
( ~ ssSkP3(X1,X0)
| member(X0,skf34(X0,X1),X1)
| ~ actual_world(X0)
| ~ group(X0,X1) ) ).
cnf(u69,negated_conjecture,
( ~ member(skc5,X0,skc6)
| hamburger(skc5,X0) ) ).
cnf(u73,negated_conjecture,
( ~ member(skc64,X0,skc65)
| hamburger(skc64,X0) ) ).
cnf(u77,negated_conjecture,
~ ssSkP2(skc66,skc65,skc64) ).
cnf(u83,negated_conjecture,
ssSkP3(skc6,skc5) ).
cnf(u88,negated_conjecture,
group(skc5,skc6) ).
cnf(u93,negated_conjecture,
table(skc64,skc66) ).
cnf(u98,negated_conjecture,
group(skc64,skc65) ).
cnf(u106,negated_conjecture,
member(skc64,skf31(skc64,skc65),skc65) ).
cnf(u109,negated_conjecture,
~ member(skc64,skf34(skc64,skc65),skc65) ).
cnf(u122,negated_conjecture,
~ ssSkP3(skc65,skc64) ).
cnf(u127,negated_conjecture,
ssSkP1(skf31(skc64,skc65),skf29(skc64,skf31(skc64,skc65)),skc64) ).
cnf(u131,negated_conjecture,
group(skc64,skf24(skc64,X1,X2)) ).
cnf(u179,negated_conjecture,
( guy(skc64,skf34(skc64,skf24(skc64,X0,X1)))
| member(skc64,skf31(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u183,negated_conjecture,
( young(skc64,skf34(skc64,skf24(skc64,X0,X1)))
| member(skc64,skf31(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u187,negated_conjecture,
member(skc64,skf31(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ).
cnf(u204,negated_conjecture,
( ~ member(skc64,X1,X2)
| ~ ssSkP3(X2,skc64) ) ).
cnf(u207,negated_conjecture,
( young(skc64,skf34(skc64,skf29(skc64,X0)))
| member(skc64,skf31(skc64,skf29(skc64,X0)),skf29(skc64,X0)) ) ).
cnf(u211,negated_conjecture,
( guy(skc64,skf34(skc64,skf29(skc64,X0)))
| member(skc64,skf31(skc64,skf29(skc64,X0)),skf29(skc64,X0)) ) ).
cnf(u234,negated_conjecture,
guy(skc64,skf31(skc64,skf24(skc64,X3,X4))) ).
cnf(u238,negated_conjecture,
young(skc64,skf31(skc64,skf24(skc64,X3,X4))) ).
cnf(u290,negated_conjecture,
( member(skc64,skf22(skf31(skc64,X2),skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1))
| member(skc64,skf32(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u309,negated_conjecture,
( guy(skc64,skf22(skf31(skc64,X5),skc64,skf24(skc64,X0,X1)))
| member(skc64,skf32(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u313,negated_conjecture,
( young(skc64,skf22(skf31(skc64,X5),skc64,skf24(skc64,X0,X1)))
| member(skc64,skf32(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u317,negated_conjecture,
( ~ ssSkP1(X5,X6,skc64)
| ~ member(skc64,X7,X6) ) ).
cnf(u320,negated_conjecture,
( ~ member(skc64,skf22(skf31(skc64,X4),skc64,skf24(skc64,X0,X1)),X3)
| ssSkP1(skf31(skc64,X4),X8,skc64)
| ~ ssSkP1(skf31(skc64,X4),skf24(skc64,X0,X1),skc64)
| member(skc64,skf32(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1))
| ~ ssSkP1(X2,X3,skc64) ) ).
cnf(u366,negated_conjecture,
guy(skc64,skf22(X3,skc64,skf24(skc64,X4,X5))) ).
cnf(u370,negated_conjecture,
young(skc64,skf22(X3,skc64,skf24(skc64,X4,X5))) ).
cnf(u384,negated_conjecture,
( member(skc64,skf17(skf24(skc64,X0,X1),skc64,X2,X3),skf24(skc64,X0,X1))
| member(skc64,skf27(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u401,negated_conjecture,
( guy(skc64,skf17(skf24(skc64,X0,X1),skc64,X5,X6))
| member(skc64,skf27(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u405,negated_conjecture,
( young(skc64,skf17(skf24(skc64,X0,X1),skc64,X5,X6))
| member(skc64,skf27(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u428,negated_conjecture,
( member(skc64,skf32(skc64,skf24(skc64,X2,X3)),skf24(skc64,X2,X3))
| member(skc64,skf17(skf24(skc64,X2,X3),skc64,X7,X8),skf24(skc64,X2,X3)) ) ).
cnf(u448,negated_conjecture,
( ~ guy(skc64,skf32(skc64,X0))
| ~ young(skc64,skf32(skc64,X0)) ) ).
cnf(u474,negated_conjecture,
young(skc64,skf32(skc64,skf24(skc64,X3,X4))) ).
cnf(u483,negated_conjecture,
( ~ three(skc64,X0)
| member(skc64,skf22(skf31(skc64,X4),skc64,X0),X0)
| ~ group(skc64,X0) ) ).
cnf(u549,negated_conjecture,
three(skc64,skf29(skc64,skf31(skc64,skc65))) ).
cnf(u569,negated_conjecture,
young(skc64,skf32(skc64,skf29(skc64,X2))) ).
cnf(u584,negated_conjecture,
member(skc64,skf22(skf31(skc64,X0),skc64,skf24(skc64,X1,X2)),skf24(skc64,X1,X2)) ).
cnf(u603,negated_conjecture,
young(skc64,skf22(skf31(skc64,X2),skc64,skf29(skc64,X3))) ).
cnf(u607,negated_conjecture,
guy(skc64,skf22(skf31(skc64,X2),skc64,skf29(skc64,X3))) ).
cnf(u662,negated_conjecture,
young(skc64,skf22(X2,skc64,skf29(skc64,X3))) ).
cnf(u666,negated_conjecture,
guy(skc64,skf22(X2,skc64,skf29(skc64,X3))) ).
cnf(u740,negated_conjecture,
~ ssSkP3(skf24(skc64,X0,X1),skc64) ).
cnf(u752,negated_conjecture,
ssSkP3(skf29(skc64,skf31(skc64,skc65)),skc64) ).
cnf(u807,negated_conjecture,
( ~ ssSkP0(X2,X5,skc65,skc64)
| ~ table(skc64,X3)
| ~ ssSkP0(X2,X3,skc65,skc64)
| ssSkP1(X2,X4,skc64) ) ).
cnf(u816,negated_conjecture,
member(skc64,skf17(skc65,skc64,X3,X4),skc65) ).
cnf(u878,negated_conjecture,
member(skc64,skf17(skf24(skc64,X2,X3),skc64,X7,X8),skf24(skc64,X2,X3)) ).
cnf(u895,negated_conjecture,
guy(skc64,skf17(skf24(skc64,X3,X4),skc64,X5,X6)) ).
cnf(u899,negated_conjecture,
young(skc64,skf17(skf24(skc64,X3,X4),skc64,X5,X6)) ).
cnf(u929,negated_conjecture,
( ~ member(skc64,skf31(skc64,skc65),X2)
| ~ ssSkP2(X0,skc65,skc64)
| ~ table(skc64,X0)
| ~ ssSkP2(X0,X2,skc64)
| ~ member(skc64,skf31(skc64,skc65),X1)
| ~ ssSkP2(X0,X1,skc64) ) ).
cnf(u967,negated_conjecture,
~ ssSkP2(X4,skc6,skc5) ).
cnf(u975,negated_conjecture,
ssSkP3(X4,skc5) ).
cnf(u988,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(u1043,negated_conjecture,
young(skc5,skf34(skc5,skf29(skc5,X2))) ).
cnf(u1050,negated_conjecture,
guy(skc5,skf34(skc5,skf29(skc5,X2))) ).
cnf(u1072,negated_conjecture,
guy(skc5,skf34(skc5,skf24(skc5,X3,X4))) ).
cnf(u1076,negated_conjecture,
young(skc5,skf34(skc5,skf24(skc5,X3,X4))) ).
cnf(u1119,negated_conjecture,
( young(skc5,skf17(skf29(skc5,X0),skc5,X3,X4))
| member(skc5,skf27(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ) ).
cnf(u1123,negated_conjecture,
( guy(skc5,skf17(skf29(skc5,X0),skc5,X3,X4))
| member(skc5,skf27(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ) ).
cnf(u1144,negated_conjecture,
( ~ group(skc5,X0)
| member(skc5,skf14(skc5,X0),X0) ) ).
cnf(u1188,negated_conjecture,
young(skc5,skf14(skc5,skf29(skc5,X2))) ).
cnf(u1192,negated_conjecture,
guy(skc5,skf14(skc5,skf29(skc5,X2))) ).
cnf(u1224,negated_conjecture,
~ ssSkP2(X0,skf29(skc5,X1),skc5) ).
cnf(u1254,negated_conjecture,
young(skc5,skf26(skc5,X2,skf29(skc5,X3))) ).
cnf(u1258,negated_conjecture,
guy(skc5,skf26(skc5,X2,skf29(skc5,X3))) ).
cnf(u1266,negated_conjecture,
( ~ group(skc5,X0)
| member(skc5,skf26(skc5,skf19(skc5,X1,X2),X0),X0) ) ).
cnf(u1333,negated_conjecture,
( guy(skc64,skf14(skc64,skf24(skc64,X0,X1)))
| member(skc64,skf26(skc64,skc66,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u1337,negated_conjecture,
( young(skc64,skf14(skc64,skf24(skc64,X0,X1)))
| member(skc64,skf26(skc64,skc66,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u1391,negated_conjecture,
( guy(skc5,skf22(skf31(skc5,X5),skc5,skf24(skc5,X0,X1)))
| member(skc5,skf32(skc5,skf24(skc5,X0,X1)),skf24(skc5,X0,X1)) ) ).
cnf(u1395,negated_conjecture,
( young(skc5,skf22(skf31(skc5,X5),skc5,skf24(skc5,X0,X1)))
| member(skc5,skf32(skc5,skf24(skc5,X0,X1)),skf24(skc5,X0,X1)) ) ).
cnf(u1617,negated_conjecture,
~ group(skc64,skf29(skc64,skf31(skc64,skc65))) ).
cnf(u1698,negated_conjecture,
member(skc64,skf26(skc64,skc66,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ).
cnf(u1719,negated_conjecture,
guy(skc64,skf26(skc64,skc66,skf24(skc64,X3,X4))) ).
cnf(u1723,negated_conjecture,
young(skc64,skf26(skc64,skc66,skf24(skc64,X3,X4))) ).
cnf(u1727,negated_conjecture,
~ ssSkP2(skc66,skf24(skc64,X2,X3),skc64) ).
cnf(u1731,negated_conjecture,
( member(skc64,skf27(skc64,skf24(skc64,skc66,skf26(skc64,skc66,skf24(skc64,X0,X1)))),skf24(skc64,skc66,skf26(skc64,skc66,skf24(skc64,X0,X1))))
| ~ ssSkP2(skc66,skf24(skc64,X0,X1),skc64) ) ).
cnf(u824,negated_conjecture,
hamburger(skc64,skf17(skc65,skc64,X0,X1)) ).
cnf(u411,negated_conjecture,
( ~ member(skc64,skf22(skf31(skc64,X0),skc64,skf24(skc64,X5,X6)),X8)
| ~ ssSkP0(X2,X3,X4,skc64)
| ~ member(skc64,skf22(skf31(skc64,X0),skc64,skf24(skc64,X5,X6)),X4)
| ~ ssSkP0(skf31(skc64,X0),X7,X8,skc64)
| ssSkP1(skf31(skc64,X0),X1,skc64)
| ~ ssSkP0(skf31(skc64,X0),X9,skf24(skc64,X5,X6),skc64)
| ~ table(skc64,X7)
| member(skc64,skf32(skc64,skf24(skc64,X5,X6)),skf24(skc64,X5,X6)) ) ).
cnf(u936,negated_conjecture,
( ~ table(skc64,X0)
| member(skc64,skf26(skc64,X0,skc65),skc65) ) ).
cnf(u951,negated_conjecture,
member(skc5,skf34(skc5,skc6),skc6) ).
cnf(clause22,negated_conjecture,
( ~ member(X0,X1,X2)
| ~ ssSkP2(X3,X2,X0)
| group(X0,skf24(X0,X4,X5)) ) ).
cnf(u1688,negated_conjecture,
( ssSkP1(skf31(skc64,skf24(skc64,X0,X1)),X2,skc64)
| member(skc64,skf26(skc64,skc66,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u1165,negated_conjecture,
( ~ ssSkP2(X0,X1,skc5)
| ~ table(skc5,X0)
| ~ group(skc5,X1) ) ).
cnf(clause37,negated_conjecture,
( ~ member(X0,X1,skf24(X0,X2,X3))
| ~ member(X0,X4,X5)
| ~ ssSkP2(X6,X5,X0)
| guy(X0,X1) ) ).
cnf(u1306,negated_conjecture,
ssSkP1(skf26(skc5,X0,skf29(skc5,X1)),skf29(skc5,skf26(skc5,X0,skf29(skc5,X1))),skc5) ).
cnf(u153,negated_conjecture,
( member(skc64,skf34(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1))
| member(skc64,skf31(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u1272,negated_conjecture,
( ~ member(skc5,skf17(skf29(skc5,X0),skc5,X4,X5),X6)
| ~ ssSkP0(X1,X2,X3,skc5)
| ~ member(skc5,skf17(skf29(skc5,X0),skc5,X4,X5),X3)
| ~ ssSkP0(X4,X5,X6,skc5)
| member(skc5,skf27(skc5,skf29(skc5,X0)),skf29(skc5,X0))
| ~ ssSkP0(X4,X7,skf29(skc5,X0),skc5)
| ssSkP0(X4,X5,skf29(skc5,X0),skc5) ) ).
cnf(u1228,negated_conjecture,
member(skc5,skf26(skc5,X0,skc6),skc6) ).
cnf(u276,negated_conjecture,
( ~ member(X2,skf22(X0,X2,X5),X9)
| ~ ssSkP1(X3,X4,X2)
| ~ member(X2,skf22(X0,X2,X5),X4)
| ~ ssSkP1(X6,X7,X2)
| ~ member(X2,X8,X7)
| ~ ssSkP1(X0,X9,X2)
| ssSkP1(X0,X1,X2) ) ).
cnf(u1482,negated_conjecture,
( ssSkP1(skf17(skf29(skc5,X0),skc5,X1,X2),skf29(skc5,skf17(skf29(skc5,X0),skc5,X1,X2)),skc5)
| member(skc5,skf27(skc5,skf29(skc5,X0)),skf29(skc5,X0))
| member(skc5,skf31(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ) ).
cnf(u907,negated_conjecture,
( ~ member(skc64,skf31(skc64,skf24(skc64,X2,X3)),X4)
| ~ ssSkP2(X0,X1,skc64)
| ~ member(skc64,skf31(skc64,skf24(skc64,X2,X3)),X1)
| ~ ssSkP2(X0,X4,skc64)
| ~ table(skc64,X0)
| ~ ssSkP2(X0,skf24(skc64,X2,X3),skc64)
| ssSkP1(skf31(skc64,skf24(skc64,X2,X3)),X5,skc64) ) ).
cnf(u872,negated_conjecture,
( ~ ssSkP0(X4,X5,skf24(skc64,X2,X0),skc64)
| ssSkP1(X0,X3,skc64)
| ~ ssSkP0(X0,X1,skf24(skc64,X2,X0),skc64)
| ~ table(skc64,X1)
| ~ ssSkP2(X2,X6,skc64)
| ~ member(skc64,X0,X6) ) ).
cnf(u904,negated_conjecture,
( ~ member(skc64,X0,X5)
| ~ table(skc64,X2)
| ~ ssSkP2(X2,X3,skc64)
| ~ member(skc64,X0,X3)
| ~ ssSkP2(X2,X4,skc64)
| ~ member(skc64,X0,X4)
| ~ ssSkP2(X2,X5,skc64)
| ssSkP1(X0,X1,skc64) ) ).
cnf(u1152,negated_conjecture,
member(skc5,skf14(skc5,skc6),skc6) ).
cnf(u999,negated_conjecture,
( member(skc5,skf34(skc5,skf29(skc5,X0)),skf29(skc5,X0))
| member(skc5,skf31(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ) ).
cnf(u1103,negated_conjecture,
( member(skc64,skf14(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1))
| member(skc64,skf26(skc64,skc66,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(clause25,negated_conjecture,
( event(X0,skf15(X0,X5,X6,X7))
| ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u421,negated_conjecture,
( ~ ssSkP0(skf31(skc64,X4),X7,skf24(skc64,X2,X3),skc64)
| ~ ssSkP0(skf31(skc64,X4),X5,skf24(skc64,X2,X3),skc64)
| ssSkP1(skf31(skc64,X4),X6,skc64)
| ~ ssSkP0(X0,X1,skf24(skc64,X2,X3),skc64)
| ~ table(skc64,X5)
| member(skc64,skf32(skc64,skf24(skc64,X2,X3)),skf24(skc64,X2,X3)) ) ).
cnf(u1100,negated_conjecture,
( ~ ssSkP1(X4,X5,X0)
| member(X0,skf14(X0,X1),X1)
| ~ group(X0,X1)
| member(X0,skf26(X0,skf19(X0,X2,X3),X1),X1)
| ~ actual_world(X0)
| ~ member(X0,X6,X5) ) ).
cnf(u1339,negated_conjecture,
( ~ member(X0,X4,X5)
| ~ group(X0,X1)
| member(X0,skf26(X0,skf19(X0,X2,X3),X1),X1)
| ~ actual_world(X0)
| member(X0,skf14(X0,X1),X1)
| member(X0,skf22(X6,X0,X5),X5) ) ).
cnf(clause44,negated_conjecture,
( ~ ssSkP0(skf26(X0,X3,X4),X3,X2,X0)
| ~ guy(X0,skf27(X0,X1))
| ~ group(X0,X2)
| ~ three(X0,X2)
| ~ young(X0,skf27(X0,X1))
| ssSkP2(X3,X5,X0) ) ).
cnf(u1684,negated_conjecture,
( ~ member(skc64,skf31(skc64,skf24(skc64,X2,X3)),X1)
| ~ ssSkP2(X0,X1,skc64)
| ~ ssSkP2(X0,skf24(skc64,X2,X3),skc64)
| ~ table(skc64,X0)
| ssSkP1(skf31(skc64,skf24(skc64,X2,X3)),X4,skc64) ) ).
cnf(clause14,negated_conjecture,
( three(X0,skf29(X0,X3))
| ~ ssSkP3(X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u672,negated_conjecture,
( ~ member(skc64,skf22(X0,skc64,skf24(skc64,X5,X6)),X8)
| ~ ssSkP0(X2,X3,X4,skc64)
| ~ member(skc64,skf22(X0,skc64,skf24(skc64,X5,X6)),X4)
| ~ ssSkP0(X0,X7,X8,skc64)
| ssSkP1(X0,X1,skc64)
| ~ ssSkP0(X0,X9,skf24(skc64,X5,X6),skc64)
| ~ table(skc64,X7) ) ).
cnf(u331,negated_conjecture,
member(skc64,skf22(X0,skc64,skf24(skc64,X1,X2)),skf24(skc64,X1,X2)) ).
cnf(u871,negated_conjecture,
( ~ ssSkP0(X4,X7,skf24(skc64,X2,X3),skc64)
| ~ ssSkP0(X4,X5,skf24(skc64,X2,X3),skc64)
| ssSkP1(X4,X6,skc64)
| ~ ssSkP0(X0,X1,skf24(skc64,X2,X3),skc64)
| ~ table(skc64,X5) ) ).
cnf(u915,negated_conjecture,
( ~ member(skc64,skf22(X2,skc64,skf24(skc64,X3,X4)),X5)
| ~ ssSkP2(X0,X1,skc64)
| ~ member(skc64,skf22(X2,skc64,skf24(skc64,X3,X4)),X1)
| ~ ssSkP2(X0,X5,skc64)
| ~ table(skc64,X0)
| ~ ssSkP2(X0,skf24(skc64,X3,X4),skc64)
| ssSkP1(skf22(X2,skc64,skf24(skc64,X3,X4)),X6,skc64) ) ).
cnf(u422,negated_conjecture,
( ~ ssSkP0(skf31(skc64,X0),X1,skf24(skc64,X2,skf31(skc64,X0)),skc64)
| ssSkP1(skf31(skc64,X0),X3,skc64)
| ~ ssSkP0(X4,X5,skf24(skc64,X2,skf31(skc64,X0)),skc64)
| ~ table(skc64,X1)
| member(skc64,skf32(skc64,skf24(skc64,X2,skf31(skc64,X0))),skf24(skc64,X2,skf31(skc64,X0)))
| ~ ssSkP2(X2,X6,skc64)
| ~ member(skc64,skf31(skc64,X0),X6) ) ).
cnf(clause1,negated_conjecture,
actual_world(skc64) ).
cnf(u409,negated_conjecture,
( ~ member(X0,skf22(X2,X0,X7),X10)
| ssSkP1(X2,X3,X0)
| ~ ssSkP0(X4,X5,X6,X0)
| ~ member(X0,skf22(X2,X0,X7),X6)
| ~ ssSkP0(X2,X1,X8,X0)
| ~ member(X0,skf22(X2,X0,X7),X8)
| ~ ssSkP0(X2,X9,X10,X0)
| ~ table(X0,X1) ) ).
cnf(clause32,negated_conjecture,
( at(X0,skf15(X0,X1,X3,X4),X4)
| ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u1155,negated_conjecture,
hamburger(skc5,skf14(skc5,skc6)) ).
cnf(u263,negated_conjecture,
( ~ at(X0,skf18(X0,skf22(X1,X0,X2),X3),X4)
| ~ with(X0,skf18(X0,skf22(X1,X0,X2),X3),X1)
| ~ table(X0,X4)
| ssSkP1(X1,X5,X0)
| ~ ssSkP1(X6,X7,X0)
| ~ member(X0,skf22(X1,X0,X2),X7) ) ).
cnf(u1776,negated_conjecture,
( ~ ssSkP0(X2,X3,skf24(skc64,X4,skf31(skc64,X0)),skc64)
| ssSkP1(skf31(skc64,X0),X1,skc64)
| ~ table(skc64,X4)
| member(skc64,skf32(skc64,skf24(skc64,X4,skf31(skc64,X0))),skf24(skc64,X4,skf31(skc64,X0)))
| ~ ssSkP2(X4,X5,skc64)
| ~ member(skc64,skf31(skc64,X0),X5)
| ~ ssSkP2(X4,X6,skc64)
| ~ member(skc64,skf31(skc64,X0),X6) ) ).
cnf(u1686,negated_conjecture,
( ~ ssSkP2(X0,skf24(skc64,X1,X2),skc64)
| ~ table(skc64,X0)
| ssSkP1(skf31(skc64,skf24(skc64,X1,X2)),X3,skc64) ) ).
cnf(u1027,negated_conjecture,
member(skc5,skf34(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ).
cnf(u1101,negated_conjecture,
( ~ group(skc64,X0)
| member(skc64,skf14(skc64,X0),X0)
| member(skc64,skf26(skc64,skc66,X0),X0) ) ).
cnf(u1085,negated_conjecture,
( ~ table(X0,X2)
| ~ actual_world(X0)
| member(X0,skf14(X0,X1),X1)
| ~ group(X0,X1)
| member(X0,skf26(X0,X2,X1),X1) ) ).
cnf(u1246,negated_conjecture,
( ~ ssSkP3(skf29(skc5,X0),skc5)
| ssSkP1(skf26(skc5,X1,skf29(skc5,X0)),skf29(skc5,skf26(skc5,X1,skf29(skc5,X0))),skc5) ) ).
cnf(u162,negated_conjecture,
( ~ member(X0,X5,X4)
| member(X0,skf32(X0,skf29(X0,X1)),skf29(X0,X1))
| member(X0,skf22(skf31(X0,X3),X0,skf29(X0,X1)),skf29(X0,X1))
| ~ ssSkP3(X4,X0)
| ssSkP3(X2,X0) ) ).
cnf(u410,negated_conjecture,
( ~ member(X3,skf17(X2,X3,X0,X1),X9)
| ~ ssSkP0(X4,X5,X6,X3)
| ~ member(X3,skf17(X2,X3,X0,X1),X6)
| ~ ssSkP0(X0,X1,X7,X3)
| ~ member(X3,skf17(X2,X3,X0,X1),X7)
| ~ ssSkP0(X0,X8,X9,X3)
| ssSkP0(X0,X1,X2,X3) ) ).
cnf(u415,negated_conjecture,
( ~ member(skc64,skf17(skf24(skc64,X3,X4),skc64,X5,X6),X7)
| ~ member(skc64,skf17(skf24(skc64,X3,X4),skc64,X5,X6),X2)
| ~ ssSkP0(X5,X6,X7,skc64)
| ~ ssSkP0(X0,X1,X2,skc64)
| ~ ssSkP0(X5,X8,skf24(skc64,X3,X4),skc64)
| ssSkP0(X5,X6,skf24(skc64,X3,X4),skc64)
| member(skc64,skf27(skc64,skf24(skc64,X3,X4)),skf24(skc64,X3,X4)) ) ).
cnf(u413,negated_conjecture,
( ~ ssSkP1(skf31(skc64,X0),skf24(skc64,X2,X3),skc64)
| ssSkP1(skf31(skc64,X0),X1,skc64)
| member(skc64,skf32(skc64,skf24(skc64,X2,X3)),skf24(skc64,X2,X3))
| ~ ssSkP1(X4,skf24(skc64,X2,X3),skc64) ) ).
cnf(clause8,negated_conjecture,
( ssSkP3(X0,X1)
| member(X1,skf31(X1,X0),X0) ) ).
cnf(clause36,negated_conjecture,
( at(X0,skf18(X0,X4,X5),skf19(X0,X5,X4))
| ~ ssSkP1(X3,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u677,negated_conjecture,
( ~ ssSkP3(skf24(skc64,X0,X1),skc64)
| ssSkP1(skf22(X2,skc64,skf24(skc64,X0,X1)),skf29(skc64,skf22(X2,skc64,skf24(skc64,X0,X1))),skc64) ) ).
cnf(clause31,negated_conjecture,
( agent(X0,skf15(X0,X1,X5,X6),X1)
| ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(clause43,negated_conjecture,
( ~ ssSkP1(skf31(X0,X3),X2,X0)
| ~ guy(X0,skf32(X0,X1))
| ~ group(X0,X2)
| ~ three(X0,X2)
| ~ young(X0,skf32(X0,X1))
| ssSkP3(X4,X0) ) ).
cnf(clause34,negated_conjecture,
( ~ member(X0,X1,skf29(X0,X2))
| ~ member(X0,X3,X4)
| ~ ssSkP3(X4,X0)
| young(X0,X1) ) ).
cnf(u1180,negated_conjecture,
( ~ ssSkP3(skf29(skc5,X0),skc5)
| ssSkP1(skf14(skc5,skf29(skc5,X0)),skf29(skc5,skf14(skc5,skf29(skc5,X0))),skc5) ) ).
cnf(u166,negated_conjecture,
( ~ member(X0,X7,X6)
| member(X0,skf27(X0,skf29(X0,X1)),skf29(X0,X1))
| member(X0,skf17(skf29(X0,X1),X0,X4,X5),skf29(X0,X1))
| ~ ssSkP3(X6,X0)
| ssSkP2(X2,X3,X0) ) ).
cnf(u901,negated_conjecture,
( ~ ssSkP0(X0,X2,skf24(skc64,X3,X0),skc64)
| ssSkP1(X0,X1,skc64)
| ~ table(skc64,X2)
| ~ ssSkP2(X3,X4,skc64)
| ~ member(skc64,X0,X4)
| ~ ssSkP2(X3,X5,skc64)
| ~ member(skc64,X0,X5) ) ).
cnf(u1240,negated_conjecture,
ssSkP1(skf26(skc5,X0,skc6),skf29(skc5,skf26(skc5,X0,skc6)),skc5) ).
cnf(u230,negated_conjecture,
( ~ ssSkP3(skf24(skc64,X0,X1),skc64)
| ssSkP1(skf31(skc64,skf24(skc64,X0,X1)),skf29(skc64,skf31(skc64,skf24(skc64,X0,X1))),skc64) ) ).
cnf(u1307,negated_conjecture,
ssSkP1(skf14(skc5,skf29(skc5,X0)),skf29(skc5,skf14(skc5,skf29(skc5,X0))),skc5) ).
cnf(clause12,negated_conjecture,
( ssSkP2(X0,X1,X2)
| member(X2,skf26(X2,X0,X1),X1) ) ).
cnf(u244,negated_conjecture,
( ~ guy(X0,skf27(X0,X1))
| ~ group(X0,X2)
| ~ three(X0,X2)
| ~ young(X0,skf27(X0,X1))
| ssSkP2(X3,X4,X0)
| member(X0,skf17(X2,X0,X5,X6),X2) ) ).
cnf(clause19,negated_conjecture,
( present(X0,skf18(X0,X4,X5))
| ~ ssSkP1(X3,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(clause38,negated_conjecture,
( ~ member(X0,X1,skf24(X0,X2,X3))
| ~ member(X0,X4,X5)
| ~ ssSkP2(X6,X5,X0)
| young(X0,X1) ) ).
cnf(u1002,negated_conjecture,
hamburger(skc5,skf34(skc5,skc6)) ).
cnf(u154,negated_conjecture,
( ~ three(X0,X1)
| ~ group(X0,X1)
| ssSkP3(X2,X0)
| member(X0,skf32(X0,X1),X1)
| member(X0,skf22(skf31(X0,X3),X0,X1),X1) ) ).
cnf(u1038,negated_conjecture,
ssSkP1(skf34(skc5,skf29(skc5,X0)),skf29(skc5,skf34(skc5,skf29(skc5,X0))),skc5) ).
cnf(u1481,negated_conjecture,
( ssSkP1(skf17(skf29(skc5,X0),skc5,X1,X2),skf29(skc5,skf17(skf29(skc5,X0),skc5,X1,X2)),skc5)
| member(skc5,skf27(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ) ).
cnf(u614,negated_conjecture,
( ~ member(skc64,skf22(X0,skc64,skc65),X6)
| ~ ssSkP0(X2,X3,X4,skc64)
| ~ member(skc64,skf22(X0,skc64,skc65),X4)
| ~ ssSkP0(X0,X5,X6,skc64)
| ssSkP1(X0,X1,skc64)
| ~ ssSkP0(X0,X7,skc65,skc64)
| ~ table(skc64,X5) ) ).
cnf(u408,negated_conjecture,
( ~ with(X0,skf15(X0,skf17(X1,X0,X2,X3),X4,X3),X2)
| ssSkP0(X2,X3,X1,X0)
| ~ ssSkP0(X5,X6,X7,X0)
| ~ member(X0,skf17(X1,X0,X2,X3),X7)
| ~ ssSkP0(X4,X3,X8,X0)
| ~ member(X0,skf17(X1,X0,X2,X3),X8) ) ).
cnf(clause23,negated_conjecture,
( with(X0,skf18(X0,X1,X3),X3)
| ~ ssSkP1(X3,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u920,negated_conjecture,
( ~ member(skc64,skf17(skc65,skc64,X2,X3),X4)
| ~ ssSkP2(X0,X1,skc64)
| ~ member(skc64,skf17(skc65,skc64,X2,X3),X1)
| ~ ssSkP2(X0,X4,skc64)
| ~ table(skc64,X0)
| ~ ssSkP2(X0,skc65,skc64)
| ssSkP1(skf17(skc65,skc64,X2,X3),X5,skc64) ) ).
cnf(u948,negated_conjecture,
( ~ ssSkP2(X0,skc65,skc64)
| ~ table(skc64,X0) ) ).
cnf(u883,negated_conjecture,
( ~ member(skc64,skf17(skf24(skc64,X3,X4),skc64,X5,X6),X7)
| ~ member(skc64,skf17(skf24(skc64,X3,X4),skc64,X5,X6),X2)
| ~ ssSkP0(X5,X6,X7,skc64)
| ~ ssSkP0(X0,X1,X2,skc64)
| ~ ssSkP0(X5,X8,skf24(skc64,X3,X4),skc64)
| ssSkP0(X5,X6,skf24(skc64,X3,X4),skc64) ) ).
cnf(u255,negated_conjecture,
( ~ at(X0,skf18(X0,skf17(X1,X0,X2,X3),X4),X3)
| ~ with(X0,skf18(X0,skf17(X1,X0,X2,X3),X4),X2)
| ssSkP0(X2,X3,X1,X0)
| ~ ssSkP1(X5,X6,X0)
| ~ member(X0,skf17(X1,X0,X2,X3),X6) ) ).
cnf(clause26,negated_conjecture,
( present(X0,skf15(X0,X5,X6,X7))
| ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u1270,negated_conjecture,
( ssSkP1(skf14(skc5,skf29(skc5,X0)),skf29(skc5,skf14(skc5,skf29(skc5,X0))),skc5)
| member(skc5,skf31(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ) ).
cnf(u262,negated_conjecture,
( ~ at(X0,skf15(X0,skf22(X1,X0,X2),X3,X4),X5)
| ~ with(X0,skf15(X0,skf22(X1,X0,X2),X3,X4),X1)
| ~ table(X0,X5)
| ssSkP1(X1,X6,X0)
| ~ ssSkP0(X7,X8,X9,X0)
| ~ member(X0,skf22(X1,X0,X2),X9) ) ).
cnf(u1752,negated_conjecture,
( ~ member(skc64,skf26(skc64,skc66,skf24(skc64,X2,X3)),X1)
| ~ ssSkP2(X0,X1,skc64)
| ~ ssSkP2(X0,skf24(skc64,X2,X3),skc64)
| ~ table(skc64,X0)
| ssSkP1(skf26(skc64,skc66,skf24(skc64,X2,X3)),X4,skc64) ) ).
cnf(u158,negated_conjecture,
( ~ member(X0,skf26(X0,X1,X2),X4)
| member(X0,skf27(X0,skf24(X0,X1,skf26(X0,X1,X2))),skf24(X0,X1,skf26(X0,X1,X2)))
| ~ ssSkP2(X1,X4,X0)
| ssSkP2(X1,X3,X0) ) ).
cnf(clause41,negated_conjecture,
( ~ ssSkP1(skf31(X0,X2),X1,X0)
| ~ three(X0,X1)
| ~ group(X0,X1)
| ssSkP3(X3,X0)
| member(X0,skf32(X0,X1),X1) ) ).
cnf(u1229,negated_conjecture,
member(skc5,skf26(skc5,X0,skf29(skc5,X1)),skf29(skc5,X1)) ).
cnf(u1760,negated_conjecture,
( ~ member(skc64,skf17(skf24(skc64,X2,X3),skc64,X4,X5),X1)
| ~ ssSkP2(X0,X1,skc64)
| ~ ssSkP2(X0,skf24(skc64,X2,X3),skc64)
| ~ table(skc64,X0)
| ssSkP1(skf17(skf24(skc64,X2,X3),skc64,X4,X5),X6,skc64)
| member(skc64,skf27(skc64,skf24(skc64,X2,X3)),skf24(skc64,X2,X3)) ) ).
cnf(u173,negated_conjecture,
( ssSkP1(skf34(skc64,skf24(skc64,X0,X1)),skf29(skc64,skf34(skc64,skf24(skc64,X0,X1))),skc64)
| member(skc64,skf31(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1)) ) ).
cnf(u1319,negated_conjecture,
( ~ member(skc64,skf14(skc64,skf24(skc64,X0,X1)),X4)
| ~ table(skc64,X2)
| ~ ssSkP2(X2,X3,skc64)
| ~ member(skc64,skf14(skc64,skf24(skc64,X0,X1)),X3)
| ~ ssSkP2(X2,X4,skc64)
| member(skc64,skf26(skc64,skc66,skf24(skc64,X0,X1)),skf24(skc64,X0,X1))
| ~ ssSkP2(X2,skf24(skc64,X0,X1),skc64)
| ssSkP1(skf14(skc64,skf24(skc64,X0,X1)),X5,skc64) ) ).
cnf(u275,negated_conjecture,
( ~ with(X0,skf18(X0,skf22(X1,X0,X2),X3),X1)
| ssSkP1(X1,X4,X0)
| ~ ssSkP1(X5,X6,X0)
| ~ member(X0,skf22(X1,X0,X2),X6)
| ~ ssSkP1(X7,X8,X0)
| ~ member(X0,X9,X8) ) ).
cnf(clause11,negated_conjecture,
( ssSkP1(X0,X1,X2)
| member(X2,skf22(X0,X2,X1),X1) ) ).
cnf(u407,negated_conjecture,
( ~ with(X0,skf15(X0,skf22(X1,X0,X2),X3,X4),X1)
| ~ table(X0,X4)
| ssSkP1(X1,X5,X0)
| ~ ssSkP0(X6,X7,X8,X0)
| ~ member(X0,skf22(X1,X0,X2),X8)
| ~ ssSkP0(X3,X4,X9,X0)
| ~ member(X0,skf22(X1,X0,X2),X9) ) ).
cnf(u1687,negated_conjecture,
( ~ table(skc64,X0)
| ssSkP1(skf31(skc64,skf24(skc64,X1,X2)),X3,skc64)
| member(skc64,skf26(skc64,X0,skf24(skc64,X1,X2)),skf24(skc64,X1,X2)) ) ).
cnf(u243,negated_conjecture,
( ~ guy(X0,skf32(X0,X1))
| ~ group(X0,X2)
| ~ three(X0,X2)
| ~ young(X0,skf32(X0,X1))
| ssSkP3(X3,X0)
| member(X0,skf22(skf31(X0,X4),X0,X2),X2) ) ).
cnf(clause2,negated_conjecture,
actual_world(skc5) ).
cnf(clause17,negated_conjecture,
( table(X0,skf19(X0,X4,X5))
| ~ ssSkP1(X3,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(clause45,negated_conjecture,
( ~ agent(X0,X1,skf17(X4,X0,X2,X3))
| ~ at(X0,X1,X3)
| ~ sit(X0,X1)
| ~ present(X0,X1)
| ~ with(X0,X1,X2)
| ~ event(X0,X1)
| ssSkP0(X2,X3,X4,X0) ) ).
cnf(u997,negated_conjecture,
( ~ group(skc5,X0)
| member(skc5,skf34(skc5,X0),X0) ) ).
cnf(u1764,negated_conjecture,
( ~ ssSkP2(X0,skf24(skc64,X1,X2),skc64)
| ~ table(skc64,X0)
| ssSkP1(skf17(skf24(skc64,X1,X2),skc64,X3,X4),X5,skc64)
| member(skc64,skf27(skc64,skf24(skc64,X1,X2)),skf24(skc64,X1,X2)) ) ).
cnf(u1748,negated_conjecture,
( ~ table(skc64,X0)
| ssSkP1(skf22(X1,skc64,skf24(skc64,X2,X3)),X4,skc64)
| member(skc64,skf26(skc64,X0,skf24(skc64,X2,X3)),skf24(skc64,X2,X3)) ) ).
cnf(u1761,negated_conjecture,
( ~ member(skc64,skf17(skf24(skc64,X2,X3),skc64,X4,X5),X1)
| ~ ssSkP2(X0,X1,skc64)
| ~ ssSkP2(X0,skf24(skc64,X2,X3),skc64)
| ~ table(skc64,X0)
| ssSkP1(skf17(skf24(skc64,X2,X3),skc64,X4,X5),X6,skc64) ) ).
cnf(u1766,negated_conjecture,
( ~ table(skc64,X0)
| ssSkP1(skf17(skf24(skc64,X1,X2),skc64,X3,X4),X5,skc64)
| member(skc64,skf26(skc64,X0,skf24(skc64,X1,X2)),skf24(skc64,X1,X2)) ) ).
cnf(u1702,negated_conjecture,
( ~ member(skc64,skf26(skc64,skc66,skf24(skc64,X2,X3)),X4)
| ~ ssSkP2(X0,X1,skc64)
| ~ member(skc64,skf26(skc64,skc66,skf24(skc64,X2,X3)),X1)
| ~ ssSkP2(X0,X4,skc64)
| ~ table(skc64,X0)
| ~ ssSkP2(X0,skf24(skc64,X2,X3),skc64)
| ssSkP1(skf26(skc64,skc66,skf24(skc64,X2,X3)),X5,skc64) ) ).
cnf(u868,negated_conjecture,
( ~ member(skc64,skf22(X3,skc64,skf24(skc64,X4,X5)),X2)
| ~ ssSkP0(X0,X1,X2,skc64)
| ~ ssSkP0(X3,X6,skf24(skc64,X4,X5),skc64)
| ssSkP1(X3,X7,skc64)
| ~ ssSkP0(X3,X8,skf24(skc64,X4,X5),skc64)
| ~ table(skc64,X6) ) ).
cnf(u803,negated_conjecture,
( ~ member(skc64,skf22(X3,skc64,skc65),X2)
| ~ ssSkP0(X0,X1,X2,skc64)
| ~ ssSkP0(X3,X4,skc65,skc64)
| ssSkP1(X3,X5,skc64)
| ~ ssSkP0(X3,X6,skc65,skc64)
| ~ table(skc64,X4) ) ).
cnf(u247,negated_conjecture,
( ~ member(X0,skf26(X0,X2,X3),X5)
| ~ young(X0,skf27(X0,X1))
| ssSkP2(X2,X4,X0)
| ~ ssSkP2(X2,X5,X0)
| ~ guy(X0,skf27(X0,X1)) ) ).
cnf(u913,negated_conjecture,
( ~ member(skc64,skf22(X2,skc64,skc65),X3)
| ~ ssSkP2(X0,X1,skc64)
| ~ member(skc64,skf22(X2,skc64,skc65),X1)
| ~ ssSkP2(X0,X3,skc64)
| ~ table(skc64,X0)
| ~ ssSkP2(X0,skc65,skc64)
| ssSkP1(skf22(X2,skc64,skc65),X4,skc64) ) ).
cnf(clause21,negated_conjecture,
( three(X0,skf24(X0,X4,X5))
| ~ ssSkP2(X3,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(clause33,negated_conjecture,
( with(X0,skf15(X0,X1,X3,X5),X3)
| ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u985,negated_conjecture,
group(skc5,skf29(skc5,X0)) ).
cnf(clause24,negated_conjecture,
( agent(X0,skf18(X0,X1,X4),X1)
| ~ ssSkP1(X3,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u1745,negated_conjecture,
( ~ ssSkP2(X0,skf24(skc64,X1,X2),skc64)
| ~ table(skc64,X0)
| ssSkP1(skf22(X3,skc64,skf24(skc64,X1,X2)),X4,skc64) ) ).
cnf(u1276,negated_conjecture,
( ~ ssSkP3(skf29(skc5,X0),skc5)
| member(skc5,skf27(skc5,skf29(skc5,X0)),skf29(skc5,X0))
| ssSkP1(skf17(skf29(skc5,X0),skc5,X1,X2),skf29(skc5,skf17(skf29(skc5,X0),skc5,X1,X2)),skc5) ) ).
cnf(u332,negated_conjecture,
hamburger(skc64,skf22(X0,skc64,skc65)) ).
cnf(u1765,negated_conjecture,
( ~ ssSkP2(X0,skf24(skc64,X1,X2),skc64)
| ~ table(skc64,X0)
| ssSkP1(skf17(skf24(skc64,X1,X2),skc64,X3,X4),X5,skc64) ) ).
cnf(u917,negated_conjecture,
( ~ member(skc64,skf17(skf24(skc64,X2,X3),skc64,X4,X5),X6)
| ~ ssSkP2(X0,X1,skc64)
| ~ member(skc64,skf17(skf24(skc64,X2,X3),skc64,X4,X5),X1)
| ~ ssSkP2(X0,X6,skc64)
| ~ table(skc64,X0)
| ~ ssSkP2(X0,skf24(skc64,X2,X3),skc64)
| ssSkP1(skf17(skf24(skc64,X2,X3),skc64,X4,X5),X7,skc64)
| member(skc64,skf27(skc64,skf24(skc64,X2,X3)),skf24(skc64,X2,X3)) ) ).
cnf(u1755,negated_conjecture,
( ~ table(skc64,X0)
| ssSkP1(skf26(skc64,skc66,skf24(skc64,X1,X2)),X3,skc64)
| member(skc64,skf26(skc64,X0,skf24(skc64,X1,X2)),skf24(skc64,X1,X2)) ) ).
cnf(u254,negated_conjecture,
( ~ at(X0,skf15(X0,skf17(X1,X0,X2,X3),X4,X5),X3)
| ~ with(X0,skf15(X0,skf17(X1,X0,X2,X3),X4,X5),X2)
| ssSkP0(X2,X3,X1,X0)
| ~ ssSkP0(X6,X7,X8,X0)
| ~ member(X0,skf17(X1,X0,X2,X3),X8) ) ).
cnf(clause28,negated_conjecture,
( ssSkP0(X1,X3,skf24(X0,X3,X1),X0)
| ~ ssSkP2(X3,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u100,negated_conjecture,
( ~ group(X0,X1)
| ~ actual_world(X0)
| member(X0,skf34(X0,X1),X1)
| member(X0,skf31(X0,X1),X1) ) ).
cnf(u1163,negated_conjecture,
ssSkP1(skf14(skc5,skc6),skf29(skc5,skf14(skc5,skc6)),skc5) ).
cnf(clause35,negated_conjecture,
( ~ member(X0,X1,skf29(X0,X2))
| ~ member(X0,X3,X4)
| ~ ssSkP3(X4,X0)
| guy(X0,X1) ) ).
cnf(u1635,negated_conjecture,
~ member(skc64,X0,skf29(skc64,skf31(skc64,skc65))) ).
cnf(clause13,negated_conjecture,
( ssSkP0(X0,X1,X2,X3)
| member(X3,skf17(X2,X3,X4,X5),X2) ) ).
cnf(u393,negated_conjecture,
( ~ ssSkP3(skf24(skc64,X0,X1),skc64)
| member(skc64,skf27(skc64,skf24(skc64,X0,X1)),skf24(skc64,X0,X1))
| ssSkP1(skf17(skf24(skc64,X0,X1),skc64,X2,X3),skf29(skc64,skf17(skf24(skc64,X0,X1),skc64,X2,X3)),skc64) ) ).
cnf(u1194,negated_conjecture,
( ~ table(skc5,X0)
| ~ group(skc5,X1)
| member(skc5,skf26(skc5,X0,X1),X1) ) ).
cnf(clause16,negated_conjecture,
( ~ member(X0,X1,X2)
| ~ ssSkP3(X2,X0)
| ssSkP1(X1,skf29(X0,X1),X0) ) ).
cnf(u1153,negated_conjecture,
member(skc5,skf14(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ).
cnf(u112,negated_conjecture,
hamburger(skc64,skf31(skc64,skc65)) ).
cnf(u827,negated_conjecture,
( ~ member(skc64,skf17(skc65,skc64,X3,X4),X5)
| ~ member(skc64,skf17(skc65,skc64,X3,X4),X2)
| ~ ssSkP0(X3,X4,X5,skc64)
| ~ ssSkP0(X0,X1,X2,skc64)
| ~ ssSkP0(X3,X6,skc65,skc64)
| ssSkP0(X3,X4,skc65,skc64) ) ).
cnf(u1271,negated_conjecture,
( ssSkP1(skf26(skc5,X0,skf29(skc5,X1)),skf29(skc5,skf26(skc5,X0,skf29(skc5,X1))),skc5)
| member(skc5,skf31(skc5,skf29(skc5,X1)),skf29(skc5,X1)) ) ).
cnf(u419,negated_conjecture,
( ~ member(skc64,skf22(skf31(skc64,X3),skc64,skf24(skc64,X4,X5)),X2)
| ~ ssSkP0(X0,X1,X2,skc64)
| ~ ssSkP0(skf31(skc64,X3),X6,skf24(skc64,X4,X5),skc64)
| ssSkP1(skf31(skc64,X3),X7,skc64)
| ~ ssSkP0(skf31(skc64,X3),X8,skf24(skc64,X4,X5),skc64)
| ~ table(skc64,X6)
| member(skc64,skf32(skc64,skf24(skc64,X4,X5)),skf24(skc64,X4,X5)) ) ).
cnf(u155,negated_conjecture,
( ~ three(X0,X1)
| ~ group(X0,X1)
| ssSkP2(X2,X3,X0)
| member(X0,skf27(X0,X1),X1)
| member(X0,skf17(X1,X0,X4,X5),X1) ) ).
cnf(u623,negated_conjecture,
( ~ member(skc64,X0,X1)
| member(skc64,skf22(X2,skc64,X1),X1) ) ).
cnf(clause42,negated_conjecture,
( ~ ssSkP0(skf26(X0,X2,X3),X2,X1,X0)
| ~ three(X0,X1)
| ~ group(X0,X1)
| ssSkP2(X2,X4,X0)
| member(X0,skf27(X0,X1),X1) ) ).
cnf(u1230,negated_conjecture,
hamburger(skc5,skf26(skc5,X0,skc6)) ).
cnf(u325,negated_conjecture,
member(skc64,skf22(X0,skc64,skc65),skc65) ).
cnf(u1754,negated_conjecture,
( ~ ssSkP2(X0,skf24(skc64,X1,X2),skc64)
| ~ table(skc64,X0)
| ssSkP1(skf26(skc64,skc66,skf24(skc64,X1,X2)),X3,skc64) ) ).
cnf(u161,negated_conjecture,
( ~ member(X0,X7,X6)
| member(X0,skf32(X0,skf24(X0,X1,X2)),skf24(X0,X1,X2))
| member(X0,skf22(skf31(X0,X4),X0,skf24(X0,X1,X2)),skf24(X0,X1,X2))
| ~ ssSkP2(X5,X6,X0)
| ssSkP3(X3,X0) ) ).
cnf(u916,negated_conjecture,
( ~ member(skc64,skf17(skf24(skc64,X2,X3),skc64,X4,X5),X6)
| ~ ssSkP2(X0,X1,skc64)
| ~ member(skc64,skf17(skf24(skc64,X2,X3),skc64,X4,X5),X1)
| ~ ssSkP2(X0,X6,skc64)
| ~ table(skc64,X0)
| ~ ssSkP2(X0,skf24(skc64,X2,X3),skc64)
| ssSkP1(skf17(skf24(skc64,X2,X3),skc64,X4,X5),X7,skc64) ) ).
cnf(clause20,negated_conjecture,
( event(X0,skf18(X0,X4,X5))
| ~ ssSkP1(X3,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u1097,negated_conjecture,
( ssSkP1(skf34(skc5,skf29(skc5,X0)),skf29(skc5,skf34(skc5,skf29(skc5,X0))),skc5)
| member(skc5,skf31(skc5,skf29(skc5,X0)),skf29(skc5,X0)) ) ).
cnf(clause15,negated_conjecture,
( ~ member(X0,X1,X2)
| ~ ssSkP3(X2,X0)
| group(X0,skf29(X0,X3)) ) ).
cnf(clause27,negated_conjecture,
( sit(X0,skf15(X0,X5,X6,X7))
| ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(u984,negated_conjecture,
ssSkP1(skf34(skc5,skc6),skf29(skc5,skf34(skc5,skc6)),skc5) ).
cnf(u947,negated_conjecture,
( ~ member(skc64,skf31(skc64,skc65),X1)
| ~ table(skc64,X0)
| ~ ssSkP2(X0,skc65,skc64)
| ~ ssSkP2(X0,X1,skc64) ) ).
cnf(clause18,negated_conjecture,
( sit(X0,skf18(X0,X4,X5))
| ~ ssSkP1(X3,X2,X0)
| ~ member(X0,X1,X2) ) ).
cnf(clause46,negated_conjecture,
( ~ agent(X0,X1,skf22(X2,X0,X3))
| ~ event(X0,X1)
| ~ present(X0,X1)
| ~ sit(X0,X1)
| ~ with(X0,X1,X2)
| ~ at(X0,X1,X4)
| ~ table(X0,X4)
| ssSkP1(X2,X5,X0) ) ).
cnf(u1012,negated_conjecture,
hamburger(skc64,skf26(skc64,skc66,skc65)) ).
cnf(u953,negated_conjecture,
member(skc64,skf26(skc64,skc66,skc65),skc65) ).
cnf(u165,negated_conjecture,
( ~ member(X0,X9,X8)
| member(X0,skf27(X0,skf24(X0,X1,X2)),skf24(X0,X1,X2))
| member(X0,skf17(skf24(X0,X1,X2),X0,X5,X6),skf24(X0,X1,X2))
| ~ ssSkP2(X7,X8,X0)
| ssSkP2(X3,X4,X0) ) ).
cnf(u1739,negated_conjecture,
( ~ member(skc64,skf22(X2,skc64,skf24(skc64,X3,X4)),X1)
| ~ ssSkP2(X0,X1,skc64)
| ~ ssSkP2(X0,skf24(skc64,X3,X4),skc64)
| ~ table(skc64,X0)
| ssSkP1(skf22(X2,skc64,skf24(skc64,X3,X4)),X5,skc64) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP026-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.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 17:49:22 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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.92/1.50 % (3783762)Input is clausal, will run a generic CNF schedule.
% 2.92/1.50 % (3783771)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=419074915:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.92/1.50 % (3783771)Instruction limit reached!
% 2.92/1.50 % (3783771)------------------------------
% 2.92/1.50 % (3783771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.50 % (3783771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.50 % (3783771)CaDiCaL version: 2.1.3
% 2.92/1.50 % (3783771)Termination reason: Instruction limit
% 2.92/1.50 % (3783771)Termination phase: Saturation
% 2.92/1.50 % (3783771)Time elapsed: 0.029 s
% 2.92/1.50 % (3783771)Peak memory usage: 88 MB
% 2.92/1.50 % (3783771)Instructions burned: 116 (million)
% 2.92/1.50 % (3783770)lrs+10_1_sil=8000:sp=occurrence:random_seed=2013996597:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.92/1.50 % (3783768)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3906460666:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.92/1.50 % (3783769)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1664114709:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.92/1.50 % (3783767)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=2055020213:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.92/1.50 % (3783773)dis-21_1_sil=8000:lcm=predicate:random_seed=3917324880: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.92/1.50 % (3783772)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4197993395:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.92/1.50 % (3783772)Refutation not found, incomplete strategy
% 2.92/1.50 % (3783772)------------------------------
% 2.92/1.50 % (3783772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.50 % (3783772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.50 % (3783772)CaDiCaL version: 2.1.3
% 2.92/1.50 % (3783772)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.50 % (3783772)Time elapsed: 0.025 s
% 2.92/1.50 % (3783772)Peak memory usage: 88 MB
% 2.92/1.50 % (3783772)Instructions burned: 30 (million)
% 2.92/1.50 % (3783770)Instruction limit reached!
% 2.92/1.50 % (3783770)------------------------------
% 2.92/1.50 % (3783770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.50 % (3783770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.50 % (3783770)CaDiCaL version: 2.1.3
% 2.92/1.50 % (3783770)Termination reason: Instruction limit
% 2.92/1.50 % (3783770)Termination phase: Saturation
% 2.92/1.50 % (3783770)Time elapsed: 0.056 s
% 2.92/1.50 % (3783770)Peak memory usage: 88 MB
% 2.92/1.50 % (3783770)Instructions burned: 107 (million)
% 2.92/1.50 % (3783775)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=470943907:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 2.92/1.50 % (3783775)Refutation not found, incomplete strategy
% 2.92/1.50 % (3783775)------------------------------
% 2.92/1.50 % (3783775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.50 % (3783775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.50 % (3783775)CaDiCaL version: 2.1.3
% 2.92/1.50 % (3783775)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.50 % (3783775)Time elapsed: 0.006 s
% 2.92/1.50 % (3783775)Peak memory usage: 88 MB
% 2.92/1.50 % (3783775)Instructions burned: 17 (million)
% 2.92/1.50 % (3783773)Instruction limit reached!
% 2.92/1.50 % (3783773)------------------------------
% 2.92/1.50 % (3783773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.50 % (3783773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.50 % (3783773)CaDiCaL version: 2.1.3
% 2.92/1.50 % (3783773)Termination reason: Instruction limit
% 2.92/1.50 % (3783773)Termination phase: Saturation
% 2.92/1.50 % (3783773)Time elapsed: 0.074 s
% 2.92/1.50 % (3783773)Peak memory usage: 89 MB
% 2.92/1.50 % (3783773)Instructions burned: 118 (million)
% 2.92/1.50 % (3783782)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2016995084:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 2.92/1.50 % (3783782)Refutation not found, incomplete strategy
% 2.92/1.50 % (3783782)------------------------------
% 2.92/1.50 % (3783782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.50 % (3783782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.50 % (3783782)CaDiCaL version: 2.1.3
% 2.92/1.50 % (3783782)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.50 % (3783782)Time elapsed: 0.005 s
% 2.92/1.50 % (3783782)Peak memory usage: 88 MB
% 2.92/1.50 % (3783782)Instructions burned: 6 (million)
% 2.92/1.50 % (3783784)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4188770943:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 2.92/1.50 % (3783775)------------------------------
% 2.92/1.50 % (3783775)------------------------------
% 2.92/1.50 % (3783772)------------------------------
% 2.92/1.50 % (3783772)------------------------------
% 2.92/1.50 % (3783784)Instruction limit reached!
% 2.92/1.50 % (3783784)------------------------------
% 2.92/1.50 % (3783784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.50 % (3783784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.50 % (3783784)CaDiCaL version: 2.1.3
% 2.92/1.50 % (3783784)Termination reason: Instruction limit
% 2.92/1.50 % (3783784)Termination phase: Saturation
% 2.92/1.50 % (3783784)Time elapsed: 0.090 s
% 2.92/1.50 % (3783784)Peak memory usage: 88 MB
% 2.92/1.50 % (3783784)Instructions burned: 221 (million)
% 2.92/1.50 % (3783787)lrs+10_64_to=lpo:sil=8000:random_seed=559052833:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 2.92/1.50 % (3783787)First to succeed.
% 2.92/1.50 % (3783787)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3783762"
% 2.92/1.50 % (3783788)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=736688029:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 2.92/1.50 % (3783788)Refutation not found, incomplete strategy
% 2.92/1.50 % (3783788)------------------------------
% 2.92/1.50 % (3783788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.50 % (3783788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.50 % (3783788)CaDiCaL version: 2.1.3
% 2.92/1.50 % (3783788)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.50 % (3783788)Time elapsed: 0.019 s
% 2.92/1.50 % (3783788)Peak memory usage: 88 MB
% 2.92/1.50 % (3783788)Instructions burned: 25 (million)
% 2.92/1.50 % (3783789)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1365342215:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 2.92/1.50 % (3783782)------------------------------
% 2.92/1.50 % (3783782)------------------------------
% 2.92/1.50 % SZS status Satisfiable for theBenchmark
% 2.92/1.50 % SZS output start Saturation.
% See solution above
% 5.13/1.70 % SZS output start Definitions and Model Updates.
% 5.13/1.70 % SZS output end Definitions and Model Updates.
% 5.13/1.70 % (3783787)------------------------------
% 5.13/1.70 % (3783787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.13/1.70 % (3783787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.13/1.70 % (3783787)CaDiCaL version: 2.1.3
% 5.13/1.70 % (3783787)Termination reason: Satisfiable
% 5.13/1.70 % (3783787)Time elapsed: 0.021 s
% 5.13/1.70 % (3783787)Peak memory usage: 89 MB
% 5.13/1.70 % (3783787)Instructions burned: 56 (million)
% 5.13/1.70 % (3783787)------------------------------
% 5.13/1.70 % (3783787)------------------------------
% 5.13/1.70 % (3783762)Success in time 0.646 s
% 5.13/1.70 % Vampire exiting
%------------------------------------------------------------------------------